Changeset 3280


Ignore:
Timestamp:
May 14, 2013, 12:11:54 PM (4 years ago)
Author:
stark
Message:

Front end final review talk?

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  
    131131  \end{itemize}
    132132
    133   At the completion of Period~3, the front end included proofs of correctness
    134   for all these, extension to stack usage, and considerable refinement of the
    135   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.
    136136 
    137137\end{frame}
     
    180180    \blue{CompCert}, provide assurances that such proofs can be completed; so
    181181    certain parts of this proof have been assumed.
    182   \item Simulation steps with \red{many cases}, sometimes similar; here we
     182  \item Simulation steps with \red{many cases}, some very similar; here we
    183183    have identified representative and more challenging cases for detailed
    184184    proof.
     
    187187\end{frame}
    188188
    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}.
    575227
    576228\end{frame}
     
    578230\begin{frame}{Step-by-Step: Getting to Labelled Source}
    579231
    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, \dots
    598 
    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.
    601253
    602254\end{frame}
     
    619271  In addition, to link this with the source program:
    620272  \begin{itemize}
    621   \item The observables for the RLabs \blue{prefix} and \blue{structured
     273  \item The observables for the RTLabs \blue{prefix} and \blue{structured
    622274      trace} are the same as for their counterparts in Clight.
    623275  \end{itemize}
     
    625277\end{frame}
    626278
    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}
    894454\end{document}
    895455
    896456% 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}
    220
    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.
    623
    7 \begin{itemize}
    8 \item `Clock' difference in Clight is sum of cost labels
    9 \item Observables, including trace of labels, is preserved to ASM
    10 \item Labelling at bottom level is sound and precise
    11 \item Sum of labels at ASM is equal to difference in real clock
    12 \end{itemize}
    13 
Note: See TracChangeset for help on using the changeset viewer.