Changeset 1745


Ignore:
Timestamp:
Feb 24, 2012, 4:07:44 PM (8 years ago)
Author:
sacerdot
Message:

Conclusions.

File:
1 edited

Legend:

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

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