source: Deliverables/addenda/indexed_labels/report.tex @ 1674

Last change on this file since 1674 was 1674, checked in by tranquil, 8 years ago

corrected some faults
still TODO: running example, language corrections

File size: 66.7 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}}
42\;\textbf{#1}\  
43}{\vskip 1em} 
44 
45\newenvironment{restate-theorem}[2][{}]{\noindent\textbf{Theorem~{#2}}\;\textbf{
46#1}\  
47}{\vskip 1em} 
48 
49\newenvironment{restate-corollary}[2][{}]{\noindent\textbf{Corollary~{#2}}
50\;\textbf{#1}\  
51}{\vskip 1em} 
52 
53\newcommand{\myparagraph}[1]{\medskip\noindent\textbf{#1}} 
54 
55\newcommand{\Proofitemb}[1]{\medskip \noindent {\bf #1\;}} 
56\newcommand{\Proofitemfb}[1]{\noindent {\bf #1\;}} 
57\newcommand{\Proofitem}[1]{\medskip \noindent $#1\;$} 
58\newcommand{\Proofitemf}[1]{\noindent $#1\;$} 
59\newcommand{\Defitem}[1]{\smallskip \noindent $#1\;$} 
60\newcommand{\Defitemt}[1]{\smallskip \noindent {\em #1\;}} 
61\newcommand{\Defitemf}[1]{\noindent $#1\;$} 
62 
63 
64%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
65%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
66 
67 
68 
69%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
70%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
71 
72\newcommand{\eqdef}{=_{\text{def}}} 
73\newcommand{\concat}{\cdot}%%{\mathbin{+}}
74\newcommand{\Int}{\mathit{int}} 
75\newcommand{\nat}{\mathit{nat}} 
76\newcommand{\String}{\mathit{string}} 
77\newcommand{\Ident}{\mathit{ident}} 
78\newcommand{\Block}{\mathit{block}} 
79\newcommand{\Signature}{\mathit{signature}} 
80 
81\newcommand{\pc}{\mathit{pc}} 
82\newcommand{\estack}{\mathit{estack}} 
83\newcommand{\Error}{\epsilon} 
84 
85%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
86%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
87 
88% --------------------------------------------------------------------- %
89% Proof rule.                                                           %
90% --------------------------------------------------------------------- %
91 
92\newcommand{\staterule}[3]{%
93  $\begin{array}{@{}l}%
94   \mbox{#1}\\%
95   \begin{array}{c}
96   #2\\ 
97   \hline 
98   \raisebox{0ex}[2.5ex]{\strut}#3%
99   \end{array}
100  \end{array}$} 
101 
102\newcommand{\GAP}{2ex} 
103 
104\newcommand{\recall}[2]{%
105 $\begin{array}{c}
106 #1\\ 
107 \hline 
108 \raisebox{0ex}[2.5ex]{\strut}#2%
109 \end{array}$} 
110 
111\newcommand{\hbra}{\noindent\hbox to \textwidth{\leaders\hrule height1.8mm
112depth-1.5mm\hfill}} 
113\newcommand{\hket}{\noindent\hbox to \textwidth{\leaders\hrule
114height0.3mm\hfill}} 
115\newcommand{\ratio}{.3} 
116 
117\newenvironment{display}[1]{\begin{tabbing} 
118  \hspace{1.5em} \= \hspace{\ratio\linewidth-1.5em} \= \hspace{1.5em} \= \kill 
119  \noindent\hbra\\[-.5em] 
120  {\ }\textsc{#1}\\[-.8ex] 
121  \hbox to \textwidth{\leaders\hrule height1.6mm depth-1.5mm\hfill}\\[-.8ex] 
122  }{\\[-.8ex]\hket 
123  \end{tabbing}} 
124 
125 
126\newcommand{\sbline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.2ex}
127\hfill\hspace*{0ex}}} 
128\newcommand{\sline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.1ex}
129\hfill\hspace*{0ex}}} 
130\newcommand{\sentry}[2]{\>$#1$\>\ \smash[t]{\vrule width 0.2mm height
131    1.2\baselineskip depth 1.5\baselineskip}\>#2} 
132 
133\newcommand{\entry}[2]{\>$#1$\>\>#2} 
134\newcommand{\clause}[2]{$#1$\>\>#2} 
135\newcommand{\category}[2]{\clause{#1::=}{#2}} 
136\newcommand{\subclause}[1]{\>\>\>#1} 
137\newcommand{\redrule}[3]{$#1$\>\>$#2$\>\>\>#3} 
138 
139%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
140%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
141 
142% environments
143
144% To be commented for LNCS
145 \newtheorem{theorem}{Theorem} 
146 \newtheorem{fact}[theorem]{Fact} 
147 \newtheorem{definition}[theorem]{Definition} 
148 \newtheorem{lemma}[theorem]{Lemma} 
149 \newtheorem{corollary}[theorem]{Corollary} 
150 \newtheorem{proposition}[theorem]{Proposition} 
151 \newtheorem{example}[theorem]{Example} 
152 \newtheorem{exercise}[theorem]{Exercise} 
153 \newtheorem{remark}[theorem]{Remark} 
154 \newtheorem{question}[theorem]{Question}
155 \newtheorem{proviso}[theorem]{Proviso} 
156  \newtheorem{conjecture}[theorem]{Conjecture}
157
158% proofs 
159 
160\newcommand{\Proof}{\noindent {\sc Proof}. } 
161\newcommand{\Proofhint}{\noindent {\sc Proof hint}. } 
162% To be commented for LNCS
163 \newcommand{\qed}{\hfill${\Box}$} 
164\newcommand{\EndProof}{\qed}
165 
166% figure environment
167 
168\newcommand{\Figbar}{{\center \rule{\hsize}{0.3mm}}}
169 %horizontal thiner line for figures
170\newenvironment{figureplr}[1][t]{\begin{figure}[#1] \Figbar}{\Figbar \end{figure}}
171%environment for figures
172%       ************Macros for mathematical symbols*************
173% Style
174 
175\newcommand{\cl}[1]{{\cal #1}}          % \cl{R} to make R calligraphic
176\newcommand{\la}{\langle}               % the brackets for pairing (see also \pair)
177\newcommand{\ra}{\rangle} 
178 
179\newcommand{\lf}{\lfloor} 
180\newcommand{\rf}{\rfloor} 
181\newcommand{\ul}[1]{\underline{#1}}     % to underline
182\newcommand{\ol}[1]{\overline{#1}}      % to overline
183\newcommand{\ok}{~ok}                   % well formed context
184 
185% Syntax
186 
187\newcommand{\Gives}{\vdash}             % in a type judgment
188\newcommand{\IGives}{\vdash_{I}}        % intuitionistic provability
189\newcommand{\AIGives}{\vdash_{{\it AI}}} %affine-intuitionistic provability
190\newcommand{\CGives}{\vdash_{C}}        % affine-intuitionistic confluent provability
191
192
193\newcommand{\Models}{\mid \! =}              % models
194
195\newcommand{\emptycxt}{\On}              % empty context
196\newcommand{\subs}[2]{[#1 / #2]} 
197\newcommand{\sub}[2]{[#2 / #1]}         % substitution \sub{x}{U} gives [U/x]
198 
199\newcommand{\Sub}[3]{[#3 / #2]#1}       % Substitution with three arguments \Sub{V}{x}{U}
200
201\newcommand{\lsub}[2]{#2 / #1}          % substitution \lsub{x}{U} gives U/x, to  be used in a list.
202 
203\newcommand{\impl}{\supset} 
204\newcommand{\arrow}{\rightarrow}        % right thin arrow
205\newcommand{\trarrow}{\stackrel{*}{\rightarrow}}        % trans closure
206%\newcommand{\limp}{\makebox[5mm]{\,$- \! {\circ}\,$}}   % linear
207                                % implication
208\newcommand{\limp}{\multimap} %linear implication
209\newcommand{\bang}{\, !} 
210% LNCS
211%\newcommand{\bang}{\oc}
212\newcommand{\limpe}[1]{\stackrel{#1}{\multimap}}
213\newcommand{\hyp}[3]{#1:(#2, #3)}
214\newcommand{\letm}[3]{{\sf let} \ ! #1 = #2 \ {\sf in} \ #3}    % modal let
215\newcommand{\lets}[3]{{\sf let} \ #1 = #2 \ {\sf in} \ #3}    % simple let
216\newcommand{\letp}[3]{{\sf let} \ \S #1 = #2 \ {\sf in} \ #3}    % paragraph let
217\newcommand{\tertype}{{\bf 1}}
218\newcommand{\behtype}{{\bf B}}
219\newcommand{\bt}[1]{{\it BT}(#1)}       % Boehm tree
220\newcommand{\cxt}[1]{#1[~]}             % Context with one hole
221\newcommand{\pr}{\parallel}             % parallel ||
222\newcommand{\Nat}{\mathbf{N}}                 % natural numbers
223\newcommand{\Natmax}{\mathbf{N}_{{\it max}}}  % natural numbers with minus infinity
224\newcommand{\Rat}{\mathbf{Q}^{+}}                 % non-negative rationals
225\newcommand{\Ratmax}{\mathbf{Q}^{+}_{{\it max}}}  % non-negative rationals with minus infinity
226\newcommand{\Alt}{ \mid\!\!\mid  } 
227\newcommand{\isum}{\oplus} 
228\newcommand{\csum}{\uplus}              %context sum
229\newcommand{\dpar}{\mid\!\mid} 
230                                        % for the production of a grammar containing \mid
231\newcommand{\infer}[2]{\begin{array}{c} #1 \\ \hline #2 \end{array}} 
232                                        % to make a centered inference rule
233 
234% (Meta-)Logic
235 
236\newcommand{\bool}{{\sf bool}}          % boolean values
237\newcommand{\Or}{\vee}                  % disjunction
238\newcommand{\OR}{\bigvee}               % big disjunction
239\newcommand{\AND}{\wedge}               % conjunction
240\newcommand{\ANDD}{\bigwedge}           % big conjunction
241\newcommand{\Arrow}{\Rightarrow}        % right double arrow
242\newcommand{\IFF}{\mbox{~~iff~~}}       % iff in roman and with spaces
243\newcommand{\iffArrow}{\Leftrightarrow} % logical equivalence
244 
245% Semantics
246 
247\newcommand{\dl}{[\![}                  % semantic [[
248\newcommand{\dr}{]\!]}                  % semantic ]]
249\newcommand{\lam}{{\bf \lambda}}        % semantic lambda
250
251
252% The equivalences for this paper
253
254% the usual ones
255\newcommand{\ubis}{\approx^u}          % usual labelled weak bis
256\newcommand{\uabis}{\approx^{u}_{ccs}} % usual labelled weak bis on CCS
257
258% the contextual conv sensitive
259\newcommand{\cbis}{\approx}        % convergence sensitive bis
260\newcommand{\cabis}{\approx_{ccs}}  % convergence sensitive bis on CCS
261
262% the labelled conv sensitive
263\newcommand{\lcbis}{\approx^{\ell}} %
264\newcommand{\lcabis}{\approx^{\ell}_{ccs}} % labelled convergence sensitive bis on CCS
265\newcommand{\lcbiswrong}{\approx^{\ell \Downarrow}} %
266
267
268
269
270
271
272
273\newcommand{\maytest}{=_{\Downarrow}}
274\newcommand{\musttest}{=_{\Downarrow_{S}}}
275
276
277 
278 
279% Sets
280 
281\newcommand{\prt}[1]{{\cal P}(#1)}      % Parts of a set
282\newcommand{\finprt}[1]{{\cal P}_{fin}(#1)}% Finite parts
283\newcommand{\finprtp}[1]{{\cal P}_{fin}^{+}(#1)}% Non-empty Finite parts
284\newcommand{\union}{\cup}               % union
285\newcommand{\inter}{\cap}               % intersection
286\newcommand{\Union}{\bigcup}            % big union
287\newcommand{\Inter}{\bigcap}            % big intersection
288\newcommand{\cpl}[1]{#1^{c}}            % complement
289\newcommand{\card}{\sharp}              % cardinality
290\newcommand{\minus}{\backslash}         % set difference
291\newcommand{\sequence}[2]{\{#1\}_{#2}}  % ex. \sequence{d_n}{n\in \omega}
292\newcommand{\comp}{\circ}               % functional composition
293%\newcommand{\oset}[1]{\{#1\}}            % set enumeration
294\newcommand{\mset}[1]{\{\! | #1 |\!\}}  % pseudo-set notation {| |}
295 
296% Domains
297 
298\newcommand{\two}{{\bf O}}              % Sierpinski space
299\newcommand{\join}{\vee}                % join
300\newcommand{\JOIN}{\bigvee}             % big join 
301\newcommand{\meet}{\wedge}              % meet
302\newcommand{\MEET}{\bigwedge}           % big meet
303\newcommand{\dcl}{\downarrow}           % down closure
304\newcommand{\ucl}{\uparrow}             % up closure
305\newcommand{\conv}{\downarrow}          % synt. conv. pred. (postfix)
306\newcommand{\diver}{\uparrow}           % diverging term
307\newcommand{\Conv}{\Downarrow}          % sem. conv. pred. (postfix)
308\newcommand{\SConv}{\Downarrow_{S}}          % sem. conv. pred. (postfix)
309\newcommand{\CConv}{\Downarrow_{C}}
310\newcommand{\Diver}{\Uparrow}           % diverging map
311\newcommand{\cpt}[1]{{\cal K}(#1)}      % compacts, write \cpt{D}
312\newcommand{\ret}{\triangleleft}        % retract
313\newcommand{\nor}{\succeq}
314\newcommand{\prj}{\underline{\ret}}     % projection
315\newcommand{\parrow}{\rightharpoonup}   % partial function space
316\newcommand{\ub}[1]{{\it UB}(#1)}       % upper bounds
317\newcommand{\mub}[1]{{\it MUB}(#1)}     % minimal upper bounds
318\newcommand{\lift}[1]{(#1)_{\bot}}      % lifting
319\newcommand{\forget}[1]{\underline{#1}} % forgetful translation
320
321%\newcommand{\rel}[1]{\;{\cal #1}\;}     % infix relation (calligraphic)
322\newcommand{\rl}[1]{\;{\cal #1}\;}             % infix relation
323\newcommand{\rel}[1]{{\cal #1}}         %calligraphic relation with no
324                                        %extra space
325\newcommand{\per}[1]{\;#1 \;} 
326\newcommand{\wddagger}{\natural}  % weak suspension
327%\newcommand{\wddagger}{=\!\!\!\!\parallel}  % weak suspension
328% Categories
329 
330\newcommand{\pair}[2]{\langle #1 , #2 \rangle} % pairing \pair{x}{y}, do not use < >.
331 
332%               *******  Notation for the $\pi$-calculus *********
333% Syntax:
334 
335 
336\newcommand{\fn}[1]{{\it fn}(#1)}                       % free names
337\newcommand{\bn}[1]{{\it bn}(#1)}                       % bound names
338\newcommand{\names}[1]{{\it n}(#1)}                     % names
339\newcommand{\true}{{\sf t}}                             % true
340\newcommand{\false}{{\sf f}}                            % false
341\newcommand{\pio}{\pi_1}                                % 1 receptor calculus
342\newcommand{\pioo}{\pi_{1}^{r}} 
343\newcommand{\piom}{\pi_{1}^{-}}                         % 1 receptor calculus wo match
344\newcommand{\pioi}{\pi_{1I}}                    % 1 receptor I-calculus
345\newcommand{\pifo}{\pi_{\w{1f}}}                                % functional calculus
346\newcommand{\pilo}{\pi_{\w{1l}}}                                % located calculus
347\newcommand{\sort}[1]{{\it st}(#1)}                     % sort
348\newcommand{\ia}[1]{{\it ia}(#1)}                     % sort
349\newcommand{\ite}[3]{{\sf if~} #1 {\sf ~then~} #2 {\sf ~else~} #3}      %if then else
350\newcommand{\casep}[2]{{\sf case}^{\times}(#1, \pair{x}{y}\Arrow#2)}      %case on pairs
351\newcommand{\casel}[3]{{\sf case}^{L}(#1, #2, \s{cons}(x,y)\Arrow#3)}      %case on lists
352\newcommand{\caseb}[3]{{\sf case}^{b}(#1, #2, \s{cons}(x,y)\Arrow#3)}      %case on lists
353\newcommand{\nil}{{\sf nil}} 
354\newcommand{\cons}{{\sf cons}} 
355\newcommand{\idle}[1]{{\it Idle}(#1)}                   %idle process
356\newcommand{\conf}[1]{\{ #1 \}}                         %configuration
357\newcommand{\link}[2]{#1 \mapsto #2}                    %likn a ->b
358\newcommand{\mand}{\mbox{ and }} 
359\newcommand{\dvec}[1]{\tilde{{\bf #1}}}                 %double vector
360\newcommand{\erloc}[1]{{\it er}_{l}(#1)}                % location erasure
361\newcommand{\w}[1]{{\it #1}}    %To write in math style
362\newcommand{\vcb}[1]{{\bf #1}} 
363\newcommand{\lc}{\langle\!|} 
364\newcommand{\rc}{|\!\rangle} 
365\newcommand{\obj}[1]{{\it obj}(#1)} 
366\newcommand{\move}[1]{{\sf move}(#1)} 
367\newcommand{\qqs}[2]{\forall\, #1\;\: #2} 
368\newcommand{\qtype}[4]{\forall #1 :  #2 . (#4,#3)} 
369\newcommand{\xst}[2]{\exists\, #1\;\: #2} 
370\newcommand{\xstu}[2]{\exists\, ! #1\;\: #2} 
371\newcommand{\dpt}{\,:\,} 
372\newcommand{\cond}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3} 
373\newcommand{\s}[1]{{\sf #1}}    % sans-serif 
374\newcommand{\vc}[1]{{\bf #1}} 
375\newcommand{\lnorm}{\lbrack\!\lbrack} 
376\newcommand{\rnorm}{\rbrack\!\rbrack} 
377\newcommand{\sem}[1]{\underline{#1}} 
378\newcommand{\tra}[1]{\langle #1 \rangle}
379\newcommand{\trb}[1]{[ #1 ]}
380\newcommand{\squn}{\mathop{\scriptstyle\sqcup}} 
381\newcommand{\lcro}{\langle\!|} 
382\newcommand{\rcro}{|\!\rangle} 
383\newcommand{\semi}[1]{\lcro #1\rcro} 
384\newcommand{\sell}{\,\ell\,} 
385\newcommand{\SDZ}[1]{\marginpar{\textbf{SDZ:} {#1}}} 
386 
387\newcommand{\when}[3]{{\sf when}~#1~{\sf then}~#2~{\sf else}~#3} 
388\newcommand{\wthen}[2]{{\sf when}~#1~{\sf then}~#2~} 
389\newcommand{\welse}[1]{{\sf else}~#1} 
390
391%Pour la fleche double, il faut rajouter :
392%      \usepackage{mathtools}
393
394\newcommand{\act}[1]{\xrightarrow{#1}} %labelled actionlow %high
395
396\newcommand{\lact}[1]{\stackrel{#1}{\makebox[5mm]{\,$- \! {\circ}\,$}}}
397
398\newcommand{\set}[1]{\{#1\}}
399\newcommand{\pst}[2]{{\sf pset}(#1,#2)}
400\newcommand{\st}[2]{{\sf set}(#1,#2)}
401\newcommand{\wrt}[2]{{\sf w}(#1,#2)}
402
403\newcommand{\chtype}[2]{{\it Ch_{#1}(#2)}}
404\newcommand{\rgtype}[2]{{\it {\sf Reg}_{#1} #2}}
405
406\newcommand{\get}[1]{{\sf get}(#1)}
407
408%\newcommand{\wact}[1]{\xRightarrow{#1}} %weak labelled action low high
409
410%\newcommand{\mact}[1]{\xrightarrow{#1}_{m}} %labelled action low %high
411
412%\newcommand{\wmact}[1]{\xRightarrow{#1}_{m}} %weak labelled action low high
413
414%\newcommand{\act}[1]{\stackrel{#1}{\rightarrow}} %labelled action low
415                                %%%high
416
417\newcommand{\acteq}[1]{\stackrel{#1}{\leadsto}} %labelled action low
418                                %%%high
419
420
421%\newcommand{\actI}[1]{\stackrel{#1}{\rightarrow_{1}}} %labelled action low
422\newcommand{\actI}[1]{\xrightarrow{#1}_{1}}
423
424%\newcommand{\actII}[1]{\stackrel{#1}{\rightarrow_{2}}} %labelled action low
425\newcommand{\actII}[1]{\xrightarrow{#1}_{2}}
426
427
428 \newcommand{\wact}[1]{\stackrel{#1}{\Rightarrow}} %weak labelled action low high
429\newcommand{\wactI}[1]{\stackrel{#1}{\Rightarrow_{1}}} %weak labelled action low high
430\newcommand{\wactII}[1]{\stackrel{#1}{\Rightarrow_{2}}} %weak labelled action low high
431
432
433\newcommand{\mact}[1]{\stackrel{#1}{\rightarrow_{m}}} %labelled action low
434%high
435\newcommand{\wmact}[1]{\stackrel{#1}{\Rightarrow_{m}}} %weak labelled action low high
436 
437%\newcommand{\lact}[1]{\stackrel{#1}{\leftarrow}}
438\newcommand{\lwact}[1]{\stackrel{#1}{\Leftarrow}} 
439 
440 
441 
442\newcommand{\eval}{\Downarrow} 
443\newcommand{\Eval}[1]{\Downarrow^{#1}} 
444 
445 
446\newcommand{\Z}{{\bf Z}} 
447\newcommand{\Real}{\mathbb{R}^{+}} 
448\newcommand{\Return}{\ensuremath{\mathtt{return}}\xspace}                 
449\newcommand{\Stop}{\ensuremath{\mathtt{stop}}\xspace} 
450\newcommand{\Wait}{\ensuremath{\mathtt{wait}}\xspace} 
451\newcommand{\Read}{\ensuremath{\mathtt{read}}\xspace} 
452\newcommand{\Write}{\ensuremath{\mathtt{write}}\xspace} 
453\newcommand{\Yield}{\ensuremath{\mathtt{yield}}\xspace} 
454\newcommand{\Next}{\ensuremath{\mathtt{next}}\xspace} 
455\newcommand{\Load}{\ensuremath{\mathtt{load}}\xspace} 
456\newcommand{\Call}{\ensuremath{\mathtt{call}}\xspace} 
457\newcommand{\Tcall}{\ensuremath{\mathtt{tcall}}\xspace} 
458\newcommand{\Pop}{\ensuremath{\mathtt{pop}}\xspace} 
459\newcommand{\Build}{\ensuremath{\mathtt{build}}\xspace} 
460\newcommand{\Branch}{\ensuremath{\mathtt{branch}}\xspace} 
461\newcommand{\Goto}{\ensuremath{\mathtt{goto}}\xspace} 
462 
463\newcommand{\hatt}[1]{#1^{+}} 
464\newcommand{\Of}{\mathbin{\w{of}}} 
465 
466\newcommand{\susp}{\downarrow} 
467\newcommand{\lsusp}{\Downarrow_L} 
468\newcommand{\wsusp}{\Downarrow} 
469\newcommand{\commits}{\searrow} 
470 
471 
472\newcommand{\spi}{S\pi} 
473 
474
475 \newcommand{\pres}[2]{#1\triangleright #2} %TCCS else next (alternative)
476% \newcommand{\pres}[2]{ \lfloor #1 \rfloor (#2)}  %TCCS else next
477\newcommand{\present}[3]{{\sf present} \ #1 \ {\sf do } \ #2 \ {\sf  else} \ #3}
478
479
480\newcommand{\tick}{{\sf tick}}          %tick action
481
482 
483 
484\newcommand{\sbis}{\equiv_L} 
485\newcommand{\emit}[2]{\ol{#1}#2} 
486%\newcommand{\present}[4]{#1(#2).#3,#4}
487\newcommand{\match}[4]{[#1=#2]#3,#4}       %pi-equality
488
489\newcommand{\matchv}[4]{[#1 \unrhd #2]#3,#4}
490
491\newcommand{\new}[2]{\nu #1 \ #2} 
492\newcommand{\outact}[3]{\new{{\bf #1}}{\emit{#2}{#3}}} 
493\newcommand{\real}{\makebox[5mm]{\,$\|\!-$}}% realizability relation
494
495\newcommand{\regterm}[2]{{\sf reg}_{#1} #2}
496\newcommand{\thread}[1]{{\sf thread} \ #1}
497\newcommand{\store}[2]{(#1 \leftarrow #2)}
498\newcommand{\pstore}[2]{(#1 \Leftarrow #2)}
499
500\newcommand{\regtype}[2]{{\sf Reg}_{#1} #2}
501\newcommand{\uregtype}[3]{{\sf Reg}_{#1}(#2, #3)}
502\newcommand{\urtype}[2]{{\sf Reg}(#1, #2)}
503
504\newcommand{\upair}[2]{[#1,#2]}
505\newcommand{\letb}[3]{\mathsf{let}\;\oc #1 = #2\;\mathsf{in}\;#3}
506
507\newcommand{\vlt}[1]{{\cal V}(#1)}
508\newcommand{\prs}[1]{{\cal P}(#1)}
509
510\newcommand{\imp}{{\sf Imp}}            %imp language
511\newcommand{\vm}{{\sf Vm}}              %virtual machine language
512\newcommand{\mips}{{\sf Mips}}          %Mips language
513\newcommand{\C}{{\sf C}}                % C language
514\newcommand{\Clight}{{\sf Clight}}        %C light language
515\newcommand{\Cminor}{{\sf Cminor}}
516\newcommand{\RTLAbs}{{\sf RTLAbs}}
517\newcommand{\RTL}{{\sf RTL}}
518\newcommand{\ERTL}{{\sf ERTL}}
519\newcommand{\LTL}{{\sf LTL}}
520\newcommand{\LIN}{{\sf LIN}}
521\newcommand{\access}[1]{\stackrel{#1}{\leadsto}}
522\newcommand{\ocaml}{{\sf ocaml}}
523\newcommand{\coq}{{\sf Coq}}
524\newcommand{\compcert}{{\sf CompCert}}
525%\newcommand{\cerco}{{\sf CerCo}}
526\newcommand{\cil}{{\sf CIL}}
527\newcommand{\scade}{{\sf Scade}}
528\newcommand{\absint}{{\sf AbsInt}}
529\newcommand{\framac}{{\sf Frama-C}}
530\newcommand{\powerpc}{{\sf PowerPc}}
531\newcommand{\lustre}{{\sf Lustre}}
532\newcommand{\esterel}{{\sf Esterel}}
533\newcommand{\ml}{{\sf ML}}
534
535\newcommand{\codeex}[1]{\texttt{#1}}   % code example
536
537\bibliographystyle{abbrv} 
538
539\title{
540INFORMATION AND COMMUNICATION TECHNOLOGIES\\
541(ICT)\\
542PROGRAMME\\
543\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
544
545\date{ }
546\author{}
547%>>>>>> new commands used in this document
548% \usepackage[nohyperref,nosvn]{mystyle}
549
550\usepackage{multirow}
551\newcolumntype{b}{@{}>{{}}}
552\newcolumntype{B}{@{}>{{}}c<{{}}@{}}
553\newcolumntype{h}[1]{@{\hspace{#1}}}
554\newcolumntype{L}{>{$}l<{$}}
555\newcolumntype{C}{>{$}c<{$}}
556\newcolumntype{R}{>{$}r<{$}}
557\newcolumntype{S}{>{$(}r<{)$}}
558\newcolumntype{n}{@{}}
559\newcommand{\spanr}[2]{\multicolumn{1}{Rn}{\multirow{#1}{*}{(#2)}}}
560\def\nocol{\multicolumn{1}{ncn}{}}
561
562\usepackage[disable, colorinlistoftodos]{todonotes}
563\usepackage{enumerate}
564\usepackage{tikz}
565
566\newcommand{\tern}[3]{#1\mathrel ? #2 : #3}
567\newcommand{\sop}[1]{\s{#1}\ }
568\newcommand{\sbin}[1]{\ \s{#1}\ }
569\newcommand{\Ell}{\mathcal L}
570\newcommand{\alphab}{\boldsymbol\alpha}
571\newcommand{\betab}{\boldsymbol\beta}
572\newcommand{\gramm}{\mathrel{::=}}
573\newcommand{\ass}{\mathrel{:=}}
574
575\renewcommand{\to}[1][]{\stackrel{#1}{\rightarrow}}
576%<<<<<<<<<<<<
577\begin{document}
578% \thispagestyle{empty}
579%
580% \vspace*{-1cm}
581% \begin{center}
582% \includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
583% \end{center}
584%
585% \begin{minipage}{\textwidth}
586% \maketitle
587% \end{minipage}
588%
589%
590% \vspace*{0.5cm}
591% \begin{center}
592% \begin{LARGE}
593% \bf
594% Report \\
595% Dependent Cost Labels
596% \\
597% \end{LARGE}
598% \end{center}
599%
600% \vspace*{2cm}
601% \begin{center}
602% \begin{large}
603% Version 0.1
604% \end{large}
605% \end{center}
606%
607% \vspace*{0.5cm}
608% \begin{center}
609% \begin{large}
610% Main Author:\\
611% Paolo Tranquilli
612% \end{large}
613% \end{center}
614%
615% \vspace*{\fill}
616% \noindent
617% Project Acronym: \cerco{}\\
618% Project full title: Certified Complexity\\
619% Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
620%
621% \clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
622%
623% \newpage
624
625\listoftodos
626
627\section{Introduction}
628In~\cite{D2.1} an approach is presented tackling the problem of building a
629compiler from a large fragment of C which is capable of lifting execution cost information
630from the compiled code and present it to the user. This endeavour is central to
631the CerCo project, which strives to produce a mechanically certified version of
632such a compiler.
633
634In rough words, the proposed approach consists in decorating the source code with
635labels at key points, and preserving such labels along the compilation chain.
636Once the final object code is produced, such labels should correspond to parts
637of the compiled code which have constant cost.
638
639There are two properties one asks of the cost estimate. The first, paramount to
640the correctness of the method, is \emph{soundness}: the actual execution cost
641is bounded by the estimate. In the labelling approach, this is guaranteed if every
642loop in the control flow of the compiled code passes through at least one cost
643label. The second, optional but desirable, is \emph{preciseness}: the estimate
644is not in fact an estimate but the actual cost. In the labelling approach, this will
645be true if for every label every possible execution of the compiled code starting
646from such a label yields the same cost. In simple architectures such as the 8051
647micro-controller this can be guaranteed by having labels at the immediate start of any
648branch of the control flow, and by ensuring no duplicate labels are present.
649
650It should be underlined that the above mentioned requirements must hold when
651executing the code at the
652end of the compilation chain. If one is careful to inject the labels at good
653key places in the source code, one can still think of two main obstacles:
654\begin{itemize}
655 \item compilation introduces important changes in the control flow, inserting
656loops or branches: an example in addressing this is the insertion of functions
657in the source code replacing instructions unavailable in the target architecture
658that require loops (e.g.\ multi-word division and generic shift in the 8051
659architecture) so that the annotation process be sound, or the effort put in
660providing unbranching translations of higher level instructions~
661\cite{D2.2};
662 \item even if the compiled code \emph{does}, as long as the the syntactic
663  control flow graph is concerned, respect the conditions for soundness and
664  preciseness, the cost of blocks of instructions might not be independent of context,
665  so that different passes through a label might have different costs: this
666  becomes a concern if one wishes to apply the approach to more complex architectures,
667  for example one with cache or pipelining.
668\end{itemize}
669
670The first point unveils a weakness of the current labelling approach when it
671comes to some common code transformations done along a compilation chain. In
672particular most of \emph{loop optimizations} disrupt such conditions directly.
673For example in what we will call \emph{loop peeling} a first iteration of the
674loop is hoisted ahead of it, possibly to have a different cost than later iterations
675because of further transformation such as dead code elimination or invariant
676code motion.
677
678The second point strikes a difference in favour to existing tools for the
679estimate of execution costs to the detriment of CerCo's approach advocated in~
680\cite{D2.1}. We will take as example the well known tool \s{aiT}~\cite{absint},
681based on abstract interpretation: such a tool allows to estimate the
682worst-case execution time (WCET) taking into account advanced aspects of the
683target architecture. \s{aiT}'s ability to
684do close estimates of execution costs even when these depend on the context of
685execution would enhance the effectiveness of CerCo's compiler, either by
686integrating such techniques in its development, or by directly calling this tool
687when ascertaining the cost of blocks of compiled code. A typical case where
688cache analysis yields a difference in the execution cost of a block is in loops:
689the first iteration will usually stumble upon more cache misses than subsequent
690iterations.
691
692If one looks closely, the source of the weakness of the labelling approach as
693presented in~\cite{D2.1} is common to both points: the inability to state
694different costs for different occurrences of labels, where the difference
695might be originated by labels being duplicated along compilation
696or the costs being sensitive to the state of execution.
697
698The preliminary work
699we present here addresses this node, introducing cost labels that are dependent
700on which iteration of its containing loops it occurs in. This is achieved by
701means of \emph{indexed labels}: all cost labels are decorated with formal
702indexes coming from the loops containing such labels. These indexes allow to
703rebuild, even after several steps of loop transformations,
704which iterations of the original loops in the source code a particular label
705occurrence belongs to. During annotation of source code, this information
706is given to the user by means of dependent costs.
707
708We concentrate on integrating the labelling approach with two loop transformations.
709For general information on compiler optimization (and loop optimizations in
710particular) we refer the reader to the vast literature on the subject
711(e.g.~\cite{muchnick,morgan}).
712
713\emph{Loop peeling}, as already mentioned, consists in preceding the loop with
714a copy of its body, appropriately guarded. This is in general useful to trigger
715further optimizations, such as ones relying on execution information which can
716be computed at compile time but which is erased by further iterations of the loop,
717or ones that use the hoisted code to be more effective at eliminating redundant
718code. Integrating this transformation to the labelling approach would also allow
719to integrate the common case of cache analysis explained above: the analysis
720of cache hits and misses in the case of usually benefits from a form of
721\emph{virtual} loop peeling~\cite{cacheprediction}.
722
723\emph{Loop unrolling} consists in repeating several times the body of the loop
724inside the loop itself (inserting appropriate guards, or avoiding them altogether
725if enough information on the loop's guard is available at compile time). This
726can limit the number of (conditional or unconditional) jumps executed by the
727code and trigger further optimizations dealing with pipelining, if applicable
728to the architecture.
729
730While covering only two loop optimizations, the work presented here poses good
731bases to extending the labelling approach to cover more and more of them, as well
732as giving hints as to how integrating in CerCo's compiler advanced cost estimation
733techniques such as cache analysis. Moreover loop peeling has the substantial
734advantage of enhancing other optimizations. Experimentation with CerCo's
735untrusted prototype compiler with constant propagation and
736partial redundancy elimination~\cite{PRE,muchnick} show how loop peeling enhances
737those other optimizations.
738
739\paragraph{Outline.}
740We will present our approach on a minimal toy imperative language, \imp{}
741with gotos, which we present in \autoref{sec:defimp} along with formal
742definition of the loop transformations. This language already
743presents most of the difficulties encountered when dealing with C, so
744we stick to it for the sake of this presentation. In \autoref{sec:labelling}
745we summarize the labelling approach as presented in~\cite{D2.1}. The following
746\autoref{sec:indexedlabels} explains \emph{indexed labels}, our proposal for
747dependent labels which are able to describe precise costs even in the presence
748of the loop transformations we consider. Finally \autoref{sec:conc} goes into
749more details regarding the implementation of indexed labels in CerCo's
750untrusted compiler and speculates on further work on the subject.
751
752
753\section{\imp{} with goto}\label{sec:defimp}
754We briefly outline the toy language which contains all the relevant instructions
755to present the development and the problems it is called to solve.
756
757The version of the minimal imperative language \imp that we will present has,
758with respect to the bare-bone usual version, \s{goto}s and labelled statements.
759Break and continue statements can be added at no particular expense. Its syntax
760and operational semantics is presented in \autoref{fig:minimp}.
761\begin{figureplr}
762$$\begin{gathered}
763\begin{array}{nlBl>(R<)n}
764\multicolumn{4}{C}{\bfseries Syntax}\\
765\multicolumn{4}{ncn}{
766  \ell,\ldots \hfill \text{(labels)} \hfill x,y,\ldots \hfill
767\text{(identifiers)}
768\hfill e,f,\ldots \hfill \text{(expression)}
769}\\
770P,S,T,\ldots &\gramm& \s{skip} \mid s;t
771\mid \sop{if}e\sbin{then}s\sbin{else}t
772\mid \sop{while} e \sbin{do} s \mid
773  x \ass e
774\\&\mid&
775\ell : s \mid \sop{goto}\ell& \spanr{-2}{statements}\\
776\\
777\multicolumn{4}{C}{\bfseries Semantics}\\
778K,\ldots  &\gramm& \s{halt} \mid S \cdot K & continuations
779\end{array}
780\\[15pt]
781\s{find}(\ell,S,K) \ass
782\left\{\begin{array}{lL}
783\bot & if $S=\s{skip},\sop{goto} \ell'$ or $x\ass e$,\\
784(T, K) & if $S=\ell:T$,\\
785\s{find}(\ell,T,K) & otherwise, if $S = \ell':T$,\\
786\s{find}(\ell,T_1,T_2\cdot K) & if defined and $S=T_1;T_2$,\\
787\s{find}(\ell,T_1,K) & if defined and
788$S=\sop{if}b\sbin{then}T_1\sbin{else}T_2$,\\
789\s{find}(\ell,T_2,K) & otherwise, if $S=T_1;T_2$ or
790$\sop{if}b\sbin{then}T_1\sbin{else}T_2$,\\
791\s{find}(\ell,T,S\cdot K) & if $S = \sop{while}b\sbin{do}T$.
792\end{array}\right.
793\\[15pt]
794\begin{array}{lBl}
795(x:=e,K,s)  &\to_P& (\s{skip},K,s[v/x]) \qquad\mbox{if }(e,s)\eval v \\ \\
796
797(S;T,K,s)  &\to_P& (S,T\cdot K,s) \\ \\
798
799(\s{if} \ b \ \s{then} \ S \ \s{else} \ T,K,s)
800&\to_P&\left\{
801\begin{array}{ll}
802(S,K,s) &\mbox{if }(b,s)\eval v \neq 0 \\
803(T,K,s) &\mbox{if }(b,s)\eval 0
804\end{array}
805\right. \\ \\
806
807
808(\s{while} \ b \ \s{do} \ S ,K,s)
809&\to_P&\left\{
810\begin{array}{ll}
811(S,\s{while} \ b \ \s{do} \ S \cdot K,s) &\mbox{if }(b,s)\eval v \neq 0 \\
812(\s{skip},K,s) &\mbox{if }(b,s)\eval 0
813\end{array}
814\right. \\ \\
815
816
817(\s{skip},S\cdot K,s)  &\to_P&(S,K,s) \\ \\
818
819(\ell : S, K, s)  &\to_P& (S,K,s) \\ \\
820
821(\sop{goto}\ell,K,s)  &\to_P& (\s{find}(\ell,P,\s{halt}),s) \\ \\
822\end{array}
823\end{gathered}$$
824
825
826\caption{The syntax and operational semantics of \imp.}
827\label{fig:minimp}
828\end{figureplr}
829The actual
830grammar for expressions is not particularly relevant so we do not give a
831precise one. For the sake of this presentation we also treat boolean and
832arithmetic expressions together (with the usual convention of an expression
833being true iff non-zero).
834
835We will suppose programs are
836\emph{well-labelled}, i.e.\ every label labels at most one occurrence of statement
837in the program, and every \s{goto} points to a label actually present in the program.
838The \s{find} helper functions has the task of not only finding the labelled
839statement in the program, but also building the correct continuation. The continuation
840built by \s{find} replaces the current continuation in the case of a jump.
841
842\paragraph{Further down the compilation chain.}
843As for the rest of the compilation chain, we abstract over it. We just posit
844every language $L$ further down the compilation chain has a suitable notion of
845sequential instructions (with one natural successor), to which we can add our
846own.
847
848\subsection{Loop transformations}
849We call a loop $L$ \emph{single-entry} in $P$ if there is no \s{goto} of $P$
850outside of $L$ which jumps to within $L$\footnote{This is a reasonable
851aproximation: it considers multi-entry also those loops having an external but
852unreachable \s{goto} jumping to them.}. Many loop optimizations do not preserve
853the semantics of multi-entry loops in general, or are otherwise rendered
854ineffective. Usually compilers implement a multi-entry loop detection which
855avoids those loops from being targeted by optimizations~\cite{muchnick,morgan}.
856
857
858\paragraph{Loop peeling.}
859$$
860\sop{while}b\sbin{do}S\mapsto
861\sop{if}b\sbin{then} S; \sop{while} b \sbin{do} S[\ell'_i/\ell_i]
862$$
863where $\ell'_i$ is a fresh label for any $\ell_i$ labelling a statement in $S$.
864This relabelling is safe as to \s{goto}s external to the loop because of the
865single-entry condition. Notice that in case of break and continue statements,
866those should be replaced with \s{goto}s in the peeled body $S$.
867
868\paragraph{Loop unrolling.}
869$$
870\sop{while}b\sbin{do}S\mapsto
871\sop{while} b \sbin{do} (S ;
872  \sop{if} b \sbin{then} (S[\ell^1_i/\ell_i] ;
873  \cdots
874  \sop{if} b \sbin{then} S[\ell^n_i/\ell_i]) \cdots)
875$$
876where $\ell^j_i$ are again fresh labels for any $\ell_i$ labelling a statement
877in $S$. This is a willingly naïf version of loop unrolling, which usually
878targets less general loops. The problem it poses to Cerco's labelling approach
879are independent of the cleverness of the actual transformation.
880
881\section{Labelling: a quick sketch of the previous approach}\label{sec:labelling}
882Plainly labelled \imp{} is obtained adding to the code \emph{cost labels}
883(with metavariables $\alpha,\beta,\ldots$), and cost-labelled statements:
884$$S,T\gramm \cdots \mid \alpha: S$$
885Cost labels allow for some program points to be tracked along the compilation
886chain. For further details we refer to\cite{D2.1}.
887
888With labels the small step semantics turns into a labelled transition
889system and a natural notion of trace (i.e.\ lists of labels) arises.
890Evaluation of statements is enriched with traces, so that rules are like
891$$
892\begin{array}{lblL}
893(\alpha: S, K,s) &\to[\alpha]_P (S,K,s)\\
894(\s{skip}, S \cdot K,s) &\to[\varepsilon]_P (S, K, s)\\
895& \text{etc.}
896\end{array}$$
897where we identify cost labels $\alpha$ with singleton traces and we use $\varepsilon$
898for the empty trace. We then write $\to[\lambda]\!\!^*$ for the transitive
899closure of the small step semantics which produces by concatenation the trace
900$\lambda$.
901
902\paragraph{Labelling.}
903Given an \imp{} program $P$ its \emph{labelling} $\alpha:\Ell(P)$ in $\ell-\imp$
904is
905defined by putting cost labels after every branching, at the start of both
906branches, and a cost label at the beginning of the program. So the relevant
907cases are
908$$\begin{aligned}
909  \Ell(\sop{if}e\sbin{then}S\sbin{else}T) &=
910    \sop{if}e\sbin{then}\alpha:\Ell(S)\sbin{else}\beta:\Ell(T)\\
911  \Ell(\sop{while}e\sbin{do}S) &=
912    (\sop{while}e\sbin{do}\alpha:\Ell(S));\beta:\s{skip}
913  \end{aligned}$$
914where $\alpha,\beta$ are fresh cost labels, and while in other cases the
915definition just passes to sub-statements.
916
917\paragraph{Labels in the rest of the compilation chain.} All languages further
918down the chain get a new sequential statement $\sop{emit}\alpha$ whose effect is
919to be consumed in a labelled transition while keeping the same state. All other
920instructions guard their operational semantics and do not emit cost labels.
921
922Preservation of semantics throughout the compilation process is restated, in
923rough terms, as
924$$\text{starting state of $P$}\to[\lambda]\!\!^*\;\text{halting state} \iff
925  \text{starting state of $\mathcal C(P)$} \to[\lambda]\!\!^*\;\text{halting state},$$
926where $P$ is a program of a language along the compilation chain, starting and
927halting states depend on the language, and $\mathcal C$ is the
928compilation function\footnote{The case of divergent computations needs
929to be addressed too. Also, the requirement can be weakened by demanding some
930sort of equivalence of the traces rather than equality. Both these issues escape
931the scope of this presentation.}.
932
933\paragraph{Instrumentations}
934Let $\mathcal C$ be the whole compilation from $\ell\imp$ to the labelled
935version of some low-level language $L$. Supposing such compilation has not
936introduced any new loop or branching, we have that
937\begin{itemize}
938 \item every loop contains at least a cost label (\emph{soundness condition}),
939and
940 \item every branching has different labels for the two branches
941  (\emph{preciseness condition}).
942\end{itemize}
943With these two conditions, we have that each and every cost label in
944$\mathcal C(P)$ for any $P$ corresponds to a block of sequential instructions,
945to which we can assign a constant \emph{cost}\footnote{This in fact requires the
946machine architecture to be simple enough, or for some form of execution analysis
947to take place.} We can therefore assume a \emph{cost mapping} $\kappa_P$ from
948cost labels to natural numbers, assigning to each cost label $\alpha$ the cost
949of the block containing the single occurrance of $\alpha$.
950
951Given any cost mapping $\kappa$, we can enrich a labelled program so that a
952particular fresh variable (the \emph{cost variable} $c$) keeps track of the
953assumulation of costs during the execution. We call this procedure
954\emph{instrumentation} of the program, and it is defined recursively by
955$$
956  \mathcal I(\alpha:S) = c \ass c + \kappa(\alpha) ; \mathcal I(S)
957$$
958while in all other cases the definition passes to substatements.
959
960\paragraph{The problem with loop optimizations.}
961Let us take loop peeling, and apply it to the labelling of a program without any
962adjustment:
963$$
964(\sop{while}e\sbin{do}\alpha:S);\beta:\s{skip}
965\mapsto
966(\sop{if}b\sbin{then} \alpha : S; \sop{while} b \sbin{do} \alpha :
967S[\ell'_i/\ell_i]);
968\beta:\s{skip}$$
969What happens is that the cost label $\alpha$ is duplicated into two distinct
970occurrences. If these two occurrences correspond to different costs in the
971compiled code, the best the cost mapping can do is to take the maximum of the
972two, preserving soundness (i.e.\ the cost estimate still bounds the actual one)
973but loosing preciseness (i.e.\ the actual cost would be strictly less than its
974estimate).
975
976\section{Indexed labels}\label{sec:indexedlabels}
977This section presents the core of the new approach. In brief points it amounts
978to the following.
979\begin{enumerate}[\bfseries \ref*{sec:indexedlabels}.1.]
980 \item\label{en:outline1}
981Enrich cost labels with formal indexes corresponding, at the beginning of
982the process, to which iteration of the loop they belong to.
983 \item\label{en:outline2}
984Each time a loop transformation is applied and a cost labels is split in
985different occurrences, each of these will be reindexed so that every time they
986are emitted their position in the original loop will be reconstructed.
987 \item\label{en:outline3}
988Along the compilation chain, add alongside the \s{emit} instruction other
989ones updating the indexes, so that iterations of the original loops can be
990rebuilt at the operational semantics level.
991 \item\label{en:outline4}
992The machinery computing the cost mapping will still work, but assigning
993costs to indexed cost labels, rather than to cost labels as we wish: however
994\emph{dependent costs} can be calculated, where dependency is on which iteration
995of the containing loops we are in.
996\end{enumerate}
997
998\subsection{Indexing the cost labels}\label{ssec:indlabs}
999\paragraph{Formal indexes and $\iota\ell\imp$.}
1000Let $i_0,i_1,\ldots$ be a sequence of distinguished fresh identifiers that will
1001be used as loop indexes. A \emph{simple expression} is an affine arithmetical
1002expression in one of these indexes, that is $a*i_k+b$ with $a,b,k \in \mathbb N$.
1003Simple expressions $e_1=a_1*i_k+b_1$, $e_2=a2*i_k+b_2$ in the same index can be
1004composed, yielding $e_1\circ e_2\ass (a_1a_2)*i_k + (a_1b2+b_1)$, and this operation
1005has an identity element in $id_k \ass 1*i_k+0$. Constants can be expressed as simple
1006expressions, so that we identify a natural $c$ with $0*i_k+c$.
1007
1008An \emph{indexing} (with metavariables $I$, $J$, \ldots) is a list of
1009transformations of successive formal indexes dictated by simple expressions,
1010that is a mapping%
1011\footnote{Here we restrict each mapping to be a simple expression
1012\emph{on the same index}. This might not be the case if more loop optimizations
1013are accounted for (for example, interchanging two nested loops).}
1014$$i_0\mapsto a_0*i_0+b_0,\dots, i_{k-1} \mapsto a_{k-1}*i_{k-1}+b_{k-1}.$$
1015
1016An \emph{indexed cost label} (metavariables $\alphab$, $\betab$, \ldots) is
1017the combination of a cost label $\alpha$ and an indexing $I$, written
1018$\alpha\la I\ra$. The cost label underlying an indexed one is called its
1019\emph{atom}. All plain labels can be considered as indexed ones by taking
1020an empty indexing.
1021
1022\imp{} with indexed labels ($\iota\ell\imp$) is defined by adding to $\imp$
1023statements with indexed labels, and by having loops with formal indexes
1024attached to them:
1025$$S,T,\ldots \gramm \cdots i_k:\sop{while}e\sbin{do}S\mid \alphab : S.$$
1026Notice than unindexed loops still are in the language: they will correspond
1027to multi-entry loops which are ignored by indexing and optimizations.
1028We will discuss the semantics later.
1029
1030\paragraph{Indexed labelling.}
1031Given an $\imp$ program $P$, in order to index loops and assign indexed labels
1032we must first of all distinguish single-entry loops. We just sketch how it can
1033be computed.
1034
1035A first pass of the program $P$ can easily compute two maps: $\s{loopof}_P$
1036from each label $\ell$ to the occurrence (i.e.\ the path) of a $\s{while}$ loop
1037containing $\ell$, or the empty path if none exists; and $\s{gotosof}_P$ from
1038a label $\ell$ to the occurrences of \s{goto}s pointing to it. Then the set
1039$\s{multyentry}_P$ of multy-entry loops of $P$ can be computed by adding to it
1040all occurrences $p$ such that there exists a label $\ell$ and an occurrence
1041$q$ with $\s{loopof}_P(\ell)=p$, $q\in \s{gotosof}_P(\ell)$ and $p\not\le q$
1042(where $\le$ is the prefix relation)\footnote{Possible simplification to this
1043procedure include keeping track just of while loops containing labels and
1044\s{goto}s (rather than paths in the syntactic tree of the program), and making
1045two passes while avoiding building the map to sets $\s{gotosof}$}.
1046
1047Let $Id_k$ be the indexing of length $k$ made from identity simple expressions,
1048i.e.\ the sequence $i_0\mapsto id_0, \ldots , i_{k-1}\mapsto id_{k-1}$. We define the tiered indexed labelling
1049$\Ell^\iota_P (S,k)$ in program $P$ for occurrence $S$ of a statement in $P$
1050and a natural $k$ by recursion, setting
1051$$
1052\Ell^\iota_P(S,k)\ass
1053\left\{
1054\begin{array}{lh{-100pt}l}
1055 (i_k:\sop{while}b\sbin{do}\alpha\la Id_{k+1}\ra : \Ell^\iota_P(T,k+1));\beta\la Id_k \ra : \s{skip}
1056\\& \text{if $S=\sop{while}b\sbin{do}T$ and $S\notin \s{multyentry}_P$,}\\[3pt]
1057(\sop{while}b\sbin{do}\alpha\la Id_k \ra : \Ell^\iota_P(T,k));\beta\la Id_k \ra : \s{skip}
1058\\& \text{otherwise, if $S=\sop{while}b\sbin{do}T$,}\\[3pt]
1059\sop{if}b\sbin{then} \alpha\la Id_k \ra : \Ell^\iota_P(T_1,k) \sbin{else} \beta\la Id_k \ra : \Ell^\iota_P(T_2,k)
1060\\&\text{if $S=\sop{if}b\sbin{then}T_1\sbin{else}T_2$,}\\[3pt]
1061\ldots
1062\end{array}
1063\right.
1064$$
1065where as usual $\alpha$ and $\beta$ are to be fresh cost labels, and other cases just keep
1066making the recursive calls on the substatements. The \emph{indexed labelling} of
1067a program $P$ is then defined as $\alpha\la \ra : \Ell^\iota_P(P,0)$, i.e.\ a
1068further fresh unindexed cost label is added at the start, and we start from level $0$.
1069
1070In other words: each single-entry loop is indexed by $i_k$ where $k$ is the number of
1071other single-entry loops containing this one, and all cost labels under the scope
1072of a single-entry loop indexed by $i_k$ are indexed by all indexes $i_0,\ldots,i_k$,
1073without any transformation.
1074
1075\subsection{Indexed labels and loop transformations}
1076We define the \emph{reindexing} $I \circ (i_k\mapsto a*i_k+b)$ as an operator
1077on indexings by setting
1078\begin{multline*}
1079(i_0\mapsto e_0,\ldots, i_k \mapsto e_k,\ldots,i_n\mapsto e_n)
1080\circ(i_k\mapsto a*i_k+b)
1081\ass\\
1082i_0\mapsto e_0,\ldots, i_k \mapsto e_k \circ(a*i_k+b),\ldots,i_n\mapsto e_n,
1083\end{multline*}
1084and extending then to indexed labels (by $\alpha\la I\ra\circ(i_k\mapsto e)\ass
1085\alpha\la I\circ (i_k\mapsto e)\ra$) and to statements in $\iota\ell\imp$
1086(by applying the above transformation to all indexed labels).
1087
1088We can then redefine loop peeling and loop unrolling taking into account indexed labels.
1089It will be possible to apply the transformation only to indexed loops, that is loops
1090that are single-entry. The attentive reader will notice that no assumption is
1091made on the labelling of the statements involved. In particular the transformation
1092can be repeated and composed at will. Also, notice that erasing all labelling
1093information (i.e.\ indexed cost labels and loop indexes) we recover exactly the
1094same transformations presented in \autoref{sec:defimp}.
1095
1096\paragraph{Indexed loop peeling.}
1097
1098$$
1099i_k:\sop{while}b\sbin{do}S\mapsto
1100\sop{if}b\sbin{then} S\circ (i_k\mapsto 0); i_k : \sop{while} b \sbin{do} S[\ell'_i/\ell_i]\circ(i_k\mapsto i_k + 1)
1101$$
1102As can be expected, the peeled iteration of the loop gets reindexed as always
1103being the first iteration of the loop, while the iterations of the remaining
1104loop get shifted by $1$.
1105
1106\paragraph{Indexed loop unrolling.}
1107$$
1108\begin{array}{l}
1109\begin{array}{ncn}
1110i_k:\sop{while}b\sbin{do}S\\
1111\tikz\node[rotate=-90,inner sep=0pt]{$\mapsto$};
1112\end{array}\\
1113i_k:\sop{while} b \sbin{do}\\
1114\quad (S\circ(i_k\mapsto n*i_k) ;\\
1115\quad \sop{if} b \sbin{then}\\
1116\quad\quad (S[\ell^1_i/\ell_i]\circ(i_k\mapsto n*i_k+1) ;\\
1117\quad\quad\quad \vdots \\
1118\quad\quad \quad \sop{if} b \sbin{then}\\
1119\quad \quad \quad \quad S[\ell^n_i/\ell_i]\circ(i_k\mapsto n*i_k+n-1)
1120)\cdots )
1121\end{array}
1122$$
1123Again, the reindexing is as can be expected: each copy of the unrolled body
1124has its indexes remapped so that when they are executed the original iteration
1125of the loop to which they correspond can be recovered.
1126
1127\subsection{Semantics and compilation of indexed labels}
1128
1129In order to make sense of loop indexes, one must keep track of their values
1130in the state. A \emph{constant indexing} (metavariables $C,\ldots$) is an
1131indexing which employs only constant simple expressions. The evaluation
1132of an indexing $I$ in a constant indexing $C$, noted $I|_C$, is defined
1133by
1134$$I\circ(i_0\mapsto c_0,\ldots, i_{k-1}\mapsto c_{k-1}) \ass
1135  \alphab\circ(i_0\mapsto c_0)\circ\cdots\circ(i_{k-1}\mapsto c_{k-1})$$
1136(using the definition of ${-}\circ{-}$ given in \autoref{ssec:indlabs}), considering it defined only
1137if the the resulting indexing is a constant one too\footnote{For example
1138$(i_0\mapsto 2*i_0,i_1\mapsto i_1+1)|_{i_0\mapsto 2}$ is undefined,
1139but $(i_0\mapsto 2*i_0,i_1\mapsto 0)|_{i_0\mapsto 2}=
1140i_0\mapsto 4,i_1\mapsto 2$, which is indeed a constant indexing,
1141even if the domain of the original indexing is not covered by the constant one.}.
1142The definition is extended to indexed labels by $\alpha\la I\ra|_C\ass \alpha\la I|_C\ra$.
1143
1144Constant indexings will be used to keep track of the exact iterations of the
1145original code the emitted labels belong to. We thus define two basic actions to
1146update constant indexings: $C[i_k{\uparrow}]$ which increments the value of
1147$i_k$ by one, and $C[i_k{\downarrow}0]$ which resets it to $0$.
1148
1149We are ready to update the definition of the operational semantics of
1150indexed labelled \imp. The emitted cost labels will now be ones indexed by
1151constant indexings. We add a special indexed loop construct for continuations
1152that keeps track of active indexed loop indexes:
1153$$K,\ldots  \gramm \cdots | i_k:\sop{while} b \sbin {do} S \sbin{then}  K$$
1154The difference between the regular stack concatenation
1155$i_k:\sop{while}b\sbin{do}S\cdot K$ and the new constructor is that the latter
1156indicates the loop is the active one in which we already are, while the former
1157is a loop that still needs to be started%
1158\footnote{In the presence of \s{continue} and \s{break} statements active
1159loops need to be kept track of in any case.}.
1160The \s{find} function is updated accordingly with the case
1161$$ \s{find}(\ell, i_k:\sop{while}b\sbin{do}S, K) \ass \s{find}(\ell, S, i_k:
1162  \sop{while}b\sbin{do}S\sbin{then}K).$$
1163The state will now be a 4-uple
1164$(S,K,s,C)$ which adds a constant indexing to the 3-uple of regular
1165semantics. The small-step rules for all statements but the
1166cost-labelled ones and the indexed loops remain the same, without
1167touching the $C$ parameter (in particular unindexed loops behave the same
1168as usual). The remaining cases are:
1169$$\begin{aligned}
1170   (\alphab : S,K,s,C) &\to[\alphab|_C]_P (S,K,s,C)\\
1171   (i_k:\sop{while}b\sbin{do}S,K,C) &\to[\varepsilon]_P
1172    \begin{cases}
1173     (S,i_k:\sop{while}b\sbin{do}S\sbin{then} K,s,C[i_k{\downarrow}0])
1174     \\\hskip 125pt \text{if $(b,s)\eval v\neq 0$,}\\
1175     \rlap{(\s{skip}, K, s, C)}\hskip 125pt \text{otherwise}
1176    \end{cases}\\
1177   (\s{skip}, i_k:\sop{while}b\sbin{do}S\sbin{then}K,C) &\to[\varepsilon]_P
1178    \begin{cases}
1179     (S,i_k:\sop{while}b\sbin{do}S\sbin{then} K,s,C[i_k{\uparrow}])
1180      \\\hskip 125pt \text{if $(b,s)\eval v\neq 0$,}\\
1181     \rlap{(\s{skip}, K, s, C)} \hskip 125pt \text{otherwise}
1182    \end{cases}
1183  \end{aligned}$$
1184Some explications are in order.
1185\begin{itemize}
1186 \item Emitting a label always instantiates it with the current indexing.
1187 \item Hitting an indexed loop the first time initializes to 0 the corresponding
1188  index; continuing the same loop inrements the index as expected.
1189 \item The \s{find} function ignores the current indexing: this is correct
1190  under the assumption that all indexed loops are single entry ones, so that
1191  when we land inside an indexed loop with a \s{goto}, we are sure that its
1192  current index is right.
1193  \item The starting state with store $s$ for a program $P$ is
1194$(P,\s{halt},s,(i_0\mapsto 0,\dots,i_{n-1}\mapsto 0)$ where $i_0,\ldots,i_{n-1}$ cover
1195all loop indexes of $P$\footnote{For a program which is the indexed labelling of an
1196\imp{} one this corresponds to the maximum nesting of single-entry loops. We can also
1197avoid computing this value in advance if we define $C[i{\downarrow}0]$ to extend
1198$C$'s domain as needed, so that the starting constant indexing can be the empty one.}.
1199\end{itemize}
1200
1201\paragraph{Compilation.}
1202Further down the compilation chain the loop
1203structure is usually partially or completely lost. We cannot rely on it anymore
1204to ensure keeping track of original source code iterations. We therefore add
1205alongside the \s{emit} instruction two other sequential instructions
1206$\sop{ind_reset}k$ and $\sop{ind_inc}k$ whose sole effect is to reset to
12070 (resp.\ increment by 1) the loop index $i_k$, as kept track of in a constant
1208indexing accompanying the state.
1209
1210The first step of compilation from $\iota\ell\imp$ consists in prefixing the
1211translation of an indexed loop $i_k:\s{while}\ b\ \s{do}\ S$ with
1212$\sop{ind_reset}k$ and postfixing the translation of its body $S$ with
1213$\sop{ind_inc}k$. Later on in the compilation chain we just need to propagate
1214the instructions dealing with cost labels.
1215
1216We would like to stress the fact that this machinery is only needed to give a
1217suitable semantics of observables on which preservation proofs can be done. By no
1218means the added instructions and the constant indexing in the state are meant
1219to change the actual (let us say denotational) semantics of the programs. In this
1220regard the two new instruction have a similar role as the \s{emit} one. A
1221forgetful mapping of everything (syntax, states, operational semantics rules)
1222can be defined erasing all occurrences of cost labels and loop indexes, and the
1223result will always be a regular version of the language considered.
1224
1225\paragraph{Stating the preservation of semantics.} In fact, the statement of preservation
1226of semantics does not change at all, if not for considering traces of evaluated
1227indexed cost labels rather than traces of plain ones.
1228
1229
1230\subsection{Dependent costs in the source code}\label{ssec:depcosts}
1231The task of producing dependent costs out of the constant costs of indexed labels
1232is quite technical. Before presenting it here, we would like to point out that
1233the annotations produced by the procedure described in this subsection, even
1234if correct, can be enormous and unreadable. In \autoref{sec:conc}, when we will
1235detail the actual implementation, we will also sketch how we mitigated this
1236problem.
1237
1238Having the result of compiling the indexed labelling $\Ell^\iota(P)$ of an \imp{}
1239program $P$, we can still suppose that a cost mapping can be computed, but
1240from indexed labels to naturals. We want to annotate the source code, so we need
1241a way to express and compute costs of cost labels, i.e.\ group the costs of
1242indexed labels to ones of their atoms. In order to do so we introduce
1243\emph{dependent costs}. Let us suppose that for the sole purpose of annotation,
1244we have available in the language ternary expressions of the form
1245$$\tern e {f_1}{f_2},$$
1246and that we have access to common operators on integers such as equality, order
1247and modulus.
1248
1249\paragraph{Simple conditions.}
1250First, we need to shift from \emph{transformations} of loop indexes to
1251\emph{conditions} on them. We identify a set of conditions on natural numbers
1252which are able to express the image of any composition of simple expressions.
1253
1254\emph{Simple conditions} are of three possible forms:
1255\begin{itemize}
1256 \item equality $i_k=n$ for some natural $n$;
1257 \item inequality $i_k\ge n$ for some natural $n$;
1258 \item modular equality together with inequality $i_k\bmod a = b\wedge i_k\ge n$
1259  for naturals $a, b, n$.
1260\end{itemize}
1261The always true simple condition is given by $i_k\ge 0$, and similarly we
1262write $i_k\bmod a = b$ as a simple condition for $i_k\bmod a = b\wedge i_k\ge 0$.
1263Given a simple condition $p$ and a constant indexing $C$ we can easily define
1264when $p$ holds for $C$ (written $p\circ C$). A \emph{dependent cost expression}
1265is an expression built solely out of integer constants and ternary expressions
1266with simple conditions at their head. Given a dependent cost expression $e$ where
1267all of the loop indexes appearing in it are in the domain of a constant indexing
1268$C$, we can define the value $e\circ C\in \mathbb N$ by
1269$$n\circ C\ass n,\qquad (\tern p e f)\circ C\ass
1270\begin{cases}
1271  e\circ C& \text{if $p\circ C$,}\\
1272  f\circ C& \text{otherwise.}
1273\end{cases}$$
1274
1275\paragraph{From indexed costs to dependent ones.}
1276Every simple expression $e$ corresponds to a simple condition $p(e)$ which expresses the
1277set of values that can be the result of it. Following is the definition of such
1278relation. We recall that in this development loop indexes are always mapped to
1279simple expressions over the same index. If it was not the case, the condition
1280obtained from an expression should be on the mapped index, not the indeterminate
1281of the simple expression. We leave to further work all generalizations of what
1282we present here.
1283$$
1284p(a*i_k+b)\ass
1285\begin{cases}
1286i_k = b & \text{if $a = 0$,}\\
1287i_k \ge b & \text{if $a = 1$,}\\
1288i_k\bmod a = b \wedge i_k \ge b & \text{otherwise}.
1289\end{cases}$$
1290Now, suppose we are given a mapping $\kappa$ from indexed labels to natural
1291numbers. We will transform it in a mapping (identified with an abuse of notation
1292with the same symbol $\kappa$) from atoms to \imp{} expressions built with
1293ternary expressions which depend solely on loop indexes. To that end we define
1294an auxiliary function $\kappa^\alpha_L$ parameterized by atoms and words of
1295simple expressions and defined on \emph{sets} of $n$-uples of simple expressions
1296(with $n$ constant across each such set, i.e.\ each set is made of words with
1297the same length).
1298
1299We will employ a bijection between words of simple expressions and indexings,
1300given by\footnote{Lists of simple expressions is in fact how indexings are
1301represented in Cerco's current implementation of the compiler.}
1302$$i_0\mapsto e_0,\ldots,i_{k-1}\mapsto e_{k-1} \cong e_0\cdots e_{k-1}.$$
1303As usual, $\varepsilon$ denotes the empty word/indexing, and juxtaposition
1304word concatenation.
1305
1306For every set $s$ of $n$-uples of simple expressions, we are in one of the following
1307three exclusive cases:
1308\begin{itemize}
1309 \item $S=\emptyset$, or
1310 \item $S=\{\varepsilon\}$, or
1311 \item there is a simple expression $e$ such that $S$ can be decomposed in
1312  $eS'+S''$, with $S'\neq \emptyset$ and none of the words in $S''$ starting with $e$
1313\end{itemize}
1314where $eS'$ denotes prepending $e$ to all elements of $S'$ and $+$ is disjoint
1315union. This classification can serve as the basis of a definition by recursion
1316on $n+\card S$ where $n$ is the size of tuples in $S$ and $\card S$ is its cardinality.
1317Indeed in the third case in $S'$ the size of tuples decreases strictly (and
1318cardinality does not increase) while for $S''$ the size of tuples remains the same
1319but cardinality strictly decreases. The expression $e$ of the third case will be chosen
1320as minimal for some total order\footnote{The specific order used does not change
1321the correctness of the procedure, but different orders can give more or less
1322readable results. A ``good'' order is the lexicographic one, with $a*i_k+b \le a'*i_k+b'$
1323if $a<a'$ or $a=a'$ and $b\le b'$.}.
1324
1325Following is the definition of the auxiliary function $\kappa^\alpha_L$, following
1326the recursion scheme presented above.
1327$$
1328\begin{aligned}
1329\kappa^\alpha_L(\emptyset) &\ass 0\\
1330\kappa^\alpha_L(\{\varepsilon\}) &\ass \kappa(\alpha\la L\ra) \\
1331\kappa^\alpha_L(eS'+S'') &\ass \tern{p(e)}{\kappa^\alpha_{Le}(S')}{\kappa^\alpha_L(S'')}
1332\end{aligned}
1333$$
1334
1335Finally, the wanted dependent cost mapping is defined by
1336$$\kappa(\alpha)\ass\kappa^\alpha_\varepsilon(\{\,L\mid \alpha\la L\ra \text{ appears
1337in the compiled code}\,\}).$$
1338
1339\paragraph{Indexed instrumentation.}
1340The \emph{indexed instrumentation} generalizes the instrumentation presented in
1341\autoref{sec:labelling}.
1342We described
1343above how cost atoms can be mapped to dependent costs. The instrumentation must
1344also insert code dealing with the loop indexes. As instrumentation is done
1345on the code produced by the labelling phase, all cost labels are indexed by
1346identity indexings. The relevant cases of the recursive definition
1347(supposing $c$ is the cost variable) are then
1348$$
1349\begin{aligned}
1350\mathcal I^\iota(\alpha\la Id_k\ra:S) &= c\ass c + \kappa(\alpha);\mathcal I^\iota(S)\\
1351\mathcal I^\iota(i_k : \sop{while}b\sbin{do}S) &=
1352  i_k \ass 0; \sop{while}b\sbin{do}(\mathcal I^\iota (S); i_k \ass i_k + 1)
1353\end{aligned}
1354$$
1355
1356\section{Notes on the implementation and further work}\label{sec:conc}
1357Implementing the indexed label approach in CerCo's untrusted OcaML prototype
1358does not introduce many aspects beyond what has already been presented for the toy
1359language \imp{} with \s{goto}s. \s{Clight}, the fragment of \s{C} which is the
1360source language of CerCo's compilation chain~\cite{D2.1}, has several more fetaures,
1361but few demand changes in the indexed labelled approach.
1362\paragraph{Indexed loops vs index update instructions.} In this presentation
1363we had indexed loops in $\iota\ell\imp$, while we hinted at the fact that later
1364languages in the compilation chain would have specific index update instructions.
1365In CerCo's actual compilation chain from \s{Clight} to 8051 assembly, indexed
1366loops are only in \s{Clight}, while from \s{Cminor} onward all languages have
1367the same three cost-involving instructions: label emitting, index resetting and
1368index incrementing.
1369\paragraph{Loop transformations in the front end.} We decided to implement
1370the two loop transformations in the front end, namely in \s{Clight}. This
1371decision is due to user readability concerns: if costs are to be presented to
1372the programmer, they should depend on structures written by the programmer
1373himself. If loop transformation were performed later it would be harder to
1374relate information on loops in the control flow graph with actual loops
1375written in the source code. Another solution would be however to index
1376loops in the source code and then use these indexes later in the compilation
1377chain to pinpoint explicit loops of the source code: loop indexes can be used
1378to preserve such information just like cost labels.
1379\paragraph{Break and continue statements.} \s{Clight}'s loop flow control
1380statements for breaking and continuing a loop are equivalent to appropriate
1381\s{goto} statements. The only difference is that we are assured that they cannot
1382cause loops to be multi-entry, and that when a transformation such as loop
1383peeling is done, they need to be replaced by actual \s{goto}s (which will happen
1384further down the compilation chain anyway).
1385\paragraph{Function calls.} Every internal function definition has its own
1386space of loop indexes. Executable semantics must thus take into account saving
1387and resetting the constant indexing of current loops upon hitting a function
1388call, and restoring it upon return of control. A peculiarity is that this cannot
1389be attached to actions saving and restoring frames: namely in the case of
1390tail calls the constant indexing needs to be saved whereas the frame does not.
1391\paragraph{Cost-labelled expressions.} In labelled \s{Clight} expressions get
1392cost labels too, because of the presence of ternary conditional expressions
1393(and lazy logical operators, which get translated to ternary expressions too).
1394Adapting the indexed labelled approach to cost-labelled expressions does not
1395pose particular problems.
1396\paragraph{Simplification of dependent costs.}
1397As already mentioned, the blind application of the procedure described in
1398\autoref{ssec:depcosts} produces unwieldy cost annotations. In the implementation
1399several transformations are used to simplify such dependent costs.
1400
1401Disjunctions of simple conditions are closed under all logical operations, and
1402it can be computed whether such a disjunction implies a simple condition
1403or its negation. This can be used to eliminate useless branches of dependent costs,
1404to merge branches that have the same value, and possibly to simplify the third
1405case of simple condition. Examples of the three transformations are respectively
1406\begin{itemize}
1407\item $
1408\verb+(_i_0 == 0)?+x\verb+:(_i_0 >= 1)?+y\verb+:+z
1409\mapsto
1410\verb+(_i_0 == 0)?+x\verb+:+y,
1411$
1412\item $
1413c\texttt{?}x\verb+:(+d\texttt{?}x\texttt{:}y\verb+)+
1414\mapsto
1415\texttt{(}c\texttt{ || }d\texttt{)?}x\texttt{:}y,
1416$
1417\item \begin{tabular}[t]{np{\linewidth}n}
1418$\verb+(_i_0 == 0)?+x\verb+:(_i_0 % 2 == 0 && _i_0 >= 2)?+y\verb+:+z
1419\mapsto$ \\\hfill
1420$\verb+(_i_0 == 0)?+x\verb+:(_i_0 % 2 == 0)?+y\verb+:+z.
1421$\end{tabular}
1422\end{itemize}
1423The second transformation tends to accumulate disjunctions, again to the detriment
1424of readability. A further transformation swaps two branches of the ternary
1425expression if the negation of the condition can be expressed with less clauses.
1426An example is
1427$$ \verb+(_i_0 % 3 == 0 || _i_0 % 3 == 1)?+x\verb+:+y \mapsto
1428\verb+(_i_0 % 3 == 2)?+y\verb+:+x.
1429$$
1430
1431\paragraph{Updates to the frama-C cost plugin.}
1432Cerco's frama-C~\cite{framac} cost plugin\todo{is there a reference for this?}{}
1433has been updated to take into account dependent
1434costs. The frama-c framework explodes ternary expressions to actual branch
1435statements introducing temporaries along the way, which makes the task of
1436analyzing ternary cost expressions rather daunting. It was deemed necessary to provide
1437an option in the compiler to use actual branch statements for cost annotations
1438rather than ternary expressions, so that at least frama-C's use of temporaries in
1439cost annotation be avoided. The cost analysis carried out by the plugin now
1440takes into account such dependent costs.
1441
1442The only limitation (which provided
1443a simplification in the code) is that within a dependent cost
1444simple conditions with modulus on the
1445same loop index should not be modulo different numbers, which corresponds to
1446the reasonable limitation of not applying multiple times loop unrolling to
1447the same loops.
1448\paragraph{Further work.}
1449Indexed labels are for now implemented only in the untrusted OcaML compiler,
1450while they are not present yet in the Matita code. Porting them should pose no
1451significant problem, and then the proof effort should begin.
1452
1453Because most of the executable operational semantics of the languages across the
1454front end and the back end are oblivious to cost labels, it should be expected
1455that the bulk of the semantic preservation proofs that still needs to be done
1456will not get any harder because of indexed labels. The only trickier point
1457would be in the translation of \s{Clight} to \s{Cminor}, where we
1458pass from structured indexed loops to atomic instructions on loop indexes.
1459
1460An invariant which should probably be proved and provably preserved along compilation
1461is the non-overlap of indexings for the same atom. Then, supposing cost
1462correctness for the unindexed approach, the indexed one will just need to
1463add the proof that
1464$$\forall C\text{ constant indexing}.\forall \alpha\la I\ra\text{ appearing in the compiled code}.
1465  \kappa(\alpha)\circ (I\circ C) = \kappa(\alpha\la I \ra).$$
1466$C$ represents a snapshot of loop indexes in the compiled code, while
1467$I\circ C$ is the corresponding snapshot in the source code. Semantics preservation
1468will make sure that when with snapshot $C$ we emit $\alpha\ra I\la$ (that is,
1469we have $\alpha\la I\circ C\ra$ in the trace), this means that $\alpha$ must be
1470emitted in the source code with indexing $I\circ C$, so the cost
1471$\kappa(\alpha)\circ (I\circ C)$ applies.
1472
1473Apart from carrying over the proofs, we would like to extend the approach
1474to more loop transformations. Important examples are loop inversion
1475(where a for loop is reversed, usually to make iterations appear as truly
1476independent) or loop interchange (where two nested loops are swapped, usually
1477to have more loop invariants or to enhance strength reduction). This introduces
1478interesting changes to the approach, where we would have indexings such as
1479$$i_0\mapsto n - i_0\quad\text{or}\quad i_0\mapsto i_1, i_1\mapsto i_0.$$
1480In particular dependency over actual variables of the code would enter the
1481frame, as indexings would depend on the number of iterations of a well-behaving
1482guarded loop (the $n$ in the first example).
1483
1484Finally, as stated in the introduction, the approach should allow integrating
1485some techniques for cache analysis, a possibility that for now has been put aside
1486as the standard 8051 architecture targeted by the CerCo project has no cache.
1487As possible developments of this line of work without straying from the 8051
1488architecture, two possibilities present themselves.
1489\begin{enumerate}
1490 \item One could extend the development to some 8051 variants, of which some have
1491  been produced with a cache.
1492 \item One could make the compiler implement its own cache: this cannot
1493  apply to RAM accesses of the standard 8051 architecture, as the difference in
1494  cost of accessing the two types of RAM is of just 1 clock cycle, which makes
1495  any implementation of cache counterproductive. So this possibility should
1496  either artificially change the accessing cost of RAM of the model just for the
1497  sake of possible future adaptations to other architectures, or otherwise
1498  model access to an external memory by means of the serial port.\end{enumerate}
1499
1500
1501%
1502% \newpage
1503%
1504% \includepdf[pages={-}]{plugin.pdf}
1505%
1506%
1507% \newpage
1508%
1509% \includepdf[pages={-}]{fopara.pdf}
1510%
1511%
1512% \newpage
1513%
1514% \includepdf[pages={-}]{tlca.pdf}
1515%
1516% \bibliographystyle{plain}
1517\bibliography{bib}
1518
1519\end{document}
Note: See TracBrowser for help on using the repository browser.