# Changeset 1762 for Deliverables/D1.2/CompilerProofOutline

Ignore:
Timestamp:
Feb 27, 2012, 1:51:15 PM (8 years ago)
Message:

Changes and fixes.

File:
1 edited

### Legend:

Unmodified
 r1761 \subsection{The LTL to LIN translation} \label{subsect.ltl.lin.translation} Ad detailed elsewhere in the reports, due to the parameterized representation of the back-end languages, the pass described here is actually much more generic than the translation from LTL to LIN. It consists in a linearization pass that maps any graph-based back-end language to its corresponding linear form, preserving its semantics. In the rest of the section, however, we will keep the names LTL and LIN for the two partial instantiations of the parameterized language. 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: \end{enumerate} 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. Note, because the LTL to LIN transformation is the first time the code of a function is linearised in the back-end, we must discover a notion of well formed function code' suitable for linearised forms. In particular, we see the notion of well formedness (yet to be formally defined) resting on the following conditions: \begin{enumerate} \item For every jump to a label in a linearised program, the target label exists at some point in the program, For every jump to a label in a linearised function code, the target label exists at some point in the function code, \item Each label is unique, appearing only once in the program, Each label is unique, appearing only once in the function code, \item The final instruction of a program must be a return. The final instruction of a function code must be a return or an unconditional jump. \end{enumerate} The final condition above is potentially a little opaque, so we explain further. 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). 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. 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. 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). \subsection{The LIN to ASM and ASM to MCS-51 machine code translations} sketched in the previous section. \section{Conclusions} The overall exercise, whose details have been only minimally reported here, has been very useful. It has allowed to spot in an early moment some criticities of the proof that have required major changes in the proof plan. It has also shown that the last passes of the compilation (e.g. assembly) and cost prediction on the object code are much more involved than more high level passes. The final estimation for the effort is surely affected by a low degree of confidence. It is however sufficient to conclude that the effort required is in line with the man power that was scheduled for the second half of the second period and for the third period. Compared to the number of men months declared in Annex I of the contract, we will need more men months. However, both at UNIBO and UEDIN there have been major differences in hiring with respect to the Annex. Therefore both sites have now an higher number of men months available, with the trade-off of a lower level of maturity of the people employed. The reviewers suggested that we use this estimation to compare two possible scenarios: a) proceed as planned, porting all the CompCert proofs to Matita or b) port D3.1 and D4.1 to Coq and re-use the CompCert proofs. We remark here again that the back-end of the two compilers, from the memory model on, are sensibly different: we are not re-proving correctness of the same piece of code. Moreover, the proof techniques are different for the front-end too. Switching to the CompCert formalization would imply the abandon of the untrusted compiler, the abandon of the experiment with a different proof technique, the abandon of the quest for an open source proof, and the abandon of the co-development of the formalization and the Matita proof assistant. In the Commitment Letter~\cite{letter} delivered to the Officer in May we clarified our personal perspective on the project goals and objectives. We do not re-describe here the point of view presented in the letter that we can condense in `we value diversity''. Clearly, if the execise would have suggested the infeasability in terms of effort of concluding the formalization or getting close to that, we would have abandoned our path and embraced the reviewer's suggestion. However, we have been comforted in the analysis we did in autumn and further progress done during the winter does not show yet any major delay with respect to the proof schedule. We are thus planning to continue the certification according to the more detailed proof plan that came out from the exercise reported in this manuscript. \end{document}