Changeset 3264


Ignore:
Timestamp:
May 10, 2013, 2:50:19 PM (4 years ago)
Author:
campbell
Message:

Draft a bit of missing content for front-end slides.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/Dissemination/front-end/front-end.tex

    r3260 r3264  
    395395\end{frame}
    396396
    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 labelling
    412 \item to \blue{structured trace} where they are embedded
    413 \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}, implicit
    421 \alert{call handling}.
    422 
    423 \end{frame}
    424 
    425397\frame{
    426398\frametitle{Front-end correctness statement}
     
    442414
    443415}
     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>
     428Switch at RTLabs:
     429\begin{itemize}
     430\item from \red{measurable} subtrace of \alert{sound} and \alert{precise}
     431labelling
     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>
     440Reason for choice: first language with explicit \alert{addresses}, implicit
     441\alert{call handling}.
     442
     443\end{frame}
    444444
    445445\section{Correctness proofs}
     
    520520\subsection{Simulations for compiler passes}
    521521
    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
     530Two stages provide the annotated version of input:
     531
     532\bigskip
     533Switch 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
     544Cost 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}
     558Cast 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
    525597
    526598\section{Checking cost labelling properties}
     
    585657likely to be at least as expensive as this check.
    586658
     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}
    587677}
    588678
Note: See TracChangeset for help on using the changeset viewer.