Changeset 3119

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


1 edited


  • Deliverables/D6.3/report.tex

    r3117 r3119  
    364364A \emph{view} over internal states is a pair $(\mathcal{V},|.|)$ where
    365 $\mathcal{V}$ is a non empty set and $|.|:\Delta \to \mathcal{V}$ is
     365$\mathcal{V}$ is a finite non empty set and $|.|:\Delta \to \mathcal{V}$ is
    366366a forgetful function over internal states.
    441441\paragraph{The labelling appraoch for data independent cost models}
    442442We now describe how the labelling approach can be slightly modified to deal
    443 with data independent cost models.
     443with a data independent cost model $(\hookrightarrow,K)$ built over
     446In the labelling approach, every basic block in the object code is identified
     447with a unique label $L$ which is also associated to the corresponding
     448basic block in the source level. Let us assume that labels are also inserted
     449after every function call and that this property is preserved during
     450compilation. Adding labels after calls makes the instrumented code heavier
     451to read and it generates more proof obligations on the instrumented code, but
     452it does not create any additional problems. The preservation during compilation
     453creates some significant technical complications in the proof of correctness
     454of the compiler, but those can be solved.
     456The static analysis performed in the last step of the basic labelling approach
     457analyses the object code in order to assign a cost to every label or,
     458equivalently, to every basic block. The cost is simply the sum of the cost
     459of very instruction in the basic block.
     461In our scenario, instructions no longer have a cost, because the cost function
     462$K$ takes in input a program counter but also a view $v$. Therefore we
     463replace the static analysis with the computation, for every basic block and
     464every $v \in \mathcal{V}$, of the sum of the costs of the instructions in the
     465block, starting in the initial view $v$. Formally, let the sequence of the
     466program counters of the basic block form the execution path $pc_0,\ldots,pc_n$.
     467The cost $K(v_0,L)$ associated to the block labelled with
     468$L$ and the initial view $v_0$ is
     469$K(pc_0,v_0) + K(pc_1,v_1) + \ldots + K(pc_n,v_n)$ where for every $i$,
     470$(pc_i,v_i) \hookrightarrow v_{k+1}$. The static analysis can be performed
     471in linear time in the size of the program because the cardinality of the sets
     472of labels (i.e. the number of basic blocks) is bounded by the size of the
     473program and because the set $V$ is finite. In the case of the pipelines of
     474the previous paragraph, the static analysis is $2^n$ times more expensive
     475than the one of the basic labelling approach, where $n$ is the number of
     476pipeline stages.
     478The first imporant theorem in the labelling approach is the correctness of the
     479static analysis: if the (dependent) cost associated to a label $L$ is $k$,
     480then executing a program from the beginning of the basic block to the end
     481of the basic block should take exactly $k$ cost units. The proof only relies
     482on associativity and commutativity of the composition of costs. Commutativity
     483is only required if basic blocks can be nested, i.e. if a basic block does not
     484terminate when it reaches a call, but it continues after the called function
     485returns. By assuming to have a cost label after each block, we do not need
     486commutativity any longer, which does not hold for the definition of $K$ we
     487just gave. The reason is that, if $pc_i$ is a function call executed in
     488the view (state) $v_i$, it is not true that, after return, the state
     489will be $v_i+1$ defined by $(pc_i,v_i) \hookrightarrow v_{i+1}$. Indeed
     490$v_{i+1}$ will be the state at the execution of the body of the call, while
     491we should know the state after the function returns. The latter cannot be
     492statically predicted. That's why we had to impose labels after calls.
     493Associativity, on the other hand, trivially holds. Therefore the proof
     494of correctness of the static analysis can be reused without any change.
     496So 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.
     497The second step consists in statically computing the transition function
     498$\hookrightarrow : \mathcal{L} \times \mathcal{V} \to \mathcal{V}$ that
     499associates to each basic block and input view the view obtained at the end
     500of the execution of the block. The definition is straightforward:
     501$(L,v) \hookrightarrow v'$ iff $((pc_0,\ldots,pc_n),v) \hookrightarrow v'$
     502where $(pc_0,\ldots,pc_n)$ are the program counters of the block labelled by
     503$L$. This transition function is not necessary in the basic labelling approach.
     504Its computation is again linear in the size of the program.
     506Both the versions of $K$ and $\hookrightarrow$ defined over labels can be
     507lifted to work over traces by folding them over the list of labels in the
     508trace: $K((L_1,\ldots,L_n),v) = K(L_1,v) + K((L_2,\ldots,L_n),v')$ where
     509$(L_1,v) \hookrightarrow v'$ and
     510$((L_1,\ldots,L_n),v) \hookrightarrow v''$ iff $(L_1,v) \hookrightarrow v'$ and
     511$((L_2,\ldots,L_n),v') \hookrightarrow v''$. The two definitions are also
     512clearly associative.
     514The second main theorem of the labelling approach is trace preservation:
     515the trace produced by the object code is the same as the trace produced by
     516the source code. Without any need to change the proof, we immediately obtain
     517as a corollary that for every view $v$, the cost $K(\tau,v)$ computed from
     518the source code trace $\tau$ is the same than the cost $K(\tau,v)$ computed
     519on the object code trace, which is again $\tau$.
     521The final step of the labelling approach is source code instrumentation.
     522In the basic labelling approach it consists in adding a global variable
     523\texttt{\_\_cost}, initialized with 0, which is incremented at the beginning
     524of every basic block with the cost of the label of the basic block.
     525Here we just need a more complex instrumentation that keeps track of the
     526values of the views during execution:
     528 \item We define two global variables \texttt{\_\_cost}, initialized at 0,
     529   and \texttt{\_\_view}, initialized with $|\delta_0|$ where $\delta_0$ is
     530   the initial value of the internal state at the beginning of program
     531   execution.
     532 \item At the beginning of every basic block labelled by $L$ we add
     533  \texttt{\_\_cost += }$K(\mbox{\texttt{\_\_view}},L)$\texttt{;} which pre-pays the cost for the
     534  execution of the block in the current view (state) \texttt{\_\_view}.
     535 \item At every exit point from the basic block we add
     536  \texttt{\_\_view = }$v$ where
Note: See TracChangeset for help on using the changeset viewer.