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

Last change on this file since 1676 was 1676, checked in by tranquil, 7 years ago

corrected some faults
still TODO: running example, language corrections

File size: 67.1 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 one, 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 one, optional but desirable, is \emph{preciseness}: the estimate
644\emph{is} 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 before hitting another one. In simple
647architectures such as the 8051
648micro-controller this can be guaranteed by having labels at the immediate start of any
649branch of the control flow, and by ensuring no duplicate labels are present.
650
651It should be underlined that the above mentioned requirements must hold when
652executing the code obtained at the
653end of the compilation chain. So even If one is careful injecting the labels at good
654key places in the source code, the requirements might still fail because of two main obstacles:
655\begin{itemize}
656 \item compilation introduces important changes in the control flow, inserting
657loops or branches: an example in addressing this is the insertion of functions
658in the source code replacing instructions unavailable in the target architecture
659and that require loops to be carried out (e.g.\ multi-word division and generic
660shift in the 8051 architecture), or the effort put in
661providing unbranching translations of higher level instructions~
662\cite{D2.2};
663 \item even if the compiled code \emph{does}, as long as the the syntactic
664  control flow graph is concerned, respect the conditions for soundness and
665  preciseness, the cost of blocks of instructions might not be independent of context,
666  so that different passes through a label might have different costs: this
667  becomes a concern if one wishes to apply the approach to more complex architectures,
668  for example one with cache or pipelining.
669\end{itemize}
670
671The first point unveils a weakness of the current labelling approach when it
672comes to some common code transformations done along a compilation chain. In
673particular most of \emph{loop optimizations} disrupt such conditions directly.
674In what we will call \emph{loop peeling}, for example, a first iteration of the
675loop is hoisted ahead of it, possibly to have a different cost than later iterations
676because of further transformation such as dead code elimination or invariant
677code motion.
678
679The second point strikes a difference in favour of existing tools for the
680estimate of execution costs and to the detriment of CerCo's approach advocated in~
681\cite{D2.1}. We will take as an example the well known tool \s{aiT}~\cite{absint},
682based on abstract interpretation: such a tool allows to estimate the
683worst-case execution time (WCET) taking into account advanced aspects of the
684target architecture. \s{aiT}'s ability to
685do close estimates of execution costs even when these depend on the context of
686execution would enhance the effectiveness of CerCo's compiler, either by
687integrating such techniques in its development, or by directly calling this tool
688when ascertaining the cost of blocks of compiled code. A typical case where
689cache analysis yields a difference in the execution cost of a block is in loops:
690the first iteration will usually stumble upon more cache misses than subsequent
691iterations.
692
693If one looks closely, the source of the weakness of the labelling approach as
694presented in~\cite{D2.1} is common to both points: the inability to state
695different costs for different occurrences of labels, where the difference
696might be originated by labels being duplicated along the compilation
697or the costs being sensitive to the current state of execution.
698
699The preliminary work
700we present here addresses this weakness by introducing cost labels that are dependent
701on which iteration of its containing loops it occurs in. This is achieved by
702means of \emph{indexed labels}: all cost labels are decorated with formal
703indexes coming from the loops containing such labels. These indexes allow to
704rebuild, even after several steps of loop transformations,
705which iterations of the original loops in the source code a particular label
706occurrence belongs to. During annotation of source code, this information
707is given to the user by means of dependent costs.
708
709We concentrate on integrating the labelling approach with two loop transformations.
710For general information on compiler optimization (and loop optimizations in
711particular) we refer the reader to the vast literature on the subject
712(e.g.~\cite{muchnick,morgan}).
713
714\emph{Loop peeling}, as already mentioned, consists in preceding the loop with
715a copy of its body, appropriately guarded. This is in general useful to trigger
716further optimizations, such as ones relying on execution information which can
717be computed at compile time but which is erased by further iterations of the loop,
718or ones that use the hoisted code to be more effective at eliminating redundant
719code. Integrating this transformation to the labelling approach would also allow
720to integrate the common case of cache analysis explained above: the analysis
721of cache hits and misses usually benefits from a form of
722\emph{virtual} loop peeling~\cite{cacheprediction}.
723
724\emph{Loop unrolling} consists in repeating several times the body of the loop
725inside the loop itself (inserting appropriate guards, or avoiding them altogether
726if enough information on the loop's guard is available at compile time). This
727can limit the number of (conditional or unconditional) jumps executed by the
728code and trigger further optimizations dealing with pipelining, if applicable
729to the architecture.
730
731While covering only two loop optimizations, the work presented here poses good
732bases to extending the labelling approach to cover more and more of them, as well
733as giving hints as to how integrating in CerCo's compiler advanced cost estimation
734techniques such as cache analysis. Moreover loop peeling has the substantial
735advantage of enhancing other optimizations. Experimentation with CerCo's
736untrusted prototype compiler with constant propagation and
737partial redundancy elimination~\cite{PRE,muchnick} show how loop peeling enhances
738those other optimizations.
739
740\paragraph{Outline.}
741We will present our approach on a minimal toy imperative language, \imp{}
742with gotos, which we present in \autoref{sec:defimp} along with formal
743definition of the loop transformations. This language already
744presents most of the difficulties encountered when dealing with C, so
745we stick to it for the sake of this presentation. In \autoref{sec:labelling}
746we summarize the labelling approach as presented in~\cite{D2.1}. The following
747\autoref{sec:indexedlabels} explains \emph{indexed labels}, our proposal for
748dependent labels which are able to describe precise costs even in the presence
749of the loop transformations we consider. Finally \autoref{sec:conc} goes into
750more details regarding the implementation of indexed labels in CerCo's
751untrusted compiler and speculates on further work on the subject.
752
753
754\section{\imp{} with goto}\label{sec:defimp}
755We briefly outline the toy language which contains all the relevant instructions
756to present the development and the problems it is called to solve.
757
758The version of the minimal imperative language \imp{} that we will present has,
759with respect to the bare-bone usual version, \s{goto}s and labelled statements.
760Break and continue statements can be added at no particular expense. Its syntax
761and operational semantics is presented in \autoref{fig:minimp}.
762\begin{figureplr}
763$$\begin{gathered}
764\begin{array}{nlBl>(R<)n}
765\multicolumn{4}{C}{\bfseries Syntax}\\
766\multicolumn{4}{ncn}{
767  \ell,\ldots \hfill \text{(labels)} \hfill x,y,\ldots \hfill
768\text{(identifiers)}
769\hfill e,f,\ldots \hfill \text{(expression)}
770}\\
771P,S,T,\ldots &\gramm& \s{skip} \mid s;t
772\mid \sop{if}e\sbin{then}s\sbin{else}t
773\mid \sop{while} e \sbin{do} s \mid
774  x \ass e
775\\&\mid&
776\ell : s \mid \sop{goto}\ell& \spanr{-2}{statements}\\
777\\
778\multicolumn{4}{C}{\bfseries Semantics}\\
779K,\ldots  &\gramm& \s{halt} \mid S \cdot K & continuations
780\end{array}
781\\[15pt]
782\s{find}(\ell,S,K) \ass
783\left\{\begin{array}{lL}
784\bot & if $S=\s{skip},\sop{goto} \ell'$ or $x\ass e$,\\
785(T, K) & if $S=\ell:T$,\\
786\s{find}(\ell,T,K) & otherwise, if $S = \ell':T$,\\
787\s{find}(\ell,T_1,T_2\cdot K) & if defined and $S=T_1;T_2$,\\
788\s{find}(\ell,T_1,K) & if defined and
789$S=\sop{if}b\sbin{then}T_1\sbin{else}T_2$,\\
790\s{find}(\ell,T_2,K) & otherwise, if $S=T_1;T_2$ or
791$\sop{if}b\sbin{then}T_1\sbin{else}T_2$,\\
792\s{find}(\ell,T,S\cdot K) & if $S = \sop{while}b\sbin{do}T$.
793\end{array}\right.
794\\[15pt]
795\begin{array}{lBl}
796(x:=e,K,s)  &\to_P& (\s{skip},K,s[v/x]) \qquad\mbox{if }(e,s)\eval v \\ \\
797
798(S;T,K,s)  &\to_P& (S,T\cdot K,s) \\ \\
799
800(\s{if} \ b \ \s{then} \ S \ \s{else} \ T,K,s)
801&\to_P&\left\{
802\begin{array}{ll}
803(S,K,s) &\mbox{if }(b,s)\eval v \neq 0 \\
804(T,K,s) &\mbox{if }(b,s)\eval 0
805\end{array}
806\right. \\ \\
807
808
809(\s{while} \ b \ \s{do} \ S ,K,s)
810&\to_P&\left\{
811\begin{array}{ll}
812(S,\s{while} \ b \ \s{do} \ S \cdot K,s) &\mbox{if }(b,s)\eval v \neq 0 \\
813(\s{skip},K,s) &\mbox{if }(b,s)\eval 0
814\end{array}
815\right. \\ \\
816
817
818(\s{skip},S\cdot K,s)  &\to_P&(S,K,s) \\ \\
819
820(\ell : S, K, s)  &\to_P& (S,K,s) \\ \\
821
822(\sop{goto}\ell,K,s)  &\to_P& (\s{find}(\ell,P,\s{halt}),s) \\ \\
823\end{array}
824\end{gathered}$$
825\caption{The syntax and operational semantics of \imp.}
826\label{fig:minimp}
827\end{figureplr}
828The actual
829grammar for expressions is not particularly relevant so we do not give a
830precise one. For the sake of conciseness we also treat boolean and
831arithmetic expressions together (with the usual convention of an expression
832being true iff non-zero). We may omit the \s{else} clause of a conditional
833if it leads to a \s{skip} statement.
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 function 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 single-entry loop detection which
855avoids the multi-entry ones from being targeted by optimizations~\cite{muchnick,morgan}.
856The loop transformations we present are local, i.e.\ they target a single loop
857and transform it. Which loops are targeted may be decided by an \emph{ad hoc}
858heuristic, however this is not important here.
859
860
861\paragraph{Loop peeling.}
862$$
863\sop{while}b\sbin{do}S\mapsto
864\sop{if}b\sbin{then} S; \sop{while} b \sbin{do} S[\ell'_i/\ell_i]
865$$
866where $\ell'_i$ is a fresh label for any $\ell_i$ labelling a statement in $S$.
867This relabelling is safe as to \s{goto}s external to the loop because of the
868single-entry condition. Notice that in case of break and continue statements,
869those should be replaced with \s{goto}s in the peeled body $S$.
870
871\paragraph{Loop unrolling.}
872$$
873\sop{while}b\sbin{do}S\mapsto
874\sop{while} b \sbin{do} (S ;
875  \sop{if} b \sbin{then} (S[\ell^1_i/\ell_i] ;
876  \cdots
877  \sop{if} b \sbin{then} S[\ell^n_i/\ell_i]) \cdots)
878$$
879where $\ell^j_i$ are again fresh labels for any $\ell_i$ labelling a statement
880in $S$. This is a willingly naïf version of loop unrolling, which usually
881targets less general loops. The problem it poses to Cerco's labelling approach
882are independent of the cleverness of the actual transformation.
883
884\section{Labelling: a quick sketch of the previous approach}\label{sec:labelling}
885Plainly labelled \imp{} is obtained adding to the code \emph{cost labels}
886(with metavariables $\alpha,\beta,\ldots$), and cost-labelled statements:
887$$S,T\gramm \cdots \mid \alpha: S$$
888Cost labels allow for some program points to be tracked along the compilation
889chain. For further details we refer to\cite{D2.1}.
890
891With labels the small step semantics turns into a labelled transition
892system and a natural notion of trace (i.e.\ lists of labels) arises.
893Evaluation of statements is enriched with traces, so that rules are like
894$$
895\begin{array}{lblL}
896(\alpha: S, K,s) &\to[\alpha]_P (S,K,s)\\
897(\s{skip}, S \cdot K,s) &\to[\varepsilon]_P (S, K, s)\\
898& \text{etc.}
899\end{array}$$
900where we identify cost labels $\alpha$ with singleton traces and we use $\varepsilon$
901for the empty trace. Cost labels are emitted by cost-labelled statements only%
902\footnote{In the general case the evaluation of expressions can emit cost labels
903too (see \autoref{sec:conc}).}. We then write $\to[\lambda]\!\!^*$ for the transitive
904closure of the small step semantics which produces by concatenation the trace
905$\lambda$.
906
907\paragraph{Labelling.}
908Given an \imp{} program $P$ its \emph{labelling} $\alpha:\Ell(P)$ in $\ell-\imp$
909is
910defined by putting cost labels after every branching, at the start of both
911branches, and a cost label at the beginning of the program. So the relevant
912cases are
913$$\begin{aligned}
914  \Ell(\sop{if}e\sbin{then}S\sbin{else}T) &=
915    \sop{if}e\sbin{then}\alpha:\Ell(S)\sbin{else}\beta:\Ell(T)\\
916  \Ell(\sop{while}e\sbin{do}S) &=
917    (\sop{while}e\sbin{do}\alpha:\Ell(S));\beta:\s{skip}
918  \end{aligned}$$
919where $\alpha,\beta$ are fresh cost labels, and while in other cases the
920definition just passes to sub-statements.
921
922\paragraph{Labels in the rest of the compilation chain.} All languages further
923down the chain get a new sequential statement $\sop{emit}\alpha$ whose effect is
924to be consumed in a labelled transition while keeping the same state. All other
925instructions guard their operational semantics and do not emit cost labels.
926
927Preservation of semantics throughout the compilation process is restated, in
928rough terms, as
929$$\text{starting state of $P$}\to[\lambda]\!\!^*\;\text{halting state} \iff
930  \text{starting state of $\mathcal C(P)$} \to[\lambda]\!\!^*\;\text{halting state},$$
931where $P$ is a program of a language along the compilation chain, starting and
932halting states depend on the language, and $\mathcal C$ is the
933compilation function\footnote{The case of divergent computations needs
934to be addressed too. Also, the requirement can be weakened by demanding some
935sort of equivalence of the traces rather than equality. Both these issues escape
936the scope of this presentation.}.
937
938\paragraph{Instrumentations}
939Let $\mathcal C$ be the whole compilation from $\ell\imp$ to the labelled
940version of some low-level language $L$. Supposing such compilation has not
941introduced any new loop or branching, we have that
942\begin{itemize}
943 \item every loop contains at least a cost label (\emph{soundness condition}),
944and
945 \item every branching has different labels for the two branches
946  (\emph{preciseness condition}).
947\end{itemize}
948With these two conditions, we have that each and every cost label in
949$\mathcal C(P)$ for any $P$ corresponds to a block of sequential instructions,
950to which we can assign a constant \emph{cost}\footnote{This in fact requires the
951machine architecture to be simple enough, or for some form of execution analysis
952to take place.} We can therefore assume a \emph{cost mapping} $\kappa_P$ from
953cost labels to natural numbers, assigning to each cost label $\alpha$ the cost
954of the block containing the single occurrance of $\alpha$.
955
956Given any cost mapping $\kappa$, we can enrich a labelled program so that a
957particular fresh variable (the \emph{cost variable} $c$) keeps track of the
958assumulation of costs during the execution. We call this procedure
959\emph{instrumentation} of the program, and it is defined recursively by
960$$
961  \mathcal I(\alpha:S) = c \ass c + \kappa(\alpha) ; \mathcal I(S)
962$$
963while in all other cases the definition passes to substatements.
964
965\paragraph{The problem with loop optimizations.}
966Let us take loop peeling, and apply it to the labelling of a program without any
967adjustment:
968$$
969(\sop{while}e\sbin{do}\alpha:S);\beta:\s{skip}
970\mapsto
971(\sop{if}b\sbin{then} \alpha : S; \sop{while} b \sbin{do} \alpha :
972S[\ell'_i/\ell_i]);
973\beta:\s{skip}$$
974What happens is that the cost label $\alpha$ is duplicated into two distinct
975occurrences. If these two occurrences correspond to different costs in the
976compiled code, the best the cost mapping can do is to take the maximum of the
977two, preserving soundness (i.e.\ the cost estimate still bounds the actual one)
978but loosing preciseness (i.e.\ the actual cost would be strictly less than its
979estimate).
980
981\section{Indexed labels}\label{sec:indexedlabels}
982This section presents the core of the new approach. In brief points it amounts
983to the following.
984\begin{enumerate}[\bfseries \ref*{sec:indexedlabels}.1.]
985 \item\label{en:outline1}
986Enrich cost labels with formal indexes corresponding, at the beginning of
987the process, to which iteration of the loop they belong to.
988 \item\label{en:outline2}
989Each time a loop transformation is applied and a cost labels is split in
990different occurrences, each of these will be reindexed so that every time they
991are emitted their position in the original loop will be reconstructed.
992 \item\label{en:outline3}
993Along the compilation chain, add alongside the \s{emit} instruction other
994ones updating the indexes, so that iterations of the original loops can be
995rebuilt at the operational semantics level.
996 \item\label{en:outline4}
997The machinery computing the cost mapping will still work, but assigning
998costs to indexed cost labels, rather than to cost labels as we wish: however
999\emph{dependent costs} can be calculated, where dependency is on which iteration
1000of the containing loops we are in.
1001\end{enumerate}
1002
1003\subsection{Indexing the cost labels}\label{ssec:indlabs}
1004\paragraph{Formal indexes and $\iota\ell\imp$.}
1005Let $i_0,i_1,\ldots$ be a sequence of distinguished fresh identifiers that will
1006be used as loop indexes. A \emph{simple expression} is an affine arithmetical
1007expression in one of these indexes, that is $a*i_k+b$ with $a,b,k \in \mathbb N$.
1008Simple expressions $e_1=a_1*i_k+b_1$, $e_2=a2*i_k+b_2$ in the same index can be
1009composed, yielding $e_1\circ e_2\ass (a_1a_2)*i_k + (a_1b2+b_1)$, and this operation
1010has an identity element in $id_k \ass 1*i_k+0$. Constants can be expressed as simple
1011expressions, so that we identify a natural $c$ with $0*i_k+c$.
1012
1013An \emph{indexing} (with metavariables $I$, $J$, \ldots) is a list of
1014transformations of successive formal indexes dictated by simple expressions,
1015that is a mapping%
1016\footnote{Here we restrict each mapping to be a simple expression
1017\emph{on the same index}. This might not be the case if more loop optimizations
1018are accounted for (for example, interchanging two nested loops).}
1019$$i_0\mapsto a_0*i_0+b_0,\dots, i_{k-1} \mapsto a_{k-1}*i_{k-1}+b_{k-1}.$$
1020
1021An \emph{indexed cost label} (metavariables $\alphab$, $\betab$, \ldots) is
1022the combination of a cost label $\alpha$ and an indexing $I$, written
1023$\alpha\la I\ra$. The cost label underlying an indexed one is called its
1024\emph{atom}. All plain labels can be considered as indexed ones by taking
1025an empty indexing.
1026
1027\imp{} with indexed labels ($\iota\ell\imp$) is defined by adding to $\imp$
1028statements with indexed labels, and by having loops with formal indexes
1029attached to them:
1030$$S,T,\ldots \gramm \cdots i_k:\sop{while}e\sbin{do}S\mid \alphab : S.$$
1031Notice than unindexed loops still are in the language: they will correspond
1032to multi-entry loops which are ignored by indexing and optimizations.
1033We will discuss the semantics later.
1034
1035\paragraph{Indexed labelling.}
1036Given an $\imp$ program $P$, in order to index loops and assign indexed labels
1037we must first of all distinguish single-entry loops. We just sketch how it can
1038be computed.
1039
1040A first pass of the program $P$ can easily compute two maps: $\s{loopof}_P$
1041from each label $\ell$ to the occurrence (i.e.\ the path) of a $\s{while}$ loop
1042containing $\ell$, or the empty path if none exists; and $\s{gotosof}_P$ from
1043a label $\ell$ to the occurrences of \s{goto}s pointing to it. Then the set
1044$\s{multientry}_P$ of multi-entry loops of $P$ can be computed by
1045$$\s{multientry}_P\ass\{\, p \mid \exists \ell,q.p =\s{loopof}_P(\ell),q\in\s{gotosof}_P(\ell), q \not\le p\,\}$$
1046where $\le$ is the prefix relation\footnote{Possible simplification to this
1047procedure include keeping track just of while loops containing labels and
1048\s{goto}s (rather than paths in the syntactic tree of the program), and making
1049two passes while avoiding building the map to sets $\s{gotosof}$}.
1050
1051Let $Id_k$ be the indexing of length $k$ made from identity simple expressions,
1052i.e.\ the sequence $i_0\mapsto id_0, \ldots , i_{k-1}\mapsto id_{k-1}$. We define the tiered indexed labelling
1053$\Ell^\iota_P (S,k)$ in program $P$ for occurrence $S$ of a statement in $P$
1054and a natural $k$ by recursion, setting
1055$$
1056\Ell^\iota_P(S,k)\ass
1057\left\{
1058\begin{array}{lh{-100pt}l}
1059 (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}
1060\\& \text{if $S=\sop{while}b\sbin{do}T$ and $S\notin \s{multientry}_P$,}\\[3pt]
1061(\sop{while}b\sbin{do}\alpha\la Id_k \ra : \Ell^\iota_P(T,k));\beta\la Id_k \ra : \s{skip}
1062\\& \text{otherwise, if $S=\sop{while}b\sbin{do}T$,}\\[3pt]
1063\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)
1064\\&\text{if $S=\sop{if}b\sbin{then}T_1\sbin{else}T_2$,}\\[3pt]
1065\ldots
1066\end{array}
1067\right.
1068$$
1069where as usual $\alpha$ and $\beta$ are to be fresh cost labels, and other cases just keep
1070making the recursive calls on the substatements. The \emph{indexed labelling} of
1071a program $P$ is then defined as $\alpha\la \ra : \Ell^\iota_P(P,0)$, i.e.\ a
1072further fresh unindexed cost label is added at the start, and we start from level $0$.
1073
1074In other words: each single-entry loop is indexed by $i_k$ where $k$ is the number of
1075other single-entry loops containing this one, and all cost labels under the scope
1076of a single-entry loop indexed by $i_k$ are indexed by all indexes $i_0,\ldots,i_k$,
1077without any transformation.
1078
1079\subsection{Indexed labels and loop transformations}
1080We define the \emph{reindexing} $I \circ (i_k\mapsto a*i_k+b)$ as an operator
1081on indexings by setting
1082\begin{multline*}
1083(i_0\mapsto e_0,\ldots, i_k \mapsto e_k,\ldots,i_n\mapsto e_n)
1084\circ(i_k\mapsto a*i_k+b)
1085\ass\\
1086i_0\mapsto e_0,\ldots, i_k \mapsto e_k \circ(a*i_k+b),\ldots,i_n\mapsto e_n,
1087\end{multline*}
1088and extending then to indexed labels (by $\alpha\la I\ra\circ(i_k\mapsto e)\ass
1089\alpha\la I\circ (i_k\mapsto e)\ra$) and to statements in $\iota\ell\imp$
1090(by applying the above transformation to all indexed labels).
1091
1092We can then redefine loop peeling and loop unrolling taking into account indexed labels.
1093It will be possible to apply the transformation only to indexed loops, that is loops
1094that are single-entry. The attentive reader will notice that no assumption is
1095made on the labelling of the statements involved. In particular the transformation
1096can be repeated and composed at will. Also, notice that erasing all labelling
1097information (i.e.\ indexed cost labels and loop indexes) we recover exactly the
1098same transformations presented in \autoref{sec:defimp}.
1099
1100\paragraph{Indexed loop peeling.}
1101
1102$$
1103i_k:\sop{while}b\sbin{do}S\mapsto
1104\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)
1105$$
1106As can be expected, the peeled iteration of the loop gets reindexed as always
1107being the first iteration of the loop, while the iterations of the remaining
1108loop get shifted by $1$.
1109
1110\paragraph{Indexed loop unrolling.}
1111$$
1112\begin{array}{l}
1113\begin{array}{ncn}
1114i_k:\sop{while}b\sbin{do}S\\
1115\tikz\node[rotate=-90,inner sep=0pt]{$\mapsto$};
1116\end{array}\\
1117i_k:\sop{while} b \sbin{do}\\
1118\quad (S\circ(i_k\mapsto n*i_k) ;\\
1119\quad \sop{if} b \sbin{then}\\
1120\quad\quad (S[\ell^1_i/\ell_i]\circ(i_k\mapsto n*i_k+1) ;\\
1121\quad\quad\quad \vdots \\
1122\quad\quad \quad \sop{if} b \sbin{then}\\
1123\quad \quad \quad \quad S[\ell^n_i/\ell_i]\circ(i_k\mapsto n*i_k+n-1)
1124)\cdots )
1125\end{array}
1126$$
1127Again, the reindexing is as can be expected: each copy of the unrolled body
1128has its indexes remapped so that when they are executed the original iteration
1129of the loop to which they correspond can be recovered.
1130
1131\subsection{Semantics and compilation of indexed labels}
1132
1133In order to make sense of loop indexes, one must keep track of their values
1134in the state. A \emph{constant indexing} (metavariables $C,\ldots$) is an
1135indexing which employs only constant simple expressions. The evaluation
1136of an indexing $I$ in a constant indexing $C$, noted $I|_C$, is defined
1137by
1138$$I\circ(i_0\mapsto c_0,\ldots, i_{k-1}\mapsto c_{k-1}) \ass
1139  \alphab\circ(i_0\mapsto c_0)\circ\cdots\circ(i_{k-1}\mapsto c_{k-1})$$
1140(using the definition of ${-}\circ{-}$ given in \autoref{ssec:indlabs}), considering it defined only
1141if the the resulting indexing is a constant one too\footnote{For example
1142$(i_0\mapsto 2*i_0,i_1\mapsto i_1+1)|_{i_0\mapsto 2}$ is undefined,
1143but $(i_0\mapsto 2*i_0,i_1\mapsto 0)|_{i_0\mapsto 2}=
1144i_0\mapsto 4,i_1\mapsto 2$, which is indeed a constant indexing,
1145even if the domain of the original indexing is not covered by the constant one.}.
1146The definition is extended to indexed labels by $\alpha\la I\ra|_C\ass \alpha\la I|_C\ra$.
1147
1148Constant indexings will be used to keep track of the exact iterations of the
1149original code the emitted labels belong to. We thus define two basic actions to
1150update constant indexings: $C[i_k{\uparrow}]$ which increments the value of
1151$i_k$ by one, and $C[i_k{\downarrow}0]$ which resets it to $0$.
1152
1153We are ready to update the definition of the operational semantics of
1154indexed labelled \imp. The emitted cost labels will now be ones indexed by
1155constant indexings. We add a special indexed loop construct for continuations
1156that keeps track of active indexed loop indexes:
1157$$K,\ldots  \gramm \cdots | i_k:\sop{while} b \sbin {do} S \sbin{then}  K$$
1158The difference between the regular stack concatenation
1159$i_k:\sop{while}b\sbin{do}S\cdot K$ and the new constructor is that the latter
1160indicates the loop is the active one in which we already are, while the former
1161is a loop that still needs to be started%
1162\footnote{In the presence of \s{continue} and \s{break} statements active
1163loops need to be kept track of in any case.}.
1164The \s{find} function is updated accordingly with the case
1165$$ \s{find}(\ell, i_k:\sop{while}b\sbin{do}S, K) \ass \s{find}(\ell, S, i_k:
1166  \sop{while}b\sbin{do}S\sbin{then}K).$$
1167The state will now be a 4-uple
1168$(S,K,s,C)$ which adds a constant indexing to the 3-uple of regular
1169semantics. The small-step rules for all statements but the
1170cost-labelled ones and the indexed loops remain the same, without
1171touching the $C$ parameter (in particular unindexed loops behave the same
1172as usual). The remaining cases are:
1173$$\begin{aligned}
1174   (\alphab : S,K,s,C) &\to[\alphab|_C]_P (S,K,s,C)\\
1175   (i_k:\sop{while}b\sbin{do}S,K,C) &\to[\varepsilon]_P
1176    \begin{cases}
1177     (S,i_k:\sop{while}b\sbin{do}S\sbin{then} K,s,C[i_k{\downarrow}0])
1178     \\\hskip 125pt \text{if $(b,s)\eval v\neq 0$,}\\
1179     \rlap{(\s{skip}, K, s, C)}\hskip 125pt \text{otherwise}
1180    \end{cases}\\
1181   (\s{skip}, i_k:\sop{while}b\sbin{do}S\sbin{then}K,C) &\to[\varepsilon]_P
1182    \begin{cases}
1183     (S,i_k:\sop{while}b\sbin{do}S\sbin{then} K,s,C[i_k{\uparrow}])
1184      \\\hskip 125pt \text{if $(b,s)\eval v\neq 0$,}\\
1185     \rlap{(\s{skip}, K, s, C)} \hskip 125pt \text{otherwise}
1186    \end{cases}
1187  \end{aligned}$$
1188Some explications are in order.
1189\begin{itemize}
1190 \item Emitting a label always instantiates it with the current indexing.
1191 \item Hitting an indexed loop the first time initializes to 0 the corresponding
1192  index; continuing the same loop inrements the index as expected.
1193 \item The \s{find} function ignores the current indexing: this is correct
1194  under the assumption that all indexed loops are single entry ones, so that
1195  when we land inside an indexed loop with a \s{goto}, we are sure that its
1196  current index is right.
1197  \item The starting state with store $s$ for a program $P$ is
1198$(P,\s{halt},s,(i_0\mapsto 0,\dots,i_{n-1}\mapsto 0)$ where $i_0,\ldots,i_{n-1}$ cover
1199all loop indexes of $P$\footnote{For a program which is the indexed labelling of an
1200\imp{} one this corresponds to the maximum nesting of single-entry loops. We can also
1201avoid computing this value in advance if we define $C[i{\downarrow}0]$ to extend
1202$C$'s domain as needed, so that the starting constant indexing can be the empty one.}.
1203\end{itemize}
1204
1205\paragraph{Compilation.}
1206Further down the compilation chain the loop
1207structure is usually partially or completely lost. We cannot rely on it anymore
1208to ensure keeping track of original source code iterations. We therefore add
1209alongside the \s{emit} instruction two other sequential instructions
1210$\sop{ind_reset}k$ and $\sop{ind_inc}k$ whose sole effect is to reset to
12110 (resp.\ increment by 1) the loop index $i_k$, as kept track of in a constant
1212indexing accompanying the state.
1213
1214The first step of compilation from $\iota\ell\imp$ consists in prefixing the
1215translation of an indexed loop $i_k:\s{while}\ b\ \s{do}\ S$ with
1216$\sop{ind_reset}k$ and postfixing the translation of its body $S$ with
1217$\sop{ind_inc}k$. Later on in the compilation chain we just need to propagate
1218the instructions dealing with cost labels.
1219
1220We would like to stress the fact that this machinery is only needed to give a
1221suitable semantics of observables on which preservation proofs can be done. By no
1222means the added instructions and the constant indexing in the state are meant
1223to change the actual (let us say denotational) semantics of the programs. In this
1224regard the two new instruction have a similar role as the \s{emit} one. A
1225forgetful mapping of everything (syntax, states, operational semantics rules)
1226can be defined erasing all occurrences of cost labels and loop indexes, and the
1227result will always be a regular version of the language considered.
1228
1229\paragraph{Stating the preservation of semantics.} In fact, the statement of preservation
1230of semantics does not change at all, if not for considering traces of evaluated
1231indexed cost labels rather than traces of plain ones.
1232
1233
1234\subsection{Dependent costs in the source code}\label{ssec:depcosts}
1235The task of producing dependent costs out of the constant costs of indexed labels
1236is quite technical. Before presenting it here, we would like to point out that
1237the annotations produced by the procedure described in this subsection, even
1238if correct, can be enormous and unreadable. In \autoref{sec:conc}, when we will
1239detail the actual implementation, we will also sketch how we mitigated this
1240problem.
1241
1242Having the result of compiling the indexed labelling $\Ell^\iota(P)$ of an \imp{}
1243program $P$, we can still suppose that a cost mapping can be computed, but
1244from indexed labels to naturals. We want to annotate the source code, so we need
1245a way to express and compute costs of cost labels, i.e.\ group the costs of
1246indexed labels to ones of their atoms. In order to do so we introduce
1247\emph{dependent costs}. Let us suppose that for the sole purpose of annotation,
1248we have available in the language ternary expressions of the form
1249$$\tern e {f_1}{f_2},$$
1250and that we have access to common operators on integers such as equality, order
1251and modulus.
1252
1253\paragraph{Simple conditions.}
1254First, we need to shift from \emph{transformations} of loop indexes to
1255\emph{conditions} on them. We identify a set of conditions on natural numbers
1256which are able to express the image of any composition of simple expressions.
1257
1258\emph{Simple conditions} are of three possible forms:
1259\begin{itemize}
1260 \item equality $i_k=n$ for some natural $n$;
1261 \item inequality $i_k\ge n$ for some natural $n$;
1262 \item modular equality together with inequality $i_k\bmod a = b\wedge i_k\ge n$
1263  for naturals $a, b, n$.
1264\end{itemize}
1265The always true simple condition is given by $i_k\ge 0$, and similarly we
1266write $i_k\bmod a = b$ as a simple condition for $i_k\bmod a = b\wedge i_k\ge 0$.
1267Given a simple condition $p$ and a constant indexing $C$ we can easily define
1268when $p$ holds for $C$ (written $p\circ C$). A \emph{dependent cost expression}
1269is an expression built solely out of integer constants and ternary expressions
1270with simple conditions at their head. Given a dependent cost expression $e$ where
1271all of the loop indexes appearing in it are in the domain of a constant indexing
1272$C$, we can define the value $e\circ C\in \mathbb N$ by
1273$$n\circ C\ass n,\qquad (\tern p e f)\circ C\ass
1274\begin{cases}
1275  e\circ C& \text{if $p\circ C$,}\\
1276  f\circ C& \text{otherwise.}
1277\end{cases}$$
1278
1279\paragraph{From indexed costs to dependent ones.}
1280Every simple expression $e$ corresponds to a simple condition $p(e)$ which expresses the
1281set of values that can be the result of it. Following is the definition of such
1282relation. We recall that in this development loop indexes are always mapped to
1283simple expressions over the same index. If it was not the case, the condition
1284obtained from an expression should be on the mapped index, not the indeterminate
1285of the simple expression. We leave to further work all generalizations of what
1286we present here.
1287$$
1288p(a*i_k+b)\ass
1289\begin{cases}
1290i_k = b & \text{if $a = 0$,}\\
1291i_k \ge b & \text{if $a = 1$,}\\
1292i_k\bmod a = b \wedge i_k \ge b & \text{otherwise}.
1293\end{cases}$$
1294Now, suppose we are given a mapping $\kappa$ from indexed labels to natural
1295numbers. We will transform it in a mapping (identified with an abuse of notation
1296with the same symbol $\kappa$) from atoms to \imp{} expressions built with
1297ternary expressions which depend solely on loop indexes. To that end we define
1298an auxiliary function $\kappa^\alpha_L$ parameterized by atoms and words of
1299simple expressions and defined on \emph{sets} of $n$-uples of simple expressions
1300(with $n$ constant across each such set, i.e.\ each set is made of words with
1301the same length).
1302
1303We will employ a bijection between words of simple expressions and indexings,
1304given by\footnote{Lists of simple expressions is in fact how indexings are
1305represented in Cerco's current implementation of the compiler.}
1306$$i_0\mapsto e_0,\ldots,i_{k-1}\mapsto e_{k-1} \cong e_0\cdots e_{k-1}.$$
1307As usual, $\varepsilon$ denotes the empty word/indexing, and juxtaposition
1308word concatenation.
1309
1310For every set $s$ of $n$-uples of simple expressions, we are in one of the following
1311three exclusive cases:
1312\begin{itemize}
1313 \item $S=\emptyset$, or
1314 \item $S=\{\varepsilon\}$, or
1315 \item there is a simple expression $e$ such that $S$ can be decomposed in
1316  $eS'+S''$, with $S'\neq \emptyset$ and none of the words in $S''$ starting with $e$
1317\end{itemize}
1318where $eS'$ denotes prepending $e$ to all elements of $S'$ and $+$ is disjoint
1319union. This classification can serve as the basis of a definition by recursion
1320on $n+\card S$ where $n$ is the size of tuples in $S$ and $\card S$ is its cardinality.
1321Indeed in the third case in $S'$ the size of tuples decreases strictly (and
1322cardinality does not increase) while for $S''$ the size of tuples remains the same
1323but cardinality strictly decreases. The expression $e$ of the third case will be chosen
1324as minimal for some total order\footnote{The specific order used does not change
1325the correctness of the procedure, but different orders can give more or less
1326readable results. A ``good'' order is the lexicographic one, with $a*i_k+b \le a'*i_k+b'$
1327if $a<a'$ or $a=a'$ and $b\le b'$.}.
1328
1329Following is the definition of the auxiliary function $\kappa^\alpha_L$, following
1330the recursion scheme presented above.
1331$$
1332\begin{aligned}
1333\kappa^\alpha_L(\emptyset) &\ass 0\\
1334\kappa^\alpha_L(\{\varepsilon\}) &\ass \kappa(\alpha\la L\ra) \\
1335\kappa^\alpha_L(eS'+S'') &\ass \tern{p(e)}{\kappa^\alpha_{Le}(S')}{\kappa^\alpha_L(S'')}
1336\end{aligned}
1337$$
1338
1339Finally, the wanted dependent cost mapping is defined by
1340$$\kappa(\alpha)\ass\kappa^\alpha_\varepsilon(\{\,L\mid \alpha\la L\ra \text{ appears
1341in the compiled code}\,\}).$$
1342
1343\paragraph{Indexed instrumentation.}
1344The \emph{indexed instrumentation} generalizes the instrumentation presented in
1345\autoref{sec:labelling}.
1346We described
1347above how cost atoms can be mapped to dependent costs. The instrumentation must
1348also insert code dealing with the loop indexes. As instrumentation is done
1349on the code produced by the labelling phase, all cost labels are indexed by
1350identity indexings. The relevant cases of the recursive definition
1351(supposing $c$ is the cost variable) are then
1352$$
1353\begin{aligned}
1354\mathcal I^\iota(\alpha\la Id_k\ra:S) &= c\ass c + \kappa(\alpha);\mathcal I^\iota(S)\\
1355\mathcal I^\iota(i_k : \sop{while}b\sbin{do}S) &=
1356  i_k \ass 0; \sop{while}b\sbin{do}(\mathcal I^\iota (S); i_k \ass i_k + 1)
1357\end{aligned}
1358$$
1359
1360\section{Notes on the implementation and further work}\label{sec:conc}
1361Implementing the indexed label approach in CerCo's untrusted OcaML prototype
1362does not introduce many aspects beyond what has already been presented for the toy
1363language \imp{} with \s{goto}s. \s{Clight}, the fragment of \s{C} which is the
1364source language of CerCo's compilation chain~\cite{D2.1}, has several more fetaures,
1365but few demand changes in the indexed labelled approach.
1366\paragraph{Indexed loops vs index update instructions.} In this presentation
1367we had indexed loops in $\iota\ell\imp$, while we hinted at the fact that later
1368languages in the compilation chain would have specific index update instructions.
1369In CerCo's actual compilation chain from \s{Clight} to 8051 assembly, indexed
1370loops are only in \s{Clight}, while from \s{Cminor} onward all languages have
1371the same three cost-involving instructions: label emitting, index resetting and
1372index incrementing.
1373\paragraph{Loop transformations in the front end.} We decided to implement
1374the two loop transformations in the front end, namely in \s{Clight}. This
1375decision is due to user readability concerns: if costs are to be presented to
1376the programmer, they should depend on structures written by the programmer
1377himself. If loop transformation were performed later it would be harder to
1378relate information on loops in the control flow graph with actual loops
1379written in the source code. Another solution would be however to index
1380loops in the source code and then use these indexes later in the compilation
1381chain to pinpoint explicit loops of the source code: loop indexes can be used
1382to preserve such information just like cost labels.
1383\paragraph{Break and continue statements.} \s{Clight}'s loop flow control
1384statements for breaking and continuing a loop are equivalent to appropriate
1385\s{goto} statements. The only difference is that we are assured that they cannot
1386cause loops to be multi-entry, and that when a transformation such as loop
1387peeling is done, they need to be replaced by actual \s{goto}s (which will happen
1388further down the compilation chain anyway).
1389\paragraph{Function calls.} Every internal function definition has its own
1390space of loop indexes. Executable semantics must thus take into account saving
1391and resetting the constant indexing of current loops upon hitting a function
1392call, and restoring it upon return of control. A peculiarity is that this cannot
1393be attached to actions saving and restoring frames: namely in the case of
1394tail calls the constant indexing needs to be saved whereas the frame does not.
1395\paragraph{Cost-labelled expressions.} In labelled \s{Clight} expressions get
1396cost labels too, because of the presence of ternary conditional expressions
1397(and lazy logical operators, which get translated to ternary expressions too).
1398Adapting the indexed labelled approach to cost-labelled expressions does not
1399pose particular problems.
1400\paragraph{Simplification of dependent costs.}
1401As already mentioned, the blind application of the procedure described in
1402\autoref{ssec:depcosts} produces unwieldy cost annotations. In the implementation
1403several transformations are used to simplify such dependent costs.
1404
1405Disjunctions of simple conditions are closed under all logical operations, and
1406it can be computed whether such a disjunction implies a simple condition
1407or its negation. This can be used to eliminate useless branches of dependent costs,
1408to merge branches that have the same value, and possibly to simplify the third
1409case of simple condition. Examples of the three transformations are respectively
1410\begin{itemize}
1411\item $
1412\verb+(_i_0 == 0)?+x\verb+:(_i_0 >= 1)?+y\verb+:+z
1413\mapsto
1414\verb+(_i_0 == 0)?+x\verb+:+y,
1415$
1416\item $
1417c\texttt{?}x\verb+:(+d\texttt{?}x\texttt{:}y\verb+)+
1418\mapsto
1419\texttt{(}c\texttt{ || }d\texttt{)?}x\texttt{:}y,
1420$
1421\item \begin{tabular}[t]{np{\linewidth}n}
1422$\verb+(_i_0 == 0)?+x\verb+:(_i_0 % 2 == 0 && _i_0 >= 2)?+y\verb+:+z
1423\mapsto$ \\\hfill
1424$\verb+(_i_0 == 0)?+x\verb+:(_i_0 % 2 == 0)?+y\verb+:+z.
1425$\end{tabular}
1426\end{itemize}
1427The second transformation tends to accumulate disjunctions, again to the detriment
1428of readability. A further transformation swaps two branches of the ternary
1429expression if the negation of the condition can be expressed with less clauses.
1430An example is
1431$$ \verb+(_i_0 % 3 == 0 || _i_0 % 3 == 1)?+x\verb+:+y \mapsto
1432\verb+(_i_0 % 3 == 2)?+y\verb+:+x.
1433$$
1434
1435\paragraph{Updates to the frama-C cost plugin.}
1436Cerco's frama-C~\cite{framac} cost plugin\todo{is there a reference for this?}{}
1437has been updated to take into account dependent
1438costs. The frama-c framework explodes ternary expressions to actual branch
1439statements introducing temporaries along the way, which makes the task of
1440analyzing ternary cost expressions rather daunting. It was deemed necessary to provide
1441an option in the compiler to use actual branch statements for cost annotations
1442rather than ternary expressions, so that at least frama-C's use of temporaries in
1443cost annotation be avoided. The cost analysis carried out by the plugin now
1444takes into account such dependent costs.
1445
1446The only limitation (which provided
1447a simplification in the code) is that within a dependent cost
1448simple conditions with modulus on the
1449same loop index should not be modulo different numbers, which corresponds to
1450the reasonable limitation of not applying multiple times loop unrolling to
1451the same loops.
1452\paragraph{Further work.}
1453Indexed labels are for now implemented only in the untrusted OcaML compiler,
1454while they are not present yet in the Matita code. Porting them should pose no
1455significant problem, and then the proof effort should begin.
1456
1457Because most of the executable operational semantics of the languages across the
1458front end and the back end are oblivious to cost labels, it should be expected
1459that the bulk of the semantic preservation proofs that still needs to be done
1460will not get any harder because of indexed labels. The only trickier point
1461would be in the translation of \s{Clight} to \s{Cminor}, where we
1462pass from structured indexed loops to atomic instructions on loop indexes.
1463
1464An invariant which should probably be proved and provably preserved along compilation
1465is the non-overlap of indexings for the same atom. Then, supposing cost
1466correctness for the unindexed approach, the indexed one will just need to
1467add the proof that
1468$$\forall C\text{ constant indexing}.\forall \alpha\la I\ra\text{ appearing in the compiled code}.
1469  \kappa(\alpha)\circ (I\circ C) = \kappa(\alpha\la I \ra).$$
1470$C$ represents a snapshot of loop indexes in the compiled code, while
1471$I\circ C$ is the corresponding snapshot in the source code. Semantics preservation
1472will make sure that when with snapshot $C$ we emit $\alpha\la I\ra$ (that is,
1473we have $\alpha\la I\circ C\ra$ in the trace), this means that $\alpha$ must be
1474emitted in the source code with indexing $I\circ C$, so the cost
1475$\kappa(\alpha)\circ (I\circ C)$ applies.
1476
1477Apart from carrying over the proofs, we would like to extend the approach
1478to more loop transformations. Important examples are loop inversion
1479(where a for loop is reversed, usually to make iterations appear as truly
1480independent) or loop interchange (where two nested loops are swapped, usually
1481to have more loop invariants or to enhance strength reduction). This introduces
1482interesting changes to the approach, where we would have indexings such as
1483$$i_0\mapsto n - i_0\quad\text{or}\quad i_0\mapsto i_1, i_1\mapsto i_0.$$
1484In particular dependency over actual variables of the code would enter the
1485frame, as indexings would depend on the number of iterations of a well-behaving
1486guarded loop (the $n$ in the first example).
1487
1488Finally, as stated in the introduction, the approach should allow integrating
1489some techniques for cache analysis, a possibility that for now has been put aside
1490as the standard 8051 architecture targeted by the CerCo project has no cache.
1491As possible developments of this line of work without straying from the 8051
1492architecture, two possibilities present themselves.
1493\begin{enumerate}
1494 \item One could extend the development to some 8051 variants, of which some have
1495  been produced with a cache.
1496 \item One could make the compiler implement its own cache: this cannot
1497  apply to RAM accesses of the standard 8051 architecture, as the difference in
1498  cost of accessing the two types of RAM is of just 1 clock cycle, which makes
1499  any implementation of cache counterproductive. So this possibility should
1500  either artificially change the accessing cost of RAM of the model just for the
1501  sake of possible future adaptations to other architectures, or otherwise
1502  model access to an external memory by means of the serial port.\end{enumerate}
1503
1504
1505%
1506% \newpage
1507%
1508% \includepdf[pages={-}]{plugin.pdf}
1509%
1510%
1511% \newpage
1512%
1513% \includepdf[pages={-}]{fopara.pdf}
1514%
1515%
1516% \newpage
1517%
1518% \includepdf[pages={-}]{tlca.pdf}
1519%
1520% \bibliographystyle{plain}
1521\bibliography{bib}
1522
1523\end{document}
Note: See TracBrowser for help on using the repository browser.