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

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

added draft first part presentation WP2

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