Changeset 3643
 Timestamp:
 Mar 8, 2017, 4:51:29 PM (8 months ago)
 Location:
 Papers/jarcerco2017
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Papers/jarcerco2017/architecture.tex
r3623 r3643 7 7 \section{Compiler architecture} 8 8 \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 >=stealth39 ]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 (tleft);54 \draw [>] (cerco)  (cost);55 \draw [>] ([yshift=1ex]cerco.south west) coordinate (t) 56 node {C source+\color{red}{cost annotations}}57 (tleft) 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 (tleft) 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 (tleft) coordinate (ded in) .. controls +(.5, 0) and +(.5, 0) .. (out);65 \draw [>] ([yshift=1ex]ded.south west) coordinate (t) 66 node {complexity obligations}67 (tleft) coordinate (out);68 \draw [<] ([yshift=1ex]check.north west) coordinate (t) 69 node {complexity proof}70 (tleft) .. 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 % head76 \draw (current bounding box.west) ++(.2,.5)77 circle (.2) ++(0,.2)  ++(0,.1) coordinate (t);78 % arms79 \draw (t)  +(.3,.2);80 \draw (t)  +(.3,.2);81 % body82 \draw (t)  ++(0,.4) coordinate (t);83 % legs84 \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 array89 that are less than or equal to a given threshold. On the right: CerCo's interaction90 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 right94 of~\autoref{test1}) on an example program (on the left95 of~\autoref{test1}). The user writes the program and feeds it to the96 CerCo compiler, which outputs an instrumented version of the same97 program that updates global variables that record the elapsed98 execution time and the stack space usage. The red lines in99 \autoref{itest1} introducing variables, functions and function calls100 starting with \lstinline'__cost' and \lstinline'__stack' are the instrumentation introduced by the101 compiler. For example, the two calls at the start of102 \lstinline'count' say that 4 bytes of stack are required, and that it103 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 complexity107 assertions in the style of Hoare logic, that are passed to a deductive108 platform (in our case FramaC). We provide as a FramaC cost plugin a109 simple automatic synthesiser for complexity assertions which can110 be overridden by the user to increase or decrease accuracy. These are the blue111 comments starting with \lstinline'/*@' in \autoref{itest1}, written in112 FramaC's specification language, ACSL. From the113 assertions, a general purpose deductive platform produces proof114 obligations which in turn can be closed by automatic or interactive115 provers, ending in a proof certificate.116 117 % NB: if you try this example with the live CD you should increase the timeout118 119 Twelve proof obligations are generated from~\autoref{itest1} (to prove120 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 of123 the array. The CVC3 prover124 closes all obligations within half a minute on routine commodity125 hardware. A simpler nonparametric version can be solved in a few126 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 invariant155 __cost <= \at(__cost,__l)+156 214*(__max(\at((lenj)+1,__l), 0)__max(1+(lenj), 0));157 for stack_cost: loop invariant158 __stack_max == \at(__stack_max,__l);159 for stack_cost: loop invariant160 __stack == \at(__stack,__l);161 loop variant lenj;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 invariants189 added by the CerCo FramaC plugin in blue. The \lstinline'__cost',190 \lstinline'__stack' and \lstinline'__stack_max' variables hold the elapsed time191 in clock cycles and the current and maximum stack usage. Their initial values192 hold the clock cycles spent in initialising the global data before calling193 \lstinline'main' and the space required by global data (and thus unavailable for194 the stack).195 }196 \label{itest1}197 \end{figure}198 9 199 10 \subsection{The compiler} 
Papers/jarcerco2017/cerco.bib
r3642 r3643 210 210 isbn = {9781841501765}, 211 211 } 212 213 @misc 214 { acsl, 215 title = {{ACSL}: the {ANSI}/{ISO} {C} specification language, reference manual}, 216 url = {https://framac.com/download/acsl_1.4.pdf}, 217 note = {Accessed March 2017}, 218 year = {2017}, 219 key = {acslthe} 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 37, 2007, Proceedings}, 228 pages = {298302}, 229 year = {2007}, 230 crossref = {DBLP:conf/cav/2007}, 231 url = {http://dx.doi.org/10.1007/9783540733683_34}, 232 doi = {10.1007/9783540733683_34}, 233 timestamp = {Mon, 03 Sep 2007 13:24:22 +0200}, 234 biburl = {http://dblp.unitrier.de/rec/bib/conf/cav/BarrettT07}, 235 bibsource = {dblp computer science bibliography, http://dblp.org} 236 } 237 212 238 213 239 @article{DBLP:journals/corr/abs12024905, 
Papers/jarcerco2017/introduction.tex
r3642 r3643 127 127 With these methods, we enable the use of more offtheshelf components (e.g. provers and invariant generators) whilst reducing the trusted code base at the same time. 128 128 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} 134 char a[] = {3, 2, 7, 14}; 135 char threshold = 4; 136 137 int 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 148 int 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 (tleft); 173 \draw [>] (cerco)  (cost); 174 \draw [>] ([yshift=1ex]cerco.south west) coordinate (t)  175 node {C source+\color{red}{cost annotations}} 176 (tleft) 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 (tleft) 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 (tleft) coordinate (ded in) .. controls +(.5, 0) and +(.5, 0) .. (out); 184 \draw [>] ([yshift=1ex]ded.south west) coordinate (t)  185 node {complexity obligations} 186 (tleft) coordinate (out); 187 \draw [<] ([yshift=1ex]check.north west) coordinate (t)  188 node {complexity proof} 189 (tleft) .. 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 227 char 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 */ 235 int 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((lenj)+1,__l), 0)__max(1+(lenj), 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 lenj; 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 */ 264 int 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 FramaC plugin in blue. 273 The \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 274 hold 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 276 the stack). 277 } 278 \label{itest1} 279 \end{figure} 280 281 How should a Software Engineer use our tool in anger? 282 We 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}. 283 An 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. 284 Figure~\ref{itest1} demonstrates one of the outputs of the CerCo C compileran embellished version of the original C source code, with cost annotations automatically inserted, the other output being an object code file, not included here. 285 The 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. 286 For 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). 287 The 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 289 The 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 FramaC~\cite{framac}). 290 We have written a simple automatic synthesiser for complexity assertions as a plugin for FramaC. 291 The behaviour of this plugin can be overridden by the user to increase or decrease accuracy. 292 These are the blue comments starting with \lstinline'/*@' in Figure~\ref{itest1}, written in FramaC's specification language, ACSL~\cite{acsl}. 293 From 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 297 Twelve proof obligations are generated from Figure~\ref{itest1}. 298 These 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. 299 Note that the synthesised time bound for \lstinline'count'$178+214*(1+\text{\lstinline'len'})$ cyclesis parametric in the length of the array. 300 The CVC3 SMT solver~\cite{DBLP:conf/cav/BarrettT07} closes all obligations within 30 seconds on commodity hardware. 301 A simpler nonparametric version can be solved in seconds. 302 303 \subsection{A brief introduction to Matita} 130 304 131 305 We 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.