Changeset 2203 for src/common


Ignore:
Timestamp:
Jul 17, 2012, 6:57:40 PM (7 years ago)
Author:
campbell
Message:

A general result about simulations of executions.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Executions.ma

    r2202 r2203  
    1111| steps_steps : ∀tr,s,e,tr',e'. steps state tr e e' → steps state (tr'⧺tr) (e_step … tr' s e) e'.
    1212
     13(* Go from individual steps to part of an execution trace. *)
     14lemma plus_exec : ∀FE:fullexec io_out io_in. ∀gl,s,tr,s'.
     15  plus … FE gl s tr s' →
     16  is_final … FE gl s' = None ? →
     17  steps (state … gl) tr
     18    (exec_inf_aux … FE gl (step … FE gl s))
     19    (exec_inf_aux … FE gl (step … FE gl s')).
     20#FE #gl #s0 #tr0 #s0' #P elim P
     21[ #s1 #tr #s2 #NF1 #EX #NF2 >EX >exec_inf_aux_unfold
     22  whd in ⊢ (???%?); >NF2
     23  %2
     24| #s1 #tr #s2 #tr' #s3 #NF1 #EX1 #P2 #IH #NF3
     25  >EX1 >exec_inf_aux_unfold
     26  whd in ⊢ (???%?); >(plus_not_final … P2) /3/
     27] qed.
     28
     29lemma plus_final : ∀FE:fullexec io_out io_in. ∀gl,s,tr,s',r.
     30  plus … FE gl s tr s' →
     31  is_final … FE gl s' = Some ? r →
     32  ∃tr'. steps (state … gl) tr
     33    (exec_inf_aux … FE gl (step … FE gl s))
     34    (e_stop … tr' r s').
     35#FE #gl #s0 #tr0 #s0' #r #P elim P
     36[ #s1 #tr #s2 #NF1 #EX #F2 >EX >exec_inf_aux_unfold
     37  whd in ⊢ (??(λ_.???%?)); >F2
     38  %{tr} %1
     39| #s1 #tr #s2 #tr' #s3 #NF1 #EX1 #P2 #IH #F3
     40  >EX1 >exec_inf_aux_unfold
     41  whd in ⊢ (??(λ_.???%?)); >(plus_not_final … P2)
     42  cases (IH F3) #tr'' #S' %{tr''} /2/
     43] qed.
     44
    1345(* In some places we do not consider wrong executions. *)
    1446
     
    1850| nw_interact : ∀o,k. (∀i. not_wrong state (k i)) → not_wrong state (e_interact … o k).
    1951
     52lemma not_wrong_not_wrong : ∀state,m.
     53  ¬ (not_wrong state (e_wrong … m)).
     54#state #m % #NW inversion NW
     55#A #B #C #D #E destruct
     56qed.
     57
     58lemma not_wrong_steps : ∀state,e,e',tr.
     59  steps state tr e e' →
     60  not_wrong state e →
     61  not_wrong state e'.
     62#state #e0 #e0' #tr0 #S elim S
     63[ //
     64| #tr #s #e #NW inversion NW
     65  #A #B #C #D #E try #F destruct //
     66| #tr #s #e #tr' #e' #S' #IH #NW @IH
     67  inversion NW
     68  #A #B #C #D #E try #F destruct //
     69] qed.
     70
     71lemma not_wrong_init : ∀FE,p.
     72  not_wrong ? (exec_inf … FE p) →
     73  ∃s. make_initial_state … p = OK ? s.
     74#FE #p whd in ⊢ (??% → ?);
     75cases (make_initial_state ??? p)
     76[ /2/
     77| normalize #m #NW @⊥
     78  inversion NW #H1 #H2 #H3 #H4 try #H5 destruct
     79] qed.
     80
     81
    2082(* One execution is simulated by another, but possibly using a different number
    21    of steps. *)
     83   of steps.  Note that we have to allow for several steps at the end to make
     84   the trace match up. *)
    2285
    23 coinductive simulates (state:Type[0]) : execution state io_out io_in → execution state io_out io_in → Prop ≝
    24 | sim_stop : ∀tr,tr',r,s1,s2,e1,e2.
    25     steps state tr e1 (e_stop … tr' r s1) →
    26     steps state tr e2 (e_stop … tr' r s2) →
    27     simulates state e1 e2
     86coinductive simulates (S1,S2:Type[0]) : execution S1 io_out io_in → execution S2 io_out io_in → Prop ≝
     87| sim_stop : ∀tr,r,s1,s2,e1,e2,tr1,tr2.
     88    steps S1 tr e1 (e_stop … tr1 r s1) →
     89    steps S2 tr e2 (e_stop … tr2 r s2) →
     90    simulates S1 S2 e1 e2
    2891| sim_steps : ∀tr,e1,e1',e2,e2'.
    29     steps state tr e1 e1' →
    30     steps state tr e2 e2' →
    31     simulates state e1' e2' →
    32     simulates state e1 e2
     92    steps S1 tr e1 e1' →
     93    steps S2 tr e2 e2' →
     94    simulates S1 S2 e1' e2' →
     95    simulates S1 S2 e1 e2
    3396| sim_interact : ∀o,k1,k2.
    34     (∀i. simulates state (k1 i) (k2 i)) →
    35     simulates state (e_interact … o k1) (e_interact … o k2).
     97    (∀i. simulates S1 S2 (k1 i) (k2 i)) →
     98    simulates S1 S2 (e_interact … o k1) (e_interact … o k2).
    3699
     100
     101(* Result for lifting simulations on states to simulations on execution traces.
     102   At the time of writing this hasn't been used in anger yet...
     103   
     104   This probably isn't the best route for the stages of the compiler that have
     105   results in terms of structured traces, but it should be good for the
     106   front-end.
     107 *)
     108
     109let corec build_cofix_simulation
     110  (FS1,FS2:fullexec io_out io_in)
     111  (g1:global … FS1) (g2:global … FS2)
     112  (SIM:state … g1 → state … g2 → Prop)
     113  (s1:state … g1) (s2:state … g2)
     114  (NF:is_final … FS1 g1 s1 = None ?)
     115  (S:SIM s1 s2)
     116  (SIM_FINAL: ∀x,y. SIM x y → is_final … FS1 g1 x = is_final … FS2 g2 y)
     117  (SIM_GOOD: ∀x,y. SIM x y →
     118         not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 x)) →
     119         is_final … FS1 g1 x = None ? →
     120         ∃tr,x',y'. And (plus … FS1 g1 x tr x') (And (plus … FS2 g2 y tr y') (SIM x' y')) )
     121  (NW:not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1)))
     122: simulates ?? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1)) (exec_inf_aux ?? FS2 g2 (step … FS2 g2 s2)) ≝ ?.
     123lapply (SIM_GOOD … S NW NF)
     124* #tr * #s1' * #s2' * #P1 * #P2 #S'
     125lapply (refl ? (is_final … FS1 g1 s1'))
     126cases (is_final … s1') in ⊢ (???% → ?);
     127[ #NF1
     128  @(sim_steps … tr … (build_cofix_simulation … S' SIM_FINAL SIM_GOOD ?))
     129  [ @(plus_exec … P1) //
     130  | @(plus_exec … P2) <SIM_FINAL //
     131  | @(not_wrong_steps … (plus_exec … P1 …)) //
     132  | //
     133  ]
     134| #r #F1
     135  cases (plus_final … P1 F1) #tr1' #S1
     136  cases (plus_final … P2 ?) [ 3: <SIM_FINAL [ @F1 | // | skip ] | 2: skip ] #tr2' #S2
     137  @(sim_stop … S1 S2)
     138] qed.
     139
     140theorem lift_simulation : ∀FE1,FE2:fullexec io_out io_in.
     141  ∀p1:program … FE1.  ∀p2:program … FE2.
     142  let g1 ≝ make_global … p1 in
     143  let g2 ≝ make_global … p2 in
     144  ∀SIM: state … g1 → state … g2 → Prop.
     145  ∀SIM_INIT: ∀s1. make_initial_state … p1 = OK ? s1 →
     146             ∃s2. And (make_initial_state … p2 = OK ? s2) (SIM s1 s2).
     147  ∀SIM_FINAL: ∀x,y. SIM x y → is_final … FE1 g1 x = is_final … FE2 g2 y.
     148  ∀SIM_GOOD: ∀x,y. SIM x y →
     149         not_wrong ? (exec_inf_aux … FE1 g1 (step … FE1 g1 x)) →
     150         is_final … FE1 g1 x = None ? →
     151         ∃tr,x',y'. And (plus … FE1 g1 x tr x') (And (plus … FE2 g2 y tr y') (SIM x' y')).
     152  let e1 ≝ exec_inf … FE1 p1 in
     153  let e2 ≝ exec_inf … FE2 p2 in
     154  not_wrong … e1 →
     155  simulates … e1 e2.
     156
     157#FE1 #FE2 #p1 #p2
     158letin g1 ≝ (make_global … p1)
     159letin g2 ≝ (make_global … p2)
     160#SIM #SIM_INIT #SIM_FINAL #SIM_GOOD
     161#NW
     162cases (not_wrong_init … p1 NW)
     163#s1 #I1
     164cases (SIM_INIT … I1) #s2 * #I2 #S
     165whd in NW:(??%) ⊢ (???%%);
     166>I1 in NW ⊢ %; >I2 whd in ⊢ (??% → ???%%);
     167change with g1 in match (make_global … p1);
     168change with g2 in match (make_global … p2);
     169
     170>exec_inf_aux_unfold whd in ⊢ (??% → ???%?);
     171lapply (SIM_FINAL … S)
     172lapply (refl ? (is_final … s1))
     173cases (is_final … s1) in ⊢ (???% → %);
     174[ #F1 #F2 >(exec_inf_aux_unfold … FE2) whd in ⊢ (??% → ???%%);
     175  <F2 whd in ⊢ (? → ???%%); #NW
     176  @(sim_steps … E0 … (build_cofix_simulation … SIM_FINAL SIM_GOOD …)) try assumption
     177  [ // | // | inversion NW #A #B #C #D #E try #F destruct assumption ]
     178| #r #F1 #F2 #NW whd in ⊢ (???%%);
     179  >exec_inf_aux_unfold whd in ⊢ (???%%);
     180  <F2 whd in ⊢ (???%%);
     181  @(sim_stop … (steps_stop …) (steps_stop …))
     182] qed.
     183
  • src/common/SmallstepExec.ma

    r2202 r2203  
    1919         repeat n' ?? exec g s1
    2020].
     21
     22(* We take care here to check that we're not at the final state.  It is not
     23   necessarily the case that a success step guarantees this (e.g., because
     24   there may be no way to stop a processor, so an infinite loop is used
     25   instead). *)
     26inductive plus (O) (I) (TS:trans_system O I) (ge:global … TS) : state … TS ge → trace → state … TS ge → Prop ≝
     27| plus_one : ∀s1,tr,s2.
     28    is_final … TS ge s1 = None ? →
     29    step … TS ge s1 = OK … 〈tr,s2〉 →
     30    plus … ge s1 tr s2
     31| plus_succ : ∀s1,tr,s2,tr',s3.
     32    is_final … TS ge s1 = None ? →
     33    step … TS ge s1 = OK … 〈tr,s2〉 →
     34    plus … ge s2 tr' s3 →
     35    plus … ge s1 (tr⧺tr') s3.
     36
     37lemma plus_not_final : ∀O,I,FE. ∀gl,s,tr,s'.
     38  plus O I FE gl s tr s' →
     39  is_final … FE gl s = None ?.
     40#O #I #FE #gl #s0 #tr0 #s0' * //
     41qed.
    2142
    2243let rec trace_map (A,B:Type[0]) (f:A → res (trace × B))
Note: See TracChangeset for help on using the changeset viewer.