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

Last change on this file since 3267 was 3210, checked in by sacerdot, 7 years ago

Final version.

File size: 23.0 KB
Line 
1\documentclass[11pt, epsf, a4wide]{article}
2
3\usepackage{../style/cerco}
4\usepackage{pdfpages}
5
6\usepackage{amsfonts}
7\usepackage{amsmath}
8\usepackage{amssymb} 
9\usepackage[english]{babel}
10\usepackage{graphicx}
11\usepackage[utf8x]{inputenc}
12\usepackage{listings}
13\usepackage{stmaryrd}
14\usepackage{url}
15\usepackage{bbm}
16
17% Amadio's macros
18\newcommand{\cost}{{\sf Cost}}
19\newcommand{\lamcost}{\sf LamCost}
20\newcommand{\cil}{{\sf CIL}}
21\newcommand{\scade}{{\sf Scade}}
22\newcommand{\absint}{{\sf AbsInt}}
23\newcommand{\framac}{{\sf Frama-C}}
24\newcommand{\acsl}{{\sf {ACSL}}}
25\newcommand{\jessie}{{\sf {Jessie}}}
26\newcommand{\powerpc}{{\sf PowerPc}}
27\newcommand{\lustre}{{\sf Lustre}}
28\newcommand{\esterel}{{\sf Esterel}}
29\newcommand{\ml}{{\sf ML}}
30\newcommand{\altergo}{{\sf {Alt-Ergo}}}
31\newcommand{\why}{{\sf {Why}}}
32\newcommand{\old}{\backslash old}
33\newcommand{\C}{{\sf C}}
34\newcommand{\coq}{{\sf Coq}}
35\newcommand{\ocaml}{{\sf ocaml}}
36\newcommand{\AND}{\wedge}               % conjunction
37\newcommand{\w}[1]{{\it #1}}    %To write in math style
38
39\title{
40INFORMATION AND COMMUNICATION TECHNOLOGIES\\
41(ICT)\\
42PROGRAMME\\
43\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
44
45\lstdefinelanguage{matita-ocaml}
46  {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try},
47   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
48   morekeywords={[3]type,of},
49   mathescape=true,
50  }
51
52\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
53        keywordstyle=\color{red}\bfseries,
54        keywordstyle=[2]\color{blue},
55        keywordstyle=[3]\color{blue}\bfseries,
56        commentstyle=\color{green},
57        stringstyle=\color{blue},
58        showspaces=false,showstringspaces=false}
59
60\lstset{extendedchars=false}
61\lstset{inputencoding=utf8x}
62\DeclareUnicodeCharacter{8797}{:=}
63\DeclareUnicodeCharacter{10746}{++}
64\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
65\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
66
67\date{}
68\author{}
69
70\begin{document}
71
72\thispagestyle{empty}
73
74\vspace*{-1cm}
75\begin{center}
76\includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
77\end{center}
78
79\begin{minipage}{\textwidth}
80\maketitle
81\end{minipage}
82
83\vspace*{0.5cm}
84\begin{center}
85\begin{LARGE}
86\textbf{
87Report n. D6.3\\
88Final Report on User Validation}
89\end{LARGE} 
90\end{center}
91
92\vspace*{2cm}
93\begin{center}
94\begin{large}
95Version 1.0
96\end{large}
97\end{center}
98
99\vspace*{0.5cm}
100\begin{center}
101\begin{large}
102Main Authors:\\
103Roberto M.~Amadio, Gabriele Pulcini, Claudio Sacerdoti Coen
104%Dominic P. Mulligan and Claudio Sacerdoti Coen
105\end{large}
106\end{center}
107
108\vspace*{\fill}
109
110\noindent
111Project Acronym: \cerco{}\\
112Project full title: Certified Complexity\\
113Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
114
115\clearpage
116\pagestyle{myheadings}
117\markright{\cerco{}, FP7-ICT-2009-C-243881}
118
119\newpage
120
121\vspace*{7cm}
122\paragraph{Abstract}
123We review the techniques experimented in CerCo for cost annotation exploitment
124at the user level. We also report on recent work towards precise time analysis
125at the source level for modern hardware architectures whose instructions cost
126is a function of the internal hardware state (pipelines, caches, branch
127prediction units, etc.).
128
129\newpage
130
131\tableofcontents
132
133\newpage
134
135\section{Task}
136\label{sect.task}
137
138The Grant Agreement describes deliverable D6.3 as follows:
139\begin{quotation}
140\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.
141
142\end{quotation}
143
144\newpage
145
146
147\section{Review of cost synthesis techniques}
148We review the {\em cost synthesis techniques} developed in the project.
149
150The {\em starting hypothesis} is that we have a certified methodology
151to annotate `blocks' in the source code with constants which provide
152a sound and possibly precise upper bound on the cost of executing the
153`blocks' after compilation to binary code.
154
155The {\em principle} that we have followed in designing the cost synthesis
156tools is that the synthetic bounds should be expressed and proved within
157a general purpose tool built to reason on the source code.
158In particular, we rely on the $\framac$ tool to reason on $\C$ code and on the $\coq$ 
159proof-assistant to reason on higher-order functional programs.
160
161This principle entails that:
162
163\begin{itemize}
164
165\item The inferred synthetic bounds are indeed {\em correct}
166as long as the general purpose tool is.
167
168\item There is {\em no limitation on the  class of programs} that can be handled
169as long as the user is willing to carry on an interactive proof.
170
171\end{itemize}
172
173Of course, {\em automation} is desirable whenever possible.  Within this
174framework, automation means writing programs that give hints to the
175general purpose tool. These hints may take the form, say, of loop
176invariants/variants, of predicates describing the structure of the heap,
177or of types in a light logic.  If these hints are
178correct and sufficiently precise the general purpose tool will produce
179a proof automatically, otherwise, user interaction is required.  What
180follows is a summary of work described in more detail in deliverables
181D5.1 and D5.3. The cost synthesis techniques we outline are at
182varying degree of maturity ranging from a complete experimental
183validation to preliminary thought experiments.
184
185
186\subsection{The $\cost$ plug-in and its application to the Lustre compiler}
187$\framac$ is a set of analysers for $\C$ programs with a specification language
188called $\acsl$. New analyses can be dynamically added through a plug-in
189system. For instance, the $\jessie$ plug-in allows deductive verification of
190$\C$ programs with respect to their specification in $\acsl$, with various
191provers as back-end tools.
192
193We developed the $\cost$ plug-in for the $\framac$ platform as a proof of
194concept of an automatic environment exploiting the cost annotations produced by
195the $\cerco$ compiler. It consists of an $\ocaml$ program
196which in first approximation takes the following actions: (1) it receives as
197input a $\C$ program, (2) it applies the $\cerco$ compiler to produce a related
198$\C$ program with cost annotations, (3) it applies some heuristics to produce a
199tentative bound on the cost of executing the $\C$ functions of the program as a
200function of the value of their parameters, (4) the user can then call the
201$\jessie$ tool to discharge the related proof
202obligations.  %\marginpar{Some facts/pointer to Cost tool.}
203
204In the following we elaborate on the soundness of the framework
205and the experiments we performed with the $\cost$ tool
206on the $\C$ programs produced by a $\lustre$ compiler.
207
208
209
210% First, the input file is fed to
211% $\framac$ that will in turn send it to the $\cost$ plug-in. The action of the
212% plug-in is then:
213% \begin{enumerate}
214% \item apply the $\cerco$ compiler to the source file;
215% \item synthesize an upper bound of the WCET of each function of the source
216%   program by reading the cost annotations added by $\cerco$;
217% \item add the results in the form of post-conditions in $\acsl$ format, relating
218%   the cost of the function before and after its execution.
219% \end{enumerate}
220
221\paragraph{Soundness}
222The soundness of the whole framework depends on the cost annotations
223added by the $\cerco$ compiler, the synthetic costs produced by the $\cost$
224plug-in, the verification conditions (VCs) generated by $\jessie$, and
225the external provers discharging the VCs.  The synthetic costs being
226in $\acsl$ format, $\jessie$ can be used to verify them.
227%RA There was a confusion between basic cost annotations and synthetic costs.
228Thus, even if the added synthetic costs are incorrect (relatively to the cost annotations),
229the process in its globality is still correct: indeed, $\jessie$ will not validate
230incorrect costs and no conclusion can be made about the WCET of
231the program in this case. In other terms, the soundness does not really depend on the action
232of the $\cost$ plug-in, which can in principle produce \emph{any}
233synthetic cost. However, in order to be able to actually prove a WCET of a
234$\C$ function, we need to add correct annotations in a way that $\jessie$
235and subsequent automatic provers have enough information to deduce
236their validity. In practice this is not straightforward
237even for very simple programs composed of branching and assignments
238(no loops and no recursion) because a fine analysis of the VCs associated with
239branching may lead to a complexity blow up.
240
241\paragraph{Experience with $\lustre$}
242$\lustre$ is a data-flow language to program
243synchronous systems and the language comes with a compiler to
244$\C$.
245We designed a wrapper for supporting $\lustre$ files.
246The $\C$ function produced by the compiler implements the {\em step function}
247of the synchronous system and computing the WCET of the function amounts to obtain
248a bound on the reaction time of the system.
249We tested the  $\cost$ plug-in and the $\lustre$ wrapper on the $\C$ programs generated by the
250$\lustre$ compiler. For programs consisting of a few hundreds loc,
251the $\cost$ plug-in computes a WCET and $\altergo$ is able to discharge all VCs
252automatically.
253
254
255
256
257\subsection{Handling $\C$ programs with simple loops}
258The cost annotations added by the $\cerco$ compiler take the form of $\C$
259instructions that update by a constant a fresh global variable called the
260\emph{cost variable}. Synthesizing a WCET of a $\C$ function thus consists in
261statically resolving an upper bound of the difference between the value of the
262cost variable before and after the execution of the function, {\em i.e.} find in the
263function the instructions that update the cost variable and establish the number
264of times they are passed through during the flow of execution. In
265order to do the analysis the plugin makes the following assumptions on the programs:
266\begin{itemize}
267\item No recursive functions.
268\item Every loop must be annotated with a {\em variant}. The
269  variants of `for' loops are automatically inferred.
270\end{itemize}
271
272The plugin proceeds as follows.
273
274\begin{itemize}
275
276\item 
277First the callgraph of the program is computed.
278If the function $f$ calls the function $g$ then the function $g$ is processed before the function $f$.
279
280\item The computation of the cost of the function is performed by traversing its control flow graph.
281The cost at a node is the maximum of the costs of the successors.
282%If the node is an assignment it is substituted in the cost in  the same way as for weakest-precondition.
283
284\item In the case of a loop with a body that has a constant cost for
285  every step of the loop, the cost is the product of the cost of the
286  body and of the variant taken at the start of the loop.
287
288\item In the case of a loop with a body whose cost depends on
289  the values of some free variables, a fresh logic function $f$ is
290  introduced to represent the cost of the loop in the logic
291  assertions. This logic function takes the variant as a first
292  parameter. The other parameters of $f$ are the free variables of the
293  body of the loop.  An axiom is added to account the fact that the
294  cost is accumulated at each step of the loop:
295  \[
296  f(v, \vec x) =
297    \textrm{if } v < 0 \textrm{ then } 0 \textrm{ else } (f(v-1, \phi(\vec x)) + \psi(\vec x))
298  \]
299  where $\vec x$ are the free variables, $v$ is the variant, $\phi$ computes the
300  modification of the variable at each step of the loop, and $\psi$ is the
301  cost of the body of the loop.
302
303\item The cost of the function is directly added as post-condition of
304  the function: $\_\_cost \le \old(\_\_cost) + t$ where $t$ is the term
305  computing the cost of the function, $\_\_cost$ is the time taken from
306  the start of the program, $\old(\_\_cost)$ is the same time but before
307  the execution of the function.
308\end{itemize}
309
310
311The user can influence the annotation by different means:
312\begin{itemize}
313\item By using more precise variants.
314\item By annotating function with cost specification. The plugin will
315  use this cost for the function instead of computing it.
316\end{itemize}
317
318
319
320
321\subsection{$\C$ programs with pointers}
322When it comes to verifying programs involving pointer-based data
323structures, such as linked lists, trees, or graphs, the use of
324traditional first-order logic to specify, and of SMT solvers to
325verify, shows some limitations. {\em Separation logic} is then an
326elegant alternative. Designed at the turn of the century, it is a
327program logic with a new notion of conjunction to express spatial
328heap separation.  Separation logic has been implemented in dedicated theorem provers
329such as {\sf Smallfoot} or {\sf VeriFast}. One
330drawback of such provers, however, is to either limit the
331expressiveness of formulas (e.g. to the so-called symbolic heaps), or
332to require some user-guidance (e.g. open/close commands in Verifast).
333
334In an attempt to conciliate both approaches, Bobot introduced the
335notion of separation predicates during his PhD thesis. The approach
336consists in reformulating some ideas from separation logic into a
337traditional verification framework where the specification language,
338the verification condition generator, and the theorem provers were not
339designed with separation logic in mind. Separation predicates are
340automatically derived from user-defined inductive predicates, on
341demand. Then they can be used in program annotations, exactly as other
342predicates, {\em i.e.}, without any constraint. Simply speaking, where
343one would write $P*Q$ in separation logic, one will here ask for the
344generation of a separation predicate {\em sep} and then use it as $P
345\AND Q \AND \w{sep}(P, Q)$.  We have implemented separation predicates
346within the $\jessie$ plug-in and tested it on a non-trivial case study
347(the composite pattern from the VACID-0 benchmark).  In this case, we
348achieve a fully automatic proof using three existing SMT solver. We
349have also used the separation predicates to reason on the {\em cost}
350of executing simple heap manipulating programs such as an in-place
351list reversal.
352
353
354
355\subsection{The cost of higher-order functional programs}
356We have analysed a rather standard compilation chain from
357a higher-order functional languages to an abstract
358{\sf RTL} language which corresponds directly to the source
359language of the back-end of the $\C$ compiler developed in the $\cerco$ project.
360The compilation consists of four transformations: continuation passing-style,
361value naming, closure conversion, and hoisting.
362
363We have shown that it is possible to extend the labelling approach
364described for the $\C$ language to a higher-order call-by-value functional language.
365
366The first issue we have considered is that of designing a `good
367labelling' function, {\em i.e.}, a function that inserts labels in the
368source code which correspond to `basic blocks' of the compiled
369code. To this end, we have introduced two labelling operators: a
370{\em pre-labelling} $\ell>M$ which emits the label $\ell$ before running $M$
371and a {\em post-labelling} $M>\ell$ which reduces $M$ to a value and then
372emits the label $\ell$.  Roughly speaking, the `good labelling'
373associates a pre-labelling to every function abstraction and a
374post-labelling to every application which is not immediately
375surrounded by an abstraction.  In particular, the post-labelling
376takes care of the functions created by the CPS translation.
377
378The second issue relates to the instrumentation of the program.
379To this end, we have relied on a {\em cost monad} which associates
380to each program a pair consisting of its denotation and the
381cost of reducing the program to a value.
382In this way, the instrumented program can still be regarded
383as a higher-order functional program.
384
385The third issue concerns the method to {\em reason on the instrumented
386(functional) program}. We have built on a higher-order Hoare logic and a related tool
387that generates automatically the proof obligations. These proof
388obligations can either be discharged automatically or
389interactively using the {\sf Coq} proof assistant and its tactics.
390Some simple experiments are described in the $\lamcost$ software.
391
392
393\subsection{The cost of memory management}
394In a realistic implementation of a functional programming language,
395the runtime environment usually includes a garbage collector.  In
396spite of considerable progress in {\em real-time garbage
397  collectors}  it seems to us that
398such collectors do not offer yet a viable path to a certified and
399usable WCET prediction of the running time of functional programs.
400As far as we know, the cost predictions concern the {\em amortized case}
401rather than the {\em worst case} and are supported more by experimental evaluations
402than by formal proofs.
403
404The approach we have adopted instead, following the seminal work
405of  Tofte {\em et al.}, is to enrich the last calculus of
406the compilation chain : (1) with a notion
407of {\em memory region}, (2) with operations to allocate and dispose
408memory regions, and (3) with a {\em type and effect system} that guarantees
409the safety of the dispose operation. This allows to further extend
410the compilation chain mentioned above and then to include the cost
411of safe memory management in our analysis. Actually, because effects are intertwined with types,
412what we have actually done, following the work of Morrisett {\em et al.}
413is to extend a {\em typed} version of the compilation chain.
414An experimental validation of the approach is left for future work and it
415would require the integration  of region-inference algorithms such as those
416developed by Aiken {\em et al.} in the compilation chain.
417
418
419
420
421\subsection{Feasible bounds by light typing}
422In our experience, the cost analysis of higher-order programs requires
423human intervention both at the level of the specification and of the
424proofs.
425One path to automation consists in devising programming disciplines
426that entail feasible bounds (polynomial time). The most interesting approaches to this problem
427build on {\em light} versions of linear logic.
428Our main contribution is to devise a type system that guarantees feasible
429bounds for a higher-order call-by-value functional language with
430references and threads.
431The first proof of this result  relies on a kind of standardisation theorem and it is of a combinatorial nature.
432More recently, we have shown that a proof of a similar result can be obtained
433by semantic means building on the so called {\em quantitative realizability
434models} proposed by Dal Lago and Hofmann.
435We believe this semantic setting is  particularly appropriate because
436it allows to reason both on typed and untyped programs.
437Thus one can imagine a framework where some programs are feasible `by typing'
438while others are feasible as a result of an `interactive proof' of the obligations
439generated by quantitative realizability.
440Beyond building such a framework, an interesting issue concerns the
441certification of {\em concrete bounds} at the level of the {\em compiled code}.
442This has to be contrasted with the current state of the art in implicit computational complexity
443where most bounds are {\em asymptotic} and are stated at the level of the {\em source code}.
444
445
446\section{Middle and Long Term Improvements}
447The future improvements that will affect the user experience falls into two
448categories:
449\begin{enumerate}
450 \item \textbf{Improvements to invariant generators}
451   The invariant generator that we implemented in the plug-in allows to
452   compute the parametric worst case execution time for all Lustre programs
453   and for almost all the C tests that we targeted. Nevertheless, at the
454   moment the generator does not degrade gracefully: if the source code does
455   not respects the syntactic requirements of the generator, no cost invariants
456   are generated at all. This behaviour is consistent with the traditional
457   use in proving functional properties, but for non functional ones we
458   are interested in always providing a worst case bound, possibly by dropping
459   the dependencies and computing a very rough one. That is the behaviour of
460   standard WCET analyzers (that, most of the time, are not parametric anyway).
461
462   Other future improvements consist in enlarging the class of recognized
463   program shapes by integrating more advanced techniques or interacting with
464   existing tools.
465
466   Both kind of improvements can be performed in the middle term.
467 \item \textbf{Improvements to cost annotation exploitment}
468   One benefit of CerCo w.r.t. traditional WCET is that the user does not need
469   to trust the bound provided by the tool, but it can at least partially
470   verify it manually or using automated techniques.
471
472   The combinations of techniques described in the previous section allowed
473   to automatically certify the parametric worst case execution time for all
474   Lustre programs and for the majority of simple C tests we had at our
475   disposal. Nevertheless, we expect automation to fail more frequently on
476   real world, industrial examples. In the middle term we should experiment
477   with more complex code and enlarge the set of techniques according to the
478   observed results. In particular, we should implement at the source level
479   at least all those that are used on the object code in standard WCET tools.
480   It may well be the case that we identify a set of recurrent proof obligations
481   that are not solved by the existing theorem provers, but that admit a
482   solution by means of a uniform strategy. In any case, the failure to
483   automatically prove sound a cost invariant does not invalidate the invariant
484   itself, assuming that the invariant generator is correct.
485 \item \textbf{Applications to time analysis for modern hardware}
486   At the moment, the main drawback of the CerCo Prototype is that it cannot be
487   ported to modern architectures whose instruction cost depend on the internal
488   state of hardware components like pipelines, caches or branch predictors.
489   The major long term improvement to the CerCo Prototype will be the study
490   of how to accommodate in the labelling approach these kind of cost models.
491   We attach to this document the technical report ``\emph{Dependent labelling
492   applied to stateful hardware components}'' which describes what seems to
493   be at the moment the most promising approach to the problem. Unsurprisingly,
494   the solution uses dependent labels, that allow to associate a different cost
495   to multiple executions of the same block. Dependent labels were developed
496   in CerCo to allow loop optimizations, where the dependency was over the
497   number of iterations of the loops. In the case of modern hardware, the
498   dependency is on approximations of the internal hardware state, that needs
499   to be made manifest in the source code too.
500
501   The strategy described in the technical report is assumed to work on
502   pipelines, while additional research is expected for caches. Moreover, in
503   the middle term we need to be implement the solution for pipelines to be
504   able to perform experiments. In particular, we need to understand the
505   behaviour on automated provers on the more complex generated cost invariants,
506   and we need to understand to which extent the cost invariants can work with
507   the more precise cost models before introducing severe approximations.
508\end{enumerate}
509
510\newpage
511
512\includepdf[pages={-}]{pipelines.pdf}
513
514\end{document}
Note: See TracBrowser for help on using the repository browser.