# Changeset 3167 for Deliverables/D3.4/Report/report.tex

Ignore:
Timestamp:
Apr 19, 2013, 12:30:24 PM (6 years ago)
Message:

A little bit about structured traces.

File:
1 edited

### Legend:

Unmodified
 r3159 the check above is much simpler overall. % TODO? Found some Clight to Cminor bugs quite quickly \section{Existence of a structured trace} \label{sec:structuredtrace} for an illustration of a structured trace. To make the definition generic we abstract over the semantics of the language, \begin{lstlisting}[language=matita] record abstract_status : Type[1] := { as_status :> Type[0] ; as_execute : relation as_status ; as_pc : DeqSet ; as_pc_of : as_status $\rightarrow$ as_pc ; as_classify : as_status $\rightarrow$ status_class ; as_label_of_pc : as_pc $\rightarrow$ option costlabel ; as_after_return : ($\Sigma$s:as_status. as_classify s =  cl_call) $\rightarrow$ as_status $\rightarrow$ Prop ; as_result: as_status $\rightarrow$ option int ; as_call_ident : ($\Sigma$s:as_status.as_classify s = cl_call) $\rightarrow$ ident ; as_tailcall_ident : ($\Sigma$s:as_status.as_classify s = cl_tailcall) $\rightarrow$ ident }. \end{lstlisting} which gives a type of states, an execution relation, some notion of program counters with decidable equality, the classification of states and functions to extract the observable intensional information (cost labels and the identity of functions that are called). The structured traces are defined using three mutually inductive types.  The core data structure is \lstinline'trace_any_label', which captures some straight-line execution until the next cost label or function return.  Each function call is embedded as a single step, with its own trace nested inside, and states classified as a `jump' (in particular branches) must be followed by a cost label. The second type, \lstinline'trace_label_label', is a \lstinline'trace_any_label' where the initial state is cost labelled. Thus a trace in this type identifies a series of steps whose cost is entirely accounted for by the label at the start. Finally, \lstinline'trace_label_return' is a sequence of \lstinline'trace_label_label' values which end in the return from the function.  These correspond to a measurable subtrace, and in particular include executions of an entire function call. TODO: design, basic structure from termination proof, how cost