Changeset 3203 for Deliverables/D3.4/Report/report.tex
- Timestamp:
- Apr 29, 2013, 12:39:45 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.4/Report/report.tex
r3191 r3203 960 960 \subsection{Construction} 961 961 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 962 The construction of the structured trace replaces syntactic cost 963 labelling properties which place requirements on where labels appear 964 in the program, with semantics properties that constrain the execution 965 traces of the program. The construction begins by defining versions 966 of the sound and precise labelling properties on the program text that 967 appears in states rather than programs, and showing that these are 968 preserved by steps of the \textsf{RTLabs} semantics. 969 970 Then we show that each cost labelling property the structured traces 971 definition requires is satisfied. These are broken up by the 972 classification of states. Similarly, we prove a step-by-step stack 973 preservation result, which states that the \textsf{RTLabs} semantics 974 never changes the lower parts of the stack. 975 976 The core part of the construction of a structured trace is to use the 977 proof of termination from the measurable trace (defined on 964 978 page~\pageref{prog:terminationproof}) to `fold up' the execution into 965 the nested form. 966 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) 979 the nested form. The results outlined above fill in the proof 980 obligations for the cost labelling properties and the stack 981 preservation result shows that calls return to the correct location. 982 983 The structured trace alone is not sufficient to capture the property 984 that the program is soundly labelled. While the structured trace 985 guarantees termination, it still permits a loop to be executed a 986 finite number of times without encountering a cost label. We 987 eliminate this by proving that no `program counter' repeats within any 988 \lstinline'trace_any_label' section by showing that it is incompatible 989 with the property that there is a bound on the number of successor 990 instructions you can follow in the CFG before you encounter a cost 991 label. 992 993 \subsubsection{Whole program structured traces} 994 995 The development of the construction above started relatively early, 996 before the measurable subtraces preservation proofs. To be confident 997 that the traces were well-formed, we also developed a whole program 998 form that embeds the traces above. This includes non-terminating 999 programs, where an infinite number of the terminating structured 1000 traces are embedded. This construction confirmed that our definition 1001 of structured traces was consistent, although we later found that we 1002 did not require them for the compiler correctness results. 1003 1004 To construct these we need to know whether each function call will 1005 eventually terminate, requiring the use of the excluded middle. This 1006 classical reasoning is local to the construction of whole program 1007 traces and is not necessary for our main results. 972 1008 973 1009 \section{Conclusion}
Note: See TracChangeset
for help on using the changeset viewer.