Changeset 3203 for Deliverables/D3.4/Report/report.tex

Timestamp:

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

Author:

campbell

Message:

Text on structured trace construction.

File:

• Deliverables/D3.4/Report/report.tex (modified) (1 diff)

Deliverables/D3.4/Report/report.tex

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