Changeset 3260

Timestamp:

May 9, 2013, 11:04:39 AM (7 years ago)

Author:

campbell

Message:

Start adapting previous talk to front-end review.

Location:

Deliverables/Dissemination/front-end

Files:

• . (added)
• cerco_logo.png (copied) (copied from Deliverables/Dissemination/proof-structured-traces/cerco_logo.png)
• compiler-plain.pdf (copied) (copied from Deliverables/D3.4/Report/compiler-plain.pdf)
• compiler.pdf (copied) (copied from Deliverables/D3.4/Report/compiler.pdf)
• compiler.svg (copied) (copied from Deliverables/D3.4/Report/compiler.svg)
• front-end.tex (copied) (copied from Deliverables/Dissemination/proof-structured-traces/proof-structured-traces.tex) (8 diffs)
• loop.pdf (added)
• loop.svg (added)
• loop1.pdf (added)
• loop1.svg (added)
• loop2.pdf (added)
• loop2.svg (added)
• loop3.pdf (added)
• loop3.svg (added)
• loop4.pdf (added)
• loop4.svg (added)
• loopx.pdf (added)
• loopx.svg (added)
• meassim.pdf (copied) (copied from Deliverables/D3.4/Report/meassim.pdf)
• meassim.svg (copied) (copied from Deliverables/D3.4/Report/meassim.svg)
• strtraces.pdf (copied) (copied from Deliverables/D3.4/Report/strtraces.pdf)
• strtraces.svg (copied) (copied from Deliverables/D3.4/Report/strtraces.svg)

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

@@ -26 +26 @@
 \begin{document}
 
-\title{A certified proof based on structured traces}
-\author{Brian Campbell}
+\title{Front-end Correctness Proofs}
+\author{Brian~Campbell, Ilias~Garnier, James~McKinna, Ian~Stark}
 \institute{LFCS, University of Edinburgh\\[1ex]
 \includegraphics[width=.3\linewidth]{cerco_logo.png}\\
@@ -90 +90 @@
 
 \frame{
+\frametitle{Outline}
+\tableofcontents
+}
+
+\section{CerCo Compiler}
+
+\frame{
 \frametitle{CerCo compiler}
 
@@ -115 +122 @@
 verification.
 }
+
+\section{Overall correctness}
 
 \begin{frame}[fragile]
@@ -202 +211 @@
 
 \begin{frame}[fragile]
-\frametitle{Goal}
+\frametitle{Overall correctness statement}
 
 \begin{center}
@@ -347 +356 @@
 \end{frame}
 
+\section{Front-end correctness}
+
+\frame{
+\frametitle{Front-end correctness}
+
+Recalling the toy compiler, need
+\begin{enumerate}
+\item Functional correctness
+\item Cost labelling sound and precise
+\item\label{it:return} To demonstrate return addresses are correct
+\end{enumerate}
+% TODO: stack space?  from obs, from fnl correctness
+
+\bigskip
+For~\ref{it:return} we generalise notion of \emph{structured traces}
+originally introduced for the correctness of timing analysis.
+}
+
 \begin{frame}[fragile]
 \frametitle{Structured traces}
@@ -375 +402 @@
 \end{center}
 
-\onslide<1>
-\green{Assembler} provides part of local cost analysis (CPP'12).
-
-\onslide<2-4>
+%\onslide<1>
+%\green{Assembler} provides part of local cost analysis (CPP'12).
+
+%\onslide<2-4>
 Switch at RTLabs:
 \begin{itemize}
@@ -386 +413 @@
 \end{itemize}
 
-\onslide<3>
-Changes \blue{syntactic} properties of labelling into \blue{semantic}
-properties.
-
-\onslide<4>
+%\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}
+
+We start with a \blue{measurable} subtrace of an execution, and the
+\textbf{prefix} of that trace from initial state.
+
+\medskip
+Need:
+\begin{itemize}
+\item Functional correctness for \textbf{prefix}
+\item \red{Structured trace} corresponding to \blue{measurable}
+  subtrace
+\item Proof that no PC \red{repeats} in structured trace,\\ to ensure
+  \blue{sound} labelling
+\item \textbf{Observables} preserved
+\item \textbf{Stack limit} observed
+\end{itemize}
+
+}
+
+\section{Correctness proofs}
+\subsection{Generic lifting result}
 
 \begin{frame}[fragile]
@@ -424 +474 @@
 \end{frame}
 
-\begin{frame}[fragile]
-\frametitle{Structured trace simulation}
-
-Lift \alert{local} simulations to \alert{structured trace} simulations
-similarly.
-
-\bigskip
-\pause
-\begin{itemize}
-\item
-Require local simulations for \alert{normal}, \alert{call} and \alert{return}
-steps
-\item allow traces to expand with extra \alert{normal} steps,
-\item allow us to collapse some \alert{normal} steps
-  \begin{itemize}
-  \item but not collapse \blue{labelled} steps
-  % TODO: why?  avoid larger change in structure
-  \item or change call structure
-  \end{itemize}
-\end{itemize}
-
-\bigskip
-Sufficient to calculate structured trace in target.
-% TODO: pics
-
-\end{frame}
-
-\begin{frame}[fragile]
-\frametitle{Structured trace local simulation example}
-
-For function call steps:
-\begin{center}
-\includegraphics[width=0.7\linewidth]{strcall.pdf}
-\end{center}
-
-\begin{itemize}
-\item May add extra steps before and after
-\item Extra steps must not be call/return
-\item Must call the same function
-\item Cost label must stay at start of function
-\end{itemize}
-
-\end{frame}
-
+%\begin{frame}[fragile]
+%\frametitle{Structured trace simulation}
+%
+%Lift \alert{local} simulations to \alert{structured trace} simulations
+%similarly.
+%
+%\bigskip
+%\pause
+%\begin{itemize}
+%\item
+%Require local simulations for \alert{normal}, \alert{call} and \alert{return}
+%steps
+%\item allow traces to expand with extra \alert{normal} steps,
+%\item allow us to collapse some \alert{normal} steps
+%  \begin{itemize}
+%  \item but not collapse \blue{labelled} steps
+%  % TODO: why?  avoid larger change in structure
+%  \item or change call structure
+%  \end{itemize}
+%\end{itemize}
+%
+%\bigskip
+%Sufficient to calculate structured trace in target.
+%% TODO: pics
+%
+%\end{frame}
+%
+%\begin{frame}[fragile]
+%\frametitle{Structured trace local simulation example}
+%
+%For function call steps:
+%\begin{center}
+%\includegraphics[width=0.7\linewidth]{strcall.pdf}
+%\end{center}
+%
+%\begin{itemize}
+%\item May add extra steps before and after
+%\item Extra steps must not be call/return
+%\item Must call the same function
+%\item Cost label must stay at start of function
+%\end{itemize}
+%
+%\end{frame}
+
+\subsection{Simulations for compiler passes}
+
+\frame{
+\frametitle{TODO}
+}
+
+\section{Checking cost labelling properties}
+
+\frame{
+\frametitle{Checking cost labelling properties}
+
+Check cost labelling is \red{sound} and \blue{precise} at
+\textbf{RTLabs}.
+\begin{itemize}
+\item Shortcut; similar to translation validation
+\end{itemize}
+
+\medskip
+At \textbf{RTLabs} properties become
+\begin{description}
+\item[\red{soundness}] bound on number of instructions in CFG until label\\
+label at start of every function
+\item[\blue{precision}]  label after every branch
+\end{description}
+
+\medskip
+Bound is the hard part; the rest is a simple syntactic check.
+}
+
+\begin{frame}[fragile]
+\frametitle{Bound on number of instructions until label}
+
+\begin{center}
+\includegraphics<1>[width=.4\linewidth]{loop.pdf}
+\includegraphics<2>[width=.4\linewidth]{loop1.pdf}
+\includegraphics<3>[width=.4\linewidth]{loop2.pdf}
+\includegraphics<4>[width=.4\linewidth]{loop3.pdf}
+\includegraphics<5>[width=.4\linewidth]{loop4.pdf}
+\includegraphics<6>[width=.4\linewidth]{loopx.pdf}
+\end{center}
+
+\begin{itemize}
+\item Pick an arbitrary node in the CFG
+\item<2-> Follow successor instructions
+\item<4-> If we find a \alert{cost label} all the traced nodes have a bound\dots
+\item<5-> \dots so remove them and pick a new node, continue
+\item<6-> But if we find an \alert{unlabelled loop} the labelling is unsound,
+  report an error
+\end{itemize}
+
+\end{frame}
+
+\frame{
+\frametitle{Checking cost labelling properties}
+
+This compile-time check is
+\begin{itemize}
+\item[$-$] partial
+\item[$-$] extra work in compilation
+\item[$\mp$] not proving anything about compilation passes
+\item[$+$] less proof burden
+\end{itemize}
+
+\bigskip
+Constructing the bound between \textbf{Cminor} and \textbf{RTLabs}
+likely to be at least as expensive as this check.
+
+}
+
+\section{Whole compiler}
 
 \begin{frame}[fragile]