source: Deliverables/D6.3/report.tex @ 3221

\documentclass[11pt, epsf, a4wide]{article}

\usepackage{../style/cerco}
\usepackage{pdfpages}

\usepackage{amsfonts}
\usepackage{amsmath}
\usepackage{amssymb} 
\usepackage[english]{babel}
\usepackage{graphicx}
\usepackage[utf8x]{inputenc}
\usepackage{listings}
\usepackage{stmaryrd}
\usepackage{url}
\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\\
(ICT)\\
PROGRAMME\\
\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}

\lstdefinelanguage{matita-ocaml}
  {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try},
   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
   morekeywords={[3]type,of},
   mathescape=true,
  }

\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
        keywordstyle=\color{red}\bfseries,
        keywordstyle=[2]\color{blue},
        keywordstyle=[3]\color{blue}\bfseries,
        commentstyle=\color{green},
        stringstyle=\color{blue},
        showspaces=false,showstringspaces=false}

\lstset{extendedchars=false}
\lstset{inputencoding=utf8x}
\DeclareUnicodeCharacter{8797}{:=}
\DeclareUnicodeCharacter{10746}{++}
\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}

\date{}
\author{}

\begin{document}

\thispagestyle{empty}

\vspace*{-1cm}
\begin{center}
\includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
\end{center}

\begin{minipage}{\textwidth}
\maketitle
\end{minipage}

\vspace*{0.5cm}
\begin{center}
\begin{LARGE}
\textbf{
Report n. D6.3\\
Final Report on User Validation}
\end{LARGE} 
\end{center}

\vspace*{2cm}
\begin{center}
\begin{large}
Version 1.0
\end{large}
\end{center}

\vspace*{0.5cm}
\begin{center}
\begin{large}
Main Authors:\\
Roberto M.~Amadio, Gabriele Pulcini, Claudio Sacerdoti Coen
%Dominic P. Mulligan and Claudio Sacerdoti Coen
\end{large}
\end{center}

\vspace*{\fill}

\noindent
Project Acronym: \cerco{}\\
Project full title: Certified Complexity\\
Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\

\clearpage
\pagestyle{myheadings}
\markright{\cerco{}, FP7-ICT-2009-C-243881}

\newpage

\vspace*{7cm}
\paragraph{Abstract}
We review the techniques experimented in CerCo for cost annotation exploitment
at the user level. We also report on recent work towards precise time analysis
at the source level for modern hardware architectures whose instructions cost 
is a function of the internal hardware state (pipelines, caches, branch
prediction units, etc.).

\newpage

\tableofcontents

\newpage

\section{Task}
\label{sect.task}

The Grant Agreement describes deliverable D6.3 as follows:
\begin{quotation}
\textbf{Final Report on User Validation}: An articulated analysis and critics of the user validation experiences. In particular we will review the effectiveness of the techniques for cost annotation exploitment that have been employed in the project and that have been validated on simple and non trivial examples. We will also identify additional techniques that could be exploited in the middle and long term to bring the CerCo compiler to its full potentialities.

\end{quotation}

\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
surrounded 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 recently, 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}.


\section{Middle and Long Term Improvements}
The future improvements that will affect the user experience falls into two
categories:
\begin{enumerate}
 \item \textbf{Improvements to invariant generators}
   The invariant generator that we implemented in the plug-in allows to
   compute the parametric worst case execution time for all Lustre programs
   and for almost all the C tests that we targeted. Nevertheless, at the
   moment the generator does not degrade gracefully: if the source code does
   not respects the syntactic requirements of the generator, no cost invariants
   are generated at all. This behaviour is consistent with the traditional
   use in proving functional properties, but for non functional ones we
   are interested in always providing a worst case bound, possibly by dropping
   the dependencies and computing a very rough one. That is the behaviour of
   standard WCET analyzers (that, most of the time, are not parametric anyway).

   Other future improvements consist in enlarging the class of recognized
   program shapes by integrating more advanced techniques or interacting with
   existing tools.

   Both kind of improvements can be performed in the middle term.
 \item \textbf{Improvements to cost annotation exploitment}
   One benefit of CerCo w.r.t. traditional WCET is that the user does not need
   to trust the bound provided by the tool, but it can at least partially
   verify it manually or using automated techniques.

   The combinations of techniques described in the previous section allowed
   to automatically certify the parametric worst case execution time for all
   Lustre programs and for the majority of simple C tests we had at our
   disposal. Nevertheless, we expect automation to fail more frequently on
   real world, industrial examples. In the middle term we should experiment
   with more complex code and enlarge the set of techniques according to the
   observed results. In particular, we should implement at the source level
   at least all those that are used on the object code in standard WCET tools.
   It may well be the case that we identify a set of recurrent proof obligations
   that are not solved by the existing theorem provers, but that admit a
   solution by means of a uniform strategy. In any case, the failure to
   automatically prove sound a cost invariant does not invalidate the invariant
   itself, assuming that the invariant generator is correct.
 \item \textbf{Applications to time analysis for modern hardware}
   At the moment, the main drawback of the CerCo Prototype is that it cannot be
   ported to modern architectures whose instruction cost depend on the internal
   state of hardware components like pipelines, caches or branch predictors.
   The major long term improvement to the CerCo Prototype will be the study
   of how to accommodate in the labelling approach these kind of cost models.
   We attach to this document the technical report ``\emph{Dependent labelling
   applied to stateful hardware components}'' which describes what seems to
   be at the moment the most promising approach to the problem. Unsurprisingly,
   the solution uses dependent labels, that allow to associate a different cost
   to multiple executions of the same block. Dependent labels were developed
   in CerCo to allow loop optimizations, where the dependency was over the
   number of iterations of the loops. In the case of modern hardware, the
   dependency is on approximations of the internal hardware state, that needs
   to be made manifest in the source code too. 

   The strategy described in the technical report is assumed to work on
   pipelines, while additional research is expected for caches. Moreover, in
   the middle term we need to be implement the solution for pipelines to be
   able to perform experiments. In particular, we need to understand the
   behaviour on automated provers on the more complex generated cost invariants,
   and we need to understand to which extent the cost invariants can work with
   the more precise cost models before introducing severe approximations. 
\end{enumerate}

\newpage

\includepdf[pages={-}]{pipelines.pdf}

\end{document}