# Changeset 3329 for Papers/fopara2013/fopara13.tex

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

passed the spell checker

File:
1 edited

### Legend:

Unmodified
 r3328 \paragraph{Problem statement.} Computer programs can be specified with both functional constraints (what a program must do) and non-functional constraints (e.g. what resources – time, space, etc – the program may use).  In the current (e.g. what resources – time, space, etc. – the program may use).  In the current state of the art, functional properties are verified for high-level source code by combining user annotations (e.g. preconditions and invariants) with a interpretation, theorem proving, etc.). By contrast, non-functional properties are generally checked on low-level object code, but also demand information about high-level functional behavior that must somehow be recreated. about high-level functional behaviour that must somehow be recreated. This situation presents several problems: 1) it can be hard to infer this Finally, source code analysis can be made during early development stages, when components have been specified but not implemented: source code modularity means that it is enough to specify the non-functional behavior of unimplemented that it is enough to specify the non-functional behaviour of unimplemented components. how to formally prove the correctness of compilers implementing this technique. We have implemented such a compiler from C to object binaries for the 8051 microcontroller, and verified it in an interactive theorem prover. We have micro-controller, and verified it in an interactive theorem prover. We have implemented a Frama-C plugin \cite{framac} that invokes the compiler on a source program and uses this to generate invariants on the high-level source that technique in the field of cost analysis. As a case study, we show how the plugin can automatically compute and certify the exact reaction time of Lustre \cite{lustre} dataflow programs compiled into C. \cite{lustre} data flow programs compiled into C. \section{Project context and objectives} instructions are torn apart and reassembled in context-specific ways so that identifying a fragment of object code with a single high level instruction is unfeasible. Even the control flow of the object and source code can be very different as a result of optimizations, for exampe due to aggressive loop infeasible. Even the control flow of the object and source code can be very different as a result of optimizations, for example due to aggressive loop optimisations. Despite the lack of a uniform, compilation- and program-independent cost model on the source language, the literature on the % %The long term success of the project is hindered by the increased complexity of % the static prediction of the non-functional behavior of modern hardware. In the % the static prediction of the non-functional behaviour of modern hardware. In the % time frame of the European contribution we have focused on the general % methodology and on the difficulties related to the development and certification % of a cost model inducing compiler. \section{The typical CerCo workflow} \section{The typical CerCo work-flow} \begin{figure}[!t] \begin{tabular}{l@{\hspace{0.2cm}}|@{\hspace{0.2cm}}l} \label{test1} \end{figure} We illustrate the workflow we envision (on the right of \autoref{test1}) We illustrate the work-flow we envision (on the right of \autoref{test1}) on an example program (on the left of \autoref{test1}). The user writes the program and feeds it to the Cerco compiler, which outputs The user writes the program and feeds it to the CerCo compiler, which outputs an instrumented version of the same program that updates global variables that record the elapsed execution time and the stack space usage. char treshold = 4; /*@ behavior stack_cost: /*@ behaviour stack_cost: ensures __stack_max <= __max(\old(__stack_max), \old(__stack)); ensures __stack == \old(__stack); behavior time_cost: behaviour time_cost: ensures __cost <= \old(__cost)+1228; */ int main(void) added by the CerCo Frama-C plugin in blue. The \texttt{\_\_cost}, \texttt{\_\_stack} and \texttt{\_\_stack\_max} variables hold the elapsed time in clock cycles and the current and max stack usage. Their initial values hold the clock cycles spent in initializying the global data before calling in clock cycles and the current and maximum stack usage. Their initial values hold the clock cycles spent in initialising the global data before calling \texttt{main} and the space required by global data (and thus unavailable for the stack). additional instructions to update global cost information like the amount of time spent during execution or the maximal stack space required; 2) $P$ and $P'$ must have the same functional behavior, i.e.\ they must produce that same output must have the same functional behaviour, i.e.\ they must produce that same output and intermediate observables; 3) $P$ and $O$ must have the same functional behavior; 4) after execution and in interesting points during execution, the behaviour; 4) after execution and in interesting points during execution, the cost information computed by $P'$ must be an upper bound of the one spent by $O$ to perform the corresponding operations (soundness property); 5) the difference an existing compiler by adding label emission statements to every intermediate language and by propagating label emission statements during compilation. The compiler is correct if it preserves both the functional behavior of the program compiler is correct if it preserves both the functional behaviour of the program and the traces of observables. % We may also ask that the function that erases the cost % emission statements commute with compilation. This optional property grants that % the labeling does not interfere with the original compiler behavior. A further % the labeling does not interfere with the original compiler behaviour. A further % set of requirements will be added later. that contains label emission statements, like loop bodies. Therefore several loop optimizations like peeling or unrolling are prevented. Moreover, precision of the object code labeling is not sufficient per se to obtain global of the object code labeling is not sufficient \emph{per se} to obtain global precision: we also implicitly assumed the static analysis to be able to associate a precise constant cost to every instruction. This is not possible in bound on the reaction time of the system. We tested the Cost plugin and the Lustre wrapper on the C programs generated by the Lustre compiler. For programs consisting of a few hundreds loc, the Cost plugin computes a WCET and Alt − consisting of a few hundred lines of code, the Cost plugin computes a WCET and Alt- Ergo is able to discharge all VCs automatically. certification are open source. Some data structures and language definitions for the front-end are directly taken from CompCert, while the back-end is a redesign of a compiler from Pascal to MIPS used by Francois Pottier for a course at the of a compiler from Pascal to MIPS used by François Pottier for a course at the Ecole Polytechnique. CerCo compiler in the interactive theorem prover Matita and have formally certified that the cost model induced on the source code correctly and precisely predicts the object code behavior. We actually induce two cost models, one for predicts the object code behaviour. We actually induce two cost models, one for time and one for stack space used. We show the correctness of the prediction only for those programs that do not exhaust the available machine stack space, a this goal, but the cost model generated for a realistic processor could be too large and complex to be exposed in the source code. Further study is required to evaluate the tecnique on a realistic processor and to introduce early approximations of the cost model to make the tecnique feasible. to evaluate the technique on a realistic processor and to introduce early approximations of the cost model to make the technique feasible. Examples of further future work consist in improving the cost invariant