Changeset 1733


Ignore:
Timestamp:
Feb 24, 2012, 10:10:18 AM (8 years ago)
Author:
campbell
Message:

More on front-end.

File:
1 edited

Legend:

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

    r1732 r1733  
    180180\subsection{Cminor to RTLabs translation}
    181181
     182In this part of the compiler we transform the program's functions into
     183control flow graphs.  It is closely related to CompCert's Cminorsel to
     184RTL transformation, albeit with target-independent operations.
     185
     186We already enforce several invariants with dependent types: some type
     187safety is enforced mostly using the type information from Cminor; and
     188that the graph is closed (by showing that each successor was recently
     189added, or corresponds to a \lstinline[language=C]'goto' label which
     190are all added before the end).  Note that this relies on a
     191monotonicity property; CompCert maintains a similar property in a
     192similar way while building RTL graphs.  We will also add a result
     193showing that all of the pseudo-register names are distinct for use by
     194later stages using the same method as Cminor.
     195
     196The simulation will relate Cminor states to RTLabs states about to
     197execute the corresponding code (with a corresponding continuation).
     198Each Cminor statement becomes zero or more RTLabs statements, with a
     199decreasing measure based on the statement and continuations similar to
     200CompCert's.  We may also follow CompCert in using a relational
     201specification of this stage so as to abstract away from the functional
     202(and highly dependently typed) definition.
     203
     204The first two labelling properties remain as before; we will show that
     205cost labels are preserved, so the function entry point will be a cost
     206label, and successors that are cost labels map still map to cost
     207labels, preserving the condition on branches.  We replace the property
     208for loops with the notion that we will always reach a cost label or
     209the end of the function by following a bounded number of successors.
     210This can be easily seen in Cminor using the requirement for cost
     211labels at the head of loops and after gotos.  It remains to show that
     212this is preserved by the translation to RTLabs.  % how?
     213
    182214\subsection{RTLabs structured trace generation}
     215
     216This proof-only step incorporates the function call structure and cost
     217labelling properties into the execution trace.  As the function calls
     218are nested within the trace, we need to distinguish between
     219terminating and non-terminating function calls.
     220
     221Thus we use the excluded middle (specialised to a function termination
     222property) to do this.  Terminating functions are built by following
     223the trace, breaking it into chunks between cost labels and recursively
     224processing function calls.  The main difficulties here are the
     225non-structurally recursive nature of the function (instead we use the
     226size of the termination proof as a measure) and using the properties
     227on RTLabs cost labelling to create the correct structure.  We also
     228show that the lower stack frames are preserved during function calls
     229in order to prove that after returning from a function call we execute
     230the correct code.  This part of the work has already been constructed,
     231but still requires a simple proof to show that flattening the structured
     232trace recreates the original flat trace.
     233
     234The non-terminating case uses the excluded middle to decide whether to
     235use the function described above to construct an inductive terminating
     236structured trace, or a coinductive version for non-termination.  It
     237follows the trace like the terminating version to build up chunks of
     238trace from cost-label to cost-label (which, by the finite distance to
     239a cost label property shown before, can be represented by an inductive
     240type), unless it encounters a non-terminating function in which case
     241it corecursively processes that.  This part of the trace
     242transformation is currently under construction, and will also need a
     243flattening result to show that it is correct.
    183244
    184245\section{The RTLabs to RTL translation}
Note: See TracChangeset for help on using the changeset viewer.