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

Last change on this file since 1748 was 1748, checked in by mulligan, 8 years ago

commit to avoid conflicts

File size: 32.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{wasysym}
18
19\lstdefinelanguage{matita-ocaml} {
20  mathescape=true
21}
22\lstset{
23  language=matita-ocaml,basicstyle=\tt,columns=flexible,breaklines=false,
24  showspaces=false, showstringspaces=false, extendedchars=false,
25  inputencoding=utf8x, tabsize=2
26}
27
28\title{Proof outline for the correctness of the CerCo compiler}
29\date{\today}
30\author{The CerCo team}
31
32\begin{document}
33
34\maketitle
35
36\section{Introduction}
37\label{sect.introduction}
38
39In 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.
40This 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.
41In 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.
42
43\section{Front-end: Clight to RTLabs}
44
45The front-end of the CerCo compiler consists of several stages:
46
47\begin{center}
48\begin{minipage}{.8\linewidth}
49\begin{tabbing}
50\quad \= $\downarrow$ \quad \= \kill
51\textsf{Clight}\\
52\> $\downarrow$ \> cast removal\\
53\> $\downarrow$ \> add runtime functions\footnote{Following the last project
54meeting we intend to move this transformation to the back-end}\\
55\> $\downarrow$ \> cost labelling\\
56\> $\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)\\
57\> $\downarrow$ \> partial redundancy elimination$^{\mbox{\scriptsize \ref{lab:opt2}}}$ (an endo-transformation)\\
58\> $\downarrow$ \> stack variable allocation and control structure
59 simplification\\
60\textsf{Cminor}\\
61\> $\downarrow$ \> generate global variable initialisation code\\
62\> $\downarrow$ \> transform to RTL graph\\
63\textsf{RTLabs}\\
64\> $\downarrow$ \> \\
65\>\,\vdots
66\end{tabbing}
67\end{minipage}
68\end{center}
69
70Here, by `endo-transformation', we mean a mapping from language back to itself:
71the loop optimization step maps the Clight language to itself.
72
73%Our overall statements of correctness with respect to costs will
74%require a correctly labelled program
75There are three layers in most of the proofs proposed:
76\begin{enumerate}
77\item invariants closely tied to the syntax and transformations using
78  dependent types,
79\item a forward simulation proof, and
80\item syntactic proofs about the cost labelling.
81\end{enumerate}
82The first will support both functional correctness and allow us to show
83the totality of some of the compiler stages (that is, those stages of
84the compiler cannot fail).  The second provides the main functional
85correctness result, and the last will be crucial for applying
86correctness results about the costings from the back-end.
87
88We will also prove that a suitably labelled RTLabs trace can be turned
89into a \emph{structured trace} which splits the execution trace into
90cost-label to cost-label chunks with nested function calls.  This
91structure was identified during work on the correctness of the
92back-end cost analysis as retaining important information about the
93structure of the execution that is difficult to reconstruct later in
94the compiler.
95
96\subsection{Clight cast removal}
97
98This transformation removes some casts inserted by the parser to make
99arithmetic promotion explicit but which are superfluous (such as
100\lstinline[language=C]'c = (short)((int)a + (int)b);' where
101\lstinline'a' and \lstinline'b' are \lstinline[language=C]'short').
102This is necessary for producing good code for our target architecture.
103
104It only affects Clight expressions, recursively detecting casts that
105can be safely eliminated.  The semantics provides a big-step
106definition for expression, so we should be able to show a lock-step
107forward simulation between otherwise identical states using a lemma
108showing that cast elimination does not change the evaluation of
109expressions.  This lemma will follow from a structural induction on
110the source expression.  We have already proved a few of the underlying
111arithmetic results necessary to validate the approach.
112
113\subsection{Clight cost labelling}
114
115This adds cost labels before and after selected statements and
116expressions, and the execution traces ought to be equivalent modulo
117the new cost labels.  Hence it requires a simple forward simulation
118with a limited amount of stuttering whereever a new cost label is
119introduced.  A bound can be given for the amount of stuttering allowed
120based on the statement or continuation to be evaluated next.
121
122We also intend to show three syntactic properties about the cost
123labelling:
124\begin{enumerate}
125\item every function starts with a cost label,
126\item every branching instruction is followed by a cost label (note that
127  exiting a loop is treated as a branch), and
128\item the head of every loop (and any \lstinline'goto' destination) is
129  a cost label.
130\end{enumerate}
131These can be shown by structural induction on the source term.
132
133\subsection{Clight to Cminor translation}
134
135This translation is the first to introduce some invariants, with the
136proofs closely tied to the implementation by dependent typing.  These
137are largely complete and show that the generated code enjoys:
138\begin{itemize}
139\item some minimal type safety shown by explicit checks on the
140  Cminor types during the transformation (a little more work remains
141  to be done here, but follows the same form);
142\item that variables named in the parameter and local variable
143  environments are distinct from one another, again by an explicit
144  check;
145\item that variables used in the generated code are present in the
146  resulting environment (either by checking their presence in the
147  source environment, or from a list of freshly generated temporary variables);
148  and
149\item that all \lstinline[language=C]'goto' labels are present (by
150  checking them against a list of source labels and proving that all
151  source labels are preserved).
152\end{itemize}
153
154The simulation will be similar to the relevant stages of CompCert
155(Clight to Csharpminor and Csharpminor to Cminor --- in the event that
156the direct proof is unwieldy we could introduce an intermediate
157language corresponding to Csharpminor).  During early experimentation
158with porting CompCert definitions to the Matita proof assistant we
159found little difficulty reproving the results for the memory model, so
160we plan to port the memory injection properties and use them to relate
161Clight in-memory variables with either the value of the local variable or a
162stack slot, depending on how it was classified.
163
164This should be sufficient to show the equivalence of (big-step)
165expression evaluation.  The simulation can then be shown by relating
166corresponding blocks of statement and continuations with their Cminor
167counterparts and proving that a few steps reaches the next matching
168state.
169
170The syntactic properties required for cost labels remain similar and a
171structural induction on the function bodies should be sufficient to
172show that they are preserved.
173
174\subsection{Cminor global initialisation code}
175
176This short phase replaces the global variable initialisation data with
177code that executes when the program starts.  Each piece of
178initialisation data in the source is matched by a new statement
179storing that data.  As each global variable is allocated a distinct
180memory block, the program state after the initialisation statements
181will be the same as the original program's state at the start of
182execution, and will proceed in the same manner afterwards.
183
184% Actually, the above is wrong...
185% ... this ought to be in a fresh main function with a fresh cost label
186
187\subsection{Cminor to RTLabs translation}
188
189In this part of the compiler we transform the program's functions into
190control flow graphs.  It is closely related to CompCert's Cminorsel to
191RTL transformation, albeit with target-independent operations.
192
193We already enforce several invariants with dependent types: some type
194safety, mostly shown using the type information from Cminor; and
195that the graph is closed (by showing that each successor was recently
196added, or corresponds to a \lstinline[language=C]'goto' label which
197are all added before the end).  Note that this relies on a
198monotonicity property; CompCert maintains a similar property in a
199similar way while building RTL graphs.  We will also add a result
200showing that all of the pseudo-register names are distinct for use by
201later stages using the same method as Cminor.
202
203The simulation will relate Cminor states to RTLabs states which are about to
204execute the code corresponding to the Cminor statement or continuation.
205Each Cminor statement becomes zero or more RTLabs statements, with a
206decreasing measure based on the statement and continuations similar to
207CompCert's.  We may also follow CompCert in using a relational
208specification of this stage so as to abstract away from the functional
209(and highly dependently typed) definition.
210
211The first two labelling properties remain as before; we will show that
212cost labels are preserved, so the function entry point will be a cost
213label, and successors to any statement that are cost labels map still
214map to cost labels, preserving the condition on branches.  We replace
215the property for loops with the notion that we will always reach a
216cost label or the end of the function after following a bounded number of
217successors.  This can be easily seen in Cminor using the requirement
218for cost labels at the head of loops and after gotos.  It remains to
219show that this is preserved by the translation to RTLabs.  % how?
220
221\subsection{RTLabs structured trace generation}
222
223This proof-only step incorporates the function call structure and cost
224labelling properties into the execution trace.  As the function calls
225are nested within the trace, we need to distinguish between
226terminating and non-terminating function calls.  Thus we use the
227excluded middle (specialised to a function termination property) to do
228this.
229
230Structured traces for terminating functions are built by following the
231flat trace, breaking it into chunks between cost labels and
232recursively processing function calls.  The main difficulties here are
233the non-structurally recursive nature of the function (instead we use
234the size of the termination proof as a measure) and using the RTLabs
235cost labelling properties to show that the constraints of the
236structured traces are observed.  We also show that the lower stack
237frames are preserved during function calls in order to prove that
238after returning from a function call we resume execution of the
239correct code.  This part of the work has already been constructed, but
240still requires a simple proof to show that flattening the structured
241trace recreates the original flat trace.
242
243The non-terminating case follows the trace like the terminating
244version to build up chunks of trace from cost-label to cost-label
245(which, by the finite distance to a cost label property shown before,
246can be represented by an inductive type).  These chunks are chained
247together in a coinductive data structure that can represent
248non-terminating traces.  The excluded middle is used to decide whether
249function calls terminate, in which case the function described above
250constructs an inductive terminating structured trace which is nested
251in the caller's trace.  Otherwise, another coinductive constructor is
252used to embed the non-terminating trace of the callee, generated by
253corecursion.  This part of the trace transformation is currently under
254construction, and will also need a flattening result to show that it
255is correct.
256
257
258\section{Backend: RTLabs to machine code}
259\label{sect.backend.rtlabs.machine.code}
260
261The compiler backend consists of the following intermediate languages, and stages of translation:
262
263\begin{center}
264\begin{minipage}{.8\linewidth}
265\begin{tabbing}
266\quad \=\,\vdots\= \\
267\> $\downarrow$ \>\\
268\> $\downarrow$ \quad \= \kill
269\textsf{RTLabs}\\
270\> $\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) \\
271\> $\downarrow$ \> instruction selection\\
272\> $\downarrow$ \> change of memory models in compiler\\
273\textsf{RTL}\\
274\> $\downarrow$ \> constant propagation$^{\mbox{\scriptsize \ref{lab:opt}}}$ (an endo-transformation) \\
275\> $\downarrow$ \> calling convention made explicit \\
276\> $\downarrow$ \> layout of activation records \\
277\textsf{ERTL}\\
278\> $\downarrow$ \> register allocation and spilling\\
279\> $\downarrow$ \> dead code elimination\\
280\textsf{LTL}\\
281\> $\downarrow$ \> function linearisation\\
282\> $\downarrow$ \> branch compression (an endo-transformation) \\
283\textsf{LIN}\\
284\> $\downarrow$ \> relabeling\\
285\textsf{ASM}\\
286\> $\downarrow$ \> pseudoinstruction expansion\\
287\textsf{MCS-51 machine code}\\
288\end{tabbing}
289\end{minipage}
290\end{center}
291
292\subsection{The RTLabs to RTL translation}
293\label{subsect.rtlabs.rtl.translation}
294
295The RTLabs to RTL translation pass marks the frontier between the two memory models used in the CerCo project.
296As a result, we require some method of translating between the values that the two memory models permit.
297Suppose we have such a translation, $\sigma$.
298Then the translation between values of the two memory models may be pictured with:
299
300\begin{displaymath}
301\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
302\end{displaymath}
303
304In the front-end, we have both integer and float values, where integer values are `sized, along with null values and pointers.
305In the back-end memory model, floats values are no longer present, as floating point arithmetic is not supported by the CerCo compiler.
306However, the back-end memory model introduces an undefined value ($\bot$) and sized pointer values.
307
308We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}.
309
310\begin{displaymath}
311\mathtt{Mem}\ \alpha = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \alpha)
312\end{displaymath}
313
314Here, \texttt{Block} consists of a \texttt{Region} paired with an identifier.
315
316\begin{displaymath}
317\mathtt{Block} ::= \mathtt{Region} \cup \mathtt{ID}
318\end{displaymath}
319
320We now have what we need for defining what is meant by the `memory' in the backend memory model.
321Namely, we instantiate the previously defined \texttt{Mem} type with the type of back-end memory values.
322
323\begin{displaymath}
324\mathtt{BEMem} = \mathtt{Mem} \mathtt{BEValue}
325\end{displaymath}
326
327Memory addresses consist of a pair of back-end memory values:
328
329\begin{displaymath}
330\mathtt{Address} = \mathtt{BEValue} \times  \mathtt{BEValue} \\
331\end{displaymath}
332
333\begin{center}
334\begin{picture}(2, 2)
335\put(-150,-20){\framebox(25,25)[c]{\texttt{v}}}
336\put(-125,-20){\framebox(25,25)[c]{\texttt{4}}}
337\put(-100,-20){\framebox(25,25)[c]{\texttt{cont}}}
338\put(-75,-20){\framebox(25,25)[c]{\texttt{cont}}}
339\put(-50,-20){\framebox(25,25)[c]{\texttt{cont}}}
340\put(-15,-10){\vector(1, 0){30}}
341\put(25,-20){\framebox(25,25)[c]{\texttt{\texttt{v1}}}}
342\put(50,-20){\framebox(25,25)[c]{\texttt{\texttt{v2}}}}
343\put(75,-20){\framebox(25,25)[c]{\texttt{\texttt{v3}}}}
344\put(100,-20){\framebox(25,25)[c]{\texttt{\texttt{v4}}}}
345\end{picture}
346\end{center}
347
348\begin{displaymath}
349\mathtt{load}\ s\ a\ M = \mathtt{Some}\ v \rightarrow \forall i \leq s.\ \mathtt{load}\ s\ (a + i)\ \sigma(M) = \mathtt{Some}\ v_i
350\end{displaymath}
351
352\begin{displaymath}
353\sigma(\mathtt{store}\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(M)
354\end{displaymath}
355
356\begin{displaymath}
357\texttt{load}^* (\mathtt{store}\ \sigma(v)\ \sigma(M))\ \sigma(a)\ \sigma(M) = \mathtt{load}^*\ \sigma(s)\ \sigma(a)\ \sigma(M)
358\end{displaymath}
359
360\begin{displaymath}
361\begin{array}{rll}
362\mathtt{State} & ::=  & (\mathtt{State} : \mathtt{Frame}^* \times \mathtt{Frame} \\
363               & \mid & \mathtt{Call} : \mathtt{Frame}^* \times \mathtt{Args} \times \mathtt{Return} \times \mathtt{Fun} \\
364               & \mid & \mathtt{Return} : \mathtt{Frame}^* \times \mathtt{Value} \times \mathtt{Return}) \times \mathtt{Mem}
365\end{array}
366\end{displaymath}
367
368\begin{displaymath}
369\mathtt{State} ::= \mathtt{Frame}^* \times \mathtt{PC} \times \mathtt{SP} \times \mathtt{ISP} \times \mathtt{CARRY} \times \mathtt{REGS}
370\end{displaymath}
371
372\begin{displaymath}
373\mathtt{State} \stackrel{\sigma}{\longrightarrow} \mathtt{State}
374\end{displaymath}
375
376\begin{displaymath}
377\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}))
378\end{displaymath}
379
380\begin{displaymath}
381\sigma(\mathtt{Return}(-)) \longrightarrow \sigma \circ \text{return one step}
382\end{displaymath}
383
384\begin{displaymath}
385\sigma(\mathtt{Call}(-)) \longrightarrow \sigma \circ \text{call one step}
386\end{displaymath}
387
388Return one step commuting diagram:
389
390\begin{displaymath}
391\begin{diagram}
392s & \rTo^{\text{one step of execution}} & s'   \\
393  & \rdTo                             & \dTo \\
394  &                                   & \llbracket s'' \rrbracket
395\end{diagram}
396\end{displaymath}
397
398Call one step commuting diagram:
399
400\begin{displaymath}
401\begin{diagram}
402s & \rTo^{\text{one step of execution}} & s'   \\
403  & \rdTo                             & \dTo \\
404  &                                   & \llbracket s'' \rrbracket
405\end{diagram}
406\end{displaymath}
407
408\begin{displaymath}
409\begin{array}{rcl}
410\mathtt{Call(id,\ args,\ dst,\ pc),\ State(FRAME, FRAMES)} & \longrightarrow & \mathtt{Call(M(args), dst)}, \\
411                                                           &                 & \mathtt{PUSH(current\_frame[PC := after\_return])}
412\end{array}
413\end{displaymath}
414
415In the case where the call is to an external function, we have:
416
417\begin{displaymath}
418\begin{array}{rcl}
419\mathtt{Call(M(args), dst)},                       & \stackrel{\mathtt{ret\_val = f(M(args))}}{\longrightarrow} & \mathtt{Return(ret\_val,\ dst,\ PUSH(...))} \\
420\mathtt{PUSH(current\_frame[PC := after\_return])} &                                                            & 
421\end{array}
422\end{displaymath}
423
424then:
425
426\begin{displaymath}
427\begin{array}{rcl}
428\mathtt{Return(ret\_val,\ dst,\ PUSH(...))} & \longrightarrow & \mathtt{pc = POP\_STACK(regs[dst := M(ret\_val)],\ pc)}
429\end{array}
430\end{displaymath}
431
432In the case where the call is to an internal function, we have:
433
434\begin{displaymath}
435\begin{array}{rcl}
436\mathtt{CALL}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc}) & \longrightarrow & \mathtt{CALL\_ID}(\mathtt{id}, \sigma'(\mathtt{args}), \sigma(\mathtt{dst}), \mathtt{pc}) \\
437\mathtt{RETURN}                                                      & \longrightarrow & \mathtt{RETURN} \\
438\end{array} 
439\end{displaymath}
440
441\begin{displaymath}
442\begin{array}{rcl}
443\mathtt{Call(M(args), dst)}                        & \longrightarrow & \mathtt{sp = alloc}, regs = \emptyset[- := PARAMS] \\
444\mathtt{PUSH(current\_frame[PC := after\_return])} &                 & \mathtt{State}(regs,\ sp,\ pc_\emptyset,\ dst)
445\end{array}
446\end{displaymath}
447
448then:
449
450\begin{displaymath}
451\begin{array}{rcl}
452\mathtt{sp = alloc}, regs = \emptyset[- := PARAMS] & \longrightarrow & \mathtt{free(sp)} \\
453\mathtt{State}(regs,\ sp,\ pc_\emptyset,\ dst)     &                 & \mathtt{Return(M(ret\_val), dst, frames)}
454\end{array}
455\end{displaymath}
456
457and finally:
458
459\begin{displaymath}
460\begin{array}{rcl}
461\mathtt{free(sp)}                         & \longrightarrow & \mathtt{pc = POP\_STACK(regs[dst := M(ret\_val)],\ pc)} \\
462\mathtt{Return(M(ret\_val), dst, frames)} &                 & 
463\end{array}
464\end{displaymath}
465
466\begin{displaymath}
467\begin{array}{rcl}
468\sigma & : & \mathtt{register} \rightarrow \mathtt{list\ register} \\
469\sigma' & : & \mathtt{list\ register} \rightarrow \mathtt{list\ register}
470\end{array}
471\end{displaymath}
472
473\subsection{The RTL to ERTL translation}
474\label{subsect.rtl.ertl.translation}
475
476\begin{displaymath}
477\begin{diagram}
478& & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket & & \\
479& \ldTo^{\text{external}} & & \rdTo^{\text{internal}} & \\
480\skull & & & & \mathtt{regs} = [\mathtt{params}/-] \\
481& & & & \mathtt{sp} = \mathtt{ALLOC} \\
482& & & & \mathtt{PUSH}(\mathtt{carry}, \mathtt{regs}, \mathtt{dst}, \mathtt{return\_addr}), \mathtt{pc}_{0}, \mathtt{regs}, \mathtt{sp} \\
483\end{diagram}
484\end{displaymath}
485
486\begin{align*}
487\llbracket \mathtt{RETURN} \rrbracket \\
488\mathtt{return\_addr} & := \mathtt{top}(\mathtt{stack}) \\
489v*                    & := m(\mathtt{rv\_regs}) \\
490\mathtt{dst}, \mathtt{sp}, \mathtt{carry}, \mathtt{regs} & := \mathtt{pop} \\
491\mathtt{regs}[v* / \mathtt{dst}] \\
492\end{align*}
493
494\begin{displaymath}
495\begin{diagram}
496s    & \rTo^1 & s' & \rTo^1 & s'' \\
497\dTo &        &    & \rdTo  & \dTo \\
498\llbracket s \rrbracket & \rTo(1,3)^1 & & & \llbracket s'' \rrbracket \\ 
499\mathtt{CALL} \\
500\end{diagram}
501\end{displaymath}
502
503\begin{displaymath}
504\begin{diagram}
505s    & \rTo^1 & s' & \rTo^1 & s'' \\
506\dTo &        &    & \rdTo  & \dTo \\
507\  & \rTo(1,3) & & & \ \\
508\mathtt{RETURN} \\
509\end{diagram}
510\end{displaymath}
511
512\begin{displaymath}
513\mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist'})
514\rightarrow \mathtt{graph} \rightarrow \mathtt{graph}
515\end{displaymath}
516
517\begin{align*}
518\mathtt{theorem} &\ \mathtt{b\_graph\_translate\_ok}: \\
519& \forall  f.\forall G_{i}.\mathtt{let}\ G_{\sigma} := \mathtt{b\_graph\_translate}\ f\ G_{i}\ \mathtt{in} \\
520&       \forall l \in G_{i}.\mathtt{subgraph}\ (f\ l)\ l\ (\mathtt{next}\ l\ G_{i})\ G_{\sigma}
521\end{align*}
522
523\begin{align*}
524\mathtt{lemma} &\ \mathtt{execute\_1\_step\_ok}: \\
525&       \forall s.  \mathtt{let}\ s' := s\ \sigma\ \mathtt{in} \\
526&       \mathtt{let}\ l := pc\ s\ \mathtt{in} \\
527&       s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma
528\end{align*}
529
530\begin{align*}
531\mathrm{RTL\ status} & \ \ \mathrm{ERTL\ status} \\
532\mathtt{sp} & = \mathtt{spl} / \mathtt{sph} \\
533\mathtt{graph} & \mapsto \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\
534& \mathrm{where}\ s = \mathrm{callee\ saved} + \nu \mathrm{RA} \\
535\end{align*}
536
537\begin{displaymath}
538\begin{diagram}
539\mathtt{CALL} & \rTo^1 & \mathtt{inside\ function} \\
540\dTo & & \dTo \\
541\underbrace{\ldots}_{\llbracket \mathtt{CALL} \rrbracket} & \rTo &
542\underbrace{\ldots}_{\mathtt{prologue}} \\
543\end{diagram}
544\end{displaymath}
545
546\begin{displaymath}
547\begin{diagram}
548\mathtt{RETURN} & \rTo^1 & \mathtt{.} \\
549\dTo & & \dTo \\
550\underbrace{\ldots}_{\mathtt{epilogue}} & \rTo &
551\underbrace{\ldots} \\
552\end{diagram}
553\end{displaymath}
554
555\begin{align*}
556\mathtt{prologue}(s) = & \mathtt{create\_new\_frame}; \\
557                       & \mathtt{pop\ ra}; \\
558                       & \mathtt{save\ callee\_saved}; \\
559                                                                                         & \mathtt{get\_params} \\
560                                                                                         & \ \ \mathtt{reg\_params}: \mathtt{move} \\
561                                                                                         & \ \ \mathtt{stack\_params}: \mathtt{push}/\mathtt{pop}/\mathtt{move} \\
562\end{align*}
563
564\begin{align*}
565\mathtt{epilogue}(s) = & \mathtt{save\ return\ to\ tmp\ real\ regs}; \\
566                                                                                         & \mathtt{restore\_registers}; \\
567                       & \mathtt{push\ ra}; \\
568                       & \mathtt{delete\_frame}; \\
569                       & \mathtt{save return} \\
570\end{align*}
571
572\begin{displaymath}
573\mathtt{CALL}\ id \mapsto \mathtt{set\_params};\ \mathtt{CALL}\ id;\ \mathtt{fetch\_result}
574\end{displaymath}
575
576\subsection{The ERTL to LTL translation}
577\label{subsect.ertl.ltl.translation}
578
579\subsection{The LTL to LIN translation}
580\label{subsect.ltl.lin.translation}
581
582We 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:
583\begin{displaymath}
584\mathtt{pc : label} \stackrel{\sigma}{\longrightarrow} \mathbb{N}
585\end{displaymath}
586
587The LTL to LIN translation pass also linearises the graph data structure into a list of instructions.
588Pseudocode for the linearisation process is as follows:
589
590\begin{lstlisting}
591let rec linearise graph visited required generated todo :=
592  match todo with
593  | l::todo ->
594    if l $\in$ visited then
595      let generated := generated $\cup\ \{$ Goto l $\}$ in
596      let required := required $\cup$ l in
597        linearise graph visited required generated todo
598    else
599      -- Get the instruction at label `l' in the graph
600      let lookup := graph(l) in
601      let generated := generated $\cup\ \{$ lookup $\}$ in
602      -- Find the successor of the instruction at label `l' in the graph
603      let successor := succ(l, graph) in
604      let todo := successor::todo in
605        linearise graph visited required generated todo
606  | []      -> (required, generated)
607\end{lstlisting}
608
609It is easy to see that this linearisation process eventually terminates.
610In 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.
611
612The 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.
613We envisage needing to prove the following invariants on the linearisation function above:
614
615\begin{enumerate}
616\item
617$\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,
618\item
619$\forall \mathtt{l} \in \mathtt{generated}.\ \mathtt{succ(l,\ graph)} \subseteq \mathtt{required} \cup \mathtt{todo}$,
620\item
621$\mathtt{required} \subseteq \mathtt{visited}$,
622\item
623$\mathtt{visited} \cap \mathtt{todo} = \emptyset$.
624\end{enumerate}
625
626The invariants collectively imply the following properties, crucial to correctness, about the linearisation process:
627
628\begin{enumerate}
629\item
630Every graph node is visited at most once,
631\item
632Every instruction that is generated is generated due to some graph node being visited,
633\item
634The successor instruction of every instruction that has been visited already will eventually be visited too.
635\end{enumerate}
636
637Note, 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.
638In particular, we see the notion of well formedness (yet to be formally defined) resting on the following conditions:
639
640\begin{enumerate}
641\item
642For every jump to a label in a linearised program, the target label exists at some point in the program,
643\item
644Each label is unique, appearing only once in the program,
645\item
646The final instruction of a program must be a return.
647\end{enumerate}
648
649We assume that these properties will be easy consequences of the invariants on the linearisation function defined above.
650
651The final condition above is potentially a little opaque, so we explain further.
652First, 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).
653However, 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.
654Each 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.
655
656\subsection{The LIN to ASM and ASM to MCS-51 machine code translations}
657\label{subsect.lin.asm.translation}
658
659The LIN to ASM translation step is trivial, being almost the identity function.
660The 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.
661
662The ASM to MCS-51 machine code translation step, and the required statements of correctness, are found in an unpublished manuscript attached to this document.
663
664\section{Estimated effort}
665Based on the rough analysis performed so far we can estimate the total
666effort for the certification of the compiler. We obtain this estimation by
667combining, for each pass: 1) the number of lines of code to be certified;
6682) the ratio of number of lines of proof to number of lines of code from
669the CompCert project~\cite{compcert} for the CompCert pass that is closest to
670ours; 3) an estimation of the complexity of the pass according to the
671analysis above.
672
673\begin{tabular}{lrlll}
674Pass origin & Code lines & CompCert ratio & Estimated effort & Estimated effort \\
675            &            &                & (based on CompCert) & \\
676\hline
677Common & 12759 & 4.25 \permil & 54.22 \\
678Cminor &  1057 & 5.23 \permil & 5.53 \\
679Clight &  1856 & 5.23 \permil & 9.71 \\ 
680RTLabs &  1252 & 1.17 \permil & 1.48 \\
681RTL    &   469 & 4.17 \permil & 1.95 \\
682ERTL   &   789 & 3.01 \permil & 2.38 \\
683LTL    &    92 & 5.94 \permil & 0.55 \\
684LIN    &   354 & 6.54 \permil & 2.31 \\
685ASM    &   984 & 4.80 \permil & 4.72 \\
686\hline
687Total common    & 12759 & 4.25 \permil & 54.22 \\
688Total front-end &  2913 & 5.23 \permil & 15.24 \\
689Total back-end  &  6853 & 4.17 \permil & 13.39 \\
690\hline
691Total           & 22525 & 3.75 \permil & 84.85 \\
692\end{tabular}
693
694We provide now some additional informations on the methodology used in the
695computation. The passes in Cerco and CompCert front-end closely match each
696other. However, there is no clear correspondence between the two back-ends.
697For instance, we enforce the calling convention immediately after instruction
698selection, whereas in CompCert this is performed in a later phase. Or we
699linearize the code at the very end, whereas CompCert performs linearization
700as soon as possible. Therefore, the first part of the exercise has consisted
701in shuffling and partitioning the CompCert code in order to assign to each
702CerCo pass the CompCert code that performs the same transformation.
703
704After this preliminary step, using the data given in~\cite{compcert} (which
705are relative to an early version of CompCert) we computed the ratio between
706men months and lines of code in CompCert for each CerCo pass. This is shown
707in the third column of Table~\ref{wildguess}. For those CerCo passes that
708have no correspondence in CompCert (like the optimizing assembler) or where
709we have insufficient data, we have used the average of the ratios computed
710above.
711
712The first column of the table shows the number of lines of code for each
713pass in CerCo. The third column is obtained multiplying the first with the
714CompCert ratio. It provides an estimate of the effort required (in men months)
715if the complexity of the proofs for CerCo and Compcert would be the same.
716
717The two proof styles, however, are on purpose completely different. Where
718CompCert uses non executable semantics, describing the various semantics with
719inductive types, we have preferred executable semantics. Therefore, CompCert
720proofs by induction and inversion become proof by functional inversion,
721performed using the Russel methodology (now called Program in Coq, but whose
722behaviour differs from Matita's one). Moreover, CompCert code is written using
723only types that belong to the Hindley-Milner fragment, whereas we have
724heavily exploited dependent types all over the code. The dependent type
725discipline offers many advantages from the point of view of clarity of the
726invariants involved and early detection of errors and it naturally combines
727well with the Russel approach which is based on dependent types. However, it
728is also well known to introduce technical problems all over the code, like
729the need to explicitly prove type equalities to be able to manipulate
730expressions in certain ways. In many situations, the difficulties encountered
731with manipulating dependent types are better addressed by improving the Matita
732system, according to the formalization driven system development. For this
733reason, and assuming a pessimistic point of view on our performance, the
734fourth columns presents the final estimation of the effort required, that also
735takes in account the complexity of the proof suggested by the informal proofs
736sketched in the previous section.
737
738\end{document}
Note: See TracBrowser for help on using the repository browser.