Ignore:
Timestamp:
Feb 24, 2012, 4:09:02 PM (8 years ago)
Author:
campbell
Message:

Revisions to front-end text.

File:
1 edited

Legend:

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

    r1745 r1746  
    8080\item syntactic proofs about the cost labelling.
    8181\end{enumerate}
    82 The first will support both function correctness and allow us to show
    83 the totality of some of the compiler stages (that is, these stages of
     82The first will support both functional correctness and allow us to show
     83the totality of some of the compiler stages (that is, those stages of
    8484the compiler cannot fail).  The second provides the main functional
    8585correctness result, and the last will be crucial for applying
     
    8888We will also prove that a suitably labelled RTLabs trace can be turned
    8989into a \emph{structured trace} which splits the execution trace into
    90 cost-label-to-cost-label chunks with nested function calls.  This
     90cost-label to cost-label chunks with nested function calls.  This
    9191structure was identified during work on the correctness of the
    9292back-end cost analysis as retaining important information about the
     
    9494the compiler.
    9595
    96 \subsection{Clight Cast removal}
    97 
    98 This removes some casts inserted by the parser to make arithmetic
    99 promotion explicit when they are superfluous (such as
    100 \lstinline[language=C]'c = (short)((int)a + (int)b);').
    101 
    102 The transformation only affects Clight expressions, recursively
    103 detecting casts that can be safely eliminated.  The semantics provides
    104 a big-step definition for expression, so we should be able to show a
    105 lock-step forward simulation using a lemma showing that cast
    106 elimination does not change the evaluation of expressions.  This lemma
    107 will follow from a structural induction on the source expression.  We
    108 have already proved a few of the underlying arithmetic results
    109 necessary to validate the approach.
     96\subsection{Clight cast removal}
     97
     98This transformation removes some casts inserted by the parser to make
     99arithmetic promotion explicit but which are superfluous (such as
     100\lstinline[language=C]'c = (short)((int)a + (int)b);' where
     101\lstinline'a' and \lstinline'b' are \lstinline[language=C]'short').
     102This is necessary for producing good code for our target architecture.
     103
     104It only affects Clight expressions, recursively detecting casts that
     105can be safely eliminated.  The semantics provides a big-step
     106definition for expression, so we should be able to show a lock-step
     107forward simulation between otherwise identical states using a lemma
     108showing that cast elimination does not change the evaluation of
     109expressions.  This lemma will follow from a structural induction on
     110the source expression.  We have already proved a few of the underlying
     111arithmetic results necessary to validate the approach.
    110112
    111113\subsection{Clight cost labelling}
     
    113115This adds cost labels before and after selected statements and
    114116expressions, and the execution traces ought to be equivalent modulo
    115 cost labels.  Hence it requires a simple forward simulation with a
    116 limited amount of stuttering whereever a new cost label is introduced.
    117 A bound can be given for the amount of stuttering allowed can be given
     117the new cost labels.  Hence it requires a simple forward simulation
     118with a limited amount of stuttering whereever a new cost label is
     119introduced.  A bound can be given for the amount of stuttering allowed
    118120based on the statement or continuation to be evaluated next.
    119121
    120122We also intend to show three syntactic properties about the cost
    121123labelling:
    122 \begin{itemize}
     124\begin{enumerate}
    123125\item every function starts with a cost label,
    124 \item every branching instruction is followed by a label (note that
     126\item every branching instruction is followed by a cost label (note that
    125127  exiting a loop is treated as a branch), and
    126128\item the head of every loop (and any \lstinline'goto' destination) is
    127129  a cost label.
    128 \end{itemize}
     130\end{enumerate}
    129131These can be shown by structural induction on the source term.
    130132
     
    143145\item that variables used in the generated code are present in the
    144146  resulting environment (either by checking their presence in the
    145   source environment, or from a list of freshly temporary variables);
     147  source environment, or from a list of freshly generated temporary variables);
    146148  and
    147149\item that all \lstinline[language=C]'goto' labels are present (by
     
    152154The simulation will be similar to the relevant stages of CompCert
    153155(Clight to Csharpminor and Csharpminor to Cminor --- in the event that
    154 the direct proof is unwieldy we could introduce a corresponding
    155 intermediate language).  During early experimentation with porting
    156 CompCert definitions to the Matita proof assistant we found little
    157 difficulty reproving the results for the memory model, so we plan to
    158 port the memory injection properties and use them to relate Clight
    159 in-memory variables with either a local variable valuation or a stack
    160 slot, depending on how it was classified.
     156the direct proof is unwieldy we could introduce an intermediate
     157language corresponding to Csharpminor).  During early experimentation
     158with porting CompCert definitions to the Matita proof assistant we
     159found little difficulty reproving the results for the memory model, so
     160we plan to port the memory injection properties and use them to relate
     161Clight in-memory variables with either the value of the local variable or a
     162stack slot, depending on how it was classified.
    161163
    162164This should be sufficient to show the equivalence of (big-step)
     
    190192
    191193We already enforce several invariants with dependent types: some type
    192 safety is enforced mostly using the type information from Cminor; and
     194safety, mostly shown using the type information from Cminor; and
    193195that the graph is closed (by showing that each successor was recently
    194196added, or corresponds to a \lstinline[language=C]'goto' label which
     
    199201later stages using the same method as Cminor.
    200202
    201 The simulation will relate Cminor states to RTLabs states about to
    202 execute the corresponding code (with a corresponding continuation).
     203The simulation will relate Cminor states to RTLabs states which are about to
     204execute the code corresponding to the Cminor statement or continuation.
    203205Each Cminor statement becomes zero or more RTLabs statements, with a
    204206decreasing measure based on the statement and continuations similar to
     
    209211The first two labelling properties remain as before; we will show that
    210212cost labels are preserved, so the function entry point will be a cost
    211 label, and successors that are cost labels map still map to cost
    212 labels, preserving the condition on branches.  We replace the property
    213 for loops with the notion that we will always reach a cost label or
    214 the end of the function by following a bounded number of successors.
    215 This can be easily seen in Cminor using the requirement for cost
    216 labels at the head of loops and after gotos.  It remains to show that
    217 this is preserved by the translation to RTLabs.  % how?
     213label, and successors to any statement that are cost labels map still
     214map to cost labels, preserving the condition on branches.  We replace
     215the property for loops with the notion that we will always reach a
     216cost label or the end of the function after following a bounded number of
     217successors.  This can be easily seen in Cminor using the requirement
     218for cost labels at the head of loops and after gotos.  It remains to
     219show that this is preserved by the translation to RTLabs.  % how?
    218220
    219221\subsection{RTLabs structured trace generation}
     
    222224labelling properties into the execution trace.  As the function calls
    223225are nested within the trace, we need to distinguish between
    224 terminating and non-terminating function calls.
    225 
    226 Thus we use the excluded middle (specialised to a function termination
    227 property) to do this.  Terminating functions are built by following
    228 the trace, breaking it into chunks between cost labels and recursively
    229 processing function calls.  The main difficulties here are the
    230 non-structurally recursive nature of the function (instead we use the
    231 size of the termination proof as a measure) and using the properties
    232 on RTLabs cost labelling to create the correct structure.  We also
    233 show that the lower stack frames are preserved during function calls
    234 in order to prove that after returning from a function call we execute
    235 the correct code.  This part of the work has already been constructed,
    236 but still requires a simple proof to show that flattening the structured
     226terminating and non-terminating function calls.  Thus we use the
     227excluded middle (specialised to a function termination property) to do
     228this.
     229
     230Structured traces for terminating functions are built by following the
     231flat trace, breaking it into chunks between cost labels and
     232recursively processing function calls.  The main difficulties here are
     233the non-structurally recursive nature of the function (instead we use
     234the size of the termination proof as a measure) and using the RTLabs
     235cost labelling properties to show that the constraints of the
     236structured traces are observed.  We also show that the lower stack
     237frames are preserved during function calls in order to prove that
     238after returning from a function call we resume execution of the
     239correct code.  This part of the work has already been constructed, but
     240still requires a simple proof to show that flattening the structured
    237241trace recreates the original flat trace.
    238242
    239 The non-terminating case uses the excluded middle to decide whether to
    240 use the function described above to construct an inductive terminating
    241 structured trace, or a coinductive version for non-termination.  It
    242 follows the trace like the terminating version to build up chunks of
    243 trace from cost-label to cost-label (which, by the finite distance to
    244 a cost label property shown before, can be represented by an inductive
    245 type), unless it encounters a non-terminating function in which case
    246 it corecursively processes that.  This part of the trace
    247 transformation is currently under construction, and will also need a
    248 flattening result to show that it is correct.
     243The non-terminating case follows the trace like the terminating
     244version to build up chunks of trace from cost-label to cost-label
     245(which, by the finite distance to a cost label property shown before,
     246can be represented by an inductive type).  These chunks are chained
     247together in a coinductive data structure that can represent
     248non-terminating traces.  The excluded middle is used to decide whether
     249function calls terminate, in which case the function described above
     250constructs an inductive terminating structured trace which is nested
     251in the caller's trace.  Otherwise, another coinductive constructor is
     252used to embed the non-terminating trace of the callee, generated by
     253corecursion.  This part of the trace transformation is currently under
     254construction, and will also need a flattening result to show that it
     255is correct.
     256
    249257
    250258\section{Backend: RTLabs to machine code}
Note: See TracChangeset for help on using the changeset viewer.