VOC

A methodology for the translation validation of optimizing compilers

Lenore Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg

Research output: Contribution to journalArticle

Abstract

There is a growing awareness, both in industry and academia, of the crucial role of formally verifying the translation from high-level source-code into low-level object code that is typically performed by an optimizing compiler. Formally verifying an optimizing compiler, as one would verify any other large program, is not feasible due to its size, ongoing evolution and modification, and, possibly, proprietary considerations. Translation validation is a novel approach that offers an alternative to the verification of translators in general and compilers in particular: Rather than verifying the compiler itself, one constructs a validation tool which, after every run of the compiler, formally confirms that the target code produced in the run is a correct translation of the source program. The paper presents VOC, a methodology for the translation validation of optimizing compilers. We distinguish between structure, preserving optimizations, for which we establish a simulation relation between the source and target code based on computational induction, and structure modifying optimizations, for which we develop specialized "permutation rules. The paper also describes VOC-64 - a prototype translation validator tool that automatically produces verification conditions for the global optimizations of the SGI Pro-64 compiler.

Original languageEnglish (US)
Pages (from-to)223-247
Number of pages25
JournalJournal of Universal Computer Science
Volume9
Issue number3
StatePublished - 2003

Fingerprint

Optimizing Compilers
Volatile organic compounds
Compiler
Methodology
Global optimization
Structure Optimization
Target
Industry
Global Optimization
Proof by induction
Permutation
Prototype
Verify
Optimization
Alternatives
Simulation

Keywords

  • Global optimizations
  • Optimizing compilers
  • Permutation rules
  • SGI Pro-64
  • Translation validation
  • Verification conditions
  • Voc-64

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

VOC : A methodology for the translation validation of optimizing compilers. / Zuck, Lenore; Pnueli, Amir; Fang, Yi; Goldberg, Benjamin.

In: Journal of Universal Computer Science, Vol. 9, No. 3, 2003, p. 223-247.

Research output: Contribution to journalArticle

@article{766b89b1ed91417f8dda4c79606e7857,
title = "VOC: A methodology for the translation validation of optimizing compilers",
abstract = "There is a growing awareness, both in industry and academia, of the crucial role of formally verifying the translation from high-level source-code into low-level object code that is typically performed by an optimizing compiler. Formally verifying an optimizing compiler, as one would verify any other large program, is not feasible due to its size, ongoing evolution and modification, and, possibly, proprietary considerations. Translation validation is a novel approach that offers an alternative to the verification of translators in general and compilers in particular: Rather than verifying the compiler itself, one constructs a validation tool which, after every run of the compiler, formally confirms that the target code produced in the run is a correct translation of the source program. The paper presents VOC, a methodology for the translation validation of optimizing compilers. We distinguish between structure, preserving optimizations, for which we establish a simulation relation between the source and target code based on computational induction, and structure modifying optimizations, for which we develop specialized {"}permutation rules. The paper also describes VOC-64 - a prototype translation validator tool that automatically produces verification conditions for the global optimizations of the SGI Pro-64 compiler.",
keywords = "Global optimizations, Optimizing compilers, Permutation rules, SGI Pro-64, Translation validation, Verification conditions, Voc-64",
author = "Lenore Zuck and Amir Pnueli and Yi Fang and Benjamin Goldberg",
year = "2003",
language = "English (US)",
volume = "9",
pages = "223--247",
journal = "Journal of Universal Computer Science",
issn = "0948-695X",
publisher = "Springer Verlag",
number = "3",

}

TY - JOUR

T1 - VOC

T2 - A methodology for the translation validation of optimizing compilers

AU - Zuck, Lenore

AU - Pnueli, Amir

AU - Fang, Yi

AU - Goldberg, Benjamin

PY - 2003

Y1 - 2003

N2 - There is a growing awareness, both in industry and academia, of the crucial role of formally verifying the translation from high-level source-code into low-level object code that is typically performed by an optimizing compiler. Formally verifying an optimizing compiler, as one would verify any other large program, is not feasible due to its size, ongoing evolution and modification, and, possibly, proprietary considerations. Translation validation is a novel approach that offers an alternative to the verification of translators in general and compilers in particular: Rather than verifying the compiler itself, one constructs a validation tool which, after every run of the compiler, formally confirms that the target code produced in the run is a correct translation of the source program. The paper presents VOC, a methodology for the translation validation of optimizing compilers. We distinguish between structure, preserving optimizations, for which we establish a simulation relation between the source and target code based on computational induction, and structure modifying optimizations, for which we develop specialized "permutation rules. The paper also describes VOC-64 - a prototype translation validator tool that automatically produces verification conditions for the global optimizations of the SGI Pro-64 compiler.

AB - There is a growing awareness, both in industry and academia, of the crucial role of formally verifying the translation from high-level source-code into low-level object code that is typically performed by an optimizing compiler. Formally verifying an optimizing compiler, as one would verify any other large program, is not feasible due to its size, ongoing evolution and modification, and, possibly, proprietary considerations. Translation validation is a novel approach that offers an alternative to the verification of translators in general and compilers in particular: Rather than verifying the compiler itself, one constructs a validation tool which, after every run of the compiler, formally confirms that the target code produced in the run is a correct translation of the source program. The paper presents VOC, a methodology for the translation validation of optimizing compilers. We distinguish between structure, preserving optimizations, for which we establish a simulation relation between the source and target code based on computational induction, and structure modifying optimizations, for which we develop specialized "permutation rules. The paper also describes VOC-64 - a prototype translation validator tool that automatically produces verification conditions for the global optimizations of the SGI Pro-64 compiler.

KW - Global optimizations

KW - Optimizing compilers

KW - Permutation rules

KW - SGI Pro-64

KW - Translation validation

KW - Verification conditions

KW - Voc-64

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

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

M3 - Article

VL - 9

SP - 223

EP - 247

JO - Journal of Universal Computer Science

JF - Journal of Universal Computer Science

SN - 0948-695X

IS - 3

ER -