Changeset 3280 for Deliverables/Dissemination
- Timestamp:
- May 14, 2013, 12:11:54 PM (8 years ago)
- Location:
- Deliverables/Dissemination/front-end/final-review
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/Dissemination/front-end/final-review/front-end.tex
r3278 r3280 131 131 \end{itemize} 132 132 133 At the completion of Period~3, the front end included proofs of correctness134 for all these, extension to stack usage, and considerable refinement of the135 existing formal development.133 At the completion of Period~3, the front end now includes proofs of 134 correctness for all these stages, extension to stack usage, and considerable 135 refinement of the existing formal development. 136 136 137 137 \end{frame} … … 180 180 \blue{CompCert}, provide assurances that such proofs can be completed; so 181 181 certain parts of this proof have been assumed. 182 \item Simulation steps with \red{many cases}, some timessimilar; here we182 \item Simulation steps with \red{many cases}, some very similar; here we 183 183 have identified representative and more challenging cases for detailed 184 184 proof. … … 187 187 \end{frame} 188 188 189 \begin{frame}[fragile] 190 \frametitle{Structure of the Proof} 191 192 \begin{center} 193 \includegraphics[width=0.7\linewidth]{compiler.pdf} 194 \end{center} 195 196 The transition from front-end to back-end marks the change: 197 \begin{itemize} 198 \item From a language with explicit call/return structure and high-level 199 control flow; 200 \item To a language with explicit addresses and control-flow graph. 201 \end{itemize} 202 203 Correspondingly, the proof hands over 204 \begin{itemize} 205 \item From measurable subtraces with labelling that must be checked 206 \blue{sound} and \blue{precise}; 207 \item To \blue{structured traces} which embed these invariants. 208 \end{itemize} 209 210 \end{frame} 211 212 213 % \frame{ 214 % \frametitle{Introduction} 215 216 % D3.4 is the front-end correctness proofs: 217 218 % \begin{description} 219 % \item[Primary focus:] novel \red{intensional} properties: \blue{cost 220 % bound correctness} 221 % \item[Secondary:] usual \red{extensional} result: \blue{functional correctness} 222 % \end{description} 223 224 % Functional correctness for similar compilers already studied in 225 % Leroy et al.'s \blue{CompCert}. 226 % \begin{itemize} 227 % \item Axiomatize similar results 228 % \end{itemize} 229 230 % \medskip 231 % Now have \blue{stack} costs as well as \blue{time} 232 % \begin{itemize} 233 % \item yields stronger overall correctness result 234 % \end{itemize} 235 236 % \medskip 237 % \alert{Extract} compiler code from development for practical execution. 238 239 % \medskip 240 % Informed by earlier formal experiment with a toy compiler. 241 % } 242 243 % TODO: could reuse some of this to make stronger intro? 244 % \frame{ 245 % \frametitle{Motivation for formalisation} 246 247 % \begin{enumerate} 248 % \item Provide \alert{assurance} about labelling approach 249 % \begin{itemize} 250 % \item more complex setting than toy compiler 251 % \end{itemize} 252 % \item demonstrate feasibility of \alert{certified} WCET toolchain 253 % % Future: proof translating compiler to provide checkable WCET certificate? 254 % \item new experiments with certified compilation: 255 % \begin{itemize} 256 % \item deeper use of \alert{dependent types} 257 % \item \alert{executable} semantics in type theory 258 % \item certification of \alert{optimising assembler} 259 % \end{itemize} 260 % \end{enumerate} 261 262 % \bigskip 263 % \pause 264 265 % \bigskip 266 % Concentrate on cost correctness. 267 % \begin{itemize} 268 % \item Keep \alert{extensional} proofs as separate as possible 269 % \end{itemize} 270 % } 271 272 % \frame{ 273 % \frametitle{Outline} 274 % \tableofcontents 275 % } 276 277 % \section{CerCo Compiler} 278 279 % \frame{ 280 % \frametitle{CerCo compiler} 281 282 % \begin{center} 283 % \includegraphics[width=0.8\linewidth]{compiler-plain.pdf} 284 % \end{center} 285 286 % \begin{itemize} 287 % \item Reuse unverified CompCert parser 288 % %\item Transform away troublesome constructs 289 % % \begin{itemize} 290 % % \item e.g.~\texttt{switch} 291 % % \item fallthrough requires slightly more sophisticated labelling 292 % % \item but not fundamentally different 293 % % \end{itemize} 294 % \item Intermediate language for most passes 295 % \item Executable semantics for each 296 % \item Outputs 297 % \begin{itemize} 298 % \item 8051 machine code 299 % \item Clight code instrumented with costs in 8051 clock cycles and 300 % bytes of stack space 301 % \end{itemize} 302 % \end{itemize} 303 % Instrumentation updates global cost variable; suitable for further analysis and 304 % verification. 305 % } 306 307 % \section{Overall correctness} 308 309 % \begin{frame}[fragile] 310 % \frametitle{Correctness of labelling approach} 311 312 % \begin{tabular}{ccc} 313 314 % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 315 % emph={[2]_cost3},emphstyle={[2]\color{blue}}] 316 % char f(char x) { 317 % char y; 318 % _cost3: 319 % if (x>10) { 320 % _cost1: 321 % y = g(x); 322 % } else { 323 % _cost2: 324 % y = 5; 325 % } 326 % return y+1; 327 % } 328 % \end{lstlisting} 329 330 % & 331 332 % \begin{minipage}{9em} 333 % \begin{center} 334 % $\Rightarrow$\\[4ex] 335 % \blue{soundness}\\[2ex] 336 % \red{precision} 337 % \end{center} 338 % \end{minipage} 339 340 % & 341 342 % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 343 % emph={[2]_cost3},emphstyle={[2]\color{blue}}] 344 % "f" 345 % emit _cost3 346 % *** Prologue *** 347 % move A, R06 348 % clear CARRY 349 % ... 350 % branch A <> 0, f10 351 % emit _cost2 352 % imm R00, 5 353 % ... 354 % f10: 355 % emit _cost1 356 % call "g" 357 % ... 358 % \end{lstlisting} 359 360 361 % \end{tabular} 362 363 % From experiments with toy compiler [D2.1, FMICS'12]: 364 % \begin{enumerate} 365 % \item Functional correctness, \emph{including trace of labels} 366 % %\item Source labelling function is sound and precise 367 % %\item Preservation of soundness and precision of labelling 368 % \item Target labelling function is sound and precise 369 % % TODO: detail about soundness and precision? 370 % \item Target cost analysis produces a map of labels to times 371 % \begin{itemize} 372 % \item Accurate for sound and precise labellings 373 % \end{itemize} 374 % %\item Correctness of instrumentation 375 % \end{enumerate} 376 377 % \end{frame} 378 379 % %\frame{ 380 % %\frametitle{} 381 % % 382 % %Due to resource constraints 383 % %\begin{itemize} 384 % %\item Instrumentation is done in language semantics 385 % %\item Soundness and precision of labelling is checked during compilation 386 % % \begin{itemize} 387 % % \item c.f.~translation validation 388 % % \end{itemize} 389 % %\item Focusing effort on novel parts --- cost proofs over functional correctness 390 % %\end{itemize} 391 % % 392 % %} 393 394 % \begin{frame}[fragile] 395 % \frametitle{Overall correctness statement} 396 397 % \begin{center} 398 % \fbox{\( \text{machine time} = \Sigma_{l\in\text{source trace}} \text{costmap}(l) \)} 399 % \end{center} 400 401 % \pause 402 403 % \begin{center} 404 % \begin{tabular}{c@{\hspace{3em}}c@{\hspace{2em}}c} 405 406 % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 407 % emph={[2]_cost3},emphstyle={[2]\color{blue}}] 408 % int f(int x) { 409 % _cost1: 410 % int y = 0; 411 % while (x) { 412 % _cost2: 413 % y = g(y); 414 % x = x - 1; 415 % } 416 % _cost3: 417 % return y; 418 % } 419 % \end{lstlisting} 420 421 % & 422 423 % \begin{uncoverenv}<2-3> 424 % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 425 % emph={[2]_cost3},emphstyle={[2]\color{blue}}] 426 % call f 427 % _cost1 428 % init y 429 % _cost2 430 % call g 431 % ... 432 % return g 433 % assign y 434 % decrement x 435 % test x 436 % _cost2 437 % ... 438 % _cost3 439 % return f 440 % \end{lstlisting} 441 % \end{uncoverenv} 442 443 % & 444 445 % \begin{uncoverenv}<3-5> 446 % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 447 % emph={[2]_cost3},emphstyle={[2]\color{blue}}] 448 % call f 449 % _cost1 450 451 % _cost2 452 % call g 453 % ... 454 % return g 455 456 457 458 % _cost2 459 % ... 460 % _cost3 461 % return f 462 % \end{lstlisting} 463 % \end{uncoverenv} 464 465 % \end{tabular} 466 % \end{center} 467 468 % \begin{overprint} 469 % \onslide<2> 470 % \begin{itemize} 471 % \item Use labels and end of function as measurement points 472 % \item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f' 473 % \end{itemize} 474 475 % \onslide<3-4> 476 % \begin{itemize} 477 % \item Use labels and end of function as measurement points 478 % \item All costs are considered local to the function 479 % \item Actual position of unobservable computation is unimportant 480 % \end{itemize} 481 482 % \onslide<5> 483 % \begin{itemize} 484 % \item Use labels and end of function as measurement points 485 % \item[$\star$] Call suitable subtraces \alert{measurable} 486 % \item[$\star$] Core part is a proof of \alert{termination} 487 % \end{itemize} 488 % \end{overprint} 489 490 % \end{frame} 491 492 % \begin{frame}[fragile] 493 % \frametitle{Correct cost analysis depends on call structure} 494 495 % Two straight-line functions: 496 497 % \begin{center} 498 % \begin{tabular}{p{0.4\linewidth}p{0.4\linewidth}} 499 500 % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 501 % emph={[2]_cost3},emphstyle={[2]\color{blue}}] 502 % "f" 503 % emit _cost1 504 % ... 505 % call "g" 506 % ... 507 % return 508 % \end{lstlisting} 509 510 % & 511 512 % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 513 % emph={[2]_cost3},emphstyle={[2]\color{blue}}, 514 % escapechar=\%] 515 % "g" 516 % emit _cost2 517 % ... 518 % %\only<2->{\blue{increase return address}}% 519 % return 520 % \end{lstlisting} 521 522 % \end{tabular} 523 % \end{center} 524 525 % Total cost should be costmap(\red{\bf\_cost1}) + costmap(\red{\bf\_cost2}). 526 527 % \begin{itemize} 528 % \item<2-> Changing return address skips code from \lstinline'f' 529 % \item<2-> Cost no longer equals sum of cost labels 530 % \end{itemize} 531 532 % \onslide<2-> 533 % \alert{Need to observe correct call/return structure.} 534 535 % \onslide<3> 536 % \emph{Not easy at ASM --- observe earlier in compiler \& maintain.} 537 538 % \end{frame} 539 540 % \section{Front-end correctness} 541 542 % \frame{ 543 % \frametitle{Front-end correctness} 544 545 % Recalling the toy compiler, need 546 % \begin{enumerate} 547 % \item Functional correctness 548 % \item Cost labelling sound and precise 549 % \item\label{it:return} To demonstrate return addresses are correct 550 % \end{enumerate} 551 % % TODO: stack space? from obs, from fnl correctness 552 553 % \bigskip 554 % For~\ref{it:return} we generalise notion of \emph{structured traces} 555 % originally introduced for the correctness of timing analysis. 556 % } 557 558 \begin{frame}[fragile] 559 \frametitle{Structured traces} 560 561 Embed call structure and label invariants into execution traces. 562 563 \begin{center} 564 \includegraphics{strtraces.pdf} 565 \end{center} 566 567 \begin{itemize} 568 \item Enforces \blue{invariants} on positions of cost labels. 569 \item \blue{Groups} execution steps according to preceding cost label. 570 \item Forbids \blue{repeating} addresses in grouped steps. 571 \end{itemize} 572 573 Constructed by folding up measurable subtraces, using the fact that labelling 574 is sound and precise. 189 \begin{frame}{Structure of the Proof} 190 191 \begin{center} 192 \includegraphics[width=0.7\linewidth]{compiler.pdf} 193 \end{center} 194 195 The transition from front-end to back-end marks the change: 196 \begin{itemize} 197 \item From a language with explicit call/return structure and high-level 198 structured control flow; 199 \item To a language where all control flow is unconstrained jumps. 200 \end{itemize} 201 202 Correspondingly, the proof hands over 203 \begin{itemize} 204 \item From measurable subtraces with labelling that must be checked 205 \blue{sound} and \blue{precise}; 206 \item To \blue{structured traces} which embed these invariants. 207 \end{itemize} 208 209 \end{frame} 210 211 \begin{frame}{Structured Traces} 212 213 Embed call structure and label invariants into execution traces. 214 215 \begin{center} 216 \includegraphics{strtraces.pdf} 217 \end{center} 218 \vspace*{-\bigskipamount} 219 \begin{itemize} 220 \item Enforces \blue{invariants} on positions of cost labels. 221 \item \blue{Groups} execution steps according to preceding cost label. 222 \item Forbids \blue{repeating} addresses in grouped steps. 223 \end{itemize} 224 225 Constructed by folding up \red{measurable subtraces}, using their termination 226 and the fact that labelling is \blue{sound} and \blue{precise}. 575 227 576 228 \end{frame} … … 578 230 \begin{frame}{Step-by-Step: Getting to Labelled Source} 579 231 580 \blue{C $\to$ Clight}581 582 \smallskip %583 To translate from C to Clight we reuse the CompCert parser.584 585 \bigskip %586 \blue{Switch Removal}587 588 \smallskip %589 Control flow for \red{\lstinline'switch'} is too subtle for simple labelling; 590 we replace with an \red{\lstinline'if .. then .. else'} tree. Proof requires 591 tracking memory extension for an extra test variable.592 593 \bigskip %594 \blue{Cost Labels}595 596 \smallskip %597 Labels added at function start, branch targets, \dots598 599 \smallskip %600 Simulation of execution is exact, just skipping over labels.232 \blue{C $\to$ Clight} 233 234 \smallskip % 235 To translate from C to Clight we reuse the CompCert parser. 236 237 \bigskip % 238 \blue{Switch Removal} 239 240 \smallskip % 241 Control flow for \red{\lstinline'switch'} is too subtle for simple 242 labelling; we replace with an \red{\lstinline'if .. then .. else'} tree. 243 Proof requires tracking memory extension for an extra test variable. 244 245 \bigskip % 246 \blue{Cost Labels} 247 248 \smallskip % 249 Labels added at function start, branch targets, \dots 250 251 \smallskip % 252 Simulation of execution is exact, just skipping over labels. 601 253 602 254 \end{frame} … … 619 271 In addition, to link this with the source program: 620 272 \begin{itemize} 621 \item The observables for the R Labs \blue{prefix} and \blue{structured273 \item The observables for the RTLabs \blue{prefix} and \blue{structured 622 274 trace} are the same as for their counterparts in Clight. 623 275 \end{itemize} … … 625 277 \end{frame} 626 278 627 628 % \section{Correctness proofs} 629 % \subsection{Generic lifting result} 630 631 \begin{frame}[fragile] 632 \frametitle{Lifting measurable traces} 633 634 For each pass find a target \alert{measurable} subtrace 635 \alert{equivalent} to any source \alert{measurable} subtrace. 636 637 \bigskip 638 639 \onslide<2-> 640 \begin{center} 641 \includegraphics{meassim.pdf} 642 \end{center} 643 644 Split normal simulation proof: 645 \begin{enumerate} 646 \item each \blue{call} becomes a \blue{call} step plus zero or 647 more \blue{normal} steps;\\ 648 following cost labels should stay next to the call step 649 \item each \blue{return} becomes a \blue{return} plus zero or 650 more \blue{normal} steps 651 \item \blue{cost} label steps are preserved 652 \item other \blue{normal} steps become zero or more \blue{normal} steps 653 \end{enumerate} 654 655 \bigskip 656 \onslide<3-> 657 Preserves the defining termination property for \alert{measurable} subtraces. 658 659 % \bigskip 660 % \onslide<4-> 661 % Due to time pressures, check \alert{soundness} and \alert{precision} of cost 662 % labels at RTLabs. 663 664 \end{frame} 665 666 %\begin{frame}[fragile] 667 %\frametitle{Structured trace simulation} 668 % 669 %Lift \alert{local} simulations to \alert{structured trace} simulations 670 %similarly. 671 % 672 %\bigskip 673 %\pause 674 %\begin{itemize} 675 %\item 676 %Require local simulations for \alert{normal}, \alert{call} and \alert{return} 677 %steps 678 %\item allow traces to expand with extra \alert{normal} steps, 679 %\item allow us to collapse some \alert{normal} steps 680 % \begin{itemize} 681 % \item but not collapse \blue{labelled} steps 682 % % TODO: why? avoid larger change in structure 683 % \item or change call structure 684 % \end{itemize} 685 %\end{itemize} 686 % 687 %\bigskip 688 %Sufficient to calculate structured trace in target. 689 %% TODO: pics 690 % 691 %\end{frame} 692 % 693 %\begin{frame}[fragile] 694 %\frametitle{Structured trace local simulation example} 695 % 696 %For function call steps: 697 %\begin{center} 698 %\includegraphics[width=0.7\linewidth]{strcall.pdf} 699 %\end{center} 700 % 701 %\begin{itemize} 702 %\item May add extra steps before and after 703 %\item Extra steps must not be call/return 704 %\item Must call the same function 705 %\item Cost label must stay at start of function 706 %\end{itemize} 707 % 708 %\end{frame} 709 710 % \subsection{Simulations for compiler passes} 711 712 %\frame{ 713 %\frametitle{TODO: at least two slides on simulations} 714 %} 715 716 % TODO: perhaps much earlier for the pre-measurable bits? 717 718 \frame{ 719 \frametitle{Front-end simulation results} 720 Cast simplification 721 \begin{itemize} 722 \item Simplify expressions for 8-bit target 723 \item Only expressions change --- statements are in lock-step 724 \item Difficult part: we allow ill-typed \textbf{Clight} at this stage 725 \item Simulation proofs complete 726 \end{itemize} 727 728 \textbf{Clight} to \textbf{Cminor} 729 \begin{itemize} 730 \item Stack allocation and control flow transformation 731 \item Similar to \textbf{CompCert}, but produces \lstinline'goto' 732 instead of \lstinline'loop' 733 \item Expressions complete 734 \item Prove a selection of statements, in particular \lstinline'while' 735 \item Tricky: Large proof terms for invariant embedded in 736 \textbf{Cminor} programs using dependent types;\\ 737 generalise them away, but difficult under binders 738 %TODO explain clearly 739 \end{itemize} 740 } 741 \frame{ 742 \frametitle{Front-end simulation results} 743 \textbf{Cminor} to \textbf{RTLabs} 744 \begin{itemize} 745 \item Construction of control-flow graph 746 \item Axiomatized simulations 747 \item But do have invariants: 748 \begin{itemize} 749 \item Statement well-typed with respect to pseudo-register 750 environment 751 \item CFG complete 752 \item Entry and exit nodes complete, unique 753 \end{itemize} 754 \item Translation function is \emph{total} as a result 755 \end{itemize} 756 } 757 758 % TODO: sloganize: proved more about unusual bits 759 760 % \section{Checking cost labelling properties} 761 762 \frame{ 763 \frametitle{Checking cost labelling properties} 764 765 Check cost labelling is \red{sound} and \blue{precise} at 766 \textbf{RTLabs}. 767 \begin{itemize} 768 \item Shortcut; similar to translation validation 769 \end{itemize} 770 771 \medskip 772 At \textbf{RTLabs} properties become 773 \begin{description} 774 \item[\red{soundness}] bound on number of instructions in CFG until label\\ 775 label at start of every function 776 \item[\blue{precision}] label after every branch 777 \end{description} 778 779 \medskip 780 Bound is the hard part; the rest is a simple syntactic check. 781 } 782 783 \begin{frame}[fragile] 784 \frametitle{Bound on number of instructions until label} 785 786 \begin{center} 787 \includegraphics<1>[width=.4\linewidth]{loop.pdf} 788 \includegraphics<2>[width=.4\linewidth]{loop1.pdf} 789 \includegraphics<3>[width=.4\linewidth]{loop2.pdf} 790 \includegraphics<4>[width=.4\linewidth]{loop3.pdf} 791 \includegraphics<5>[width=.4\linewidth]{loop4.pdf} 792 \includegraphics<6>[width=.4\linewidth]{loopx.pdf} 793 \end{center} 794 795 \begin{itemize} 796 \item Pick an arbitrary node in the CFG 797 \item<2-> Follow successor instructions 798 \item<4-> If we find a \alert{cost label} all the traced nodes have a bound\dots 799 \item<5-> \dots so remove them and pick a new node, continue 800 \item<6-> But if we find an \alert{unlabelled loop} the labelling is unsound, 801 report an error 802 \end{itemize} 803 804 \end{frame} 805 806 \frame{ 807 \frametitle{Checking cost labelling properties} 808 809 This compile-time check is 810 \begin{itemize} 811 \item[$-$] partial 812 \item[$-$] extra work in compilation 813 \item[$\mp$] not proving anything about compilation passes 814 \item[$+$] less proof burden 815 \end{itemize} 816 817 \bigskip 818 In a full proof would go from 819 \begin{quote} 820 cost labels at the head of loops in \textbf{Cminor} 821 \end{quote} 822 to 823 \begin{quote} 824 bound on instructions to cost label in \textbf{RTLabs} 825 \end{quote} 826 Showing existence of the bound alone likely to require at least as much 827 proof effort as this check. 828 829 } 830 831 % \section{Construction of structured traces} 832 833 \frame{ 834 \frametitle{Construction of structured traces} 835 \begin{center} 836 \includegraphics{strtraces.pdf} 837 \end{center} 838 \begin{enumerate} 839 \item Extend sound and precise labelling to semantic states 840 \item Prove they are preserved by steps of semantics 841 \item Prove \textbf{RTLabs} semantics preserve the stack 842 \item Use \alert{termination} proof from \alert{measurable} subtrace 843 to create structure 844 \item Proof obligations for cost labelling are discharged by semantic 845 results above 846 \end{enumerate} 847 } 848 849 % \section{Whole compiler} 850 851 \begin{frame}[fragile] 852 \frametitle{Putting the proof together} 853 854 \begin{center} 855 \includegraphics[width=0.8\linewidth]{compiler.pdf} 856 \end{center} 857 858 \begin{itemize} 859 \item `Clock' difference in Clight is sum of cost labels 860 \item Observables, including trace of labels, is preserved to ASM 861 \item Labelling at bottom level is sound and precise 862 \item Sum of labels at ASM is equal to difference in real clock 863 \end{itemize} 864 865 \end{frame} 866 867 \frame{ 868 \frametitle{Conclusion} 869 870 Sketched proof for formalised CerCo front-end 871 872 \begin{itemize} 873 \item Intensional proofs can be layered on top of extensional results 874 \item Preserving call-structure key ingredient 875 \item Compile-time cost labelling checks can reduce proof burden 876 \item[$\star$] Don't need huge changes to extensional proof techniques 877 \end{itemize} 878 879 \pause 880 Future: 881 \begin{itemize} 882 \item Expect results to generalise to more general labelling schemes 883 \begin{itemize} 884 \item hence more sophisticated targets 885 \end{itemize} 886 \item Other compiler correctness techniques 887 \begin{itemize} 888 \item Decompilation? 889 \end{itemize} 890 \end{itemize} 891 892 } 893 279 \begin{frame}{Lifting Measurable Traces} 280 281 For each pass find a target \red{measurable subtrace} equivalent to any 282 source \red{measurable subtrace}. 283 284 \begin{center} 285 \includegraphics{meassim.pdf} 286 \end{center} 287 288 Split normal simulation proof: 289 \begin{enumerate} 290 \item each \blue{call} becomes a \blue{call} step plus zero or more 291 \blue{normal} steps; following cost labels should stay next to the call 292 step 293 \item each \blue{return} becomes a \blue{return} plus zero or 294 more \blue{normal} steps 295 \item \blue{cost} label steps are preserved 296 \item other \blue{normal} steps become zero or more \blue{normal} steps 297 \end{enumerate} 298 299 This preserves the defining property for \red{measurable subtraces}. 300 301 \end{frame} 302 303 \begin{frame}{Front-End Simulation Results} 304 \blue{Cast simplification} 305 \begin{itemize} 306 \item Simplify expressions for 8-bit target. 307 \item Only expressions change --- statements are in lock-step. 308 \end{itemize} 309 310 \blue{Clight to Cminor} 311 \begin{itemize} 312 \item Stack allocation and control flow transformation. 313 \item Similar to \blue{CompCert}, but using \red{\lstinline'goto'} instead 314 of \red{\lstinline'loop'} 315 \item Large proof terms for invariants embedded in Cminor programs using 316 dependent types. 317 \end{itemize} 318 319 \blue{Cminor to RTLabs} 320 \begin{itemize} 321 \item Construction of control-flow graph. 322 \item Embedded invariants mean that translation function is \red{total}. 323 \end{itemize} 324 \end{frame} 325 326 \begin{frame}{Checking Cost Labelling} 327 328 Building structured traces in \blue{RTLabs} depends on having cost labelling 329 on the linear trace that is \red{sound} and \red{precise}. 330 331 \medskip % 332 Instead of carrying this as an invariant all the way through each previous 333 pass, we take a \blue{shortcut} and check on the spot. 334 335 \medskip % 336 This is similar to \blue{translation validation}. 337 338 \medskip % 339 The specific requirements for labelling \blue{RTLabs} code are: 340 \begin{description}[\red{soundness}] 341 \item[\red{soundness}] At every point, a finite bound on the number of 342 instructions until the next label; 343 \item[\red{soundness}] A label at the start of every function; 344 \item[\red{precision}] A label after every branch. 345 \end{description} 346 347 \medskip % 348 The bound is the hard part; the rest is a simple syntactic check. 349 \end{frame} 350 351 \begin{frame}[fragile]{Checking Bound to Next Label} 352 353 \begin{center} 354 \begin{overprint}[0.5\linewidth] 355 \onslide<1>\includegraphics[width=0.8\linewidth]{loop.pdf} 356 \onslide<2>\includegraphics[width=0.8\linewidth]{loop1.pdf} 357 \onslide<3>\includegraphics[width=0.8\linewidth]{loop2.pdf} 358 \onslide<4>\includegraphics[width=0.8\linewidth]{loop3.pdf} 359 \onslide<5>\includegraphics[width=0.8\linewidth]{loop4.pdf} 360 \onslide<6->\includegraphics[width=0.8\linewidth]{loopx.pdf} 361 \end{overprint} 362 \end{center} 363 \begin{itemize} 364 \item Pick an arbitrary node in the CFG; 365 \item<2-> Follow successor instructions; 366 \item<4-> If we find a \alert{cost label} all the traced nodes have a 367 bound\dots 368 \item<5-> \dots so remove them and pick a new node, continue; 369 \item<6-> But if we find an \alert{unlabelled loop} then the labelling is 370 unsound, report an error. 371 \end{itemize} 372 373 \onslide<7-> 374 When complete, we have a proof that every loop contains a label. 375 376 \end{frame} 377 378 \begin{frame}{Checking Cost Labelling} 379 380 This check of soundness and precision in RTLabs: 381 \begin{itemize} 382 \item Is partial --- will only succeed when invariants hold; 383 \item Extracts to additional checking code in the compiler; 384 \item[\checkmark] Significantly reduces the proof effort. 385 \end{itemize} 386 387 \medskip % 388 The last point is our key observation: a conventional proof would require 389 showing that: 390 \begin{quote} 391 \red{If} every loop in \blue{Cminor} code is headed by a cost label; 392 \\[1\jot] 393 \red{Then} at every point in every \blue{RTLabs} execution there is a 394 finite bound on the number of instructions until the next cost label. 395 \end{quote} 396 We expect that proving existence in general of this bound alone to be 397 considerably harder than the whole check. 398 399 \end{frame} 400 401 \begin{frame}{Putting the Proofs Together} 402 403 \begin{center} 404 \includegraphics[width=0.7\linewidth]{compiler.pdf} 405 \end{center} 406 407 The front-end proof demonstrates that for any Clight execution: 408 \begin{itemize} 409 \item We have a corresponding \blue{structured trace} with \blue{invariants} 410 \dots 411 \item \dots and with the same \blue{observables} of labels and call/return. 412 \end{itemize} 413 414 The back-end proof takes this structured trace and shows that 415 \begin{itemize} 416 \item There is a corresponding assembler trace \dots 417 \item \dots with \blue{sound} and \blue{precise} labelling and the same 418 \blue{observables}. 419 \end{itemize} 420 421 Combining these gives a proof that time and space costs computed on the 422 source are exactly those observed on executing the binary. 423 424 \end{frame} 425 426 \begin{frame}{Summary} 427 428 CerCo WP3 has produced the front-end of a C-to-8051 compiler that annotates 429 C source with runtime cycle counts and stack space. 430 431 \medskip % 432 This is formalised in the Matita proof assistant, with a proof of 433 correctness, and can be extracted as an executable compiler. 434 435 \smallskip % 436 \begin{itemize} 437 \item Modular \blue{layering} of intensional proofs over extensional 438 results; 439 \item Extensional results richer than normal and carefully chosen, but do 440 not require large changes to proof techniques. 441 \item \blue{Compile-time checks} on intermediate code reduce proof effort. 442 \item \blue{Structured traces} as a repository for invariant information. 443 \item \blue{Measurable subtraces} as a unit of cost proof. 444 \end{itemize} 445 446 \smallskip % 447 Going beyond this, in future projects (REMS, \dots) we plan to: 448 \begin{itemize} 449 \item Generalize labelling schemes for more sophisticated targets; 450 \item Apply \blue{decompilation} to jump the gap from source to binary. 451 \end{itemize} 452 453 \end{frame} 894 454 \end{document} 895 455 896 456 % LocalWords: LFCS Matita CerCo intensional WCET toolchain CompCert Clight ASM 897 % LocalWords: reexecutes subtrace RTLabs subtraces 457 % LocalWords: reexecutes subtrace RTLabs subtraces Garnier McKinna cerco 458 % LocalWords: Axiomatization axiomatized Cminor goto -
Deliverables/Dissemination/front-end/final-review/front-end.vrb
r3278 r3280 1 \frametitle {Putting the proof together} 1 \frametitle {Checking Bound to Next Label}\par \begin{center} 2 \begin{overprint}[0.5\linewidth] 3 \onslide<1>\includegraphics[width=0.8\linewidth]{loop.pdf} 4 \onslide<2>\includegraphics[width=0.8\linewidth]{loop1.pdf} 5 \onslide<3>\includegraphics[width=0.8\linewidth]{loop2.pdf} 6 \onslide<4>\includegraphics[width=0.8\linewidth]{loop3.pdf} 7 \onslide<5>\includegraphics[width=0.8\linewidth]{loop4.pdf} 8 \onslide<6->\includegraphics[width=0.8\linewidth]{loopx.pdf} 9 \end{overprint} 10 \end{center} 11 \begin{itemize} 12 \item Pick an arbitrary node in the CFG; 13 \item<2-> Follow successor instructions; 14 \item<4-> If we find a \alert{cost label} all the traced nodes have a 15 bound\dots 16 \item<5-> \dots so remove them and pick a new node, continue; 17 \item<6-> But if we find an \alert{unlabelled loop} then the labelling is 18 unsound, report an error. 19 \end{itemize} 2 20 3 \begin{center} 4 \includegraphics[width=0.8\linewidth]{compiler.pdf} 5 \end{center} 21 \onslide<7-> 22 When complete, we have a proof that every loop contains a label. 6 23 7 \begin{itemize}8 \item `Clock' difference in Clight is sum of cost labels9 \item Observables, including trace of labels, is preserved to ASM10 \item Labelling at bottom level is sound and precise11 \item Sum of labels at ASM is equal to difference in real clock12 \end{itemize}13
Note: See TracChangeset
for help on using the changeset viewer.