Changeset 2451 for Papers


Ignore:
Timestamp:
Nov 10, 2012, 5:31:22 PM (6 years ago)
Author:
mulligan
Message:

Structured traces paper for Brian as per e-mail conversation yesterday.

File:
1 edited

Legend:

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

    r2331 r2451  
    2222\label{sect.introduction}
    2323
     24Compiler correctness proofs are typically based on simulation results for local
     25portions of code.  This is because compiler formalisation efforts have focussed
     26their attention on providing guarantees about the extensional behaviour of
     27generated code.  In contrast, we have found that invariants about the
     28structure of program execution are valuable when the compiler also provides
     29guarantees about intensional properties of generated code, such as execution
     30time.
     31
     32Our compiler produces assembly code as output.   The structure of assembly program
     33execution is unconstrained.  For example, an arbitrary assembly program is free
     34to modify the call stack in any way that it
     35chooses.  As a result, we cannot assume that the execution path of an assembly
     36function call will return to the subsequent instruction after the call is
     37complete. This freedom presents a problem when trying to prove that the
     38execution costs of a program are correctly predicted by our compiler. Fortunately, we
     39are able to preserve information from earlier stages of the compilation chain
     40and use this information in the cost preservation proof.  This information is
     41passed in the form of a \emph{structured trace}, a novel enrichment of
     42execution traces with invariants about the structure of the program.
     43
     44
     45
    2446%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
    2547% Section.                                                                    %
Note: See TracChangeset for help on using the changeset viewer.