Changeset 3167


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

A little bit about structured traces.

File:
1 edited

Legend:

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

    r3159 r3167  
    636636the check above is much simpler overall.
    637637
     638% TODO? Found some Clight to Cminor bugs quite quickly
     639
    638640\section{Existence of a structured trace}
    639641\label{sec:structuredtrace}
     
    649651for an illustration of a structured trace.
    650652
    651 
     653To make the definition generic we abstract over the semantics of the
     654language,
     655\begin{lstlisting}[language=matita]
     656record abstract_status : Type[1] :=
     657  { as_status :> Type[0]
     658  ; as_execute : relation as_status
     659  ; as_pc : DeqSet
     660  ; as_pc_of : as_status $\rightarrow$ as_pc
     661  ; as_classify : as_status $\rightarrow$ status_class
     662  ; as_label_of_pc : as_pc $\rightarrow$ option costlabel
     663  ; as_after_return : ($\Sigma$s:as_status. as_classify s =  cl_call) $\rightarrow$ as_status $\rightarrow$ Prop
     664  ; as_result: as_status $\rightarrow$ option int
     665  ; as_call_ident : ($\Sigma$s:as_status.as_classify s = cl_call) $\rightarrow$ ident
     666  ; as_tailcall_ident : ($\Sigma$s:as_status.as_classify s = cl_tailcall) $\rightarrow$ ident
     667  }.
     668\end{lstlisting}
     669which gives a type of states, an execution relation, some notion of
     670program counters with decidable equality, the classification of states
     671and functions to extract the observable intensional information (cost
     672labels and the identity of functions that are called).
     673
     674The structured traces are defined using three mutually inductive
     675types.  The core data structure is \lstinline'trace_any_label', which
     676captures some straight-line execution until the next cost label or
     677function return.  Each function call is embedded as a single step,
     678with its own trace nested inside, and states classified as a `jump'
     679(in particular branches) must be followed by a cost label.
     680
     681The second type, \lstinline'trace_label_label', is a
     682\lstinline'trace_any_label' where the initial state is cost labelled.
     683Thus a trace in this type identifies a series of steps whose cost is
     684entirely accounted for by the label at the start.
     685
     686Finally, \lstinline'trace_label_return' is a sequence of
     687\lstinline'trace_label_label' values which end in the return from the
     688function.  These correspond to a measurable subtrace, and in
     689particular include executions of an entire function call.
    652690
    653691TODO: design, basic structure from termination proof, how cost
Note: See TracChangeset for help on using the changeset viewer.