Changeset 3478 for LTS/DICE2014


Ignore:
Timestamp:
Sep 22, 2014, 4:50:21 PM (5 years ago)
Author:
piccolo
Message:

fixed costlabels

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/DICE2014/slides.tex

    r3467 r3478  
    2121]{powerdot}
    2222%\documentclass[mode=handout,nopagebreaks,paper=a4paper]{powerdot}
    23 
     23\usepackage{multirow}
    2424%\usepackage[latin1]{inputenc}
    2525\usepackage{pstricks,pst-node,pst-text,pst-tree}
     
    217217$\;$\\[-9mm]
    218218\begin{center}
    219 \includegraphics[width=7cm]{cerco.eps}
     219\includegraphics[width=6cm]{cerco.eps}
    220220\end{center}
    221221This talk:
     
    223223\begin{minipage}{12cm}
    224224\begin{itemize}
    225 \item There are some hidden assumption and limitations of labelling approach: {\red instructions with multiple predecessors} and {\red function 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 been formalized 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}.
    228228\end{itemize}
    229229\end{minipage}
     
    279279\item No more label emission statements.
    280280\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}
     284swith(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}
     294swith(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}
    293317\end{wideslide}
    294318
     
    338362\end{minipage}
    339363}\\[3mm]
     364\onslide{2-}{
    340365{\red Assumptions:}
    341366\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-}{
    345372{\red Problems:}
    346373\begin{itemize}
    347 \item It does not work with {\blue non-commutative 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 non-commutative 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}{
    353381\begin{itemize}
    354382\item The usual notion of {\red flat execution trace} is inadequate for a simulation argument.
     
    356384\item Traces of called function are {\red nested}, invariants on position of costlabels are {\red enforced} and steps are grouped {\red according to costlabels}.
    357385\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}
    387440$\;$\\[-7mm]
    388441\begin{lstlisting}[language=Grafite]
     
    392445\end{lstlisting}
    393446\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-}{
    396453\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.
    399457\end{itemize}
    400458\end{wideslide}
     
    409467still requirred to be commutative.
    410468\end{itemize}
     469\onslide{2-}{
    411470\psshadowbox{
    412471\begin{minipage}{12cm}
    413472We 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.
    414473\end{minipage}
    415 }
     474}}
    416475$\;$\\
     476\onslide{3-}{
    417477{\red Drawbacks}
    418478\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 function-calls 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 function-calls 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}
     486At 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}
     505To 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}
     521Static 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}
     538cost_{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}{
     544Lifting 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}{
     554Under 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}
     557cost_{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
    457565
    458566\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.
     567Improvement 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}$).
    464574\end{itemize}
    465575Future works
    466576\begin{itemize}
    467577\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 [Tranquilli13QPLAS].
     578\item We would like to extend our framework to compilation process that does not preserve basic block structure as in [Tranquilli13].
    469579\end{itemize}
    470580\end{wideslide}
Note: See TracChangeset for help on using the changeset viewer.