Changeset 1741 for Deliverables

Timestamp:

Feb 24, 2012, 3:24:45 PM (9 years ago)

Author:

sacerdot

Message:

...

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (7 diffs)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -15 +15 @@
 \usepackage{skull}
 \usepackage{stmaryrd}
+\usepackage{wasysym}
 
 \lstdefinelanguage{matita-ocaml} {
@@ -53 +54 @@
 meeting we intend to move this transformation to the back-end}\\
 \> $\downarrow$ \> cost labelling\\
-\> $\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)\\
+\> $\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)\\
+\> $\downarrow$ \> partial redundancy elimination$^{\mbox{\scriptsize \ref{lab:opt2}}}$ (an endo-transformation)\\
 \> $\downarrow$ \> stack variable allocation and control structure
  simplification\\
@@ -60 +62 @@
 \> $\downarrow$ \> transform to RTL graph\\
 \textsf{RTLabs}\\
-\> $\downarrow$ \> start of target specific back-end\\
-\>\quad \vdots
+\> $\downarrow$ \> \\
+\>\,\vdots
 \end{tabbing}
 \end{minipage}
@@ -254 +256 @@
 \begin{minipage}{.8\linewidth}
 \begin{tabbing}
-\quad \= $\downarrow$ \quad \= \kill
+\quad \=\,\vdots\= \\
+\> $\downarrow$ \>\\
+\> $\downarrow$ \quad \= \kill
 \textsf{RTLabs}\\
 \> $\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) \\
 \> $\downarrow$ \> calling convention made explicit \\
-\> $\downarrow$ \> stack frame generation \\
+\> $\downarrow$ \> layout of activation records \\
 \textsf{ERTL}\\
 \> $\downarrow$ \> register allocation and spilling\\
@@ -272 +276 @@
 \textsf{ASM}\\
 \> $\downarrow$ \> pseudoinstruction expansion\\
-\textsf{Machine code}\\
+\textsf{MCS-51 machine code}\\
 \end{tabbing}
 \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.
 
+\section{Estimated effort}
+Based on the rough analysis performed so far we can now estimate the total
+effort for the certification of the compiler. We obtain the estimation by
+combining, for each pass: 1) the number of lines of code to be certified;
+2) the ratio number of lines of proof on number of lines of code from
+CompCert project~\cite{compcert} for the CompCert pass that is closer to
+ours; 3) an estimation of the complexity of the pass according to the
+analysis above.
+
+\begin{tabular}{lrll}
+Pass origin & Code lines & CompCert ratio & Estimated effort \\
+Clight & \\
+Cminor & \\
+RTLabs & 1252 & 1.17 \permil & 1.5 \\
+RTL    &  469 & 2.90 \permil & 1.4 \\
+ERTL   &  789 & 2.79 \permil & 2.2 \\
+LTL    &      & \\
+LIN    &  354 & 7.34 \permil & 2.6 \\
+ASM    &      & \\
+\end{tabular}
+
 \end{document}