Changeset 2625 for Papers/itp2013/ccexec.tex
 Timestamp:
 Feb 6, 2013, 8:14:38 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec.tex
r2622 r2625 354 354 as \texttt{cl\_other}); finally $(\texttt{as\_after\_return}~s_1~s_2)$ holds 355 355 if the next instruction to be executed in $s_2$ follows the function call 356 to be executed in (the witness of the $\Sigma$type) $s_1$. 356 to be executed in (the witness of the $\Sigma$type) $s_1$. The two functions 357 \texttt{as\_label} and \texttt{as\_cost\_ident} are used to extract the 358 cost label/function call target from states whose next instruction is 359 a cost emission/function call statement. 357 360 358 361 … … 518 521 \end{comment} 519 522 A \texttt{trace\_label\_return} is isomorphic to a list of 520 \texttt{trace\_label\_label}s that end with a cost emission followed by a 521 \texttt{trace\_label\_label} that ends with a return. 522 523 The interesting cases are those of $(\texttt{trace\_any\_label}~b~s_1~s_2)$. 523 \texttt{trace\_label\_label}s that ends with a cost emission followed by a 524 return terminated \texttt{trace\_label\_label}. 525 The interesting cases are those of $\texttt{trace\_any\_label}~b~s_1~s_2$. 524 526 A \texttt{trace\_any\_label} is a sequence of steps built by a syntax directed 525 527 definition on the classification of $s_1$. The constructors of the datatype … … 529 531 \begin{enumerate} 530 532 \item the trace is never empty; it ends with a return iff $b$ is 531 true (\texttt{ends\_with\_ret})533 true 532 534 \item a jump must always be the last instruction of the trace, and it must 533 535 be followed by a cost emission statement; i.e. the target of a jump … … 536 538 \item a cost emission statement can never occur inside the trace, only in 537 539 the status immediately after 538 \item the trace for a function call step is made from a subtrace of type 539 $(\texttt{trace\_label\_return}~s_1~s_2)$, possibly followed by the 540 \item the trace for a function call step is made of a subtrace for the 541 function body of type 542 $\texttt{trace\_label\_return}~s_1~s_2$, possibly followed by the 540 543 rest of the trace for this basic block. The subtrace represents the 541 544 function execution. Being an inductive datum, it grants totality of … … 549 552 instruction is a cost emission statement. We only show here the type of one 550 553 of them: 551 \begin{ verbatim}554 \begin{alltt} 552 555 flatten_trace_label_return: 553 (S: abstract_status) 554 (start_status: S) (final_status: S) 555 (the_trace: trace_label_return S start_status final_status) 556 on the_trace: list (as_cost_label S) 557 \end{verbatim} 556 \(\forall\)S: abstract_status. \(\forall\)\(s_1,s_2\). 557 trace_label_return \(s_1\) \(s_2\) \(\to\) list (as_cost_label S) 558 \end{alltt} 558 559 559 560 \paragraph{Cost prediction on structured traces} 560 561 561 The first main theorem of CerCo about structuredtraces562 The first main theorem of CerCo about traces 562 563 (theorem \texttt{compute\_max\_trace\_label\_return\_cost\_ok\_with\_trace}) 563 564 holds for the … … 565 566 of the structured traces to the concrete status of object code programs. 566 567 Simplifying a bit, it states that 567 $\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2. 568 clock~s_2 = clock~s_1 + \Sigma_{s \in \texttt{flatten\_trace\_label\_return}~\tau} k(L(s))$ where $L$ maps a labelled state to its emitted label, and the 568 \begin{equation}\label{th1} 569 \begin{array}{l}\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.\\~~ 570 \texttt{clock}~s_2 = \texttt{clock}~s_1 + \Sigma_{s \in (\texttt{flatten\_trace\_label\_return}~\tau)}\;k(\mathcal{L}(s)) 571 \end{array} 572 \end{equation} 573 where $\mathcal{L}$ maps a labelled state to its emitted label, and the 569 574 cost model $k$ is statically computed from the object code 570 575 by associating to each label \texttt{L} the sum of the cost of the instructions … … 597 602 interested only in those compiler passes that maps a trace $\tau_1$ to a trace 598 603 $\tau_2$ such that 599 \begin{displaymath}(\texttt{flatten\_trace\_label\_return}~\tau_1 = \texttt{flatten\_trace\_label\_return}~\tau_2)\label{condition1}\end{displaymath} 600 The reason is that when this happens we obviously have the 601 following corollary to the previous theorem: 602 $$\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2. 603 clock~s_2  clock~s_1 = \Sigma_{s \in \texttt{flatten\_trace\_label\_return}~\tau_1} k(L(s)) = \Sigma_{s \in \texttt{flatten\_trace\_label\_return}~\tau_2} k(L(s))$$ 604 The 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 604 \begin{equation}\texttt{flatten\_trace\_label\_return}~\tau_1 = \texttt{flatten\_trace\_label\_return}~\tau_2\label{condition1}\label{th2}\end{equation} 605 The reason is that the combination of~\ref{th1} with~\ref{th2} yields the 606 corollary 607 \begin{equation}\begin{array}{l}\label{th3} 608 \forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.\\~~~~~\; 609 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)) 610 \end{array}\end{equation} 611 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 605 612 transfer the cost model from the target to the source code and reason on the 606 613 source code only. 607 614 608 615 We are therefore interested in conditions stronger than~\ref{condition1}. 609 Therefore we introduce here a similarity relation between traces that captures 610 the fact that two traces have the same structure and that 611 implies~\ref{condition1} (theorem \texttt{tlr\_rel\_to\_traces\_same\_flatten}). Two traces are similar when one can be obtained from 612 the other by erasing or inserting steps classified as \texttt{other} into the 613 \texttt{trace\_any\_label} blocks of the trace. In particular, 616 Therefore we introduce here a similarity relation between traces with 617 the same structure. Theorem~\texttt{tlr\_rel\_to\_traces\_same\_flatten} 618 in the Matita formalization shows that~\ref{th2} holds for every pair 619 $(\tau_1,\tau_2)$ of similar traces. 620 621 Intuitively, two traces are similar when one can be obtained from 622 the other by erasing or inserting silent steps, i.e. states that are 623 not \texttt{as\_costed} and that are classified as \texttt{other}. 624 Silent steps do not alter the structure of the traces. 625 In particular, 614 626 the relation maps function calls to function calls to the same function, 615 627 label emission statements to emissions of the same label, concatenation of … … 617 629 the same emissione statement, etc. 618 630 619 The similarity relation definition if simple, but it involves a large 620 number of cases. In the formalization, we define 621 $(\texttt{tlr\_rel}~tlr_1~tlr_2)$ by structural recursion on $tlr_1$ and pattern 622 matching over $tlr_2$. Here we turn 631 In the formalization the three similarity relations  one for each trace 632 kind  are defined by structural recursion on the first trace and pattern 633 matching over the second. Here we turn 623 634 the definition into inference rules for the sake of readability. We also 624 635 omit from trace constructors all arguments, but those that are traces or that … … 756 767 757 768 In the preceding rules, a $taa$ is an inhabitant of the 758 $ (\texttt{trace\_any\_any}~s_1~s_2)$ inductive data type whose definition759 we do not givein the paper for lack of space. It is the type of valid769 $\texttt{trace\_any\_any}~s_1~s_2$ inductive data type whose definition 770 is not in the paper for lack of space. It is the type of valid 760 771 prefixes (even empty ones) of \texttt{trace\_any\_label}s that do not contain 761 772 any function call. Therefore it 762 773 is possible to concatenate (using ``$@$'') a \texttt{trace\_any\_any} to the 763 left of a \texttt{trace\_any\_label}. The intuition is that two traces are 764 similar if one of them can perform more silent (non observables) moves, 765 whose sequences are here represented by \texttt{trace\_any\_any}. 774 left of a \texttt{trace\_any\_label}. A \texttt{trace\_any\_any} captures 775 a sequence of silent moves. 766 776 767 777 The \texttt{tal\_collapsable} unary predicate over \texttt{trace\_any\_label}s … … 788 798 forward simulation is the existence of a relation $R$ over states such that 789 799 if $s_1 R s_2$ and $s_1 \to^1 s_1'$ then there exists an $s_2'$ such that 790 $s_ 1'\to^* s_2'$ and $s_1' R s_2'$. In our context, we need to replace the800 $s_2 \to^* s_2'$ and $s_1' R s_2'$. In our context, we need to replace the 791 801 one and multi step transition relations $\to^n$ with the existence of 792 802 a structured trace between the two states, and we need to add the request that … … 801 811 in the general case. To understand why, consider the case of a function call 802 812 and the pass that fixes the parameter passing conventions. A function 803 call in the source code takes in input an arbitrary number of pseudoregisters (the actual parameters to pass) and returns an arbitrary number of pseudoregisters (where the result is stored). A function call in the target callhas no813 call in the source code takes in input an arbitrary number of pseudoregisters (the actual parameters to pass) and returns an arbitrary number of pseudoregisters (where the result is stored). A function call in the target language has no 804 814 input nor output parameters. The pass must add explicit code before and after 805 815 the function call to move the pseudoregisters content from/to the hardware … … 850 860 For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$, and 851 861 $\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 852 $ (\texttt{as\_costed}~s_1')$, there exists an $s_2'$ and a $taaf$ of type $(\texttt{trace\_any\_any\_free}~s_2~s_2')$ such that $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either862 $\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 853 863 $taaf$ is non empty, or one among $s_1$ and $s_1'$ is \texttt{as\_costed}. 854 864 \end{condition} 855 865 856 In the above condition, a $ (\texttt{trace\_any\_any\_free}~s_1~s_2)$ is an866 In the above condition, a $\texttt{trace\_any\_any\_free}~s_1~s_2$ is an 857 867 inductive type of structured traces that do not contain function calls or 858 868 cost emission statements. Differently from a \texttt{trace\_any\_any}, the … … 867 877 868 878 \begin{condition}[Case \texttt{cl\_call}] 869 For all $s_1,s_1',s_2$ s uch that$s_1 \mathcal{S} s_1'$ and870 $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_call}$, there exists $s_2', s_b, s_a$, a $taa_1$ of type871 $ (\texttt{trace\_any\_any}~s_2~s_b)$, a $taa_2$ of type872 $ (\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that:879 For all $s_1,s_1',s_2$ s.t. $s_1 \mathcal{S} s_1'$ and 880 $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_call}$, there exists $s_2', s_b, s_a$, a 881 $\texttt{trace\_any\_any}~s_2~s_b$, and a 882 $\texttt{trace\_any\_any\_free}~s_a~s_2'$ such that: 873 883 $s_a$ is classified as a \texttt{cl\_call}, the \texttt{as\_identifiers} of 874 the two call states are the same, $s_1 \mathcal{C} s_b$, the predicate875 $ (\texttt{as\_execute}~s_b~s_a)$ holds, $s_1' \mathcal{L} s_b$ and884 the two call states are the same, $s_1 \mathcal{C} s_b$, 885 $\texttt{as\_execute}~s_b~s_a$ holds, $s_1' \mathcal{L} s_b$ and 876 886 $s_1' \mathcal{S} s_2'$. 877 887 \end{condition}
Note: See TracChangeset
for help on using the changeset viewer.