# Changeset 1829

Ignore:
Timestamp:
Mar 13, 2012, 11:46:25 AM (8 years ago)
Message:

changes to my presentation, just one point left to consider

File:
1 edited

### Legend:

Unmodified
 r1824 \end{frame} \begin{frame}[fragile] \frametitle{Who pays? I} \begin{lstlisting} int main(int argc, char** argv) { label1: ... some_function(); label2: ... } \end{lstlisting} \begin{itemize} \item Question: where do we put cost labels to capture execution costs? \item Proof obligations complicated by panoply of labels \item Doesn't work well with \texttt{g(h() + 2 + f())} \item To prove accuracy we need to show \texttt{some\_function()} terminates! \item \texttt{some\_function()} may not return correctly \end{itemize} \end{frame} \begin{frame} \frametitle{Who pays? II} \begin{itemize} \item Solution: omit \texttt{label2} and just keep \texttt{label1} \item We pay for everything up front' when entering a function \item No need to prove \texttt{some\_function()} terminates \item But now execution of functions in CerCo takes a particular form \item Functions begin with a label, call other functions that begin with a label, eventually return, but \emph{return} to the correct place \item Recursive structure' \end{itemize} \end{frame} \begin{frame} \frametitle{Structured traces I} We introduced a notion of structured traces' \item These are intended to statically capture the execution trace of a program These are intended to statically capture the (good) execution traces of a program \item That is, functions return to where they ought \item Come in two variants: inductive and coinductive A well formed program must have labels appearing at certain spots \item Similarly, the final instruction executed when executing a function must be a \texttt{RET} instruction Similarly, the final instruction executed when executing a function must be a \texttt{RET} \item Execution must then continue in body of calling function, at correct place \item These invariants, and others, are crystalised in the specific syntactic form of a structured trace \begin{frame} \frametitle{The next period} % XXX: todo UNIBO has following pool of remaining manpower (postdocs): \begin{center} \begin{tabular}{ll} Person & Man months remaining \\ \hline Boender & 14 months \\ Mulligan & 6 months \\ Tranquilli & 10 months \\ \end{tabular} \end{center} \begin{itemize} \item Boender finishing assembler correctness proof \item Mulligan proofs of correctness for 1 intermediate language \item Tranquilli proofs of correctness for 2 intermediate languages \item Sacerdoti Coen floating' \item Believe we have enough manpower to complete backend \end{itemize} \end{frame}