source: Papers/structured-traces-2012/structured-traces.tex @ 2455

Last change on this file since 2455 was 2455, checked in by campbell, 7 years ago

Dump rough notes on RTLabs structured traces existence proof.

File size: 7.6 KB
Line 
1\documentclass[a4paper, 10pt]{article}
2
3\usepackage[english]{babel}
4\usepackage[colorlinks]{hyperref}
5\usepackage{microtype}
6
7\author{Brian Campbell, Dominic P. Mulligan, Claudio Sacerdoti Coen,\\Ian Stark and Paolo Tranquilli}
8\title{Structured traces}
9\date{}
10
11\begin{document}
12
13\maketitle
14
15\begin{abstract}
16\end{abstract}
17
18%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
19% Section.                                                                    %
20%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
21\section{Introduction}
22\label{sect.introduction}
23
24Compiler correctness proofs are typically based on simulation results for local
25portions of code.  This is because compiler formalisation efforts have focussed
26their attention on providing guarantees about the extensional behaviour of
27generated code.  In contrast, we have found that invariants about the
28structure of program execution are valuable when the compiler also provides
29guarantees about intensional properties of generated code, such as execution
30time.
31
32Our compiler produces assembly code as output.   The structure of assembly program
33execution is unconstrained.  For example, an arbitrary assembly program is free
34to modify the call stack in any way that it
35chooses.  As a result, we cannot assume that the execution path of an assembly
36function call will return to the subsequent instruction after the call is
37complete. This freedom presents a problem when trying to prove that the
38execution costs of a program are correctly predicted by our compiler. Fortunately, we
39are able to preserve information from earlier stages of the compilation chain
40and use this information in the cost preservation proof.  This information is
41passed in the form of a \emph{structured trace}, a novel enrichment of
42execution traces with invariants about the structure of the program.
43
44
45
46%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
47% Section.                                                                    %
48%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
49\section{Body of paper that is complex}
50\label{sect.body}
51
52%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
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%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
150% Section.                                                                    %
151%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
152\section{Conclusion}
153\label{sect.conclusion}
154
155\end{document}
Note: See TracBrowser for help on using the repository browser.