Changeset 3264 for Deliverables/Dissemination
- Timestamp:
- May 10, 2013, 2:50:19 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/Dissemination/front-end/front-end.tex
r3260 r3264 395 395 \end{frame} 396 396 397 \begin{frame}[fragile]398 \frametitle{Structure in the compiler proof}399 400 \begin{center}401 \includegraphics[width=0.8\linewidth]{compiler.pdf}402 \end{center}403 404 %\onslide<1>405 %\green{Assembler} provides part of local cost analysis (CPP'12).406 407 %\onslide<2-4>408 Switch at RTLabs:409 \begin{itemize}410 \item from \red{measurable} subtrace of \alert{sound} and \alert{precise}411 labelling412 \item to \blue{structured trace} where they are embedded413 \end{itemize}414 415 %\onslide<3>416 %Changes \blue{syntactic} properties of labelling into \blue{semantic}417 %properties.418 419 %\onslide<4>420 Reason for choice: first language with explicit \alert{addresses}, implicit421 \alert{call handling}.422 423 \end{frame}424 425 397 \frame{ 426 398 \frametitle{Front-end correctness statement} … … 442 414 443 415 } 416 417 \begin{frame}[fragile] 418 \frametitle{Structure in the compiler proof} 419 420 \begin{center} 421 \includegraphics[width=0.8\linewidth]{compiler.pdf} 422 \end{center} 423 424 %\onslide<1> 425 %\green{Assembler} provides part of local cost analysis (CPP'12). 426 427 %\onslide<2-4> 428 Switch at RTLabs: 429 \begin{itemize} 430 \item from \red{measurable} subtrace of \alert{sound} and \alert{precise} 431 labelling 432 \item to \blue{structured trace} where they are embedded 433 \end{itemize} 434 435 %\onslide<3> 436 %Changes \blue{syntactic} properties of labelling into \blue{semantic} 437 %properties. 438 439 %\onslide<4> 440 Reason for choice: first language with explicit \alert{addresses}, implicit 441 \alert{call handling}. 442 443 \end{frame} 444 444 445 445 \section{Correctness proofs} … … 520 520 \subsection{Simulations for compiler passes} 521 521 522 \frame{ 523 \frametitle{TODO} 524 } 522 %\frame{ 523 %\frametitle{TODO: at least two slides on simulations} 524 %} 525 526 % TODO: perhaps much earlier for the pre-measurable bits? 527 \frame{ 528 \frametitle{Simulation between input and annotated code} 529 530 Two stages provide the annotated version of input: 531 532 \bigskip 533 Switch removal 534 \begin{itemize} 535 \item \lstinline[language=C]'switch' statement control flow too subtle 536 for simple labelling 537 \item Replaces with \lstinline[language=C]'if ... then ... else' tree 538 \item Tricky part of proof memory extension for extra variable 539 \item Partial proof: validate approach, but not relevant to 540 intensional properties 541 \end{itemize} 542 543 \bigskip 544 Cost labelling 545 \begin{itemize} 546 \item For simulation don't care \emph{which} labels are added 547 \item Just have to skip over extra cost label expressions and 548 statements 549 \item Complete simulation proof, simple 550 \end{itemize} 551 552 % TODO: consider whether to mention full simulation 553 % termination-preserving proof? 554 } 555 556 \frame{ 557 \frametitle{Front-end simulation results} 558 Cast simplification 559 \begin{itemize} 560 \item Simplify expressions for 8-bit target 561 \item Only expressions change --- statements are in lock-step 562 \item Difficult part: we allow ill-typed \textbf{Clight} at this stage 563 \item Simulation proofs complete 564 \end{itemize} 565 566 \textbf{Clight} to \textbf{Cminor} 567 \begin{itemize} 568 \item Stack allocation and control flow transformation 569 \item Similar to \textbf{CompCert}, but produces \lstinline'goto' 570 instead of \lstinline'loop' 571 \item Expressions complete 572 \item Prove a selection of statements, in particular \lstinline'while' 573 \item Tricky: Large proof terms for invariant embedded in 574 \textbf{Cminor} programs using dependent types;\\ 575 generalise them away, but difficult under binders 576 %TODO explain clearly 577 \end{itemize} 578 } 579 \frame{ 580 \frametitle{Front-end simulation results} 581 \textbf{Cminor} to \textbf{RTLabs} 582 \begin{itemize} 583 \item Construction of control-flow graph 584 \item Axiomatized simulations 585 \item But do have invariants: 586 \begin{itemize} 587 \item Statement well-typed with respect to pseudo-register 588 environment 589 \item CFG complete 590 \item Entry and exit nodes complete, unique 591 \end{itemize} 592 \item Translation function is \emph{total} as a result 593 \end{itemize} 594 } 595 596 % TODO: sloganize: proved more about unusual bits 525 597 526 598 \section{Checking cost labelling properties} … … 585 657 likely to be at least as expensive as this check. 586 658 659 } 660 661 \section{Construction of structured traces} 662 663 \frame{ 664 \frametitle{Construction of structured traces} 665 \begin{center} 666 \includegraphics{strtraces.pdf} 667 \end{center} 668 \begin{enumerate} 669 \item Extend sound and precise labelling to semantic states 670 \item Prove they are preserved by steps of semantics 671 \item Prove \textbf{RTLabs} semantics preserve the stack 672 \item Use \alert{termination} proof from \alert{measurable} subtrace 673 to create structure 674 \item Proof obligations for cost labelling are discharged by semantic 675 results above 676 \end{enumerate} 587 677 } 588 678
Note: See TracChangeset
for help on using the changeset viewer.