Translation validation is a technique that verifies the results of
every run of a translator, such as a compiler, instead of the translator
itself. Previous papers by the authors and others have described
translation validation for compilers that perform loop optimizations
(such as interchange, tiling, fusion, etc), using a proof rule that
treats loop optimizations 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 improves the validation process for
compile-time optimizations, it can also be used to ensure the
correctness of speculative loop optimizations, the aggressive
optimizations which are only correct under certain conditions that
cannot be known at compile time. Based on the new permutation rule,
with the help of an automatic theorem prover, CVC Lite, an algorithm
is proposed for validating loop optimizations. 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.