Changeset 3659
 Timestamp:
 Mar 16, 2017, 12:54:45 PM (3 months ago)
 Location:
 Papers/jarcerco2017
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Papers/jarcerco2017/cerco.tex
r3657 r3659 26 26 \usepackage{amsfonts} 27 27 \usepackage{amsmath} 28 \usepackage{amssymb} 28 \usepackage{amssymb} 29 \usepackage{array} 29 30 \usepackage[british]{babel} 30 31 \usepackage{color} 32 \usepackage{enumerate} 31 33 \usepackage{fancybox} 32 34 \usepackage{fancyvrb} … … 39 41 \usepackage{mdwlist} 40 42 \usepackage{microtype} 43 \usepackage{multirow} 41 44 \usepackage{stmaryrd} 42 45 \usepackage{url} … … 71 74 \DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}} 72 75 76 \newcolumntype{b}{@{}>{{}}} 77 \newcolumntype{B}{@{}>{{}}c<{{}}@{}} 78 \newcolumntype{h}[1]{@{\hspace{#1}}} 79 \newcolumntype{L}{>{$}l<{$}} 80 \newcolumntype{C}{>{$}c<{$}} 81 \newcolumntype{R}{>{$}r<{$}} 82 \newcolumntype{S}{>{$(}r<{)$}} 83 \newcolumntype{n}{@{}} 84 \newcommand{\spanr}[2]{\multicolumn{1}{Rn}{\multirow{#1}{*}{(#2)}}} 85 \def\nocol{\multicolumn{1}{ncn}{}} 86 73 87 \newcommand{\cerco}{CerCo} 74 88 \newcommand{\ocaml}{OCaml} … … 76 90 \newcommand{\matita}{Matita} 77 91 \newcommand{\sdcc}{\texttt{sdcc}} 92 93 \newcommand{\tern}[3]{#1\mathrel ? #2 : #3} 94 \newcommand{\sop}[1]{\s{#1}\ } 95 \newcommand{\sbin}[1]{\ \s{#1}\ } 96 \newcommand{\Ell}{\mathcal L} 97 \newcommand{\alphab}{\boldsymbol\alpha} 98 \newcommand{\betab}{\boldsymbol\beta} 99 \newcommand{\gramm}{\mathrel{::=}} 100 \newcommand{\ass}{\mathrel{:=}} 101 102 \renewcommand{\to}[1][]{\stackrel{#1}{\rightarrow}} 103 104 \newcommand{\eg}{\emph{e.g.\ }} 105 \newcommand{\ie}{\emph{i.e.\ }} 106 107 \newcommand{\inde}{\hspace{20pt}} 108 109 \usetikzlibrary{decorations.pathreplacing} 110 \newcommand{\tikztarget}[2]{% 111 \tikz[remember picture, baseline={(#1.base)}]{ 112 \node (#1) [inner sep = 0pt]{#2};}} 113 \newcommand{\tikztargetm}[2]{% 114 \tikz[remember picture, baseline={(#1.base)}]{ 115 \node (#1) [inner sep = 0pt]{$#2$};}} 116 117 \newenvironment{comment}{{\bf MORE WORK:}} 118 119 \newenvironment{restateproposition}[2][{}]{\noindent\textbf{Proposition~{#2}} 120 \;\textbf{#1}\ 121 }{\vskip 1em} 122 123 \newenvironment{restatetheorem}[2][{}]{\noindent\textbf{Theorem~{#2}}\;\textbf{ 124 #1}\ 125 }{\vskip 1em} 126 127 \newenvironment{restatecorollary}[2][{}]{\noindent\textbf{Corollary~{#2}} 128 \;\textbf{#1}\ 129 }{\vskip 1em} 130 131 \newcommand{\myparagraph}[1]{\medskip\noindent\textbf{#1}} 132 133 \newcommand{\Proofitemb}[1]{\medskip \noindent {\bf #1\;}} 134 \newcommand{\Proofitemfb}[1]{\noindent {\bf #1\;}} 135 \newcommand{\Proofitem}[1]{\medskip \noindent $#1\;$} 136 \newcommand{\Proofitemf}[1]{\noindent $#1\;$} 137 \newcommand{\Defitem}[1]{\smallskip \noindent $#1\;$} 138 \newcommand{\Defitemt}[1]{\smallskip \noindent {\em #1\;}} 139 \newcommand{\Defitemf}[1]{\noindent $#1\;$} 140 141 142 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 143 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 144 145 146 147 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 148 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 149 150 \newcommand{\eqdef}{=_{\text{def}}} 151 \newcommand{\concat}{\cdot}%%{\mathbin{+}} 152 \newcommand{\Int}{\mathit{int}} 153 \newcommand{\nat}{\mathit{nat}} 154 \newcommand{\String}{\mathit{string}} 155 \newcommand{\Ident}{\mathit{ident}} 156 \newcommand{\Block}{\mathit{block}} 157 \newcommand{\Signature}{\mathit{signature}} 158 159 \newcommand{\pc}{\mathit{pc}} 160 \newcommand{\estack}{\mathit{estack}} 161 \newcommand{\Error}{\epsilon} 162 163 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 164 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 165 166 %  % 167 % Proof rule. % 168 %  % 169 170 \newcommand{\staterule}[3]{% 171 $\begin{array}{@{}l}% 172 \mbox{#1}\\% 173 \begin{array}{c} 174 #2\\ 175 \hline 176 \raisebox{0ex}[2.5ex]{\strut}#3% 177 \end{array} 178 \end{array}$} 179 180 \newcommand{\GAP}{2ex} 181 182 \newcommand{\recall}[2]{% 183 $\begin{array}{c} 184 #1\\ 185 \hline 186 \raisebox{0ex}[2.5ex]{\strut}#2% 187 \end{array}$} 188 189 \newcommand{\hbra}{\noindent\hbox to \textwidth{\leaders\hrule height1.8mm 190 depth1.5mm\hfill}} 191 \newcommand{\hket}{\noindent\hbox to \textwidth{\leaders\hrule 192 height0.3mm\hfill}} 193 \newcommand{\ratio}{.3} 194 195 \newenvironment{display}[1]{\begin{tabbing} 196 \hspace{1.5em} \= \hspace{\ratio\linewidth1.5em} \= \hspace{1.5em} \= \kill 197 \noindent\hbra\\[.5em] 198 {\ }\textsc{#1}\\[.8ex] 199 \hbox to \textwidth{\leaders\hrule height1.6mm depth1.5mm\hfill}\\[.8ex] 200 }{\\[.8ex]\hket 201 \end{tabbing}} 202 203 204 \newcommand{\sbline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.2ex} 205 \hfill\hspace*{0ex}}} 206 \newcommand{\sline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.1ex} 207 \hfill\hspace*{0ex}}} 208 \newcommand{\sentry}[2]{\>$#1$\>\ \smash[t]{\vrule width 0.2mm height 209 1.2\baselineskip depth 1.5\baselineskip}\>#2} 210 211 \newcommand{\entry}[2]{\>$#1$\>\>#2} 212 \newcommand{\clause}[2]{$#1$\>\>#2} 213 \newcommand{\category}[2]{\clause{#1::=}{#2}} 214 \newcommand{\subclause}[1]{\>\>\>#1} 215 \newcommand{\redrule}[3]{$#1$\>\>$#2$\>\>\>#3} 216 % proofs 217 218 \newcommand{\Proof}{\noindent {\sc Proof}. } 219 \newcommand{\Proofhint}{\noindent {\sc Proof hint}. } 220 \newcommand{\EndProof}{\qed} 221 222 % figure environment 223 224 \newcommand{\Figbar}{{\center \rule{\hsize}{0.3mm}}} 225 %horizontal thiner line for figures 226 \newenvironment{figureplr}[1][t]{\begin{figure}[#1] \Figbar}{\Figbar \end{figure}} 227 %environment for figures 228 % ************Macros for mathematical symbols************* 229 % Style 230 231 \newcommand{\cl}[1]{{\cal #1}} % \cl{R} to make R calligraphic 232 \newcommand{\la}{\langle} % the brackets for pairing (see also \pair) 233 \newcommand{\ra}{\rangle} 234 235 \newcommand{\lf}{\lfloor} 236 \newcommand{\rf}{\rfloor} 237 \newcommand{\ul}[1]{\underline{#1}} % to underline 238 \newcommand{\ol}[1]{\overline{#1}} % to overline 239 \newcommand{\ok}{~ok} % well formed context 240 241 % Syntax 242 243 \newcommand{\Gives}{\vdash} % in a type judgment 244 \newcommand{\IGives}{\vdash_{I}} % intuitionistic provability 245 \newcommand{\AIGives}{\vdash_{{\it AI}}} %affineintuitionistic provability 246 \newcommand{\CGives}{\vdash_{C}} % affineintuitionistic confluent provability 247 248 249 \newcommand{\Models}{\mid \! =} % models 250 251 \newcommand{\emptycxt}{\On} % empty context 252 \newcommand{\subs}[2]{[#1 / #2]} 253 \newcommand{\sub}[2]{[#2 / #1]} % substitution \sub{x}{U} gives [U/x] 254 255 \newcommand{\Sub}[3]{[#3 / #2]#1} % Substitution with three arguments \Sub{V}{x}{U} 256 257 \newcommand{\lsub}[2]{#2 / #1} % substitution \lsub{x}{U} gives U/x, to be used in a list. 258 259 \newcommand{\impl}{\supset} 260 \newcommand{\arrow}{\rightarrow} % right thin arrow 261 \newcommand{\trarrow}{\stackrel{*}{\rightarrow}} % trans closure 262 %\newcommand{\limp}{\makebox[5mm]{\,$ \! {\circ}\,$}} % linear 263 % implication 264 \newcommand{\limp}{\multimap} %linear implication 265 \newcommand{\bang}{\, !} 266 % LNCS 267 %\newcommand{\bang}{\oc} 268 \newcommand{\limpe}[1]{\stackrel{#1}{\multimap}} 269 %\newcommand{\hyp}[3]{#1:(#2, #3)} 270 \newcommand{\letm}[3]{{\sf let} \ ! #1 = #2 \ {\sf in} \ #3} % modal let 271 \newcommand{\lets}[3]{{\sf let} \ #1 = #2 \ {\sf in} \ #3} % simple let 272 \newcommand{\letp}[3]{{\sf let} \ \S #1 = #2 \ {\sf in} \ #3} % paragraph let 273 \newcommand{\tertype}{{\bf 1}} 274 \newcommand{\behtype}{{\bf B}} 275 \newcommand{\bt}[1]{{\it BT}(#1)} % Boehm tree 276 \newcommand{\cxt}[1]{#1[~]} % Context with one hole 277 \newcommand{\pr}{\parallel} % parallel  278 \newcommand{\Nat}{\mathbf{N}} % natural numbers 279 \newcommand{\Natmax}{\mathbf{N}_{{\it max}}} % natural numbers with minus infinity 280 \newcommand{\Rat}{\mathbf{Q}^{+}} % nonnegative rationals 281 \newcommand{\Ratmax}{\mathbf{Q}^{+}_{{\it max}}} % nonnegative rationals with minus infinity 282 %\newcommand{\Alt}{ \mid\!\!\mid } 283 \newcommand{\isum}{\oplus} 284 \newcommand{\csum}{\uplus} %context sum 285 \newcommand{\dpar}{\mid\!\mid} 286 \newcommand{\todo}[1]{} 287 % for the production of a grammar containing \mid 288 \newcommand{\infer}[2]{\begin{array}{c} #1 \\ \hline #2 \end{array}} 289 % to make a centered inference rule 290 291 % (Meta)Logic 292 293 \newcommand{\bool}{{\sf bool}} % boolean values 294 \newcommand{\Or}{\vee} % disjunction 295 \newcommand{\OR}{\bigvee} % big disjunction 296 \newcommand{\AND}{\wedge} % conjunction 297 \newcommand{\ANDD}{\bigwedge} % big conjunction 298 \newcommand{\Arrow}{\Rightarrow} % right double arrow 299 \newcommand{\IFF}{\mbox{~~iff~~}} % iff in roman and with spaces 300 \newcommand{\iffArrow}{\Leftrightarrow} % logical equivalence 301 302 % Semantics 303 304 \newcommand{\dl}{[\![} % semantic [[ 305 \newcommand{\dr}{]\!]} % semantic ]] 306 307 308 % The equivalences for this paper 309 310 % the usual ones 311 \newcommand{\ubis}{\approx^u} % usual labelled weak bis 312 \newcommand{\uabis}{\approx^{u}_{ccs}} % usual labelled weak bis on CCS 313 314 % the contextual conv sensitive 315 \newcommand{\cbis}{\approx} % convergence sensitive bis 316 \newcommand{\cabis}{\approx_{ccs}} % convergence sensitive bis on CCS 317 318 % the labelled conv sensitive 319 \newcommand{\lcbis}{\approx^{\ell}} % 320 \newcommand{\lcabis}{\approx^{\ell}_{ccs}} % labelled convergence sensitive bis on CCS 321 \newcommand{\lcbiswrong}{\approx^{\ell \Downarrow}} % 322 323 \newcommand{\maytest}{=_{\Downarrow}} 324 \newcommand{\musttest}{=_{\Downarrow_{S}}} 325 326 % Sets 327 328 \newcommand{\prt}[1]{{\cal P}(#1)} % Parts of a set 329 \newcommand{\finprt}[1]{{\cal P}_{fin}(#1)}% Finite parts 330 \newcommand{\finprtp}[1]{{\cal P}_{fin}^{+}(#1)}% Nonempty Finite parts 331 \newcommand{\union}{\cup} % union 332 \newcommand{\inter}{\cap} % intersection 333 \newcommand{\Union}{\bigcup} % big union 334 \newcommand{\Inter}{\bigcap} % big intersection 335 \newcommand{\cpl}[1]{#1^{c}} % complement 336 \newcommand{\card}{\sharp} % cardinality 337 \newcommand{\minus}{\backslash} % set difference 338 \newcommand{\sequence}[2]{\{#1\}_{#2}} % ex. \sequence{d_n}{n\in \omega} 339 \newcommand{\comp}{\circ} % functional composition 340 %\newcommand{\oset}[1]{\{#1\}} % set enumeration 341 \newcommand{\mset}[1]{\{\!  #1 \!\}} % pseudoset notation { } 342 343 % Domains 344 345 \newcommand{\two}{{\bf O}} % Sierpinski space 346 \newcommand{\join}{\vee} % join 347 \newcommand{\JOIN}{\bigvee} % big join 348 \newcommand{\meet}{\wedge} % meet 349 \newcommand{\MEET}{\bigwedge} % big meet 350 \newcommand{\dcl}{\downarrow} % down closure 351 \newcommand{\ucl}{\uparrow} % up closure 352 \newcommand{\conv}{\downarrow} % synt. conv. pred. (postfix) 353 \newcommand{\diver}{\uparrow} % diverging term 354 \newcommand{\Conv}{\Downarrow} % sem. conv. pred. (postfix) 355 \newcommand{\SConv}{\Downarrow_{S}} % sem. conv. pred. (postfix) 356 \newcommand{\CConv}{\Downarrow_{C}} 357 \newcommand{\Diver}{\Uparrow} % diverging map 358 \newcommand{\cpt}[1]{{\cal K}(#1)} % compacts, write \cpt{D} 359 \newcommand{\ret}{\triangleleft} % retract 360 \newcommand{\nor}{\succeq} 361 \newcommand{\prj}{\underline{\ret}} % projection 362 \newcommand{\parrow}{\rightharpoonup} % partial function space 363 \newcommand{\ub}[1]{{\it UB}(#1)} % upper bounds 364 \newcommand{\mub}[1]{{\it MUB}(#1)} % minimal upper bounds 365 \newcommand{\lift}[1]{(#1)_{\bot}} % lifting 366 \newcommand{\forget}[1]{\underline{#1}} % forgetful translation 367 368 %\newcommand{\rel}[1]{\;{\cal #1}\;} % infix relation (calligraphic) 369 \newcommand{\rl}[1]{\;{\cal #1}\;} % infix relation 370 \newcommand{\rel}[1]{{\cal #1}} %calligraphic relation with no 371 %extra space 372 \newcommand{\per}[1]{\;#1 \;} 373 \newcommand{\wddagger}{\natural} % weak suspension 374 %\newcommand{\wddagger}{=\!\!\!\!\parallel} % weak suspension 375 % Categories 376 377 \newcommand{\pair}[2]{\langle #1 , #2 \rangle} % pairing \pair{x}{y}, do not use < >. 378 379 % ******* Notation for the $\pi$calculus ********* 380 % Syntax: 381 382 \newcommand{\fn}[1]{{\it fn}(#1)} % free names 383 \newcommand{\bn}[1]{{\it bn}(#1)} % bound names 384 \newcommand{\names}[1]{{\it n}(#1)} % names 385 \newcommand{\true}{{\sf t}} % true 386 \newcommand{\false}{{\sf f}} % false 387 \newcommand{\pio}{\pi_1} % 1 receptor calculus 388 \newcommand{\pioo}{\pi_{1}^{r}} 389 \newcommand{\piom}{\pi_{1}^{}} % 1 receptor calculus wo match 390 \newcommand{\pioi}{\pi_{1I}} % 1 receptor Icalculus 391 \newcommand{\pifo}{\pi_{\w{1f}}} % functional calculus 392 \newcommand{\pilo}{\pi_{\w{1l}}} % located calculus 393 \newcommand{\sort}[1]{{\it st}(#1)} % sort 394 \newcommand{\ia}[1]{{\it ia}(#1)} % sort 395 \newcommand{\ite}[3]{{\sf if~} #1 {\sf ~then~} #2 {\sf ~else~} #3} %if then else 396 \newcommand{\casep}[2]{{\sf case}^{\times}(#1, \pair{x}{y}\Arrow#2)} %case on pairs 397 \newcommand{\casel}[3]{{\sf case}^{L}(#1, #2, \s{cons}(x,y)\Arrow#3)} %case on lists 398 \newcommand{\caseb}[3]{{\sf case}^{b}(#1, #2, \s{cons}(x,y)\Arrow#3)} %case on lists 399 \newcommand{\nil}{{\sf nil}} 400 \newcommand{\cons}{{\sf cons}} 401 \newcommand{\idle}[1]{{\it Idle}(#1)} %idle process 402 \newcommand{\conf}[1]{\{ #1 \}} %configuration 403 \newcommand{\link}[2]{#1 \mapsto #2} %likn a >b 404 \newcommand{\mand}{\mbox{ and }} 405 \newcommand{\dvec}[1]{\tilde{{\bf #1}}} %double vector 406 \newcommand{\erloc}[1]{{\it er}_{l}(#1)} % location erasure 407 \newcommand{\w}[1]{{\it #1}} %To write in math style 408 \newcommand{\vcb}[1]{{\bf #1}} 409 \newcommand{\lc}{\langle\!} 410 \newcommand{\rc}{\!\rangle} 411 \newcommand{\obj}[1]{{\it obj}(#1)} 412 \newcommand{\move}[1]{{\sf move}(#1)} 413 \newcommand{\qqs}[2]{\forall\, #1\;\: #2} 414 \newcommand{\qtype}[4]{\forall #1 : #2 . (#4,#3)} 415 \newcommand{\xst}[2]{\exists\, #1\;\: #2} 416 \newcommand{\xstu}[2]{\exists\, ! #1\;\: #2} 417 \newcommand{\dpt}{\,:\,} 418 \newcommand{\cond}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3} 419 \newcommand{\s}[1]{{\sf #1}} % sansserif 420 \newcommand{\vc}[1]{{\bf #1}} 421 \newcommand{\lnorm}{\lbrack\!\lbrack} 422 \newcommand{\rnorm}{\rbrack\!\rbrack} 423 \newcommand{\sem}[1]{\underline{#1}} 424 \newcommand{\tra}[1]{\langle #1 \rangle} 425 \newcommand{\trb}[1]{[ #1 ]} 426 \newcommand{\squn}{\mathop{\scriptstyle\sqcup}} 427 \newcommand{\lcro}{\langle\!} 428 \newcommand{\rcro}{\!\rangle} 429 \newcommand{\semi}[1]{\lcro #1\rcro} 430 \newcommand{\sell}{\,\ell\,} 431 \newcommand{\SDZ}[1]{\marginpar{\textbf{SDZ:} {#1}}} 432 433 \newcommand{\when}[3]{{\sf when}~#1~{\sf then}~#2~{\sf else}~#3} 434 \newcommand{\wthen}[2]{{\sf when}~#1~{\sf then}~#2~} 435 \newcommand{\welse}[1]{{\sf else}~#1} 436 437 %Pour la fleche double, il faut rajouter : 438 % \usepackage{mathtools} 439 440 \newcommand{\act}[1]{\xrightarrow{#1}} %labelled actionlow %high 441 442 \newcommand{\lact}[1]{\stackrel{#1}{\makebox[5mm]{\,$ \! {\circ}\,$}}} 443 444 \newcommand{\set}[1]{\{#1\}} 445 \newcommand{\pst}[2]{{\sf pset}(#1,#2)} 446 \newcommand{\st}[2]{{\sf set}(#1,#2)} 447 \newcommand{\wrt}[2]{{\sf w}(#1,#2)} 448 449 \newcommand{\chtype}[2]{{\it Ch_{#1}(#2)}} 450 \newcommand{\rgtype}[2]{{\it {\sf Reg}_{#1} #2}} 451 452 \newcommand{\get}[1]{{\sf get}(#1)} 453 454 %\newcommand{\wact}[1]{\xRightarrow{#1}} %weak labelled action low high 455 456 %\newcommand{\mact}[1]{\xrightarrow{#1}_{m}} %labelled action low %high 457 458 %\newcommand{\wmact}[1]{\xRightarrow{#1}_{m}} %weak labelled action low high 459 460 %\newcommand{\act}[1]{\stackrel{#1}{\rightarrow}} %labelled action low 461 %%%high 462 463 \newcommand{\acteq}[1]{\stackrel{#1}{\leadsto}} %labelled action low 464 %%%high 465 466 467 %\newcommand{\actI}[1]{\stackrel{#1}{\rightarrow_{1}}} %labelled action low 468 \newcommand{\actI}[1]{\xrightarrow{#1}_{1}} 469 470 %\newcommand{\actII}[1]{\stackrel{#1}{\rightarrow_{2}}} %labelled action low 471 \newcommand{\actII}[1]{\xrightarrow{#1}_{2}} 472 473 474 \newcommand{\wact}[1]{\stackrel{#1}{\Rightarrow}} %weak labelled action low high 475 \newcommand{\wactI}[1]{\stackrel{#1}{\Rightarrow_{1}}} %weak labelled action low high 476 \newcommand{\wactII}[1]{\stackrel{#1}{\Rightarrow_{2}}} %weak labelled action low high 477 478 479 \newcommand{\mact}[1]{\stackrel{#1}{\rightarrow_{m}}} %labelled action low 480 %high 481 \newcommand{\wmact}[1]{\stackrel{#1}{\Rightarrow_{m}}} %weak labelled action low high 482 483 %\newcommand{\lact}[1]{\stackrel{#1}{\leftarrow}} 484 \newcommand{\lwact}[1]{\stackrel{#1}{\Leftarrow}} 485 486 487 488 \newcommand{\eval}{\Downarrow} 489 \newcommand{\Eval}[1]{\Downarrow^{#1}} 490 491 492 \newcommand{\Z}{{\bf Z}} 493 \newcommand{\Real}{\mathbb{R}^{+}} 494 \newcommand{\Return}{\ensuremath{\mathtt{return}}\xspace} 495 \newcommand{\Stop}{\ensuremath{\mathtt{stop}}\xspace} 496 \newcommand{\Wait}{\ensuremath{\mathtt{wait}}\xspace} 497 \newcommand{\Read}{\ensuremath{\mathtt{read}}\xspace} 498 \newcommand{\Write}{\ensuremath{\mathtt{write}}\xspace} 499 \newcommand{\Yield}{\ensuremath{\mathtt{yield}}\xspace} 500 \newcommand{\Next}{\ensuremath{\mathtt{next}}\xspace} 501 \newcommand{\Load}{\ensuremath{\mathtt{load}}\xspace} 502 \newcommand{\Call}{\ensuremath{\mathtt{call}}\xspace} 503 \newcommand{\Tcall}{\ensuremath{\mathtt{tcall}}\xspace} 504 \newcommand{\Pop}{\ensuremath{\mathtt{pop}}\xspace} 505 \newcommand{\Build}{\ensuremath{\mathtt{build}}\xspace} 506 \newcommand{\Branch}{\ensuremath{\mathtt{branch}}\xspace} 507 \newcommand{\Goto}{\ensuremath{\mathtt{goto}}\xspace} 508 509 \newcommand{\hatt}[1]{#1^{+}} 510 \newcommand{\Of}{\mathbin{\w{of}}} 511 512 \newcommand{\susp}{\downarrow} 513 \newcommand{\lsusp}{\Downarrow_L} 514 \newcommand{\wsusp}{\Downarrow} 515 \newcommand{\commits}{\searrow} 516 517 518 \newcommand{\spi}{S\pi} 519 520 521 \newcommand{\pres}[2]{#1\triangleright #2} %TCCS else next (alternative) 522 % \newcommand{\pres}[2]{ \lfloor #1 \rfloor (#2)} %TCCS else next 523 \newcommand{\present}[3]{{\sf present} \ #1 \ {\sf do } \ #2 \ {\sf else} \ #3} 524 525 526 \newcommand{\tick}{{\sf tick}} %tick action 527 528 529 530 \newcommand{\sbis}{\equiv_L} 531 \newcommand{\emit}[2]{\ol{#1}#2} 532 %\newcommand{\present}[4]{#1(#2).#3,#4} 533 \newcommand{\match}[4]{[#1=#2]#3,#4} %piequality 534 535 \newcommand{\matchv}[4]{[#1 \unrhd #2]#3,#4} 536 537 \newcommand{\new}[2]{\nu #1 \ #2} 538 \newcommand{\outact}[3]{\new{{\bf #1}}{\emit{#2}{#3}}} 539 \newcommand{\real}{\makebox[5mm]{\,$\\!$}}% realizability relation 540 541 \newcommand{\regterm}[2]{{\sf reg}_{#1} #2} 542 \newcommand{\thread}[1]{{\sf thread} \ #1} 543 \newcommand{\store}[2]{(#1 \leftarrow #2)} 544 \newcommand{\pstore}[2]{(#1 \Leftarrow #2)} 545 546 \newcommand{\regtype}[2]{{\sf Reg}_{#1} #2} 547 \newcommand{\uregtype}[3]{{\sf Reg}_{#1}(#2, #3)} 548 \newcommand{\urtype}[2]{{\sf Reg}(#1, #2)} 549 550 \newcommand{\upair}[2]{[#1,#2]} 551 \newcommand{\letb}[3]{\mathsf{let}\;\oc #1 = #2\;\mathsf{in}\;#3} 552 553 \newcommand{\vlt}[1]{{\cal V}(#1)} 554 \newcommand{\prs}[1]{{\cal P}(#1)} 555 556 \newcommand{\imp}{{\sf Imp}} %imp language 557 \newcommand{\vm}{{\sf Vm}} %virtual machine language 558 \newcommand{\mips}{{\sf Mips}} %Mips language 559 \newcommand{\C}{{\sf C}} % C language 560 \newcommand{\Clight}{{\sf Clight}} %C light language 561 \newcommand{\Cminor}{{\sf Cminor}} 562 \newcommand{\RTLAbs}{{\sf RTLAbs}} 563 \newcommand{\RTL}{{\sf RTL}} 564 \newcommand{\ERTL}{{\sf ERTL}} 565 \newcommand{\LTL}{{\sf LTL}} 566 \newcommand{\LIN}{{\sf LIN}} 567 \newcommand{\access}[1]{\stackrel{#1}{\leadsto}} 568 569 \newcommand{\codeex}[1]{\texttt{#1}} % code example 78 570 79 571 \title{CerCo: Certified Complexity\thanks{The project CerCo acknowledges the 
Papers/jarcerco2017/proof.tex
r3657 r3659 5 5 % Technical issues in front end (Brian?) 6 6 % Main theorem statement 7 8 \section{Introduction} 9 In~\cite{D2.1}, Armadio \emph{et al} propose an approach for building a compiler for a large fragment of the \textsc{c} programming language. 10 The novelty of their proposal lies in the fact that their proposed design is capable of lifting execution cost information from the compiled code and presenting it to the user. 11 This idea is foundational for the CerCo project, which strives to produce a mechanically certified version of such a compiler. 12 13 To summarise, Armadio's proposal consisted of `decorations' on the source code, along with the insertion of labels at key points. 14 These labels are preserved as compilation progresses, from one intermediate language to another. 15 Once the final object code is produced, such labels should correspond to the parts of the compiled code that have a constant cost. 16 17 Two properties must hold of any cost estimate. 18 The first property, paramount to the correctness of the method, is \emph{soundness}, that is, that the actual execution cost is bounded by the estimate. 19 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. 20 The second property, optional but desirable, is \emph{preciseness}: the estimate \emph{is} the actual cost. 21 In the labelling approach, this will be true if, for every label, every possible execution of the compiled code starting from such a label yields the same cost before hitting another one. 22 In simple architectures such as the 8051 microcontroller this can be guaranteed by placing labels at the start of any branch in the control flow, and by ensuring that no labels are duplicated. 23 24 The reader should note that the above mentioned requirements must hold when executing the code obtained at the end of the compilation chain. 25 So even if one is careful about injecting the labels at suitable places in the source code, the requirements might still fail because of two main obstacles: 26 \begin{itemize} 27 \item 28 The compilation process introduces important changes in the control flow, inserting loops or branches. 29 For example, the insertion of functions in the source code replacing instructions that are unavailable in the target architecture. 30 This require loops to be inserted (for example, for multiword division and generic shift in the 8051 architecture), or effort spent in providing unbranching translations of higher level instructions~\cite{D2.2}. 31 \item 32 Even when the compiled code \emph{does}as far as the the syntactic control flow graph is concernedrespect 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. 33 This becomes a concern if one wishes to apply the approach to more complex architectures, for example one with caching or pipelining. 34 \end{itemize} 35 The first point unveils a weakness of the current labelling approach when it comes to some common code transformations performed along a compilation chain. 36 In particular, most \emph{loop optimisations} are disruptive, in the sense outlined in the first bulletpoint above. 37 An example optimisation of this kind is \emph{loop peeling}. 38 This optimisation is employed by compilers in order to trigger other optimisations, for example, dead code elimination or invariant code motion. 39 Here, a first iteration of the loop is hoisted out of the body of the loop, possibly being assigned a different cost than later iterations. 40 41 The second bulletpoint above highlights another weakness. Different tools allow to predict up to a certain extent the behaviour of cache. 42 For example, the well known tool \s{aiT}~\cite{absint}based on abstract interpretationallows the user to estimate the worstcase execution time (\textsc{wcet}) of a piece of source code, taking into account advanced features of the target architecture. While 43 such a tool is not fit for a compositional approach which is central to CerCo's project\footnote{\s{aiT} assumes the cache is empty at the start of computation, and treats each procedure call separately, unrolling a great part of the control flow.}, 44 \s{aiT}'s ability to produce tight estimates of execution costs would sthill enhance the effectiveness of the CerCo compiler, \eg{} by integrating such techniques in its development. 45 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. 46 47 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 the compilation, or the costs being sensitive to the current state of execution. 48 The preliminary work we present here addresses this weakness by introducing cost labels that are dependent on which iteration of its containing loops it occurs in. 49 This is achieved by means of \emph{indexed labels}; all cost labels are decorated with formal indices coming from the loops containing such labels. 50 These indices allow us to rebuild, even after multiple loop transformations, which iterations of the original loops in the source code a particular label occurrence belongs to. 51 During the annotation stage of the source code, this information is presented to the user by means of \emph{dependent costs}. 52 53 We concentrate on integrating the labelling approach with two loop transformations. 54 For general information on general compiler optimisations (and loop optimisations in particular) we refer the reader to the vast literature on the subject (\eg\cite{muchnick,morgan}). 55 56 \paragraph{Loop peeling} 57 As already mentioned, loop peeling consists in preceding the loop with a copy of its body, appropriately guarded. 58 This is used, in general, to trigger further optimisations, such as those that rely on execution information which can be computed at compile time, but which is erased by further iterations of the loop, or those that use the hoisted code to be more effective at eliminating redundant code. 59 Integrating this transformation in to the labelling approach would also allow the integration of the common case of cache analysis explained above; the analysis of cache hits and misses usually benefits from a form of \emph{virtual} loop peeling~\cite{cacheprediction}. 60 61 \paragraph{Loop unrolling} 62 This optimisation consists of the repetition of several copies of the body of the loop inside the loop itself (inserting appropriate guards, or avoiding them altogether if enough information about the loop's guard is available at compile time). 63 This can limit the number of (conditional or unconditional) jumps executed by the code and trigger further optimisations dealing with pipelining, if appropriate for the architecture. 64 \\\\ 65 Whilst we cover only two loop optimisations in this report, we argue that the work presented herein poses a good foundation for extending the labelling approach, in order to cover more and more common optimisations, as well as gaining insight into how to integrate advanced cost estimation techniques, such as cache analysis, into the CerCo compiler. 66 Moreover loop peeling itself has the fortuitous property of enhancing and enabling other optimisations. 67 Experimentation with CerCo's untrusted prototype compiler, which implements constant propagation and partial redundancy elimination~\cite{PRE,muchnick}, show how loop peeling enhances those other optimisations. 68 69 \paragraph{Outline} 70 We will present our approach on a minimal `toy' imperative language, \imp{} with \s{goto}s, which we present in Section~\ref{sec:defimp} along with formal definitions of the loop transformations. 71 This language already presents most of the difficulties encountered when dealing with \textsc{c}, so we stick to it for the sake of this presentation. 72 In Section~\ref{sec:labelling} we summarize the labelling approach as presented in~\cite{D2.1}. 73 Section~\ref{sec:indexedlabels} presents \emph{indexed labels}, our proposal for dependent labels which are able to describe precise costs even in the presence of the various loop transformations we consider. 74 Finally Section~\ref{sec:conc} goes into more detail regarding the implementation of indexed labels in CerCo's untrusted compiler and speculates on further work on the subject. 75 76 \section{\imp{} with goto}\label{sec:defimp} 77 We briefly outline the toy language, \imp{} with \s{goto}s. 78 The language was designed in order to pose problems for the existing labelling approach, and as a testing ground for our new notion of indexed labels. 79 80 The syntax and operational semantics of our toy language are presented in~\ref{fig:minimp}. 81 Note, we may augment the language further, with \s{break} and \s{continue}, at no further expense. 82 \begin{figureplr} 83 $$\begin{gathered} 84 \begin{array}{nlBl>(R<)n} 85 \multicolumn{4}{C}{\bfseries Syntax}\\ 86 \multicolumn{4}{ncn}{ 87 \ell,\ldots \hfill \text{(labels)} \hfill x,y,\ldots \hfill 88 \text{(identifiers)} 89 \hfill e,f,\ldots \hfill \text{(expression)} 90 }\\ 91 P,S,T,\ldots &\gramm& \s{skip} \mid s;t 92 \mid \sop{if}e\sbin{then}s\sbin{else}t 93 \mid \sop{while} e \sbin{do} s \mid 94 x \ass e 95 \\&\mid& 96 \ell : s \mid \sop{goto}\ell& \spanr{2}{statements}\\ 97 \\ 98 \multicolumn{4}{C}{\bfseries Semantics}\\ 99 K,\ldots &\gramm& \s{halt} \mid S \cdot K & continuations 100 \end{array} 101 \\[15pt] 102 \s{find}(\ell,S,K) \ass 103 \left\{\begin{array}{lL} 104 \bot & if $S=\s{skip},\sop{goto} \ell'$ or $x\ass e$,\\ 105 (T, K) & if $S=\ell:T$,\\ 106 \s{find}(\ell,T,K) & otherwise, if $S = \ell':T$,\\ 107 \s{find}(\ell,T_1,T_2\cdot K) & if defined and $S=T_1;T_2$,\\ 108 \s{find}(\ell,T_1,K) & if defined and 109 $S=\sop{if}b\sbin{then}T_1\sbin{else}T_2$,\\ 110 \s{find}(\ell,T_2,K) & otherwise, if $S=T_1;T_2$ or 111 $\sop{if}b\sbin{then}T_1\sbin{else}T_2$,\\ 112 \s{find}(\ell,T,S\cdot K) & if $S = \sop{while}b\sbin{do}T$. 113 \end{array}\right. 114 \\[15pt] 115 \begin{array}{lBl} 116 (x:=e,K,s) &\to_P& (\s{skip},K,s[v/x]) \qquad\mbox{if }(e,s)\eval v \\ \\ 117 118 (S;T,K,s) &\to_P& (S,T\cdot K,s) \\ \\ 119 120 (\s{if} \ b \ \s{then} \ S \ \s{else} \ T,K,s) 121 &\to_P&\left\{ 122 \begin{array}{ll} 123 (S,K,s) &\mbox{if }(b,s)\eval v \neq 0 \\ 124 (T,K,s) &\mbox{if }(b,s)\eval 0 125 \end{array} 126 \right. \\ \\ 127 128 129 (\s{while} \ b \ \s{do} \ S ,K,s) 130 &\to_P&\left\{ 131 \begin{array}{ll} 132 (S,\s{while} \ b \ \s{do} \ S \cdot K,s) &\mbox{if }(b,s)\eval v \neq 0 \\ 133 (\s{skip},K,s) &\mbox{if }(b,s)\eval 0 134 \end{array} 135 \right. \\ \\ 136 137 138 (\s{skip},S\cdot K,s) &\to_P&(S,K,s) \\ \\ 139 140 (\ell : S, K, s) &\to_P& (S,K,s) \\ \\ 141 142 (\sop{goto}\ell,K,s) &\to_P& (\s{find}(\ell,P,\s{halt}),s) \\ \\ 143 \end{array} 144 \end{gathered}$$ 145 \caption{The syntax and operational semantics of \imp.} 146 \label{fig:minimp} 147 \end{figureplr} 148 The precise grammar for expressions is not particularly relevant so we do not give one in full. 149 For the sake of conciseness we also treat boolean and arithmetic expressions together (with the usual \textsc{c} convention of an expression being true iff nonzero). 150 We may omit the \s{else} clause of a conditional if it leads to a \s{skip} statement. 151 152 We will presuppose that all programs are \emph{welllabelled}, \ie every label labels at most one occurrence of a statement in a program, and every \s{goto} points to a label actually present in the program. 153 The \s{find} helper function has the task of not only finding the labelled statement in the program, but also building the correct continuation. 154 The continuation built by \s{find} replaces the current continuation in the case of a jump. 155 156 \paragraph{Further down the compilation chain} 157 We abstract over the rest of the compilation chain. 158 We posit the existence of a suitable notion of `sequential instructions', wherein each instruction has a single natural successor to which we can add our own, for every language $L$ further down the compilation chain. 159 160 \subsection{Loop transformations} 161 We call a loop $L$ \emph{singleentry} in $P$ if there is no \s{goto} to $P$ outside of $L$ which jumps into $L$.\footnote{This is a reasonable aproximation: it defines a loop as multientry if it has an external but unreachable \s{goto} jumping into it.} 162 Many loop optimisations do not preserve the semantics of multientry loops in general, or are otherwise rendered ineffective. 163 Usually compilers implement a singleentry loop detection which avoids the multientry ones from being targeted by optimisations~\cite{muchnick,morgan}. 164 The loop transformations we present are local, \ie they target a single loop and transform it. 165 Which loops are targeted may be decided by some \emph{ad hoc} heuristic. 166 However, the precise details of which loops are targetted and how is not important here. 167 168 \paragraph{Loop peeling} 169 $$ 170 \sop{while}b\sbin{do}S \mapsto \sop{if}b\sbin{then} S; \sop{while} b \sbin{do} S[\ell'_i/\ell_i] 171 $$ 172 where $\ell'_i$ is a fresh label for any $\ell_i$ labelling a statement in $S$. 173 This relabelling is safe for \s{goto}s occurring outside the loop because of the singleentry condition. 174 Note that for \s{break} and \s{continue} statements, those should be replaced with \s{goto}s in the peeled body $S$. 175 176 \paragraph{Loop unrolling} 177 $$ 178 \sop{while}b\sbin{do}S\mapsto 179 \sop{while} b \sbin{do} (S ; 180 \sop{if} b \sbin{then} (S[\ell^1_i/\ell_i] ; 181 \cdots 182 \sop{if} b \sbin{then} S[\ell^n_i/\ell_i]) \cdots) 183 $$ 184 where $\ell^j_i$ are again fresh labels for any $\ell_i$ labelling a statement in $S$. 185 This is a wilfully na\"{i}ve version of loop unrolling, which usually targets less general loops. 186 The problem this transformation poses to CerCo's labelling approach are independent of the sophistication of the actual transformation. 187 188 \begin{example} 189 In \autoref{fig:example1} we show a program (a wilfully inefficient computation of of the 190 sum of the first $n$ factorials) and a possible transformation of it, combining loop 191 peeling and loop unrolling. 192 \begin{figureplr} 193 $$ 194 \fbox{$\begin{array}{l} 195 s\ass 0;\\ 196 i\ass 0;\\ 197 \sop{while}i<n\sbin{do}\\ 198 \inde p\ass 1;\\ 199 \inde j\ass 1;\\ 200 \inde \sop{while}j \le i\sbin{do}\\ 201 \inde \inde p\ass j*p\\ 202 \inde \inde j\ass j+1;\\ 203 \inde s\ass s+p;\\ 204 \inde i\ass i+1;\\ 205 \end{array} 206 $} 207 \mapsto 208 \fbox{$\begin{array}{l} 209 s\ass 0;\\ 210 i\ass 0;\\ 211 \tikztargetm{a}{\s{if}}\ i<n\sbin{then}\\ 212 \inde p\ass 1;\\ 213 \inde j\ass 1;\\ 214 \inde \sop{while}j \le i\sbin{do}\\ 215 \inde \inde p\ass j*p\\ 216 \inde \inde j\ass j+1;\\ 217 \inde s\ass s+p;\\ 218 \inde i\ass i+1;\\ 219 \inde \tikztargetm{d}{\s{while}}\ i<n\sbin{do}\\ 220 \inde \inde p\ass 1;\\ 221 \inde \inde j\ass 1;\\ 222 \inde \inde \tikztargetm{b}{\s{if}}\ j \le i\sbin{then}\\ 223 \inde \inde \inde p\ass j*p\\ 224 \inde \inde \inde j\ass j+1;\\ 225 \inde \inde \inde \sop{if}j \le i\sbin{then}\\ 226 \inde \inde \inde \inde p\ass j*p\\ 227 \inde \inde \inde \inde j\ass j+1;\\ 228 \inde \inde \inde \inde \s{while}\ j \le i\sbin{do}\\ 229 \inde \inde \inde \inde \inde p\ass j*p\\ 230 \inde \inde \inde \inde \inde j\ass j+1;\\ 231 \inde \inde \inde \inde \inde \sop{if}j \le i\sbin{then}\\ 232 \inde \inde \inde \inde \inde \inde p\ass j*p\\ 233 \inde \inde \inde \inde \inde \inde \tikztargetm{c}j\ass j+1;\\ 234 \inde \inde s\ass s+p;\\ 235 \inde \inde i\ass i+1;\\ 236 \inde \inde \sop{if}i<n\sbin{then}\\ 237 \inde \inde \inde p\ass 1;\\ 238 \inde \inde \inde j\ass 1;\\ 239 \inde \inde \inde \tikztargetm{e}{\s{while}}\ j < i\sbin{do}\\ 240 \inde \inde \inde \inde p\ass j*p\\ 241 \inde \inde \inde \inde j\ass j+1;\\ 242 \inde \inde \inde \inde \s{if}\ j < i\sbin{then}\\ 243 \inde \inde \inde \inde \inde p\ass j*p\\ 244 \inde \inde \inde \inde \inde \tikztargetm{f}j\ass j+1;\\ 245 \inde \inde \inde s\ass s+p;\\ 246 \inde \inde \inde i\ass i+1\tikztargetm{g};{} 247 \end{array} 248 $}\tikztargetm{right}{} 249 \begin{tikzpicture}[overlay, remember picture, thick, 250 brace/.style = {decorate, decoration={brace, amplitude = 15pt}}, 251 label/.style = {sloped, anchor = base, yshift = 17pt, font = \large}] 252 \draw [brace, transform canvas={xshift=5pt}] (b.northright)  node[label]{peeled} (c.southright); 253 \draw [brace, transform canvas={xshift=30pt}] (b.northright)  node[label]{unrolled} (c.southright); 254 \draw [brace, transform canvas={xshift=5pt}] (e.northright)  node[label]{unrolled} (f.southright); 255 \draw [brace, transform canvas={xshift=55pt}] (d.northright)  node[label]{unrolled} (g.southright); 256 \draw [brace, transform canvas={xshift=80pt}] (a.northright)  node[label]{peeled} (g.southright); 257 \end{tikzpicture} 258 \hspace{85pt}{} 259 $$ 260 \caption{An example of loop transformations done on an \imp{} program. Parentheses are omitted in favour of 261 blocks by indentation.} 262 \label{fig:example1} 263 \end{figureplr} 264 \end{example} 265 266 \section{Labelling: a quick sketch of the previous approach} 267 \label{sec:labelling} 268 Plainly labelled \imp{} is obtained by adding to the code \emph{cost labels} (with metavariables $\alpha,\beta,\ldots$), and costlabelled statements: 269 $$ 270 S,T\gramm \cdots \mid \alpha: S 271 $$ 272 Cost labels allow us to track some program points along the compilation chain. 273 For further details we refer to~\cite{D2.1}. 274 275 With labels the small step semantics turns into a labelled transition system along with a natural notion of trace (\ie lists of labels) arises. 276 The evaluation of statements is enriched with traces, so that rules follow a pattern similar to the following: 277 $$ 278 \begin{array}{lblL} 279 (\alpha: S, K,s) &\to[\alpha]_P (S,K,s)\\ 280 (\s{skip}, S \cdot K,s) &\to[\varepsilon]_P (S, K, s)\\ 281 & \text{etc.} 282 \end{array}$$ 283 Here, we identify cost labels $\alpha$ with singleton traces and we use $\varepsilon$ for the empty trace. 284 Cost labels are emitted by costlabelled statements only\footnote{In the general case the evaluation of expressions can emit cost labels too (see~\ref{sec:conc}).}. 285 We then write $\to[\lambda]\!\!^*$ for the transitive closure of the small step semantics which produces by concatenation the trace $\lambda$. 286 287 \paragraph{Labelling} 288 Given an \imp{} program $P$ its \emph{labelling} $\alpha:\Ell(P)$ in $\ell\imp$ is defined by putting cost labels after every branching statement, at the start of both branches, and a cost label at the beginning of the program. Also, every labelled statement gets a cost label, 289 which is a conservative approach to ensuring that all loops have labels inside them, as a loop might be done with \s{goto}s. 290 The relevant cases are 291 $$\begin{aligned} 292 \Ell(\sop{if}e\sbin{then}S\sbin{else}T) &= 293 \sop{if}e\sbin{then}\alpha:\Ell(S)\sbin{else}\beta:\Ell(T)\\ 294 \Ell(\sop{while}e\sbin{do}S) &= 295 (\sop{while}e\sbin{do}\alpha:\Ell(S));\beta:\s{skip}\\ 296 \Ell(\ell : S) &= 297 (\ell : \alpha : \Ell(S)) 298 \end{aligned}$$ 299 where $\alpha,\beta$ are fresh cost labels. 300 In all other cases the definition just passes to substatements. 301 302 \paragraph{Labels in the rest of the compilation chain} 303 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. 304 All other instructions guard their operational semantics and do not emit cost labels. 305 306 Preservation of semantics throughout the compilation process is restated, in rough terms, as: 307 $$ 308 \text{starting state of $P$}\to[\lambda]\!\!^*\;\text{halting state} \iff 309 \text{starting state of $\mathcal C(P)$} \to[\lambda]\!\!^*\;\text{halting state} 310 $$ 311 Here $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. 312 Also, the requirement can be weakened by demanding some sort weaker form of equivalence of the traces than equality. 313 Both of these issues are beyond the scope of this presentation.}. 314 315 \paragraph{Instrumentations} 316 Let $\mathcal C$ be the whole compilation from $\ell\imp$ to the labelled version of some lowlevel language $L$. 317 Supposing such compilation has not introduced any new loop or branching, we have that: 318 \begin{itemize} 319 \item 320 Every loop contains at least a cost label (\emph{soundness condition}) 321 \item 322 Every branching has different labels for the two branches (\emph{preciseness condition}). 323 \end{itemize} 324 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.} 325 We therefore may assume the existence of 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$. 326 327 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 summation of costs during the execution. 328 We call this procedure \emph{instrumentation} of the program, and it is defined recursively by: 329 $$ 330 \mathcal I(\alpha:S) = c \ass c + \kappa(\alpha) ; \mathcal I(S) 331 $$ 332 In all other cases the definition passes to substatements. 333 334 \paragraph{The problem with loop optimisations} 335 Let us take loop peeling, and apply it to the labelling of a program without any prior adjustment: 336 $$ 337 (\sop{while}e\sbin{do}\alpha:S);\beta:\s{skip} 338 \mapsto 339 (\sop{if}b\sbin{then} \alpha : S; \sop{while} b \sbin{do} \alpha : 340 S[\ell'_i/\ell_i]); 341 \beta:\s{skip} 342 $$ 343 What happens is that the cost label $\alpha$ is duplicated with two distinct occurrences. 344 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 (\ie the cost estimate still bounds the actual one) but losing preciseness (\ie the actual cost could be strictly less than its estimate). 345 346 \section{Indexed labels} 347 \label{sec:indexedlabels} 348 This section presents the core of the new approach. 349 In brief points it amounts to the following: 350 \begin{enumerate}[\bfseries~\ref*{sec:indexedlabels}.1.] 351 \item 352 \label{en:outline1} 353 Enrich cost labels with formal indices corresponding, at the beginning of the process, to which iteration of the loop they belong to. 354 \item 355 \label{en:outline2} 356 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. 357 \item 358 \label{en:outline3} 359 Along the compilation chain, alongside the \s{emit} instruction we add other instructions updating the indices, so that iterations of the original loops can be rebuilt at the operational semantics level. 360 \item 361 \label{en:outline4} 362 The machinery computing the cost mapping will still work, but assigning costs to indexed cost labels, rather than to cost labels as we wish. 363 However, \emph{dependent costs} can be calculated, where dependency is on which iteration of the containing loops we are in. 364 \end{enumerate} 365 366 \subsection{Indexing the cost labels} 367 \label{ssec:indlabs} 368 369 \paragraph{Formal indices and $\iota\ell\imp$} 370 Let $i_0,i_1,\ldots$ be a sequence of distinguished fresh identifiers that will be used as loop indices. 371 A \emph{simple expression} is an affine arithmetical expression in one of these indices, that is $a*i_k+b$ with $a,b,k \in \mathbb N$. 372 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$. 373 Constants can be expressed as simple expressions, so that we identify a natural $c$ with $0*i_k+c$. 374 375 An \emph{indexing} (with metavariables $I$, $J$, \ldots) is a list of transformations of successive formal indices dictated by simple expressions, that is a mapping\footnote{Here we restrict each mapping to be a simple expression \emph{on the same index}. 376 This might not be the case if more loop optimisations are accounted for (for example, interchanging two nested loops).} 377 $$ 378 i_0\mapsto a_0*i_0+b_0,\dots, i_{k1} \mapsto a_{k1}*i_{k1}+b_{k1} 379 $$ 380 381 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$. 382 The cost label underlying an indexed one is called its \emph{atom}. 383 All plain labels can be considered as indexed ones by taking an empty indexing. 384 385 \imp{} with indexed labels ($\iota\ell\imp$) is defined by adding to $\imp$ statements with indexed labels, and by having loops with formal indices attached to them: 386 $$ 387 S,T,\ldots \gramm \cdots i_k:\sop{while}e\sbin{do}S\mid \alphab : S 388 $$ 389 Note than unindexed loops still exist in the language: they will correspond to multientry loops which are ignored by indexing and optimisations. 390 We will discuss the semantics later. 391 392 \paragraph{Indexed labelling} 393 Given an $\imp$ program $P$, in order to index loops and assign indexed labels, we must first distinguish singleentry loops. 394 We sketch how this can be computed in the sequel. 395 396 A first pass of the program $P$ can easily compute two maps: $\s{loopof}_P$ from each label $\ell$ to the occurrence (\ie 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. 397 Then the set $\s{multientry}_P$ of multientry loops of $P$ can be computed by 398 $$ 399 \s{multientry}_P\ass\{\, p \mid \exists \ell,q.p =\s{loopof}_P(\ell),q\in\s{gotosof}_P(\ell), q \not\le p\,\} 400 $$ 401 Here $\le$ is the prefix relation\footnote{Possible simplifications to this procedure include keeping track of just the 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}$}. 402 403 Let $Id_k$ be the indexing of length $k$ made from identity simple expressions, \ie the sequence $i_0\mapsto id_0, \ldots , i_{k1}\mapsto id_{k1}$. 404 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: 405 $$ 406 \Ell^\iota_P(S,k)\ass 407 \left\{ 408 \begin{array}{lh{100pt}l} 409 (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} 410 \\& \text{if $S=\sop{while}b\sbin{do}T$ and $S\notin \s{multientry}_P$,}\\[3pt] 411 (\sop{while}b\sbin{do}\alpha\la Id_k \ra : \Ell^\iota_P(T,k));\beta\la Id_k \ra : \s{skip} 412 \\& \text{otherwise, if $S=\sop{while}b\sbin{do}T$,}\\[3pt] 413 \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) 414 \\&\text{if $S=\sop{if}b\sbin{then}T_1\sbin{else}T_2$,}\\[3pt] 415 \ell:\alpha\la Id_k\ra : \Ell_P^\iota(T,k) & \text{if $S = \ell : T$,}\\[3pt] 416 \ldots 417 \end{array} 418 \right. 419 $$ 420 Here, as usual, $\alpha$ and $\beta$ are fresh cost labels, and other cases just keep making the recursive calls on the substatements. 421 The \emph{indexed labelling} of a program $P$ is then defined as $\alpha\la \ra : \Ell^\iota_P(P,0)$, \ie a further fresh unindexed cost label is added at the start, and we start from level $0$. 422 423 In plainer words: each singleentry loop is indexed by $i_k$ where $k$ is the number of other singleentry loops containing this one, and all cost labels under the scope of a singleentry loop indexed by $i_k$ are indexed by all indices $i_0,\ldots,i_k$, without any transformation. 424 425 \subsection{Indexed labels and loop transformations}\label{ssec:looptrans} 426 We define the \emph{reindexing} $I \circ (i_k\mapsto a*i_k+b)$ as an operator on indexings by setting: 427 \begin{multline*} 428 (i_0\mapsto e_0,\ldots, i_k \mapsto e_k,\ldots,i_n\mapsto e_n) 429 \circ(i_k\mapsto a*i_k+b) 430 \ass\\ 431 i_0\mapsto e_0,\ldots, i_k \mapsto e_k \circ(a*i_k+b),\ldots,i_n\mapsto e_n, 432 \end{multline*} 433 We further extend to indexed labels (by $\alpha\la I\ra\circ(i_k\mapsto e)\ass \alpha\la I\circ (i_k\mapsto e)\ra$) and also to statements in $\iota\ell\imp$ (by applying the above transformation to all indexed labels). 434 435 We can then redefine loop peeling and loop unrolling, taking into account indexed labels. 436 It will only be possible to apply the transformation to indexed loops, that is loops that are singleentry. 437 The attentive reader will notice that no assumptions are made on the labelling of the statements that are involved. 438 In particular the transformation can be repeated and composed at will. 439 Also, note that after erasing all labelling information (\ie indexed cost labels and loop indices) we recover exactly the same transformations presented in~\ref{sec:defimp}. 440 441 \paragraph{Indexed loop peeling} 442 $$ 443 i_k:\sop{while}b\sbin{do}S\mapsto 444 \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) 445 $$ 446 As can be expected, the peeled iteration of the loop gets reindexed, always being the first iteration of the loop, while the iterations of the remaining loop are shifted by $1$. Notice that this transformation can lower the actual depth of some loops, however their index is left untouched. 447 448 \paragraph{Indexed loop unrolling} 449 $$ 450 \begin{array}{l} 451 \begin{array}{ncn} 452 i_k:\sop{while}b\sbin{do}S\\ 453 \tikz\node[rotate=90,inner sep=0pt]{$\mapsto$}; 454 \end{array}\\ 455 i_k:\sop{while} b \sbin{do}\\ 456 \quad (S\circ(i_k\mapsto n*i_k) ;\\ 457 \quad \sop{if} b \sbin{then}\\ 458 \quad\quad (S[\ell^1_i/\ell_i]\circ(i_k\mapsto n*i_k+1) ;\\ 459 \quad\quad\quad \vdots \\ 460 \quad\quad \quad \sop{if} b \sbin{then}\\ 461 \quad \quad \quad \quad S[\ell^n_i/\ell_i]\circ(i_k\mapsto n*i_k+n1) 462 )\cdots ) 463 \end{array} 464 $$ 465 Again, the reindexing is as expected: each copy of the unrolled body has its indices remapped so that when they are executed, the original iteration of the loop to which they correspond can be recovered. 466 467 \subsection{Semantics and compilation of indexed labels} 468 In order to make sense of loop indices, one must keep track of their values in the state. 469 A \emph{constant indexing} (metavariables $C,\ldots$) is an indexing which employs only constant simple expressions. 470 The evaluation of an indexing $I$ in a constant indexing $C$, noted $I_C$, is defined by: 471 $$ 472 I\circ(i_0\mapsto c_0,\ldots, i_{k1}\mapsto c_{k1}) \ass \alphab\circ(i_0\mapsto c_0)\circ\cdots\circ(i_{k1}\mapsto c_{k1}) 473 $$ 474 Here, we are using the definition of ${}\circ{}$ given in~\ref{ssec:indlabs}. 475 We consider the above 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$, is indeed a constant indexing, even if the domain of the original indexing is not covered by the constant one.}. 476 The definition is extended to indexed labels by $\alpha\la I\ra_C\ass \alpha\la I_C\ra$. 477 478 Constant indexings will be used to keep track of the exact iterations of the original code that the emitted labels belong to. 479 We thus define two basic actions to update constant indexings: $C[i_k{\uparrow}]$ increments the value of $i_k$ by one, and $C[i_k{\downarrow}0]$ resets it to $0$. 480 481 We are ready to update the definition of the operational semantics of indexed labelled \imp. 482 The emitted cost labels will now be ones indexed by constant indexings. 483 We add a special indexed loop construct for continuations that keeps track of active indexed loop indices: 484 $$ 485 K,\ldots \gramm \cdots  i_k:\sop{while} b \sbin {do} S \sbin{then} K 486 $$ 487 The difference between the regular stack concatenation $i_k:\sop{while}b\sbin{do}S\cdot K$ and the new constructor is that the latter indicates the loop is the active one in which we already are, while the former is a loop that still needs to be started\footnote{In the presence of \s{continue} and \s{break} statements active loops need to be kept track of in any case.}. 488 The \s{find} function is updated accordingly with the case 489 $$ 490 \s{find}(\ell, i_k:\sop{while}b\sbin{do}S, K) \ass \s{find}(\ell, S, i_k: \sop{while}b\sbin{do}S\sbin{then}K) 491 $$ 492 The state will now be a 4tuple $(S,K,s,C)$ which adds a constant indexing to the triple of the regular semantics. 493 The smallstep rules for all statements remain the same, without touching the $C$ parameter (in particular unindexed loops behave the same as usual), apart from the ones regarding costlabels and indexed loops. 494 The remaining cases are: 495 $$\begin{aligned} 496 (\alphab : S,K,s,C) &\to[\alphab_C]_P (S,K,s,C)\\ 497 (i_k:\sop{while}b\sbin{do}S,K,C) &\to[\varepsilon]_P 498 \begin{cases} 499 (S,i_k:\sop{while}b\sbin{do}S\sbin{then} K,s,C[i_k{\downarrow}0]) 500 \\\hskip 125pt \text{if $(b,s)\eval v\neq 0$,}\\ 501 \rlap{(\s{skip}, K, s, C)}\hskip 125pt \text{otherwise} 502 \end{cases}\\ 503 (\s{skip}, i_k:\sop{while}b\sbin{do}S\sbin{then}K,C) &\to[\varepsilon]_P 504 \begin{cases} 505 (S,i_k:\sop{while}b\sbin{do}S\sbin{then} K,s,C[i_k{\uparrow}]) 506 \\\hskip 125pt \text{if $(b,s)\eval v\neq 0$,}\\ 507 \rlap{(\s{skip}, K, s, C)} \hskip 125pt \text{otherwise} 508 \end{cases} 509 \end{aligned}$$ 510 Some explanations are in order: 511 \begin{itemize} 512 \item 513 Emitting a label always instantiates it with the current indexing. 514 \item 515 Hitting an indexed loop the first time initializes the corresponding index to 0; continuing the same loop increments the index as expected. 516 \item 517 The \s{find} function ignores the current indexing: this is correct under the assumption that all indexed loops are single entry, so that when we land inside an indexed loop with a \s{goto}, we are sure that its current index is right. 518 \item 519 The starting state with store $s$ for a program $P$ is $(P,\s{halt},s,(i_0\mapsto 0,\dots,i_{n1}\mapsto 0)$ where $i_0,\ldots,i_{n1}$ cover all loop indices of $P$\footnote{For a program which is the indexed labelling of an \imp{} one this corresponds to the maximum nesting of singleentry loops. 520 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.}. 521 \end{itemize} 522 523 \paragraph{Compilation} 524 Further down the compilation chain the loop structure is usually partially or completely lost. 525 We cannot rely on it anymore to keep track of the original source code iterations. 526 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. 527 528 The first step of compilation from $\iota\ell\imp$ consists of 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$. 529 Later in the compilation chain we must propagate the instructions dealing with cost labels. 530 531 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. 532 By no means are the added instructions and the constant indexing in the state meant to change the actual (let us say denotational) semantics of the programs. 533 In this regard the two new instruction have a similar role as the \s{emit} one. 534 A forgetful mapping of everything (syntax, states, operational semantics rules) can be defined erasing all occurrences of cost labels and loop indices, and the result will always be a regular version of the language considered. 535 536 \paragraph{Stating the preservation of semantics} 537 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. 538 539 \subsection{Dependent costs in the source code} 540 \label{ssec:depcosts} 541 The task of producing dependent costs from constant costs induced by indexed labels is quite technical. 542 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. 543 In Section~\ref{sec:conc}, where we detail the actual implementation, we will also sketch how we mitigated this problem. 544 545 Having the result of compiling the indexed labelling $\Ell^\iota(P)$ of an \imp{} program $P$, we may still suppose that a cost mapping can be computed, but from indexed labels to naturals. 546 We want to annotate the source code, so we need a way to express and compute the costs of cost labels, \ie group the costs of indexed labels to ones of their atoms. 547 In order to do so we introduce \emph{dependent costs}. 548 Let us suppose that for the sole purpose of annotation, we have available in the language ternary expressions of the form 549 $$\tern e {f_1}{f_2},$$ 550 and that we have access to common operators on integers such as equality, order and modulus. 551 552 \paragraph{Simple conditions} 553 554 First, we need to shift from \emph{transformations} of loop indices to \emph{conditions} on them. 555 We identify a set of conditions on natural numbers which are able to express the image of any composition of simple expressions. 556 \emph{Simple conditions} are of three possible forms: 557 \begin{itemize} 558 \item 559 Equality $i_k=n$ for some natural $n$. 560 \item 561 Inequality $i_k\ge n$ for some natural $n$. 562 \item 563 Modular equality together with inequality $i_k\bmod a = b\wedge i_k\ge n$ for naturals $a, b, n$. 564 \end{itemize} 565 The `always true' simple condition is given by $i_k\ge 0$. 566 We write $i_k\bmod a = b$ as a simple condition for $i_k\bmod a = b\wedge i_k\ge 0$. 567 568 Given a simple condition $p$ and a constant indexing $C$ we can easily define when $p$ holds for $C$ (written $p\circ C$). 569 A \emph{dependent cost expression} is an expression built solely out of integer constants and ternary expressions with simple conditions at their head. 570 Given a dependent cost expression $e$ where all of the loop indices appearing in it are in the domain of a constant indexing $C$, we can define the value $e\circ C\in \mathbb N$ by: 571 $$n\circ C\ass n,\qquad (\tern p e f)\circ C\ass 572 \begin{cases} 573 e\circ C& \text{if $p\circ C$,}\\ 574 f\circ C& \text{otherwise.} 575 \end{cases}$$ 576 577 \paragraph{From indexed costs to dependent ones} 578 Every simple expression $e$ corresponds to a simple condition $p(e)$ which expresses the set of values that $e$ can take. 579 Following is the definition of such a relation. 580 We recall that in this development, loop indices are always mapped to simple expressions over the same index. 581 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. 582 We leave all generalisations of what we present here for further work: 583 $$ 584 p(a*i_k+b)\ass 585 \begin{cases} 586 i_k = b & \text{if $a = 0$,}\\ 587 i_k \ge b & \text{if $a = 1$,}\\ 588 i_k\bmod a = b' \wedge i_k \ge b & \text{otherwise, where $b' = b\bmod a$}. 589 \end{cases} 590 $$ 591 Now, suppose we are given a mapping $\kappa$ from indexed labels to natural numbers. 592 We will transform it in a mapping (identified, via abuse of notation, with the same symbol $\kappa$) from atoms to \imp{} expressions built with ternary expressions which depend solely on loop indices. 593 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, \ie each set is made of words all with the same length). 594 595 We will employ a bijection between words of simple expressions and indexings, given by:\footnote{Lists of simple expressions are in fact how indexings are represented in CerCo's current implementation of the compiler.} 596 $$ 597 i_0\mapsto e_0,\ldots,i_{k1}\mapsto e_{k1} \cong e_0\cdots e_{k1}. 598 $$ 599 As usual, $\varepsilon$ denotes the empty word/indexing, and juxtaposition is used to denote word concatenation. 600 601 For every set $s$ of $n$uples of simple expressions, we are in one of the following three exclusive cases: 602 \begin{itemize} 603 \item 604 $S=\emptyset$. 605 \item 606 $S=\{\varepsilon\}$. 607 \item 608 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$. 609 \end{itemize} 610 Here $eS'$ denotes prepending $e$ to all elements of $S'$ and $+$ is disjoint union. 611 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. 612 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. 613 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<a'$ or $a=a'$ and $b\le b'$.}. 614 615 Following is the definition of the auxiliary function $\kappa^\alpha_L$, which follows the recursion scheme presented above: 616 $$ 617 \begin{aligned} 618 \kappa^\alpha_L(\emptyset) &\ass 0\\ 619 \kappa^\alpha_L(\{\varepsilon\}) &\ass \kappa(\alpha\la L\ra) \\ 620 \kappa^\alpha_L(eS'+S'') &\ass \tern{p(e)}{\kappa^\alpha_{Le}(S')}{\kappa^\alpha_L(S'')} 621 \end{aligned} 622 $$ 623 \noindent 624 Finally, the wanted dependent cost mapping is defined by 625 $$ 626 \kappa(\alpha)\ass\kappa^\alpha_\varepsilon(\{\,L\mid \alpha\la L\ra \text{ appears in the compiled code}\,\}) 627 $$ 628 629 \paragraph{Indexed instrumentation} 630 The \emph{indexed instrumentation} generalises the instrumentation presented in~\ref{sec:labelling}. 631 We described above how cost atoms can be mapped to dependent costs. 632 The instrumentation must also insert code dealing with the loop indices. 633 As instrumentation is done on the code produced by the labelling phase, all cost labels are indexed by identity indexings. 634 The relevant cases of the recursive definition (supposing $c$ is the cost variable) are then: 635 $$ 636 \begin{aligned} 637 \mathcal I^\iota(\alpha\la Id_k\ra:S) &= c\ass c + \kappa(\alpha);\mathcal I^\iota(S)\\ 638 \mathcal I^\iota(i_k : \sop{while}b\sbin{do}S) &= 639 i_k \ass 0; \sop{while}b\sbin{do}(\mathcal I^\iota (S); i_k \ass i_k + 1) 640 \end{aligned} 641 $$ 642 643 \subsection{A detailed example}\label{ssec:detailedex} 644 Take the program in \autoref{fig:example1}. Its initial labelling will be: 645 $$\begin{array}{l} 646 \alpha\la\ra : s\ass 0;\\ 647 i\ass 0;\\ 648 i_0:\sop{while}i<n\sbin{do}\\ 649 \inde \beta\la i_0\ra : p\ass 1;\\ 650 \inde j\ass 1;\\ 651 \inde i_1:\sop{while}j \le i\sbin{do}\\ 652 \inde \inde \gamma\la i_0, i_1\ra : p\ass j*p\\ 653 \inde \inde j\ass j+1;\\ 654 \inde \delta\la i_0\ra : s\ass s+p;\\ 655 \inde i\ass i+1;\\ 656 \epsilon\la\ra:\s{skip} 657 \end{array} 658 $$ 659 (a single \s{skip} after the $\delta$ label has been suppressed, and we are using the identification 660 between indexings and tuples of simple expressions explained in \autoref{ssec:depcosts}). 661 Supposing for example, $n=3$ 662 the trace of the program will be 663 $$\alpha\la\ra\,\beta\la 0 \ra\, \delta\la 0\ra\,\beta\la 1\ra\,\gamma\la 1,0\ra\, 664 \delta\la 1\ra\,\beta\la 2\ra\,\gamma\la 2,0\ra\,\gamma\la 2, 1\ra\,\delta\la 2\ra\, 665 \epsilon\la\ra$$ 666 Now let as apply the transformations of \autoref{fig:example1} with the additional 667 information detailed in \autoref{ssec:looptrans}. The result is shown in 668 \autoref{fig:example2}. 669 \begin{figureplr} 670 $$ 671 \begin{array}{l} 672 \mbox{\color{blue}\boldmath$\alpha\la\ra $}:s\ass 0;\\ 673 i\ass 0;\\ 674 \tikztargetm{a}{\s{if}}\ i<n\sbin{then}\\ 675 \inde \mbox{\color{blue}\boldmath$\beta\la0\ra $}:p\ass 1;\\ 676 \inde j\ass 1;\\ 677 \inde i_1:\sop{while}j \le i\sbin{do}\\ 678 \inde \inde \mbox{\color{blue}\boldmath$\gamma\la 0, i_1\ra $}:p\ass j*p\\ 679 \inde \inde j\ass j+1;\\ 680 \inde \mbox{\color{blue}\boldmath$\delta\la 0\ra $}: s\ass s+p;\\ 681 \inde i\ass i+1;\\ 682 \inde i_0:\tikztargetm{d}{\s{while}}\ i<n\sbin{do}\\ 683 \inde \inde \mbox{\color{blue}\boldmath$\beta\la 2*i_0+1\ra $}:p\ass 1;\\ 684 \inde \inde j\ass 1;\\ 685 \inde \inde \tikztargetm{b}{\s{if}}\ j \le i\sbin{then}\\ 686 \inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la 2*i_0+1, 0\ra $}:p\ass j*p\\ 687 \inde \inde \inde j\ass j+1;\\ 688 \inde \inde \inde \sop{if}j \le i\sbin{then}\\ 689 \inde \inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la 2*i_0+1, 1\ra $}: p\ass j*p\\ 690 \inde \inde \inde \inde j\ass j+1;\\ 691 \inde \inde \inde \inde i_1:\s{while}\ j \le i\sbin{do}\\ 692 \inde \inde \inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la 2*i_0+1, 2*i_1 + 2 \ra $}:p\ass j*p\\ 693 \inde \inde \inde \inde \inde j\ass j+1;\\ 694 \inde \inde \inde \inde \inde \sop{if}j \le i\sbin{then}\\ 695 \inde \inde \inde \inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la 2*i_0+1, 2*i_1 + 3\ra $}:p\ass j*p\\ 696 \inde \inde \inde \inde \inde \inde \tikztargetm{c}j\ass j+1;\\ 697 \inde \inde \mbox{\color{blue}\boldmath$\delta\la 2*i_0+1\ra$}: s\ass s+p;\\ 698 \inde \inde i\ass i+1;\\ 699 \inde \inde \sop{if}i<n\sbin{then}\\ 700 \inde \inde \inde \mbox{\color{blue}\boldmath$\beta\la 2*i_0+2\ra $}:p\ass 1;\\ 701 \inde \inde \inde j\ass 1;\\ 702 \inde \inde \inde i_1:\tikztargetm{e}{\s{while}}\ j < i\sbin{do}\\ 703 \inde \inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la 2*i_0+2, 2*i_1\ra$}: p\ass j*p\\ 704 \inde \inde \inde \inde j\ass j+1;\\ 705 \inde \inde \inde \inde \s{if}\ j < i\sbin{then}\\ 706 \inde \inde \inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la2*i_0+2, 2*i_1+1\ra$}: p\ass j*p\\ 707 \inde \inde \inde \inde \inde \tikztargetm{f}j\ass j+1;\\ 708 \inde \inde \inde \mbox{\color{blue}\boldmath$\delta\la 2*i_0+2\ra $}: s\ass s+p;\\ 709 \inde \inde \inde i\ass i+1\tikztargetm{g};{}\\ 710 \mbox{\color{blue}\boldmath$\epsilon\la\ra $}:\s{skip} 711 \end{array}$$ 712 \caption{The result of applying reindexing loop transformations on the 713 program in \autoref{fig:example1}.}\label{fig:example2} 714 \end{figureplr} 715 One can check that the transformed code leaves the same trace when executed. 716 717 Now let us compute the dependent cost of $\gamma$, supposing no other loop transformations 718 are done. Ordering its indexings we 719 have the following list: 720 \begin{equation} 721 \label{eq:inds} 722 \begin{aligned} 723 &0, i_1\\ 724 &2*i_0+1, 0\\ 725 &2*i_0+1, 1\\ 726 &2*i_0+1, 2*i_1+2\\ 727 &2*i_0+1, 2*i_1+3\\ 728 &2*i_0+2, 2*i_1\\ 729 &2*i_0+2, 2*i_1+1 730 \end{aligned} 731 \end{equation} 732 733 The resulting dependent cost will then be 734 \def\indetern#1#2#3{\begin{tabular}[t]{nL}(#1)\mathrel ?{}\\\hskip 15pt #2:{}\\\hskip 15pt #3\end{tabular}} 735 \def\tern#1#2#3{(#1)\mathrel ? #2:#3} 736 \begin{equation}\label{eq:ex} 737 \kappa^\iota(\gamma)= 738 \indetern{i_0 = 0} 739 {\tern{i_1\ge 0}a0} 740 {\indetern{i_0\bmod 2 = 1 \wedge i_0\ge 1} 741 {\indetern{i_1=0} 742 b 743 {\indetern{i_1 = 1} 744 c 745 {\indetern{i_1\bmod 2 = 0 \wedge i_1\ge 2} 746 d 747 {\tern{i_1\bmod 2 = 1 \wedge i_1\ge 3}e0} 748 } 749 } 750 } 751 {\indetern{i_0\bmod 2 = 0 \wedge i_0\ge 2} 752 {\indetern{i_1 \bmod 2 = 0 \wedge i_1 \ge 0} 753 f 754 {\tern{i_1 \bmod 2 = 1 \wedge i_1 \ge 1}g0} 755 } 756 0 757 } 758 } 759 \end{equation} 760 We will see later on \autopageref{pag:continued} how such an expression can be simplified. 761 \section{Notes on the implementation and further work} 762 \label{sec:conc} 763 Implementing the indexed label approach in CerCo's untrusted Ocaml prototype does not introduce many new challenges beyond what has already been presented for the toy language, \imp{} with \s{goto}s. 764 \s{Clight}, the \s{C} fragment source language of CerCo's compilation chain~\cite{D2.1}, has several more fetaures, but few demand changes in the indexed labelled approach. 765 766 \paragraph{Indexed loops \emph{vs}. index update instructions} 767 In our presentation we have indexed loops in $\iota\ell\imp$, while we hinted that later languages in the compilation chain would have specific index update instructions. 768 In CerCo's actual compilation chain from \s{Clight} to 8051 assembly, indexed loops are only in \s{Clight}, while from \s{Cminor} onward all languages have the same three costinvolving instructions: label emitting, index resetting and index incrementing. 769 770 \paragraph{Loop transformations in the front end} 771 We decided to implement the two loop transformations in the front end, namely in \s{Clight}. 772 This decision is due to user readability concerns: if costs are to be presented to the programmer, they should depend on structures written by the programmer himself. 773 If loop transformation were performed later it would be harder to create a correspondence between loops in the control flow graph and actual loops written in the source code. 774 However, another solution would be to index loops in the source code and then use these indices later in the compilation chain to pinpoint explicit loops of the source code: loop indices can be used to preserve such information, just like cost labels. 775 776 \paragraph{Break and continue statements} 777 \s{Clight}'s loop flow control statements for breaking and continuing a loop are equivalent to appropriate \s{goto} statements. 778 The only difference is that we are assured that they cannot cause loops to be multientry, and that when a transformation such as loop peeling is complete, they need to be replaced by actual \s{goto}s (which happens further down the compilation chain anyway). 779 780 \paragraph{Function calls} 781 Every internal function definition has its own space of loop indices. 782 Executable semantics must thus take into account saving and resetting the constant indexing of current loops upon hitting a function call, and restoring it upon return of control. 783 A peculiarity is that this cannot be attached to actions that save and restore frames: namely in the case of tail calls the constant indexing needs to be saved whereas the frame does not. 784 785 \paragraph{Costlabelled expressions} 786 In labelled \s{Clight}, expressions also get cost labels, due to the presence of ternary conditional expressions (and lazy logical operators, which get translated to ternary expressions too). 787 Adapting the indexed labelled approach to costlabelled expressions does not pose any particular problems. 788 789 \paragraph{Simplification of dependent costs} 790 As previously mentioned, the na\"{i}ve application of the procedure described in~\ref{ssec:depcosts} produces unwieldy cost annotations. 791 In our implementation several transformations are used to simplify such complex dependent costs. 792 793 Disjunctions of simple conditions are closed under all logical operations, and it can be computed whether such a disjunction implies a simple condition or its negation. 794 This can be used to eliminate useless branches of dependent costs, to merge branches that share the same value, and possibly to simplify the third case of simple condition. 795 Examples of the three transformations are respectively: 796 \begin{itemize} 797 \item $ 798 \verb+(_i_0 == 0)?+x\verb+:(_i_0 >= 1)?+y\verb+:+z 799 \mapsto 800 \verb+(_i_0 == 0)?+x\verb+:+y, 801 $ 802 \item $ 803 c\texttt{?}x\verb+:(+d\texttt{?}x\texttt{:}y\verb+)+ 804 \mapsto 805 \texttt{(}c\texttt{  }d\texttt{)?}x\texttt{:}y, 806 $ 807 \item \begin{tabular}[t]{np{\linewidth}n} 808 $\verb+(_i_0 == 0)?+x\verb+:(_i_0 % 2 == 0 && _i_0 >= 2)?+y\verb+:+z 809 \mapsto$ \\\hfill 810 $\verb+(_i_0 == 0)?+x\verb+:(_i_0 % 2 == 0)?+y\verb+:+z. 811 $\end{tabular} 812 \end{itemize} 813 The second transformation tends to accumulate disjunctions, to the detriment of readability. 814 A further transformation swaps two branches of the ternary expression if the negation of the condition can be expressed with fewer clauses. 815 For example: 816 $$ \verb+(_i_0 % 3 == 0  _i_0 % 3 == 1)?+x\verb+:+y \mapsto 817 \verb+(_i_0 % 3 == 2)?+y\verb+:+x. 818 $$ 819 Picking up again the example depicted in \autoref{ssec:detailedex}, \label{pag:continued} 820 we can see that the cost in \eqref{eq:ex} can be simplified to the following, 821 using some of the transformation described above: 822 $$ 823 \kappa^\iota(\gamma)= 824 \indetern{i_0 = 0} 825 a 826 {\indetern{i_0\bmod 2 = 1} 827 {\indetern{i_1=0} 828 b 829 {\indetern{i_1 = 1} 830 c 831 {\indetern{i_1\bmod 2 = 0} 832 de 833 } 834 } 835 } 836 {\indetern{i_1 \bmod 2 = 0} 837 fg 838 } 839 } 840 $$ 841 One should keep in mind that the example was wilfully complicated, in practice 842 the cost expressions produced have rarely more clauses 843 than the number of nested loops containing the annotation. 844 \paragraph{Updates to the framaC cost plugin} 845 Cerco's framaC~\cite{framac} cost plugin\todo{is there a reference for this?}{} has been updated to take into account our new notion of dependent costs. 846 The framac framework expands ternary expressions to branch statements, introducing temporaries along the way. 847 This makes the task of analyzing ternary cost expressions rather daunting. 848 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 framaC's use of temporaries in cost annotation could be avoided. 849 The cost analysis carried out by the plugin now takes into account such dependent costs. 850 851 The only limitation (which actually simplifies the code) is that, within a dependent cost, simple conditions with modulus on the same loop index should not be modulo different numbers. 852 This corresponds to a reasonable limitation on the number of times loop unrolling may be applied to the same loop: at most once. 853 854 \paragraph{Further work} 855 For the time being, indexed labels are only implemented in the untrusted Ocaml compiler, while they are not present yet in the Matita code. 856 Porting them should pose no significant problem. 857 Once ported, the task of proving properties about them in Matita can begin. 858 859 Because most of the executable operational semantics of the languages across the frontend and the backend 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. 860 The only trickier point that we foresee would be in the translation of \s{Clight} to \s{Cminor}, where we pass from structured indexed loops to atomic instructions on loop indices. 861 862 An invariant which should probably be proved and provably preserved along the compilation chain is the nonoverlap of indexings for the same atom. 863 Then, supposing cost correctness for the unindexed approach, the indexed one will just need to amend the proof that 864 $$\forall C\text{ constant indexing}.\forall \alpha\la I\ra\text{ appearing in the compiled code}. 865 \kappa(\alpha)\circ (I\circ C) = \kappa(\alpha\la I \ra). 866 $$ 867 Here, $C$ represents a snapshot of loop indices in the compiled code, while $I\circ C$ is the corresponding snapshot in the source code. 868 Semantics preservation will ensure that when, with snapshot $C$, we emit $\alpha\la I\ra$ (that is, we have $\alpha\la I\circ C\ra$ in the trace), $\alpha$ must also be emitted in the source code with indexing $I\circ C$, so the cost $\kappa(\alpha)\circ (I\circ C)$ applies. 869 870 Aside from carrying over the proofs, we would like to extend the approach to more loop transformations. 871 Important examples are loop inversion (where a for loop is reversed, usually to make iterations appear to be truly independent) or loop interchange (where two nested loops are swapped, usually to have more loop invariants or to enhance strength reduction). 872 This introduces interesting changes to the approach, where we would have indexings such as: 873 $$i_0\mapsto n  i_0\quad\text{or}\quad i_0\mapsto i_1, i_1\mapsto i_0.$$ 874 In particular dependency over actual variables of the code would enter the frame, as indexings would depend on the number of iterations of a wellbehaving guarded loop (the $n$ in the first example). 875 876 Finally, as stated in the introduction, the approach should allow some integration of techniques for cache analysis, a possibility that for now has been put aside as the standard 8051 target architecture for the CerCo project lacks a cache. 877 Two possible developments for this line of work present themselves: 878 \begin{enumerate} 879 \item 880 One could extend the development to some 8051 variants, of which some have been produced with a cache. 881 \item 882 One could make the compiler implement its own cache: this cannot apply to \textsc{ram} accesses of the standard 8051 architecture, as the difference in cost of accessing the two types of \textsc{ram} is only one clock cycle, which makes any implementation of cache counterproductive. 883 So for this proposal, we could either artificially change the accessing cost of \textsc{ram} of the model just for the sake of possible future adaptations to other architectures, or otherwise model access to an external memory by means of the serial port. 884 \end{enumerate} 7 885 8 886 \section{Compiler proof}
Note: See TracChangeset
for help on using the changeset viewer.