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

Last change on this file since 1761 was 1761, checked in by sacerdot, 8 years ago

...

File size: 46.3 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\usepackage{array}
18\newcolumntype{b}{@{}>{{}}}
19\newcolumntype{B}{@{}>{{}}c<{{}}@{}}
20\newcolumntype{h}[1]{@{\hspace{#1}}}
21\newcolumntype{L}{>{$}l<{$}}
22\newcolumntype{C}{>{$}c<{$}}
23\newcolumntype{R}{>{$}r<{$}}
24\newcolumntype{S}{>{$(}r<{)$}}
25\newcolumntype{n}{@{}}
26\usepackage{wasysym}
27
28
29\lstdefinelanguage{matita-ocaml} {
30  mathescape=true
31}
32\lstset{
33  language=matita-ocaml,basicstyle=\tt,columns=flexible,breaklines=false,
34  showspaces=false, showstringspaces=false, extendedchars=false,
35  inputencoding=utf8x, tabsize=2
36}
37
38\title{Proof outline for the correctness of the CerCo compiler}
39\date{\today}
40\author{The CerCo team}
41
42\begin{document}
43
44\maketitle
45
46\section{Introduction}
47\label{sect.introduction}
48
49In the last project review of the CerCo project, the project reviewers
50recommended us to quickly outline a paper-and-pencil correctness proof
51for each of the stages of the CerCo compiler in order to allow for an
52estimation of the complexity and time required to complete the formalization
53of the proof. This has been possible starting from month 18 when we have
54completed the formalization in Matita of the datastructures and code of
55the compiler.
56
57In this document we provide a very high-level, pen-and-paper
58sketch of what we view as the best path to completing the correctness proof
59for the compiler. In 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.  We sketch the overall correctness results, and also briefly describe the parts of the proof that have already
60been completed at the end of the First Period.
61
62In the last section we finally present an estimation of the effort required
63for the certification in Matita of the compiler and we draw conclusions.
64
65\section{Front-end: Clight to RTLabs}
66
67The front-end of the CerCo compiler consists of several stages:
68
69\begin{center}
70\begin{minipage}{.8\linewidth}
71\begin{tabbing}
72\quad \= $\downarrow$ \quad \= \kill
73\textsf{Clight}\\
74\> $\downarrow$ \> cast removal\\
75\> $\downarrow$ \> add runtime functions\footnote{Following the last project
76meeting we intend to move this transformation to the back-end}\\
77\> $\downarrow$ \> cost labelling\\
78\> $\downarrow$ \> loop optimizations\footnote{\label{lab:opt2}To be ported from the untrusted compiler and certified only in case of early completion of the certification of the other passes.} (an endo-transformation)\\
79\> $\downarrow$ \> partial redundancy elimination$^{\mbox{\scriptsize \ref{lab:opt2}}}$ (an endo-transformation)\\
80\> $\downarrow$ \> stack variable allocation and control structure
81 simplification\\
82\textsf{Cminor}\\
83\> $\downarrow$ \> generate global variable initialisation code\\
84\> $\downarrow$ \> transform to RTL graph\\
85\textsf{RTLabs}\\
86\> $\downarrow$ \> \\
87\>\,\vdots
88\end{tabbing}
89\end{minipage}
90\end{center}
91
92Here, by `endo-transformation', we mean a mapping from language back to itself:
93the loop optimization step maps the Clight language to itself.
94
95%Our overall statements of correctness with respect to costs will
96%require a correctly labelled program
97There are three layers in most of the proofs proposed:
98\begin{enumerate}
99\item invariants closely tied to the syntax and transformations using
100  dependent types (such as the presence of variable names in environments),
101\item a forward simulation proof relating each small-step of the
102  source to zero or more steps of the target, and
103\item proofs about syntactic properties of the cost labelling.
104\end{enumerate}
105The first will support both functional correctness and allow us to
106show the totality of some of the compiler stages (that is, those
107stages of the compiler cannot fail).  The second provides the main
108functional correctness result, including the preservation of cost
109labels in the traces, and the last will be crucial for applying
110correctness results about the costings from the back-end by showing
111that they appear in enough places so that we can assign all of the
112execution costs to them.
113
114We will also prove that a suitably labelled RTLabs trace can be turned
115into a \emph{structured trace} which splits the execution trace into
116cost-label to cost-label chunks with nested function calls.  This
117structure was identified during work on the correctness of the
118back-end cost analysis as retaining important information about the
119structure of the execution that is difficult to reconstruct later in
120the compiler.
121
122\subsection{Clight cast removal}
123
124This transformation removes some casts inserted by the parser to make
125arithmetic promotion explicit but which are superfluous (such as
126\lstinline[language=C]'c = (short)((int)a + (int)b);' where
127\lstinline'a' and \lstinline'b' are \lstinline[language=C]'short').
128This is necessary for producing good code for our target architecture.
129
130It only affects Clight expressions, recursively detecting casts that
131can be safely eliminated.  The semantics provides a big-step
132definition for expression, so we should be able to show a lock-step
133forward simulation between otherwise identical states using a lemma
134showing that cast elimination does not change the evaluation of
135expressions.  This lemma will follow from a structural induction on
136the source expression.  We have already proved a few of the underlying
137arithmetic results necessary to validate the approach.
138
139\subsection{Clight cost labelling}
140
141This adds cost labels before and after selected statements and
142expressions, and the execution traces ought to be equivalent modulo
143the new cost labels.  Hence it requires a simple forward simulation
144with a limited amount of stuttering whereever a new cost label is
145introduced.  A bound can be given for the amount of stuttering allowed
146based on the statement or continuation to be evaluated next.
147
148We also intend to show three syntactic properties about the cost
149labelling:
150\begin{enumerate}
151\item every function starts with a cost label,
152\item every branching instruction is followed by a cost label (note that
153  exiting a loop is treated as a branch), and
154\item the head of every loop (and any \lstinline'goto' destination) is
155  a cost label.
156\end{enumerate}
157These can be shown by structural induction on the source term.
158
159\subsection{Clight to Cminor translation}
160
161This translation is the first to introduce some invariants, with the
162proofs closely tied to the implementation by dependent typing.  These
163are largely complete and show that the generated code enjoys:
164\begin{itemize}
165\item some minimal type safety shown by explicit checks on the
166  Cminor types during the transformation (a little more work remains
167  to be done here, but follows the same form);
168\item that variables named in the parameter and local variable
169  environments are distinct from one another, again by an explicit
170  check;
171\item that variables used in the generated code are present in the
172  resulting environment (either by checking their presence in the
173  source environment, or from a list of freshly generated temporary variables);
174  and
175\item that all \lstinline[language=C]'goto' labels are present (by
176  checking them against a list of source labels and proving that all
177  source labels are preserved).
178\end{itemize}
179
180The simulation will be similar to the relevant stages of CompCert
181(Clight to Csharpminor and Csharpminor to Cminor --- in the event that
182the direct proof is unwieldy we could introduce an intermediate
183language corresponding to Csharpminor).  During early experimentation
184with porting CompCert definitions to the Matita proof assistant we
185found little difficulty reproving the results for the memory model, so
186we plan to port the memory injection properties and use them to relate
187Clight in-memory variables with either the value of the local variable or a
188stack slot, depending on how it was classified.
189
190This should be sufficient to show the equivalence of (big-step)
191expression evaluation.  The simulation can then be shown by relating
192corresponding blocks of statement and continuations with their Cminor
193counterparts and proving that a few steps reaches the next matching
194state.
195
196The syntactic properties required for cost labels remain similar and a
197structural induction on the function bodies should be sufficient to
198show that they are preserved.
199
200\subsection{Cminor global initialisation code}
201
202This short phase replaces the global variable initialisation data with
203code that executes when the program starts.  Each piece of
204initialisation data in the source is matched by a new statement
205storing that data.  As each global variable is allocated a distinct
206memory block, the program state after the initialisation statements
207will be the same as the original program's state at the start of
208execution, and will proceed in the same manner afterwards.
209
210% Actually, the above is wrong...
211% ... this ought to be in a fresh main function with a fresh cost label
212
213\subsection{Cminor to RTLabs translation}
214
215In this part of the compiler we transform the program's functions into
216control flow graphs.  It is closely related to CompCert's Cminorsel to
217RTL transformation, albeit with target-independent operations.
218
219We already enforce several invariants with dependent types: some type
220safety, mostly shown using the type information from Cminor; and
221that the graph is closed (by showing that each successor was recently
222added, or corresponds to a \lstinline[language=C]'goto' label which
223are all added before the end).  Note that this relies on a
224monotonicity property; CompCert maintains a similar property in a
225similar way while building RTL graphs.  We will also add a result
226showing that all of the pseudo-register names are distinct for use by
227later stages using the same method as Cminor.
228
229The simulation will relate Cminor states to RTLabs states which are about to
230execute the code corresponding to the Cminor statement or continuation.
231Each Cminor statement becomes zero or more RTLabs statements, with a
232decreasing measure based on the statement and continuations similar to
233CompCert's.  We may also follow CompCert in using a relational
234specification of this stage so as to abstract away from the functional
235(and highly dependently typed) definition.
236
237The first two labelling properties remain as before; we will show that
238cost labels are preserved, so the function entry point will be a cost
239label, and successors to any statement that are cost labels map still
240map to cost labels, preserving the condition on branches.  We replace
241the property for loops with the notion that we will always reach a
242cost label or the end of the function after following a bounded number of
243successors.  This can be easily seen in Cminor using the requirement
244for cost labels at the head of loops and after gotos.  It remains to
245show that this is preserved by the translation to RTLabs.  % how?
246
247\subsection{RTLabs structured trace generation}
248
249This proof-only step incorporates the function call structure and cost
250labelling properties into the execution trace.  As the function calls
251are nested within the trace, we need to distinguish between
252terminating and non-terminating function calls.  Thus we use the
253excluded middle (specialised to a function termination property) to do
254this.
255
256Structured traces for terminating functions are built by following the
257flat trace, breaking it into chunks between cost labels and
258recursively processing function calls.  The main difficulties here are
259the non-structurally recursive nature of the function (instead we use
260the size of the termination proof as a measure) and using the RTLabs
261cost labelling properties to show that the constraints of the
262structured traces are observed.  We also show that the lower stack
263frames are preserved during function calls in order to prove that
264after returning from a function call we resume execution of the
265correct code.  This part of the work has already been constructed, but
266still requires a simple proof to show that flattening the structured
267trace recreates the original flat trace.
268
269The non-terminating case follows the trace like the terminating
270version to build up chunks of trace from cost-label to cost-label
271(which, by the finite distance to a cost label property shown before,
272can be represented by an inductive type).  These chunks are chained
273together in a coinductive data structure that can represent
274non-terminating traces.  The excluded middle is used to decide whether
275function calls terminate, in which case the function described above
276constructs an inductive terminating structured trace which is nested
277in the caller's trace.  Otherwise, another coinductive constructor is
278used to embed the non-terminating trace of the callee, generated by
279corecursion.  This part of the trace transformation is currently under
280construction, and will also need a flattening result to show that it
281is correct.
282
283
284\section{Backend: RTLabs to machine code}
285\label{sect.backend.rtlabs.machine.code}
286
287The compiler backend consists of the following intermediate languages, and stages of translation:
288
289\begin{center}
290\begin{minipage}{.8\linewidth}
291\begin{tabbing}
292\quad \=\,\vdots\= \\
293\> $\downarrow$ \>\\
294\> $\downarrow$ \quad \= \kill
295\textsf{RTLabs}\\
296\> $\downarrow$ \> copy propagation\footnote{\label{lab:opt}To be ported from the untrusted compiler and certified only in case of early completion of the certification of the other passes.} (an endo-transformation) \\
297\> $\downarrow$ \> instruction selection\\
298\> $\downarrow$ \> change of memory models in compiler\\
299\textsf{RTL}\\
300\> $\downarrow$ \> constant propagation$^{\mbox{\scriptsize \ref{lab:opt}}}$ (an endo-transformation) \\
301\> $\downarrow$ \> calling convention made explicit \\
302\> $\downarrow$ \> layout of activation records \\
303\textsf{ERTL}\\
304\> $\downarrow$ \> register allocation and spilling\\
305\> $\downarrow$ \> dead code elimination\\
306\textsf{LTL}\\
307\> $\downarrow$ \> function linearisation\\
308\> $\downarrow$ \> branch compression (an endo-transformation) \\
309\textsf{LIN}\\
310\> $\downarrow$ \> relabeling\\
311\textsf{ASM}\\
312\> $\downarrow$ \> pseudoinstruction expansion\\
313\textsf{MCS-51 machine code}\\
314\end{tabbing}
315\end{minipage}
316\end{center}
317
318\subsection{The RTLabs to RTL translation}
319\label{subsect.rtlabs.rtl.translation}
320
321The RTLabs to RTL translation pass marks the frontier between the two memory models used in the CerCo project.
322As a result, we require some method of translating between the values that the two memory models permit.
323Suppose we have such a translation, $\sigma$.
324Then the translation between values of the two memory models may be pictured with:
325
326\begin{displaymath}
327\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{null}_i \mid \mathtt{ptr}_i
328\end{displaymath}
329
330In the front-end, we have both integer and float values, where integer values are `sized', along with null values and pointers. Some frontenv values are
331representables in a byte, but some others require more bits.
332
333In the back-end model all values are meant to be represented in a single byte.
334Values can thefore be undefined, be one byte long integers or be indexed
335fragments of a pointer, null or not. Floats values are no longer present, as floating point arithmetic is not supported by the CerCo compiler.
336
337The $\sigma$ map implements a one-to-many relation: a single front-end value
338is mapped to a sequence of back-end values when its size is more then one byte.
339
340We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}. Both kinds of memory can be
341thought as an instance of a generic \texttt{Mem} data type parameterized over
342the kind of values stored in memory.
343
344\begin{displaymath}
345\mathtt{Mem}\ \alpha = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \alpha)
346\end{displaymath}
347
348Here, \texttt{Block} consists of a \texttt{Region} paired with an identifier.
349
350\begin{displaymath}
351\mathtt{Block} ::= \mathtt{Region} \times \mathtt{ID}
352\end{displaymath}
353
354We now have what we need for defining what is meant by the `memory' in the backend memory model.
355Namely, we instantiate the previously defined \texttt{Mem} type with the type of back-end memory values.
356
357\begin{displaymath}
358\mathtt{BEMem} = \mathtt{Mem} \mathtt{BEValue}
359\end{displaymath}
360
361Memory addresses consist of a pair of back-end memory values:
362
363\begin{displaymath}
364\mathtt{Address} = \mathtt{BEValue} \times  \mathtt{BEValue} \\
365\end{displaymath}
366
367The back- and front-end memory models differ in how they represent sized integeer values in memory.
368In particular, the front-end stores integer values as a header, with size information, followed by a string of `continuation' blocks, marking out the full representation of the value in memory.
369In contrast, the layout of sized integer values in the back-end memory model consists of a series of byte-sized `chunks':
370
371\begin{center}
372\begin{picture}(0, 25)
373\put(-125,0){\framebox(25,25)[c]{\texttt{v,4}}}
374\put(-100,0){\framebox(25,25)[c]{\texttt{cont}}}
375\put(-75,0){\framebox(25,25)[c]{\texttt{cont}}}
376\put(-50,0){\framebox(25,25)[c]{\texttt{cont}}}
377\put(-15,10){\vector(1, 0){30}}
378\put(25,0){\framebox(25,25)[c]{\texttt{\texttt{v$_1$}}}}
379\put(50,0){\framebox(25,25)[c]{\texttt{\texttt{v$_2$}}}}
380\put(75,0){\framebox(25,25)[c]{\texttt{\texttt{v$_3$}}}}
381\put(100,0){\framebox(25,25)[c]{\texttt{\texttt{v$_4$}}}}
382\end{picture}
383\end{center}
384
385Chunks for pointers are pairs made of the original pointer and the index of the chunk.
386Therefore, when assembling the chunks together, we can always recognize if all chunks refer to the same value or if the operation is meaningless.
387
388The differing memory representations of values in the two memory models imply the need for a series of lemmas on the actions of \texttt{load} and \texttt{store} to ensure correctness.
389The first lemma required has the following statement:
390\begin{displaymath}
391\mathtt{load}\ s\ a\ M = \mathtt{Some}\ v \rightarrow \forall i \leq s.\ \mathtt{load}\ s\ (a + i)\ \sigma(M) = \mathtt{Some}\ v_i
392\end{displaymath}
393That is, if we are successful in reading a value of size $s$ from memory at address $a$ in front-end memory, then we should successfully be able to read a value from memory in the back-end memory at \emph{any} address from address $a$ up to and including address $a + i$, where $i \leq s$.
394
395Next, we must show that \texttt{store} properly commutes with the $\sigma$-map between memory spaces:
396\begin{displaymath}
397\sigma(\mathtt{store}\ a\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(a)\ \sigma(M)
398\end{displaymath}
399That is, if we store a value \texttt{v} in the front-end memory \texttt{M} at address \texttt{a} and transform the resulting memory with $\sigma$, then this is equivalent to storing a transformed value $\mathtt{\sigma(v)}$ at address $\mathtt{\sigma(a)}$ into the back-end memory $\mathtt{\sigma(M)}$.
400
401Finally, we must prove that \texttt{load}, \texttt{store} and $\sigma$ all properly commute.
402Writing \texttt{load}$^*$ for multiple consecutive iterations of \texttt{load}, we must prove:
403\begin{displaymath}
404\texttt{load}^* (\mathtt{store}\ \sigma(a')\ \sigma(v)\ \sigma(M))\ \sigma(a)\ \sigma(M) = \mathtt{load}^*\ \sigma(s)\ \sigma(a)\ \sigma(M)
405\end{displaymath}
406That is, suppose we store a transformed value $\mathtt{\sigma(v)}$ into a back-end memory $\mathtt{\sigma(M)}$ at address $\mathtt{\sigma(a')}$, using \texttt{store}, and then load the correct number of bytes (for the size of $\mathtt{\sigma(v)}$ at address $\sigma(a)$.
407Then, this should be equivalent to loading the correct number of bytes from address $\sigma(a)$ in an unaltered version of $\mathtt{\sigma(M)}$, \emph{providing} that the memory regions occupied by the two sequences of bytes at the two addresses do not overlap.
408This will entail more proof obligations, demonstrating that the $\sigma$-map between memory spaces respects memory regions.
409
410\begin{displaymath}
411\begin{array}{rll}
412\mathtt{State} & ::=  & (\mathtt{State} : \mathtt{Frame}^* \times \mathtt{Frame} \\
413               & \mid & \mathtt{Call} : \mathtt{Frame}^* \times \mathtt{Args} \times \mathtt{Return} \times \mathtt{Fun} \\
414               & \mid & \mathtt{Return} : \mathtt{Frame}^* \times \mathtt{Value} \times \mathtt{Return}) \times \mathtt{Mem}
415\end{array}
416\end{displaymath}
417
418\begin{displaymath}
419\mathtt{State} ::= \mathtt{Frame}^* \times \mathtt{PC} \times \mathtt{SP} \times \mathtt{ISP} \times \mathtt{CARRY} \times \mathtt{REGS}
420\end{displaymath}
421
422\begin{displaymath}
423\mathtt{State} \stackrel{\sigma}{\longrightarrow} \mathtt{State}
424\end{displaymath}
425
426\begin{displaymath}
427\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}))
428\end{displaymath}
429
430\begin{displaymath}
431\sigma(\mathtt{Return}(-)) \longrightarrow \sigma \circ \text{return one step}
432\end{displaymath}
433
434\begin{displaymath}
435\sigma(\mathtt{Call}(-)) \longrightarrow \sigma \circ \text{call one step}
436\end{displaymath}
437
438Return one step commuting diagram:
439
440\begin{displaymath}
441\begin{diagram}
442s & \rTo^{\text{one step of execution}} & s'   \\
443  & \rdTo                             & \dTo \\
444  &                                   & \llbracket s'' \rrbracket
445\end{diagram}
446\end{displaymath}
447
448Call one step commuting diagram:
449
450\begin{displaymath}
451\begin{diagram}
452s & \rTo^{\text{one step of execution}} & s'   \\
453  & \rdTo                             & \dTo \\
454  &                                   & \llbracket s'' \rrbracket
455\end{diagram}
456\end{displaymath}
457
458\begin{displaymath}
459\begin{array}{rcl}
460\mathtt{Call(id,\ args,\ dst,\ pc),\ State(FRAME, FRAMES)} & \longrightarrow & \mathtt{Call(M(args), dst)}, \\
461                                                           &                 & \mathtt{PUSH(current\_frame[PC := after\_return])}
462\end{array}
463\end{displaymath}
464
465In the case where the call is to an external function, we have:
466
467\begin{displaymath}
468\begin{array}{rcl}
469\mathtt{Call(M(args), dst)},                       & \stackrel{\mathtt{ret\_val = f(M(args))}}{\longrightarrow} & \mathtt{Return(ret\_val,\ dst,\ PUSH(...))} \\
470\mathtt{PUSH(current\_frame[PC := after\_return])} &                                                            & 
471\end{array}
472\end{displaymath}
473
474then:
475
476\begin{displaymath}
477\begin{array}{rcl}
478\mathtt{Return(ret\_val,\ dst,\ PUSH(...))} & \longrightarrow & \mathtt{pc = POP\_STACK(regs[dst := M(ret\_val)],\ pc)}
479\end{array}
480\end{displaymath}
481
482In the case where the call is to an internal function, we have:
483
484\begin{displaymath}
485\begin{array}{rcl}
486\mathtt{CALL}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc}) & \longrightarrow & \mathtt{CALL\_ID}(\mathtt{id}, \sigma'(\mathtt{args}), \sigma(\mathtt{dst}), \mathtt{pc}) \\
487\mathtt{RETURN}                                                      & \longrightarrow & \mathtt{RETURN} \\
488\end{array} 
489\end{displaymath}
490
491\begin{displaymath}
492\begin{array}{rcl}
493\mathtt{Call(M(args), dst)}                        & \longrightarrow & \mathtt{sp = alloc}, regs = \emptyset[- := PARAMS] \\
494\mathtt{PUSH(current\_frame[PC := after\_return])} &                 & \mathtt{State}(regs,\ sp,\ pc_\emptyset,\ dst)
495\end{array}
496\end{displaymath}
497
498then:
499
500\begin{displaymath}
501\begin{array}{rcl}
502\mathtt{sp = alloc}, regs = \emptyset[- := PARAMS] & \longrightarrow & \mathtt{free(sp)} \\
503\mathtt{State}(regs,\ sp,\ pc_\emptyset,\ dst)     &                 & \mathtt{Return(M(ret\_val), dst, frames)}
504\end{array}
505\end{displaymath}
506
507and finally:
508
509\begin{displaymath}
510\begin{array}{rcl}
511\mathtt{free(sp)}                         & \longrightarrow & \mathtt{pc = POP\_STACK(regs[dst := M(ret\_val)],\ pc)} \\
512\mathtt{Return(M(ret\_val), dst, frames)} &                 & 
513\end{array}
514\end{displaymath}
515
516\begin{displaymath}
517\begin{array}{rcl}
518\sigma & : & \mathtt{register} \rightarrow \mathtt{list\ register} \\
519\sigma' & : & \mathtt{list\ register} \rightarrow \mathtt{list\ register}
520\end{array}
521\end{displaymath}
522
523\subsection{The RTL to ERTL translation}
524\label{subsect.rtl.ertl.translation}
525
526\begin{displaymath}
527\begin{diagram}
528& & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket & & \\
529& \ldTo^{\text{external}} & & \rdTo^{\text{internal}} & \\
530\skull & & & & \mathtt{regs} = [\mathtt{params}/-] \\
531& & & & \mathtt{sp} = \mathtt{ALLOC} \\
532& & & & \mathtt{PUSH}(\mathtt{carry}, \mathtt{regs}, \mathtt{dst}, \mathtt{return\_addr}), \mathtt{pc}_{0}, \mathtt{regs}, \mathtt{sp} \\
533\end{diagram}
534\end{displaymath}
535
536\begin{align*}
537\llbracket \mathtt{RETURN} \rrbracket \\
538\mathtt{return\_addr} & := \mathtt{top}(\mathtt{stack}) \\
539v*                    & := m(\mathtt{rv\_regs}) \\
540\mathtt{dst}, \mathtt{sp}, \mathtt{carry}, \mathtt{regs} & := \mathtt{pop} \\
541\mathtt{regs}[v* / \mathtt{dst}] \\
542\end{align*}
543
544\begin{displaymath}
545\begin{diagram}
546s    & \rTo^1 & s' & \rTo^1 & s'' \\
547\dTo &        &    & \rdTo  & \dTo \\
548\llbracket s \rrbracket & \rTo(1,3)^1 & & & \llbracket s'' \rrbracket \\ 
549\mathtt{CALL} \\
550\end{diagram}
551\end{displaymath}
552
553\begin{displaymath}
554\begin{diagram}
555s    & \rTo^1 & s' & \rTo^1 & s'' \\
556\dTo &        &    & \rdTo  & \dTo \\
557\  & \rTo(1,3) & & & \ \\
558\mathtt{RETURN} \\
559\end{diagram}
560\end{displaymath}
561
562\begin{displaymath}
563\mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist'})
564\rightarrow \mathtt{graph} \rightarrow \mathtt{graph}
565\end{displaymath}
566
567\begin{align*}
568\mathtt{theorem} &\ \mathtt{b\_graph\_translate\_ok}: \\
569& \forall  f.\forall G_{i}.\mathtt{let}\ G_{\sigma} := \mathtt{b\_graph\_translate}\ f\ G_{i}\ \mathtt{in} \\
570&       \forall l \in G_{i}.\mathtt{subgraph}\ (f\ l)\ l\ (\mathtt{next}\ l\ G_{i})\ G_{\sigma}
571\end{align*}
572
573\begin{align*}
574\mathtt{lemma} &\ \mathtt{execute\_1\_step\_ok}: \\
575&       \forall s.  \mathtt{let}\ s' := s\ \sigma\ \mathtt{in} \\
576&       \mathtt{let}\ l := pc\ s\ \mathtt{in} \\
577&       s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma
578\end{align*}
579
580\begin{align*}
581\mathrm{RTL\ status} & \ \ \mathrm{ERTL\ status} \\
582\mathtt{sp} & = \mathtt{spl} / \mathtt{sph} \\
583\mathtt{graph} &  \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\
584& \mathrm{where}\ s = \mathrm{callee\ saved} + \nu \mathrm{RA} \\
585\end{align*}
586
587\begin{displaymath}
588\begin{diagram}
589\mathtt{CALL} & \rTo^1 & \mathtt{inside\ function} \\
590\dTo & & \dTo \\
591\underbrace{\ldots}_{\llbracket \mathtt{CALL} \rrbracket} & \rTo &
592\underbrace{\ldots}_{\mathtt{prologue}} \\
593\end{diagram}
594\end{displaymath}
595
596\begin{displaymath}
597\begin{diagram}
598\mathtt{RETURN} & \rTo^1 & \mathtt{.} \\
599\dTo & & \dTo \\
600\underbrace{\ldots}_{\mathtt{epilogue}} & \rTo &
601\underbrace{\ldots} \\
602\end{diagram}
603\end{displaymath}
604
605\begin{align*}
606\mathtt{prologue}(s) = & \mathtt{create\_new\_frame}; \\
607                       & \mathtt{pop\ ra}; \\
608                       & \mathtt{save\ callee\_saved}; \\
609                                                                                         & \mathtt{get\_params} \\
610                                                                                         & \ \ \mathtt{reg\_params}: \mathtt{move} \\
611                                                                                         & \ \ \mathtt{stack\_params}: \mathtt{push}/\mathtt{pop}/\mathtt{move} \\
612\end{align*}
613
614\begin{align*}
615\mathtt{epilogue}(s) = & \mathtt{save\ return\ to\ tmp\ real\ regs}; \\
616                                                                                         & \mathtt{restore\_registers}; \\
617                       & \mathtt{push\ ra}; \\
618                       & \mathtt{delete\_frame}; \\
619                       & \mathtt{save return} \\
620\end{align*}
621
622\begin{displaymath}
623\mathtt{CALL}\ id \mapsto \mathtt{set\_params};\ \mathtt{CALL}\ id;\ \mathtt{fetch\_result}
624\end{displaymath}
625
626\subsection{The ERTL to LTL translation}
627\label{subsect.ertl.ltl.translation}
628\newcommand{\declsf}[1]{\expandafter\newcommand\expandafter{\csname #1\endcsname}{\mathop{\mathsf{#1}}\nolimits}}
629\declsf{Livebefore}
630\declsf{Liveafter}
631\declsf{Defined}
632\declsf{Used}
633\declsf{Eliminable}
634\declsf{StatementSem}
635For the liveness analysis, we aim at a map
636$\ell \in \mathtt{label} \mapsto $ live registers at $\ell$.
637We define the following operators on ERTL statements.
638$$
639\begin{array}{lL>{(ex. $}L<{)$}}
640\Defined(s) & registers defined at $s$ & r_1\leftarrow r_2+r_3 \mapsto \{r_1,C\}, \mathtt{CALL}~id\mapsto \text{caller-save}
641\\
642\Used(s) & registers used at $s$ & r_1\leftarrow r_2+r_3 \mapsto \{r_2,r_3\}, \mathtt{CALL}~id\mapsto \text{parameters}
643\end{array}
644$$
645Given $LA:\mathtt{label}\to\mathtt{lattice}$ (where $\mathtt{lattice}$
646is the type of sets of registers\footnote{More precisely, it is thethe lattice
647of pairs of sets of pseudo-registers and sets of hardware registers,
648with pointwise operations.}, we also have have the following
649predicates:
650$$
651\begin{array}{lL}
652\Eliminable_{LA}(\ell) & iff $s(\ell)$ has side-effects only on $r\notin LA(\ell)$
653\\&
654(ex.\ $\ell : r_1\leftarrow r_2+r_3 \mapsto (\{r_1,C\}\cap LA(\ell)\neq\emptyset,
655  \mathtt{CALL}id\mapsto \text{never}$)
656\\
657\Livebefore_{LA}(\ell) &$:=
658  \begin{cases}
659    LA(\ell) &\text{if $\Eliminable_{LA}(\ell)$,}\\
660    (LA(\ell)\setminus \Defined(s(\ell)))\cup \Used(s(\ell) &\text{otherwise}.
661  \end{cases}$
662\end{array}
663$$
664In particular, $\Livebefore$ has type $(\mathtt{label}\to\mathtt{lattice})\to
665\mathtt{label}\to\mathtt{lattice}$.
666
667The equation on which we build the fixpoint is then
668$$\Liveafter(\ell) \doteq \bigcup_{\ell' >_1 \ell} \Livebefore_{\Liveafter}(\ell')$$
669where $\ell' >_1 \ell$ denotes that $\ell'$ is an immediate successor of $\ell$
670in the graph. We do not require the fixpoint to be the least one, so the hypothesis
671on $\Liveafter$ that we require is
672$$\Liveafter(\ell) \supseteq \bigcup_{\ell' >_1 \ell} \Livebefore(\ell')$$
673(for shortness we drop the subscript from $\Livebefore$).
674\subsection{The LTL to LIN translation}
675\label{subsect.ltl.lin.translation}
676
677We 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:
678\begin{displaymath}
679\mathtt{pc : label} \stackrel{\sigma}{\longrightarrow} \mathbb{N}
680\end{displaymath}
681
682The LTL to LIN translation pass also linearises the graph data structure into a list of instructions.
683Pseudocode for the linearisation process is as follows:
684
685\begin{lstlisting}
686let rec linearise graph visited required generated todo :=
687  match todo with
688  | l::todo ->
689    if l $\in$ visited then
690      let generated := generated $\cup\ \{$ Goto l $\}$ in
691      let required := required $\cup$ l in
692        linearise graph visited required generated todo
693    else
694      -- Get the instruction at label `l' in the graph
695      let lookup := graph(l) in
696      let generated := generated $\cup\ \{$ lookup $\}$ in
697      -- Find the successor of the instruction at label `l' in the graph
698      let successor := succ(l, graph) in
699      let todo := successor::todo in
700        linearise graph visited required generated todo
701  | []      -> (required, generated)
702\end{lstlisting}
703
704It is easy to see that this linearisation process eventually terminates.
705In 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.
706
707The 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.
708We envisage needing to prove the following invariants on the linearisation function above:
709
710\begin{enumerate}
711\item
712$\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,
713\item
714$\forall \mathtt{l} \in \mathtt{generated}.\ \mathtt{succ(l,\ graph)} \subseteq \mathtt{required} \cup \mathtt{todo}$,
715\item
716$\mathtt{required} \subseteq \mathtt{visited}$,
717\item
718$\mathtt{visited} \cap \mathtt{todo} = \emptyset$.
719\end{enumerate}
720
721The invariants collectively imply the following properties, crucial to correctness, about the linearisation process:
722
723\begin{enumerate}
724\item
725Every graph node is visited at most once,
726\item
727Every instruction that is generated is generated due to some graph node being visited,
728\item
729The successor instruction of every instruction that has been visited already will eventually be visited too.
730\end{enumerate}
731
732Note, 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.
733In particular, we see the notion of well formedness (yet to be formally defined) resting on the following conditions:
734
735\begin{enumerate}
736\item
737For every jump to a label in a linearised program, the target label exists at some point in the program,
738\item
739Each label is unique, appearing only once in the program,
740\item
741The final instruction of a program must be a return.
742\end{enumerate}
743
744We assume that these properties will be easy consequences of the invariants on the linearisation function defined above.
745
746The final condition above is potentially a little opaque, so we explain further.
747First, 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).
748However, 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.
749Each 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.
750
751\subsection{The LIN to ASM and ASM to MCS-51 machine code translations}
752\label{subsect.lin.asm.translation}
753
754The LIN to ASM translation step is trivial, being almost the identity function.
755The 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.
756
757The ASM to MCS-51 machine code translation step, and the required statements of correctness, are found in an unpublished manuscript attached to this document.
758This is the most complex translation because of the huge number of cases
759to be addressed and because of the complexity of the two semantics.
760Moreover, in the assembly code we have conditional and unconditional jumps
761to arbitrary locations in the code, which are not supported by the MCS-51
762instruction set. The latter has several kind of jumps characterized by a
763different instruction size and execution time, but limited in range. For
764instance, conditional jumps to locations whose destination is more than
765$2^7$ bytes away from the jump instruction location are not supported at
766all and need to be emulated with a code transformation. The problem, which
767is known in the litterature as branch displacement and that applies also
768to modern architectures, is known to be hard and is often NP. As far as we
769know, we will provide the first formally verified proof of correctness for
770an assembler that implements branch displacement. We are also providing
771the first verified proof of correctness of a mildly optimizing branch
772displacement algorithm that, at the moment, is almost finished, but not
773described in the companion paper. This proof by itself took about 6 men
774months.
775
776\section{Correctness of cost prediction}
777Roughly speaking,
778the proof of correctness of cost prediction shows that the cost of executing
779a labelled object code program is the same as the sum over all labels in the
780program execution trace of the cost statically associated to the label and
781computed on the object code itself.
782
783In presence of object level function calls, the previous statement is, however,
784incorrect. The reason is twofold. First of all, a function call may diverge.
785To the last labels that comes before the call, however, we also associate
786the cost of the instructions that follow the call. Therefore, in the
787sum over all labels, when we meet a label we pre-pay for the instructions
788after function calls, assuming all calls to be terminating. This choice is
789driven by considerations on the source code. Functions can be called also
790inside expressions and it would be too disruptive to put labels inside
791expressions to capture the cost of instructions that follow a call. Moreover,
792adding a label after each call would produce a much higher number of proof
793obligations in the certification of source programs using Frama-C. The
794proof obligations, moreover, would be guarded by termination of all functions
795involved, that also generates lots of additional complex proof obligations
796that have little to do with execution costs. With our approach, instead, we
797put less burden on the user, at the price of proving a weaker statement:
798the estimated and actual costs will be the same if and only if the high level
799program is converging. For prefixes of diverging programs we can provide
800a similar result where the equality is replaced by an inequality (loss of
801precision).
802
803Assuming totality of functions is however not sufficient yet at the object
804level. Even if a function returns, there is no guarantee that it will transfer
805control back to the calling point. For instance, the function could have
806manipulated the return address from its stack frame. Moreover, an object level
807program can forge any address and transfer control to it, with no guarantee
808on the execution behaviour and labelling properties of the called program.
809
810To solve the problem, we introduced the notion of \emph{structured trace}
811that come in two flavours: structured traces for total programs (an inductive
812type) and structured traces for diverging programs (a co-inductive type based
813on the previous one). Roughly speaking, a structured trace represents the
814execution of a well behaved program that is subject to several constraints
815like
816\begin{enumerate}
817 \item All function calls return control just after the calling point
818 \item The execution of all function bodies start with a label and end with
819   a RET (even the ones reached by invoking a function pointer)
820 \item All instructions are covered by a label (required by correctness of
821   the labelling approach)
822 \item The target of all conditional jumps must be labelled (a sufficient
823   but not necessary condition for precision of the labelling approach)
824 \item \label{prop5} Two structured traces with the same structure yield the same
825   cost traces.
826\end{enumerate}
827
828Correctness of cost predictions is proved only for structured execution traces,
829i.e. well behaved programs. The forward simulation proof for all back-end
830passes will actually be a proof of preservation of the structure of
831the structured traces that, because of property \ref{prop5}, will imply
832correctness of the cost prediction for the back-end. The Clight to RTLabs
833will also include a proof that associates to each converging execution its
834converging structured trace and to each diverging execution its diverging
835structured trace.
836
837There are also other two issues that invalidate the naive statement of
838correctness of cost prediciton given above. The algorithm that statically
839computes the cost of blocks is correct only when the object code is \emph{well
840formed} and the program counter is \emph{reachable}.
841A well formed object code is such that
842the program counter will never overflow after the execution step of
843the processor. An overflow that occurs during fetching but is overwritten
844during execution is, however, correct and necessary to accept correct
845programs that are as large as the program memory. Temporary overflows add
846complications to the proof. A reachable address is an address that can be
847obtained by fetching (not executing!) a finite number of times from the
848beginning of the code memory without ever overflowing. The complication is that
849the static prediction traverses the code memory assuming that the memory will
850be read sequentially from the beginning and that all jumps jump only to
851reachable addresses. When this property is violated, the way the code memory
852is interpreted is uncorrect and the cost computed is totally meaningless.
853The reachability relation is closed by fetching for well formed programs.
854The property that calls to function pointers only target reachable and
855well labelled locations, however, is not statically predictable and it is
856enforced in the structured trace.
857
858The proof of correctness of cost predictions has been quite complex. Setting
859up the good invariants (structured traces, well formed programs, reachability)
860and completing the proof has required more than 3 men months while the initally
861estimated effort was much lower. In the paper-and-pencil proof for IMP, the
862corresponding proof was obvious and only took two lines.
863
864The proof itself is quite involved. We
865basically need to show as an important lemma that the sum of the execution
866costs over a structured trace, where the costs are summed in execution order,
867is equivalent to the sum of the execution costs in the order of pre-payment.
868The two orders are quite different and the proof is by mutual recursion over
869the definition of the converging structured traces, which is a family of three
870mutual inductive types. The fact that this property only holds for converging
871function calls in hidden in the definition of the structured traces.
872Then we need to show that the order of pre-payment
873corresponds to the order induced by the cost traces extracted from the
874structured trace. Finally, we need to show that the statically computed cost
875for one block corresponds to the cost dinamically computed in pre-payment
876order.
877
878\section{Overall results}
879
880Functional correctness of the compiled code can be shown by composing
881the simulations to show that the target behaviour matches the
882behaviour of the source program, if the source program does not `go
883wrong'.  More precisely, we show that there is a forward simulation
884between the source trace and a (flattened structured) trace of the
885output, and conclude equivalence because the target's semantics are
886in the form of an executable function, and hence
887deterministic.
888
889Combining this with the correctness of the assignment of costs to cost
890labels at the ASM level for a structured trace, we can show that the
891cost of executing any compiled function (including the main function)
892is equal to the sum of all the values for cost labels encountered in
893the \emph{source code's} trace of the function.
894
895\section{Estimated effort}
896Based on the rough analysis performed so far we can estimate the total
897effort for the certification of the compiler. We obtain this estimation by
898combining, for each pass: 1) the number of lines of code to be certified;
8992) the ratio of number of lines of proof to number of lines of code from
900the CompCert project~\cite{compcert} for the CompCert pass that is closest to
901ours; 3) an estimation of the complexity of the pass according to the
902analysis above.
903
904\begin{tabular}{lrlrr}
905Pass origin & Code lines & CompCert ratio & Estimated effort & Estimated effort \\
906            &            &                & (based on CompCert) & \\
907\hline
908Common &  4864 & 4.25 \permil & 20.67 & 17.0 \\
909Cminor &  1057 & 5.23 \permil & 5.53  &  6.0 \\
910Clight &  1856 & 5.23 \permil & 9.71  & 10.0 \\ 
911RTLabs &  1252 & 1.17 \permil & 1.48  &  5.0 \\
912RTL    &   469 & 4.17 \permil & 1.95  &  2.0 \\
913ERTL   &   789 & 3.01 \permil & 2.38  & 2.5 \\
914LTL    &    92 & 5.94 \permil & 0.55  & 0.5 \\
915LIN    &   354 & 6.54 \permil & 2.31  &   1.0 \\
916ASM    &   984 & 4.80 \permil & 4.72  &  10.0 \\
917\hline
918Total common    &  4864 & 4.25 \permil & 20.67 & 17.0 \\
919Total front-end &  2913 & 5.23 \permil & 15.24 & 16.0 \\
920Total back-end  &  6853 & 4.17 \permil & 13.39 & 21.0 \\
921\hline
922Total           & 14630 & 3.75 \permil & 49.30 & 54.0 \\
923\end{tabular}
924
925We provide now some additional informations on the methodology used in the
926computation. The passes in Cerco and CompCert front-end closely match each
927other. However, there is no clear correspondence between the two back-ends.
928For instance, we enforce the calling convention immediately after instruction
929selection, whereas in CompCert this is performed in a later phase. Or we
930linearize the code at the very end, whereas CompCert performs linearization
931as soon as possible. Therefore, the first part of the exercise has consisted
932in shuffling and partitioning the CompCert code in order to assign to each
933CerCo pass the CompCert code that performs the same transformation.
934
935After this preliminary step, using the data given in~\cite{compcert} (which
936are relative to an early version of CompCert) we computed the ratio between
937men months and lines of code in CompCert for each CerCo pass. This is shown
938in the third column of Table~\ref{wildguess}. For those CerCo passes that
939have no correspondence in CompCert (like the optimizing assembler) or where
940we have insufficient data, we have used the average of the ratios computed
941above.
942
943The first column of the table shows the number of lines of code for each
944pass in CerCo. The third column is obtained multiplying the first with the
945CompCert ratio. It provides an estimate of the effort required (in men months)
946if the complexity of the proofs for CerCo and Compcert would be the same.
947
948The two proof styles, however, are on purpose completely different. Where
949CompCert uses non executable semantics, describing the various semantics with
950inductive types, we have preferred executable semantics. Therefore, CompCert
951proofs by induction and inversion become proof by functional inversion,
952performed using the Russel methodology (now called Program in Coq, but whose
953behaviour differs from Matita's one). Moreover, CompCert code is written using
954only types that belong to the Hindley-Milner fragment, whereas we have
955heavily exploited dependent types all over the code. The dependent type
956discipline offers many advantages from the point of view of clarity of the
957invariants involved and early detection of errors and it naturally combines
958well with the Russel approach which is based on dependent types. However, it
959is also well known to introduce technical problems all over the code, like
960the need to explicitly prove type equalities to be able to manipulate
961expressions in certain ways. In many situations, the difficulties encountered
962with manipulating dependent types are better addressed by improving the Matita
963system, according to the formalization driven system development. For this
964reason, and assuming a pessimistic point of view on our performance, the
965fourth columns presents the final estimation of the effort required, that also
966takes in account the complexity of the proof suggested by the informal proofs
967sketched in the previous section.
968
969\end{document}
Note: See TracBrowser for help on using the repository browser.