Changeset 1741 for Deliverables


Ignore:
Timestamp:
Feb 24, 2012, 3:24:45 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1740 r1741  
    1515\usepackage{skull}
    1616\usepackage{stmaryrd}
     17\usepackage{wasysym}
    1718
    1819\lstdefinelanguage{matita-ocaml} {
     
    5354meeting we intend to move this transformation to the back-end}\\
    5455\> $\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)\\
    5658\> $\downarrow$ \> stack variable allocation and control structure
    5759 simplification\\
     
    6062\> $\downarrow$ \> transform to RTL graph\\
    6163\textsf{RTLabs}\\
    62 \> $\downarrow$ \> start of target specific back-end\\
    63 \>\quad \vdots
     64\> $\downarrow$ \> \\
     65\>\,\vdots
    6466\end{tabbing}
    6567\end{minipage}
     
    254256\begin{minipage}{.8\linewidth}
    255257\begin{tabbing}
    256 \quad \= $\downarrow$ \quad \= \kill
     258\quad \=\,\vdots\= \\
     259\> $\downarrow$ \>\\
     260\> $\downarrow$ \quad \= \kill
    257261\textsf{RTLabs}\\
    258262\> $\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) \\
     
    261265\> $\downarrow$ \> constant propagation$^{\mbox{\scriptsize \ref{lab:opt}}}$ (an endo-transformation) \\
    262266\> $\downarrow$ \> calling convention made explicit \\
    263 \> $\downarrow$ \> stack frame generation \\
     267\> $\downarrow$ \> layout of activation records \\
    264268\textsf{ERTL}\\
    265269\> $\downarrow$ \> register allocation and spilling\\
     
    272276\textsf{ASM}\\
    273277\> $\downarrow$ \> pseudoinstruction expansion\\
    274 \textsf{Machine code}\\
     278\textsf{MCS-51 machine code}\\
    275279\end{tabbing}
    276280\end{minipage}
     
    588592The ASM to MCS-51 machine code translation step, and the required statements of correctness, are found in an unpublished manuscript attached to this document.
    589593
     594\section{Estimated effort}
     595Based on the rough analysis performed so far we can now estimate the total
     596effort for the certification of the compiler. We obtain the estimation by
     597combining, for each pass: 1) the number of lines of code to be certified;
     5982) the ratio number of lines of proof on number of lines of code from
     599CompCert project~\cite{compcert} for the CompCert pass that is closer to
     600ours; 3) an estimation of the complexity of the pass according to the
     601analysis above.
     602
     603\begin{tabular}{lrll}
     604Pass origin & Code lines & CompCert ratio & Estimated effort \\
     605Clight & \\
     606Cminor & \\
     607RTLabs & 1252 & 1.17 \permil & 1.5 \\
     608RTL    &  469 & 2.90 \permil & 1.4 \\
     609ERTL   &  789 & 2.79 \permil & 2.2 \\
     610LTL    &      & \\
     611LIN    &  354 & 7.34 \permil & 2.6 \\
     612ASM    &      & \\
     613\end{tabular}
     614
    590615\end{document}
Note: See TracChangeset for help on using the changeset viewer.