Changeset 3661


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

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

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

Legend:

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

    r3653 r3661  
    13491349
    13501350
    1351 @inproceedings{Cousot:1977:AIU:512950.512973,
     1351@inproceedings{Cousot1977,
    13521352 author = {Cousot, Patrick and Cousot, Radhia},
    13531353 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 r3661  
    5757Case studies demonstrated the feasibility of using the Hume programming language for developing resource-constrained applications~~\cite{BoneAChenZHMWW2007:ACM}.
    5858
    59 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.
     59The 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.
    6060See~\cite{stateart} for a survey of state-of-the-art techniques in the WCET field.
    6161A 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 r3661  
    77\label{sect.framac.plugin}
    88
    9 The Cost plug-in for the Frama − C platform has been developed in order to
     9The Cost plug-in for the Frama-C platform has been developed in order to
    1010automatically synthesize the cost annotations added by the CerCo compiler on a
    1111C source program into assertions of the WCET of the functions in the program.
     
    1313file as a parameter and creates a new C file that is the former with additional
    1414cost annotations (C code) and WCET assertions (ACSL annotations).  First, the
    15 input file is fed to Frama − C that will in turn send it to the Cost plug-in.
     15input file is fed to Frama-C that will in turn send it to the Cost plug-in.
    1616The action of the plug-in is then:
    1717
     
    2424\end{enumerate}
    2525
    26 % XXX add figure?
    27 
    28 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
     26\begin{figure}[h!]
     27% XXX figure
     28\caption{The Cost plug-in}
     29\label{fig:costplugin}
     30\end{figure}
     31
     32Then, the user can either {\em trust} the results (the WCET of the functions), or want to
     33{\em verify} them, in which case they can call Jessie.
     34We continue our description of the plug-in by discussing the soundness of the framework,
     35because, as we will see, the action of the plug-in is not involved in this issue. Then, the details
    2936of the plug-in will be presented.
    3037
    3138\subsection{Soundness}
    3239
    33 As figure 3 suggests, the soundness of the whole framework depends on the cost
     40As figure~\ref{fig:costplugin} suggests, the soundness of the whole framework depends on the cost
    3441annotations added by CerCo, the synthesis made by the Cost plug-in, the VCs
    3542generated by Jessie, and the VCs discharged by external provers. Since the Cost
    3643plug-in adds annotations in ACSL format, Jessie (or other verification plug-ins
    37 for Frama − C) can be used to verify these annotations.  Thus, even if the
     44for Frama-C) can be used to verify these annotations.  Thus, even if the
    3845added annotations are incorrect, the process in its globality is still correct:
    3946indeed, Jessie will not validate incorrect annotations and no conclusion can be
     
    6572        \item each function is independently processed and associated a WCET that may
    6673                depend on the cost of the other functions. This is done with a mix between
    67                 abstract interpretation \cite{blerp} and syntactic recognition of specific
     74                abstract interpretation~\cite{Cousot1977} and syntactic recognition of specific
    6875                loops for which we can decide the number of iterations. The abstract domain
    6976                used is made of expressions whose variables can only be formal parameters
     
    8289\end{itemize}
    8390
    84 Figure 4 shows the result of the Cost plug-in when fed the program in figure
    85 1a. There are several differences from the manually annotated program, the most
     91Figure~\ref{fig:example-post} shows the result of the Cost plug-in when fed the program in
     92figure~\ref{fig:example-pre}
     93
     94\begin{figure}[!h]
     95\begin{lstlisting}[language=C]
     96int is_sorted (int *tab, int size) {
     97        int i, res = 1;
     98
     99        for (i = 0 ; i < size-1 ; i++) if (tab[i] > tab[i+1]) res = 0;
     100
     101        return res;
     102}
     103\end{lstlisting}
     104\caption{Example program before CerCo}
     105\label{fig:example-pre}
     106\end{figure}
     107
     108\begin{figure}[!h]
     109\begin{lstlisting}[language=C]
     110int _cost = 0;
     111
     112/*@ ensures _cost ≡ \old(_cost) + incr; */
     113void _cost_incr (int incr) { _cost = _cost + incr; }
     114
     115/*@ ensures ( _cost ≤ \old(_cost)+(101+(0<size-1?(size-1)*195:0))); */
     116int is_sorted (int *tab, int size) {
     117        int i, res = 1, _cost_tmp0;
     118
     119        _cost_incr(97);
     120
     121        _cost_tmp0 = _cost;
     122        /*@ loop invariant (0 < size-1) ⇒ (i ≤ size-1);
     123          @ loop invariant (0 ≥ size-1) ⇒ (i ≡ 0);
     124          @ loop invariant ( _cost ≤ _cost_tmp0+i*195);
     125          @ loop variant (size-1)-i; */
     126        for (i = 0; i < size-1; i++) {
     127                _cost_incr(91);
     128                if (tab[i] > tab[i+1]) { _cost_incr(104); res = 0; }
     129                else _cost_incr(84);
     130        }
     131
     132        _cost_incr(4);
     133        return res;
     134}
     135\end{lstlisting}
     136\caption{Result of the Cost plug-in}
     137\label{fig:example-post}
     138\end{figure}
     139
     140There are several differences from the manually annotated program, the most
    86141noticeable being:
    87142
     
    102157\end{itemize}
    103158
    104 Running Jessie on the program generates VCs that are all proved by Alt − Ergo:
     159Running Jessie on the program generates VCs that are all proved by Alt-Ergo:
    105160the WCET computed by the Cost plug-in is correct.
     161
     162\subsection{Lustre case study}
     163
     164Lustre is a synchronous language where reactive systems are described by flow of values. It comes with a compiler that transforms a
     165Lustre node (any part of or the whole system) into a C step function that represents one synchronous cycle of the node. A WCET for
     166the step function is thus a worst case reaction time for the component. The generated C step function neither contains loops nor is
     167recursive, which makes it particularly well suited for a use with the Cost plug-in with a complete support.
     168
     169We 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
     170corresponding to the node. Optionally, verification with Jessie or testing can be toggled. The flow of the wrapper is described in
     171figure 5. It simply executes a command line, reads the results, and sends them to the next command.
     172
     173A typical run of the wrapper looks as follows (we use the parity example from our distribution of Lustre; it computes the parity bit
     174of a boolean array):
     175
     176frama-c lustre -verify -test parity.lus parity
     177
     178Invoking the above command line produces the following output:
     179
     180WCET 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.
     181
     182\begin{itemize}
     183        \item All the intermediary results of the wrapper are stored in files. Verbosity can be turned on to show the different commands
     184                invoked and the resulting files.
     185        \item The step function generated with the Lustre compiler for the node parity is called \verb+parity_step+. It might call
     186                functions that are not defined but only prototyped, such as \verb+parity_O_parity+ or \verb+parity_O_done+. Those are functions
     187                that the user of the Lustre compiler can use for debugging, but that are not part of the parity system. Therefore, we leave their
     188                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
     189                the user).
     190        \item Testing consists in adding a main function to the C file, that will run the step function on a parameterized number of input
     191                states for a parameterized number of cycles. The C file contains information that allows to syntatically distinguish integer
     192                variables used as booleans, which helps in generating interesting input states. After each iteration of the step function, the
     193                value of the cost variable is fetched in order to compute its overall minimum, maximum and average value for one step. If the
     194                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.
     195\end{itemize}
     196
     197\subsection{Experiments}
     198
     199The Cost plug-in and the Lustre wrapper have been developed in order to validate CerCo's framework for modular WCET analysis, by
     200showing the results that could be obtained with this approach. Through CerCo , they allow (semi-)automatic generation and
     201certification of WCET for C and Lustre programs. For the latter, the WCET represents a bound for thereaction time of a component.
     202This section presents results obtained on C programs typically found in embedded software, where WCET is of great importance.
     203
     204The Cost plug-in is written in 3895 lines of OCaml. They mainly cover an abstract interpretation of C together with a syntactic
     205recognition of specific loops, in a modular fashion: the abstract domains (one for C values and another for cost values) can be
     206changed. The Lustre 8 wrapper is made of 732 lines of OCaml consisting in executing a command, reading the results and sending them
     207to the next command.
     208
     209We 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
     210fils, we report its type (either a standard algorithm written in C, a cryptographic protocol for embedded software, or a C program
     211generated from Lustre files), a quick description of the program, the number of lines of the original code and the number of VCs
     212generated. A WCET is found by the Cost plug-in for every one of these programs, and Alt−Ergo was able to discharge all VCs.
     213
     214{\small
     215\begin{center}
     216\begin{tabular}{|l|c|l|c|c|}
     217\hline
     218\multicolumn{1}{|c|}{File} & Type & \multicolumn{1}{c|}{Description} & LOC & VCs \\
     219\hline
     220\verb+3-way.c+ & C & Three way block cipher & 144 & 34 \\
     221\hline
     222\verb+a5.c+ & C & A5 stream cipher, used in GSM cellular & 226 & 18 \\
     223\hline
     224\verb+array_sum.c+ & S & Sums the elements of an integer array & 15 & 9 \\
     225\hline
     226\verb+fact.c+ & S & Factorial function, imperative implementation & 12 & 9 \\
     227\hline
     228\verb+is_sorted.c+ & S & Sorting verification of an array & 8 & 8 \\
     229\hline
     230\verb+LFSR.c+ & C & 32-bit linear-feedback shift register & 47 & 3 \\
     231\hline
     232\verb+minus.c+ & L & Two modes button & 193 & 8 \\
     233\hline
     234\verb+mmb.c+ & C & Modular multiplication-based block cipher & 124 & 6 \\
     235\hline
     236\verb+parity.lus+ & L & Parity bit of a boolean array & 359 & 12 \\
     237\hline
     238\verb+random.c+ & C & Random number generator & 146 & 3 \\
     239\hline
     240\multicolumn{5}{|c|}{S: standard algorithm C: cryptographic protocol} \\
     241\multicolumn{5}{|c|}{L: C generated from a Lustre file} \\
     242\hline
     243\end{tabular}
     244\end{center}
     245}
     246
     247Since 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
     248covering awide range of programs. CerCo always succeeds, but the Cost plug-in may fail in synthesizing a WCET, and automatic provers
     249may fail in discharging some VCs. We can improve the abstract domains, the form of recognized loops, or the hints that help automatic
     250provers.
     251
     252For now, a typical program that is processed by the Cost plug-in and whose VCs are fullydischarged by automatic provers is made of
     253loops with a counter incremented or decremented at the end of the loop, and where the guard condition is a comparison of the counter
     254with some expression. The expressions incrementing or decrementing the counter and used in the guard condition must be so that the
     255abstract interpretation succeeded in relating them to anarithmetic expressions whose variables are parameters of the function. With a
     256flat 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.