Changeset 3119
 Timestamp:
 Apr 10, 2013, 7:15:06 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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