Changeset 2941
- Timestamp:
- Mar 22, 2013, 9:46:18 PM (8 years ago)
- Location:
- Deliverables/Dissemination/proof-structured-traces
- Files:
-
- 5 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/Dissemination/proof-structured-traces/compiler.svg
r2585 r2941 178 178 transform="scale(-0.6,-0.6)" /> 179 179 </marker> 180 <inkscape:perspective 181 id="perspective2895" 182 inkscape:persp3d-origin="0.5 : 0.33333333 : 1" 183 inkscape:vp_z="1 : 0.5 : 1" 184 inkscape:vp_y="0 : 1000 : 0" 185 inkscape:vp_x="0 : 0.5 : 1" 186 sodipodi:type="inkscape:persp3d" /> 187 <inkscape:perspective 188 id="perspective2920" 189 inkscape:persp3d-origin="0.5 : 0.33333333 : 1" 190 inkscape:vp_z="1 : 0.5 : 1" 191 inkscape:vp_y="0 : 1000 : 0" 192 inkscape:vp_x="0 : 0.5 : 1" 193 sodipodi:type="inkscape:persp3d" /> 194 <marker 195 inkscape:stockid="Arrow2Mend" 196 orient="auto" 197 refY="0" 198 refX="0" 199 id="Arrow2Mend-8" 200 style="overflow:visible"> 201 <path 202 id="path3678-01" 203 style="font-size:12px;fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round" 204 d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z" 205 transform="scale(-0.6,-0.6)" /> 206 </marker> 180 207 </defs> 181 208 <sodipodi:namedview … … 186 213 inkscape:pageopacity="0.0" 187 214 inkscape:pageshadow="2" 188 inkscape:zoom=" 2"189 inkscape:cx=" 225.5371"190 inkscape:cy="5 36.39819"215 inkscape:zoom="4" 216 inkscape:cx="123.51808" 217 inkscape:cy="505.66774" 191 218 inkscape:document-units="px" 192 inkscape:current-layer="layer 1"219 inkscape:current-layer="layer2" 193 220 showgrid="true" 194 221 showguides="true" … … 199 226 inkscape:window-y="25" 200 227 inkscape:window-maximized="1" 201 inkscape:snap-global=" false">228 inkscape:snap-global="true"> 202 229 <inkscape:grid 203 230 type="xygrid" … … 253 280 <path 254 281 style="fill:none;stroke:#0000ff;stroke-width:1;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:3, 1;stroke-dashoffset:0" 255 d="M 222.5 512.375 C 218.345 512.375 215 515.72 215 519.875 L 215 537.375 L 47.5 537.375 C 43.345 537.375 40 540.72 40 544.875 L 40 549.875 C 40 554.03 43.345 557.375 47.5 557.375 L 222.5 557.375 L 242.5 557.375 C 246.655 557.375 250 554.03 250 549.875 L 250 544.875 L 250 519.875 C 250 515.72 246.655 512.375 242.5 512.375 L 222.5 512.375 z " 256 id="rect4273" /> 282 d="m 222.5,512.375 c -4.155,0 -7.5,3.345 -7.5,7.5 l 0,17.5 -215,0 c -4.155,0 -7.5,3.345 -7.5,7.5 l 0,5 c 0,4.155 3.345,7.5 7.5,7.5 l 222.5,0 20,0 c 4.155,0 7.5,-3.345 7.5,-7.5 l 0,-5 0,-25 c 0,-4.155 -3.345,-7.5 -7.5,-7.5 l -20,0 z" 283 id="rect4273" 284 sodipodi:nodetypes="cccccccccccccc" /> 257 285 <rect 258 286 style="fill:none;stroke:#00ff00;stroke-width:1;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:3, 1;stroke-dashoffset:0" … … 260 288 width="30" 261 289 height="40" 262 x=" 40"290 x="-5" 263 291 y="542.36218" 264 292 ry="7.5" /> … … 306 334 xml:space="preserve" 307 335 style="font-size:8px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:center;text-anchor:middle;fill:#00b600;fill-opacity:1;stroke:none;font-family:LMRoman8;-inkscape-font-specification:LMRoman8" 308 x=" 92.960938"336 x="47.960938" 309 337 y="572.36218" 310 338 id="text4310"><tspan 311 339 sodipodi:role="line" 312 340 id="tspan4312" 313 x=" 92.960938"341 x="47.960938" 314 342 y="572.36218">Cost map</tspan><tspan 315 343 sodipodi:role="line" 316 x=" 92.960938"344 x="47.960938" 317 345 y="582.36218" 318 346 id="tspan4314">generation</tspan></text> … … 389 417 xml:space="preserve" 390 418 style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:center;text-anchor:middle;fill:#000000;fill-opacity:1;stroke:none;font-family:LMSans10;-inkscape-font-specification:LMSans10" 391 x=" 133.83789"419 x="82.837891" 392 420 y="552.36218" 393 421 id="text2852"><tspan 394 422 sodipodi:role="line" 395 423 id="tspan2854" 396 x=" 133.83789"424 x="82.837891" 397 425 y="552.36218">LTL</tspan></text> 398 426 <text 399 427 xml:space="preserve" 400 428 style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:center;text-anchor:middle;fill:#000000;fill-opacity:1;stroke:none;font-family:LMSans10;-inkscape-font-specification:LMSans10" 401 x=" 92.646484"429 x="47.646484" 402 430 y="552.36218" 403 431 id="text2856"><tspan 404 432 sodipodi:role="line" 405 433 id="tspan2858" 406 x=" 92.646484"434 x="47.646484" 407 435 y="552.36218">LIN</tspan></text> 408 436 <text 409 437 xml:space="preserve" 410 438 style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:center;text-anchor:middle;fill:#000000;fill-opacity:1;stroke:none;font-family:LMSans10;-inkscape-font-specification:LMSans10" 411 x=" 55.498047"439 x="10.498047" 412 440 y="552.36218" 413 441 id="text2860"><tspan 414 442 sodipodi:role="line" 415 443 id="tspan2862" 416 x=" 55.498047"444 x="10.498047" 417 445 y="552.36218">ASM</tspan></text> 418 446 <text 419 447 xml:space="preserve" 420 448 style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:center;text-anchor:middle;fill:#000000;fill-opacity:1;stroke:none;font-family:LMSans10;-inkscape-font-specification:LMSans10" 421 x=" 55.303047"449 x="10.303047" 422 450 y="577.36218" 423 451 id="text2864"><tspan 424 452 sodipodi:role="line" 425 453 id="tspan2866" 426 x=" 55.303047"454 x="10.303047" 427 455 y="577.36218">8051</tspan></text> 428 456 <path … … 440 468 <path 441 469 style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)" 442 d="m 55.123439,557.36218 0,10"470 d="m 10.123439,557.36218 0,10" 443 471 id="path2872-36" /> 444 472 <path … … 456 484 <path 457 485 style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)" 458 d="m 115,549.36218 -10,0"486 d="m 70,549.36218 -10,0" 459 487 id="path2874-4-4" /> 460 488 <path 461 489 style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)" 462 d="m 79.999996,549.36218 -9.999996,0"490 d="m 34.999996,549.36218 -9.999996,0" 463 491 id="path2874-4-1" /> 492 <text 493 xml:space="preserve" 494 style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:center;text-anchor:middle;fill:#000000;fill-opacity:1;stroke:none;font-family:LMSans10;-inkscape-font-specification:LMSans10" 495 x="126.44727" 496 y="552.36218" 497 id="text2848-0"><tspan 498 sodipodi:role="line" 499 id="tspan2850-7" 500 x="126.44727" 501 y="552.36218">ERTLptr</tspan></text> 502 <path 503 style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)" 504 d="m 106,549.36218 -10,0" 505 id="path2874-4-2-6" /> 464 506 </g> 465 507 </svg> -
Deliverables/Dissemination/proof-structured-traces/proof-structured-traces.tex
r2589 r2941 32 32 \footnotesize Project FP7-ICT-2009-C-243881 33 33 } 34 \date{CerCo workshop , HiPEAC 2013\\23rd January2013}34 \date{CerCo workshop\\23rd March 2013} 35 35 \maketitle 36 36 … … 50 50 \end{itemize} 51 51 52 Talk will only mention \alert{time} costs; but also do stack. 53 52 54 \bigskip 53 55 \alert{Extract} compiler code from development for practical execution. … … 83 85 Concentrate on cost correctness. 84 86 \begin{itemize} 85 \item Keep changes to \alert{extensional} proof minimal87 \item Keep \alert{extensional} proofs as separate as possible 86 88 \end{itemize} 87 89 } … … 91 93 92 94 \begin{center} 93 \includegraphics[width=0. 7\linewidth]{compiler-plain.pdf}95 \includegraphics[width=0.8\linewidth]{compiler-plain.pdf} 94 96 \end{center} 95 97 … … 107 109 \begin{itemize} 108 110 \item 8051 machine code 109 \item Clight code annotated with \alert{cost labels} 110 \item \alert{Cost map} of cost labels to 8051 clock cycles 111 \end{itemize} 112 \end{itemize} 111 \item Clight code instrumented with costs in 8051 clock cycles 112 \end{itemize} 113 \end{itemize} 114 Instrumentation updates global cost variable; suitable for further analysis and 115 verification. 113 116 } 114 117 … … 337 340 338 341 \onslide<2-> 339 Need to enforce correct call/return structure. 342 \alert{Need to enforce correct call/return structure.} 340 343 341 344 \onslide<3> … … 369 372 370 373 \begin{center} 371 \includegraphics[width=0. 7\linewidth]{compiler.pdf}374 \includegraphics[width=0.8\linewidth]{compiler.pdf} 372 375 \end{center} 373 376 … … 404 407 Split normal simulation proof into three: 405 408 \begin{enumerate} 406 \item \blue{normal} steps become zero or more \blue{normal} steps407 409 \item \blue{call/return} steps become a \blue{call/return} step plus zero or 408 410 more \blue{normal} steps 409 \item \blue{cost} steps are preserved 411 \item \blue{cost} label steps are preserved 412 \item other \blue{normal} steps become zero or more \blue{normal} steps 410 413 \end{enumerate} 411 414 … … 470 473 471 474 \begin{center} 472 \includegraphics[width=0. 7\linewidth]{compiler.pdf}475 \includegraphics[width=0.8\linewidth]{compiler.pdf} 473 476 \end{center} 474 477 … … 492 495 \item Preserving trace structure provides correctness in more challenging 493 496 setting 494 \item F ormal proof still in progress495 \begin{itemize} 496 \item key definitions, structured trace lifting, some simulations done497 \item increasing confidence in approach498 \end{itemize} 499 \item[$\star$] Don't need huge changes to ex isting proofs497 \item Finishing off formal proof 498 \begin{itemize} 499 \item axioms for some regular simulation results 500 \item concentrating on intensional proofs 501 \end{itemize} 502 \item[$\star$] Don't need huge changes to extensional proof techniques 500 503 \end{itemize} 501 504
Note: See TracChangeset
for help on using the changeset viewer.