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

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

more changes, talking about parameters

File size: 14.0 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={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{
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}
99
100\newpage
101
102\tableofcontents
103
104\newpage
105
106%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
107% SECTION.                                                                    %
108%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
109\section{Task}
110\label{sect.task}
111
112The Grant Agreement states that Task T4.3, entitled `Formal semantics of intermediate languages' has associated Deliverable D4.3, consisting of the following:
113\begin{quotation}
114Executable 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.
115\end{quotation}
116This report details our implementation of this deliverable.
117
118%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
119% SECTION.                                                                    %
120%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
121\subsection{Connections with other deliverables}
122\label{subsect.connections.with.other.deliverables}
123
124Deliverable D4.3 enjoys a close relationship with three other deliverables, namely deliverables D2.2, D4.3 and D4.4.
125
126Deliverable 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.
127In 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.
128Any 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.
129
130Deliverable D4.2 can be seen as a `sister' deliverable to the deliverable reported on herein.
131In 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.
132As a result, a substantial amount of Matita code is shared between the two deliverables.
133
134Deliverable D4.4, the backend correctness proofs, is the immediate successor of this deliverable.
135
136%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
137% SECTION.                                                                    %
138%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
139\section{The backend intermediate languages' semantics in Matita}
140\label{sect.backend.intermediate.languages.semantics.matita}
141
142%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
143% SECTION.                                                                    %
144%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
145\subsection{Abstracting related languages}
146\label{subsect.abstracting.related.languages}
147
148As 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.
149In 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.
150Equivalent intermediate languages to those present in the O'Caml code can be recovered by specialising this joint structure.
151
152As 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.
153However, 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.
154In particular, the semantics of both LTL and LIN are implemented in exactly the same way.
155The only difference between the two languages is how the next instruction to be interpreted is fetched.
156In LTL, this involves looking up in a graph, whereas in LTL, this involves fetching from a list of instructions.
157
158As 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.
159Furthermore, 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.
160
161%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
162% SECTION.                                                                    %
163%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
164\subsection{Type parameters, and their purpose}
165\label{subsect.type.parameters.their.purpose}
166
167We 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.
168As 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.
169We now summarise what each parameter is.
170
171\begin{lstlisting}
172record params__: Type[1] ≝
173{
174  acc_a_reg: Type[0];
175  acc_b_reg: Type[0];
176  dpl_reg: Type[0];
177  dph_reg: Type[0];
178  pair_reg: Type[0];
179  generic_reg: Type[0];
180  call_args: Type[0];
181  call_dest: Type[0];
182  extend_statements: Type[0]
183}.
184\end{lstlisting}
185
186As 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:
187\begin{lstlisting}
188inductive joint_instruction (p: params__) (globals: list ident): Type[0] :=
189  | COMMENT: String → joint_instruction p globals
190  | COST_LABEL: costlabel → joint_instruction p globals
191  ...
192\end{lstlisting}
193
194We extend \texttt{params\_\_} with a type corresponding
195\begin{lstlisting}
196record params_: Type[1] ≝
197{
198  pars__ :> params__;
199  succ: Type[0]
200}.
201\end{lstlisting}
202
203\begin{lstlisting}
204inductive joint_statement (p:params_) (globals: list ident): Type[0] :=
205  | sequential: joint_instruction p globals → succ p → joint_statement p globals
206  | GOTO: label → joint_statement p globals
207  | RETURN: joint_statement p globals.
208\end{lstlisting}
209
210\begin{lstlisting}
211record params0: Type[1] ≝
212 { pars__' :> params__
213 ; resultT: Type[0]
214 ; paramsT: Type[0]
215 }.
216\end{lstlisting}
217
218\begin{lstlisting}
219record params1 : Type[1] ≝
220 { pars0 :> params0
221 ; localsT: Type[0]
222 }.
223\end{lstlisting}
224
225\begin{lstlisting}
226record params (globals: list ident): Type[1] ≝
227 { succ_ : Type[0]
228 ; pars1 :> params1
229 ; codeT: Type[0]
230 ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals)
231 }.
232\end{lstlisting}
233
234\begin{lstlisting}
235definition graph_params_: params__ $\rightarrow$ params_ :=
236  $\lambda$pars__. mk_params_ pars__ label.
237\end{lstlisting}
238
239\begin{lstlisting}
240record joint_internal_function (globals: list ident) (p:params globals) : Type[0] :=
241{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
242  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
243(*  joint_if_sig: signature;  -- dropped in front end *)
244  joint_if_result   : resultT p;
245  joint_if_params   : paramsT p;
246  joint_if_locals   : localsT p;
247(*CSC: XXXXX stacksize unused for LTL-...*)
248  joint_if_stacksize: nat;
249  joint_if_code     : codeT … p;
250(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
251  joint_if_entry    : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?;
252(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
253  joint_if_exit     : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?
254}.
255\end{lstlisting}
256
257%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
258% SECTION.                                                                    %
259%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
260\subsection{Use of monads}
261\label{subsect.use.of.monads}
262
263Monads are a categorical notion that have recently gained an amount of traction in functional programming circles.
264In particular, it was noted by Moggi that monads could be used to sequence \emph{effectful} computations in a pure manner.
265Here, `effectful computations' cover a lot of ground, from writing to files, generating fresh names, or updating an ambient notion of state.
266
267In the semantics of both front and backend intermediate languages, we make use of monads.
268In particular, we make use of two forms of monad:
269\begin{enumerate}
270\item
271An `error monad', which signals that a computation either has completed successfully, or returns with an error message.
272The sequencing operation of the error monad ensures that the result of chained computations in return the error message of the first failed computation.
273This monad is used extensively in the semantics to signal a state which cannot be recovered from.
274For instance, in the semantics of RTLabs, we make use of the error monad to signal bad final states:
275\begin{lstlisting}
276XXX better example
277\end{lstlisting}
278\item
279An `IO' monad, signalling the emission or reading of data to some external location or memory address.
280Here, 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).
281Most functions in the intermediate language semantics fall into the IO monad.
282\end{enumerate}
283This monadic infrastructure is shared between the frontend and backend languages.
284
285%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
286% SECTION.                                                                    %
287%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
288\section{Future work}
289\label{sect.future.work}
290
291A few small axioms remain to be closed.
292These relate to fetching the next instruction to be interpreted from the control flow graph, or linearised representation, of the language.
293Closing these axioms should not be a problem.
294No further work remains, aside from `tidying up' the code.
295
296\newpage
297
298%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
299% SECTION.                                                                    %
300%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
301\section{Code listing}
302\label{sect.code.listing}
303
304%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
305% SECTION.                                                                    %
306%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
307\subsection{Listing of files}
308\label{subsect.listing.files}
309
310Semantics specific files (files relating to language translations ommitted):
311\begin{center}
312\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
313Title & Description \\
314\hline
315\texttt{RTLabs/syntax.ma} & The syntax of RTLabs \\
316\texttt{RTLabs/semantics.ma} & The semantics of RTLabs \\
317\texttt{joint/Joint.ma} & Abstracted syntax for backend languages \\
318\texttt{joint/SemanticUtils.ma} & Generic utilities used in the semantics of all `joint' intermediate languages \\
319\texttt{RTL/RTL.ma} & The syntax of RTL \\
320\texttt{RTL/semantics.ma} & The semantics of RTL \\
321\texttt{ERTL/ERTL.ma} & The syntax of ERTL \\
322\texttt{ERTL/semantics.ma} & The semantics of ERTL \\
323\texttt{LTL/LTL.ma} & The syntax of LTL \\
324\texttt{LTL/semantics.ma} & The semantics of LTL \\
325\texttt{LIN/LIN.ma} & The syntax of LIN \\
326\texttt{LIN/semantics.ma} & The semantics of LIN
327\end{tabular*}
328\end{center}
329
330%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
331% SECTION.                                                                    %
332%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
333\subsection{Listing of important functions and axioms}
334\label{subsect.listing.important.functions.axioms}
335
336We list some important functions and axioms in the backend semantics:
337
338\end{document}
Note: See TracBrowser for help on using the repository browser.