Changeset 2455 for Papers

Nov 12, 2012, 4:39:57 PM (6 years ago)

Dump rough notes on RTLabs structured traces existence proof.

1 edited


  • Papers/structured-traces-2012/structured-traces.tex

    r2451 r2455  
     53% Definitions, choices, etc                                                   %
     55\section{Definition of structured traces}
     58TODO: abstraction of intermediate language semantics, definition of structured
     59traces, commentary on decisions made, pretty diagrams
     62% Edinburgh work on existence of RTLabs str traces                            %
     64\section{Existence of structured traces}
     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)
     73% TODO: no I/O in present construction - do we need to do something about that?
     75[Bit of a braindump for now.]
     77TODO: choice of language (esp, first to have reasonable PCs),
     78restricted use of excluded middle for termination
     80Currently in the order of the proof, rearrange.
     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
     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?
     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).
     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.
     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.
     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.
     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.)
     137Both structured traces and flat traces are determined by their start state
     138because there's no I/O, so get flattening = original trace.
     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.
    53150% Section.                                                                    %
Note: See TracChangeset for help on using the changeset viewer.