Properties of execution prefixes


Require Import Peano_dec List Vbase Relations ExtraRelations.
Require Import actions c11 opsemsets coherence.
Set Implicit Arguments.


Useful lemmas for deriving In a acts

Section AccessIn.

Variable acts : list actid.
Variable lab : actidact.
Variables (sb asw : relation actid).
Hypothesis (EF: ExecutionFinite acts lab sb asw).

Lemma is_access_In a : is_access (lab a) → In a acts.

Lemma is_fence_In a : is_fence (lab a) → In a acts.

Lemma is_sc_In a : is_sc (lab a) → In a acts.

Lemma is_na_In a : is_na (lab a) → In a acts.

Lemma is_write_In a : is_write (lab a) → In a acts.

Lemma is_writeL_In a l : is_writeL (lab a) lIn a acts.

Lemma is_readL_In a l : is_readL (lab a) lIn a acts.

Lemma is_rmw_In a : is_rmw (lab a) → In a acts.

Lemma is_release_write_In:
   a (ACC: is_release_write (lab a)), In a acts.

Lemma is_acquire_read_In:
   a (ACC: is_acquire_read (lab a)), In a acts.

Lemma is_release_fence_In:
   a (ACC: is_release_fence (lab a)), In a acts.

Lemma is_acquire_fence_In:
   a (ACC: is_acquire_fence (lab a)), In a acts.

End AccessIn.

Hint Immediate
     is_access_In is_fence_In is_sc_In
     is_write_In is_writeL_In
      is_readL_In
     is_na_In is_rmw_In
     is_release_write_In is_acquire_read_In
     is_release_fence_In is_acquire_fence_In
: is_in.


Lemma pref_LabIn:
   o1 o2 (Pref: pref_opsem o1 o2)
         a (IN: In a (Acts o1)),
    Lab o1 a = Lab o2 a.


Lemma clos_trans_sb_In1:
   acts lab sb asw (EF: ExecutionFinite acts lab sb asw)
         a b (SB: clos_trans _ sb a b),
    In a acts.

Lemma clos_trans_sb_In2:
   acts lab sb asw (EF: ExecutionFinite acts lab sb asw)
         a b (SB: clos_trans _ sb a b),
    In b acts.

Hint Immediate
     clos_trans_sb_In1 clos_trans_sb_In2 : in_acts.

Lemma Pref_clos_trans :
   o1 o2 (Pref: pref_opsem o1 o2),
    clos_trans _ (Sb o1)
    <-→ restr_rel (fun xIn x (Acts o1)) (clos_trans _ (Sb o2)).

Lemma Pref_release_seq_elem1:
   o1 (EF: ExecutionFinite (Acts o1) (Lab o1) (Sb o1) (Asw o1))
         o2 (Pref: pref_opsem o1 o2) mt2,
    inclusion _
              (restr_rel (fun xIn x (Acts o1)) (release_seq_elem mt2 (Lab o2) (Sb o2)))
              (release_seq_elem mt2 (Lab o1) (Sb o1)).


Lemma Pref_release_seq_elem2:
   o1 (EF: ExecutionFinite (Acts o1) (Lab o1) (Sb o1) (Asw o1))
         o2 (Pref: pref_opsem o1 o2) mt2
         x y (RS: release_seq_elem mt2 (Lab o1) (Sb o1) x y)
             (AX: In x (Acts o1))
             (AY: In y (Acts o1)),
    restr_rel (fun xIn x (Acts o1)) (release_seq_elem mt2 (Lab o2) (Sb o2)) x y.

Lemma Pref_release_seq1:
   o1 (EF: ExecutionFinite (Acts o1) (Lab o1) (Sb o1) (Asw o1))
         o2 (Pref: pref_opsem o1 o2)
         rf1 rf2 (PrefRF: same_relation _ (fun x yrf1 y = Some x)
                          (restr_rel (fun xIn x (Acts o1)) (fun x yrf2 y = Some x)))
                 (Pref_UCRF: upward_closed (fun x yrf2 y = Some x)
                                           (fun xIn x (Acts o1)))
         mo1 mo2 (PrefMO: same_relation _ mo1 (restr_rel (fun xIn x (Acts o1)) mo2)) mt2,
    inclusion _
              (restr_rel (fun xIn x (Acts o1)) (release_seq mt2 (Lab o2) (Sb o2) rf2 mo2))
              (release_seq mt2 (Lab o1) (Sb o1) rf1 mo1).

Lemma Pref_release_seq3:
   o1 (EF: ExecutionFinite (Acts o1) (Lab o1) (Sb o1) (Asw o1))
         o2 (Pref: pref_opsem o1 o2)
         rf1 rf2 (PrefRF: same_relation _ (fun x yrf1 y = Some x)
                          (restr_rel (fun xIn x (Acts o1)) (fun x yrf2 y = Some x)))
         mo1 mo2 (PrefMO: same_relation _ mo1 (restr_rel (fun xIn x (Acts o1)) mo2))
         mt2 (Pref_UCMO: snd mt2 = MT3origupward_closed mo2 (fun xIn x (Acts o1)))
         x y (RS: release_seq mt2 (Lab o1) (Sb o1) rf1 mo1 x y)
             (AX: In x (Acts o1)),
    restr_rel (fun xIn x (Acts o1)) (release_seq mt2 (Lab o2) (Sb o2) rf2 mo2) x y.

Lemma Pref_UCSbt :
   o1 o2 (Pref: pref_opsem o1 o2),
    upward_closed (clos_trans actid (Sb o2)) (fun xIn x (Acts o1)).

Lemma hb_unfold mt2 lab sb asw rf mo :
  happens_before mt2 lab sb asw rf mo =
  clos_trans actid
        (union actid sb
           (union actid (synchronizes_with mt2 lab sb rf mo true) asw)).

Lemma rf_rel_none:
   (a: actid) (rf: actidoption actid),
    rf a = None b (RF: rf a = Some b), False.

Lemma rf_same_rel_fun:
   (P: actidProp)
         (rf1 rf2: actidoption actid)
         (PrefRF: same_relation _
                                (fun x yrf1 y = Some x)
                                (restr_rel P (fun x yrf2 y = Some x)))
         (Pref_UCRF: upward_closed (fun x yrf2 y = Some x) P)
         a (PA: P a),
    rf1 a = rf2 a.

Section Pref_Axioms.

  Variables o1 o2 : opsem.
  Hypothesis Pref : pref_opsem o1 o2.

  Variables rf1 rf2 : actidoption actid.
  Hypothesis PrefRF : same_relation _ (fun x yrf1 y = Some x)
                      (restr_rel (fun xIn x (Acts o1)) (fun x yrf2 y = Some x)).
  Hypothesis Pref_UCRF: upward_closed (fun x yrf2 y = Some x)
                                       (fun xIn x (Acts o1)).

  Variables mo1 mo2 : relation actid.
  Hypothesis PrefMO : same_relation _ mo1 (restr_rel (fun xIn x (Acts o1)) mo2).

  Variable mt2 : modeltyp_threadid * modeltyp_relseq.

  Definition condition_for_ucmo mt2 :=
    fst mt2 = MT2orig snd mt2 = MT3orig.

  Hypothesis Pref_UCMO :
    condition_for_ucmo mt2upward_closed mo2 (fun xIn x (Acts o1)).

  Variables sc1 sc2 : relation actid.
  Hypothesis PrefSC : same_relation _ sc1 (restr_rel (fun xIn x (Acts o1)) sc2).

Lemma Pref_ExecutionFinite :
  ExecutionFinite (Acts o1) (Lab o1) (Sb o1) (Asw o1).

Hint Resolve Pref_ExecutionFinite.

Lemma Pref_UCRS :
  upward_closed (release_seq mt2 (Lab o2) (Sb o2) rf2 mo2) (fun xIn x (Acts o1)).

Lemma Pref_UCSW :
  upward_closed (synchronizes_with mt2 (Lab o2) (Sb o2) rf2 mo2 true)
                (fun xIn x (Acts o1)).

Lemma Pref_UCHB:
  upward_closed (happens_before mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2)
                (fun xIn x (Acts o1)).

Lemma Pref_synchronizes_with:
  synchronizes_with mt2 (Lab o1) (Sb o1) rf1 mo1 true
  <-→ restr_rel (fun xIn x (Acts o1))
                 (synchronizes_with mt2 (Lab o2) (Sb o2) rf2 mo2 true).

Lemma Pref_happens_before:
  happens_before mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1
  <-→ restr_rel (fun xIn x (Acts o1))
                 (happens_before mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2).


Lemma Pref_ConsistentMO:
  ConsistentMO (Lab o2) mo2
  ConsistentMO (Lab o1) mo1.

Lemma Pref_ConsistentMOhb:
   (Cmohb : ConsistentMOhb mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    ConsistentMOhb mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.

Lemma Pref_ConsistentSC:
    ConsistentSC mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2 sc2
    ConsistentSC mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1 sc1.

Lemma Pref_ConsistentRF_dom_none:
   (CrfN : ConsistentRF_dom_none mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    ConsistentRF_dom_none mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.

Lemma Pref_ConsistentRF_dom_some:
   (CrfS : ConsistentRF_dom_some mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    ConsistentRF_dom_some mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.

Lemma Pref_ConsistentRF:
   (Crf : ConsistentRF (Lab o2) rf2),
    ConsistentRF (Lab o1) rf1.

Lemma Pref_ConsistentRFhb:
   (Crfhb : ConsistentRFhb mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    ConsistentRFhb mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.

Lemma Pref_ConsistentRF_na:
  
    (Crfhb : ConsistentRF_na mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    ConsistentRF_na mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.

Lemma Pref_sc_restr:
  same_relation _
    (sc_restr (Lab o1) sc1)
    (restr_rel (fun xIn x (Acts o1)) (sc_restr (Lab o2) sc2)).

Lemma Pref_SCrestriction:
   (Scr : SCrestriction mt2 MTSChb (Lab o2) (Sb o2) (Asw o2) rf2 mo2 sc2),
    SCrestriction mt2 MTSChb (Lab o1) (Sb o1) (Asw o1) rf1 mo1 sc1.

Lemma Pref_CoherentRR:
   (Crr : CoherentRR mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    CoherentRR mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.

Lemma Pref_CoherentWR:
   (Cwr : CoherentWR mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    CoherentWR mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.

Lemma Pref_CoherentRW:
   (Crw : CoherentRW mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    CoherentRW mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.

Lemma Pref_AtomicRMW:
   (Armw : AtomicRMW (Lab o2) rf2 mo2),
    AtomicRMW (Lab o1) rf1 mo1.

Lemma Pref_ConsistentAlloc:
   (Calloc: ConsistentAlloc (Lab o2)),
    ConsistentAlloc (Lab o1).

Lemma Pref_ConsistentDSB:
   (Cdsb : ConsistentDSB (Lab o2) (Sb o2) (Dsb o2)),
    ConsistentDSB (Lab o1) (Sb o1) (Dsb o1).

Lemma Pref_ConsistentSB:
   (Csb : ConsistentSB (Lab o2) (Sb o2)),
    ConsistentSB (Lab o1) (Sb o1).





Lemma Pref_hbUrfnaAcyclic:
  acyclic (fun a b
             happens_before mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2 a b
              rfna (Lab o2) rf2 a b) →
  acyclic (fun a b
             happens_before mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1 a b
              rfna (Lab o1) rf1 a b).

Lemma Pref_hbUrfAcyclic:
  acyclic (fun a b
             happens_before mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2 a b
              rf2 b = Some a) →
  acyclic (fun a b
             happens_before mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1 a b
              rf1 b = Some a).

Lemma Pref_dsbUrfAcyclic:
  acyclic (fun a bDsb o2 a b rf2 b = Some a) →
  acyclic (fun a bDsb o1 a b rf1 b = Some a).

Lemma Pref_AcyclicityAxiom :
   mt,
    AcyclicityAxiom mt mt2 (Lab o2) (Sb o2) (Dsb o2) (Asw o2) rf2 mo2
    AcyclicityAxiom mt mt2 (Lab o1) (Sb o1) (Dsb o1) (Asw o1) rf1 mo1.

Lemma Pref_Consistent :
   mt,
    Consistent mt mt2 MTSChb (Acts o2) (Lab o2) (Sb o2) (Dsb o2) (Asw o2) rf2 mo2 sc2
    Consistent mt mt2 MTSChb (Acts o1) (Lab o1) (Sb o1) (Dsb o1) (Asw o1) rf1 mo1 sc1.

Lemma Pref_Semiconsistent :
   mt,
    Semiconsistent mt mt2 MTSChb (Acts o2) (Lab o2) (Sb o2) (Dsb o2) (Asw o2) rf2 mo2 sc2
    Semiconsistent mt mt2 MTSChb (Acts o1) (Lab o1) (Sb o1) (Dsb o1) (Asw o1) rf1 mo1 sc1.

End Pref_Axioms.

Theorem Pref_Consistent2 :
   mt o1 o2 w,
    pref_opsem o1 o2
    upward_closed (fun x y : actidRf w y = Some x) ((In (A:=actid))^~ (Acts o1)) →
    pre_execution mt (MT2sb,MT3rf) MTSChb o2 w
     w',
      pre_execution mt (MT2sb,MT3rf) MTSChb o1 w'.

This page has been generated by coqdoc