Changeset 1745 for Deliverables/D1.2/CompilerProofOutline
 Timestamp:
 Feb 24, 2012, 4:07:44 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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