Translation validation of loop optimizations and software pipelining in the TVOC framework

In memory of Amir Pnueli

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

Abstract

Translation validation (TV) is the process of proving that the execution of a translator has generated an output that is a correct translation of the input. When applied to optimizing compilers, TV is used to prove that the generated target code is a correct translation of the source program being compiled. This is in contrast to verifying a compiler, i.e. ensuring that the compiler will generate correct target code for every possible source program - which is generally a far more difficult endeavor. This paper reviews the TVOC framework developed by Amir Pnueli and his colleagues for translation validation for optimizing compilers, where the program being compiled undergoes substantional transformation for the purposes of optimization. The paper concludes with a discussion of how recent work on the TV of software pipelining by Tristan & Leroy can be incorporated into the TVOC framework.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 17th International Symposium, SAS 2010, Proceedings
Pages6-21
Number of pages16
Volume6337 LNCS
DOIs
StatePublished - 2010
Event17th International Static Analysis Symposium, SAS 2010 - Perpignan, France
Duration: Sep 14 2010Sep 16 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6337 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other17th International Static Analysis Symposium, SAS 2010
CountryFrance
CityPerpignan
Period9/14/109/16/10

Fingerprint

Software pipelining
Optimization
Optimizing Compilers
Compiler
Target
Framework
Output

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Goldberg, B. (2010). Translation validation of loop optimizations and software pipelining in the TVOC framework: In memory of Amir Pnueli. In Static Analysis - 17th International Symposium, SAS 2010, Proceedings (Vol. 6337 LNCS, pp. 6-21). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6337 LNCS). https://doi.org/10.1007/978-3-642-15769-1_3

Translation validation of loop optimizations and software pipelining in the TVOC framework : In memory of Amir Pnueli. / Goldberg, Benjamin.

Static Analysis - 17th International Symposium, SAS 2010, Proceedings. Vol. 6337 LNCS 2010. p. 6-21 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6337 LNCS).

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

Goldberg, B 2010, Translation validation of loop optimizations and software pipelining in the TVOC framework: In memory of Amir Pnueli. in Static Analysis - 17th International Symposium, SAS 2010, Proceedings. vol. 6337 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6337 LNCS, pp. 6-21, 17th International Static Analysis Symposium, SAS 2010, Perpignan, France, 9/14/10. https://doi.org/10.1007/978-3-642-15769-1_3
Goldberg B. Translation validation of loop optimizations and software pipelining in the TVOC framework: In memory of Amir Pnueli. In Static Analysis - 17th International Symposium, SAS 2010, Proceedings. Vol. 6337 LNCS. 2010. p. 6-21. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-15769-1_3
Goldberg, Benjamin. / Translation validation of loop optimizations and software pipelining in the TVOC framework : In memory of Amir Pnueli. Static Analysis - 17th International Symposium, SAS 2010, Proceedings. Vol. 6337 LNCS 2010. pp. 6-21 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{1dd6cbc40adf44fda806eadc4d4dcf0a,
title = "Translation validation of loop optimizations and software pipelining in the TVOC framework: In memory of Amir Pnueli",
abstract = "Translation validation (TV) is the process of proving that the execution of a translator has generated an output that is a correct translation of the input. When applied to optimizing compilers, TV is used to prove that the generated target code is a correct translation of the source program being compiled. This is in contrast to verifying a compiler, i.e. ensuring that the compiler will generate correct target code for every possible source program - which is generally a far more difficult endeavor. This paper reviews the TVOC framework developed by Amir Pnueli and his colleagues for translation validation for optimizing compilers, where the program being compiled undergoes substantional transformation for the purposes of optimization. The paper concludes with a discussion of how recent work on the TV of software pipelining by Tristan & Leroy can be incorporated into the TVOC framework.",
author = "Benjamin Goldberg",
year = "2010",
doi = "10.1007/978-3-642-15769-1_3",
language = "English (US)",
isbn = "3642157688",
volume = "6337 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "6--21",
booktitle = "Static Analysis - 17th International Symposium, SAS 2010, Proceedings",

}

TY - GEN

T1 - Translation validation of loop optimizations and software pipelining in the TVOC framework

T2 - In memory of Amir Pnueli

AU - Goldberg, Benjamin

PY - 2010

Y1 - 2010

N2 - Translation validation (TV) is the process of proving that the execution of a translator has generated an output that is a correct translation of the input. When applied to optimizing compilers, TV is used to prove that the generated target code is a correct translation of the source program being compiled. This is in contrast to verifying a compiler, i.e. ensuring that the compiler will generate correct target code for every possible source program - which is generally a far more difficult endeavor. This paper reviews the TVOC framework developed by Amir Pnueli and his colleagues for translation validation for optimizing compilers, where the program being compiled undergoes substantional transformation for the purposes of optimization. The paper concludes with a discussion of how recent work on the TV of software pipelining by Tristan & Leroy can be incorporated into the TVOC framework.

AB - Translation validation (TV) is the process of proving that the execution of a translator has generated an output that is a correct translation of the input. When applied to optimizing compilers, TV is used to prove that the generated target code is a correct translation of the source program being compiled. This is in contrast to verifying a compiler, i.e. ensuring that the compiler will generate correct target code for every possible source program - which is generally a far more difficult endeavor. This paper reviews the TVOC framework developed by Amir Pnueli and his colleagues for translation validation for optimizing compilers, where the program being compiled undergoes substantional transformation for the purposes of optimization. The paper concludes with a discussion of how recent work on the TV of software pipelining by Tristan & Leroy can be incorporated into the TVOC framework.

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

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

U2 - 10.1007/978-3-642-15769-1_3

DO - 10.1007/978-3-642-15769-1_3

M3 - Conference contribution

SN - 3642157688

SN - 9783642157684

VL - 6337 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 6

EP - 21

BT - Static Analysis - 17th International Symposium, SAS 2010, Proceedings

ER -