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

Changes and fixes.

File:
1 edited

Legend:

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

    r1761 r1762  
    674674\subsection{The LTL to LIN translation}
    675675\label{subsect.ltl.lin.translation}
     676Ad detailed elsewhere in the reports, due to the parameterized representation of
     677the back-end languages, the pass described here is actually much more generic
     678than the translation from LTL to LIN. It consists in a linearization pass
     679that maps any graph-based back-end language to its corresponding linear form,
     680preserving its semantics. In the rest of the section, however, we will keep
     681the names LTL and LIN for the two partial instantiations of the parameterized
     682language.
    676683
    677684We 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:
     
    730737\end{enumerate}
    731738
    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.
     739Note, because the LTL to LIN transformation is the first time the code of
     740a function is linearised in the back-end, we must discover a notion of `well formed function code' suitable for linearised forms.
    733741In particular, we see the notion of well formedness (yet to be formally defined) resting on the following conditions:
    734742
    735743\begin{enumerate}
    736744\item
    737 For every jump to a label in a linearised program, the target label exists at some point in the program,
     745For every jump to a label in a linearised function code, the target label exists at some point in the function code,
    738746\item
    739 Each label is unique, appearing only once in the program,
     747Each label is unique, appearing only once in the function code,
    740748\item
    741 The final instruction of a program must be a return.
     749The final instruction of a function code must be a return or an unconditional
     750jump.
    742751\end{enumerate}
    743752
     
    745754
    746755The 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.
     756The 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).
    750757
    751758\subsection{The LIN to ASM and ASM to MCS-51 machine code translations}
     
    967974sketched in the previous section.
    968975
     976\section{Conclusions}
     977The overall exercise, whose details have been only minimally reported here,
     978has been very useful. It has allowed to spot in an early moment some criticities
     979of the proof that have required major changes in the proof plan. It has also
     980shown that the last passes of the compilation (e.g. assembly) and cost
     981prediction on the object code are much more involved than more high level
     982passes.
     983
     984The final estimation for the effort is surely affected by a low degree of
     985confidence. It is however sufficient to conclude that the effort required
     986is in line with the man power that was scheduled for the second half of the
     987second period and for the third period. Compared to the number of men months
     988declared in Annex I of the contract, we will need more men months. However,
     989both at UNIBO and UEDIN there have been major differences in hiring with
     990respect to the Annex. Therefore both sites have now an higher number of men
     991months available, with the trade-off of a lower level of maturity of the
     992people employed.
     993
     994The reviewers suggested that we use this estimation to compare two possible
     995scenarios: a) proceed as planned, porting all the CompCert proofs to Matita
     996or b) port D3.1 and D4.1 to Coq and re-use the CompCert proofs.
     997We remark here again that the back-end of the two compilers, from the
     998memory model on, are sensibly different: we are not re-proving correctness
     999of the same piece of code. Moreover, the proof techniques are different for
     1000the front-end too. Switching to the CompCert formalization would imply
     1001the abandon of the untrusted compiler, the abandon of the experiment with
     1002a different proof technique, the abandon of the quest for an open source
     1003proof, and the abandon of the co-development of the formalization and the
     1004Matita proof assistant. In the Commitment Letter~\cite{letter} delivered
     1005to the Officer in May we clarified our personal perspective on the project
     1006goals and objectives. We do not re-describe here the point of view presented
     1007in the letter that we can condense in ``we value diversity''.
     1008
     1009Clearly, if the execise would have suggested the infeasability in terms of
     1010effort of concluding the formalization or getting close to that, we would have
     1011abandoned our path and embraced the reviewer's suggestion. However, we
     1012have been comforted in the analysis we did in autumn and further progress done
     1013during the winter does not show yet any major delay with respect to the
     1014proof schedule. We are thus planning to continue the certification according
     1015to the more detailed proof plan that came out from the exercise reported in
     1016this manuscript.
     1017
    9691018\end{document}
Note: See TracChangeset for help on using the changeset viewer.