# Changeset 3267 for Deliverables/Dissemination/front-end/front-end.tex

Ignore:
Timestamp:
May 13, 2013, 11:26:11 AM (7 years ago)
Message:

Improve a few awkward parts of front-end slides.

File:
1 edited

### Legend:

Unmodified
 r3266 \frametitle{Introduction} D3.4 is the front-end correctness proofs: D3.4 consists of the front-end correctness proofs: \begin{description} \item[Primary focus:] novel \red{intensional} properties: \blue{cost bound correctness} \item[Secondary:] usual \red{extensional} result: \blue{functional correctness} \end{description} Functional correctness for similar compilers already studied in Leroy et al.'s \blue{CompCert}. \begin{itemize} \vskip-2ex \begin{itemize} \item Now have \blue{stack} costs as well as \blue{time}\\ --- yields stronger overall correctness result \item Informed by earlier formal experiment with a toy compiler. \end{itemize} \medskip \begin{description} \item[Secondary focus:] usual \red{extensional} result: \blue{functional correctness} \end{description} \vskip-2ex \begin{itemize} \item Similar functional correctness already studied in \blue{CompCert} \item Axiomatize similar results \end{itemize} \medskip Now have \blue{stack} costs as well as \blue{time} \begin{itemize} \item yields stronger overall correctness result \end{itemize} \medskip \alert{Extract} compiler code from development for practical execution. \medskip Informed by earlier formal experiment with a toy compiler. \item \red{Intensional} proofs form a layer on top \end{itemize} } \begin{center} \includegraphics[width=0.8\linewidth]{compiler-plain.pdf} \end{center} \begin{itemize} \item Reuse unverified CompCert parser \includegraphics[width=0.6\linewidth]{compiler-plain.pdf} \end{center} \begin{itemize} \item Reuse unverified CompCert \alert{parser} %\item Transform away troublesome constructs %  \begin{itemize} %  \end{itemize} \item Intermediate language for most passes \item Executable semantics for each \item \alert{Executable semantics} for each \item \alert{Extract} OCaml compiler code from development \item Outputs \begin{itemize} \item 8051 machine code \item Clight code instrumented with costs in 8051 clock cycles and bytes of stack space \item \alert{8051 machine code} \item Clight code instrumented with costs in 8051 \alert{clock cycles} and \alert{bytes of stack space} \end{itemize} \end{itemize} \frametitle{Overall correctness statement} $\text{max predicted stack usage} \leq \text{limit}$ implies \begin{itemize} \item successful execution, with \end{itemize} \begin{center} \fbox{$$\text{machine time} = \Sigma_{l\in\text{source trace}} \text{costmap}(l)$$} \end{center} \pause \end{frame} \begin{frame}[fragile] \frametitle{Overall correctness statement} \begin{center} \fbox{$$\text{machine time} = \Sigma_{l\in\text{source trace}} \text{costmap}(l)$$} \end{center} %\pause \begin{center} & \begin{uncoverenv}<2-3> \begin{uncoverenv}<1-2> \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, emph={[2]_cost3},emphstyle={[2]\color{blue}}] & \begin{uncoverenv}<3-5> \begin{uncoverenv}<2-4> \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, emph={[2]_cost3},emphstyle={[2]\color{blue}}] \begin{overprint} \onslide<2> \begin{itemize} \item Use labels and end of function as measurement points \item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f' \end{itemize} \onslide<3-4> \begin{itemize} \item Use labels and end of function as measurement points \item All costs are considered local to the function \item Actual position of unobservable computation is unimportant \end{itemize} \onslide<5> \begin{itemize} \item Use labels and end of function as measurement points \item[$\star$] Call suitable subtraces \alert{measurable} \item[$\star$] Core part is a proof of \alert{termination} \end{itemize} \onslide<1-2> \begin{itemize} \item Which parts can we measure execution costs of? \item Actual position of unobservable computation is unimportant \item Want to get \alert{exact} execution time \end{itemize} \onslide<3> \begin{itemize} \item Use labels and end of function as measurement points \item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f' \item All costs are considered local to the function \end{itemize} \onslide<4> \begin{itemize} \item Use labels and end of function as measurement points \item[$\star$] Call suitable subtraces \alert{measurable} \item[$\star$] Core part is a proof that the trace \alert{terminates} at return \end{itemize} % \onslide<1> % \begin{itemize} % \item Use labels and end of function as measurement points % \item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f' % \end{itemize} % \onslide<2-3> % \begin{itemize} % \item Use labels and end of function as measurement points % \item All costs are considered local to the function % \item Actual position of unobservable computation is unimportant % \end{itemize} % \onslide<4> % \begin{itemize} % \item Use labels and end of function as measurement points % \item[$\star$] Call suitable subtraces \alert{measurable} % \item[$\star$] Core part is a proof of \alert{termination} % \end{itemize} \end{overprint} \frametitle{Front-end correctness statement} Given a \blue{measurable} subtrace of a \textbf{Clight} execution, including Given a \red{measurable} subtrace of a \textbf{Clight} execution, including the \textbf{prefix} of that trace from initial state, \begin{itemize} \item a new \textbf{prefix} \item a \red{structured trace} corresponding to \blue{measurable} \item a \blue{structured trace} corresponding to \red{measurable} subtrace \item the no \red{repeating} addresses property \item the no \blue{repeating} addresses property \item proof that the same \textbf{stack limit} is observed \end{itemize} which the back-end requires, and \begin{itemize} \item the observables for the \textbf{prefix} and \red{structured \item the observables for the \textbf{prefix} and \blue{structured trace} are the same as their \textbf{Clight} counterparts \end{itemize} 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 \item Tricky part of proof: memory extension for extra variable \item Partial proof: enough to validate approach;\\ \quad --- this stage not relevant to intensional properties \end{itemize} \item But do have invariants: \begin{itemize} \item Statement well-typed with respect to pseudo-register \item[$\bullet$] Statements well-typed with respect to pseudo-register environment \item CFG complete \item Entry and exit nodes complete, unique \item[$\bullet$] CFG complete \item[$\bullet$] Entry and exit nodes present, unique \end{itemize} \item Translation function is \emph{total} as a result \begin{itemize} \item Clock' difference in Clight is sum of cost labels \item Observables, including trace of labels, is preserved to ASM \item Labelling at bottom level is sound and precise \item Sum of labels at ASM is equal to difference in real clock \item Instantiate measurable subtracing lifting with simulations \item Show existence of \textbf{RTLabs} structured trace \item Apply back-end to show \textbf{RTLabs} costs correct \item Use equivalence of observables to show \textbf{Clight} costs correct % \item Clock' difference in Clight is sum of cost labels % \item Observables, including trace of labels, is preserved to ASM % \item Labelling at bottom level is sound and precise % \item Sum of labels at ASM is equal to difference in real clock \end{itemize}