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

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

Moved paper structure comments to their relevant sections

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