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{ |
---|
36 | INFORMATION AND COMMUNICATION TECHNOLOGIES\\ |
---|
37 | (ICT)\\ |
---|
38 | PROGRAMME\\ |
---|
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{ |
---|
83 | Report n. D4.4\\ |
---|
84 | ?????????????? |
---|
85 | } |
---|
86 | \end{LARGE} |
---|
87 | \end{center} |
---|
88 | |
---|
89 | \vspace*{2cm} |
---|
90 | \begin{center} |
---|
91 | \begin{large} |
---|
92 | Version 1.1 |
---|
93 | \end{large} |
---|
94 | \end{center} |
---|
95 | |
---|
96 | \vspace*{0.5cm} |
---|
97 | \begin{center} |
---|
98 | \begin{large} |
---|
99 | Main Authors:\\ |
---|
100 | ???????????? |
---|
101 | \end{large} |
---|
102 | \end{center} |
---|
103 | |
---|
104 | \vspace*{\fill} |
---|
105 | |
---|
106 | \noindent |
---|
107 | Project Acronym: \cerco{}\\ |
---|
108 | Project full title: Certified Complexity\\ |
---|
109 | Proposal/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} |
---|
119 | BLA BLA BLA |
---|
120 | \newpage |
---|
121 | |
---|
122 | \tableofcontents |
---|
123 | |
---|
124 | \newpage |
---|
125 | |
---|
126 | \section{The Back-End Correctness Proof at a Glance} |
---|
127 | |
---|
128 | The back-end part of the compiler takes an \s{RTLabs} program together with |
---|
129 | an initialising cost label and gives the assembly code to be fed to the |
---|
130 | assembler. From the semantic point of view, at this stage of the compiler, |
---|
131 | we are interested in propagating structured traces, as explained in \cite{?}. |
---|
132 | |
---|
133 | A 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 | |
---|
139 | First, here all language semantics share a common interface via \verb+abstract_status+, |
---|
140 | which is at the base of the definition of structured traces. |
---|
141 | The generic shape of each pass of the back-end is thus the same: we get in input an unstructured |
---|
142 | prefix trace followed by a structured one which we want to measure in the source language, |
---|
143 | and we need to prove the existence of the corresponding unstructured and structured |
---|
144 | traces in the target language, with the two traces producing the same observables. |
---|
145 | |
---|
146 | From \s{RTL} down to \s{LIN} we are in the common syntactic and semantic language |
---|
147 | we call \verb+joint+. Inside the first of these languages, \s{RTL}, we pass |
---|
148 | from separate local memory spaces for each function call to a unique one. Even |
---|
149 | though parameters are passed on stack only in \s{ERTL} and variable allocation |
---|
150 | and spilling is done in \s{LTL}, we already have values on stack at this stage, |
---|
151 | and we ensure all the stack space that will eventually be needed is allocated |
---|
152 | at each call. |
---|
153 | |
---|
154 | The next two passes live in the graph part of \verb+joint+, and can benefit from |
---|
155 | a generic approach to graph translation and its proof of correctness, as described |
---|
156 | in~\cite{mauro}. |
---|
157 | |
---|
158 | Next, 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 |
---|
160 | obligations asking that the common semantic operations of the two languages |
---|
161 | depend on program counters in memory only to control the flow. Program counters |
---|
162 | are indeed the only semantic entity that changes during this pass. |
---|
163 | |
---|
164 | The last pass is, as far as function bodies are concerned, a simple linear |
---|
165 | map---every \s{LIN} instruction is mapped to a single \s{ASM} instruction, |
---|
166 | so that we may say that \s{LIN} is a subset of \s{ASM}. Less straightforward |
---|
167 | is that function bodies are merged together, and that pointers pass from |
---|
168 | formal data to actual one. Values in memory need therefore to be remapped |
---|
169 | to 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 |
---|
173 | that all semantics from \s{RTLabs} down to object code can be expressed |
---|
174 | with the \verb+abstract_status+ record, by which all our definitions of traces |
---|
175 | are expressed. |
---|
176 | \begin{figure} |
---|
177 | \begin{lstlisting} |
---|
178 | record 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 |
---|
192 | of invariant that all back-end passes need to preserve.} |
---|
193 | \label{fig:ft_and_tlr} |
---|
194 | \end{figure} |
---|
195 | The parameters of the record fix respectively the intensional events encountered |
---|
196 | in 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+ |
---|
198 | takes place (\verb+fn_is_current+), and the initial state. |
---|
199 | The additional property \verb+tlr_unrpt+ |
---|
200 | tells that program counters do not repeat locally (i.e.\ between two labels) |
---|
201 | in \verb+tlr+, a property needed for the soundness of the cost static analysis |
---|
202 | (cf.~\cite{?}). |
---|
203 | |
---|
204 | \subsection{The statement.} |
---|
205 | The back-end correctness theorem proves the \s{matita} statement in |
---|
206 | \autoref{fig:statement}. The output of the a proof is |
---|
207 | a \verb+ft_and_tlr+ structure as outlined before, which constitutes the |
---|
208 | preconditions of the assembly proof. The \verb+sigma+ and \verb+pol+ |
---|
209 | parameters are passed to \s{ASM}'s semantics, however they have significance |
---|
210 | only with respect to the \s{ASM} to object code correctness |
---|
211 | \footnote{\verb+sigma+ and \verb+pol+ are what allows to maps instructions |
---|
212 | between \s{ASM} and the produced object code. This information isgained during |
---|
213 | the jump expansion pass, cf.~\cite{?}.}. |
---|
214 | |
---|
215 | \begin{figure} |
---|
216 | \begin{subfigure}{\linewidth} |
---|
217 | \begin{lstlisting} |
---|
218 | theorem back_end_correct : |
---|
219 | ∀observe,init_cost,p_rtlabs,p_asm,stack_m,max_stack,prefix,subtrace,fn. |
---|
220 | back_end observe init_cost p_rtlabs = |
---|
221 | return 〈 p_asm, stack_m, max_stack 〉 → |
---|
222 | back_end_preconditions p_rtlabs (stack_sizes stack_m) max_stack prefix subtrace fn → |
---|
223 | ∀sigma,pol. |
---|
224 | ft_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} |
---|
232 | record 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 | |
---|
251 | Care 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+), |
---|
253 | together with the maximal usable stack (\verb+max_stack+, $2^{16}$ minus the size occupied by globals). |
---|
254 | While programs in the front end do not fail for stack overflow, the stack |
---|
255 | information is lifted to source much in the same ways as time consumption information, |
---|
256 | so that we can actually use as a hypothesis on input source traces that they |
---|
257 | do not use more stack than allowed. |
---|
258 | This hypothesis is included in the \verb+measurable+ predicate over |
---|
259 | front-end traces, and we put it to use during the back-end pass, |
---|
260 | where we pass to a unique bounded stack space for all functions. More details |
---|
261 | will be presented in \autoref{sec:?}. |
---|
262 | |
---|
263 | The above explanation is why the back-end correctness results requires some additional preconditions |
---|
264 | with 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 |
---|
267 | state \verb+ra_init+ of the program in \s{RTLabs} (with a proof that it is |
---|
268 | actually the initial state). |
---|
269 | |
---|
270 | \section{From an unbounded to a bounded stack} |
---|
271 | The way the \verb+ft_and_tlr+ is propagated is almost everwhere by means of |
---|
272 | the proof of existence of a special relation between states that is a simulation |
---|
273 | with respect to execution. There are more details involved than in a usual |
---|
274 | extensional proof, regarding the intensional preservation. The details are |
---|
275 | contained in~\cite{?}. |
---|
276 | |
---|
277 | Here we concentrate on a particular aspect that eludes the generic treatment: |
---|
278 | the moment when we pass from an unbounded stack to a bounded one. This passage |
---|
279 | is delicate for two reasons. Firstly, while usually we can assure forward simulation |
---|
280 | of an execution step by simply depending on that step not producing an error, |
---|
281 | here is no more the case, as the stack overflow must start happening somewhere in |
---|
282 | the back-end. Secondly, merging the stack spaces of the function calls requires |
---|
283 | mapping the pointer values contained in memory. |
---|
284 | |
---|
285 | In order to tackle these subtleties, we firstly decided to isolate this passage, |
---|
286 | without mingling it with other pass-dependent semantic preservation proofs. |
---|
287 | Rather than performing the proof when passing from a language to another, |
---|
288 | we decided to split in three the semantics of a single language (\s{RTL}). |
---|
289 | |
---|
290 | The first one, called \verb+RTL_semantics_separate+, mimics how stack is modelled |
---|
291 | in \s{RTLabs}: each function gets allocated upon call an independent stack space. |
---|
292 | Passing from \s{RTLabs} to this semantics involves the usual simulation relation. |
---|
293 | A peculiarity is that data pointers need not change. |
---|
294 | |
---|
295 | The middle, second one, is very similar to the two above. Called |
---|
296 | \verb+RTL_semantics_separate_overflow+, it has separate allocated stack spaces |
---|
297 | just as \verb+RTL_semantics_separate+. However the execution is defined |
---|
298 | so that if the call stack as a whole uses more space than (later) physically |
---|
299 | available, an error is issued. The actual states are identical, |
---|
300 | and the simulation is an almost trivial 1-to-1, where the stack correctness |
---|
301 | inherited from \verb+back_end_preconditions+ can be easily put to use even |
---|
302 | if the generic results for structure preserving simulation actually cannot be |
---|
303 | used here. |
---|
304 | |
---|
305 | The third one, defined as \verb+RTL_semantics_unique+, switches to a semantics with |
---|
306 | a single, bounded stack space, where moreover memory has already been granted to |
---|
307 | globals too. From this semantics down to \s{LIN}, all data in memory excluding |
---|
308 | pieces of program counters remain the same. However in order to show a |
---|
309 | forwarding simulation from \verb+RTL_semantics_separate_overflow+, one needs to |
---|
310 | remap data pointers. No further hypothesis on stack usage needs to be employed, |
---|
311 | as it is integrated in the fact that the execution step does not fail. |
---|
312 | |
---|
313 | \end{document} |
---|