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

Ying Hu, Clark Barrett, Benjamin Goldberg

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004
EditorsJ.R. Cuellar, Z. Liu
Pages281-289
Number of pages9
StatePublished - 2004
EventProceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004 - Beijing, China
Duration: Sep 28 2004Sep 30 2004

Publication series

NameProceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004

Other

OtherProceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004
CountryChina
CityBeijing
Period9/28/049/30/04

Keywords

  • Compiler validation
  • Formal methods
  • Speculative loop optimizations
  • Translation validation

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint Dive into the research topics of 'Theory and algorithms for the generation and validation of speculative loop optimizations'. Together they form a unique fingerprint.

  • Cite this

    Hu, Y., Barrett, C., & Goldberg, B. (2004). Theory and algorithms for the generation and validation of speculative loop optimizations. In J. R. Cuellar, & Z. Liu (Eds.), Proceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004 (pp. 281-289). (Proceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004).