# Changeset 3119 for Deliverables

Ignore:
Timestamp:
Apr 10, 2013, 7:15:06 PM (8 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r3117 A \emph{view} over internal states is a pair $(\mathcal{V},|.|)$ where $\mathcal{V}$ is a non empty set and $|.|:\Delta \to \mathcal{V}$ is $\mathcal{V}$ is a finite non empty set and $|.|:\Delta \to \mathcal{V}$ is a forgetful function over internal states. \paragraph{The labelling appraoch for data independent cost models} We now describe how the labelling approach can be slightly modified to deal with data independent cost models. with a data independent cost model $(\hookrightarrow,K)$ built over $(\mathcal{V},|.|)$. In the labelling approach, every basic block in the object code is identified with a unique label $L$ which is also associated to the corresponding basic block in the source level. Let us assume that labels are also inserted after every function call and that this property is preserved during compilation. Adding labels after calls makes the instrumented code heavier to read and it generates more proof obligations on the instrumented code, but it does not create any additional problems. The preservation during compilation creates some significant technical complications in the proof of correctness of the compiler, but those can be solved. The static analysis performed in the last step of the basic labelling approach analyses the object code in order to assign a cost to every label or, equivalently, to every basic block. The cost is simply the sum of the cost of very instruction in the basic block. In our scenario, instructions no longer have a cost, because the cost function $K$ takes in input a program counter but also a view $v$. Therefore we replace the static analysis with the computation, for every basic block and every $v \in \mathcal{V}$, of the sum of the costs of the instructions in the block, starting in the initial view $v$. Formally, let the sequence of the program counters of the basic block form the execution path $pc_0,\ldots,pc_n$. The cost $K(v_0,L)$ associated to the block labelled with $L$ and the initial view $v_0$ is $K(pc_0,v_0) + K(pc_1,v_1) + \ldots + K(pc_n,v_n)$ where for every $i$, $(pc_i,v_i) \hookrightarrow v_{k+1}$. The static analysis can be performed in linear time in the size of the program because the cardinality of the sets of labels (i.e. the number of basic blocks) is bounded by the size of the program and because the set $V$ is finite. In the case of the pipelines of the previous paragraph, the static analysis is $2^n$ times more expensive than the one of the basic labelling approach, where $n$ is the number of pipeline stages. The first imporant theorem in the labelling approach is the correctness of the static analysis: if the (dependent) cost associated to a label $L$ is $k$, then executing a program from the beginning of the basic block to the end of the basic block should take exactly $k$ cost units. The proof only relies on associativity and commutativity of the composition of costs. Commutativity is only required if basic blocks can be nested, i.e. if a basic block does not terminate when it reaches a call, but it continues after the called function returns. By assuming to have a cost label after each block, we do not need commutativity any longer, which does not hold for the definition of $K$ we just gave. The reason is that, if $pc_i$ is a function call executed in the view (state) $v_i$, it is not true that, after return, the state will be $v_i+1$ defined by $(pc_i,v_i) \hookrightarrow v_{i+1}$. Indeed $v_{i+1}$ will be the state at the execution of the body of the call, while we should know the state after the function returns. The latter cannot be statically predicted. That's why we had to impose labels after calls. Associativity, on the other hand, trivially holds. Therefore the proof of correctness of the static analysis can be reused without any change. So far, we have computed the dependent cost $K: \mathcal{V} \times \mathcal{L} \to \mathbb{N}$ that associates a cost to basic blocks and views. The second step consists in statically computing the transition function $\hookrightarrow : \mathcal{L} \times \mathcal{V} \to \mathcal{V}$ that associates to each basic block and input view the view obtained at the end of the execution of the block. The definition is straightforward: $(L,v) \hookrightarrow v'$ iff $((pc_0,\ldots,pc_n),v) \hookrightarrow v'$ where $(pc_0,\ldots,pc_n)$ are the program counters of the block labelled by $L$. This transition function is not necessary in the basic labelling approach. Its computation is again linear in the size of the program. Both the versions of $K$ and $\hookrightarrow$ defined over labels can be lifted to work over traces by folding them over the list of labels in the trace: $K((L_1,\ldots,L_n),v) = K(L_1,v) + K((L_2,\ldots,L_n),v')$ where $(L_1,v) \hookrightarrow v'$ and $((L_1,\ldots,L_n),v) \hookrightarrow v''$ iff $(L_1,v) \hookrightarrow v'$ and $((L_2,\ldots,L_n),v') \hookrightarrow v''$. The two definitions are also clearly associative. The second main theorem of the labelling approach is trace preservation: the trace produced by the object code is the same as the trace produced by the source code. Without any need to change the proof, we immediately obtain as a corollary that for every view $v$, the cost $K(\tau,v)$ computed from the source code trace $\tau$ is the same than the cost $K(\tau,v)$ computed on the object code trace, which is again $\tau$. The final step of the labelling approach is source code instrumentation. In the basic labelling approach it consists in adding a global variable \texttt{\_\_cost}, initialized with 0, which is incremented at the beginning of every basic block with the cost of the label of the basic block. Here we just need a more complex instrumentation that keeps track of the values of the views during execution: \begin{itemize} \item We define two global variables \texttt{\_\_cost}, initialized at 0, and \texttt{\_\_view}, initialized with $|\delta_0|$ where $\delta_0$ is the initial value of the internal state at the beginning of program execution. \item At the beginning of every basic block labelled by $L$ we add \texttt{\_\_cost += }$K(\mbox{\texttt{\_\_view}},L)$\texttt{;} which pre-pays the cost for the execution of the block in the current view (state) \texttt{\_\_view}. \item At every exit point from the basic block we add \texttt{\_\_view = }$v$ where \end{itemize} \end{document}