Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import Omega List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsSepAlg GpsModel GpsModelLemmas.
Require Import GpsGlobal GpsVisible GpsGlobalHelper.

Local Open Scope string_scope.

Set Implicit Arguments.

C.3.4. Protocol equivalence for writes


Definition pre_write_prot_equiv IE acts amap (mo : relation actid) L b r_pre r' :=
  match amap b with
    | Aalloc l n
           loc, l loc l + n res_get r' loc = p_bot
    | Astore typ l _
         (ISREL: is_release_wtyp typ) τ S,
          res_get r_pre l p_bot
          res_get r' l = p_at τ S
           a,
             INa : In a acts
             MO : immediate mo a b
             Wa : is_writeL (amap a) l
           v_env,
            ( Sxxx, res_get (out_rf (b::acts) L a) l = p_at τ Sxxx
                          slist_lt S Sxxx)
            env_move IE r_pre l v_env (out_rf (b::acts) L a)
    | Armw typ l _ _
         (ISACQ: is_acquire_utyp typ) (ISREL: is_release_utyp typ) τ S,
          res_get r_pre l = p_at τ S
           Su,
            res_get r' l = p_at τ Su get_state S = get_state Su
    | _True
  end.

Lemma pwpe :
   b acts amap sb rf mo sc
    (CONS : Consistent (b :: acts) amap sb rf mo sc)
    (ND' : NoDup (b :: acts))
    (PC : prefix_closed sb rf acts)
    (PI : pres_in sb rf b acts)
    L IE
    (RELY : rely IE (in_sb (b :: acts) L b) (amap b)
      (in_sb (b :: acts) L b in_rf (b :: acts) L b))
    EE r
    (V : a : actid, In a acts valid_node IE (b :: acts) (b::acts) amap rf L EE a)
    (CC : compat amap sb rf (upd L (TsbS b) (L (TsbS b) r)))
    (CO : conform (b :: acts) amap mo L acts)
    (VG : valid_ghost (incoming (b :: acts) L b)
      (r out_esc (b :: acts) L EE b))
  (RS : res_lt (res_strip (incoming (b :: acts) L b)) r)
  (NDE: NoDup EE)
  (LR : label_restr (b :: acts) amap sb rf L EE),
   pre_write_prot_equiv IE acts amap mo L b
     (in_sb (b :: acts) L b in_rf (b :: acts) L b) (incoming (b :: acts) L b).

Lemma wpe :
   IE b acts amap mo L r_pre r r' r'',
    pre_write_prot_equiv IE acts amap mo L b r_pre r
    valid_ghost r (r' r'')
    res_lt (res_strip r) r'
    write_prot_equiv IE (amap b) r_pre r'.


This page has been generated by coqdoc