Changeset 1758


Ignore:
Timestamp:
Feb 24, 2012, 7:01:29 PM (8 years ago)
Author:
campbell
Message:

Minor improvements to front-end; add an overall statement.

File:
1 edited

Legend:

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

    r1757 r1758  
    5757In this document we provide a very high-level, pen-and-paper
    5858sketch of what we view as the best path to completing the correctness proof
    59 for the compiler. In particular, for every translation between two intermediate languages, in both the front- and back-ends, we identify the key translation steps, and identify some invariants that we view as being important for the correctness proof. We also briefly describe the parts of the proof that have already
     59for the compiler. In particular, for every translation between two intermediate languages, in both the front- and back-ends, we identify the key translation steps, and identify some invariants that we view as being important for the correctness proof.  We sketch the overall correctness results, and also briefly describe the parts of the proof that have already
    6060been completed at the end of the First Period.
    6161
     
    9898\begin{enumerate}
    9999\item invariants closely tied to the syntax and transformations using
    100   dependent types,
    101 \item a forward simulation proof, and
    102 \item syntactic proofs about the cost labelling.
     100  dependent types (such as the presence of variable names in environments),
     101\item a forward simulation proof relating each small-step of the
     102  source to zero or more steps of the target, and
     103\item proofs about syntactic properties of the cost labelling.
    103104\end{enumerate}
    104 The first will support both functional correctness and allow us to show
    105 the totality of some of the compiler stages (that is, those stages of
    106 the compiler cannot fail).  The second provides the main functional
    107 correctness result, and the last will be crucial for applying
    108 correctness results about the costings from the back-end.
     105The first will support both functional correctness and allow us to
     106show the totality of some of the compiler stages (that is, those
     107stages of the compiler cannot fail).  The second provides the main
     108functional correctness result, including the preservation of cost
     109labels in the traces, and the last will be crucial for applying
     110correctness results about the costings from the back-end by showing
     111that they appear in enough places so that we can assign all of the
     112execution costs to them.
    109113
    110114We will also prove that a suitably labelled RTLabs trace can be turned
     
    776780T O D O ! ! !
    777781
     782\section{Overall results}
     783
     784Functional correctness of the compiled code can be shown by composing
     785the simulations to show that the target behaviour matches the
     786behaviour of the source program, if the source program does not `go
     787wrong'.  More precisely, we show that there is a forward simulation
     788between the source trace and a (flattened structured) trace of the
     789output, and conclude equivalence because the target's semantics are
     790in the form of an executable function, and hence
     791deterministic.
     792
     793Combining this with the correctness of the assignment of costs to cost
     794labels at the ASM level for a structured trace, we can show that the
     795cost of executing any compiled function (including the main function)
     796is equal to the sum of all the values for cost labels encountered in
     797the \emph{source code's} trace of the function.
     798
    778799\section{Estimated effort}
    779800Based on the rough analysis performed so far we can estimate the total
Note: See TracChangeset for help on using the changeset viewer.