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

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

back-end slides

File size: 30.4 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\item The Matita proof is \structure{complete}
494\end{itemize}
495\end{frame}
496%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
497\begin{frame}%
498%[]
499\frametitle{Back to back-end correctness}
500\begin{theorem}
501  $$ \begin{tikzpicture}
502     \node (s1) [is other, label=above:$s_1$] {};
503     \node (m1) [is other, label=above:$m_1$, right=4cm of s1] {};
504     \node (t1) [is other, label=above:$t_1$, right=4cm of m1] {};
505     \draw [-stealth] (s1) -- node [above] {unstructured trace} (m1);
506     \draw [-stealth] (m1) -- node [above] {structured trace} (t1);
507     \begin{scope}[blue]
508     \node (s2) [is other, label=below:$s_2$, below=1cm of s1] {};
509     \node (m2) [is other, label=below:$m_2$, right=4cm of s2] {};
510     \node (t2) [is other, label=below:$t_2$, right=4cm of m2] {};
511     \draw [-stealth] (s2) -- node [below] {unstructured trace} (m2);
512     \draw [-stealth] (m2) -- node [below] {structured trace} (t2);
513     \path ($(s1)!.5!(m1)$) -- node [sloped] {\LARGE$\approx$} ($(s2)!.5!(m2)$);
514     \path ($(m1)!.5!(t1)$) -- node [sloped] {\LARGE$\approx$} ($(m2)!.5!(t2)$);
515     \end{scope}
516     \node (l1) [left=of s1] {RTLabs:};
517     \node (l2) [left=of s2] {ASM:};
518     \node [rotate=-90, blue] at ($(l1)!.5!(l2)$) {$\Rightarrow$};
519    \end{tikzpicture}
520$$
521\end{theorem}
522\begin{itemize}
523 \item Defining $R$'s, proving diagrams, composing signle pass results bring us
524 halfway there
525 \item What about stack bounds?
526\end{itemize}
527
528\end{frame}
529%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
530
531\section{Dealing with the stack}
532
533\begin{frame}%
534%[]
535\frametitle{From an unbounded to a bounded stack}
536\begin{itemize}
537 \item In the front end, each call gets allocated a new stack space
538 \item In ASM, the stack is all in the (bounded) external memory
539 \item \structure{Somewhere in-between we must do the switch}
540 \item \alert{Two issues}:
541     \begin{itemize}
542     \item The stack overflow error does not come from a source execution error
543     \item When we change the stack layout, we need to remap values and thus states
544     \end{itemize}
545 \item Mixing the above issues within a compilation pass complicates things
546 \item \structure{Our plan}: do the switch within a single language, one issue at a time
547\end{itemize}
548
549\end{frame}
550
551\begin{frame}%
552%[]
553\frametitle{Three semantics for RTL}
554\begin{enumerate}
555 \item \structure{Independent stack spaces}: just like RTLabs, no overflow errors
556 \item \structure{Independent stack spaces with overflow error}: a stack usage
557 field is used to induce an error
558 \begin{itemize}
559  \item We use stack usage hypothesis (coming from front-end correctness)
560  to ensure error does not occur
561  \item States need not be remapped
562 \end{itemize}
563 \item \structure{Unique bounded stack space}
564 \begin{itemize}
565  \item Remap states, absence of stack overflow errors ensures this can be done
566  correctly
567 \end{itemize}
568\end{enumerate}
569\begin{itemize}
570 \item From now on, forget stack bounds: the fact that they are respected comes
571 from absence of errors in the trace
572\end{itemize}
573\end{frame}
574%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
575\begin{frame}%
576%[]
577\frametitle{Evolution of stack usage}
578Once the stack is unique, the space required evolves during compilation
579\begin{itemize}
580\item In RTL only referenced local variables end on stack
581\item In ERTL function parameters too
582\item In LTL the spilled variables are added
583\end{itemize}
584$$
585\begin{tikzpicture}[thick, line cap=round,
586    m/.style = {execute at begin node=$, execute at end node=$}]
587\begin{scope}[every node/.style={draw, rectangle,
588    minimum width=1.25cm, m}, every label/.style={minimum width=0, draw=none}]
589    \node (main src) [minimum height=.5cm]
590        [label=left:main] {};
591    \node (f1 src) [above=-1pt of main src,minimum height=1cm]
592        [label=left:f] {};
593    \node (g src) [above=-1pt of f1 src,minimum height=.75cm]
594        [label=left:g] {};
595    \node (f2 src) [above=-1pt of g src,minimum height=1cm]
596        [label=left:f] {};
597
598    \node (main tgt) at ([xshift=2cm]main src.south east) [anchor=south west,minimum height=1cm]
599        [label=right:main] {};
600    \node (f1 tgt) [above=-1pt of main tgt,minimum height=1.25cm]
601        [label=right:f] {};
602    \node (g tgt) [above=-1pt of f1 tgt,minimum height=1.5cm]
603        [label=right:g] {};
604    \node (f2 tgt) [above=-1pt of g tgt,minimum height=1.25cm]
605        [label=right:f] {};
606
607\end{scope}
608\foreach \x/\off in {main/.5, f1/1, g/.75, f2/1} {
609    \draw [densely dashed, semithick]
610        ([yshift=1pt]\x\space src.south east) --
611        ([yshift=1pt]\x\space tgt.south west);
612    \draw [densely dashed, semithick] (\x\space src.north east) --
613        ([yshift=\off cm]\x\space tgt.south west) coordinate (tmp)
614        -- (tmp-|\x\space tgt.east);
615    \fill [pattern=dots, opacity=.5] (tmp) |- (\x\space tgt.north east) |- (tmp);
616    \path (\x\space src.east) -- node [sloped] {$\hookrightarrow$}
617        ($(\x\space tgt.south west)!.5!(tmp)$);
618}
619\node (heading tgt) [above=.125cm of f2 tgt] {target stack};
620\node (heading src) at (heading tgt-|f2 src) {source stack};
621
622\draw [|->] (heading src) -- (heading tgt);
623\end{tikzpicture}
624$$
625\end{frame}
626
627\begin{frame}%
628%[]
629\frametitle{Using a parametric stack size}
630\begin{columns}[c]
631\column{.5\linewidth}
632\begin{itemize}
633 \item Remapping locations complicates things
634 \item We opted for \structure{parametric} stack sizes (i.e.\ a family of
635    semantics for each language), equal on both sides of each pass
636 \item Correctness results require some lower bounds for the parameter
637\end{itemize}
638\column{.6\linewidth}
639\begin{tikzpicture}[thick, line cap=round,
640    m/.style = {execute at begin node=$, execute at end node=$}]
641\begin{scope}[every node/.style={draw, rectangle,
642    minimum width=1.25cm, m}, every label/.style={minimum width=0, draw=none}]
643    \node (main src) [minimum height=1.25cm]
644        [label=left:main] {};
645    \node (f1 src) [above=-1pt of main src,minimum height=1.75cm]
646        [label=left:f] {};
647    \node (g src) [above=-1pt of f1 src,minimum height=1.75cm]
648        [label=left:g] {};
649    \node (f2 src) [above=-1pt of g src,minimum height=1.75cm]
650        [label=left:f] {};
651
652    \node (main tgt) at ([xshift=2cm]main src.south east) [anchor=south west,minimum height=1.25cm]
653        [label=right:main] {};
654    \node (f1 tgt) [above=-1pt of main tgt,minimum height=1.75cm]
655        [label=right:f] {};
656    \node (g tgt) [above=-1pt of f1 tgt,minimum height=1.75cm]
657        [label=right:g] {};
658    \node (f2 tgt) [above=-1pt of g tgt,minimum height=1.75cm]
659        [label=right:f] {};
660
661\end{scope}
662\foreach \x/\off/\o in {main/.5/1, f1/1/1.25, g/.75/1.5, f2/1/1.25} {
663    \draw [densely dashed, semithick]
664        ([yshift=1pt]\x\space src.south east) --
665        ([yshift=1pt]\x\space tgt.south west);
666    \draw [densely dashed, semithick]
667        ([yshift=\off cm]\x\space src.south west) --
668        ([yshift=\off cm]\x\space tgt.south west) coordinate (tmp)
669        -- (tmp-|\x\space tgt.east);
670    \fill [pattern=dots, opacity=.5] (tmp) --
671        ([yshift=\o cm]\x\space tgt.south west) coordinate (tmp2) -| (tmp-|\x\space tgt.east) -- (tmp);
672    \draw [densely dashed] (tmp2) -- (tmp2-|\x\space tgt.east);
673    \fill [pattern=north east lines, opacity=.5]
674        (tmp2) |- (\x\space tgt.north east) |- (tmp2);
675    \path ($(\x\space src.south east)!.5!(\x\space src.east|-tmp)$) --
676        node {$\hookrightarrow$}
677        ($(\x\space tgt.south west)!.5!(tmp)$);
678    \fill [pattern=north east lines, opacity=.5]
679        (\x\space src.west|-tmp) coordinate (tmp) |- (\x\space src.north east) |- (tmp);
680}
681\node (heading tgt) [above=.125cm of f2 tgt] {target stack};
682\node (heading src) at (heading tgt-|f2 src) {source stack};
683
684\draw [|->] (heading src) -- (heading tgt);
685\end{tikzpicture}
686\end{columns}
687\end{frame}
688\section{Details on the passes}
689%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
690\begin{frame}%
691%[]
692\frametitle{RTLabs $\to$ RTL}
693\begin{itemize}
694 \item Most of the effort must go to the \structure{extensional} part, as multi-byte operations
695 are replaced by sequences of single byte operations
696 \item Status: sketched
697\end{itemize}
698\end{frame}
699%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
700\begin{frame}%
701%[]
702\frametitle{RTL $\to$ ERTL}
703\begin{itemize}
704 \item A \structure{graph} pass
705 \item Implements the calling convention, with the first accesses to stack
706 \item From the intensional point of view: calls have prefixes and suffixes, and
707 function bodies have preambles
708 \item Status: the scaffolding underlying all graph passes
709 is done. The proof obligations regarding this particular pass are open
710\end{itemize}
711\end{frame}
712%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
713\begin{frame}%
714%[]
715\frametitle{ERTL $\to$ LTL}
716\begin{itemize}
717\item A \structure{graph} pass
718\item Register allocation, spilling, saving and restoring callee-saved hardware registers
719\item From the intensional point of view, calls to pointer have prefixes, and
720function bodies have preambles
721\item  Status: the scaffolding underlying all graph passes
722 is done. The proof obligations regarding this particular pass are almost finished
723\end{itemize}
724\end{frame}
725%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
726\begin{frame}%
727%[]
728\frametitle{LTL $\to$ LIN}
729\begin{itemize}
730 \item A \structure{linearisation}
731 \item From the intensional point of view, calls can have suffixes (GOTOs)
732 \item Status: the generic linearisation scaffolding is complete.
733 The proof obligations regarding this particular pass are open (but easy)
734\end{itemize}
735
736\end{frame}
737%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
738\begin{frame}%
739%[]
740\frametitle{LIN $\to$ ASM}
741\begin{itemize}
742\item A 1-to-1 simulation
743\item Function names and code labels are collapsed in the same global namespace
744\item Status: open
745\end{itemize}
746\end{frame}
747%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
748
749\section{Assembler correctness}
750
751\begin{frame}%
752%[]
753\frametitle{Assembler correctness}
754Assembler outputs \structure{labelled} object code and the \structure{cost map}
755\begin{theorem}
756  $$ \begin{tikzpicture}
757     \node (s1) [is other, label=above:$s_1$] {};
758     \node (m1) [is other, label=above:$m_1$, right=4cm of s1] {};
759     \node (t1) [is other, label=above:$t_1$, right=4cm of m1] {};
760     \draw [-stealth] (s1) -- node [above] {unstructured trace} (m1);
761     \draw [-stealth] (m1) -- node [above] {structured trace} (t1);
762     \begin{scope}[blue]
763     \node (s2) [is other, label=below:$s_2$, below=1cm of s1] {};
764     \node (m2) [is other, label=below:$m_2$, right=4cm of s2] {};
765     \node (t2) [is other, label=below:$t_2$, right=4cm of m2] {};
766     \draw [-stealth] (s2) -- node [below] {unstructured trace} (m2);
767     \draw [-stealth] (m2) -- node [below] {structured trace} (t2);
768     \path ($(s1)!.5!(m1)$) -- node [sloped] {\LARGE$\approx$} ($(s2)!.5!(m2)$);
769     \path ($(m1)!.5!(t1)$) -- node [sloped] {\LARGE$\approx$} ($(m2)!.5!(t2)$);
770     \end{scope}
771     \node (l1) [left=of s1] {ASM:};
772     \node (l2) [left=of s2] {LOC:};
773     \node [rotate=-90, blue] at ($(l1)!.5!(l2)$) {$\Rightarrow$};
774    \end{tikzpicture}
775$$
776and
777$$
778\sum_{\mathclap{l\in\text{ASM structured trace}}}\costmap(l) =
779\clock(t_2) - \clock(m_2)$$
780\end{theorem}
781\end{frame}
782%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
783\begin{frame}%
784%[]
785\frametitle{Preserving the traces}
786\begin{itemize}
787 \item The preservation of structured traces part is as in the back-end
788 \item A novelty in the extensional part is our proof of the correctness
789 of a branch displacement algorithm
790\end{itemize}
791\end{frame}
792%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
793\begin{frame}%
794%[]
795\frametitle{Proving the cost map correct}
796\begin{itemize}
797 \item The \structure{cost map} is based on a static analysis
798 \begin{itemize}
799     \item For each label, start from the labelled instruction
800     \item While \alert{no branch} and \alert{no label} is encountered,
801         sum the clock count of the instruction
802 \end{itemize}
803 \item Correctness is based on dealing with a \structure{structured trace}
804 \begin{itemize}
805 \item Branching states are always followed by labels
806 \item When returning from a call, we land at the correct point in the block
807     whose cost was already paid by a label
808 \end{itemize}
809\end{itemize}
810
811\end{frame}
812
813\end{document}
814
815% LocalWords:  LFCS Matita CerCo intensional WCET toolchain CompCert Clight ASM
816% LocalWords:  reexecutes subtrace RTLabs subtraces
Note: See TracBrowser for help on using the repository browser.