source: LTS/DICE2014/slides.tex @ 3534

Last change on this file since 3534 was 3478, checked in by piccolo, 5 years ago

fixed costlabels

File size: 19.8 KB
Line 
1%%% \listfiles %%%%%%%%%%%%%%%%%% POWERDOT %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2\documentclass[
3%% mode=present,
4%% mode=print,
5% mode=handout,
6% nopagebreaks,
7%paper=a4paper,
8paper=screen,
9%% display=slidesnotes,
10%% size=11pt,
11%% size=12pt,
12%% size=14pt,
13%% size=17pt,
14%% size=20pt,
15  style=simple,
16%% style=fyma,
17%% orient=portrait,
18%% blackslide,
19%% fleqn,
20%  clock,
21]{powerdot}
22%\documentclass[mode=handout,nopagebreaks,paper=a4paper]{powerdot}
23\usepackage{multirow}
24%\usepackage[latin1]{inputenc}
25\usepackage{pstricks,pst-node,pst-text,pst-tree}
26%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
27% Work around some bugs in marvosym with overwriting symbols:
28\let\labOrigRightarrow=\Rightarrow
29        \RequirePackage{marvosym}
30\let\Rightarrow=\labOrigRightarrow
31%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
32%\usepackage{mathabx}
33\usepackage{amsmath}
34\usepackage{amsfonts}
35\usepackage{amsbsy}
36\usepackage{amssymb}
37\usepackage{latexsym}
38\usepackage[mathscr]{euscript}
39%\usepackage{framed}
40%\usepackage[framed]{ntheorem}
41\usepackage[all,color,dvips]{xy}
42%\UseCrayolaColors
43%\usepackage{amsfonts}
44%\usepackage{graphicx}
45%\usepackage{color}
46\usepackage{colortbl}
47\usepackage{stmaryrd}
48%\usepackage{mathabx}
49%\usepackage[bbgreekl]{mathbbol}
50%\usepackage{epic,eepic}
51%\usepackage{xcolor}
52%\usepackage{pifont}
53\usepackage{proof}
54\usepackage{cmll}
55
56
57%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
58% Personal VERBATIM and CODE
59%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
60%\usepackage{fancybox}
61%\usepackage{fancyvrb}
62%\usepackage{verbatim}
63%\usepackage{listings}
64%\lstnewenvironment{code}{%
65%\lstset{frame=single,escapeinside=`',
66%   backgroundcolor=\color{yellow!20},
67%   language=lisp,
68%   basicstyle=\footnotesize\ttfamily}}{}
69
70%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
71% Personal Definition of new colors
72\usepackage{crayola}
73%%%%% COLORI TRASPARENTI %%%%%%%%%%%%%%%
74%\usepackage{pstricks-add}
75% \defineTColor{TRed}{red}
76% \defineTColor{TGreen}{green}
77% \defineTColor{TBlue}{blue}
78% \defineTColor{TBlue}{blue}
79% \defineTColor{TLemon}{LemonChiffon}
80%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81\usepackage{listings}
82\def\lstlanguagefiles{lst-grafite.tex}
83
84
85\def\tuple#1{\langle #1 \rangle}
86\input{unimacro.tex}
87%\newcommand\emslide[3]{\onslide*{#1}{#2}\onslide*{#3}{\psframebox[fillstyle=solid,fillcolor=Yellow,linecolor=Yellow]{#2}}}
88
89\title{\blue The Labelling Approach to Precise Resource Analysis on the Source Code, Revisited\\[3mm]}
90\author{
91\hspace*{9mm}  \begin{tabular}{l}
92  {\red Mauro Piccolo} \\[1mm]
93  %\href{http://www.di.unito.it/~paolini}{\red Luca Paolini} \\[1mm]
94  %{\tt paolini@di.unito.it}\\[1mm]
95  {Universit\`a di Torino}\\
96  {Dipartimento di Informatica}\\[3mm]
97  {\red A joint work with Claudio Sacerdoti Coen and Paolo Tranquilli}\\[3mm]
98\end{tabular}
99}
100\date{\hspace*{9mm} DICE 2014 Grenoble, 6 April 2014}
101
102\begin{document}
103\maketitle
104\begin{wideslide}{Concrete and certified complexity}
105$\;$\\[-7mm]
106\includegraphics[width=\textwidth]{code.eps}
107\\[-5mm]
108\begin{itemize}
109\item Reasoning about the complexity is rather made on the source.\\[-2mm]
110\item Concrete execution costs are better guess on the binary code.
111\end{itemize}
112\begin{center}
113\\[-10mm]
114How can we {\blue lift} in a provably correct way information on the execution cost of the binary code to cost annotation on the source code?
115\end{center}
116\end{wideslide}
117
118\begin{wideslide}[method=direct,toc=Labelling approach]{Labelling approach (Ayache, Amadio and R\'egis-Gianas)}
119The user writes the program
120\begin{lstlisting}
121I1;
122for(int i=0;i<2;i++){ 
123  I2;
124}
125\end{lstlisting}
126\end{wideslide}
127
128\begin{wideslide}[method=direct,toc=Labelling approach]{Labelling approach}
129The program will be processed by a special pre-compiler which inserts some label emission statements
130\begin{lstlisting}
131EMIT L1;
132I1;
133for(int i=0;i<2;i++){ 
134  EMIT L2;
135  I2;
136}
137EMIT L3;
138\end{lstlisting}
139\end{wideslide}
140
141\begin{wideslide}[method=file,toc=Labelling approach]{Labelling approach}
142\onslide*{1}{The program is then compiled into an object code emitting the same sequence of labels}
143\onslide*{2}{The object code is processed by a static code analyzer to determine the cost of each block of code}
144\begin{center}
145\begin{tabular}{l l l}
146\begin{lstlisting}
147EMIT L1;
148I1;
149for(int i=0;i<2;i++){ 
150  EMIT L2;
151  I2;
152}
153EMIT L3;
154\end{lstlisting}
155&$\qquad$&
156\begin{lstlisting}
157    EMIT L1;
158    I3
159l1: COND l1
160    EMIT L2
161    I4
162    GOTO l1
163l2: EMIT L3
164\end{lstlisting}
165\end{tabular}
166\end{center}
167\onslide*{2}{
168\begin{center}
169\begin{tabular}{|l|l|}
170\hline
171Label & Cost \\
172\hline
173L1 & $cost(I3) + cost(COND \ l1) = k_1$ \\
174L2 & $cost(I4) + cost(GOTO \ l1) = k_2$ \\
175L3 & $k_3$\\
176\hline
177\end{tabular}
178\end{center}
179}
180\end{wideslide}
181\begin{wideslide}[method=direct]{Labelling approach}
182The complier gives an instrumented version of the source code
183\begin{center}
184\begin{tabular}{l l l}
185\begin{lstlisting}
186cost += k_1
187instr 1;
188for(int i=0;i<2;i++){ 
189  cost += k_2
190  instr 2;
191}
192cost += k_3
193\end{lstlisting}
194&$\qquad$&
195\begin{lstlisting}
196    EMIT L1;
197    instr 3
198l1: COND l1
199    EMIT L2
200    instr 4
201    GOTO l1
202l2: EMIT L3
203\end{lstlisting}
204\end{tabular}
205\end{center}
206$\;$ \\
207\psshadowbox{
208\begin{minipage}{10.5cm}
209\centering We can make assertions on the variable cost which contains the {\red precise} cost of the computation.
210\end{minipage}
211}
212$\;$\\[3mm]
213Precise means that the predicted cost and the real one is bounded by a constant $\delta$ that depends only on the program (not on the input!).
214\end{wideslide}
215
216\begin{wideslide}{Certified complexity}
217$\;$\\[-9mm]
218\begin{center}
219\includegraphics[width=6cm]{cerco.eps}
220\end{center}
221This talk:
222\psshadowbox{
223\begin{minipage}{12cm}
224\begin{itemize}
225\item We revise the labelling approach to lift some restriction: {\red instructions having only one predecessor} and {\red absence of function calls}.
226\item We replace simple status independent costs with arbitrary semantics domains used in {\red abstract interpretation} to analyze caches, pipelines,$\ldots$.
227\item All the presented results are formalized in the {\red Matita proof assistant}.
228\end{itemize}
229\end{minipage}
230}
231\end{wideslide}
232
233
234
235\begin{wideslide}[method=direct]{Conditional statements and multiple predecessors}
236$\;$\\[-4mm]
237{\red Assumptions:}
238\psshadowbox{
239\begin{minipage}{12cm}
240\begin{itemize}
241\item Each object code instruction should fall into the scope of a label.
242\item Each object code instruction having multiple successors (e.g. conditionals) should pass control to basic blocks starting with a label emission statement.
243\item The cost of the conditional instruction should be the same whatever branch is taken.
244\end{itemize}
245\end{minipage}
246} \\[4mm]
247{\red Problem!} \\
248\begin{tabular}[t]{l l l l l}
249\begin{lstlisting}
250if(E){
251  EMIT L;
252  I;
253}
254\end{lstlisting}
255& $\qquad\qquad$ &
256\begin{lstlisting}
257    SJNEQ l1
258    JUMP l3
259l1: JUMP l2
260...
261l2: EMIT L
262    I;
263\end{lstlisting}
264& $\qquad\qquad$ &
265\begin{lstlisting}
266    SJNEQ l1
267    JUMP l3
268l1: EMIT L
269    JUMP l2
270...
271l2: I;
272\end{lstlisting}
273\end{tabular}
274\end{wideslide}
275
276\begin{wideslide}[method=direct]{Solution: labelled transition system semantics}
277\begin{itemize}
278\item We incorporate label emission in the semantics of the instructions.
279\item No more label emission statements.
280\end{itemize}
281\begin{center}
282\begin{tabular}{ll l}
283\begin{lstlisting}
284swith(E){
285  case e1 :
286  Emit L1;
287  I1;
288  case e2 :
289  Emit L2;
290  I2;
291}
292\end{lstlisting} &$\qquad$&
293\begin{lstlisting}
294swith(E){
295  case e1,L1 :
296
297  I1;
298  case L3,e2,L2 : //L3 emitted coming
299                  // from case e1
300  I2;
301}
302\end{lstlisting}
303\end{tabular}
304\end{center}
305% \begin{lstlisting}[language=Grafite]
306% record abstract_status : Type[2] ≝
307%  { as_status :> Type[0]
308%  ; as_execute : ActionLabel → relation as_status
309%  ; as_syntactical_succ : relation as_status
310%  ; as_classify : as_status → status_class
311%  ; as_initial : as_status → bool
312%  ; as_final : as_status → bool
313%  ; jump_emits : ∀s1,s2,l.as_classify ... s1 = cl_jump →
314%       as_execute l s1 s2 → is_non_silent_cost_act l
315%  }.
316% \end{lstlisting}
317\end{wideslide}
318
319\begin{wideslide}[method=file]{Function calls}
320\begin{center}
321\begin{tabular}{l l l}
322\begin{lstlisting}
323void main(){
324  EMIT L1;
325  I1;
326  (*f)();
327  I2;
328}
329
330void g(){
331  EMIT L2;
332  I3;
333}
334\end{lstlisting}
335& $\qquad\qquad$ &
336\begin{lstlisting}
337main :
338  EMIT L1
339  I4
340  CALL
341  I5
342  RETURN
343
344g :
345  EMIT L2
346  I6;
347  RETURN
348\end{lstlisting}
349\end{tabular}
350\end{center}
351What label should pay the cost for the block I5? \\
352\onslide{2}{
353{\red The only reasonable answer is L1!}
354}
355\end{wideslide}
356
357\begin{wideslide}{Label emission and function calls}
358$\;$ \\[-5mm]
359\psshadowbox{
360\begin{minipage}{12cm}
361The scope of labels should extend to the next label emission statement or the end of the function, stepping over function calls.
362\end{minipage}
363}\\[3mm]
364\onslide{2-}{
365{\red Assumptions:}
366\begin{itemize}
367\item<2-> All the instruction in the (static) block are reached during computation.
368\item<2-> The cost function should be commutative.
369\end{itemize}
370}
371\onslide{3-}{
372{\red Problems:}
373\begin{itemize}
374\item<3-> It does not work with {\blue non-commutative cost functions}. Because of stateful hardware components (cache, pipelines ...) this method does not scale to {\blue modern hardware}.
375\item<3-> It does not work with {\blue compiler that do not respect the calling structure} of the source code because it is not possible to statically predict {\blue which instruction will be executed after a function return}.
376\end{itemize}}
377\end{wideslide}
378
379\begin{wideslide}{First solution: structured traces}
380\onslide*{1}{
381\begin{itemize}
382\item The usual notion of {\red flat execution trace} is inadequate for a simulation argument.
383\item {\red Embed the call/return} into execution trace.
384\item Traces of called function are {\red nested}, invariants on position of costlabels are {\red enforced} and steps are grouped {\red according to costlabels}.
385\end{itemize}
386}
387\onslide*{2-}{
388\begin{tabular}{l c}
389\onslide*{3,4,5}{\green}$\tt EMIT \; L_1$ &  \onslide*{2,3,4}{{\red Flat trace}} \onslide*{5}{{\red Structured trace}}\\
390\onslide*{3,4,5}{\green}$\tt I_1$ & \multirow{7}{*}{
391\onslide*{2,3,4}{
392\xymatrix{ \onslide*{3,4}{\green} \bullet \onslide*{1,2}{\ar[r]^{{\tt L_1}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green L_1}}} & \onslide*{3,4}{\green} \bullet \onslide*{1,2}{\ar[r]^{{\tt I_1}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green I_1}}} & \onslide*{3,4}{\green} \ldots \onslide*{1,2}{\ar[r]^{{\tt I_n}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green I_n}}} & \onslide*{3,4}{\green} \bullet \onslide*{1,2}{\ar[r]^{{\tt CALL}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green CALL}}} & \bullet \ar[r]^{{\tt J_1}} & \ldots \ar[r]^{{\tt RET}} & \onslide*{3,4}{\green} \bullet \onslide*{1,2}{\ar[r]^{{\tt I_{n+1}}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green I_{n+1}}}} & \onslide*{3,4}{\green} \ldots \onslide*{1,2}{\ar[r]^{{\tt I_m}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green I_m}}} & \onslide*{3,4}{\green} \bullet }
393}
394\onslide*{5}{
395\xymatrix{ & & & \bullet \ar[r]^{{\tt J_1}} & \black \ldots \ar[r] & \bullet \ar[d]^{{\tt RET}}\\
396\green \bullet \ar@[green][r]^{{\tt \green L_1}} & \green \bullet \ar@[green][r]^{{\tt \green I_1}} & \green \ldots \ar@[green][r]^{{\tt \green I_n}} & \green \bullet \ar@[green][u]^{{\tt \green CALL}}  & \triangleright & \green \bullet \ar@[green][r]^{{\tt \green I_{n+1}}} & \green \ldots \ar@[green][r]^{{\tt \green I_m}} & \green \bullet }
397}
398}\\
399\onslide*{3,4,5}{\green}$\vdots$ & \\
400\onslide*{3,4,5}{\green}$\tt I_n$ &  \\
401\onslide*{3,4,5}{\green}$\tt CALL$ & \\
402\onslide*{3,4,5}{\green}$\tt I_{n+1}$ & \\
403\onslide*{3,4,5}{\green}$\vdots$ & \\
404\onslide*{3,4,5}{\green}$\tt I_m$
405\end{tabular}
406}
407$\;$\\[3mm]
408\onslide*{4}{{\red What is the global invariant granting both that call/return are balanced and that we can statically predict the return address?}}
409
410% \onslide*{2}{
411% \xymatrix{a & b \\
412%           c & d}
413% }
414\end{wideslide}
415
416% \begin{wideslide}[method=direct]{Measurable traces}
417% $\;$\\[-7mm]
418% \begin{lstlisting}[language=Grafite]
419% inductive pre_measurable_trace (S : abstract_status) :
420% ∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝
421% | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base… st)
422% | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel.
423%    ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
424%    as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl →
425%    pre_measurable_trace … (t_ind … prf … tl)
426% ……… 
427% | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2.
428%    ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3.
429%    ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4.
430%    as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io
431%    →  is_call_act l1 → ¬ is_call_post_label … st1 →
432%    pre_measurable_trace … t1 → pre_measurable_trace … t2 →
433%    as_syntactical_succ S st1 st4 →
434%    is_unlabelled_ret_act l2 →
435%    pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
436% \end{lstlisting}
437% \end{wideslide}
438
439\begin{wideslide}[method=file]{Simulation statement}
440$\;$\\[-7mm]
441\begin{lstlisting}[language=Grafite]
442theorem simulates_pre_mesurable:
443∀S : abstract_status.∀rel : relations S.∀s1,s1' : S. ∀t1: raw_trace S s1 s1'.
444simulation_conditions S rel → pre_measurable_trace … t1 → ∀s2 : S.as_classify … s2 ≠ cl_io → Srel … rel s1 s2 → ∃s2'. ∃t2: raw_trace … s2 s2'.pre_measurable_trace … t2 ∧ get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧ Srel … rel s1' s2'.
445\end{lstlisting}
446\begin{itemize}
447\item<2-> Simulation conditions are local conditions for {\red sequential}, {\red conditional}, {\red call} and {\red return} steps.
448\begin{center}
449\onslide*{2}{
450\xymatrix{st1 \ar[rr] \ar@{.}[d]|-{sim} & & st1' \ar@{.}[d]|-{sim} \\
451          st2 \ar[rr]^{*} & & st2'}}
452\onslide*{3-}{
453\includegraphics[width=5cm]{diag.eps}
454}
455\end{center}
456\item<4-> The generated trace should contain {\red the same sequence of costlabels} (up to permutation) of the starting one.
457\end{itemize}
458\end{wideslide}
459
460\begin{wideslide}{Return instructions are labelled}
461$\;$\\[-7mm]
462{\red Problems}
463\begin{itemize}
464\item Local simulation condition are quite techical and the beauty of simulation argument
465is lost in details.
466\item It does not solve the problem with stateful hardware, since the cost function is
467still requirred to be commutative.
468\end{itemize}
469\onslide{2-}{
470\psshadowbox{
471\begin{minipage}{12cm}
472We ask every function call to be immediately followed by a label emission statement so the scope of a label no longer extends after a function call.
473\end{minipage}
474}}
475$\;$\\
476\onslide{3-}{
477{\red Drawbacks}
478\begin{itemize}
479\item<3-> A lot of labels should be injected in the code!
480\item<3-> The value of the variable $\tt cost$ at the end of a block containing function-calls is the sum of the increments that occurs after every call.
481\item<3-> A proof of termination is requirred!
482\end{itemize}}
483\end{wideslide}
484
485\begin{wideslide}{Return post label pass}
486At the level of source code, we define a {\blue sound and precise} translation to a program having all return instructions that are followed by a label emission. \\[4mm]
487\begin{tabular}{l c l}
488\onslide*{1,2,3}{$\tt EMIT \; L;$}\onslide*{4}{$\tt cost += k_1 + k_2;$} & \multirow{7}{6cm}{\centering $\Rightarrow$} & \onslide*{2}{$\red \tt EMIT \; L1$}\onslide*{3-}{$\tt cost+=k_1;$} \\
489$\tt I_1;$ &                                   & \onslide{2-}{$\tt I_1;$} \\
490$\vdots$ &                                     & \onslide{2-}{$\vdots$} \\
491$\tt f();$ &                                   & \onslide{2-}{$\tt f();$} \\
492$\tt I_2;$ &                                   & \onslide*{2}{{\red $\tt EMIT \; L2;$}}\onslide*{3-}{$\tt cost+=k_2$;} \\
493$\vdots$ &                                     & \onslide{2-}{$\tt I_2;$} \\
494$\tt I_n;$ &                                   & \onslide{2-}{$\vdots$} \\ 
495           &                                   & \onslide{2-}{$\tt I_n$} 
496\end{tabular}
497\end{wideslide}
498
499
500\begin{wideslide}{Return post label pass}
501\begin{itemize}
502\item<1-> {\blue Benefits}: the user can reason with smaller blocks and simpler costs and the compiler do not need to care about extra invariant.
503\item<1-> {\red Drawbacks}: This pass is not always possible in case of non commutative costs.
504\end{itemize}
505To prove correctness it is necessary to define a state relation (being preserved during the translation) keeping track of the fresh labels created.\\[3mm]
506\onslide*{2-}{
507\begin{center}
508\psshadowbox{
509\begin{minipage}{6cm}
510{\red \centering About 3000 lines of Matita code!}
511\end{minipage}
512}
513\end{center}
514}
515\end{wideslide}
516
517\begin{wideslide}{Static analysis correctness}
518\onslide*{1}{
519\psshadowbox{
520\begin{minipage}{12cm}
521Static analysis of cost is {\red correct} when the actual cost of executing a block of instructions of the object code starting from a label (dynamic cost) is equal to the sum of the costs of each reached label of the trace computed by the static analyzer (static cost).
522\end{minipage}
523}}
524\onslide*{2-}{
525\begin{tabular}{l l}
526$\tt \onslide*{3-}{\red} EMIT \; L1$ & \multirow{7}{*}{\xymatrix{\onslide*{1,2,3}{\bullet} \onslide*{4-}{s_1} \onslide*{2-}{\ar[r]^{{\tt L_1}}} \onslide*{3-}{\ar@[red][r]^{{\tt \red L_1}}} & \onslide*{1,2,3}{\bullet} \onslide*{4-}{s_2} \onslide*{2}{\ar[r]} \onslide*{3-}{\ar@[red][r]^{{\tt \red I_1}}} & \onslide*{4-}{s_3} \onslide*{1,2,3}{\bullet} \onslide*{2}{\ar[r]} \onslide*{3-}{\ar@[red][r]^{{\tt \red I_2}}} & \onslide*{1,2,3}{\bullet} \onslide*{4-}{s_4} \onslide*{2}{\ar[r]} \onslide*{3-}{\ar@[red][r]^{{\tt \red COND}}} & \onslide*{1,2,3}{\bullet} \onslide*{4-}{s_5} \onslide*{2}{\ar[r]^{{\tt L_2}}} \onslide*{3-}{\ar@[blue][r]^{{\tt \blue L_2}}} & \onslide*{1,2,3}{\bullet} \onslide*{4-}{s_6} \onslide*{2}{\ar[r]} \onslide*{3-}{\ar@[blue][r]^{{\tt \blue I_3}}} & \onslide*{1,2,3}{\bullet} \onslide*{4-}{s_7} \onslide*{2}{\ar[r]} \onslide*{3-}{\ar@[blue][r]^{{\tt \blue I_4}}} & \onslide*{1,2,3}{\bullet} \onslide*{4-}{s_8}}}  \\ 
527$\tt \onslide*{3-}{\red} I_1$ & \\
528$\tt \onslide*{3-}{\red} I_2$ & \\
529$\tt \onslide*{3-}{\red} COND \; l1$ & \\
530$\tt \onslide*{3-}{\blue} EMIT \; L2$ & \\
531$\tt \onslide*{3-}{\blue} I_3$ & \\
532$\tt \onslide*{3-}{\blue} I_4$ & 
533\end{tabular}
534}
535$\;$\\[3mm]
536\onslide*{3}{
537$$\begin{array}{l l l}
538cost_{trace} &=& {\red k(I_1) + k(I_2) + k(COND)}+ {\blue k(I_3) + k(I_4)} \\
539       &=& {\red(k(I_1) + k(I_2) + k(COND))} + {\blue (k(I_3) + k(I_4))} \\
540       &=& {\red cost(L_1)} + {\blue cost(L_2)}
541\end{array} $$
542}
543\onslide*{4}{
544Lifting to cost dependent from the state
545\begin{itemize}
546\item The cost is a function from states to states which can be composed (the cost is incorporated in the state).
547\item To compute complexity, one is interested only on a part of the state
548\end{itemize}
549\begin{center}
550{\red Galois connection} between an abstract transition system and a concrete one.
551\end{center}
552}
553\onslide*{5}{
554Under the hypothesis that $s_1$ is in connection with the abstract state $a_1$ and $\den{-}$ is the function computing the cost of the instruction in the abstract state (i.e. an {\red action on the cost monoid}), we have
555$$
556\begin{array}{l l l}
557cost_{trace} &=& cost\_of({\blue \den{{\tt I_4}} (\den{{\tt I_3}}} ({\red \den{{\tt COND}}  (\den{{\tt I_2}} (\den{{\tt I_1}}} a_1))))) \\
558           &=& cost\_of(({\blue (\den{{\tt I_4}} \circ \den{{\tt I_3}})} \circ {\red (\den{{\tt COND}} \circ \den{{\tt I_2}} \circ \den{{\tt I_1}})}) a_1) \\
559           &=& cost\_of(({\blue cost(L_2)} \circ {\red cost(L_1)}) a_1)
560\end{array}
561$$
562}
563\end{wideslide}
564
565
566\begin{wideslide}{Conclusion}
567Improvement of the labelling approach.
568\begin{itemize}
569\item Function calls.
570\item Instructions with multiple predecessors (e.g. switch, goto $\ldots$).
571\item Costs for stateful hardware (e.g. cache, pipelines $\ldots$).
572\item From lifting of costs ($\mathbb{N}$)
573 to lifting of abstract interpretation ($\mathcal{A} \to \mathcal{A}$).
574\end{itemize}
575Future works
576\begin{itemize}
577\item Abandoning SOS semantics.
578\item We would like to extend our framework to compilation process that does not preserve basic block structure as in [Tranquilli13].
579\end{itemize}
580\end{wideslide}
581\end{document}
Note: See TracBrowser for help on using the repository browser.