# Changeset 3158

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

Some text on measurable subtraces throughout the front-end.

Location:
Deliverables/D3.4/Report
Files:
1 edited

Unmodified
Removed
• ## Deliverables/D3.4/Report/report.tex

 r3142 \item transformation to \textsf{RTLabs} control flow graph \end{enumerate} TODO: layered approach - main part is the common measurable preservation proof; fine-grained version of normal simulation results does rest. \todo{I keep mentioning forward sim results - I probably ought to say something about determinancy} We have taken a common approach to each pass: first we build (or axiomatise) forward simulation results that are similar to normal compiler proofs, but slightly more fine-grained so that we can see that the call structure and relative placement of cost labels is preserved. Then we instantiate a general result which shows that we can find a \emph{measurable} subtrace in the target of the pass that corresponds to the measurable subtract in the source.  By repeated application of this result we can find a measurable subtrace of the execution of the \textsf{RTLabs} code, suitable for the construction of a structured trace (see Section~\ref{sec:structuredtrace}.  This is essentially an extra layer on top of the simulation proofs that provides us with the extra information required for our intensional correctness proof. \subsection{Generic measurable subtrace lifting proof} Sketch properties required; need to preserve prefix as well as meas subtrace; how to deal with untidy edges wrt to sim rel; anything to say about obs, stack? Our generic proof is parametrised on a record containing small-step semantics for the source and target language, a classification of states (the same form of classification is used when defining structured traces), a simulation relation which loosely respects the classification and cost labelling \todo{this isn't very helpful} and four simulation results: \begin{enumerate} \item a step from a normal' state (which is not classified as a call or return) which is not a cost label is simulated by zero or more normal' steps; \item a step from a call' state followed by a cost label step is simulated by a step from a call' state, a corresponding label step, then zero or more normal' steps; \item a step from a call' state not followed by a cost label similarly (note that this case cannot occur in a well-labelled program, but we do not have enough information locally to exploit this); and \item a cost label step is simulated by a cost label step. \end{enumerate} Finally, we need to know that a successfully translated program will have an initial state in the simulation relation with the original program's initial state. \begin{figure} \begin{center} \includegraphics[width=0.5\linewidth]{meassim.pdf} \end{center} \caption{Tiling of simulation for a measurable subtrace} \label{fig:tiling} \end{figure} To find the measurable subtrace in the target program's execution we walk along the original program's execution trace applying the appropriate simulation result by induction on the number of steps. While the number of steps taken varies, the overall structure is preserved, as illustrated in Figure~\ref{fig:tiling}.  By preserving the structure we also maintain the same intensional observables.  One delicate point is that the cost label following a call must remain directly afterwards\footnote{The prototype compiler allowed some straight-line code to appear before the cost label until a later stage of the compiler, but we must move the requirement forward to fit with the structured traces.} % Damn it, I should have just moved the cost label forwards in RTLabs, % like the prototype does in RTL to ERTL; the result would have been % simpler.  Or was there some reason not to do that? (both in the program code and in the execution trace), even if we introduce extra steps, for example to store parameters in memory in \textsf{Cminor}.  Thus we have a version of the call simulation that deals with both in one result. In addition to the subtrace we are interested in measuring we must also prove that the earlier part of the trace is also preserved in order to use the simulation from the initial state.  It also guarantees that we do not run out of stack space before the subtrace we are interested in.  The lemmas for this prefix and the measurable subtrace are similar, following the pattern above.  However, the measurable subtrace also requires us to rebuild the termination proof.  This has a recursive form: \begin{lstlisting}[language=matita] let rec will_return_aux C (depth:nat) (trace:list (cs_state … C × trace)) on trace : bool := match trace with [ nil $\Rightarrow$ false | cons h tl $\Rightarrow$ let $\langle$s,tr$\rangle$ := h in match cs_classify C s with [ cl_call $\Rightarrow$ will_return_aux C (S depth) tl | cl_return $\Rightarrow$ match depth with [ O $\Rightarrow$ match tl with [ nil $\Rightarrow$ true | _ $\Rightarrow$ false ] | S d $\Rightarrow$ will_return_aux C d tl ] | _ $\Rightarrow$ will_return_aux C depth tl ] ]. \end{lstlisting} The \lstinline'depth' is the number of return states we need to see before we have returned to the original function (initially zero) and \lstinline'trace' the measurable subtrace obtained from the running the semantics for the correct number of steps.  This definition unfolds tail recursively for each step, and once the corresponding simulation result has been applied a new one for the target can be asserted by unfolding and applying the induction hypothesis on the shorter trace. This then gives us an overall result for any simulation fitting the requirements above (contained in the \lstinline'meas_sim' record): \begin{lstlisting}[language=matita] theorem measured_subtrace_preserved : $\forall$MS:meas_sim. $\forall$p1,p2,m,n,stack_cost,max. ms_compiled MS p1 p2 $\rightarrow$ measurable (ms_C1 MS) p1 m n stack_cost max $\rightarrow$ $\exists$m',n'. measurable (ms_C2 MS) p2 m' n' stack_cost max $\wedge$ observables (ms_C1 MS) p1 m n = observables (ms_C2 MS) p2 m' n'. \end{lstlisting} The stack space requirement that is embedded in \lstinline'measurable' is a consequence of the preservation of observables. TODO: how to deal with untidy edges wrt to sim rel; anything to say about obs? TODO: say something about termination measures; cost labels are statements/exprs in these languages; split call/return gives simpler simulations \subsection{Simulation results for each pass} \section{Existence of a structured trace} \label{sec:structuretrace} \label{sec:structuredtrace} TODO: design, basic structure from termination proof, how cost
Note: See TracChangeset for help on using the changeset viewer.