Changeset 3478


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

fixed costlabels

Location:
LTS
Files:
5 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}
  • LTS/Language.ma

    r3449 r3478  
    926926lemma fresh_keep_n_ok : ∀n,m,l.
    927927is_fresh_for_return l n → n ≤ m → is_fresh_for_return l m.
    928 #n #m #l lapply n -n lapply m -m elim l // ** #x #xs #IH #n #m
     928#n #m #l lapply n -n lapply m -m elim l // *
     929[1,2,3: * #x] #xs #IH #n #m
    929930normalize [2: * #H1] #H2 #H3 [ %] /2 by transitive_le/
    930931qed.
     
    13551356lemma fresh_for_subset : ∀l1,l2,n.l1 ⊆ l2 → is_fresh_for_return … l2 n →
    13561357is_fresh_for_return … l1 n.
    1357 #l1 elim l1 // ** #x #xs #IH #l2 #n * #H1 #H2 #H3 whd
     1358#l1 elim l1 // * [1,2,3: * #x] #xs #IH #l2 #n * #H1 #H2 #H3 whd
    13581359try(@IH) // % [2: @IH //] elim l2 in H1 H3; normalize [*]
    1359 ** #y #ys #IH normalize
     1360* [1,2,3: * #y] #ys #IH normalize
    13601361[2,3: * [2,4: #H3 [2: @IH //] * #H4 #H5 @IH //
    13611362|*: #EQ destruct * //
    13621363]]
    13631364*
    1364 [ #EQ destruct ] #H3 #H4 @IH //
     1365[1,3: #EQ destruct ] #H3 #H4 @IH //
    13651366qed.
    13661367
    13671368lemma fresh_append : ∀n,l1,l2.is_fresh_for_return l1 n → is_fresh_for_return l2 n →
    13681369is_fresh_for_return (l1@l2) n.
    1369 #n #l1 lapply n -n elim l1 // ** #x #xs #IH #n #l2 [2: * #H1 ] #H2 #H3
     1370#n #l1 lapply n -n elim l1 // * [1,2,3: * #x] #xs #IH #n #l2 [2: * #H1 ] #H2 #H3
    13701371[ % // @IH //] @IH //
    13711372qed.
  • LTS/Simulation.ma

    r3449 r3478  
    110110                  | None ⇒ []
    111111                  ]
    112     | init_act ⇒ []
    113     ] @ tl
     112
     113   ] @ tl
    114114].
    115115
     
    240240 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).
    241241#S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *
    242 [#f * #l | * [| * #l] | *  [| #l] |] #prf #tl #IH #t2 normalize try @eq_f @IH
     242[#f * #l | * [| * #l] | *  [| #l] ] #prf #tl #IH #t2 normalize try @eq_f @IH
    243243qed.
    244244 
     
    402402
    403403record measurable_trace (S : abstract_status) : Type[0] ≝
    404  { L_label: ActionLabel
     404 { L_label: option ActionLabel
    405405 ; R_label : option ActionLabel
    406406 ; L_pre_state : option S
     
    411411 ; pre_meas : pre_measurable_trace … trace
    412412 ; L_init_ok : match L_pre_state with
    413                [ None ⇒ bool_to_Prop(as_initial … L_s1) ∧ L_label = init_act
    414                | Some s ⇒ is_costlabelled_act L_label ∧
    415                           as_execute … L_label s L_s1
     413               [ None ⇒ bool_to_Prop(as_initial … L_s1) ∧ L_label = None ?
     414               | Some s ⇒ ∃l. L_label = Some ? l ∧ is_costlabelled_act l ∧
     415                          as_execute … l s L_s1
    416416               ]
    417417 ; R_fin_ok : match R_label with
     
    454454∀rel : relations S.
    455455simulation_conditions … rel →
    456 ∀s1,s1': S.∀l.l ≠ init_act → l ≠ cost_act (None ?) →  as_execute S l s1 s1' →
     456∀s1,s1': S.∀l.l ≠ cost_act (None ?) →  as_execute S l s1 s1' →
    457457(as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) →
    458458∀s2.
     
    463463(is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧
    464464(as_classify … s1' ≠ cl_io → as_classify … s2'' ≠ cl_io).
    465 #S #rel #good #s1 #s1' #l #l_noinit #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
     465#S #rel #good #s1 #s1' #l #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
    466466[ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ)
    467467  cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1'
     
    477477    %{exe} %{s2''} %{(t_base …)} % [2: >EQs1' * #H @⊥ @H % ] %
    478478     [ /4 by or_intror, conj, nmk/] * #f * #l #EQ destruct
    479   | #Hclass_s1' cases l in prf l_noinit l_notau;
    480     [ #f #l #prf #_ #_ inversion(is_call_post_label … s1)
     479  | #Hclass_s1' cases l in prf l_notau;
     480    [ #f #l #prf #_ inversion(is_call_post_label … s1)
    481481      [ #Hpost cases(simulate_call_pl … good … prf … REL)
    482482        [2: >Hpost % |3,4: assumption]
     
    492492     ]
    493493   | *
    494      [ #prf #_ #_ cases(simulate_ret_n … good … prf … REL) [2,3: //] #s2' * #s2''
     494     [ #prf #_ cases(simulate_ret_n … good … prf … REL) [2,3: //] #s2' * #s2''
    495495       * #s2''' * #t1 * #exe * #t3 *** #REL' #sil_t1 #sil_t3 #_ %{s2'}
    496496       %{t1} %{(or_introl … sil_t1)} %{s2''} %{exe} %{s2'''} %{t3} %
    497497       [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
    498498       % [ % // % // ] * #f * #l #EQ destruct
    499      | #l #prf #_ #_ cases(simulate_ret_l … good … prf … REL) [2,3: //]
     499     | #l #prf #_ cases(simulate_ret_l … good … prf … REL) [2,3: //]
    500500       #s2' * #s2'' * #s2''' * #t1 * #exe * #t3 ** #REL' #sil_t1 #sil_t3
    501501       %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} %
     
    503503       % [ % // % //] * #f * #l #EQ destruct
    504504    ]
    505   | * [ #_ #_ * #H @⊥ @H % ] #lab #prf #_ #_
     505  | * [ #_ * #H @⊥ @H % ] #lab #prf #_
    506506    cases(simulate_label … prf … REL) [2,3,4: // ] #s2' * #s2'' * #s2''' * #t1
    507507    * #exe * #t3 ** #REL' #sil_t1 #sil_t3 %{s2'} %{t1} %{sil_t1} %{s2''} %{exe}
     
    509509    [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
    510510    % [% // % //] * #f * #l #EQ destruct
    511   | #_ * #H @⊥ @H %
    512511  ]
    513512  % //
     
    549548[2: #REL_pre
    550549    cut
    551      (∃pre_state: S.
     550     (∃pre_state: S.∃ l.
    552551      ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i ∧
    553       ∃middle_state: S.
    554        as_execute … (L_label … t) pre_state middle_state ∧
     552      ∃middle_state: S.L_label … t = Some ? l ∧
     553       as_execute … l pre_state middle_state ∧
    555554      ∃final_state: S.
    556555      ∃tr_i2: raw_trace S middle_state final_state. silent_trace … tr_i2 ∧
    557556       as_classify … final_state ≠ cl_io ∧
    558557       Srel … rel (L_s1 … t) final_state)
    559     [ lapply(L_init_ok … t) >EQpre normalize nodelta * #Hcost #exe   
    560       cases(instr_execute_commute … good … (L_label … t) … exe … REL_pre)
    561       [2,3: % #EQ >EQ in Hcost; * |4: %2 @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
     558      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #l ** #EQllabe #Hcost #exe   
     559      cases(instr_execute_commute … good … l … exe … REL_pre)
     560      [2: % #EQ >EQ in Hcost; * |3: %2 @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
    562561      #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL' #Hcall
    563       #Hclass %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} % // % //
     562      #Hclass %{s2'} %{l} %{t1} %{sil_t1} %{s2''} % [% //] %{s2'''} %{t3} % // % //
    564563      cases sil_t3 [/2 by pre_silent_io/ ] inversion t3
    565564      [ #H109 #H110 #H111 #H112 #H113 destruct @Hclass @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
    566565      #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 cases H125
    567566      #H @⊥ @H %]
    568     * #pre_state * #tr_i * #silent_i * #middle_state * #step_pre_middle
     567    * #pre_state * #l' * #tr_i * #silent_i * #middle_state ** #EQl' #step_pre_middle
    569568    * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL
    570569| #REL
    571   cut(bool_to_Prop (as_initial S s2)∧L_label S t=init_act)
     570  cut(bool_to_Prop (as_initial S s2)∧L_label S t=None ?)
    572571      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //]
    573572        @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label
     
    602601         * >EQpost #EQ destruct #exe
    603602          cases(instr_execute_commute … good … final_label … exe … REL')
    604           [2,3,6,7: % #EQ destruct cases H1 [1,3,5,7: * |*: normalize #EQ destruct]
    605           |4,8: %1 @tail_of_premeasurable_is_not_io //
     603          [2,5: % #EQ destruct cases H1 [1,3,5,7: * |*: normalize #EQ destruct]
     604          |3,6: %1 @tail_of_premeasurable_is_not_io //
    606605          ]
    607606          #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL'
     
    613612     normalize nodelta /5 by conj/
    614613|3: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (Some ? post_state') … (tr_i2 @ t' @ tr') …)}
    615     normalize nodelta [2: % // lapply(L_init_ok … t) >EQpre normalize nodelta * //
     614    normalize nodelta [2: %{l'} % // % // lapply(L_init_ok … t) >EQpre normalize nodelta * #l'' ** >EQl'
     615      #EQ destruct //
    616616    |3: /3 by append_silent_premeasurable, append_premeasurable_silent/
    617617    |4: % [2: %{final_state'} /5 by ex_intro, conj/ ] % /8 by ex_intro, conj/ % [ /3 by conj/]
     
    625625  normalize nodelta
    626626  [ assumption
    627   | % // lapply(L_init_ok … t) >EQpre normalize nodelta * //
     627  | %{l'} % // % // lapply(L_init_ok … t) >EQpre normalize nodelta * #l'' ** >EQl' #EQ destruct //
    628628  | /4 by append_premeasurable_silent/
    629629  | % // % [2: %{pre_state} /3/ ] % [ /2/] >get_cost_label_append
  • LTS/Traces.ma

    r3396 r3478  
    3333 | a_call : CallCostLabel → CostLabel
    3434 | a_return_post : ReturnPostCostLabel → CostLabel
    35  | a_non_functional_label : NonFunctionalLabel → CostLabel.
     35 | a_non_functional_label : NonFunctionalLabel → CostLabel
     36 | i_act : CostLabel.
    3637
    3738coercion a_call.
     
    149150  | a_non_functional_label x1 ⇒
    150151     λc2.match c2 with [a_non_functional_label y1 ⇒ x1 == y1 | _ ⇒ false ]
     152  | i_act ⇒ λc2.match c2 with [i_act ⇒ true | _ ⇒ false ]
    151153  ].
    152154
    153155lemma eq_costlabel_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
    154156(c1 ≠ c2 → P false) → P (eq_costlabel c1 c2).
    155 #P * #c1 * #c2 #H1 #H2 whd in match (eq_costlabel ??);
     157#P * [1,2,3: #c1 |] * [1,2,3,5,6,7,9,10,11,13,14,15: #c2 |*:]
     158#H1 #H2 whd in match (eq_costlabel ??);
    156159try (@H2 % #EQ destruct)
    157160[ change with (eq_call_cost_lab ??) in ⊢ (?%); @eq_call_cost_lab_elim
     
    162165| change with (eq_nf_label ??) in ⊢ (?%); @eq_fn_label_elim
    163166  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
     167| @H1 %
    164168]
    165169qed.
     
    187191 | call_act : FunctionName → CallCostLabel → ActionLabel
    188192 | ret_act : option(ReturnPostCostLabel) → ActionLabel
    189  | cost_act : option NonFunctionalLabel → ActionLabel
    190  | init_act : ActionLabel.
     193 | cost_act : option NonFunctionalLabel → ActionLabel.
    191194 
    192195definition is_cost_label : ActionLabel → Prop ≝
     
    263266                    | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
    264267                    | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
    265                     | init_act ⇒ False
    266268                    ].
    267269(*
  • LTS/Vm.ma

    r3465 r3478  
    411411    return (op … abs_t (instr_m … instr) n)
    412412  ].
    413  
    414 inductive InitCostLabel : Type[0] ≝
    415   costlab : CostLabel → InitCostLabel
    416 | initial_act : InitCostLabel.
    417 
    418 definition eq_init_costlabel ≝ (λi1,i2.match i1 with
    419  [ initial_act ⇒ match i2 with [initial_act ⇒ true | _ ⇒ false ]
    420  | costlab c ⇒ match i2 with [costlab c1 ⇒ c == c1 | _ ⇒ false ]
    421  ]).
    422 
    423 definition DEQInitCostLabel ≝ mk_DeqSet InitCostLabel eq_init_costlabel ?.
    424 * [#c] * [1,3: #c1] whd in match eq_init_costlabel; normalize nodelta
    425 [4: /2/ | 2,3: % #EQ destruct] % [ #H >(\P H) % | #EQ destruct >(\b (refl …)) %]
    426 qed.
    427 
    428 coercion costlab.
    429 
    430 definition list_cost_to_list_initcost : list CostLabel → list InitCostLabel ≝
    431 map … costlab.
    432 
    433 coercion list_cost_to_list_initcost.
    434  
     413
     414
    435415record cost_map_T (dom : DeqSet) (codom : Type[0]) : Type[1] ≝
    436416{ map_type :> Type[0]
     
    442422}.
    443423
    444 definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (InitCostLabel × ℕ) ≝
     424definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (CostLabel × ℕ) ≝
    445425λp,i,program_counter.
    446426match i with
    447427  [ Seq _ opt_l ⇒ match opt_l with
    448                   [ Some lbl ⇒ [〈costlab (a_non_functional_label lbl),S program_counter〉]
     428                  [ Some lbl ⇒ [〈(a_non_functional_label lbl),S program_counter〉]
    449429                  | None ⇒ [ ]
    450430                  ]
    451431  | Ijmp _ ⇒ [ ]
    452   | CJump _ newpc ltrue lfalse ⇒ [〈costlab (a_non_functional_label ltrue),newpc〉;
    453                                   〈costlab (a_non_functional_label lfalse),S program_counter〉]
    454   | Iio lin _ lout ⇒ [〈costlab (a_non_functional_label lin),program_counter〉;
    455                       〈costlab (a_non_functional_label lout),S program_counter〉]
     432  | CJump _ newpc ltrue lfalse ⇒ [〈(a_non_functional_label ltrue),newpc〉;
     433                                  〈(a_non_functional_label lfalse),S program_counter〉]
     434  | Iio lin _ lout ⇒ [〈(a_non_functional_label lin),program_counter〉;
     435                      〈(a_non_functional_label lout),S program_counter〉]
    456436  | Icall f ⇒ [ ]
    457437  | Iret ⇒ [ ]
     
    459439
    460440let rec labels_pc (p : assembler_params)
    461 (prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (InitCostLabel × ℕ) ≝
     441(prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝
    462442match prog with
    463 [ nil ⇒ [〈initial_act,O〉] @
    464         map … (λx.let〈y,z〉 ≝ x in 〈costlab (a_call z),y〉) (call_label_fun … p) @
    465         map … (λx.let〈y,z〉 ≝ x in 〈costlab (a_return_post z),y〉) (return_label_fun … p)
     443[ nil ⇒ [〈i_act,O〉] @
     444        map … (λx.let〈y,z〉 ≝ x in 〈(a_call z),y〉) (call_label_fun … p) @
     445        map … (λx.let〈y,z〉 ≝ x in 〈(a_return_post z),y〉) (return_label_fun … p)
    466446| cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p is (S program_counter)
    467447].
     
    485465 label_of_pc ReturnPostCostLabel (return_label_fun p) x1=return x2 →
    486466 ∀m.
    487    mem … 〈costlab (a_return_post x2),x1〉 (labels_pc p (instructions p prog) m).
     467   mem … 〈(a_return_post x2),x1〉 (labels_pc p (instructions p prog) m).
    488468 #p * #l #endmain #_ whd in match (labels_pc ???); #x1 #x2 #H elim l
    489469[ #m @mem_append_l2 @mem_append_l2 whd in H:(??%?);
     
    499479 label_of_pc CallCostLabel (call_label_fun p) x1=return x2 →
    500480 ∀m.
    501    mem … 〈costlab (a_call x2),x1〉 (labels_pc p (instructions p prog) m).
     481   mem … 〈(a_call x2),x1〉 (labels_pc p (instructions p prog) m).
    502482 #p * #l #endmain #_ whd in match (labels_pc ???); #x1 #x2 #H elim l
    503483[ #m @mem_append_l2 @mem_append_l1 whd in H:(??%?);
     
    530510*) 
    531511
    532 unification hint  0 ≔ ;
    533     X ≟ DEQInitCostLabel
    534 (* ---------------------------------------- *) ⊢
    535     InitCostLabel ≡ carr X.
    536 
    537 
    538 unification hint  0 ≔ p1,p2;
    539     X ≟ DEQInitCostLabel
    540 (* ---------------------------------------- *) ⊢
    541     eq_init_costlabel p1 p2 ≡ eqb X p1 p2.
    542    
    543 
    544512let rec m_foldr (M : Monad) (X,Y : Type[0]) (f : X→Y→M Y) (l : list X) (y : Y) on l : M Y ≝
    545513match l with
     
    549517
    550518definition static_analisys : ∀p : assembler_params.∀abs_t : monoid.(AssemblerInstr p → abs_t) →
    551 ∀mT : cost_map_T DEQInitCostLabel abs_t.AssemblerProgram p → option mT ≝
     519∀mT : cost_map_T DEQCostLabel abs_t.AssemblerProgram p → option mT ≝
    552520λp,abs_t,instr_m,mT,prog.
    553521let prog_size ≝ S (|instructions … prog|) in
     
    709677|cost_act x ⇒
    710678   match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
    711 |init_act⇒[ ]
    712679] = [x] ∧
    713  (mem … 〈costlab x,pc … st2〉 (labels_pc p (instructions … prog) O)).
     680 (mem … 〈x,pc … st2〉 (labels_pc p (instructions … prog) O)).
    714681#p #p' #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta
    715682>EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta
     
    744711|cost_act x ⇒
    745712   match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
    746 |init_act⇒[ ]
    747713] = [ ] ∧ pc … st2 = f (pc … st1).
    748714#p #p' #prog #st1 #st2 #l #i #f #EQi whd in match eval_vmstate; normalize nodelta
     
    770736∀lbl.
    771737mem … lbl (get_costlabels_of_trace … t) →
    772 mem … (costlab lbl) (map ?? \fst … (labels_pc … (instructions p prog) O)).
     738mem … (lbl) (map ?? \fst … (labels_pc … (instructions p prog) O)).
    773739#p #p' #prog #st1 #st2 #t elim t
    774740[ #st #lbl *
     
    902868qed.
    903869
     870definition actionlabel_to_costlabel : ActionLabel → list CostLabel ≝
     871λa.match a with
     872[ call_act f l ⇒ [a_call l]
     873| ret_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_return_post l]]
     874| cost_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_non_functional_label l]]
     875].
     876
     877definition get_costlabels_of_measurable_trace : ∀S : abstract_status.measurable_trace S → list CostLabel ≝
     878λS,t.
     879 match L_label … t with
     880 [ None ⇒ [i_act]
     881 | Some l ⇒ actionlabel_to_costlabel l
     882 ] @
     883 get_costlabels_of_trace … (trace … t).
     884
    904885(*get_costlabels_of_measurable_trace deve aggiungere la label iniziale.*)
    905 theorem static_dynamic : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog.
     886theorem static_dynamic_meas : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog.
    906887∀abs_t : abstract_transition_sys (m … p').∀instr_m.
    907888∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1.
    908889∀EQmap : static_analisys p ? instr_m mT prog = return map1.
    909890∀t : measurable_trace (asm_operational_semantics p p' prog).
    910 ∀a1.rel_galois … good st1 (L_s1 … t)
     891∀a1.rel_galois … good (L_s1 … t) a1
    911892let stop_state ≝ match R_post_state … t with [None ⇒ R_s2 … t | Some x ⇒ x ] in
    912 ∀costs.
    913 costs = dependent_map CostLabel ? (get_costlabels_of_measurable_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
    914 rel_galois … good stop_state (act_abs … abs_t (big_op … costs) a1).
    915 
    916 
    917 
     893∀abs_trace.
     894abs_trace = dependent_map CostLabel ? (get_costlabels_of_measurable_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
     895rel_galois … good stop_state (act_abs … abs_t (big_op … abs_trace) a1).
     896[2: @hide_prf
     897    whd in match get_costlabels_of_measurable_trace in prf; normalize nodelta in prf;
     898    cases(mem_append ???? prf) -prf
     899    [2: #prf cases(mem_map ????? (labels_of_trace_are_in_code … prf)) *
     900        #lbl' #pc * #Hmem #EQ destruct   
     901        >(proj1 … (static_analisys_ok … no_dup … EQmap … Hmem))
     902        @(proj2 … (static_analisys_ok … no_dup … EQmap … Hmem))
     903    | inversion(L_label … t) normalize nodelta [| #lbl'] #EQleft
     904      [ * [2: *] #EQ destruct cases daemon (* i_act sta sempre nel codice *)
     905      | (* per inversione su as_execute *) cases daemon
     906      ]
     907    ]
     908]
     909#p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap1 #t #a1 #rel_galois #abs_trace #EQabs_trace
     910xxxxxx
     911lapply(static_dynamic … (trace …t) … abs_trace) try //
     912
     913
Note: See TracChangeset for help on using the changeset viewer.