Changeset 3654


Ignore:
Timestamp:
Mar 16, 2017, 9:00:28 AM (9 months ago)
Author:
boender
Message:

Used D5.1 as a base for the Frama-C plug-in chapter

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/framac.tex

    r3615 r3654  
    66\section{FramaC plugin}
    77\label{sect.framac.plugin}
     8
     9The Cost plug-in for the Frama − C platform has been developed in order to
     10automatically synthesize the cost annotations added by the CerCo compiler on a
     11C source program into assertions of the WCET of the functions in the program.
     12The architecture of the plug-in is depicted in figure 3. It accepts a C source
     13file as a parameter and creates a new C file that is the former with additional
     14cost annotations (C code) and WCET assertions (ACSL annotations).  First, the
     15input file is fed to Frama − C that will in turn send it to the Cost plug-in.
     16The action of the plug-in is then:
     17
     18\begin{enumerate}
     19        \item apply the CerCo compiler to the source file;
     20        \item synthesize an upper bound of the WCET of each function of the source
     21                program by reading the cost annotations added by CerCo;
     22        \item   add the results in the form of post-conditions in ACSL format,
     23                relating the cost of the function before and after its execution.
     24\end{enumerate}
     25
     26% XXX add figure?
     27
     28Then, 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
     29of the plug-in will be presented.
     30
     31\subsection{Soundness}
     32
     33As figure 3 suggests, the soundness of the whole framework depends on the cost
     34annotations added by CerCo, the synthesis made by the Cost plug-in, the VCs
     35generated by Jessie, and the VCs discharged by external provers. Since the Cost
     36plug-in adds annotations in ACSL format, Jessie (or other verification plug-ins
     37for Frama − C) can be used to verify these annotations.  Thus, even if the
     38added annotations are incorrect, the process in its globality is still correct:
     39indeed, Jessie will not validate incorrect annotations and no conclusion can be
     40made about the WCET of the program in this case. This means that the Cost
     41plug-in can add any annotation for the WCET of a function, the whole framework
     42will still be correct and thus its soundness does not depend on the action of
     43the Cost plug-in. However, in order to be able to actually prove a WCET of a
     44function, we need to add correct annotations in a way that Jessie and
     45subsequent automatic provers have enough information to deduce validity.
     46
     47\subsection{Inner workings}
     48
     49The cost annotations added by the CerCo compiler take the form of C
     50instructions that update by a constant a fresh global variable called the cost
     51variable. Synthesizing a WCET of a C function thus consists in statically
     52resolving an upper bound of the difference between the value of the cost
     53variable before and after the execution of the function, i.e. find in the
     54function the instructions that update the cost variable and establish the
     55number of times they are passed through during the flow of execution. This
     56raises two main issues: indecidability caused by loop constructs, and function
     57calls. Indeed, a side effect of function calls is to change the value of the
     58cost variable. When a function calls another one, the cost of the callee is
     59part of the cost of the caller. This means that the computation of a WCET of
     60each function of a C program is subject to the calling dependencies. To cope
     61with the issues of loops and function calls, the Cost plug-in proceeds as
     62follows:
     63
     64\begin{enumerate}
     65        \item each function is independently processed and associated a WCET that may
     66                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
     68                loops for which we can decide the number of iterations. The abstract domain
     69                used is made of expressions whose variables can only be formal parameters
     70                of the function;
     71        \item a system of inequations is built from the result of the previous step,
     72                and is tried to be solved with a fixpoint. At each iteration, the fixpoint
     73                replaces in all the inequations the references to the cost of a function by
     74                its associated cost if it is independent of the other functions;
     75        \item ACSL annotations are added to the program according to the result of
     76                the above fixpoint.  Note that the two previous steps may fail in finding a
     77                concrete WCET for some functions, because of imprecision inherent to
     78                abstract interpretation, and recursion in the source program not solved by
     79                the fixpoint. At each program point that requires an annotation (function
     80                definitions and loops), annotations are added if a solution was found for
     81                the program point.
     82\end{itemize}
     83
     84Figure 4 shows the result of the Cost plug-in when fed the program in figure
     851a. There are several differences from the manually annotated program, the most
     86noticeable being:
     87
     88\begin{itemize}
     89        \item the manually annotated program had a pre-condition that the size formal
     90                parameter needed to be greater or equal to 1. The Cost plug-in does not
     91                make such an assumption, but instead considers both the case where size is
     92                greater or equal to 1, and the case where it is not. This results in a
     93                ternary expression inside the WCET specification (the post-condition or
     94                ensures clause), and some new loop invariants;
     95        \item the loop invariant specifying the value of the cost variable depending
     96                on the iteration number refers to a new local variable named cost tmp0. It
     97                represents the value of the cost variable right before the loop is
     98                executed. It allows to express the cost inside the loop with regards to the
     99                cost before the loop, instead of the cost at the beginning of the function;
     100                it often makes the expression a lot shorter and eases the work for nested
     101                loops.
     102\end{itemize}
     103
     104Running Jessie on the program generates VCs that are all proved by Alt − Ergo:
     105the WCET computed by the Cost plug-in is correct.
Note: See TracChangeset for help on using the changeset viewer.