Changeset 1741 for Deliverables
- Timestamp:
- Feb 24, 2012, 3:24:45 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D1.2/CompilerProofOutline/outline.tex
r1740 r1741 15 15 \usepackage{skull} 16 16 \usepackage{stmaryrd} 17 \usepackage{wasysym} 17 18 18 19 \lstdefinelanguage{matita-ocaml} { … … 53 54 meeting we intend to move this transformation to the back-end}\\ 54 55 \> $\downarrow$ \> cost labelling\\ 55 \> $\downarrow$ \> loop optimizations\footnote{To be ported from the untrusted compiler and certified only in case of early completion of the certification of the other passes.} (an endo-transformation)\\ 56 \> $\downarrow$ \> loop optimizations\footnote{\label{lab:opt2}To be ported from the untrusted compiler and certified only in case of early completion of the certification of the other passes.} (an endo-transformation)\\ 57 \> $\downarrow$ \> partial redundancy elimination$^{\mbox{\scriptsize \ref{lab:opt2}}}$ (an endo-transformation)\\ 56 58 \> $\downarrow$ \> stack variable allocation and control structure 57 59 simplification\\ … … 60 62 \> $\downarrow$ \> transform to RTL graph\\ 61 63 \textsf{RTLabs}\\ 62 \> $\downarrow$ \> start of target specific back-end\\63 \>\ quad\vdots64 \> $\downarrow$ \> \\ 65 \>\,\vdots 64 66 \end{tabbing} 65 67 \end{minipage} … … 254 256 \begin{minipage}{.8\linewidth} 255 257 \begin{tabbing} 256 \quad \= $\downarrow$ \quad \= \kill 258 \quad \=\,\vdots\= \\ 259 \> $\downarrow$ \>\\ 260 \> $\downarrow$ \quad \= \kill 257 261 \textsf{RTLabs}\\ 258 262 \> $\downarrow$ \> copy propagation\footnote{\label{lab:opt}To be ported from the untrusted compiler and certified only in case of early completion of the certification of the other passes.} (an endo-transformation) \\ … … 261 265 \> $\downarrow$ \> constant propagation$^{\mbox{\scriptsize \ref{lab:opt}}}$ (an endo-transformation) \\ 262 266 \> $\downarrow$ \> calling convention made explicit \\ 263 \> $\downarrow$ \> stack frame generation\\267 \> $\downarrow$ \> layout of activation records \\ 264 268 \textsf{ERTL}\\ 265 269 \> $\downarrow$ \> register allocation and spilling\\ … … 272 276 \textsf{ASM}\\ 273 277 \> $\downarrow$ \> pseudoinstruction expansion\\ 274 \textsf{M achine code}\\278 \textsf{MCS-51 machine code}\\ 275 279 \end{tabbing} 276 280 \end{minipage} … … 588 592 The ASM to MCS-51 machine code translation step, and the required statements of correctness, are found in an unpublished manuscript attached to this document. 589 593 594 \section{Estimated effort} 595 Based on the rough analysis performed so far we can now estimate the total 596 effort for the certification of the compiler. We obtain the estimation by 597 combining, for each pass: 1) the number of lines of code to be certified; 598 2) the ratio number of lines of proof on number of lines of code from 599 CompCert project~\cite{compcert} for the CompCert pass that is closer to 600 ours; 3) an estimation of the complexity of the pass according to the 601 analysis above. 602 603 \begin{tabular}{lrll} 604 Pass origin & Code lines & CompCert ratio & Estimated effort \\ 605 Clight & \\ 606 Cminor & \\ 607 RTLabs & 1252 & 1.17 \permil & 1.5 \\ 608 RTL & 469 & 2.90 \permil & 1.4 \\ 609 ERTL & 789 & 2.79 \permil & 2.2 \\ 610 LTL & & \\ 611 LIN & 354 & 7.34 \permil & 2.6 \\ 612 ASM & & \\ 613 \end{tabular} 614 590 615 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.