TY - JOUR
T1 - Proving correctness of compiler optimizations by temporal logic
AU - Lacey, David
AU - Jones, Neil D.
AU - Van Wyk, Eric
AU - Frederiksen, Carl Christian
PY - 2002
Y1 - 2002
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=0036038554&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0036038554&partnerID=8YFLogxK
U2 - 10.1145/503272.503299
DO - 10.1145/503272.503299
M3 - Conference article
AN - SCOPUS:0036038554
SN - 0730-8566
SP - 283
EP - 294
JO - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
JF - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
T2 - POPL 2002: 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Y2 - 16 January 2002 through 18 January 2002
ER -