Changeset 1829


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

changes to my presentation, just one point left to consider

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/Presentations/WP4-dominic.tex

    r1824 r1829  
    483483\end{frame}
    484484
     485\begin{frame}[fragile]
     486\frametitle{Who pays? I}
     487\begin{lstlisting}
     488int main(int argc, char** argv) {
     489  label1:
     490    ...
     491    some_function();
     492  label2:
     493    ...
     494}
     495\end{lstlisting}
     496\begin{itemize}
     497\item
     498Question: where do we put cost labels to capture execution costs?
     499\item
     500Proof obligations complicated by panoply of labels
     501\item
     502Doesn't work well with \texttt{g(h() + 2 + f())}
     503\item
     504To prove accuracy we need to show \texttt{some\_function()} terminates!
     505\item
     506\texttt{some\_function()} may not return correctly
     507\end{itemize}
     508\end{frame}
     509
     510\begin{frame}
     511\frametitle{Who pays? II}
     512\begin{itemize}
     513\item
     514Solution: omit \texttt{label2} and just keep \texttt{label1}
     515\item
     516We pay for everything `up front' when entering a function
     517\item
     518No need to prove \texttt{some\_function()} terminates
     519\item
     520But now execution of functions in CerCo takes a particular form
     521\item
     522Functions begin with a label, call other functions that begin with a label, eventually return, but \emph{return} to the correct place
     523\item
     524`Recursive structure'
     525\end{itemize}
     526\end{frame}
     527
    485528\begin{frame}
    486529\frametitle{Structured traces I}
     
    489532We introduced a notion of `structured traces'
    490533\item
    491 These are intended to statically capture the execution trace of a program
     534These are intended to statically capture the (good) execution traces of a program
     535\item
     536That is, functions return to where they ought
    492537\item
    493538Come in two variants: inductive and coinductive
     
    521566A well formed program must have labels appearing at certain spots
    522567\item
    523 Similarly, the final instruction executed when executing a function must be a \texttt{RET} instruction
     568Similarly, the final instruction executed when executing a function must be a \texttt{RET}
     569\item
     570Execution must then continue in body of calling function, at correct place
    524571\item
    525572These invariants, and others, are crystalised in the specific syntactic form of a structured trace
     
    675722\begin{frame}
    676723\frametitle{The next period}
    677 % XXX: todo
     724UNIBO has following pool of remaining manpower (postdocs):
     725\begin{center}
     726\begin{tabular}{ll}
     727Person & Man months remaining \\
     728\hline
     729Boender & 14 months \\
     730Mulligan & 6 months \\
     731Tranquilli & 10 months \\
     732\end{tabular}
     733\end{center}
     734\begin{itemize}
     735\item
     736Boender finishing assembler correctness proof
     737\item
     738Mulligan proofs of correctness for 1 intermediate language
     739\item
     740Tranquilli proofs of correctness for 2 intermediate languages
     741\item
     742Sacerdoti Coen `floating'
     743\item
     744Believe we have enough manpower to complete backend
     745\end{itemize}
    678746\end{frame}
    679747
Note: See TracChangeset for help on using the changeset viewer.