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

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

added more to header of file, commit to avoid conflicts with jaap

File size: 7.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
18\lstdefinelanguage{matita-ocaml} {
19  mathescape=true
20}
21\lstset{
22  language=matita-ocaml,basicstyle=\tt,columns=flexible,breaklines=false,
23  showspaces=false, showstringspaces=false, extendedchars=false,
24  inputencoding=utf8x, tabsize=2
25}
26
27\title{Proof outline for the correctness of the CerCo compiler}
28\date{\today}
29\author{The CerCo team}
30
31\begin{document}
32
33\maketitle
34
35\section{Introduction}
36\label{sect.introduction}
37
38\section{The RTLabs to RTL translation}
39\label{sect.rtlabs.rtl.translation}
40
41% dpm: type system and casting load (???)
42We require a map, $\sigma$, between \texttt{Values} of the front-end memory model to lists of \texttt{BEValues} of the back-end memory model:
43
44\begin{displaymath}
45\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
46\end{displaymath}
47
48We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}.
49
50\begin{displaymath}
51\mathtt{Mem}\ \alpha = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \alpha)
52\end{displaymath}
53
54where
55
56\begin{displaymath}
57\mathtt{Block} ::= \mathtt{Region} \cup \mathtt{ID}
58\end{displaymath}
59
60\begin{displaymath}
61\mathtt{BEMem} = \mathtt{Mem} \mathtt{Value}
62\end{displaymath}
63
64\begin{displaymath}
65\mathtt{Address} = \mathtt{BEValue} \times  \mathtt{BEValue} \\
66\end{displaymath}
67
68\begin{displaymath}
69\mathtt{Mem} = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \mathtt{Cont} \mid \mathtt{Value} \times \mathtt{Size} \mid \mathtt{null})
70\end{displaymath}
71
72\begin{center}
73\begin{picture}(2, 2)
74% picture of sigma mapping memory to memory
75TODO
76\end{picture}
77\end{center}
78
79\begin{displaymath}
80\mathtt{load}\ s\ a\ M = \mathtt{Some}\ v \rightarrow \forall i \leq s.\ \mathtt{load}\ s\ (a + i)\ \sigma(M) = \mathtt{Some}\ v_i
81\end{displaymath}
82
83\begin{displaymath}
84\sigma(\mathtt{store}\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(M)
85\end{displaymath}
86
87\begin{displaymath}
88\begin{array}{rll}
89\mathtt{State} & ::=  & (\mathtt{State} : \mathtt{Frame}^* \times \mathtt{Frame} \\
90               & \mid & \mathtt{Call} : \mathtt{Frame}^* \times \mathtt{Args} \times \mathtt{Return} \times \mathtt{Fun} \\
91               & \mid & \mathtt{Return} : \mathtt{Frame}^* \times \mathtt{Value} \times \mathtt{Return}) \times \mathtt{Mem}
92\end{array}
93\end{displaymath}
94
95\begin{displaymath}
96\mathtt{State} ::= \mathtt{Frame}^* \times \mathtt{PC} \times \mathtt{SP} \times \mathtt{ISP} \times \mathtt{CARRY} \times \mathtt{REGS}
97\end{displaymath}
98
99\begin{displaymath}
100\mathtt{State} \stackrel{\sigma}{\longrightarrow} \mathtt{State}
101\end{displaymath}
102
103\begin{displaymath}
104\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}))
105\end{displaymath}
106
107\begin{displaymath}
108\sigma(\mathtt{Return}(-)) \longrightarrow \sigma \circ \text{return one step}
109\end{displaymath}
110
111\begin{displaymath}
112\sigma(\mathtt{Call}(-)) \longrightarrow \sigma \circ \text{call one step}
113\end{displaymath}
114
115Return one step commuting diagram:
116
117\begin{displaymath}
118\begin{diagram}
119s & \rTo^{\text{one step of execution}} & s'   \\
120  & \rdTo                             & \dTo \\
121  &                                   & \llbracket s'' \rrbracket
122\end{diagram}
123\end{displaymath}
124
125Call one step commuting diagram:
126
127\begin{displaymath}
128\begin{diagram}
129s & \rTo^{\text{one step of execution}} & s'   \\
130  & \rdTo                             & \dTo \\
131  &                                   & \llbracket s'' \rrbracket
132\end{diagram}
133\end{displaymath}
134
135\begin{displaymath}
136\begin{diagram}
137\mathtt{CALL}(\mathtt{id},\ \mathtt{args},\ \mathtt{dst},\ \mathtt{pc}),\ \mathtt{State}(\mathtt{Frame},\ \mathtt{Frames}) & \rTo & \mathtt{Call}(FINISH ME)
138\end{diagram}
139\end{displaymath}
140
141\begin{displaymath}
142\begin{array}{rcl}
143\mathtt{CALL}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc}) & \longrightarrow & \mathtt{CALL\_ID}(\mathtt{id}, \sigma'(\mathtt{args}), \sigma(\mathtt{dst}), \mathtt{pc}) \\
144\mathtt{RETURN}                                                      & \longrightarrow & \mathtt{RETURN} \\
145\end{array} 
146\end{displaymath}
147
148\begin{displaymath}
149\begin{array}{rcl}
150\sigma & : & \mathtt{register} \rightarrow \mathtt{list\ register} \\
151\sigma' & : & \mathtt{list\ register} \rightarrow \mathtt{list\ register}
152\end{array} 
153\end{displaymath}
154
155\section{The RTL to ERTL translation}
156\label{sect.rtl.ertl.translation}
157
158\begin{displaymath}
159\begin{diagram}
160        &                         & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket &                         & \\
161        & \ldTo^{\text{external}} &                                                                                               & \rdTo^{\text{internal}} & \\
162 \skull &                         &                                                                                               &                         & FINISH ME
163\end{diagram}
164\end{displaymath}
165
166\section{The ERTL to LTL translation}
167\label{sect.ertl.ltl.translation}
168
169\section{The LTL to LIN translation}
170\label{sect.ltl.lin.translation}
171
172We 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:
173\begin{displaymath}
174\mathtt{pc : label} \stackrel{\sigma}{\longrightarrow} \mathbb{N}
175\end{displaymath}
176
177The LTL to LIN translation pass also linearises the graph data structure into a list of instructions.
178Pseudocode for the linearisation process is as follows:
179
180\begin{lstlisting}
181let rec linearise graph visited required generated todo :=
182  match todo with
183  | l::todo ->
184    if l $\in$ visited then
185      let generated := generated $\cup\ \{$ Goto l $\}$ in
186      let required := required $\cup$ l in
187        linearise graph visited required generated todo
188    else
189      -- Get the instruction at label ``l'' in the graph
190      let lookup := graph(l) in
191      let generated := generated $\cup\ \{$ lookup $\}$ in
192      -- Find the successor of the instruction at label ``l'' in the graph
193      let successor := succ(l, graph) in
194      let todo := successor::todo in
195        linearise graph visited required generated todo
196  | []      -> (required, generated)
197\end{lstlisting}
198
199
200\section{The LIN to ASM and ASM to MCS-51 machine code translations}
201\label{sect.lin.asm.translation}
202
203The LIN to ASM translation step is trivial, being almost the identity function.
204The 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.
205
206The ASM to MCS-51 machine code translation step, and the required statements of correctness, are found in an unpublished manuscript attached to this document.
207
208\end{document}
Note: See TracBrowser for help on using the repository browser.