source: Deliverables/D4.2-4.3/reports/D4-3.tex @ 1407

Last change on this file since 1407 was 1407, checked in by mulligan, 9 years ago

almost finished

File size: 25.7 KB
Line 
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{
16INFORMATION AND COMMUNICATION TECHNOLOGIES\\
17(ICT)\\
18PROGRAMME\\
19\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
20
21\lstdefinelanguage{matita-ocaml}
22  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,let,in,rec,match,return,with,Type,try},
23   morekeywords={[2]whd,normalize,elim,cases,destruct},
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{
63Report n. D4.3\\
64Formal semantics of intermediate languages
65}
66\end{LARGE} 
67\end{center}
68
69\vspace*{2cm}
70\begin{center}
71\begin{large}
72Version 1.0
73\end{large}
74\end{center}
75
76\vspace*{0.5cm}
77\begin{center}
78\begin{large}
79Main Authors:\\
80Dominic P. Mulligan and Claudio Sacerdoti Coen
81\end{large}
82\end{center}
83
84\vspace*{\fill}
85
86\noindent
87Project Acronym: \cerco{}\\
88Project full title: Certified Complexity\\
89Proposal/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}
99We describe the encoding in the Calculus of Constructions of the semantics of the CerCo compiler's backend intermediate languages.
100The CerCo backend consists of five distinct languages: RTL, RTLntl, ERTL, LTL and LIN.
101We describe a process of heavy abstraction of the intermediate languages and their semantics.
102We 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
116The 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}
118Executable 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}
120This 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
128Deliverable D4.3 enjoys a close relationship with three other deliverables, namely deliverables D2.2, D4.3 and D4.4.
129
130Deliverable 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.
131In 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.
132Any 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
134Deliverable D4.2 can be seen as a `sister' deliverable to the deliverable reported on herein.
135In 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.
136As a result, a substantial amount of Matita code is shared between the two deliverables.
137
138Deliverable 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
152As 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.
153In 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.
154Equivalent intermediate languages to those present in the O'Caml code can be recovered by specialising this joint structure.
155
156As 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.
157However, 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.
158In particular, the semantics of both LTL and LIN are implemented in exactly the same way.
159The only difference between the two languages is how the next instruction to be interpreted is fetched.
160In LTL, this involves looking up in a graph, whereas in LTL, this involves fetching from a list of instructions.
161
162As 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.
163Furthermore, 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
171We 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.
172As 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
174We begin the abstraction process with the \texttt{params\_\_} record.
175This holds the types of the representations of the different register varieties in the intermediate languages:
176\begin{lstlisting}
177record params__: Type[1] ≝
178{
179  acc_a_reg: Type[0];
180  acc_b_reg: Type[0];
181  dpl_reg: Type[0];
182  dph_reg: Type[0];
183  pair_reg: Type[0];
184  generic_reg: Type[0];
185  call_args: Type[0];
186  call_dest: Type[0];
187  extend_statements: Type[0]
188}.
189\end{lstlisting}
190We summarise what these types mean, and how they are used in both the semantics and the translation process:
191\begin{center}
192\begin{tabular*}{\textwidth}{p{4cm}p{11cm}}
193Type & Explanation \\
194\hline
195\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.\\
196\texttt{acc\_b\_reg} & Similar to the accumulator A field, but for the processor's auxilliary accumulator, B. \\
197\texttt{dpl\_reg} & The type of the representation of the low eight bit register of the MCS-51's single 16 bit register, DPL.  Can be either a pseudoregister or the hardware DPL register. \\
198\texttt{dph\_reg} & Similar to the DPL register but for the eight high bits of the 16-bit register. \\
199\texttt{pair\_reg} & Various different `move' instructions have been merged into a single move instruction in the joint language.  A value can either be moved to or from the accumulator in some languages, or moved to and from an arbitrary pseudoregister in others.  This type encodes how we should move data around the registers and accumulators. \\
200\texttt{generic\_reg} & The representation of generic registers (i.e. those that are not devoted to a specific task). \\
201\texttt{call\_args} & The number of arguments to a function.  For some languages this is irrelevant. \\
202\texttt{call\_dest} & \\
203\texttt{extend\_statements} & Instructions that are specific to a particular intermediate language, and which cannot be abstracted into the joint language.
204\end{tabular*}
205\end{center}
206
207As 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:
208\begin{lstlisting}
209inductive joint_instruction (p: params__) (globals: list ident): Type[0] :=
210  | COMMENT: String → joint_instruction p globals
211  | COST_LABEL: costlabel → joint_instruction p globals
212  ...
213\end{lstlisting}
214
215We extend \texttt{params\_\_} with a type corresponding to labels, \texttt{succ}, obtaining a new record type of parameters called \texttt{params\_}:
216\begin{lstlisting}
217record params_: Type[1] ≝
218{
219  pars__ :> params__;
220  succ: Type[0]
221}.
222\end{lstlisting}
223The 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.
224Using \texttt{param\_} we can define statements of the joint language:
225\begin{lstlisting}
226inductive joint_statement (p:params_) (globals: list ident): Type[0] :=
227  | sequential: joint_instruction p globals → succ p → joint_statement p globals
228  | GOTO: label → joint_statement p globals
229  | RETURN: joint_statement p globals.
230\end{lstlisting}
231Note that in the joint language, instructions are `linear', in that they have an immediate successor.
232Statements, 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.
233
234For the semantics, we need further parametererised types.
235In particular, we parameterise the result and parameter type of an internal function call in \texttt{params0}:
236\begin{lstlisting}
237record params0: Type[1] ≝
238 { pars__' :> params__
239 ; resultT: Type[0]
240 ; paramsT: Type[0]
241 }.
242\end{lstlisting}
243We further extend \texttt{params0} with a type for local variables in internal function calls:
244\begin{lstlisting}
245record params1 : Type[1] ≝
246 { pars0 :> params0
247 ; localsT: Type[0]
248 }.
249\end{lstlisting}
250Again, we expand our parameters with types corresponding to the code representation (either a control flow graph or a list of statements).
251Further, we hypothesise a generic method for looking up the next instruction in the graph, called \texttt{lookup}.
252Note that \texttt{lookup} may fail, and returns an \texttt{option} type:
253\begin{lstlisting}
254record params (globals: list ident): Type[1] ≝
255 { succ_ : Type[0]
256 ; pars1 :> params1
257 ; codeT: Type[0]
258 ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals)
259 }.
260\end{lstlisting}
261We now have what we need to define internal functions for the joint language.
262The first two `universe' fields are only used in the compilation process, for generating fresh names, and do not affect the semantics.
263The rest of the fields affect both compilation and semantics.
264In particular, we have parameterised result types, function parameter types and the type of local variables.
265Note also that we have lifted the hypothesised \texttt{lookup} function from \texttt{params} into a dependent sigma type, which combines a label (the entry and exit points of the control flow graph or list) combined with a proof that the label is in the graph structure:
266\begin{lstlisting}
267record joint_internal_function (globals: list ident) (p:params globals) : Type[0] :=
268{
269  joint_if_luniverse: universe LabelTag;
270  joint_if_runiverse: universe RegisterTag;
271  joint_if_result   : resultT p;
272  joint_if_params   : paramsT p;
273  joint_if_locals   : localsT p;
274  joint_if_stacksize: nat;
275  joint_if_code     : codeT … p;
276  joint_if_entry    : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?;
277  joint_if_exit     : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?
278}.
279\end{lstlisting}
280Naturally, a question arises as to why we have chosen to split up the parameterisation into so many intermediate records, each slightly extending earlier ones.
281The reason is because some intermediate languages share a host of parameters, and only differ on some others.
282For instance, in instantiating the ERTL language, certain parameters are shared with RTL, whilst others are ERTL specific:
283\begin{lstlisting}
284...
285definition ertl_params__: params__ :=
286 mk_params__ register register register register (move_registers × move_registers)
287  register nat unit ertl_statement_extension.
288...
289definition ertl_params1: params1 := rtl_ertl_params1 ertl_params0.
290definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0.
291...
292definition ertl_statement := joint_statement ertl_params_.
293
294definition ertl_internal_function :=
295  $\lambda$globals.joint_internal_function … (ertl_params globals).
296\end{lstlisting}
297Here, \texttt{rtl\_ertl\_params1} are the common parameters of the ERTL and RTL languages:
298\begin{lstlisting}
299definition rtl_ertl_params1 := $\lambda$pars0. mk_params1 pars0 (list register).
300\end{lstlisting}
301
302The record \texttt{more\_sem\_params} bundles together functions that store and retrieve values in various forms of register:
303\begin{lstlisting}
304record more_sem_params (p:params_): Type[1] :=
305{
306  framesT: Type[0];
307  regsT: Type[0];
308  succ_pc: succ p → address → res address;
309  greg_store_: generic_reg p → beval → regsT → res regsT;
310  greg_retrieve_: regsT → generic_reg p → res beval;
311  acca_store_: acc_a_reg p → beval → regsT → res regsT;
312  acca_retrieve_: regsT → acc_a_reg p → res beval;
313  accb_store_: acc_b_reg p → beval → regsT → res regsT;
314  accb_retrieve_: regsT → acc_b_reg p → res beval;
315  dpl_store_: dpl_reg p → beval → regsT → res regsT;
316  dpl_retrieve_: regsT → dpl_reg p → res beval;
317  dph_store_: dph_reg p → beval → regsT → res regsT;
318  dph_retrieve_: regsT → dph_reg p → res beval;
319  pair_reg_move_: regsT → pair_reg p → res regsT;
320  pointer_of_label: label → $\Sigma$p:pointer. ptype p = Code
321}.
322\end{lstlisting}
323For instance, \texttt{greg\_store\_} and \texttt{greg\_retrieve\_} store and retrieve values from a generic register, respectively.
324Similarly, \texttt{pair\_reg\_move} implements the generic move instruction of the joint language.
325Here \texttt{framesT} is the type of stack frames.
326
327We extend \texttt{more\_sem\_params} with yet more parameters via \texttt{more\_sem\_params2}:
328\begin{lstlisting}
329record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] :=
330{
331  more_sparams1 :> more_sem_params p;
332  fetch_statement:
333    genv … p → state (mk_sem_params … more_sparams1) →
334    res (joint_statement (mk_sem_params … more_sparams1) globals);
335  ...
336  save_frame:
337    address → nat → paramsT … p → call_args p → call_dest p →
338    state (mk_sem_params … more_sparams1) →
339    res (state (mk_sem_params … more_sparams1));
340  pop_frame:
341    genv globals p → state (mk_sem_params … more_sparams1) →
342    res ((state (mk_sem_params … more_sparams1)));
343  ...
344  set_result:
345    list val → state (mk_sem_params … more_sparams1) →
346    res (state (mk_sem_params … more_sparams1));
347  exec_extended:
348    genv globals p → extend_statements (mk_sem_params … more_sparams1) →
349    succ p → state (mk_sem_params … more_sparams1) →
350    IO io_out io_in (trace × (state (mk_sem_params … more_sparams1)))
351 }.
352\end{lstlisting}
353Here, \texttt{fetch\_statement} fetches the next statement to be executed, \texttt{save\_frame} and \texttt{pop\_frame} manipulate stack frames, \texttt{set\_result} saves the result of the function computation, and \texttt{exec\_extended} is a function that executes the extended statements, peculiar to each individual intermediate language.
354
355We bundle \texttt{params} and \texttt{sem\_params} together into a single record.
356This will be used in the function \texttt{eval\_statement} which executes a single statement of the joint language:
357\begin{lstlisting}
358record sem_params2 (globals: list ident): Type[1] :=
359{
360  p2 :> params globals;
361  more_sparams2 :> more_sem_params2 globals p2
362}.
363\end{lstlisting}
364\noindent
365The \texttt{state} record holds the current state of the interpreter:
366\begin{lstlisting}
367record state (p: sem_params): Type[0] :=
368{
369  st_frms: framesT ? p;
370  pc: address;
371  sp: pointer;
372  carry: beval;
373  regs: regsT ? p;
374  m: bemem
375}.
376\end{lstlisting}
377Here \texttt{st\_frms} represent stack frames, \texttt{pc} the program counter, \texttt{sp} the stack pointer, \texttt{carry} the carry flag, \texttt{regs} the generic registers and \texttt{m} external RAM.
378We use the function \texttt{eval\_statement} to evaluate a single joint statement:
379\begin{lstlisting}
380definition eval_statement:
381  ∀globals: list ident.∀p:sem_params2 globals.
382    genv globals p → state p → IO io_out io_in (trace × (state p)) :=
383...
384\end{lstlisting}
385We examine the type of this function.
386Note that it returns a monadic action, \texttt{IO}, denoting that it may have an IO \emph{side effect}, where the program reads or writes to some external device or memory address.
387Monads and their use are further discussed in Subsection~\ref{subsect.use.of.monads}.
388Further, the function returns a new state, updated by the single step of execution of the program.
389Finally, a \emph{trace} is also returned, which records the trace of cost labels that the program passes through, in order to calculate the cost model for the CerCo compiler.
390
391%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
392% SECTION.                                                                    %
393%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
394\subsection{Use of monads}
395\label{subsect.use.of.monads}
396
397Monads are a categorical notion that have recently gained an amount of traction in functional programming circles.
398In particular, it was noted by Moggi that monads could be used to sequence \emph{effectful} computations in a pure manner.
399Here, `effectful computations' cover a lot of ground, from writing to files, generating fresh names, or updating an ambient notion of state.
400
401A monad can be characterised by the following:
402\begin{itemize}
403\item
404A data type, $M$.
405For instance, the \texttt{option} type in O'Caml or Matita.
406\item
407A way to `inject' or `lift' pure values into this data type (usually called \texttt{return}).
408We call this function \texttt{return} and say that it must have type $\alpha \rightarrow M \alpha$, where $M$ is the name of the monad.
409In our example, the `lifting' function for the \texttt{option} monad can be implemented as:
410\begin{lstlisting}
411let return x = Some x
412\end{lstlisting}
413\item
414A way to `sequence' monadic functions together, to form another monadic function, usually called \texttt{bind}.
415Bind has type $M \alpha \rightarrow (\alpha \rightarrow M \beta) \rightarrow M \beta$.
416We can see that bind `unpacks' a monadic value, applies a function after unpacking, and `repacks' the new value in the monad.
417In our example, the sequencing function for the \texttt{option} monad can be implemented as:
418\begin{lstlisting}
419let bind o f =
420  match o with
421    None -> None
422    Some s -> f s
423\end{lstlisting}
424\item
425A series of algebraic laws that relate \texttt{return} and \texttt{bind}, ensuring that the sequencing operation `does the right thing' by retaining the order of effects.
426These \emph{monad laws} should also be useful in reasoning about monadic computations in the proof of correctness of the compiler.
427\end{itemize}
428In the semantics of both front and backend intermediate languages, we make use of monads.
429This monadic infrastructure is shared between the frontend and backend languages.
430
431In particular, an `IO' monad, signalling the emission or reading of data to some external location or memory address, is heavily used in the semantics of the intermediate languages.
432Here, the monad's sequencing operation ensures that emissions and reads are maintained in the correct order.
433Most functions in the intermediate language semantics fall into the IO monad.
434In particular, we have already seen how the \texttt{eval\_statement} function of the joint language is monadic, with type:
435\begin{lstlisting}
436definition eval_statement:
437  ∀globals: list ident.∀p:sem_params2 globals.
438    genv globals p → state p → IO io_out io_in (trace × (state p)) :=
439...
440\end{lstlisting}
441If we in the body of \texttt{eval\_statement}, we may also see how the monad sequences effects.
442For instance, in the case for the \texttt{LOAD} statement, we have the following:
443\begin{lstlisting}
444definition eval_statement:
445  ∀globals: list ident. ∀p:sem_params2 globals.
446    genv globals p → state p → IO io_out io_in (trace × (state p)) :=
447  $\lambda$globals, p, ge, st.
448  ...
449  match s with
450  | LOAD dst addrl addrh ⇒
451    ! vaddrh $\leftarrow$ dph_retrieve … st addrh;
452    ! vaddrl $\leftarrow$ dpl_retrieve … st addrl;
453    ! vaddr $\leftarrow$ pointer_of_address 〈vaddrl,vaddrh〉;
454    ! v $\leftarrow$ opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
455    ! st $\leftarrow$ acca_store p … dst v st;
456    ! st $\leftarrow$ next … l st ;
457      ret ? $\langle$E0, st$\rangle$
458\end{lstlisting}
459Here, we employ a certain degree of syntactic sugaring.
460The syntax
461\begin{lstlisting}
462  ...
463! vaddrh $\leftarrow$ dph_retrieve … st addrh;
464! vaddrl $\leftarrow$ dpl_retrieve … st addrl;
465  ...
466\end{lstlisting}
467is sugaring for the \texttt{IO} monad's binding operation.
468We can expand this sugaring to the following much more verbose code:
469\begin{lstlisting}
470  ...
471  bind (dph_retrieve … st addrh) ($\lambda$vaddrh. bind (dpl_retrieve … st addrl)
472    ($\lambda$vaddrl. ...))
473\end{lstlisting}
474Note also that the function \texttt{ret} is implementing the `lifting', or return function of the \texttt{IO} monad.
475
476We believe the sugaring for the monadic bind operation makes the program much more readable, and therefore easier to reason about.
477In particular, note that the functions \texttt{dph\_retrieve}, \texttt{pointer\_of\_address}, \texttt{acca\_store} and \texttt{next} are all monadic.
478The function \texttt{opt\_to\_res} is also --- this is a `utility' function that lifts an option type into the \texttt{IO} monad.
479
480%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
481% SECTION.                                                                    %
482%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
483\section{Future work}
484\label{sect.future.work}
485
486A few small axioms remain to be closed.
487These relate to fetching the next instruction to be interpreted from the control flow graph, or linearised representation, of the language.
488Closing these axioms should not be a problem.
489No further work remains, aside from `tidying up' the code.
490
491\newpage
492
493%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
494% SECTION.                                                                    %
495%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
496\section{Code listing}
497\label{sect.code.listing}
498
499%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
500% SECTION.                                                                    %
501%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
502\subsection{Listing of files}
503\label{subsect.listing.files}
504
505Semantics specific files (files relating to language translations ommitted):
506\begin{center}
507\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
508Title & Description \\
509\hline
510\texttt{RTLabs/syntax.ma} & The syntax of RTLabs \\
511\texttt{RTLabs/semantics.ma} & The semantics of RTLabs \\
512\texttt{joint/Joint.ma} & Abstracted syntax for backend languages \\
513\texttt{joint/SemanticUtils.ma} & Generic utilities used in the semantics of all `joint' intermediate languages \\
514\texttt{RTL/RTL.ma} & The syntax of RTL \\
515\texttt{RTL/semantics.ma} & The semantics of RTL \\
516\texttt{ERTL/ERTL.ma} & The syntax of ERTL \\
517\texttt{ERTL/semantics.ma} & The semantics of ERTL \\
518\texttt{LTL/LTL.ma} & The syntax of LTL \\
519\texttt{LTL/semantics.ma} & The semantics of LTL \\
520\texttt{LIN/LIN.ma} & The syntax of LIN \\
521\texttt{LIN/semantics.ma} & The semantics of LIN
522\end{tabular*}
523\end{center}
524
525%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
526% SECTION.                                                                    %
527%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
528\subsection{Listing of important functions and axioms}
529\label{subsect.listing.important.functions.axioms}
530
531We list some important functions and axioms in the backend semantics:
532
533\end{document}
Note: See TracBrowser for help on using the repository browser.