# Changeset 1824 for Deliverables

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

More changes to presentation, following Claudio's comments

File:
1 edited

### Legend:

Unmodified
 r1822 \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} \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} \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}} \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} 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} \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 \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} \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 \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? 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} 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' \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 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} 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} 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} 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}