Changeset 3643


Ignore:
Timestamp:
Mar 8, 2017, 4:51:29 PM (7 weeks ago)
Author:
mulligan
Message:

...

Location:
Papers/jar-cerco-2017
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/architecture.tex

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

    r3642 r3643  
    210210  isbn      = {978-1-84150-176-5},
    211211}
     212
     213@misc
     214{ acsl,
     215  title = {{ACSL}: the {ANSI}/{ISO} {C} specification language, reference manual},
     216  url   = {https://frama-c.com/download/acsl_1.4.pdf},
     217  note  = {Accessed March 2017},
     218  year  = {2017},
     219  key   = {acsl-the}
     220}
     221
     222@inproceedings{DBLP:conf/cav/BarrettT07,
     223  author    = {Clark Barrett and
     224               Cesare Tinelli},
     225  title     = {{CVC3}},
     226  booktitle = {Computer Aided Verification, 19th International Conference, {CAV}
     227               2007, Berlin, Germany, July 3-7, 2007, Proceedings},
     228  pages     = {298--302},
     229  year      = {2007},
     230  crossref  = {DBLP:conf/cav/2007},
     231  url       = {http://dx.doi.org/10.1007/978-3-540-73368-3_34},
     232  doi       = {10.1007/978-3-540-73368-3_34},
     233  timestamp = {Mon, 03 Sep 2007 13:24:22 +0200},
     234  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cav/BarrettT07},
     235  bibsource = {dblp computer science bibliography, http://dblp.org}
     236}
     237
    212238
    213239@article{DBLP:journals/corr/abs-1202-4905,
  • Papers/jar-cerco-2017/introduction.tex

    r3642 r3643  
    127127With these methods, we enable the use of more off-the-shelf components (e.g. provers and invariant generators) whilst reducing the trusted code base at the same time.
    128128
    129 \subsection{Introduction to Matita}
     129\subsection{A proposed workflow}
     130
     131\begin{figure}[!t]
     132\begin{tabular}{l@{\hspace{0.2cm}}|@{\hspace{0.2cm}}l}
     133\begin{lstlisting}
     134char a[] = {3, 2, 7, 14};
     135char threshold = 4;
     136
     137int count(char *p, int len) {
     138  char j;
     139  int found = 0;
     140  for (j=0; j < len; j++) {
     141    if (*p <= threshold)
     142      found++;
     143    p++;
     144    }
     145  return found;
     146}
     147
     148int main() {
     149  return count(a,4);
     150}
     151\end{lstlisting}
     152&
     153%  $\vcenter{\includegraphics[width=7.5cm]{interaction_diagram.pdf}}$
     154\begin{tikzpicture}[
     155    baseline={([yshift=-.5ex]current bounding box)},
     156    element/.style={draw, text width=1.6cm, on chain, text badly centered},
     157    >=stealth
     158    ]
     159{[start chain=going below, node distance=.5cm]
     160\node [element] (cerco) {CerCo\\compiler};
     161\node [element] (cost)  {CerCo\\cost plugin};
     162{[densely dashed]
     163\node [element] (ded)   {Deductive\\platform};
     164\node [element] (check) {Proof\\checker};
     165}
     166}
     167\coordinate [left=3.5cm of cerco] (left);
     168{[every node/.style={above, text width=3.5cm, text badly centered,
     169                     font=\scriptsize}]
     170\draw [<-] ([yshift=-1ex]cerco.north west) coordinate (t) --
     171    node {C source}
     172    (t-|left);
     173\draw [->] (cerco) -- (cost);
     174\draw [->] ([yshift=1ex]cerco.south west) coordinate (t) --
     175    node {C source+\color{red}{cost annotations}}
     176    (t-|left) coordinate (cerco out);
     177\draw [->] ([yshift=1ex]cost.south west) coordinate (t) --
     178    node {C source+\color{red}{cost annotations}\\+\color{blue}{synthesized assertions}}
     179    (t-|left) coordinate (out);
     180{[densely dashed]
     181\draw [<-] ([yshift=-1ex]ded.north west) coordinate (t) --
     182    node {C source+\color{red}{cost annotations}\\+\color{blue}{complexity assertions}}
     183    (t-|left) coordinate (ded in) .. controls +(-.5, 0) and +(-.5, 0) .. (out);
     184\draw [->] ([yshift=1ex]ded.south west) coordinate (t) --
     185    node {complexity obligations}
     186    (t-|left) coordinate (out);
     187\draw [<-] ([yshift=-1ex]check.north west) coordinate (t) --
     188    node {complexity proof}
     189    (t-|left) .. controls +(-.5, 0) and +(-.5, 0) .. (out);
     190\draw [dash phase=2.5pt] (cerco out) .. controls +(-1, 0) and +(-1, 0) ..
     191    (ded in);
     192}}
     193%% user:
     194% head
     195\draw (current bounding box.west) ++(-.2,.5)
     196    circle (.2) ++(0,-.2) -- ++(0,-.1) coordinate (t);
     197% arms
     198\draw (t) -- +(-.3,-.2);
     199\draw (t) -- +(.3,-.2);
     200% body
     201\draw (t) -- ++(0,-.4) coordinate (t);
     202% legs
     203\draw (t) -- +(-.2,-.6);
     204\draw (t) -- +(.2,-.6);
     205\end{tikzpicture}
     206\end{tabular}
     207\caption{On the left: C code to count the number of elements in an array
     208 that are less than or equal to a given threshold. On the right: CerCo's interaction
     209 diagram. Components provided by CerCo are drawn with a solid border.}
     210\label{test1}
     211\end{figure}
     212
     213\fvset{commandchars=\\\{\}}
     214\lstset{morecomment=[s][\color{blue}]{/*@}{*/},
     215        moredelim=[is][\color{blue}]{$}{$},
     216        moredelim=[is][\color{red}]{|}{|},
     217        lineskip=-2pt}
     218\begin{figure}[!p]
     219\begin{lstlisting}
     220|int __cost = 33, __stack = 5, __stack_max = 5;|
     221|void __cost_incr(int incr) { __cost += incr; }|
     222|void __stack_incr(int incr) {
     223  __stack += incr;
     224  __stack_max = __stack_max < __stack ? __stack : __stack_max;
     225}|
     226
     227char a[4] = {3, 2, 7, 14};  char threshold = 4;
     228
     229/*@ behavior stack_cost:
     230      ensures __stack_max <= __max(\old(__stack_max), 4+\old(__stack));
     231      ensures __stack == \old(__stack);
     232    behavior time_cost:
     233      ensures __cost <= \old(__cost)+(178+214*__max(1+\at(len,Pre), 0));
     234*/
     235int count(char *p, int len) {
     236  char j;  int found = 0;
     237  |__stack_incr(4);  __cost_incr(111);|
     238  $__l: /* internal */$
     239  /*@ for time_cost: loop invariant
     240        __cost <= \at(__cost,__l)+
     241                  214*(__max(\at((len-j)+1,__l), 0)-__max(1+(len-j), 0));
     242      for stack_cost: loop invariant
     243        __stack_max == \at(__stack_max,__l);
     244      for stack_cost: loop invariant
     245        __stack == \at(__stack,__l);
     246      loop variant len-j;
     247  */
     248  for (j = 0; j < len; j++) {
     249    |__cost_incr(78);|
     250    if (*p <= threshold) { |__cost_incr(136);| found ++; }
     251    else { |__cost_incr(114);| }
     252    p ++;
     253  }
     254  |__cost_incr(67);  __stack_incr(-4);|
     255  return found;
     256}
     257
     258/*@ behavior stack_cost:
     259      ensures __stack_max <= __max(\old(__stack_max), 6+\old(__stack));
     260      ensures __stack == \old(__stack);
     261    behavior time_cost:
     262      ensures __cost <= \old(__cost)+1358;
     263*/
     264int main(void) {
     265  int t;
     266  |__stack_incr(2);  __cost_incr(110);|
     267  t = count(a,4);
     268  |__stack_incr(-2);|
     269  return t;
     270}
     271\end{lstlisting}
     272\caption{The instrumented version of the program in Figure~\ref{test1},  with instrumentation added by the CerCo compiler in red and cost invariants added by the CerCo Frama-C plugin in blue.
     273The \lstinline'__cost', \lstinline'__stack' and \lstinline'__stack_max' variables hold the elapsed time in clock cycles and the current and maximum stack usage. Their initial values
     274hold the clock cycles spent in initialising the global data before calling
     275\lstinline'main' and the space required by global data (and thus unavailable for
     276the stack).
     277}
     278\label{itest1}
     279\end{figure}
     280
     281How should a Software Engineer use our tool in anger?
     282We illustrate an example C program on the left in Figure~\ref{test1}, and a prospective workflow making use of our toolset on the right of Figure~\ref{test1}.
     283An engineer writes their C program and feeds it as input to the CerCo compiler, which outputs an instrumented version of the same program that updates fresh global variables that record the elapsed execution time and the stack space usage.
     284Figure~\ref{itest1} demonstrates one of the outputs of the CerCo C compiler---an embellished version of the original C source code, with cost annotations automatically inserted, the other output being an object code file, not included here.
     285The red lines in Figure~\ref{itest1} introducing variables, functions and function calls starting with \lstinline'__cost' and \lstinline'__stack' are the instrumentation introduced by the compiler.
     286For example, the two calls at the start of \lstinline'count' say that 4 bytes of stack are required, and that it takes 111 cycles to reach the next cost annotation (in the loop body).
     287The compiler establishes these costs labelled object code that it generates, and lifts them back through the compilation chain, where they are finally reflected as cost annotations at the source level.
     288
     289The annotated program can then be enriched with complexity assertions in the style of Hoare logic, that are passed to a deductive platform (in our case Frama-C~\cite{framac}).
     290We have written a simple automatic synthesiser for complexity assertions as a plugin for Frama-C.
     291The behaviour of this plugin can be overridden by the user to increase or decrease accuracy.
     292These are the blue comments starting with \lstinline'/*@' in Figure~\ref{itest1}, written in Frama-C's specification language, ACSL~\cite{acsl}.
     293From these assertions, a general purpose deductive platform produces proof obligations which in turn can be closed by automatic or interactive provers, ending in a proof certificate.
     294
     295% NB: if you try this example with the live CD you should increase the timeout
     296
     297Twelve proof obligations are generated from Figure~\ref{itest1}.
     298These obligations are to prove that the loop invariant holds after one execution if it holds before, to prove that the whole program execution takes at most 1358 cycles, and so on.
     299Note that the synthesised time bound for \lstinline'count'---$178+214*(1+\text{\lstinline'len'})$ cycles---is parametric in the length of the array.
     300The CVC3 SMT solver~\cite{DBLP:conf/cav/BarrettT07} closes all obligations within 30 seconds on commodity hardware.
     301A simpler non-parametric version can be solved in seconds.
     302
     303\subsection{A brief introduction to Matita}
    130304
    131305We now briefly introduce Matita, the interactive theorem prover that was used in CerCo to certify all proofs.
Note: See TracChangeset for help on using the changeset viewer.