Changeset 3203

Apr 29, 2013, 12:39:45 PM (4 years ago)

Text on structured trace construction.

1 edited


  • Deliverables/D3.4/Report/report.tex

    r3191 r3203  
    962 The core part of the construction of a fixed trace is to use the proof
    963 of termination from the measurable trace (defined on
     962The construction of the structured trace replaces syntactic cost
     963labelling properties which place requirements on where labels appear
     964in the program, with semantics properties that constrain the execution
     965traces of the program.  The construction begins by defining versions
     966of the sound and precise labelling properties on the program text that
     967appears in states rather than programs, and showing that these are
     968preserved by steps of the \textsf{RTLabs} semantics.
     970Then we show that each cost labelling property the structured traces
     971definition requires is satisfied.  These are broken up by the
     972classification of states.  Similarly, we prove a step-by-step stack
     973preservation result, which states that the \textsf{RTLabs} semantics
     974never changes the lower parts of the stack.
     976The core part of the construction of a structured trace is to use the
     977proof of termination from the measurable trace (defined on
    964978page~\pageref{prog:terminationproof}) to `fold up' the execution into
    965 the nested form.
    967 TODO: design, basic structure from termination proof, how cost
    968 labelling props are baked in; unrepeating PCs, remainder of sound
    969 labellings; coinductive version for whole programs, reason/relevance,
    970 use of em (maybe a general comment about uses of classical reasoning
    971 in development)
     979the nested form.  The results outlined above fill in the proof
     980obligations for the cost labelling properties and the stack
     981preservation result shows that calls return to the correct location.
     983The structured trace alone is not sufficient to capture the property
     984that the program is soundly labelled.  While the structured trace
     985guarantees termination, it still permits a loop to be executed a
     986finite number of times without encountering a cost label.  We
     987eliminate this by proving that no `program counter' repeats within any
     988\lstinline'trace_any_label' section by showing that it is incompatible
     989with the property that there is a bound on the number of successor
     990instructions you can follow in the CFG before you encounter a cost
     993\subsubsection{Whole program structured traces}
     995The development of the construction above started relatively early,
     996before the measurable subtraces preservation proofs.  To be confident
     997that the traces were well-formed, we also developed a whole program
     998form that embeds the traces above.  This includes non-terminating
     999programs, where an infinite number of the terminating structured
     1000traces are embedded.  This construction confirmed that our definition
     1001of structured traces was consistent, although we later found that we
     1002did not require them for the compiler correctness results.
     1004To construct these we need to know whether each function call will
     1005eventually terminate, requiring the use of the excluded middle.  This
     1006classical reasoning is local to the construction of whole program
     1007traces and is not necessary for our main results.
Note: See TracChangeset for help on using the changeset viewer.