Changeset 2479


Ignore:
Timestamp:
Nov 20, 2012, 5:12:30 PM (7 years ago)
Author:
mulligan
Message:

A small amount of rewriting as i didn't like the original introduction that we developed in Edinburgh.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/structured-traces-2012/structured-traces.tex

    r2455 r2479  
    2222\label{sect.introduction}
    2323
    24 Compiler correctness proofs are typically based on simulation results for local
    25 portions of code.  This is because compiler formalisation efforts have focussed
    26 their attention on providing guarantees about the extensional behaviour of
    27 generated code.  In contrast, we have found that invariants about the
    28 structure of program execution are valuable when the compiler also provides
    29 guarantees about intensional properties of generated code, such as execution
    30 time.
     24Compiler correctness proofs are typically based on simulation results for local portions of code.
     25This is because compiler formalisation efforts have focused their attention on providing guarantees about the extensional behaviour of generated code.
     26In contrast, when verified compiler projects also consider the intensional behaviour of generated code such as execution time or space, we have found that invariants about the structure of program execution are particularly valuable.
    3127
    32 Our compiler produces assembly code as output.   The structure of assembly program
     28The ideas summaried in this paper have been developed within the context of the CerCo (`Certified Complexity') project, though by no means are limited in their scope or application to this project.
     29CerCo's ultimate aim is to produce a verified C compiler for a large subset of the C programming language.
     30Unlike previous compiler verification projects---notably Leroy's CompCert project at \textsc{inria}---CerCo is also concerned with the intensional correctness of our compiler.
     31In particular, the CerCo C compiler will lift, in a provably correct way, a cost model induced by the compilation process back to the C-source level.
     32
     33
     34The structure of assembly program
    3335execution is unconstrained.  For example, an arbitrary assembly program is free
    3436to modify the call stack in any way that it
Note: See TracChangeset for help on using the changeset viewer.