Proving correctness of compiler optimizations by temporal logic

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

Research output: Contribution to journalConference article

52 Scopus citations

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.

Original languageEnglish (US)
Pages (from-to)283-294
Number of pages12
JournalConference Record of the Annual ACM Symposium on Principles of Programming Languages
DOIs
StatePublished - Jan 1 2002
EventPOPL 2002: 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Portland, OR, United States
Duration: Jan 16 2002Jan 18 2002

Fingerprint Dive into the research topics of 'Proving correctness of compiler optimizations by temporal logic'. Together they form a unique fingerprint.

  • Cite this