source: Deliverables/Dissemination/back-end/back-end.tex @ 3281

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

back end correctness slides, alas still incomplete

File size: 28.3 KB
Line 
1\documentclass[nopanel]{beamer}
2% \usepackage{graphicx,color}
3\usepackage{amsfonts}
4\usepackage{listings}
5
6\lstset{basicstyle=\footnotesize\tt,columns=flexible,breaklines=false,
7        keywordstyle=\color{red}\bfseries,
8        keywordstyle=[2]\color{blue},
9        commentstyle=\color{green},
10        stringstyle=\color{blue},
11        showspaces=false,showstringspaces=false}
12
13
14\setbeamertemplate{footline}[page number]
15\setbeamertemplate{sidebar right}{}
16
17\setbeamercolor{alerted text}{fg=red!70!orange}
18
19\newcommand{\red}[1]{\textcolor{red}{#1}}
20\newcommand{\blue}[1]{\textcolor{blue}{#1}}
21\newcommand{\green}[1]{\textcolor{green}{#1}}
22\newcommand{\grey}[1]{\textcolor{grey}{#1}}
23
24\usepackage{tikz}
25\usetikzlibrary{positioning,calc,patterns,chains,shapes.geometric}
26\makeatletter
27\pgfutil@ifundefined{pgf@arrow@code@implies}{% supply for lack of double arrow special arrow tip if it is not there%
28  \pgfarrowsdeclare{implies}{implies}%
29  {%
30  \pgfarrowsleftextend{2.2pt}%
31  \pgfarrowsrightextend{2.2pt}%
32  }%
33  {%
34    \pgfsetdash{}{0pt} % do not dash%
35    \pgfsetlinewidth{.33pt}%
36    \pgfsetroundjoin   % fix join%
37    \pgfsetroundcap    % fix cap%
38    \pgfpathmoveto{\pgfpoint{-1.5pt}{2.5pt}}%
39    \pgfpathcurveto{\pgfpoint{-.75pt}{1.5pt}}{\pgfpoint{0.5pt}{.5pt}}{\pgfpoint{2pt}{0pt}}%
40    \pgfpathcurveto{\pgfpoint{0.5pt}{-.5pt}}{\pgfpoint{-.75pt}{-1.5pt}}{\pgfpoint{-1.5pt}{-2.5pt}}%
41    \pgfusepathqstroke%
42  }%
43}{}%
44\makeatother
45
46\tikzset{state/.style={inner sep = 0, outer sep = 2pt, draw, fill},
47         every node/.style={inner sep=2pt},
48         every on chain/.style = {inner sep = 0, outer sep = 2pt},
49         join all/.style = {every on chain/.append style={join}},
50         on/.style={on chain={#1}, state},
51         m/.style={execute at begin node=$, execute at end node=$},
52         node distance=3mm,
53         is other/.style={circle, minimum size = 3pt, state},
54         other/.style={on, is other},
55         is jump/.style={diamond, minimum size = 6pt, state},
56         jump/.style={on, is jump},
57         is call/.style={regular polygon, regular polygon sides=3, minimum size=5pt, state},
58         call/.style={on=going below, is call, node distance=6mm, label=above left:$#1$},
59         is ret/.style={regular polygon, regular polygon sides=3, minimum size=5pt, shape border rotate=180, state},
60         ret/.style={on=going above, is ret, node distance=6mm},
61         chain/.style={start chain=#1 going left},
62         rev ar/.style={stealth-, thick},
63         ar/.style={-stealth, thick},
64         every join/.style={rev ar},
65         labelled/.style={fill=white, label=above:$#1$},
66         vcenter/.style={baseline={([yshift=-.5ex]current bounding box)}},
67         every picture/.style={thick},
68         double equal sign distance/.prefix style={double distance=1.5pt}, %% if already defined (newest version of pgf) it should be ignored%}
69         implies/.style={double, -implies, thin, double equal sign distance, shorten <=5pt, shorten >=5pt},
70}
71
72\addtolength{\parskip}{0.3em}
73
74\newcommand{\s}[1]{\textsf{#1}}
75\newcommand{\clap}[1]{\hbox to 0pt{\hss#1\hss}}
76\def\mathclap{\mathpalette\mathclapinternal}
77\def\mathclapinternal#1#2{%
78           \clap{$\mathsurround=0pt#1{#2}$}}
79\DeclareMathOperator{\costmap}{costmap}
80\DeclareMathOperator{\clock}{clock}
81
82
83\begin{document}
84
85\title{Front-end Correctness Proofs}
86\author{Jaap~Boender, Dominic~P.~Mulligan, Mauro~Piccolo, Claudio~Sacerdoti~Coen,
87\structure{Paolo~Tranquilli}}
88\institute{DISI, University of Bologna\\[1ex]
89\includegraphics[width=.3\linewidth]{cerco_logo.png}\\
90\footnotesize Project FP7-ICT-2009-C-243881
91}
92\date{CerCo review meeting\\16th May 2013}
93\maketitle
94
95\begin{frame}
96\frametitle{Introduction}
97
98D4.4 consists of the back-end correctness proofs:
99
100\begin{description}
101\item[Primary focus:] novel \red{intensional} properties: \blue{cost
102    bound correctness}
103\end{description}
104\vskip-2ex
105\begin{itemize}
106\item Now have \blue{stack} costs as well as \blue{time}\\
107--- yields stronger overall correctness result
108\end{itemize}
109
110\medskip
111\begin{description}
112\item[Secondary focus:] usual \red{extensional} result: \blue{functional correctness}
113\end{description}
114\vskip-2ex
115\begin{itemize}
116\item Similar functional correctness already studied in
117\blue{CompCert}
118\item Axiomatize similar results
119\item \red{Intensional} proofs form a layer on top
120\end{itemize}
121\end{frame}
122
123\begin{frame}%
124%[]
125\frametitle{The back-end at a glance}
126$$\overbrace{\s{RTLabs} \longrightarrow
127\overbrace{\underbrace{\overbrace{\s{RTL}}^{\mathclap{\text{stack merge}}} \longrightarrow \s{ERTL} \longrightarrow \s{LTL}}_{\texttt{joint}\text{ graph languages}}\longrightarrow
128\hskip -42.5pt\overbrace{\hskip 42.5pt\s{LIN}}^{\text{linearisation}}}^{\texttt{joint}\text{ languages}}\longrightarrow
129\hskip -42.5pt\underbrace{\hskip 42.5pt\s{ASM}}_{\text{linear map}}}^{\texttt{abstract\_status}\text{ (structured traces)}}$$
130\end{frame}
131%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
132\begin{frame}%
133%[]
134\frametitle{Back-end correctness}
135\begin{theorem}
136  $$ \begin{tikzpicture}
137     \node (s1) [is other, label=above:$s_1$] {};
138     \node (m1) [is other, label=above:$m_1$, right=4cm of s1] {};
139     \node (t1) [is other, label=above:$t_1$, right=4cm of m1] {};
140     \draw [-stealth] (s1) -- node [above] {unstructured trace} (m1);
141     \draw [-stealth] (m1) -- node [above] {structured trace} (t1);
142     \begin{scope}[blue]
143     \node (s2) [is other, label=below:$s_2$, below=1cm of s1] {};
144     \node (m2) [is other, label=below:$m_2$, right=4cm of s2] {};
145     \node (t2) [is other, label=below:$t_2$, right=4cm of m2] {};
146     \draw [-stealth] (s2) -- node [below] {unstructured trace} (m2);
147     \draw [-stealth] (m2) -- node [below] {structured trace} (t2);
148     \path ($(s1)!.5!(m1)$) -- node [sloped] {\LARGE$\approx$} ($(s2)!.5!(m2)$);
149     \path ($(m1)!.5!(t1)$) -- node [sloped] {\LARGE$\approx$} ($(m2)!.5!(t2)$);
150     \end{scope}
151     \node (l1) [left=of s1] {RTLabs:};
152     \node (l2) [left=of s2] {ASM:};
153     \node [rotate=-90, blue] at ($(l1)!.5!(l2)$) {$\Rightarrow$};
154    \end{tikzpicture}
155$$
156\begin{itemize}
157 \item $\approx$ denotes having the same \structure{observables} (labels, calls, returns)
158 \item The RTLabs traces respect stack bounds
159\end{itemize}
160\end{theorem}
161
162\end{frame}
163%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
164\section{Preserving structure}
165\begin{frame}%
166%[]
167\frametitle{Structured traces}
168\begin{center}
169\begin{tikzpicture}
170\begin{scope}[chain, join all]
171\node [ret] {};
172\node [other] {};
173\node [other] {};
174\node [other] (f) {};
175\node [ret] {};
176\node [other] {};
177\node [other] {};
178\node [other, labelled=\epsilon] {};
179\node [other] (g) {};
180\node [ret] {};
181\node [other] {};
182\node [other] {};
183\node [other, labelled=\delta] {};
184\node [jump] {};
185\node [other] {};
186\node [other, labelled=\gamma] {};
187\node [call=g, join=with g by {-, densely dashed}] {};
188\foreach \i in {1,...,2} \node [other] {};
189\node [other, labelled=\beta] {};
190\node [call=f, join=with f by {-, densely dashed}] {};
191\foreach \i in {1,...,2} \node [other] {};
192\node [other, labelled=\alpha] {};
193\end{scope}
194
195\end{tikzpicture}
196\end{center}
197\begin{columns}[t]
198\column{.5\linewidth}
199\begin{itemize}
200 \item States are classified:
201     \tikz\node [is call] {}; call,
202     \tikz\node [is ret] {}; return,
203     \tikz\node [is jump] {}; branch,
204     \tikz\node [is other] {}; other
205 \item
206     \tikz[chain] \node [other, labelled=\alpha] (a) {}; :
207       labelled state
208 \item \tikz[chain, vcenter, join all] { \node [on chain, draw=none, fill=none] {}; \node [call=f, node distance=6mm] {}; } :
209        calling $f$, forces label
210\end{itemize}
211\column{.5\linewidth}
212\begin{itemize}
213 \item \tikz[chain] \node [jump] {}; : branch state, forces label
214 \item \tikz[chain, join all] { \node [other] {};
215                     \begin{scope} [start branch=call going left, ,every join/.style={-, densely dashed, thick},every label/.style={overlay}]
216                       \node [on, is call, node distance=4 mm] {};
217                     \end{scope}
218                     \node [ret, node distance=4 mm] {};} :
219        executing return we land after the corresponding call
220\end{itemize}
221
222\end{columns}
223\end{frame}
224
225\begin{frame}%
226%[]
227\frametitle{Extensional simulation}
228\begin{itemize}
229 \item Usual \structure{extensional} simulation ($S$ for semantical relation):
230     $$ \begin{tikzpicture}[node distance=12mm, thick]
231         \node [is other] (a) {};
232         \node [is other, right=of a] (b) {};
233         \node [is other, below=of a] (c) {};
234         \draw (a) -- node [fill=white] {$S$} (c);
235         \draw [-stealth] (a) -- (b) ;
236         \begin{scope}[blue]
237             \node [is other, right=of c] (d) {};
238             \node [is other] (e) at ($(c)!.333!(d)$) {};
239             \node [is other] (f) at ($(c)!.667!(d)$) {};
240             \draw (b) -- node [fill=white] {$S$} (d);
241             \draw (c) [-stealth] -- (e);
242             \draw (e) [dotted] -- (f);
243             \draw [-stealth] (f) -- (d);
244             \path (a) -- node [sloped] {$\Rightarrow$} (d);
245         \end{scope}
246        \end{tikzpicture}$$
247 \item We need to add \structure{intensional} preservation
248\end{itemize}
249\end{frame}
250
251\begin{frame}%
252%[]
253\frametitle{Preserving labels}
254\begin{itemize}
255 \item We need to preserve traversed labels
256 \item Can we delegate to the semantical relation $S$? \alert{No}
257 \item Take a call (ignore intensional call preservation for the moment):
258 $$ \begin{tikzpicture}[every join/.style={ar}, join all, thick]
259    \node (s1) [is call] {};
260    \begin{scope}[start chain, node distance=2mm, blue]
261    \node (s2) [black, on, is other, below=9mm of s1] {};
262    \node [on, is other] {};
263    \node [on, is call] {};
264    \node (l) [on, is other, fill=white, label=below:$\uncover<-1>\alpha$] {};
265    \node [on, is other] {};
266    \node [on, is other] {};
267    \node [on, is other] {};
268    \node (t2) [on, is other] {};
269    \end{scope}
270    \node (t1) [is other, labelled=\uncover<-1>\alpha] at (s1-|l) {};
271     \begin{scope}[start chain=first]
272      \chainin (s1); \chainin (t1);
273     \end{scope}
274    \draw (s1) -- node [fill=white] {$S$} (s2);
275    \draw [blue] (t1) -- node [fill=white] {$S$} (t2);
276    \uncover<2->{
277        \draw [blue] (t1) -- node [fill=white] {$L$} (l);
278    }
279    \end{tikzpicture}
280  $$ 
281  \item \alert{Labels are not synchronised with semantical relation!}
282  \item<2-> $L$ relation: states are co-labelled
283\end{itemize}
284\end{frame}
285
286\begin{frame}%
287%[]
288\frametitle{Preserving calls}
289\begin{itemize}
290 \item If we want to localise simulation result, we need need something to preserve
291     the \tikz{\node (a) [is call] {}; \node [right=of a, is other] (b) {}; \draw [densely dashed, thick] (a) -- (b);}
292     relation
293 \item We use a \structure{call relation} $C$ (based on program counters)
294 \item For call states, we finally ask
295 $$ \begin{tikzpicture}[every join/.style={ar}, join all, thick]
296     \begin{scope}[start chain=going above]
297        \node (s1) [on, call=f] {};
298        \node (t1) [on, is other] {};
299     \end{scope}
300    \begin{scope}[start chain, node distance=2mm, blue]
301    \node (s2) [on, is other, below=9mm of s1, black] {};
302    \node [on, is other] {};
303    \node [on, is other] {};
304    \node (c) [on, is call, label=above right:$f$] {};
305    \node (l) [node distance=3mm, on chain=going above, is other] {};
306    \node [on chain=going right, is other] {};
307    \node [on, is other] {};
308    \node (t2) [on, is other] {};
309    \end{scope}
310    \draw (s1) to node [fill=white] {$S$} (s2);
311    \draw [blue] (t1) to [bend left] node [fill=white] {$S$} (t2);
312    \draw [blue] (t1) to [bend left] node [fill=white] {$L$} (l);
313    \draw [blue] (t1) to node [fill=white] {$C$} (c);
314    \end{tikzpicture}
315  $$ 
316\end{itemize}
317\end{frame}
318
319\begin{frame}%
320%[]
321\frametitle{Preserving returns}
322\begin{itemize}
323 \item How do we put to use the $C$ relation?
324 \item Define relation $R$ as
325 $$ \tikz[vcenter, start chain=going below, node distance=8mm] {
326     \node [on, is other, label=right:$s_1$] {}; \node [on, is other, label=right:$s_2$] {};
327     \draw (chain-1) -- node [fill=white] {$R$} (chain-2);
328 } \iff \tikz[vcenter, start chain=going left, node distance=8mm] {
329     \node [on, is other, label=right:$s_1$] {};
330     \node [on, is call, join=by {-, densely dashed}] {};
331     \node [on=going below, is call] {};
332     \node [on=going right, is other, label=right:$s_2$, join=by {-, blue, densely dashed}] {};
333     \draw (chain-2) -- node [fill=white] {$C$} (chain-3);
334     \draw [blue, implies] (chain-2) to [out=-45, in=90] ($(chain-3)!.5!(chain-4)$);
335 }$$
336\item Then ask
337 $$ \begin{tikzpicture}[every join/.style={ar}, join all, thick]
338     \begin{scope}[start chain=going below]
339        \node (s1) [on, is ret] {};
340        \node (t1) [on, is other] {};
341     \end{scope}
342    \begin{scope}[start chain, node distance=2mm, blue]
343    \node (s2) [on, is other, below=4mm of t1, black] {};
344    \node [on, is other] {};
345    \node [on, is other] {};
346    \node (c) [on, is ret] {};
347    \node (r) [node distance=3mm, on chain=going below, is other] {};
348    \node [on chain=going right, is other] {};
349    \node [on, is other] {};
350    \node (t2) [on, is other] {};
351    \end{scope}
352    \draw (s1) to [bend right=45] node [fill=white] {$S$} (s2);
353    \draw [blue] (t1) to [bend left=90, looseness=1] node [fill=white] {$S,L$} (t2);
354    \draw [blue] (t1) to [bend left=90, looseness=1.2] node [fill=white] {$R$} (r);
355    \end{tikzpicture}
356  $$ 
357
358\end{itemize}
359\end{frame}
360
361\begin{frame}%
362%[]
363\frametitle{All cases}
364\begin{columns}[t]
365\column{.4\linewidth}
366\begin{itemize}
367 \item \structure{Call} states
368 $$ \begin{tikzpicture}[every join/.style={ar}, join all, thick]
369     \begin{scope}[start chain=going above]
370        \node (s1) [on, call=f] {};
371        \node (t1) [on, is other] {};
372     \end{scope}
373    \begin{scope}[start chain, node distance=2mm, blue]
374    \node (s2) [on, is other, below=9mm of s1, black] {};
375    \node [on, is other] {};
376    \node [on, is other] {};
377    \node (c) [on, is call, label=above right:$f$] {};
378    \node (l) [node distance=3mm, on chain=going above, is other] {};
379    \node [on chain=going right, is other] {};
380    \node [on, is other] {};
381    \node (t2) [on, is other] {};
382    \end{scope}
383    \draw (s1) to node [fill=white] {$S$} (s2);
384    \draw [blue] (t1) to [bend left] node [fill=white] {$S$} (t2);
385    \draw [blue] (t1) to [bend left] node [fill=white] {$L$} (l);
386    \draw [blue] (t1) to node [fill=white] {$C$} (c);
387    \end{tikzpicture}
388  $$ 
389\end{itemize}
390\column{.4\linewidth}
391\begin{itemize}
392\item \structure{Return} states
393 $$ \begin{tikzpicture}[every join/.style={ar}, join all, thick]
394     \begin{scope}[start chain=going below]
395        \node (s1) [on, is ret] {};
396        \node (t1) [on, is other] {};
397     \end{scope}
398    \begin{scope}[start chain, node distance=2mm, blue]
399    \node (s2) [on, is other, below=4mm of t1, black] {};
400    \node [on, is other] {};
401    \node [on, is other] {};
402    \node (c) [on, is ret] {};
403    \node (r) [node distance=3mm, on chain=going below, is other] {};
404    \node [on chain=going right, is other] {};
405    \node [on, is other] {};
406    \node (t2) [on, is other] {};
407    \end{scope}
408    \draw (s1) to [bend right=45] node [fill=white] {$S$} (s2);
409    \draw [blue, overlay] (t1) to [bend left=90, looseness=1] node [fill=white] {$S,L$} (t2);
410    \draw [blue, overlay] (t1) to [bend left=90, looseness=1.2] node [fill=white] {$R$} (r);
411    \end{tikzpicture}
412  $$ 
413\end{itemize}
414\end{columns}
415\begin{columns}[t]
416\column{.4\linewidth}
417\begin{itemize}
418\item \structure{Branch} states
419 $$ \begin{tikzpicture}[every join/.style={ar}, join all, thick,
420                            every label/.style=overlay]
421     \begin{scope}[start chain=going right]
422        \node (s1) [on, is jump] {};
423        \node (t1) [on, is other, fill=white, label=above:$\alpha$] {};
424     \end{scope}
425    \begin{scope}[start chain, node distance=2mm, blue]
426    \node (s2) [on, is other, below=9mm of s1, black] {};
427    \node [on, is other] {};
428    \node [on, is other] {};
429    \node [on, is other] {};
430    \node [on, is other] {};
431    \node (t2) [on, is other] {};
432    \end{scope}
433    \draw (s1) to node [fill=white] {$S$} (s2);
434    \draw [blue] (t1) to node [fill=white] {$S,L$} (t2);
435    \end{tikzpicture}
436  $$ 
437\end{itemize}
438\column{.4\linewidth}
439\begin{itemize}
440 \item \structure{Other} states
441 $$ \begin{tikzpicture}[every join/.style={ar}, join all, thick]
442     \begin{scope}[start chain=going right]
443        \node (s1) [on, is other] {};
444        \node (t1) [on, is other] {};
445     \end{scope}
446    \begin{scope}[start chain, node distance=2mm, blue]
447    \node (s2) [on, is other, below=9mm of s1, black] {};
448    \node [on, is other] {};
449    \node [on, is other] {};
450    \node [on, is other] {};
451    \node [on, is other] {};
452    \node (t2) [on, is other] {};
453    \end{scope}
454    \draw (s1) to node [fill=white] {$S$} (s2);
455    \draw [blue] (t1) to node [fill=white] {$S,L$} (t2);
456    \end{tikzpicture}
457  $$ 
458\end{itemize}
459\end{columns}
460\vskip 20pt
461Notice that if you forget intensional information, you get back usual extensional
462simulation
463\end{frame}
464
465\begin{frame}%
466%[]
467\frametitle{The result}
468\begin{theorem}
469 Given relations $S$ and $C$ such that the variuous diagrams hold,
470 then
471 $$ \begin{tikzpicture}
472     \node (s1) [is other, label=above:$s_1$] {};
473     \node (m1) [is other, label=above:$m_1$, right=4cm of s1] {};
474     \node (t1) [is other, label=above:$t_1$, right=4cm of m1] {};
475     \draw [-stealth] (s1) -- node [above] {unstructured trace} (m1);
476     \draw [-stealth] (m1) -- node [above] {structured trace} (t1);
477     \node (s2) [is other, label=below:$s_2$, below=1cm of s1] {};
478     \draw (s1) -- node [fill=white] {$S,L$} (s2);
479     \begin{scope}[blue]
480     \node (m2) [is other, label=below:$m_2$, right=4cm of s2] {};
481     \node (t2) [is other, label=below:$t_2$, right=4cm of m2] {};
482     \draw [-stealth] (s2) -- node [below] {unstructured trace} (m2);
483     \draw [-stealth] (m2) -- node [below] {structured trace} (t2);
484     \path ($(s1)!.5!(m1)$) -- node [sloped] {\LARGE$\approx$} ($(s2)!.5!(m2)$);
485     \path ($(m1)!.5!(t1)$) -- node [sloped] {\LARGE$\approx$} ($(m2)!.5!(t2)$);
486     \end{scope}
487    \end{tikzpicture}
488$$
489\end{theorem}
490\begin{itemize}
491\item The issues with defining a good $S$ are no different than in extensional proofs
492\item $C$ is defined based on program counters only
493\end{itemize}
494\end{frame}
495%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
496\begin{frame}%
497%[]
498\frametitle{Back to back-end correctness}
499\begin{theorem}
500  $$ \begin{tikzpicture}
501     \node (s1) [is other, label=above:$s_1$] {};
502     \node (m1) [is other, label=above:$m_1$, right=4cm of s1] {};
503     \node (t1) [is other, label=above:$t_1$, right=4cm of m1] {};
504     \draw [-stealth] (s1) -- node [above] {unstructured trace} (m1);
505     \draw [-stealth] (m1) -- node [above] {structured trace} (t1);
506     \begin{scope}[blue]
507     \node (s2) [is other, label=below:$s_2$, below=1cm of s1] {};
508     \node (m2) [is other, label=below:$m_2$, right=4cm of s2] {};
509     \node (t2) [is other, label=below:$t_2$, right=4cm of m2] {};
510     \draw [-stealth] (s2) -- node [below] {unstructured trace} (m2);
511     \draw [-stealth] (m2) -- node [below] {structured trace} (t2);
512     \path ($(s1)!.5!(m1)$) -- node [sloped] {\LARGE$\approx$} ($(s2)!.5!(m2)$);
513     \path ($(m1)!.5!(t1)$) -- node [sloped] {\LARGE$\approx$} ($(m2)!.5!(t2)$);
514     \end{scope}
515     \node (l1) [left=of s1] {RTLabs:};
516     \node (l2) [left=of s2] {ASM:};
517     \node [rotate=-90, blue] at ($(l1)!.5!(l2)$) {$\Rightarrow$};
518    \end{tikzpicture}
519$$
520\end{theorem}
521\begin{itemize}
522 \item Defining $R$'s, proving diagrams, composing signle pass results bring us
523 halfway there
524 \item What about stack bounds?
525\end{itemize}
526
527\end{frame}
528%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
529
530\section{Dealing with the stack}
531
532\begin{frame}%
533%[]
534\frametitle{From an unbounded to a bounded stack}
535\begin{itemize}
536 \item In the front end, each call gets allocated a new stack space
537 \item In ASM, the stack is all in the (bounded) external memory
538 \item \structure{Somewhere in-between we must do the switch}
539 \item \alert{Two issues}:
540     \begin{itemize}
541     \item The stack overflow error does not come from a source execution error
542     \item When we change the stack layout, we need to remap values and thus states
543     \end{itemize}
544 \item Mixing the above issues within a compilation pass complicates things
545 \item \structure{Our plan}: do the switch within a single language, one issue at a time
546\end{itemize}
547
548\end{frame}
549
550\begin{frame}%
551%[]
552\frametitle{Three semantics for RTL}
553\begin{enumerate}
554 \item \structure{Independent stack spaces}: just like RTLabs, no overflow errors
555 \item \structure{Independent stack spaces with overflow error}: a stack usage
556 field is used to induce an error
557 \begin{itemize}
558  \item We use stack usage hypothesis (coming from front-end correctness)
559  to ensure error does not occur
560  \item States need not be remapped
561 \end{itemize}
562 \item \structure{Unique bounded stack space}
563 \begin{itemize}
564  \item Remap states, absence of stack overflow errors ensures this can be done
565  correctly
566 \end{itemize}
567\end{enumerate}
568\begin{itemize}
569 \item From now on, forget stack bounds: the fact that they are respected comes
570 from absence of errors in the trace
571\end{itemize}
572\end{frame}
573%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
574\begin{frame}%
575%[]
576\frametitle{Evolution of stack usage}
577Once the stack is unique, the space required evolves during compilation
578\begin{itemize}
579\item In RTL only referenced local variables end on stack
580\item In ERTL function parameters too
581\item In LTL the spilled variables are added
582\end{itemize}
583$$
584\begin{tikzpicture}[thick, line cap=round,
585    m/.style = {execute at begin node=$, execute at end node=$}]
586\begin{scope}[every node/.style={draw, rectangle,
587    minimum width=1.25cm, m}, every label/.style={minimum width=0, draw=none}]
588    \node (main src) [minimum height=.5cm]
589        [label=left:main] {};
590    \node (f1 src) [above=-1pt of main src,minimum height=1cm]
591        [label=left:f] {};
592    \node (g src) [above=-1pt of f1 src,minimum height=.75cm]
593        [label=left:g] {};
594    \node (f2 src) [above=-1pt of g src,minimum height=1cm]
595        [label=left:f] {};
596
597    \node (main tgt) at ([xshift=2cm]main src.south east) [anchor=south west,minimum height=1cm]
598        [label=right:main] {};
599    \node (f1 tgt) [above=-1pt of main tgt,minimum height=1.25cm]
600        [label=right:f] {};
601    \node (g tgt) [above=-1pt of f1 tgt,minimum height=1.5cm]
602        [label=right:g] {};
603    \node (f2 tgt) [above=-1pt of g tgt,minimum height=1.25cm]
604        [label=right:f] {};
605
606\end{scope}
607\foreach \x/\off in {main/.5, f1/1, g/.75, f2/1} {
608    \draw [densely dashed, semithick]
609        ([yshift=1pt]\x\space src.south east) --
610        ([yshift=1pt]\x\space tgt.south west);
611    \draw [densely dashed, semithick] (\x\space src.north east) --
612        ([yshift=\off cm]\x\space tgt.south west) coordinate (tmp)
613        -- (tmp-|\x\space tgt.east);
614    \fill [pattern=dots, opacity=.5] (tmp) |- (\x\space tgt.north east) |- (tmp);
615    \path (\x\space src.east) -- node [sloped] {$\hookrightarrow$}
616        ($(\x\space tgt.south west)!.5!(tmp)$);
617}
618\node (heading tgt) [above=.125cm of f2 tgt] {target stack};
619\node (heading src) at (heading tgt-|f2 src) {source stack};
620
621\draw [|->] (heading src) -- (heading tgt);
622\end{tikzpicture}
623$$
624\end{frame}
625
626\begin{frame}%
627%[]
628\frametitle{Using a parametric stack size}
629\begin{columns}[c]
630\column{.5\linewidth}
631\begin{itemize}
632 \item Remapping locations complicates things
633 \item We opted for \structure{parametric} stack sizes (i.e.\ a family of
634    semantics for each language), equal on both sides of each pass
635 \item Correctness results require some lower bounds for the parameter
636\end{itemize}
637\column{.6\linewidth}
638\begin{tikzpicture}[thick, line cap=round,
639    m/.style = {execute at begin node=$, execute at end node=$}]
640\begin{scope}[every node/.style={draw, rectangle,
641    minimum width=1.25cm, m}, every label/.style={minimum width=0, draw=none}]
642    \node (main src) [minimum height=1.25cm]
643        [label=left:main] {};
644    \node (f1 src) [above=-1pt of main src,minimum height=1.75cm]
645        [label=left:f] {};
646    \node (g src) [above=-1pt of f1 src,minimum height=1.75cm]
647        [label=left:g] {};
648    \node (f2 src) [above=-1pt of g src,minimum height=1.75cm]
649        [label=left:f] {};
650
651    \node (main tgt) at ([xshift=2cm]main src.south east) [anchor=south west,minimum height=1.25cm]
652        [label=right:main] {};
653    \node (f1 tgt) [above=-1pt of main tgt,minimum height=1.75cm]
654        [label=right:f] {};
655    \node (g tgt) [above=-1pt of f1 tgt,minimum height=1.75cm]
656        [label=right:g] {};
657    \node (f2 tgt) [above=-1pt of g tgt,minimum height=1.75cm]
658        [label=right:f] {};
659
660\end{scope}
661\foreach \x/\off/\o in {main/.5/1, f1/1/1.25, g/.75/1.5, f2/1/1.25} {
662    \draw [densely dashed, semithick]
663        ([yshift=1pt]\x\space src.south east) --
664        ([yshift=1pt]\x\space tgt.south west);
665    \draw [densely dashed, semithick]
666        ([yshift=\off cm]\x\space src.south west) --
667        ([yshift=\off cm]\x\space tgt.south west) coordinate (tmp)
668        -- (tmp-|\x\space tgt.east);
669    \fill [pattern=dots, opacity=.5] (tmp) --
670        ([yshift=\o cm]\x\space tgt.south west) coordinate (tmp2) -| (tmp-|\x\space tgt.east) -- (tmp);
671    \draw [densely dashed] (tmp2) -- (tmp2-|\x\space tgt.east);
672    \fill [pattern=north east lines, opacity=.5]
673        (tmp2) |- (\x\space tgt.north east) |- (tmp2);
674    \path ($(\x\space src.south east)!.5!(\x\space src.east|-tmp)$) --
675        node {$\hookrightarrow$}
676        ($(\x\space tgt.south west)!.5!(tmp)$);
677    \fill [pattern=north east lines, opacity=.5]
678        (\x\space src.west|-tmp) coordinate (tmp) |- (\x\space src.north east) |- (tmp);
679}
680\node (heading tgt) [above=.125cm of f2 tgt] {target stack};
681\node (heading src) at (heading tgt-|f2 src) {source stack};
682
683\draw [|->] (heading src) -- (heading tgt);
684\end{tikzpicture}
685\end{columns}
686\end{frame}
687%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
688\begin{frame}%
689%[]
690\section{Assembler correctness}
691
692\frametitle{Assembler correctness}
693Assembler outputs \structure{labelled} object code and the \structure{cost map}
694\begin{theorem}
695  $$ \begin{tikzpicture}
696     \node (s1) [is other, label=above:$s_1$] {};
697     \node (m1) [is other, label=above:$m_1$, right=4cm of s1] {};
698     \node (t1) [is other, label=above:$t_1$, right=4cm of m1] {};
699     \draw [-stealth] (s1) -- node [above] {unstructured trace} (m1);
700     \draw [-stealth] (m1) -- node [above] {structured trace} (t1);
701     \begin{scope}[blue]
702     \node (s2) [is other, label=below:$s_2$, below=1cm of s1] {};
703     \node (m2) [is other, label=below:$m_2$, right=4cm of s2] {};
704     \node (t2) [is other, label=below:$t_2$, right=4cm of m2] {};
705     \draw [-stealth] (s2) -- node [below] {unstructured trace} (m2);
706     \draw [-stealth] (m2) -- node [below] {structured trace} (t2);
707     \path ($(s1)!.5!(m1)$) -- node [sloped] {\LARGE$\approx$} ($(s2)!.5!(m2)$);
708     \path ($(m1)!.5!(t1)$) -- node [sloped] {\LARGE$\approx$} ($(m2)!.5!(t2)$);
709     \end{scope}
710     \node (l1) [left=of s1] {ASM:};
711     \node (l2) [left=of s2] {LOC:};
712     \node [rotate=-90, blue] at ($(l1)!.5!(l2)$) {$\Rightarrow$};
713    \end{tikzpicture}
714$$
715and
716$$
717\sum_{\mathclap{l\in\text{ASM structured trace}}}\costmap(l) =
718\clock(t_2) - \clock(m_2)$$
719\end{theorem}
720\end{frame}
721%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
722\begin{frame}%
723%[]
724\frametitle{Preserving the traces}
725\begin{itemize}
726 \item The preservation of structured traces part is as in the back-end
727 \item A novelty in the extensional part is our proof of the correctness
728 of a branch displacement algorithm
729\end{itemize}
730\end{frame}
731%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
732\begin{frame}%
733%[]
734\frametitle{Proving the cost map correct}
735\begin{itemize}
736 \item The \structure{cost map} is based on a static analysis
737 \begin{itemize}
738     \item For each label, start from the labelled instruction
739     \item While \alert{no branch} and \alert{no label} is encountered,
740         sum the clock count of the instruction
741 \end{itemize}
742 \item Correctness is based on dealing with a \structure{structured trace}
743 \begin{itemize}
744 \item Branching states are always followed by labels
745 \item When returning from a call, we land at the correct point in the block
746     whose cost was already paid by a label
747 \end{itemize}
748\end{itemize}
749
750\end{frame}
751
752\end{document}
753
754% LocalWords:  LFCS Matita CerCo intensional WCET toolchain CompCert Clight ASM
755% LocalWords:  reexecutes subtrace RTLabs subtraces
Note: See TracBrowser for help on using the repository browser.