Changeset 1824 for Deliverables/D1.2

Timestamp:

Mar 12, 2012, 5:27:32 PM (8 years ago)

Author:

mulligan

Message:

More changes to presentation, following Claudio's comments

File:

• Deliverables/D1.2/Presentations/WP4-dominic.tex (modified) (16 diffs)

Deliverables/D1.2/Presentations/WP4-dominic.tex

@@ -78 +78 @@
 \item
 LIN is a linearised form of LTL, and is the exit point of the compiler's backend
+\item
+In contrast to frontend, backend is very different to CompCert's
 \end{itemize}
 \end{frame}
@@ -110 +112 @@
 \begin{itemize}
 \item
-Looking at O'Caml code, languages after RTLabs are similar
-\item
-Similar instructions, similar semantics, and so on
-\item
-Differences are slight
-\item
-Pseudoregisters used instead of hardware registers
-\item
-A few new unique instructions for each language
-\item
-In semantics: some notion of `successor' of an instruction, etc.
+Consecutive languages in backend must be similar
+\item
+Transformations between languages translate away some small specific set of features
+\item
+But looking at O'Caml code, not clear precisely what differences between languages are, as code is repeated
+\item
+Not clear if translation passes can commute, for instance
+\item
+CerCo passes are in a different order to CompCert (calling convention and register allocation done in different places)
+\item
+Instruction selection done early: changing subset of instructions used would require instructions to be duplicated everywhere in backend
 \end{itemize}
 \end{frame}
@@ -181 +183 @@
 \end{frame}
 
-\begin{frame}
-\frametitle{\texttt{Joint}: advantages}
-\begin{itemize}
-\item
-Why use \texttt{Joint}, as opposed to defining all languages individually?
-\item
-Reduces repeated code (fewer bugs, or places to change)
-\item
-Unify some proofs, making correctness proof easier
-\item
-Easier to add new intermediate languages as needed
-\item
-Easier to see relationship between consecutive languages at a glance
-\end{itemize}
-\end{frame}
-
 \begin{frame}[fragile]
 \frametitle{Instruction embedding in \texttt{Joint}}
@@ -211 +197 @@
 \item
 Instructions from the MCS-51 instruction set embedded in \texttt{Joint} syntax
+\end{itemize}
+\end{frame}
+
+\begin{frame}
+\frametitle{\texttt{Joint}: advantages}
+\begin{itemize}
+\item
+Why use \texttt{Joint}, as opposed to defining all languages individually?
+\item
+Reduces repeated code (fewer bugs, or places to change)
+\item
+Unify some proofs, making correctness proof easier
+\item
+Easier to add new intermediate languages as needed
+\item
+Easier to see relationship between consecutive languages at a glance
+\item
+Simplifies instruction selection (i.e. porting to a new platform, or expanding subset of instructions emitted)
+\item
+We can investigate which translation passes commute much more easily
 \end{itemize}
 \end{frame}
@@ -235 +241 @@
   regsT: Type[0];
   ...
-  acca_store_: acc_a_reg p → beval → regsT → res regsT;
-  acca_retrieve_: regsT → acc_a_reg p → res beval;
+  acca_store_: acc_a_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT;
+  acca_retrieve_: regsT $\rightarrow$ acc_a_reg p $\rightarrow$ res beval;
   ...
-  pair_reg_move_: regsT → pair_reg p → res regsT
+  pair_reg_move_: regsT $\rightarrow$ pair_reg p $\rightarrow$ res regsT
  }.
 \end{lstlisting}
@@ -347 +353 @@
 \begin{itemize}
 \item
+\texttt{Joint} clearly separates fetching from program execution
+\item
+We can vary how one works whilst fixing the other
+\item
+Linearisation is moving from fetching from a graph-based language to fetching from a list-based program representation
+\item
 The order of transformations in O'Caml prototype is fixed
 \item
@@ -366 +378 @@
 \item
 Many transformations and optimisations can work fine on a linearised form
+\item
+The only place in the backend that requires a graph-based language is in the ERTL pass, where we do a dataflow analysis
 \end{itemize}
 \end{frame}
@@ -373 +387 @@
 \begin{itemize}
 \item
-We had six months of `free time', time not allotted in the Contract to working on any explicit deliverable
+We had six months of time which is not reported on in any deliverable
 \item
 We invested this time working on:
 \begin{itemize}
 \item
+The global proof sketch
+\item
+The setup of `proof infrastructure', common definitions, lemmas, invariants etc. required for main body of proof
+\item
 The proof of correctness for the assembler
 \item
@@ -407 +425 @@
 \begin{itemize}
 \item
-`Jump expansion' is our name for the following (standard) problem
+`Jump expansion' is our name for the standard `branch displacement' problem
 \item
 Given a pseudojump to a label $l$, how best can this be expanded into an assembly instruction \texttt{SJMP}, \texttt{AJMP} or \texttt{LJMP} to a concrete address?
@@ -431 +449 @@
 Further, we know that the assembler only fails to assemble a program if a good policy does not exist (a side-effect of using dependent types)
 \item
-A bad policy is a function that expands a given pseudojump into a concrete jump instruction that is `too small' for the distance to be jumped
+A bad policy is a function that expands a given pseudojump into a concrete jump instruction that is `too small' for the distance to be jumped, or makes the program consume too much memory
 \end{itemize}
 \end{frame}
@@ -445 +463 @@
 Termination of the procedure is proved, as well as a safety property, stating that jumps are not expanded into jumps that are too long
 \item
-Optimality is not proved
+His strategy is not optimal (though the computed solution is optimal for the strategy employed)
 \item
 Boender's work is the first formal treatment of the `jump expansion problem'
@@ -455 +473 @@
 \begin{itemize}
 \item
-Assuming the existence of a good jump expansion property, we completed about 50\% of the correctness proof for the assembler
-\item
-Boender's work constitutes a large missing piece (modulo a few missing lemmas), but holes still remain in the main proof
-\item
-We abandoned this work to start on other tasks
+Assuming the existence of a good jump expansion property, we completed about 75\% of the correctness proof for the assembler
+\item
+Boender's work has just been completed (modulo a few missing lemmas)
+\item
+We abandoned the main assembler proof to start work on other tasks (and wait for Boender to finish)
 \item
 However, we intend to return to the proof, and publishing an account of the work (possibly) as a journal paper
@@ -617 +635 @@
 This proof is surprisingly tricky to complete (about 3 man months of work so far)
 \item
-Is now about 75\% complete
+Is now about 95\% complete
 \end{itemize}
 \end{frame}
@@ -631 +649 @@
 It is unclear whether they will be
 \item
-Just a generalization of what is already there
-\item
-Supposed to make formalization easier
+Just a generalisation of what is already there
+\item
+Supposed to make formalisation easier
+\item
+Further, we want to ensure that the untrusted compiler is as correct as possible, for experiments in e.g. Frama-C
+\item
+Porting a large change to the untrusted compiler would jeopardise these experiments
 \end{itemize}
 \end{frame}
@@ -649 +671 @@
 These include major speed-ups of e.g. printing large goals, bug fixes, the porting of CerCo code to standard library, and more options for passing to tactics
 \end{itemize}
+\end{frame}
+
+\begin{frame}
+\frametitle{The next period}
+% XXX: todo
 \end{frame}
 
@@ -662 +689 @@
 Refactored many of the backend intermediate languages into a common, parametric `joint' language, that is later specialised
 \item
-Spotted opportunities for commuting backend translation passes
-\item
-Used six months of `free time' to define structured traces and start the proof of correctness for the assembler
+Spotted opportunities for possibly commuting backend translation passes
+\item
+Used six months to define structured traces and start the proof of correctness for the assembler
+\item
+Distinguished our proof from CompCert's by heavy use of dependent types throughout whole compiler
 \end{itemize}
 \end{frame}