Ignore:
Timestamp:
Feb 17, 2014, 12:09:32 PM (6 years ago)
Author:
mulligan
Message:

More changes, including more missing references (including to CerCo?'s site with deliverables and papers) added. Finished up to Section 4.3.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3442 r3443  
    505505char a[4] = {3, 2, 7, 14};  char threshold = 4;
    506506
    507 /*@ behavior stack_cost:
     507/*@ behaviour stack_cost:
    508508      ensures __stack_max <= __max(\old(__stack_max), 4+\old(__stack));
    509509      ensures __stack == \old(__stack);
    510     behavior time_cost:
     510    behaviour time_cost:
    511511      ensures __cost <= \old(__cost)+(178+214*__max(1+\at(len,Pre), 0));
    512512*/
     
    534534}
    535535
    536 /*@ behavior stack_cost:
     536/*@ behaviour stack_cost:
    537537      ensures __stack_max <= __max(\old(__stack_max), 6+\old(__stack));
    538538      ensures __stack == \old(__stack);
    539     behavior time_cost:
     539    behaviour time_cost:
    540540      ensures __cost <= \old(__cost)+1358;
    541541*/
     
    609609\subsection{The (basic) labelling approach}
    610610The labelling approach is the foundational insight that underlies all the developments in CerCo.
    611 It allows the tracking of the evolution of
    612 basic blocks during the compilation process in order to propagate the cost model from the
     611It facilitates the tracking of basic block evolution during the compilation process in order to propagate the cost model from the
    613612object code to the source code without losing precision in the process.
    614613\paragraph{Problem statement.} Given a source program $P$, we want to obtain an
     
    704703way to achieve that is to impose correctness and precision
    705704requirements on the source code labelling produced at the start, and
    706 to demand that the compiler to preserve these
     705to demand that the compiler preserves these
    707706properties too. The latter requirement imposes serious limitations on the
    708 compilation strategy and optimizations: the compiler may not duplicate any code
    709 that contains label emission statements, like loop bodies. Therefore several
     707compilation strategy and optimisations: the compiler may not duplicate any code
     708that contains label emission statements, like loop bodies. Therefore various
    710709loop optimisations like peeling or unrolling are prevented. Moreover, precision
    711710of the object code labelling is not sufficient \emph{per se} to obtain global
     
    720719`while' language, all remaining compilers target realistic source
    721720languages---a pure higher order functional language and a large subset
    722 of C with pointers, gotos and all data structures---and real world
     721of C with pointers, \texttt{goto}s and all data structures---and real world
    723722target processors---MIPS and the Intel 8051/8052 processor
    724723family. Moreover, they achieve a level of optimisation that ranges
     
    765764the C language and the 8051/8052 family, and does not yet implement any
    766765advanced optimisations. Its user interface, however, is the same as the
    767 other version for interoperability. In
     766other version for interoperability purposes. In
    768767particular, the Frama-C CerCo plugin descibed in
    769768Section~\ref{sec:exploit} can work without recompilation
     
    777776The (trusted) CerCo compiler implements the following optimisations: cast
    778777simplification, constant propagation in expressions, liveness analysis driven
    779 spilling of registers, dead code elimination, branch displacement, and tunneling.
     778spilling of registers, dead code elimination, branch displacement, and tunnelling.
    780779The two latter optimisations are performed by our optimising assembler
    781780\cite{correctness}. The back-end of the compiler works on three address
     
    789788the front-end are directly taken from CompCert, while the back-end is a redesign
    790789of a compiler from Pascal to MIPS used by Fran\c{c}ois Pottier for a course at the
    791 Ecole Polytechnique.
     790\'{E}cole Polytechnique.
    792791
    793792The main differences in the CerCo compiler are:
     
    830829functional correctness for most passes. In order to complete the
    831830proof for non-functional properties, we have introduced a new,
    832 structured, form of execution traces, with the
     831structured, form of execution trace, with the
    833832related notions for forward similarity and the intensional
    834833consequences of forward similarity. We have also introduced a unified
     
    838837The details on the proof techniques employed
    839838and
    840 the proof sketch can be found in the CerCo deliverables and papers.
     839the proof sketch can be found in the CerCo deliverables and papers~\cite{cerco-deliverables}.
    841840In this section we will only hint at the correctness statement, which turned
    842841out to be more complex than expected.
     
    11181117
    11191118Other examples of future work are to improve the cost invariant
    1120 generator algorithms and the coverage of compiler optimizations, to combining
     1119generator algorithms and the coverage of compiler optimisations, to combining
    11211120the labelling approach with the type and effect discipline of~\cite{typeffects}
    11221121to handle languages with implicit memory management, and to experiment with
Note: See TracChangeset for help on using the changeset viewer.