Theory and algorithms for the generation and validation of speculative loop optimizations

Ying Hu, Clark Barrett, Benjamin Goldberg

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

Abstract

Translation validation is a technique that verifies the results of every run of a translator, such as a compiler, instead of the translator itself. Previous papers by the authors and others have described translation validation for compilers that perform loop optimizations (such as interchange, tiling, fusion, etc), using a proof rule that treats loop optimizations as permutations. In this paper, we describe an improved permutation proof rule which considers the initial conditions and invariant conditions of the loop. This new proof rule not only improves the validation process for compile-time optimizations, it can also be used to ensure the correctness of speculative loop optimizations, the aggressive optimizations which are only correct under certain conditions that cannot be known at compile time. Based on the new permutation rule, with the help of an automatic theorem prover, CVC Lite, an algorithm is proposed for validating loop optimizations. The same permutation proof rule can also be used (within a compiler, for example) to generate the runtime tests necessary to support speculative optimizations.

Original languageEnglish (US)
Title of host publicationProceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004
EditorsJ.R. Cuellar, Z. Liu
Pages281-289
Number of pages9
StatePublished - 2004
EventProceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004 - Beijing, China
Duration: Sep 28 2004Sep 30 2004

Other

OtherProceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004
CountryChina
CityBeijing
Period9/28/049/30/04

Fingerprint

Interchanges
Fusion reactions

Keywords

  • Compiler validation
  • Formal methods
  • Speculative loop optimizations
  • Translation validation

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Hu, Y., Barrett, C., & Goldberg, B. (2004). Theory and algorithms for the generation and validation of speculative loop optimizations. In J. R. Cuellar, & Z. Liu (Eds.), Proceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004 (pp. 281-289)

Theory and algorithms for the generation and validation of speculative loop optimizations. / Hu, Ying; Barrett, Clark; Goldberg, Benjamin.

Proceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004. ed. / J.R. Cuellar; Z. Liu. 2004. p. 281-289.

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

Hu, Y, Barrett, C & Goldberg, B 2004, Theory and algorithms for the generation and validation of speculative loop optimizations. in JR Cuellar & Z Liu (eds), Proceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004. pp. 281-289, Proceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004, Beijing, China, 9/28/04.
Hu Y, Barrett C, Goldberg B. Theory and algorithms for the generation and validation of speculative loop optimizations. In Cuellar JR, Liu Z, editors, Proceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004. 2004. p. 281-289
Hu, Ying ; Barrett, Clark ; Goldberg, Benjamin. / Theory and algorithms for the generation and validation of speculative loop optimizations. Proceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004. editor / J.R. Cuellar ; Z. Liu. 2004. pp. 281-289
@inproceedings{cafd48985f4f4c12baaee0c70b7b5c1c,
title = "Theory and algorithms for the generation and validation of speculative loop optimizations",
abstract = "Translation validation is a technique that verifies the results of every run of a translator, such as a compiler, instead of the translator itself. Previous papers by the authors and others have described translation validation for compilers that perform loop optimizations (such as interchange, tiling, fusion, etc), using a proof rule that treats loop optimizations as permutations. In this paper, we describe an improved permutation proof rule which considers the initial conditions and invariant conditions of the loop. This new proof rule not only improves the validation process for compile-time optimizations, it can also be used to ensure the correctness of speculative loop optimizations, the aggressive optimizations which are only correct under certain conditions that cannot be known at compile time. Based on the new permutation rule, with the help of an automatic theorem prover, CVC Lite, an algorithm is proposed for validating loop optimizations. The same permutation proof rule can also be used (within a compiler, for example) to generate the runtime tests necessary to support speculative optimizations.",
keywords = "Compiler validation, Formal methods, Speculative loop optimizations, Translation validation",
author = "Ying Hu and Clark Barrett and Benjamin Goldberg",
year = "2004",
language = "English (US)",
isbn = "076952222X",
pages = "281--289",
editor = "J.R. Cuellar and Z. Liu",
booktitle = "Proceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004",

}

TY - GEN

T1 - Theory and algorithms for the generation and validation of speculative loop optimizations

AU - Hu, Ying

AU - Barrett, Clark

AU - Goldberg, Benjamin

PY - 2004

Y1 - 2004

N2 - Translation validation is a technique that verifies the results of every run of a translator, such as a compiler, instead of the translator itself. Previous papers by the authors and others have described translation validation for compilers that perform loop optimizations (such as interchange, tiling, fusion, etc), using a proof rule that treats loop optimizations as permutations. In this paper, we describe an improved permutation proof rule which considers the initial conditions and invariant conditions of the loop. This new proof rule not only improves the validation process for compile-time optimizations, it can also be used to ensure the correctness of speculative loop optimizations, the aggressive optimizations which are only correct under certain conditions that cannot be known at compile time. Based on the new permutation rule, with the help of an automatic theorem prover, CVC Lite, an algorithm is proposed for validating loop optimizations. The same permutation proof rule can also be used (within a compiler, for example) to generate the runtime tests necessary to support speculative optimizations.

AB - Translation validation is a technique that verifies the results of every run of a translator, such as a compiler, instead of the translator itself. Previous papers by the authors and others have described translation validation for compilers that perform loop optimizations (such as interchange, tiling, fusion, etc), using a proof rule that treats loop optimizations as permutations. In this paper, we describe an improved permutation proof rule which considers the initial conditions and invariant conditions of the loop. This new proof rule not only improves the validation process for compile-time optimizations, it can also be used to ensure the correctness of speculative loop optimizations, the aggressive optimizations which are only correct under certain conditions that cannot be known at compile time. Based on the new permutation rule, with the help of an automatic theorem prover, CVC Lite, an algorithm is proposed for validating loop optimizations. The same permutation proof rule can also be used (within a compiler, for example) to generate the runtime tests necessary to support speculative optimizations.

KW - Compiler validation

KW - Formal methods

KW - Speculative loop optimizations

KW - Translation validation

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

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

M3 - Conference contribution

SN - 076952222X

SN - 9780769522227

SP - 281

EP - 289

BT - Proceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004

A2 - Cuellar, J.R.

A2 - Liu, Z.

ER -