Amir Pnueli Weizmann Institute of Science
There is a growing awareness, both in industry and academia, of the crucial role of formally proving the correctness of safety-critical portions of systems. If one is to prove that the high-level specification is correctly implemented at the lower level, one needs to verify the compiler which performs the translation. Verifying the correctness of modern optimizing compilers is challenging due to the use of complex hardware and sophisticated analysis and optimization algorithms. The introduction of new microprocessors architectures, such as the EPIC class of architectures exemplified by the IA-64, places even a heavier responsibility on optimizing compilers.
Translation validation is a novel approach that offers an alternative to the verification of translators in general and compilers in particular. According to the translation validation approach, rather than verifying the compiler itself, one constructs a validation tool which, after every compilation run, establishes that the target code produced on that run is a correct translation of the source program.
The talk will describe the formal notion of a target program being a correct translation of a source program, and the methods by which such a relation can be formally established. We begin with structure preserving optimizations which admit a well-defined mapping of control points in the target program to corresponding control points in the source program. Most high-level optimizations belong to this class. For such transformations, we apply the well known method of simulation which relates the execution between two target control points to the corresponding source execution. A more challenging class of optimizations does not guarantee such correspondence and, for this class, we present specialized approaches to which we refer as meta-rules which establish their correctness. Typical optimizations belonging to this class are loop splitting and fusion, loop tiling, and loop interchange.