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

\documentclass[11pt, epsf, a4wide]{article}

\usepackage{../../style/cerco}

\usepackage{amsfonts}
\usepackage{amsmath}
\usepackage{amssymb} 
\usepackage[english]{babel}
\usepackage{graphicx}
\usepackage[utf8x]{inputenc}
\usepackage{listings}
\usepackage{stmaryrd}
\usepackage{url}

\title{
INFORMATION AND COMMUNICATION TECHNOLOGIES\\
(ICT)\\
PROGRAMME\\
\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}

\lstdefinelanguage{matita-ocaml}
  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,let,in,rec,match,return,with,Type,try},
   morekeywords={[2]whd,normalize,elim,cases,destruct},
   morekeywords={[3]type,of},
   mathescape=true,
  }

\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
        keywordstyle=\color{red}\bfseries,
        keywordstyle=[2]\color{blue},
        keywordstyle=[3]\color{blue}\bfseries,
        commentstyle=\color{green},
        stringstyle=\color{blue},
        showspaces=false,showstringspaces=false}

\lstset{extendedchars=false}
\lstset{inputencoding=utf8x}
\DeclareUnicodeCharacter{8797}{:=}
\DeclareUnicodeCharacter{10746}{++}
\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}

\date{}
\author{}

\begin{document}

\thispagestyle{empty}

\vspace*{-1cm}
\begin{center}
\includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png}
\end{center}

\begin{minipage}{\textwidth}
\maketitle
\end{minipage}

\vspace*{0.5cm}
\begin{center}
\begin{LARGE}
\textbf{
Report n. D4.3\\
Formal semantics of intermediate languages
}
\end{LARGE} 
\end{center}

\vspace*{2cm}
\begin{center}
\begin{large}
Version 1.0
\end{large}
\end{center}

\vspace*{0.5cm}
\begin{center}
\begin{large}
Main Authors:\\
Dominic P. Mulligan and Claudio Sacerdoti Coen
\end{large}
\end{center}

\vspace*{\fill}

\noindent
Project Acronym: \cerco{}\\
Project full title: Certified Complexity\\
Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\

\clearpage
\pagestyle{myheadings}
\markright{\cerco{}, FP7-ICT-2009-C-243881}

\newpage

\vspace*{7cm}
\paragraph{Abstract}
We describe the encoding in the Calculus of Constructions of the semantics of the CerCo compiler's backend intermediate languages.
The CerCo backend consists of five distinct languages: RTL, RTLntl, ERTL, LTL and LIN.
We describe a process of heavy abstraction of the intermediate languages and their semantics.
We hope that this process will ease the burden of Deliverable D4.4, the proof of correctness for the compiler.

\newpage

\tableofcontents

\newpage

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\section{Task}
\label{sect.task}

The Grant Agreement states that Task T4.3, entitled `Formal semantics of intermediate languages' has associated Deliverable D4.3, consisting of the following:
\begin{quotation}
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.
\end{quotation}
This report details our implementation of this deliverable.

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\subsection{Connections with other deliverables}
\label{subsect.connections.with.other.deliverables}

Deliverable D4.3 enjoys a close relationship with three other deliverables, namely deliverables D2.2, D4.3 and D4.4.

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.
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.
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.

Deliverable D4.2 can be seen as a `sister' deliverable to the deliverable reported on herein.
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.
As a result, a substantial amount of Matita code is shared between the two deliverables.

Deliverable D4.4, the backend correctness proofs, is the immediate successor of this deliverable.

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\section{The backend intermediate languages' semantics in Matita}
\label{sect.backend.intermediate.languages.semantics.matita}

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\subsection{Abstracting related languages}
\label{subsect.abstracting.related.languages}

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.
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.
Equivalent intermediate languages to those present in the O'Caml code can be recovered by specialising this joint structure.

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.
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.
In particular, the semantics of both LTL and LIN are implemented in exactly the same way.
The only difference between the two languages is how the next instruction to be interpreted is fetched.
In LTL, this involves looking up in a graph, whereas in LTL, this involves fetching from a list of instructions.

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.
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.

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\subsection{Type parameters, and their purpose}
\label{subsect.type.parameters.their.purpose}

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.
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.

We begin the abstraction process with the \texttt{params\_\_} record.
This holds the types of the representations of the different register varieties in the intermediate languages:
\begin{lstlisting}
record params__: Type[1] ≝
{
  acc_a_reg: Type[0];
  acc_b_reg: Type[0];
  dpl_reg: Type[0];
  dph_reg: Type[0];
  pair_reg: Type[0];
  generic_reg: Type[0];
  call_args: Type[0];
  call_dest: Type[0];
  extend_statements: Type[0]
}.
\end{lstlisting}
We summarise what these types mean, and how they are used in both the semantics and the translation process:
\begin{center}
\begin{tabular*}{\textwidth}{p{4cm}p{11cm}}
Type & Explanation \\
\hline
\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.\\
\texttt{acc\_b\_reg} & Similar to the accumulator A field, but for the processor's auxilliary accumulator, B. \\
\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. \\
\texttt{dph\_reg} & Similar to the DPL register but for the eight high bits of the 16-bit register. \\
\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. \\
\texttt{generic\_reg} & The representation of generic registers (i.e. those that are not devoted to a specific task). \\
\texttt{call\_args} & The number of arguments to a function.  For some languages this is irrelevant. \\
\texttt{call\_dest} & \\
\texttt{extend\_statements} & Instructions that are specific to a particular intermediate language, and which cannot be abstracted into the joint language.
\end{tabular*}
\end{center}

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:
\begin{lstlisting}
inductive joint_instruction (p: params__) (globals: list ident): Type[0] :=
  | COMMENT: String → joint_instruction p globals
  | COST_LABEL: costlabel → joint_instruction p globals
  ...
\end{lstlisting}

We extend \texttt{params\_\_} with a type corresponding to labels, \texttt{succ}, obtaining a new record type of parameters called \texttt{params\_}:
\begin{lstlisting}
record params_: Type[1] ≝
{
  pars__ :> params__;
  succ: Type[0]
}.
\end{lstlisting}
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.
Using \texttt{param\_} we can define statements of the joint language:
\begin{lstlisting}
inductive joint_statement (p:params_) (globals: list ident): Type[0] :=
  | sequential: joint_instruction p globals → succ p → joint_statement p globals
  | GOTO: label → joint_statement p globals
  | RETURN: joint_statement p globals.
\end{lstlisting}
Note that in the joint language, instructions are `linear', in that they have an immediate successor.
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.

For the semantics, we need further parametererised types.
In particular, we parameterise the result and parameter type of an internal function call in \texttt{params0}:
\begin{lstlisting}
record params0: Type[1] ≝
 { pars__' :> params__
 ; resultT: Type[0]
 ; paramsT: Type[0]
 }.
\end{lstlisting}
We further extend \texttt{params0} with a type for local variables in internal function calls:
\begin{lstlisting}
record params1 : Type[1] ≝
 { pars0 :> params0
 ; localsT: Type[0]
 }.
\end{lstlisting}
Again, we expand our parameters with types corresponding to the code representation (either a control flow graph or a list of statements).
Further, we hypothesise a generic method for looking up the next instruction in the graph, called \texttt{lookup}.
Note that \texttt{lookup} may fail, and returns an \texttt{option} type:
\begin{lstlisting}
record params (globals: list ident): Type[1] ≝
 { succ_ : Type[0]
 ; pars1 :> params1
 ; codeT: Type[0]
 ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals)
 }.
\end{lstlisting}
We now have what we need to define internal functions for the joint language.
The first two `universe' fields are only used in the compilation process, for generating fresh names, and do not affect the semantics.
The rest of the fields affect both compilation and semantics.
In particular, we have parameterised result types, function parameter types and the type of local variables.
Note 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:
\begin{lstlisting}
record joint_internal_function (globals: list ident) (p:params globals) : Type[0] :=
{
  joint_if_luniverse: universe LabelTag;
  joint_if_runiverse: universe RegisterTag;
  joint_if_result   : resultT p;
  joint_if_params   : paramsT p;
  joint_if_locals   : localsT p;
  joint_if_stacksize: nat;
  joint_if_code     : codeT … p;
  joint_if_entry    : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?;
  joint_if_exit     : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?
}.
\end{lstlisting}
Naturally, a question arises as to why we have chosen to split up the parameterisation into so many intermediate records, each slightly extending earlier ones.
The reason is because some intermediate languages share a host of parameters, and only differ on some others.
For instance, in instantiating the ERTL language, certain parameters are shared with RTL, whilst others are ERTL specific:
\begin{lstlisting}
...
definition ertl_params__: params__ :=
 mk_params__ register register register register (move_registers × move_registers)
  register nat unit ertl_statement_extension.
...
definition ertl_params1: params1 := rtl_ertl_params1 ertl_params0.
definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0.
...
definition ertl_statement := joint_statement ertl_params_.

definition ertl_internal_function :=
  $\lambda$globals.joint_internal_function … (ertl_params globals).
\end{lstlisting}
Here, \texttt{rtl\_ertl\_params1} are the common parameters of the ERTL and RTL languages:
\begin{lstlisting}
definition rtl_ertl_params1 := $\lambda$pars0. mk_params1 pars0 (list register).
\end{lstlisting}

The record \texttt{more\_sem\_params} bundles together functions that store and retrieve values in various forms of register:
\begin{lstlisting}
record more_sem_params (p:params_): Type[1] :=
{
  framesT: Type[0];
  empty_framesT: framesT;
  regsT: Type[0];
  empty_regsT: regsT;
  call_args_for_main: call_args p;
  call_dest_for_main: call_dest p;
  succ_pc: succ p → address → res address;
  greg_store_: generic_reg p → beval → regsT → res regsT;
  greg_retrieve_: regsT → generic_reg p → res beval;
  acca_store_: acc_a_reg p → beval → regsT → res regsT;
  acca_retrieve_: regsT → acc_a_reg p → res beval;
  ...
  dpl_store_: dpl_reg p → beval → regsT → res regsT;
  dpl_retrieve_: regsT → dpl_reg p → res beval;
  ...
  pair_reg_move_: regsT → pair_reg p → res regsT;
  pointer_of_label: label → $\Sigma$p:pointer. ptype p = Code
}.
\end{lstlisting}
For instance, \texttt{greg\_store\_} and \texttt{greg\_retrieve\_} store and retrieve values from a generic register, respectively.
Similarly, \texttt{pair\_reg\_move} implements the generic move instruction of the joint language.
Here \texttt{framesT} is the type of stack frames, with \texttt{empty\_framesT} an empty stack frame.

The two hypothesised values \texttt{call\_args\_for\_main} and \texttt{call\_dest\_for\_main} deal with problems with the \texttt{main} function of the program, and how it is handled.
In particular, we need to know when the \texttt{main} function has finished executing.
But this is complicated, in C, by the fact that the \texttt{main} function is explicitly allowed to be recursive (disallowed in C++).
Therefore, to understand whether the exiting \texttt{main} function is really exiting, or just recursively calling itself, we need to remember the address at which \texttt{main} is located.
This is done with \texttt{call\_dest\_for\_main}, whereas \texttt{call\_args\_for\_main} holds the \texttt{main} function's arguments.

We extend \texttt{more\_sem\_params} with yet more parameters via \texttt{more\_sem\_params2}:
\begin{lstlisting}
record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] :=
{
  more_sparams1 :> more_sem_params p;
  fetch_statement:
    genv … p → state (mk_sem_params … more_sparams1) →
    res (joint_statement (mk_sem_params … more_sparams1) globals);
  ...
  save_frame:
    address → nat → paramsT … p → call_args p → call_dest p →
    state (mk_sem_params … more_sparams1) →
    res (state (mk_sem_params … more_sparams1));
  pop_frame:
    genv globals p → state (mk_sem_params … more_sparams1) →
    res ((state (mk_sem_params … more_sparams1)));
  ...
  set_result:
    list val → state (mk_sem_params … more_sparams1) →
    res (state (mk_sem_params … more_sparams1));
  exec_extended:
    genv globals p → extend_statements (mk_sem_params … more_sparams1) →
    succ p → state (mk_sem_params … more_sparams1) →
    IO io_out io_in (trace × (state (mk_sem_params … more_sparams1)))
 }.
\end{lstlisting}
Here, \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.

We bundle \texttt{params} and \texttt{sem\_params} together into a single record.
This will be used in the function \texttt{eval\_statement} which executes a single statement of the joint language:
\begin{lstlisting}
record sem_params2 (globals: list ident): Type[1] :=
{
  p2 :> params globals;
  more_sparams2 :> more_sem_params2 globals p2
}.
\end{lstlisting}
\noindent
The \texttt{state} record holds the current state of the interpreter:
\begin{lstlisting}
record state (p: sem_params): Type[0] :=
{
  st_frms: framesT ? p;
  pc: address;
  sp: pointer;
  carry: beval;
  regs: regsT ? p;
  m: bemem
}.
\end{lstlisting}
Here \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.
We use the function \texttt{eval\_statement} to evaluate a single joint statement:
\begin{lstlisting}
definition eval_statement:
  ∀globals: list ident.∀p:sem_params2 globals.
    genv globals p → state p → IO io_out io_in (trace × (state p)) :=
...
\end{lstlisting}
We examine the type of this function.
Note 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.
Monads and their use are further discussed in Subsection~\ref{subsect.use.of.monads}.
Further, the function returns a new state, updated by the single step of execution of the program.
Finally, 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.

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\subsection{Use of monads}
\label{subsect.use.of.monads}

Monads are a categorical notion that have recently gained an amount of traction in functional programming circles.
In particular, it was noted by Moggi that monads could be used to sequence \emph{effectful} computations in a pure manner.
Here, `effectful computations' cover a lot of ground, from writing to files, generating fresh names, or updating an ambient notion of state.

A monad can be characterised by the following:
\begin{itemize}
\item
A data type, $M$.
For instance, the \texttt{option} type in O'Caml or Matita.
\item
A way to `inject' or `lift' pure values into this data type (usually called \texttt{return}).
We call this function \texttt{return} and say that it must have type $\alpha \rightarrow M \alpha$, where $M$ is the name of the monad.
In our example, the `lifting' function for the \texttt{option} monad can be implemented as:
\begin{lstlisting}
let return x = Some x
\end{lstlisting}
\item
A way to `sequence' monadic functions together, to form another monadic function, usually called \texttt{bind}.
Bind has type $M \alpha \rightarrow (\alpha \rightarrow M \beta) \rightarrow M \beta$.
We can see that bind `unpacks' a monadic value, applies a function after unpacking, and `repacks' the new value in the monad.
In our example, the sequencing function for the \texttt{option} monad can be implemented as:
\begin{lstlisting}
let bind o f =
  match o with
    None -> None
    Some s -> f s
\end{lstlisting}
\item
A 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.
These \emph{monad laws} should also be useful in reasoning about monadic computations in the proof of correctness of the compiler.
\end{itemize}
In the semantics of both front and backend intermediate languages, we make use of monads.
This monadic infrastructure is shared between the frontend and backend languages.

In 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.
Here, the monad's sequencing operation ensures that emissions and reads are maintained in the correct order.
Most functions in the intermediate language semantics fall into the IO monad.
In particular, we have already seen how the \texttt{eval\_statement} function of the joint language is monadic, with type:
\begin{lstlisting}
definition eval_statement:
  ∀globals: list ident.∀p:sem_params2 globals.
    genv globals p → state p → IO io_out io_in (trace × (state p)) :=
...
\end{lstlisting}
If we in the body of \texttt{eval\_statement}, we may also see how the monad sequences effects.
For instance, in the case for the \texttt{LOAD} statement, we have the following:
\begin{lstlisting}
definition eval_statement:
  ∀globals: list ident. ∀p:sem_params2 globals.
    genv globals p → state p → IO io_out io_in (trace × (state p)) :=
  $\lambda$globals, p, ge, st.
  ...
  match s with
  | LOAD dst addrl addrh ⇒
    ! vaddrh $\leftarrow$ dph_retrieve … st addrh;
    ! vaddrl $\leftarrow$ dpl_retrieve … st addrl;
    ! vaddr $\leftarrow$ pointer_of_address 〈vaddrl,vaddrh〉;
    ! v $\leftarrow$ opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    ! st $\leftarrow$ acca_store p … dst v st;
    ! st $\leftarrow$ next … l st ;
      ret ? $\langle$E0, st$\rangle$
\end{lstlisting}
Here, we employ a certain degree of syntactic sugaring.
The syntax
\begin{lstlisting}
  ...
! vaddrh $\leftarrow$ dph_retrieve … st addrh;
! vaddrl $\leftarrow$ dpl_retrieve … st addrl;
  ...
\end{lstlisting}
is sugaring for the \texttt{IO} monad's binding operation.
We can expand this sugaring to the following much more verbose code:
\begin{lstlisting}
  ...
  bind (dph_retrieve … st addrh) ($\lambda$vaddrh. bind (dpl_retrieve … st addrl)
    ($\lambda$vaddrl. ...))
\end{lstlisting}
Note also that the function \texttt{ret} is implementing the `lifting', or return function of the \texttt{IO} monad.

We believe the sugaring for the monadic bind operation makes the program much more readable, and therefore easier to reason about.
In particular, note that the functions \texttt{dph\_retrieve}, \texttt{pointer\_of\_address}, \texttt{acca\_store} and \texttt{next} are all monadic.
The function \texttt{opt\_to\_res} is also --- this is a `utility' function that lifts an option type into the \texttt{IO} monad.

\subsection{Memory models}
\label{subsect.memory.models}

Currently, the semantics of the front and backend intermediate languages are built around two distinct memory models.
The frontend languages reuse the CompCert memory model, whereas the backend languages employ a bespoke model tailored to their needs.
This split between the memory models is reflective of the fact that the front and backend language have different requirements from their memory models, to a certain extent.

In particular, the CompCert memory model places quite heavy restrictions on where in memory one can read from.
To read a value in this memory model, you must supply an address, complete with a number of `chunks' to read following that address.
The read is only successful if you attempt to read at a genuine `value boundary', and read the appropriate number of memory chunks for that value.
As a result, with the CompCert memory model you are unable to read the third byte of a 32-bit integer value directly from memory, for instance.
This has some consequences for the CompCert compiler, namely an inability to write a \texttt{memcpy} routine.

However, the CerCo memory model operates differently, as we need to move data `piecemeal' between stacks in the backend of the compiler.
As a result, the bespoke memory model allows one to read data at any memory location, not just on value boundaries.
This has the advantage that we can successfully write a \texttt{memcpy} routine with the CerCo compiler (remembering that \texttt{memcpy} is nothing more than `read a byte, copy a byte' repeated in a loop), an advantage over CompCert.

Right now, the two memory models are interfaced during the translation from RTLabs to RTL.
It is an open question whether we will unify the two memory models, using only the backend, bespoke memory model throughout the compiler, as the CompCert memory model seems to work fine for the frotend, where such byte-by-byte copying is not needed.
However, should we decide to port the frontend to the new memory model, it has been written in such an abstract way that doing so would be relatively straightforward.

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\section{Future work}
\label{sect.future.work}

A few small axioms remain to be closed.
These relate to fetching the next instruction to be interpreted from the control flow graph, or linearised representation, of the language.
Closing these axioms should not be a problem.

Further, tailcalls to external functions are currently axiomatised.
This is due to there being a difficulty with how stackframes are handled with external function calls.
We leave this for further work, due to there being no pressing need to implement this feature at the present time.

There is also, as mentioned, an open problem as to whether the frontend languages should use the same memory model as the backend languages, as opposed to reusing the CompCert memory model.
Should this decision be taken, this will likely be straightforward but potentially time consuming.

\newpage

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\section{Code listing}
\label{sect.code.listing}

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\subsection{Listing of files}
\label{subsect.listing.files}

Semantics specific files (files relating to language translations ommitted).
Syntax specific files:
\begin{center}
\begin{tabular*}{\textwidth}{p{5.5cm}p{9.5cm}}
Title & Description \\
\hline
\texttt{RTLabs/syntax.ma} & The syntax of RTLabs \\
\texttt{joint/Joint.ma} & Abstracted syntax for backend languages \\
\texttt{RTL/RTL.ma} & The syntax of RTL \\
\texttt{ERTL/ERTL.ma} & The syntax of ERTL \\
\texttt{LIN/joint\_LTL\_LIN.ma} & The syntax of the abstracted combined LTL and LIN language \\
\texttt{LTL/LTL.ma} & The specialisation of the above file to the syntax of LTL \\
\texttt{LIN/LIN.ma} & The specialisation of the above file to the syntax of LIN \\
\end{tabular*}
\end{center}

\noindent
Semantics specific files:
\begin{center}
\begin{tabular*}{\textwidth}{p{5.5cm}p{9.5cm}}
Title & Description \\
\hline
\texttt{RTLabs/semantics.ma} & The semantics of RTLabs \\
\texttt{joint/semantics.ma} & The semantics of the abstracted backend languages. \\
\texttt{joint/SemanticUtils.ma} & Generic utilities used in the semantics of all `joint' intermediate languages \\
\texttt{RTL/semantics.ma} & The semantics of RTL \\
\texttt{ERTL/semantics.ma} & The semantics of ERTL \\
\texttt{LIN/joint\_LTL\_LIN\_semantics.ma} & The semantics of the joint LTL-LIN language \\
\texttt{LTL/semantics.ma} & The semantics of LTL \\
\texttt{LIN/semantics.ma} & The semantics of LIN
\end{tabular*}
\end{center}

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\subsection{Listing of important functions and axioms}
\label{subsect.listing.important.functions.axioms}

We list some important functions and axioms in the backend semantics:

\end{document}