Translation Validation for Optimizing Compilers
Franziska Ebert
The task of verifying a compiler formally becomes harder and harder due to the size of the compiler, its ongoing evolution and modifications. Whereas generic compiler verification has to be adapted after each compiler modification, translation validation is a novel approach that is fully independent of the compiler. Instead of verifying the compiler itself, the source program and the target program are compared after each translation. If the target program is proven to be a correct translation of the source program, the compiler was proven to be correct for this special input. In order to define a correct translation, refinement mappings are introduced which map states and variables of the target program to states and variables, respectively, of the source program.
While compiling a program, an optimizing compiler might apply several program transformations which affect the structure of the original program. Thus, establishing the refinement mapping is often not obvious. This thesis work shows how it can be proven automatically that the target program is a correct translation of the source program without instrumenting the optimizing compiler. Thereby, the focus of this thesis is set on structure-modifying transformations.
The algorithm for finding a refinement mapping searches for a transformation chain that transforms the source system into the target system. If such a transformation chain can be found, the trivial refinement mapping between the target system and the transformed source system can be established. The transformation chain together with the refinement mapping are a proof that the target program is a correct translation of the source program.
This algorithm is based on an exhaustive search using Breadth First Search (BFS), i.e. all possible transformation chains are computed and it is checked whether the target system refines one of the resulting systems. This algorithm is shown to be correct and terminating for a given (restricted) set of transformations. Furthermore, we show which properties a compiler transformation has to fulfill such that the algorithm can be extended with this transformation without loosing termination or correctness.
To reduce the search space, some optimizations for the algorithm are introduced that remove duplicated subtrees and infinite transformation chains. Also we show how metrics can be used to extend the class of transformations such that the algorithm still is terminating and correct.
Diploma Thesis.