Changeset 3158

Apr 17, 2013, 7:17:49 PM (4 years ago)

Some text on measurable subtraces throughout the front-end.

2 added
1 edited


  • Deliverables/D3.4/Report/report.tex

    r3142 r3158  
    448448\item transformation to \textsf{RTLabs} control flow graph
    451 TODO: layered approach - main part is the common measurable
    452 preservation proof; fine-grained version of normal simulation results
    453 does rest.
     450\todo{I keep mentioning forward sim results - I probably ought to say
     451  something about determinancy} We have taken a common approach to
     452each pass: first we build (or axiomatise) forward simulation results
     453that are similar to normal compiler proofs, but slightly more
     454fine-grained so that we can see that the call structure and relative
     455placement of cost labels is preserved.
     457Then we instantiate a general result which shows that we can find a
     458\emph{measurable} subtrace in the target of the pass that corresponds
     459to the measurable subtract in the source.  By repeated application of
     460this result we can find a measurable subtrace of the execution of the
     461\textsf{RTLabs} code, suitable for the construction of a structured
     462trace (see Section~\ref{sec:structuredtrace}.  This is essentially an
     463extra layer on top of the simulation proofs that provides us with the
     464extra information required for our intensional correctness proof.
    455466\subsection{Generic measurable subtrace lifting proof}
    457 Sketch properties required; need to preserve prefix as well as meas
    458 subtrace; how to deal with untidy edges wrt to sim rel; anything to
    459 say about obs, stack?
     468Our generic proof is parametrised on a record containing small-step
     469semantics for the source and target language, a classification of
     470states (the same form of classification is used when defining
     471structured traces), a simulation relation which loosely respects the
     472classification and cost labelling \todo{this isn't very helpful} and
     473four simulation results:
     475\item a step from a `normal' state (which is not classified as a call
     476  or return) which is not a cost label is simulated by zero or more
     477  `normal' steps;
     478\item a step from a `call' state followed by a cost label step is
     479  simulated by a step from a `call' state, a corresponding label step,
     480  then zero or more `normal' steps;
     481\item a step from a `call' state not followed by a cost label
     482  similarly (note that this case cannot occur in a well-labelled
     483  program, but we do not have enough information locally to exploit
     484  this); and
     485\item a cost label step is simulated by a cost label step.
     487Finally, we need to know that a successfully translated program will
     488have an initial state in the simulation relation with the original
     489program's initial state.
     495\caption{Tiling of simulation for a measurable subtrace}
     499To find the measurable subtrace in the target program's execution we
     500walk along the original program's execution trace applying the
     501appropriate simulation result by induction on the number of steps.
     502While the number of steps taken varies, the overall structure is
     503preserved, as illustrated in Figure~\ref{fig:tiling}.  By preserving
     504the structure we also maintain the same intensional observables.  One
     505delicate point is that the cost label following a call must remain
     506directly afterwards\footnote{The prototype compiler allowed some
     507  straight-line code to appear before the cost label until a later
     508  stage of the compiler, but we must move the requirement forward to
     509  fit with the structured traces.}
     510% Damn it, I should have just moved the cost label forwards in RTLabs,
     511% like the prototype does in RTL to ERTL; the result would have been
     512% simpler.  Or was there some reason not to do that?
     513(both in the program code and in the execution trace), even if we
     514introduce extra steps, for example to store parameters in memory in
     515\textsf{Cminor}.  Thus we have a version of the call simulation
     516that deals with both in one result.
     518In addition to the subtrace we are interested in measuring we must
     519also prove that the earlier part of the trace is also preserved in
     520order to use the simulation from the initial state.  It also
     521guarantees that we do not run out of stack space before the subtrace
     522we are interested in.  The lemmas for this prefix and the measurable
     523subtrace are similar, following the pattern above.  However, the
     524measurable subtrace also requires us to rebuild the termination
     525proof.  This has a recursive form:
     527let rec will_return_aux C (depth:nat)
     528                             (trace:list (cs_state … C × trace)) on trace : bool :=
     529match trace with
     530[ nil $\Rightarrow$ false
     531| cons h tl $\Rightarrow$
     532  let $\langle$s,tr$\rangle$ := h in
     533  match cs_classify C s with
     534  [ cl_call $\Rightarrow$ will_return_aux C (S depth) tl
     535  | cl_return $\Rightarrow$
     536      match depth with
     537      [ O $\Rightarrow$ match tl with [ nil $\Rightarrow$ true | _ $\Rightarrow$ false ]
     538      | S d $\Rightarrow$ will_return_aux C d tl
     539      ]
     540  | _ $\Rightarrow$ will_return_aux C depth tl
     541  ]
     544The \lstinline'depth' is the number of return states we need to see
     545before we have returned to the original function (initially zero) and
     546\lstinline'trace' the measurable subtrace obtained from the running
     547the semantics for the correct number of steps.  This definition
     548unfolds tail recursively for each step, and once the corresponding
     549simulation result has been applied a new one for the target can be
     550asserted by unfolding and applying the induction hypothesis on the
     551shorter trace.
     553This then gives us an overall result for any simulation fitting the
     554requirements above (contained in the \lstinline'meas_sim' record):
     556theorem measured_subtrace_preserved :
     557  $\forall$MS:meas_sim.
     558  $\forall$p1,p2,m,n,stack_cost,max.
     559  ms_compiled MS p1 p2 $\rightarrow$
     560  measurable (ms_C1 MS) p1 m n stack_cost max $\rightarrow$
     561  $\exists$m',n'.
     562    measurable (ms_C2 MS) p2 m' n' stack_cost max $\wedge$
     563    observables (ms_C1 MS) p1 m n = observables (ms_C2 MS) p2 m' n'.
     565The stack space requirement that is embedded in \lstinline'measurable'
     566is a consequence of the preservation of observables.
     568TODO: how to deal with untidy edges wrt to sim rel; anything to
     569say about obs?
     571TODO: say something about termination measures; cost labels are
     572statements/exprs in these languages; split call/return gives simpler
    461575\subsection{Simulation results for each pass}
    473587\section{Existence of a structured trace}
    474 \label{sec:structuretrace}
    476590TODO: design, basic structure from termination proof, how cost
Note: See TracChangeset for help on using the changeset viewer.