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

...

File:
1 edited

Legend:

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

    r2612 r2613  
    1010% a built-in definition.
    1111%\newtheorem{theorem}{Theorem}
     12\newtheorem{condition}{Condition}
    1213
    1314\lstdefinelanguage{coq}
     
    850851put the labelling approach in motion.
    851852
     853\begin{condition}[Case \texttt{cl\_other}]
     854 For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$ and
     855 $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$, there exists an $s_2'$ and a $taaf$ of type $(\texttt{trace\_any\_any\_free}~s_2~s_2')$ such that $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either
     856$taaf$ is non empty, or one among $s_1$ and $s_1'$ is \texttt{as\_costed}.
     857\end{condition}
     858
     859The intuition is that one step can be replaced with zero or more steps if it
     860preserves the relation between the data and if the two final statuses are
     861labelled in the same way. Moreover, we must take special care of the empty case
     862to avoid collapsing two consecutive states that emit the same label to just
     863one state, missing one of the two emissions.
     864
    852865\begin{verbatim}
    853866definition status_simulation ≝
     
    874887        as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
    875888        call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
    876         ∃st2_after_call,st2'.
    877         ∃taa2 : trace_any_any … st2 st2_pre_call.
    878         ∃taa2' : trace_any_any … st2_after_call st2'.
    879         as_execute … st2_pre_call st2_after_call ∧
    880         sim_status_rel st1' st2' ∧
    881         label_rel … st1' st2_after_call
    882       | cl_tailcall ⇒ ∀prf.
    883         (*
    884              st1' ------------S----------\
    885               ↑ \                         \
    886              st1 \--L--\                   \
    887               |         \                   \
    888               S         st2_after_call →taa→ st2'
    889               |             ↑
    890              st2 →taa→ st2_pre_call
    891         *)
    892         ∃st2_pre_call.
    893         as_tailcall_ident ? st2_pre_call = as_tailcall_ident ? («st1, prf») ∧
    894889        ∃st2_after_call,st2'.
    895890        ∃taa2 : trace_any_any … st2 st2_pre_call.
     
    949944    ].
    950945\end{verbatim}
     946\begin{comment}
     947\begin{verbatim}
     948definition status_simulation ≝
     949  λS1 : abstract_status.
     950  λS2 : abstract_status.
     951  λsim_status_rel : status_rel S1 S2.
     952    ∀st1,st1',st2.as_execute S1 st1 st1' →
     953    sim_status_rel st1 st2 →
     954    match as_classify … st1 with
     955    [ None ⇒ True
     956    | Some cl ⇒
     957      match cl with
     958      [ cl_call ⇒ ∀prf.
     959        (*
     960             st1' ------------S----------\
     961              ↑ \                         \
     962             st1 \--L--\                   \
     963              | \       \                   \
     964              S  \-C-\  st2_after_call →taa→ st2'
     965              |       \     ↑
     966             st2 →taa→ st2_pre_call
     967        *)
     968        ∃st2_pre_call.
     969        as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
     970        call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
     971        ∃st2_after_call,st2'.
     972        ∃taa2 : trace_any_any … st2 st2_pre_call.
     973        ∃taa2' : trace_any_any … st2_after_call st2'.
     974        as_execute … st2_pre_call st2_after_call ∧
     975        sim_status_rel st1' st2' ∧
     976        label_rel … st1' st2_after_call
     977      | cl_return ⇒
     978        (*
     979             st1
     980            / ↓
     981           | st1'----------S,L------------\
     982           S   \                           \
     983            \   \-----R-------\            |     
     984             \                 |           |
     985             st2 →taa→ st2_ret |           |
     986                          ↓   /            |
     987                     st2_after_ret →taaf→ st2'
     988
     989           we also ask that st2_after_ret be not labelled if the taaf tail is
     990           not empty
     991        *)
     992        ∃st2_ret,st2_after_ret,st2'.
     993        ∃taa2 : trace_any_any … st2 st2_ret.
     994        ∃taa2' : trace_any_any_free … st2_after_ret st2'.
     995        (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
     996        as_classifier … st2_ret cl_return ∧
     997        as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
     998        ret_rel … sim_status_rel st1' st2_after_ret ∧
     999        label_rel … st1' st2'
     1000      | cl_other ⇒
     1001          (*         
     1002          st1 → st1'
     1003            |      \
     1004            S      S,L
     1005            |        \
     1006           st2 →taaf→ st2'
     1007           
     1008           the taaf can be empty (e.g. tunneling) but we ask it must not be the
     1009           case when both st1 and st1' are labelled (we would be able to collapse
     1010           labels otherwise)
     1011         *)
     1012        ∃st2'.
     1013        ∃taa2 : trace_any_any_free … st2 st2'.
     1014        (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
     1015        sim_status_rel st1' st2' ∧
     1016        label_rel … st1' st2'
     1017      | cl_jump ⇒
     1018        (* just like cl_other, but with a hypothesis more *)
     1019        as_costed … st1' →
     1020        ∃st2'.
     1021        ∃taa2 : trace_any_any_free … st2 st2'.
     1022        (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
     1023        sim_status_rel st1' st2' ∧
     1024        label_rel … st1' st2'
     1025      ]
     1026    ].
     1027\end{verbatim}
     1028\end{comment}
    9511029
    9521030\begin{verbatim}
Note: See TracChangeset for help on using the changeset viewer.