Translation and run-time validation of optimized code

Lenore Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg, Ying Hu

Research output: Contribution to journalArticle

Abstract

The translation and run-time validation approaches of optimizing compilers are discussed. The translation validation approach performs a validation check after every run of the compiler, producing a formal proof that the target code is a correct implementation of the source code. A set of permutation rules is also described for more aggressive optimizations which, typically, alter the loop structure of the code, such as loop distribution and fusion, loop tiling, and lop interchanges. The run-time validation approach of speculative loop optimizations, that involves run-time tests, ensures the correctness of loop optimizations which neither the compiler nor compiler-validation techniques can guarantee the correctness.

Original languageEnglish (US)
Pages (from-to)187-208
Number of pages22
JournalElectronic Notes in Theoretical Computer Science
Volume70
Issue number4
DOIs
StatePublished - Dec 2002

Fingerprint

Compiler
Interchanges
Optimization
Correctness
Optimizing Compilers
Fusion reactions
Formal Proof
Tiling
Fusion
Permutation
Target

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

Translation and run-time validation of optimized code. / Zuck, Lenore; Pnueli, Amir; Fang, Yi; Goldberg, Benjamin; Hu, Ying.

In: Electronic Notes in Theoretical Computer Science, Vol. 70, No. 4, 12.2002, p. 187-208.

Research output: Contribution to journalArticle

@article{b91babd407044124bea8a4cb5ef8b97c,
title = "Translation and run-time validation of optimized code",
abstract = "The translation and run-time validation approaches of optimizing compilers are discussed. The translation validation approach performs a validation check after every run of the compiler, producing a formal proof that the target code is a correct implementation of the source code. A set of permutation rules is also described for more aggressive optimizations which, typically, alter the loop structure of the code, such as loop distribution and fusion, loop tiling, and lop interchanges. The run-time validation approach of speculative loop optimizations, that involves run-time tests, ensures the correctness of loop optimizations which neither the compiler nor compiler-validation techniques can guarantee the correctness.",
author = "Lenore Zuck and Amir Pnueli and Yi Fang and Benjamin Goldberg and Ying Hu",
year = "2002",
month = "12",
doi = "10.1016/S1571-0661(04)80584-X",
language = "English (US)",
volume = "70",
pages = "187--208",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "4",

}

TY - JOUR

T1 - Translation and run-time validation of optimized code

AU - Zuck, Lenore

AU - Pnueli, Amir

AU - Fang, Yi

AU - Goldberg, Benjamin

AU - Hu, Ying

PY - 2002/12

Y1 - 2002/12

N2 - The translation and run-time validation approaches of optimizing compilers are discussed. The translation validation approach performs a validation check after every run of the compiler, producing a formal proof that the target code is a correct implementation of the source code. A set of permutation rules is also described for more aggressive optimizations which, typically, alter the loop structure of the code, such as loop distribution and fusion, loop tiling, and lop interchanges. The run-time validation approach of speculative loop optimizations, that involves run-time tests, ensures the correctness of loop optimizations which neither the compiler nor compiler-validation techniques can guarantee the correctness.

AB - The translation and run-time validation approaches of optimizing compilers are discussed. The translation validation approach performs a validation check after every run of the compiler, producing a formal proof that the target code is a correct implementation of the source code. A set of permutation rules is also described for more aggressive optimizations which, typically, alter the loop structure of the code, such as loop distribution and fusion, loop tiling, and lop interchanges. The run-time validation approach of speculative loop optimizations, that involves run-time tests, ensures the correctness of loop optimizations which neither the compiler nor compiler-validation techniques can guarantee the correctness.

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

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

U2 - 10.1016/S1571-0661(04)80584-X

DO - 10.1016/S1571-0661(04)80584-X

M3 - Article

AN - SCOPUS:18544365268

VL - 70

SP - 187

EP - 208

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 4

ER -