Conference paper
Proving correctness of compiler optimizations by temporal logic
Proceedings of the 29th Principles of Programming Languages Symposium, pp.283-294
Principles of Programming Languages (POPL) Symposium, 29th (Portland, United States, 16-Jan-2002–18-Jan-2002)
Association for Computer Machinery
2002
Abstract
Many classical compiler optimizations can be elegantly expressed using rewrite rules of form: I ⇒ I′ if φ, where I, I′ are intermediate language instructions and φ is a property expressed in a temporal logic suitable for describing program data flow. Its reading: If the current program π contains an instruction of form I at some control point p, and if flow condition φ is satisfied at p, then replace I by I′. 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. The meaning of correctness is that for any program π, if Rewrite(π, π′, p, I ⇒ I′ if φ) then [π] = [π′], i.e. π and π′ have exactly the same semantics.
Details
- Title
- Proving correctness of compiler optimizations by temporal logic
- Authors
- David Lacey (Author) - University of Oxford, United KingdomN D Jones (Author) - University of Copenhagen, DenmarkE Van Wyk (Author) - University of Oxford, United KingdomC C Frederiksen (Author) - University of Copenhagen, Denmark
- Publication details
- Proceedings of the 29th Principles of Programming Languages Symposium, pp.283-294
- Conference details
- Principles of Programming Languages (POPL) Symposium, 29th (Portland, United States, 16-Jan-2002–18-Jan-2002)
- Publisher
- Association for Computer Machinery
- Date published
- 2002
- DOI
- 10.1145/503272.503299
- ISBN
- 9781581134506
- Organisation Unit
- Cyber Institute; University of the Sunshine Coast, Queensland
- Language
- English
- Record Identifier
- 99449574302621
- Output Type
- Conference paper
Metrics
2 File views/ downloads
459 Record Views