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

Benjamin Goldberg, Lenore Zuck, Clark Barrett

Research output: Contribution to journalArticle

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
DOIs
StatePublished - May 30 2005

Fingerprint

Optimizing Compilers
Compiler
Optimization
Reordering
Correctness
Formal Proof
Compilation
Instrumentation
Heuristics
Target
Methodology

Keywords

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

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

Into the Loops : Practical Issues in Translation Validation for Optimizing Compilers. / Goldberg, Benjamin; Zuck, Lenore; Barrett, Clark.

In: Electronic Notes in Theoretical Computer Science, Vol. 132, 30.05.2005, p. 53-71.

Research output: Contribution to journalArticle

@article{1a29136fe7514d0a9a32d1ac1be149e8,
title = "Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers",
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).",
keywords = "Distribution, Formal methods, Fusion, Loop optimizations, ORC, Translation validation",
author = "Benjamin Goldberg and Lenore Zuck and Clark Barrett",
year = "2005",
month = "5",
day = "30",
doi = "10.1016/j.entcs.2005.01.030",
language = "English (US)",
volume = "132",
pages = "53--71",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

TY - JOUR

T1 - Into the Loops

T2 - Practical Issues in Translation Validation for Optimizing Compilers

AU - Goldberg, Benjamin

AU - Zuck, Lenore

AU - Barrett, Clark

PY - 2005/5/30

Y1 - 2005/5/30

N2 - 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).

AB - 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).

KW - Distribution

KW - Formal methods

KW - Fusion

KW - Loop optimizations

KW - ORC

KW - Translation validation

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

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

U2 - 10.1016/j.entcs.2005.01.030

DO - 10.1016/j.entcs.2005.01.030

M3 - Article

AN - SCOPUS:18544363078

VL - 132

SP - 53

EP - 71

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -