Changeset 2455 for Papers


Ignore:
Timestamp:
Nov 12, 2012, 4:39:57 PM (7 years ago)
Author:
campbell
Message:

Dump rough notes on RTLabs structured traces existence proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/structured-traces-2012/structured-traces.tex

    r2451 r2455  
    5151
    5252%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     53% Definitions, choices, etc                                                   %
     54%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     55\section{Definition of structured traces}
     56\label{sect.defn}
     57
     58TODO: abstraction of intermediate language semantics, definition of structured
     59traces, commentary on decisions made, pretty diagrams
     60
     61%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     62% Edinburgh work on existence of RTLabs str traces                            %
     63%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     64\section{Existence of structured traces}
     65\label{sect.rtlabs}
     66
     67%  existence proof details that I think are irrelevant to this paper:
     68%  - fn ids are memory block ids rather than the original name
     69%  - a shadow stack is maintained because the semantics don't record the fn id
     70%  - we first go from flat traces made from exec_inf to ones which include
     71%    evidence of each step of execution (flat_trace)
     72
     73% TODO: no I/O in present construction - do we need to do something about that?
     74
     75[Bit of a braindump for now.]
     76
     77TODO: choice of language (esp, first to have reasonable PCs),
     78restricted use of excluded middle for termination
     79
     80Currently in the order of the proof, rearrange.
     81
     82Brief note on abstraction: PCs are fn id / cfg node id pairs (with slight
     83variations for call/ret/fin states)
     84% fn ids are actually blocks, and there's a shadow stack to record which we
     85% are on, but that's not really relevant
     86Only statements considered as `jumps' are conditionals (no unconditional jumps
     87because we're in a cfg).
     88\verb'as_after_return' property is that next caller node and caller fn must be
     89preserved.
     90
     91\verb'will_return' asserts that a prefix of a trace eventually returns, using
     92the call/ret/jump/other classification fn.  Will use excluded middle on this
     93for deciding termination.  Use length of these as part of termination witness
     94for construction fn.
     95% lemmas for composing (will_return_prepend), slicing (will_return_remove_call)
     96% will_return?
     97
     98Specifications of cost labelling (???.ma), lift them to runtime notions of
     99globalenvs, states, preserved by steps (\verb'well_cost_labelled_state_step').
     100Label follows a conditional (\verb'well_cost_labelled_jump'), call
     101(semantically, i.e., the first thing in a function is the cost label).
     102
     103(RTLabs) Stack preservation - essential for \verb'as_after_return' (and more?)
     104- as with structured traces it ends with the state \emph{after} the return.
     105Like \verb'will_return' do composition, steps (including over calls).  Then
     106we extract \verb'as_after_return'.  Note: these proofs are technically fairly
     107routine, once we've got the right definitions.
     108
     109\verb'make_label_return' and it's mutually defined functions
     110\verb'make_label_label' and \verb'make_any_label' are the main results for
     111finite subtraces.  These consume a prefix of the flat trace (given some
     112hypotheses about well labelling) according to a \verb'will_return' structure
     113that determines how much is used.  A record is returned containing the end
     114state, the remainder of the trace, a proof of stack preservation, and the
     115remainder (if any) of the \verb'will_terminates' structure.  The functions
     116themselves examine the flat trace, checks for a cost label where they can
     117optionally appear and proves the properties embedded in the structured traces
     118using the above lemmas.  They are given in a mixed definition/proof script
     119style; unusually some of the proofs are partly contained in the definition to
     120make full use of dependent pattern matching.
     121
     122
     123Abstract successors from semantics to syntax; rephrase bound on instructions
     124from cost spec to bound on (local) steps to label; prove that the bound
     125reduces as you would expect (requires \verb'as_after_return'), that sound
     126labelled lifted to semantics is preserved by steps.
     127
     128Construction of whole program traces proceeds using excluded middle on existence
     129of a \verb'will_return' structure.  Terminating executions just embed the
     130structured trace from \verb'make_label_return', but non-terminating executions
     131are built by a cofixpoint which extracts a finite prefix, which is constructed
     132in a similar way to \verb'make_label_return', but using the bound on steps to a
     133cost label to demonstrate termination and stopping on the next cost label in
     134the function, or another non-terminating function call.  (Better to describe
     135the idea, then note interesting things about the implementation.)
     136
     137Both structured traces and flat traces are determined by their start state
     138because there's no I/O, so get flattening = original trace.
     139
     140Also show separate non-repeating property (no repeated PC without a cost label)
     141by splitting on whether a repeated state is a cost label - if so it can't
     142reappear in the relevant part of the structured trace, if not we break the
     143sound labelling property on instructions by finding a loop of successor
     144instructions without a cost label.  (Note: this is on instructions, above we
     145used a derived version on states.)  Rule out repeated call states by reference
     146to the successor instruction.  Applying this throughout the structured trace
     147give the \verb'*_sound_unrepeating' properties.
     148
     149%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
    53150% Section.                                                                    %
    54151%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
Note: See TracChangeset for help on using the changeset viewer.