Require Import Classical List Relations.
Require Import Vbase ExtraRelations cactions RAmodels.
Set Implicit Arguments.
Definition TSO_read_maximal lab sb rf (tso : relation actid) :=
∀ a b (TSO: tso a b) c (RF: rf c = Some a)
(HB: sb b c ∨ tso b c) (W: is_write (lab b))
(LOC: loc (lab a) = loc (lab b)),
False.
Definition of the TSO memory model using a memory order tso that is total on
stores.
Definition ConsistentTSO acts lab sb rf tso :=
≪ FIN : ExecutionFinite acts lab sb ≫ ∧
≪ CsbT: transitive sb ≫ ∧
≪ CrfD: ConsistentRF_dom lab rf ≫ ∧
≪ COrf: CompleteRF lab rf ≫ ∧
≪ CsbI: irreflexive sb ≫ ∧
≪ CtsoF: is_total (fun a ⇒ is_write (lab a)) tso ≫ ∧
≪ CtsoT: transitive tso ≫ ∧
≪ CtsoI: irreflexive tso ≫ ∧
≪ CpoIN: ∀ a b (PO: sb a b) (Aa: is_access (lab a)) (Ab: is_access (lab b)),
tso a b ∨ is_write_only (lab a) ∧ is_read_only (lab b) ≫ ∧
≪ CrfIN: ∀ a b (PO: rf b = Some a), tso a b ∨ sb a b ≫ ∧
≪ Cwr : TSO_read_maximal lab sb rf tso ≫.
Alternative definition of the TSO memory model using a modification order mo.
Definition TSO_alt_coherence_condition lab sb rf (mo: relation actid) :=
∀ a b (TSO: mo a b) c (RF: rf c = Some a)
(HB: happens_before sb rf b c ∨ mo b c ∨
(∃ m n, mo b m ∧ rf n = Some m ∧ ¬ sb m n ∧ sb n c) ∨
(∃ m, mo b m ∧ is_rmw (lab m) ∧ sb m c))
(LOC: loc (lab a) = loc (lab b)),
False.
Definition ConsistentTSOalt acts lab sb rf mo :=
≪ FIN : ExecutionFinite acts lab sb ≫ ∧
≪ CsbT: transitive sb ≫ ∧
≪ CrfD: ConsistentRF_dom lab rf ≫ ∧
≪ COrf: CompleteRF lab rf ≫ ∧
≪ ACYC: irreflexive (happens_before sb rf) ≫ ∧
≪ CmoD: ConsistentMO_big_dom lab mo ≫ ∧
≪ CmoF: is_total (fun a ⇒ is_write (lab a)) mo ≫ ∧
≪ CmoT: transitive mo ≫ ∧
≪ CmoI: irreflexive mo ≫ ∧
≪ Cww : CoherentWW sb rf mo ≫ ∧
≪ Cwr : TSO_alt_coherence_condition lab sb rf mo ≫.
We start with some helper lemmas about these definitions.
Lemma ConsistentTSO_hb :
∀ acts lab sb rf tso (C : ConsistentTSO acts lab sb rf tso)
a b (HB: happens_before sb rf a b)
(A: is_access (lab a)) (B: is_access (lab b)),
tso a b ∨ sb a b ∧ is_write_only (lab a) ∧ is_read_only (lab b).
Lemma ConsistentTSO_hb_no_access :
∀ acts lab sb rf tso (C : ConsistentTSO acts lab sb rf tso)
a b (HB: happens_before sb rf a b)
(A: is_access (lab b) = false),
sb a b ∨
(∃ d, tso a d ∧ is_write (lab a) ∧ is_read (lab d) ∧ sb d b) ∨
∃ c d, sb a c ∧ is_write (lab c) ∧ is_read (lab d) ∧ tso c d ∧ sb d b.
Lemma ConsistentTSOalt_hb :
∀ acts lab sb rf mo (C : ConsistentTSOalt acts lab sb rf mo) a b
(HB : clos_trans (fun a b ⇒ mo a b ∨ sb a b ∧ is_read (lab a)
∨ rf b = Some a ∧ ¬ sb a b) a b)
(W : is_write (lab a)),
happens_before sb rf a b ∨
mo a b ∨
(∃ m : actid, mo a m ∧ rf b = Some m ∧ ¬ sb m b) ∨
(∃ m n : actid, mo a m ∧ rf n = Some m ∧ ¬ sb m n ∧ sb n b) ∨
(∃ m : actid, mo a m ∧ is_rmw (lab m) ∧ sb m b).
Next, we show that the two definitions of TSO are equivalent.
First, the original definition is stronger than the alternative one.
Equivalence between the two TSO definitions
Theorem ConsistentTSO_alt1 :
∀ acts lab sb rf tso (C : ConsistentTSO acts lab sb rf tso),
ConsistentTSOalt acts lab sb rf (restr_rel (fun x ⇒ is_write (lab x)) tso).
Second, the alternative definition is stronger than the original one.
Theorem ConsistentTSO_alt2 :
∀ acts lab sb rf mo (C : ConsistentTSOalt acts lab sb rf mo),
ConsistentTSO acts lab sb rf
(clos_trans (fun a b ⇒ mo a b ∨ sb a b ∧ is_read (lab a)
∨ rf b = Some a ∧ ¬ sb a b)).
Putting the two directions together, the two definitions are equivalent.
Theorem ConsistentTSO_alternative :
∀ acts lab sb rf,
(∃ tso, ConsistentTSO acts lab sb rf tso) ↔
(∃ mo, ConsistentTSOalt acts lab sb rf mo).
Definition tso_protected_events lab sb rf (B : actid → Prop) :=
≪ PhbF : is_total B (happens_before sb rf) ≫ ∧
≪ Prace: ∀ a b (RACE: races_with lab sb rf a b), B a ∨ B b ≫ ∧
≪ Prfe : ∀ a b (RF: rf b = Some a) (NPO: ¬ sb a b), B a ∨ B b ≫.
Theorem tso_protected_sc_reduction :
∀ acts lab sb rf mo
(CONS: ConsistentRA acts lab sb rf mo)
(WF: wellformed_fences lab sb)
(NOUPD: ∀ a, ¬ is_rmw (lab a))
(NOWW: no_ww_races lab sb rf) B
(PR: tso_protected_events lab sb rf B),
∃ tso, ConsistentTSO acts lab sb rf tso.
This page has been generated by coqdoc