Paper Summary

The paper describes a system for verifying program transformations performed by the compiler. Usually such transformations are optimization-related, and the paper provides arguments on why optimizing compilers must be checked for correctness.

The method proposed involves proving the equivalence of the program before and after the transformations take place. Since program equivalence in general is undecidable, a less powerful equivalence is proven, using knowledge of the transformations performed by the compiler and providing a framework to express this equivalence as a simulation relation. The focus of the paper is to check compiler passes over the program, passes that are usually restricted in scope.

The program equivalence relation is defined using the simulation relation between two program.
The simulation relation for two programs S and T contains elements of the form (PC_S, PC_T, List(E)), where PC_X is a program point in program X, and List(E) is a list of expressions relating variables from S and T at the given program points.
A simulation relation is said to be correct if for each element in the relation, all pairs of executions of S and T starting at the corresponding program points (given by the simulation relation element) are equivalent.
A pair of executions is equivalent if both lead to the same sequence of function calls and returns.

The paper further restricts the simulation relation:

• the expressions in a simulation relation element can only be equalities;
• only intraprocedural relations are considered;
• branches in the target program must correspond to branches in the source program.

An inference algorithm that can infer the simulation relation from the compilation process (I suppose they meant from consecutive versions of the program) is described. This inference algorithm imposes the above restrictions on the simulation relation.

The algorithm for checking the simulation relation uses symbolically evaluated versions of the program. One interesting note: they compare the symbolic evaluation process used to rewriting the function as a purely functional program composed of mutually recursive functions (each basic block becomes a side-effect-free function).

The Translation Validation Infrastructure described in the paper is going to be useful in proving the correctness of program transformation tools - that is to say, when the nature of the transformation is somewhat known (maybe it is localized or otherwise easy to separate from the original program).