\documentclass[11pt,epsf,a4wide]{article}
\usepackage{../../style/cerco}
\usepackage{pdfpages}
\usepackage{graphics}
% For SLNCS comment above and use
% \documentclass{llncs}
\RequirePackage[latin1]{inputenc}
% Mettre les différents packages et fonctions que l'on utilise
\usepackage[english]{babel}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{xspace}
\usepackage{latexsym}
\usepackage{url}
\usepackage{xspace}
%\usepackage{fancyvrb}
\usepackage[all]{xy}
%packages pour LNCS
%\usepackage{semantic}
%\usepackage{cmll}
% Packages for RR
\usepackage{graphics,color}
\RequirePackage[latin1]{inputenc}
\usepackage{array}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newenvironment{comment}{{\bf MORE WORK:}}
\newenvironment{restate-proposition}[2][{}]{\noindent\textbf{Proposition~{#2}}
\;\textbf{#1}\
}{\vskip 1em}
\newenvironment{restate-theorem}[2][{}]{\noindent\textbf{Theorem~{#2}}\;\textbf{
#1}\
}{\vskip 1em}
\newenvironment{restate-corollary}[2][{}]{\noindent\textbf{Corollary~{#2}}
\;\textbf{#1}\
}{\vskip 1em}
\newcommand{\myparagraph}[1]{\medskip\noindent\textbf{#1}}
\newcommand{\Proofitemb}[1]{\medskip \noindent {\bf #1\;}}
\newcommand{\Proofitemfb}[1]{\noindent {\bf #1\;}}
\newcommand{\Proofitem}[1]{\medskip \noindent $#1\;$}
\newcommand{\Proofitemf}[1]{\noindent $#1\;$}
\newcommand{\Defitem}[1]{\smallskip \noindent $#1\;$}
\newcommand{\Defitemt}[1]{\smallskip \noindent {\em #1\;}}
\newcommand{\Defitemf}[1]{\noindent $#1\;$}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\eqdef}{=_{\text{def}}}
\newcommand{\concat}{\cdot}%%{\mathbin{+}}
\newcommand{\Int}{\mathit{int}}
\newcommand{\nat}{\mathit{nat}}
\newcommand{\String}{\mathit{string}}
\newcommand{\Ident}{\mathit{ident}}
\newcommand{\Block}{\mathit{block}}
\newcommand{\Signature}{\mathit{signature}}
\newcommand{\pc}{\mathit{pc}}
\newcommand{\estack}{\mathit{estack}}
\newcommand{\Error}{\epsilon}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% --------------------------------------------------------------------- %
% Proof rule. %
% --------------------------------------------------------------------- %
\newcommand{\staterule}[3]{%
$\begin{array}{@{}l}%
\mbox{#1}\\%
\begin{array}{c}
#2\\
\hline
\raisebox{0ex}[2.5ex]{\strut}#3%
\end{array}
\end{array}$}
\newcommand{\GAP}{2ex}
\newcommand{\recall}[2]{%
$\begin{array}{c}
#1\\
\hline
\raisebox{0ex}[2.5ex]{\strut}#2%
\end{array}$}
\newcommand{\hbra}{\noindent\hbox to \textwidth{\leaders\hrule height1.8mm
depth-1.5mm\hfill}}
\newcommand{\hket}{\noindent\hbox to \textwidth{\leaders\hrule
height0.3mm\hfill}}
\newcommand{\ratio}{.3}
\newenvironment{display}[1]{\begin{tabbing}
\hspace{1.5em} \= \hspace{\ratio\linewidth-1.5em} \= \hspace{1.5em} \= \kill
\noindent\hbra\\[-.5em]
{\ }\textsc{#1}\\[-.8ex]
\hbox to \textwidth{\leaders\hrule height1.6mm depth-1.5mm\hfill}\\[-.8ex]
}{\\[-.8ex]\hket
\end{tabbing}}
\newcommand{\sbline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.2ex}
\hfill\hspace*{0ex}}}
\newcommand{\sline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.1ex}
\hfill\hspace*{0ex}}}
\newcommand{\sentry}[2]{\>$#1$\>\ \smash[t]{\vrule width 0.2mm height
1.2\baselineskip depth 1.5\baselineskip}\>#2}
\newcommand{\entry}[2]{\>$#1$\>\>#2}
\newcommand{\clause}[2]{$#1$\>\>#2}
\newcommand{\category}[2]{\clause{#1::=}{#2}}
\newcommand{\subclause}[1]{\>\>\>#1}
\newcommand{\redrule}[3]{$#1$\>\>$#2$\>\>\>#3}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% environments
% To be commented for LNCS
\newtheorem{theorem}{Theorem}
\newtheorem{fact}[theorem]{Fact}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{example}[theorem]{Example}
\newtheorem{exercise}[theorem]{Exercise}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{question}[theorem]{Question}
\newtheorem{proviso}[theorem]{Proviso}
\newtheorem{conjecture}[theorem]{Conjecture}
% proofs
\newcommand{\Proof}{\noindent {\sc Proof}. }
\newcommand{\Proofhint}{\noindent {\sc Proof hint}. }
% To be commented for LNCS
\newcommand{\qed}{\hfill${\Box}$}
\newcommand{\EndProof}{\qed}
% figure environment
\newcommand{\Figbar}{{\center \rule{\hsize}{0.3mm}}}
%horizontal thiner line for figures
\newenvironment{figureplr}{\begin{figure}[t] \Figbar}{\Figbar \end{figure}}
%environment for figures
% ************Macros for mathematical symbols*************
% Style
\newcommand{\cl}[1]{{\cal #1}} % \cl{R} to make R calligraphic
\newcommand{\la}{\langle} % the brackets for pairing (see also \pair)
\newcommand{\ra}{\rangle}
\newcommand{\lf}{\lfloor}
\newcommand{\rf}{\rfloor}
\newcommand{\ul}[1]{\underline{#1}} % to underline
\newcommand{\ol}[1]{\overline{#1}} % to overline
\newcommand{\ok}{~ok} % well formed context
% Syntax
\newcommand{\Gives}{\vdash} % in a type judgment
\newcommand{\IGives}{\vdash_{I}} % intuitionistic provability
\newcommand{\AIGives}{\vdash_{{\it AI}}} %affine-intuitionistic provability
\newcommand{\CGives}{\vdash_{C}} % affine-intuitionistic confluent provability
\newcommand{\Models}{\mid \! =} % models
\newcommand{\emptycxt}{\On} % empty context
\newcommand{\subs}[2]{[#1 / #2]}
\newcommand{\sub}[2]{[#2 / #1]} % substitution \sub{x}{U} gives [U/x]
\newcommand{\Sub}[3]{[#3 / #2]#1} % Substitution with three arguments \Sub{V}{x}{U}
\newcommand{\lsub}[2]{#2 / #1} % substitution \lsub{x}{U} gives U/x, to be used in a list.
\newcommand{\impl}{\supset}
\newcommand{\arrow}{\rightarrow} % right thin arrow
\newcommand{\trarrow}{\stackrel{*}{\rightarrow}} % trans closure
%\newcommand{\limp}{\makebox[5mm]{\,$- \! {\circ}\,$}} % linear
% implication
\newcommand{\limp}{\multimap} %linear implication
\newcommand{\bang}{\, !}
% LNCS
%\newcommand{\bang}{\oc}
\newcommand{\limpe}[1]{\stackrel{#1}{\multimap}}
\newcommand{\hyp}[3]{#1:(#2, #3)}
\newcommand{\letm}[3]{{\sf let} \ ! #1 = #2 \ {\sf in} \ #3} % modal let
\newcommand{\lets}[3]{{\sf let} \ #1 = #2 \ {\sf in} \ #3} % simple let
\newcommand{\letp}[3]{{\sf let} \ \S #1 = #2 \ {\sf in} \ #3} % paragraph let
\newcommand{\tertype}{{\bf 1}}
\newcommand{\behtype}{{\bf B}}
\newcommand{\bt}[1]{{\it BT}(#1)} % Boehm tree
\newcommand{\cxt}[1]{#1[~]} % Context with one hole
\newcommand{\pr}{\parallel} % parallel ||
\newcommand{\Nat}{\mathbf{N}} % natural numbers
\newcommand{\Natmax}{\mathbf{N}_{{\it max}}} % natural numbers with minus infinity
\newcommand{\Rat}{\mathbf{Q}^{+}} % non-negative rationals
\newcommand{\Ratmax}{\mathbf{Q}^{+}_{{\it max}}} % non-negative rationals with minus infinity
\newcommand{\Alt}{ \mid\!\!\mid }
\newcommand{\isum}{\oplus}
\newcommand{\csum}{\uplus} %context sum
\newcommand{\dpar}{\mid\!\mid}
% for the production of a grammar containing \mid
\newcommand{\infer}[2]{\begin{array}{c} #1 \\ \hline #2 \end{array}}
% to make a centered inference rule
% (Meta-)Logic
\newcommand{\bool}{{\sf bool}} % boolean values
\newcommand{\Or}{\vee} % disjunction
\newcommand{\OR}{\bigvee} % big disjunction
\newcommand{\AND}{\wedge} % conjunction
\newcommand{\ANDD}{\bigwedge} % big conjunction
\newcommand{\Arrow}{\Rightarrow} % right double arrow
\newcommand{\IFF}{\mbox{~~iff~~}} % iff in roman and with spaces
\newcommand{\iffArrow}{\Leftrightarrow} % logical equivalence
% Semantics
\newcommand{\dl}{[\![} % semantic [[
\newcommand{\dr}{]\!]} % semantic ]]
\newcommand{\lam}{{\bf \lambda}} % semantic lambda
% The equivalences for this paper
% the usual ones
\newcommand{\ubis}{\approx^u} % usual labelled weak bis
\newcommand{\uabis}{\approx^{u}_{ccs}} % usual labelled weak bis on CCS
% the contextual conv sensitive
\newcommand{\cbis}{\approx} % convergence sensitive bis
\newcommand{\cabis}{\approx_{ccs}} % convergence sensitive bis on CCS
% the labelled conv sensitive
\newcommand{\lcbis}{\approx^{\ell}} %
\newcommand{\lcabis}{\approx^{\ell}_{ccs}} % labelled convergence sensitive bis on CCS
\newcommand{\lcbiswrong}{\approx^{\ell \Downarrow}} %
\newcommand{\maytest}{=_{\Downarrow}}
\newcommand{\musttest}{=_{\Downarrow_{S}}}
% Sets
\newcommand{\prt}[1]{{\cal P}(#1)} % Parts of a set
\newcommand{\finprt}[1]{{\cal P}_{fin}(#1)}% Finite parts
\newcommand{\finprtp}[1]{{\cal P}_{fin}^{+}(#1)}% Non-empty Finite parts
\newcommand{\union}{\cup} % union
\newcommand{\inter}{\cap} % intersection
\newcommand{\Union}{\bigcup} % big union
\newcommand{\Inter}{\bigcap} % big intersection
\newcommand{\cpl}[1]{#1^{c}} % complement
\newcommand{\card}{\sharp} % cardinality
\newcommand{\minus}{\backslash} % set difference
\newcommand{\sequence}[2]{\{#1\}_{#2}} % ex. \sequence{d_n}{n\in \omega}
\newcommand{\comp}{\circ} % functional composition
%\newcommand{\oset}[1]{\{#1\}} % set enumeration
\newcommand{\mset}[1]{\{\! | #1 |\!\}} % pseudo-set notation {| |}
% Domains
\newcommand{\two}{{\bf O}} % Sierpinski space
\newcommand{\join}{\vee} % join
\newcommand{\JOIN}{\bigvee} % big join
\newcommand{\meet}{\wedge} % meet
\newcommand{\MEET}{\bigwedge} % big meet
\newcommand{\dcl}{\downarrow} % down closure
\newcommand{\ucl}{\uparrow} % up closure
\newcommand{\conv}{\downarrow} % synt. conv. pred. (postfix)
\newcommand{\diver}{\uparrow} % diverging term
\newcommand{\Conv}{\Downarrow} % sem. conv. pred. (postfix)
\newcommand{\SConv}{\Downarrow_{S}} % sem. conv. pred. (postfix)
\newcommand{\CConv}{\Downarrow_{C}}
\newcommand{\Diver}{\Uparrow} % diverging map
\newcommand{\cpt}[1]{{\cal K}(#1)} % compacts, write \cpt{D}
\newcommand{\ret}{\triangleleft} % retract
\newcommand{\nor}{\succeq}
\newcommand{\prj}{\underline{\ret}} % projection
\newcommand{\parrow}{\rightharpoonup} % partial function space
\newcommand{\ub}[1]{{\it UB}(#1)} % upper bounds
\newcommand{\mub}[1]{{\it MUB}(#1)} % minimal upper bounds
\newcommand{\lift}[1]{(#1)_{\bot}} % lifting
\newcommand{\forget}[1]{\underline{#1}} % forgetful translation
%\newcommand{\rel}[1]{\;{\cal #1}\;} % infix relation (calligraphic)
\newcommand{\rl}[1]{\;{\cal #1}\;} % infix relation
\newcommand{\rel}[1]{{\cal #1}} %calligraphic relation with no
%extra space
\newcommand{\per}[1]{\;#1 \;}
\newcommand{\wddagger}{\natural} % weak suspension
%\newcommand{\wddagger}{=\!\!\!\!\parallel} % weak suspension
% Categories
\newcommand{\pair}[2]{\langle #1 , #2 \rangle} % pairing \pair{x}{y}, do not use < >.
% ******* Notation for the $\pi$-calculus *********
% Syntax:
\newcommand{\fn}[1]{{\it fn}(#1)} % free names
\newcommand{\bn}[1]{{\it bn}(#1)} % bound names
\newcommand{\names}[1]{{\it n}(#1)} % names
\newcommand{\true}{{\sf t}} % true
\newcommand{\false}{{\sf f}} % false
\newcommand{\pio}{\pi_1} % 1 receptor calculus
\newcommand{\pioo}{\pi_{1}^{r}}
\newcommand{\piom}{\pi_{1}^{-}} % 1 receptor calculus wo match
\newcommand{\pioi}{\pi_{1I}} % 1 receptor I-calculus
\newcommand{\pifo}{\pi_{\w{1f}}} % functional calculus
\newcommand{\pilo}{\pi_{\w{1l}}} % located calculus
\newcommand{\sort}[1]{{\it st}(#1)} % sort
\newcommand{\ia}[1]{{\it ia}(#1)} % sort
\newcommand{\ite}[3]{{\sf if~} #1 {\sf ~then~} #2 {\sf ~else~} #3} %if then else
\newcommand{\casep}[2]{{\sf case}^{\times}(#1, \pair{x}{y}\Arrow#2)} %case on pairs
\newcommand{\casel}[3]{{\sf case}^{L}(#1, #2, \s{cons}(x,y)\Arrow#3)} %case on lists
\newcommand{\caseb}[3]{{\sf case}^{b}(#1, #2, \s{cons}(x,y)\Arrow#3)} %case on lists
\newcommand{\nil}{{\sf nil}}
\newcommand{\cons}{{\sf cons}}
\newcommand{\idle}[1]{{\it Idle}(#1)} %idle process
\newcommand{\conf}[1]{\{ #1 \}} %configuration
\newcommand{\link}[2]{#1 \mapsto #2} %likn a ->b
\newcommand{\mand}{\mbox{ and }}
\newcommand{\dvec}[1]{\tilde{{\bf #1}}} %double vector
\newcommand{\erloc}[1]{{\it er}_{l}(#1)} % location erasure
\newcommand{\w}[1]{{\it #1}} %To write in math style
\newcommand{\vcb}[1]{{\bf #1}}
\newcommand{\lc}{\langle\!|}
\newcommand{\rc}{|\!\rangle}
\newcommand{\obj}[1]{{\it obj}(#1)}
\newcommand{\move}[1]{{\sf move}(#1)}
\newcommand{\qqs}[2]{\forall\, #1\;\: #2}
\newcommand{\qtype}[4]{\forall #1 : #2 . (#4,#3)}
\newcommand{\xst}[2]{\exists\, #1\;\: #2}
\newcommand{\xstu}[2]{\exists\, ! #1\;\: #2}
\newcommand{\dpt}{\,:\,}
\newcommand{\cond}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3}
\newcommand{\s}[1]{{\sf #1}} % sans-serif
\newcommand{\vc}[1]{{\bf #1}}
\newcommand{\lnorm}{\lbrack\!\lbrack}
\newcommand{\rnorm}{\rbrack\!\rbrack}
\newcommand{\sem}[1]{\underline{#1}}
\newcommand{\tra}[1]{\langle #1 \rangle}
\newcommand{\trb}[1]{[ #1 ]}
\newcommand{\squn}{\mathop{\scriptstyle\sqcup}}
\newcommand{\lcro}{\langle\!|}
\newcommand{\rcro}{|\!\rangle}
\newcommand{\semi}[1]{\lcro #1\rcro}
\newcommand{\sell}{\,\ell\,}
\newcommand{\SDZ}[1]{\marginpar{\textbf{SDZ:} {#1}}}
\newcommand{\when}[3]{{\sf when}~#1~{\sf then}~#2~{\sf else}~#3}
\newcommand{\wthen}[2]{{\sf when}~#1~{\sf then}~#2~}
\newcommand{\welse}[1]{{\sf else}~#1}
%Pour la fleche double, il faut rajouter :
% \usepackage{mathtools}
\newcommand{\act}[1]{\xrightarrow{#1}} %labelled actionlow %high
\newcommand{\lact}[1]{\stackrel{#1}{\makebox[5mm]{\,$- \! {\circ}\,$}}}
\newcommand{\set}[1]{\{#1\}}
\newcommand{\pst}[2]{{\sf pset}(#1,#2)}
\newcommand{\st}[2]{{\sf set}(#1,#2)}
\newcommand{\wrt}[2]{{\sf w}(#1,#2)}
\newcommand{\chtype}[2]{{\it Ch_{#1}(#2)}}
\newcommand{\rgtype}[2]{{\it {\sf Reg}_{#1} #2}}
\newcommand{\get}[1]{{\sf get}(#1)}
%\newcommand{\wact}[1]{\xRightarrow{#1}} %weak labelled action low high
%\newcommand{\mact}[1]{\xrightarrow{#1}_{m}} %labelled action low %high
%\newcommand{\wmact}[1]{\xRightarrow{#1}_{m}} %weak labelled action low high
%\newcommand{\act}[1]{\stackrel{#1}{\rightarrow}} %labelled action low
%%%high
\newcommand{\acteq}[1]{\stackrel{#1}{\leadsto}} %labelled action low
%%%high
%\newcommand{\actI}[1]{\stackrel{#1}{\rightarrow_{1}}} %labelled action low
\newcommand{\actI}[1]{\xrightarrow{#1}_{1}}
%\newcommand{\actII}[1]{\stackrel{#1}{\rightarrow_{2}}} %labelled action low
\newcommand{\actII}[1]{\xrightarrow{#1}_{2}}
\newcommand{\wact}[1]{\stackrel{#1}{\Rightarrow}} %weak labelled action low high
\newcommand{\wactI}[1]{\stackrel{#1}{\Rightarrow_{1}}} %weak labelled action low high
\newcommand{\wactII}[1]{\stackrel{#1}{\Rightarrow_{2}}} %weak labelled action low high
\newcommand{\mact}[1]{\stackrel{#1}{\rightarrow_{m}}} %labelled action low
%high
\newcommand{\wmact}[1]{\stackrel{#1}{\Rightarrow_{m}}} %weak labelled action low high
%\newcommand{\lact}[1]{\stackrel{#1}{\leftarrow}}
\newcommand{\lwact}[1]{\stackrel{#1}{\Leftarrow}}
\newcommand{\eval}{\Downarrow}
\newcommand{\Eval}[1]{\Downarrow^{#1}}
\newcommand{\Z}{{\bf Z}}
\newcommand{\Real}{\mathbb{R}^{+}}
\newcommand{\Return}{\ensuremath{\mathtt{return}}\xspace}
\newcommand{\Stop}{\ensuremath{\mathtt{stop}}\xspace}
\newcommand{\Wait}{\ensuremath{\mathtt{wait}}\xspace}
\newcommand{\Read}{\ensuremath{\mathtt{read}}\xspace}
\newcommand{\Write}{\ensuremath{\mathtt{write}}\xspace}
\newcommand{\Yield}{\ensuremath{\mathtt{yield}}\xspace}
\newcommand{\Next}{\ensuremath{\mathtt{next}}\xspace}
\newcommand{\Load}{\ensuremath{\mathtt{load}}\xspace}
\newcommand{\Call}{\ensuremath{\mathtt{call}}\xspace}
\newcommand{\Tcall}{\ensuremath{\mathtt{tcall}}\xspace}
\newcommand{\Pop}{\ensuremath{\mathtt{pop}}\xspace}
\newcommand{\Build}{\ensuremath{\mathtt{build}}\xspace}
\newcommand{\Branch}{\ensuremath{\mathtt{branch}}\xspace}
\newcommand{\Goto}{\ensuremath{\mathtt{goto}}\xspace}
\newcommand{\hatt}[1]{#1^{+}}
\newcommand{\Of}{\mathbin{\w{of}}}
\newcommand{\susp}{\downarrow}
\newcommand{\lsusp}{\Downarrow_L}
\newcommand{\wsusp}{\Downarrow}
\newcommand{\commits}{\searrow}
\newcommand{\spi}{S\pi}
\newcommand{\pres}[2]{#1\triangleright #2} %TCCS else next (alternative)
% \newcommand{\pres}[2]{ \lfloor #1 \rfloor (#2)} %TCCS else next
\newcommand{\present}[3]{{\sf present} \ #1 \ {\sf do } \ #2 \ {\sf else} \ #3}
\newcommand{\tick}{{\sf tick}} %tick action
\newcommand{\sbis}{\equiv_L}
\newcommand{\emit}[2]{\ol{#1}#2}
%\newcommand{\present}[4]{#1(#2).#3,#4}
\newcommand{\match}[4]{[#1=#2]#3,#4} %pi-equality
\newcommand{\matchv}[4]{[#1 \unrhd #2]#3,#4}
\newcommand{\new}[2]{\nu #1 \ #2}
\newcommand{\outact}[3]{\new{{\bf #1}}{\emit{#2}{#3}}}
\newcommand{\real}{\makebox[5mm]{\,$\|\!-$}}% realizability relation
\newcommand{\regterm}[2]{{\sf reg}_{#1} #2}
\newcommand{\thread}[1]{{\sf thread} \ #1}
\newcommand{\store}[2]{(#1 \leftarrow #2)}
\newcommand{\pstore}[2]{(#1 \Leftarrow #2)}
\newcommand{\regtype}[2]{{\sf Reg}_{#1} #2}
\newcommand{\uregtype}[3]{{\sf Reg}_{#1}(#2, #3)}
\newcommand{\urtype}[2]{{\sf Reg}(#1, #2)}
\newcommand{\upair}[2]{[#1,#2]}
\newcommand{\letb}[3]{\mathsf{let}\;\oc #1 = #2\;\mathsf{in}\;#3}
\newcommand{\vlt}[1]{{\cal V}(#1)}
\newcommand{\prs}[1]{{\cal P}(#1)}
\newcommand{\imp}{{\sf Imp}} %imp language
\newcommand{\vm}{{\sf Vm}} %virtual machine language
\newcommand{\mips}{{\sf Mips}} %Mips language
\newcommand{\C}{{\sf C}} % C language
\newcommand{\Clight}{{\sf Clight}} %C light language
\newcommand{\Cminor}{{\sf Cminor}}
\newcommand{\RTLAbs}{{\sf RTLAbs}}
\newcommand{\RTL}{{\sf RTL}}
\newcommand{\ERTL}{{\sf ERTL}}
\newcommand{\LTL}{{\sf LTL}}
\newcommand{\LIN}{{\sf LIN}}
\newcommand{\access}[1]{\stackrel{#1}{\leadsto}}
\newcommand{\ocaml}{{\sf ocaml}}
\newcommand{\coq}{{\sf Coq}}
\newcommand{\compcert}{{\sf CompCert}}
%\newcommand{\cerco}{{\sf CerCo}}
\newcommand{\cil}{{\sf CIL}}
\newcommand{\scade}{{\sf Scade}}
\newcommand{\absint}{{\sf AbsInt}}
\newcommand{\framac}{{\sf Frama-C}}
\newcommand{\powerpc}{{\sf PowerPc}}
\newcommand{\lustre}{{\sf Lustre}}
\newcommand{\esterel}{{\sf Esterel}}
\newcommand{\ml}{{\sf ML}}
\newcommand{\codeex}[1]{\texttt{#1}} % code example
\bibliographystyle{abbrv}
\title{
INFORMATION AND COMMUNICATION TECHNOLOGIES\\
(ICT)\\
PROGRAMME\\
\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
\date{ }
\author{}
%>>>>>> new commands used in this document
% \usepackage[nohyperref,nosvn]{mystyle}
\usepackage{multirow}
\newcolumntype{b}{@{}>{{}}}
\newcolumntype{B}{@{}>{{}}c<{{}}@{}}
\newcolumntype{h}[1]{@{\hspace{#1}}}
\newcolumntype{L}{>{$}l<{$}}
\newcolumntype{C}{>{$}c<{$}}
\newcolumntype{R}{>{$}r<{$}}
\newcolumntype{S}{>{$(}r<{)$}}
\newcolumntype{n}{@{}}
\newcommand{\spanr}[2]{\multicolumn{1}{Rn}{\multirow{#1}{*}{(#2)}}}
\def\nocol{\multicolumn{1}{ncn}{}}
\usepackage[disable, colorinlistoftodos]{todonotes}
\usepackage{enumerate}
\usepackage{tikz}
\newcommand{\tern}[3]{#1\mathrel ? #2 : #3}
\newcommand{\sop}[1]{\s{#1}\ }
\newcommand{\sbin}[1]{\ \s{#1}\ }
\newcommand{\Ell}{\mathcal L}
\newcommand{\alphab}{\boldsymbol\alpha}
\newcommand{\betab}{\boldsymbol\beta}
\newcommand{\gramm}{\mathrel{::=}}
\newcommand{\ass}{\mathrel{:=}}
%<<<<<<<<<<<<
\begin{document}
% \thispagestyle{empty}
%
% \vspace*{-1cm}
% \begin{center}
% \includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
% \end{center}
%
% \begin{minipage}{\textwidth}
% \maketitle
% \end{minipage}
%
%
% \vspace*{0.5cm}
% \begin{center}
% \begin{LARGE}
% \bf
% Report \\
% Dependent Cost Labels
% \\
% \end{LARGE}
% \end{center}
%
% \vspace*{2cm}
% \begin{center}
% \begin{large}
% Version 0.1
% \end{large}
% \end{center}
%
% \vspace*{0.5cm}
% \begin{center}
% \begin{large}
% Main Author:\\
% Paolo Tranquilli
% \end{large}
% \end{center}
%
% \vspace*{\fill}
% \noindent
% Project Acronym: \cerco{}\\
% Project full title: Certified Complexity\\
% Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
%
% \clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
%
% \newpage
\listoftodos
\section{Introduction}
In~\cite{D2.1} an approach is presented tackling the problem of building a
compiler from a large fragment of C which is capable of lifting execution cost information
from the compiled code and present it to the user. This endeavour is central to
the CerCo project, which strives to produce a mechanically certified version of
such a compiler.
In rough words, the proposed approach consists in decorating the source code with
labels at key points, and preserving such labels along the compilation chain.
Once the final object code is produced, such labels should correspond to parts
of the compiled code which have constant cost.
There are two properties one asks of the cost estimate. The first, paramount to
the correctness of the method, is \emph{soundness}: the actual execution cost
is bounded by the estimate. In the labelling approach, this is guaranteed if every
loop in the control flow of the compiled code passes through at least one cost
label. The second, optional but desirable, is \emph{preciseness}: the estimate
is not in fact an estimate but the actual cost. In the labelling approach, this will
true if for every label every possible execution of the compiled code starting
from such a label yields the same cost. In simple architectures such as the 8051
micro-controller this can be guaranteed by having labels at the immediate start of any
branch of the control flow, and by ensuring no duplicate labels are present.
It should be underlined that the above mentioned requirements must hold when
executing the code at the
end of the compilation chain. If one is careful to inject the labels at good
key places in the source code, one can still think of two main obstacles:
\begin{itemize}
\item compilation introduces important changes in the control flow, inserting
loops or branches: an example in addressing this is the insertion of functions
in the source code replacing instructions unavailable in the target architecture
that require loops (e.g.\ multi-word division and generic shift in the 8051
architecture) so that the annotation process be sound, or the effort put in
providing unbranching translations of higher level instructions~
\cite{D2.2};
\item even if the compiled code \emph{does}, as long as the the syntactic
control flow graph is concerned, respect the conditions for soundness and
preciseness, the cost of blocks of instructions might not be independent of context,
so that different passes through a label might have different costs: this
becomes a concern if one wishes to apply the approach to more complex architectures,
for example one with cache or pipelining.
\end{itemize}
The first point unveils a weakness of the current labelling approach when it
comes to some common code transformations done along a compilation chain. In
particular most of \emph{loop optimizations} disrupt such conditions directly.
For example in what we will call \emph{loop peeling} a first iteration of the
loop is hoisted ahead of it, possibly to have a different cost than later iterations
because of further transformation such as dead code elimination or invariant
code motion.
The second point strikes a difference in favour to existing tools for the
estimate of execution costs to the detriment of CerCo's approach advocated in~
\cite{D2.1}. We will take as example the well known tool \s{aiT}~\cite{absint},
based on abstract interpretation: such a tool allows to estimate the
worst-case execution time (WCET) taking into account advanced aspects of the
target architecture. \s{aiT}'s ability to
do close estimates of execution costs even when these depend on the context of
execution would enhance the effectiveness of CerCo's compiler, either by
integrating such techniques in its development, or by directly calling this tool
when ascertaining the cost of blocks of compiled code. A typical case where
cache analysis yields a difference in the execution cost of a block is in loops:
the first iteration will usually stumble upon more cache misses than subsequent
iterations.
If one looks closely, the source of the weakness of the labelling approach as
presented in~\cite{D2.1} is common to both points: the inability to state
different costs for different occurrences of labels, where the difference
might be originated by labels being duplicated along compilation
or the costs being sensitive to the state of execution.
The preliminary work
we present here addresses this node, introducing cost labels that are dependent
on which iteration of its containing loops it occurs in. This is achieved by
means of \emph{indexed labels}: all cost labels are decorated with formal
indexes coming from the loops containing such labels. These indexes allow to
rebuild, even after several steps of loop transformations,
which iterations of the original loops in the source code a particular label
occurrence belongs to. During annotation of source code, this information
is given to the user by means of dependent costs.
We concentrate on integrating the labelling approach with two loop transformations.
For general information on compiler optimization (and loop optimizations in
particular) we refer the reader to the vast literature on the subject
(e.g.~\cite{muchnick,morgan}).
\emph{Loop peeling}, as already mentioned, consists in preceding the loop with
a copy of its body, appropriately guarded. This is in general useful to trigger
further optimizations, such as ones relying on execution information which can
be computed at compile time but which is erased by further iterations of the loop,
or ones that use the hoisted code to be more effective at eliminating redundant
code. Integrating this transformation to the labelling approach would also allow
to integrate the common case of cache analysis explained above: the analysis
of cache hits and misses in the case of usually benefits from a form of
\emph{virtual} loop peeling~\cite{cacheprediction}.
\emph{Loop unrolling} consists in repeating several times the body of the loop
inside the loop itself (inserting appropriate guards, or avoiding them altogether
if enough information on the loop's guard is available at compile time). This
can limit the number of (conditional or unconditional) jumps executed by the
code and trigger further optimizations dealing with pipelining, if applicable
to the architecture.
While covering only two loop optimizations, the work presented here poses good
bases to extending the labelling approach to cover more and more of them, as well
as giving hints as to how integrating in CerCo's compiler advanced cost estimation
techniques such as cache analysis. Moreover loop peeling has the substantial
advantage of enhancing other optimizations. Experimentation with CerCo's
untrusted prototype compiler with constant propagation and
partial redundancy elimination~\cite{PRE,muchnick} show how loop peeling enhances
those other optimizations.
\paragraph{Outline.}
We will present our approach on a minimal toy imperative language, \imp{}
with gotos, which we present in \autoref{sec:defimp} along with formal
definition of the loop transformations. This language already
presents most of the difficulties encountered when dealing with C, so
we stick to it for the sake of this presentation. In \autoref{sec:labelling}
we summarize the labelling approach as presented in~\cite{D2.1}. The following
\autoref{sec:indexedlabels} explains \emph{indexed labels}, our proposal for
dependent labels which are able to describe precise costs even in the presence
of the loop transformations we consider. Finally \autoref{sec:conc} goes into
more details regarding the implementation of indexed labels in CerCo's
untrusted compiler and speculates on further work on the subject.
\section{\imp{} with goto}\label{sec:defimp}
We briefly outline the toy language which contains all the relevant instructions
to present the development and the problems it is called to solve.
The version of the minimal imperative language \imp that we will present has,
with respect to the barebone usual version, \s{goto}s and labelled statements.
Break and continue statements can be added at no particular expense. Its syntax
and operational semantics is presented in \autoref{fig:minimp}. The actual
grammar for expressions is not particularily relevant so we do not give a
precise one. For the sake of this presentation we also trat boolean and
arithmetic expressions together (with the usual convention of an expression
being true iff non-zero). We will consistently suppose programs are
\emph{well-labelled}, i.e.\ every label labels at most one occurrence of statement
in the program, and every \s{goto} points to a label actually present in the program.
\begin{figure}
$$\begin{gathered}
\begin{array}{nlBl>(R<)n}
\multicolumn{4}{C}{\bfseries Syntax}\\
\multicolumn{4}{ncn}{
\ell,\ldots \hfill \text{(labels)} \hfill x,y,\ldots \hfill
\text{(identifiers)}
\hfill e,f,\ldots \hfill \text{(expression)}
}\\
P,S,T,\ldots &\gramm& \s{skip} \mid s;t
\mid \sop{if}e\sbin{then}s\sbin{else}t
\mid \sop{while} e \sbin{do} s \mid
x \ass e
\\&\mid&
\ell : s \mid \sop{goto}\ell& \spanr{-2}{statements}\\
\\
\multicolumn{4}{C}{\bfseries Semantics}\\
K,\ldots &\gramm& \s{halt} \mid S \cdot K & continuations
\end{array}
\\[15pt]
\s{find}(\ell,S,K) \ass
\left\{\begin{array}{lL}
\bot & if $S=\s{skip},\sop{goto} \ell'$ or $x\ass e$,\\
(T, K) & if $S=\ell:T$,\\
\s{find}(\ell,T,K) & otherwise, if $S = \ell':T$,\\
\s{find}(\ell,T_1,T_2\cdot K) & if defined and $S=T_1;T_2$,\\
\s{find}(\ell,T_1,K) & if defined and
$S=\sop{if}b\sbin{then}T_1\sbin{else}T_2$,\\
\s{find}(\ell,T_2,K) & otherwise, if $S=T_1;T_2$ or
$\sop{if}b\sbin{then}T_1\sbin{else}T_2$,\\
\s{find}(\ell,T,S\cdot K) & if $S = \sop{while}b\sbin{do}T$.
\end{array}\right.
\\[15pt]
\begin{array}{lBl}
(x:=e,K,s) &\to_P& (\s{skip},K,s[v/x]) \qquad\mbox{if }(e,s)\eval v \\ \\
(S;T,K,s) &\to_P& (S,T\cdot K,s) \\ \\
(\s{if} \ b \ \s{then} \ S \ \s{else} \ T,K,s)
&\to_P&\left\{
\begin{array}{ll}
(S,K,s) &\mbox{if }(b,s)\eval v \neq 0 \\
(T,K,s) &\mbox{if }(b,s)\eval 0
\end{array}
\right. \\ \\
(\s{while} \ b \ \s{do} \ S ,K,s)
&\to_P&\left\{
\begin{array}{ll}
(S,\s{while} \ b \ \s{do} \ S \cdot K,s) &\mbox{if }(b,s)\eval v \neq 0 \\
(\s{skip},K,s) &\mbox{if }(b,s)\eval 0
\end{array}
\right. \\ \\
(\s{skip},S\cdot K,s) &\to_P&(S,K,s) \\ \\
(\ell : S, K, s) &\to_P& (S,K,s) \\ \\
(\sop{goto}\ell,K,s) &\to_P& (\s{find}(\ell,P,\s{halt}),s) \\ \\
\end{array}
\end{gathered}$$
\caption{The syntax and operational semantics of \imp.}
\label{fig:minimp}
\end{figure}
\paragraph{Further down the compilation chain.}
As for the rest of the compilation chain, we abstract over it. We just posit
every language $L$ further down the compilation chain has a suitable notion of
sequential instructions (with one natural successor), to which we can add our
own.
\subsection{Loop transformations}
We call a loop $L$ \emph{single-entry} in $P$ if there is no \s{goto} of $P$
outside of $L$ which jumps to within $L$\footnote{This is a reasonable
aproximation: it considers multi-entry also those loops having an external but
unreachable \s{goto} jumping to them.}. Many loop optimizations do not preserve
the semantics of multi-entry loops in general, or are otherwise rendered
ineffective. Usually compilers implement a multi-entry loop detection which
avoids those loops from being targeted by optimizations~\cite{muchnick,morgan}.
\paragraph{Loop peeling.}
$$
\sop{while}b\sbin{do}S\mapsto
\sop{if}b\sbin{then} S; \sop{while} b \sbin{do} S[\ell'_i/\ell_i]
$$
where $\ell'_i$ is a fresh label for any $\ell_i$ labelling a statement in $S$.
This relabelling is safe as to \s{goto}s external to the loop because of the
single-entry condition. Notice that in case of break and continue statements,
those should be replaced with \s{goto}s in the peeled body $S$.
\paragraph{Loop unrolling.}
$$
\sop{while}b\sbin{do}S\mapsto
\sop{while} b \sbin{do} (S ;
\sop{if} b \sbin{then} (S[\ell^1_i/\ell_i] ;
\cdots
\sop{if} b \sbin{then} S[\ell^n_i/\ell_i]) \cdots)
$$
where $\ell^j_i$ are again fresh labels for any $\ell_i$ labelling a statement
in $S$. This is a willingly naïf version of loop unrolling, which usually
targets less general loops. The problem it poses to Cerco's labelling approach
are independent of the cleverness of the actual transformation.
\section{Labelling: a quick sketch of the previous approach}\label{sec:labelling}
Plainly labelled \imp{} is obtained adding to the code \emph{cost labels}
(with metavariables $\alpha,\beta,\ldots$), and cost-labelled statements:
$$S,T\gramm \cdots \mid \alpha: S$$
Cost labels allow for some program points to be tracked along the compilation
chain. For further details we refer to\cite{D2.1}.
With labels the small step semantics turns into a labelled transition
system and a natural notion of trace (i.e.\ lists of labels) arises.
Evaluation of statements is enriched with traces, so that rules are like
$$
\begin{array}{lblL}
(\alpha: S, K,s) &\to[\alpha]_P (S,K,s)\\
(\s{skip}, S \cdot K,s) &\to[\varepsilon]_P (S, K, s)\\
& \text{etc.}
\end{array}$$
\paragraph{Labelling.}
Given an \imp{} program $P$ its \emph{labelling} $\alpha:\Ell(P)$ in $\ell-\imp$
is
defined by putting cost labels after every branching, at the start of both
branches, and a cost label at the beginning of the program. So the relevant
cases are
$$\begin{aligned}
\Ell(\sop{if}e\sbin{then}S\sbin{else}T) &=
\sop{if}e\sbin{then}\alpha:\Ell(S)\sbin{else}\beta:\Ell(T)\\
\Ell(\sop{while}e\sbin{do}S) &=
(\sop{while}e\sbin{do}\alpha:\Ell(S));\beta:\s{skip}
\end{aligned}$$
where $\alpha,\beta$ are fresh cost labels, and while in other cases the
definition just passes to sub-statements.
\paragraph{Labels in the rest of the compilation chain.} All languages further
down the chain get a new sequential statement $\sop{emit}\alpha$ whose effect is
to be consumed in a labelled transition while keeping the same state. All other
instructions guard their operational semantics and do not emit cost labels.
Preservation of semantics throughout the compilation process is restated, in
rough terms, as
$$\text{starting state of $P$}\to[\lambda]\!\!^*\;\text{halting state} \iff
\text{starting state of $\mathcal C(P)$} \to[\lambda]\!\!^*\;\text{halting state},$$
where $P$ is a program of a language along the compilation chain, starting and
halting states depend on the language, and $\mathcal C$ is the
compilation function\footnote{The case of divergent computations needs
to be addressed too. Also, the requirement can be weakened by demanding some
sort of equivalence of the traces rather than equality. Both these issues escape
the scope of this presentation.}.
\paragraph{Instrumentations}
Let $\mathcal C$ be the whole compilation from $\ell\imp$ to the labelled
version of some low-level language $L$. Supposing such compilation has not
introduced any new loop or branching, we have that
\begin{itemize}
\item every loop contains at least a cost label (\emph{soundness condition}),
and
\item every branching has different labels for the two branches
(\emph{preciseness condition}).
\end{itemize}
With these two conditions, we have that each and every cost label in
$\mathcal C(P)$ for any $P$ corresponds to a block of sequential instructions,
to which we can assign a constant \emph{cost}\footnote{This in fact requires the
machine architecture to be simple enough, or for some form of execution analysis
to take place.} We can therefore assume a \emph{cost mapping} $\kappa_P$ from
cost labels to natural numbers, assigning to each cost label $\alpha$ the cost
of the block containing the single occurrance of $\alpha$.
Given any cost mapping $\kappa$, we can enrich a labelled program so that a
particular fresh variable (the \emph{cost variable} $c$) keeps track of the
assumulation of costs during the execution. We call this procedure
\emph{instrumentation} of the program, and it is defined recursively by
$$
\mathcal I(\alpha:S) = c \ass c + \kappa(\alpha) ; \mathcal I(S)
$$
while in all other cases the definition passes to substatements.
\paragraph{The problem with loop optimizations.}
Let us take loop peeling, and apply it to the labelling of a program without any
adjustment:
$$
(\sop{while}e\sbin{do}\alpha:S);\beta:\s{skip}
\mapsto
(\sop{if}b\sbin{then} \alpha : S; \sop{while} b \sbin{do} \alpha :
S[\ell'_i/\ell_i]);
\beta:\s{skip}$$
What happens is that the cost label $\alpha$ is duplicated into two distinct
occurrences. If these two occurrences correspond to different costs in the
compiled code, the best the cost mapping can do is to take the maximum of the
two, preserving soundness (i.e.\ the cost estimate still bounds the actual one)
but loosing preciseness (i.e.\ the actual cost would be strictly less than its
estimate).
\section{Indexed labels}\label{sec:indexedlabels}
This section presents the core of the new approach. In brief points it amounts
to the following.
\begin{enumerate}[\bfseries \ref*{sec:indexedlabels}.1.]
\item\label{en:outline1}
Enrich cost labels with formal indexes corresponding, at the beginning of
the process, to which iteration of the loop they belong to.
\item\label{en:outline2}
Each time a loop transformation is applied and a cost labels is split in
different occurrences, each of these will be reindexed so that every time they
are emitted their position in the original loop will be reconstructed.
\item\label{en:outline3}
Along the compilation chain, add alongside the \s{emit} instruction other
ones updating the indexes, so that iterations of the original loops can be
rebuilt at the operational semantics level.
\item\label{en:outline4}
The machinery computing the cost mapping will still work, but assigning
costs to indexed cost labels, rather than to cost labels as we wish: however
\emph{dependent costs} can be calculated, where dependency is on which iteration
of the containing loops we are in.
\end{enumerate}
\subsection{Indexing the cost labels}\label{ssec:indlabs}
\paragraph{Formal indexes and $\iota\ell\imp$.}
Let $i_0,i_1,\ldots$ be a sequence of distinguished fresh identifiers that will
be used as loop indexes. A \emph{simple expression} is an affine arithmetical
expression in one of these indexes, that is $a*i_k+b$ with $a,b,k \in \mathbb N$.
Simple expressions $e_1=a_1*i_k+b_1$, $e_2=a2*i_k+b_2$ in the same index can be
composed, yielding $e_1\circ e_2\ass (a_1a_2)*i_k + (a_1b2+b_1)$, and this operation
has an identity element in $id_k \ass 1*i_k+0$. Constants can be expressed as simple
expressions, so that we identify a natural $c$ with $0*i_k+c$.
An \emph{indexing} (with metavariables $I$, $J$, \ldots) is a list of
transformations of successive formal indexes dictated by simple expressions,
that is a mapping%
\footnote{Here we restrict each mapping to be a simple expression
\emph{on the same index}. This might not be the case if more loop optimizations
are accounted for (for example, interchanging two nested loops).}
$$i_0\mapsto a_0*i_0+b_0,\dots, i_{k-1} \mapsto a_{k-1}*i_{k-1}+b_{k-1}.$$
An \emph{indexed cost label} (metavariables $\alphab$, $\betab$, \ldots) is
the combination of a cost label $\alpha$ and an indexing $I$, written
$\alpha\la I\ra$. The cost label underlying an indexed one is called its
\emph{atom}. All plain labels can be considered as indexed ones by taking
an empty indexing.
\imp{} with indexed labels ($\iota\ell\imp$) is defined by adding to $\imp$
statements with indexed labels, and by having loops with formal indexes
attached to them:
$$S,T,\ldots \gramm \cdots i_k:\sop{while}e\sbin{do}S\mid \alphab : S.$$
Notice than unindexed loops still are in the language: they will correspond
to multi-entry loops which are ignored by indexing and optimizations.
We will discuss the semantics later.
\paragraph{Indexed labelling.}
Given an $\imp$ program $P$, in order to index loops and assign indexed labels
we must first of all distinguish single-entry loops. We just sketch how it can
be computed.
A first pass of the program $P$ can easily compute two maps: $\s{loopof}_P$
from each label $\ell$ to the occurrence (i.e.\ the path) of a $\s{while}$ loop
containing $\ell$, or the empty path if none exists; and $\s{gotosof}_P$ from
a label $\ell$ to the occurrences of \s{goto}s pointing to it. Then the set
$\s{multyentry}_P$ of multy-entry loops of $P$ can be computed by adding to it
all occurrences $p$ such that there exists a label $\ell$ and an occurrence
$q$ with $\s{loopof}_P(\ell)=p$, $q\in \s{gotosof}_P(\ell)$ and $p\not\le q$
(where $\le$ is the prefix relation)\footnote{Possible simplification to this
procedure include keeping track just of while loops containing labels and
\s{goto}s (rather than paths in the syntactic tree of the program), and making
two passes while avoiding building the map to sets $\s{gotosof}$}.
Let $Id_k$ be the indexing of length $k$ made from identity simple expressions,
i.e.\ the sequence $i_0\mapsto id_0, \ldots , i_{k-1}\mapsto id_{k-1}$. We define the tiered indexed labelling
$\Ell^\iota_P (S,k)$ in program $P$ for occurrence $S$ of a statement in $P$
and a natural $k$ by recursion, setting
$$
\Ell^\iota_P(S,k)\ass
\left\{
\begin{array}{lh{-100pt}l}
(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}
\\& \text{if $S=\sop{while}b\sbin{do}T$ and $S\notin \s{multyentry}_P$,}\\[3pt]
(\sop{while}b\sbin{do}\alpha\la Id_k \ra : \Ell^\iota_P(T,k));\beta\la Id_k \ra : \s{skip}
\\& \text{otherwise, if $S=\sop{while}b\sbin{do}T$,}\\[3pt]
\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)
\\&\text{if $S=\sop{if}b\sbin{then}T_1\sbin{else}T_2$,}\\[3pt]
\ldots
\end{array}
\right.
$$
where as usual $\alpha$ and $\beta$ are to be fresh cost labels, and other cases just keep
making the recursive calls on the substatements. The \emph{indexed labelling} of
a program $P$ is then defined as $\alpha\la \ra : \Ell^\iota_P(P,0)$, i.e.\ a
further fresh unindexed cost label is added at the start, and we start from level $0$.
In other words: each single-entry loop is indexed by $i_k$ where $k$ is the number of
other single-entry loops containing this one, and all cost labels under the scope
of a single-entry loop indexed by $i_k$ are indexed by all indexes $i_0,\ldots,i_k$,
without any transformation.
\subsection{Indexed labels and loop transformations}
We define the \emph{reindexing} $I \circ (i_k\mapsto a*i_k+b)$ as an operator
on indexings by setting
\begin{multline*}
(i_0\mapsto e_0,\ldots, i_k \mapsto e_k,\ldots,i_n\mapsto e_n)
\circ(i_k\mapsto a*i_k+b)
\ass\\
i_0\mapsto e_0,\ldots, i_k \mapsto e_k \circ(a*i_k+b),\ldots,i_n\mapsto e_n,
\end{multline*}
and extending then to indexed labels (by $\alpha\la I\ra\circ(i_k\mapsto e)\ass
\alpha\la I\circ (i_k\mapsto e)\ra$) and to statements in $\iota\ell\imp$
(by applying the above transformation to all indexed labels).
We can then redefine loop peeling and loop unrolling taking into account indexed labels.
It will be possible to apply the transformation only to indexed loops, that is loops
that are single-entry. The attentive reader will notice that no assumption is
made on the labelling of the statements involved. In particular the transformation
can be repeated and composed at will. Also, notice that erasing all labelling
information (i.e.\ indexed cost labels and loop indexes) we recover exactly the
same transformations presented in \autoref{sec:defimp}.
\paragraph{Indexed loop peeling.}
$$
i_k:\sop{while}b\sbin{do}S\mapsto
\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)
$$
As can be expected, the peeled iteration of the loop gets reindexed as always
being the first iteration of the loop, while the iterations of the remaining
loop get shifted by $1$.
\paragraph{Indexed loop unrolling.}
$$
\begin{array}{l}
\begin{array}{ncn}
i_k:\sop{while}b\sbin{do}S\\
\tikz\node[rotate=-90,inner sep=0pt]{$\mapsto$};
\end{array}\\
i_k:\sop{while} b \sbin{do}\\
\quad (S\circ(i_k\mapsto n*i_k) ;\\
\quad \sop{if} b \sbin{then}\\
\quad\quad (S[\ell^1_i/\ell_i]\circ(i_k\mapsto n*i_k+1) ;\\
\quad\quad\quad \vdots \\
\quad\quad \quad \sop{if} b \sbin{then}\\
\quad \quad \quad \quad S[\ell^n_i/\ell_i]\circ(i_k\mapsto n*i_k+n-1)
)\cdots )
\end{array}
$$
Again, the reindexing is as can be expected: each copy of the unrolled body
has its indexes remapped so that when they are executed the original iteration
of the loop to which they correspond can be recovered.
\subsection{Semantics and compilation of indexed labels}
In order to make sense of loop indexes, one must keep track of their values
in the state. A \emph{constant indexing} (metavariables $C,\ldots$) is an
indexing which employs only constant simple expressions. The evaluation
of an indexing $I$ in a constant indexing $C$, noted $I|_C$, is defined
by
$$I\circ(i_0\mapsto c_0,\ldots, i_{k-1}\mapsto c_{k-1}) \ass
\alphab\circ(i_0\mapsto c_0)\circ\cdots\circ(i_{k-1}\mapsto c_{k-1})$$
(using the definition of ${-}\circ{-}$ given in \autoref{ssec:indlabs}), considering it defined only
if the the resulting indexing is a constant one too\footnote{For example
$(i_0\mapsto 2*i_0,i_1\mapsto i_1+1)|_{i_0\mapsto 2}$ is undefined,
but $(i_0\mapsto 2*i_0,i_1\mapsto 0)|_{i_0\mapsto 2}=
i_0\mapsto 4,i_1\mapsto 2$, which is indeed a constant indexing,
even if the domain of the original indexing is not covered by the constant one.}.
The definition is extended to indexed labels by $\alpha\la I\ra|_C\ass \alpha\la I|_C\ra$.
Constant indexings will be used to keep track of the exact iterations of the
original code the emitted labels belong to. We thus define two basic actions to
update constant indexings: $C[i_k{\uparrow}]$ which increments the value of
$i_k$ by one, and $C[i_k{\downarrow}0]$ which resets it to $0$.
We are ready to update the definition of the operational semantics of
indexed labelled \imp. The emitted cost labels will now be ones indexed by
constant indexings. We add loop index increments as constructors to continuations%
\footnote{This is unneeded if we keep track of active loops (like is necessary
in the presence of \s{continue} and \s{break} statements).}:
$$K,\ldots \gramm \cdots | i_k{\uparrow} \cdot K$$
The state will now be a 4-uple
$(S,K,s,C)$ which adds a constant indexing to the 3-uple of regular
semantics. The small-step rules for all statements but the
cost-labelled ones and the indexed loops remain the same, without
touching the $C$ parameter (in particular unindexed loops behave the same
as usual). The remaining cases are:
$$\begin{aligned}
(\alphab : S,K,s,C) &\to[\alphab|_C]_P (S,K,s,C)\\
(i_k:\sop{while}b\sbin{do}S,K,C) &\to[\varepsilon]_P
\begin{cases}
(S,i_k{\uparrow} \cdot \sop{while}b\sbin{do}S\cdot K,s,C[i_k{\downarrow}0])
& \text{if $(b,s)\eval v\neq 0$,}\\
(\s{skip}, K, s, C) & \text{otherwise}
\end{cases}\\
(\s{skip},i_k{\uparrow} \cdot K,s,C) &\to[\varepsilon]_P (\s{skip}, K, s, C[i_k{\uparrow}])
\end{aligned}$$
The starting state with store $s$ for a program $P$ becomes then
$(P,\s{halt},s,(i_0\mapsto 0,\dots,i_{n-1}\mapsto 0)$ where $i_0,\ldots,i_{n-1}$ cover
all loop indexes of $P$\footnote{For a program which is the indexed labelling of an
\imp{} one this corresponds to the maximum nesting of single-entry loops. We can also
avoid computing this value in advance if we define $C[i{\downarrow}0]$ to extend
$C$'s domain as needed, so that the starting constant indexing can be the empty one.}.
\paragraph{Compilation.}
Further down the compilation chain the loop
structure is usually partially or completely lost. We cannot rely on it anymore
to ensure keeping track of original source code iterations. We therefore add
alongside the \s{emit} instruction two other sequential instructions
$\sop{ind_reset}k$ and $\sop{ind_inc}k$ whose sole effect is to reset to
0 (resp.\ increment by 1) the loop index $i_k$, as kept track of in a constant
indexing accompanying the state.
The first step of compilation from $\iota\ell\imp$ consists in prefixing the
translation of an indexed loop $i_k:\s{while}\ b\ \s{do}\ S$ with
$\sop{ind_reset}k$ and postfixing the translation of its body $S$ with
$\sop{ind_inc}k$. Later on in the compilation chain we just need to propagate
the instructions dealing with cost labels.
We would like to stress the fact that this machinery is only needed to give a
suitable semantics of observables on which preservation proofs can be done. By no
means the added instructions and the constant indexing in the state are meant
to change the actual (let us say denotational) semantics of the programs. In this
regard the two new instruction have a similar role as the \s{emit} one. A
forgetful mapping of everything (syntax, states, operational semantics rules)
can be defined erasing all occurrences of cost labels and loop indexes, and the
result will always be a regular version of the language considered.
\paragraph{Stating the preservation of semantics.} In fact, the statement of preservation
of semantics does not change at all, if not for considering traces of evaluated
indexed cost labels rather than traces of plain ones.
\subsection{Dependent costs in the source code}\label{ssec:depcosts}
The task of producing dependent costs out of the constant costs of indexed labels
is quite technical. Before presenting it here, we would like to point out that
the annotations produced by the procedure described in this subsection, even
if correct, can be enormous and unreadable. In \autoref{sec:conc}, when we will
detail the actual implementation, we will also sketch how we mitigated this
problem.
Having the result of compiling the indexed labelling $\Ell^\iota(P)$ of an \imp{}
program $P$, we can still suppose that a cost mapping can be computed, but
from indexed labels to naturals. We want to annotate the source code, so we need
a way to express and compute costs of cost labels, i.e.\ group the costs of
indexed labels to ones of their atoms. In order to do so we introduce
\emph{dependent costs}. Let us suppose that for the sole purpose of annotation,
we have available in the language ternary expressions of the form
$$\tern e {f_1}{f_2},$$
and that we have access to common operators on integers such as equality, order
and modulus.
\paragraph{Simple conditions.}
First, we need to shift from \emph{transformations} of loop indexes to
\emph{conditions} on them. We identify a set of conditions on natural numbers
which are able to express the image of any composition of simple expressions.
\emph{Simple conditions} are of three possible forms:
\begin{itemize}
\item equality $i_k=n$ for some natural $n$;
\item inequality $i_k\ge n$ for some natural $n$;
\item modular equality together with inequality $i_k\bmod a = b\wedge i_k\ge n$
for naturals $a, b, n$.
\end{itemize}
The always true simple condition is given by $i_k\ge 0$, and similarly we
write $i_k\bmod a = b$ as a simple condition for $i_k\bmod a = b\wedge i_k\ge 0$.
Given a simple condition $p$ and a constant indexing $C$ we can easily define
when $p$ holds for $C$ (written $p\circ C$). A \emph{dependent cost expression}
is an expression built solely out of integer constants and ternary expressions
with simple conditions at their head. Given a dependent cost expression $e$ where
all of the loop indexes appearing in it are in the domain of a constant indexing
$C$, we can define the value $e\circ C\in \mathbb N$ by
$$n\circ C\ass n,\qquad (\tern p e f)\circ C\ass
\begin{cases}
e\circ C& \text{if $p\circ C$,}\\
f\circ C& \text{otherwise.}
\end{cases}$$
\paragraph{From indexed costs to dependent ones.}
Every simple expression $e$ corresponds to a simple condition $p(e)$ which expresses the
set of values that can be the result of it. Following is the definition of such
relation. We recall that in this development loop indexes are always mapped to
simple expressions over the same index. If it was not the case, the condition
obtained from an expression should be on the mapped index, not the indeterminate
of the simple expression. We leave to further work all generalizations of what
we present here.
$$
p(a*i_k+b)\ass
\begin{cases}
i_k = b & \text{if $a = 0$,}\\
i_k \ge b & \text{if $a = 1$,}\\
i_k\bmod a = b \wedge i_k \ge b & \text{otherwise}.
\end{cases}$$
Now, suppose we are given a mapping $\kappa$ from indexed labels to natural
numbers. We will transform it in a mapping (identified with an abuse of notation
with the same symbol $\kappa$) from atoms to \imp{} expressions built with
ternary expressions which depend solely on loop indexes. To that end we define
an auxiliary function $\kappa^\alpha_L$ parameterized by atoms and words of
simple expressions and defined on \emph{sets} of $n$-uples of simple expressions
(with $n$ constant across each such set, i.e.\ each set is made of words with
the same length).
We will employ a bijection between words of simple expressions and indexings,
given by\footnote{Lists of simple expressions is in fact how indexings are
represented in Cerco's current implementation of the compiler.}
$$i_0\mapsto e_0,\ldots,i_{k-1}\mapsto e_{k-1} \cong e_0\cdots e_{k-1}.$$
As usual, $\varepsilon$ denotes the empty word/indexing, and juxtaposition
word concatenation.
For every set $s$ of $n$-uples of simple expressions, we are in one of the following
three exclusive cases:
\begin{itemize}
\item $S=\emptyset$, or
\item $S=\{\varepsilon\}$, or
\item there is a simple expression $e$ such that $S$ can be decomposed in
$eS'+S''$, with $S'\neq \emptyset$ and none of the words in $S''$ starting with $e$
\end{itemize}
where $eS'$ denotes prepending $e$ to all elements of $S'$ and $+$ is disjoint
union. This classification can serve as the basis of a definition by recursion
on $n+\card S$ where $n$ is the size of tuples in $S$ and $\card S$ is its cardinality.
Indeed in the third case in $S'$ the size of tuples decreases strictly (and
cardinality does not increase) while for $S''$ the size of tuples remains the same
but cardinality strictly decreases. The expression $e$ of the third case will be chosen
as minimal for some total order\footnote{The specific order used does not change
the correctness of the procedure, but different orders can give more or less
readable results. A ``good'' order is the lexicographic one, with $a*i_k+b \le a'*i_k+b'$
if $a= 1)?+y\verb+:+z
\mapsto
\verb+(_i_0 == 0)?+x\verb+:+y,
$
\item $
c\texttt{?}x\verb+:(+d\texttt{?}x\texttt{:}y\verb+)+
\mapsto
\texttt{(}c\texttt{ || }d\texttt{)?}x\texttt{:}y,
$
\item \begin{tabular}[t]{np{\linewidth}n}
$\verb+(_i_0 == 0)?+x\verb+:(_i_0 % 2 == 0 && _i_0 >= 2)?+y\verb+:+z
\mapsto$ \\\hfill
$\verb+(_i_0 == 0)?+x\verb+:(_i_0 % 2 == 0)?+y\verb+:+z.
$\end{tabular}
\end{itemize}
The second transformation tends to accumulate disjunctions, again to the detriment
of readability. A further transformation swaps two branches of the ternary
expression if the negation of the condition can be expressed with less clauses.
An example is
$$ \verb+(_i_0 % 3 == 0 || _i_0 % 3 == 1)?+x\verb+:+y \mapsto
\verb+(_i_0 % 3 == 2)?+y\verb+:+x.
$$
\paragraph{Updates to the frama-C cost plugin.}
Cerco's frama-C~\cite{framac} cost plugin\todo{is there a reference for this?}{}
has been updated to take into account dependent
costs. The frama-c framework explodes ternary expressions to actual branch
statements introducing temporaries along the way, which makes the task of
analyzing ternary cost expressions rather daunting. It was deemed necessary to provide
an option in the compiler to use actual branch statements for cost annotations
rather than ternary expressions, so that at least frama-C's use of temporaries in
cost annotation be avoided. The cost analysis carried out by the plugin now
takes into account such dependent costs.
The only limitation (which provided
a simplification in the code) is that within a dependent cost
simple conditions with modulus on the
same loop index should not be modulo different numbers, which corresponds to
the reasonable limitation of not applying multiple times loop unrolling to
the same loops.
\paragraph{Further work.}
Indexed labels are for now implemented only in the untrusted OcaML compiler,
while they are not present yet in the Matita code. Porting them should pose no
significant problem, and then the proof effort should begin.
Because most of the executable operational semantics of the languages across the
front end and the back end are oblivious to cost labels, it should be expected
that the bulk of the semantic preservation proofs that still needs to be done
will not get any harder because of indexed labels. The only trickier point
would be in the translation of \s{Clight} to \s{Cminor}, where we
pass from structured indexed loops to atomic instructions on loop indexes.
An invariant which should probably be proved and provably preserved along compilation
is the non-overlap of indexings for the same atom. Then, supposing cost
correctness for the unindexed approach, the indexed one will just need to
add the proof that
$$\forall C\text{ constant indexing}.\forall \alpha\la I\ra\text{ appearing in the compiled code}.
\kappa(\alpha)\circ (I\circ C) = \kappa(\alpha\la I \ra).$$
$C$ represents a snapshot of loop indexes in the compiled code, while
$I\circ C$ is the corresponding snapshot in the source code.
A part from carrying over the proofs, we would like to extend the approach
to more loop transformations. Important examples are loop inversion
(where a for loop is reversed, usually to make iterations appear as truly
independent) or loop interchange (where two nested loops are swapped, usually
to have more loop invariants or to enhance strength reduction). This introduces
interesting changes to the approach, where we would have indexings such as
$$i_0\mapsto n - i_0\quad\text{or}\quad i_0\mapsto i_1, i_1\mapsto i_0.$$
In particular dependency over actual variables of the code would enter the
frame, as indexings would depend on the number of iterations of a well-behaving
guarded loop (the $n$ in the first example).
%
% \newpage
%
% \includepdf[pages={-}]{plugin.pdf}
%
%
% \newpage
%
% \includepdf[pages={-}]{fopara.pdf}
%
%
% \newpage
%
% \includepdf[pages={-}]{tlca.pdf}
%
% \bibliographystyle{plain}
\bibliography{bib}
\end{document}