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

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

added skull.sty for daemon (skull) symbol

File size: 5.4 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\begin{displaymath}
143\begin{diagram}
144        &                         & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket &                         & \\
145        & \ldTo^{\text{external}} &                                                                                               & \rdTo^{\text{internal}} & \\
146 \skull &                         &                                                                                               & 
147\end{diagram}
148\end{displaymath}
149
150\section{The RTL to ERTL translation}
151\label{sect.rtl.ertl.translation}
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
159\section{The LIN to ASM translation}
160\label{sect.lin.asm.translation}
161
162\section{The ASM to MCS-51 machine code translation}
163\label{sect.asm.mcs-51.machine.code.translation}
164
165\end{document}
Note: See TracBrowser for help on using the repository browser.