Changeset 3337


Ignore:
Timestamp:
Jun 7, 2013, 3:12:26 PM (4 years ago)
Author:
mulligan
Message:

Final changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3336 r3337  
    768768Frama-C \cite{framac} is a set of analysers for C programs with a
    769769specification language called ACSL. New analyses can be dynamically added
    770 through a plugin system. For instance, the Jessie plugin allows deductive
     770via a plugin system. For instance, the Jessie plugin allows deductive
    771771verification of C programs with respect to their specification in ACSL, with
    772772various provers as back-end tools.
     
    784784Lustre compiler.
    785785
    786 \paragraph{Soundness.} The soundness of the whole framework depends on the cost
     786\paragraph{Soundness} The soundness of the whole framework depends on the cost
    787787annotations added by the CerCo compiler, the synthetic costs produced by the
    788 Cost plugin, the verification conditions (VCs) generated by Jessie, and the
     788cost plugin, the verification conditions (VCs) generated by Jessie, and the
    789789external provers discharging the VCs. The synthetic costs being in ACSL format,
    790790Jessie can be used to verify them. Thus, even if the added synthetic costs are
     
    792792correct: indeed, Jessie will not validate incorrect costs and no conclusion can
    793793be made about the WCET of the program in this case. In other terms, the
    794 soundness does not really depend on the action of the Cost plugin, which can in
     794soundness does not really depend on the action of the cost plugin, which can in
    795795principle produce any synthetic cost. However, in order to be able to actually
    796796prove a WCET of a C function, we need to add correct annotations in a way that
     
    799799composed of branching and assignments (no loops and no recursion) because a fine
    800800analysis of the VCs associated with branching may lead to a complexity blow up.
    801 \paragraph{Experience with Lustre.} Lustre is a data-flow language to program
    802 synchronous systems and the language comes with a compiler to C. We designed a
     801\paragraph{Experience with Lustre} Lustre is a data-flow language for programming
     802synchronous systems, with the language coming with a compiler to C. We designed a
    803803wrapper for supporting Lustre files.
    804804The C function produced by the compiler implements the step function of the
     
    806806bound on the reaction time of the system. We tested the Cost plugin and the
    807807Lustre wrapper on the C programs generated by the Lustre compiler. For programs
    808 consisting of a few hundred lines of code, the Cost plugin computes a WCET and Alt-
     808consisting of a few hundred lines of code, the cost plugin computes a WCET and Alt-
    809809Ergo is able to discharge all VCs automatically.
    810810
    811 \paragraph{Handling C programs with simple loops.}
     811\paragraph{Handling C programs with simple loops}
    812812The cost annotations added by the CerCo compiler take the form of C instructions
    813813that update by a constant a fresh global variable called the cost variable.
     
    818818through during the flow of execution. In order to do the analysis the plugin
    819819makes the following assumptions on the programs:
    820 1. No recursive functions.
    821 2. Every loop must be annotated with a variant. The variants of ‘for’ loops are
     8201) there are no recursive functions;
     8212) every loop must be annotated with a variant. The variants of `for' loops are
    822822automatically inferred.
    823823
     
    838838loop. An axiom is added to account the fact that the cost is accumulated at each
    839839step of the loop.
    840 The cost of the function is directly added as post-condition of the function
    841 
    842 The user can influence the annotation by different means:
    843 by using more precise variants or
    844 by annotating function with cost specification. The plugin will use this cost
     840The cost of the function is directly added as post-condition of the function.
     841
     842The user can influence the annotation by two different means:
     8431) by using more precise variants;
     8442) by annotating functions with cost specifications. The plugin will use this cost
    845845for the function instead of computing it.
    846 \paragraph{C programs with pointers.}
     846\paragraph{C programs with pointers}
    847847When it comes to verifying programs involving pointer-based data structures,
    848848such as linked lists, trees, or graphs, the use of traditional first-order logic
    849849to specify, and of SMT solvers to verify, shows some limitations. Separation
    850 logic \cite{separation} is then an elegant alternative. It is a program logic
     850logic~\cite{separation} is an elegant alternative. It is a program logic
    851851with a new notion of conjunction to express spatial heap separation. Bobot has
    852 recently introduced in the Jessie plugin automatically generated separation
    853 predicates to simulate separation logic reasoning in a traditional verification
    854 framework where the specification language, the verification condition
     852recently introduced automatically generated separation
     853predicates to simulate separation logic reasoning in the Jessie plugin where the specification language, the verification condition
    855854generator, and the theorem provers were not designed with separation logic in
    856855mind. CerCo's plugin can exploit the separation predicates to automatically
     
    858857in-place list reversal.
    859858
    860 \subsection{The CerCo Compiler}
     859\subsection{The CerCo compiler}
    861860In CerCo we have developed a certain number of cost preserving compilers based
    862 on the labeling approach. Excluding an initial certified compiler for a While
     861on the labeling approach. Excluding an initial certified compiler for a `while'
    863862language, all remaining compilers target realistic source languages---a pure
    864863higher order functional language and a large subset of C with pointers, gotos
    865864and all data structures---and real world target processors---MIPS and the
    866 Intel 8051/8052 processor family. Moreover, they achieve a level of optimization
    867 that ranges from moderate (comparable to gcc level 1) to intermediate (including
     865Intel 8051/8052 processor family. Moreover, they achieve a level of optimisation
     866that ranges from moderate (comparable to GCC level 1) to intermediate (including
    868867loop peeling and unrolling, hoisting and late constant propagation). The so
    869 called Trusted CerCo Compiler is the only one that was implemented in the
     868called \emph{Trusted CerCo Compiler} is the only one that was implemented in the
    870869interactive theorem prover Matita~\cite{matita} and its costs certified. The code distributed
    871 is obtained extracting OCaml code from the Matita implementation. In the rest of
     870is extracted OCaml code from the Matita implementation. In the rest of
    872871this section we will only focus on the Trusted CerCo Compiler, that only targets
    873 the C language and the 8051/8052 family, and that does not implement the
    874 advanced optimizations yet. Its user interface, however, is the same as the one
     872the C language and the 8051/8052 family, and that does not implement any
     873advanced optimisations yet. Its user interface, however, is the same as the one
    875874of the other versions, in order to trade safety with additional performances. In
    876875particular, the Frama-C CerCo plugin can work without recompilation with all
     
    882881that may require approximations or dependent costs.
    883882
    884 The (trusted) CerCo compiler implements the following optimizations: cast
     883The (trusted) CerCo compiler implements the following optimisations: cast
    885884simplification, constant propagation in expressions, liveness analysis driven
    886 spilling of registers, dead code elimination, branch displacement, tunneling.
    887 The two latter optimizations are performed by our optimizing assembler
    888 \cite{correctness}. The back-end of the compiler works on three addresses
     885spilling of registers, dead code elimination, branch displacement, and tunneling.
     886The two latter optimisations are performed by our optimising assembler
     887\cite{correctness}. The back-end of the compiler works on three address
    889888instructions, preferred to static single assignment code for the simplicity of
    890889the formal certification.
     
    892891The CerCo compiler is loosely based on the CompCert compiler \cite{compcert}, a
    893892recently developed certified compiler from C to the PowerPC, ARM and x86
    894 microprocessors. Contrarily to CompCert, both the CerCo code and its
     893microprocessors. Contrary to CompCert, both the CerCo code and its
    895894certification are open source. Some data structures and language definitions for
    896895the front-end are directly taken from CompCert, while the back-end is a redesign
    897 of a compiler from Pascal to MIPS used by François Pottier for a course at the
     896of a compiler from Pascal to MIPS used by Fran\c{c}ois Pottier for a course at the
    898897Ecole Polytechnique.
    899898
     
    901900\begin{enumerate}
    902901\item all of our intermediate languages include label emitting instructions to
    903 implement the labeling approach, and the compiler preserves execution traces.
     902implement the labeling approach, and the compiler preserves execution traces,
    904903\item traditionally compilers target an assembly language with additional
    905904macro-instructions to be expanded before assembly; for CerCo we need to go all
    906905the way down to object code in order to perform the static analysis. Therefore
    907 we integrated also an optimizing assembler and a static analyser.
     906we integrated also an optimising assembler and a static analyser,
    908907\item to avoid implementing a linker and a loader, we do not support separate
    909908compilation and external calls. Adding a linker and a loader is a transparent
    910 process to the labeling approach and should create no unknown problem.
    911 \item we target an 8-bit processor. Targeting an 8 bit processor requires
     909process to the labeling approach and should create no unknown problem,
     910\item we target an 8-bit processor. Targeting an 8-bit processor requires
    912911several changes and increased code size, but it is not fundamentally more
    913 complex. The proof of correctness, however, becomes much harder.
     912complex. The proof of correctness, however, becomes much harder,
    914913\item we target a microprocessor that has a non uniform memory model, which is
    915914still often the case for microprocessors used in embedded systems and that is
     
    923922\end{enumerate}
    924923
    925 \subsection{A formal certification of the CerCo compiler}
     924\subsection{Formal certification of the CerCo compiler}
    926925We implemented the
    927926CerCo compiler in the interactive theorem prover Matita and have formally
    928927certified that the cost model induced on the source code correctly and precisely
    929928predicts the object code behaviour. We actually induce two cost models, one for
    930 time and one for stack space used. We show the correctness of the prediction
     929time and one for stack space consumption. We show the correctness of the prediction
    931930only for those programs that do not exhaust the available machine stack space, a
    932 property that thanks to the stack cost model we can statically analyse on the
     931property that---thanks to the stack cost model---we can statically analyse on the
    933932source code using our Frama-C tool. The preservation of functional properties we
    934933take as an assumption, not itself formally proved in CerCo.  Other projects have
     
    948947out to be more complex than what we expected at the beginning.
    949948
    950 \paragraph{The statement.}
     949\paragraph{The statement}
    951950Real time programs are often reactive programs that loop forever responding to
    952951events (inputs) by performing some computation followed by some action (output)
     
    978977space is a clear requirement of meaningfulness of a run, because source programs
    979978do not crash for lack of space while object code ones do. The balancing of
    980 function calls/returns is a requirement for precision: the labeling approach
     979function calls and returns is a requirement for precision: the labeling approach
    981980allows the scope of label emission statements to extend after function calls to
    982981minimize the number of labels. Therefore a label pays for all the instructions
     
    988987safe bound, not that it is exact. The last condition on the entry/exit points of
    989988a run is used to identify sub-runs whose code correspond to a sequence of blocks
    990 that we can measure precisely. Any other choice would start/end the run in the
     989that we can measure precisely. Any other choice would start or end the run in the
    991990middle of a block and we would be forced again to weaken the statement taking as
    992991a bound the cost obtained counting in all the instructions that precede the
    993 starting one in the block/follow the final one in the block.
     992starting one in the block, or follow the final one in the block.
    994993I/O operations can be performed in the prefix of the run, but not in the
    995994measurable sub-run. Therefore we prove that we can predict reaction times, but
     
    998997\section{Future work}
    999998
    1000 All the CerCo software and deliverables can be found on-line at the
    1001 address \url{http://cerco.cs.unibo.it}.
     999All the CerCo software and deliverables can be found on the CerCo homepage at~\url{http://cerco.cs.unibo.it}.
    10021000
    10031001The results obtained so far are encouraging and provide evidence that
    10041002it is possible to perform static time and space analysis at the source level
    1005 without loosing accuracy, reducing the trusted code base and reconciling the
     1003without losing accuracy, reducing the trusted code base and reconciling the
    10061004study of functional and non-functional properties of programs. The
    10071005techniques introduced seem to be scalable, cover both imperative and
    1008 functional languages and are compatible with every compiler optimization
     1006functional languages and are compatible with every compiler optimisation
    10091007considered by us so far.
    10101008
    1011 To prove that compilers can keep track of optimizations
     1009To prove that compilers can keep track of optimisations
    10121010and induce a precise cost model on the source code, we targeted a simple
    10131011architecture that admits a cost model that is execution history independent.
     
    10171015to basic blocks that can be later transferred by the labeling approach to
    10181016the source code and represented in a meaningful way to the user. The dependent
    1019 labeling approach that we have studied seems a promising tools to achieve
     1017labeling approach that we have studied seems a promising tool to achieve
    10201018this goal, but the cost model generated for a realistic processor could be too
    10211019large and complex to be exposed in the source code. Further study is required
     
    10251023Examples of further future work consist in improving the cost invariant
    10261024generator algorithms and the coverage of compiler optimizations, in combining
    1027 the labeling approach with type \& effect discipline \cite{typeffects}
     1025the labeling approach with the type and effect discipline of~\cite{typeffects}
    10281026to handle languages with implicit memory management, and in experimenting with
    10291027our tools in early development phases. Some larger case study is also necessary
    1030 to evaluate the CerCo's prototype on industrial size programs.
     1028to evaluate the CerCo's prototype on realistic, industrial-scale programs.
    10311029
    10321030\bibliographystyle{llncs}
     
    10371035
    10381036\bibitem{cerco} \textbf{Certified Complexity}. R.M. Amadio, A. Asperti, N. Ayache,
    1039 B. Campbell, D. Mulligan, R. Pollack, Y. Regis-Gianas, C. Sacerdoti Coen, I.
     1037B. Campbell, D. P. Mulligan, R. Pollack, Y. Regis-Gianas, C. Sacerdoti Coen, I.
    10401038Stark, in Procedia Computer Science, Volume 7, 2011, Proceedings of the 2 nd
    10411039European Future Technologies Conference and Exhibition 2011 (FET 11), 175-177.
    10421040
    10431041\bibitem{labeling} \textbf{Certifying and Reasoning on Cost Annotations in C
    1044 Programs}, N.  Ayache, R.M. Amadio, Y.Régis-Gianas, in Proc. FMICS, Springer
     1042Programs}, N.  Ayache, R.M. Amadio, Y.R\'{e}gis-Gianas, in Proc. FMICS, Springer
    10451043LNCS
    104610447437: 32-46, 2012.
     
    10491047\bibitem{labeling2} \textbf{Certifying and reasoning on cost annotations of
    10501048functional programs}.
    1051 R.M. Amadio, Y. Régis-Gianas. Proceedings of the Second international conference
     1049R.M. Amadio, Y. R\'{e}gis-Gianas. Proceedings of the Second international conference
    10521050on Foundational and Practical Aspects of Resource Analysis FOPARA 2011 Springer
    10531051LNCS 7177:72-89, 2012.
     
    10761074\bibitem{correctness} \textbf{On the correctness of an optimising assembler for
    10771075the intel MCS-51 microprocessor}.
    1078   D.P. Mulligan, C. Sacerdoti Coen. In Proceedings of the Second
     1076  D. P. Mulligan, C. Sacerdoti Coen. In Proceedings of the Second
    10791077international conference on Certified Programs and Proofs, Springer-Verlag 2012.
    10801078
    10811079\bibitem{proartis} \textbf{PROARTIS: Probabilistically Analysable Real-Time
    1082 Systems}, F.J. Cazorla, E. Quiñones, T. Vardanega, L. Cucu, B. Triquet, G.
     1080Systems}, F.J. Cazorla, E. Qui\~{n}ones, T. Vardanega, L. Cucu, B. Triquet, G.
    10831081Bernat, E. Berger, J. Abella, F. Wartel, M. Houston, et al., in ACM Transactions
    10841082on Embedded Computing Systems, 2012.
Note: See TracChangeset for help on using the changeset viewer.