Theory and algorithms for the generation and validation of speculative loop optimizations

Translation validation is a technique that verifies the re-sults of every run of a translator, such as a compiler, in-stead of the translator itself. Previous papers by the authors and others have described translation validation for com-pilers that perform loop optimizations (such as interchange, tiling, fusion, etc), using a proof rule that treats loop opti-mizations as permutations. In this paper, we describe an improved permutation proof rule which considers the initial conditions and invariant conditions of the loop. This new proof rule not only im-proves the validation process for compile-time optimiza-tions, it can also be used to ensure the correctness of speculative loop optimizations, the aggressive optimizations which are only correct under certain conditions that can-not be known at compile time. Based on the new permu-tation rule, with the help of an automatic theorem prover, CVC Lite, an algorithm is proposed for validating loop op-timizations. The same permutation proof rule can also be used (within a compiler, for example) to generate the run-time tests necessary to support speculative optimizations. Key words: Compiler validation, speculative loop optimizations, translation validation, for-mal methods. 1