source: Papers/jar-cerco-2017/architecture.tex @ 3613

Last change on this file since 3613 was 3613, checked in by boender, 3 years ago

Cut paper into sections, continued introduction rewrite

File size: 6.9 KB
Line 
1\section{Compiler architecture}
2\label{sect.compiler.architecture}
3
4\subsection{The typical CerCo workflow}
5
6\begin{figure}[!t]
7\begin{tabular}{l@{\hspace{0.2cm}}|@{\hspace{0.2cm}}l}
8\begin{lstlisting}
9char a[] = {3, 2, 7, 14};
10char threshold = 4;
11
12int count(char *p, int len) {
13  char j;
14  int found = 0;
15  for (j=0; j < len; j++) {
16    if (*p <= threshold)
17      found++;
18    p++;
19    }
20  return found;
21}
22
23int main() {
24  return count(a,4);
25}
26\end{lstlisting}
27&
28%  $\vcenter{\includegraphics[width=7.5cm]{interaction_diagram.pdf}}$
29\begin{tikzpicture}[
30    baseline={([yshift=-.5ex]current bounding box)},
31    element/.style={draw, text width=1.6cm, on chain, text badly centered},
32    >=stealth
33    ]
34{[start chain=going below, node distance=.5cm]
35\node [element] (cerco) {CerCo\\compiler};
36\node [element] (cost)  {CerCo\\cost plugin};
37{[densely dashed]
38\node [element] (ded)   {Deductive\\platform};
39\node [element] (check) {Proof\\checker};
40}
41}
42\coordinate [left=3.5cm of cerco] (left);
43{[every node/.style={above, text width=3.5cm, text badly centered,
44                     font=\scriptsize}]
45\draw [<-] ([yshift=-1ex]cerco.north west) coordinate (t) --
46    node {C source}
47    (t-|left);
48\draw [->] (cerco) -- (cost);
49\draw [->] ([yshift=1ex]cerco.south west) coordinate (t) --
50    node {C source+\color{red}{cost annotations}}
51    (t-|left) coordinate (cerco out);
52\draw [->] ([yshift=1ex]cost.south west) coordinate (t) --
53    node {C source+\color{red}{cost annotations}\\+\color{blue}{synthesized assertions}}
54    (t-|left) coordinate (out);
55{[densely dashed]
56\draw [<-] ([yshift=-1ex]ded.north west) coordinate (t) --
57    node {C source+\color{red}{cost annotations}\\+\color{blue}{complexity assertions}}
58    (t-|left) coordinate (ded in) .. controls +(-.5, 0) and +(-.5, 0) .. (out);
59\draw [->] ([yshift=1ex]ded.south west) coordinate (t) --
60    node {complexity obligations}
61    (t-|left) coordinate (out);
62\draw [<-] ([yshift=-1ex]check.north west) coordinate (t) --
63    node {complexity proof}
64    (t-|left) .. controls +(-.5, 0) and +(-.5, 0) .. (out);
65\draw [dash phase=2.5pt] (cerco out) .. controls +(-1, 0) and +(-1, 0) ..
66    (ded in);
67}}
68%% user:
69% head
70\draw (current bounding box.west) ++(-.2,.5)
71    circle (.2) ++(0,-.2) -- ++(0,-.1) coordinate (t);
72% arms
73\draw (t) -- +(-.3,-.2);
74\draw (t) -- +(.3,-.2);
75% body
76\draw (t) -- ++(0,-.4) coordinate (t);
77% legs
78\draw (t) -- +(-.2,-.6);
79\draw (t) -- +(.2,-.6);
80\end{tikzpicture}
81\end{tabular}
82\caption{On the left: C code to count the number of elements in an array
83 that are less than or equal to a given threshold. On the right: CerCo's interaction
84 diagram. Components provided by CerCo are drawn with a solid border.}
85\label{test1}
86\end{figure}
87We illustrate the workflow we envisage (on the right
88of~\autoref{test1}) on an example program (on the left
89of~\autoref{test1}).  The user writes the program and feeds it to the
90CerCo compiler, which outputs an instrumented version of the same
91program that updates global variables that record the elapsed
92execution time and the stack space usage.  The red lines in
93\autoref{itest1} introducing variables, functions and function calls
94starting with \lstinline'__cost' and \lstinline'__stack' are the instrumentation introduced by the
95compiler.  For example, the two calls at the start of
96\lstinline'count' say that 4 bytes of stack are required, and that it
97takes 111 cycles to reach the next cost annotation (in the loop body).
98The compiler measures these on the labelled object code that it generates.
99
100 The annotated program can then be enriched with complexity
101assertions in the style of Hoare logic, that are passed to a deductive
102platform (in our case Frama-C). We provide as a Frama-C cost plugin a
103simple automatic synthesiser for complexity assertions which can
104be overridden by the user to increase or decrease accuracy.  These are the blue
105comments starting with \lstinline'/*@' in \autoref{itest1}, written in
106Frama-C's specification language, ACSL.  From the
107assertions, a general purpose deductive platform produces proof
108obligations which in turn can be closed by automatic or interactive
109provers, ending in a proof certificate.
110
111% NB: if you try this example with the live CD you should increase the timeout
112
113Twelve proof obligations are generated from~\autoref{itest1} (to prove
114that the loop invariant holds after one execution if it holds before,
115to prove that the whole program execution takes at most 1358 cycles, and so on).  Note that the synthesised time bound for \lstinline'count',
116$178+214*(1+\text{\lstinline'len'})$ cycles, is parametric in the length of
117the array. The CVC3 prover
118closes all obligations within half a minute on routine commodity
119hardware.  A simpler non-parametric version can be solved in a few
120seconds.
121%
122\fvset{commandchars=\\\{\}}
123\lstset{morecomment=[s][\color{blue}]{/*@}{*/},
124        moredelim=[is][\color{blue}]{$}{$},
125        moredelim=[is][\color{red}]{|}{|},
126        lineskip=-2pt}
127\begin{figure}[!p]
128\begin{lstlisting}
129|int __cost = 33, __stack = 5, __stack_max = 5;|
130|void __cost_incr(int incr) { __cost += incr; }|
131|void __stack_incr(int incr) {
132  __stack += incr;
133  __stack_max = __stack_max < __stack ? __stack : __stack_max;
134}|
135
136char a[4] = {3, 2, 7, 14};  char threshold = 4;
137
138/*@ behavior stack_cost:
139      ensures __stack_max <= __max(\old(__stack_max), 4+\old(__stack));
140      ensures __stack == \old(__stack);
141    behavior time_cost:
142      ensures __cost <= \old(__cost)+(178+214*__max(1+\at(len,Pre), 0));
143*/
144int count(char *p, int len) {
145  char j;  int found = 0;
146  |__stack_incr(4);  __cost_incr(111);|
147  $__l: /* internal */$
148  /*@ for time_cost: loop invariant
149        __cost <= \at(__cost,__l)+
150                  214*(__max(\at((len-j)+1,__l), 0)-__max(1+(len-j), 0));
151      for stack_cost: loop invariant
152        __stack_max == \at(__stack_max,__l);
153      for stack_cost: loop invariant
154        __stack == \at(__stack,__l);
155      loop variant len-j;
156  */
157  for (j = 0; j < len; j++) {
158    |__cost_incr(78);|
159    if (*p <= threshold) { |__cost_incr(136);| found ++; }
160    else { |__cost_incr(114);| }
161    p ++;
162  }
163  |__cost_incr(67);  __stack_incr(-4);|
164  return found;
165}
166
167/*@ behavior stack_cost:
168      ensures __stack_max <= __max(\old(__stack_max), 6+\old(__stack));
169      ensures __stack == \old(__stack);
170    behavior time_cost:
171      ensures __cost <= \old(__cost)+1358;
172*/
173int main(void) {
174  int t;
175  |__stack_incr(2);  __cost_incr(110);|
176  t = count(a,4);
177  |__stack_incr(-2);|
178  return t;
179}
180\end{lstlisting}
181\caption{The instrumented version of the program in \autoref{test1},
182 with instrumentation added by the CerCo compiler in red and cost invariants
183 added by the CerCo Frama-C plugin in blue. The \lstinline'__cost',
184 \lstinline'__stack' and \lstinline'__stack_max' variables hold the elapsed time
185in clock cycles and the current and maximum stack usage. Their initial values
186hold the clock cycles spent in initialising the global data before calling
187\lstinline'main' and the space required by global data (and thus unavailable for
188the stack).
189}
190\label{itest1}
191\end{figure}
Note: See TracBrowser for help on using the repository browser.