Journal article
Compiler optimization correctness by temporal logic
Higher-Order and Symbolic Computation, Vol.17(3), pp.173-206
2004
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.
Details
- Title
- Compiler optimization correctness by temporal logic
- Authors
- David Lacey (Author) - University of Warwick, United KingdomN D Jones (Author) - University of Copenhagen, DenmarkE Van Wyk (Author) - University of Minnesota, United StatesC C Frederiksen (Author) - University of Tokyo, Japan
- Publication details
- Higher-Order and Symbolic Computation, Vol.17(3), pp.173-206
- Publisher
- Springer New York LLC
- Date published
- 2004
- DOI
- 10.1023/B:LISP.0000029444.99264.c0
- ISSN
- 1388-3690
- Copyright note
- Copyright © 2004 Kluwer Academic Publishers. This article is published with open access at Springerlink.com
- Organisation Unit
- Cyber Institute; University of the Sunshine Coast, Queensland
- Language
- English
- Record Identifier
- 99450191702621
- Output Type
- Journal article
Metrics
54 File views/ downloads
481 Record Views