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

Last change on this file since 3267 was 2558, checked in by amadio, 8 years ago

r

File size: 29.6 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{\ilcost}{{\sf IndLabCost}}
519\newcommand{\ilacc}{{\sf IndLabAcc}}
520\newcommand{\cil}{{\sf CIL}}
521\newcommand{\scade}{{\sf Scade}}
522\newcommand{\absint}{{\sf AbsInt}}
523\newcommand{\framac}{{\sf Frama-C}}
524\newcommand{\powerpc}{{\sf PowerPc}}
525\newcommand{\lustre}{{\sf Lustre}}
526\newcommand{\esterel}{{\sf Esterel}}
527\newcommand{\ml}{{\sf ML}}
528
529\newcommand{\codeex}[1]{\texttt{#1}}   % code example
530
531\bibliographystyle{abbrv} 
532
533\title{
534INFORMATION AND COMMUNICATION TECHNOLOGIES\\
535(ICT)\\
536PROGRAMME\\
537\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
538
539\date{ }
540\author{}
541
542\begin{document}
543\thispagestyle{empty}
544
545\vspace*{-1cm}
546\begin{center}
547\includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
548\end{center}
549
550\begin{minipage}{\textwidth}
551\maketitle
552\end{minipage}
553
554
555\vspace*{0.5cm}
556\begin{center}
557\begin{LARGE}
558\bf
559Report \\
560D5.1 Untrusted CerCo Prototype \\
561and \\
562D5.3 Case study: analysis of synchronous code
563\\
564\end{LARGE} 
565\end{center}
566
567\vspace*{2cm}
568\begin{center}
569\begin{large}
570Version 1.0
571\end{large}
572\end{center}
573
574\vspace*{0.5cm}
575\begin{center}
576\begin{large}
577Main Authors:\\
578Roberto M.~Amadio, Nicolas~Ayache, Yann~R\'egis-Gianas, Paolo Tranquilli
579\end{large}
580\end{center}
581
582\vspace*{\fill}
583\noindent
584Project Acronym: \cerco{}\\
585Project full title: Certified Complexity\\
586Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
587
588\clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
589
590\newpage
591
592
593\vspace*{7cm}
594
595\paragraph{Summary}
596The deliverable D5.1-D5.3 is composed of the following parts:
597
598\begin{enumerate}
599
600\item This summary.
601
602\item The paper \cite{A12} and the related software $\cost$.
603
604\item The paper \cite{T12} and the related prototype compiler \ilacc{} (and its \cost{} branch, \ilcost{}).
605
606\item The paper \cite{ARG11} and the related software $\lamcost$.
607
608\item The paper \cite{MA11}.
609
610\end{enumerate}
611
612This document and the softwares mentioned above can be downloaded at the
613page:
614\begin{center}
615{\tt http://cerco.cs.unibo.it/}
616\end{center}
617
618{\scriptsize
619\begin{thebibliography}{99}
620
621
622\bibitem{A12}
623N.~Ayache.
624\newblock Synthesis of certified cost bounds.
625\newblock Universit\'e Paris Diderot. Internal report documenting the $\cost$ software, 2012.
626
627
628\bibitem{ARG11}
629R.M.~Amadio, Y.~R\'egis-Gianas.
630\newblock Certifying and reasoning on cost annotations of functional programs.
631\newblock In Proc. FOPARA, Springer LNCS (to appear), 2012.
632\newblock Also Research Report, Universit\'e Paris Diderot,
633{\tt http://hal.inria.fr/inria-00629473/en/}, 2011.
634
635
636\bibitem{MA11}
637A.~Madet, R.M.~Amadio.
638\newblock An Elementary Affine $\lambda$-Calculus with Multithreading and Side Effects.
639\newblock In Proc. TLCA, Springer LNCS 6690:138-152, 2011.
640\newblock Also Research Report, Universit\'e Paris Diderot,
641{\tt http://hal.archives-ouvertes.fr/hal-00569095/fr/}, 2011.
642
643\bibitem{T12}
644P.~Tranquilli.
645\newblock Indexed labels for loop iteration dependent costs.
646\newblock Universit\`a di Bologna. Internal report documenting the indexed labels software, 2012.
647
648\end{thebibliography}}
649
650\newpage
651
652\paragraph{Aim}
653The main aim of WP5 is to develop proof of concept prototypes where
654the (untrusted) compiler implemented in WP2 is interfaced with existing tools
655in order to synthesize complexity  assertions on the execution
656time of programs. Eventually, the approach should be adapted to
657the trusted compiler developed in WP3 and WP4 (cf. deliverable D5.2 at
658month 36).
659
660The main planned contribution of deliverable D5.1 is a
661tool that takes as input an annotated C program produced by the CerCo
662compiler and tries to synthesize a certified bound on the execution
663time of the program.  The related expected contribution of deliverable
664D5.3 amounts to apply the tool described in D5.1 to the C programs generated
665by a Lustre compiler.  This planned work is described in the first
666document...which accompanies a software distribution...
667Frama-C plug-in ...more examples...
668
669\paragraph{Synthesis of certified cost bounds}
670The main planned contribution of deliverable D5.1 is a tool that takes
671as input an annotated $\C$ program produced by the $\cerco$ compiler
672and tries to synthesize a certified bound on the execution time of the
673program.  The related expected contribution of deliverable D5.3
674amounts to apply the developed tool to the $\C$ programs generated by
675a $\lustre$ compiler.  This work is described in the first document
676\cite{A12} which accompanies a software distribution called $\cost$.
677The development takes the form of a `$\framac$ plug-in'.  $\framac$ is
678an open source and well-established platform to reason formally on
679$\C$ programs. The proof obligations generated from Hoare style
680assertions on $\C$ programs are passed to a small number of provers
681that try to discharge them automatically. The platform has been
682designed to be extensible by means of so called plug-in's written in
683$\ocaml$.  The $\cost$ software is a $\framac$ plug-in which in first
684approximation takes the following actions: (1) it receives as input a
685$\C$ program, (2) it applies the $\cerco$ compiler to produce a
686related $\C$ program with cost annotations, (3) it applies some
687heuristics to produce a tentative bound on the cost of executing a
688$\C$ function as a function of the value of its parameters, (4) it
689calls the provers embedded in the $\framac$ tool to discharge the
690related proof obligations.  The current size of the $\cost$ plug-in is
6914K lines of $\ocaml$ code.  More details are available in the first
692part of the document \cite{A12}.  The second part of the document
693(formally, corresponding to deliverable D5.3) tries to delimit the
694practical applicability of the plug-in. To this end, the tool has been
695applied to the $\C$ code generated by the $\lustre$ compiler and to
696some other simple $\C$ programs.
697
698We pause to recall a redistribution of the workforce of the UPD site.
699Following the resignation of the doctoral student at the end of year
7001, the contract of the post-doc which expired at month 13
701has been as extended till month 33. 
702It follows that in the UPD site there has been a shift of manpower from
703the third to the second year. Because of this shift we
704anticipate the presentation of deliverable D5.3 at month 24 rather
705than month 36.
706
707
708\paragraph{Indexed labels for loop iteration dependent costs}
709The first year scientific review report, among other things, contrasts
710the $\cerco$ approach with the one adopted in tools such as $\absint$
711which are used by the WCET community and it recommends that the
712approach to cost annotations described in WP2 is made {\em coarser},
713{\em i.e.}, that a label covers a larger portion of code.  During the
714second year, most of the work of a post-doc at UNIBO was aimed at
715addressing this remark \cite{T12}.  This has resulted in a refinement
716of the labelling approach into a so called {\em indexed labelling}.
717It consists in formally indexing cost labels with the iterations of
718the containing loops they occur in within the source code.  These
719indexes can be transformed during the compilation, and when lifted
720back to source code they produce dependent costs. Preliminary
721experiments suggest that this refinement allows to retain preciseness
722when the program is subject to loop transformations such as loop
723peeling and loop unrolling.  A prototype implementation has been
724developed on top of the untrusted $\cerco$ compiler D2.2.
725
726
727% so as to take into account the effects of
728%% cache memories and pipelines. Following this suggestion
729%% a post-doc at UB has worked on these issues and we have invited
730%% C. Ferdinand to present the AbsInt tool.
731%% (*** Lack of compositionality --- timing anomalies --- ***)
732
733
734
735\paragraph{Certifying and reasoning on cost annotations of functional programs}
736During the second year some unplanned work related to deliverables
737D5.1 and D5.3 has taken place at UPD.  The main development
738\cite{ARG11} concerns the extension of the $\cerco$ labelling approach
739described in D2.1 to a standard compilation chain from a higher-order
740functional language of the $\ml$ family to $\C$.  This
741work shows that the approach is sufficiently general to be applied to
742higher-order programs whose concrete complexity is generally regarded
743as difficult to estimate.  Moreover, the introduction of
744higher-order functions calls for a higher-order logic to reason on the
745cost annotations.  In this respect, we have built on previous work by
746one of the authors on a higher-order Hoare logic. Starting from a
747(higher-order) specification of the expected cost of a function our
748tool $\lamcost$ produces automatically a list of proof obligations. Preliminary
749experiments suggest that a large part of these proof obligations can
750be discharged automatically and that the remaining ones can be proved
751in a proof assistant such as $\coq$.  Ongoing work that should be
752completed within the third year of the project is extending the
753compilation chain and the cost analysis to include garbage collection
754using a {\em region based} memory management \`a la Tofte-Talpin.
755
756\paragraph{An Elementary Affine $\lambda$-Calculus with Multithreading and Side Effects.}
757A second development at UPD is of a more speculative nature and is
758concerned with the design of a type system for a functional language
759with side effects that guarantees complexity bounds \cite{MA11}. As far as we
760know, this is the first work that accounts for side effects. The
761obtained result concerns {\em elementary time} and ongoing work that
762should be completed within the third year of the project concerns a
763similar result for {\em polynomial time}.  We regard this work as a
764step towards bridging the $\cerco$ approach with the work on {\em
765  Implicit computational complexity} (ICC) in which our universities
766are also involved (in 2011, the $\cerco$ project organised in Paris a
767joint workshop with an ICC oriented project).  As a matter of fact,
768there is still a large gap to be filled before the results in ICC can
769have an impact on the practice of programming.
770
771A second development is of a more speculative nature and
772concerned with the development of a type system
773for a functional langauge with side effects that guarantees a complexity
774bound... First work to account for side effects... Ongoing work tries to
775extend the framework to polynomial time. Eventually we hope to join
776the thread on implicit complexity...???
777
778
779
780\newpage
781
782\includepdf[pages={-}]{plugin.pdf}
783
784
785\newpage
786
787\includepdf[pages={-}]{tranquilli.pdf}
788
789\newpage
790
791
792\includepdf[pages={-}]{fopara.pdf}
793
794
795\newpage
796
797\includepdf[pages={-}]{tlca.pdf}
798
799
800\end{document}
Note: See TracBrowser for help on using the repository browser.