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 :
forall mt2 lab sb rf rf' mo x y,
release_seq mt2 lab sb rf mo x y ->
(forall x (RMW: is_rmw (lab x)), rf' x = rf x) ->
release_seq mt2 lab sb rf' mo x y.
Proof.
unfold release_seq, NW; ins; desf; eauto.
destruct mt2; desf; induction H; ins; desf; desf;
try rewrite <- H0 in *; eauto using release_seq_alt.
Qed.
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 :
forall 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).
Proof.
ins; unfold lin_ext_a, fupd; repeat red; ins; desf; desf.
destruct (eqP a0 b) as [|M]; desf; eauto 8; eapply T in M; tauto.
destruct (eqP b0 b) as [|M]; desf; eauto 8; eapply T in M; tauto.
eapply T in NEQ; tauto.
Qed.
Lemma irreflexive_lin_ext_a :
forall X (rel : relation X)
(IRR: irreflexive rel)
a b (NEQ: a <> b)
(C: forall x, rel x a -> False)
(D: forall x, rel a x -> False) (cond : Prop),
irreflexive (lin_ext_a rel cond a b).
Proof.
unfold lin_ext_a; red; ins; desf; eauto.
Qed.
Lemma transitive_lin_ext_a :
forall (X: eqType) (rel : relation X)
(IRR: irreflexive rel)
(T: transitive _ rel) a b
(C: forall x, rel x a -> False)
(D: forall x, rel a x -> False) (cond : Prop),
transitive _ (lin_ext_a rel cond a b).
Proof.
unfold lin_ext_a; red; ins; desf; eauto 10;
exfalso; eauto.
Qed.
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 :
forall 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).
Proof.
ins; unfold lin_ext_b, fupd; repeat red; ins; desf; desf.
destruct (eqP a0 a) as [|M]; desf; eauto 8; eapply T in M; tauto.
destruct (eqP b0 a) as [|M]; desf; eauto 8; eapply T in M; tauto.
eapply T in NEQ; tauto.
Qed.
Lemma irreflexive_lin_ext_b :
forall X (rel : relation X)
(IRR: irreflexive rel)
a b (NEQ: a <> b)
(C: forall x, rel x b -> False)
(D: forall x, rel b x -> False) (cond : Prop),
irreflexive (lin_ext_b rel cond a b).
Proof.
unfold lin_ext_b; red; ins; desf; eauto.
Qed.
Lemma transitive_lin_ext_b :
forall (X: eqType) (rel : relation X)
(IRR: irreflexive rel)
(T: transitive _ rel) a b
(C: forall x, rel x b -> False)
(D: forall x, rel b x -> False) (cond : Prop),
transitive _ (lin_ext_b rel cond a b).
Proof.
unfold lin_ext_b; red; ins; desf; eauto 10;
exfalso; eauto.
Qed.
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 :
forall X (rel : relation X) (A: acyclic rel) (cond: Prop) a b
(C: forall x, rel x b -> cond -> x = a \/ rel x a),
transitive _ (lin_ext_c rel cond a b).
Proof.
unfold lin_ext_c; red; ins; desf; eauto using clos_trans.
by right; repeat split; eauto using clos_trans; intro; desf;
eapply t_rt_step in H0; desf; eapply C in H1; eauto;
desf; eauto using rt_t_trans, clos_trans.
by eapply t_rt_step in H; desf; eapply C in H0; eauto;
desf; eauto using rt_t_trans, clos_trans.
Qed.
Lemma irreflexive_lin_ext_c :
forall X (rel : relation X) (A: acyclic rel) cond a b,
irreflexive (lin_ext_c rel cond a b).
Proof.
unfold lin_ext_c; red; ins; desf; eauto.
Qed.
Lemma acyclic_lin_ext_c :
forall X (rel : relation X) (A: acyclic rel) (cond: Prop) a b
(C: forall x, rel x b -> cond -> x = a \/ rel x a),
acyclic (lin_ext_c rel cond a b).
Proof.
eauto using trans_irr_acyclic, irreflexive_lin_ext_c, transitive_lin_ext_c.
Qed.
Lemma lin_ext_c_extends :
forall X (rel : relation X) cond a b x y,
rel x y -> lin_ext_c rel cond a b x y.
Proof.
unfold lin_ext_c; eauto using t_step.
Qed.
Lemma release_seq_upd_mo :
forall 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: forall x, mo x x -> False)
(NMO: forall x, mo a x -> False)
(NMO: forall x, mo x a -> False)
(NRF: forall 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: forall 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.
Proof.
unfold lin_ext_a, release_seq, release_seq_elem, same_thread; ins;
destruct mt2 as [mt2 []]; ins.
case eqP; ins; clarify; des; clarify; rewrite ?TEQ in *; eauto using clos_trans;
try solve[exfalso; eauto 6]; unfold NW; try by right; repeat split; eauto using clos_trans.
desf;
try (rewrite t_step_rt in * |-; desf; eapply DOM in RSE; desf; eauto using clos_trans;
rewrite clos_refl_transE in *; desf; vauto);
right; repeat split; eauto using clos_trans;
ins; exploit RSO; eauto 6; intro Z; desf; eauto using clos_trans;
rewrite t_step_rt in Z; desf; eapply DOM in Z; desf;
eauto using t_rt_trans, clos_trans;
rewrite clos_refl_transE in Z0; desf; vauto; try solve [exfalso; eauto].
right; repeat split; ins; eauto;
ins; exploit RSO; eauto 6; intro Z; desf; eauto using clos_trans;
rewrite t_step_rt in Z; desf; eapply DOM in Z; desf;
eauto using t_rt_trans, clos_trans;
rewrite clos_refl_transE in Z0; desf; vauto; try solve [exfalso; eauto].
desf; desf;
induction RS; unfold same_thread in *; desf; ins; try destruct (eqP c a);
desf; try solve [exfalso; eauto]; rewrite ?TEQ in *; eauto using release_seq_alt.
rewrite t_step_rt in RSthr; desf; eapply DOM in RSthr; desf;
rewrite clos_refl_transE in *; desf; vauto; try solve [exfalso; eauto];
eapply RS_thr; try red; ins; eauto using clos_trans.
Qed.
Lemma release_seq_upd_ow :
forall 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: forall 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.
Proof.
ins.
eapply release_seq_upd_mo with (sb:=sb) (a:=a) in RS; eauto;
ins; desf; rewrite ?Ab; ins; desf;
kill_incons2 Aa Ab;
unfold release_seq, release_seq_elem, same_thread in *; ins; desf; desf; unfold NW; eauto; try right; desf;
kill_incons2 Aa Ab;
try (by repeat split; eauto; ins; exploit RSO; eauto; ins; desf; ins; desf; eauto;
rewrite Aa; ins; vauto);
try (by destruct mt2 as [[] []]; ins; desf; desf;
induction RS; unfold same_thread in *; ins; desf;
try destruct (eqP c a); desf; kill_incons2 Aa Ab;
eauto using release_seq_alt).
Qed.
Lemma OW_adj_hb :
forall 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: forall 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.
Proof.
ins; induction HB as [??[]|]; desf; eauto with hb;
unfold synchronizes_with, diff_thread in * |-; unfold NW; des; ins; clarify;
generalize (Crf _ _ RF); ins; desc;
eapply release_seq_upd_ow in RS; eauto; try (by intro; subst; rewrite Aa in *; ins);
repeat match goal with H: context[?a == ?b] |- _ => destruct (eqP a b) end;
ins; clarify; kill_incons2 Aa Ab;
try (by eapply t_step; vauto; right; left; red; unfold NW; eauto;
rewrite ?Ab; ins; des; eauto 24 using clos_trans).
eapply hb_trans with b; eauto with hb; apply sw_in_hb;
red; des; unfold NW, diff_thread; eauto; rewrite ?Ab; ins; eauto 14 using clos_trans.
eapply hb_trans with b; eauto with hb; apply sw_in_hb;
red; des; unfold NW, diff_thread; eauto; rewrite ?Ab; ins; eauto 14 using clos_trans.
by eapply sw_in_hb; red; unnw; do 2 right; left; repeat split; ins;
repeat eexists; try eexact RS; eauto using clos_trans;
instantiate; rewrite ?Ab; ins.
by eapply sw_in_hb; red; unnw; do 3 right; repeat split; ins;
repeat eexists; try eexact RS; eauto using clos_trans;
instantiate; rewrite ?Ab; ins.
Qed.
Lemma OW_adj_hb_a :
forall 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: forall x, sb a x -> x = b \/ sb b x)
(DOM': forall x, asw a x -> x = b \/ asw b x),
c = b \/ happens_before mt2 lab sb asw rf mo b c.
Proof.
unfold happens_before; intros; apply t_step_rt in HB; desc.
unfold synchronizes_with in HB; rewrite Aa in HB; ins; desf;
rewrite clos_refl_transE in HB0.
by apply DOM in HB; desf; eauto using clos_trans.
by apply DOM' in HB; desf; eauto 6 using clos_trans.
Qed.
Given two adjacent writes to the same location and with the same
access type, we can eliminate the first one.
Theorem OW_adjacent :
forall 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: forall x, sb a x -> x = b \/ sb b x)
(DOM': forall x, asw a x -> x = b \/ asw b x)
v' lab' (LAB': lab' = fupd lab a (Astore tid typ l v')),
exists mo' sc',
<< CONS': Semiconsistent mt mt2 MTSChb acts lab' sb dsb asw rf mo' sc' >> /\
<< OBS: forall 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 >>.
Proof.
ins; unfold Semiconsistent in *; desc.
assert (INa: In a acts) by (eapply or_introl, FIN in SBR; desf).
exists (lin_ext_a mo True a b), (lin_ext_a sc (typ = WATsc) a b).
subst; repeat apply conj; unfold NW; ins.
by unfold fupd in *; desf; desf; apply FIN.
by apply FIN.
by subst; intros x HB; eapply (IRR x); eapply OW_adj_hb; eauto.
{
unfold fupd in *; destruct mt; ins; unfold rfna in *;
intros x HB; eapply (ACYC x); revert HB;
generalize x at 1 3; induction 1; desf; vauto;
kill_incons2 Aa Ab;
eauto using t_step, OW_adj_hb.
}
by red; ins; eapply Csb in SB; unfold fupd; desf; ins; desf; rewrite ?Aa, ?Ab in *.
by eapply Cdsb.
by unfold fupd; desf; ins; revert DSB; apply Cdsb.
by unfold fupd; desf; ins; revert DSB; apply Cdsb.
by unfold fupd, lin_ext_a in *; ins; desf; desf; ins; eauto; kill_incons Aa Ab.
by dupdes Cmo; apply transitive_lin_ext_a; ins; kill_incons Aa Ab.
by dupdes Cmo; apply (is_total_lin_ext_a (fun x => is_writeL x l0));
ins; rewrite Ab; ins.
by dupdes Cmo; apply irreflexive_lin_ext_a; ins; kill_incons Aa Ab; congruence.
unfold fupd.
repeat red; ins; eapply (OW_adj_hb Crf) in REL; eauto.
desf; desf; ins; desf; eauto 6; try solve [exfalso; eauto using t_step].
by right; right; right; repeat split; ins; eapply CmoH; eauto; rewrite ?Ab; ins;
eapply t_trans; eauto; vauto.
by eapply (@OW_adj_hb_a mt2 lab sb) in REL; eauto;
desf; eauto; eapply CmoH in REL; eauto 6; rewrite ?Ab.
by eapply CmoH in REL; eauto.
by unfold lin_ext_a, fupd in *; ins; desf; desf; ins; eauto; kill_incons Aa Ab.
by dupdes Csc; apply transitive_lin_ext_a; ins; kill_incons Aa Ab.
by dupdes Csc; eapply (is_total_lin_ext_a (fun x => is_sc x));
ins; try rewrite Ab; ins; desf.
by dupdes Csc; eapply irreflexive_lin_ext_a; ins; kill_incons Aa Ab; congruence.
red in Csc; desc; unfold fupd in *.
red; ins; eapply (OW_adj_hb Crf) in REL; eauto.
red; desf; desf; ins; desf; eauto; try solve [exfalso; eauto using t_step].
by right; right; right; repeat split; ins; eapply Chbsc; eauto; rewrite ?Ab; ins;
eapply t_trans; eauto; vauto.
by eapply (@OW_adj_hb_a mt2 lab sb) in REL; eauto;
desf; eauto; eapply Chbsc in REL; eauto 6; rewrite ?Ab; ins.
dupdes Csc; desc; unfold lin_ext_a, fupd in *.
red; ins; desf; ins; desf; ins; kill_incons Aa Ab.
by eapply Cmosc in REL; eauto.
by eapply Cmosc in REL1; rewrite ?Ab; ins; eauto 6.
by eapply Cmosc in REL1; rewrite ?Ab; ins; eauto 6.
unfold fupd in *.
red; ins; desf; subst; kill_incons Aa Ab.
exploit Cscr; eauto.
unfold lin_ext_a, sc_restr_cond, immediate, sc_restr; intros X; des; [left|right];
desf; desf; split; ins; eauto;
desf; ins; desf; kill_incons Aa Ab; try rewrite Ab in *; ins.
by eapply (X0 c); ins.
by ins; eapply (X0 b); try rewrite Ab; ins.
by eapply (X0 x); ins; eauto using OW_adj_hb.
by eapply OW_adj_hb in HB; eauto; eapply (X0 b); rewrite ?Ab; ins;
eapply t_trans; vauto.
unfold fupd in *.
red; ins; eapply (OW_adj_hb Crf) in HB; eauto; desf; ins; desf; eauto.
by eapply (@OW_adj_hb_a mt2 lab sb) in HB; eauto; desf; eauto;
rewrite ?Ab in *; ins; eapply CrfN; eauto; instantiate; rewrite ?Ab; ins.
by unfold fupd in *;
red; ins; eapply Crf in RF; desf; ins; desf; rewrite ?Aa, ?Ab in *; ins; eauto.
by subst; red; ins; eapply CrfH; eauto using OW_adj_hb.
unfold fupd, lin_ext_a in *; red; ins; desf; desf; kill_incons Aa Ab;
eapply Crr; eauto using OW_adj_hb.
unfold fupd, lin_ext_a in *; red; ins; desf; desf; kill_incons Aa Ab; ins.
by eapply Cwr; eauto using OW_adj_hb.
eapply Cwr; try exact MO0; try exact RF; eauto; instantiate; rewrite ?Ab; ins.
eapply (OW_adj_hb Crf) in HB; eauto; desf; ins; desf; eauto.
eapply (@OW_adj_hb_a mt2 lab sb) in HB; eauto; desf; eauto; kill_incons Aa Ab.
unfold fupd, lin_ext_a in *; red; ins; desf; desf; kill_incons Aa Ab; ins.
by eapply Crw; eauto using OW_adj_hb.
by eapply CrfH; eauto; eapply t_trans; vauto; eapply OW_adj_hb; eauto.
by eapply Crw; try exact RF; try exact MO0; eauto; instantiate; rewrite ?Ab; ins;
eapply t_trans; vauto; eapply OW_adj_hb; eauto.
by unfold fupd, lin_ext_a in *; red; ins; desf; ins; edestruct Crmw; eauto; split; ins; eauto;
desf; eauto; kill_incons Aa Ab.
by unfold fupd in *; red; ins; desf; desf; eapply Ca; eauto.
by unfold fupd, lin_ext_a in *; ins; split; ins; desf; try tauto; rewrite ?Ab in *; ins;
eapply (loceq_mo Cmo) in H1; rewrite Ab in *; ins; desf.
unfold fupd in *.
red; ins.
edestruct H with (a0 := if a0 == a then b else a0) (b0 := if b0 == a then b else b0); eauto.
by des_if; ins; rewrite ?Ab; ins.
by des_if; ins; rewrite ?Ab; ins.
by des_if; ins; rewrite ?Ab; ins; subst; rewrite ?Aa in *; ins.
by des_if; ins; subst; rewrite ?Aa in *; ins.
by des_if; ins; subst; rewrite ?Aa in *; ins.
by des_if; ins; subst; rewrite ?Aa in *; ins.
by clear WRI NA; desf; desf; rewrite ?Aa in *; ins; eauto using OW_adj_hb.
by clear WRI NA; desf; desf; rewrite ?Aa in *; ins; eauto using OW_adj_hb.
Qed.
Corollary OW_adjacent_paper :
forall 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 ->
exists rf' mo' sc',
<< CONS': Consistent mt mt2 MTSChb acts lab' sb dsb asw rf' mo' sc' >> /\
<< OBS: forall 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' >>.
Proof.
unfold NW, adjacent; ins; desc; exploit OW_adjacent; eauto using Consistent_weaken;
ins; desf; try by destruct (eq_nat_dec x b); eauto.
eexists,,,; eauto using Consistent_restrict_rf; rewrite !racy_if_not_race_free;
intuition; eauto using race_free_restrict_rf.
Qed.
Lemma RAx_adj_hb_b :
forall 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: forall x, sb x b -> x = a \/ sb x a)
(DOM': forall x, asw x b -> x = a \/ asw x a),
c = a \/ happens_before mt2 lab sb asw rf mo c a.
Proof.
unfold happens_before; intros; apply t_rt_step in HB; desc.
unfold synchronizes_with in HB0; rewrite A in HB0; ins; desf;
rewrite clos_refl_transE in HB.
by apply DOM in HB0; desf; eauto using clos_trans.
by apply DOM' in HB0; desf; eauto 6 using clos_trans.
Qed.
Lemma RAx_adj_release_seq :
forall 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': forall x (RMW: is_rmw (lab x)), rf' x = rf x),
release_seq mt2 lab sb rf' mo x y.
Proof.
ins; eapply release_seq_only_rmw_rf_relevant, H'.
unfold release_seq, NW in *; ins; desf; desf; vauto;
try right; repeat (split; try done);
try by try apply (proj1 Cmo) in H; rewrite Ab in *; ins; desf.
unfold release_seq_elem, same_thread in *; desf; desf; ins; desf; eauto;
by try apply (proj1 Cmo) in H; rewrite Ab in *; ins; desf.
ins; unfold release_seq_elem, same_thread in *;
exploit H1; eauto; desf; desf; ins; desf; eauto;
by try apply (proj1 Cmo) in MA; rewrite Ab in *; ins; desf.
destruct mt2; desf; induction H; unfold same_thread in *; ins; desf; ins; desf;
eauto using release_seq_alt;
eapply RS_thr; ins; unfold same_thread; rewrite ?Ab; ins.
Qed.
Lemma RAW_adj_hb :
forall 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.
Proof.
ins; induction HB as [??[|[]]|]; eauto with hb.
unfold synchronizes_with, diff_thread in * |-; unfold NW; des; ins; clarify;
(eapply RAx_adj_release_seq with (rf' := rf) in RS; eauto;
[|by clear - Ab; ins; desf; desf; rewrite Ab in *; ins]);
repeat match goal with H: context[?a == ?b] |- _ => destruct (eqP a b) end;
ins; clarify; kill_incons2 Aa Ab;
try (by apply sw_in_hb; red; unnw;
first [left; repeat split; ins; [] |
right; left; repeat split; ins; [] |
do 2 right; left; repeat split; ins; [] |
do 3 right; repeat split; ins; [] ]; unfold same_thread;
repeat eexists; try eexact RS; eauto using clos_trans;
instantiate; rewrite ?Aa, ?Ab; ins);
destruct mt2; ins;
clear AT; try clear AT'; try clear AT'';
red in RS; unfold same_thread in *;
desf; desf; kill_incons2 Aa Ab; rewrite ?Aa in *; ins;
eauto using t_sb_in_hb, clos_trans;
try red in RSE; try inv RS; unfold same_thread in *; ins; desf; rewrite ?Aa in *; ins;
eauto 8 using t_sb_in_hb, clos_trans.
by apply Csb in SB; apply (clos_trans_eq _ Csb) in SBR;
rewrite Aa in *; ins; congruence.
by apply Csb in SB; apply (clos_trans_eq _ Csb) in SBR;
rewrite Aa in *; ins; congruence.
by apply Csb in SB; apply (clos_trans_eq _ Csb) in SBW;
rewrite Aa in *; ins; congruence.
by apply Csb in SB; apply (clos_trans_eq _ Csb) in SBW;
rewrite Aa in *; ins; congruence.
by apply Csb in SB; apply (clos_trans_eq _ Csb) in SBW;
apply (clos_trans_eq _ Csb) in SBR; rewrite Aa in *; ins; congruence.
by apply Csb in SB; apply (clos_trans_eq _ Csb) in SBW;
apply (clos_trans_eq _ Csb) in SBR; rewrite Aa in *; ins; congruence.
Qed.
Theorem RAW_adjacent :
forall 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: forall x, sb x b -> x = a \/ sb x a)
(DOM': forall 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),
exists 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 >>.
Proof.
intros; red in CONS; desc.
assert (INb: In b acts) by (eapply or_introl, FIN in SB; desf).
set (rf' := fun x => if x == b then Some a else rf x).
set (sc' := restr_rel (fun x => is_sc (lab' x)) (tot_ext acts
(lin_ext_c (fun x y => happens_before mt2 lab' sb asw rf' mo x y \/ sc x y)
(fst mt2 = MT2sb) a b))).
assert (ACYC' : acyclic
(fun x y =>
happens_before mt2
(fun x0 => if x0 == b then Aload tid typ' l v else lab x0) sb asw
(fun x0 => if x0 == b then Some a else rf x0) mo x y \/ sc x y)). {
clear sc' rf'.
dupdes Csc; repeat red; ins.
eapply cycle_decomp_u_total in H; try apply (is_total_lin_ext_b (fun x => is_sc x)); try edone.
des.
eapply clos_trans_of_transitive in H; try red; eauto using hb_trans.
by eapply IRR; eauto; instantiate; ins; desc; eauto using RAW_adj_hb.
eapply clos_trans_of_transitive in H0; eauto.
rewrite clos_refl_transE in H; desf; try subst n; eauto.
eapply clos_trans_of_transitive in H; try red; eauto using hb_trans; desc.
eapply RAW_adj_hb in H; eauto.
by eapply cycle_hbsc; eauto.
}
assert (IRRsc: irreflexive sc'). {
subst sc' rf' lab'; unfold restr_rel; red; ins.
apply proj1 in H.
eapply tot_ext_irr, H; eapply acyclic_lin_ext_c; ins; desf.
2: by exfalso; eapply (proj1 Csc) in H0; rewrite Ab in *; desf.
eapply t_rt_step in H0; desf.
by eapply DOM in H2; desf; [rewrite clos_refl_transE in *; desf; eauto|];
right; left; eapply t_rt_step; eauto.
cut (z = a \/ clos_trans _ sb z a).
by ins; rewrite clos_refl_transE in *; desf; eauto with hb.
clear - SB Aa H1 IRR H2.
red in H2; desf; try done; clear AT; ins; desf; try (by exfalso; eauto with hb);
by red in RS; red in SWthr; destruct mt2; ins; desf; desf; eauto using clos_trans;
try unfold release_seq_elem, same_thread in RSE; ins; desf; desf; eauto using clos_trans;
try rewrite Aa in *; ins; inv RS; desf; desf; eauto using clos_trans; try rewrite Aa in *; ins;
try unfold release_seq_elem, same_thread in *; ins; eauto using clos_trans.
by eapply DOM' in H2; desf; [rewrite clos_refl_transE in *; desf; eauto|];
right; left; eapply t_rt_step; eauto.
}
clear ACYC'.
exists rf', sc'; repeat apply conj; unfold NW; ins.
by clear IRRsc; desf; desf; apply FIN.
by apply FIN.
by subst rf' sc' lab'; red; ins; eapply (IRR x), RAW_adj_hb; eauto.
{
clear IRRsc; subst sc' lab' rf'.
destruct mt; ins; unfold rfna in *.
by intros x HB; eapply (ACYC x); revert HB;
generalize x at 1 3; induction 1; desf; vauto;
kill_incons Aa Ab;
eauto using t_step, RAW_adj_hb, t_sb_in_hb.
by intros x HB; eapply (ACYC x); revert HB;
generalize x at 1 3; induction 1; desf; vauto;
kill_incons Aa Ab;
eauto using t_step, RAW_adj_hb, t_sb_in_hb.
intros x HB.
cut (clos_trans actid ((fun a0 b0 => dsb a0 b0 \/ rf b0 = Some a0) UNION1 (a, b)) x x).
2: by revert HB; generalize x at 1 3; induction 1; desf; desf; eauto using clos_trans.
clear HB; intro HB; apply cycle_decomp_u1 in HB; desf; eauto.
apply clos_refl_transE in HB; desf; try congruence.
apply t_step_rt in HB; desf; kill_incons Aa Ab.
by apply (proj1 (proj2 Cdsb)) in HB; desf; rewrite ?Ab in *.
}
by subst sc' lab'; red; ins; eapply Csb in SB0; unfold fupd; desf; ins; desf; rewrite ?Aa, ?Ab in *.
by eapply Cdsb.
by subst sc' lab'; unfold fupd; desf; ins; revert DSB; apply Cdsb.
by subst sc' lab'; unfold fupd; desf; ins; revert DSB; apply Cdsb.
by clear IRRsc; ins; desf; desf; ins; eauto; kill_incons Aa Ab.
by dupdes Cmo; red; ins; desf;
eauto 6; exfalso; eauto; kill_incons Aa Ab.
by clear IRRsc; red; ins; desf; desf; ins; desf; eauto;
eapply Cmo in NEQ; eauto; tauto.
by clear IRRsc; dupdes Cmo; red; ins; desf; desf; eauto; try congruence;
kill_incons Aa Ab.
clear IRRsc; subst lab' rf'.
repeat red; ins; eapply (RAW_adj_hb Crf) in REL; eauto.
desf; desf; ins; desf; eauto; try solve [exfalso; eauto using t_step].
by eapply CmoH in REL; eauto.
by subst sc'; red in MO; tauto.
by subst sc'; apply restr_rel_trans, tot_ext_trans.
subst sc' rf' lab'.
apply is_total_restr; red; ins; eapply tot_ext_total; ins.
by desf; desf; apply FIN; intro X; rewrite X in *; ins; desf; desf.
by desf; desf; apply FIN; intro X; rewrite X in *; ins; desf; desf.
by red; ins; subst sc'; split; try done; apply tot_ext_extends; left; vauto.
by subst rf' sc' lab'; split; ins; desf; desf; kill_incons Aa Ab;
eapply Csc in REL; ins; apply tot_ext_extends; left; vauto.
{
subst rf' sc' lab'.
red; ins; desf; desf; kill_incons Aa Ab.
ins; desf.
case_eq (is_sc (lab a0)); [left|right].
rewrite Aa in *; ins; desf.
split.
unfold sc_restr, restr_rel; desf; desf; ins; desf.
by rewrite Aa in *; ins; intuition;
eapply tot_ext_extends, lin_ext_c_extends; eauto with hb.
unfold sc_restr, restr_rel; ins; desf; subst; eauto.
destruct (eqP c a0) as [|NEQ].
by subst c; eapply (IRRsc a0); split; ins; desf; ins.
eapply Csc in NEQ; ins; des.
by eapply IRRsc with a0; split; try eapply tot_ext_trans; eauto; desf; ins;
eauto using tot_ext_extends, lin_ext_c_extends.
by eapply IRRsc with b; split; try eapply tot_ext_trans; eauto; desf; ins;
apply tot_ext_extends; right; intuition.
unfold sc_restr, restr_rel; split; ins; desf; subst; eauto.
by eapply IRRsc with b; split; try eapply tot_ext_trans; eauto; desf; ins;
apply tot_ext_extends; right; intuition.
exploit Cscr; eauto.
unfold immediate, sc_restr; intros X; des; [left|right];
desf; desf; split; ins; eauto;
desf; ins; desf; kill_incons Aa Ab; try rewrite Ab in *; ins.
repeat (split; try done); desf; desf; try eapply tot_ext_extends, lin_ext_c_extends; eauto.
by eapply (proj1 Csc) in X; desc.
destruct (eqP a0 c) as [|NEQ]; desf; eauto.
destruct (eqP c b0) as [|NEQ']; desf; eauto.
red in R1; red in R2; desc.
desf; desf.
eapply Csc in NEQ; des; eapply Csc in NEQ'; des; try done.
by eapply X0; eauto.
by eapply IRRsc with b0; split; try eapply tot_ext_trans; eauto; desf; ins;
apply tot_ext_extends; eauto using lin_ext_c_extends.
by eapply IRRsc with a0; split; try eapply tot_ext_trans; eauto; desf; ins;
apply tot_ext_extends; eauto using lin_ext_c_extends.
by eapply IRRsc with a0; split; try eapply tot_ext_trans; eauto; desf; ins;
apply tot_ext_extends; eauto using lin_ext_c_extends.
destruct (eqP x b0) as [|NEQ]; desf; eauto.
red in SC0; desc; ins.
desf; desf.
eapply Csc in NEQ; des; ins.
by eapply X0; eauto using RAW_adj_hb.
by eapply IRRsc with b0; split; try eapply tot_ext_trans; eauto; desf; ins;
apply tot_ext_extends; eauto using lin_ext_c_extends.
}
by clear IRRsc; red; ins; subst lab' rf'; eapply (RAW_adj_hb Crf) in HB; eauto; desf; ins; desf; desf;
eauto.
by clear IRRsc; subst lab' rf' sc';
red; ins; desf; desf; ins; try eapply Crf in RF; desf; ins; desf; rewrite ?Aa, ?Ab in *; ins;
repeat eexists; eauto; intro HB; eapply (RAW_adj_hb Crf) in HB; eauto; ins;
eapply (ACYC b), t_step, or_introl, t_trans; vauto.
clear IRRsc; subst lab' rf' sc'.
red; ins; eapply (RAW_adj_hb Crf) in HB; eauto; desf; desf.
by eapply (IRR b), t_trans; vauto.
eby eapply CrfH.
clear IRRsc; subst lab' rf' sc'; red; ins; desf; desf; kill_incons Aa Ab;
eapply RAW_adj_hb in HB; eauto.
by eapply RAx_adj_hb_b with (sb := sb) in HB; eauto; desf; kill_incons Aa Ab;
eapply Crw; eauto;
exploit loceq_rf; eauto; exploit loceq_mo; eauto; instantiate; congruence.
by eapply Cwr in MO; try exact RFb; eauto using hb_trans, sb_in_hb;
exploit loceq_rf; eauto; exploit loceq_mo; eauto; instantiate; congruence.
by clear IRRsc; subst lab' rf' sc'; red; ins; desf; desf; kill_incons Aa Ab;
eapply RAW_adj_hb in HB; eauto;
eapply RAx_adj_hb_b with (sb := sb) in HB; eauto;
desf; kill_incons Aa Ab; eapply cycle_hbmo; eauto.
by clear IRRsc; subst lab' rf' sc'; red; ins; desf; desf; kill_incons Aa Ab; ins;
eapply RAW_adj_hb in HB; eauto; eapply cycle_hbmo; eauto using hb_trans, sb_in_hb.
by clear IRRsc; subst rf'; red; ins; desf; ins; edestruct Crmw; eauto; split; ins; eauto;
desf; eauto; kill_incons Aa Ab.
by clear IRRsc; red; ins; desf; desf; eapply Ca; eauto.
clear IRRsc; subst lab' rf' sc'.
red; ins.
edestruct H with (a0 := if a0 == b then a else a0) (b0 := if b0 == b then a else b0); eauto.
by des_if; ins; rewrite ?Aa; ins.
by des_if; ins; rewrite ?Aa; ins.
by des_if; ins; rewrite ?Aa; ins; subst; rewrite ?Ab in *; ins.
by des_if; ins; subst; rewrite ?Ab in *; ins.
by des_if; ins; subst; rewrite ?Ab in *; ins.
by des_if; ins; subst; rewrite ?Ab in *; ins.
by clear WRI NA; desf; desf; rewrite ?Ab in *; ins; eauto using RAW_adj_hb.
by clear WRI NA; desf; desf; rewrite ?Ab in *; ins; eauto using RAW_adj_hb.
Qed.
Corollary RAW_adjacent_paper :
forall 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) ->
exists 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 >>.
Proof.
unfold NW, adjacent; ins; desc; exploit RAW_adjacent; eauto using Consistent_weaken;
ins; desc; try (by destruct (eq_nat_dec x a); eauto); try (by desf).
eexists,,; eauto using Consistent_restrict_rf; rewrite !racy_if_not_race_free;
intuition; eauto using race_free_restrict_rf.
Qed.
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 :
forall 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.
Proof.
ins; induction HB as [??[|[]]|]; desf; eauto with hb.
unfold synchronizes_with, diff_thread in * |-; unfold NW; des; ins; clarify;
(eapply RAx_adj_release_seq with (rf' := rf) in RS; eauto;
[|by clear - Ab; ins; desf; desf; rewrite Ab in *; ins]); eauto;
repeat match goal with H: context[?a == ?b] |- _ => destruct (eqP a b) end;
ins; clarify; kill_incons2 Aa Ab;
try (by apply sw_in_hb; red; unnw; first_splitsok;
repeat eexists; try eexact RS; try eexact RF;
eauto using clos_trans;
instantiate; rewrite ?Aa, ?Ab; ins);
try (by eapply hb_trans with a; eauto with hb;
apply sw_in_hb; red; unnw; unfold diff_thread; rewrite ?Aa, ?Ab; ins;
first_splitsok;
repeat eexists; try eexact RS; try eexact RF;
eauto using clos_trans;
instantiate; rewrite ?Aa, ?Ab; ins).
Qed.
Theorem RAR_adjacent :
forall 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: forall x, sb x b -> x = a \/ sb x a)
(DOM: forall 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),
exists 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 >>.
Proof.
intros; red in CONS; desc.
assert (INb: In b acts) by (eapply or_introl, FIN in SBab; desf).
set (rf' := fun x => if x == b then rf a else rf x).
exists rf', (lin_ext_b sc (typ = RATsc) a b); repeat apply conj; unfold NW; ins.
by desf; desf; apply FIN.
by apply FIN.
by subst lab' rf'; intros x HB; eapply (IRR x);
eauto using t_step, RAR_adj_hb, sb_in_hb.
{
destruct mt; ins; unfold rfna in *.
subst lab' rf'; intros x HB; eapply (ACYC x); revert HB;
generalize x at 1 3; induction 1; desf; vauto;
kill_incons Aa Ab;
eauto using t_step, RAR_adj_hb, sb_in_hb.
by eapply t_trans; eapply t_step; eauto using sb_in_hb.
by ins; desf; eapply t_trans with a; eapply t_step;
rewrite ?Aa; ins; eauto using sb_in_hb.
subst lab' rf'; intros x HB; eapply (ACYC x); revert HB;
generalize x at 1 3; induction 1; desf; vauto;
kill_incons Aa Ab;
eauto using t_step, RAR_adj_hb, sb_in_hb.
by eapply t_trans; eapply t_step; eauto using sb_in_hb.
subst lab' rf'; intros x HB.
destruct (rf a) as [c|] eqn: RF.
cut (clos_trans actid ((fun a0 b0 => dsb a0 b0 \/ rf b0 = Some a0) UNION1 (c, b)) x x).
2: by revert HB; generalize x at 1 3; induction 1; desf; desf; eauto using clos_trans.
clear HB; intro HB; apply cycle_decomp_u1 in HB; desf; eauto.
apply clos_refl_transE in HB; desf; kill_incons Aa Ab.
apply t_step_rt in HB; desf; kill_incons Aa Ab.
by apply (proj1 (proj2 Cdsb)) in HB; desf; rewrite ?Ab in *.
eapply (ACYC x); revert HB;
generalize x at 1 3; induction 1; desf; vauto;
kill_incons Aa Ab;
eauto using t_step, RAR_adj_hb, sb_in_hb.
}
by red; ins; eapply Csb in SB; unfold fupd; desf; ins; desf; rewrite ?Aa, ?Ab in *.
by eapply Cdsb.
by unfold fupd; desf; ins; revert DSB; apply Cdsb.
by unfold fupd; desf; ins; revert DSB; apply Cdsb.
by ins; desf; desf; ins; eauto; kill_incons Aa Ab.
by dupdes Cmo; red; ins; desf;
eauto 6; exfalso; eauto; kill_incons Aa Ab.
by red; ins; desf; desf; ins; desf; eauto;
eapply Cmo in NEQ; eauto; tauto.
by dupdes Cmo; red; ins; desf; desf; eauto; try congruence;
kill_incons Aa Ab.
subst lab' rf'.
repeat red; ins; eapply (RAR_adj_hb Crf) in REL; eauto.
desf; desf; ins; desf; eauto; try solve [exfalso; eauto using t_step].
by eapply CmoH in REL; eauto.
by dupdes Csc; unfold lin_ext_b in *; ins; desf; desf; kill_incons Aa Ab.
by dupdes Csc; apply transitive_lin_ext_b; ins; kill_incons Aa Ab.
subst lab'.
by dupdes Csc; apply (is_total_lin_ext_b (fun x => is_sc x)); ins; eauto;
rewrite ?Aa; desf.
by dupdes Csc; apply irreflexive_lin_ext_b; try red; ins; desf; kill_incons Aa Ab.
{
dupdes Csc; subst rf' lab'; red; ins; eapply RAR_adj_hb in REL; eauto.
red; desf; ins; desf; eauto; try solve [exfalso; eauto using t_step].
by eapply RAx_adj_hb_b with (sb := sb) in REL; desf; eauto;
eapply Chbsc in REL; rewrite ?Aa; ins; eauto 8.
by right; right; left; repeat split; ins;
eapply Chbsc; rewrite ?Aa; ins; eauto using hb_trans, sb_in_hb.
}
by dupdes Csc; dupdes Cmo; subst rf' lab'; repeat red; ins;
desf; ins; desf; eauto; kill_incons Aa Ab; try solve [exfalso; eauto].
by unfold lin_ext_b in *; subst rf' lab'; red; ins; desf; desf; kill_incons Aa Ab; ins; desf;
exploit Cscr; eauto; instantiate; rewrite ?Aa; simpls; intro X;
unfold immediate, sc_restr in *; (des; [left|right]); repeat split; ins; desf; ins;
rewrite ?Aa in *; ins; eauto 8 using RAR_adj_hb; desf; kill_incons Aa Ab.
red; ins; subst lab' rf'; eapply RAR_adj_hb in HB; eauto;
desf; ins; desf; desf; eauto.
by eapply RAx_adj_hb_b with (sb := sb) (a:=a) in HB; eauto; desf;
rewrite ?Aa in *; ins; eauto; exploit CrfN; eauto; instantiate; rewrite ?Aa; ins.
by subst lab' rf';
red; ins; desf; desf; ins; try eapply Crf in RF; desf; ins; desf;
rewrite ?Aa, ?Ab in *; ins; desf;
repeat eexists; eauto.
by subst lab' rf';
red; ins; desf; desf; eapply (RAR_adj_hb Crf) in HB;
eauto using hb_trans, sb_in_hb.
subst lab' rf'; red; ins; desf; desf; kill_incons Aa Ab;
eapply RAR_adj_hb in HB; eauto; ins.
by eapply RAx_adj_hb_b with (sb := sb) in HB; eauto; desf; kill_incons Aa Ab;
eapply Crr; eauto; instantiate; rewrite Aa.
by desf; eapply Crr with (a:=a) (b:=b0); eauto using hb_trans, sb_in_hb;
eapply loceq_rf in RFa; eauto; eapply loceq_rf in RFb; eauto;
rewrite Aa in *; ins.
by subst lab' rf'; red; ins; desf; desf; kill_incons Aa Ab;
eapply RAR_adj_hb in HB; eauto;
eapply RAx_adj_hb_b with (sb := sb) in HB; eauto; desf;
desf; kill_incons Aa Ab; eapply Cwr; eauto; instantiate; rewrite Aa; ins.
by subst lab' rf'; red; ins; desf; desf; kill_incons Aa Ab; ins;
eapply RAR_adj_hb in HB; eauto;
desf; kill_incons Aa Ab; eapply Crw in MO; try exact RF; eauto using hb_trans, sb_in_hb;
instantiate; rewrite Aa; ins.
by subst rf'; red; ins; desf; ins; edestruct Crmw; eauto; split; ins; eauto;
desf; eauto; kill_incons Aa Ab.
by red; ins; desf; desf; eapply Ca; eauto.
subst lab' rf'.
red; ins.
edestruct H with (a0 := if a0 == b then a else a0) (b0 := if b0 == b then a else b0); eauto.
by des_if; ins; rewrite ?Aa; ins.
by des_if; ins; rewrite ?Aa; ins.
by des_if; ins; rewrite ?Aa; ins; subst; rewrite ?Ab in *; ins.
by des_if; ins; subst; rewrite ?Ab in *; ins.
by des_if; ins; subst; rewrite ?Ab in *; ins.
by des_if; ins; subst; rewrite ?Ab in *; ins.
by clear WRI NA; desf; desf; rewrite ?Ab in *; ins; eauto using RAR_adj_hb.
by clear WRI NA; desf; desf; rewrite ?Ab in *; ins; eauto using RAR_adj_hb.
Qed.
Corollary RAR_adjacent_paper :
forall 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 ->
exists 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 >>.
Proof.
unfold NW, adjacent; ins; desc; exploit RAR_adjacent; eauto using Consistent_weaken;
ins; desf; try by destruct (eq_nat_dec x a); eauto.
eexists,,; eauto using Consistent_restrict_rf; rewrite !racy_if_not_race_free;
intuition; eauto using race_free_restrict_rf.
Qed.
This page has been generated by coqdoc