Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers

Benjamin Goldberg, Lenore Zuck, Clark Barrett

Research output: Contribution to journalConference article

Abstract

Translation Validation is a technique for ensuring that the target code produced by a translator is a correct translation of the source code. Rather than verifying the translator itself, 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 optimizations have been performed (in the case of the current ORC, this instrumentation is fortunately part of the compiler). This paper addresses all the issues above. It presents a uniform proof rule that encompasses 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).

Original languageEnglish (US)
Pages (from-to)53-71
Number of pages19
JournalElectronic Notes in Theoretical Computer Science
Volume132
Issue number1
DOIs
StatePublished - May 30 2005
EventProceedings pf the 3rd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2004) -
Duration: Apr 3 2004Apr 3 2005

Keywords

  • Distribution
  • Formal methods
  • Fusion
  • Loop optimizations
  • ORC
  • Translation validation

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers'. Together they form a unique fingerprint.

  • Cite this