source: Deliverables/D5.1-5.3/report.tex @ 1690

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

up d5.1-5.3

File size: 28.8 KB
Line 
1
2\documentclass[11pt,epsf,a4wide]{article}
3\usepackage{../style/cerco}
4\usepackage{pdfpages}
5
6\usepackage{graphics}
7
8% For SLNCS comment above and use
9% \documentclass{llncs}
10
11
12
13
14
15\RequirePackage[latin1]{inputenc}     
16 
17% Mettre les différents packages et fonctions que l'on utilise
18\usepackage[english]{babel} 
19\usepackage{amsmath} 
20\usepackage{amsfonts} 
21\usepackage{amssymb} 
22\usepackage{xspace} 
23\usepackage{latexsym} 
24\usepackage{url} 
25\usepackage{xspace} 
26%\usepackage{fancyvrb}
27\usepackage[all]{xy} 
28%packages pour LNCS
29%\usepackage{semantic}
30%\usepackage{cmll}
31% Packages for RR
32\usepackage{graphics,color}             
33\RequirePackage[latin1]{inputenc}   
34\usepackage{array}
35 
36%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
37%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
38 
39\newenvironment{comment}{{\bf MORE WORK:}} 
40 
41\newenvironment{restate-proposition}[2][{}]{\noindent\textbf{Proposition~{#2}}\;\textbf{#1}\  
42}{\vskip 1em} 
43 
44\newenvironment{restate-theorem}[2][{}]{\noindent\textbf{Theorem~{#2}}\;\textbf{#1}\  
45}{\vskip 1em} 
46 
47\newenvironment{restate-corollary}[2][{}]{\noindent\textbf{Corollary~{#2}}\;\textbf{#1}\  
48}{\vskip 1em} 
49 
50\newcommand{\myparagraph}[1]{\medskip\noindent\textbf{#1}} 
51 
52\newcommand{\Proofitemb}[1]{\medskip \noindent {\bf #1\;}} 
53\newcommand{\Proofitemfb}[1]{\noindent {\bf #1\;}} 
54\newcommand{\Proofitem}[1]{\medskip \noindent $#1\;$} 
55\newcommand{\Proofitemf}[1]{\noindent $#1\;$} 
56\newcommand{\Defitem}[1]{\smallskip \noindent $#1\;$} 
57\newcommand{\Defitemt}[1]{\smallskip \noindent {\em #1\;}} 
58\newcommand{\Defitemf}[1]{\noindent $#1\;$} 
59 
60 
61%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
62%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
63 
64 
65 
66%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
67%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
68 
69\newcommand{\eqdef}{=_{\text{def}}} 
70\newcommand{\concat}{\cdot}%%{\mathbin{+}}
71\newcommand{\Int}{\mathit{int}} 
72\newcommand{\nat}{\mathit{nat}} 
73\newcommand{\String}{\mathit{string}} 
74\newcommand{\Ident}{\mathit{ident}} 
75\newcommand{\Block}{\mathit{block}} 
76\newcommand{\Signature}{\mathit{signature}} 
77 
78\newcommand{\pc}{\mathit{pc}} 
79\newcommand{\estack}{\mathit{estack}} 
80\newcommand{\Error}{\epsilon} 
81 
82%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
83%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
84 
85% --------------------------------------------------------------------- %
86% Proof rule.                                                           %
87% --------------------------------------------------------------------- %
88 
89\newcommand{\staterule}[3]{%
90  $\begin{array}{@{}l}%
91   \mbox{#1}\\%
92   \begin{array}{c}
93   #2\\ 
94   \hline 
95   \raisebox{0ex}[2.5ex]{\strut}#3%
96   \end{array}
97  \end{array}$} 
98 
99\newcommand{\GAP}{2ex} 
100 
101\newcommand{\recall}[2]{%
102 $\begin{array}{c}
103 #1\\ 
104 \hline 
105 \raisebox{0ex}[2.5ex]{\strut}#2%
106 \end{array}$} 
107 
108\newcommand{\hbra}{\noindent\hbox to \textwidth{\leaders\hrule height1.8mm depth-1.5mm\hfill}} 
109\newcommand{\hket}{\noindent\hbox to \textwidth{\leaders\hrule height0.3mm\hfill}} 
110\newcommand{\ratio}{.3} 
111 
112\newenvironment{display}[1]{\begin{tabbing} 
113  \hspace{1.5em} \= \hspace{\ratio\linewidth-1.5em} \= \hspace{1.5em} \= \kill 
114  \noindent\hbra\\[-.5em] 
115  {\ }\textsc{#1}\\[-.8ex] 
116  \hbox to \textwidth{\leaders\hrule height1.6mm depth-1.5mm\hfill}\\[-.8ex] 
117  }{\\[-.8ex]\hket 
118  \end{tabbing}} 
119 
120 
121\newcommand{\sbline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.2ex}\hfill\hspace*{0ex}}} 
122\newcommand{\sline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.1ex}\hfill\hspace*{0ex}}} 
123\newcommand{\sentry}[2]{\>$#1$\>\ \smash[t]{\vrule width 0.2mm height
124    1.2\baselineskip depth 1.5\baselineskip}\>#2} 
125 
126\newcommand{\entry}[2]{\>$#1$\>\>#2} 
127\newcommand{\clause}[2]{$#1$\>\>#2} 
128\newcommand{\category}[2]{\clause{#1::=}{#2}} 
129\newcommand{\subclause}[1]{\>\>\>#1} 
130\newcommand{\redrule}[3]{$#1$\>\>$#2$\>\>\>#3} 
131 
132%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
133%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
134 
135% environments
136
137% To be commented for LNCS
138 \newtheorem{theorem}{Theorem} 
139 \newtheorem{fact}[theorem]{Fact} 
140 \newtheorem{definition}[theorem]{Definition} 
141 \newtheorem{lemma}[theorem]{Lemma} 
142 \newtheorem{corollary}[theorem]{Corollary} 
143 \newtheorem{proposition}[theorem]{Proposition} 
144 \newtheorem{example}[theorem]{Example} 
145 \newtheorem{exercise}[theorem]{Exercise} 
146 \newtheorem{remark}[theorem]{Remark} 
147 \newtheorem{question}[theorem]{Question}
148 \newtheorem{proviso}[theorem]{Proviso} 
149  \newtheorem{conjecture}[theorem]{Conjecture}
150
151% proofs 
152 
153\newcommand{\Proof}{\noindent {\sc Proof}. } 
154\newcommand{\Proofhint}{\noindent {\sc Proof hint}. } 
155% To be commented for LNCS
156 \newcommand{\qed}{\hfill${\Box}$} 
157\newcommand{\EndProof}{\qed}
158 
159% figure environment
160 
161\newcommand{\Figbar}{{\center \rule{\hsize}{0.3mm}}}    %horizontal thiner line for figures
162\newenvironment{figureplr}{\begin{figure}[t] \Figbar}{\Figbar \end{figure}} 
163                                                        %environment for figures
164%       ************Macros for mathematical symbols*************
165% Style
166 
167\newcommand{\cl}[1]{{\cal #1}}          % \cl{R} to make R calligraphic
168\newcommand{\la}{\langle}               % the brackets for pairing (see also \pair)
169\newcommand{\ra}{\rangle} 
170 
171\newcommand{\lf}{\lfloor} 
172\newcommand{\rf}{\rfloor} 
173\newcommand{\ul}[1]{\underline{#1}}     % to underline
174\newcommand{\ol}[1]{\overline{#1}}      % to overline
175\newcommand{\ok}{~ok}                   % well formed context
176 
177% Syntax
178 
179\newcommand{\Gives}{\vdash}             % in a type judgment
180\newcommand{\IGives}{\vdash_{I}}        % intuitionistic provability
181\newcommand{\AIGives}{\vdash_{{\it AI}}} %affine-intuitionistic provability
182\newcommand{\CGives}{\vdash_{C}}        % affine-intuitionistic confluent provability
183
184
185\newcommand{\Models}{\mid \! =}              % models
186
187\newcommand{\emptycxt}{\On}              % empty context
188\newcommand{\subs}[2]{[#1 / #2]} 
189\newcommand{\sub}[2]{[#2 / #1]}         % substitution \sub{x}{U} gives [U/x]   
190\newcommand{\Sub}[3]{[#3 / #2]#1}       % Substitution with three arguments \Sub{V}{x}{U}
191
192\newcommand{\lsub}[2]{#2 / #1}          % substitution \lsub{x}{U} gives U/x, to be used in a list.
193 
194\newcommand{\impl}{\supset} 
195\newcommand{\arrow}{\rightarrow}        % right thin arrow
196\newcommand{\trarrow}{\stackrel{*}{\rightarrow}}        % trans closure
197%\newcommand{\limp}{\makebox[5mm]{\,$- \! {\circ}\,$}}   % linear
198                                % implication
199\newcommand{\limp}{\multimap} %linear implication
200\newcommand{\bang}{\, !} 
201% LNCS
202%\newcommand{\bang}{\oc}
203\newcommand{\limpe}[1]{\stackrel{#1}{\multimap}}
204\newcommand{\hyp}[3]{#1:(#2, #3)}
205\newcommand{\letm}[3]{{\sf let} \ ! #1 = #2 \ {\sf in} \ #3}    % modal let
206\newcommand{\lets}[3]{{\sf let} \ #1 = #2 \ {\sf in} \ #3}    % simple let
207\newcommand{\letp}[3]{{\sf let} \ \S #1 = #2 \ {\sf in} \ #3}    % paragraph let
208\newcommand{\tertype}{{\bf 1}}
209\newcommand{\behtype}{{\bf B}}
210\newcommand{\bt}[1]{{\it BT}(#1)}       % Boehm tree
211\newcommand{\cxt}[1]{#1[~]}             % Context with one hole
212\newcommand{\pr}{\parallel}             % parallel ||
213\newcommand{\Nat}{\mathbf{N}}                 % natural numbers
214\newcommand{\Natmax}{\mathbf{N}_{{\it max}}}  % natural numbers with minus infinity
215\newcommand{\Rat}{\mathbf{Q}^{+}}                 % non-negative rationals
216\newcommand{\Ratmax}{\mathbf{Q}^{+}_{{\it max}}}  % non-negative rationals with minus infinity
217\newcommand{\Alt}{ \mid\!\!\mid  } 
218\newcommand{\isum}{\oplus} 
219\newcommand{\csum}{\uplus}              %context sum
220\newcommand{\dpar}{\mid\!\mid} 
221                                        % for the production of a grammar containing \mid
222\newcommand{\infer}[2]{\begin{array}{c} #1 \\ \hline #2 \end{array}} 
223                                        % to make a centered inference rule
224 
225% (Meta-)Logic
226 
227\newcommand{\bool}{{\sf bool}}          % boolean values
228\newcommand{\Or}{\vee}                  % disjunction
229\newcommand{\OR}{\bigvee}               % big disjunction
230\newcommand{\AND}{\wedge}               % conjunction
231\newcommand{\ANDD}{\bigwedge}           % big conjunction
232\newcommand{\Arrow}{\Rightarrow}        % right double arrow
233\newcommand{\IFF}{\mbox{~~iff~~}}       % iff in roman and with spaces
234\newcommand{\iffArrow}{\Leftrightarrow} % logical equivalence
235 
236% Semantics
237 
238\newcommand{\dl}{[\![}                  % semantic [[
239\newcommand{\dr}{]\!]}                  % semantic ]]
240\newcommand{\lam}{{\bf \lambda}}        % semantic lambda
241
242
243% The equivalences for this paper
244
245% the usual ones
246\newcommand{\ubis}{\approx^u}          % usual labelled weak bis
247\newcommand{\uabis}{\approx^{u}_{ccs}} % usual labelled weak bis on CCS
248
249% the contextual conv sensitive
250\newcommand{\cbis}{\approx}        % convergence sensitive bis
251\newcommand{\cabis}{\approx_{ccs}}  % convergence sensitive bis on CCS
252
253% the labelled conv sensitive
254\newcommand{\lcbis}{\approx^{\ell}} %
255\newcommand{\lcabis}{\approx^{\ell}_{ccs}} % labelled convergence sensitive bis on CCS
256\newcommand{\lcbiswrong}{\approx^{\ell \Downarrow}} %
257
258
259
260
261
262
263
264\newcommand{\maytest}{=_{\Downarrow}}
265\newcommand{\musttest}{=_{\Downarrow_{S}}}
266
267
268 
269 
270% Sets
271 
272\newcommand{\prt}[1]{{\cal P}(#1)}      % Parts of a set
273\newcommand{\finprt}[1]{{\cal P}_{fin}(#1)}% Finite parts
274\newcommand{\finprtp}[1]{{\cal P}_{fin}^{+}(#1)}% Non-empty Finite parts
275\newcommand{\union}{\cup}               % union
276\newcommand{\inter}{\cap}               % intersection
277\newcommand{\Union}{\bigcup}            % big union
278\newcommand{\Inter}{\bigcap}            % big intersection
279\newcommand{\cpl}[1]{#1^{c}}            % complement
280\newcommand{\card}{\sharp}              % cardinality
281\newcommand{\minus}{\backslash}         % set difference
282\newcommand{\sequence}[2]{\{#1\}_{#2}}  % ex. \sequence{d_n}{n\in \omega}
283\newcommand{\comp}{\circ}               % functional composition
284%\newcommand{\oset}[1]{\{#1\}}            % set enumeration
285\newcommand{\mset}[1]{\{\! | #1 |\!\}}  % pseudo-set notation {| |}
286 
287% Domains
288 
289\newcommand{\two}{{\bf O}}              % Sierpinski space
290\newcommand{\join}{\vee}                % join
291\newcommand{\JOIN}{\bigvee}             % big join 
292\newcommand{\meet}{\wedge}              % meet
293\newcommand{\MEET}{\bigwedge}           % big meet
294\newcommand{\dcl}{\downarrow}           % down closure
295\newcommand{\ucl}{\uparrow}             % up closure
296\newcommand{\conv}{\downarrow}          % synt. conv. pred. (postfix)
297\newcommand{\diver}{\uparrow}           % diverging term
298\newcommand{\Conv}{\Downarrow}          % sem. conv. pred. (postfix)
299\newcommand{\SConv}{\Downarrow_{S}}          % sem. conv. pred. (postfix)
300\newcommand{\CConv}{\Downarrow_{C}}
301\newcommand{\Diver}{\Uparrow}           % diverging map
302\newcommand{\cpt}[1]{{\cal K}(#1)}      % compacts, write \cpt{D}
303\newcommand{\ret}{\triangleleft}        % retract
304\newcommand{\nor}{\succeq}
305\newcommand{\prj}{\underline{\ret}}     % projection
306\newcommand{\parrow}{\rightharpoonup}   % partial function space
307\newcommand{\ub}[1]{{\it UB}(#1)}       % upper bounds
308\newcommand{\mub}[1]{{\it MUB}(#1)}     % minimal upper bounds
309\newcommand{\lift}[1]{(#1)_{\bot}}      % lifting
310\newcommand{\forget}[1]{\underline{#1}} % forgetful translation
311
312%\newcommand{\rel}[1]{\;{\cal #1}\;}     % infix relation (calligraphic)
313\newcommand{\rl}[1]{\;{\cal #1}\;}             % infix relation
314\newcommand{\rel}[1]{{\cal #1}}         %calligraphic relation with no
315                                        %extra space
316\newcommand{\per}[1]{\;#1 \;} 
317\newcommand{\wddagger}{\natural}  % weak suspension
318%\newcommand{\wddagger}{=\!\!\!\!\parallel}  % weak suspension
319% Categories
320 
321\newcommand{\pair}[2]{\langle #1 , #2 \rangle} % pairing \pair{x}{y}, do not use < >.
322 
323%               *******  Notation for the $\pi$-calculus *********
324% Syntax:
325 
326 
327\newcommand{\fn}[1]{{\it fn}(#1)}                       % free names
328\newcommand{\bn}[1]{{\it bn}(#1)}                       % bound names
329\newcommand{\names}[1]{{\it n}(#1)}                     % names
330\newcommand{\true}{{\sf t}}                             % true
331\newcommand{\false}{{\sf f}}                            % false
332\newcommand{\pio}{\pi_1}                                % 1 receptor calculus
333\newcommand{\pioo}{\pi_{1}^{r}} 
334\newcommand{\piom}{\pi_{1}^{-}}                         % 1 receptor calculus wo match
335\newcommand{\pioi}{\pi_{1I}}                    % 1 receptor I-calculus
336\newcommand{\pifo}{\pi_{\w{1f}}}                                % functional calculus
337\newcommand{\pilo}{\pi_{\w{1l}}}                                % located calculus
338\newcommand{\sort}[1]{{\it st}(#1)}                     % sort
339\newcommand{\ia}[1]{{\it ia}(#1)}                     % sort
340\newcommand{\ite}[3]{{\sf if~} #1 {\sf ~then~} #2 {\sf ~else~} #3}      %if then else
341\newcommand{\casep}[2]{{\sf case}^{\times}(#1, \pair{x}{y}\Arrow#2)}      %case on pairs
342\newcommand{\casel}[3]{{\sf case}^{L}(#1, #2, \s{cons}(x,y)\Arrow#3)}      %case on lists
343\newcommand{\caseb}[3]{{\sf case}^{b}(#1, #2, \s{cons}(x,y)\Arrow#3)}      %case on lists
344\newcommand{\nil}{{\sf nil}} 
345\newcommand{\cons}{{\sf cons}} 
346\newcommand{\idle}[1]{{\it Idle}(#1)}                   %idle process
347\newcommand{\conf}[1]{\{ #1 \}}                         %configuration
348\newcommand{\link}[2]{#1 \mapsto #2}                    %likn a ->b
349\newcommand{\mand}{\mbox{ and }} 
350\newcommand{\dvec}[1]{\tilde{{\bf #1}}}                 %double vector
351\newcommand{\erloc}[1]{{\it er}_{l}(#1)}                % location erasure
352\newcommand{\w}[1]{{\it #1}}    %To write in math style
353\newcommand{\vcb}[1]{{\bf #1}} 
354\newcommand{\lc}{\langle\!|} 
355\newcommand{\rc}{|\!\rangle} 
356\newcommand{\obj}[1]{{\it obj}(#1)} 
357\newcommand{\move}[1]{{\sf move}(#1)} 
358\newcommand{\qqs}[2]{\forall\, #1\;\: #2} 
359\newcommand{\qtype}[4]{\forall #1 :  #2 . (#4,#3)} 
360\newcommand{\xst}[2]{\exists\, #1\;\: #2} 
361\newcommand{\xstu}[2]{\exists\, ! #1\;\: #2} 
362\newcommand{\dpt}{\,:\,} 
363\newcommand{\cond}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3} 
364\newcommand{\s}[1]{{\sf #1}}    % sans-serif 
365\newcommand{\vc}[1]{{\bf #1}} 
366\newcommand{\lnorm}{\lbrack\!\lbrack} 
367\newcommand{\rnorm}{\rbrack\!\rbrack} 
368\newcommand{\sem}[1]{\underline{#1}} 
369\newcommand{\tra}[1]{\langle #1 \rangle}
370\newcommand{\trb}[1]{[ #1 ]}
371\newcommand{\squn}{\mathop{\scriptstyle\sqcup}} 
372\newcommand{\lcro}{\langle\!|} 
373\newcommand{\rcro}{|\!\rangle} 
374\newcommand{\semi}[1]{\lcro #1\rcro} 
375\newcommand{\sell}{\,\ell\,} 
376\newcommand{\SDZ}[1]{\marginpar{\textbf{SDZ:} {#1}}} 
377 
378\newcommand{\when}[3]{{\sf when}~#1~{\sf then}~#2~{\sf else}~#3} 
379\newcommand{\wthen}[2]{{\sf when}~#1~{\sf then}~#2~} 
380\newcommand{\welse}[1]{{\sf else}~#1} 
381
382%Pour la fleche double, il faut rajouter :
383%      \usepackage{mathtools}
384
385\newcommand{\act}[1]{\xrightarrow{#1}} %labelled actionlow %high
386
387\newcommand{\lact}[1]{\stackrel{#1}{\makebox[5mm]{\,$- \! {\circ}\,$}}}
388
389\newcommand{\set}[1]{\{#1\}}
390\newcommand{\pst}[2]{{\sf pset}(#1,#2)}
391\newcommand{\st}[2]{{\sf set}(#1,#2)}
392\newcommand{\wrt}[2]{{\sf w}(#1,#2)}
393
394\newcommand{\chtype}[2]{{\it Ch_{#1}(#2)}}
395\newcommand{\rgtype}[2]{{\it {\sf Reg}_{#1} #2}}
396
397\newcommand{\get}[1]{{\sf get}(#1)}
398
399%\newcommand{\wact}[1]{\xRightarrow{#1}} %weak labelled action low high
400
401%\newcommand{\mact}[1]{\xrightarrow{#1}_{m}} %labelled action low %high
402
403%\newcommand{\wmact}[1]{\xRightarrow{#1}_{m}} %weak labelled action low high
404
405%\newcommand{\act}[1]{\stackrel{#1}{\rightarrow}} %labelled action low
406                                %%%high
407
408\newcommand{\acteq}[1]{\stackrel{#1}{\leadsto}} %labelled action low
409                                %%%high
410
411
412%\newcommand{\actI}[1]{\stackrel{#1}{\rightarrow_{1}}} %labelled action low
413\newcommand{\actI}[1]{\xrightarrow{#1}_{1}}
414
415%\newcommand{\actII}[1]{\stackrel{#1}{\rightarrow_{2}}} %labelled action low
416\newcommand{\actII}[1]{\xrightarrow{#1}_{2}}
417
418
419 \newcommand{\wact}[1]{\stackrel{#1}{\Rightarrow}} %weak labelled action low high
420\newcommand{\wactI}[1]{\stackrel{#1}{\Rightarrow_{1}}} %weak labelled action low high
421\newcommand{\wactII}[1]{\stackrel{#1}{\Rightarrow_{2}}} %weak labelled action low high
422
423
424\newcommand{\mact}[1]{\stackrel{#1}{\rightarrow_{m}}} %labelled action low %high
425\newcommand{\wmact}[1]{\stackrel{#1}{\Rightarrow_{m}}} %weak labelled action low high
426 
427%\newcommand{\lact}[1]{\stackrel{#1}{\leftarrow}}
428\newcommand{\lwact}[1]{\stackrel{#1}{\Leftarrow}} 
429 
430 
431 
432\newcommand{\eval}{\Downarrow} 
433\newcommand{\Eval}[1]{\Downarrow^{#1}} 
434 
435 
436\newcommand{\Z}{{\bf Z}} 
437\newcommand{\Real}{\mathbb{R}^{+}} 
438\newcommand{\Return}{\ensuremath{\mathtt{return}}\xspace}                 
439\newcommand{\Stop}{\ensuremath{\mathtt{stop}}\xspace} 
440\newcommand{\Wait}{\ensuremath{\mathtt{wait}}\xspace} 
441\newcommand{\Read}{\ensuremath{\mathtt{read}}\xspace} 
442\newcommand{\Write}{\ensuremath{\mathtt{write}}\xspace} 
443\newcommand{\Yield}{\ensuremath{\mathtt{yield}}\xspace} 
444\newcommand{\Next}{\ensuremath{\mathtt{next}}\xspace} 
445\newcommand{\Load}{\ensuremath{\mathtt{load}}\xspace} 
446\newcommand{\Call}{\ensuremath{\mathtt{call}}\xspace} 
447\newcommand{\Tcall}{\ensuremath{\mathtt{tcall}}\xspace} 
448\newcommand{\Pop}{\ensuremath{\mathtt{pop}}\xspace} 
449\newcommand{\Build}{\ensuremath{\mathtt{build}}\xspace} 
450\newcommand{\Branch}{\ensuremath{\mathtt{branch}}\xspace} 
451\newcommand{\Goto}{\ensuremath{\mathtt{goto}}\xspace} 
452 
453\newcommand{\hatt}[1]{#1^{+}} 
454\newcommand{\Of}{\mathbin{\w{of}}} 
455 
456\newcommand{\susp}{\downarrow} 
457\newcommand{\lsusp}{\Downarrow_L} 
458\newcommand{\wsusp}{\Downarrow} 
459\newcommand{\commits}{\searrow} 
460 
461 
462\newcommand{\spi}{S\pi} 
463 
464
465 \newcommand{\pres}[2]{#1\triangleright #2} %TCCS else next (alternative)
466% \newcommand{\pres}[2]{ \lfloor #1 \rfloor (#2)}  %TCCS else next
467\newcommand{\present}[3]{{\sf present} \ #1 \ {\sf do } \ #2 \ {\sf  else} \ #3}
468
469
470\newcommand{\tick}{{\sf tick}}          %tick action
471
472 
473 
474\newcommand{\sbis}{\equiv_L} 
475\newcommand{\emit}[2]{\ol{#1}#2} 
476%\newcommand{\present}[4]{#1(#2).#3,#4}
477\newcommand{\match}[4]{[#1=#2]#3,#4}       %pi-equality
478
479\newcommand{\matchv}[4]{[#1 \unrhd #2]#3,#4}
480
481\newcommand{\new}[2]{\nu #1 \ #2} 
482\newcommand{\outact}[3]{\new{{\bf #1}}{\emit{#2}{#3}}} 
483\newcommand{\real}{\makebox[5mm]{\,$\|\!-$}}% realizability relation
484
485\newcommand{\regterm}[2]{{\sf reg}_{#1} #2}
486\newcommand{\thread}[1]{{\sf thread} \ #1}
487\newcommand{\store}[2]{(#1 \leftarrow #2)}
488\newcommand{\pstore}[2]{(#1 \Leftarrow #2)}
489
490\newcommand{\regtype}[2]{{\sf Reg}_{#1} #2}
491\newcommand{\uregtype}[3]{{\sf Reg}_{#1}(#2, #3)}
492\newcommand{\urtype}[2]{{\sf Reg}(#1, #2)}
493
494\newcommand{\upair}[2]{[#1,#2]}
495\newcommand{\letb}[3]{\mathsf{let}\;\oc #1 = #2\;\mathsf{in}\;#3}
496
497\newcommand{\vlt}[1]{{\cal V}(#1)}
498\newcommand{\prs}[1]{{\cal P}(#1)}
499
500\newcommand{\imp}{{\sf Imp}}            %imp language
501\newcommand{\vm}{{\sf Vm}}              %virtual machine language
502\newcommand{\mips}{{\sf Mips}}          %Mips language
503\newcommand{\C}{{\sf C}}                % C language
504\newcommand{\Clight}{{\sf Clight}}        %C light language
505\newcommand{\Cminor}{{\sf Cminor}}
506\newcommand{\RTLAbs}{{\sf RTLAbs}}
507\newcommand{\RTL}{{\sf RTL}}
508\newcommand{\ERTL}{{\sf ERTL}}
509\newcommand{\LTL}{{\sf LTL}}
510\newcommand{\LIN}{{\sf LIN}}
511\newcommand{\access}[1]{\stackrel{#1}{\leadsto}}
512\newcommand{\ocaml}{{\sf ocaml}}
513\newcommand{\coq}{{\sf Coq}}
514\newcommand{\compcert}{{\sf CompCert}}
515%\newcommand{\cerco}{{\sf CerCo}}
516\newcommand{\cost}{{\sf Cost}}
517\newcommand{\lamcost}{\sf LamCost}
518\newcommand{\cil}{{\sf CIL}}
519\newcommand{\scade}{{\sf Scade}}
520\newcommand{\absint}{{\sf AbsInt}}
521\newcommand{\framac}{{\sf Frama-C}}
522\newcommand{\powerpc}{{\sf PowerPc}}
523\newcommand{\lustre}{{\sf Lustre}}
524\newcommand{\esterel}{{\sf Esterel}}
525\newcommand{\ml}{{\sf ML}}
526
527\newcommand{\codeex}[1]{\texttt{#1}}   % code example
528
529\bibliographystyle{abbrv} 
530
531\title{
532INFORMATION AND COMMUNICATION TECHNOLOGIES\\
533(ICT)\\
534PROGRAMME\\
535\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
536
537\date{ }
538\author{}
539
540\begin{document}
541\thispagestyle{empty}
542
543\vspace*{-1cm}
544\begin{center}
545\includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
546\end{center}
547
548\begin{minipage}{\textwidth}
549\maketitle
550\end{minipage}
551
552
553\vspace*{0.5cm}
554\begin{center}
555\begin{LARGE}
556\bf
557Report \\
558D5.1 Untrusted CerCo Prototype \\
559and \\
560D5.3 Case study: analysis of synchronous code
561\\
562\end{LARGE} 
563\end{center}
564
565\vspace*{2cm}
566\begin{center}
567\begin{large}
568Version 1.0
569\end{large}
570\end{center}
571
572\vspace*{0.5cm}
573\begin{center}
574\begin{large}
575Main Authors:\\
576Roberto M.~Amadio, Nicolas~Ayache, Yann~R\'egis-Gianas, Paolo Tranquilli
577\end{large}
578\end{center}
579
580\vspace*{\fill}
581\noindent
582Project Acronym: \cerco{}\\
583Project full title: Certified Complexity\\
584Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
585
586\clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
587
588\newpage
589
590
591\vspace*{7cm}
592
593\paragraph{Summary}
594The deliverable D5.1-D5.3 is composed of the following parts:
595
596\begin{enumerate}
597
598\item This summary.
599
600\item The paper \cite{A12} and the related software $\cost$.
601
602\item The paper \cite{T12} and the related software.
603
604\item The paper \cite{ARG11} and the related software $\lamcost$.
605
606\item The paper \cite{MA11}.
607
608\end{enumerate}
609
610This document and the softwares above can be downloaded at the
611page:
612\begin{center}
613{\tt http://cerco.cs.unibo.it/}
614\end{center}
615
616{\scriptsize
617\begin{thebibliography}{99}
618
619
620\bibitem{A12}
621N.~Ayache.
622\newblock Synthesis of certified cost bounds.
623\newblock Universit\'e Paris Diderot. Internal report documenting the $\cost$ software, 2012.
624
625
626\bibitem{ARG11}
627R.M.~Amadio, Y.~R\'egis-Gianas.
628\newblock Certifying and reasoning on cost annotations of functional programs.
629\newblock In Proc. FOPARA, Springer LNCS (to appear), 2012.
630\newblock Also Research Report, Universit\'e Paris Diderot,
631{\tt http://hal.inria.fr/inria-00629473/en/}, 2011.
632
633
634\bibitem{MA11}
635A.~Madet, R.M.~Amadio.
636\newblock An Elementary Affine $\lambda$-Calculus with Multithreading and Side Effects.
637\newblock In Proc. TLCA, Springer LNCS 6690:138-152, 2011.
638\newblock Also Research Report, Universit\'e Paris Diderot,
639{\tt http://hal.archives-ouvertes.fr/hal-00569095/fr/}, 2011.
640
641\bibitem{T12}
642P.~Tranquilli.
643\newblock Indexed labels for loop iteration dependent costs.
644\newblock Universit\`a di Bologna. Internal report documenting the indexed labels software, 2012.
645
646\end{thebibliography}}
647
648\newpage
649
650\paragraph{Aim}
651The main aim of WP5 is to develop proof of concept prototypes where
652the (untrusted) compiler implemented in WP2 is interfaced with existing tools
653in order to synthesize complexity  assertions on the execution
654time of programs. Eventually, the approach should be adapted to
655the trusted compiler developed in WP3 and WP4 (cf. deliverable D5.2 at
656month 36).
657
658
659\paragraph{Synthesis of certified cost bounds}
660The main planned contribution of deliverable D5.1 is a tool that takes
661as input an annotated $\C$ program produced by the $\cerco$ compiler
662and tries to synthesize a certified bound on the execution time of the
663program.  The related expected contribution of deliverable D5.3
664amounts to apply the developed tool to the $\C$ programs generated by
665a $\lustre$ compiler.  This work is described in the first document
666\cite{A12} which accompanies a software distribution called $\cost$.
667The development takes the form of a `$\framac$ plug-in'.  $\framac$ is
668an open source and well-established platform to reason formally on
669$\C$ programs. The proof obligations generated from Hoare style
670assertions on $\C$ programs are passed to a small number of provers
671that try to discharge them automatically. The platform has been
672designed to be extensible by means of so called plug-in's written in
673$\ocaml$.  The $\cost$ software is a $\framac$ plug-in which in first
674approximation takes the following actions: (1) it receives as input a
675$\C$ program, (2) it applies the $\cerco$ compiler to produce a
676related $\C$ program with cost annotations, (3) it applies some
677heuristics to produce a tentative bound on the cost of executing a
678$\C$ function as a function of the value of its parameters, (4) it
679calls the provers embedded in the $\framac$ tool to discharge the
680related proof obligations.  The current size of the $\cost$ plug-in is
6814K lines of $\ocaml$ code.  More details are available in the first
682part of the document \cite{A12}.  The second part of the document
683(formally, corresponding to deliverable D5.3) tries to delimit the
684practical applicability of the plug-in. To this end, the tool has been
685applied to the $\C$ code generated by the $\lustre$ compiler and to
686some other simple $\C$ programs.
687
688We pause to recall a redistribution of the workforce of the UPD site.
689Following the resignation of the doctoral student at the end of year
6901, the contract of the post-doc has been extended till month 33.
691It follows that in the UPD site there has been a shift of manpower
692from the third to the second year. Because of this shift we decided to
693anticipate the presentation of deliverable D5.3 at month 24 rather
694than month 36. Besides this contingent reason, it is clear that the
695development of the synthesis tool must go hand in hand with its
696experimentation on larger and larger classes of programs.  The UPD
697post-doc is expected to continue work on D5.1 and D5.3 till the end of
698its contract.
699
700
701\paragraph{Indexed labels for loop iteration dependent costs}
702The first year scientific review report, among other things, contrasts
703the $\cerco$ approach with the one adopted in tools such as $\absint$
704which are used by the WCET community and it recommends that the
705approach to cost annotations described in WP2 is made {\em coarser},
706{\em i.e.}, that a label covers a larger portion of code.  During the
707second year, most of the work of a post-doc at UNIBO was aimed at
708addressing this remark \cite{T12}.  This has resulted in a refinement
709of the labelling approach into a so called {\em indexed labelling}.
710It consists in formally indexing cost labels with the iterations of
711the containing loops they occur in within the source code.  These
712indexes can be transformed during the compilation, and when lifted
713back to source code they produce dependent costs. Preliminary
714experiments suggest that this refinement allows to retain preciseness
715when the program is subject to loop transformations such as loop
716peeling and loop unrolling.  A prototype implementation has been
717developed on top of the untrusted $\cerco$ compiler D2.2.
718
719
720% so as to take into account the effects of
721%% cache memories and pipelines. Following this suggestion
722%% a post-doc at UB has worked on these issues and we have invited
723%% C. Ferdinand to present the AbsInt tool.
724%% (*** Lack of compositionality --- timing anomalies --- ***)
725
726
727
728\paragraph{Certifying and reasoning on cost annotations of functional programs}
729During the second year some unplanned work related to deliverables
730D5.1 and D5.3 has taken place at UPD.  The main development
731\cite{ARG11} concerns the extension of the $\cerco$ labelling approach
732described in D2.1 to a standard compilation chain from a higher-order
733functional language of the $\ml$ family to $\C$.  This
734work shows that the approach is sufficiently general to be applied to
735higher-order programs whose concrete complexity is generally regarded
736as difficult to estimate.  Moreover, the introduction of
737higher-order functions calls for a higher-order logic to reason on the
738cost annotations.  In this respect, we have built on previous work by
739one of the authors on a higher-order Hoare logic. Starting from a
740(higher-order) specification of the expected cost of a function our
741tool $\lamcost$ produces automatically a list of proof obligations. Preliminary
742experiments suggest that a large part of these proof obligations can
743be discharged automatically and that the remaining ones can be proved
744in a proof assistant such as $\coq$.  Ongoing work that should be
745completed within the third year of the project is extending the
746compilation chain and the cost analysis to include garbage collection
747using a {\em region based} memory management \`a la Tofte-Talpin.
748
749\paragraph{An Elementary Affine $\lambda$-Calculus with Multithreading and Side Effects.}
750A second development at UPD is of a more speculative nature and is
751concerned with the design of a type system for a functional language
752with side effects that guarantees complexity bounds. As far as we
753know, this is the first work that accounts for side effects. The
754obtained result concerns {\em elementary time} and ongoing work that
755should be completed within the third year of the project concerns a
756similar result for {\em polynomial time}.  We regard this work as a
757step towards bridging the $\cerco$ approach with the work on {\em
758  Implicit computational complexity} (ICC) in which our universities
759are also involved (in 2011, the $\cerco$ project organised in Paris a
760joint workshop with an ICC oriented project).  As a matter of fact,
761there is still a large gap to be filled before the results in ICC can
762have an impact on the practice of programming.
763
764
765
766
767
768\newpage
769
770\includepdf[pages={-}]{plugin.pdf}
771
772
773\newpage
774
775\includepdf[pages={-}]{tranquilli.pdf}
776
777\newpage
778
779
780\includepdf[pages={-}]{fopara.pdf}
781
782
783\newpage
784
785\includepdf[pages={-}]{tlca.pdf}
786
787
788\end{document}
Note: See TracBrowser for help on using the repository browser.