Changeset 3216


Ignore:
Timestamp:
Apr 29, 2013, 11:15:46 PM (4 years ago)
Author:
campbell
Message:

Revisions throughout 3.4.

File:
1 edited

Legend:

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

    r3214 r3216  
    309309\subsection{Main goals}
    310310
    311 TODO: need an example for this
    312 
    313311Informally, our main intensional result links the time difference in a source
    314312code execution to the time difference in the object code, expressing the time
     
    342340guarantees on; they must start at a cost label and end at the return
    343341of the enclosing function of the cost label\footnote{We expect that
    344   this would generalise to subtraces between cost labels in the same
    345   function, but could not justify the extra complexity that would be
    346   required to show this.}.  A typical example of such a subtrace is
    347 the execution of an entire function from the cost label at the start
    348 of the function until it returns.  We call such any such subtrace
    349 \emph{measurable} if it (and the prefix of the trace from the start to
    350 the subtrace) can also be executed within the available stack space.
     342  this would generalise to more general subtraces by subtracting costs
     343  for unwanted measurable suffixes of a measurable subtrace.}.  A
     344typical example of such a subtrace is the execution of an entire
     345function from the cost label at the start of the function until it
     346returns.  We call such any such subtrace \emph{measurable} if it (and
     347the prefix of the trace from the start to the subtrace) can also be
     348executed within the available stack space.
    351349
    352350Now we can give the main intensional statement for the compiler.
     
    357355function calls and returns.
    358356
     357
     358
    359359More formally, the definition of this statement in \matita{} is
    360360\begin{lstlisting}[language=matita]
    361361definition simulates :=
    362362  $\lambda$p: compiler_output.
    363   let initial_status := initialise_status $\dots$ (cm (c_labelled_object_code $\dots$ p)) in
     363  let initial_status := initialise_status $...$ (cm (c_labelled_object_code $...$ p)) in
    364364  $\forall$m1,m2.
    365    measurable Clight_pcs (c_labelled_clight $\dots$ p) m1 m2
    366     (lookup_stack_cost (c_stack_cost $\dots$ p)) (c_max_stack $\dots$ p) $\rightarrow$
     365   measurable Clight_pcs (c_labelled_clight $...$ p) m1 m2
     366       (stack_sizes (c_stack_cost $...$ p)) (c_max_stack $...$ p) $\rightarrow$
    367367  $\forall$c1,c2.
    368    clock_after Clight_pcs (c_labelled_clight $\dots$ p) m1 (c_clight_cost_map $\dots$ p) = OK $\dots$ c1 $\rightarrow$
    369    clock_after Clight_pcs (c_labelled_clight $\dots$ p) (m1+m2) (c_clight_cost_map $\dots$ p) = OK $\dots$ c2 $\rightarrow$
     368   clock_after Clight_pcs (c_labelled_clight $...$ p) m1 (c_clight_cost_map $...$ p) = OK $...$ c1 $\rightarrow$
     369   clock_after Clight_pcs (c_labelled_clight $...$ p) (m1+m2) (c_clight_cost_map $...$ p) = OK $...$ c2 $\rightarrow$
    370370  $\exists$n1,n2.
    371    observables Clight_pcs (c_labelled_clight $\dots$ p) m1 m2 =
    372    observables (OC_preclassified_system (c_labelled_object_code $\dots$ p))
    373     (c_labelled_object_code $\dots$ p) n1 n2
     371   observables Clight_pcs (c_labelled_clight $...$ p) m1 m2 =
     372     observables (OC_preclassified_system (c_labelled_object_code $...$ p))
     373          (c_labelled_object_code $...$ p) n1 n2
    374374  $\wedge$
    375    c2 - c1 = clock $\dots$ (execute n2 ? initial_status) - clock $\dots$ (execute n1 ? initial_status).
     375   clock ?? (execute (n1+n2) ? initial_status) =
     376     clock ?? (execute n1 ? initial_status) + (c2-c1).
    376377\end{lstlisting}
    377378where the \lstinline'measurable', \lstinline'clock_after' and
    378 \lstinline'observables' definitions can be applied to multiple
     379\lstinline'observables' definitions are generic definitions for multiple
    379380languages; in this case the \lstinline'Clight_pcs' record applies them
    380381to \textsf{Clight} programs.
     
    387388  $\forall$input_program,output.
    388389  compile input_program = return output $\rightarrow$
    389   not_wrong … (exec_inf … clight_fullexec input_program) $\rightarrow$
     390  not_wrong $...$ (exec_inf $...$ clight_fullexec input_program) $\rightarrow$
    390391  sim_with_labels
    391    (exec_inf clight_fullexec input_program)
    392    (exec_inf … clight_fullexec (c_labelled_clight … output))
     392   (exec_inf $...$ clight_fullexec input_program)
     393   (exec_inf $...$ clight_fullexec (c_labelled_clight $...$ output))
    393394\end{lstlisting}
    394395That is, any successful compilation produces a labelled program that
     
    396397`undefined behaviour'.
    397398
    398 Note that this provides full functional correctness, including
     399Note that this statement provides full functional correctness, including
    399400preservation of (non-)termination.  The intensional result above does
    400401not do this directly --- it does not guarantee the same result or same
    401402termination.  There are two mitigating factors, however: first, to
    402 prove the intensional property you need local simulation results that
     403prove the intensional property you need local simulation results --- these
    403404can be pieced together to form full behavioural equivalence, only time
    404405constraints have prevented us from doing so.  Second, if we wish to
     
    412413
    413414The essential parts of the intensional proof were outlined during work
    414 on a toy
    415 compiler~\cite{d2.1,springerlink:10.1007/978-3-642-32469-7_3}.  These
    416 are
     415on a toy compiler in Task
     4162.1~\cite{d2.1,springerlink:10.1007/978-3-642-32469-7_3}.  These are
    417417\begin{enumerate}
    418418\item functional correctness, in particular preserving the trace of
     
    441441
    442442Jointly, we generalised the structured traces to apply to any of the
    443 intermediate languages with some idea of program counter.  This means
     443intermediate languages which have some idea of program counter.  This means
    444444that they are introduced part way through the compiler, see
    445445Figure~\ref{fig:compiler}.  Proving that a structured trace can be
     
    451451  language and so the structural properties are ensured by the
    452452  semantics.
    453 \item Many of the back-end languages from \textsf{RTL} share a common
     453\item Many of the back-end languages from \textsf{RTL} onwards share a common
    454454  core set of definitions, and using structured traces throughout
    455455  increases this uniformity.
     
    497497with the transformations in \textsf{Clight} that produce the source
    498498program with cost labels, then show that measurable traces can be
    499 lifted to \textsf{RTLabs}, and finally that we can construct the
     499lifted to \textsf{RTLabs}, and finally show that we can construct the
    500500properties listed above ready for the back-end proofs.
    501501
     
    505505As explained on page~\pageref{page:switchintro}, the costs of complex
    506506C \lstinline[language=C]'switch' statements cannot be represented with
    507 the simple labelling.  Our first pass replaces these statements with
    508 simpler C code, allowing our second pass to perform the cost
    509 labelling.  We show that the behaviour of programs is unchanged by
    510 these passes.
     507the simple labelling used in the formalised compiler.  Our first pass
     508replaces these statements with simpler C code, allowing our second
     509pass to perform the cost labelling.  We show that the behaviour of
     510programs is unchanged by these passes using forward
     511simulations\footnote{All of our languages are deterministic, which can
     512be seen directly from their executable definitions.  Thus we know that
     513forward simulations are sufficient because the target cannot have any
     514other behaviour.}.
    511515
    512516\subsection{Switch removal}
    513517
    514 The intermediate languages of the front-end have no jump tables.
    515 Hence, we have to compile the \lstinline[language=C]'switch'
    516 constructs away before going from \textsf{Clight} to \textsf{Cminor}.
     518We compile away \lstinline[language=C]'switch' statements into more
     519basic \textsf{Clight} code.
    517520Note that this transformation does not necessarily deteriorate the
    518521efficiency of the generated code. For instance, compilers such as GCC
     
    535538may contain \lstinline[language=C]'break' statements, which have the
    536539effect of exiting the switch statement. In the absence of break, the
    537 execution falls through each case sequentially. In our current implementation,
     540execution falls through each case sequentially. In our implementation,
    538541we produce an equivalent sequence of ``if-then'' chained by gotos:
    539542\begin{lstlisting}[language=C]
     
    545548   if(fresh == v2) {
    546549     lbl_case2:
    547      $\llbracket$stmt2;$\rrbracket$
     550     $\llbracket$stmt2$\rrbracket$;
    548551     goto lbl_case2;
    549552   };
     
    554557The proof had to tackle the following points:
    555558\begin{itemize}
    556 \item the source and target memories are not the same (cf. fresh variable),
     559\item the source and target memories are not the same (due to the fresh variable),
    557560\item the flow of control is changed in a non-local way (e.g. \textbf{goto}
    558561  instead of \textbf{break}).
     
    584587steps for the added cost labels.  The extra instructions do not change
    585588the memory or local environments, although we have to keep track of
    586 the extra instructions in continuations.
     589the extra instructions that appear in continuations, for example
     590during the execution of a \lstinline[language=C]'while' loop.
    587591
    588592We do not attempt to capture any cost properties of the labelling in
    589 the simulation proof, allowing the proof to be oblivious to the choice
     593the simulation proof\footnote{We describe how the cost properties are
     594established in Section~\ref{sec:costchecks}.}, allowing the proof to be oblivious to the choice
    590595of cost labels.  Hence we do not have to reason about the threading of
    591596name generation through the labelling function, greatly reducing the
    592 amount of effort required.  We describe how the cost properties are
    593 established in Section~\ref{sec:costchecks}.
     597amount of effort required.
    594598
    595599%TODO: both give one-step-sim-by-many forward sim results; switch
     
    611615\item transformation to \textsf{RTLabs} control flow graph
    612616\end{enumerate}
    613 \todo{I keep mentioning forward sim results - I probably ought to say
    614   something about determinancy} We have taken a common approach to
     617We have taken a common approach to
    615618each pass: first we build (or axiomatise) forward simulation results
    616 that are similar to normal compiler proofs, but slightly more
     619that are similar to normal compiler proofs, but which are slightly more
    617620fine-grained so that we can see that the call structure and relative
    618621placement of cost labels is preserved.
     
    623626this result we can find a measurable subtrace of the execution of the
    624627\textsf{RTLabs} code, suitable for the construction of a structured
    625 trace (see Section~\ref{sec:structuredtrace}.  This is essentially an
     628trace (see Section~\ref{sec:structuredtrace}).  This is essentially an
    626629extra layer on top of the simulation proofs that provides us with the
    627 extra information required for our intensional correctness proof.
     630additional information required for our intensional correctness proof.
    628631
    629632\subsection{Generic measurable subtrace lifting proof}
     
    632635semantics for the source and target language, a classification of
    633636states (the same form of classification is used when defining
    634 structured traces), a simulation relation which loosely respects the
    635 classification and cost labelling \todo{this isn't very helpful} and
    636 four simulation results:
     637structured traces), a simulation relation which respects the
     638classification and cost labelling and
     639four simulation results.  The simulations are split by the starting state's
     640classification and whether it is a cost label, which will allow us to
     641observe that the call structure is preserved.  They are:
    637642\begin{enumerate}
    638643\item a step from a `normal' state (which is not classified as a call
     
    689694\label{prog:terminationproof}
    690695\begin{lstlisting}[language=matita]
    691 let rec will_return_aux C (depth:nat)
    692                              (trace:list (cs_state … C × trace)) on trace : bool :=
    693 match trace with
    694 [ nil $\Rightarrow$ false
    695 | cons h tl $\Rightarrow$
    696   let $\langle$s,tr$\rangle$ := h in
    697   match cs_classify C s with
    698   [ cl_call $\Rightarrow$ will_return_aux C (S depth) tl
    699   | cl_return $\Rightarrow$
    700       match depth with
    701       [ O $\Rightarrow$ match tl with [ nil $\Rightarrow$ true | _ $\Rightarrow$ false ]
    702       | S d $\Rightarrow$ will_return_aux C d tl
    703       ]
    704   | _ $\Rightarrow$ will_return_aux C depth tl
    705   ]
    706 ].
     696  let rec will_return_aux C (depth:nat)
     697                               (trace:list (cs_state $...$ C × trace)) on trace : bool :=
     698  match trace with
     699  [ nil $\Rightarrow$ false
     700  | cons h tl $\Rightarrow$
     701    let $\langle$s,tr$\rangle$ := h in
     702    match cs_classify C s with
     703    [ cl_call $\Rightarrow$ will_return_aux C (S depth) tl
     704    | cl_return $\Rightarrow$
     705        match depth with
     706        [ O $\Rightarrow$ match tl with [ nil $\Rightarrow$ true | _ $\Rightarrow$ false ]
     707        | S d $\Rightarrow$ will_return_aux C d tl
     708        ]
     709    | _ $\Rightarrow$ will_return_aux C depth tl
     710    ]
     711  ].
    707712\end{lstlisting}
    708713The \lstinline'depth' is the number of return states we need to see
     
    728733\end{lstlisting}
    729734The stack space requirement that is embedded in \lstinline'measurable'
    730 is a consequence of the preservation of observables.
     735is a consequence of the preservation of observables, because it is
     736determined by the functions called and returned from, which are observable.
    731737
    732738TODO: how to deal with untidy edges wrt to sim rel; anything to
    733739say about obs?
    734740
    735 TODO: say something about termination measures; cost labels are
     741TODO: cost labels are
    736742statements/exprs in these languages; split call/return gives simpler
    737743simulations
     
    739745\subsection{Simulation results for each pass}
    740746
    741 \paragraph{Cast simplification.}
    742 
    743 The parser used in Cerco introduces a lot of explicit type casts.
     747We now consider the simulation results for the passes, each of which
     748is used to instantiate the
     749\lstinline[language=matita]'measured_subtrace_preserved' theorem to
     750construct the measurable subtrace for the next language.
     751
     752\subsubsection{Cast simplification}
     753
     754The parser used in \cerco{} introduces a lot of explicit type casts.
    744755If left as they are, these constructs can greatly hamper the
    745756quality of the generated code -- especially as the architecture
    746 we consider is an $8$ bit one. In \textsf{Clight}, casts are
     757we consider is an $8$-bit one. In \textsf{Clight}, casts are
    747758expressions. Hence, most of the work of this transformation
    748759proceeds on expressions. The tranformation proceeds by recursively
     
    754765\begin{lstlisting}[language=matita]
    755766let rec simplify_expr (e:expr) (target_sz:intsize) (target_sg:signedness)
    756   : Σresult:bool×expr.
    757     ∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) ≝ $\ldots$
    758 
    759 and simplify_inside (e:expr) : Σresult:expr. conservation e result ≝ $\ldots$
     767  : $\Sigma$result:bool$\times$expr.
     768    $\forall$ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) := $\ldots$
     769
     770and simplify_inside (e:expr) : $\Sigma$result:expr. conservation e result := $\ldots$
    760771\end{lstlisting}
    761772
     
    781792inductive simplify_inv
    782793  (ge : genv) (en : env) (m : mem)
    783   (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool → Prop ≝
    784 | Inv_eq : result_flag. $\ldots$
     794  (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool $\rightarrow$ Prop :=
     795| Inv_eq : $\forall$result_flag. $\ldots$
    785796     simplify_inv ge en m e1 e2 target_sz target_sg result_flag
    786 | Inv_coerce_ok : ∀src_sz,src_sg.
    787      (typeof e1) = (Tint src_sz src_sg) → (typeof e2) = (Tint target_sz target_sg) →     
    788      (smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2)) →
     797| Inv_coerce_ok : $\forall$src_sz,src_sg.
     798     typeof e1 = Tint src_sz src_sg $\rightarrow$
     799     typeof e2 = Tint target_sz target_sg $\rightarrow$     
     800     smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2) $\rightarrow$
    789801     simplify_inv ge en m e1 e2 target_sz target_sg true.
    790802\end{lstlisting}
    791803
    792 The \textsf{conservation} invariant simply states the conservation
     804The \textsf{conservation} invariant for \textsf{simplify\_inside} simply states the conservation
    793805of the semantics, as in the \textsf{Inv\_eq} constructor of the previous
    794806invariant.
    795807
    796808\begin{lstlisting}[language=matita]
    797 definition conservation ≝ λe,result. ∀ge,en,m.
     809definition conservation := $\lambda$e,result. $\forall$ge,en,m.
    798810          res_sim ? (exec_expr ge en m e) (exec_expr ge en m result)
    799          ∧ res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
    800          ∧ typeof e = typeof result.
     811       $\wedge$ res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
     812       $\wedge$ typeof e = typeof result.
    801813\end{lstlisting}
    802814
     
    805817inconsistently typed programs, a canonical case being a particular
    806818integer constant of a certain size typed with another size. This
    807 prompted the need to introduce numerous type checks, complexifying
    808 both the implementation and the proof.
     819prompted the need to introduce numerous type checks, making
     820both the implementation and the proof more complex, even though more
     821comprehensive checks are made in the next stage.
    809822\todo{Make this a particular case of the more general statement on baking more invariants in the Clight language}
    810823
    811 \paragraph{Clight to Cminor.}
    812 
    813 This pass is the last one operating on the Clight intermediate language.
    814 Its input is a full \textsf{Clight} program, and its output is a \textsf{Cminor}
    815 program. Note that we do not use an equivalent of the C\#minor language: we
    816 translate directly to Cminor. This presents the advantage of not requiring the
    817 special loop constructs, nor the explicit block structure. Another salient
    818 point of our approach is that a significant part of the properties needed for
    819 the simulation proof were directly encoded in dependently typed translation
    820 functions. This concerns more precisely freshness conditions and well-typedness
    821 conditions. The main effects of the transformation from \textsf{Clight} to
     824\subsection{Clight to Cminor}
     825
     826This pass is the last one operating on the \textsf{Clight} language.
     827Its input is a full \textsf{Clight} program, and its output is a
     828\textsf{Cminor} program. Note that we do not use an equivalent of
     829Compcert's \textsf{C\#minor} language: we translate directly to a
     830variant of \textsf{Cminor}. This presents the advantage of not
     831requiring the special loop constructs, nor the explicit block
     832structure. Another salient point of our approach is that a significant
     833number of the properties needed for the simulation proof were directly
     834encoded in dependently typed translation functions.  In particular,
     835freshness conditions and well-typedness conditions are included. The
     836main effects of the transformation from \textsf{Clight} to
    822837\textsf{Cminor} are listed below.
    823838
     
    827842  local variables is moved out of the modelled memory and stored in a
    828843  dedicated environment.
    829 \item In Clight, each local variable has a dedicated memory block, whereas
     844\item In \textsf{Clight}, each local variable has a dedicated memory block, whereas
    830845  stack-allocated locals are bundled together on a function-by-function basis.
    831846\item Loops are converted to jumps.
     
    843858manipulations (as in the later version of Compcert's memory model). We proved
    844859roughly 80 \% of the required lemmas. Some difficulties encountered were notably
    845 due to some too relaxed conditions on pointer validity (problem fixed during development).
    846 Some more conditions had to be added to take care of possible overflows when converting
    847 from \textbf{Z} block bounds to $16$ bit pointer offsets (in pratice, these overflows
     860due to some overly relaxed conditions on pointer validity (fixed during development).
     861Some more side conditions had to be added to take care of possible overflows when converting
     862from \textbf{Z} block bounds to $16$ bit pointer offsets (in practice, these overflows
    848863only occur in edge cases that are easily ruled out -- but this fact is not visible
    849864in memory injections). Concretely, some of the lemmas on the preservation of simulation of
    850 loads after writes were axiomatised, for lack of time.
     865loads after writes were axiomatised, due to a lack of time.
    851866
    852867\subparagraph{Simulation proof.}
    853868
    854 The correction proof for this transformation was not terminated. We proved the
     869The correctness proof for this transformation was not completed. We proved the
    855870simulation result for expressions and for some subset of the critical statement cases.
    856871Notably lacking are the function entry and exit, where the memory injection is
    857 properly set up. As can be guessed, a significant amount of work has to be performed
     872properly set up. As would be expected, a significant amount of work has to be performed
    858873to show the conservation of all invariants at each simulation step.
    859874
     
    864879
    865880Ideally, we would provide proofs that the cost labelling pass always
    866 produced programs that are soundly and precisely labelled and that
     881produces programs that are soundly and precisely labelled and that
    867882each subsequent pass preserves these properties.  This would match our
    868883use of dependent types to eliminate impossible sources of errors
     
    895910checking this is more difficult.
    896911
    897 The implementation works through the set of nodes in the graph,
     912The implementation progresses through the set of nodes in the graph,
    898913following successors until a cost label is found or a label-free cycle
    899914is discovered (in which case the property does not hold and we stop).
     
    909924was then used to prove the implementation sound and complete.
    910925
    911 While we have not attempted to proof that the cost labelled properties
     926While we have not attempted to prove that the cost labelled properties
    912927are established and preserved earlier in the compiler, we expect that
    913 the effort for the \textsf{Cminor} to \textsf{RTLabs} would be similar
    914 to the work outlined above, because it involves the change from
    915 requiring a cost label at particular positions to requiring cost
    916 labels to break loops in the CFG.  As there are another three passes
    917 to consider (including the labelling itself), we believe that using
    918 the check above is much simpler overall.
     928the effort for the \textsf{Cminor} to \textsf{RTLabs} stage alone
     929would be similar to the work outlined above, because it involves the
     930change from requiring a cost label at particular positions to
     931requiring cost labels to break loops in the CFG.  As there are another
     932three passes to consider (including the labelling itself), we believe
     933that using the check above is much simpler overall.
    919934
    920935% TODO? Found some Clight to Cminor bugs quite quickly
     
    923938\label{sec:structuredtrace}
    924939
    925 \emph{Structured traces} enrich the execution trace of a program by
    926 nesting function calls in a mixed-step style and embedding the cost
     940The \emph{structured traces} introduced in Section~\ref{sec:fegoals} enrich the execution trace of a program by
     941nesting function calls in a mixed-step style and embedding the cost labelling
    927942properties of the program.  It was originally designed to support the
    928943proof of correctness for the timing analysis of the object code in the
     
    948963  }.
    949964\end{lstlisting}
    950 which gives a type of states, an execution relation, some notion of
    951 program counters with decidable equality, the classification of states
     965which gives a type of states, an execution relation\footnote{All of
     966  our semantics are executable, but using a relation was simpler in
     967  the abstraction.}, some notion of
     968program counters with decidable equality, the classification of states,
    952969and functions to extract the observable intensional information (cost
    953970labels and the identity of functions that are called).  The
     
    961978The structured traces are defined using three mutually inductive
    962979types.  The core data structure is \lstinline'trace_any_label', which
    963 captures some straight-line execution until the next cost label or
    964 function return.  Each function call is embedded as a single step,
    965 with its own trace nested inside and the before and after states
    966 linked by \lstinline'as_after_return', and states classified as a
    967 `jump' (in particular branches) must be followed by a cost label.
     980captures some straight-line execution until the next cost label or the
     981return from the enclosing function.  Any function calls are embedded as
     982a single step, with its own trace nested inside and the before and
     983after states linked by \lstinline'as_after_return'; and states
     984classified as a `jump' (in particular branches) must be followed by a
     985cost label.
    968986
    969987The second type, \lstinline'trace_label_label', is a
     
    981999
    9821000The construction of the structured trace replaces syntactic cost
    983 labelling properties which place requirements on where labels appear
     1001labelling properties, which place requirements on where labels appear
    9841002in the program, with semantics properties that constrain the execution
    9851003traces of the program.  The construction begins by defining versions
    986 of the sound and precise labelling properties on the program text that
    987 appears in states rather than programs, and showing that these are
    988 preserved by steps of the \textsf{RTLabs} semantics.
     1004of the sound and precise labelling properties on states and global
     1005environments (for the code that appears in each of them) rather than
     1006whole programs, and showing that these are preserved by steps of the
     1007\textsf{RTLabs} semantics.
    9891008
    9901009Then we show that each cost labelling property the structured traces
    991 definition requires is satisfied.  These are broken up by the
     1010definition requires is locally satisfied.  These are broken up by the
    9921011classification of states.  Similarly, we prove a step-by-step stack
    9931012preservation result, which states that the \textsf{RTLabs} semantics
     
    10111030label.
    10121031
    1013 \subsubsection{Whole program structured traces}
     1032\subsubsection{Complete execution structured traces}
    10141033
    10151034The development of the construction above started relatively early,
    1016 before the measurable subtraces preservation proofs.  To be confident
    1017 that the traces were well-formed, we also developed a whole program
    1018 form that embeds the traces above.  This includes non-terminating
    1019 programs, where an infinite number of the terminating structured
    1020 traces are embedded.  This construction confirmed that our definition
    1021 of structured traces was consistent, although we later found that we
    1022 did not require them for the compiler correctness results.
     1035before the measurable subtrace preservation proofs.  To be confident
     1036that the traces were well-formed at that time, we also developed a
     1037complete execution form that embeds the traces above.  This includes
     1038non-terminating program executions, where an infinite number of the terminating
     1039structured traces are embedded.  This construction confirmed that our
     1040definition of structured traces was consistent, although we later
     1041found that we did not require the whole execution version for the
     1042compiler correctness results.
    10231043
    10241044To construct these we need to know whether each function call will
     
    10321052concentrating on the novel intensional parts of the proof, we have
    10331053shown that it is possible to construct certifying compilers that
    1034 correctly report execution time and stack space costs.
     1054correctly report execution time and stack space costs.  The layering
     1055of intensional correctness proofs on top of normal simulation results
     1056provides a useful separation of concerns, and could permit the reuse
     1057of existing results.
     1058
     1059
    10351060
    10361061TODO: appendix on code layout?
Note: See TracChangeset for help on using the changeset viewer.