Changeset 1762 for Deliverables/D1.2/CompilerProofOutline

Timestamp:

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

Author:

sacerdot

Message:

Changes and fixes.

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (4 diffs)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -674 +674 @@
 \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:
@@ -730 +737 @@
 \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}
 
@@ -745 +754 @@
 
 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}
@@ -967 +974 @@
 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}