Changeset 3305
 Timestamp:
 May 29, 2013, 6:25:11 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec.tex
r3222 r3305 4 4 \usepackage{color} 5 5 \usepackage{listings} 6 \usepackage{bcprules} 6 \usepackage{bcprules}%\bcprulessavespace 7 7 \usepackage{verbatim} 8 8 \usepackage{alltt} 9 \usepackage{subcaption} 10 \usepackage{listings} 11 \usepackage{amssymb} 12 % \usepackage{amsmath} 13 \usepackage{multicol} 14 15 \providecommand{\eqref}[1]{(\ref{#1})} 9 16 10 17 % NB: might be worth removing this if changing class in favour of … … 29 36 showspaces=false,showstringspaces=false, 30 37 xleftmargin=1em} 38 39 \usepackage{tikz} 40 \usetikzlibrary{positioning,calc,patterns,chains,shapes.geometric,scopes} 41 \makeatletter 42 \pgfutil@ifundefined{pgf@arrow@code@implies}{% supply for lack of double arrow special arrow tip if it is not there% 43 \pgfarrowsdeclare{implies}{implies}% 44 {% 45 \pgfarrowsleftextend{2.2pt}% 46 \pgfarrowsrightextend{2.2pt}% 47 }% 48 {% 49 \pgfsetdash{}{0pt} % do not dash% 50 \pgfsetlinewidth{.33pt}% 51 \pgfsetroundjoin % fix join% 52 \pgfsetroundcap % fix cap% 53 \pgfpathmoveto{\pgfpoint{1.5pt}{2.5pt}}% 54 \pgfpathcurveto{\pgfpoint{.75pt}{1.5pt}}{\pgfpoint{0.5pt}{.5pt}}{\pgfpoint{2pt}{0pt}}% 55 \pgfpathcurveto{\pgfpoint{0.5pt}{.5pt}}{\pgfpoint{.75pt}{1.5pt}}{\pgfpoint{1.5pt}{2.5pt}}% 56 \pgfusepathqstroke% 57 }% 58 }{}% 59 \makeatother 60 61 \tikzset{state/.style={inner sep = 0, outer sep = 2pt, draw, fill}, 62 every node/.style={inner sep=2pt}, 63 every on chain/.style = {inner sep = 0, outer sep = 2pt}, 64 join all/.style = {every on chain/.append style={join}}, 65 on/.style={on chain={#1}, state}, 66 m/.style={execute at begin node=$, execute at end node=$}, 67 node distance=3mm, 68 is other/.style={circle, minimum size = 3pt, state}, 69 other/.style={on, is other}, 70 is jump/.style={diamond, minimum size = 6pt, state}, 71 jump/.style={on, is jump}, 72 is call/.style={regular polygon, regular polygon sides=3, minimum size=5pt, state}, 73 call/.style={on=going below, is call, node distance=6mm, label=above left:$#1$}, 74 is ret/.style={regular polygon, regular polygon sides=3, minimum size=5pt, shape border rotate=180, state}, 75 ret/.style={on=going above, is ret, node distance=6mm}, 76 chain/.style={start chain=#1 going left}, 77 rev ar/.style={stealth, thick}, 78 ar/.style={stealth, thick}, 79 every join/.style={rev ar}, 80 labelled/.style={fill=white, label=above:$#1$}, 81 vcenter/.style={baseline={([yshift=.5ex]current bounding box)}}, 82 every picture/.style={thick}, 83 double equal sign distance/.prefix style={double distance=1.5pt}, %% if already defined (newest version of pgf) it should be ignored%} 84 implies/.style={double, implies, thin, double equal sign distance, shorten <=5pt, shorten >=5pt}, 85 new/.style={densely dashed}, 86 rel/.style={font=\scriptsize, fill=white, inner sep=2pt}, 87 diag/.style={row sep={11mm,between origins}, 88 column sep={11mm,between origins}, 89 every node/.style={draw, is other}}, 90 small vgap/.style={row sep={7mm,between origins}}, 91 } 92 93 \def\L{\mathrel{\mathcal L}} 94 \def\S{\mathrel{\mathcal S}} 95 \def\R{\mathrel{\mathcal R}} 96 \def\C{\mathrel{\mathcal C}} 97 98 \newsavebox{\execbox} 99 \savebox{\execbox}{\tikz[baseline=.5ex]\draw [stealth] (0,0)  ++(1em, 0);} 100 \newcommand{\exec}{\ensuremath{\mathrel{\usebox{\execbox}}}} 101 \let\ar\rightsquigarrow 102 \renewcommand{\verb}{\lstinline[mathescape]} 103 104 \let\class\triangleright 105 \let\andalso\quad 106 107 \newcommand{\append}{\mathbin{@}} 31 108 32 109 \begin{document} … … 56 133 57 134 \section{Introduction} 58 59 135 The \emph{labelling approach} has been introduced in~\cite{easylabelling} as 60 136 a technique to \emph{lift} cost models for nonfunctional properties of programs … … 338 414 In order to have a definition that works on multiple intermediate languages, 339 415 we abstract the type of structure traces over an abstract data type of 340 abstract statuses: 341 \begin{alltt} 342 record abstract_status := \{ S: Type[0]; 343 as_execute: S \(\to\) S \(\to\) Prop; as_classify: S \(\to\) classification; 344 as_costed: S \(\to\) Prop; as_label: \(\forall\) s. as_costed S s \(\to\) label; 345 as_call_ident: \(\forall\) s. as_classify S s = cl_call \(\to\) label; 346 as_after_return: 347 (\(\Sigma\)s:as_status. as_classify s = Some ? cl_call) \(\to\) as_status \(\to\) Prop \} 348 \end{alltt} 349 The predicate $\texttt{as\_execute}~s_1~s_2$ holds if $s_1$ evolves into 350 $s_2$ in one step;\\ $\texttt{as\_classify}~s~c$ holds if the next instruction 351 to be executed in $s$ is classified according to $c \in 352 \{\texttt{cl\_return,cl\_jump,cl\_call,cl\_other}\}$ (we omit tailcalls for simplicity); 353 the predicate $\texttt{as\_costed}~s$ holds if the next instruction to be 354 executed in $s$ is a cost emission statement (also classified 355 as \texttt{cl\_other}); finally $(\texttt{as\_after\_return}~s_1~s_2)$ holds 356 if the next instruction to be executed in $s_2$ follows the function call 357 to be executed in (the witness of the $\Sigma$type) $s_1$. The two functions 358 \texttt{as\_label} and \texttt{as\_cost\_ident} are used to extract the 359 cost label/function call target from states whose next instruction is 360 a cost emission/function call statement. 361 416 abstract statuses, which we aptly call $\texttt{abstract\_status}$. The fields 417 of this record are the following. 418 \begin{itemize} 419 \item \verb+S : Type[0]+, the type of states. 420 \item \verb+as_execute : S $\to$ S $\to$ Prop+, a binary predicate stating 421 an execution step. We write $s_1\exec s_2$ for $\verb+as_execute+~s_1~s_2$. 422 \item \verb+as_classifier : S $\to$ classification+, a function tagging all 423 states with a class in 424 $\{\texttt{cl\_return,cl\_jump,cl\_call,cl\_other}\}$, depending on the instruction 425 that is about to be executed (we omit tailcalls for simplicity). We will 426 use $s \class c$ as a shorthand for both $\texttt{as\_classifier}~s=c$ 427 (if $c$ is a classification) and $\texttt{as\_classifier}~s\in c$ 428 (if $c$ is a set of classifications). 429 \item \verb+as_label : S $\to$ option label+, telling whether the 430 next instruction to be executed in $s$ is a cost emission statement, 431 and if yes returning the associated cost label. Our shorthand for this function 432 will be $\ell$, and we will also abuse the notation by using $\ell~s$ as a 433 predicate stating that $s$ is labelled. 434 \item \verb+as_call_ident : ($\Sigma$s:S. s $\class$ cl_call) $\to$ label+, 435 telling the identifier of the function which is being called in a 436 \verb+cl_call+ state. We will use the shorthand $s\uparrow f$ for 437 $\verb+as_call_ident+~s = f$. 438 \item \verb+as_after_return : ($\Sigma$s:S. s $\class$ cl_call) $\to$ S $\to$ Prop+, 439 which holds on the \verb+cl_call+ state $s_1$ and a state $s_2$ when the 440 instruction to be executed in $s_2$ follows the function call to be 441 executed in (the witness of the $\Sigma$type) $s_1$. We will use the notation 442 $s_1\ar s_2$ for this relation. 443 \end{itemize} 444 445 % \begin{alltt} 446 % record abstract_status := \{ S: Type[0]; 447 % as_execute: S \(\to\) S \(\to\) Prop; as_classifier: S \(\to\) classification; 448 % as_label: S \(\to\) option label; as_called: (\(\Sigma\)s:S. c s = cl_call) \(\to\) label; 449 % as_after_return: (\(\Sigma\)s:S. c s = cl_call) \(\to\) S \(\to\) Prop \} 450 % \end{alltt} 362 451 363 452 The inductive type for structured traces is actually made by three multiple 364 453 inductive types with the following semantics: 365 454 \begin{enumerate} 366 \item $(\texttt{trace\_label\_return}~s_1~s_2)$ is a trace that begins in 455 \item $(\texttt{trace\_label\_return}~s_1~s_2)$ (shorthand $\verb+TLR+~s_1~s_2$) 456 is a trace that begins in 367 457 the state $s_1$ (included) and ends just before the state $s_2$ (excluded) 368 458 such that the instruction to be executed in $s_1$ is a label emission … … 374 464 one or more basic blocks, all starting with a label emission 375 465 (e.g. in case of loops). 376 \item $(\texttt{trace\_any\_label}~b~s_1~s_2)$ is a trace that begins in 466 \item $(\texttt{trace\_any\_label}~b~s_1~s_2)$ (shorthand $\verb+TAL+~b~s_1~s_2$) 467 is a trace that begins in 377 468 the state $s_1$ (included) and ends just before the state $s_2$ (excluded) 378 469 such that the instruction to be executed in $s_2$/in the state before … … 381 472 any label emission statement. It captures the notion of a suffix of a 382 473 basic block. 383 \item $(\texttt{trace\_label\_label}~b~s_1~s_2)$ is the special case of384 $ (\texttt{trace\_any\_label}~b~s_1~s_2)$ such that the instruction to be474 \item $(\texttt{trace\_label\_label}~b~s_1~s_2)$ (shorthand $\verb+TLL+~b~s_1~s_2$ is the special case of 475 $\verb+TAL+~b~s_1~s_2)$ such that the instruction to be 385 476 executed in $s_1$ is a label emission statement. It captures the notion of 386 477 a basic block. 387 478 \end{enumerate} 388 479 389 \infrule[\texttt{tlr\_base}] 390 {\texttt{trace\_label\_label}~true~s_1~s_2} 391 {\texttt{trace\_label\_return}~s_1~s_2} 392 393 \infrule[\texttt{tlr\_step}] 394 {\texttt{trace\_label\_label}~false~s_1~s_2 \andalso 395 \texttt{trace\_label\_return}~s_2~s_3 480 \begin{multicols}{3} 481 \infrule[\verb+tlr_base+] 482 {\texttt{TLL}~true~s_1~s_2} 483 {\texttt{TLR}~s_1~s_2} 484 485 \infrule[\verb+tlr_step+] 486 {\texttt{TLL}~false~s_1~s_2 \andalso 487 \texttt{TLR}~s_2~s_3 396 488 } 397 {\texttt{ trace\_label\_return}~s_1~s_3}398 399 \infrule[\ texttt{tll\_base}]400 {\texttt{ trace\_any\_label}~b~s_1~s_2 \andalso401 \ texttt{as\_costed}~s_1489 {\texttt{TLR}~s_1~s_3} 490 491 \infrule[\verb+tll_base+] 492 {\texttt{TAL}~b~s_1~s_2 \andalso 493 \ell~s_1 402 494 } 403 {\texttt{trace\_label\_label}~b~s_1~s_2} 404 405 \infrule[\texttt{tal\_base\_not\_return}] 406 {\texttt{as\_execute}~s_1~s_2 \andalso 407 \texttt{as\_classify}~s_1 \in \{\texttt{cl\_jump,cl\_other}\} \andalso 408 \texttt{as\_costed}~s_2 495 {\texttt{TLL}~b~s_1~s_2} 496 \end{multicols} 497 498 \infrule[\verb+tal_base_not_return+] 499 {s_1\exec s_2 \andalso 500 s_1\class\{\verb+cl_jump+, \verb+cl_other+\}\andalso 501 \ell~s_2 409 502 } 410 {\texttt{ trace\_any\_label}~false~s_1~s_2}411 412 \infrule[\ texttt{tal\_base\_return}]413 { \texttt{as\_execute}~s_1~s_2 \andalso414 \texttt{as\_classify}~s_1 = \texttt{cl\_return} \\503 {\texttt{TAL}~false~s_1~s_2} 504 505 \infrule[\verb+tal_base_return+] 506 {s_1\exec s_2 \andalso 507 s_1 \class \texttt{cl\_return} 415 508 } 416 {\texttt{ trace\_any\_label}~true~s_1~s_2}417 418 \infrule[\ texttt{tal\_base\_call}]419 { \texttt{as\_execute}~s_1~s_2 \andalso420 \texttt{as\_classify}~s_1 = \texttt{cl\_call} \\421 \texttt{as\_after\_return}~s_1~s_3 \andalso422 \texttt{ trace\_label\_return}~s_2~s_3 \andalso423 \ texttt{as\_costed}~s_3509 {\texttt{TAL}~true~s_1~s_2} 510 511 \infrule[\verb+tal_base_call+] 512 {s_1\exec s_2 \andalso 513 s_1 \class \texttt{cl\_call} \andalso 514 s_1\ar s_3 \andalso 515 \texttt{TLR}~s_2~s_3 \andalso 516 \ell~s_3 424 517 } 425 {\texttt{trace\_any\_label}~false~s_1~s_3} 426 427 \infrule[\texttt{tal\_step\_call}] 428 {\texttt{as\_execute}~s_1~s_2 \andalso 429 \texttt{as\_classify}~s_1 = \texttt{cl\_call} \\ 430 \texttt{as\_after\_return}~s_1~s_3 \andalso 431 \texttt{trace\_label\_return}~s_2~s_3 \\ 432 \lnot \texttt{as\_costed}~s_3 \andalso 433 \texttt{trace\_any\_label}~b~s_3~s_4 518 {\texttt{TAL}~false~s_1~s_3} 519 520 \infrule[\verb+tal_step_call+] 521 {s_1\exec s_2 \andalso 522 s_1 \class \texttt{cl\_call} \andalso 523 s_1\ar s_3 \andalso 524 \texttt{TLR}~s_2~s_3 \andalso 525 \texttt{TAL}~b~s_3~s_4 434 526 } 435 {\texttt{ trace\_any\_label}~b~s_1~s_4}436 437 \infrule[\ texttt{tal\_step\_default}]438 { \texttt{as\_execute}~s_1~s_2 \andalso439 \lnot \ texttt{as\_costed}~s_2 \\440 \texttt{ trace\_any\_label}~b~s_2~s_3441 \texttt{as\_classify}~s_1 =\texttt{cl\_other}527 {\texttt{TAL}~b~s_1~s_4} 528 529 \infrule[\verb+tal_step_default+] 530 {s_1\exec s_2 \andalso 531 \lnot \ell~s_2 \andalso 532 \texttt{TAL}~b~s_2~s_3\andalso 533 s_1 \class \texttt{cl\_other} 442 534 } 443 {\texttt{trace\_any\_label}~b~s_1~s_3} 444 445 535 {\texttt{TAL}~b~s_1~s_3} 446 536 \begin{comment} 447 537 \begin{verbatim} … … 549 639 \end{enumerate} 550 640 551 The three mutual structural recursive functions \texttt{flatten\_trace\_label\_return, flatten\_trace\_label\_label} and \texttt{flatten\_trance\_any\_label} 552 allow to extract from a structured trace the list of states whose next 553 instruction is a cost emission statement. We only show here the type of one 554 of them: 555 \begin{alltt} 556 flatten_trace_label_return: 557 \(\forall\)S: abstract_status. \(\forall\)\(s_1,s_2\). 558 trace_label_return \(s_1\) \(s_2\) \(\to\) list (as_cost_label S) 559 \end{alltt} 560 561 \paragraph{Cost prediction on structured traces} 641 There are three mutual structural recursive functions, one for each of 642 \verb+TLR+, \verb+TLL+ and \verb+TAL+, for which we use the same notation 643 $\,.\,$: the \emph{flattening} of the traces. These functions 644 allow to extract from a structured trace the list of emitted cost labels. 645 % We only show here the type of one 646 % of them: 647 % \begin{alltt} 648 % flatten_trace_label_return: 649 % \(\forall\)S: abstract_status. \(\forall\)\(s_1,s_2\). 650 % trace_label_return \(s_1\) \(s_2\) \(\to\) list (as_cost_label S) 651 % \end{alltt} 652 653 \paragraph{Cost prediction on structured traces.} 562 654 563 655 The first main theorem of CerCo about traces … … 568 660 Simplifying a bit, it states that 569 661 \begin{equation}\label{th1} 570 \begin{array}{l}\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.\\~~ 571 \texttt{clock}~s_2 = \texttt{clock}~s_1 + \Sigma_{s \in (\texttt{flatten\_trace\_label\_return}~\tau)}\;k(\mathcal{L}(s)) 662 \begin{array}{l}\forall s_1,s_2. \forall \tau: \texttt{TLR}~s_1~s_2.~ 663 \texttt{clock}~s_2 = \texttt{clock}~s_1 + 664 \Sigma_{\alpha \in \tau}\;k(\alpha) 572 665 \end{array} 573 666 \end{equation} 574 where $\mathcal{L}$ maps a labelled state to its emitted label, and the 575 cost model $k$ is statically computed from the object code 576 by associating to each label \texttt{L} the sum of the cost of the instructions 577 in the basic block that starts at \texttt{L} and ends before the next labelled 667 where the cost model $k$ is statically computed from the object code 668 by associating to each label $\alpha$ the sum of the cost of the instructions 669 in the basic block that starts at $\alpha$ and ends before the next labelled 578 670 instruction. The theorem is proved by structural induction over the structured 579 671 trace, and is based on the invariant that … … 582 674 the structured trace starts with $s_1$, then eventually it will contain also 583 675 $s_2$. When $s_1$ is not a function call, the result holds trivially because 584 of the $ (\texttt{as\_execute}~s_1~s_2)$ condition obtained by inversion on676 of the $s_1\exec s_2$ condition obtained by inversion on 585 677 the trace. The only non 586 678 trivial case is the one of function calls: the cost model computation function … … 590 682 this state. 591 683 592 \paragraph{Structured traces similarity and cost prediction invariance }684 \paragraph{Structured traces similarity and cost prediction invariance.} 593 685 594 686 A compiler pass maps source to object code and initial states to initial … … 603 695 interested only in those compiler passes that maps a trace $\tau_1$ to a trace 604 696 $\tau_2$ such that 605 \begin{equation} \texttt{flatten\_trace\_label\_return}~\tau_1 = \texttt{flatten\_trace\_label\_return}~\tau_2\label{condition1}\label{th2}\end{equation}606 The reason is that the combination of~\ ref{th1} with~\ref{th2} yields the697 \begin{equation}\tau_1 = \tau_2.\label{th2}\end{equation} 698 The reason is that the combination of~\eqref{th1} with~\eqref{th2} yields the 607 699 corollary 608 \begin{equation}\begin{array}{l}\label{th3} 609 \forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.\\~~~~~\; 610 clock~s_2  clock~s_1\\~ = \Sigma_{s \in (\texttt{flatten\_trace\_label\_return}~\tau_1)}\;k(\mathcal{L}(s))\\~ = \Sigma_{s \in (\texttt{flatten\_trace\_label\_return}~\tau_2)}\;k(\mathcal{L}(s)) 611 \end{array}\end{equation} 700 \begin{equation}\label{th3} 701 \forall s_1,s_2. \forall \tau: \texttt{TLR}~s_1~s_2.~ 702 \texttt{clock}~s_2  \texttt{clock}~s_1 = 703 \Sigma_{\alpha \in \tau_1}\;k(\alpha) = 704 \Sigma_{\alpha \in \tau_2}\;k(\alpha). 705 \end{equation} 612 706 This corollary states that the actual execution time of the program can be computed equally well on the source or target language. Thus it becomes possible to 613 707 transfer the cost model from the target to the source code and reason on the 614 708 source code only. 615 709 616 We are therefore interested in conditions stronger than~\ ref{condition1}.710 We are therefore interested in conditions stronger than~\eqref{th2}. 617 711 Therefore we introduce here a similarity relation between traces with 618 712 the same structure. Theorem~\texttt{tlr\_rel\_to\_traces\_same\_flatten} 619 in the Matita formalisation shows that~\ ref{th2} holds for every pair713 in the Matita formalisation shows that~\eqref{th2} holds for every pair 620 714 $(\tau_1,\tau_2)$ of similar traces. 621 715 622 716 Intuitively, two traces are similar when one can be obtained from 623 717 the other by erasing or inserting silent steps, i.e. states that are 624 not \texttt{as\_costed} and that are classified as \texttt{ other}.718 not \texttt{as\_costed} and that are classified as \texttt{cl\_other}. 625 719 Silent steps do not alter the structure of the traces. 626 720 In particular, … … 635 729 the definition into inference rules for the sake of readability. We also 636 730 omit from trace constructors all arguments, but those that are traces or that 637 are used in the premises of the rules. 638 731 are used in the premises of the rules. By abuse of notation we denote all three 732 relations by infixing $\approx$ 733 734 \begin{multicols}{2} 639 735 \infrule 640 { \texttt{tll\_rel}~tll_1~tll_2736 {tll_1\approx tll_2 641 737 } 642 {\texttt{tlr\_ rel}~(\texttt{tlr\_base}~tll_1)~(\texttt{tlr\_base}~tll_2)}738 {\texttt{tlr\_base}~tll_1 \approx \texttt{tlr\_base}~tll_2} 643 739 644 740 \infrule 645 { \texttt{tll\_rel}~tll_1~tll_2 \andalso646 \texttt{tlr\_rel}~tlr_1~tlr_2741 {tll_1 \approx tll_2 \andalso 742 tlr_1 \approx tlr_2 647 743 } 648 {\texttt{tlr\_rel}~(\texttt{tlr\_step}~tll_1~tlr_1)~(\texttt{tlr\_step}~tll_2~tlr_2)} 744 {\texttt{tlr\_step}~tll_1~tlr_1 \approx \texttt{tlr\_step}~tll_2~tlr_2} 745 \end{multicols} 649 746 650 747 \infrule 651 {\ texttt{as\_label}~H_1 = \texttt{as\_label}~H_2 \andalso652 \texttt{tal\_rel}~tal_1~tal_2748 {\ell~s_1 = \ell~s_2 \andalso 749 tal_1\approx tal_2 653 750 } 654 {\texttt{tll\_ rel}~(\texttt{tll\_base}~tal_1~H_1)~(\texttt{tll\_base}~tal_2~H_2)}751 {\texttt{tll\_base}~s_1~tal_1 \approx \texttt{tll\_base}~s_2~tal_2} 655 752 656 753 \infrule 657 754 {} 658 {\texttt{tal\_ rel}~\texttt{tal\_base\_not\_return}~(taa @\texttt{tal\_base\_not\_return}}755 {\texttt{tal\_base\_not\_return}\approx taa \append \texttt{tal\_base\_not\_return}} 659 756 660 757 \infrule 661 758 {} 662 {\texttt{tal\_ rel}~\texttt{tal\_base\_return}~(taa @\texttt{tal\_base\_return}}759 {\texttt{tal\_base\_return}\approx taa \append \texttt{tal\_base\_return}} 663 760 664 761 \infrule 665 { \texttt{tlr\_rel}~tlr_1~tlr_2 \andalso666 \texttt{as\_call\_ident}~H_1 = \texttt{as\_call\_ident}~H_2762 {tlr_1\approx tlr_2 \andalso 763 s_1 \uparrow f \andalso s_2\uparrow f 667 764 } 668 {\texttt{tal\_ rel}~(\texttt{tal\_base\_call}~H_1~tlr_1)~(taa @ \texttt{tal\_base\_call}~H_2~tlr_2)}765 {\texttt{tal\_base\_call}~s_1~tlr_1\approx taa \append \texttt{tal\_base\_call}~s_2~tlr_2} 669 766 670 767 \infrule 671 { \texttt{tlr\_rel}~tlr_1~tlr_2 \andalso672 \texttt{as\_call\_ident}~H_1 = \texttt{as\_call\_ident}~H_2\andalso768 {tlr_1\approx tlr_2 \andalso 769 s_1 \uparrow f \andalso s_2\uparrow f \andalso 673 770 \texttt{tal\_collapsable}~tal_2 674 771 } 675 {\texttt{tal\_ rel}~(\texttt{tal\_base\_call}~tlr_1)~(taa @ \texttt{tal\_step\_call}~tlr_2~tal_2)}772 {\texttt{tal\_base\_call}~s_1~tlr_1 \approx taa \append \texttt{tal\_step\_call}~s_2~tlr_2~tal_2)} 676 773 677 774 \infrule 678 { \texttt{tlr\_rel}~tlr_1~tlr_2 \andalso679 \texttt{as\_call\_ident}~H_1 = \texttt{as\_call\_ident}~H_2\andalso775 {tlr_1\approx tlr_2 \andalso 776 s_1 \uparrow f \andalso s_2\uparrow f \andalso 680 777 \texttt{tal\_collapsable}~tal_1 681 778 } 682 {\texttt{tal\_ rel}~(\texttt{tal\_step\_call}~tlr_1~tal_1)~(taa @ \texttt{tal\_base\_call}~tlr_2)}779 {\texttt{tal\_step\_call}~s_1~tlr_1~tal_1 \approx taa \append \texttt{tal\_base\_call}~s_2~tlr_2)} 683 780 684 781 \infrule 685 { \texttt{tlr\_rel}~tlr_1~tlr_2 \andalso686 \texttt{tal\_rel}~tal_1~tal_2 \andalso687 \texttt{as\_call\_ident}~H_1 = \texttt{as\_call\_ident}~H_2782 {tlr_1 \approx tlr_2 \andalso 783 s_1 \uparrow f \andalso s_2\uparrow f 784 tal_1 \approx tal_2 \andalso 688 785 } 689 {\texttt{tal\_ rel}~(\texttt{tal\_step\_call}~tlr_1~tal_1)~(taa @ \texttt{tal\_step\_call}~tlr_2~tal_2)}786 {\texttt{tal\_step\_call}~s_1~tlr_1~tal_1 \approx taa \append \texttt{tal\_step\_call}~s_2~tlr_2~tal_2} 690 787 691 788 \infrule 692 { \texttt{tal\_rel}~tal_1~tal_2789 {tal_1\approx tal_2 693 790 } 694 {\texttt{tal\_ rel}~(\texttt{tal\_step\_default}~tal_1)~tal_2}791 {\texttt{tal\_step\_default}~tal_1 \approx tal_2} 695 792 \begin{comment} 696 793 \begin{verbatim} … … 768 865 769 866 In the preceding rules, a $taa$ is an inhabitant of the 770 $\texttt{trace\_any\_any}~s_1~s_2$ inductive data type whose definition 867 $\texttt{trace\_any\_any}~s_1~s_2$ (shorthand $\texttt{TAA}~s_1~s_2$), 868 an inductive data type whose definition 771 869 is not in the paper for lack of space. It is the type of valid 772 prefixes (even empty ones) of \texttt{ trace\_any\_label}s that do not contain870 prefixes (even empty ones) of \texttt{TAL}'s that do not contain 773 871 any function call. Therefore it 774 is possible to concatenate (using ``$ @$'') a \texttt{trace\_any\_any} to the775 left of a \texttt{ trace\_any\_label}. A \texttt{trace\_any\_any} captures872 is possible to concatenate (using ``$\append$'') a \texttt{TAA} to the 873 left of a \texttt{TAL}. A \texttt{TAA} captures 776 874 a sequence of silent moves. 777 875 778 The \texttt{tal\_collapsable} unary predicate over \texttt{ trace\_any\_label}s876 The \texttt{tal\_collapsable} unary predicate over \texttt{TAL}'s 779 877 holds when the argument does not contain any function call and it ends 780 878 with a label (not a return). The intuition is that after a function call we … … 865 963 compiler pass. 866 964 867 \paragraph{Relation sets }965 \paragraph{Relation sets.} 868 966 869 967 We introduce now the four relations $\mathcal{S,C,L,R}$ between abstract … … 906 1004 \end{alltt} 907 1005 908 \paragraph{1to0ormany forward simulation conditions} 1006 \begin{figure} 1007 \centering 1008 \begin{tabular}{@{}c@{}c@{}} 1009 \begin{subfigure}{.475\linewidth} 1010 \centering 1011 \begin{tikzpicture}[every join/.style={ar}, join all, thick, 1012 every label/.style=overlay, node distance=10mm] 1013 \matrix [diag] (m) {% 1014 \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\ 1015 \node (s2) {}; & \node (t2) {}; \\ 1016 }; 1017 \node [above=0 of t1, overlay] {$\alpha$}; 1018 {[stealth] 1019 \draw (s1)  (t1); 1020 \draw [new] (s2)  node [above] {$*$} (t2); 1021 } 1022 \draw (s1) to node [rel] {$\S$} (s2); 1023 \draw [new] (t1) to node [rel] {$\S,\L$} (t2); 1024 \end{tikzpicture} 1025 \caption{The \texttt{cl\_jump} case.} 1026 \label{subfig:cl_jump} 1027 \end{subfigure} 1028 & 1029 \begin{subfigure}{.475\linewidth} 1030 \centering 1031 \begin{tikzpicture}[every join/.style={ar}, join all, thick, 1032 every label/.style=overlay, node distance=10mm] 1033 \matrix [diag] (m) {% 1034 \node (s1) {}; & \node (t1) {};\\ 1035 \node (s2) {}; & \node (t2) {}; \\ 1036 }; 1037 {[stealth] 1038 \draw (s1)  (t1); 1039 \draw [new] (s2)  node [above] {$*$} (t2); 1040 } 1041 \draw (s1) to node [rel] {$\S$} (s2); 1042 \draw [new] (t1) to node [rel] {$\S,\L$} (t2); 1043 \end{tikzpicture} 1044 \caption{The \texttt{cl\_oher} case.} 1045 \label{subfig:cl_other} 1046 \end{subfigure} 1047 \\ 1048 \begin{subfigure}{.475\linewidth} 1049 \centering 1050 \begin{tikzpicture}[every join/.style={ar}, join all, thick, 1051 every label/.style=overlay, node distance=10mm] 1052 \matrix [diag, small vgap] (m) {% 1053 \node (t1) {}; \\ 1054 \node (s1) [is call] {}; \\ 1055 & \node (l) {}; & \node (t2) {};\\ 1056 \node (s2) {}; & \node (c) [is call] {};\\ 1057 }; 1058 {[stealth] 1059 \draw (s1)  node [left] {$f$} (t1); 1060 \draw [new] (s2)  node [above] {$*$} (c); 1061 \draw [new] (c)  node [right] {$f$} (l); 1062 \draw [new] (l)  node [above] {$*$} (t2); 1063 } 1064 \draw (s1) to node [rel] {$\S$} (s2); 1065 \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2); 1066 \draw [new] (t1) to [bend left] node [rel] {$\L$} (l); 1067 \draw [new] (t1) to node [rel] {$\C$} (c); 1068 \end{tikzpicture} 1069 \caption{The \texttt{cl\_call} case.} 1070 \label{subfig:cl_call} 1071 \end{subfigure} 1072 & 1073 \begin{subfigure}{.475\linewidth} 1074 \centering 1075 \begin{tikzpicture}[every join/.style={ar}, join all, thick, 1076 every label/.style=overlay, node distance=10mm] 1077 \matrix [diag, small vgap] (m) {% 1078 \node (s1) [is ret] {}; \\ 1079 \node (t1) {}; \\ 1080 \node (s2) {}; & \node (c) [is ret] {};\\ 1081 & \node (r) {}; & \node (t2) {}; \\ 1082 }; 1083 {[stealth] 1084 \draw (s1)  (t1); 1085 \draw [new] (s2)  node [above] {$*$} (c); 1086 \draw [new] (c)  (r); 1087 \draw [new] (r)  node [above] {$*$} (t2); 1088 } 1089 \draw (s1) to [bend right=45] node [rel] {$\S$} (s2); 1090 \draw [new, overlay] (t1) to [bend left=90, looseness=1] node [rel] {$\S,\L$} (t2); 1091 \draw [new, overlay] (t1) to [bend left=90, looseness=1.2] node [rel] {$\R$} (r); 1092 \end{tikzpicture} 1093 \caption{The \texttt{cl\_return} case.} 1094 \label{subfig:cl_return} 1095 \end{subfigure} 1096 \end{tabular} 1097 \caption{The hypotheses for the preservation of structured traces, simplified. 1098 Dashed lines 1099 and arrows indicates how the diagrams must be closed when solid relations 1100 are present.} 1101 \label{fig:forwardsim} 1102 \end{figure} 1103 1104 \paragraph{1to0ormany forward simulation conditions.} 909 1105 \begin{condition}[Cases \texttt{cl\_other} and \texttt{cl\_jump}] 910 For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$, and 911 $\texttt{as\_execute}~s_1~s_1'$, and $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$ or $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$ and 912 $\texttt{as\_costed}~s_1'$, there exists an $s_2'$ and a $\texttt{trace\_any\_any\_free}~s_2~s_2'$ called $taaf$ such that $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either 1106 For all $s_1,s_1',s_2$ such that $s_1 \S s_1'$, and 1107 $s_1\exec s_1'$, and either $s_1 \class \texttt{cl\_other}$ or 1108 both $s_1\class\texttt{cl\_other}\}$ and $\ell~s_1'$, 1109 there exists an $s_2'$ and a $\texttt{trace\_any\_any\_free}~s_2~s_2'$ called $taaf$ 1110 such that $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either 913 1111 $taaf$ is non empty, or one among $s_1$ and $s_1'$ is \texttt{as\_costed}. 914 1112 \end{condition} 915 1113 916 In the above condition, a $\texttt{trace\_any\_any\_free}~s_1~s_2$ is an 1114 In the above condition, a $\texttt{trace\_any\_any\_free}~s_1~s_2$ (which from now on 1115 will be shorthanded as \verb+TAAF+) is an 917 1116 inductive type of structured traces that do not contain function calls or 918 cost emission statements. Differently from a \ texttt{trace\_any\_any}, the1117 cost emission statements. Differently from a \verb+TAA+, the 919 1118 instruction to be executed in the lookahead state $s_2$ may be a cost emission 920 1119 statement. … … 923 1122 preserves the relation between the data and if the two final statuses are 924 1123 labelled in the same way. Moreover, we must take special care of the empty case 925 to avoid collapsing two consecutive states that emit the same label to just 926 one state, missing one of the two emissions. 1124 to avoid collapsing two consecutive states that emit a label, missing one of the two emissions. 927 1125 928 1126 \begin{condition}[Case \texttt{cl\_call}] 929 For all $s_1,s_1',s_2$ s.t. $s_1 \ mathcal{S}s_1'$ and930 $ \texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_call}$, there exists $s_2', s_b, s_a$, a931 $\ texttt{trace\_any\_any}~s_2~s_b$, and a932 $\ texttt{trace\_any\_any\_free}~s_a~s_2'$ such that:933 $s_a $ is classified as a \texttt{cl\_call}, the \texttt{as\_identifiers}of934 the two call states are the same, $s_1 \mathcal{C} s_ b$,935 $ \texttt{as\_execute}~s_b~s_a$ holds, $s_1' \mathcal{L}s_b$ and936 $s_1' \ mathcal{S}s_2'$.1127 For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$ and 1128 $s_1\exec s_1'$ and $s_1 \class \texttt{cl\_call}$, there exists $s_a, s_b, s_2'$, a 1129 $\verb+TAA+~s_2~s_a$, and a 1130 $\verb+TAAF+~s_b~s_2'$ such that: 1131 $s_a\class\texttt{cl\_call}$, the \texttt{as\_call\_ident}'s of 1132 the two call states are the same, $s_1 \mathcal{C} s_a$, 1133 $s_a\exec s_b$, $s_1' \L s_b$ and 1134 $s_1' \S s_2'$. 937 1135 \end{condition} 938 1136 … … 945 1143 946 1144 \begin{condition}[Case \texttt{cl\_return}] 947 For all $s_1,s_1',s_2$ s.t. $s_1 \ mathcal{S}s_1'$,948 $ \texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_return}$, there exists $s_2', s_b, s_a$, a949 $\ texttt{trace\_any\_any}~s_2~s_b$, a950 $\ texttt{trace\_any\_any\_free}~s_a~s_2'$ called $taaf$ such that:1145 For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$, 1146 $s_1\exec s_1'$ and $s_1 \class \texttt{cl\_return}$, there exists $s_a, s_b, s_2'$, a 1147 $\verb+TAA+~s_2~s_a$, a 1148 $\verb+TAAF+~s_b~s_2'$ called $taaf$ such that: 951 1149 $s_a$ is classified as a \texttt{cl\_return}, 952 $s_1 \mathcal{C} s_b$, the predicate 953 $\texttt{as\_execute}~s_b~s_a$ holds, 954 $s_1' \mathcal{R} s_a$ and 955 $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either 956 $taaf$ is non empty, or $s_a$ is not \texttt{as\_costed}. 1150 $s_a\exec s_b$, 1151 $s_1' \R s_b$ and 1152 $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either 1153 $taaf$ is non empty, or $\lnot \ell~s_a$. 957 1154 \end{condition} 958 1155 … … 1067 1264 \begin{theorem}[\texttt{status\_simulation\_produce\_tlr}] 1068 1265 For every $s_1,s_1',s_{2_b},s_2$ s.t. 1069 there is a $\texttt{ trace\_label\_return}~s_1~s_1'$ called $tlr_1$ and a1070 $\ texttt{trace\_any\_any}~s_{2_b}~s_2$ and $s_1 \mathcal{L}s_{2_b}$ and1071 $s_1 \ mathcal{S}s_2$, there exists $s_{2_m},s_2'$ s.t.1072 there is a $\texttt{ trace\_label\_return}~s_{2_b}~s_{2_m}$ called $tlr_2$ and1073 there is a $\ texttt{trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taaf$1074 s.t. if $taaf$ is non empty then $\lnot (\ texttt{as\_costed}~s_{2_m})$,1075 and $ \texttt{tlr\_rel}~tlr_1~tlr_2$1076 and $s_1' (\mathcal{S} \cap \mathcal{L})s_2'$ and1077 $s_1' \ mathcal{R}s_{2_m}$.1266 there is a $\texttt{TLR}~s_1~s_1'$ called $tlr_1$ and a 1267 $\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and 1268 $s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t. 1269 there is a $\texttt{TLR}~s_{2_b}~s_{2_m}$ called $tlr_2$ and 1270 there is a $\verb+TAAF+~s_{2_m}~s_2'$ called $taaf$ 1271 s.t. if $taaf$ is non empty then $\lnot (\ell~s_{2_m})$, 1272 and $tlr_1\approx tlr_2$ 1273 and $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and 1274 $s_1' \R s_{2_m}$. 1078 1275 \end{theorem} 1079 1276 1080 1277 The theorem states that a \texttt{trace\_label\_return} in the source code 1081 1278 together with a precomputed preamble of silent states 1082 (the \ texttt{trace\_any\_any}) in the target code induces a1083 similar \texttt{trace\_label\_return} tracein the target code which can be1279 (the \verb+TAA+) in the target code induces a 1280 similar \texttt{trace\_label\_return} in the target code which can be 1084 1281 followed by a sequence of silent states. Note that the statement does not 1085 require the produced \texttt{trace\_label\_return} t race to start with the1282 require the produced \texttt{trace\_label\_return} to start with the 1086 1283 precomputed preamble, even if this is likely to be the case in concrete 1087 1284 implementations. The preamble in input is necessary for compositionality, e.g. … … 1092 1289 \begin{theorem}[\texttt{status\_simulation\_produce\_tll}] 1093 1290 For every $s_1,s_1',s_{2_b},s_2$ s.t. 1094 there is a $\texttt{ trace\_label\_label}~b~s_1~s_1'$ called $tll_1$ and a1095 $\ texttt{trace\_any\_any}~s_{2_b}~s_2$ and $s_1 \mathcal{L}s_{2_b}$ and1096 $s_1 \ mathcal{S}s_2$, there exists $s_{2_m},s_2'$ s.t.1291 there is a $\texttt{TLL}~b~s_1~s_1'$ called $tll_1$ and a 1292 $\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and 1293 $s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t. 1097 1294 \begin{itemize} 1098 1295 \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$ 1099 and a trace $\texttt{ trace\_label\_label}~b~s_{2_b}~s_{2_m}$ called $tll_2$1100 and a $\texttt{ trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taa_2$ s.t.1101 $s_1' (\mathcal{S} \cap \mathcal{L})s_2'$ and1102 $s_1' \ mathcal{R}s_{2_m}$ and1103 $ \texttt{tll\_rel}~tll_1~tll_2$ and1104 if $taa_2$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$1296 and a trace $\texttt{TLL}~b~s_{2_b}~s_{2_m}$ called $tll_2$ 1297 and a $\texttt{TAAF}~s_{2_m}~s_2'$ called $taa_2$ s.t. 1298 $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and 1299 $s_1' \R s_{2_m}$ and 1300 $tll_1\approx tll_2$ and 1301 if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$; 1105 1302 \item else there exists $s_2'$ and a 1106 $\texttt{ trace\_label\_label}~b~s_{2_b}~s_2'$ called $tll_2$ such that1107 $s_1' (\mathcal{S} \cap \mathcal{L})s_2'$ and1108 $ \texttt{tll\_rel}~tll_1~tll_2$.1303 $\texttt{TLL}~b~s_{2_b}~s_2'$ called $tll_2$ such that 1304 $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and 1305 $tll_1\approx tll_2$. 1109 1306 \end{itemize} 1110 1307 \end{theorem} … … 1118 1315 \begin{theorem}[\texttt{status\_simulation\_produce\_tal}] 1119 1316 For every $s_1,s_1',s_2$ s.t. 1120 there is a $\texttt{ trace\_any\_label}~b~s_1~s_1'$ called $tal_1$ and1317 there is a $\texttt{TAL}~b~s_1~s_1'$ called $tal_1$ and 1121 1318 $s_1 \mathcal{S} s_2$ 1122 1319 \begin{itemize} 1123 1320 \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$ 1124 and a trace $\texttt{ trace\_any\_label}~b~s_2~s_{2_m}$ called $tal_2$ and a1125 $\texttt{ trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taa_2$ s.t.1126 $s_1' (\mathcal{S} \cap \mathcal{L})s_2'$ and1127 $s_1' \ mathcal{R}s_{2_m}$ and1128 $ \texttt{tal\_rel}~tal_1~tal_2$ and1129 if $taa_2$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$1321 and a trace $\texttt{TAL}~b~s_2~s_{2_m}$ called $tal_2$ and a 1322 $\texttt{TAAF}~s_{2_m}~s_2'$ called $taa_2$ s.t. 1323 $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and 1324 $s_1' \R s_{2_m}$ and 1325 $tal_1 \approx tal_2$ and 1326 if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$; 1130 1327 \item else there exists $s_2'$ and a 1131 $\texttt{ trace\_any\_label}~b~s_2~s_2'$ called $tal_2$ such that1132 either $s_1' (\mathcal{S} \cap \mathcal{L})s_2'$ and1133 $ \texttt{tal\_rel}~tal_1~tal_2$1134 or $s_1' (\mathcal{S} \cap \mathcal{L})s_2$ and1135 $\texttt{tal\_collapsable}~tal_1$ and $\lnot (\texttt{as\_costed}~s_1)$1328 $\texttt{TAL}~b~s_2~s_2'$ called $tal_2$ such that 1329 either $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and 1330 $tal_1\approx tal_2$ 1331 or $s_1' \mathrel{{\S} \cap {\L}} s_2$ and 1332 $\texttt{tal\_collapsable}~tal_1$ and $\lnot \ell~s_1$. 1136 1333 \end{itemize} 1137 1334 \end{theorem} … … 1229 1426 the CerCo compiler exploiting the main theorem of this paper. 1230 1427 1231 \paragraph{Related works }1428 \paragraph{Related works.} 1232 1429 CerCo is the first project that explicitly tries to induce a 1233 1430 precise cost model on the source code in order to establish nonfunctional
Note: See TracChangeset
for help on using the changeset viewer.