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

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

Rephrased introduction.

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