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

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

some changes to the report

File size: 6.2 KB
Line 
1\documentclass[a4paper, 10pt]{article}
2
3\usepackage{a4wide}
4\usepackage{amsfonts}
5\usepackage{amsmath}
6\usepackage{amssymb}
7\usepackage[english]{babel}
8\usepackage{diagrams}
9\usepackage[colorlinks]{hyperref}
10\usepackage{microtype}
11\usepackage{skull}
12\usepackage{stmaryrd}
13
14\title{Proof outline for the correctness of the CerCo compiler}
15\date{\today}
16\author{The CerCo team}
17
18\begin{document}
19
20\maketitle
21
22\section{Introduction}
23\label{sect.introduction}
24
25\section{The RTLabs to RTL translation}
26\label{sect.rtlabs.rtl.translation}
27
28% dpm: type system and casting load (???)
29We require a map, $\sigma$, between \texttt{Values} of the front-end memory model to lists of \texttt{BEValues} of the back-end memory model:
30
31\begin{displaymath}
32\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
33\end{displaymath}
34
35We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}.
36
37\begin{displaymath}
38\mathtt{Mem}\ \alpha = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \alpha)
39\end{displaymath}
40
41where
42
43\begin{displaymath}
44\mathtt{Block} ::= \mathtt{Region} \cup \mathtt{ID}
45\end{displaymath}
46
47\begin{displaymath}
48\mathtt{BEMem} = \mathtt{Mem} \mathtt{Value}
49\end{displaymath}
50
51\begin{displaymath}
52\mathtt{Address} = \mathtt{BEValue} \times  \mathtt{BEValue} \\
53\end{displaymath}
54
55\begin{displaymath}
56\mathtt{Mem} = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \mathtt{Cont} \mid \mathtt{Value} \times \mathtt{Size} \mid \mathtt{null})
57\end{displaymath}
58
59\begin{center}
60\begin{picture}(2, 2)
61% picture of sigma mapping memory to memory
62TODO
63\end{picture}
64\end{center}
65
66\begin{displaymath}
67\mathtt{load}\ s\ a\ M = \mathtt{Some}\ v \rightarrow \forall i \leq s.\ \mathtt{load}\ s\ (a + i)\ \sigma(M) = \mathtt{Some}\ v_i
68\end{displaymath}
69
70\begin{displaymath}
71\sigma(\mathtt{store}\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(M)
72\end{displaymath}
73
74\begin{displaymath}
75\begin{array}{rll}
76\mathtt{State} & ::=  & (\mathtt{State} : \mathtt{Frame}^* \times \mathtt{Frame} \\
77               & \mid & \mathtt{Call} : \mathtt{Frame}^* \times \mathtt{Args} \times \mathtt{Return} \times \mathtt{Fun} \\
78               & \mid & \mathtt{Return} : \mathtt{Frame}^* \times \mathtt{Value} \times \mathtt{Return}) \times \mathtt{Mem}
79\end{array}
80\end{displaymath}
81
82\begin{displaymath}
83\mathtt{State} ::= \mathtt{Frame}^* \times \mathtt{PC} \times \mathtt{SP} \times \mathtt{ISP} \times \mathtt{CARRY} \times \mathtt{REGS}
84\end{displaymath}
85
86\begin{displaymath}
87\mathtt{State} \stackrel{\sigma}{\longrightarrow} \mathtt{State}
88\end{displaymath}
89
90\begin{displaymath}
91\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}))
92\end{displaymath}
93
94\begin{displaymath}
95\sigma(\mathtt{Return}(-)) \longrightarrow \sigma \circ \text{return one step}
96\end{displaymath}
97
98\begin{displaymath}
99\sigma(\mathtt{Call}(-)) \longrightarrow \sigma \circ \text{call one step}
100\end{displaymath}
101
102Return one step commuting diagram:
103
104\begin{displaymath}
105\begin{diagram}
106s & \rTo^{\text{one step of execution}} & s'   \\
107  & \rdTo                             & \dTo \\
108  &                                   & \llbracket s'' \rrbracket
109\end{diagram}
110\end{displaymath}
111
112Call one step commuting diagram:
113
114\begin{displaymath}
115\begin{diagram}
116s & \rTo^{\text{one step of execution}} & s'   \\
117  & \rdTo                             & \dTo \\
118  &                                   & \llbracket s'' \rrbracket
119\end{diagram}
120\end{displaymath}
121
122\begin{displaymath}
123\begin{diagram}
124\mathtt{CALL}(\mathtt{id},\ \mathtt{args},\ \mathtt{dst},\ \mathtt{pc}),\ \mathtt{State}(\mathtt{Frame},\ \mathtt{Frames}) & \rTo & \mathtt{Call}(FINISH ME)
125\end{diagram}
126\end{displaymath}
127
128\begin{displaymath}
129\begin{array}{rcl}
130\mathtt{CALL}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc}) & \longrightarrow & \mathtt{CALL\_ID}(\mathtt{id}, \sigma'(\mathtt{args}), \sigma(\mathtt{dst}), \mathtt{pc}) \\
131\mathtt{RETURN}                                                      & \longrightarrow & \mathtt{RETURN} \\
132\end{array} 
133\end{displaymath}
134
135\begin{displaymath}
136\begin{array}{rcl}
137\sigma & : & \mathtt{register} \rightarrow \mathtt{list\ register} \\
138\sigma' & : & \mathtt{list\ register} \rightarrow \mathtt{list\ register}
139\end{array} 
140\end{displaymath}
141
142\section{The RTL to ERTL translation}
143\label{sect.rtl.ertl.translation}
144
145\begin{displaymath}
146\begin{diagram}
147        &                         & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket &                         & \\
148        & \ldTo^{\text{external}} &                                                                                               & \rdTo^{\text{internal}} & \\
149 \skull &                         &                                                                                               &                         & FINISH ME
150\end{diagram}
151\end{displaymath}
152
153\section{The ERTL to LTL translation}
154\label{sect.ertl.ltl.translation}
155
156\section{The LTL to LIN translation}
157\label{sect.ltl.lin.translation}
158
159We 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:
160\begin{displaymath}
161\mathtt{pc : label} \stackrel{\sigma}{\longrightarrow} \mathbb{N}
162\end{displaymath}
163
164The linerisation process is as follows:
165
166\begin{enumerate}
167\item
168Perform a previsit of the graph
169\end{enumerate}
170
171
172\section{The LIN to ASM and ASM to MCS-51 machine code translations}
173\label{sect.lin.asm.translation}
174
175The LIN to ASM translation step is trivial, being almost the identity function.
176The 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.
177
178The ASM to MCS-51 machine code translation step, and the required statements of correctness, are found in an unpublished manuscript attached to this document.
179
180\end{document}
Note: See TracBrowser for help on using the repository browser.