Changeset 3152 for Deliverables

Timestamp:

Apr 16, 2013, 2:46:53 PM (8 years ago)

Author:

amadio

Message:

r

File:

• Deliverables/D6.3/report.tex (modified) (3 diffs)

Deliverables/D6.3/report.tex

@@ -15 +15 @@
 \usepackage{bbm}
 
+% Amadio's macros
+\newcommand{\cost}{{\sf Cost}}
+\newcommand{\lamcost}{\sf LamCost}
+\newcommand{\cil}{{\sf CIL}}
+\newcommand{\scade}{{\sf Scade}}
+\newcommand{\absint}{{\sf AbsInt}}
+\newcommand{\framac}{{\sf Frama-C}}
+\newcommand{\acsl}{{\sf {ACSL}}}
+\newcommand{\jessie}{{\sf {Jessie}}}
+\newcommand{\powerpc}{{\sf PowerPc}}
+\newcommand{\lustre}{{\sf Lustre}}
+\newcommand{\esterel}{{\sf Esterel}}
+\newcommand{\ml}{{\sf ML}}
+\newcommand{\altergo}{{\sf {Alt-Ergo}}}
+\newcommand{\why}{{\sf {Why}}}
+\newcommand{\old}{\backslash old}
+\newcommand{\C}{{\sf C}}
+\newcommand{\coq}{{\sf Coq}}
+\newcommand{\ocaml}{{\sf ocaml}}
+\newcommand{\AND}{\wedge}               % conjunction 
+\newcommand{\w}[1]{{\it #1}}    %To write in math style 
+
 \title{
 INFORMATION AND COMMUNICATION TECHNOLOGIES\\
@@ -79 +101 @@
 \begin{large}
 Main Authors:\\
-XXXX %Dominic P. Mulligan and Claudio Sacerdoti Coen
+Roberto M.~Amadio, Claudio Sacerdoti Coen
+%Dominic P. Mulligan and Claudio Sacerdoti Coen
 \end{large}
 \end{center}
@@ -117 +140 @@
 \newpage
 
+
+\section{Review of cost synthesis techniques}
+We review the {\em cost synthesis techniques} developed in the project.
+
+The {\em starting hypothesis} is that we have a certified methodology
+to annotate `blocks' in the source code with constants which provide
+a sound and possibly precise upper bound on the cost of executing the 
+`blocks' after compilation to binary code.
+
+The {\em principle} that we have followed in designing the cost synthesis
+tools is that the synthetic bounds should be expressed and proved within 
+a general purpose tool built to reason on the source code.
+In particular, we rely on the $\framac$ tool to reason on $\C$ code and on the $\coq$ 
+proof-assistant to reason on higher-order functional programs.
+
+This principle entails that:
+
+\begin{itemize}
+
+\item The inferred synthetic bounds are indeed {\em correct}
+as long as the general purpose tool is.
+
+\item There is {\em no limitation on the  class of programs} that can be handled 
+as long as the user is willing to carry on an interactive proof.
+
+\end{itemize}
+
+Of course, {\em automation} is desirable whenever possible.  Within this
+framework, automation means writing programs that give hints to the
+general purpose tool. These hints may take the form, say, of loop
+invariants/variants, of predicates describing the structure of the heap,
+or of types in a light logic.  If these hints are
+correct and sufficiently precise the general purpose tool will produce
+a proof automatically, otherwise, user interaction is required.  What
+follows is a summary of work described in more detail in deliverables
+D5.1 and D5.3. The cost synthesis techniques we outline are at
+varying degree of maturity ranging from a complete experimental
+validation to preliminary thought experiments.
+
+
+\subsection{The $\cost$ plug-in and its application to the Lustre compiler}
+$\framac$ is a set of analysers for $\C$ programs with a specification language
+called $\acsl$. New analyses can be dynamically added through a plug-in
+system. For instance, the $\jessie$ plug-in allows deductive verification of
+$\C$ programs with respect to their specification in $\acsl$, with various
+provers as back-end tools. 
+
+We developed the $\cost$ plug-in for the $\framac$ platform as a proof of
+concept of an automatic environment exploiting the cost annotations produced by
+the $\cerco$ compiler. It consists of an $\ocaml$ program 
+which in first approximation takes the following actions: (1) it receives as
+input a $\C$ program, (2) it applies the $\cerco$ compiler to produce a related
+$\C$ program with cost annotations, (3) it applies some heuristics to produce a
+tentative bound on the cost of executing the $\C$ functions of the program as a
+function of the value of their parameters, (4) the user can then call the
+$\jessie$ tool to discharge the related proof
+obligations.  %\marginpar{Some facts/pointer to Cost tool.}
+
+In the following we elaborate on the soundness of the framework
+and the experiments we performed with the $\cost$ tool 
+on the $\C$ programs produced by a $\lustre$ compiler.
+
+
+
+% First, the input file is fed to
+% $\framac$ that will in turn send it to the $\cost$ plug-in. The action of the
+% plug-in is then:
+% \begin{enumerate}
+% \item apply the $\cerco$ compiler to the source file;
+% \item synthesize an upper bound of the WCET of each function of the source
+%   program by reading the cost annotations added by $\cerco$;
+% \item add the results in the form of post-conditions in $\acsl$ format, relating
+%   the cost of the function before and after its execution.
+% \end{enumerate}
+
+\paragraph{Soundness}
+The soundness of the whole framework depends on the cost annotations
+added by the $\cerco$ compiler, the synthetic costs produced by the $\cost$
+plug-in, the verification conditions (VCs) generated by $\jessie$, and
+the external provers discharging the VCs.  The synthetic costs being
+in $\acsl$ format, $\jessie$ can be used to verify them.
+%RA There was a confusion between basic cost annotations and synthetic costs.
+Thus, even if the added synthetic costs are incorrect (relatively to the cost annotations), 
+the process in its globality is still correct: indeed, $\jessie$ will not validate
+incorrect costs and no conclusion can be made about the WCET of
+the program in this case. In other terms, the soundness does not really depend on the action
+of the $\cost$ plug-in, which can in principle produce \emph{any}
+synthetic cost. However, in order to be able to actually prove a WCET of a
+$\C$ function, we need to add correct annotations in a way that $\jessie$
+and subsequent automatic provers have enough information to deduce
+their validity. In practice this is not straightforward
+even for very simple programs composed of branching and assignments
+(no loops and no recursion) because a fine analysis of the VCs associated with 
+branching may lead to a complexity blow up.
+
+\paragraph{Experience with $\lustre$}
+$\lustre$ is a data-flow language to program 
+synchronous systems and the language comes with a compiler to
+$\C$.
+We designed a wrapper for supporting $\lustre$ files. 
+The $\C$ function produced by the compiler implements the {\em step function}
+of the synchronous system and computing the WCET of the function amounts to obtain 
+a bound on the reaction time of the system. 
+We tested the  $\cost$ plug-in and the $\lustre$ wrapper on the $\C$ programs generated by the
+$\lustre$ compiler. For programs consisting of a few hundreds loc, 
+the $\cost$ plug-in computes a WCET and $\altergo$ is able to discharge all VCs
+automatically.
+
+
+
+
+\subsection{Handling $\C$ programs with simple loops}
+The cost annotations added by the $\cerco$ compiler take the form of $\C$
+instructions that update by a constant a fresh global variable called the
+\emph{cost variable}. Synthesizing a WCET of a $\C$ function thus consists in
+statically resolving an upper bound of the difference between the value of the
+cost variable before and after the execution of the function, {\em i.e.} find in the
+function the instructions that update the cost variable and establish the number
+of times they are passed through during the flow of execution. In
+order to do the analysis the plugin makes the following assumptions on the programs:
+\begin{itemize}
+\item No recursive functions.
+\item Every loop must be annotated with a {\em variant}. The
+  variants of `for' loops are automatically inferred.
+\end{itemize}
+
+The plugin proceeds as follows.
+
+\begin{itemize}
+
+\item 
+First the callgraph of the program is computed.
+If the function $f$ calls the function $g$ then the function $g$ is processed before the function $f$.
+
+\item The computation of the cost of the function is performed by traversing its control flow graph.
+The cost at a node is the maximum of the costs of the successors.
+%If the node is an assignment it is substituted in the cost in  the same way as for weakest-precondition. 
+
+\item In the case of a loop with a body that has a constant cost for
+  every step of the loop, the cost is the product of the cost of the
+  body and of the variant taken at the start of the loop.
+
+\item In the case of a loop with a body whose cost depends on
+  the values of some free variables, a fresh logic function $f$ is
+  introduced to represent the cost of the loop in the logic
+  assertions. This logic function takes the variant as a first
+  parameter. The other parameters of $f$ are the free variables of the
+  body of the loop.  An axiom is added to account the fact that the
+  cost is accumulated at each step of the loop:
+  \[
+  f(v, \vec x) =
+    \textrm{if } v < 0 \textrm{ then } 0 \textrm{ else } (f(v-1, \phi(\vec x)) + \psi(\vec x))
+  \]
+  where $\vec x$ are the free variables, $v$ is the variant, $\phi$ computes the 
+  modification of the variable at each step of the loop, and $\psi$ is the 
+  cost of the body of the loop.
+
+\item The cost of the function is directly added as post-condition of
+  the function: $\_\_cost \le \old(\_\_cost) + t$ where $t$ is the term
+  computing the cost of the function, $\_\_cost$ is the time taken from
+  the start of the program, $\old(\_\_cost)$ is the same time but before
+  the execution of the function.
+\end{itemize}
+
+
+The user can influence the annotation by different means:
+\begin{itemize}
+\item By using more precise variants.
+\item By annotating function with cost specification. The plugin will
+  use this cost for the function instead of computing it.
+\end{itemize}
+
+
+
+
+\subsection{$\C$ programs with pointers}
+When it comes to verifying programs involving pointer-based data
+structures, such as linked lists, trees, or graphs, the use of
+traditional first-order logic to specify, and of SMT solvers to
+verify, shows some limitations. {\em Separation logic} is then an
+elegant alternative. Designed at the turn of the century, it is a
+program logic with a new notion of conjunction to express spatial
+heap separation.  Separation logic has been implemented in dedicated theorem provers
+such as {\sf Smallfoot} or {\sf VeriFast}. One
+drawback of such provers, however, is to either limit the
+expressiveness of formulas (e.g. to the so-called symbolic heaps), or
+to require some user-guidance (e.g. open/close commands in Verifast).
+
+In an attempt to conciliate both approaches, Bobot introduced the
+notion of separation predicates during his PhD thesis. The approach
+consists in reformulating some ideas from separation logic into a
+traditional verification framework where the specification language,
+the verification condition generator, and the theorem provers were not
+designed with separation logic in mind. Separation predicates are
+automatically derived from user-defined inductive predicates, on
+demand. Then they can be used in program annotations, exactly as other
+predicates, {\em i.e.}, without any constraint. Simply speaking, where
+one would write $P*Q$ in separation logic, one will here ask for the
+generation of a separation predicate {\em sep} and then use it as $P
+\AND Q \AND \w{sep}(P, Q)$.  We have implemented separation predicates
+within the $\jessie$ plug-in and tested it on a non-trivial case study
+(the composite pattern from the VACID-0 benchmark).  In this case, we
+achieve a fully automatic proof using three existing SMT solver. We
+have also used the separation predicates to reason on the {\em cost}
+of executing simple heap manipulating programs such as an in-place
+list reversal.
+
+
+
+\subsection{The cost of higher-order functional programs}
+We have analysed a rather standard compilation chain from
+a higher-order functional languages to an abstract
+{\sf RTL} language which corresponds directly to the source
+language of the back-end of the $\C$ compiler developed in the $\cerco$ project.
+The compilation consists of four transformations: continuation passing-style,
+value naming, closure conversion, and hoisting.
+
+We have shown that it is possible to extend the labelling approach
+described for the $\C$ language to a higher-order call-by-value functional language.
+
+The first issue we have considered is that of designing a `good
+labelling' function, {\em i.e.}, a function that inserts labels in the
+source code which correspond to `basic blocks' of the compiled
+code. To this end, we have introduced two labelling operators: a
+{\em pre-labelling} $\ell>M$ which emits the label $\ell$ before running $M$
+and a {\em post-labelling} $M>\ell$ which reduces $M$ to a value and then
+emits the label $\ell$.  Roughly speaking, the `good labelling'
+associates a pre-labelling to every function abstraction and a
+post-labelling to every application which is not immediately
+sourrounded by an abstraction.  In particular, the post-labelling
+takes care of the functions created by the CPS translation.
+
+The second issue relates to the instrumentation of the program. 
+To this end, we have relied on a {\em cost monad} which associates
+to each program a pair consisting of its denotation and the
+cost of reducing the program to a value. 
+In this way, the instrumented program can still be regarded
+as a higher-order functional program.
+
+The third issue concerns the method to {\em reason on the instrumented
+(functional) program}. We have built on a higher-order Hoare logic and a related tool
+that generates automatically the proof obligations. These proof
+obligations can either be discharged automatically or 
+interactively using the {\sf Coq} proof assistant and its tactics. 
+Some simple experiments are described in the $\lamcost$ software.
+
+
+\subsection{The cost of memory management}
+In a realistic implementation of a functional programming language,
+the runtime environment usually includes a garbage collector.  In
+spite of considerable progress in {\em real-time garbage
+  collectors}  it seems to us that
+such collectors do not offer yet a viable path to a certified and
+usable WCET prediction of the running time of functional programs.
+As far as we know, the cost predictions concern the {\em amortized case}
+rather than the {\em worst case} and are supported more by experimental evaluations
+than by formal proofs.
+
+The approach we have adopted instead, following the seminal work
+of  Tofte {\em et al.}, is to enrich the last calculus of
+the compilation chain : (1) with a notion
+of {\em memory region}, (2) with operations to allocate and dispose
+memory regions, and (3) with a {\em type and effect system} that guarantees
+the safety of the dispose operation. This allows to further extend 
+the compilation chain mentioned above and then to include the cost 
+of safe memory management in our analysis. Actually, because effects are intertwined with types,
+what we have actually done, following the work of Morrisett {\em et al.},  
+is to extend a {\em typed} version of the compilation chain. 
+An experimental validation of the approach is left for future work and it 
+would require the integration  of region-inference algorithms such as those 
+developed by Aiken {\em et al.} in the compilation chain.
+
+
+
+
+\subsection{Feasible bounds by light typing}
+In our experience, the cost analysis of higher-order programs requires 
+human intervention both at the level of the specification and of the 
+proofs. 
+One path to automation consists in devising programming disciplines
+that entail feasible bounds (polynomial time). The most interesting approaches to this problem
+build on {\em light} versions of linear logic. 
+Our main contribution is to devise a type system that guarantees feasible
+bounds for a higher-order call-by-value functional language with 
+references and threads. 
+The first proof of this result  relies on a kind of standardisation theorem and it is of a combinatorial nature.
+More recentely, we have shown that a proof of a similar result can be obtained
+by semantic means building on the so called {\em quantitative realizability 
+models} proposed by Dal Lago and Hofmann.
+We believe this semantic setting is  particularly appropriate because
+it allows to reason both on typed and untyped programs.
+Thus one can imagine a framework where some programs are feasible `by typing'
+while others are feasible as a result of an `interactive proof' of the obligations
+generated by quantitative realizability. 
+Beyond building such a framework, an interesting issue concerns the 
+certification of {\em concrete bounds} at the level of the {\em compiled code}.
+This has to be contrasted with the current state of the art in implicit computational complexity
+where most bounds are {\em asymptotic} and are stated at the level of the {\em source code}.
+
+
+
+
+\newpage
+
 \includepdf[pages={-}]{pipelines.pdf}