1 | \documentclass[11pt, epsf, a4wide]{article} |
---|
2 | |
---|
3 | \usepackage{../../style/cerco} |
---|
4 | |
---|
5 | \usepackage{amsfonts} |
---|
6 | \usepackage{amsmath} |
---|
7 | \usepackage{amssymb} |
---|
8 | \usepackage[english]{babel} |
---|
9 | \usepackage{graphicx} |
---|
10 | \usepackage[utf8x]{inputenc} |
---|
11 | \usepackage{listings} |
---|
12 | \usepackage{stmaryrd} |
---|
13 | \usepackage{url} |
---|
14 | |
---|
15 | \title{ |
---|
16 | INFORMATION AND COMMUNICATION TECHNOLOGIES\\ |
---|
17 | (ICT)\\ |
---|
18 | PROGRAMME\\ |
---|
19 | \vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}} |
---|
20 | |
---|
21 | \lstdefinelanguage{matita-ocaml} |
---|
22 | {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try}, |
---|
23 | morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct}, |
---|
24 | morekeywords={[3]type,of}, |
---|
25 | mathescape=true, |
---|
26 | } |
---|
27 | |
---|
28 | \lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false, |
---|
29 | keywordstyle=\color{red}\bfseries, |
---|
30 | keywordstyle=[2]\color{blue}, |
---|
31 | keywordstyle=[3]\color{blue}\bfseries, |
---|
32 | commentstyle=\color{green}, |
---|
33 | stringstyle=\color{blue}, |
---|
34 | showspaces=false,showstringspaces=false} |
---|
35 | |
---|
36 | \lstset{extendedchars=false} |
---|
37 | \lstset{inputencoding=utf8x} |
---|
38 | \DeclareUnicodeCharacter{8797}{:=} |
---|
39 | \DeclareUnicodeCharacter{10746}{++} |
---|
40 | \DeclareUnicodeCharacter{9001}{\ensuremath{\langle}} |
---|
41 | \DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}} |
---|
42 | |
---|
43 | \date{} |
---|
44 | \author{} |
---|
45 | |
---|
46 | \begin{document} |
---|
47 | |
---|
48 | \thispagestyle{empty} |
---|
49 | |
---|
50 | \vspace*{-1cm} |
---|
51 | \begin{center} |
---|
52 | \includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png} |
---|
53 | \end{center} |
---|
54 | |
---|
55 | \begin{minipage}{\textwidth} |
---|
56 | \maketitle |
---|
57 | \end{minipage} |
---|
58 | |
---|
59 | \vspace*{0.5cm} |
---|
60 | \begin{center} |
---|
61 | \begin{LARGE} |
---|
62 | \textbf{ |
---|
63 | Report n. D4.3\\ |
---|
64 | Formal semantics of intermediate languages |
---|
65 | } |
---|
66 | \end{LARGE} |
---|
67 | \end{center} |
---|
68 | |
---|
69 | \vspace*{2cm} |
---|
70 | \begin{center} |
---|
71 | \begin{large} |
---|
72 | Version 1.0 |
---|
73 | \end{large} |
---|
74 | \end{center} |
---|
75 | |
---|
76 | \vspace*{0.5cm} |
---|
77 | \begin{center} |
---|
78 | \begin{large} |
---|
79 | Main Authors:\\ |
---|
80 | Dominic P. Mulligan and Claudio Sacerdoti Coen |
---|
81 | \end{large} |
---|
82 | \end{center} |
---|
83 | |
---|
84 | \vspace*{\fill} |
---|
85 | |
---|
86 | \noindent |
---|
87 | Project Acronym: \cerco{}\\ |
---|
88 | Project full title: Certified Complexity\\ |
---|
89 | Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\ |
---|
90 | |
---|
91 | \clearpage |
---|
92 | \pagestyle{myheadings} |
---|
93 | \markright{\cerco{}, FP7-ICT-2009-C-243881} |
---|
94 | |
---|
95 | \newpage |
---|
96 | |
---|
97 | \vspace*{7cm} |
---|
98 | \paragraph{Abstract} |
---|
99 | We describe the encoding in the Calculus of Constructions of the semantics of the CerCo compiler's backend intermediate languages. |
---|
100 | The CerCo backend consists of five distinct languages: RTL, RTLntl, ERTL, LTL and LIN. |
---|
101 | We describe a process of heavy abstraction of the intermediate languages and their semantics. |
---|
102 | We hope that this process will ease the burden of Deliverable D4.4, the proof of correctness for the compiler. |
---|
103 | |
---|
104 | \newpage |
---|
105 | |
---|
106 | \tableofcontents |
---|
107 | |
---|
108 | \newpage |
---|
109 | |
---|
110 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
111 | % SECTION. % |
---|
112 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
113 | \section{Task} |
---|
114 | \label{sect.task} |
---|
115 | |
---|
116 | The Grant Agreement states that Task T4.3, entitled `Formal semantics of intermediate languages' has associated Deliverable D4.3, consisting of the following: |
---|
117 | \begin{quotation} |
---|
118 | Executable Formal Semantics of back-end intermediate languages: This prototype is the formal counterpart of deliverable D2.1 for the back end side of the compiler and validates it. |
---|
119 | \end{quotation} |
---|
120 | This report details our implementation of this deliverable. |
---|
121 | |
---|
122 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
123 | % SECTION. % |
---|
124 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
125 | \subsection{Connections with other deliverables} |
---|
126 | \label{subsect.connections.with.other.deliverables} |
---|
127 | |
---|
128 | Deliverable D4.3 enjoys a close relationship with three other deliverables, namely deliverables D2.2, D4.3 and D4.4. |
---|
129 | |
---|
130 | Deliverable D2.2, the O'Caml implementation of a cost preserving compiler for a large subset of the C programming language, is the basis upon which we have implemented the current deliverable. |
---|
131 | In particular, the architecture of the compiler, its intermediate languages and their semantics, and the overall implementation of the Matita encodings has been taken from the O'Caml compiler. |
---|
132 | Any variations from the O'Caml design are due to bugs identified in the prototype compiler during the Matita implementation, our identification of code that can be abstracted and made generic, or our use of Matita's much stronger type system to enforce invariants through the use of dependent types. |
---|
133 | |
---|
134 | Deliverable D4.2 can be seen as a `sister' deliverable to the deliverable reported on herein. |
---|
135 | In particular, where this deliverable reports on the encoding in the Calculus of Constructions of the backend semantics, D4.2 is the encoding in the Calculus of Constructions of the mutual translations of those languages. |
---|
136 | As a result, a substantial amount of Matita code is shared between the two deliverables. |
---|
137 | |
---|
138 | Deliverable D4.4, the backend correctness proofs, is the immediate successor of this deliverable. |
---|
139 | |
---|
140 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
141 | % SECTION. % |
---|
142 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
143 | \section{The backend intermediate languages' semantics in Matita} |
---|
144 | \label{sect.backend.intermediate.languages.semantics.matita} |
---|
145 | |
---|
146 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
147 | % SECTION. % |
---|
148 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
149 | \subsection{Abstracting related languages} |
---|
150 | \label{subsect.abstracting.related.languages} |
---|
151 | |
---|
152 | As mentioned in the report for Deliverable D4.2, a systematic process of abstraction, over the O'Caml code, has taken place in the Matita encoding. |
---|
153 | In particular, we have merged many of the syntaxes of the intermediate languages (i.e. RTL, ERTL, LTL and LIN) into a single `joint' syntax, which is parameterised by various types. |
---|
154 | Equivalent intermediate languages to those present in the O'Caml code can be recovered by specialising this joint structure. |
---|
155 | |
---|
156 | As mentioned in the report for Deliverable D4.2, there are a number of advantages that this process of abstraction brings, from code reuse to allowing us to get a clearer view of the intermediate languages and their structure. |
---|
157 | However, the semantics of the intermediate languages allow us to concretely demonstrate this improvement in clarity, by noting that the semantics of the LTL and the semantics of the LIN languages are identical. |
---|
158 | In particular, the semantics of both LTL and LIN are implemented in exactly the same way. |
---|
159 | The only difference between the two languages is how the next instruction to be interpreted is fetched. |
---|
160 | In LTL, this involves looking up in a graph, whereas in LTL, this involves fetching from a list of instructions. |
---|
161 | |
---|
162 | As a result, we see that the semantics of LIN and LTL are both instances of a single, more general language that is parametric in how the next instruction is fetched. |
---|
163 | Furthermore, any prospective proof that the semantics of LTL and LIN are identical is not almost trivial, saving a deal of work in Deliverable D4.4. |
---|
164 | |
---|
165 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
166 | % SECTION. % |
---|
167 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
168 | \subsection{Type parameters, and their purpose} |
---|
169 | \label{subsect.type.parameters.their.purpose} |
---|
170 | |
---|
171 | We mentioned in the Deliverable D4.2 report that all joint languages are parameterised by a number of types, which are later specialised to each distinct intermediate language. |
---|
172 | As this parameterisation process is also dependent on designs decisions in the language semantics, we have so far held off summarising the role of each parameter. |
---|
173 | We now summarise what each parameter is. |
---|
174 | |
---|
175 | \begin{lstlisting} |
---|
176 | record params__: Type[1] ≝ |
---|
177 | { |
---|
178 | acc_a_reg: Type[0]; |
---|
179 | acc_b_reg: Type[0]; |
---|
180 | dpl_reg: Type[0]; |
---|
181 | dph_reg: Type[0]; |
---|
182 | pair_reg: Type[0]; |
---|
183 | generic_reg: Type[0]; |
---|
184 | call_args: Type[0]; |
---|
185 | call_dest: Type[0]; |
---|
186 | extend_statements: Type[0] |
---|
187 | }. |
---|
188 | \end{lstlisting} |
---|
189 | We summarise what these types mean: |
---|
190 | \begin{center} |
---|
191 | \begin{tabular*}{\textwidth}{p{4cm}p{11cm}} |
---|
192 | Type & Explanation \\ |
---|
193 | \hline |
---|
194 | \texttt{acc\_a\_reg} & The type of the accumulator A register. In some languages this is implemented as the hardware accumulator, whereas in others this is a pseudoregister.\\ |
---|
195 | \texttt{acc\_b\_reg} & Similar to the accumulator A field, but for the processor's auxilliary accumulator, B. \\ |
---|
196 | \texttt{dpl\_reg} & \\ |
---|
197 | \texttt{dph\_reg} & \\ |
---|
198 | \texttt{pair\_reg} & \\ |
---|
199 | \texttt{generic\_reg} & \\ |
---|
200 | \texttt{call\_args} & \\ |
---|
201 | \texttt{call\_dest} & \\ |
---|
202 | \texttt{extend\_statements} & |
---|
203 | \end{tabular*} |
---|
204 | \end{center} |
---|
205 | |
---|
206 | As mentioned in the report for Deliverable D4.2, the record \texttt{params\_\_} is enough to be able to specify the instructions of the joint languages: |
---|
207 | \begin{lstlisting} |
---|
208 | inductive joint_instruction (p: params__) (globals: list ident): Type[0] := |
---|
209 | | COMMENT: String → joint_instruction p globals |
---|
210 | | COST_LABEL: costlabel → joint_instruction p globals |
---|
211 | ... |
---|
212 | \end{lstlisting} |
---|
213 | |
---|
214 | We extend \texttt{params\_\_} with a type corresponding to labels, \texttt{succ}, obtaining a new record type of parameters called \texttt{params\_}: |
---|
215 | \begin{lstlisting} |
---|
216 | record params_: Type[1] ≝ |
---|
217 | { |
---|
218 | pars__ :> params__; |
---|
219 | succ: Type[0] |
---|
220 | }. |
---|
221 | \end{lstlisting} |
---|
222 | The type \texttt{succ} corresponds to labels, in the case of control flow graph based languages, or is instantiated to the unit type for the linearised language, LIN. |
---|
223 | Using \texttt{param\_} we can define statements of the joint language: |
---|
224 | \begin{lstlisting} |
---|
225 | inductive joint_statement (p:params_) (globals: list ident): Type[0] := |
---|
226 | | sequential: joint_instruction p globals → succ p → joint_statement p globals |
---|
227 | | GOTO: label → joint_statement p globals |
---|
228 | | RETURN: joint_statement p globals. |
---|
229 | \end{lstlisting} |
---|
230 | Note that in the joint language, instructions are `linear', in that they have an immediate successor. |
---|
231 | Statements, on the other hand, consist of either a linear instruction, or a \texttt{GOTO} or \texttt{RETURN} statement, both of which can jump to an arbitrary place in the program. |
---|
232 | |
---|
233 | For the semantics, we need further parametererised types. |
---|
234 | In particular, we parameterise the result and parameter type of an internal function call in \texttt{params0}: |
---|
235 | \begin{lstlisting} |
---|
236 | record params0: Type[1] ≝ |
---|
237 | { pars__' :> params__ |
---|
238 | ; resultT: Type[0] |
---|
239 | ; paramsT: Type[0] |
---|
240 | }. |
---|
241 | \end{lstlisting} |
---|
242 | We further extend \texttt{params0} with a type for local variables in internal function calls: |
---|
243 | \begin{lstlisting} |
---|
244 | record params1 : Type[1] ≝ |
---|
245 | { pars0 :> params0 |
---|
246 | ; localsT: Type[0] |
---|
247 | }. |
---|
248 | \end{lstlisting} |
---|
249 | |
---|
250 | \begin{lstlisting} |
---|
251 | record params (globals: list ident): Type[1] ≝ |
---|
252 | { succ_ : Type[0] |
---|
253 | ; pars1 :> params1 |
---|
254 | ; codeT: Type[0] |
---|
255 | ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals) |
---|
256 | }. |
---|
257 | \end{lstlisting} |
---|
258 | |
---|
259 | \begin{lstlisting} |
---|
260 | definition graph_params_: params__ $\rightarrow$ params_ := |
---|
261 | $\lambda$pars__. mk_params_ pars__ label. |
---|
262 | \end{lstlisting} |
---|
263 | |
---|
264 | \begin{lstlisting} |
---|
265 | record joint_internal_function (globals: list ident) (p:params globals) : Type[0] := |
---|
266 | { joint_if_luniverse: universe LabelTag; (*CSC: used only for compilation*) |
---|
267 | joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*) |
---|
268 | (* joint_if_sig: signature; -- dropped in front end *) |
---|
269 | joint_if_result : resultT p; |
---|
270 | joint_if_params : paramsT p; |
---|
271 | joint_if_locals : localsT p; |
---|
272 | (*CSC: XXXXX stacksize unused for LTL-...*) |
---|
273 | joint_if_stacksize: nat; |
---|
274 | joint_if_code : codeT … p; |
---|
275 | (*CSC: XXXXX entry unused for LIN, but invariant in that case... *) |
---|
276 | joint_if_entry : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?; |
---|
277 | (*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *) |
---|
278 | joint_if_exit : $\Sigma$l: label. lookup … joint_if_code l ≠ None ? |
---|
279 | }. |
---|
280 | \end{lstlisting} |
---|
281 | |
---|
282 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
283 | % SECTION. % |
---|
284 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
285 | \subsection{Use of monads} |
---|
286 | \label{subsect.use.of.monads} |
---|
287 | |
---|
288 | Monads are a categorical notion that have recently gained an amount of traction in functional programming circles. |
---|
289 | In particular, it was noted by Moggi that monads could be used to sequence \emph{effectful} computations in a pure manner. |
---|
290 | Here, `effectful computations' cover a lot of ground, from writing to files, generating fresh names, or updating an ambient notion of state. |
---|
291 | |
---|
292 | In the semantics of both front and backend intermediate languages, we make use of monads. |
---|
293 | In particular, we make use of two forms of monad: |
---|
294 | \begin{enumerate} |
---|
295 | \item |
---|
296 | An `error monad', which signals that a computation either has completed successfully, or returns with an error message. |
---|
297 | The sequencing operation of the error monad ensures that the result of chained computations in return the error message of the first failed computation. |
---|
298 | This monad is used extensively in the semantics to signal a state which cannot be recovered from. |
---|
299 | For instance, in the semantics of RTLabs, we make use of the error monad to signal bad final states: |
---|
300 | \begin{lstlisting} |
---|
301 | XXX better example |
---|
302 | \end{lstlisting} |
---|
303 | \item |
---|
304 | An `IO' monad, signalling the emission or reading of data to some external location or memory address. |
---|
305 | Here, the monads sequencing operation ensures that emissions and reads are maintained in the correct order (i.e. it maintains a `trace', or ordered sequence of IO events). |
---|
306 | Most functions in the intermediate language semantics fall into the IO monad. |
---|
307 | \end{enumerate} |
---|
308 | This monadic infrastructure is shared between the frontend and backend languages. |
---|
309 | |
---|
310 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
311 | % SECTION. % |
---|
312 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
313 | \section{Future work} |
---|
314 | \label{sect.future.work} |
---|
315 | |
---|
316 | A few small axioms remain to be closed. |
---|
317 | These relate to fetching the next instruction to be interpreted from the control flow graph, or linearised representation, of the language. |
---|
318 | Closing these axioms should not be a problem. |
---|
319 | No further work remains, aside from `tidying up' the code. |
---|
320 | |
---|
321 | \newpage |
---|
322 | |
---|
323 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
324 | % SECTION. % |
---|
325 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
326 | \section{Code listing} |
---|
327 | \label{sect.code.listing} |
---|
328 | |
---|
329 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
330 | % SECTION. % |
---|
331 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
332 | \subsection{Listing of files} |
---|
333 | \label{subsect.listing.files} |
---|
334 | |
---|
335 | Semantics specific files (files relating to language translations ommitted): |
---|
336 | \begin{center} |
---|
337 | \begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}} |
---|
338 | Title & Description \\ |
---|
339 | \hline |
---|
340 | \texttt{RTLabs/syntax.ma} & The syntax of RTLabs \\ |
---|
341 | \texttt{RTLabs/semantics.ma} & The semantics of RTLabs \\ |
---|
342 | \texttt{joint/Joint.ma} & Abstracted syntax for backend languages \\ |
---|
343 | \texttt{joint/SemanticUtils.ma} & Generic utilities used in the semantics of all `joint' intermediate languages \\ |
---|
344 | \texttt{RTL/RTL.ma} & The syntax of RTL \\ |
---|
345 | \texttt{RTL/semantics.ma} & The semantics of RTL \\ |
---|
346 | \texttt{ERTL/ERTL.ma} & The syntax of ERTL \\ |
---|
347 | \texttt{ERTL/semantics.ma} & The semantics of ERTL \\ |
---|
348 | \texttt{LTL/LTL.ma} & The syntax of LTL \\ |
---|
349 | \texttt{LTL/semantics.ma} & The semantics of LTL \\ |
---|
350 | \texttt{LIN/LIN.ma} & The syntax of LIN \\ |
---|
351 | \texttt{LIN/semantics.ma} & The semantics of LIN |
---|
352 | \end{tabular*} |
---|
353 | \end{center} |
---|
354 | |
---|
355 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
356 | % SECTION. % |
---|
357 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
358 | \subsection{Listing of important functions and axioms} |
---|
359 | \label{subsect.listing.important.functions.axioms} |
---|
360 | |
---|
361 | We list some important functions and axioms in the backend semantics: |
---|
362 | |
---|
363 | \end{document} |
---|