source: Deliverables/D1.1/Presentations/WP2-roberto.tex @ 666

Last change on this file since 666 was 666, checked in by amadio, 9 years ago

WP-roberto update

File size: 37.1 KB
Line 
1
2
3
4
5
6\documentclass{beamer}
7
8\usetheme{Frankfurt}
9%\logo{\includegraphics[height=1.0cm]{fetopen.png}}
10% smaller
11\logo{\includegraphics[height=0.6cm]{fetopen.png}}
12
13
14\usepackage[english]{babel}
15\usepackage{inputenc}
16
17
18
19                           
20%\documentclass[landscape]{seminar}
21
22% \usepackage[latin1]{inputenc}
23% \usepackage[frenchb]{babel}
24
25
26%TO HAVE AN ARTICLE STYLE
27%\documentclass[11pt]{article}
28%\usepackage{latexsym}
29%\usepackage{amsfonts}
30%\usepackage{a4wide}
31
32
33
34% TO HAVE COLOURS IN SLIDES, USAGE \Blu{}, \Red{}, \Green{}, \Purple{}
35\usepackage{epsfig}
36\usepackage{color}
37\usepackage{fancybox}
38\usepackage{color}
39\usepackage{alltt}
40\definecolor{c1114}{rgb}{1,0.2156862745098,0.75294117647059}
41\definecolor{c1112}{rgb}{1,0,0}
42\definecolor{c1121}{rgb}{0,0,0.54509803921569}
43\definecolor{c1123}{rgb}{0,0.5,0}
44\def\Green#1{\textcolor{c1123}{#1}}
45\def\Blu#1{\textcolor{c1121}{#1}}
46\def\Red#1{\textcolor{c1112}{#1}}
47\def\Purple#1{\textcolor{c1114}{#1}}
48\definecolor{c1082}{rgb}{0.,0.,0.}
49\definecolor{c1083}{rgb}{1,0,0}
50
51% TO NEUTRALIZE COLOURS
52%\newcommand{\Red}[1]{#1}
53%\newcommand{\Blu}[1]{#1}
54%\newcommand{\Green}[1]{#1}
55%\newcommand{\Purple}[1]{#1}
56
57%TO NEUTRALIZE SLIDE
58% replace {slide} by {slid} and insert
59%\newenvironment{slid}{}{}
60
61% ALSO REMOVE \newpage
62
63
64\newcommand{\eqdef}{=_{\text{def}}} 
65\newcommand{\concat}{\cdot}%%{\mathbin{+}}
66
67\newcommand{\Models}{\mid \! =}              % models
68\newcommand{\Int}{\mathit{int}} 
69\newcommand{\nat}{\mathit{nat}} 
70\newcommand{\String}{\mathit{string}} 
71\newcommand{\Ident}{\mathit{ident}} 
72\newcommand{\Block}{\mathit{block}} 
73\newcommand{\Signature}{\mathit{signature}} 
74 
75\newcommand{\pc}{\mathit{pc}} 
76\newcommand{\estack}{\mathit{estack}} 
77\newcommand{\Error}{\epsilon} 
78 
79%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
80%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81 
82% --------------------------------------------------------------------- %
83% Proof rule.                                                           %
84% --------------------------------------------------------------------- %
85 
86\newcommand{\staterule}[3]{%
87  $\begin{array}{@{}l}%
88   \mbox{#1}\\%
89   \begin{array}{c}
90   #2\\ 
91   \hline 
92   \raisebox{0ex}[2.5ex]{\strut}#3%
93   \end{array}
94  \end{array}$} 
95 
96\newcommand{\GAP}{2ex} 
97 
98\newcommand{\recall}[2]{%
99 $\begin{array}{c}
100 #1\\ 
101 \hline 
102 \raisebox{0ex}[2.5ex]{\strut}#2%
103 \end{array}$} 
104 
105\newcommand{\hbra}{\noindent\hbox to \textwidth{\leaders\hrule height1.8mm depth-1.5mm\hfill}} 
106\newcommand{\hket}{\noindent\hbox to \textwidth{\leaders\hrule height0.3mm\hfill}} 
107\newcommand{\ratio}{.3} 
108 
109\newenvironment{display}[1]{\begin{tabbing} 
110  \hspace{1.5em} \= \hspace{\ratio\linewidth-1.5em} \= \hspace{1.5em} \= \kill 
111  \noindent\hbra\\[-.5em] 
112  {\ }\textsc{#1}\\[-.8ex] 
113  \hbox to \textwidth{\leaders\hrule height1.6mm depth-1.5mm\hfill}\\[-.8ex] 
114  }{\\[-.8ex]\hket 
115  \end{tabbing}} 
116 
117 
118\newcommand{\sbline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.2ex}\hfill\hspace*{0ex}}} 
119\newcommand{\sline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.1ex}\hfill\hspace*{0ex}}} 
120\newcommand{\sentry}[2]{\>$#1$\>\ \smash[t]{\vrule width 0.2mm height
121    1.2\baselineskip depth 1.5\baselineskip}\>#2} 
122 
123\newcommand{\entry}[2]{\>$#1$\>\>#2} 
124\newcommand{\clause}[2]{$#1$\>\>#2} 
125\newcommand{\category}[2]{\clause{#1::=}{#2}} 
126\newcommand{\subclause}[1]{\>\>\>#1} 
127\newcommand{\redrule}[3]{$#1$\>\>$#2$\>\>\>#3} 
128 
129%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
130%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
131 
132% environments
133 
134%% \newtheorem{theorem}{Theorem}
135%% \newtheorem{fact}[theorem]{Fact}
136%% \newtheorem{definition}[theorem]{Definition}
137%% \newtheorem{lemma}[theorem]{Lemma}
138%% \newtheorem{corollary}[theorem]{Corollary}
139%% \newtheorem{proposition}[theorem]{Proposition}
140%% \newtheorem{example}[theorem]{Example}
141%% \newtheorem{exercise}[theorem]{Exercise}
142%% \newtheorem{remark}[theorem]{Remark}
143%% \newtheorem{proviso}[theorem]{Proviso}
144%%  \newtheorem{conjecture}[theorem]{Conjecture}
145
146% proofs 
147 
148%\newcommand{\Proof}{\noindent {\sc Proof}. }
149\newcommand{\Proofhint}{\noindent {\sc Proof hint}. } 
150%\newcommand{\qed}{\hfill${\Box}$}
151\newcommand{\EndProof}{\qed}
152 
153% figure environment
154 
155\newcommand{\Figbar}{{\center \rule{\hsize}{0.3mm}}}    %horizontal thiner line for figures
156\newenvironment{figureplr}{\begin{figure}[t] \Figbar}{\Figbar \end{figure}} 
157                                                        %environment for figures
158%       ************Macros for mathematical symbols*************
159% Style
160 
161\newcommand{\cl}[1]{{\cal #1}}          % \cl{R} to make R calligraphic
162\newcommand{\la}{\langle}               % the brackets for pairing (see also \pair)
163\newcommand{\ra}{\rangle} 
164 
165\newcommand{\lf}{\lfloor} 
166\newcommand{\rf}{\rfloor} 
167\newcommand{\ul}[1]{\underline{#1}}     % to underline
168\newcommand{\ol}[1]{\overline{#1}}      % to overline
169\newcommand{\ok}{~ok}                   % well formed context
170 
171% Syntax
172 
173\newcommand{\Gives}{\vdash}             % in a type judgment
174\newcommand{\emptycxt}{\O}              % empty context
175\newcommand{\subs}[2]{[#1 / #2]} 
176\newcommand{\sub}[2]{[#2 / #1]}         % substitution \sub{x}{U} gives [U/x]   
177\newcommand{\Sub}[3]{[#3 / #2]#1}       % Substitution with three arguments \Sub{V}{x}{U}
178
179\newcommand{\lsub}[2]{#2 / #1}          % substitution \lsub{x}{U} gives U/x, to be used in a list.
180 
181\newcommand{\impl}{\supset} 
182%\newcommand{\imp}{{\sc Imp}}            %imp language
183%\newcommand{\vm}{{\sc Vm}}              %virtual machine language
184\newcommand{\arrow}{\rightarrow}        % right thin arrow
185\newcommand{\trarrow}{\stackrel{*}{\rightarrow}}        % trans closure
186\newcommand{\bt}[1]{{\it BT}(#1)}       % Boehm tree
187\newcommand{\cxt}[1]{#1[~]}             % Context with one hole
188\newcommand{\pr}{\parallel}             % parallel ||
189\newcommand{\Nat}{\mathbf{N}}                 % natural numbers
190\newcommand{\Natmax}{\mathbf{N}_{{\it max}}}  % natural numbers with minus infinity
191\newcommand{\Rat}{\mathbf{Q}^{+}}                 % non-negative rationals
192\newcommand{\Ratmax}{\mathbf{Q}^{+}_{{\it max}}}  % non-negative rationals with minus infinity
193\newcommand{\Alt}{ \mid\!\!\mid  } 
194\newcommand{\isum}{\oplus} 
195\newcommand{\dpar}{\mid\!\mid} 
196                                        % for the production of a grammar containing \mid
197\newcommand{\infer}[2]{\begin{array}{c} #1 \\ \hline #2 \end{array}} 
198                                        % to make a centered inference rule
199 
200% (Meta-)Logic
201 
202\newcommand{\bool}{{\sf bool}}          % boolean values
203\newcommand{\Or}{\vee}                  % disjunction
204\newcommand{\OR}{\bigvee}               % big disjunction
205\newcommand{\AND}{\wedge}               % conjunction
206\newcommand{\ANDD}{\bigwedge}           % big conjunction
207\newcommand{\Arrow}{\Rightarrow}        % right double arrow
208\newcommand{\IFF}{\mbox{~~iff~~}}       % iff in roman and with spaces
209\newcommand{\iffArrow}{\Leftrightarrow} % logical equivalence
210 
211% Semantics
212 
213\newcommand{\dl}{[\![}                  % semantic [[
214\newcommand{\dr}{]\!]}                  % semantic ]]
215\newcommand{\lam}{{\bf \lambda}}        % semantic lambda
216
217
218% The equivalences for this paper
219
220% the usual ones
221\newcommand{\ubis}{\approx^u}          % usual labelled weak bis
222\newcommand{\uabis}{\approx^{u}_{ccs}} % usual labelled weak bis on CCS
223
224% the contextual conv sensitive
225\newcommand{\cbis}{\approx}        % convergence sensitive bis
226\newcommand{\cabis}{\approx_{ccs}}  % convergence sensitive bis on CCS
227
228% the labelled conv sensitive
229\newcommand{\lcbis}{\approx^{\ell}} %
230\newcommand{\lcabis}{\approx^{\ell}_{ccs}} % labelled convergence sensitive bis on CCS
231\newcommand{\lcbiswrong}{\approx^{\ell \Downarrow}} %
232
233
234
235
236\newcommand{\maytest}{=_{\Downarrow}}
237\newcommand{\musttest}{=_{\Downarrow_{S}}}
238
239
240 
241 
242% Sets
243 
244\newcommand{\prt}[1]{{\cal P}(#1)}      % Parts of a set
245\newcommand{\finprt}[1]{{\cal P}_{fin}(#1)}% Finite parts
246\newcommand{\finprtp}[1]{{\cal P}_{fin}^{+}(#1)}% Non-empty Finite parts
247\newcommand{\union}{\cup}               % union
248\newcommand{\inter}{\cap}               % intersection
249\newcommand{\Union}{\bigcup}            % big union
250\newcommand{\Inter}{\bigcap}            % big intersection
251\newcommand{\cpl}[1]{#1^{c}}            % complement
252\newcommand{\card}{\sharp}              % cardinality
253\newcommand{\minus}{\backslash}         % set difference
254\newcommand{\sequence}[2]{\{#1\}_{#2}}  % ex. \sequence{d_n}{n\in \omega}
255\newcommand{\comp}{\circ}               % functional composition
256\newcommand{\set}[1]{\{#1\}}            % set enumeration
257\newcommand{\pset}[1]{\{\! | #1 |\!\}}  % pseudo-set notation {| |}
258 
259% Domains
260 
261\newcommand{\two}{{\bf O}}              % Sierpinski space
262\newcommand{\join}{\vee}                % join
263\newcommand{\JOIN}{\bigvee}             % big join 
264\newcommand{\meet}{\wedge}              % meet
265\newcommand{\MEET}{\bigwedge}           % big meet
266\newcommand{\dcl}{\downarrow}           % down closure
267\newcommand{\ucl}{\uparrow}             % up closure
268\newcommand{\conv}{\downarrow}          % synt. conv. pred. (postfix)
269%\newcommand{\diver}{\uparrow}           % diverging term
270\newcommand{\Conv}{\Downarrow}          % sem. conv. pred. (postfix)
271\newcommand{\SConv}{\Downarrow_{S}}          % sem. conv. pred. (postfix)
272\newcommand{\CConv}{\Downarrow_{C}}
273\newcommand{\diver}{\Uparrow}           % diverging map
274\newcommand{\cpt}[1]{{\cal K}(#1)}      % compacts, write \cpt{D}
275\newcommand{\ret}{\triangleleft}        % retract
276\newcommand{\nor}{\succeq}
277\newcommand{\prj}{\underline{\ret}}     % projection
278\newcommand{\parrow}{\rightharpoonup}   % partial function space
279\newcommand{\ub}[1]{{\it UB}(#1)}       % upper bounds
280\newcommand{\mub}[1]{{\it MUB}(#1)}     % minimal upper bounds
281\newcommand{\lift}[1]{(#1)_{\bot}}      % lifting
282%\newcommand{\rel}[1]{\;{\cal #1}\;}     % infix relation (calligraphic)
283\newcommand{\rl}[1]{\;{\cal #1}\;}             % infix relation
284\newcommand{\rel}[1]{{\cal #1}}         %calligraphic relation with no
285                                        %extra space
286\newcommand{\per}[1]{\;#1 \;} 
287\newcommand{\wddagger}{\natural}  % weak suspension
288%\newcommand{\wddagger}{=\!\!\!\!\parallel}  % weak suspension
289% Categories
290 
291\newcommand{\pair}[2]{\langle #1 , #2 \rangle} % pairing \pair{x}{y}, do not use < >.
292 
293%               *******  Notation for the $\pi$-calculus *********
294% Syntax:
295 
296 
297\newcommand{\fn}[1]{{\it fn}(#1)}                       % free names
298\newcommand{\bn}[1]{{\it bn}(#1)}                       % bound names
299\newcommand{\names}[1]{{\it n}(#1)}                     % names
300\newcommand{\true}{{\sf t}}                             % true
301\newcommand{\false}{{\sf f}}                            % false
302\newcommand{\pio}{\pi_1}                                % 1 receptor calculus
303\newcommand{\pioo}{\pi_{1}^{r}} 
304\newcommand{\piom}{\pi_{1}^{-}}                         % 1 receptor calculus wo match
305\newcommand{\pioi}{\pi_{1I}}                    % 1 receptor I-calculus
306\newcommand{\pifo}{\pi_{\w{1f}}}                                % functional calculus
307\newcommand{\pilo}{\pi_{\w{1l}}}                                % located calculus
308\newcommand{\sort}[1]{{\it st}(#1)}                     % sort
309\newcommand{\ia}[1]{{\it ia}(#1)}                     % sort
310\newcommand{\ite}[3]{{\sf if~} #1 {\sf ~then~} #2 {\sf ~else~} #3}      %if then else
311\newcommand{\casep}[2]{{\sf case}^{\times}(#1, \pair{x}{y}\Arrow#2)}      %case on pairs
312\newcommand{\casel}[3]{{\sf case}^{L}(#1, #2, \s{cons}(x,y)\Arrow#3)}      %case on lists
313\newcommand{\caseb}[3]{{\sf case}^{b}(#1, #2, \s{cons}(x,y)\Arrow#3)}      %case on lists
314\newcommand{\nil}{{\sf nil}} 
315\newcommand{\cons}{{\sf cons}} 
316\newcommand{\idle}[1]{{\it Idle}(#1)}                   %idle process
317\newcommand{\conf}[1]{\{ #1 \}}                         %configuration
318\newcommand{\link}[2]{#1 \mapsto #2}                    %likn a ->b
319\newcommand{\mand}{\mbox{ and }} 
320\newcommand{\dvec}[1]{\tilde{{\bf #1}}}                 %double vector
321\newcommand{\erloc}[1]{{\it er}_{l}(#1)}                % location erasure
322\newcommand{\w}[1]{{\it #1}}    %To write in math style
323\newcommand{\vcb}[1]{{\bf #1}} 
324\newcommand{\lc}{\langle\!|} 
325\newcommand{\rc}{|\!\rangle} 
326\newcommand{\obj}[1]{{\it obj}(#1)} 
327\newcommand{\move}[1]{{\sf move}(#1)} 
328\newcommand{\qqs}[2]{\forall\, #1\;\: #2} 
329\newcommand{\xst}[2]{\exists\, #1\;\: #2} 
330\newcommand{\xstu}[2]{\exists\, ! #1\;\: #2} 
331\newcommand{\dpt}{\,:\,} 
332\newcommand{\cond}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3} 
333\newcommand{\s}[1]{{\sf #1}}    % sans-serif 
334\newcommand{\vc}[1]{{\bf #1}} 
335\newcommand{\lnorm}{\lbrack\!\lbrack} 
336\newcommand{\rnorm}{\rbrack\!\rbrack} 
337\newcommand{\sem}[1]{\underline{#1}} 
338\newcommand{\squn}{\mathop{\scriptstyle\sqcup}} 
339\newcommand{\lcro}{\langle\!|} 
340\newcommand{\rcro}{|\!\rangle} 
341\newcommand{\semi}[1]{\lcro #1\rcro} 
342\newcommand{\sell}{\,\ell\,} 
343\newcommand{\SDZ}[1]{\marginpar{\textbf{SDZ:} {#1}}} 
344 
345\newcommand{\when}[3]{{\sf when}~#1~{\sf then}~#2~{\sf else}~#3} 
346\newcommand{\wthen}[2]{{\sf when}~#1~{\sf then}~#2~} 
347\newcommand{\welse}[1]{{\sf else}~#1} 
348
349%Pour la fleche double, il faut rajouter :
350%      \usepackage{mathtools}
351
352\newcommand{\act}[1]{\stackrel{#1}{\rightarrow}} %labelled actionlow %high
353
354%\newcommand{\wact}[1]{\xRightarrow{#1}} %weak labelled action low high
355
356%\newcommand{\mact}[1]{\xrightarrow{#1}_{m}} %labelled action low %high
357
358%\newcommand{\wmact}[1]{\xRightarrow{#1}_{m}} %weak labelled action low high
359
360%\newcommand{\act}[1]{\stackrel{#1}{\rightarrow}} %labelled action low
361                                %%%high
362
363\newcommand{\acteq}[1]{\stackrel{#1}{\leadsto}} %labelled action low
364                                %%%high
365
366
367%\newcommand{\actI}[1]{\stackrel{#1}{\rightarrow_{1}}} %labelled action low
368\newcommand{\actI}[1]{\xrightarrow{#1}_{1}}
369
370%\newcommand{\actII}[1]{\stackrel{#1}{\rightarrow_{2}}} %labelled action low
371\newcommand{\actII}[1]{\xrightarrow{#1}_{2}}
372
373
374 \newcommand{\wact}[1]{\stackrel{#1}{\Rightarrow}} %weak labelled action low high
375\newcommand{\wactI}[1]{\stackrel{#1}{\Rightarrow_{1}}} %weak labelled action low high
376\newcommand{\wactII}[1]{\stackrel{#1}{\Rightarrow_{2}}} %weak labelled action low high
377
378
379\newcommand{\mact}[1]{\stackrel{#1}{\rightarrow_{m}}} %labelled action low %high
380\newcommand{\wmact}[1]{\stackrel{#1}{\Rightarrow_{m}}} %weak labelled action low high
381 
382\newcommand{\lact}[1]{\stackrel{#1}{\leftarrow}} 
383\newcommand{\lwact}[1]{\stackrel{#1}{\Leftarrow}} 
384 
385 
386 
387\newcommand{\eval}{\Downarrow} 
388\newcommand{\Eval}[1]{\Downarrow^{#1}} 
389 
390 
391\newcommand{\Z}{{\bf Z}} 
392\newcommand{\Real}{\mathbb{R}^{+}} 
393\newcommand{\Return}{\ensuremath{\mathtt{return}}\xspace}                 
394\newcommand{\Stop}{\ensuremath{\mathtt{stop}}\xspace} 
395\newcommand{\Wait}{\ensuremath{\mathtt{wait}}\xspace} 
396\newcommand{\Read}{\ensuremath{\mathtt{read}}\xspace} 
397\newcommand{\Write}{\ensuremath{\mathtt{write}}\xspace} 
398\newcommand{\Yield}{\ensuremath{\mathtt{yield}}\xspace} 
399\newcommand{\Next}{\ensuremath{\mathtt{next}}\xspace} 
400\newcommand{\Load}{\ensuremath{\mathtt{load}}\xspace} 
401\newcommand{\Call}{\ensuremath{\mathtt{call}}\xspace} 
402\newcommand{\Tcall}{\ensuremath{\mathtt{tcall}}\xspace} 
403\newcommand{\Pop}{\ensuremath{\mathtt{pop}}\xspace} 
404\newcommand{\Build}{\ensuremath{\mathtt{build}}\xspace} 
405\newcommand{\Branch}{\ensuremath{\mathtt{branch}}\xspace} 
406\newcommand{\Goto}{\ensuremath{\mathtt{goto}}\xspace} 
407 
408\newcommand{\hatt}[1]{#1^{+}} 
409\newcommand{\Of}{\mathbin{\w{of}}} 
410 
411\newcommand{\susp}{\downarrow} 
412\newcommand{\lsusp}{\Downarrow_L} 
413\newcommand{\wsusp}{\Downarrow} 
414\newcommand{\commits}{\searrow} 
415 
416 
417\newcommand{\spi}{S\pi} 
418 
419
420 \newcommand{\pres}[2]{#1\triangleright #2} %TCCS else next (alternative)
421% \newcommand{\pres}[2]{ \lfloor #1 \rfloor (#2)}  %TCCS else next
422\newcommand{\present}[3]{{\sf present} \ #1 \ {\sf do } \ #2 \ {\sf  else} \ #3}
423
424
425\newcommand{\tick}{{\sf tick}}          %tick action
426
427 
428 
429\newcommand{\sbis}{\equiv_L} 
430\newcommand{\emit}[2]{\ol{#1}#2} 
431%\newcommand{\present}[4]{#1(#2).#3,#4}
432\newcommand{\match}[4]{[#1=#2]#3,#4}       %pi-equality
433
434\newcommand{\matchv}[4]{[#1 > #2]#3,#4}
435
436\newcommand{\new}[2]{\nu #1 \ #2} 
437\newcommand{\outact}[3]{\new{{\bf #1}}{\emit{#2}{#3}}} 
438\newcommand{\real}{\makebox[5mm]{\,$\|\!-$}}% realizability relation
439 
440
441
442\newcommand{\tit}[1]{\begin{center} \Red{{\bf #1 }}\end{center}}
443\newcommand{\stit}[1]{\begin{center} #1 \end{center}}
444\newcommand{\chpt}[1]{\begin{center} \Red{{\huge #1 }}\end{center}}
445\newcommand{\bem}[1]{\Blu{{\em #1}}}
446\newcommand{\NB}{{\bf NB}~}
447\newcommand{\Refer}[1]{\Green{{\small {\bf Ref} \ #1}}}
448
449\newcommand{\tact}[2]{\ensuremath{\underset{#1}{\act{~#2~}}}}
450\newcommand{\tacteq}[2]{\ensuremath{\underset{#1}{\acteq{~#2~}}}}
451\newcommand{\twbis}{\approx^{t}}        % typed weak bis
452
453\newcommand{\regterm}[2]{{\sf reg}_{#1} #2}
454\newcommand{\thread}[1]{{\sf thread} \ #1}
455\newcommand{\store}[2]{(#1 \Leftarrow #2)}
456\newcommand{\gt}[1]{{\sf get}(#1)}
457\newcommand{\st}[2]{{\sf set}(#1,#2)}
458\newcommand{\regtype}[2]{{\sf Reg}_{#1} #2}
459
460\newcommand{\Beh}{{\bf B}}
461\newcommand{\Ter}{{\bf 1}}
462
463\newcommand{\imp}{{\sf Imp}}            %imp language
464\newcommand{\vm}{{\sf Vm}}              %virtual machine language
465\newcommand{\mips}{{\sf Mips}}          %Mips language
466\newcommand{\eighty}{{\sf 8051}}
467\newcommand{\asm}{{\sf ASM}}
468\newcommand{\C}{{\sf C}}                % C language
469\newcommand{\gcc}{{\sf gcc}}            %gcc
470\newcommand{\Clight}{{\sf Clight}}        %C light language
471\newcommand{\Cminor}{{\sf Cminor}}
472\newcommand{\RTLAbs}{{\sf RTLAbs}}
473\newcommand{\RTL}{{\sf RTL}}
474\newcommand{\ERTL}{{\sf ERTL}}
475\newcommand{\LTL}{{\sf LTL}}
476\newcommand{\LIN}{{\sf LIN}}
477\newcommand{\access}[1]{\stackrel{#1}{\leadsto}}
478\newcommand{\ocaml}{{\sf ocaml}}
479\newcommand{\coq}{{\sf Coq}}
480\newcommand{\compcert}{{\sf CompCert}}
481\newcommand{\cerco}{{\sf CerCo}}
482\newcommand{\cil}{{\sf CIL}}
483\newcommand{\scade}{{\sf Scade}}
484\newcommand{\absint}{{\sf AbsInt}}
485\newcommand{\framac}{{\sf Frama-C}}
486\newcommand{\powerpc}{{\sf PowerPc}}
487\newcommand{\lustre}{{\sf Lustre}}
488\newcommand{\esterel}{{\sf Esterel}}
489\newcommand{\ml}{{\sf ML}}
490%\newcommand{\ocaml}{{\sf OCAML}}
491
492
493
494\author{Roberto M. Amadio}
495\institute{Universit\'e Paris Diderot}
496
497\title{$\cerco$ Work Package 2: Untrusted Compiler Prototype (part 1)}
498\date{March 11, 2011}
499
500\begin{document}
501
502\begin{frame}
503\maketitle
504\end{frame}
505
506
507
508
509\begin{frame}
510
511\frametitle{Goal and schedule of WP2}
512Implement a {\bf proof-of-concept prototype} of the cost annotating compiler.
513
514{\small
515\begin{description}
516
517\item[Task 2.1] Architectural design ($\Arrow$ D2.1)
518
519\item[Task 2.2] Intermediate languages and data structures ($\Arrow$ D2.1)
520
521\item[Task 2.3] Implementation ($\Arrow$ D2.2)
522
523\item[Task 2.4] Integration validation and testing (terminates at T0+18, no deliverable)
524\end{description}
525
526\begin{description}
527
528\item[D2.1] Compiler design and Intermediate languages (T0+6).
529
530\item[D2.2] Untrusted cost-annotating $\ocaml$ compiler (T0+12).
531
532\end{description}}
533
534{\small \Red{\NB} This first part is an {\bf introduction} to Tasks 2.1 and 2.2. The
535second part will give more details on Task 2.2, discuss Task 2.3 (with demo),
536and  provide some perspectives on Task 2.4 and WP5.}
537
538\end{frame}
539
540
541
542
543
544\begin{frame}
545
546\frametitle{People involved at UPD site}
547
548
549{\small
550\begin{tabular}{|c|c|c|}
551
552\hline
553{\bf Name}           &{\bf Status} &{\bf Rough Allocated Time} \\\hline
554Roberto \textsc{Amadio} &Professor &1 day/week \\
555Yann \textsc{R\'egis-Gianas} &Assistant Professor &1 day/week \\
556Nicolas \textsc{Ayache}      &Post-doc      &full time, 11 months \\
557Ronan \textsc{Saillard}      &Internship+PhD &full time, 8 months \\
558Kayvan \textsc{Memarian}     &Internship   &1.5 days/week, 4 months \\ \hline
559\end{tabular}}
560
561
562~\\~\\
563\Red{{\bf NB}} Internships are very important: dissemination, speed up development,
564explore side paths, preliminary training towards research (PhD),$\ldots$
565
566\end{frame}
567
568
569\begin{frame}
570
571\frametitle{$\cerco$ goals and approach (again)}
572
573\begin{itemize}
574
575\item Bound and certify the {\bf number of cycles} that it takes to run a
576given  piece of code on a given processor with a given compiler.
577
578\item Target {\bf $\C$ programs}, and in particular the kind of $\C$ 
579programs produced for embedded applications
580(such as those generated by the $\scade$ compiler).
581
582\item {\bf Reflect the cost information} obtained at the machine level
583back into the $\C$ source code.
584
585\item {\bf Extract synthetic bounds} by reasoning on
586the annotated $\C$  programs (for which several general purpose tools now exist).
587
588\end{itemize}
589
590\Red{\NB} Technically, this can be seen as a refinement of ongoing work on {\bf compiler certification}   
591(see, e.g., $\compcert$ project).
592
593\end{frame}
594
595
596
597
598\begin{frame}
599
600\frametitle{More motivation}
601Resource analysis of programming models should, if we are serious about it,
602eventually have an impact on programming practice. Limiting factors include:
603
604\begin{itemize}
605
606\item Bounds are {\bf asymptotic} and sometimes a bit {\bf shaky} (exotic compilers):  we need an effort to make them concrete and reliable.
607
608\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.
609
610\item Implicit complexity programming languages are a straight jacket: {\bf restrictions} are often complex and too difficult to program with.
611
612\end{itemize}
613
614\end{frame}
615
616
617
618\begin{frame}
619
620\frametitle{A potential connection}
621Could use this work as a {\bf platform} to experiment with
622\Blu{{\em implicit complexity programming languages}}.
623
624{\small
625\begin{enumerate}
626
627\item Write a program in your preferred implicit complexity programming language.
628\item Compile it to $\C$.
629\item $\cerco$ compiles $\C$ to machine code and provides precise and certified information on execution time of $\C$ code.
630\item Use your implicit complexity analysis to produce automatically a synthetic bound on the resources used by the program.
631\item If you want to push this further, try to lift the assertions about the $\C$ code to assertions on your source program.
632\end{enumerate}}
633\Red{\NB} Might be another case study for WP5.
634\end{frame}
635
636
637
638\begin{frame}
639
640\frametitle{Current technology and our challenge (again)}
641\begin{itemize}
642
643
644\item Compilation phases are heavily {\bf inspected and tested} 
645but not formally checked with a proof assistant.
646\[
647\lustre \arrow \C \arrow \textsc{binary~ code}
648\]
649\item Binary code must be {\bf annotated} with (uncertified)
650information on the number of iterations of loops.
651
652\item Tools such as \textsc{AbsInt} perform WCET analysis of
653{\bf sequences of instructions of binary code}.
654
655\end{itemize}
656
657\noindent \Red{{\bf Our challenge}}
658Lift in a {\em certified way} whathever information we have on the execution
659cost of the binary code to an information on the $\C$ source code (a kind
660of {\bf decompilation}).
661
662\end{frame}
663
664
665
666
667
668\begin{frame}
669
670\frametitle{Is this really possible?}
671
672\begin{itemize}
673
674\item 
675What are the  annotations, and how are we going to actually
676prove that they are correct? \\
677$\Arrow$ We need a {\bf proof methodology}.~\\~\\
678
679\item 
680Is it possible to produce annotations of the source code
681that predict soundly and precisely the execution cost?\\
682$\Arrow$ We need to {\bf show that the approach scales}.
683
684\end{itemize}
685
686\end{frame}
687
688
689
690
691\begin{frame}
692
693\frametitle{Preliminary ideas}
694
695\begin{itemize}
696
697\item 
698A cost annotation is an {\bf instrumentation} of the source program
699that keeps track of the execution cost of the program.
700
701\item 
702The computed cost should be {\bf correct} and possibly {\bf precise} 
703relatively to the compiled code.
704
705\item 
706Starting from the annotated source program apply standard tools
707to reason about $\C$ programs in order to {\bf extract synthetic bounds}.
708
709\end{itemize}
710
711\end{frame}
712
713
714
715
716\begin{frame}
717
718\frametitle{A small size case study (direct approach 1/3)}
719
720{\footnotesize
721\[
722\begin{array}{ccccc}
723
724      &\cl{C}   &                          &\cl{C'}              \\
725
726\imp   &\arrow        &\vm                &\arrow       &\mips        \\
727
728\ \quad\downarrow \w{An}_{\imp}
729&
730&\ \quad\downarrow \w{An}_{\vm}
731&
732&\ \quad\downarrow \w{An}_{\mips} \\
733
734\imp   &             &\vm             & &\mips        \\
735
736\end{array}
737\]}
738\begin{itemize}
739
740\item $\imp$: an imperative language with while loops.
741
742\item $\vm$: a virtual machine with a stack.
743
744\item $\mips$: an assembly like language with registers and RAM memory.
745
746\item $\cl{C}$: relies on the stack to evaluate numerical expressions.
747
748\item $\cl{C'}$: statically allocates the base of the stack in the registers and the
749rest in RAM memory. This requires a `stack height' analysis of the $\vm$ code.
750
751\item $\w{An}_{\mips}$: counts the number of $\mips$ instructions executed.
752
753\end{itemize}
754
755\end{frame}
756
757
758\begin{frame}
759\frametitle{A small size case study (direct approach 2/3)}
760{\footnotesize
761\[
762\begin{array}{ccccc}
763
764      &\cl{C}   &                          &\cl{C'}              \\
765
766\imp   &\arrow        &\vm                &\arrow       &\mips        \\
767
768\ \quad\downarrow \w{An}_{\imp}
769&
770&\ \quad\downarrow \w{An}_{\vm}
771&
772&\ \quad\downarrow \w{An}_{\mips} \\
773
774\imp   &             &\vm             & &\mips        \\
775
776\end{array}
777\]}
778
779\begin{itemize}
780
781
782\item The annotation functions instrument the
783code so that it {\bf monitors its execution cost} by incrementing
784a (fresh) \w{cost} variable.
785
786\item In particular, the annotation function of the object code
787$\w{An}_{\mips}$ is a  {\bf compelling definition} of the execution cost.
788
789\end{itemize}
790\end{frame}
791
792
793\begin{frame}
794
795\frametitle{A small size case study (direct approach 3/3)}
796
797{\footnotesize
798\[
799\begin{array}{ccccc}
800
801      &\cl{C}   &                          &\cl{C'}              \\
802
803\imp   &\arrow        &\vm                &\arrow       &\mips        \\
804
805\ \quad\downarrow \w{An}_{\imp}
806&
807&\ \quad\downarrow \w{An}_{\vm}
808&
809&\ \quad\downarrow \w{An}_{\mips} \\
810
811\imp   &             &\vm             & &\mips        \\
812
813\end{array}
814\]}
815
816\begin{itemize}
817\item The annotation function at step $i$ is {\bf correct} with
818respect to the one at step $i+1$ of the compilation
819if
820
821{\small
822\[
823\begin{array}{lc}
824\mbox{`Predicted' cost} &(\w{An}_{i}(S),s[0/\w{cost}])\eval s'[c/\w{cost}]\\\hline
825\mbox{`Real' cost}       &(\w{An}_{i+1}(\cl{C}_{i,i+1}(S)),s[0/\w{cost}]) \eval s'[d/\w{cost}] \quad d \leq c
826\end{array}
827\]}
828
829\item Further it is {\bf precise} if \ $c\leq d+\kappa(S)$.
830
831\end{itemize}
832
833\end{frame}
834
835\begin{frame}
836
837\frametitle{Problems with the direct approach}
838K. \textsc{Memarian} formalized this in \textsc{Coq} 
839(500 lines of specification and 2400 lines of proofs).
840
841\begin{itemize}
842
843\item Proofs have to manipulate {\bf numerical values}.
844
845\item Proofs about the bounds are {\bf intertwined} 
846with those of functional correctness and get much larger
847(factor $7$ in the experiment).
848
849\item To be precise we need to explicit a lot of {\bf contextual information}
850which is at odd with proof compositionality.
851
852\end{itemize}
853
854\end{frame}
855
856
857\begin{frame}
858
859\frametitle{Second attempt: labelling approach (1/7)}
860{\footnotesize
861\[
862\begin{array}{ccccc}
863
864
865\imp      &                              &                          &                & \\
866
867\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
868
869\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
870
871\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
872&
873&\ \quad\downarrow \w{er}_{\vm}
874&
875&\ \quad\downarrow \w{er}_{\mips} \\ 
876
877\imp   &\arrow             &\vm             &\arrow &\mips        \\
878      &\cl{C}   &                          &\cl{C'}              \\
879\end{array}
880\]}
881
882\begin{description}
883
884\item[Labelled languages] All languages are enriched with \bem{labelled instructions} generating \bem{labelled transitions}.
885
886\item[Erasures] The \bem{erasure functions} are just functions that remove all labelling instructions.
887
888\end{description}
889
890\end{frame}
891
892
893
894\begin{frame}
895
896\frametitle{Labelling approach  (2/7)}
897{\footnotesize
898\[
899\begin{array}{ccccc}
900
901
902\imp      &                              &                          &                & \\
903
904\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
905
906\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
907
908\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
909&
910&\ \quad\downarrow \w{er}_{\vm}
911&
912&\ \quad\downarrow \w{er}_{\mips} \\ 
913
914\imp   &\arrow             &\vm             &\arrow &\mips        \\
915      &\cl{C}   &                          &\cl{C'}              \\
916\end{array}
917\]}
918
919\begin{description}
920
921
922
923\item[Extended compilation] The compilation functions are \bem{extended} to the labelled languages.
924
925\item[Commutation] Compilation and erasure functions \bem{commute}:
926\[
927\w{er}_{\vm} \comp \cl{C} = \cl{C} \comp \w{er}_{\imp} \qquad
928\w{er}_{\mips} \comp \cl{C'} = \cl{C'} \comp \w{er}_{\vm}
929\]
930
931\end{description}
932\end{frame}
933
934
935
936\begin{frame}
937
938\frametitle{Labelling approach (3/7)}
939{\footnotesize
940\[
941\begin{array}{ccccc}
942
943
944\imp      &                              &                          &                & \\
945
946\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
947
948\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
949
950\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
951&
952&\ \quad\downarrow \w{er}_{\vm}
953&
954&\ \quad\downarrow \w{er}_{\mips} \\ 
955
956\imp   &\arrow             &\vm             &\arrow &\mips        \\
957      &\cl{C}   &                          &\cl{C'}              \\
958\end{array}
959\]}
960
961{\small
962\begin{description}
963
964\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}$.
965
966\item[Instrumentation]
967Given a \bem{`cost function'} associating costs to labels,
968an \bem{instrumentation} of the source language is a
969function $\cl{I}_{\imp}$  replacing  labels with suitable increments
970of a fresh \bem{cost variable}.
971
972\item[Annotation]
973 An \bem{annotation} of the source language is defined as:
974\[
975\w{An}_{\imp} = \cl{I}_{\imp}\comp \cl{L}~.
976\]
977
978\end{description}}
979
980\end{frame}
981
982\begin{frame}
983
984\frametitle{Labelling approach (4/7)}
985{\footnotesize
986\[
987\begin{array}{ccccc}
988
989
990\imp      &                              &                          &                & \\
991
992\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
993
994\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
995
996\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
997&
998&\ \quad\downarrow \w{er}_{\vm}
999&
1000&\ \quad\downarrow \w{er}_{\mips} \\ 
1001
1002\imp   &\arrow             &\vm             &\arrow &\mips        \\
1003      &\cl{C}   &                          &\cl{C'}              \\
1004\end{array}
1005\]}
1006
1007\begin{description}
1008
1009\item[Simulation]
1010The simulation properties of the compilation functions are {\em lifted} to the labelled languages.
1011%With a proper design of the labelled languages this just means taking into account the rules that
1012%generate labelled transitions. 
1013Let $\lambda$ denote a sequence of labels. Then:% we have:
1014\end{description}
1015\[
1016(S,s)\eval (s',\lambda)  \quad \Arrow \quad 
1017(\cl{C}(S),s) \eval (s',\lambda) \quad \Arrow \quad
1018(\cl{C'}(\cl{C}(S)),s) \eval (s',\lambda)
1019\]
1020
1021\end{frame}
1022
1023
1024\begin{frame}
1025
1026
1027\frametitle{Labelling approach (5/7)}
1028{\footnotesize
1029\[
1030\begin{array}{ccccc}
1031
1032
1033\imp      &                              &                          &                & \\
1034
1035\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
1036
1037\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
1038
1039\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
1040&
1041&\ \quad\downarrow \w{er}_{\vm}
1042&
1043&\ \quad\downarrow \w{er}_{\mips} \\ 
1044
1045\imp   &\arrow             &\vm             &\arrow &\mips        \\
1046      &\cl{C}   &                          &\cl{C'}             
1047\end{array}
1048\]}
1049
1050\begin{description}
1051
1052\item[Numerical vs. Symbolic cost] By {\bf diagram chasing} we derive:
1053\[
1054\infer{(\w{An}(S),s[c/\w{cost}])  \eval s'[c+\delta/\w{cost}]}
1055{(\cl{C'}(\cl{C}(\cl{L}(S))),s[c/\w{cost}])  \eval (s'[c/\w{cost}],\lambda)}
1056\]
1057where $\delta$ is the numerical (additive) cost associated with $\lambda$.
1058
1059\end{description}
1060
1061\end{frame}
1062
1063
1064
1065\begin{frame}
1066
1067\frametitle{Labelling approach (6/7)}
1068{\footnotesize
1069\[
1070\begin{array}{ccccc}
1071
1072
1073\imp      &                              &                          &                & \\
1074
1075\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
1076
1077\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
1078
1079\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
1080&
1081&\ \quad\downarrow \w{er}_{\vm}
1082&
1083&\ \quad\downarrow \w{er}_{\mips} \\ 
1084
1085\imp   &\arrow             &\vm             &\arrow &\mips        \\
1086      &\cl{C}   &                          &\cl{C'}              \\
1087\end{array}
1088\]}
1089
1090\begin{description}
1091
1092\item[When is the labelling $\cl{L}$ interesting?]
1093I.e., knowing that
1094\[
1095\cl{C'}(\cl{C}(S)) = \w{er}_{\mips}(\cl{C'}(\cl{C}(\cl{L}(S)))
1096\]
1097{\bf under which conditions} can we conclude that $\lambda$, {\em i.e.},
1098$\delta$, is a sound and  possibly precise description of the real execution cost?
1099\end{description}
1100\end{frame}
1101
1102
1103\begin{frame}
1104
1105\frametitle{Labelling approach (7/7)}
1106Conditions to be checked on the labelled binary code.
1107
1108{\small
1109\begin{itemize}
1110
1111\item Assume a sound over-approximation of
1112the {\bf control flow} of the labelled object code
1113$(\cl{C'}(\cl{C}(L(S))$.
1114This is a directed, rooted graph where some nodes are labelled.
1115
1116\item The labelling is {\bf sound} if in the CFG
1117all nodes are reachable from a labelled node and
1118all loops go through a labelled node.
1119
1120\item In this case, the {\bf cost of a label} $\ell$ is the cost
1121of the most expensive path in the control flow graph starting
1122from a node labelled $\ell$
1123and, crossing unlabelled nodes, arriving at a labelled one
1124or an unlabelled one without
1125successors (call such paths {\bf simple}).
1126
1127\item A sound labelling is {\bf precise} if for all labels $\ell$ the
1128paths of the kind
1129described above starting from a node labelled $\ell$ have the same cost.
1130
1131
1132\end{itemize}}
1133
1134\end{frame}
1135
1136\begin{frame}
1137
1138\frametitle{Advantages of the labelling approach}
1139
1140\begin{itemize}
1141
1142\item  Costs are handled {\bf symbolically} 
1143as labels are propagated by the compiler.
1144
1145\item  Proofs of {\bf functional correctness stay simple} 
1146(just one additional case to cover the labels)
1147
1148\item  {\bf No need to explicit the contextual information}.
1149The numerical cost is computed only at the assembly language level
1150and then it is reflected back to the source.
1151
1152\end{itemize}
1153
1154\end{frame}
1155
1156
1157\begin{frame}
1158
1159\frametitle{A larger experiment: a $\C$ to $\mips$ compiler}
1160{\footnotesize
1161\[
1162\begin{array}{cccccccccc}
1163&&\C &\arrow &\Clight &\arrow &\Cminor &\arrow &\RTLAbs &\qquad \mbox{(front end)}\\
1164                                              &&&&&&&&\downarrow \\
1165 \mips &\leftarrow &\LIN &\leftarrow  &\LTL &\leftarrow  &\ERTL  &\leftarrow &\RTL &\qquad \mbox{(back-end)}
1166\end{array}
1167\]
1168}
1169
1170{\small
1171\begin{itemize}
1172
1173\item Moderate optimisations: register allocation, dead-code elimination,$\ldots$ (a bit more efficient than {\tt gcc0}).
1174
1175\item Roughly, we implement the labelling approach on top of a compiler quite
1176close to $\compcert$.
1177
1178\item Around 10K lines of $\ocaml$ code. No proofs, just code inspection and test. We used the software  in a master level compilation course.
1179
1180\end{itemize}}
1181
1182\end{frame}
1183
1184
1185\begin{frame}
1186
1187\frametitle{Observed soundness and precision for the $C$ compiler}
1188As a rule of thumb,  we lose {\bf soundness} if we miss loops in the generated  code.
1189We lose {\bf precision} if we miss branching in the generated code.
1190
1191\begin{itemize}
1192
1193\item The first situation never arises in the considered compilation chain.
1194
1195\item The second situation can be handled by some pre-processing of the $\C$ code
1196(e.g., logical \bem{and} compiled as a conditional expression).
1197
1198\end{itemize}
1199
1200\end{frame}
1201
1202
1203
1204\begin{frame}
1205
1206\frametitle{What comes next}
1207This work was completed in the first 7 months of the project.
1208The following 5 months have been spent:
1209
1210
1211\begin{itemize}
1212\item Enhancing and debugging the compiler.
1213
1214\item Extending the formal proofs on the toy compiler.
1215
1216\item Porting the compiler from $\mips$  to $\eighty$ (and teaching this).
1217
1218\item Integrating the {\sc Ocaml/Matita} description of $\eighty$.
1219
1220\end{itemize}
1221
1222This is covered  in the second part of the talk.
1223
1224\end{frame}
1225
1226\end{document}
1227
1228
Note: See TracBrowser for help on using the repository browser.