Changeset 1762 for Deliverables/D1.2/CompilerProofOutline
- Timestamp:
- Feb 27, 2012, 1:51:15 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D1.2/CompilerProofOutline/outline.tex
r1761 r1762 674 674 \subsection{The LTL to LIN translation} 675 675 \label{subsect.ltl.lin.translation} 676 Ad detailed elsewhere in the reports, due to the parameterized representation of 677 the back-end languages, the pass described here is actually much more generic 678 than the translation from LTL to LIN. It consists in a linearization pass 679 that maps any graph-based back-end language to its corresponding linear form, 680 preserving its semantics. In the rest of the section, however, we will keep 681 the names LTL and LIN for the two partial instantiations of the parameterized 682 language. 676 683 677 684 We require a map, $\sigma$, from LTL statuses, where program counters are represented as labels in a graph data structure, to LIN statuses, where program counters are natural numbers: … … 730 737 \end{enumerate} 731 738 732 Note, because the LTL to LIN transformation is the first time the program is linearised, we must discover a notion of `well formed program' suitable for linearised forms. 739 Note, because the LTL to LIN transformation is the first time the code of 740 a function is linearised in the back-end, we must discover a notion of `well formed function code' suitable for linearised forms. 733 741 In particular, we see the notion of well formedness (yet to be formally defined) resting on the following conditions: 734 742 735 743 \begin{enumerate} 736 744 \item 737 For every jump to a label in a linearised program, the target label exists at some point in the program,745 For every jump to a label in a linearised function code, the target label exists at some point in the function code, 738 746 \item 739 Each label is unique, appearing only once in the program,747 Each label is unique, appearing only once in the function code, 740 748 \item 741 The final instruction of a program must be a return. 749 The final instruction of a function code must be a return or an unconditional 750 jump. 742 751 \end{enumerate} 743 752 … … 745 754 746 755 The final condition above is potentially a little opaque, so we explain further. 747 First, the only instructions that can reasonably appear in final position at the end of a program are returns or backward jumps, as any other instruction would cause execution to `fall out' of the end of the program (for example, when a function invoked with \texttt{CALL} returns, it returns to the next instruction past the \texttt{CALL} that invoked it). 748 However, in LIN, though each function's graph has been linearised, the entire program is not yet fully linearised into a list of instructions, but rather, a list of `functions', each consisting of a linearised body along with other data. 749 Each well-formed function must end with a call to \texttt{RET}, and therefore the only correct instruction that can terminate a LIN program is a \texttt{RET} instruction. 756 The only instructions that can reasonably appear in final position at the end of a function code are returns or backward jumps, as any other instruction would cause execution to `fall out' of the end of the program (for example, when a function invoked with \texttt{CALL} returns, it returns to the next instruction past the \texttt{CALL} that invoked it). 750 757 751 758 \subsection{The LIN to ASM and ASM to MCS-51 machine code translations} … … 967 974 sketched in the previous section. 968 975 976 \section{Conclusions} 977 The overall exercise, whose details have been only minimally reported here, 978 has been very useful. It has allowed to spot in an early moment some criticities 979 of the proof that have required major changes in the proof plan. It has also 980 shown that the last passes of the compilation (e.g. assembly) and cost 981 prediction on the object code are much more involved than more high level 982 passes. 983 984 The final estimation for the effort is surely affected by a low degree of 985 confidence. It is however sufficient to conclude that the effort required 986 is in line with the man power that was scheduled for the second half of the 987 second period and for the third period. Compared to the number of men months 988 declared in Annex I of the contract, we will need more men months. However, 989 both at UNIBO and UEDIN there have been major differences in hiring with 990 respect to the Annex. Therefore both sites have now an higher number of men 991 months available, with the trade-off of a lower level of maturity of the 992 people employed. 993 994 The reviewers suggested that we use this estimation to compare two possible 995 scenarios: a) proceed as planned, porting all the CompCert proofs to Matita 996 or b) port D3.1 and D4.1 to Coq and re-use the CompCert proofs. 997 We remark here again that the back-end of the two compilers, from the 998 memory model on, are sensibly different: we are not re-proving correctness 999 of the same piece of code. Moreover, the proof techniques are different for 1000 the front-end too. Switching to the CompCert formalization would imply 1001 the abandon of the untrusted compiler, the abandon of the experiment with 1002 a different proof technique, the abandon of the quest for an open source 1003 proof, and the abandon of the co-development of the formalization and the 1004 Matita proof assistant. In the Commitment Letter~\cite{letter} delivered 1005 to the Officer in May we clarified our personal perspective on the project 1006 goals and objectives. We do not re-describe here the point of view presented 1007 in the letter that we can condense in ``we value diversity''. 1008 1009 Clearly, if the execise would have suggested the infeasability in terms of 1010 effort of concluding the formalization or getting close to that, we would have 1011 abandoned our path and embraced the reviewer's suggestion. However, we 1012 have been comforted in the analysis we did in autumn and further progress done 1013 during the winter does not show yet any major delay with respect to the 1014 proof schedule. We are thus planning to continue the certification according 1015 to the more detailed proof plan that came out from the exercise reported in 1016 this manuscript. 1017 969 1018 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.