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

Last change on this file since 2479 was 2479, checked in by mulligan, 7 years ago

A small amount of rewriting as i didn't like the original introduction that we developed in Edinburgh.

File size: 8.2 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 portions of code.
25This is because compiler formalisation efforts have focused their attention on providing guarantees about the extensional behaviour of generated code.
26In contrast, when verified compiler projects also consider the intensional behaviour of generated code such as execution time or space, we have found that invariants about the structure of program execution are particularly valuable.
27
28The ideas summaried in this paper have been developed within the context of the CerCo (`Certified Complexity') project, though by no means are limited in their scope or application to this project.
29CerCo's ultimate aim is to produce a verified C compiler for a large subset of the C programming language.
30Unlike previous compiler verification projects---notably Leroy's CompCert project at \textsc{inria}---CerCo is also concerned with the intensional correctness of our compiler.
31In particular, the CerCo C compiler will lift, in a provably correct way, a cost model induced by the compilation process back to the C-source level.
32
33
34The structure of assembly program
35execution is unconstrained.  For example, an arbitrary assembly program is free
36to modify the call stack in any way that it
37chooses.  As a result, we cannot assume that the execution path of an assembly
38function call will return to the subsequent instruction after the call is
39complete. This freedom presents a problem when trying to prove that the
40execution costs of a program are correctly predicted by our compiler. Fortunately, we
41are able to preserve information from earlier stages of the compilation chain
42and use this information in the cost preservation proof.  This information is
43passed in the form of a \emph{structured trace}, a novel enrichment of
44execution traces with invariants about the structure of the program.
45
46
47
48%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
49% Section.                                                                    %
50%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
51\section{Body of paper that is complex}
52\label{sect.body}
53
54%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
55% Definitions, choices, etc                                                   %
56%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
57\section{Definition of structured traces}
58\label{sect.defn}
59
60TODO: abstraction of intermediate language semantics, definition of structured
61traces, commentary on decisions made, pretty diagrams
62
63%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
64% Edinburgh work on existence of RTLabs str traces                            %
65%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
66\section{Existence of structured traces}
67\label{sect.rtlabs}
68
69%  existence proof details that I think are irrelevant to this paper:
70%  - fn ids are memory block ids rather than the original name
71%  - a shadow stack is maintained because the semantics don't record the fn id
72%  - we first go from flat traces made from exec_inf to ones which include
73%    evidence of each step of execution (flat_trace)
74
75% TODO: no I/O in present construction - do we need to do something about that?
76
77[Bit of a braindump for now.]
78
79TODO: choice of language (esp, first to have reasonable PCs),
80restricted use of excluded middle for termination
81
82Currently in the order of the proof, rearrange.
83
84Brief note on abstraction: PCs are fn id / cfg node id pairs (with slight
85variations for call/ret/fin states)
86% fn ids are actually blocks, and there's a shadow stack to record which we
87% are on, but that's not really relevant
88Only statements considered as `jumps' are conditionals (no unconditional jumps
89because we're in a cfg).
90\verb'as_after_return' property is that next caller node and caller fn must be
91preserved.
92
93\verb'will_return' asserts that a prefix of a trace eventually returns, using
94the call/ret/jump/other classification fn.  Will use excluded middle on this
95for deciding termination.  Use length of these as part of termination witness
96for construction fn.
97% lemmas for composing (will_return_prepend), slicing (will_return_remove_call)
98% will_return?
99
100Specifications of cost labelling (???.ma), lift them to runtime notions of
101globalenvs, states, preserved by steps (\verb'well_cost_labelled_state_step').
102Label follows a conditional (\verb'well_cost_labelled_jump'), call
103(semantically, i.e., the first thing in a function is the cost label).
104
105(RTLabs) Stack preservation - essential for \verb'as_after_return' (and more?)
106- as with structured traces it ends with the state \emph{after} the return.
107Like \verb'will_return' do composition, steps (including over calls).  Then
108we extract \verb'as_after_return'.  Note: these proofs are technically fairly
109routine, once we've got the right definitions.
110
111\verb'make_label_return' and it's mutually defined functions
112\verb'make_label_label' and \verb'make_any_label' are the main results for
113finite subtraces.  These consume a prefix of the flat trace (given some
114hypotheses about well labelling) according to a \verb'will_return' structure
115that determines how much is used.  A record is returned containing the end
116state, the remainder of the trace, a proof of stack preservation, and the
117remainder (if any) of the \verb'will_terminates' structure.  The functions
118themselves examine the flat trace, checks for a cost label where they can
119optionally appear and proves the properties embedded in the structured traces
120using the above lemmas.  They are given in a mixed definition/proof script
121style; unusually some of the proofs are partly contained in the definition to
122make full use of dependent pattern matching.
123
124
125Abstract successors from semantics to syntax; rephrase bound on instructions
126from cost spec to bound on (local) steps to label; prove that the bound
127reduces as you would expect (requires \verb'as_after_return'), that sound
128labelled lifted to semantics is preserved by steps.
129
130Construction of whole program traces proceeds using excluded middle on existence
131of a \verb'will_return' structure.  Terminating executions just embed the
132structured trace from \verb'make_label_return', but non-terminating executions
133are built by a cofixpoint which extracts a finite prefix, which is constructed
134in a similar way to \verb'make_label_return', but using the bound on steps to a
135cost label to demonstrate termination and stopping on the next cost label in
136the function, or another non-terminating function call.  (Better to describe
137the idea, then note interesting things about the implementation.)
138
139Both structured traces and flat traces are determined by their start state
140because there's no I/O, so get flattening = original trace.
141
142Also show separate non-repeating property (no repeated PC without a cost label)
143by splitting on whether a repeated state is a cost label - if so it can't
144reappear in the relevant part of the structured trace, if not we break the
145sound labelling property on instructions by finding a loop of successor
146instructions without a cost label.  (Note: this is on instructions, above we
147used a derived version on states.)  Rule out repeated call states by reference
148to the successor instruction.  Applying this throughout the structured trace
149give the \verb'*_sound_unrepeating' properties.
150
151%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
152% Section.                                                                    %
153%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
154\section{Conclusion}
155\label{sect.conclusion}
156
157\end{document}
Note: See TracBrowser for help on using the repository browser.