Changeset 3260


Ignore:
Timestamp:
May 9, 2013, 11:04:39 AM (4 years ago)
Author:
campbell
Message:

Start adapting previous talk to front-end review.

Location:
Deliverables/Dissemination/front-end
Files:
13 added
9 copied

Legend:

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

    r3253 r3260  
    2626\begin{document}
    2727
    28 \title{A certified proof based on structured traces}
    29 \author{Brian Campbell}
     28\title{Front-end Correctness Proofs}
     29\author{Brian~Campbell, Ilias~Garnier, James~McKinna, Ian~Stark}
    3030\institute{LFCS, University of Edinburgh\\[1ex]
    3131\includegraphics[width=.3\linewidth]{cerco_logo.png}\\
     
    9090
    9191\frame{
     92\frametitle{Outline}
     93\tableofcontents
     94}
     95
     96\section{CerCo Compiler}
     97
     98\frame{
    9299\frametitle{CerCo compiler}
    93100
     
    115122verification.
    116123}
     124
     125\section{Overall correctness}
    117126
    118127\begin{frame}[fragile]
     
    202211
    203212\begin{frame}[fragile]
    204 \frametitle{Goal}
     213\frametitle{Overall correctness statement}
    205214
    206215\begin{center}
     
    347356\end{frame}
    348357
     358\section{Front-end correctness}
     359
     360\frame{
     361\frametitle{Front-end correctness}
     362
     363Recalling the toy compiler, need
     364\begin{enumerate}
     365\item Functional correctness
     366\item Cost labelling sound and precise
     367\item\label{it:return} To demonstrate return addresses are correct
     368\end{enumerate}
     369% TODO: stack space?  from obs, from fnl correctness
     370
     371\bigskip
     372For~\ref{it:return} we generalise notion of \emph{structured traces}
     373originally introduced for the correctness of timing analysis.
     374}
     375
    349376\begin{frame}[fragile]
    350377\frametitle{Structured traces}
     
    375402\end{center}
    376403
    377 \onslide<1>
    378 \green{Assembler} provides part of local cost analysis (CPP'12).
    379 
    380 \onslide<2-4>
     404%\onslide<1>
     405%\green{Assembler} provides part of local cost analysis (CPP'12).
     406
     407%\onslide<2-4>
    381408Switch at RTLabs:
    382409\begin{itemize}
     
    386413\end{itemize}
    387414
    388 \onslide<3>
    389 Changes \blue{syntactic} properties of labelling into \blue{semantic}
    390 properties.
    391 
    392 \onslide<4>
     415%\onslide<3>
     416%Changes \blue{syntactic} properties of labelling into \blue{semantic}
     417%properties.
     418
     419%\onslide<4>
    393420Reason for choice: first language with explicit \alert{addresses}, implicit
    394421\alert{call handling}.
    395422
    396423\end{frame}
     424
     425\frame{
     426\frametitle{Front-end correctness statement}
     427
     428We start with a \blue{measurable} subtrace of an execution, and the
     429\textbf{prefix} of that trace from initial state.
     430
     431\medskip
     432Need:
     433\begin{itemize}
     434\item Functional correctness for \textbf{prefix}
     435\item \red{Structured trace} corresponding to \blue{measurable}
     436  subtrace
     437\item Proof that no PC \red{repeats} in structured trace,\\ to ensure
     438  \blue{sound} labelling
     439\item \textbf{Observables} preserved
     440\item \textbf{Stack limit} observed
     441\end{itemize}
     442
     443}
     444
     445\section{Correctness proofs}
     446\subsection{Generic lifting result}
    397447
    398448\begin{frame}[fragile]
     
    424474\end{frame}
    425475
    426 \begin{frame}[fragile]
    427 \frametitle{Structured trace simulation}
    428 
    429 Lift \alert{local} simulations to \alert{structured trace} simulations
    430 similarly.
    431 
    432 \bigskip
    433 \pause
    434 \begin{itemize}
    435 \item
    436 Require local simulations for \alert{normal}, \alert{call} and \alert{return}
    437 steps
    438 \item allow traces to expand with extra \alert{normal} steps,
    439 \item allow us to collapse some \alert{normal} steps
    440   \begin{itemize}
    441   \item but not collapse \blue{labelled} steps
    442   % TODO: why?  avoid larger change in structure
    443   \item or change call structure
    444   \end{itemize}
    445 \end{itemize}
    446 
    447 \bigskip
    448 Sufficient to calculate structured trace in target.
    449 % TODO: pics
    450 
    451 \end{frame}
    452 
    453 \begin{frame}[fragile]
    454 \frametitle{Structured trace local simulation example}
    455 
    456 For function call steps:
    457 \begin{center}
    458 \includegraphics[width=0.7\linewidth]{strcall.pdf}
    459 \end{center}
    460 
    461 \begin{itemize}
    462 \item May add extra steps before and after
    463 \item Extra steps must not be call/return
    464 \item Must call the same function
    465 \item Cost label must stay at start of function
    466 \end{itemize}
    467 
    468 \end{frame}
    469 
     476%\begin{frame}[fragile]
     477%\frametitle{Structured trace simulation}
     478%
     479%Lift \alert{local} simulations to \alert{structured trace} simulations
     480%similarly.
     481%
     482%\bigskip
     483%\pause
     484%\begin{itemize}
     485%\item
     486%Require local simulations for \alert{normal}, \alert{call} and \alert{return}
     487%steps
     488%\item allow traces to expand with extra \alert{normal} steps,
     489%\item allow us to collapse some \alert{normal} steps
     490%  \begin{itemize}
     491%  \item but not collapse \blue{labelled} steps
     492%  % TODO: why?  avoid larger change in structure
     493%  \item or change call structure
     494%  \end{itemize}
     495%\end{itemize}
     496%
     497%\bigskip
     498%Sufficient to calculate structured trace in target.
     499%% TODO: pics
     500%
     501%\end{frame}
     502%
     503%\begin{frame}[fragile]
     504%\frametitle{Structured trace local simulation example}
     505%
     506%For function call steps:
     507%\begin{center}
     508%\includegraphics[width=0.7\linewidth]{strcall.pdf}
     509%\end{center}
     510%
     511%\begin{itemize}
     512%\item May add extra steps before and after
     513%\item Extra steps must not be call/return
     514%\item Must call the same function
     515%\item Cost label must stay at start of function
     516%\end{itemize}
     517%
     518%\end{frame}
     519
     520\subsection{Simulations for compiler passes}
     521
     522\frame{
     523\frametitle{TODO}
     524}
     525
     526\section{Checking cost labelling properties}
     527
     528\frame{
     529\frametitle{Checking cost labelling properties}
     530
     531Check cost labelling is \red{sound} and \blue{precise} at
     532\textbf{RTLabs}.
     533\begin{itemize}
     534\item Shortcut; similar to translation validation
     535\end{itemize}
     536
     537\medskip
     538At \textbf{RTLabs} properties become
     539\begin{description}
     540\item[\red{soundness}] bound on number of instructions in CFG until label\\
     541label at start of every function
     542\item[\blue{precision}]  label after every branch
     543\end{description}
     544
     545\medskip
     546Bound is the hard part; the rest is a simple syntactic check.
     547}
     548
     549\begin{frame}[fragile]
     550\frametitle{Bound on number of instructions until label}
     551
     552\begin{center}
     553\includegraphics<1>[width=.4\linewidth]{loop.pdf}
     554\includegraphics<2>[width=.4\linewidth]{loop1.pdf}
     555\includegraphics<3>[width=.4\linewidth]{loop2.pdf}
     556\includegraphics<4>[width=.4\linewidth]{loop3.pdf}
     557\includegraphics<5>[width=.4\linewidth]{loop4.pdf}
     558\includegraphics<6>[width=.4\linewidth]{loopx.pdf}
     559\end{center}
     560
     561\begin{itemize}
     562\item Pick an arbitrary node in the CFG
     563\item<2-> Follow successor instructions
     564\item<4-> If we find a \alert{cost label} all the traced nodes have a bound\dots
     565\item<5-> \dots so remove them and pick a new node, continue
     566\item<6-> But if we find an \alert{unlabelled loop} the labelling is unsound,
     567  report an error
     568\end{itemize}
     569
     570\end{frame}
     571
     572\frame{
     573\frametitle{Checking cost labelling properties}
     574
     575This compile-time check is
     576\begin{itemize}
     577\item[$-$] partial
     578\item[$-$] extra work in compilation
     579\item[$\mp$] not proving anything about compilation passes
     580\item[$+$] less proof burden
     581\end{itemize}
     582
     583\bigskip
     584Constructing the bound between \textbf{Cminor} and \textbf{RTLabs}
     585likely to be at least as expensive as this check.
     586
     587}
     588
     589\section{Whole compiler}
    470590
    471591\begin{frame}[fragile]
Note: See TracChangeset for help on using the changeset viewer.