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

Last change on this file since 3180 was 3180, checked in by tranquil, 7 years ago

first commit: report on back-end correctness proof

File size: 12.8 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[all]{xy}
13
14\newcommand{\clap}[1]{\hbox to 0pt{\hss#1\hss}}
15\def\mathclap{\mathpalette\mathclapinternal}
16\def\mathclapinternal#1#2{%
17           \clap{$\mathsurround=0pt#1{#2}$}}
18
19\newcommand{\unif}{\ensuremath{\stackrel{\scriptscriptstyle ?}{\equiv}}}
20\newcommand{\founif}{\ensuremath{\stackrel{\scriptscriptstyle ?}{=}}}
21\newcommand{\vect}[1]{\ensuremath{\stackrel{\to}{#1}}}
22\newcommand{\sem}[1]{\ensuremath{[\![#1]\!]}}
23\newcommand{\bsem}[2]{\ensuremath{[\![#1;\;#2]\!]}}
24\newcommand{\s}[1]{\textsf{#1}}
25
26\renewcommand{\verb}{\lstinline}
27\def\lstlanguagefiles{lst-grafite.tex}
28\lstset{language=Grafite}
29
30\usepackage{lscape}
31\usepackage{stmaryrd}
32\usepackage{threeparttable}
33\usepackage{caption,subcaption}
34\usepackage{url}
35\title{
36INFORMATION AND COMMUNICATION TECHNOLOGIES\\
37(ICT)\\
38PROGRAMME\\
39\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
40
41\lstdefinelanguage{matita-ocaml}
42  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try},
43   morekeywords={[2]whd,normalize,elim,cases,destruct},
44   morekeywords={[3]type,of},
45   mathescape=true,
46  }
47
48\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
49        keywordstyle=\color{red}\bfseries,
50        keywordstyle=[2]\color{blue},
51        keywordstyle=[3]\color{blue}\bfseries,
52        commentstyle=\color{green},
53        stringstyle=\color{blue},
54        showspaces=false,showstringspaces=false}
55
56\lstset{extendedchars=false}
57\lstset{inputencoding=utf8x}
58\DeclareUnicodeCharacter{8797}{:=}
59\DeclareUnicodeCharacter{10746}{++}
60\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
61\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
62
63\date{}
64\author{}
65
66\begin{document}
67
68\thispagestyle{empty}
69
70\vspace*{-1cm}
71\begin{center}
72\includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
73\end{center}
74
75\begin{minipage}{\textwidth}
76\maketitle
77\end{minipage}
78
79\vspace*{0.5cm}
80\begin{center}
81\begin{LARGE}
82\textbf{
83Report n. D4.4\\
84??????????????
85}
86\end{LARGE} 
87\end{center}
88
89\vspace*{2cm}
90\begin{center}
91\begin{large}
92Version 1.1
93\end{large}
94\end{center}
95
96\vspace*{0.5cm}
97\begin{center}
98\begin{large}
99Main Authors:\\
100????????????
101\end{large}
102\end{center}
103
104\vspace*{\fill}
105
106\noindent
107Project Acronym: \cerco{}\\
108Project full title: Certified Complexity\\
109Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
110
111\clearpage
112\pagestyle{myheadings}
113\markright{\cerco{}, FP7-ICT-2009-C-243881}
114
115\newpage
116
117\vspace*{7cm}
118\paragraph{Abstract}
119BLA BLA BLA
120\newpage
121
122\tableofcontents
123
124\newpage
125
126\section{The Back-End Correctness Proof at a Glance}
127
128The back-end part of the compiler takes an \s{RTLabs} program together with
129an initialising cost label and gives the assembly code to be fed to the
130assembler. From the semantic point of view, at this stage of the compiler,
131we are interested in propagating structured traces, as explained in \cite{?}.
132
133A schema with all the back-end passes and the salient and common points of each one is the following:
134$$\overbrace{\s{RTLabs} \longrightarrow
135\overbrace{\underbrace{\overbrace{\s{RTL}}^{\mathclap{\text{stack merge}}} \longrightarrow \s{ERTL} \longrightarrow \s{LTL}}_{\texttt{joint}\text{ graph languages}}\longrightarrow
136\hskip -42.5pt\overbrace{\hskip 42.5pt\s{LIN}}^{\text{linearisation}}}^{\texttt{joint}\text{ languages}}\longrightarrow
137\hskip -42.5pt\underbrace{\hskip 42.5pt\s{ASM}}_{\text{linear map}}}^{\texttt{abstract\_status}}$$
138
139First, here all language semantics share a common interface via \verb+abstract_status+,
140which is at the base of the definition of structured traces.
141The generic shape of each pass of the back-end is thus the same: we get in input an unstructured
142prefix trace followed by a structured one which we want to measure in the source language,
143and we need to prove the existence of the corresponding unstructured and structured
144traces in the target language, with the two traces producing the same observables.
145
146From \s{RTL} down to \s{LIN} we are in the common syntactic and semantic language
147we call \verb+joint+. Inside the first of these languages, \s{RTL}, we pass
148from separate local memory spaces for each function call to a unique one. Even
149though parameters are passed on stack only in \s{ERTL} and variable allocation
150and spilling is done in \s{LTL}, we already have values on stack at this stage,
151and we ensure all the stack space that will eventually be needed is allocated
152at each call.
153
154The next two passes live in the graph part of \verb+joint+, and can benefit from
155a generic approach to graph translation and its proof of correctness, as described
156in~\cite{mauro}.
157
158Next, a generic \verb+joint+ linearisation pass is performed to go from
159\s{LTL} to \s{LIN}. The proof is generic too, with reasonable and straightforward proof
160obligations asking that the common semantic operations of the two languages
161depend on program counters in memory only to control the flow. Program counters
162are indeed the only semantic entity that changes during this pass.
163
164The last pass is, as far as function bodies are concerned, a simple linear
165map---every \s{LIN} instruction is mapped to a single \s{ASM} instruction,
166so that we may say that \s{LIN} is a subset of \s{ASM}. Less straightforward
167is that function bodies are merged together, and that pointers pass from
168formal data to actual one. Values in memory need therefore to be remapped
169to relate the states in the two languages.
170
171\subsection{A common invariant.} This block of traces with properties is recurrent enough to merit the
172\s{matita} definition in \autoref{fig:ft_and_tlr}. We rely on the fact
173that all semantics from \s{RTLabs} down to object code can be expressed
174with the \verb+abstract_status+ record, by which all our definitions of traces
175are expressed.
176\begin{figure}
177\begin{lstlisting}
178record ft_and_tlr (S : abstract_status) (prefix, subtrace : list intensional_event)
179(fn : ident) (st1 : S) : Prop ≝
180{ st2 : S
181; st3 : S
182; ft : flat_trace S st1 st2
183; tlr : trace_label_return S st2 st3
184; tlr_unrpt : tlr_unrepeating … tlr
185; ft_is_prefix : ft_observables … ft = prefix
186; fn_is_current : ft_current_function … ft = Some ? fn
187; tlr_is_subtrace : observables_trace_label_return … tlr fn = subtrace
188}.
189\end{lstlisting}
190\caption{The \verb+ft_and_tlr+ record (which stands for
191\verb+flat_trace+ and \verb+trace_label_return+), which abstracts the kind
192of invariant that all back-end passes need to preserve.}
193\label{fig:ft_and_tlr}
194\end{figure}
195The parameters of the record fix respectively the intensional events encountered
196in the prefix (as stated by \verb+ft_is_prefix+), the ones in the structured trace
197(\verb+tlr_is_subtrace+) and the name of the function in which \verb+tlr+
198takes place (\verb+fn_is_current+), and the initial state.
199The additional property \verb+tlr_unrpt+
200tells that program counters do not repeat locally (i.e.\ between two labels)
201in \verb+tlr+, a property needed for the soundness of the cost static analysis
202(cf.~\cite{?}).
203
204\subsection{The statement.}
205The back-end correctness theorem proves the \s{matita} statement in
206\autoref{fig:statement}. The output of the a proof is
207a \verb+ft_and_tlr+ structure as outlined before, which constitutes the
208preconditions of the assembly proof. The \verb+sigma+ and \verb+pol+
209parameters are passed to \s{ASM}'s semantics, however they have significance
210only with respect to the \s{ASM} to object code correctness
211\footnote{\verb+sigma+ and \verb+pol+ are what allows to maps instructions
212between \s{ASM} and the produced object code. This information isgained during
213the jump expansion pass, cf.~\cite{?}.}.
214
215\begin{figure}
216\begin{subfigure}{\linewidth}
217\begin{lstlisting}
218theorem back_end_correct :
219∀observe,init_cost,p_rtlabs,p_asm,stack_m,max_stack,prefix,subtrace,fn.
220back_end observe init_cost p_rtlabs =
221    return 〈 p_asm, stack_m, max_stack 〉 →
222back_end_preconditions p_rtlabs (stack_sizes stack_m) max_stack prefix subtrace fn →
223∀sigma,pol.
224ft_and_tlr (ASM_status p_asm sigma pol)
225    prefix subtrace fn (initialise_status ? p_asm).
226\end{lstlisting}
227\caption{The statement.}
228\end{subfigure}
229\\[10pt]
230\begin{subfigure}{\linewidth}
231\begin{lstlisting}
232record back_end_preconditions (p_rtlabs : RTLabs_program)
233(stacksizes : ident → option ℕ) (max_stack : ℕ)
234(prefix, subtrace : list intensional_event) (fn : ident) : Prop ≝
235{ ra_init : RTLabs_status (make_global p_rtlabs)
236; ra_init_ok : make_ext_initial_state p_rtlabs = return ra_init
237; ra_max :
238  le (maximum (update_stacksize_info stacksizes (mk_stacksize_info 0 0)
239    (extract_call_ud_from_observables (prefix @ subtrace)))) max_stack
240; ra_ft_tlr : ft_and_tlr (RTLabs_status (make_global p_rtlabs))
241    prefix subtrace fn ra_init
242}.
243\end{lstlisting}
244\caption{The definition of preconditions for the correctness of the back-end.}
245\label{subfig:back_end_preconditions}
246\end{subfigure}
247\caption{The statement of the back-end correctness result.}
248\label{fig:statement}
249\end{figure}
250
251Care must be taken in dealing with the stack. The back-end pass produces a
252\emph{stack model}: the amount of stack needed by each function (\verb+stack_m+),
253together with the maximal usable stack (\verb+max_stack+, $2^{16}$ minus the size occupied by globals).
254While programs in the front end do not fail for stack overflow, the stack
255information is lifted to source much in the same ways as time consumption information,
256so that we can actually use as a hypothesis on input source traces that they
257do not use more stack than allowed.
258This hypothesis is included in the \verb+measurable+ predicate over
259front-end traces, and we put it to use during the back-end pass,
260where we pass to a unique bounded stack space for all functions. More details
261will be presented in \autoref{sec:?}.
262
263The above explanation is why the back-end correctness results requires some additional preconditions
264with respect to a \verb+ft_and_tlr+ for \s{RTLabs}. This is accomplished by the
265\verb+ra_max+ field in the record \verb+back_end_preconditions+
266(\autoref{subfig:back_end_preconditions}). The other fields hold the initial
267state \verb+ra_init+ of the program in \s{RTLabs} (with a proof that it is
268actually the initial state).
269
270\section{From an unbounded to a bounded stack}
271The way the \verb+ft_and_tlr+ is propagated is almost everwhere by means of
272the proof of existence of a special relation between states that is a simulation
273with respect to execution. There are more details involved than in a usual
274extensional proof, regarding the intensional preservation. The details are
275contained in~\cite{?}.
276
277Here we concentrate on a particular aspect that eludes the generic treatment:
278the moment when we pass from an unbounded stack to a bounded one. This passage
279is delicate for two reasons. Firstly, while usually we can assure forward simulation
280of an execution step by simply depending on that step not producing an error,
281here is no more the case, as the stack overflow must start happening somewhere in
282the back-end. Secondly, merging the stack spaces of the function calls requires
283mapping the pointer values contained in memory.
284
285In order to tackle these subtleties, we firstly decided to isolate this passage,
286without mingling it with other pass-dependent semantic preservation proofs.
287Rather than performing the proof when passing from a language to another,
288we decided to split in three the semantics of a single language (\s{RTL}).
289
290The first one, called \verb+RTL_semantics_separate+, mimics how stack is modelled
291in \s{RTLabs}: each function gets allocated upon call an independent stack space.
292Passing from \s{RTLabs} to this semantics involves the usual simulation relation.
293A peculiarity is that data pointers need not change.
294
295The middle, second one, is very similar to the two above. Called
296\verb+RTL_semantics_separate_overflow+, it has separate allocated stack spaces
297just as \verb+RTL_semantics_separate+. However the execution is defined
298so that if the call stack as a whole uses more space than (later) physically
299available, an error is issued. The actual states are identical,
300and the simulation is an almost trivial 1-to-1, where the stack correctness
301inherited from \verb+back_end_preconditions+ can be easily put to use even
302if the generic results for structure preserving simulation actually cannot be
303used here.
304
305The third one, defined as \verb+RTL_semantics_unique+, switches to a semantics with
306a single, bounded stack space, where moreover memory has already been granted to
307globals too. From this semantics down to \s{LIN}, all data in memory excluding
308pieces of program counters remain the same. However in order to show a
309forwarding simulation from \verb+RTL_semantics_separate_overflow+, one needs to
310remap data pointers. No further hypothesis on stack usage needs to be employed,
311as it is integrated in the fact that the execution step does not fail.
312
313\end{document}
Note: See TracBrowser for help on using the repository browser.