Translation and run-time validation of loop transformations

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

Research output: Contribution to journalArticle

Abstract

This paper presents new approaches to the validation of loop optimizations that compilers use to obtain the highest performance from modern architectures. Rather than verify the compiler, the approach of translation validationperforms a validation check after every run of the compiler, producing a formal proof that the produced target code is a correct implementation of the source code. As part of an active and ongoing research project on translation validation, we have previously described approaches for validating optimizations that preserve the loop structure of the code and have presented a simulation-based general technique for validating such optimizations. In this paper, for more aggressive optimizations that alter the loop structure of the code-such as distribution, fusion, tiling, and interchange-we present a set of permutation ruleswhich establish that the transformed code satisfies all the implied data dependencies necessary for the validity of the considered transformation. We describe the extensions to our tool voc-64 which are required to validate these structure-modifying optimizations. This paper also discusses preliminary work on run-time validation of speculative loop optimizations. This involves using run-time tests to ensure the correctness of loop optimizations whose correctness cannot be guaranteed at compile time. Unlike compiler validation, run-time validation must not only determine when an optimization has generated incorrect code, but also recover from the optimization without aborting the program or producing an incorrect result. This technique has been applied to several loop optimizations, including loop interchange and loop tiling, and appears to be quite promising.

Original languageEnglish (US)
Pages (from-to)335-360
Number of pages26
JournalFormal Methods in System Design
Volume27
Issue number3 SPEC. ISS.
DOIs
StatePublished - Nov 2005

Fingerprint

Loop Transformations
Optimization
Compiler
Tiling
Interchanges
Correctness
Compiler Optimization
Structure Optimization
Data Dependency
Formal Proof
Fusion
Permutation
High Performance
Verify
Fusion reactions
Target
Necessary

Keywords

  • Global optimizations
  • Loop transformations
  • Optimizing compilers
  • Reordering transformations
  • Run-time validation
  • Speculative optimizations
  • Translation validation
  • Verification conditions

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computational Theory and Mathematics

Cite this

Translation and run-time validation of loop transformations. / Zuck, Lenore; Pnueli, Amir; Goldberg, Benjamin; Barrett, Clark; Fang, Yi; Hu, Ying.

In: Formal Methods in System Design, Vol. 27, No. 3 SPEC. ISS., 11.2005, p. 335-360.

Research output: Contribution to journalArticle

Zuck, L, Pnueli, A, Goldberg, B, Barrett, C, Fang, Y & Hu, Y 2005, 'Translation and run-time validation of loop transformations', Formal Methods in System Design, vol. 27, no. 3 SPEC. ISS., pp. 335-360. https://doi.org/10.1007/s10703-005-3402-z
Zuck, Lenore ; Pnueli, Amir ; Goldberg, Benjamin ; Barrett, Clark ; Fang, Yi ; Hu, Ying. / Translation and run-time validation of loop transformations. In: Formal Methods in System Design. 2005 ; Vol. 27, No. 3 SPEC. ISS. pp. 335-360.
@article{638a1426f8cf4de3a9a52974e6307870,
title = "Translation and run-time validation of loop transformations",
abstract = "This paper presents new approaches to the validation of loop optimizations that compilers use to obtain the highest performance from modern architectures. Rather than verify the compiler, the approach of translation validationperforms a validation check after every run of the compiler, producing a formal proof that the produced target code is a correct implementation of the source code. As part of an active and ongoing research project on translation validation, we have previously described approaches for validating optimizations that preserve the loop structure of the code and have presented a simulation-based general technique for validating such optimizations. In this paper, for more aggressive optimizations that alter the loop structure of the code-such as distribution, fusion, tiling, and interchange-we present a set of permutation ruleswhich establish that the transformed code satisfies all the implied data dependencies necessary for the validity of the considered transformation. We describe the extensions to our tool voc-64 which are required to validate these structure-modifying optimizations. This paper also discusses preliminary work on run-time validation of speculative loop optimizations. This involves using run-time tests to ensure the correctness of loop optimizations whose correctness cannot be guaranteed at compile time. Unlike compiler validation, run-time validation must not only determine when an optimization has generated incorrect code, but also recover from the optimization without aborting the program or producing an incorrect result. This technique has been applied to several loop optimizations, including loop interchange and loop tiling, and appears to be quite promising.",
keywords = "Global optimizations, Loop transformations, Optimizing compilers, Reordering transformations, Run-time validation, Speculative optimizations, Translation validation, Verification conditions",
author = "Lenore Zuck and Amir Pnueli and Benjamin Goldberg and Clark Barrett and Yi Fang and Ying Hu",
year = "2005",
month = "11",
doi = "10.1007/s10703-005-3402-z",
language = "English (US)",
volume = "27",
pages = "335--360",
journal = "Formal Methods in System Design",
issn = "0925-9856",
publisher = "Springer Netherlands",
number = "3 SPEC. ISS.",

}

TY - JOUR

T1 - Translation and run-time validation of loop transformations

AU - Zuck, Lenore

AU - Pnueli, Amir

AU - Goldberg, Benjamin

AU - Barrett, Clark

AU - Fang, Yi

AU - Hu, Ying

PY - 2005/11

Y1 - 2005/11

N2 - This paper presents new approaches to the validation of loop optimizations that compilers use to obtain the highest performance from modern architectures. Rather than verify the compiler, the approach of translation validationperforms a validation check after every run of the compiler, producing a formal proof that the produced target code is a correct implementation of the source code. As part of an active and ongoing research project on translation validation, we have previously described approaches for validating optimizations that preserve the loop structure of the code and have presented a simulation-based general technique for validating such optimizations. In this paper, for more aggressive optimizations that alter the loop structure of the code-such as distribution, fusion, tiling, and interchange-we present a set of permutation ruleswhich establish that the transformed code satisfies all the implied data dependencies necessary for the validity of the considered transformation. We describe the extensions to our tool voc-64 which are required to validate these structure-modifying optimizations. This paper also discusses preliminary work on run-time validation of speculative loop optimizations. This involves using run-time tests to ensure the correctness of loop optimizations whose correctness cannot be guaranteed at compile time. Unlike compiler validation, run-time validation must not only determine when an optimization has generated incorrect code, but also recover from the optimization without aborting the program or producing an incorrect result. This technique has been applied to several loop optimizations, including loop interchange and loop tiling, and appears to be quite promising.

AB - This paper presents new approaches to the validation of loop optimizations that compilers use to obtain the highest performance from modern architectures. Rather than verify the compiler, the approach of translation validationperforms a validation check after every run of the compiler, producing a formal proof that the produced target code is a correct implementation of the source code. As part of an active and ongoing research project on translation validation, we have previously described approaches for validating optimizations that preserve the loop structure of the code and have presented a simulation-based general technique for validating such optimizations. In this paper, for more aggressive optimizations that alter the loop structure of the code-such as distribution, fusion, tiling, and interchange-we present a set of permutation ruleswhich establish that the transformed code satisfies all the implied data dependencies necessary for the validity of the considered transformation. We describe the extensions to our tool voc-64 which are required to validate these structure-modifying optimizations. This paper also discusses preliminary work on run-time validation of speculative loop optimizations. This involves using run-time tests to ensure the correctness of loop optimizations whose correctness cannot be guaranteed at compile time. Unlike compiler validation, run-time validation must not only determine when an optimization has generated incorrect code, but also recover from the optimization without aborting the program or producing an incorrect result. This technique has been applied to several loop optimizations, including loop interchange and loop tiling, and appears to be quite promising.

KW - Global optimizations

KW - Loop transformations

KW - Optimizing compilers

KW - Reordering transformations

KW - Run-time validation

KW - Speculative optimizations

KW - Translation validation

KW - Verification conditions

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

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

U2 - 10.1007/s10703-005-3402-z

DO - 10.1007/s10703-005-3402-z

M3 - Article

VL - 27

SP - 335

EP - 360

JO - Formal Methods in System Design

JF - Formal Methods in System Design

SN - 0925-9856

IS - 3 SPEC. ISS.

ER -