Changeset 3478 for LTS/DICE2014
 Timestamp:
 Sep 22, 2014, 4:50:21 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/DICE2014/slides.tex
r3467 r3478 21 21 ]{powerdot} 22 22 %\documentclass[mode=handout,nopagebreaks,paper=a4paper]{powerdot} 23 23 \usepackage{multirow} 24 24 %\usepackage[latin1]{inputenc} 25 25 \usepackage{pstricks,pstnode,psttext,psttree} … … 217 217 $\;$\\[9mm] 218 218 \begin{center} 219 \includegraphics[width= 7cm]{cerco.eps}219 \includegraphics[width=6cm]{cerco.eps} 220 220 \end{center} 221 221 This talk: … … 223 223 \begin{minipage}{12cm} 224 224 \begin{itemize} 225 \item There are some hidden assumption and limitations of labelling approach: {\red instructions with multiple predecessors} and {\redfunction calls}.226 \item We present a {\red revisitation of labelling approach} able to cope the above mentioned limitations.227 \item All the presented results have beenformalized in the {\red Matita proof assistant}.225 \item We revise the labelling approach to lift some restriction: {\red instructions having only one predecessor} and {\red absence of function calls}. 226 \item We replace simple status independent costs with arbitrary semantics domains used in {\red abstract interpretation} to analyze caches, pipelines,$\ldots$. 227 \item All the presented results are formalized in the {\red Matita proof assistant}. 228 228 \end{itemize} 229 229 \end{minipage} … … 279 279 \item No more label emission statements. 280 280 \end{itemize} 281 \begin{lstlisting}[language=Grafite] 282 record abstract_status : Type[2] ≝ 283 { as_status :> Type[0] 284 ; as_execute : ActionLabel → relation as_status 285 ; as_syntactical_succ : relation as_status 286 ; as_classify : as_status → status_class 287 ; as_initial : as_status → bool 288 ; as_final : as_status → bool 289 ; jump_emits : ∀s1,s2,l.as_classify ... s1 = cl_jump → 290 as_execute l s1 s2 → is_non_silent_cost_act l 291 }. 292 \end{lstlisting} 281 \begin{center} 282 \begin{tabular}{ll l} 283 \begin{lstlisting} 284 swith(E){ 285 case e1 : 286 Emit L1; 287 I1; 288 case e2 : 289 Emit L2; 290 I2; 291 } 292 \end{lstlisting} &$\qquad$& 293 \begin{lstlisting} 294 swith(E){ 295 case e1,L1 : 296 297 I1; 298 case L3,e2,L2 : //L3 emitted coming 299 // from case e1 300 I2; 301 } 302 \end{lstlisting} 303 \end{tabular} 304 \end{center} 305 % \begin{lstlisting}[language=Grafite] 306 % record abstract_status : Type[2] ≝ 307 % { as_status :> Type[0] 308 % ; as_execute : ActionLabel → relation as_status 309 % ; as_syntactical_succ : relation as_status 310 % ; as_classify : as_status → status_class 311 % ; as_initial : as_status → bool 312 % ; as_final : as_status → bool 313 % ; jump_emits : ∀s1,s2,l.as_classify ... s1 = cl_jump → 314 % as_execute l s1 s2 → is_non_silent_cost_act l 315 % }. 316 % \end{lstlisting} 293 317 \end{wideslide} 294 318 … … 338 362 \end{minipage} 339 363 }\\[3mm] 364 \onslide{2}{ 340 365 {\red Assumptions:} 341 366 \begin{itemize} 342 \item All the instruction in the (static) block are reached during computation. 343 \item The cost function should be commutative. 344 \end{itemize} 367 \item<2> All the instruction in the (static) block are reached during computation. 368 \item<2> The cost function should be commutative. 369 \end{itemize} 370 } 371 \onslide{3}{ 345 372 {\red Problems:} 346 373 \begin{itemize} 347 \item It does not work with {\blue noncommutative cost functions}. Because of stateful hardware components (cache, pipelines ...) this method does not scale to {\blue modern hardware}. 348 \item It does not work with {\blue compiler that do not respect the calling structure} of the source code because it is not possible to statically predict {\blue which instruction will be executed after a function return}. 349 \end{itemize} 350 \end{wideslide} 351 352 \begin{wideslide}[method=direct]{First solution: structured traces} 374 \item<3> It does not work with {\blue noncommutative cost functions}. Because of stateful hardware components (cache, pipelines ...) this method does not scale to {\blue modern hardware}. 375 \item<3> It does not work with {\blue compiler that do not respect the calling structure} of the source code because it is not possible to statically predict {\blue which instruction will be executed after a function return}. 376 \end{itemize}} 377 \end{wideslide} 378 379 \begin{wideslide}{First solution: structured traces} 380 \onslide*{1}{ 353 381 \begin{itemize} 354 382 \item The usual notion of {\red flat execution trace} is inadequate for a simulation argument. … … 356 384 \item Traces of called function are {\red nested}, invariants on position of costlabels are {\red enforced} and steps are grouped {\red according to costlabels}. 357 385 \end{itemize} 358 \begin{center} 359 \includegraphics[width=8cm]{trace.eps} 360 \end{center} 361 \end{wideslide} 362 363 \begin{wideslide}[method=direct]{Measurable traces} 364 $\;$\\[7mm] 365 \begin{lstlisting}[language=Grafite] 366 inductive pre_measurable_trace (S : abstract_status) : 367 ∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝ 368  pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base… st) 369  pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel. 370 ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. 371 as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl → 372 pre_measurable_trace … (t_ind … prf … tl) 373 ……… 374  pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2. 375 ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3. 376 ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4. 377 as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io 378 → is_call_act l1 → ¬ is_call_post_label … st1 → 379 pre_measurable_trace … t1 → pre_measurable_trace … t2 → 380 as_syntactical_succ S st1 st4 → 381 is_unlabelled_ret_act l2 → 382 pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))). 383 \end{lstlisting} 384 \end{wideslide} 385 386 \begin{wideslide}[method=direct]{Simulation statement} 386 } 387 \onslide*{2}{ 388 \begin{tabular}{l c} 389 \onslide*{3,4,5}{\green}$\tt EMIT \; L_1$ & \onslide*{2,3,4}{{\red Flat trace}} \onslide*{5}{{\red Structured trace}}\\ 390 \onslide*{3,4,5}{\green}$\tt I_1$ & \multirow{7}{*}{ 391 \onslide*{2,3,4}{ 392 \xymatrix{ \onslide*{3,4}{\green} \bullet \onslide*{1,2}{\ar[r]^{{\tt L_1}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green L_1}}} & \onslide*{3,4}{\green} \bullet \onslide*{1,2}{\ar[r]^{{\tt I_1}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green I_1}}} & \onslide*{3,4}{\green} \ldots \onslide*{1,2}{\ar[r]^{{\tt I_n}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green I_n}}} & \onslide*{3,4}{\green} \bullet \onslide*{1,2}{\ar[r]^{{\tt CALL}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green CALL}}} & \bullet \ar[r]^{{\tt J_1}} & \ldots \ar[r]^{{\tt RET}} & \onslide*{3,4}{\green} \bullet \onslide*{1,2}{\ar[r]^{{\tt I_{n+1}}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green I_{n+1}}}} & \onslide*{3,4}{\green} \ldots \onslide*{1,2}{\ar[r]^{{\tt I_m}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green I_m}}} & \onslide*{3,4}{\green} \bullet } 393 } 394 \onslide*{5}{ 395 \xymatrix{ & & & \bullet \ar[r]^{{\tt J_1}} & \black \ldots \ar[r] & \bullet \ar[d]^{{\tt RET}}\\ 396 \green \bullet \ar@[green][r]^{{\tt \green L_1}} & \green \bullet \ar@[green][r]^{{\tt \green I_1}} & \green \ldots \ar@[green][r]^{{\tt \green I_n}} & \green \bullet \ar@[green][u]^{{\tt \green CALL}} & \triangleright & \green \bullet \ar@[green][r]^{{\tt \green I_{n+1}}} & \green \ldots \ar@[green][r]^{{\tt \green I_m}} & \green \bullet } 397 } 398 }\\ 399 \onslide*{3,4,5}{\green}$\vdots$ & \\ 400 \onslide*{3,4,5}{\green}$\tt I_n$ & \\ 401 \onslide*{3,4,5}{\green}$\tt CALL$ & \\ 402 \onslide*{3,4,5}{\green}$\tt I_{n+1}$ & \\ 403 \onslide*{3,4,5}{\green}$\vdots$ & \\ 404 \onslide*{3,4,5}{\green}$\tt I_m$ 405 \end{tabular} 406 } 407 $\;$\\[3mm] 408 \onslide*{4}{{\red What is the global invariant granting both that call/return are balanced and that we can statically predict the return address?}} 409 410 % \onslide*{2}{ 411 % \xymatrix{a & b \\ 412 % c & d} 413 % } 414 \end{wideslide} 415 416 % \begin{wideslide}[method=direct]{Measurable traces} 417 % $\;$\\[7mm] 418 % \begin{lstlisting}[language=Grafite] 419 % inductive pre_measurable_trace (S : abstract_status) : 420 % ∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝ 421 %  pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base… st) 422 %  pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel. 423 % ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. 424 % as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl → 425 % pre_measurable_trace … (t_ind … prf … tl) 426 % ……… 427 %  pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2. 428 % ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3. 429 % ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4. 430 % as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io 431 % → is_call_act l1 → ¬ is_call_post_label … st1 → 432 % pre_measurable_trace … t1 → pre_measurable_trace … t2 → 433 % as_syntactical_succ S st1 st4 → 434 % is_unlabelled_ret_act l2 → 435 % pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))). 436 % \end{lstlisting} 437 % \end{wideslide} 438 439 \begin{wideslide}[method=file]{Simulation statement} 387 440 $\;$\\[7mm] 388 441 \begin{lstlisting}[language=Grafite] … … 392 445 \end{lstlisting} 393 446 \begin{itemize} 394 \item Simulation conditions are local conditions for {\red sequential}, {\red conditional}, {\red call} and {\red return} steps. 395 \begin{center} 447 \item<2> Simulation conditions are local conditions for {\red sequential}, {\red conditional}, {\red call} and {\red return} steps. 448 \begin{center} 449 \onslide*{2}{ 450 \xymatrix{st1 \ar[rr] \ar@{.}[d]{sim} & & st1' \ar@{.}[d]{sim} \\ 451 st2 \ar[rr]^{*} & & st2'}} 452 \onslide*{3}{ 396 453 \includegraphics[width=5cm]{diag.eps} 397 \end{center} 398 \item The generated trace should contain {\red the same sequence of costlabels} (up to permutation) of the starting one. 454 } 455 \end{center} 456 \item<4> The generated trace should contain {\red the same sequence of costlabels} (up to permutation) of the starting one. 399 457 \end{itemize} 400 458 \end{wideslide} … … 409 467 still requirred to be commutative. 410 468 \end{itemize} 469 \onslide{2}{ 411 470 \psshadowbox{ 412 471 \begin{minipage}{12cm} 413 472 We ask every function call to be immediately followed by a label emission statement so the scope of a label no longer extends after a function call. 414 473 \end{minipage} 415 } 474 }} 416 475 $\;$\\ 476 \onslide{3}{ 417 477 {\red Drawbacks} 418 478 \begin{itemize} 419 \item A lot of labels should be injected in the code! 420 \item The value of the variable $\tt cost$ at the end of a block containing functioncalls is the sum of the increments that occurs after every call. 421 \item A proof of termination is requirred! 422 \end{itemize} 423 \end{wideslide} 424 425 \begin{wideslide}[method=direct]{Return post label pass} 426 We define a {\blue sound and precise} translation to a program having all return instructions that are followed by a label emission. 427 \begin{lstlisting}[language=Grafite] 428 lemma correctness : ∀p,p',prog.no_duplicates_labels … prog → let 〈t_prog,m,keep〉 ≝ trans_prog … prog in ∀s1,s2,s1' : state p.∀abs_top,abs_tail. 429 ∀t : raw_trace (operational_semantics…p' prog) s1 s2.pre_measurable_trace…t → state_rel…m keep abs_top abs_tail s1 s1' → ∃abs_top',abs_tail'.∃s2'. 430 ∃t' : raw_trace (operational_semantics…p' t_prog) s1' s2'. 431 state_rel…m keep abs_top' abs_tail' s2 s2' ∧ is_permutation … ∧ len…t = len…t' ∧ pre_measurable_trace…t'. 432 \end{lstlisting} 433 \begin{itemize} 434 \item {\blue Benefits}: the user can reason with smaller blocks and simpler costs and the compiler do not need to care about extra invariant. 435 \item {\red Drawbacks}: This pass is not always possible in case of non commutative costs. 436 \end{itemize} 437 \end{wideslide} 438 439 \begin{wideslide}[method=direct]{Static/dynamic correctness} 440 \begin{lstlisting}[language=Grafite] 441 lemma static_dynamic : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog. 442 ∀abs_t : abstract_transition_sys (m…p').∀instr_m. 443 ∀good : static_galois…(asm_static_analisys_data p p' prog abs_t instr_m). 444 ∀mT,map1.∀EQmap : static_analisys p ? instr_m mT prog = return map1. 445 ∀st1,st2 : vm_state p p'. 446 ∀ter : terminated_trace (asm_operational_semantics p p' prog) st2. 447 ∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2. 448 ∀k.pre_measurable_trace…t → 449 block_cost p prog…instr_m (pc…st1) (S ((instructions…prog))) = return k → 450 ∀a1.rel_galois…good st1 a1 → 451 let stop_state ≝ match R_post_step…ter with [None ⇒ st2  Some x ⇒ \snd x ] in 452 ∀costs.costs = dependent_map CostLabel ? (get_costlabels_of_trace…t) 453 (λlbl,prf.(opt_safe…(get_map…map1 lbl) ?)) → 454 rel_galois…good stop_state (act_abs…abs_t (big_op…costs) (act_abs…abs_t k a1)). 455 \end{lstlisting} 456 \end{wideslide} 479 \item<3> A lot of labels should be injected in the code! 480 \item<3> The value of the variable $\tt cost$ at the end of a block containing functioncalls is the sum of the increments that occurs after every call. 481 \item<3> A proof of termination is requirred! 482 \end{itemize}} 483 \end{wideslide} 484 485 \begin{wideslide}{Return post label pass} 486 At the level of source code, we define a {\blue sound and precise} translation to a program having all return instructions that are followed by a label emission. \\[4mm] 487 \begin{tabular}{l c l} 488 \onslide*{1,2,3}{$\tt EMIT \; L;$}\onslide*{4}{$\tt cost += k_1 + k_2;$} & \multirow{7}{6cm}{\centering $\Rightarrow$} & \onslide*{2}{$\red \tt EMIT \; L1$}\onslide*{3}{$\tt cost+=k_1;$} \\ 489 $\tt I_1;$ & & \onslide{2}{$\tt I_1;$} \\ 490 $\vdots$ & & \onslide{2}{$\vdots$} \\ 491 $\tt f();$ & & \onslide{2}{$\tt f();$} \\ 492 $\tt I_2;$ & & \onslide*{2}{{\red $\tt EMIT \; L2;$}}\onslide*{3}{$\tt cost+=k_2$;} \\ 493 $\vdots$ & & \onslide{2}{$\tt I_2;$} \\ 494 $\tt I_n;$ & & \onslide{2}{$\vdots$} \\ 495 & & \onslide{2}{$\tt I_n$} 496 \end{tabular} 497 \end{wideslide} 498 499 500 \begin{wideslide}{Return post label pass} 501 \begin{itemize} 502 \item<1> {\blue Benefits}: the user can reason with smaller blocks and simpler costs and the compiler do not need to care about extra invariant. 503 \item<1> {\red Drawbacks}: This pass is not always possible in case of non commutative costs. 504 \end{itemize} 505 To prove correctness it is necessary to define a state relation (being preserved during the translation) keeping track of the fresh labels created.\\[3mm] 506 \onslide*{2}{ 507 \begin{center} 508 \psshadowbox{ 509 \begin{minipage}{6cm} 510 {\red \centering About 3000 lines of Matita code!} 511 \end{minipage} 512 } 513 \end{center} 514 } 515 \end{wideslide} 516 517 \begin{wideslide}{Static analysis correctness} 518 \onslide*{1}{ 519 \psshadowbox{ 520 \begin{minipage}{12cm} 521 Static analysis of cost is {\red correct} when the actual cost of executing a block of instructions of the object code starting from a label (dynamic cost) is equal to the sum of the costs of each reached label of the trace computed by the static analyzer (static cost). 522 \end{minipage} 523 }} 524 \onslide*{2}{ 525 \begin{tabular}{l l} 526 $\tt \onslide*{3}{\red} EMIT \; L1$ & \multirow{7}{*}{\xymatrix{\onslide*{1,2,3}{\bullet} \onslide*{4}{s_1} \onslide*{2}{\ar[r]^{{\tt L_1}}} \onslide*{3}{\ar@[red][r]^{{\tt \red L_1}}} & \onslide*{1,2,3}{\bullet} \onslide*{4}{s_2} \onslide*{2}{\ar[r]} \onslide*{3}{\ar@[red][r]^{{\tt \red I_1}}} & \onslide*{4}{s_3} \onslide*{1,2,3}{\bullet} \onslide*{2}{\ar[r]} \onslide*{3}{\ar@[red][r]^{{\tt \red I_2}}} & \onslide*{1,2,3}{\bullet} \onslide*{4}{s_4} \onslide*{2}{\ar[r]} \onslide*{3}{\ar@[red][r]^{{\tt \red COND}}} & \onslide*{1,2,3}{\bullet} \onslide*{4}{s_5} \onslide*{2}{\ar[r]^{{\tt L_2}}} \onslide*{3}{\ar@[blue][r]^{{\tt \blue L_2}}} & \onslide*{1,2,3}{\bullet} \onslide*{4}{s_6} \onslide*{2}{\ar[r]} \onslide*{3}{\ar@[blue][r]^{{\tt \blue I_3}}} & \onslide*{1,2,3}{\bullet} \onslide*{4}{s_7} \onslide*{2}{\ar[r]} \onslide*{3}{\ar@[blue][r]^{{\tt \blue I_4}}} & \onslide*{1,2,3}{\bullet} \onslide*{4}{s_8}}} \\ 527 $\tt \onslide*{3}{\red} I_1$ & \\ 528 $\tt \onslide*{3}{\red} I_2$ & \\ 529 $\tt \onslide*{3}{\red} COND \; l1$ & \\ 530 $\tt \onslide*{3}{\blue} EMIT \; L2$ & \\ 531 $\tt \onslide*{3}{\blue} I_3$ & \\ 532 $\tt \onslide*{3}{\blue} I_4$ & 533 \end{tabular} 534 } 535 $\;$\\[3mm] 536 \onslide*{3}{ 537 $$\begin{array}{l l l} 538 cost_{trace} &=& {\red k(I_1) + k(I_2) + k(COND)}+ {\blue k(I_3) + k(I_4)} \\ 539 &=& {\red(k(I_1) + k(I_2) + k(COND))} + {\blue (k(I_3) + k(I_4))} \\ 540 &=& {\red cost(L_1)} + {\blue cost(L_2)} 541 \end{array} $$ 542 } 543 \onslide*{4}{ 544 Lifting to cost dependent from the state 545 \begin{itemize} 546 \item The cost is a function from states to states which can be composed (the cost is incorporated in the state). 547 \item To compute complexity, one is interested only on a part of the state 548 \end{itemize} 549 \begin{center} 550 {\red Galois connection} between an abstract transition system and a concrete one. 551 \end{center} 552 } 553 \onslide*{5}{ 554 Under the hypothesis that $s_1$ is in connection with the abstract state $a_1$ and $\den{}$ is the function computing the cost of the instruction in the abstract state (i.e. an {\red action on the cost monoid}), we have 555 $$ 556 \begin{array}{l l l} 557 cost_{trace} &=& cost\_of({\blue \den{{\tt I_4}} (\den{{\tt I_3}}} ({\red \den{{\tt COND}} (\den{{\tt I_2}} (\den{{\tt I_1}}} a_1))))) \\ 558 &=& cost\_of(({\blue (\den{{\tt I_4}} \circ \den{{\tt I_3}})} \circ {\red (\den{{\tt COND}} \circ \den{{\tt I_2}} \circ \den{{\tt I_1}})}) a_1) \\ 559 &=& cost\_of(({\blue cost(L_2)} \circ {\red cost(L_1)}) a_1) 560 \end{array} 561 $$ 562 } 563 \end{wideslide} 564 457 565 458 566 \begin{wideslide}{Conclusion} 459 \begin{itemize} 460 \item We present an improvement of the labelling approach for a precise resource analisys of the source code. 461 \item We extend labelling approach to cope hidden assumptions on conditional instructions and function calls. 462 \item We are able (almost always) to deal with non commutative costs. 463 \item The usual assumption that compilation preserves the structure of basic blocks is still present. 567 Improvement of the labelling approach. 568 \begin{itemize} 569 \item Function calls. 570 \item Instructions with multiple predecessors (e.g. switch, goto $\ldots$). 571 \item Costs for stateful hardware (e.g. cache, pipelines $\ldots$). 572 \item From lifting of costs ($\mathbb{N}$) 573 to lifting of abstract interpretation ($\mathcal{A} \to \mathcal{A}$). 464 574 \end{itemize} 465 575 Future works 466 576 \begin{itemize} 467 577 \item Abandoning SOS semantics. 468 \item We would like to extend our framework to compilation process that does not preserve basic block structure as in [Tranquilli13 QPLAS].578 \item We would like to extend our framework to compilation process that does not preserve basic block structure as in [Tranquilli13]. 469 579 \end{itemize} 470 580 \end{wideslide}
Note: See TracChangeset
for help on using the changeset viewer.