Changeset 1745 for Deliverables

Timestamp:

Feb 24, 2012, 4:07:44 PM (8 years ago)

Author:

sacerdot

Message:

Conclusions.

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (1 diff)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -669 +669 @@
 \end{tabular}
 
+We provide now some additional informations on the methodology used in the
+computation. The passes in Cerco and CompCert front-end closely match each
+other. However, there is no clear correspondence between the two back-ends.
+For instance, we enforce the calling convention immediately after instruction
+selection, whereas in CompCert this is performed in a later phase. Or we
+linearize the code at the very end, whereas CompCert performs linearization
+as soon as possible. Therefore, the first part of the exercise has consisted
+in shuffling and partitioning the CompCert code in order to assign to each
+CerCo pass the CompCert code that performs the same transformation.
+
+After this preliminary step, using the data given in~\cite{compcert} (which
+are relative to an early version of CompCert) we computed the ratio between
+men months and lines of code in CompCert for each CerCo pass. This is shown
+in the third column of Table~\ref{wildguess}. For those CerCo passes that
+have no correspondence in CompCert (like the optimizing assembler) or where
+we have insufficient data, we have used the average of the ratios computed
+above.
+
+The first column of the table shows the number of lines of code for each
+pass in CerCo. The third column is obtained multiplying the first with the
+CompCert ratio. It provides an estimate of the effort required (in men months)
+if the complexity of the proofs for CerCo and Compcert would be the same.
+
+The two proof styles, however, are on purpose completely different. Where
+CompCert uses non executable semantics, describing the various semantics with
+inductive types, we have preferred executable semantics. Therefore, CompCert
+proofs by induction and inversion become proof by functional inversion,
+performed using the Russel methodology (now called Program in Coq, but whose
+behaviour differs from Matita's one). Moreover, CompCert code is written using
+only types that belong to the Hindley-Milner fragment, whereas we have
+heavily exploited dependent types all over the code. The dependent type
+discipline offers many advantages from the point of view of clarity of the
+invariants involved and early detection of errors and it naturally combines
+well with the Russel approach which is based on dependent types. However, it
+is also well known to introduce technical problems all over the code, like
+the need to explicitly prove type equalities to be able to manipulate
+expressions in certain ways. In many situations, the difficulties encountered
+with manipulating dependent types are better addressed by improving the Matita
+system, according to the formalization driven system development. For this
+reason, and assuming a pessimistic point of view on our performance, the
+fourth columns presents the final estimation of the effort required, that also
+takes in account the complexity of the proof suggested by the informal proofs
+sketched in the previous section.
+
 \end{document}