source: LTS/DICE2014/slides.tex @ 3478

%%% \listfiles %%%%%%%%%%%%%%%%%% POWERDOT %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[
%% mode=present,
%% mode=print,
% mode=handout,
% nopagebreaks,
%paper=a4paper,
paper=screen,
%% display=slidesnotes,
%% size=11pt,
%% size=12pt,
%% size=14pt,
%% size=17pt,
%% size=20pt,
  style=simple,
%% style=fyma,
%% orient=portrait,
%% blackslide,
%% fleqn,
%  clock,
]{powerdot}
%\documentclass[mode=handout,nopagebreaks,paper=a4paper]{powerdot}
\usepackage{multirow}
%\usepackage[latin1]{inputenc}
\usepackage{pstricks,pst-node,pst-text,pst-tree}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Work around some bugs in marvosym with overwriting symbols:
\let\labOrigRightarrow=\Rightarrow
        \RequirePackage{marvosym}
\let\Rightarrow=\labOrigRightarrow
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\usepackage{mathabx}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amsbsy}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage[mathscr]{euscript}
%\usepackage{framed}
%\usepackage[framed]{ntheorem}
\usepackage[all,color,dvips]{xy}
%\UseCrayolaColors
%\usepackage{amsfonts}
%\usepackage{graphicx}
%\usepackage{color}
\usepackage{colortbl}
\usepackage{stmaryrd}
%\usepackage{mathabx}
%\usepackage[bbgreekl]{mathbbol}
%\usepackage{epic,eepic}
%\usepackage{xcolor}
%\usepackage{pifont}
\usepackage{proof}
\usepackage{cmll}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Personal VERBATIM and CODE
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\usepackage{fancybox}
%\usepackage{fancyvrb}
%\usepackage{verbatim}
%\usepackage{listings}
%\lstnewenvironment{code}{%
%\lstset{frame=single,escapeinside=`',
%   backgroundcolor=\color{yellow!20},
%   language=lisp,
%   basicstyle=\footnotesize\ttfamily}}{}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Personal Definition of new colors
\usepackage{crayola}
%%%%% COLORI TRASPARENTI %%%%%%%%%%%%%%%
%\usepackage{pstricks-add}
% \defineTColor{TRed}{red}
% \defineTColor{TGreen}{green}
% \defineTColor{TBlue}{blue}
% \defineTColor{TBlue}{blue}
% \defineTColor{TLemon}{LemonChiffon}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{listings}
\def\lstlanguagefiles{lst-grafite.tex}


\def\tuple#1{\langle #1 \rangle}
\input{unimacro.tex}
%\newcommand\emslide[3]{\onslide*{#1}{#2}\onslide*{#3}{\psframebox[fillstyle=solid,fillcolor=Yellow,linecolor=Yellow]{#2}}}

\title{\blue The Labelling Approach to Precise Resource Analysis on the Source Code, Revisited\\[3mm]}
\author{
\hspace*{9mm}  \begin{tabular}{l}
  {\red Mauro Piccolo} \\[1mm]
  %\href{http://www.di.unito.it/~paolini}{\red Luca Paolini} \\[1mm]
  %{\tt paolini@di.unito.it}\\[1mm]
  {Universit\`a di Torino}\\
  {Dipartimento di Informatica}\\[3mm]
  {\red A joint work with Claudio Sacerdoti Coen and Paolo Tranquilli}\\[3mm]
\end{tabular}
}
\date{\hspace*{9mm} DICE 2014 Grenoble, 6 April 2014}

\begin{document}
\maketitle
\begin{wideslide}{Concrete and certified complexity}
$\;$\\[-7mm]
\includegraphics[width=\textwidth]{code.eps}
\\[-5mm]
\begin{itemize}
\item Reasoning about the complexity is rather made on the source.\\[-2mm]
\item Concrete execution costs are better guess on the binary code.
\end{itemize}
\begin{center}
\\[-10mm]
How 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?
\end{center}
\end{wideslide}

\begin{wideslide}[method=direct,toc=Labelling approach]{Labelling approach (Ayache, Amadio and R\'egis-Gianas)}
The user writes the program
\begin{lstlisting}
I1;
for(int i=0;i<2;i++){ 
  I2; 
}
\end{lstlisting}
\end{wideslide}

\begin{wideslide}[method=direct,toc=Labelling approach]{Labelling approach}
The program will be processed by a special pre-compiler which inserts some label emission statements
\begin{lstlisting}
EMIT L1;
I1;
for(int i=0;i<2;i++){ 
  EMIT L2;
  I2; 
}
EMIT L3;
\end{lstlisting}
\end{wideslide}

\begin{wideslide}[method=file,toc=Labelling approach]{Labelling approach}
\onslide*{1}{The program is then compiled into an object code emitting the same sequence of labels}
\onslide*{2}{The object code is processed by a static code analyzer to determine the cost of each block of code}
\begin{center}
\begin{tabular}{l l l}
\begin{lstlisting}
EMIT L1;
I1;
for(int i=0;i<2;i++){ 
  EMIT L2;
  I2; 
}
EMIT L3;
\end{lstlisting}
&$\qquad$&
\begin{lstlisting}
    EMIT L1;
    I3
l1: COND l1 
    EMIT L2
    I4
    GOTO l1
l2: EMIT L3
\end{lstlisting}
\end{tabular}
\end{center}
\onslide*{2}{
\begin{center}
\begin{tabular}{|l|l|}
\hline
Label & Cost \\
\hline
L1 & $cost(I3) + cost(COND \ l1) = k_1$ \\
L2 & $cost(I4) + cost(GOTO \ l1) = k_2$ \\
L3 & $k_3$\\
\hline
\end{tabular}
\end{center}
}
\end{wideslide}
\begin{wideslide}[method=direct]{Labelling approach}
The complier gives an instrumented version of the source code
\begin{center}
\begin{tabular}{l l l}
\begin{lstlisting}
cost += k_1
instr 1;
for(int i=0;i<2;i++){ 
  cost += k_2
  instr 2; 
}
cost += k_3
\end{lstlisting}
&$\qquad$&
\begin{lstlisting}
    EMIT L1;
    instr 3
l1: COND l1 
    EMIT L2
    instr 4
    GOTO l1
l2: EMIT L3
\end{lstlisting}
\end{tabular}
\end{center}
$\;$ \\
\psshadowbox{
\begin{minipage}{10.5cm}
\centering We can make assertions on the variable cost which contains the {\red precise} cost of the computation.
\end{minipage}
}
$\;$\\[3mm]
Precise 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!).
\end{wideslide}

\begin{wideslide}{Certified complexity}
$\;$\\[-9mm]
\begin{center}
\includegraphics[width=6cm]{cerco.eps}
\end{center}
This talk:
\psshadowbox{
\begin{minipage}{12cm}
\begin{itemize}
\item We revise the labelling approach to lift some restriction: {\red instructions having only one predecessor} and {\red absence of function calls}.
\item We replace simple status independent costs with arbitrary semantics domains used in {\red abstract interpretation} to analyze caches, pipelines,$\ldots$.
\item All the presented results are formalized in the {\red Matita proof assistant}.
\end{itemize}
\end{minipage}
}
\end{wideslide}



\begin{wideslide}[method=direct]{Conditional statements and multiple predecessors}
$\;$\\[-4mm]
{\red Assumptions:}
\psshadowbox{
\begin{minipage}{12cm}
\begin{itemize}
\item Each object code instruction should fall into the scope of a label.
\item Each object code instruction having multiple successors (e.g. conditionals) should pass control to basic blocks starting with a label emission statement.
\item The cost of the conditional instruction should be the same whatever branch is taken.
\end{itemize}
\end{minipage}
} \\[4mm]
{\red Problem!} \\
\begin{tabular}[t]{l l l l l}
\begin{lstlisting}
if(E){
  EMIT L;
  I;
}
\end{lstlisting}
& $\qquad\qquad$ &
\begin{lstlisting}
    SJNEQ l1
    JUMP l3
l1: JUMP l2
... 
l2: EMIT L
    I;
\end{lstlisting}
& $\qquad\qquad$ &
\begin{lstlisting}
    SJNEQ l1
    JUMP l3
l1: EMIT L
    JUMP l2
... 
l2: I;
\end{lstlisting}
\end{tabular}
\end{wideslide}

\begin{wideslide}[method=direct]{Solution: labelled transition system semantics}
\begin{itemize}
\item We incorporate label emission in the semantics of the instructions.
\item No more label emission statements.
\end{itemize}
\begin{center}
\begin{tabular}{ll l}
\begin{lstlisting}
swith(E){
  case e1 :
  Emit L1;
  I1;
  case e2 :
  Emit L2;
  I2;
}
\end{lstlisting} &$\qquad$&
\begin{lstlisting}
swith(E){
  case e1,L1 :

  I1;
  case L3,e2,L2 : //L3 emitted coming 
                  // from case e1
  I2;
}
\end{lstlisting}
\end{tabular}
\end{center}
% \begin{lstlisting}[language=Grafite]
% record abstract_status : Type[2] ≝ 
%  { as_status :> Type[0]
%  ; as_execute : ActionLabel → relation as_status
%  ; as_syntactical_succ : relation as_status
%  ; as_classify : as_status → status_class
%  ; as_initial : as_status → bool
%  ; as_final : as_status → bool
%  ; jump_emits : ∀s1,s2,l.as_classify ... s1 = cl_jump → 
%       as_execute l s1 s2 → is_non_silent_cost_act l
%  }.
% \end{lstlisting}
\end{wideslide}

\begin{wideslide}[method=file]{Function calls}
\begin{center}
\begin{tabular}{l l l}
\begin{lstlisting}
void main(){
  EMIT L1;
  I1;
  (*f)();
  I2;
}

void g(){
  EMIT L2;
  I3;
}
\end{lstlisting}
& $\qquad\qquad$ &
\begin{lstlisting}
main :
  EMIT L1
  I4
  CALL
  I5
  RETURN

g :
  EMIT L2
  I6;
  RETURN
\end{lstlisting}
\end{tabular}
\end{center}
What label should pay the cost for the block I5? \\
\onslide{2}{
{\red The only reasonable answer is L1!}
}
\end{wideslide}

\begin{wideslide}{Label emission and function calls}
$\;$ \\[-5mm]
\psshadowbox{
\begin{minipage}{12cm}
The scope of labels should extend to the next label emission statement or the end of the function, stepping over function calls.
\end{minipage}
}\\[3mm]
\onslide{2-}{
{\red Assumptions:}
\begin{itemize}
\item<2-> All the instruction in the (static) block are reached during computation.
\item<2-> The cost function should be commutative.
\end{itemize}
}
\onslide{3-}{
{\red Problems:}
\begin{itemize}
\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}.
\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}.
\end{itemize}}
\end{wideslide}

\begin{wideslide}{First solution: structured traces}
\onslide*{1}{
\begin{itemize}
\item The usual notion of {\red flat execution trace} is inadequate for a simulation argument.
\item {\red Embed the call/return} into execution trace.
\item Traces of called function are {\red nested}, invariants on position of costlabels are {\red enforced} and steps are grouped {\red according to costlabels}.
\end{itemize}
}
\onslide*{2-}{
\begin{tabular}{l c}
\onslide*{3,4,5}{\green}$\tt EMIT \; L_1$ &  \onslide*{2,3,4}{{\red Flat trace}} \onslide*{5}{{\red Structured trace}}\\
\onslide*{3,4,5}{\green}$\tt I_1$ & \multirow{7}{*}{
\onslide*{2,3,4}{
\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 }
}
\onslide*{5}{
\xymatrix{ & & & \bullet \ar[r]^{{\tt J_1}} & \black \ldots \ar[r] & \bullet \ar[d]^{{\tt RET}}\\
\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 }
}
}\\
\onslide*{3,4,5}{\green}$\vdots$ & \\
\onslide*{3,4,5}{\green}$\tt I_n$ &  \\
\onslide*{3,4,5}{\green}$\tt CALL$ & \\
\onslide*{3,4,5}{\green}$\tt I_{n+1}$ & \\
\onslide*{3,4,5}{\green}$\vdots$ & \\
\onslide*{3,4,5}{\green}$\tt I_m$
\end{tabular}
}
$\;$\\[3mm]
\onslide*{4}{{\red What is the global invariant granting both that call/return are balanced and that we can statically predict the return address?}}

% \onslide*{2}{
% \xymatrix{a & b \\
%           c & d}
% }
\end{wideslide}

% \begin{wideslide}[method=direct]{Measurable traces}
% $\;$\\[-7mm]
% \begin{lstlisting}[language=Grafite]
% inductive pre_measurable_trace (S : abstract_status) :
% ∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝ 
% | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base… st)
% | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel.
%    ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
%    as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl → 
%    pre_measurable_trace … (t_ind … prf … tl)
% ………  
% | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2.
%    ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3.
%    ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4.
%    as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io 
%    →  is_call_act l1 → ¬ is_call_post_label … st1 → 
%    pre_measurable_trace … t1 → pre_measurable_trace … t2 → 
%    as_syntactical_succ S st1 st4 → 
%    is_unlabelled_ret_act l2 → 
%    pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
% \end{lstlisting} 
% \end{wideslide}

\begin{wideslide}[method=file]{Simulation statement}
$\;$\\[-7mm]
\begin{lstlisting}[language=Grafite]
theorem simulates_pre_mesurable:
∀S : abstract_status.∀rel : relations S.∀s1,s1' : S. ∀t1: raw_trace S s1 s1'.
simulation_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'.
\end{lstlisting}
\begin{itemize}
\item<2-> Simulation conditions are local conditions for {\red sequential}, {\red conditional}, {\red call} and {\red return} steps.
\begin{center}
\onslide*{2}{
\xymatrix{st1 \ar[rr] \ar@{.}[d]|-{sim} & & st1' \ar@{.}[d]|-{sim} \\
          st2 \ar[rr]^{*} & & st2'}}
\onslide*{3-}{
\includegraphics[width=5cm]{diag.eps}
}
\end{center}
\item<4-> The generated trace should contain {\red the same sequence of costlabels} (up to permutation) of the starting one.
\end{itemize}
\end{wideslide}

\begin{wideslide}{Return instructions are labelled}
$\;$\\[-7mm]
{\red Problems}
\begin{itemize}
\item Local simulation condition are quite techical and the beauty of simulation argument 
is lost in details.
\item It does not solve the problem with stateful hardware, since the cost function is 
still requirred to be commutative.
\end{itemize}
\onslide{2-}{
\psshadowbox{
\begin{minipage}{12cm}
We 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.
\end{minipage}
}}
$\;$\\
\onslide{3-}{
{\red Drawbacks}
\begin{itemize}
\item<3-> A lot of labels should be injected in the code!
\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.
\item<3-> A proof of termination is requirred!
\end{itemize}}
\end{wideslide}

\begin{wideslide}{Return post label pass}
At 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]
\begin{tabular}{l c l}
\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;$} \\
$\tt I_1;$ &                                   & \onslide{2-}{$\tt I_1;$} \\
$\vdots$ &                                     & \onslide{2-}{$\vdots$} \\
$\tt f();$ &                                   & \onslide{2-}{$\tt f();$} \\
$\tt I_2;$ &                                   & \onslide*{2}{{\red $\tt EMIT \; L2;$}}\onslide*{3-}{$\tt cost+=k_2$;} \\
$\vdots$ &                                     & \onslide{2-}{$\tt I_2;$} \\
$\tt I_n;$ &                                   & \onslide{2-}{$\vdots$} \\ 
           &                                   & \onslide{2-}{$\tt I_n$} 
\end{tabular}
\end{wideslide}


\begin{wideslide}{Return post label pass}
\begin{itemize}
\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.
\item<1-> {\red Drawbacks}: This pass is not always possible in case of non commutative costs.
\end{itemize}
To prove correctness it is necessary to define a state relation (being preserved during the translation) keeping track of the fresh labels created.\\[3mm]
\onslide*{2-}{
\begin{center}
\psshadowbox{
\begin{minipage}{6cm}
{\red \centering About 3000 lines of Matita code!}
\end{minipage}
}
\end{center}
}
\end{wideslide}

\begin{wideslide}{Static analysis correctness}
\onslide*{1}{
\psshadowbox{
\begin{minipage}{12cm}
Static 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).
\end{minipage}
}}
\onslide*{2-}{
\begin{tabular}{l l}
$\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}}}  \\ 
$\tt \onslide*{3-}{\red} I_1$ & \\
$\tt \onslide*{3-}{\red} I_2$ & \\
$\tt \onslide*{3-}{\red} COND \; l1$ & \\
$\tt \onslide*{3-}{\blue} EMIT \; L2$ & \\
$\tt \onslide*{3-}{\blue} I_3$ & \\
$\tt \onslide*{3-}{\blue} I_4$ & 
\end{tabular}
}
$\;$\\[3mm]
\onslide*{3}{
$$\begin{array}{l l l}
cost_{trace} &=& {\red k(I_1) + k(I_2) + k(COND)}+ {\blue k(I_3) + k(I_4)} \\
       &=& {\red(k(I_1) + k(I_2) + k(COND))} + {\blue (k(I_3) + k(I_4))} \\
       &=& {\red cost(L_1)} + {\blue cost(L_2)}
\end{array} $$
}
\onslide*{4}{
Lifting to cost dependent from the state
\begin{itemize}
\item The cost is a function from states to states which can be composed (the cost is incorporated in the state).
\item To compute complexity, one is interested only on a part of the state
\end{itemize}
\begin{center}
{\red Galois connection} between an abstract transition system and a concrete one.
\end{center}
}
\onslide*{5}{
Under 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
$$
\begin{array}{l l l}
cost_{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))))) \\
           &=& 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) \\
           &=& cost\_of(({\blue cost(L_2)} \circ {\red cost(L_1)}) a_1)
\end{array}
$$
}
\end{wideslide}


\begin{wideslide}{Conclusion}
Improvement of the labelling approach.
\begin{itemize}
\item Function calls.
\item Instructions with multiple predecessors (e.g. switch, goto $\ldots$).
\item Costs for stateful hardware (e.g. cache, pipelines $\ldots$).
\item From lifting of costs ($\mathbb{N}$)
 to lifting of abstract interpretation ($\mathcal{A} \to \mathcal{A}$).
\end{itemize}
Future works
\begin{itemize}
\item Abandoning SOS semantics.
\item We would like to extend our framework to compilation process that does not preserve basic block structure as in [Tranquilli13].
\end{itemize}
\end{wideslide}
\end{document}