TY - GEN

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

AU - Hu, Ying

AU - Barrett, Clark

AU - Goldberg, Benjamin

PY - 2004/12/1

Y1 - 2004/12/1

N2 - 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 runtime tests necessary to support speculative optimizations.

AB - 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 runtime tests necessary to support speculative optimizations.

KW - Compiler validation

KW - Formal methods

KW - Speculative loop optimizations

KW - Translation validation

UR - http://www.scopus.com/inward/record.url?scp=16244387365&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=16244387365&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:16244387365

SN - 076952222X

SN - 9780769522227

T3 - Proceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004

SP - 281

EP - 289

BT - Proceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004

A2 - Cuellar, J.R.

A2 - Liu, Z.

T2 - Proceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004

Y2 - 28 September 2004 through 30 September 2004

ER -