Sciweavers

Share
POPL
2002
ACM

Proving correctness of compiler optimizations by temporal logic

9 years 10 months ago
Proving correctness of compiler optimizations by temporal logic
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.
David Lacey, Neil D. Jones, Eric Van Wyk, Carl Chr
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2002
Where POPL
Authors David Lacey, Neil D. Jones, Eric Van Wyk, Carl Christian Frederiksen
Comments (0)
books