Changeset 3264 for Deliverables/Dissemination

Timestamp:

May 10, 2013, 2:50:19 PM (8 years ago)

Author:

campbell

Message:

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

File:

• Deliverables/Dissemination/front-end/front-end.tex (modified) (4 diffs)

Deliverables/Dissemination/front-end/front-end.tex

@@ -395 +395 @@
 \end{frame}
 
-\begin{frame}[fragile]
-\frametitle{Structure in the compiler proof}
-
-\begin{center}
-\includegraphics[width=0.8\linewidth]{compiler.pdf}
-\end{center}
-
-%\onslide<1>
-%\green{Assembler} provides part of local cost analysis (CPP'12).
-
-%\onslide<2-4>
-Switch at RTLabs:
-\begin{itemize}
-\item from \red{measurable} subtrace of \alert{sound} and \alert{precise}
-labelling
-\item to \blue{structured trace} where they are embedded
-\end{itemize}
-
-%\onslide<3>
-%Changes \blue{syntactic} properties of labelling into \blue{semantic}
-%properties.
-
-%\onslide<4>
-Reason for choice: first language with explicit \alert{addresses}, implicit
-\alert{call handling}.
-
-\end{frame}
-
 \frame{
 \frametitle{Front-end correctness statement}
@@ -442 +414 @@
 
 }
+
+\begin{frame}[fragile]
+\frametitle{Structure in the compiler proof}
+
+\begin{center}
+\includegraphics[width=0.8\linewidth]{compiler.pdf}
+\end{center}
+
+%\onslide<1>
+%\green{Assembler} provides part of local cost analysis (CPP'12).
+
+%\onslide<2-4>
+Switch at RTLabs:
+\begin{itemize}
+\item from \red{measurable} subtrace of \alert{sound} and \alert{precise}
+labelling
+\item to \blue{structured trace} where they are embedded
+\end{itemize}
+
+%\onslide<3>
+%Changes \blue{syntactic} properties of labelling into \blue{semantic}
+%properties.
+
+%\onslide<4>
+Reason for choice: first language with explicit \alert{addresses}, implicit
+\alert{call handling}.
+
+\end{frame}
 
 \section{Correctness proofs}
@@ -520 +520 @@
 \subsection{Simulations for compiler passes}
 
-\frame{
-\frametitle{TODO}
-}
+%\frame{
+%\frametitle{TODO: at least two slides on simulations}
+%}
+
+% TODO: perhaps much earlier for the pre-measurable bits?
+\frame{
+\frametitle{Simulation between input and annotated code}
+
+Two stages provide the annotated version of input:
+
+\bigskip
+Switch removal
+\begin{itemize}
+\item \lstinline[language=C]'switch' statement control flow too subtle
+  for simple labelling
+\item Replaces with \lstinline[language=C]'if ... then ... else' tree
+\item Tricky part of proof memory extension for extra variable
+\item Partial proof: validate approach, but not relevant to
+  intensional properties
+\end{itemize}
+
+\bigskip
+Cost labelling
+\begin{itemize}
+\item For simulation don't care \emph{which} labels are added
+\item Just have to skip over extra cost label expressions and
+  statements
+\item Complete simulation proof, simple
+\end{itemize}
+
+% TODO: consider whether to mention full simulation
+% termination-preserving proof?
+}
+
+\frame{
+\frametitle{Front-end simulation results}
+Cast simplification
+\begin{itemize}
+\item Simplify expressions for 8-bit target
+\item Only expressions change --- statements are in lock-step
+\item Difficult part: we allow ill-typed \textbf{Clight} at this stage
+\item Simulation proofs complete
+\end{itemize}
+
+\textbf{Clight} to \textbf{Cminor}
+\begin{itemize}
+\item Stack allocation and control flow transformation
+\item Similar to \textbf{CompCert}, but produces \lstinline'goto'
+  instead of \lstinline'loop'
+\item Expressions complete
+\item Prove a selection of statements, in particular \lstinline'while'
+\item Tricky: Large proof terms for invariant embedded in
+  \textbf{Cminor} programs using dependent types;\\
+  generalise them away, but difficult under binders
+%TODO explain clearly
+\end{itemize}
+}
+\frame{
+\frametitle{Front-end simulation results}
+\textbf{Cminor} to \textbf{RTLabs}
+\begin{itemize}
+\item Construction of control-flow graph
+\item Axiomatized simulations
+\item But do have invariants:
+  \begin{itemize}
+  \item Statement well-typed with respect to pseudo-register
+    environment
+  \item CFG complete
+  \item Entry and exit nodes complete, unique
+  \end{itemize}
+\item Translation function is \emph{total} as a result
+\end{itemize}
+}
+
+% TODO: sloganize: proved more about unusual bits
 
 \section{Checking cost labelling properties}
@@ -585 +657 @@
 likely to be at least as expensive as this check.
 
+}
+
+\section{Construction of structured traces}
+
+\frame{
+\frametitle{Construction of structured traces}
+\begin{center}
+\includegraphics{strtraces.pdf}
+\end{center}
+\begin{enumerate}
+\item Extend sound and precise labelling to semantic states
+\item Prove they are preserved by steps of semantics
+\item Prove \textbf{RTLabs} semantics preserve the stack
+\item Use \alert{termination} proof from \alert{measurable} subtrace
+  to create structure
+\item Proof obligations for cost labelling are discharged by semantic
+  results above
+\end{enumerate}
 }