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

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

wp2 revised

File size: 37.0 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\begin{description}
515
516\item[Task 2.1] Architectural design ($\Arrow$ D2.1)
517
518\item[Task 2.2] Intermediate languages and data structures ($\Arrow$ D2.1)
519
520\item[Task 2.3] Implementation ($\Arrow$ D2.2)
521
522\item[Task 2.4] Integration validation and testing (terminates at T0+18, no deliverable)
523\end{description}
524
525\begin{description}
526
527\item[D2.1] Compiler design and Intermediate languages (T0+6).
528
529\item[D2.2] Untrusted cost-annotating $\ocaml$ compiler (T0+12).
530
531\end{description}
532{\small \Red{\NB} This first part is an {\bf introduction} to Tasks 2.1 and 2.2. The
533second part will give more details on Task 2.2, discuss Task 2.3 (with demo),
534and  provide some perspectives on Task 2.4 and WP5.}
535
536\end{frame}
537
538
539\begin{frame}
540
541\frametitle{People involved at UPD site}
542
543
544{\small
545\begin{tabular}{|c|c|c|}
546
547\hline
548{\bf Name}           &{\bf Status} &{\bf Rough Allocated Time} \\\hline
549Roberto \textsc{Amadio} &Professor &1 day/week \\
550Yann \textsc{R\'egis-Gianas} &Assistant Professor &1 day/week \\
551Nicolas \textsc{Ayache}      &Post-doc      &full time, 11 months \\
552Ronan \textsc{Saillard}      &Internship+PhD &full time, 8 months \\
553Kayvan \textsc{Memarian}     &Internship   &1.5 days/week, 4 months \\ \hline
554\end{tabular}}
555
556
557~\\~\\
558\Red{{\bf NB}} Internships are very important: dissemination, speed up development,
559explore side paths, preliminary training towards research (PhD),$\ldots$
560
561\end{frame}
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576\begin{frame}
577
578\frametitle{Motivation}
579Resource analysis of programming models should, if we are serious about it,
580eventually have an impact on programming practice. Limiting factors include:
581
582\begin{itemize}
583
584\item Bounds are {\bf asymptotic} and sometimes a bit {\bf shaky} (exotic compilers):  we need an effort to make them concrete and reliable.
585
586\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.
587
588\item Implicit complexity programming languages are a straight jacket: {\bf restrictions} are often complex and too difficult to program with.
589
590\end{itemize}
591
592\end{frame}
593
594
595\begin{frame}
596
597\frametitle{$\cerco$ goals and approach}
598
599\begin{itemize}
600
601\item Bound and certify the {\bf number of cycles} that it takes to run a
602given  piece of code on a given processor with a given compiler.
603
604\item Target {\bf $\C$ programs}, and in particular the kind of $\C$ 
605programs produced for embedded applications
606(such as those generated by the $\scade$ compiler).
607
608\item {\bf Reflect the cost information} obtained at the machine level
609back into the $\C$ source code.
610
611\item {\bf Extract synthetic bounds} by reasoning on
612the annotated $\C$  programs (for which several general purpose tools now exist).
613
614\end{itemize}
615
616\Red{\NB} Technically, this can be seen as a refinement of ongoing work on {\bf compiler certification}   
617(see, e.g., $\compcert$ project).
618
619\end{frame}
620
621
622
623\begin{frame}
624
625\frametitle{Current technology and our challenge}
626\begin{itemize}
627
628
629\item Compilation phases are heavily {\bf inspected and tested} 
630but not formally checked with a proof assistant.
631\[
632\lustre \arrow \C \arrow \textsc{binary~ code}
633\]
634\item Binary code must be {\bf annotated} with (uncertified)
635information on the number of iterations of loops.
636
637\item Tools such as \textsc{AbsInt} perform WCET analysis of
638{\bf sequences of instructions of binary code}.
639
640\end{itemize}
641
642\noindent \Red{{\bf Our challenge}}
643Lift in a {\em certified way} whathever information we have on the execution
644cost of the binary code to an information on the $\C$ source code (a kind
645of {\bf decompilation}).
646
647\end{frame}
648
649
650
651\begin{frame}
652
653\frametitle{A potential connection}
654Could use this work as a {\bf platform} to experiment with
655\Blu{{\em implicit complexity programming languages}}.
656
657{\small
658\begin{enumerate}
659
660\item Write a program in your preferred implicit complexity programming language.
661\item Compile it to $\C$.
662\item $\cerco$ compiles $\C$ to machine code and provides precise and certified information on execution time of $\C$ code.
663\item Use your implicit complexity analysis to produce automatically a synthetic bound on the resources used by the program.
664\item If you want to push this further, try to lift the assertions about the $\C$ code to assertions on your source program.
665\end{enumerate}}
666\end{frame}
667
668
669
670
671\begin{frame}
672
673\frametitle{Is this really possible?}
674
675\begin{itemize}
676
677\item 
678What are the  annotations, and how are we going to actually
679prove that they are correct? \\
680$\Arrow$ We need a {\bf proof methodology}.~\\~\\
681
682\item 
683Is it possible to produce annotations of the source code
684that predict soundly and precisely the execution cost?\\
685$\Arrow$ We need to {\bf show that the approach scales}.
686
687\end{itemize}
688
689\end{frame}
690
691
692
693
694\begin{frame}
695
696\frametitle{Preliminary ideas}
697
698\begin{itemize}
699
700\item 
701A cost annotation is an {\bf instrumentation} of the source program
702that keeps track of the execution cost of the program.
703
704\item 
705The computed cost should be {\bf correct} and possibly {\bf precise} 
706relatively to the compiled code.
707
708\item 
709Starting from the annotated source program apply standard tools
710to reason about $\C$ programs in order to {\bf extract synthetic bounds}.
711
712\end{itemize}
713
714\end{frame}
715
716
717
718
719\begin{frame}
720
721\frametitle{A small size case study (direct approach 1/3)}
722
723{\footnotesize
724\[
725\begin{array}{ccccc}
726
727      &\cl{C}   &                          &\cl{C'}              \\
728
729\imp   &\arrow        &\vm                &\arrow       &\mips        \\
730
731\ \quad\downarrow \w{An}_{\imp}
732&
733&\ \quad\downarrow \w{An}_{\vm}
734&
735&\ \quad\downarrow \w{An}_{\mips} \\
736
737\imp   &             &\vm             & &\mips        \\
738
739\end{array}
740\]}
741\begin{itemize}
742
743\item $\imp$: an imperative language with while loops.
744
745\item $\vm$: a virtual machine with a stack.
746
747\item $\mips$: an assembly like language with registers and RAM memory.
748
749\item $\cl{C}$: relies on the stack to evaluate numerical expressions.
750
751\item $\cl{C'}$: statically allocates the base of the stack in the registers and the
752rest in RAM memory. This requires a `stack height' analysis of the $\vm$ code.
753
754\item $\w{An}_{\mips}$: counts the number of $\mips$ instructions executed.
755
756\end{itemize}
757
758\end{frame}
759
760
761\begin{frame}
762\frametitle{A small size case study (direct approach 2/3)}
763{\footnotesize
764\[
765\begin{array}{ccccc}
766
767      &\cl{C}   &                          &\cl{C'}              \\
768
769\imp   &\arrow        &\vm                &\arrow       &\mips        \\
770
771\ \quad\downarrow \w{An}_{\imp}
772&
773&\ \quad\downarrow \w{An}_{\vm}
774&
775&\ \quad\downarrow \w{An}_{\mips} \\
776
777\imp   &             &\vm             & &\mips        \\
778
779\end{array}
780\]}
781
782\begin{itemize}
783
784
785\item The annotation functions instrument the
786code so that it {\bf monitors its execution cost} by incrementing
787a (fresh) \w{cost} variable.
788
789\item In particular, the annotation function of the object code
790$\w{An}_{\mips}$ is a  {\bf compelling definition} of the execution cost.
791
792\end{itemize}
793\end{frame}
794
795
796\begin{frame}
797
798\frametitle{A small size case study (direct approach 3/3)}
799
800{\footnotesize
801\[
802\begin{array}{ccccc}
803
804      &\cl{C}   &                          &\cl{C'}              \\
805
806\imp   &\arrow        &\vm                &\arrow       &\mips        \\
807
808\ \quad\downarrow \w{An}_{\imp}
809&
810&\ \quad\downarrow \w{An}_{\vm}
811&
812&\ \quad\downarrow \w{An}_{\mips} \\
813
814\imp   &             &\vm             & &\mips        \\
815
816\end{array}
817\]}
818
819\begin{itemize}
820\item The annotation function at step $i$ is {\bf correct} with
821respect to the one at step $i+1$ of the compilation
822if
823
824{\small
825\[
826\begin{array}{lc}
827\mbox{`Predicted' cost} &(\w{An}_{i}(S),s[0/\w{cost}])\eval s'[c/\w{cost}]\\\hline
828\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
829\end{array}
830\]}
831
832\item Further it is {\bf precise} if \ $c\leq d+\kappa(S)$.
833
834\end{itemize}
835
836\end{frame}
837
838\begin{frame}
839
840\frametitle{Problems with the direct approach}
841K. \textsc{Memarian} formalized this in \textsc{Coq} 
842(500 lines of specification and 2400 lines of proofs).
843
844\begin{itemize}
845
846\item Proofs have to manipulate {\bf numerical values}.
847
848\item Proofs about the bounds are {\bf intertwined} 
849with those of functional correctness and get much larger
850(factor $7$ in the experiment).
851
852\item To be precise we need to explicit a lot of {\bf contextual information}
853which is at odd with proof compositionality.
854
855\end{itemize}
856
857\end{frame}
858
859
860\begin{frame}
861
862\frametitle{Second attempt: labelling approach (1/7)}
863{\footnotesize
864\[
865\begin{array}{ccccc}
866
867
868\imp      &                              &                          &                & \\
869
870\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
871
872\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
873
874\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
875&
876&\ \quad\downarrow \w{er}_{\vm}
877&
878&\ \quad\downarrow \w{er}_{\mips} \\ 
879
880\imp   &\arrow             &\vm             &\arrow &\mips        \\
881      &\cl{C}   &                          &\cl{C'}              \\
882\end{array}
883\]}
884
885\begin{description}
886
887\item[Labelled languages] All languages are enriched with \bem{labelled instructions} generating \bem{labelled transitions}.
888
889\item[Erasures] The \bem{erasure functions} are just functions that remove all labelling instructions.
890
891\end{description}
892
893\end{frame}
894
895
896
897\begin{frame}
898
899\frametitle{Labelling approach  (2/7)}
900{\footnotesize
901\[
902\begin{array}{ccccc}
903
904
905\imp      &                              &                          &                & \\
906
907\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
908
909\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
910
911\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
912&
913&\ \quad\downarrow \w{er}_{\vm}
914&
915&\ \quad\downarrow \w{er}_{\mips} \\ 
916
917\imp   &\arrow             &\vm             &\arrow &\mips        \\
918      &\cl{C}   &                          &\cl{C'}              \\
919\end{array}
920\]}
921
922\begin{description}
923
924
925
926\item[Extended compilation] The compilation functions are \bem{extended} to the labelled languages.
927
928\item[Commutation] Compilation and erasure functions \bem{commute}:
929\[
930\w{er}_{\vm} \comp \cl{C} = \cl{C} \comp \w{er}_{\imp} \qquad
931\w{er}_{\mips} \comp \cl{C'} = \cl{C'} \comp \w{er}_{\vm}
932\]
933
934\end{description}
935\end{frame}
936
937
938
939\begin{frame}
940
941\frametitle{Labelling approach (3/7)}
942{\footnotesize
943\[
944\begin{array}{ccccc}
945
946
947\imp      &                              &                          &                & \\
948
949\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
950
951\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
952
953\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
954&
955&\ \quad\downarrow \w{er}_{\vm}
956&
957&\ \quad\downarrow \w{er}_{\mips} \\ 
958
959\imp   &\arrow             &\vm             &\arrow &\mips        \\
960      &\cl{C}   &                          &\cl{C'}              \\
961\end{array}
962\]}
963
964{\small
965\begin{description}
966
967\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}$.
968
969\item[Instrumentation]
970Given a \bem{`cost function'} associating costs to labels,
971an \bem{instrumentation} of the source language is a
972function $\cl{I}_{\imp}$  replacing  labels with suitable increments
973of a fresh \bem{cost variable}.
974
975\item[Annotation]
976 An \bem{annotation} of the source language is defined as:
977\[
978\w{An}_{\imp} = \cl{I}_{\imp}\comp \cl{L}~.
979\]
980
981\end{description}}
982
983\end{frame}
984
985\begin{frame}
986
987\frametitle{Labelling approach (4/7)}
988{\footnotesize
989\[
990\begin{array}{ccccc}
991
992
993\imp      &                              &                          &                & \\
994
995\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
996
997\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
998
999\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
1000&
1001&\ \quad\downarrow \w{er}_{\vm}
1002&
1003&\ \quad\downarrow \w{er}_{\mips} \\ 
1004
1005\imp   &\arrow             &\vm             &\arrow &\mips        \\
1006      &\cl{C}   &                          &\cl{C'}              \\
1007\end{array}
1008\]}
1009
1010\begin{description}
1011
1012\item[Simulation]
1013The simulation properties of the compilation functions are {\em lifted} to the labelled languages.
1014%With a proper design of the labelled languages this just means taking into account the rules that
1015%generate labelled transitions. 
1016Let $\lambda$ denote a sequence of labels. Then:% we have:
1017\end{description}
1018\[
1019(S,s)\eval (s',\lambda)  \quad \Arrow \quad 
1020(\cl{C}(S),s) \eval (s',\lambda) \quad \Arrow \quad
1021(\cl{C'}(\cl{C}(S)),s) \eval (s',\lambda)
1022\]
1023
1024\end{frame}
1025
1026
1027\begin{frame}
1028
1029
1030\frametitle{Labelling approach (5/7)}
1031{\footnotesize
1032\[
1033\begin{array}{ccccc}
1034
1035
1036\imp      &                              &                          &                & \\
1037
1038\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
1039
1040\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
1041
1042\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
1043&
1044&\ \quad\downarrow \w{er}_{\vm}
1045&
1046&\ \quad\downarrow \w{er}_{\mips} \\ 
1047
1048\imp   &\arrow             &\vm             &\arrow &\mips        \\
1049      &\cl{C}   &                          &\cl{C'}             
1050\end{array}
1051\]}
1052
1053\begin{description}
1054
1055\item[Numerical vs. Symbolic cost] By {\bf diagram chasing} we derive:
1056\[
1057\infer{(\w{An}(S),s[c/\w{cost}])  \eval s'[c+\delta/\w{cost}]}
1058{(\cl{C'}(\cl{C}(\cl{L}(S))),s[c/\w{cost}])  \eval (s'[c/\w{cost}],\lambda)}
1059\]
1060where $\delta$ is the numerical (additive) cost associated with $\lambda$.
1061
1062\end{description}
1063
1064\end{frame}
1065
1066
1067
1068\begin{frame}
1069
1070\frametitle{Labelling approach (6/7)}
1071{\footnotesize
1072\[
1073\begin{array}{ccccc}
1074
1075
1076\imp      &                              &                          &                & \\
1077
1078\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
1079
1080\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
1081
1082\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
1083&
1084&\ \quad\downarrow \w{er}_{\vm}
1085&
1086&\ \quad\downarrow \w{er}_{\mips} \\ 
1087
1088\imp   &\arrow             &\vm             &\arrow &\mips        \\
1089      &\cl{C}   &                          &\cl{C'}              \\
1090\end{array}
1091\]}
1092
1093\begin{description}
1094
1095\item[When is the labelling $\cl{L}$ interesting?]
1096I.e., knowing that
1097\[
1098\cl{C'}(\cl{C}(S)) = \w{er}_{\mips}(\cl{C'}(\cl{C}(\cl{L}(S)))
1099\]
1100{\bf under which conditions} can we conclude that $\lambda$, {\em i.e.},
1101$\delta$, is a sound and  possibly precise description of the real execution cost?
1102\end{description}
1103\end{frame}
1104
1105
1106\begin{frame}
1107
1108\frametitle{Labelling approach (7/7)}
1109Conditions to be checked on the labelled binary code.
1110
1111{\small
1112\begin{itemize}
1113
1114\item Assume a sound over-approximation of
1115the {\bf control flow} of the labelled object code
1116$(\cl{C'}(\cl{C}(L(S))$.
1117This is a directed, rooted graph where some nodes are labelled.
1118
1119\item The labelling is {\bf sound} if in the CFG
1120all nodes are reachable from a labelled node and
1121all loops go through a labelled node.
1122
1123\item In this case, the {\bf cost of a label} $\ell$ is the cost
1124of the most expensive path in the control flow graph starting
1125from a node labelled $\ell$
1126and, crossing unlabelled nodes, arriving at a labelled one
1127or an unlabelled one without
1128successors (call such paths {\bf simple}).
1129
1130\item A sound labelling is {\bf precise} if for all labels $\ell$ the
1131paths of the kind
1132described above starting from a node labelled $\ell$ have the same cost.
1133
1134
1135\end{itemize}}
1136
1137\end{frame}
1138
1139\begin{frame}
1140
1141\frametitle{Advantages of the labelling approach}
1142
1143\begin{itemize}
1144
1145\item  Costs are handled {\bf symbolically} 
1146as labels are propagated by the compiler.
1147
1148\item  Proofs of {\bf functional correctness stay simple} 
1149(just one additional case to cover the labels)
1150
1151\item  {\bf No need to explicit the contextual information}.
1152The numerical cost is computed only at the assembly language level
1153and then it is reflected back to the source.
1154
1155\end{itemize}
1156
1157\end{frame}
1158
1159
1160\begin{frame}
1161
1162\frametitle{A larger experiment: a $\C$ to $\mips$ compiler}
1163{\footnotesize
1164\[
1165\begin{array}{cccccccccc}
1166&&\C &\arrow &\Clight &\arrow &\Cminor &\arrow &\RTLAbs &\qquad \mbox{(front end)}\\
1167                                              &&&&&&&&\downarrow \\
1168 \mips &\leftarrow &\LIN &\leftarrow  &\LTL &\leftarrow  &\ERTL  &\leftarrow &\RTL &\qquad \mbox{(back-end)}
1169\end{array}
1170\]
1171}
1172
1173{\small
1174\begin{itemize}
1175
1176\item Moderate optimisations: register allocation, dead-code elimination,$\ldots$ (a bit more efficient than {\tt gcc0}).
1177
1178\item Roughly, we implement the labelling approach on top of a compiler quite
1179close to $\compcert$.
1180
1181\item Around 10K lines of $\ocaml$ code. No proofs, just code inspection and test. We used the software  in a master level compilation course.
1182
1183\end{itemize}}
1184
1185\end{frame}
1186
1187
1188\begin{frame}
1189
1190\frametitle{Observed soundness and precision for the $C$ compiler}
1191As a rule of thumb,  we lose {\bf soundness} if we miss loops in the generated  code.
1192We lose {\bf precision} if we miss branching in the generated code.
1193
1194\begin{itemize}
1195
1196\item The first situation never arises in the considered compilation chain.
1197
1198\item The second situation can be handled by some pre-processing of the $\C$ code
1199(e.g., logical \bem{and} compiled as a conditional expression).
1200
1201\end{itemize}
1202
1203\end{frame}
1204
1205
1206
1207\begin{frame}
1208
1209\frametitle{What comes next}
1210This work was completed in the first 7 months of the project.
1211The following 5 months have been spent:
1212
1213
1214\begin{itemize}
1215\item Enhancing and debugging the compiler.
1216
1217\item Extending the formal proofs on the toy compiler.
1218
1219\item Porting the compiler from $\mips$  to $\eighty$ (and teaching this).
1220
1221\item Integrating the {\sc Ocaml/Matita} description of $\eighty$.
1222
1223\end{itemize}
1224
1225This is covered  in the second part of the talk.
1226
1227\end{frame}
1228
1229\end{document}
1230
1231
Note: See TracBrowser for help on using the repository browser.