Changeset 2612 for Papers


Ignore:
Timestamp:
Feb 6, 2013, 3:15:04 PM (6 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/itp-2013/ccexec.tex

    r2611 r2612  
    342342;  as_classify: S -> classification
    343343;  as_costed: S -> Prop
     344;  as_label: \forall s. as_costed S s -> label
     345;  as_call_ident: \forall s. as_classify S s = cl_call -> label
    344346;  as_after_return:
    345347    (Σs:as_status. as_classify s = Some ? cl_call) → as_status → Prop
     
    402404\infrule[\texttt{tal\_base\_not\_return}]
    403405 {\texttt{as\_execute}~s_1~s_2 \andalso
    404   \texttt{as\_classifier}~s_1~k \\
    405   k \in \{\texttt{cl\_jump,cl\_other}\} \andalso
     406  \texttt{as\_classify}~s_1 \in \{\texttt{cl\_jump,cl\_other}\} \andalso
    406407  \texttt{as\_costed}~s_2
    407408 }
     
    410411\infrule[\texttt{tal\_base\_return}]
    411412 {\texttt{as\_execute}~s_1~s_2 \andalso
    412   \texttt{as\_classifier}~s_1~\texttt{cl\_return} \\
     413  \texttt{as\_classify}~s_1 = \texttt{cl\_return} \\
    413414 }
    414415 {\texttt{trace\_any\_label}~true~s_1~s_2}
     
    416417\infrule[\texttt{tal\_base\_call}]
    417418 {\texttt{as\_execute}~s_1~s_2 \andalso
    418   \texttt{as\_classifier}~s_1~\texttt{cl\_call} \\
     419  \texttt{as\_classify}~s_1 = \texttt{cl\_call} \\
    419420  \texttt{as\_after\_return}~s_1~s_3 \andalso
    420421  \texttt{trace\_label\_return}~s_2~s_3 \andalso
     
    425426\infrule[\texttt{tal\_step\_call}]
    426427 {\texttt{as\_execute}~s_1~s_2 \andalso
    427   \texttt{as\_classifier}~s_1~\texttt{cl\_call} \\
     428  \texttt{as\_classify}~s_1 = \texttt{cl\_call} \\
    428429  \texttt{as\_after\_return}~s_1~s_3 \andalso
    429430  \texttt{trace\_label\_return}~s_2~s_3 \\
     
    435436\infrule[\texttt{tal\_step\_default}]
    436437 {\texttt{as\_execute}~s_1~s_2 \andalso
     438  \lnot \texttt{as\_costed}~s_2 \\
    437439  \texttt{trace\_any\_label}~b~s_2~s_3
    438   \texttt{as\_classifier}~s_1~\texttt{cl\_other} \\
    439   \lnot \texttt{as\_costed}~s_2
     440  \texttt{as\_classify}~s_1 = \texttt{cl\_other}
    440441 }
    441442 {\texttt{trace\_any\_label}~b~s_1~s_3}
     
    620621
    621622The similarity relation definition if simple, but it involves a large
    622 number of cases. We only show here a few of the cases:
     623number of cases. In the formalization, we define
     624$(\texttt{tlr\_rel}~tlr_1~tlr_2)$ by structural recursion on $tlr_1$ and pattern
     625matching over $tlr_2$. Here we turn
     626the definition into inference rules for the sake of readability. We also
     627omit from trace constructors all arguments, but those that are traces or that
     628are used in the premises of the rules.
     629
     630\infrule
     631 {\texttt{tll\_rel}~tll_1~tll_2
     632 }
     633 {\texttt{tlr\_rel}~(\texttt{tlr\_base}~tll_1)~(\texttt{tlr\_base}~tll_2)}
     634
     635\infrule
     636 {\texttt{tll\_rel}~tll_1~tll_2 \andalso
     637  \texttt{tlr\_rel}~tlr_1~tlr_2
     638 }
     639 {\texttt{tlr\_rel}~(\texttt{tlr\_step}~tll_1~tlr_1)~(\texttt{tlr\_step}~tll_2~tlr_2)}
     640
     641\infrule
     642 {\texttt{as\_label}~H_1 = \texttt{as\_label}~H_2 \andalso
     643  \texttt{tal\_rel}~tal_1~tal_2
     644 }
     645 {\texttt{tll\_rel}~(\texttt{tll\_base}~tal_1~H_1)~(\texttt{tll\_base}~tal_2~H_2)}
     646
     647\infrule
     648 {}
     649 {\texttt{tal\_rel}~\texttt{tal\_base\_not\_return}~(taa @ \texttt{tal\_base\_not\_return}}
     650
     651\infrule
     652 {}
     653 {\texttt{tal\_rel}~\texttt{tal\_base\_return}~(taa @ \texttt{tal\_base\_return}}
     654
     655\infrule
     656 {\texttt{tlr\_rel}~tlr_1~tlr_2 \andalso
     657  \texttt{as\_call\_ident}~H_1 = \texttt{as\_call\_ident}~H_2
     658 }
     659 {\texttt{tal\_rel}~(\texttt{tal\_base\_call}~H_1~tlr_1)~(taa @ \texttt{tal\_base\_call}~H_2~tlr_2)}
     660
     661\infrule
     662 {\texttt{tlr\_rel}~tlr_1~tlr_2 \andalso
     663  \texttt{as\_call\_ident}~H_1 = \texttt{as\_call\_ident}~H_2 \andalso
     664  \texttt{tal\_collapsable}~tal_2
     665 }
     666 {\texttt{tal\_rel}~(\texttt{tal\_base\_call}~tlr_1)~(taa @ \texttt{tal\_step\_call}~tlr_2~tal_2)}
     667
     668\infrule
     669 {\texttt{tlr\_rel}~tlr_1~tlr_2 \andalso
     670  \texttt{as\_call\_ident}~H_1 = \texttt{as\_call\_ident}~H_2 \andalso
     671  \texttt{tal\_collapsable}~tal_1
     672 }
     673 {\texttt{tal\_rel}~(\texttt{tal\_step\_call}~tlr_1~tal_1)~(taa @ \texttt{tal\_base\_call}~tlr_2)}
     674
     675\infrule
     676 {\texttt{tlr\_rel}~tlr_1~tlr_2 \andalso
     677  \texttt{tal\_rel}~tal_1~tal_2 \andalso
     678  \texttt{as\_call\_ident}~H_1 = \texttt{as\_call\_ident}~H_2
     679 }
     680 {\texttt{tal\_rel}~(\texttt{tal\_step\_call}~tlr_1~tal_1)~(taa @ \texttt{tal\_step\_call}~tlr_2~tal_2)}
     681
     682\infrule
     683 {\texttt{tal\_rel}~tal_1~tal_2
     684 }
     685 {\texttt{tal\_rel}~(\texttt{tal\_step\_default}~tal_1)~tal_2}
     686\begin{comment}
    623687\begin{verbatim}
    624688let rec tlr_rel S1 st1 st1' S2 st2 st2'
     
    678742      tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
    679743      tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2
    680   | tal_base_tailcall st1 st1' st1'' _ prf tlr1 ⇒
    681     fl2 = ends_with_ret ∧
    682     ∃st2mid,G.as_tailcall_ident S2 («st2mid, G») = as_tailcall_ident ? «st1, prf» ∧
    683     ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
    684     ∃tlr2 : trace_label_return ? st2mid' st2'.
    685       tal2 ≃ taa @ (tal_base_tailcall … H G tlr2) ∧ tlr_rel … tlr1 tlr2
    686744  | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒
    687745    ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
     
    698756  ].
    699757\end{verbatim}
     758\end{comment}
     759
     760In the preceding rules, a $taa$ is an inhabitant of the
     761$(\texttt{trace\_any\_any}~s_1~s_2)$ inductive data type whose definition
     762we do not give in the paper for lack of space. It is the type of valid
     763prefixes (even empty ones) of \texttt{trace\_any\_label}s that do not contain
     764any function call. Therefore it
     765is possible to concatenate (using ``$@$'') a \texttt{trace\_any\_any} to the
     766left of a \texttt{trace\_any\_label}. The intuition is that two traces are
     767similar if one of them can perform more silent (non observables) moves,
     768whose sequences are here represented by \texttt{trace\_any\_any}.
     769
     770The \texttt{tal\_collapsable} unary predicate over \texttt{trace\_any\_label}s
     771holds when the argument does not contain any function call and it ends
     772with a label (not a return). The intuition is that after a function call we
     773can still perform a sequence of silent actions while remaining similar.
    700774
    701775\section{Forward simulation}
Note: See TracChangeset for help on using the changeset viewer.