Changeset 1824 for Deliverables/D1.2
- Timestamp:
- Mar 12, 2012, 5:27:32 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D1.2/Presentations/WP4-dominic.tex
r1822 r1824 78 78 \item 79 79 LIN is a linearised form of LTL, and is the exit point of the compiler's backend 80 \item 81 In contrast to frontend, backend is very different to CompCert's 80 82 \end{itemize} 81 83 \end{frame} … … 110 112 \begin{itemize} 111 113 \item 112 Looking at O'Caml code, languages after RTLabs are similar113 \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.114 Consecutive languages in backend must be similar 115 \item 116 Transformations between languages translate away some small specific set of features 117 \item 118 But looking at O'Caml code, not clear precisely what differences between languages are, as code is repeated 119 \item 120 Not clear if translation passes can commute, for instance 121 \item 122 CerCo passes are in a different order to CompCert (calling convention and register allocation done in different places) 123 \item 124 Instruction selection done early: changing subset of instructions used would require instructions to be duplicated everywhere in backend 123 125 \end{itemize} 124 126 \end{frame} … … 181 183 \end{frame} 182 184 183 \begin{frame}184 \frametitle{\texttt{Joint}: advantages}185 \begin{itemize}186 \item187 Why use \texttt{Joint}, as opposed to defining all languages individually?188 \item189 Reduces repeated code (fewer bugs, or places to change)190 \item191 Unify some proofs, making correctness proof easier192 \item193 Easier to add new intermediate languages as needed194 \item195 Easier to see relationship between consecutive languages at a glance196 \end{itemize}197 \end{frame}198 199 185 \begin{frame}[fragile] 200 186 \frametitle{Instruction embedding in \texttt{Joint}} … … 211 197 \item 212 198 Instructions 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 206 Why use \texttt{Joint}, as opposed to defining all languages individually? 207 \item 208 Reduces repeated code (fewer bugs, or places to change) 209 \item 210 Unify some proofs, making correctness proof easier 211 \item 212 Easier to add new intermediate languages as needed 213 \item 214 Easier to see relationship between consecutive languages at a glance 215 \item 216 Simplifies instruction selection (i.e. porting to a new platform, or expanding subset of instructions emitted) 217 \item 218 We can investigate which translation passes commute much more easily 213 219 \end{itemize} 214 220 \end{frame} … … 235 241 regsT: Type[0]; 236 242 ... 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; 239 245 ... 240 pair_reg_move_: regsT → pair_reg p →res regsT246 pair_reg_move_: regsT $\rightarrow$ pair_reg p $\rightarrow$ res regsT 241 247 }. 242 248 \end{lstlisting} … … 347 353 \begin{itemize} 348 354 \item 355 \texttt{Joint} clearly separates fetching from program execution 356 \item 357 We can vary how one works whilst fixing the other 358 \item 359 Linearisation is moving from fetching from a graph-based language to fetching from a list-based program representation 360 \item 349 361 The order of transformations in O'Caml prototype is fixed 350 362 \item … … 366 378 \item 367 379 Many transformations and optimisations can work fine on a linearised form 380 \item 381 The only place in the backend that requires a graph-based language is in the ERTL pass, where we do a dataflow analysis 368 382 \end{itemize} 369 383 \end{frame} … … 373 387 \begin{itemize} 374 388 \item 375 We had six months of `free time', time not allotted in the Contract to working on any explicitdeliverable389 We had six months of time which is not reported on in any deliverable 376 390 \item 377 391 We invested this time working on: 378 392 \begin{itemize} 379 393 \item 394 The global proof sketch 395 \item 396 The setup of `proof infrastructure', common definitions, lemmas, invariants etc. required for main body of proof 397 \item 380 398 The proof of correctness for the assembler 381 399 \item … … 407 425 \begin{itemize} 408 426 \item 409 `Jump expansion' is our name for the following (standard)problem427 `Jump expansion' is our name for the standard `branch displacement' problem 410 428 \item 411 429 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) 432 450 \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 451 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 434 452 \end{itemize} 435 453 \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 446 464 \item 447 Optimality is not proved 465 His strategy is not optimal (though the computed solution is optimal for the strategy employed) 448 466 \item 449 467 Boender's work is the first formal treatment of the `jump expansion problem' … … 455 473 \begin{itemize} 456 474 \item 457 Assuming the existence of a good jump expansion property, we completed about 50\% of the correctness proof for the assembler458 \item 459 Boender's work constitutes a large missing piece (modulo a few missing lemmas), but holes still remain in the main proof460 \item 461 We abandoned th is work to start on other tasks475 Assuming the existence of a good jump expansion property, we completed about 75\% of the correctness proof for the assembler 476 \item 477 Boender's work has just been completed (modulo a few missing lemmas) 478 \item 479 We abandoned the main assembler proof to start work on other tasks (and wait for Boender to finish) 462 480 \item 463 481 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) 618 636 \item 619 Is now about 75\% complete637 Is now about 95\% complete 620 638 \end{itemize} 621 639 \end{frame} … … 631 649 It is unclear whether they will be 632 650 \item 633 Just a generalization of what is already there 634 \item 635 Supposed to make formalization easier 651 Just a generalisation of what is already there 652 \item 653 Supposed to make formalisation easier 654 \item 655 Further, we want to ensure that the untrusted compiler is as correct as possible, for experiments in e.g. Frama-C 656 \item 657 Porting a large change to the untrusted compiler would jeopardise these experiments 636 658 \end{itemize} 637 659 \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 650 672 \end{itemize} 673 \end{frame} 674 675 \begin{frame} 676 \frametitle{The next period} 677 % XXX: todo 651 678 \end{frame} 652 679 … … 662 689 Refactored many of the backend intermediate languages into a common, parametric `joint' language, that is later specialised 663 690 \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 691 Spotted opportunities for possibly commuting backend translation passes 692 \item 693 Used six months to define structured traces and start the proof of correctness for the assembler 694 \item 695 Distinguished our proof from CompCert's by heavy use of dependent types throughout whole compiler 667 696 \end{itemize} 668 697 \end{frame}
Note: See TracChangeset
for help on using the changeset viewer.