# Changeset 3661

Ignore:
Timestamp:
Mar 16, 2017, 2:34:24 PM (15 months ago)
Message:

Added second part of technical report as basis for Frama-C section

Location:
Papers/jar-cerco-2017
Files:
3 edited

Unmodified
Added
Removed
• ## Papers/jar-cerco-2017/cerco.bib

 r3653 @inproceedings{Cousot:1977:AIU:512950.512973, @inproceedings{Cousot1977, author = {Cousot, Patrick and Cousot, Radhia}, title = {Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints},
• ## Papers/jar-cerco-2017/conclusions.tex

 r3653 Case studies demonstrated the feasibility of using the Hume programming language for developing resource-constrained applications~~\cite{BoneAChenZHMWW2007:ACM}. The current state of the art in concrete timing analysis is represented by WCET tools, which use Abstract Interpretation~\cite{Cousot:1977:AIU:512950.512973}, control flow analyses, and detailed models of hardware to derive tight time bounds on expected program execution time. The current state of the art in concrete timing analysis is represented by WCET tools, which use Abstract Interpretation~\cite{Cousot1977}, control flow analyses, and detailed models of hardware to derive tight time bounds on expected program execution time. See~\cite{stateart} for a survey of state-of-the-art techniques in the WCET field. A variety of academic and commercial sources provide advanced WCET tooling: for example, aiT~\cite{absint}, bound-T~\cite{bound-T}, SWEET~\cite{Lisper2014}, Heptane~\cite{heptane}, and OTAWA~\cite{otawa}.
• ## Papers/jar-cerco-2017/framac.tex

 r3655 \label{sect.framac.plugin} The Cost plug-in for the Frama − C platform has been developed in order to The Cost plug-in for the Frama-C platform has been developed in order to automatically synthesize the cost annotations added by the CerCo compiler on a C source program into assertions of the WCET of the functions in the program. file as a parameter and creates a new C file that is the former with additional cost annotations (C code) and WCET assertions (ACSL annotations).  First, the input file is fed to Frama − C that will in turn send it to the Cost plug-in. input file is fed to Frama-C that will in turn send it to the Cost plug-in. The action of the plug-in is then: \end{enumerate} % XXX add figure? Then, the user can either trust the results (the WCET of the functions), or want to verify them, in which case he can call Jessie.  We continue our description of the plug-in by discussing the soundness of the framework, because, as we will see, the action of the plug-in is not involved in this issue. Then, the details \begin{figure}[h!] % XXX figure \caption{The Cost plug-in} \label{fig:costplugin} \end{figure} Then, the user can either {\em trust} the results (the WCET of the functions), or want to {\em verify} them, in which case they can call Jessie. We continue our description of the plug-in by discussing the soundness of the framework, because, as we will see, the action of the plug-in is not involved in this issue. Then, the details of the plug-in will be presented. \subsection{Soundness} As figure 3 suggests, the soundness of the whole framework depends on the cost As figure~\ref{fig:costplugin} suggests, the soundness of the whole framework depends on the cost annotations added by CerCo, the synthesis made by the Cost plug-in, the VCs generated by Jessie, and the VCs discharged by external provers. Since the Cost plug-in adds annotations in ACSL format, Jessie (or other verification plug-ins for Frama − C) can be used to verify these annotations.  Thus, even if the for Frama-C) can be used to verify these annotations.  Thus, even if the added annotations are incorrect, the process in its globality is still correct: indeed, Jessie will not validate incorrect annotations and no conclusion can be \item each function is independently processed and associated a WCET that may depend on the cost of the other functions. This is done with a mix between abstract interpretation \cite{blerp} and syntactic recognition of specific abstract interpretation~\cite{Cousot1977} and syntactic recognition of specific loops for which we can decide the number of iterations. The abstract domain used is made of expressions whose variables can only be formal parameters \end{itemize} Figure 4 shows the result of the Cost plug-in when fed the program in figure 1a. There are several differences from the manually annotated program, the most Figure~\ref{fig:example-post} shows the result of the Cost plug-in when fed the program in figure~\ref{fig:example-pre} \begin{figure}[!h] \begin{lstlisting}[language=C] int is_sorted (int *tab, int size) { int i, res = 1; for (i = 0 ; i < size-1 ; i++) if (tab[i] > tab[i+1]) res = 0; return res; } \end{lstlisting} \caption{Example program before CerCo} \label{fig:example-pre} \end{figure} \begin{figure}[!h] \begin{lstlisting}[language=C] int _cost = 0; /*@ ensures _cost ≡ \old(_cost) + incr; */ void _cost_incr (int incr) { _cost = _cost + incr; } /*@ ensures ( _cost ≤ \old(_cost)+(101+(0 tab[i+1]) { _cost_incr(104); res = 0; } else _cost_incr(84); } _cost_incr(4); return res; } \end{lstlisting} \caption{Result of the Cost plug-in} \label{fig:example-post} \end{figure} There are several differences from the manually annotated program, the most noticeable being: \end{itemize} Running Jessie on the program generates VCs that are all proved by Alt − Ergo: Running Jessie on the program generates VCs that are all proved by Alt-Ergo: the WCET computed by the Cost plug-in is correct. \subsection{Lustre case study} Lustre is a synchronous language where reactive systems are described by flow of values. It comes with a compiler that transforms a Lustre node (any part of or the whole system) into a C step function that represents one synchronous cycle of the node. A WCET for the step function is thus a worst case reaction time for the component. The generated C step function neither contains loops nor is recursive, which makes it particularly well suited for a use with the Cost plug-in with a complete support. We designed a wrapper that has for inputs a Lustre file and a node inside the file, and outputs the cost of the C step function corresponding to the node. Optionally, verification with Jessie or testing can be toggled. The flow of the wrapper is described in figure 5. It simply executes a command line, reads the results, and sends them to the next command. A typical run of the wrapper looks as follows (we use the parity example from our distribution of Lustre; it computes the parity bit of a boolean array): frama-c lustre -verify -test parity.lus parity Invoking the above command line produces the following output: WCET of parity step: 2220+ cost of parity O parity+ cost of parity O done(not verified).Verifying the result (this may take some time)...WCET is proven correct.Testing the result (this may take some time)...Estimated WCET: 2220Minimum: 2144Maximum: 2220Average: 2151Estimated WCET is correct for these executions. \begin{itemize} \item All the intermediary results of the wrapper are stored in files. Verbosity can be turned on to show the different commands invoked and the resulting files. \item The step function generated with the Lustre compiler for the node parity is called \verb+parity_step+. It might call functions that are not defined but only prototyped, such as \verb+parity_O_parity+ or \verb+parity_O_done+. Those are functions that the user of the Lustre compiler can use for debugging, but that are not part of the parity system. Therefore, we leave their cost abstract in the expression of the cost of the step function, and we set their cost to 0 when testing (this can be changed by the user). \item Testing consists in adding a main function to the C file, that will run the step function on a parameterized number of input states for a parameterized number of cycles. The C file contains information that allows to syntatically distinguish integer variables used as booleans, which helps in generating interesting input states. After each iteration of the step function, the value of the cost variable is fetched in order to compute its overall minimum, maximum and average value for one step. If the maximum were to be greater than the WCET computed by the Cost plug-in, then we could conclude of an error in the plug-in. \end{itemize} \subsection{Experiments} The Cost plug-in and the Lustre wrapper have been developed in order to validate CerCo's framework for modular WCET analysis, by showing the results that could be obtained with this approach. Through CerCo , they allow (semi-)automatic generation and certification of WCET for C and Lustre programs. For the latter, the WCET represents a bound for thereaction time of a component. This section presents results obtained on C programs typically found in embedded software, where WCET is of great importance. The Cost plug-in is written in 3895 lines of OCaml. They mainly cover an abstract interpretation of C together with a syntactic recognition of specific loops, in a modular fashion: the abstract domains (one for C values and another for cost values) can be changed. The Lustre 8 wrapper is made of 732 lines of OCaml consisting in executing a command, reading the results and sending them to the next command. We ran the plug-in and the Lustre wrapper on some files found on the web, from the Lustre distribution or written by hand. For each fils, we report its type (either a standard algorithm written in C, a cryptographic protocol for embedded software, or a C program generated from Lustre files), a quick description of the program, the number of lines of the original code and the number of VCs generated. A WCET is found by the Cost plug-in for every one of these programs, and Alt−Ergo was able to discharge all VCs. {\small \begin{center} \begin{tabular}{|l|c|l|c|c|} \hline \multicolumn{1}{|c|}{File} & Type & \multicolumn{1}{c|}{Description} & LOC & VCs \\ \hline \verb+3-way.c+ & C & Three way block cipher & 144 & 34 \\ \hline \verb+a5.c+ & C & A5 stream cipher, used in GSM cellular & 226 & 18 \\ \hline \verb+array_sum.c+ & S & Sums the elements of an integer array & 15 & 9 \\ \hline \verb+fact.c+ & S & Factorial function, imperative implementation & 12 & 9 \\ \hline \verb+is_sorted.c+ & S & Sorting verification of an array & 8 & 8 \\ \hline \verb+LFSR.c+ & C & 32-bit linear-feedback shift register & 47 & 3 \\ \hline \verb+minus.c+ & L & Two modes button & 193 & 8 \\ \hline \verb+mmb.c+ & C & Modular multiplication-based block cipher & 124 & 6 \\ \hline \verb+parity.lus+ & L & Parity bit of a boolean array & 359 & 12 \\ \hline \verb+random.c+ & C & Random number generator & 146 & 3 \\ \hline \multicolumn{5}{|c|}{S: standard algorithm C: cryptographic protocol} \\ \multicolumn{5}{|c|}{L: C generated from a Lustre file} \\ \hline \end{tabular} \end{center} } Since the goal of the Cost plug-in is a proof of concept of a full framework with CerCo , we did not put too much effort or time for covering awide range of programs. CerCo always succeeds, but the Cost plug-in may fail in synthesizing a WCET, and automatic provers may fail in discharging some VCs. We can improve the abstract domains, the form of recognized loops, or the hints that help automatic provers. For now, a typical program that is processed by the Cost plug-in and whose VCs are fullydischarged by automatic provers is made of loops with a counter incremented or decremented at the end of the loop, and where the guard condition is a comparison of the counter with some expression. The expressions incrementing or decrementing the counter and used in the guard condition must be so that the abstract interpretation succeeded in relating them to anarithmetic expressions whose variables are parameters of the function. With a flat domain currently used, this means that the values of these expressions may not be modified during a loop.
Note: See TracChangeset for help on using the changeset viewer.