Changeset 1824


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

More changes to presentation, following Claudio's comments

File:
1 edited

Legend:

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

    r1822 r1824  
    7878\item
    7979LIN is a linearised form of LTL, and is the exit point of the compiler's backend
     80\item
     81In contrast to frontend, backend is very different to CompCert's
    8082\end{itemize}
    8183\end{frame}
     
    110112\begin{itemize}
    111113\item
    112 Looking at O'Caml code, languages after RTLabs are similar
    113 \item
    114 Similar instructions, similar semantics, and so on
    115 \item
    116 Differences are slight
    117 \item
    118 Pseudoregisters used instead of hardware registers
    119 \item
    120 A few new unique instructions for each language
    121 \item
    122 In semantics: some notion of `successor' of an instruction, etc.
     114Consecutive languages in backend must be similar
     115\item
     116Transformations between languages translate away some small specific set of features
     117\item
     118But looking at O'Caml code, not clear precisely what differences between languages are, as code is repeated
     119\item
     120Not clear if translation passes can commute, for instance
     121\item
     122CerCo passes are in a different order to CompCert (calling convention and register allocation done in different places)
     123\item
     124Instruction selection done early: changing subset of instructions used would require instructions to be duplicated everywhere in backend
    123125\end{itemize}
    124126\end{frame}
     
    181183\end{frame}
    182184
    183 \begin{frame}
    184 \frametitle{\texttt{Joint}: advantages}
    185 \begin{itemize}
    186 \item
    187 Why use \texttt{Joint}, as opposed to defining all languages individually?
    188 \item
    189 Reduces repeated code (fewer bugs, or places to change)
    190 \item
    191 Unify some proofs, making correctness proof easier
    192 \item
    193 Easier to add new intermediate languages as needed
    194 \item
    195 Easier to see relationship between consecutive languages at a glance
    196 \end{itemize}
    197 \end{frame}
    198 
    199185\begin{frame}[fragile]
    200186\frametitle{Instruction embedding in \texttt{Joint}}
     
    211197\item
    212198Instructions from the MCS-51 instruction set embedded in \texttt{Joint} syntax
     199\end{itemize}
     200\end{frame}
     201
     202\begin{frame}
     203\frametitle{\texttt{Joint}: advantages}
     204\begin{itemize}
     205\item
     206Why use \texttt{Joint}, as opposed to defining all languages individually?
     207\item
     208Reduces repeated code (fewer bugs, or places to change)
     209\item
     210Unify some proofs, making correctness proof easier
     211\item
     212Easier to add new intermediate languages as needed
     213\item
     214Easier to see relationship between consecutive languages at a glance
     215\item
     216Simplifies instruction selection (i.e. porting to a new platform, or expanding subset of instructions emitted)
     217\item
     218We can investigate which translation passes commute much more easily
    213219\end{itemize}
    214220\end{frame}
     
    235241  regsT: Type[0];
    236242  ...
    237   acca_store_: acc_a_reg p → beval → regsT → res regsT;
    238   acca_retrieve_: regsT → acc_a_reg p → res beval;
     243  acca_store_: acc_a_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT;
     244  acca_retrieve_: regsT $\rightarrow$ acc_a_reg p $\rightarrow$ res beval;
    239245  ...
    240   pair_reg_move_: regsT → pair_reg p → res regsT
     246  pair_reg_move_: regsT $\rightarrow$ pair_reg p $\rightarrow$ res regsT
    241247 }.
    242248\end{lstlisting}
     
    347353\begin{itemize}
    348354\item
     355\texttt{Joint} clearly separates fetching from program execution
     356\item
     357We can vary how one works whilst fixing the other
     358\item
     359Linearisation is moving from fetching from a graph-based language to fetching from a list-based program representation
     360\item
    349361The order of transformations in O'Caml prototype is fixed
    350362\item
     
    366378\item
    367379Many transformations and optimisations can work fine on a linearised form
     380\item
     381The only place in the backend that requires a graph-based language is in the ERTL pass, where we do a dataflow analysis
    368382\end{itemize}
    369383\end{frame}
     
    373387\begin{itemize}
    374388\item
    375 We had six months of `free time', time not allotted in the Contract to working on any explicit deliverable
     389We had six months of time which is not reported on in any deliverable
    376390\item
    377391We invested this time working on:
    378392\begin{itemize}
    379393\item
     394The global proof sketch
     395\item
     396The setup of `proof infrastructure', common definitions, lemmas, invariants etc. required for main body of proof
     397\item
    380398The proof of correctness for the assembler
    381399\item
     
    407425\begin{itemize}
    408426\item
    409 `Jump expansion' is our name for the following (standard) problem
     427`Jump expansion' is our name for the standard `branch displacement' problem
    410428\item
    411429Given 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?
     
    431449Further, 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)
    432450\item
    433 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
     451A 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
    434452\end{itemize}
    435453\end{frame}
     
    445463Termination of the procedure is proved, as well as a safety property, stating that jumps are not expanded into jumps that are too long
    446464\item
    447 Optimality is not proved
     465His strategy is not optimal (though the computed solution is optimal for the strategy employed)
    448466\item
    449467Boender's work is the first formal treatment of the `jump expansion problem'
     
    455473\begin{itemize}
    456474\item
    457 Assuming the existence of a good jump expansion property, we completed about 50\% of the correctness proof for the assembler
    458 \item
    459 Boender's work constitutes a large missing piece (modulo a few missing lemmas), but holes still remain in the main proof
    460 \item
    461 We abandoned this work to start on other tasks
     475Assuming the existence of a good jump expansion property, we completed about 75\% of the correctness proof for the assembler
     476\item
     477Boender's work has just been completed (modulo a few missing lemmas)
     478\item
     479We abandoned the main assembler proof to start work on other tasks (and wait for Boender to finish)
    462480\item
    463481However, we intend to return to the proof, and publishing an account of the work (possibly) as a journal paper
     
    617635This proof is surprisingly tricky to complete (about 3 man months of work so far)
    618636\item
    619 Is now about 75\% complete
     637Is now about 95\% complete
    620638\end{itemize}
    621639\end{frame}
     
    631649It is unclear whether they will be
    632650\item
    633 Just a generalization of what is already there
    634 \item
    635 Supposed to make formalization easier
     651Just a generalisation of what is already there
     652\item
     653Supposed to make formalisation easier
     654\item
     655Further, we want to ensure that the untrusted compiler is as correct as possible, for experiments in e.g. Frama-C
     656\item
     657Porting a large change to the untrusted compiler would jeopardise these experiments
    636658\end{itemize}
    637659\end{frame}
     
    649671These 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
    650672\end{itemize}
     673\end{frame}
     674
     675\begin{frame}
     676\frametitle{The next period}
     677% XXX: todo
    651678\end{frame}
    652679
     
    662689Refactored many of the backend intermediate languages into a common, parametric `joint' language, that is later specialised
    663690\item
    664 Spotted opportunities for commuting backend translation passes
    665 \item
    666 Used six months of `free time' to define structured traces and start the proof of correctness for the assembler
     691Spotted opportunities for possibly commuting backend translation passes
     692\item
     693Used six months to define structured traces and start the proof of correctness for the assembler
     694\item
     695Distinguished our proof from CompCert's by heavy use of dependent types throughout whole compiler
    667696\end{itemize}
    668697\end{frame}
Note: See TracChangeset for help on using the changeset viewer.