root/Deliverables/D1.1/Presentations/WP2-roberto.tex @ 626

\documentclass{beamer}

\usetheme{Frankfurt}
%\logo{\includegraphics[height=1.0cm]{fetopen.png}}
% smaller 
\logo{\includegraphics[height=0.6cm]{fetopen.png}}


\usepackage[english]{babel}
\usepackage{inputenc}



                           
%\documentclass[landscape]{seminar}

% \usepackage[latin1]{inputenc}
% \usepackage[frenchb]{babel}


%TO HAVE AN ARTICLE STYLE
%\documentclass[11pt]{article}
%\usepackage{latexsym}
%\usepackage{amsfonts}
%\usepackage{a4wide} 



% TO HAVE COLOURS IN SLIDES, USAGE \Blu{}, \Red{}, \Green{}, \Purple{}
\usepackage{epsfig}
\usepackage{color}
\usepackage{fancybox}
\usepackage{color}
\usepackage{alltt}
\definecolor{c1114}{rgb}{1,0.2156862745098,0.75294117647059}
\definecolor{c1112}{rgb}{1,0,0}
\definecolor{c1121}{rgb}{0,0,0.54509803921569}
\definecolor{c1123}{rgb}{0,0.5,0}
\def\Green#1{\textcolor{c1123}{#1}}
\def\Blu#1{\textcolor{c1121}{#1}}
\def\Red#1{\textcolor{c1112}{#1}}
\def\Purple#1{\textcolor{c1114}{#1}}
\definecolor{c1082}{rgb}{0.,0.,0.}
\definecolor{c1083}{rgb}{1,0,0}

% TO NEUTRALIZE COLOURS
%\newcommand{\Red}[1]{#1} 
%\newcommand{\Blu}[1]{#1} 
%\newcommand{\Green}[1]{#1} 
%\newcommand{\Purple}[1]{#1} 

%TO NEUTRALIZE SLIDE
% replace {slide} by {slid} and insert
%\newenvironment{slid}{}{}

% ALSO REMOVE \newpage


\newcommand{\eqdef}{=_{\text{def}}} 
\newcommand{\concat}{\cdot}%%{\mathbin{+}} 

\newcommand{\Models}{\mid \! =}              % models 
\newcommand{\Int}{\mathit{int}} 
\newcommand{\nat}{\mathit{nat}} 
\newcommand{\String}{\mathit{string}} 
\newcommand{\Ident}{\mathit{ident}} 
\newcommand{\Block}{\mathit{block}} 
\newcommand{\Signature}{\mathit{signature}} 
 
\newcommand{\pc}{\mathit{pc}} 
\newcommand{\estack}{\mathit{estack}} 
\newcommand{\Error}{\epsilon} 
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 
% --------------------------------------------------------------------- % 
% Proof rule.                                                           % 
% --------------------------------------------------------------------- % 
 
\newcommand{\staterule}[3]{% 
  $\begin{array}{@{}l}% 
   \mbox{#1}\\% 
   \begin{array}{c} 
   #2\\  
   \hline 
   \raisebox{0ex}[2.5ex]{\strut}#3% 
   \end{array} 
  \end{array}$} 
 
\newcommand{\GAP}{2ex} 
 
\newcommand{\recall}[2]{% 
 $\begin{array}{c} 
 #1\\  
 \hline 
 \raisebox{0ex}[2.5ex]{\strut}#2% 
 \end{array}$} 
 
\newcommand{\hbra}{\noindent\hbox to \textwidth{\leaders\hrule height1.8mm depth-1.5mm\hfill}} 
\newcommand{\hket}{\noindent\hbox to \textwidth{\leaders\hrule height0.3mm\hfill}} 
\newcommand{\ratio}{.3} 
 
\newenvironment{display}[1]{\begin{tabbing} 
  \hspace{1.5em} \= \hspace{\ratio\linewidth-1.5em} \= \hspace{1.5em} \= \kill 
  \noindent\hbra\\[-.5em] 
  {\ }\textsc{#1}\\[-.8ex] 
  \hbox to \textwidth{\leaders\hrule height1.6mm depth-1.5mm\hfill}\\[-.8ex] 
  }{\\[-.8ex]\hket 
  \end{tabbing}} 
 
 
\newcommand{\sbline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.2ex}\hfill\hspace*{0ex}}} 
\newcommand{\sline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.1ex}\hfill\hspace*{0ex}}} 
\newcommand{\sentry}[2]{\>$#1$\>\ \smash[t]{\vrule width 0.2mm height 
    1.2\baselineskip depth 1.5\baselineskip}\>#2} 
 
\newcommand{\entry}[2]{\>$#1$\>\>#2} 
\newcommand{\clause}[2]{$#1$\>\>#2} 
\newcommand{\category}[2]{\clause{#1::=}{#2}} 
\newcommand{\subclause}[1]{\>\>\>#1} 
\newcommand{\redrule}[3]{$#1$\>\>$#2$\>\>\>#3} 
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 
% environments 
 
%% \newtheorem{theorem}{Theorem} 
%% \newtheorem{fact}[theorem]{Fact} 
%% \newtheorem{definition}[theorem]{Definition} 
%% \newtheorem{lemma}[theorem]{Lemma} 
%% \newtheorem{corollary}[theorem]{Corollary} 
%% \newtheorem{proposition}[theorem]{Proposition} 
%% \newtheorem{example}[theorem]{Example} 
%% \newtheorem{exercise}[theorem]{Exercise} 
%% \newtheorem{remark}[theorem]{Remark} 
%% \newtheorem{proviso}[theorem]{Proviso} 
%%  \newtheorem{conjecture}[theorem]{Conjecture}

% proofs  
 
%\newcommand{\Proof}{\noindent {\sc Proof}. } 
\newcommand{\Proofhint}{\noindent {\sc Proof hint}. } 
%\newcommand{\qed}{\hfill${\Box}$} 
\newcommand{\EndProof}{\qed}
 
% figure environment 
 
\newcommand{\Figbar}{{\center \rule{\hsize}{0.3mm}}}    %horizontal thiner line for figures 
\newenvironment{figureplr}{\begin{figure}[t] \Figbar}{\Figbar \end{figure}} 
                                                        %environment for figures 
%       ************Macros for mathematical symbols************* 
% Style 
 
\newcommand{\cl}[1]{{\cal #1}}          % \cl{R} to make R calligraphic 
\newcommand{\la}{\langle}               % the brackets for pairing (see also \pair) 
\newcommand{\ra}{\rangle} 
 
\newcommand{\lf}{\lfloor} 
\newcommand{\rf}{\rfloor} 
\newcommand{\ul}[1]{\underline{#1}}     % to underline 
\newcommand{\ol}[1]{\overline{#1}}      % to overline 
\newcommand{\ok}{~ok}                   % well formed context 
 
% Syntax 
 
\newcommand{\Gives}{\vdash}             % in a type judgment 
\newcommand{\emptycxt}{\O}              % empty context 
\newcommand{\subs}[2]{[#1 / #2]} 
\newcommand{\sub}[2]{[#2 / #1]}         % substitution \sub{x}{U} gives [U/x]    
\newcommand{\Sub}[3]{[#3 / #2]#1}       % Substitution with three arguments \Sub{V}{x}{U} 

\newcommand{\lsub}[2]{#2 / #1}          % substitution \lsub{x}{U} gives U/x, to be used in a list. 
 
\newcommand{\impl}{\supset} 
%\newcommand{\imp}{{\sc Imp}}            %imp language
%\newcommand{\vm}{{\sc Vm}}              %virtual machine language
\newcommand{\arrow}{\rightarrow}        % right thin arrow 
\newcommand{\trarrow}{\stackrel{*}{\rightarrow}}        % trans closure 
\newcommand{\bt}[1]{{\it BT}(#1)}       % Boehm tree 
\newcommand{\cxt}[1]{#1[~]}             % Context with one hole 
\newcommand{\pr}{\parallel}             % parallel || 
\newcommand{\Nat}{\mathbf{N}}                 % natural numbers 
\newcommand{\Natmax}{\mathbf{N}_{{\it max}}}  % natural numbers with minus infinity 
\newcommand{\Rat}{\mathbf{Q}^{+}}                 % non-negative rationals 
\newcommand{\Ratmax}{\mathbf{Q}^{+}_{{\it max}}}  % non-negative rationals with minus infinity 
\newcommand{\Alt}{ \mid\!\!\mid  } 
\newcommand{\isum}{\oplus} 
\newcommand{\dpar}{\mid\!\mid} 
                                        % for the production of a grammar containing \mid 
\newcommand{\infer}[2]{\begin{array}{c} #1 \\ \hline #2 \end{array}} 
                                        % to make a centered inference rule 
 
% (Meta-)Logic 
 
\newcommand{\bool}{{\sf bool}}          % boolean values 
\newcommand{\Or}{\vee}                  % disjunction 
\newcommand{\OR}{\bigvee}               % big disjunction 
\newcommand{\AND}{\wedge}               % conjunction 
\newcommand{\ANDD}{\bigwedge}           % big conjunction 
\newcommand{\Arrow}{\Rightarrow}        % right double arrow 
\newcommand{\IFF}{\mbox{~~iff~~}}       % iff in roman and with spaces 
\newcommand{\iffArrow}{\Leftrightarrow} % logical equivalence 
 
% Semantics 
 
\newcommand{\dl}{[\![}                  % semantic [[ 
\newcommand{\dr}{]\!]}                  % semantic ]] 
\newcommand{\lam}{{\bf \lambda}}        % semantic lambda 


% The equivalences for this paper

% the usual ones
\newcommand{\ubis}{\approx^u}          % usual labelled weak bis
\newcommand{\uabis}{\approx^{u}_{ccs}} % usual labelled weak bis on CCS

% the contextual conv sensitive
\newcommand{\cbis}{\approx}        % convergence sensitive bis
\newcommand{\cabis}{\approx_{ccs}}  % convergence sensitive bis on CCS

% the labelled conv sensitive
\newcommand{\lcbis}{\approx^{\ell}} %
\newcommand{\lcabis}{\approx^{\ell}_{ccs}} % labelled convergence sensitive bis on CCS
\newcommand{\lcbiswrong}{\approx^{\ell \Downarrow}} %




\newcommand{\maytest}{=_{\Downarrow}}
\newcommand{\musttest}{=_{\Downarrow_{S}}}


 
 
% Sets 
 
\newcommand{\prt}[1]{{\cal P}(#1)}      % Parts of a set 
\newcommand{\finprt}[1]{{\cal P}_{fin}(#1)}% Finite parts 
\newcommand{\finprtp}[1]{{\cal P}_{fin}^{+}(#1)}% Non-empty Finite parts 
\newcommand{\union}{\cup}               % union 
\newcommand{\inter}{\cap}               % intersection 
\newcommand{\Union}{\bigcup}            % big union 
\newcommand{\Inter}{\bigcap}            % big intersection 
\newcommand{\cpl}[1]{#1^{c}}            % complement 
\newcommand{\card}{\sharp}              % cardinality 
\newcommand{\minus}{\backslash}         % set difference 
\newcommand{\sequence}[2]{\{#1\}_{#2}}  % ex. \sequence{d_n}{n\in \omega} 
\newcommand{\comp}{\circ}               % functional composition 
\newcommand{\set}[1]{\{#1\}}            % set enumeration 
\newcommand{\pset}[1]{\{\! | #1 |\!\}}  % pseudo-set notation {| |} 
 
% Domains 
 
\newcommand{\two}{{\bf O}}              % Sierpinski space 
\newcommand{\join}{\vee}                % join 
\newcommand{\JOIN}{\bigvee}             % big join  
\newcommand{\meet}{\wedge}              % meet 
\newcommand{\MEET}{\bigwedge}           % big meet 
\newcommand{\dcl}{\downarrow}           % down closure 
\newcommand{\ucl}{\uparrow}             % up closure 
\newcommand{\conv}{\downarrow}          % synt. conv. pred. (postfix) 
%\newcommand{\diver}{\uparrow}           % diverging term 
\newcommand{\Conv}{\Downarrow}          % sem. conv. pred. (postfix) 
\newcommand{\SConv}{\Downarrow_{S}}          % sem. conv. pred. (postfix) 
\newcommand{\CConv}{\Downarrow_{C}}
\newcommand{\diver}{\Uparrow}           % diverging map 
\newcommand{\cpt}[1]{{\cal K}(#1)}      % compacts, write \cpt{D} 
\newcommand{\ret}{\triangleleft}        % retract 
\newcommand{\nor}{\succeq}
\newcommand{\prj}{\underline{\ret}}     % projection 
\newcommand{\parrow}{\rightharpoonup}   % partial function space 
\newcommand{\ub}[1]{{\it UB}(#1)}       % upper bounds 
\newcommand{\mub}[1]{{\it MUB}(#1)}     % minimal upper bounds 
\newcommand{\lift}[1]{(#1)_{\bot}}      % lifting 
%\newcommand{\rel}[1]{\;{\cal #1}\;}     % infix relation (calligraphic) 
\newcommand{\rl}[1]{\;{\cal #1}\;}             % infix relation 
\newcommand{\rel}[1]{{\cal #1}}         %calligraphic relation with no 
                                        %extra space 
\newcommand{\per}[1]{\;#1 \;} 
\newcommand{\wddagger}{\natural}  % weak suspension 
%\newcommand{\wddagger}{=\!\!\!\!\parallel}  % weak suspension 
% Categories 
 
\newcommand{\pair}[2]{\langle #1 , #2 \rangle} % pairing \pair{x}{y}, do not use < >. 
 
%               *******  Notation for the $\pi$-calculus ********* 
% Syntax: 
 
 
\newcommand{\fn}[1]{{\it fn}(#1)}                       % free names 
\newcommand{\bn}[1]{{\it bn}(#1)}                       % bound names 
\newcommand{\names}[1]{{\it n}(#1)}                     % names 
\newcommand{\true}{{\sf t}}                             % true 
\newcommand{\false}{{\sf f}}                            % false 
\newcommand{\pio}{\pi_1}                                % 1 receptor calculus 
\newcommand{\pioo}{\pi_{1}^{r}} 
\newcommand{\piom}{\pi_{1}^{-}}                         % 1 receptor calculus wo match 
\newcommand{\pioi}{\pi_{1I}}                    % 1 receptor I-calculus 
\newcommand{\pifo}{\pi_{\w{1f}}}                                % functional calculus 
\newcommand{\pilo}{\pi_{\w{1l}}}                                % located calculus 
\newcommand{\sort}[1]{{\it st}(#1)}                     % sort 
\newcommand{\ia}[1]{{\it ia}(#1)}                     % sort 
\newcommand{\ite}[3]{{\sf if~} #1 {\sf ~then~} #2 {\sf ~else~} #3}      %if then else 
\newcommand{\casep}[2]{{\sf case}^{\times}(#1, \pair{x}{y}\Arrow#2)}      %case on pairs 
\newcommand{\casel}[3]{{\sf case}^{L}(#1, #2, \s{cons}(x,y)\Arrow#3)}      %case on lists 
\newcommand{\caseb}[3]{{\sf case}^{b}(#1, #2, \s{cons}(x,y)\Arrow#3)}      %case on lists 
\newcommand{\nil}{{\sf nil}} 
\newcommand{\cons}{{\sf cons}} 
\newcommand{\idle}[1]{{\it Idle}(#1)}                   %idle process 
\newcommand{\conf}[1]{\{ #1 \}}                         %configuration 
\newcommand{\link}[2]{#1 \mapsto #2}                    %likn a ->b 
\newcommand{\mand}{\mbox{ and }} 
\newcommand{\dvec}[1]{\tilde{{\bf #1}}}                 %double vector 
\newcommand{\erloc}[1]{{\it er}_{l}(#1)}                % location erasure 
\newcommand{\w}[1]{{\it #1}}    %To write in math style 
\newcommand{\vcb}[1]{{\bf #1}} 
\newcommand{\lc}{\langle\!|} 
\newcommand{\rc}{|\!\rangle} 
\newcommand{\obj}[1]{{\it obj}(#1)}  
\newcommand{\move}[1]{{\sf move}(#1)}  
\newcommand{\qqs}[2]{\forall\, #1\;\: #2} 
\newcommand{\xst}[2]{\exists\, #1\;\: #2} 
\newcommand{\xstu}[2]{\exists\, ! #1\;\: #2} 
\newcommand{\dpt}{\,:\,} 
\newcommand{\cond}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3} 
\newcommand{\s}[1]{{\sf #1}}    % sans-serif  
\newcommand{\vc}[1]{{\bf #1}} 
\newcommand{\lnorm}{\lbrack\!\lbrack} 
\newcommand{\rnorm}{\rbrack\!\rbrack} 
\newcommand{\sem}[1]{\underline{#1}} 
\newcommand{\squn}{\mathop{\scriptstyle\sqcup}} 
\newcommand{\lcro}{\langle\!|} 
\newcommand{\rcro}{|\!\rangle} 
\newcommand{\semi}[1]{\lcro #1\rcro} 
\newcommand{\sell}{\,\ell\,} 
\newcommand{\SDZ}[1]{\marginpar{\textbf{SDZ:} {#1}}} 
 
\newcommand{\when}[3]{{\sf when}~#1~{\sf then}~#2~{\sf else}~#3}  
\newcommand{\wthen}[2]{{\sf when}~#1~{\sf then}~#2~}  
\newcommand{\welse}[1]{{\sf else}~#1}  

%Pour la fleche double, il faut rajouter :
%      \usepackage{mathtools}

\newcommand{\act}[1]{\stackrel{#1}{\rightarrow}} %labelled actionlow %high

%\newcommand{\wact}[1]{\xRightarrow{#1}} %weak labelled action low high

%\newcommand{\mact}[1]{\xrightarrow{#1}_{m}} %labelled action low %high

%\newcommand{\wmact}[1]{\xRightarrow{#1}_{m}} %weak labelled action low high

%\newcommand{\act}[1]{\stackrel{#1}{\rightarrow}} %labelled action low
                                %%%high 

\newcommand{\acteq}[1]{\stackrel{#1}{\leadsto}} %labelled action low
                                %%%high 


%\newcommand{\actI}[1]{\stackrel{#1}{\rightarrow_{1}}} %labelled action low
\newcommand{\actI}[1]{\xrightarrow{#1}_{1}}

%\newcommand{\actII}[1]{\stackrel{#1}{\rightarrow_{2}}} %labelled action low
\newcommand{\actII}[1]{\xrightarrow{#1}_{2}}


 \newcommand{\wact}[1]{\stackrel{#1}{\Rightarrow}} %weak labelled action low high 
\newcommand{\wactI}[1]{\stackrel{#1}{\Rightarrow_{1}}} %weak labelled action low high
\newcommand{\wactII}[1]{\stackrel{#1}{\Rightarrow_{2}}} %weak labelled action low high


\newcommand{\mact}[1]{\stackrel{#1}{\rightarrow_{m}}} %labelled action low %high 
\newcommand{\wmact}[1]{\stackrel{#1}{\Rightarrow_{m}}} %weak labelled action low high 
 
\newcommand{\lact}[1]{\stackrel{#1}{\leftarrow}} 
\newcommand{\lwact}[1]{\stackrel{#1}{\Leftarrow}} 
 
 
 
\newcommand{\eval}{\Downarrow} 
\newcommand{\Eval}[1]{\Downarrow^{#1}} 
 
 
\newcommand{\Z}{{\bf Z}} 
\newcommand{\Real}{\mathbb{R}^{+}}  
\newcommand{\Return}{\ensuremath{\mathtt{return}}\xspace}                 
\newcommand{\Stop}{\ensuremath{\mathtt{stop}}\xspace} 
\newcommand{\Wait}{\ensuremath{\mathtt{wait}}\xspace} 
\newcommand{\Read}{\ensuremath{\mathtt{read}}\xspace} 
\newcommand{\Write}{\ensuremath{\mathtt{write}}\xspace} 
\newcommand{\Yield}{\ensuremath{\mathtt{yield}}\xspace} 
\newcommand{\Next}{\ensuremath{\mathtt{next}}\xspace} 
\newcommand{\Load}{\ensuremath{\mathtt{load}}\xspace} 
\newcommand{\Call}{\ensuremath{\mathtt{call}}\xspace} 
\newcommand{\Tcall}{\ensuremath{\mathtt{tcall}}\xspace} 
\newcommand{\Pop}{\ensuremath{\mathtt{pop}}\xspace} 
\newcommand{\Build}{\ensuremath{\mathtt{build}}\xspace} 
\newcommand{\Branch}{\ensuremath{\mathtt{branch}}\xspace} 
\newcommand{\Goto}{\ensuremath{\mathtt{goto}}\xspace} 
 
\newcommand{\hatt}[1]{#1^{+}} 
\newcommand{\Of}{\mathbin{\w{of}}} 
 
\newcommand{\susp}{\downarrow} 
\newcommand{\lsusp}{\Downarrow_L} 
\newcommand{\wsusp}{\Downarrow} 
\newcommand{\commits}{\searrow} 
 
 
\newcommand{\spi}{S\pi} 
 

 \newcommand{\pres}[2]{#1\triangleright #2} %TCCS else next (alternative)
% \newcommand{\pres}[2]{ \lfloor #1 \rfloor (#2)}  %TCCS else next
\newcommand{\present}[3]{{\sf present} \ #1 \ {\sf do } \ #2 \ {\sf  else} \ #3}


\newcommand{\tick}{{\sf tick}}          %tick action

 
 
\newcommand{\sbis}{\equiv_L} 
\newcommand{\emit}[2]{\ol{#1}#2}  
%\newcommand{\present}[4]{#1(#2).#3,#4} 
\newcommand{\match}[4]{[#1=#2]#3,#4}       %pi-equality 

\newcommand{\matchv}[4]{[#1 > #2]#3,#4}

\newcommand{\new}[2]{\nu #1 \ #2} 
\newcommand{\outact}[3]{\new{{\bf #1}}{\emit{#2}{#3}}} 
\newcommand{\real}{\makebox[5mm]{\,$\|\!-$}}% realizability relation 
 


\newcommand{\tit}[1]{\begin{center} \Red{{\bf #1 }}\end{center}}
\newcommand{\stit}[1]{\begin{center} #1 \end{center}}
\newcommand{\chpt}[1]{\begin{center} \Red{{\huge #1 }}\end{center}}
\newcommand{\bem}[1]{\Blu{{\em #1}}}
\newcommand{\NB}{{\bf NB}~}
\newcommand{\Refer}[1]{\Green{{\small {\bf Ref} \ #1}}}

\newcommand{\tact}[2]{\ensuremath{\underset{#1}{\act{~#2~}}}}
\newcommand{\tacteq}[2]{\ensuremath{\underset{#1}{\acteq{~#2~}}}}
\newcommand{\twbis}{\approx^{t}}        % typed weak bis

\newcommand{\regterm}[2]{{\sf reg}_{#1} #2}
\newcommand{\thread}[1]{{\sf thread} \ #1}
\newcommand{\store}[2]{(#1 \Leftarrow #2)}
\newcommand{\gt}[1]{{\sf get}(#1)}
\newcommand{\st}[2]{{\sf set}(#1,#2)}
\newcommand{\regtype}[2]{{\sf Reg}_{#1} #2}

\newcommand{\Beh}{{\bf B}}
\newcommand{\Ter}{{\bf 1}}

\newcommand{\imp}{{\sf Imp}}            %imp language
\newcommand{\vm}{{\sf Vm}}              %virtual machine language
\newcommand{\mips}{{\sf Mips}}          %Mips language
\newcommand{\eighty}{{\sf 8051}}
\newcommand{\asm}{{\sf ASM}}
\newcommand{\C}{{\sf C}}                % C language
\newcommand{\gcc}{{\sf gcc}}            %gcc
\newcommand{\Clight}{{\sf Clight}}        %C light language
\newcommand{\Cminor}{{\sf Cminor}}
\newcommand{\RTLAbs}{{\sf RTLAbs}}
\newcommand{\RTL}{{\sf RTL}}
\newcommand{\ERTL}{{\sf ERTL}}
\newcommand{\LTL}{{\sf LTL}}
\newcommand{\LIN}{{\sf LIN}}
\newcommand{\access}[1]{\stackrel{#1}{\leadsto}}
\newcommand{\ocaml}{{\sf ocaml}}
\newcommand{\coq}{{\sf Coq}}
\newcommand{\compcert}{{\sf CompCert}}
\newcommand{\cerco}{{\sf CerCo}}
\newcommand{\cil}{{\sf CIL}}
\newcommand{\scade}{{\sf Scade}}
\newcommand{\absint}{{\sf AbsInt}}
\newcommand{\framac}{{\sf Frama-C}}
\newcommand{\powerpc}{{\sf PowerPc}}
\newcommand{\lustre}{{\sf Lustre}}
\newcommand{\esterel}{{\sf Esterel}}
\newcommand{\ml}{{\sf ML}}
%\newcommand{\ocaml}{{\sf OCAML}}



\author{Roberto M. Amadio}
\institute{Universit\'e Paris Diderot}

\title{CerCo Work Package 2: Untrusted Compiler Prototype (part 1)}
\date{March 11, 2011}

\begin{document}

\begin{frame}
\maketitle
\end{frame}




\begin{frame}

\frametitle{Goal and schedule of WP2}
Implement a {\bf proof-of-concept prototype} of the cost annotating compiler.

\begin{description}

\item[Task 2.1] Architectural design ($\Arrow$ D2.1)

\item[Task 2.2] Intermediate languages and data structures ($\Arrow$ D2.1)

\item[Task 2.3] Implementation ($\Arrow$ D2.2)

\item[Task 2.4] Integration validation and testing (terminates at T0+18, no deliverable)
\end{description}

\begin{description}

\item[D2.1] Compiler design and Intermediate languages (T0+6).

\item[D2.2] Untrusted cost-annotating $\ocaml$ compiler (T0+12). 

\end{description}
{\small This first part is an {\bf introduction} to Tasks 2.1 and 2.2. The
second part will give more details on Task 2.2, discuss Task 2.3 (with demo), 
and  provide some perspectives on Task 2.4 and WP5.}

\end{frame}


\begin{frame}

\frametitle{People involved at Paris site}


\begin{tabular}{|c|c|c|}

\hline
{\bf Name}           &{\bf Status} &{\bf Rough Allocated Time} \\\hline
Roberto Amadio &Professor &1 day/week \\
Yann R\'egis-Gianas &Assistant Professor &1 day/week \\
Nicolas Ayache      &Post-doc      &full time, 11 months \\
Ronan Saillard      &Internship+PhD &full time, 8 months \\
Kayvan Memarian     &Internship   &1.5 days/week, 4 months \\ \hline
\end{tabular}

\end{frame}














\begin{frame}

\frametitle{Motivation}
Resource analysis of programming models should, if we are serious about it,
eventually have an impact on programming practice. Limiting factors include:

\begin{itemize}

\item Bounds are {\bf asymptotic} and sometimes a bit {\bf shaky} (exotic compilers):  we need an effort to make them concrete and reliable.

\item Should focus on software applications that {\bf do care about resource bounds}. E.g., focus on embedded programs rather than on pure functional programs.

\item Implicit complexity programming languages are a straight jacket: {\bf restrictions} are often complex and too difficult to program with.

\end{itemize}

\end{frame}


\begin{frame}

\frametitle{CerCo goals and approach}

\begin{itemize}

\item Bound and certify the {\bf number of cycles} that it takes to run a 
given  piece of code on a given processor with a given compiler.

\item Target {\bf C programs}, and in particular the kind of C 
programs produced for embedded applications 
(such as those generated by the SCADE compiler).

\item {\bf Reflect the cost information} obtained at the machine level 
back into the C source code.

\item {\bf Extract synthetic bounds} by reasoning on 
the annotated C  programs (for which several general purpose tools now exist).

\end{itemize}

\NB Technically, this can be seen as a refinement of ongoing work on {\bf compiler certification}   
(see, e.g., CompCert project).

\end{frame}



\begin{frame}

\frametitle{Current technology and our challenge}
\begin{itemize}


\item Compilation phases are heavily {\bf inspected and tested} 
but not formally checked with a proof assistant.
\[
\textsc{Lustre} \arrow \textsc{C} \arrow \textsc{binary~ code}
\]
\item Binary code must be {\bf annotated} with (uncertified) 
information on the number of iterations of loops.

\item Tools such as \textsc{AbsInt} perform WCET analysis of 
{\bf sequences of instructions of binary code}.

\end{itemize}

\noindent{\bf Our challenge}
Lift in a certified way whathever information we have on the execution
cost of the binary code to an information on the C source code (a kind
of {\bf decompilation}).

\end{frame}



\begin{frame}

\frametitle{A potential connection}
Could use this work as a {\bf platform} to experiment with 
`implicit complexity programming languages'.

{\small
\begin{enumerate}

\item Write a program in your preferred implicit-complexity programming language.
\item Compile it to C.
\item CerCo compiles C to machine code and provides precise and certified information on execution time of C code.
\item Use your implicit complexity analysis to produce automatically a synthetic bound on the resources used by the program.
\item If you want to push this further, try to lift the assertions about the C code to assertions on your source program.
\end{enumerate}}
\end{frame}




\begin{frame}

\frametitle{Is this really possible?}

\begin{itemize}

\item 
What are the  annotations, and how are we going to actually 
prove that they are correct? \\
$\Arrow$ We need a {\bf proof methodology}.~\\~\\

\item 
Is it possible to produce annotations of the source code 
that predict soundly and precisely the execution cost?\\
$\Arrow$ We need to {\bf show that the approach scales}.

\end{itemize}

\end{frame}




\begin{frame}

\frametitle{Preliminary ideas}

\begin{itemize}

\item 
A cost annotation is an {\bf instrumentation} of the source program 
that keeps track of the execution cost of the program.

\item 
The computed cost should be {\bf correct} and possibly {\bf precise} 
relatively to the compiled code.

\item 
Starting from the annotated source program apply standard tools
to reason about C programs in order to {\bf extract synthetic bounds}.

\end{itemize}

\end{frame}




\begin{frame}

\frametitle{A small size case study (direct approach 1/3)}

{\footnotesize
\[
\begin{array}{ccccc}

      &\cl{C}   &                          &\cl{C'}              \\

\imp   &\arrow        &\vm                &\arrow       &\mips        \\

\ \quad\downarrow \w{An}_{\imp}
&
&\ \quad\downarrow \w{An}_{\vm}
&
&\ \quad\downarrow \w{An}_{\mips} \\

\imp   &             &\vm             & &\mips        \\

\end{array}
\]}
\begin{itemize}

\item $\imp$: an imperative language with while loops.

\item $\vm$: a virtual machine with a stack.

\item $\mips$: an assembly like language with registers and RAM memory.

\item $\cl{C}$: relies on the stack to evaluate numerical expressions.

\item $\cl{C'}$: statically allocates the base of the stack in the registers and the
rest in RAM memory. This requires a `stack height' analysis of the $\vm$ code.

\item $\w{An}_{\mips}$: counts the number of $\mips$ instructions executed.

\end{itemize}

\end{frame}


\begin{frame}
\frametitle{A small size case study (direct approach 2/3)}
{\footnotesize
\[
\begin{array}{ccccc}

      &\cl{C}   &                          &\cl{C'}              \\

\imp   &\arrow        &\vm                &\arrow       &\mips        \\

\ \quad\downarrow \w{An}_{\imp}
&
&\ \quad\downarrow \w{An}_{\vm}
&
&\ \quad\downarrow \w{An}_{\mips} \\

\imp   &             &\vm             & &\mips        \\

\end{array}
\]}

\begin{itemize}


\item The annotation functions instrument the 
code so that it {\bf monitors its execution cost} by incrementing
a (fresh) \w{cost} variable.

\item In particular, the annotation function of the object code 
$\w{An}_{\mips}$ is a  {\bf compelling definition} of the execution cost.

\end{itemize}
\end{frame}


\begin{frame}

\frametitle{A small size case study (direct approach 3/3)}

{\footnotesize
\[
\begin{array}{ccccc}

      &\cl{C}   &                          &\cl{C'}              \\

\imp   &\arrow        &\vm                &\arrow       &\mips        \\

\ \quad\downarrow \w{An}_{\imp}
&
&\ \quad\downarrow \w{An}_{\vm}
&
&\ \quad\downarrow \w{An}_{\mips} \\

\imp   &             &\vm             & &\mips        \\

\end{array}
\]}

\begin{itemize}
\item The annotation function at step $i$ is {\bf correct} with 
respect to the one at step $i+1$ of the compilation
if 

{\small
\[
\infer{(\w{An}_{i}(S),s[0/\w{cost}])\eval s'[c/\w{cost}]}
{\begin{array}{c}
(\w{An}_{i+1}(\cl{C}_{i,i+1}(S)),s[0/\w{cost}]) \eval s'[d/\w{cost}]  \\
d \leq c
\end{array}}
\]}

\item Further it is {\bf precise} if \ $c\leq d+\kappa(S)$.

\end{itemize}

\end{frame}

\begin{frame}

\frametitle{Problems with the direct approach}
K. \textsc{Memarian} formalized this in \textsc{Coq} 
(500 lines of specification and 2400 lines of proofs).

\begin{itemize}

\item Proofs have to manipulate {\bf numerical values}.

\item Proofs about the bounds are {\bf intertwined} 
with those of functional correctness and get much larger
(factor $7$ in the experiment).

\item To be precise we need to explicit a lot of {\bf contextual information}
which is at odd with proof compositionality.

\end{itemize}

\end{frame}


\begin{frame}

\frametitle{Second attempt: labelling approach (1/7)}
{\footnotesize
\[
\begin{array}{ccccc}


\imp      &                              &                          &                & \\

\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\

\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\

\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
&
&\ \quad\downarrow \w{er}_{\vm}
&
&\ \quad\downarrow \w{er}_{\mips} \\ 

\imp   &\arrow             &\vm             &\arrow &\mips        \\
      &\cl{C}   &                          &\cl{C'}              \\
\end{array}
\]}

\begin{description}

\item[Labelled languages] All languages are enriched with \bem{labelled instructions} generating \bem{labelled transitions}.

\item[Erasures] The \bem{erasure functions} are just functions that remove all labelling instructions.

\end{description}

\end{frame}



\begin{frame}

\frametitle{Labelling approach  (2/7)}
{\footnotesize
\[
\begin{array}{ccccc}


\imp      &                              &                          &                & \\

\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\

\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\

\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
&
&\ \quad\downarrow \w{er}_{\vm}
&
&\ \quad\downarrow \w{er}_{\mips} \\ 

\imp   &\arrow             &\vm             &\arrow &\mips        \\
      &\cl{C}   &                          &\cl{C'}              \\
\end{array}
\]}

\begin{description}



\item[Extended compilation] The compilation functions are \bem{extended} to the labelled languages.

\item[Commutation] Compilation and erasure functions \bem{commute}:
\[
\w{er}_{\vm} \comp \cl{C} = \cl{C} \comp \w{er}_{\imp} \qquad
\w{er}_{\mips} \comp \cl{C'} = \cl{C'} \comp \w{er}_{\vm}
\]

\end{description}
\end{frame}



\begin{frame}

\frametitle{Labelling approach (3/7)}
{\footnotesize
\[
\begin{array}{ccccc}


\imp      &                              &                          &                & \\

\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\

\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\

\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
&
&\ \quad\downarrow \w{er}_{\vm}
&
&\ \quad\downarrow \w{er}_{\mips} \\ 

\imp   &\arrow             &\vm             &\arrow &\mips        \\
      &\cl{C}   &                          &\cl{C'}              \\
\end{array}
\]}

{\small
\begin{description}

\item[Labelling] A \bem{labelling} of the source language is just a function $\cl{L}$ such that $\w{er}_{\imp}\comp \cl{L}=\w{id}_{\imp}$.

\item[Instrumentation]
Given a \bem{`cost function'} associating costs to labels,
an \bem{instrumentation} of the source language is a 
function $\cl{I}_{\imp}$  replacing  labels with suitable increments
of a fresh \bem{cost variable}.

\item[Annotation]
 An \bem{annotation} of the source language is defined as: 
\[
\w{An}_{\imp} = \cl{I}_{\imp}\comp \cl{L}~.
\]

\end{description}}

\end{frame}

\begin{frame}

\frametitle{Labelling approach (4/7)}
{\footnotesize
\[
\begin{array}{ccccc}


\imp      &                              &                          &                & \\

\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\

\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\

\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
&
&\ \quad\downarrow \w{er}_{\vm}
&
&\ \quad\downarrow \w{er}_{\mips} \\ 

\imp   &\arrow             &\vm             &\arrow &\mips        \\
      &\cl{C}   &                          &\cl{C'}              \\
\end{array}
\]}

{\bf Simulation}
The simulation properties of the compilation functions are lifted to the labelled languages.

With a proper design of the labelled languages this just means taking into account the rules that
generate labelled transitions.  

Let $\lambda$ denote a sequence of labels. Then we have:
\[
(S,s)\eval (s',\lambda)  \quad \Arrow \quad 
(\cl{C}(S),s) \eval (s',\lambda) \quad \Arrow \quad
(\cl{C'}(\cl{C}(S)),s) \eval (s',\lambda)
\]

\end{frame}


\begin{frame}


\frametitle{Labelling approach (5/7)}
{\footnotesize
\[
\begin{array}{ccccc}


\imp      &                              &                          &                & \\

\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\

\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\

\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
&
&\ \quad\downarrow \w{er}_{\vm}
&
&\ \quad\downarrow \w{er}_{\mips} \\ 

\imp   &\arrow             &\vm             &\arrow &\mips        \\
      &\cl{C}   &                          &\cl{C'}              
\end{array}
\]}

By {\bf diagram chasing} we get:
\[
\infer{(\w{An}(S),s[c/\w{cost}])  \eval s'[c+\delta/\w{cost}]}
{(\cl{C}(\cl{L}(S)),s[c/\w{cost}])  \eval (s'[c/\w{cost}],\lambda)}
\]
where $\delta$ is an `arbitrary additive cost' 
of the sequence of labels $\lambda$.

\end{frame}



\begin{frame}

\frametitle{Labelling approach (6/7)}
{\footnotesize
\[
\begin{array}{ccccc}


\imp      &                              &                          &                & \\

\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\

\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\

\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
&
&\ \quad\downarrow \w{er}_{\vm}
&
&\ \quad\downarrow \w{er}_{\mips} \\ 

\imp   &\arrow             &\vm             &\arrow &\mips        \\
      &\cl{C}   &                          &\cl{C'}              \\
\end{array}
\]}

Knowing that 
\[
\cl{C'}(\cl{C}(S)) = \w{er}_{\mips}(\cl{C'}(\cl{C}(\cl{L}(S)))
\]
{\bf under which conditions} can we conclude that $\lambda$, {\em i.e.}, $\delta$, is a sound and  possibly precise description of the real execution cost?

\end{frame}


\begin{frame}

\frametitle{Labelling approach (7/7)}

{\small
\begin{itemize}

\item Assume a sound over-approximation of 
the {\bf control flow} of the labelled object code
$(\cl{C'}(\cl{C}(L(S))$. 
This is a directed, rooted graph where some nodes are labelled.

\item The labelling is {\bf sound} if in the CFG
all nodes are reachable from a labelled node and 
all loops go through a labelled node.

\item In this case, the {\bf cost of a label} $\ell$ is the cost 
of the most expensive path in the control flow graph starting 
from a node labelled $\ell$
and, crossing unlabelled nodes, arriving at a labelled one 
or an unlabelled one without
successors (call such paths {\bf simple}).

\item A sound labelling is {\bf precise} if for all labels $\ell$ the 
paths of the kind
described above starting from a node labelled $\ell$ have the same cost.


\end{itemize}}

\end{frame}

\begin{frame}

\frametitle{Advantages of the labelling approach}

\begin{itemize}

\item  Costs are handled {\bf symbolically} 
as labels are propagated by the compiler.

\item  Proofs of {\bf functional correctness stay simple} 
(just one additional case to cover the labels)

\item  {\bf No need to explicit the contextual information}. 
The numerical cost is computed only at the assembly language level
and then it is reflected back to the source.

\end{itemize}

\end{frame}


\begin{frame}

\frametitle{A larger experiment: a $C$ to $\mips$ compiler}
{\footnotesize
\[
\begin{array}{cccccccccc}
&&\C &\arrow &\Clight &\arrow &\Cminor &\arrow &\RTLAbs &\qquad \mbox{(front end)}\\
                                              &&&&&&&&\downarrow \\
 \mips &\leftarrow &\LIN &\leftarrow  &\LTL &\leftarrow  &\ERTL  &\leftarrow &\RTL &\qquad \mbox{(back-end)}
\end{array}
\]
}

{\small
\begin{itemize}

\item Moderate optimisations: register allocation, dead-code elimination,$\ldots$ (a bit more efficient than {\tt gcc0}).

\item Roughly, we implement the labelling approach on top of a compiler quite
close to {\sc CompCert}.

\item Around 10K lines of $\ocaml$ code. No proofs, just code inspection and test. We used the software  in a master level compilation course.

\end{itemize}}

\end{frame}


\begin{frame}

\frametitle{Observed soundness and precision for the $C$ compiler}
As a rule of thumb,  we lose {\bf soundness} if we miss loops in the generated  code.
We lose {\bf precision} if we miss branching in the generated code.

\begin{itemize}

\item The first situation never arises in the considered compilation chain.

\item The second situation can be handled by some pre-processing of the C code
(e.g., logical \bem{and} compiled as a conditional expression).

\end{itemize}

\end{frame}



\begin{frame}

\frametitle{What comes next}
This work was completed in the first 7 months of the project.
The following months have been spent:


\begin{itemize}

\item Extending the formal proofs on the toy compiler.

\item Enhancing and debugging the compiler.

\item Porting it to the 8051 processor.

\item Integrating the {\sc Ocaml/Matita} description of 8051.

\end{itemize}

This is discussed in the second part of the talk.

\end{frame}

\end{document}