Between Dec 19, 2024 and Jan 2, 2025, datasets can be submitted to DRUM but will not be processed until after the break. Staff will not be available to answer email during this period, and will not be able to provide DOIs until after Jan 2. If you are in need of a DOI during this period, consider Dryad or OpenICPSR. Submission responses to the UDC may also be delayed during this time.

Browsing by Author "Lacey, David"

Now showing 1 - 2 of 2
  • Thumbnail Image
    Item
    Compiler Optimization Correctness by Temporal Logic
    (2004) Lacey, David; D. Jones, Neil; Van Wyk, Eric; Christian Frederiksen, Carl
    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 transformation-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.
  • Thumbnail Image
    Item
    Proving Correctness of Compiler Optimizations by Temporal Logic
    (2002) Lacey, David; D. Jones, Neil; Van Wyk, Eric; Christian Frederiksen, Carl
    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' φ ) then [[ π ]] ≡ [[ π' ]], i.e. π and π' have exactly the same semantics.