Ignore:
Timestamp:
Feb 6, 2013, 11:16:24 PM (6 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/itp-2013/ccexec.tex

    r2632 r2633  
    11911191the source code a non uniform cost model determined from the object code
    11921192produced. The cost model assigns a cost to each basic block of the program.
    1193 The main theorem of the labelling approach says that there is an exact
     1193The main theorem of the approach says that there is an exact
    11941194correspondence between the sequence of basic blocks started in the source
    11951195and object code, and that no instruction in the source or object code is
    1196 executed outside a basic block. Thus the overall cost of object code execution
    1197 can be computed precisely on the source code.
     1196executed outside a basic block. Thus the cost of object code execution
     1197can be computed precisely on the source.
    11981198
    11991199In this paper we scale the labelling approach to cover a programming language
     
    12261226
    12271227The short term future work consists in the completion of the certification of
    1228 the CerCo compiler. In particular, the results presented in this paper will
    1229 be used to certify all the passes of the back-end of the compiler.
     1228the CerCo compiler exploiting the main theorem of this paper.
    12301229
    12311230\paragraph{Related works}
    1232 CerCo is the first certification project which explicitly tries to induce a
     1231CerCo is the first project that explicitly tries to induce a
    12331232precise cost model on the source code in order to establish non-functional
    12341233properties of programs on an high level language. Traditional certifications
    12351234of compilers, like~\cite{compcert2,piton}, only explicitly prove preservation
    1236 of the functional properties via forward simulations.
     1235of the functional properties.
    12371236
    12381237Usually forward simulations take the following form: for each transition
Note: See TracChangeset for help on using the changeset viewer.