Ignore:
Timestamp:
Mar 22, 2013, 9:46:18 PM (7 years ago)
Author:
campbell
Message:

Update proof slides.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/Dissemination/proof-structured-traces/proof-structured-traces.tex

    r2589 r2941  
    3232\footnotesize Project FP7-ICT-2009-C-243881
    3333}
    34 \date{CerCo workshop, HiPEAC 2013\\23rd January 2013}
     34\date{CerCo workshop\\23rd March 2013}
    3535\maketitle
    3636
     
    5050\end{itemize}
    5151
     52Talk will only mention \alert{time} costs; but also do stack.
     53
    5254\bigskip
    5355\alert{Extract} compiler code from development for practical execution.
     
    8385Concentrate on cost correctness.
    8486\begin{itemize}
    85 \item Keep changes to \alert{extensional} proof minimal
     87\item Keep \alert{extensional} proofs as separate as possible
    8688\end{itemize}
    8789}
     
    9193
    9294\begin{center}
    93 \includegraphics[width=0.7\linewidth]{compiler-plain.pdf}
     95\includegraphics[width=0.8\linewidth]{compiler-plain.pdf}
    9496\end{center}
    9597
     
    107109  \begin{itemize}
    108110  \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}
     114Instrumentation updates global cost variable; suitable for further analysis and
     115verification.
    113116}
    114117
     
    337340
    338341\onslide<2->
    339 Need to enforce correct call/return structure.
     342\alert{Need to enforce correct call/return structure.}
    340343
    341344\onslide<3>
     
    369372
    370373\begin{center}
    371 \includegraphics[width=0.7\linewidth]{compiler.pdf}
     374\includegraphics[width=0.8\linewidth]{compiler.pdf}
    372375\end{center}
    373376
     
    404407Split normal simulation proof into three:
    405408\begin{enumerate}
    406 \item \blue{normal} steps become zero or more \blue{normal} steps
    407409\item \blue{call/return} steps become a \blue{call/return} step plus zero or
    408410  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
    410413\end{enumerate}
    411414
     
    470473
    471474\begin{center}
    472 \includegraphics[width=0.7\linewidth]{compiler.pdf}
     475\includegraphics[width=0.8\linewidth]{compiler.pdf}
    473476\end{center}
    474477
     
    492495\item Preserving trace structure provides correctness in more challenging
    493496  setting
    494 \item Formal proof still in progress
    495   \begin{itemize}
    496   \item key definitions, structured trace lifting, some simulations done
    497   \item increasing confidence in approach
    498   \end{itemize}
    499 \item[$\star$] Don't need huge changes to existing proofs
     497\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
    500503\end{itemize}
    501504
Note: See TracChangeset for help on using the changeset viewer.