Compiler optimization correctness by temporal logic

David Lacey, Neil D. Jones, Eric Van Wyk, Carl Christian Frederiksen

Research output: Contribution to journalArticlepeer-review

25 Scopus citations

Abstract

Rewrite rules with side conditions can elegantly express many classical compiler optimizations for imperative programming languages. In this paper, programs are written in an intermediate language and transform ation-enabling side conditions are specified in a temporal logic suitable for describing program data flow. The purpose of this paper is to show how such transformations may be proven correct. Our methodology is illustrated by Three familiar optimizations: dead code elimination, constant folding, and code motion. A transformation is correct if whenever it can be applied to a program, the original and transformed programs are semantically equivalent, i.e., they compute the same input-output function. The proofs of semantic equivalence inductively show that a transformation-specific bisimulation relation holds between the original and transformed program computations.

Original languageEnglish (US)
Pages (from-to)173-206
Number of pages34
JournalHigher-Order and Symbolic Computation
Volume17
Issue number3
DOIs
StatePublished - Sep 2004

Bibliographical note

Funding Information:
∗This research was partially supported by the Danish Natural Science Research Council (PLT project), the EEC (Daedalus project) and Microsoft Research.

Keywords

  • Compiler verification
  • Model checking
  • Optimizing compilers
  • Temporal logic

Fingerprint Dive into the research topics of 'Compiler optimization correctness by temporal logic'. Together they form a unique fingerprint.

Cite this