Changeset 3119 for Deliverables/D6.3

Timestamp:

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

Author:

sacerdot

Message:

...

File:

• Deliverables/D6.3/report.tex (modified) (2 diffs)

Deliverables/D6.3/report.tex

@@ -363 +363 @@
 
 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.
 
@@ -441 +441 @@
 \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}