COCV'04 Preliminary Version Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers

Translation Validation is a technique for ensuring that the target code produced by a trans-lator is a correct translation of the source code. Rather than verifying the translator it-self, translation validation validates the correctness of each translation, generating a formal proof that it is indeed a correct. Recently, translation validation has been applied to prove the correctness of compilation in general, and optimizations in particular. Tvoc, a tool for the Translation Validation of Optimizing Compilers developed by the authors and their colleagues, successfully handles many optimizations employed by Intel’s ORC compiler. Tvoc, however, is somewhat limited when dealing with loop reordering transformations. First, in the theory upon which it is based, separate proof rules are needed for different categories of loop reordering transformations. Second, Tvoc has difficulties dealing with combinations of optimizations that are performed on the same block of code. Finally, Tvoc relies on information, provided by the compiler, indicating which optimiza-tions have been performed (in the case of the current ORC, this instrumentation is fortu-nately part of the compiler). This paper addresses all the issues above. It presents a uniform proof rule that encom-passes all reordering transformations performed by the Intel ORC compiler, describes a methodology for translation validation in the presence of combinations of optimizations, and presents heuristics for determining which optimizations occurred (rather than relying on the compiler for this information)