Changeset 1683


Ignore:
Timestamp:
Feb 9, 2012, 5:41:26 PM (6 years ago)
Author:
tranquil
Message:

abstract and running example

Location:
Deliverables/addenda/indexed_labels
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/addenda/indexed_labels/report.tex

    r1678 r1683  
    574574
    575575\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$};}}
    576589%<<<<<<<<<<<<
    577590\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.: FP7-ICT-2009-C-243881 \cerco{}\\
    620 %
    621 % \clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
    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
     607Report \\
     608Indexed Labels for Loop Iteration Dependent Costs
     609\\
     610\end{LARGE}
     611\end{center}
     612
     613\vspace*{2cm}
     614\begin{center}
     615\begin{large}
     616Version 0.1
     617\end{large}
     618\end{center}
     619
     620\vspace*{0.5cm}
     621\begin{center}
     622\begin{large}
     623Main Author:\\
     624Paolo Tranquilli
     625\end{large}
     626\end{center}
     627
     628\vspace*{\fill}
     629\noindent
     630Project Acronym: \cerco{}\\
     631Project full title: Certified Complexity\\
     632Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
     633
     634\clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
     635
     636\newpage
     637
     638\begin{abstract}
     639We present an extension to the labelling approach to lift resource
     640consumption information from compiled to source code~\cite{D2.1}. Cost labels
     641inserted at key points of the source code and kept track of during compilation
     642allow such a task. However, this approach is looses preciseness when differences
     643arise as to the cost of the same portion of code, whether due to code
     644transformation such as loop optimisation or advanced architecture features
     645(\eg cache). Our approach addresses this weakness as to some loop transformations
     646that rearrange the iterations of a loop (namely loop peeling and unrolling). It
     647consists in formally indexing cost labels with which iteration of the containing
     648loop they occur in, relative to the source code. This indexes can be transformed
     649during the compilation, and when lifted back to source code they produce dependent
     650costs.
     651
     652The proposed changes have been implemented in CerCo's untrusted prototype compiler
     653from a large fragment of C to 8051 assembly~\cite{D2.2}.
     654\end{abstract}
     655
    624656
    625657\listoftodos
     
    670702
    671703We 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}).
     704For 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}).
    673705
    674706\paragraph{Loop peeling}
     
    768800We may omit the \s{else} clause of a conditional if it leads to a \s{skip} statement.
    769801
    770 We will presuppose that all programs are \emph{well-labelled}, 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.
     802We will presuppose that all programs are \emph{well-labelled}, \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.
    771803The \s{find} helper function has the task of not only finding the labelled statement in the program, but also building the correct continuation.
    772804The continuation built by \s{find} replaces the current continuation in the case of a jump.
     
    780812Many loop optimisations do not preserve the semantics of multi-entry loops in general, or are otherwise rendered ineffective.
    781813Usually compilers implement a single-entry loop detection which avoids the multi-entry 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.
     814The loop transformations we present are local, \ie they target a single loop and transform it.
    783815Which loops are targeted may be decided by some \emph{ad hoc} heuristic.
    784816However, the precise details of which loops are targetted and how is not important here.
     
    801833$$
    802834where $\ell^j_i$ are again fresh labels for any $\ell_i$ labelling a statement in $S$.
    803 This is a willfully na\"{i}ve version of loop unrolling, which usually targets less general loops.
     835This is a wilfully na\"{i}ve version of loop unrolling, which usually targets less general loops.
    804836The problem this transformation poses to CerCo's labelling approach are independent of the sophistication of the actual transformation.
     837
     838\begin{example}
     839In \autoref{fig:example1} we show a program (a wilfully inefficient computation of of the
     840sum of the first $n$ factorials) and a possible transformation of it, combining loop
     841peeling and loop unrolling.
     842\begin{figureplr}
     843$$
     844\fbox{$\begin{array}{l}
     845s\ass 0;\\
     846i\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}
     859s\ass 0;\\
     860i\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,
     900brace/.style = {decorate, decoration={brace, amplitude = 15pt}},
     901label/.style = {sloped, anchor = base, yshift = 17pt, font = \large}]
     902\draw [brace, transform canvas={xshift=5pt}] (b.north-|right) -- node[label]{peeled} (c.south-|right);
     903\draw [brace, transform canvas={xshift=30pt}] (b.north-|right) -- node[label]{unrolled} (c.south-|right);
     904\draw [brace, transform canvas={xshift=5pt}] (e.north-|right) -- node[label]{unrolled} (f.south-|right);
     905\draw [brace, transform canvas={xshift=55pt}] (d.north-|right) -- node[label]{unrolled} (g.south-|right);
     906\draw [brace, transform canvas={xshift=80pt}] (a.north-|right) -- node[label]{peeled} (g.south-|right);
     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
     911blocks by indentation.}
     912\label{fig:example1}
     913\end{figureplr}
     914\end{example}
    805915
    806916\section{Labelling: a quick sketch of the previous approach}
     
    813923For further details we refer to~\cite{D2.1}.
    814924
    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.
     925With labels the small step semantics turns into a labelled transition system along with a natural notion of trace (\ie lists of labels) arises.
    816926The evaluation of statements is enriched with traces, so that rules follow a pattern similar to the following:
    817927$$
     
    826936
    827937\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.
     938Given 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,
     939which is a conservative approach to ensuring that all loops have labels inside them, as a loop might be done with \s{goto}s.
    829940The relevant cases are
    830941$$\begin{aligned}
     
    832943    \sop{if}e\sbin{then}\alpha:\Ell(S)\sbin{else}\beta:\Ell(T)\\
    833944  \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))
    835948  \end{aligned}$$
    836949where $\alpha,\beta$ are fresh cost labels.
     
    879992$$
    880993What 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).
     994If 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).
    882995
    883996\section{Indexed labels}
     
    9311044We sketch how this can be computed in the sequel.
    9321045
    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.
     1046A 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.
    9341047Then the set $\s{multientry}_P$ of multi-entry loops of $P$ can be computed by
    9351048$$
     
    9381051Here $\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}$}.
    9391052
    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_{k-1}\mapsto id_{k-1}$.
     1053Let $Id_k$ be the indexing of length $k$ made from identity simple expressions, \ie the sequence $i_0\mapsto id_0, \ldots , i_{k-1}\mapsto id_{k-1}$.
    9411054We 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:
    9421055$$
     
    9501063\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)
    9511064\\&\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]
    9521066\ldots
    9531067\end{array}
     
    9551069$$
    9561070Here, 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$.
     1071The \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$.
    9581072
    9591073In plainer words: each single-entry loop is indexed by $i_k$ where $k$ is the number of other single-entry loops containing this one, and all cost labels under the scope of a single-entry loop indexed by $i_k$ are indexed by all indices $i_0,\ldots,i_k$, without any transformation.
    9601074
    961 \subsection{Indexed labels and loop transformations}
     1075\subsection{Indexed labels and loop transformations}\label{ssec:looptrans}
    9621076We define the \emph{reindexing} $I \circ (i_k\mapsto a*i_k+b)$ as an operator on indexings by setting:
    9631077\begin{multline*}
     
    9731087The attentive reader will notice that no assumptions are made on the labelling of the statements that are involved.
    9741088In 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}.
     1089Also, 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}.
    9761090
    9771091\paragraph{Indexed loop peeling}
     
    9801094\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)
    9811095$$
    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$.
     1096As 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.
    9831097
    9841098\paragraph{Indexed loop unrolling}
     
    10801194
    10811195Having 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.
     1196We 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.
    10831197In order to do so we introduce \emph{dependent costs}.
    10841198Let us suppose that for the sole purpose of annotation, we have available in the language ternary expressions of the form
     
    11221236i_k = b & \text{if $a = 0$,}\\
    11231237i_k \ge b & \text{if $a = 1$,}\\
    1124 i_k\bmod a = b \wedge i_k \ge b & \text{otherwise}.
     1238i_k\bmod a = b' \wedge i_k \ge b & \text{otherwise, where $b' = b\bmod a$}.
    11251239\end{cases}
    11261240$$
    11271241Now, suppose we are given a mapping $\kappa$ from indexed labels to natural numbers.
    11281242We 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).
     1243To 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).
    11301244
    11311245We 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.}
     
    11771291$$
    11781292
     1293\subsection{A detailed example}\label{ssec:detailedex}
     1294Take the program in \autoref{fig:example1}. Its initial labelling will be:
     1295$$\begin{array}{l}
     1296\alpha\la\ra : s\ass 0;\\
     1297i\ass 0;\\
     1298i_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
     1310between indexings and tuples of simple expressions explained in \autoref{ssec:depcosts}).
     1311Supposing for example, $n=3$
     1312the 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$$
     1316Now let as apply the transformations of \autoref{fig:example1} with the additional
     1317information 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;\\
     1323i\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
     1363program in \autoref{fig:example1}.}\label{fig:example2}
     1364\end{figureplr}
     1365One can check that the transformed code leaves the same trace when executed.
     1366
     1367Now let us compute the dependent cost of $\gamma$, supposing no other loop transformations
     1368are done. Ordering its indexings we
     1369have 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
     1383The 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}
     1410We will see later on \autopageref{pag:continued} how such an expression can be simplified.
    11791411\section{Notes on the implementation and further work}
    11801412\label{sec:conc}
     
    12351467\verb+(_i_0 % 3 == 2)?+y\verb+:+x.
    12361468$$
    1237 
     1469Picking up again the example depicted in \autoref{ssec:detailedex}, \label{pag:continued}
     1470we can see that the cost in \eqref{eq:ex} can be simplified to the following,
     1471using 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$$
     1491One should keep in mind that the example was wilfully complicated, in practice
     1492the cost expressions produced have rarely more clauses
     1493than the number of nested loops containing the annotation.
    12381494\paragraph{Updates to the frama-C cost plugin}
    12391495Cerco's frama-C~\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.