Changeset 3329


Ignore:
Timestamp:
Jun 6, 2013, 5:15:43 PM (4 years ago)
Author:
tranquil
Message:

passed the spell checker

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3328 r3329  
    110110\paragraph{Problem statement.} Computer programs can be specified with both
    111111functional constraints (what a program must do) and non-functional constraints
    112 (e.g. what resources – time, space, etc – the program may use).  In the current
     112(e.g. what resources – time, space, etc. – the program may use).  In the current
    113113state of the art, functional properties are verified for high-level source code
    114114by combining user annotations (e.g. preconditions and invariants) with a
     
    116116interpretation, theorem proving, etc.). By contrast, non-functional properties
    117117are generally checked on low-level object code, but also demand information
    118 about high-level functional behavior that must somehow be recreated.
     118about high-level functional behaviour that must somehow be recreated.
    119119
    120120This situation presents several problems: 1) it can be hard to infer this
     
    150150Finally, source code analysis can be made during early development stages, when
    151151components have been specified but not implemented: source code modularity means
    152 that it is enough to specify the non-functional behavior of unimplemented
     152that it is enough to specify the non-functional behaviour of unimplemented
    153153components.
    154154
     
    158158how to formally prove the correctness of compilers implementing this technique.
    159159We have implemented such a compiler from C to object binaries for the 8051
    160 microcontroller, and verified it in an interactive theorem prover. We have
     160micro-controller, and verified it in an interactive theorem prover. We have
    161161implemented a Frama-C plugin \cite{framac} that invokes the compiler on a source
    162162program and uses this to generate invariants on the high-level source that
     
    165165technique in the field of cost analysis. As a case study, we show how the
    166166plugin can automatically compute and certify the exact reaction time of Lustre
    167 \cite{lustre} dataflow programs compiled into C.
     167\cite{lustre} data flow programs compiled into C.
    168168
    169169\section{Project context and objectives}
     
    219219instructions are torn apart and reassembled in context-specific ways so that
    220220identifying a fragment of object code with a single high level instruction is
    221 unfeasible. Even the control flow of the object and source code can be very
    222 different as a result of optimizations, for exampe due to aggressive loop
     221infeasible. Even the control flow of the object and source code can be very
     222different as a result of optimizations, for example due to aggressive loop
    223223optimisations. Despite the lack of a uniform, compilation- and
    224224program-independent cost model on the source language, the literature on the
     
    337337%
    338338%The long term success of the project is hindered by the increased complexity of
    339 % the static prediction of the non-functional behavior of modern hardware. In the
     339% the static prediction of the non-functional behaviour of modern hardware. In the
    340340% time frame of the European contribution we have focused on the general
    341341% methodology and on the difficulties related to the development and certification
    342342% of a cost model inducing compiler.
    343343
    344 \section{The typical CerCo workflow}
     344\section{The typical CerCo work-flow}
    345345\begin{figure}[!t]
    346346\begin{tabular}{l@{\hspace{0.2cm}}|@{\hspace{0.2cm}}l}
     
    421421\label{test1}
    422422\end{figure}
    423 We illustrate the workflow we envision (on the right of \autoref{test1})
     423We illustrate the work-flow we envision (on the right of \autoref{test1})
    424424on an example program (on the left of \autoref{test1}).
    425 The user writes the program and feeds it to the Cerco compiler, which outputs
     425The user writes the program and feeds it to the CerCo compiler, which outputs
    426426an instrumented version of the same program that updates global variables
    427427that record the elapsed execution time and the stack space usage.
     
    458458char treshold = 4;
    459459
    460 /*@ behavior stack_cost:
     460/*@ behaviour stack_cost:
    461461      ensures __stack_max <=
    462462              __max(\old(__stack_max), \old(__stack));
    463463      ensures __stack == \old(__stack);
    464464     
    465     behavior time_cost:
     465    behaviour time_cost:
    466466      ensures __cost <= \old(__cost)+1228; */
    467467int main(void)
     
    500500 added by the CerCo Frama-C plugin in blue. The \texttt{\_\_cost},
    501501 \texttt{\_\_stack} and \texttt{\_\_stack\_max} variables hold the elapsed time
    502 in clock cycles and the current and max stack usage. Their initial values
    503 hold the clock cycles spent in initializying the global data before calling
     502in clock cycles and the current and maximum stack usage. Their initial values
     503hold the clock cycles spent in initialising the global data before calling
    504504\texttt{main} and the space required by global data (and thus unavailable for
    505505the stack).
     
    559559additional instructions to update global cost information like the amount of
    560560time spent during execution or the maximal stack space required; 2) $P$ and $P'$
    561 must have the same functional behavior, i.e.\ they must produce that same output
     561must have the same functional behaviour, i.e.\ they must produce that same output
    562562and intermediate observables; 3) $P$ and $O$ must have the same functional
    563 behavior; 4) after execution and in interesting points during execution, the
     563behaviour; 4) after execution and in interesting points during execution, the
    564564cost information computed by $P'$ must be an upper bound of the one spent by $O$
    565565to perform the corresponding operations (soundness property); 5) the difference
     
    586586an existing compiler by adding label emission statements to every intermediate
    587587language and by propagating label emission statements during compilation. The
    588 compiler is correct if it preserves both the functional behavior of the program
     588compiler is correct if it preserves both the functional behaviour of the program
    589589and the traces of observables.
    590590% We may also ask that the function that erases the cost
    591591% emission statements commute with compilation. This optional property grants that
    592 % the labeling does not interfere with the original compiler behavior. A further
     592% the labeling does not interfere with the original compiler behaviour. A further
    593593% set of requirements will be added later.
    594594
     
    640640that contains label emission statements, like loop bodies. Therefore several
    641641loop optimizations like peeling or unrolling are prevented. Moreover, precision
    642 of the object code labeling is not sufficient per se to obtain global
     642of the object code labeling is not sufficient \emph{per se} to obtain global
    643643precision: we also implicitly assumed the static analysis to be able to
    644644associate a precise constant cost to every instruction. This is not possible in
     
    804804bound on the reaction time of the system. We tested the Cost plugin and the
    805805Lustre wrapper on the C programs generated by the Lustre compiler. For programs
    806 consisting of a few hundreds loc, the Cost plugin computes a WCET and Alt −
     806consisting of a few hundred lines of code, the Cost plugin computes a WCET and Alt-
    807807Ergo is able to discharge all VCs automatically.
    808808
     
    892892certification are open source. Some data structures and language definitions for
    893893the front-end are directly taken from CompCert, while the back-end is a redesign
    894 of a compiler from Pascal to MIPS used by Francois Pottier for a course at the
     894of a compiler from Pascal to MIPS used by François Pottier for a course at the
    895895Ecole Polytechnique.
    896896
     
    924924CerCo compiler in the interactive theorem prover Matita and have formally
    925925certified that the cost model induced on the source code correctly and precisely
    926 predicts the object code behavior. We actually induce two cost models, one for
     926predicts the object code behaviour. We actually induce two cost models, one for
    927927time and one for stack space used. We show the correctness of the prediction
    928928only for those programs that do not exhaust the available machine stack space, a
     
    10171017this goal, but the cost model generated for a realistic processor could be too
    10181018large and complex to be exposed in the source code. Further study is required
    1019 to evaluate the tecnique on a realistic processor and to introduce early
    1020 approximations of the cost model to make the tecnique feasible.
     1019to evaluate the technique on a realistic processor and to introduce early
     1020approximations of the cost model to make the technique feasible.
    10211021
    10221022Examples of further future work consist in improving the cost invariant
Note: See TracChangeset for help on using the changeset viewer.