source: Papers/fopara2013/fopara13.tex @ 3425

Last change on this file since 3425 was 3425, checked in by campbell, 6 years ago

Rearrange section 4

File size: 63.7 KB
Line 
1\documentclass{llncs}
2
3\usepackage{amsfonts}
4\usepackage{amsmath}
5\usepackage{amssymb} 
6\usepackage[english]{babel}
7\usepackage{color}
8\usepackage{fancybox}
9\usepackage{fancyvrb}
10\usepackage{graphicx}
11\usepackage[colorlinks,
12            bookmarks,bookmarksopen,bookmarksdepth=2]{hyperref}
13\usepackage{hyphenat}
14\usepackage[utf8x]{inputenc}
15\usepackage{listings}
16\usepackage{mdwlist}
17\usepackage{microtype}
18\usepackage{stmaryrd}
19\usepackage{url}
20
21\usepackage{tikz}
22\usetikzlibrary{positioning,calc,patterns,chains,shapes.geometric,scopes}
23
24%\renewcommand{\verb}{\lstinline}
25%\def\lstlanguagefiles{lst-grafite.tex}
26%\lstset{language=Grafite}
27\lstset{language=C,basewidth=.5em,lineskip=-2pt}
28
29\newlength{\mylength}
30\newenvironment{frametxt}%
31        {\setlength{\fboxsep}{5pt}
32                \setlength{\mylength}{\linewidth}%
33                \addtolength{\mylength}{-2\fboxsep}%
34                \addtolength{\mylength}{-2\fboxrule}%
35                \Sbox
36                \minipage{\mylength}%
37                        \setlength{\abovedisplayskip}{0pt}%
38                        \setlength{\belowdisplayskip}{0pt}%
39                }%
40                {\endminipage\endSbox
41                        \[\fbox{\TheSbox}\]}
42
43\title{Certified Complexity (CerCo)\thanks{The project CerCo acknowledges the
44financial support of the Future and Emerging Technologies (FET) programme within
45the Seventh Framework Programme for Research of the European Commission, under
46FET-Open grant number: 243881}}
47\author{
48%Roberto
49R.~M. Amadio$^{4}$ \and
50%Nicolas
51N.~Ayache$^{3,4}$ \and
52%François
53F.~Bobot$^{3,4}$ \and
54%Jacob
55J.~P. Boender$^1$ \and
56%Brian
57B.~Campbell$^2$ \and
58%Ilias
59I.~Garnier$^2$ \and
60%Antoine
61A.~Madet$^4$ \and
62%James
63J.~McKinna$^2$ \and
64%Dominic
65D.~P. Mulligan$^1$ \and
66%Mauro
67M.~Piccolo$^1$ \and
68%Randy
69R.~Pollack$^2$ \and
70%Yann
71Y.~R\'egis-Gianas$^{3,4}$ \and
72%Claudio
73C.~Sacerdoti Coen$^1$ \and
74%Ian
75I.~Stark$^2$ \and
76%Paolo
77P.~Tranquilli$^1$}
78\institute{Dipartimento di Informatica - Scienza e Ingegneria, Universit\'a di
79Bologna \and
80LFCS, School of Informatics, University of Edinburgh
81\and INRIA (Team $\pi$r2 )
82\and
83Universit\`e Paris Diderot
84}
85
86\bibliographystyle{splncs03}
87
88\begin{document}
89
90\maketitle
91
92% Brian: I've changed "without loss of accuracy" because we discuss
93% important precision/complexity tradeoffs for advanced architectures
94% in the dependent labelling section.
95\begin{abstract}
96This paper provides an overview of the FET-Open Project CerCo
97(`Certified Complexity'). The project's main achievement is
98the development of a technique for analysing non-functional
99properties of programs (time, space) at the source level, with little or no loss of accuracy
100and with a small, trusted code base. The main software component
101developed is a certified compiler producing cost annotations. The compiler
102translates source code to object code and produces an instrumented copy of the
103source code. This instrumentation exposes at
104the source level---and tracks precisely---the actual (non-asymptotic)
105computational cost of the input program. Untrusted invariant generators and trusted theorem provers
106can then be used to compute and certify the parametric execution time of the
107code.
108\end{abstract}
109
110% ---------------------------------------------------------------------------- %
111% SECTION                                                                      %
112% ---------------------------------------------------------------------------- %
113\section{Introduction}
114
115\paragraph{Problem statement.} Computer programs can be specified with both
116functional constraints (what a program must do) and non-functional constraints
117(e.g. what resources---time, space, etc.---the program may use).  In the current
118state of the art, functional properties are verified for high-level source code
119by combining user annotations (e.g. preconditions and invariants) with a
120multitude of automated analyses (invariant generators, type systems, abstract
121interpretation, theorem proving, and so on). By contrast, non-functional properties
122are generally checked on low-level object code, but also demand information
123about high-level functional behaviour that must somehow be recreated.
124
125This situation presents several problems: 1) it can be hard to infer this
126high-level structure in the presence of compiler optimisations; 2) techniques
127working on object code are not useful in early development, yet problems
128detected later are more expensive to tackle; 3) parametric cost analysis is very
129hard: how can we reflect a cost that depends on the execution state (e.g. the
130value of a register or a carry bit) to a cost that the user can understand
131looking at source code? 4) functional analysis performed only on object code
132makes any contribution from the programmer hard, leading to less precision in
133the estimates.
134
135\paragraph{Vision and approach.} We want to reconcile functional and
136non-functional analyses: to share information and perform both at the same time
137on source code.
138%
139What has previously prevented this approach is the lack of a uniform and precise
140cost model for high-level code: 1) each statement occurrence is compiled
141differently and optimisations may change control flow; 2) the cost of an object
142code instruction may depend on the runtime state of hardware components like
143pipelines and caches, all of which are not visible in the source code.
144
145To solve the issue, we envision a new generation of compilers able to keep track
146of program structure through compilation and optimisation, and to exploit that
147information to define a cost model for source code that is precise, non-uniform,
148and accounts for runtime state. With such a source-level cost model we can
149reduce non-functional verification to the functional case and exploit the state
150of the art in automated high-level verification~\cite{survey}. The techniques
151currently used by the Worst Case Execution Time (WCET) community, which perform the analysis on object code,
152are still available but can now be coupled with an additional source-level
153analysis. Where the approach produces precise cost models too complex to reason
154about, safe approximations can be used to trade complexity with precision.
155Finally, source code analysis can be made during early development stages, when
156components have been specified but not implemented: source code modularity means
157that it is enough to specify the non-functional behaviour of unimplemented
158components.
159
160\paragraph{Contributions.} We have developed what we refer to as \emph{the labeling approach} \cite{labeling}, a
161technique to implement compilers that induce cost models on source programs by
162very lightweight tracking of code changes through compilation. We have studied
163how to formally prove the correctness of compilers implementing this technique.
164We have implemented such a compiler from C to object binaries for the 8051
165micro-controller, and verified it in an interactive theorem prover. We have
166implemented a Frama-C plugin \cite{framac} that invokes the compiler on a source
167program and uses this to generate invariants on the high-level source that
168correctly model low-level costs. Finally, the plugin certifies that the program
169respects these costs by calling automated theorem provers, a new and innovative
170technique in the field of cost analysis. As a case study, we show how the
171plugin can automatically compute and certify the exact reaction time of Lustre
172\cite{lustre} data flow programs compiled into C.
173
174\section{Project context and objectives}
175Formal methods for verification of functional properties of programs have
176now reached a level of maturity and automation that is facilitating a slow but
177increasing adoption in production environments. For safety critical code, it is
178becoming commonplace to combine rigorous software engineering methodologies and testing
179with static analysis, taking the strong points of each approach and mitigating
180their weaknesses. Of particular interest are open frameworks
181for the combination of different formal methods, where the programs can be
182progressively specified and are continuously enriched with new safety
183guarantees: every method contributes knowledge (e.g. new invariants) that
184becomes an assumption for later analysis.
185
186The scenario for the verification of non-functional properties (time spent,
187memory used, energy consumed) is bleaker and the future seems to be getting even
188worse. Most industries verify that real time systems meet their deadlines
189by simply performing many runs of the system and timing their execution,  computing the
190maximum time and adding an empirical safety margin, claiming the result to be a
191bound for the WCET of the program. Formal methods and software to statically
192analyse the WCET of programs exist, but they often produce bounds that are too
193pessimistic to be useful. Recent advancements in hardware architectures are all
194focused on the improvement of the average case performance, not the
195predictability of the worst case. Execution time is becoming increasingly
196dependent on execution history and the internal state of
197hardware components like pipelines and caches. Multi-core processors and non-uniform
198memory models are drastically reducing the possibility of performing
199static analysis in isolation, because programs are less and less time
200composable. Clock-precise hardware models are necessary for static analysis, and
201obtaining them is becoming harder as a consequence of the increased sophistication
202of hardware design.
203
204Despite the aforementioned problems, the need for reliable real time systems and programs is
205increasing, and there is increasing pressure from the research community towards
206the differentiation of hardware. The aim is to introduce alternative
207hardware with more predictable behaviour and hence more suitability for static
208analyses, for example, the decoupling of execution time from execution history
209by introducing randomisation \cite{proartis}.
210
211In the CerCo project \cite{cerco} we do not try to address this problem, optimistically
212assuming that static analysis of non-functional properties of programs will
213become feasible in the longer term. The main objective of our work is
214instead to bring together static analysis of functional and non-functional
215properties, which, according to the current state of the art, are completely
216independent activities with limited exchange of information: while the
217functional properties are verified on the source code, the analysis of
218non-functional properties is entirely performed on the object code to exploit
219clock-precise hardware models.
220
221\subsection{Current object-code methods}
222
223Analysis currently takes place on object code for two main reasons.
224First, there cannot be a uniform, precise cost model for source
225code instructions (or even basic blocks). During compilation, high level
226instructions are torn apart and reassembled in context-specific ways so that
227identifying a fragment of object code and a single high level instruction is
228infeasible. Even the control flow of the object and source code can be very
229different as a result of optimisations, for example aggressive loop
230optimisations may completely transform source level loops. Despite the lack of a uniform, compilation- and
231program-independent cost model on the source language, the literature on the
232analysis of non-asymptotic execution time on high level languages that assumes
233such a model is growing and gaining momentum. However, unless we can provide a
234replacement for such cost models, this literature's future practical impact looks
235to be minimal. Some hope has been provided by the EmBounded project \cite{embounded}, which
236compositionally compiles high-level code to a byte code that is executed by an
237emulator with guarantees on the maximal execution time spent for each byte code
238instruction. That approach provides a uniform model at the price of the model's
239precision (each cost is a pessimistic upper bound) and performance of the
240executed code (because the byte code is emulated  compositionally instead of
241performing a fully non-compositional compilation).
242
243The second reason to perform the analysis on the object code is that bounding
244the worst case execution time of small code fragments in isolation (e.g. loop
245bodies) and then adding up the bounds yields very poor estimates because no
246knowledge on the hardware state can be assumed when executing the fragment. By
247analysing longer runs the bound obtained becomes more precise because the lack
248of knowledge on the initial state has less of an effect on longer computations.
249
250The cost of an execution is the sum of the cost of basic blocks multiplied by
251the number of times they are executed, which is a functional property of the
252program. Therefore, in order to perform (parametric) time analysis of programs,
253it is necessary to combine a cost model with control and data flow analysis.
254Current state of the art WCET technology
255\cite{stateart} performs the analysis on the object code, where the logic of the
256program is harder to reconstruct and most information available at the source
257code level has been lost. Imprecision in the analysis leads to useless bounds. To
258augment precision, the tools ask the user to provide constraints on the object
259code control flow, usually in the form of bounds on the number of iterations of
260loops or linear inequalities on them. This requires the user to manually link
261the source and object code, translating his assumptions on the source code
262(which may be wrong) to object code constraints. The task is error prone and
263hard, especially in the presence of complex compiler optimisations.
264
265Traditional techniques for WCET that work on object code are also affected by
266another problem: they cannot be applied before the generation of the object
267code. Functional properties can be analysed in early development stages, while
268analysis of non-functional properties may come too late to avoid expensive
269changes to the program architecture.
270
271\subsection{CerCo}
272
273In CerCo we propose a radically new approach to the problem: we reject the idea
274of a uniform cost model and we propose that the compiler, which knows how the
275code is translated, must return the cost model for basic blocks of high level
276instructions. It must do so by keeping track of the control flow modifications
277to reverse them and by interfacing with static analysers.
278
279By embracing compilation, instead of avoiding it like EmBounded did, a CerCo
280compiler can at the same time produce efficient code and return costs that are
281as precise as the static analysis can be. Moreover, we allow our costs to be
282parametric: the cost of a block can depend on actual program data or on a
283summary of the execution history or on an approximated representation of the
284hardware state. For example, loop optimizations may assign to a loop body a cost
285that is a function of the number of iterations performed. As another example,
286the cost of a block may be a function of the vector of stalled pipeline states,
287which can be exposed in the source code and updated at each basic block exit. It
288is parametricity that allows one to analyse small code fragments without losing
289precision: in the analysis of the code fragment we do not have to ignore the
290initial hardware state. On the contrary, we can assume that we know exactly which
291state (or mode, as the WCET literature calls it) we are in.
292
293The CerCo approach has the potential to dramatically improve the state of the
294art. By performing control and data flow analyses on the source code, the error
295prone translation of invariants is completely avoided. It is in fact performed
296by the compiler itself when it induces the cost model on the source language.
297Moreover, any available technique for the verification of functional properties
298can be immediately reused and multiple techniques can collaborate together to
299infer and certify cost invariants for the program. Parametric cost analysis
300becomes the default one, with non parametric bounds used as last resorts when
301trading the complexity of the analysis with its precision. \emph{A priori}, no
302technique previously used in traditional WCET is lost: they can just be applied
303at the source code level.
304 Our approach can also work in the early
305stages of development by axiomatically attaching costs to unimplemented components.
306
307
308All software used to verify properties of programs must be as bug free as
309possible. The trusted code base for verification is made by the code that needs
310to be trusted to believe that the property holds. The trusted code base of
311state-of-the-art WCET tools is very large: one needs to trust the control flow
312analyser and the linear programming libraries it uses and also the formal models
313of the hardware. In CerCo we are moving the control flow analysis to the source
314code and we are introducing a non-standard compiler too. To reduce the trusted
315code base, we implemented a prototype and a static analyser in an interactive
316theorem prover, which was used to certify that the cost computed on the source
317code is indeed the one actually spent by the hardware. Formal models of the
318hardware and of the high level source languages were also implemented in the
319interactive theorem prover. Control flow analysis on the source code has been
320obtained using invariant generators, tools to produce proof obligations from
321generated invariants and automatic theorem provers to verify the obligations. If
322the automatic provers are able to generate proof traces that can be
323independently checked, the only remaining component that enters the trusted code
324base is an off-the-shelf invariant generator which, in turn, can be proved
325correct using an interactive theorem prover. Therefore we achieve the double
326objective of allowing the use of more off-the-shelf components (e.g. provers and
327invariant generators) whilst reducing the trusted code base at the same time.
328
329%\paragraph{Summary of the CerCo objectives.} To summarize, the goal of CerCo is
330% to reconcile functional with non-functional analysis by performing them together
331% on the source code, sharing common knowledge about execution invariants. We want
332% to achieve the goal implementing a new generation of compilers that induce a
333% parametric, precise cost model for basic blocks on the source code. The compiler
334% should be certified using an interactive theorem prover to minimize the trusted
335% code base of the analysis. Once the cost model is induced, off-the-shelf tools
336% and techniques can be combined together to infer and prove parametric cost
337% bounds.
338%The long term benefits of the CerCo vision are expected to be:
339%1. the possibility to perform static analysis during early development stages
340%2.  parametric bounds made easier
341%3.  the application of off-the-shelf techniques currently unused for the
342% analysis of non-functional properties, like automated proving and type systems
343%4. simpler and safer interaction with the user, that is still asked for
344% knowledge, but on the source code, with the additional possibility of actually
345% verifying the provided knowledge
346%5. a reduced trusted code base
347%6. the increased accuracy of the bounds themselves.
348%
349%The long term success of the project is hindered by the increased complexity of
350% the static prediction of the non-functional behaviour of modern hardware. In the
351% time frame of the European contribution we have focused on the general
352% methodology and on the difficulties related to the development and certification
353% of a cost model inducing compiler.
354
355\section{The typical CerCo workflow}
356\begin{figure}[!t]
357\begin{tabular}{l@{\hspace{0.2cm}}|@{\hspace{0.2cm}}l}
358\begin{lstlisting}
359char a[] = {3, 2, 7, 14};
360char threshold = 4;
361
362int count(char *p, int len) {
363  char j;
364  int found = 0;
365  for (j=0; j < len; j++) {
366    if (*p <= threshold)
367      found++;
368    p++;
369    }
370  return found;
371}
372
373int main() {
374  return count(a,4);
375}
376\end{lstlisting}
377&
378%  $\vcenter{\includegraphics[width=7.5cm]{interaction_diagram.pdf}}$
379\begin{tikzpicture}[
380    baseline={([yshift=-.5ex]current bounding box)},
381    element/.style={draw, text width=1.6cm, on chain, text badly centered},
382    >=stealth
383    ]
384{[start chain=going below, node distance=.5cm]
385\node [element] (cerco) {CerCo\\compiler};
386\node [element] (cost)  {CerCo\\cost plugin};
387{[densely dashed]
388\node [element] (ded)   {Deductive\\platform};
389\node [element] (check) {Proof\\checker};
390}
391}
392\coordinate [left=3.5cm of cerco] (left);
393{[every node/.style={above, text width=3.5cm, text badly centered,
394                     font=\scriptsize}]
395\draw [<-] ([yshift=-1ex]cerco.north west) coordinate (t) --
396    node {C source}
397    (t-|left);
398\draw [->] (cerco) -- (cost);
399\draw [->] ([yshift=1ex]cerco.south west) coordinate (t) --
400    node {C source+\color{red}{cost annotations}}
401    (t-|left) coordinate (cerco out);
402\draw [->] ([yshift=1ex]cost.south west) coordinate (t) --
403    node {C source+\color{red}{cost annotations}\\+\color{blue}{synthesized assertions}}
404    (t-|left) coordinate (out);
405{[densely dashed]
406\draw [<-] ([yshift=-1ex]ded.north west) coordinate (t) --
407    node {C source+\color{red}{cost annotations}\\+\color{blue}{complexity assertions}}
408    (t-|left) coordinate (ded in) .. controls +(-.5, 0) and +(-.5, 0) .. (out);
409\draw [->] ([yshift=1ex]ded.south west) coordinate (t) --
410    node {complexity obligations}
411    (t-|left) coordinate (out);
412\draw [<-] ([yshift=-1ex]check.north west) coordinate (t) --
413    node {complexity proof}
414    (t-|left) .. controls +(-.5, 0) and +(-.5, 0) .. (out);
415\draw [dash phase=2.5pt] (cerco out) .. controls +(-1, 0) and +(-1, 0) ..
416    (ded in);
417}}
418%% user:
419% head
420\draw (current bounding box.west) ++(-.2,.5)
421    circle (.2) ++(0,-.2) -- ++(0,-.1) coordinate (t);
422% arms
423\draw (t) -- +(-.3,-.2);
424\draw (t) -- +(.3,-.2);
425% body
426\draw (t) -- ++(0,-.4) coordinate (t);
427% legs
428\draw (t) -- +(-.2,-.6);
429\draw (t) -- +(.2,-.6);
430\end{tikzpicture}
431\end{tabular}
432\caption{On the left: code to count the array's elements
433 that are less than or equal to the threshold. On the right: CerCo's interaction
434 diagram. CerCo's components are drawn solid.}
435\label{test1}
436\end{figure}
437We illustrate the workflow we envisage (on the right of~\autoref{test1})
438on an example program (on the left of~\autoref{test1}).
439The user writes the program and feeds it to the CerCo compiler, which outputs
440an instrumented version of the same program that updates global variables
441that record the elapsed execution time and the stack space usage.
442The red lines in \autoref{itest1} are the instrumentation introduced by the
443compiler. The annotated program can then be enriched with complexity assertions
444in the style of Hoare logic, that are passed to a deductive platform (in our
445case Frama-C). We provide as a Frama-C cost plugin a simple automatic
446synthesiser for complexity assertions (the blue lines in \autoref{itest1}),
447which can be overridden by the user to increase or decrease accuracy. From the
448assertions, a general purpose deductive platform produces proof obligations
449which in turn can be closed by automatic or interactive provers, ending in a
450proof certificate.
451
452% NB: if you try this example with the live CD you should increase the timeout
453
454Twelve proof obligations are generated from~\autoref{itest1} (to prove
455that the loop invariant holds after one execution if it holds before,
456to prove that the whole program execution takes at most 1358 cycles,
457etc.).  Note that the synthesised time bound for \lstinline'count',
458$178+214*(1+\lstinline'len')$ cycles, is parametric in the length of
459the array. The CVC3 prover
460closes all obligations within half a minute on routine commodity
461hardware.  A simpler non-parametric version can be solved in a few
462seconds.
463%
464\fvset{commandchars=\\\{\}}
465\lstset{morecomment=[s][\color{blue}]{/*@}{*/},
466        moredelim=[is][\color{blue}]{$}{$},
467        moredelim=[is][\color{red}]{|}{|}}
468\begin{figure}[!p]
469\begin{lstlisting}
470|int __cost = 33, __stack = 5, __stack_max = 5;|
471|void __cost_incr(int incr) { __cost += incr; }|
472|void __stack_incr(int incr) {
473  __stack += incr;
474  __stack_max = __stack_max < __stack ? __stack : __stack_max;
475}|
476
477char a[4] = {3, 2, 7, 14};  char threshold = 4;
478
479/*@ behavior stack_cost:
480      ensures __stack_max <= __max(\old(__stack_max), 4+\old(__stack));
481      ensures __stack == \old(__stack);
482    behavior time_cost:
483      ensures __cost <= \old(__cost)+(178+214*__max(1+\at(len,Pre), 0));
484*/
485int count(unsigned char *p, int len) {
486  char j;  int found = 0;
487  |__stack_incr(4);  __cost_incr(111);|
488  $__l: /* internal */$
489  /*@ for time_cost: loop invariant
490        __cost <= \at(__cost,__l)+
491                  214*(__max(\at((len-j)+1,__l), 0)-__max(1+(len-j), 0));
492      for stack_cost: loop invariant
493        __stack_max == \at(__stack_max,__l);
494      for stack_cost: loop invariant
495        __stack == \at(__stack,__l);
496      loop variant len-j;
497  */
498  for (j = 0; j < len; j++) {
499    |__cost_incr(78);|
500    if (*p <= threshold) { |__cost_incr(136);| found ++; }
501    else { |__cost_incr(114);| }
502    p ++;
503  }
504  |__cost_incr(67);  __stack_incr(-4);|
505  return found;
506}
507
508/*@ behavior stack_cost:
509      ensures __stack_max <= __max(\old(__stack_max), 6+\old(__stack));
510      ensures __stack == \old(__stack);
511    behavior time_cost:
512      ensures __cost <= \old(__cost)+1358;
513*/
514int main(void) {
515  int t;
516  |__stack_incr(2);  __cost_incr(110);|
517  t = count(a,4);
518  |__stack_incr(-2);|
519  return t;
520}
521\end{lstlisting}
522\caption{The instrumented version of the program in \autoref{test1},
523 with instrumentation added by the CerCo compiler in red and cost invariants
524 added by the CerCo Frama-C plugin in blue. The \texttt{\_\_cost},
525 \texttt{\_\_stack} and \texttt{\_\_stack\_max} variables hold the elapsed time
526in clock cycles and the current and maximum stack usage. Their initial values
527hold the clock cycles spent in initialising the global data before calling
528\texttt{main} and the space required by global data (and thus unavailable for
529the stack).
530}
531\label{itest1}
532\end{figure}
533\section{Main scientific and technical results}
534First we describe the basic labeling approach and our compiler
535implementations that use it.  This is suitable for basic architectures
536with simple cost models.  Then we will discuss the dependent labeling
537extension which is suitable for more advanced processor architectures
538and compiler optimisations.  At the end of this section we will
539demonstrate automated high level reasoning about the source level
540costs provided by the compilers.
541
542% \emph{Dependent labeling~\cite{?}.} The basic labeling approach assumes a
543% bijective mapping between object code and source code O(1) blocks (called basic
544% blocks). This assumption is violated by many program optimizations (e.g. loop
545% peeling and loop unrolling). It also assumes the cost model computed on the
546% object code to be non parametric: every block must be assigned a cost that does
547% not depend on the state. This assumption is violated by stateful hardware like
548% pipelines, caches, branch prediction units. The dependent labeling approach is
549% an extension of the basic labeling approach that allows to handle parametric
550% cost models. We showed how the method allows to deal with loop optimizations and
551% pipelines, and we speculated about its applications to caches.
552%
553% \emph{Techniques to exploit the induced cost model.} Every technique used for
554% the analysis of functional properties of programs can be adapted to analyse the
555% non-functional properties of the source code instrumented by compilers that
556% implement the labeling approach. In order to gain confidence in this claim, we
557% showed how to implement a cost invariant generator combining abstract
558% interpretation with separation logic ideas \cite{separation}. We integrated
559% everything in the Frama-C modular architecture, in order to compute proof
560% obligations from functional and cost invariants and to use automatic theorem
561% provers on them. This is an example of a new technique that is not currently
562% exploited in WCET analysis. It also shows how precise functional invariants
563% benefits the non-functional analysis too. Finally, we show how to fully
564% automatically analyse the reaction time of Lustre nodes that are first compiled
565% to C using a standard Lustre compiler and then processed by a C compiler that
566% implements the labeling approach.
567
568% \emph{The CerCo compiler.} This is a compiler from a large subset of the C
569% program to 8051/8052 object code,
570% integrating the labeling approach and a static analyser for 8051 executables.
571% The latter can be implemented easily and does not require dependent costs
572% because the 8051 microprocessor is a very simple one, with constant-cost
573% instruction. It was chosen to separate the issue of exact propagation of the
574% cost model from the orthogonal problem of the static analysis of object code
575% that may require approximations or dependent costs. The compiler comes in
576% several versions: some are prototypes implemented directly in OCaml, and they
577% implement both the basic and dependent labeling approaches; the final version
578% is extracted from a Matita certification and at the moment implements only the
579% basic approach.
580
581\subsection{The (basic) labeling approach}
582The labeling approach is the foundational insight that underlies all the developments in CerCo.
583It allows the tracking of the evolution of
584basic blocks during the compilation process in order to propagate the cost model from the
585object code to the source code without losing precision in the process.
586\paragraph{Problem statement.} Given a source program $P$, we want to obtain an
587instrumented source program $P'$,  written in the same programming language, and
588the object code $O$ such that: 1) $P'$ is obtained by inserting into $P$ some
589additional instructions to update global cost information like the amount of
590time spent during execution or the maximal stack space required; 2) $P$ and $P'$ 
591must have the same functional behaviour, i.e.\ they must produce that same output
592and intermediate observables; 3) $P$ and $O$ must have the same functional
593behaviour; 4) after execution and in interesting points during execution, the
594cost information computed by $P'$ must be an upper bound of the one spent by $O$ 
595to perform the corresponding operations (soundness property); 5) the difference
596between the costs computed by $P'$ and the execution costs of $O$ must be
597bounded by a program-dependent constant (precision property).
598
599\paragraph{The labeling software components.} We solve the problem in four
600stages \cite{labeling}, implemented by four software components that are used
601in sequence.
602
603The first component labels the source program $P$ by injecting label emission
604statements in appropriate positions to mark the beginning of basic blocks.
605% The
606% set of labels with their positions is called labeling.
607The syntax and semantics
608of the source programming language is augmented with label emission statements.
609The statement ``EMIT $\ell$'' behaves like a NOP instruction that does not affect the
610program state or control flow, but its execution is observable.
611% Therefore the observables of a run of a program becomes a stream
612% of label emissions: $\ell_1,\ldots,\ell_n$, called the program trace. We clarify the conditions
613% that the labeling must respect later.
614
615The second component is a labeling preserving compiler. It can be obtained from
616an existing compiler by adding label emission statements to every intermediate
617language and by propagating label emission statements during compilation. The
618compiler is correct if it preserves both the functional behaviour of the program
619and the traces of observables.
620% We may also ask that the function that erases the cost
621% emission statements commute with compilation. This optional property grants that
622% the labeling does not interfere with the original compiler behaviour. A further
623% set of requirements will be added later.
624
625The third component is a static object code analyser. It takes as input a labeled
626object code and it computes the scope of each of its label emission statements,
627i.e.\ the tree of instructions that may be executed after the statement and before
628a new label emission is encountered.
629It is a tree and not a sequence because the scope
630may contain a branching statement. In order to grant that such a finite tree
631exists, the object code must not contain any loop that is not broken by a label
632emission statement. This is the first requirement of a sound labeling. The
633analyser fails if the labeling is unsound. For each scope, the analyser
634computes an upper bound of the execution time required by the scope, using the
635maximum of the costs of the two branches in case of a conditional statement.
636Finally, the analyser computes the cost of a label by taking the maximum of the
637costs of the scopes of every statement that emits that label.
638
639The fourth and last component takes in input the cost model computed at step 3
640and the labelled code computed at step 1. It outputs a source program obtained
641by replacing each label emission statement with a statement that increments the
642global cost variable with the cost associated to the label by the cost model. 
643The obtained source code is the instrumented source code.
644
645\paragraph{Correctness.} Requirements 1, 2 and 3 of the problem statement
646obviously hold, with 2 and 3 being a consequence of the definition of a correct
647labeling preserving compiler. It is also obvious that the value of the global
648cost variable of an instrumented source code is at any time equal to the sum of
649the costs of the labels emitted by the corresponding labelled code. Moreover,
650because the compiler preserves all traces, the sum of the costs of the labels
651emitted in the source and target labelled code are the same. Therefore, to
652satisfy the fourth requirement, we need to grant that the time taken to execute
653the object code is equal to the sum of the costs of the labels emitted by the
654object code. We collect all the necessary conditions for this to happen in the
655definition of a sound labeling: a) all loops must be broken by a cost emission
656statement;  b) all program instructions must be in the scope of some cost
657emission statement. To satisfy also the fifth requirement, additional
658requirements must be imposed on the object code labeling to avoid all uses of
659the maximum in the cost computation: the labeling is precise if every label is
660emitted at most once and both branches of a conditional jump start with a label
661emission statement.
662
663The correctness and precision of the labeling approach only rely on the
664correctness and precision of the object code labeling. The simplest
665way to achieve them is to impose correctness and precision
666requirements also on the initial labeling produced by the first software
667component, and to ask the compiler to preserve these
668properties too. The latter requirement imposes serious limitations on the
669compilation strategy and optimizations: the compiler may not duplicate any code
670that contains label emission statements, like loop bodies. Therefore several
671loop optimisations like peeling or unrolling are prevented. Moreover, precision
672of the object code labeling is not sufficient \emph{per se} to obtain global
673precision: we implicitly assumed that a precise constant cost can be assigned
674to every instruction. This is not possible in
675the presence of stateful hardware whose state influences the cost of operations,
676like pipelines and caches. In Section~\ref{lab:deplabel} we will see an extension of the
677basic labeling approach to cover this situation.
678
679In CerCo we have developed several cost preserving compilers based on
680the labeling approach. Excluding an initial certified compiler for a
681`while' language, all remaining compilers target realistic source
682languages---a pure higher order functional language and a large subset
683of C with pointers, gotos and all data structures---and real world
684target processors---MIPS and the Intel 8051/8052 processor
685family. Moreover, they achieve a level of optimisation that ranges
686from moderate (comparable to GCC level 1) to intermediate (including
687loop peeling and unrolling, hoisting and late constant propagation).
688We describe the C compilers in detail in the following section.
689
690Two compilation chains were implemented for a purely functional
691higher-order language~\cite{labeling2}. The two main changes required
692to deal with functional languages are: 1) because global variables and
693updates are not available, the instrumentation phase produces monadic
694code to `update' the global costs; 2) the requirements for a sound and
695precise labeling of the source code must be changed when the
696compilation is based on CPS translations.  In particular, we need to
697introduce labels emitted before a statement is executed and also
698labels emitted after a statement is executed. The latter capture code
699that is inserted by the CPS translation and that would escape all
700label scopes.
701
702% Brian: one of the reviewers pointed out that standard Prolog implementations
703% do have some global state that apparently survives backtracking and might be
704% used.  As we haven't experimented with this, I think it's best to elide it
705% entirely.
706
707% Phases 1, 2 and 3 can be applied as well to logic languages (e.g. Prolog).
708% However, the instrumentation phase cannot: in standard Prolog there is no notion
709% of (global) variable whose state is not retracted during backtracking.
710% Therefore, the cost of executing computations that are later backtracked would
711% not be correctly counted in. Any extension of logic languages with
712% non-backtrackable state could support our labeling approach.
713
714\subsection{The CerCo C compilers}
715We implemented two C compilers, one implemented directly in OCaml and
716the other implemented in the interactive theorem prover
717Matita~\cite{matita}.  The first acted as a prototype for the second,
718but also supported MIPS and acted as a testbed for more advanced
719features such as the dependent labeling approach
720in Section~\ref{lab:deplabel}.
721
722The second C compiler is the \emph{Trusted CerCo Compiler}, whose cost
723predictions are formally verified. The code distributed
724is extracted OCaml code from the Matita implementation. In the rest of
725this section we will only focus on the Trusted CerCo Compiler, that only targets
726the C language and the 8051/8052 family, and that does not implement any
727advanced optimisations yet. Its user interface, however, is the same as the one
728of the other version, in order to trade safety with additional performances. In
729particular, the Frama-C CerCo plugin can work without recompilation
730with both of our C compilers.
731
732The 8051/8052 microprocessor is a very simple one, with constant-cost
733instructions. It was chosen to separate the issue of exact propagation of the
734cost model from the orthogonal problem of the static analysis of object code
735that may require approximations or dependent costs.
736
737The (trusted) CerCo compiler implements the following optimisations: cast
738simplification, constant propagation in expressions, liveness analysis driven
739spilling of registers, dead code elimination, branch displacement, and tunneling.
740The two latter optimisations are performed by our optimising assembler
741\cite{correctness}. The back-end of the compiler works on three address
742instructions, preferred to static single assignment code for the simplicity of
743the formal certification.
744
745The CerCo compiler is loosely based on the CompCert compiler \cite{compcert}, a
746recently developed certified compiler from C to the PowerPC, ARM and x86
747microprocessors. In contrast to CompCert, both the CerCo code and its
748certification are fully open source. Some data structures and language definitions for
749the front-end are directly taken from CompCert, while the back-end is a redesign
750of a compiler from Pascal to MIPS used by Fran\c{c}ois Pottier for a course at the
751Ecole Polytechnique.
752
753The main differences in the CerCo compiler are:
754\begin{enumerate}
755\item All the intermediate languages include label emitting instructions to
756implement the labeling approach, and the compiler preserves execution traces.
757\item Traditionally compilers target an assembly language with additional
758macro-instructions to be expanded before assembly; for CerCo we need to go all
759the way down to object code in order to perform the static analysis. Therefore
760we integrated also an optimising assembler and a static analyser.
761\item In order to avoid the additional work of implementing a linker
762 and a loader, we do not support separate
763compilation and external calls. Adding them is orthogonal
764to the labeling approach and should not introduce extra problems.
765\item We target an 8-bit processor, in contrast to CompCert's 32-bit targets. This requires
766many changes and more compiler code, but it is not fundamentally more
767complex. The proof of correctness, however, becomes much harder.
768\item We target a microprocessor that has a non uniform memory model, which is
769still often the case for microprocessors used in embedded systems and that is
770becoming common again in multi-core processors. Therefore the compiler has to
771keep track of data and it must move data between memory regions in the proper
772way. Moreover the size of pointers to different regions is not uniform. An
773additional difficulty was that the space available for the stack in internal
774memory in the 8051 is tiny, allowing only a minor number of nested calls. To
775support full recursion in order to test the CerCo tools also on recursive
776programs, the compiler implements a stack in external memory.
777\end{enumerate}
778
779\subsection{Formal certification of the CerCo compiler}
780We have formally
781certified in the Matita interactive proof assistant that the cost models induced on the source code by the
782Trusted CerCo Compiler correctly and precisely
783predict the object code behaviour. There are two cost models, one for execution
784time and one for stack space consumption. We show the correctness of the prediction
785only for those programs that do not exhaust the available machine stack space, a
786property that---thanks to the stack cost model---we can statically analyse on the
787source code using our Frama-C tool. The preservation of functional properties we
788take as an assumption, not itself formally proved in CerCo.  Other projects have
789already certified the preservation of functional semantics in similar compilers,
790and we have not attempted to directly repeat that work. In order to complete the
791proof for non-functional properties, we have introduced a new semantics for
792programming languages based on a new kind of structured observables with the
793relative notions of forward similarity and the study of the intensional
794consequences of forward similarity. We have also introduced a unified
795representation for back-end intermediate languages that was exploited to provide
796a uniform proof of forward similarity.
797
798The details on the proof techniques employed
799and
800the proof sketch can be collected from the CerCo deliverables and papers.
801In this section we will only hint at the correctness statement, which turned
802out to be more complex than what we expected at the beginning.
803
804\paragraph{The statement.}
805Real time programs are often reactive programs that loop forever responding to
806events (inputs) by performing some computation followed by some action (output)
807and the return to the initial state. For looping programs the overall execution
808time does not make sense. The same happens for reactive programs that spend an
809unpredictable amount of time in I/O. What is interesting is the reaction time
810that measure the time spent between I/O events. Moreover, we are interested in
811predicting and ruling out programs that crash running out of space on a certain
812input.
813Therefore we need to look for a statement that talks about sub-runs of a
814program. The most natural statement is that the time predicted on the source
815code and spent on the object code by two corresponding sub-runs are the same.
816The problem to solve to make this statement formal is how to identify the
817corresponding sub-runs and how to single out those that are meaningful.
818The solution we found is based on the notion of measurability. We say that a run
819has a \emph{measurable sub-run} when both the prefix of the sub-run and the
820sub-run do not exhaust the stack space, the number of function calls and returns
821in the sub-run is the same, the sub-run does not perform any I/O and the sub-run
822starts with a label emission statement and ends with a return or another label
823emission statements. The stack usage is estimated using the stack usage model
824that is computed by the compiler.
825
826The statement that we formally proved is: for each C run with a measurable
827sub-run, there exists an object code run with a sub-run, such that the observables
828of the pairs of prefixes and sub-runs are the same and the time spent by the
829object code in the sub-run is the same as the one predicted on the source code
830using the time cost model generated by the compiler.
831We briefly discuss the constraints for measurability. Not exhausting the stack
832space is a clear requirement of meaningfulness of a run, because source programs
833do not crash for lack of space while object code ones do. The balancing of
834function calls and returns is a requirement for precision: the labeling approach
835allows the scope of label emission statements to extend after function calls to
836minimize the number of labels. Therefore a label pays for all the instructions
837in a block, excluding those executed in nested function calls. If the number of
838calls/returns is unbalanced, it means that there is a call we have not returned
839to that could be followed by additional instructions whose cost has already been
840taken in account. To make the statement true (but less precise) in this
841situation, we could only say that the cost predicted on the source code is a
842safe bound, not that it is exact. The last condition on the entry/exit points of
843a run is used to identify sub-runs whose code correspond to a sequence of blocks
844that we can measure precisely. Any other choice would start or end the run in the
845middle of a block and we would be forced again to weaken the statement taking as
846a bound the cost obtained counting in all the instructions that precede the
847starting one in the block, or follow the final one in the block.
848I/O operations can be performed in the prefix of the run, but not in the
849measurable sub-run. Therefore we prove that we can predict reaction times, but
850not I/O times, as desired.
851
852\subsection{Dependent labeling}
853\label{lab:deplabel}
854The core idea of the basic labeling approach is to establish a tight connection
855between basic blocks executed in the source and target languages. Once the
856connection is established, any cost model computed on the object code can be
857transferred to the source code, without affecting the code of the compiler or
858its proof. In particular, it is immediate that we can also transport cost models
859that associate to each label functions from hardware state to natural numbers.
860However, a problem arises during the instrumentation phase that replaces cost
861emission statements with increments of global cost variables. The global cost
862variable must be incremented with the result of applying the function associated
863to the label to the hardware state at the time of execution of the block.
864The hardware state comprises both the functional state that affects the
865computation (the value of the registers and memory) and the non-functional
866state that does not (the pipeline and cache contents, for example). The former is
867in correspondence with the source code state, but reconstructing the
868correspondence may be hard and lifting the cost model to work on the source code
869state is likely to produce cost expressions that are too complex to understand and reason about.
870Fortunately, in all modern architectures the cost of executing single
871instructions is either independent of the functional state or the jitter---the
872difference between the worst and best case execution times---is small enough
873to be bounded without losing too much precision. Therefore we only consider
874dependencies on the `non-functional' parts of the state.
875
876The non-functional state has no correspondence in the high level state and does
877not influence the functional properties. What can be done is to expose the
878non-functional state in the source code. We present here the basic
879intuition in a simplified form: the technical details that allow us to handle the
880general case are more complex and can be found in~\cite{paolo}. We add
881to the source code an additional global variable that represents the
882non-functional state and another one that remembers the last labels emitted. The
883state variable must be updated at every label emission statement, using an
884update function which is computed during static analysis too. The update
885function associates to each label a function from the recently emitted labels
886and old state to the new state. It is computed by composing the semantics of every
887instruction in a basic block and restricting it to the non-functional part of
888the state.
889
890Not all the details of the non-functional state needs to be exposed, and the
891technique works better when the part of state that is required can be summarized
892in a simple data structure. For example, to handle simple but realistic
893pipelines it is sufficient to remember a short integer that encodes the position
894of bubbles (stuck instructions) in the pipeline. In any case, it is not necessary
895for the user to understand the meaning of the state to reason over the properties
896of the
897program. Moreover, at any moment the user, or the invariant generator tools that
898analyse the instrumented source code produced by the compiler, can decide to
899trade precision of the analysis for simplicity by approximating the parametric
900cost with safe non parametric bounds. Interestingly, the functional analysis of
901the code could determine which blocks are executed more frequently in order to
902use more aggressive approximations for the ones that are executed least.
903
904Dependent labeling can also be applied to allow the compiler to duplicate
905blocks that contain labels (e.g. in loop optimisations)~\cite{paolo}. The effect is to assign
906a different cost to the different occurrences of a duplicated label. For
907example, loop peeling turns a loop into the concatenation of a copy of the loop
908body for the first iteration and the conditional execution of the
909loop for successive iterations. Further optimisations will compile the two
910copies of the loop differently, with the first body usually
911taking more time.
912
913By introducing a variable that keeps track of the iteration number, we can
914associate to the label a cost that is a function of the iteration number. The
915same technique works for loop unrolling without modifications: the function will
916assign a cost to the even iterations and another cost to the odd ones. The
917actual work to be done consists of introducing within the source code, and for each
918loop, a variable that counts the number of iterations. The loop optimisation code
919that duplicate the loop bodies must also modify the code to correctly propagate
920the update of the iteration numbers. The technical details are more complex and
921can be found in the CerCo reports and publications. The implementation, however,
922is quite simple (and forms part of our OCaml version of the compiler)
923and the changes to a loop optimising compiler are minimal.
924
925\subsection{Techniques to exploit the induced cost model}
926We now turn our attention to synthesising high-level costs, such as
927the execution time of a whole program.  We consider as our starting point source level costs
928provided by basic labeling, in other words annotations
929on the source code which are constants that provide a sound and sufficiently
930precise upper bound on the cost of executing the blocks after compilation to
931object code.
932
933The principle that we have followed in designing the cost synthesis tools is
934that the synthetic bounds should be expressed and proved within a general
935purpose tool built to reason on the source code. In particular, we rely on the
936Frama-C tool to reason on C code and on the Coq proof-assistant to reason on
937higher-order functional programs.
938
939This principle entails that: 1)
940The inferred synthetic bounds are indeed correct as long as the general purpose
941tool is; 2) there is no limitation on the class of programs that can be handled
942as long as the user is willing to carry on an interactive proof.
943
944Of course, automation is desirable whenever possible. Within this framework,
945automation means writing programs that give hints to the general purpose tool.
946These hints may take the form, say, of loop invariants/variants, of predicates
947describing the structure of the heap, or of types in a light logic. If these
948hints are correct and sufficiently precise the general purpose tool will produce
949a proof automatically, otherwise, user interaction is required.
950
951\paragraph{The Cost plugin and its application to the Lustre compiler.}
952Frama-C \cite{framac} is a set of analysers for C programs with a
953specification language called ACSL. New analyses can be dynamically added
954via a plugin system. For instance, the Jessie plugin allows deductive
955verification of C programs with respect to their specification in ACSL, with
956various provers as back-end tools.
957We developed the CerCo Cost plugin for the Frama-C platform as a proof of
958concept of an automatic environment exploiting the cost annotations produced by
959the CerCo compiler. It consists of an OCaml program which essentially
960takes the following actions: 1) it receives as input a C program, 2) it
961applies the CerCo compiler to produce a related C program with cost annotations,
9623) it applies some heuristics to produce a tentative bound on the cost of
963executing the C functions of the program as a function of the value of their
964parameters, 4) the user can then call the Jessie plugin to discharge the
965related proof obligations.
966In the following we elaborate on the soundness of the framework and the
967experiments we performed with the Cost tool on the C programs produced by a
968Lustre compiler.
969
970\paragraph{Soundness.} The soundness of the whole framework depends on the cost
971annotations added by the CerCo compiler, the synthetic costs produced by the
972cost plugin, the verification conditions (VCs) generated by Jessie, and the
973external provers discharging the VCs. The synthetic costs being in ACSL format,
974Jessie can be used to verify them. Thus, even if the added synthetic costs are
975incorrect (relatively to the cost annotations), the process as a whole is still
976correct: indeed, Jessie will not validate incorrect costs and no conclusion can
977be made about the WCET of the program in this case. In other terms, the
978soundness does not really depend on the action of the cost plugin, which can in
979principle produce any synthetic cost. However, in order to be able to actually
980prove a WCET of a C function, we need to add correct annotations in a way that
981Jessie and subsequent automatic provers have enough information to deduce their
982validity. In practice this is not straightforward even for very simple programs
983composed of branching and assignments (no loops and no recursion) because a fine
984analysis of the VCs associated with branching may lead to a complexity blow up.
985\paragraph{Experience with Lustre.} Lustre is a data-flow language for programming
986synchronous systems, with a compiler which targets C. We designed a
987wrapper for supporting Lustre files.
988The C function produced by the compiler implements the step function of the
989synchronous system and computing the WCET of the function amounts to obtain a
990bound on the reaction time of the system. We tested the Cost plugin and the
991Lustre wrapper on the C programs generated by the Lustre compiler. For programs
992consisting of a few hundred lines of code, the cost plugin computes a
993WCET and Alt-Ergo is able to discharge all VCs automatically.
994
995\paragraph{Handling C programs with simple loops.}
996The cost annotations added by the CerCo compiler take the form of C instructions
997that update a fresh global variable called the cost variable by a constant.
998Synthesizing a WCET of a C function thus consists of statically resolving an
999upper bound of the difference between the value of the cost variable before and
1000after the execution of the function, i.e. finding the instructions
1001that update the cost variable and establish the number of times they are passed
1002through during the flow of execution. To perform the analysis the plugin
1003makes the following assumptions on the programs:
10041) there are no recursive functions;
10052) every loop must be annotated with a variant. The variants of `for' loops are
1006automatically inferred.
1007
1008The plugin proceeds as follows.
1009First the call graph of the program is computed.
1010Then the computation of the cost of the function is performed by traversing its
1011control flow graph. If the function $f$ calls the function $g$ 
1012then the function $g$ 
1013is processed before the function $f$. The cost at a node is the maximum of the
1014costs of the successors.
1015In the case of a loop with a body that has a constant cost for every step of the
1016loop, the cost is the product of the cost of the body and of the variant taken
1017at the start of the loop.
1018In the case of a loop with a body whose cost depends on the values of some free
1019variables, a fresh logic function $f$ is introduced to represent the cost of the
1020loop in the logic assertions. This logic function takes the variant as a first
1021parameter. The other parameters of $f$ are the free variables of the body of the
1022loop. An axiom is added to account the fact that the cost is accumulated at each
1023step of the loop.
1024The cost of the function is directly added as post-condition of the function.
1025
1026The user can influence the annotation by two different means:
10271) by using more precise variants;
10282) by annotating functions with cost specifications. The plugin will use this cost
1029for the function instead of computing it.
1030\paragraph{C programs with pointers.}
1031When it comes to verifying programs involving pointer-based data structures,
1032such as linked lists, trees, or graphs, the use of traditional first-order logic
1033to specify, and of SMT solvers to verify, shows some limitations. Separation
1034logic~\cite{separation} is an elegant alternative. It is a program logic
1035with a new notion of conjunction to express spatial heap separation. Bobot has
1036recently introduced automatically generated separation
1037predicates to simulate separation logic reasoning in the Jessie plugin where the specification language, the verification condition
1038generator, and the theorem provers were not designed with separation logic in
1039mind. CerCo's plugin can exploit the separation predicates to automatically
1040reason on the cost of execution of simple heap manipulation programs such as an
1041in-place list reversal.
1042
1043\section{Conclusions and future work}
1044
1045All the CerCo software and deliverables can be found on the CerCo homepage at~\url{http://cerco.cs.unibo.it}.
1046
1047The results obtained so far are encouraging and provide evidence that
1048it is possible to perform static time and space analysis at the source level
1049without losing accuracy, reducing the trusted code base and reconciling the
1050study of functional and non-functional properties of programs. The
1051techniques introduced seem to be scalable, cover both imperative and
1052functional languages and are compatible with every compiler optimisation
1053considered by us so far.
1054
1055To prove that compilers can keep track of optimisations
1056and induce a precise cost model on the source code, we targeted a simple
1057architecture that admits a cost model that is execution history independent.
1058The most important future work is dealing with hardware architectures
1059characterized by history dependent stateful components, like caches and
1060pipelines. The main issue consists in assigning a parametric, dependent cost
1061to basic blocks that can be later transferred by the labeling approach to
1062the source code and represented in a meaningful way to the user. The dependent
1063labeling approach that we have studied seems a promising tool to achieve
1064this goal, but the cost model generated for a realistic processor could be too
1065large and complex to be exposed in the source code. Further study is required
1066to evaluate the technique on a realistic processor and to introduce early
1067approximations of the cost model to make the technique feasible.
1068
1069Examples of further future work consist in improving the cost invariant
1070generator algorithms and the coverage of compiler optimizations, in combining
1071the labeling approach with the type and effect discipline of~\cite{typeffects}
1072to handle languages with implicit memory management, and in experimenting with
1073our tools in early development phases. Some larger case study is also necessary
1074to evaluate the CerCo's prototype on realistic, industrial-scale programs.
1075
1076% \bibliographystyle{splncs}
1077\bibliography{fopara13}
1078% \begin{thebibliography}{19}
1079%
1080% \bibitem{survey} \textbf{A Survey of Static Program Analysis Techniques}
1081% W.~W\"ogerer. Technical report. Technische Universit\"at Wien 2005
1082%
1083% \bibitem{cerco} \textbf{Certified Complexity}. R.M. Amadio, A. Asperti, N. Ayache,
1084% B. Campbell, D. P. Mulligan, R. Pollack, Y. Regis-Gianas, C. Sacerdoti Coen, I.
1085% Stark, in Procedia Computer Science, Volume 7, 2011, Proceedings of the 2 nd
1086% European Future Technologies Conference and Exhibition 2011 (FET 11), 175-177.
1087%
1088% \bibitem{labeling} \textbf{Certifying and Reasoning on Cost Annotations in C
1089% Programs}, N.  Ayache, R.M. Amadio, Y.R\'{e}gis-Gianas, in Proc. FMICS, Springer
1090% LNCS
1091% 7437: 32-46, 2012.
1092% %, DOI:10.1007/978-3-642-32469-7\_3.
1093%
1094% \bibitem{labeling2} \textbf{Certifying and reasoning on cost annotations of
1095% functional programs}.
1096% R.M. Amadio, Y. R\'{e}gis-Gianas. Proceedings of the Second international conference
1097% on Foundational and Practical Aspects of Resource Analysis FOPARA 2011 Springer
1098% LNCS 7177:72-89, 2012.
1099%
1100% \bibitem{compcert} \textbf{Formal verification of a realistic compiler}. X. Leroy,  In Commun. ACM 52(7), 107–115, 2009.
1101%
1102% \bibitem{framac} \textbf{Frama-C user manual}. L. Correnson, P. Cuoq, F. Kirchner, V. Prevosto, A. Puccetti, J. Signoles,
1103% B. Yakobowski. in CEA-LIST, Software Safety Laboratory, Saclay, F-91191,
1104% \url{http://frama-c.com/}.
1105%
1106% \bibitem{paolo} \textbf{Indexed Labels for Loop Iteration Dependent Costs}. P.
1107% Tranquilli, in Proceedings of the 11th International Workshop on Quantitative
1108% Aspects of Programming Languages and Systems (QAPL 2013), Rome, 23rd-24th March
1109% 2013, Electronic Proceedings in Theoretical Computer Science, to appear in 2013.
1110%
1111% \bibitem{separation} \textbf{Intuitionistic reasoning about shared mutable data
1112% structure} J.C. Reynolds. In Millennial Perspectives in Computer Science,
1113% pages 303–321, Houndsmill, Hampshire, 2000. Palgrave.
1114%
1115% \bibitem{lustre} \textbf{LUSTRE: a declarative language for real-time
1116% programming}
1117% P. Caspi, D. Pilaud, N. Halbwachs, J.A. Plaice. In Proceedings of
1118% the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages ACM
1119% 1987.
1120%
1121% \bibitem{correctness} \textbf{On the correctness of an optimising assembler for
1122% the intel MCS-51 microprocessor}.
1123%   D. P. Mulligan, C. Sacerdoti Coen. In Proceedings of the Second
1124% international conference on Certified Programs and Proofs, Springer-Verlag 2012.
1125%
1126% \bibitem{proartis} \textbf{PROARTIS: Probabilistically Analysable Real-Time
1127% Systems}, F.J. Cazorla, E. Qui\~{n}ones, T. Vardanega, L. Cucu, B. Triquet, G.
1128% Bernat, E. Berger, J. Abella, F. Wartel, M. Houston, et al., in ACM Transactions
1129% on Embedded Computing Systems, 2012.
1130%
1131% \bibitem{embounded} \textbf{The EmBounded project (project paper)}. K. Hammond,
1132% R. Dyckhoff, C. Ferdinand, R. Heckmann, M. Hofmann, H. Loidl, G. Michaelson, J.
1133% Serot, A. Wallace, in Trends in Functional Programming, Volume 6, Intellect
1134% Press, 2006.
1135%
1136% \bibitem{matita}
1137% \textbf{The Matita Interactive Theorem Prover}.
1138% A. Asperti, C. Sacerdoti Coen, W. Ricciotti, E. Tassi.
1139% 23rd International Conference on Automated Deduction, CADE 2011.
1140%
1141% \bibitem{typeffects} \textbf{The Type and Effect Discipline}. J.-P. Talpin,
1142%  P. Jouvelot.
1143%   In Proceedings of the Seventh Annual Symposium on Logic in Computer Science
1144% (LICS '92), Santa Cruz, California, USA, June 22-25, 1992.
1145% IEEE Computer Society 1992.
1146%
1147% \bibitem{stateart} \textbf{The worst-case execution-time problem overview of
1148% methods
1149% and survey of tools.} R. Wilhelm et al., in  ACM Transactions on Embedded
1150% Computing Systems, 7:1–53, May 2008.
1151%
1152% %\bibitem{proartis2} \textbf{A Cache Design for Probabilistic Real-Time
1153% % Systems}, L. Kosmidis, J. Abella, E. Quinones, and F. Cazorla, in Design,
1154% % Automation, and Test in Europe (DATE), Grenoble, France, 03/2013.
1155%
1156% \end{thebibliography}
1157
1158
1159%\bibliography{fopara13.bib}
1160
1161\end{document}
Note: See TracBrowser for help on using the repository browser.