source: Deliverables/D1.2/CompilerProofOutline/outline.tex @ 1731

Last change on this file since 1731 was 1731, checked in by campbell, 9 years ago

A bit of front-end proof outline.

File size: 17.2 KB
Line 
1\documentclass[a4paper, 10pt]{article}
2
3\usepackage{a4wide}
4\usepackage{amsfonts}
5\usepackage{amsmath}
6\usepackage{amssymb}
7\usepackage[english]{babel}
8\usepackage{color}
9\usepackage{diagrams}
10\usepackage{graphicx}
11\usepackage[colorlinks]{hyperref}
12\usepackage[utf8x]{inputenc}
13\usepackage{listings}
14\usepackage{microtype}
15\usepackage{skull}
16\usepackage{stmaryrd}
17
18\lstdefinelanguage{matita-ocaml} {
19  mathescape=true
20}
21\lstset{
22  language=matita-ocaml,basicstyle=\tt,columns=flexible,breaklines=false,
23  showspaces=false, showstringspaces=false, extendedchars=false,
24  inputencoding=utf8x, tabsize=2
25}
26
27\title{Proof outline for the correctness of the CerCo compiler}
28\date{\today}
29\author{The CerCo team}
30
31\begin{document}
32
33\maketitle
34
35\section{Introduction}
36\label{sect.introduction}
37
38In the last project review of the CerCo project, the project reviewers expressed the opinion that it would be a good idea to attempt to write down some of the statements of the correctness theorems that we intend to prove about the complexity preserving compiler.
39This document provides a very high-level, pen-and-paper sketch of what we view as the best path to completing the correctness proof for the compiler.
40In particular, for every translation between two intermediate languages, in both the front- and back-ends, we identify the key translation steps, and identify some invariants that we view as being important for the correctness proof.
41
42\section{Front-end: Clight to RTLabs}
43
44The front-end of the CerCo compiler consists of several stages:
45
46\begin{center}
47\begin{minipage}{.8\linewidth}
48\begin{tabbing}
49\quad \= $\downarrow$ \quad \= \kill
50\textsf{Clight}\\
51\> $\downarrow$ \> cast removal\\
52\> $\downarrow$ \> add runtime functions\footnote{Following the last project
53meeting we intend to move this transformation to the back-end}\\
54\> $\downarrow$ \> cost labelling\\
55\> $\downarrow$ \> stack variable allocation and control structure
56 simplification\\
57\textsf{Cminor}\\
58\> $\downarrow$ \> generate global variable initialisation code\\
59\> $\downarrow$ \> transform to RTL graph\\
60\textsf{RTLabs}\\
61\> $\downarrow$ \> start of target specific back-end\\
62\>\quad \vdots
63\end{tabbing}
64\end{minipage}
65\end{center}
66
67%Our overall statements of correctness with respect to costs will
68%require a correctly labelled program
69
70There are three layers in most of the proofs proposed:
71\begin{enumerate}
72\item invariants closely tied to the syntax and transformations using
73  dependent types,
74\item a forward simulation proof, and
75\item syntactic proofs about the cost labelling.
76\end{enumerate}
77The first will support both function correctness and allow us to show
78the totality of some of the compiler stages (that is, these stages of
79the compiler cannot fail).  The second provides the main functional
80correctness result, and the last will be crucial for applying
81correctness results about the costings from the back-end.
82
83We will also prove that a suitably labelled RTLabs trace can be turned
84into a \emph{structured trace} which splits the execution trace into
85cost-label-to-cost-label chunks with nested function calls.  This
86structure was identified during work on the correctness of the
87back-end cost analysis as retaining important information about the
88structure of the execution that is difficult to reconstruct later in
89the compiler.
90
91\subsection{Clight Cast removal}
92
93This removes some casts inserted by the parser to make arithmetic
94promotion explicit when they are superfluous (such as
95\lstinline[language=C]'c = (short)((int)a + (int)b);').
96
97The transformation only affects Clight expressions, recursively
98detecting casts that can be safely eliminated.  The semantics provides
99a big-step definition for expression, so we should be able to show a
100lock-step forward simulation using a lemma showing that cast
101elimination does not change the evaluation of expressions.  This lemma
102will follow from a structural induction on the source expression.  We
103have already proved a few of the underlying arithmetic results
104necessary to validate the approach.
105
106\subsection{Clight cost labelling}
107
108This adds cost labels before and after selected statements and
109expressions, and the execution traces ought to be equivalent modulo
110cost labels.  Hence it requires a simple forward simulation with a
111limited amount of stuttering whereever a new cost label is introduced.
112A bound can be given for the amount of stuttering allowed can be given
113based on the statement or continuation to be evaluated next.
114
115We also intend to show three syntactic properties about the cost
116labelling:
117\begin{itemize}
118\item every function starts with a cost label,
119\item every branching instruction is followed by a label (note that
120  exiting a loop is treated as a branch), and
121\item the head of every loop (and any \lstinline'goto' destination) is
122  a cost label.
123\end{itemize}
124These can be shown by structural induction on the source term.
125
126\subsection{Clight to Cminor translation}
127
128\subsection{Cminor global initialisation code}
129
130\subsection{Cminor to RTLabs translation}
131
132\subsection{RTLabs structured trace generation}
133
134\section{The RTLabs to RTL translation}
135\label{sect.rtlabs.rtl.translation}
136
137% dpm: type system and casting load (???)
138We require a map, $\sigma$, between \texttt{Values} of the front-end memory model to lists of \texttt{BEValues} of the back-end memory model:
139
140\begin{displaymath}
141\mathtt{Value} ::= \bot \mid \mathtt{int(size)} \mid \mathtt{float} \mid \mathtt{null} \mid \mathtt{ptr} \quad\stackrel{\sigma}{\longrightarrow}\quad \mathtt{BEValue} ::= \bot \mid \mathtt{byte} \mid \mathtt{int}_i \mid \mathtt{ptr}_i
142\end{displaymath}
143
144We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}.
145
146\begin{displaymath}
147\mathtt{Mem}\ \alpha = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \alpha)
148\end{displaymath}
149
150where
151
152\begin{displaymath}
153\mathtt{Block} ::= \mathtt{Region} \cup \mathtt{ID}
154\end{displaymath}
155
156\begin{displaymath}
157\mathtt{BEMem} = \mathtt{Mem} \mathtt{Value}
158\end{displaymath}
159
160\begin{displaymath}
161\mathtt{Address} = \mathtt{BEValue} \times  \mathtt{BEValue} \\
162\end{displaymath}
163
164\begin{displaymath}
165\mathtt{Mem} = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \mathtt{Cont} \mid \mathtt{Value} \times \mathtt{Size} \mid \mathtt{null})
166\end{displaymath}
167
168\begin{center}
169\begin{picture}(2, 2)
170% picture of sigma mapping memory to memory
171TODO
172\end{picture}
173\end{center}
174
175\begin{displaymath}
176\mathtt{load}\ s\ a\ M = \mathtt{Some}\ v \rightarrow \forall i \leq s.\ \mathtt{load}\ s\ (a + i)\ \sigma(M) = \mathtt{Some}\ v_i
177\end{displaymath}
178
179\begin{displaymath}
180\sigma(\mathtt{store}\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(M)
181\end{displaymath}
182
183\begin{displaymath}
184\begin{array}{rll}
185\mathtt{State} & ::=  & (\mathtt{State} : \mathtt{Frame}^* \times \mathtt{Frame} \\
186               & \mid & \mathtt{Call} : \mathtt{Frame}^* \times \mathtt{Args} \times \mathtt{Return} \times \mathtt{Fun} \\
187               & \mid & \mathtt{Return} : \mathtt{Frame}^* \times \mathtt{Value} \times \mathtt{Return}) \times \mathtt{Mem}
188\end{array}
189\end{displaymath}
190
191\begin{displaymath}
192\mathtt{State} ::= \mathtt{Frame}^* \times \mathtt{PC} \times \mathtt{SP} \times \mathtt{ISP} \times \mathtt{CARRY} \times \mathtt{REGS}
193\end{displaymath}
194
195\begin{displaymath}
196\mathtt{State} \stackrel{\sigma}{\longrightarrow} \mathtt{State}
197\end{displaymath}
198
199\begin{displaymath}
200\sigma(\mathtt{State} (\mathtt{Frame}^* \times \mathtt{Frame})) \longrightarrow ((\sigma(\mathtt{Frame}^*), \sigma(\mathtt{PC}), \sigma(\mathtt{SP}), 0, 0, \sigma(\mathtt{REGS})), \sigma(\mathtt{Mem}))
201\end{displaymath}
202
203\begin{displaymath}
204\sigma(\mathtt{Return}(-)) \longrightarrow \sigma \circ \text{return one step}
205\end{displaymath}
206
207\begin{displaymath}
208\sigma(\mathtt{Call}(-)) \longrightarrow \sigma \circ \text{call one step}
209\end{displaymath}
210
211Return one step commuting diagram:
212
213\begin{displaymath}
214\begin{diagram}
215s & \rTo^{\text{one step of execution}} & s'   \\
216  & \rdTo                             & \dTo \\
217  &                                   & \llbracket s'' \rrbracket
218\end{diagram}
219\end{displaymath}
220
221Call one step commuting diagram:
222
223\begin{displaymath}
224\begin{diagram}
225s & \rTo^{\text{one step of execution}} & s'   \\
226  & \rdTo                             & \dTo \\
227  &                                   & \llbracket s'' \rrbracket
228\end{diagram}
229\end{displaymath}
230
231\begin{displaymath}
232\begin{diagram}
233\mathtt{CALL}(\mathtt{id},\ \mathtt{args},\ \mathtt{dst},\ \mathtt{pc}),\ \mathtt{State}(\mathtt{Frame},\ \mathtt{Frames}) & \rTo & \mathtt{Call}(FINISH ME)
234\end{diagram}
235\end{displaymath}
236
237\begin{displaymath}
238\begin{array}{rcl}
239\mathtt{CALL}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc}) & \longrightarrow & \mathtt{CALL\_ID}(\mathtt{id}, \sigma'(\mathtt{args}), \sigma(\mathtt{dst}), \mathtt{pc}) \\
240\mathtt{RETURN}                                                      & \longrightarrow & \mathtt{RETURN} \\
241\end{array} 
242\end{displaymath}
243
244\begin{displaymath}
245\begin{array}{rcl}
246\sigma & : & \mathtt{register} \rightarrow \mathtt{list\ register} \\
247\sigma' & : & \mathtt{list\ register} \rightarrow \mathtt{list\ register}
248\end{array} 
249\end{displaymath}
250
251\section{The RTL to ERTL translation}
252\label{sect.rtl.ertl.translation}
253
254\begin{displaymath}
255\begin{diagram}
256& & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket & & \\
257& \ldTo^{\text{external}} & & \rdTo^{\text{internal}} & \\
258\skull & & & & \mathtt{regs} = [\mathtt{params}/-] \\
259& & & & \mathtt{sp} = \mathtt{ALLOC} \\
260& & & & \mathtt{PUSH}(\mathtt{carry}, \mathtt{regs}, \mathtt{dst}, \mathtt{return\_addr}), \mathtt{pc}_{0}, \mathtt{regs}, \mathtt{sp} \\
261\end{diagram}
262\end{displaymath}
263
264\begin{align*}
265\llbracket \mathtt{RETURN} \rrbracket \\
266\mathtt{return\_addr} & := \mathtt{top}(\mathtt{stack}) \\
267v*                    & := m(\mathtt{rv\_regs}) \\
268\mathtt{dst}, \mathtt{sp}, \mathtt{carry}, \mathtt{regs} & := \mathtt{pop} \\
269\mathtt{regs}[v* / \mathtt{dst}] \\
270\end{align*}
271
272\begin{displaymath}
273\begin{diagram}
274s    & \rTo^1 & s' & \rTo^1 & s'' \\
275\dTo &        &    & \rdTo  & \dTo \\
276\llbracket s \rrbracket & \rTo(1,3)^1 & & & \llbracket s'' \rrbracket \\ 
277\mathtt{CALL} \\
278\end{diagram}
279\end{displaymath}
280
281\begin{displaymath}
282\begin{diagram}
283s    & \rTo^1 & s' & \rTo^1 & s'' \\
284\dTo &        &    & \rdTo  & \dTo \\
285\  & \rTo(1,3) & & & \ \\
286\mathtt{RETURN} \\
287\end{diagram}
288\end{displaymath}
289
290\begin{displaymath}
291\mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist'})
292\rightarrow \mathtt{graph} \rightarrow \mathtt{graph}
293\end{displaymath}
294
295\begin{align*}
296\mathtt{theorem} &\ \mathtt{b\_graph\_translate\_ok}: \\
297& \forall  f.\forall G_{i}.\mathtt{let}\ G_{\sigma} := \mathtt{b\_graph\_translate}\ f\ G_{i}\ \mathtt{in} \\
298&       \forall l \in G_{i}.\mathtt{subgraph}\ (f\ l)\ l\ (\mathtt{next}\ l\ G_{i})\ G_{\sigma}
299\end{align*}
300
301\begin{align*}
302\mathtt{lemma} &\ \mathtt{execute\_1\_step\_ok}: \\
303&       \forall s.  \mathtt{let}\ s' := s\ \sigma\ \mathtt{in} \\
304&       \mathtt{let}\ l := pc\ s\ \mathtt{in} \\
305&       s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma
306\end{align*}
307
308\begin{align*}
309\mathrm{RTL\ status} & \ \ \mathrm{ERTL\ status} \\
310\mathtt{sp} & = \mathtt{spl} / \mathtt{sph} \\
311\mathtt{graph} & \mapsto \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\
312& \mathrm{where}\ s = \mathrm{callee\ saved} + \nu \mathrm{RA} \\
313\end{align*}
314
315\begin{displaymath}
316\begin{diagram}
317\mathtt{CALL} & \rTo^1 & \mathtt{inside\ function} \\
318\dTo & & \dTo \\
319\underbrace{\ldots}_{\llbracket \mathtt{CALL} \rrbracket} & \rTo &
320\underbrace{\ldots}_{\mathtt{prologue}} \\
321\end{diagram}
322\end{displaymath}
323
324\begin{displaymath}
325\begin{diagram}
326\mathtt{RETURN} & \rTo^1 & \mathtt{.} \\
327\dTo & & \dTo \\
328\underbrace{\ldots}_{\mathtt{epilogue}} & \rTo &
329\underbrace{\ldots} \\
330\end{diagram}
331\end{displaymath}
332
333\begin{align*}
334\mathtt{prologue}(s) = & \mathtt{create\_new\_frame}; \\
335                       & \mathtt{pop\ ra}; \\
336                       & \mathtt{save\ callee\_saved}; \\
337                                                                                         & \mathtt{get\_params} \\
338                                                                                         & \ \ \mathtt{reg\_params}: \mathtt{move} \\
339                                                                                         & \ \ \mathtt{stack\_params}: \mathtt{push}/\mathtt{pop}/\mathtt{move} \\
340\end{align*}
341
342\begin{align*}
343\mathtt{epilogue}(s) = & \mathtt{save\ return\ to\ tmp\ real\ regs}; \\
344                                                                                         & \mathtt{restore\_registers}; \\
345                       & \mathtt{push\ ra}; \\
346                       & \mathtt{delete\_frame}; \\
347                       & \mathtt{save return} \\
348\end{align*}
349
350\begin{displaymath}
351\mathtt{CALL} id \mapsto \mathtt{set\_params}; \mathtt{CALL} id; \mathtt{fetch\_result}
352\end{displaymath}
353
354\section{The ERTL to LTL translation}
355\label{sect.ertl.ltl.translation}
356
357\section{The LTL to LIN translation}
358\label{sect.ltl.lin.translation}
359
360We require a map, $\sigma$, from LTL statuses, where program counters are represented as labels in a graph data structure, to LIN statuses, where program counters are natural numbers:
361\begin{displaymath}
362\mathtt{pc : label} \stackrel{\sigma}{\longrightarrow} \mathbb{N}
363\end{displaymath}
364
365The LTL to LIN translation pass also linearises the graph data structure into a list of instructions.
366Pseudocode for the linearisation process is as follows:
367
368\begin{lstlisting}
369let rec linearise graph visited required generated todo :=
370  match todo with
371  | l::todo ->
372    if l $\in$ visited then
373      let generated := generated $\cup\ \{$ Goto l $\}$ in
374      let required := required $\cup$ l in
375        linearise graph visited required generated todo
376    else
377      -- Get the instruction at label `l' in the graph
378      let lookup := graph(l) in
379      let generated := generated $\cup\ \{$ lookup $\}$ in
380      -- Find the successor of the instruction at label `l' in the graph
381      let successor := succ(l, graph) in
382      let todo := successor::todo in
383        linearise graph visited required generated todo
384  | []      -> (required, generated)
385\end{lstlisting}
386
387It is easy to see that this linearisation process eventually terminates.
388In particular, the size of the visited label set is monotonically increasing, and is bounded above by the size of the graph that we are linearising.
389
390The initial call to \texttt{linearise} sees the \texttt{visited}, \texttt{required} and \texttt{generated} sets set to the empty set, and \texttt{todo} initialized with the singleton list consisting of the entry point of the graph.
391We envisage needing to prove the following invariants on the linearisation function above:
392
393\begin{enumerate}
394\item
395$\mathtt{visited} \approx \mathtt{generated}$, where $\approx$ is \emph{multiset} equality, as \texttt{generated} is a set of instructions where instructions may mention labels multiple times, and \texttt{visited} is a set of labels,
396\item
397$\forall \mathtt{l} \in \mathtt{generated}.\ \mathtt{succ(l,\ graph)} \subseteq \mathtt{required} \cup \mathtt{todo}$,
398\item
399$\mathtt{required} \subseteq \mathtt{visited}$,
400\item
401$\mathtt{visited} \cap \mathtt{todo} = \emptyset$.
402\end{enumerate}
403
404The invariants collectively imply the following properties, crucial to correctness, about the linearisation process:
405
406\begin{enumerate}
407\item
408Every graph node is visited at most once,
409\item
410Every instruction that is generated is generated due to some graph node being visited,
411\item
412The successor instruction of every instruction that has been visited already will eventually be visited too.
413\end{enumerate}
414
415Note, because the LTL to LIN transformation is the first time the program is linearised, we must discover a notion of `well formed program' suitable for linearised forms.
416In particular, we see the notion of well formedness (yet to be formally defined) resting on the following conditions:
417
418\begin{enumerate}
419\item
420For every jump to a label in a linearised program, the target label exists at some point in the program,
421\item
422Each label is unique, appearing only once in the program,
423\item
424The final instruction of a program must be a return.
425\end{enumerate}
426
427We assume that these properties will be easy consequences of the invariants on the linearisation function defined above.
428
429The final condition above is potentially a little opaque, so we explain further.
430First, the only instructions that can reasonably appear in final position at the end of a program are returns or backward jumps, as any other instruction would cause execution to `fall out' of the end of the program (for example, when a function invoked with \texttt{CALL} returns, it returns to the next instruction past the \texttt{CALL} that invoked it).
431However, in LIN, though each function's graph has been linearised, the entire program is not yet fully linearised into a list of instructions, but rather, a list of `functions', each consisting of a linearised body along with other data.
432Each well-formed function must end with a call to \texttt{RET}, and therefore the only correct instruction that can terminate a LIN program is a \texttt{RET} instruction.
433
434\section{The LIN to ASM and ASM to MCS-51 machine code translations}
435\label{sect.lin.asm.translation}
436
437The LIN to ASM translation step is trivial, being almost the identity function.
438The only non-trivial feature of the LIN to ASM translation is that all labels are `named apart' so that there is no chance of freshly generated labels from different namespaces clashing with labels from another namespace.
439
440The ASM to MCS-51 machine code translation step, and the required statements of correctness, are found in an unpublished manuscript attached to this document.
441
442\end{document}
Note: See TracBrowser for help on using the repository browser.