Changeset 2480


Ignore:
Timestamp:
Nov 20, 2012, 6:39:20 PM (7 years ago)
Author:
mulligan
Message:

Some more changes.

File:
1 edited

Legend:

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

    r2479 r2480  
    3030Unlike previous compiler verification projects---notably Leroy's CompCert project at \textsc{inria}---CerCo is also concerned with the intensional correctness of our compiler.
    3131In 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.
     32As the CerCo compiler knows how every C expression is expanded into machine code by the compilation process, and as we have a precise cost model for machine code instructions, we can pass this cost model backwards through the compiler, back to the C source level.
    3233
     34However, the structure of machine code execution is unconstrained.
     35For example, an arbitrary machine code program is free to modify the call stack in any way that it chooses.
     36As a result, we cannot assume that the execution path of a machine code function call will return to the subsequent instruction after the call is complete.
     37This freedom presents a problem when trying to prove that the execution costs of a program are correctly predicted by our compiler.
    3338
    34 The structure of assembly program
    35 execution is unconstrained.  For example, an arbitrary assembly program is free
    36 to modify the call stack in any way that it
    37 chooses.  As a result, we cannot assume that the execution path of an assembly
    38 function call will return to the subsequent instruction after the call is
    39 complete. This freedom presents a problem when trying to prove that the
    40 execution costs of a program are correctly predicted by our compiler. Fortunately, we
    41 are able to preserve information from earlier stages of the compilation chain
    42 and use this information in the cost preservation proof.  This information is
    43 passed in the form of a \emph{structured trace}, a novel enrichment of
    44 execution traces with invariants about the structure of the program.
     39Fortunately, we are able to preserve information from earlier stages of the compilation chain and use this information in the cost preservation proof.
     40This information is passed in the form of a \emph{structured trace}, a novel enrichment of execution traces with invariants about the structure of the program.
    4541
    4642
Note: See TracChangeset for help on using the changeset viewer.