source: Deliverables/D4.4/paolo.tex @ 3180

\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[all]{xy}

\newcommand{\clap}[1]{\hbox to 0pt{\hss#1\hss}}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathclapinternal#1#2{%
           \clap{$\mathsurround=0pt#1{#2}$}}

\newcommand{\unif}{\ensuremath{\stackrel{\scriptscriptstyle ?}{\equiv}}}
\newcommand{\founif}{\ensuremath{\stackrel{\scriptscriptstyle ?}{=}}}
\newcommand{\vect}[1]{\ensuremath{\stackrel{\to}{#1}}}
\newcommand{\sem}[1]{\ensuremath{[\![#1]\!]}}
\newcommand{\bsem}[2]{\ensuremath{[\![#1;\;#2]\!]}}
\newcommand{\s}[1]{\textsf{#1}}

\renewcommand{\verb}{\lstinline}
\def\lstlanguagefiles{lst-grafite.tex}
\lstset{language=Grafite}

\usepackage{lscape}
\usepackage{stmaryrd}
\usepackage{threeparttable}
\usepackage{caption,subcaption}
\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,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.4\\
??????????????
}
\end{LARGE} 
\end{center}

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

\vspace*{0.5cm}
\begin{center}
\begin{large}
Main Authors:\\
????????????
\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}
BLA BLA BLA
\newpage

\tableofcontents

\newpage

\section{The Back-End Correctness Proof at a Glance}

The back-end part of the compiler takes an \s{RTLabs} program together with
an initialising cost label and gives the assembly code to be fed to the
assembler. From the semantic point of view, at this stage of the compiler,
we are interested in propagating structured traces, as explained in \cite{?}.

A schema with all the back-end passes and the salient and common points of each one is the following:
$$\overbrace{\s{RTLabs} \longrightarrow
\overbrace{\underbrace{\overbrace{\s{RTL}}^{\mathclap{\text{stack merge}}} \longrightarrow \s{ERTL} \longrightarrow \s{LTL}}_{\texttt{joint}\text{ graph languages}}\longrightarrow
\hskip -42.5pt\overbrace{\hskip 42.5pt\s{LIN}}^{\text{linearisation}}}^{\texttt{joint}\text{ languages}}\longrightarrow
\hskip -42.5pt\underbrace{\hskip 42.5pt\s{ASM}}_{\text{linear map}}}^{\texttt{abstract\_status}}$$

First, here all language semantics share a common interface via \verb+abstract_status+,
which is at the base of the definition of structured traces.
The generic shape of each pass of the back-end is thus the same: we get in input an unstructured
prefix trace followed by a structured one which we want to measure in the source language,
and we need to prove the existence of the corresponding unstructured and structured
traces in the target language, with the two traces producing the same observables.

From \s{RTL} down to \s{LIN} we are in the common syntactic and semantic language
we call \verb+joint+. Inside the first of these languages, \s{RTL}, we pass
from separate local memory spaces for each function call to a unique one. Even
though parameters are passed on stack only in \s{ERTL} and variable allocation
and spilling is done in \s{LTL}, we already have values on stack at this stage,
and we ensure all the stack space that will eventually be needed is allocated
at each call.

The next two passes live in the graph part of \verb+joint+, and can benefit from
a generic approach to graph translation and its proof of correctness, as described
in~\cite{mauro}.

Next, a generic \verb+joint+ linearisation pass is performed to go from
\s{LTL} to \s{LIN}. The proof is generic too, with reasonable and straightforward proof
obligations asking that the common semantic operations of the two languages
depend on program counters in memory only to control the flow. Program counters
are indeed the only semantic entity that changes during this pass.

The last pass is, as far as function bodies are concerned, a simple linear
map---every \s{LIN} instruction is mapped to a single \s{ASM} instruction,
so that we may say that \s{LIN} is a subset of \s{ASM}. Less straightforward
is that function bodies are merged together, and that pointers pass from
formal data to actual one. Values in memory need therefore to be remapped
to relate the states in the two languages.

\subsection{A common invariant.} This block of traces with properties is recurrent enough to merit the
\s{matita} definition in \autoref{fig:ft_and_tlr}. We rely on the fact
that all semantics from \s{RTLabs} down to object code can be expressed
with the \verb+abstract_status+ record, by which all our definitions of traces
are expressed.
\begin{figure}
\begin{lstlisting}
record ft_and_tlr (S : abstract_status) (prefix, subtrace : list intensional_event)
(fn : ident) (st1 : S) : Prop ≝
{ st2 : S
; st3 : S
; ft : flat_trace S st1 st2
; tlr : trace_label_return S st2 st3
; tlr_unrpt : tlr_unrepeating … tlr
; ft_is_prefix : ft_observables … ft = prefix
; fn_is_current : ft_current_function … ft = Some ? fn
; tlr_is_subtrace : observables_trace_label_return … tlr fn = subtrace
}.
\end{lstlisting}
\caption{The \verb+ft_and_tlr+ record (which stands for
\verb+flat_trace+ and \verb+trace_label_return+), which abstracts the kind
of invariant that all back-end passes need to preserve.}
\label{fig:ft_and_tlr}
\end{figure}
The parameters of the record fix respectively the intensional events encountered
in the prefix (as stated by \verb+ft_is_prefix+), the ones in the structured trace
(\verb+tlr_is_subtrace+) and the name of the function in which \verb+tlr+
takes place (\verb+fn_is_current+), and the initial state.
The additional property \verb+tlr_unrpt+
tells that program counters do not repeat locally (i.e.\ between two labels)
in \verb+tlr+, a property needed for the soundness of the cost static analysis
(cf.~\cite{?}).

\subsection{The statement.}
The back-end correctness theorem proves the \s{matita} statement in
\autoref{fig:statement}. The output of the a proof is
a \verb+ft_and_tlr+ structure as outlined before, which constitutes the
preconditions of the assembly proof. The \verb+sigma+ and \verb+pol+
parameters are passed to \s{ASM}'s semantics, however they have significance
only with respect to the \s{ASM} to object code correctness
\footnote{\verb+sigma+ and \verb+pol+ are what allows to maps instructions
between \s{ASM} and the produced object code. This information isgained during
the jump expansion pass, cf.~\cite{?}.}.

\begin{figure}
\begin{subfigure}{\linewidth}
\begin{lstlisting}
theorem back_end_correct :
∀observe,init_cost,p_rtlabs,p_asm,stack_m,max_stack,prefix,subtrace,fn.
back_end observe init_cost p_rtlabs =
    return 〈 p_asm, stack_m, max_stack 〉 →
back_end_preconditions p_rtlabs (stack_sizes stack_m) max_stack prefix subtrace fn →
∀sigma,pol.
ft_and_tlr (ASM_status p_asm sigma pol)
    prefix subtrace fn (initialise_status ? p_asm).
\end{lstlisting}
\caption{The statement.}
\end{subfigure}
\\[10pt]
\begin{subfigure}{\linewidth}
\begin{lstlisting}
record back_end_preconditions (p_rtlabs : RTLabs_program)
(stacksizes : ident → option ℕ) (max_stack : ℕ)
(prefix, subtrace : list intensional_event) (fn : ident) : Prop ≝
{ ra_init : RTLabs_status (make_global p_rtlabs)
; ra_init_ok : make_ext_initial_state p_rtlabs = return ra_init
; ra_max :
  le (maximum (update_stacksize_info stacksizes (mk_stacksize_info 0 0)
    (extract_call_ud_from_observables (prefix @ subtrace)))) max_stack
; ra_ft_tlr : ft_and_tlr (RTLabs_status (make_global p_rtlabs))
    prefix subtrace fn ra_init
}.
\end{lstlisting}
\caption{The definition of preconditions for the correctness of the back-end.}
\label{subfig:back_end_preconditions}
\end{subfigure}
\caption{The statement of the back-end correctness result.}
\label{fig:statement}
\end{figure}

Care must be taken in dealing with the stack. The back-end pass produces a
\emph{stack model}: the amount of stack needed by each function (\verb+stack_m+),
together with the maximal usable stack (\verb+max_stack+, $2^{16}$ minus the size occupied by globals).
While programs in the front end do not fail for stack overflow, the stack
information is lifted to source much in the same ways as time consumption information,
so that we can actually use as a hypothesis on input source traces that they
do not use more stack than allowed.
This hypothesis is included in the \verb+measurable+ predicate over
front-end traces, and we put it to use during the back-end pass,
where we pass to a unique bounded stack space for all functions. More details
will be presented in \autoref{sec:?}.

The above explanation is why the back-end correctness results requires some additional preconditions
with respect to a \verb+ft_and_tlr+ for \s{RTLabs}. This is accomplished by the
\verb+ra_max+ field in the record \verb+back_end_preconditions+
(\autoref{subfig:back_end_preconditions}). The other fields hold the initial
state \verb+ra_init+ of the program in \s{RTLabs} (with a proof that it is
actually the initial state).

\section{From an unbounded to a bounded stack}
The way the \verb+ft_and_tlr+ is propagated is almost everwhere by means of
the proof of existence of a special relation between states that is a simulation
with respect to execution. There are more details involved than in a usual
extensional proof, regarding the intensional preservation. The details are
contained in~\cite{?}.

Here we concentrate on a particular aspect that eludes the generic treatment:
the moment when we pass from an unbounded stack to a bounded one. This passage
is delicate for two reasons. Firstly, while usually we can assure forward simulation
of an execution step by simply depending on that step not producing an error,
here is no more the case, as the stack overflow must start happening somewhere in
the back-end. Secondly, merging the stack spaces of the function calls requires
mapping the pointer values contained in memory.

In order to tackle these subtleties, we firstly decided to isolate this passage,
without mingling it with other pass-dependent semantic preservation proofs.
Rather than performing the proof when passing from a language to another,
we decided to split in three the semantics of a single language (\s{RTL}).

The first one, called \verb+RTL_semantics_separate+, mimics how stack is modelled
in \s{RTLabs}: each function gets allocated upon call an independent stack space.
Passing from \s{RTLabs} to this semantics involves the usual simulation relation.
A peculiarity is that data pointers need not change.

The middle, second one, is very similar to the two above. Called
\verb+RTL_semantics_separate_overflow+, it has separate allocated stack spaces
just as \verb+RTL_semantics_separate+. However the execution is defined
so that if the call stack as a whole uses more space than (later) physically
available, an error is issued. The actual states are identical,
and the simulation is an almost trivial 1-to-1, where the stack correctness
inherited from \verb+back_end_preconditions+ can be easily put to use even
if the generic results for structure preserving simulation actually cannot be
used here.

The third one, defined as \verb+RTL_semantics_unique+, switches to a semantics with
a single, bounded stack space, where moreover memory has already been granted to
globals too. From this semantics down to \s{LIN}, all data in memory excluding
pieces of program counters remain the same. However in order to show a
forwarding simulation from \verb+RTL_semantics_separate_overflow+, one needs to
remap data pointers. No further hypothesis on stack usage needs to be employed,
as it is integrated in the fact that the execution step does not fail.

\end{document}