 Timestamp:
 Jun 4, 2013, 6:19:47 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/fopara2013/fopara13.tex
r3309 r3310 7 7 \usepackage{color} 8 8 \usepackage{fancybox} 9 \usepackage{fancyvrb} 9 10 \usepackage{graphicx} 10 11 \usepackage[colorlinks]{hyperref} … … 20 21 %\def\lstlanguagefiles{lstgrafite.tex} 21 22 %\lstset{language=Grafite} 23 \lstset{language=C} 22 24 23 25 \newlength{\mylength} … … 234 236 I/O operations can be performed in the prefix of the run, but not in the measurable subrun. Therefore we prove that we can predict reaction times, but not I/O times, as it should be. 235 237 238 \begin{figure}[t] 239 \begin{lstlisting} 240 char a[] = {3, 2, 7, 4}; 241 char treshold = 4; 242 243 int main() { 244 char j; 245 char *p = a; 246 int found = 0; 247 for (j=0; j < 4; j++) { 248 if (*p <= treshold) { found++; } 249 p++; 250 } 251 return found; 252 } 253 \end{lstlisting} 254 \caption{A simple C program.} 255 \label{test1} 256 \end{figure} 257 258 \fvset{commandchars=\\\{\}} 259 260 \lstset{morecomment=[s][\color{blue}]{/*@}{*/}, 261 moredelim=[is][\color{blue}]{$}{$}, 262 moredelim=[is][\color{red}]{}{}} 263 264 265 \begin{figure}[!p] 266 \begin{lstlisting} 267 int __cost = 33; int __stack = 5, __stack_max = 5; 268 269 void __cost_incr(int incr) { __cost = __cost + incr; } 270 271 void __stack_incr(int incr) { 272 __stack = __stack + incr; 273 __stack_max = __stack_max < __stack ? __stack : __stack_max; 274 } 275 276 unsigned char a[4] = { 3, 2, 7, 252, }; 277 unsigned char treshold = 4; 278 279 /*@ behavior stack_cost: 280 ensures __stack_max <= 281 __max(\old(__stack_max), \old(__stack)); 282 ensures __stack == \old(__stack); 283 284 behavior time_cost: 285 ensures __cost <= \old(__cost)+1228; */ 286 int main(void) 287 { 288 char j; 289 char *p; 290 int found; 291 __stack_incr(0); __cost_incr(91); 292 p = a; 293 found = 0; 294 $__l: /* internal */$ 295 /*@ for time_cost: loop invariant 296 __cost <= 297 \at(__cost,__l)+220*(__max(\at(5j,__l), 0)__max (5j, 0)); 298 for stack_cost: loop invariant 299 __stack_max == \at(__stack_max,__l); 300 for stack_cost: loop invariant 301 __stack == \at(__stack,__l); 302 loop variant 4j; */ 303 for (j = 0; j < 4; j++) { 304 __cost_incr(76); 305 if (*p <= treshold) { 306 __cost_incr(144); 307 found++; 308 } else { 309 __cost_incr(122); 310 } 311 p++; 312 } 313 __cost_incr(37); __stack_incr(0); 314 return found; 315 } 316 \end{lstlisting} 317 \caption{The instrumented version of the program in \autoref{test1}.} 318 \label{itest1} 319 \end{figure} 320 321 236 322 \bibliography{fopara13.bib} 237 323
Note: See TracChangeset
for help on using the changeset viewer.