ganler / ResearchReading

General system research material (not limited to paper) reading notes.
GNU General Public License v3.0
20 stars 1 forks source link

PLDI'14 | Compiler Validation via Equivalence Modulo Inputs #69

Closed ganler closed 2 years ago

ganler commented 2 years ago

Distinguished paper!

PDF: https://www.vuminhle.com/pdf/pldi14-emi.pdf Slides: https://people.inf.ethz.ch/suz/publications/emi-talk.pdf 3rd-party blog review: https://www.cs.cornell.edu/courses/cs6120/2019fa/blog/equivalence-modulo-inputs/

Key idea: EMI = Equivalence Modulo Inputs

Metamorphic testing: Generating equivalent (you define it) inputs and expecting the same output results from them.

Ideally, it is good to have semantically equivalent programs. i.e., \forall i \in I, P_a(i) == P_b(i). But that's a bit hard for a general-purpose programming language. Okay, to make things easier, you can relax the constraint: "\forall i \in I" to "\forall i \in I'" where I' is a limited set of inputs. If the programs are equivalent on a limited set of inputs, we call it EMI. i.e., Q is an EMI-variant of P on input set I iff \forall i \in I, P(i) = Q(i);

Then how can we easily get equivalent programs on a limited set of inputs? Okay, that's where things get interesting. Say we have input x and original program P. We first collect the path of P(x) so that we know where the "dead" code is (statements that are not executed). We then mutate (i.e., erase) the “dead" code to get Q. Very simple but working!!!