Require Import Peano_dec ClassicalDescription List Vbase Relations.
Require Import ExtraRelations actions c11 cmon coherence reorder.
Set Implicit Arguments.
Function update for functions of type actid → B. This is
defined on actid → B functions instead of arbitrary A → B
functions to work around a limitation of Coq's unification
Definition fupd B f (x : actid) (v : B) (y : actid) :=
if y == x then v else f y.
Lemma release_seq_only_rmw_rf_relevant :
∀ mt2 lab sb rf rf' mo x y,
release_seq mt2 lab sb rf mo x y →
(∀ x (RMW: is_rmw (lab x)), rf' x = rf x) →
release_seq mt2 lab sb rf' mo x y.
Helper lemmas for extending a strict total order
Definition lin_ext_a A (rel : relation A) (cond : Prop) (a b x y : A) :=
rel x y ∨
cond ∧ x = a ∧ y = b ∨
cond ∧ x = a ∧ rel b y ∨
cond ∧ y = a ∧ rel x b.
Lemma is_total_lin_ext_a :
∀ X (f: X → Prop) g rel
(T: is_total (fun y ⇒ f (g y)) rel)
a b v (C: f v → f (g b)) (cond : Prop) (C : f v → cond),
is_total (fun y ⇒ f (fupd g a v y)) (lin_ext_a rel cond a b).
Lemma irreflexive_lin_ext_a :
∀ X (rel : relation X)
(IRR: irreflexive rel)
a b (NEQ: a ≠ b)
(C: ∀ x, rel x a → False)
(D: ∀ x, rel a x → False) (cond : Prop),
irreflexive (lin_ext_a rel cond a b).
Lemma transitive_lin_ext_a :
∀ (X: eqType) (rel : relation X)
(IRR: irreflexive rel)
(T: transitive _ rel) a b
(C: ∀ x, rel x a → False)
(D: ∀ x, rel a x → False) (cond : Prop),
transitive _ (lin_ext_a rel cond a b).
Definition lin_ext_b A (rel : relation A) (cond : Prop) (a b x y : A) :=
rel x y ∨
cond ∧ x = a ∧ y = b ∨
cond ∧ x = b ∧ rel a y ∨
cond ∧ y = b ∧ rel x a.
Lemma is_total_lin_ext_b :
∀ X (f: X → Prop) g rel
(T: is_total (fun y ⇒ f (g y)) rel)
a b v (C: f v → f (g a)) (cond : Prop) (C : f v → cond),
is_total (fun y ⇒ f (fupd g b v y)) (lin_ext_b rel cond a b).
Lemma irreflexive_lin_ext_b :
∀ X (rel : relation X)
(IRR: irreflexive rel)
a b (NEQ: a ≠ b)
(C: ∀ x, rel x b → False)
(D: ∀ x, rel b x → False) (cond : Prop),
irreflexive (lin_ext_b rel cond a b).
Lemma transitive_lin_ext_b :
∀ (X: eqType) (rel : relation X)
(IRR: irreflexive rel)
(T: transitive _ rel) a b
(C: ∀ x, rel x b → False)
(D: ∀ x, rel b x → False) (cond : Prop),
transitive _ (lin_ext_b rel cond a b).
Definition lin_ext_c A (rel : relation A) (cond: Prop) (a b x y : A) :=
clos_trans _ rel x y ∨
cond ∧ x = b ∧ clos_trans _ rel a y ∧ y ≠ b.
Lemma transitive_lin_ext_c :
∀ X (rel : relation X) (A: acyclic rel) (cond: Prop) a b
(C: ∀ x, rel x b → cond → x = a ∨ rel x a),
transitive _ (lin_ext_c rel cond a b).
Lemma irreflexive_lin_ext_c :
∀ X (rel : relation X) (A: acyclic rel) cond a b,
irreflexive (lin_ext_c rel cond a b).
Lemma acyclic_lin_ext_c :
∀ X (rel : relation X) (A: acyclic rel) (cond: Prop) a b
(C: ∀ x, rel x b → cond → x = a ∨ rel x a),
acyclic (lin_ext_c rel cond a b).
Lemma lin_ext_c_extends :
∀ X (rel : relation X) cond a b x y,
rel x y → lin_ext_c rel cond a b x y.
Lemma release_seq_upd_mo :
∀ mt2 lab sb rf mo x y a b
(RS: release_seq mt2 lab sb rf (lin_ext_a mo True a b) x y)
(Cmo: ∀ x, mo x x → False)
(NMO: ∀ x, mo a x → False)
(NMO: ∀ x, mo x a → False)
(NRF: ∀ x, rf x = Some a → False)
(TEQ: thread (lab a) = thread (lab b))
(NAEQ: is_na (lab a) ↔ is_na (lab b))
(SB: sb a b)
(DOM: ∀ x, sb a x → x = b ∨ sb b x)
(NRMW: ¬ is_rmw (lab b))
(NEQ: y ≠ a),
if x == a then release_seq mt2 lab sb rf mo b y else release_seq mt2 lab sb rf mo x y.
Lemma release_seq_upd_ow :
∀ lab rf mo x y
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
a tid (Aa: lab a = Askip tid)
b typ l v (Ab: lab b = Astore tid typ l v) v'
(sb : relation actid) (SB: sb a b)
(DOM: ∀ x, sb a x → x = b ∨ sb b x) mt2
(RS: release_seq mt2 (fun x ⇒ if x == a then Astore tid typ l v' else lab x) sb
rf (lin_ext_a mo True a b) x y)
(NEQ: y ≠ a),
if x == a then release_seq mt2 lab sb rf mo b y else release_seq mt2 lab sb rf mo x y.
Lemma OW_adj_hb :
∀ lab mo rf x y
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
a tid (Aa: lab a = Askip tid)
b (sb : relation actid) (SB: sb a b)
(DOM: ∀ x, sb a x → x = b ∨ sb b x) asw
typ l v (Ab: lab b = Astore tid typ l v) mt2 v'
(HB: happens_before mt2 (fun x ⇒ if x == a then Astore tid typ l v' else lab x)
sb asw rf (lin_ext_a mo True a b) x y),
happens_before mt2 lab sb asw rf mo x y.
Lemma OW_adj_hb_a :
∀ mt2 lab sb asw rf mo a c
(HB: happens_before mt2 lab sb asw rf mo a c) tid
(Aa: lab a = Askip tid) b
(SBR: sb a b)
(DOM: ∀ x, sb a x → x = b ∨ sb b x)
(DOM': ∀ x, asw a x → x = b ∨ asw b x),
c = b ∨ happens_before mt2 lab sb asw rf mo b c.
Given two adjacent writes to the same location and with the same
access type, we can eliminate the first one.
Theorem OW_adjacent :
∀ mt (MT: mt ≠ MTorig) mt2 acts lab dsb sb asw rf mo sc
(CONS: Semiconsistent mt mt2 MTSChb acts lab sb dsb asw rf mo sc)
a tid (Aa: lab a = Askip tid)
b typ l v (Ab: lab b = Astore tid typ l v)
(SBR: sb a b)
(DOM: ∀ x, sb a x → x = b ∨ sb b x)
(DOM': ∀ x, asw a x → x = b ∨ asw b x)
v' lab' (LAB': lab' = fupd lab a (Astore tid typ l v')),
∃ mo' sc',
≪ CONS': Semiconsistent mt mt2 MTSChb acts lab' sb dsb asw rf mo' sc' ≫ ∧
≪ OBS: ∀ c d (INc: In c acts) (INd: In d acts)
(NLc: loc (lab c) ≠ l) (NLd: loc (lab d) ≠ l),
mo c d ↔ mo' c d ≫ ∧
≪ RACE: race_free mt2 lab' sb asw rf mo' → race_free mt2 lab sb asw rf mo ≫.
Corollary OW_adjacent_paper :
∀ mt mt2 acts lab dsb sb asw rf mo sc
tid typ l v a b v' lab',
Consistent mt mt2 MTSChb acts lab sb dsb asw rf mo sc →
sb a b →
adjacent sb a b →
adjacent asw a b →
lab a = Askip tid →
lab b = Astore tid typ l v →
lab' = fupd lab a (Astore tid typ l v') →
mt ≠ MTorig →
∃ rf' mo' sc',
≪ CONS': Consistent mt mt2 MTSChb acts lab' sb dsb asw rf' mo' sc' ≫ ∧
≪ OBS: ∀ c d (INc: In c acts) (INd: In d acts)
(NLc: loc (lab c) ≠ l) (NLd: loc (lab d) ≠ l),
mo c d ↔ mo' c d ≫ ∧
≪ RACE: racy mt2 lab sb asw rf mo → racy mt2 lab' sb asw rf' mo' ≫.
Lemma RAx_adj_hb_b :
∀ mt2 lab sb asw rf mo b c
(HB: happens_before mt2 lab sb asw rf mo c b) tid
(A: lab b = Askip tid) a
(SBR: sb a b)
(DOM: ∀ x, sb x b → x = a ∨ sb x a)
(DOM': ∀ x, asw x b → x = a ∨ asw x a),
c = a ∨ happens_before mt2 lab sb asw rf mo c a.
Lemma RAx_adj_release_seq :
∀ lab sb rf mo
(Cmo: ConsistentMO lab mo)
b tid (Ab: lab b = Askip tid)
mt2 typ l v x y
(H: release_seq mt2 (fun x ⇒ if x == b then Aload tid typ l v else lab x)
sb rf mo x y)
rf' (H': ∀ x (RMW: is_rmw (lab x)), rf' x = rf x),
release_seq mt2 lab sb rf' mo x y.
Lemma RAW_adj_hb :
∀ lab mo rf x y
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
a tid typ l v (Aa: lab a = Astore tid typ l v)
b (Ab: lab b = Askip tid)
(sb: relation actid) (SB: sb a b)
(Csb: ConsistentSB lab sb) asw typ' mt2
(HB: happens_before mt2 (fun x ⇒ if x == b then Aload tid typ' l v else lab x)
sb asw (fun x ⇒ if x == b then Some a else rf x) mo x y),
happens_before mt2 lab sb asw rf mo x y.
Theorem RAW_adjacent :
∀ mt (MT: mt ≠ MTorig) mt2 acts lab sb dsb asw rf mo sc
(CONS: Semiconsistent mt mt2 MTSChb acts lab sb dsb asw rf mo sc)
tid typ l v
a (Aa: lab a = Astore tid typ l v)
b (Ab: lab b = Askip tid)
(SB: sb a b)
(DOM: ∀ x, sb x b → x = a ∨ sb x a)
(DOM': ∀ x, asw x b → x = a ∨ asw x a)
lab' typ'
(SCtyp': typ' = RATsc → fst mt2 = MT2sb)
(LAB': lab' = fun x ⇒ if x == b then Aload tid typ' l v else lab x),
∃ rf' sc',
≪ CONS': Semiconsistent mt mt2 MTSChb acts lab' sb dsb asw rf' mo sc' ≫ ∧
≪ RACE: race_free mt2 lab' sb asw rf' mo → race_free mt2 lab sb asw rf mo ≫.
Corollary RAW_adjacent_paper :
∀ mt mt2 acts lab dsb sb asw rf mo sc tid typ typ' l v a b lab',
Consistent mt mt2 MTSChb acts lab sb dsb asw rf mo sc →
sb a b →
adjacent sb a b →
adjacent asw a b →
lab a = Astore tid typ l v →
lab b = Askip tid →
lab' = fupd lab b (Aload tid typ' l v) →
mt ≠ MTorig →
(fst mt2 = MT2sb ∨ typ' ≠ RATsc) →
∃ rf' sc',
≪ CONS': Consistent mt mt2 MTSChb acts lab' sb dsb asw rf' mo sc' ≫ ∧
≪ RACE: racy mt2 lab sb asw rf mo → racy mt2 lab' sb asw rf' mo ≫.
Ltac first_splitsok :=
first [left; repeat split; unfold same_thread; ins; [] |
right; left; repeat split; unfold same_thread; ins; [] |
do 2 right; left; repeat split; unfold same_thread; ins; [] |
do 3 right; repeat split; unfold same_thread; ins; [] ].
Lemma RAR_adj_hb :
∀ lab mo rf x y
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
a tid typ l v (Aa: lab a = Aload tid typ l v)
b (Ab: lab b = Askip tid)
(sb : relation actid) (SB: sb a b) mt2 asw
(HB: happens_before mt2 (fun x ⇒ if x == b then Aload tid typ l v else lab x)
sb asw (fun x ⇒ if x == b then rf a else rf x) mo x y),
happens_before mt2 lab sb asw rf mo x y.
Theorem RAR_adjacent :
∀ mt (MT: mt ≠ MTorig) mt2 acts lab sb dsb asw rf mo sc
(CONS: Semiconsistent mt mt2 MTSChb acts lab sb dsb asw rf mo sc)
tid typ l v
a (Aa: lab a = Aload tid typ l v)
b (Ab: lab b = Askip tid)
(SBab: sb a b)
(DOM: ∀ x, sb x b → x = a ∨ sb x a)
(DOM: ∀ x, asw x b → x = a ∨ asw x a)
lab' (LAB': lab' = fun x ⇒ if x == b then Aload tid typ l v else lab x),
∃ rf' sc',
≪ CONS': Semiconsistent mt mt2 MTSChb acts lab' sb dsb asw rf' mo sc' ≫ ∧
≪ RACE: race_free mt2 lab' sb asw rf' mo → race_free mt2 lab sb asw rf mo ≫.
Corollary RAR_adjacent_paper :
∀ mt mt2 acts lab dsb sb asw rf mo sc tid typ l v a b lab',
Consistent mt mt2 MTSChb acts lab sb dsb asw rf mo sc →
sb a b →
adjacent sb a b →
adjacent asw a b →
lab a = Aload tid typ l v →
lab b = Askip tid →
lab' = fupd lab b (Aload tid typ l v) →
mt ≠ MTorig →
∃ rf' sc',
≪ CONS': Consistent mt mt2 MTSChb acts lab' sb dsb asw rf' mo sc' ≫ ∧
≪ RACE: racy mt2 lab sb asw rf mo → racy mt2 lab' sb asw rf' mo ≫.
This page has been generated by coqdoc