Changeset 1683
 Timestamp:
 Feb 9, 2012, 5:41:26 PM (6 years ago)
 Location:
 Deliverables/addenda/indexed_labels
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/addenda/indexed_labels/report.tex
r1678 r1683 574 574 575 575 \renewcommand{\to}[1][]{\stackrel{#1}{\rightarrow}} 576 577 \newcommand{\eg}{\emph{e.g.\ }} 578 \newcommand{\ie}{\emph{i.e.\ }} 579 580 \newcommand{\inde}{\hspace{20pt}} 581 582 \usetikzlibrary{decorations.pathreplacing} 583 \newcommand{\tikztarget}[2]{% 584 \tikz[remember picture, baseline={(#1.base)}]{ 585 \node (#1) [inner sep = 0pt]{#2};}} 586 \newcommand{\tikztargetm}[2]{% 587 \tikz[remember picture, baseline={(#1.base)}]{ 588 \node (#1) [inner sep = 0pt]{$#2$};}} 576 589 %<<<<<<<<<<<< 577 590 \begin{document} 578 % \thispagestyle{empty} 579 % 580 % \vspace*{1cm} 581 % \begin{center} 582 % \includegraphics[width=0.6\textwidth]{../style/cerco_logo.png} 583 % \end{center} 584 % 585 % \begin{minipage}{\textwidth} 586 % \maketitle 587 % \end{minipage} 588 % 589 % 590 % \vspace*{0.5cm} 591 % \begin{center} 592 % \begin{LARGE} 593 % \bf 594 % Report \\ 595 % Dependent Cost Labels 596 % \\ 597 % \end{LARGE} 598 % \end{center} 599 % 600 % \vspace*{2cm} 601 % \begin{center} 602 % \begin{large} 603 % Version 0.1 604 % \end{large} 605 % \end{center} 606 % 607 % \vspace*{0.5cm} 608 % \begin{center} 609 % \begin{large} 610 % Main Author:\\ 611 % Paolo Tranquilli 612 % \end{large} 613 % \end{center} 614 % 615 % \vspace*{\fill} 616 % \noindent 617 % Project Acronym: \cerco{}\\ 618 % Project full title: Certified Complexity\\ 619 % Proposal/Contract no.: FP7ICT2009C243881 \cerco{}\\ 620 % 621 % \clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7ICT2009C243881} 622 % 623 % \newpage 591 \thispagestyle{empty} 592 593 \vspace*{1cm} 594 \begin{center} 595 \includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png} 596 \end{center} 597 598 \begin{minipage}{\textwidth} 599 \maketitle 600 \end{minipage} 601 602 603 \vspace*{0.5cm} 604 \begin{center} 605 \begin{LARGE} 606 \bf 607 Report \\ 608 Indexed Labels for Loop Iteration Dependent Costs 609 \\ 610 \end{LARGE} 611 \end{center} 612 613 \vspace*{2cm} 614 \begin{center} 615 \begin{large} 616 Version 0.1 617 \end{large} 618 \end{center} 619 620 \vspace*{0.5cm} 621 \begin{center} 622 \begin{large} 623 Main Author:\\ 624 Paolo Tranquilli 625 \end{large} 626 \end{center} 627 628 \vspace*{\fill} 629 \noindent 630 Project Acronym: \cerco{}\\ 631 Project full title: Certified Complexity\\ 632 Proposal/Contract no.: FP7ICT2009C243881 \cerco{}\\ 633 634 \clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7ICT2009C243881} 635 636 \newpage 637 638 \begin{abstract} 639 We present an extension to the labelling approach to lift resource 640 consumption information from compiled to source code~\cite{D2.1}. Cost labels 641 inserted at key points of the source code and kept track of during compilation 642 allow such a task. However, this approach is looses preciseness when differences 643 arise as to the cost of the same portion of code, whether due to code 644 transformation such as loop optimisation or advanced architecture features 645 (\eg cache). Our approach addresses this weakness as to some loop transformations 646 that rearrange the iterations of a loop (namely loop peeling and unrolling). It 647 consists in formally indexing cost labels with which iteration of the containing 648 loop they occur in, relative to the source code. This indexes can be transformed 649 during the compilation, and when lifted back to source code they produce dependent 650 costs. 651 652 The proposed changes have been implemented in CerCo's untrusted prototype compiler 653 from a large fragment of C to 8051 assembly~\cite{D2.2}. 654 \end{abstract} 655 624 656 625 657 \listoftodos … … 670 702 671 703 We concentrate on integrating the labelling approach with two loop transformations. 672 For general information on general compiler optimisations (and loop optimisations in particular) we refer the reader to the vast literature on the subject ( e.g.~\cite{muchnick,morgan}).704 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}). 673 705 674 706 \paragraph{Loop peeling} … … 768 800 We may omit the \s{else} clause of a conditional if it leads to a \s{skip} statement. 769 801 770 We will presuppose that all programs are \emph{welllabelled}, i.e.\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.802 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. 771 803 The \s{find} helper function has the task of not only finding the labelled statement in the program, but also building the correct continuation. 772 804 The continuation built by \s{find} replaces the current continuation in the case of a jump. … … 780 812 Many loop optimisations do not preserve the semantics of multientry loops in general, or are otherwise rendered ineffective. 781 813 Usually compilers implement a singleentry loop detection which avoids the multientry ones from being targeted by optimisations~\cite{muchnick,morgan}. 782 The loop transformations we present are local, i.e.\they target a single loop and transform it.814 The loop transformations we present are local, \ie they target a single loop and transform it. 783 815 Which loops are targeted may be decided by some \emph{ad hoc} heuristic. 784 816 However, the precise details of which loops are targetted and how is not important here. … … 801 833 $$ 802 834 where $\ell^j_i$ are again fresh labels for any $\ell_i$ labelling a statement in $S$. 803 This is a wil lfully na\"{i}ve version of loop unrolling, which usually targets less general loops.835 This is a wilfully na\"{i}ve version of loop unrolling, which usually targets less general loops. 804 836 The problem this transformation poses to CerCo's labelling approach are independent of the sophistication of the actual transformation. 837 838 \begin{example} 839 In \autoref{fig:example1} we show a program (a wilfully inefficient computation of of the 840 sum of the first $n$ factorials) and a possible transformation of it, combining loop 841 peeling and loop unrolling. 842 \begin{figureplr} 843 $$ 844 \fbox{$\begin{array}{l} 845 s\ass 0;\\ 846 i\ass 0;\\ 847 \sop{while}i<n\sbin{do}\\ 848 \inde p\ass 1;\\ 849 \inde j\ass 1;\\ 850 \inde \sop{while}j \le i\sbin{do}\\ 851 \inde \inde p\ass j*p\\ 852 \inde \inde j\ass j+1;\\ 853 \inde s\ass s+p;\\ 854 \inde i\ass i+1;\\ 855 \end{array} 856 $} 857 \mapsto 858 \fbox{$\begin{array}{l} 859 s\ass 0;\\ 860 i\ass 0;\\ 861 \tikztargetm{a}{\s{if}}\ i<n\sbin{then}\\ 862 \inde p\ass 1;\\ 863 \inde j\ass 1;\\ 864 \inde \sop{while}j \le i\sbin{do}\\ 865 \inde \inde p\ass j*p\\ 866 \inde \inde j\ass j+1;\\ 867 \inde s\ass s+p;\\ 868 \inde i\ass i+1;\\ 869 \inde \tikztargetm{d}{\s{while}}\ i<n\sbin{do}\\ 870 \inde \inde p\ass 1;\\ 871 \inde \inde j\ass 1;\\ 872 \inde \inde \tikztargetm{b}{\s{if}}\ j \le i\sbin{then}\\ 873 \inde \inde \inde p\ass j*p\\ 874 \inde \inde \inde j\ass j+1;\\ 875 \inde \inde \inde \sop{if}j \le i\sbin{then}\\ 876 \inde \inde \inde \inde p\ass j*p\\ 877 \inde \inde \inde \inde j\ass j+1;\\ 878 \inde \inde \inde \inde \s{while}\ j \le i\sbin{do}\\ 879 \inde \inde \inde \inde \inde p\ass j*p\\ 880 \inde \inde \inde \inde \inde j\ass j+1;\\ 881 \inde \inde \inde \inde \inde \sop{if}j \le i\sbin{then}\\ 882 \inde \inde \inde \inde \inde \inde p\ass j*p\\ 883 \inde \inde \inde \inde \inde \inde \tikztargetm{c}j\ass j+1;\\ 884 \inde \inde s\ass s+p;\\ 885 \inde \inde i\ass i+1;\\ 886 \inde \inde \sop{if}i<n\sbin{then}\\ 887 \inde \inde \inde p\ass 1;\\ 888 \inde \inde \inde j\ass 1;\\ 889 \inde \inde \inde \tikztargetm{e}{\s{while}}\ j < i\sbin{do}\\ 890 \inde \inde \inde \inde p\ass j*p\\ 891 \inde \inde \inde \inde j\ass j+1;\\ 892 \inde \inde \inde \inde \s{if}\ j < i\sbin{then}\\ 893 \inde \inde \inde \inde \inde p\ass j*p\\ 894 \inde \inde \inde \inde \inde \tikztargetm{f}j\ass j+1;\\ 895 \inde \inde \inde s\ass s+p;\\ 896 \inde \inde \inde i\ass i+1\tikztargetm{g};{} 897 \end{array} 898 $}\tikztargetm{right}{} 899 \begin{tikzpicture}[overlay, remember picture, thick, 900 brace/.style = {decorate, decoration={brace, amplitude = 15pt}}, 901 label/.style = {sloped, anchor = base, yshift = 17pt, font = \large}] 902 \draw [brace, transform canvas={xshift=5pt}] (b.northright)  node[label]{peeled} (c.southright); 903 \draw [brace, transform canvas={xshift=30pt}] (b.northright)  node[label]{unrolled} (c.southright); 904 \draw [brace, transform canvas={xshift=5pt}] (e.northright)  node[label]{unrolled} (f.southright); 905 \draw [brace, transform canvas={xshift=55pt}] (d.northright)  node[label]{unrolled} (g.southright); 906 \draw [brace, transform canvas={xshift=80pt}] (a.northright)  node[label]{peeled} (g.southright); 907 \end{tikzpicture} 908 \hspace{85pt}{} 909 $$ 910 \caption{An example of loop transformations done on an \imp{} program. Parentheses are omitted in favour of 911 blocks by indentation.} 912 \label{fig:example1} 913 \end{figureplr} 914 \end{example} 805 915 806 916 \section{Labelling: a quick sketch of the previous approach} … … 813 923 For further details we refer to~\cite{D2.1}. 814 924 815 With labels the small step semantics turns into a labelled transition system along with a natural notion of trace ( i.e.\lists of labels) arises.925 With labels the small step semantics turns into a labelled transition system along with a natural notion of trace (\ie lists of labels) arises. 816 926 The evaluation of statements is enriched with traces, so that rules follow a pattern similar to the following: 817 927 $$ … … 826 936 827 937 \paragraph{Labelling} 828 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. 938 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, 939 which is a conservative approach to ensuring that all loops have labels inside them, as a loop might be done with \s{goto}s. 829 940 The relevant cases are 830 941 $$\begin{aligned} … … 832 943 \sop{if}e\sbin{then}\alpha:\Ell(S)\sbin{else}\beta:\Ell(T)\\ 833 944 \Ell(\sop{while}e\sbin{do}S) &= 834 (\sop{while}e\sbin{do}\alpha:\Ell(S));\beta:\s{skip} 945 (\sop{while}e\sbin{do}\alpha:\Ell(S));\beta:\s{skip}\\ 946 \Ell(\ell : S) &= 947 (\ell : \alpha : \Ell(S)) 835 948 \end{aligned}$$ 836 949 where $\alpha,\beta$ are fresh cost labels. … … 879 992 $$ 880 993 What happens is that the cost label $\alpha$ is duplicated with two distinct occurrences. 881 If these two occurrences correspond to different costs in the compiled code, the best the cost mapping can do is to take the maximum of the two, preserving soundness ( i.e.\ the cost estimate still bounds the actual one) but losing preciseness (i.e.\ the actual cost would be strictly less than its estimate).994 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). 882 995 883 996 \section{Indexed labels} … … 931 1044 We sketch how this can be computed in the sequel. 932 1045 933 A first pass of the program $P$ can easily compute two maps: $\s{loopof}_P$ from each label $\ell$ to the occurrence ( i.e.\the path) of a $\s{while}$ loop containing $\ell$, or the empty path if none exists; and $\s{gotosof}_P$ from a label $\ell$ to the occurrences of \s{goto}s pointing to it.1046 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. 934 1047 Then the set $\s{multientry}_P$ of multientry loops of $P$ can be computed by 935 1048 $$ … … 938 1051 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}$}. 939 1052 940 Let $Id_k$ be the indexing of length $k$ made from identity simple expressions, i.e.\the sequence $i_0\mapsto id_0, \ldots , i_{k1}\mapsto id_{k1}$.1053 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}$. 941 1054 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: 942 1055 $$ … … 950 1063 \sop{if}b\sbin{then} \alpha\la Id_k \ra : \Ell^\iota_P(T_1,k) \sbin{else} \beta\la Id_k \ra : \Ell^\iota_P(T_2,k) 951 1064 \\&\text{if $S=\sop{if}b\sbin{then}T_1\sbin{else}T_2$,}\\[3pt] 1065 \ell:\alpha\la Id_k\ra : \Ell_P^\iota(T,k) & \text{if $S = \ell : T$,}\\[3pt] 952 1066 \ldots 953 1067 \end{array} … … 955 1069 $$ 956 1070 Here, as usual, $\alpha$ and $\beta$ are fresh cost labels, and other cases just keep making the recursive calls on the substatements. 957 The \emph{indexed labelling} of a program $P$ is then defined as $\alpha\la \ra : \Ell^\iota_P(P,0)$, i.e.\a further fresh unindexed cost label is added at the start, and we start from level $0$.1071 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$. 958 1072 959 1073 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. 960 1074 961 \subsection{Indexed labels and loop transformations} 1075 \subsection{Indexed labels and loop transformations}\label{ssec:looptrans} 962 1076 We define the \emph{reindexing} $I \circ (i_k\mapsto a*i_k+b)$ as an operator on indexings by setting: 963 1077 \begin{multline*} … … 973 1087 The attentive reader will notice that no assumptions are made on the labelling of the statements that are involved. 974 1088 In particular the transformation can be repeated and composed at will. 975 Also, note that after erasing all labelling information ( i.e.\indexed cost labels and loop indices) we recover exactly the same transformations presented in~\ref{sec:defimp}.1089 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}. 976 1090 977 1091 \paragraph{Indexed loop peeling} … … 980 1094 \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) 981 1095 $$ 982 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$. 1096 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. 983 1097 984 1098 \paragraph{Indexed loop unrolling} … … 1080 1194 1081 1195 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. 1082 We want to annotate the source code, so we need a way to express and compute the costs of cost labels, i.e.\group the costs of indexed labels to ones of their atoms.1196 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. 1083 1197 In order to do so we introduce \emph{dependent costs}. 1084 1198 Let us suppose that for the sole purpose of annotation, we have available in the language ternary expressions of the form … … 1122 1236 i_k = b & \text{if $a = 0$,}\\ 1123 1237 i_k \ge b & \text{if $a = 1$,}\\ 1124 i_k\bmod a = b \wedge i_k \ge b & \text{otherwise}.1238 i_k\bmod a = b' \wedge i_k \ge b & \text{otherwise, where $b' = b\bmod a$}. 1125 1239 \end{cases} 1126 1240 $$ 1127 1241 Now, suppose we are given a mapping $\kappa$ from indexed labels to natural numbers. 1128 1242 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. 1129 To that end we define an auxiliary function $\kappa^\alpha_L$, parameterized by atoms and words of simple expressions, and defined on \emph{sets} of $n$uples of simple expressions (with $n$ constant across each such set, i.e.\each set is made of words all with the same length).1243 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). 1130 1244 1131 1245 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.} … … 1177 1291 $$ 1178 1292 1293 \subsection{A detailed example}\label{ssec:detailedex} 1294 Take the program in \autoref{fig:example1}. Its initial labelling will be: 1295 $$\begin{array}{l} 1296 \alpha\la\ra : s\ass 0;\\ 1297 i\ass 0;\\ 1298 i_0:\sop{while}i<n\sbin{do}\\ 1299 \inde \beta\la i_0\ra : p\ass 1;\\ 1300 \inde j\ass 1;\\ 1301 \inde i_1:\sop{while}j \le i\sbin{do}\\ 1302 \inde \inde \gamma\la i_0, i_1\ra : p\ass j*p\\ 1303 \inde \inde j\ass j+1;\\ 1304 \inde \delta\la i_0\ra : s\ass s+p;\\ 1305 \inde i\ass i+1;\\ 1306 \epsilon\la\ra:\s{skip} 1307 \end{array} 1308 $$ 1309 (a single \s{skip} after the $\delta$ label has been suppressed, and we are using the identification 1310 between indexings and tuples of simple expressions explained in \autoref{ssec:depcosts}). 1311 Supposing for example, $n=3$ 1312 the trace of the program will be 1313 $$\alpha\la\ra\,\beta\la 0 \ra\, \delta\la 0\ra\,\beta\la 1\ra\,\gamma\la 1,0\ra\, 1314 \delta\la 1\ra\,\beta\la 2\ra\,\gamma\la 2,0\ra\,\gamma\la 2, 1\ra\,\delta\la 2\ra\, 1315 \epsilon\la\ra$$ 1316 Now let as apply the transformations of \autoref{fig:example1} with the additional 1317 information detailed in \autoref{ssec:looptrans}. The result is shown in 1318 \autoref{fig:example2}. 1319 \begin{figureplr} 1320 $$ 1321 \begin{array}{l} 1322 \mbox{\color{blue}\boldmath$\alpha\la\ra $}:s\ass 0;\\ 1323 i\ass 0;\\ 1324 \tikztargetm{a}{\s{if}}\ i<n\sbin{then}\\ 1325 \inde \mbox{\color{blue}\boldmath$\beta\la0\ra $}:p\ass 1;\\ 1326 \inde j\ass 1;\\ 1327 \inde i_1:\sop{while}j \le i\sbin{do}\\ 1328 \inde \inde \mbox{\color{blue}\boldmath$\gamma\la 0, i_1\ra $}:p\ass j*p\\ 1329 \inde \inde j\ass j+1;\\ 1330 \inde \mbox{\color{blue}\boldmath$\delta\la 0\ra $}: s\ass s+p;\\ 1331 \inde i\ass i+1;\\ 1332 \inde i_0:\tikztargetm{d}{\s{while}}\ i<n\sbin{do}\\ 1333 \inde \inde \mbox{\color{blue}\boldmath$\beta\la 2*i_0+1\ra $}:p\ass 1;\\ 1334 \inde \inde j\ass 1;\\ 1335 \inde \inde \tikztargetm{b}{\s{if}}\ j \le i\sbin{then}\\ 1336 \inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la 2*i_0+1, 0\ra $}:p\ass j*p\\ 1337 \inde \inde \inde j\ass j+1;\\ 1338 \inde \inde \inde \sop{if}j \le i\sbin{then}\\ 1339 \inde \inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la 2*i_0+1, 1\ra $}: p\ass j*p\\ 1340 \inde \inde \inde \inde j\ass j+1;\\ 1341 \inde \inde \inde \inde i_1:\s{while}\ j \le i\sbin{do}\\ 1342 \inde \inde \inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la 2*i_0+1, 2*i_1 + 2 \ra $}:p\ass j*p\\ 1343 \inde \inde \inde \inde \inde j\ass j+1;\\ 1344 \inde \inde \inde \inde \inde \sop{if}j \le i\sbin{then}\\ 1345 \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\\ 1346 \inde \inde \inde \inde \inde \inde \tikztargetm{c}j\ass j+1;\\ 1347 \inde \inde \mbox{\color{blue}\boldmath$\delta\la 2*i_0+1\ra$}: s\ass s+p;\\ 1348 \inde \inde i\ass i+1;\\ 1349 \inde \inde \sop{if}i<n\sbin{then}\\ 1350 \inde \inde \inde \mbox{\color{blue}\boldmath$\beta\la 2*i_0+2\ra $}:p\ass 1;\\ 1351 \inde \inde \inde j\ass 1;\\ 1352 \inde \inde \inde i_1:\tikztargetm{e}{\s{while}}\ j < i\sbin{do}\\ 1353 \inde \inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la 2*i_0+2, 2*i_1\ra$}: p\ass j*p\\ 1354 \inde \inde \inde \inde j\ass j+1;\\ 1355 \inde \inde \inde \inde \s{if}\ j < i\sbin{then}\\ 1356 \inde \inde \inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la2*i_0+2, 2*i_1+1\ra$}: p\ass j*p\\ 1357 \inde \inde \inde \inde \inde \tikztargetm{f}j\ass j+1;\\ 1358 \inde \inde \inde \mbox{\color{blue}\boldmath$\delta\la 2*i_0+2\ra $}: s\ass s+p;\\ 1359 \inde \inde \inde i\ass i+1\tikztargetm{g};{}\\ 1360 \mbox{\color{blue}\boldmath$\epsilon\la\ra $}:\s{skip} 1361 \end{array}$$ 1362 \caption{The result of applying reindexing loop transformations on the 1363 program in \autoref{fig:example1}.}\label{fig:example2} 1364 \end{figureplr} 1365 One can check that the transformed code leaves the same trace when executed. 1366 1367 Now let us compute the dependent cost of $\gamma$, supposing no other loop transformations 1368 are done. Ordering its indexings we 1369 have the following list: 1370 \begin{equation} 1371 \label{eq:inds} 1372 \begin{aligned} 1373 &0, i_1\\ 1374 &2*i_0+1, 0\\ 1375 &2*i_0+1, 1\\ 1376 &2*i_0+1, 2*i_1+2\\ 1377 &2*i_0+1, 2*i_1+3\\ 1378 &2*i_0+2, 2*i_1\\ 1379 &2*i_0+2, 2*i_1+1 1380 \end{aligned} 1381 \end{equation} 1382 1383 The resulting dependent cost will then be 1384 \def\indetern#1#2#3{\begin{tabular}[t]{nL}(#1)\mathrel ?{}\\\hskip 15pt #2:{}\\\hskip 15pt #3\end{tabular}} 1385 \def\tern#1#2#3{(#1)\mathrel ? #2:#3} 1386 \begin{equation}\label{eq:ex} 1387 \kappa^\iota(\gamma)= 1388 \indetern{i_0 = 0} 1389 {\tern{i_1\ge 0}a0} 1390 {\indetern{i_0\bmod 2 = 1 \wedge i_0\ge 1} 1391 {\indetern{i_1=0} 1392 b 1393 {\indetern{i_1 = 1} 1394 c 1395 {\indetern{i_1\bmod 2 = 0 \wedge i_1\ge 2} 1396 d 1397 {\tern{i_1\bmod 2 = 1 \wedge i_1\ge 3}e0} 1398 } 1399 } 1400 } 1401 {\indetern{i_0\bmod 2 = 0 \wedge i_0\ge 2} 1402 {\indetern{i_1 \bmod 2 = 0 \wedge i_1 \ge 0} 1403 f 1404 {\tern{i_1 \bmod 2 = 1 \wedge i_1 \ge 1}g0} 1405 } 1406 0 1407 } 1408 } 1409 \end{equation} 1410 We will see later on \autopageref{pag:continued} how such an expression can be simplified. 1179 1411 \section{Notes on the implementation and further work} 1180 1412 \label{sec:conc} … … 1235 1467 \verb+(_i_0 % 3 == 2)?+y\verb+:+x. 1236 1468 $$ 1237 1469 Picking up again the example depicted in \autoref{ssec:detailedex}, \label{pag:continued} 1470 we can see that the cost in \eqref{eq:ex} can be simplified to the following, 1471 using some of the transformation described above: 1472 $$ 1473 \kappa^\iota(\gamma)= 1474 \indetern{i_0 = 0} 1475 a 1476 {\indetern{i_0\bmod 2 = 1} 1477 {\indetern{i_1=0} 1478 b 1479 {\indetern{i_1 = 1} 1480 c 1481 {\indetern{i_1\bmod 2 = 0} 1482 de 1483 } 1484 } 1485 } 1486 {\indetern{i_1 \bmod 2 = 0} 1487 fg 1488 } 1489 } 1490 $$ 1491 One should keep in mind that the example was wilfully complicated, in practice 1492 the cost expressions produced have rarely more clauses 1493 than the number of nested loops containing the annotation. 1238 1494 \paragraph{Updates to the framaC cost plugin} 1239 1495 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.
Note: See TracChangeset
for help on using the changeset viewer.