Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 permission path fslassn fslassnsem fslmodel fslassnlemmas fslhmap.
Set Implicit Arguments.
Helper lemmas for establishing the synchronization paths.
Lemma step_from_normal PS PSg:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
edge1 (EV: edge_valid lab sb rf edge1) b (B: hb_snd edge1 = Some b)
hmap ga (VALID: hmap_valid lab sb rf hmap ga b) hf1 g1 (MAP: hmap edge1 = Hdef hf1 g1)
l (ALL: hf1 l ≠ @HVnone PS PSg) (LAB: HVlabeled (hf1 l) HLnormal),
is_sb edge1 ∧
∃ edge2 hf2 g2, hb_snd edge1 = Some (hb_fst edge2) ∧ edge_valid lab sb rf edge2 ∧
hmap edge2 = Hdef hf2 g2 ∧ hf2 l ≠ @HVnone PS PSg ∧
(HVlabeled (hf2 l) HLnormal ∧ ¬ is_rf edge2 ∨
HVlabeled (hf2 l) HLtriangle ∧ is_sb edge2 ∧ is_release_fence (lab (hb_fst edge2)) ∨
HVlabeled (hf2 l) HLnabla ∧ ¬ is_sb edge2 ∧ is_release_write (lab (hb_fst edge2))).
Proof.
ins.
assert (edge1NOTrf: ¬ is_rf edge1).
{
destruct edge1; ins; desf.
intro; eapply no_normals_on_rf2; eauto.
}
unfold hmap_valid, unique in VALID;
desfh; desc; try (destruct DISJ; desc); destruct edge1; ins; (split; [done |]); try revert TYP; desfh;
rewrite ?(pU0 _ EV), ?MAP in *; desfh.
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
assert (D := hplus_def_inv_l _ _ EQ); desf; rewrite D in ×.
symmetry in D; eapply hsum_preserves_label in D; eauto; desf.
2: by repeat (rewrite In_map; eexists; split; try edone); apply pOK.
symmetry in EQ; eapply hplus_preserves_label in EQ; eauto; desf.
eapply hplus_preserves_label_inv in DEF; eauto; desf.
× symmetry in DEF; eapply hsum_preserves_label_inv in DEF; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_sb b _), _, _; repeat split; ins; eauto.
eby apply qOK.
× eexists (hb_sink b), _, _; repeat split; ins; eauto.
by red; rewrite Heq.
}
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
eapply hplus_preserves_label with (l := l) in qEQ; eauto; desf;
try (by unfold hupd; desf; desf).
eexists (hb_sb b _), _, _; repeat split; ins; eauto.
}
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
eapply hplus_preserves_label with (l := l) in qEQ; eauto; desf;
try (eby unfold hupd; desf; desf).
eexists (hb_sb b _), _, _; repeat split; ins; eauto.
}
{
rewrite hdef_alt in qD; desf; rewrite qD in ×.
eapply hplus_preserves_label in qEQ; eauto; desf.
eexists (hb_sb b _), _, _; repeat split; ins; eauto.
}
{
ins; clear TYP.
apply hdef_alt in qD; desf; rewrite qD in ×.
destruct (classic (l = l0)); desf.
× eexists (hb_sb b _), _, _; repeat split; ins; eauto.
by intro; eapply hplus_nalloc in qEQ; eauto; desf; rewrite hupds in ×.
eapply (hplus_preserves_label _ _ _ _ HLnormal) in qEQ; try (by rewrite hupds; vauto).
desf; eauto.
× eapply hplus_preserves_label_inv in pEQ'; eauto; desf.
by unfold hupd in *; desf; desf.
rewrite !(hplusAC (Hdef hf' _)) in qEQ.
eapply hplus_preserves_label in qEQ; eauto; desf.
eexists (hb_sb b _), _, _; repeat split; ins; eauto.
}
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
eexists (hb_sb b _), _, _; repeat (split; eauto; []).
apply hplus_gheap in qEQ; desf; ins.
unfold hupd; desf; desf; eauto.
split; try done.
left; split; ins.
by apply Pfull_is_not_Pzero.
}
{
rewrite (initialize_alloc _ _ l0) in ALL.
apply (initialize_preserves_label _ _ l0) in LAB.
symmetry in UPD; eapply hplus_preserves_label_inv in UPD; eauto; desfh.
× ins; clear TYP.
apply hplus_not_undef_l, hdef_alt in DEF; desf; rewrite DEF in ×.
eapply hplus_preserves_label in qEQ; eauto; desf.
eexists (hb_sb b _), _, _; repeat split; ins; eauto.
× eapply hplus_preserves_label_inv in UPD; eauto; desfh.
+ apply hplus_not_undef_l, hdef_alt in DEF; desf; rewrite DEF in ×.
rewrite hplusAC in qEQ; eapply hplus_preserves_label in qEQ; eauto; desf.
eexists (hb_sb b _), _, _; repeat split; ins; eauto.
+ ins; desf.
by exploit label_is_consistent_with_exact_label_spec; eauto.
red in rfsSIM; desf.
symmetry in rfsSIM0; eapply hplus_preserves_label in rfsSIM0; eauto; desf.
eapply HFsim_alloc_label in rfsSIM1; eauto; desf.
eapply hplus_preserves_label_inv in rfsSIM; eauto; desf.
- symmetry in rfsSIM; eapply hsum_preserves_label_inv in rfsSIM; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_rf b _), _, _; ins; repeat split; eauto.
by apply rfsOK.
right; right; repeat split; try done.
2: by rewrite Heq; ins; desf.
apply exact_label_hplus_dist in TRAN; desf.
eapply exact_label_hsum_dist in TRAN.
2: by repeat (rewrite In_map; eexists; split; try edone); apply rfsOK.
exploit label_is_consistent_with_exact_label_spec; eauto; ins; instantiate; congruence.
- eexists (hb_sink b), _, _; ins; repeat split; eauto.
by red; rewrite Heq.
right; right; repeat split; try done.
2: by rewrite Heq; ins; desf.
rewrite rfsSIM in TRAN; apply exact_label_hplus_dist in TRAN; desf.
exploit label_is_consistent_with_exact_label_spec; eauto; ins; instantiate; congruence.
}
{
symmetry in pEQ; eapply hplus_preserves_label_inv in pEQ; eauto; desf.
× apply hplus_not_undef_l, hdef_alt in DEF; desf; rewrite DEF in ×.
eexists (hb_sb b _ ), _, _; do 3 (split; try edone).
unfold hupd in pEQ1; desf; desf.
eapply hplus_preserves_label in qEQ; try rewrite hupds; ins.
2: by instantiate (1 := HLnormal); vauto.
desf; eauto.
× eapply hplus_preserves_label_inv in pEQ; eauto; desf.
+ rewrite Hsim_sym in RELsim; eapply Hsim_alloc_label in RELsim; eauto; desf.
apply exact_label_hplus_dist in TRANout; desf.
exploit label_is_consistent_with_exact_label_spec; eauto; ins; desf.
apply hplus_not_undef_r, hdef_alt in DEF; desf; rewrite DEF in ×.
eapply hplus_preserves_label in rOutEQ; eauto; desf.
red in RELlabel; desf.
by exploit label_is_consistent_with_exact_label_spec; try exact RELlabel; eauto.
eapply hplus_preserves_label_inv in DEF; eauto; desf.
- symmetry in DEF; eapply hsum_preserves_label_inv in DEF; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_rf b _ ), _, _; repeat split; eauto; ins.
by apply rfsOutOK.
rewrite Heq; ins; desf; eauto.
- eexists (hb_sink b), _, _; repeat split; eauto; ins.
by red; rewrite Heq.
rewrite Heq; ins; desf; eauto.
+ apply hplus_not_undef_l, hdef_alt in DEF; desf; rewrite DEF in ×.
eexists (hb_sb b _ ), _, _; do 3 (split; try edone).
rewrite !(hplusAC (Hdef hf'0 _)) in qEQ.
eapply hplus_preserves_label in qEQ; ins; desf; eauto.
}
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
eexists (hb_sb b _), _, _; do 3 (split; try edone).
symmetry in pEQ; eapply hplus_preserves_label_inv in pEQ; eauto; desf.
× eapply hplus_preserves_label in qEQ; eauto; desf; eauto.
× eapply hplus_preserves_label_inv in pEQ; eauto; desf.
+ rewrite Hsim_sym in RELsim; eapply Hsim_alloc_label in RELsim; eauto; desf.
exploit label_is_consistent_with_exact_label_spec; eauto; ins; desf.
rewrite hplusAC in qEQ; eapply hplus_preserves_label in qEQ; eauto; desf.
split; try done.
right; left; repeat split; try done.
rewrite Heq; ins; desf.
exploit ACQ; ins.
inv x.
+ rewrite Hsim_sym in ACQsim; eapply Hsim_alloc_label in ACQsim; eauto; desf.
exploit label_is_consistent_with_exact_label_spec; eauto; ins; desf.
rewrite !(hplusAC (Hdef hf'1 _)) in qEQ; eapply hplus_preserves_label in qEQ; eauto; desf; eauto.
}
Qed.
Lemma step_from_triangle PS PSg:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
edge1 (EV: edge_valid lab sb rf edge1) b (B: hb_snd edge1 = Some b)
hmap ga (VALID: hmap_valid lab sb rf hmap ga b) hf1 g1 (MAP: hmap edge1 = Hdef hf1 g1)
l (ALL: hf1 l ≠ @HVnone PS PSg) (LAB: HVlabeled (hf1 l) HLtriangle),
is_sb edge1 ∧
∃ edge2 hf2 g2, hb_snd edge1 = Some (hb_fst edge2) ∧ edge_valid lab sb rf edge2 ∧
hmap edge2 = Hdef hf2 g2 ∧ hf2 l ≠ @HVnone PS PSg ∧
(HVlabeled (hf2 l) HLtriangle ∧ ¬ is_rf edge2 ∨
HVlabeled (hf2 l) HLnabla ∧ ¬ is_sb edge2 ∧ is_write (lab (hb_fst edge2)) ∨
HVlabeled (hf2 l) HLnabla ∧ is_sink edge2).
Proof.
ins.
assert (edge1NOTrf: ¬ is_rf edge1).
{
destruct edge1; ins; desf.
exploit triangles_never_on_rf2; try exact MAP1; eauto; ins.
eby eexists; split.
}
unfold hmap_valid, unique in VALID;
desfh; desc; try (destruct DISJ; desc); destruct edge1; ins; (split; [done |]); try revert TYP; desfh;
rewrite ?(pU0 _ EV), ?MAP in *; desfh.
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
assert (D := hplus_def_inv_l _ _ EQ); desf; rewrite D in ×.
symmetry in D; eapply hsum_preserves_label in D; eauto; desf.
2: by repeat (rewrite In_map; eexists; split; try edone); apply pOK.
symmetry in EQ; eapply hplus_preserves_label in EQ; eauto; desf.
eapply hplus_preserves_label_inv in DEF; eauto; desf.
× symmetry in DEF; eapply hsum_preserves_label_inv in DEF; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_sb b _), _, _; repeat split; ins; eauto.
eby apply qOK.
× eexists (hb_sink b), _, _; repeat split; ins; eauto.
by red; rewrite Heq.
}
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
apply hplus_gheap in qEQ; desf.
eexists (hb_sb b _), _, _; repeat split; ins; eauto; unfold hupd; desf; desf; eauto.
}
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
apply hplus_gheap in qEQ; desf.
eexists (hb_sb b _), _, _; repeat split; ins; eauto; unfold hupd; desf; desf; eauto.
}
{
rewrite hdef_alt in qD; desf; rewrite qD in ×.
eapply hplus_preserves_label in qEQ; eauto; desf.
eexists (hb_sb b _), _, _; repeat split; ins; eauto.
}
{
ins; clear TYP.
apply hdef_alt in qD; desf; rewrite qD in ×.
eexists (hb_sb b _), _, _; do 3 (split; try edone).
eapply hplus_preserves_label_inv in pEQ'; eauto; desf.
by clear - pEQ'0 pEQ'1; unfold hupd in *; desf; desf; ins; unfold is_triangle in *; desf.
rewrite !(hplusAC (Hdef hf' _)) in qEQ.
eapply hplus_preserves_label in qEQ; desf; eauto.
}
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
apply hplus_gheap in qEQ; desf.
eexists (hb_sb b _), _, _; repeat split; ins; eauto; unfold hupd; desf; desf; eauto.
exploit labeled_lvalue; eauto; ins.
}
{
rewrite (initialize_alloc _ _ l0) in ALL.
apply (initialize_preserves_label _ _ l0) in LAB.
symmetry in UPD; eapply hplus_preserves_label_inv in UPD; eauto; desfh.
× ins; clear TYP.
apply hplus_not_undef_l, hdef_alt in DEF; desf; rewrite DEF in ×.
eapply hplus_preserves_label in qEQ; eauto; desf.
eexists (hb_sb b _), _, _; repeat split; ins; eauto.
× eapply hplus_preserves_label_inv in UPD; eauto; desfh.
+ apply hplus_not_undef_l, hdef_alt in DEF; desf; rewrite DEF in ×.
rewrite hplusAC in qEQ; eapply hplus_preserves_label in qEQ; eauto; desf.
eexists (hb_sb b _), _, _; repeat split; ins; eauto.
+ ins; desf.
2: by exploit label_is_consistent_with_exact_label_spec; eauto.
red in rfsSIM; desf.
symmetry in rfsSIM0; eapply hplus_preserves_label in rfsSIM0; eauto; desf.
eapply HFsim_alloc_label in rfsSIM1; eauto; desf.
rewrite rfsSIM in TRAN; exploit label_is_consistent_with_exact_label_spec; eauto; ins; desf.
eapply hplus_preserves_label_inv in rfsSIM; eauto; desf.
- symmetry in rfsSIM; eapply hsum_preserves_label_inv in rfsSIM; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_rf b _), _, _; ins; repeat split; eauto.
by apply rfsOK.
rewrite Heq; ins; eauto.
- eexists (hb_sink b), _, _; ins; repeat split; eauto.
by red; rewrite Heq.
}
{
symmetry in pEQ; eapply hplus_preserves_label_inv in pEQ; eauto; desf.
by clear - pEQ0 pEQ1; unfold hupd in *; desf; desf; ins; unfold is_triangle in *; desf.
eapply hplus_preserves_label_inv in pEQ; eauto; desf.
× rewrite Hsim_sym in RELsim; eapply Hsim_alloc_label in RELsim; eauto; desf.
apply exact_label_hplus_dist in TRANout; desf.
exploit label_is_consistent_with_exact_label_spec; eauto; ins; desf.
apply hplus_not_undef_r, hdef_alt in DEF; desf; rewrite DEF in ×.
eapply hplus_preserves_label in rOutEQ; eauto; desf.
red in RELlabel; desf.
2: by exploit label_is_consistent_with_exact_label_spec; try exact RELlabel1; eauto.
eapply hplus_preserves_label_inv in DEF; eauto; desf.
+ symmetry in DEF; eapply hsum_preserves_label_inv in DEF; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_rf b _ ), _, _; repeat split; eauto; ins.
by apply rfsOutOK.
rewrite Heq; ins; desf; eauto.
+ eexists (hb_sink b), _, _; repeat split; eauto; ins.
by red; rewrite Heq.
× apply hplus_not_undef_l, hdef_alt in DEF; desf; rewrite DEF in ×.
eexists (hb_sb b _ ), _, _; do 3 (split; try edone).
rewrite !(hplusAC (Hdef hf'0 _)) in qEQ.
eapply hplus_preserves_label in qEQ; ins; desf; eauto.
}
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
eexists (hb_sb b _), _, _; do 3 (split; try edone).
symmetry in pEQ; eapply hplus_preserves_label_inv in pEQ; eauto; desf.
by eapply hplus_preserves_label in qEQ; eauto; desf; eauto.
by eapply hplus_preserves_label_inv in pEQ; eauto; desf;
exploit label_is_consistent_with_exact_label_spec; eauto; ins.
}
Qed.
Lemma step_from_nabla PS PSg:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
edge1 (EV: edge_valid lab sb rf edge1) b (B: hb_snd edge1 = Some b)
hmap ga (VALID: hmap_valid lab sb rf hmap ga b) hf1 g1 (MAP: hmap edge1 = Hdef hf1 g1)
l (ALL: hf1 l ≠ @HVnone PS PSg) (LAB: HVlabeled (hf1 l) HLnabla),
∃ edge2 hf2 g2, hb_snd edge1 = Some (hb_fst edge2) ∧ edge_valid lab sb rf edge2 ∧
hmap edge2 = Hdef hf2 g2 ∧ hf2 l ≠ @HVnone PS PSg ∧
(HVlabeled (hf2 l) HLnabla ∧ ¬ is_rf edge2 ∨
is_rf edge1 ∧ HVlabeled (hf2 l) HLnormal ∧ ¬ is_rf edge2 ∧ is_acquire_read (lab (hb_fst edge2)) ∨
is_sb edge1 ∧ HVlabeled (hf2 l) HLnormal ∧ is_sb edge2 ∧ is_acquire_fence (lab (hb_fst edge2)) ∨
is_rf edge1 ∧ HVlabeled (hf2 l) HLnabla ∧ ¬ is_sb edge2 ∧ is_rmw (lab (hb_fst edge2))).
Proof.
ins.
unfold hmap_valid, unique in VALID;
desfh; desc; try (destruct DISJ; desc); destruct edge1; ins; try revert TYP; desfh;
rewrite ?(pU0 _ EV), ?MAP in *; desfh;
try (by specialize (CONS_RF b); rewrite EV, Heq in CONS_RF; desf);
try (by rewrite rEQ in MAP; inv MAP).
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
assert (D := hplus_def_inv_l _ _ EQ); desf; rewrite D in ×.
symmetry in D; eapply hsum_preserves_label in D; eauto; desf.
2: by repeat (rewrite In_map; eexists _; split; try edone); apply pOK.
symmetry in EQ; eapply hplus_preserves_label in EQ; eauto; desf.
eapply hplus_preserves_label_inv in DEF; eauto; desf.
× symmetry in DEF; eapply hsum_preserves_label_inv in DEF; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_sb b _), _, _; repeat split; ins; eauto.
eby apply qOK.
× eexists (hb_sink b), _, _; repeat split; ins; eauto.
by red; rewrite Heq.
}
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
apply hplus_gheap in qEQ; desf.
eexists (hb_sb b _), _, _; repeat split; ins; eauto; unfold hupd; desf; desf; eauto.
}
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
apply hplus_gheap in qEQ; desf.
eexists (hb_sb b _), _, _; repeat split; ins; eauto; unfold hupd; desf; desf; eauto.
}
{
rewrite hdef_alt in qD; desf; rewrite qD in ×.
eapply hplus_preserves_label in qEQ; eauto; desf.
eexists (hb_sb b _), _, _; repeat split; ins; eauto.
}
{
ins; clear TYP.
apply hdef_alt in qD; desf; rewrite qD in ×.
eexists (hb_sb b _), _, _; do 3 (split; try edone).
eapply hplus_preserves_label_inv in pEQ'; eauto; desf.
by clear - pEQ'0 pEQ'1; unfold hupd in *; desf; desf; ins; unfold is_nabla in *; desf.
rewrite !(hplusAC (Hdef hf' _)) in qEQ.
eapply hplus_preserves_label in qEQ; desf; eauto.
}
{
apply hdef_alt in qD; desf; rewrite qD in ×.
eexists (hb_sb b _), _, _; do 3 (split; try edone). revert TYP.
red in TRAN; desf; rewrite TRAN in ×.
symmetry in TRAN; eapply hsum_preserves_label in TRAN; eauto; desf.
2: by repeat (rewrite In_map; eexists; split; try edone); apply rfsOK.
rewrite Hsim_sym in rfsSIM; eapply Hsim_alloc_label in rfsSIM; eauto; desf.
rewrite hplusAC in qEQ; eapply hplus_preserves_label in qEQ; eauto; desf.
by simpl; rewrite Heq; ins; desfh; exploit label_is_consistent_with_exact_label_spec; try exact rfsSIM1; eauto;
ins; subst lbl'; desf; eauto 8.
}
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
apply hplus_gheap in qEQ; desf.
eexists (hb_sb b _), _, _; repeat split; ins; eauto; unfold hupd; desf; desf; eauto.
exploit labeled_lvalue; eauto; ins.
}
{
rewrite (initialize_alloc _ _ l0) in ALL.
apply (initialize_preserves_label _ _ l0) in LAB.
symmetry in UPD; eapply hplus_preserves_label_inv in UPD; eauto; desfh.
× ins; clear TYP.
apply hplus_not_undef_l, hdef_alt in DEF; desf; rewrite DEF in ×.
eexists (hb_sb b _), _, _; repeat (split; eauto; []).
eapply hplus_preserves_label in qEQ; eauto; desf; eauto.
× eapply hplus_preserves_label_inv in UPD; eauto; desfh.
+ ins; clear TYP.
apply hplus_not_undef_l, hdef_alt in DEF; desf; rewrite DEF in ×.
eexists (hb_sb b _), _, _; repeat (split; eauto; []).
rewrite hplusAC in qEQ; eapply hplus_preserves_label in qEQ; eauto; desf; eauto.
+ by ins; desf; exploit label_is_consistent_with_exact_label_spec; eauto.
}
{
symmetry in pEQ; eapply hplus_preserves_label_inv in pEQ; eauto; desf.
by by clear - pEQ0 pEQ1; unfold hupd in *; desf; desf; ins; unfold is_nabla in *; desf.
eapply hplus_preserves_label_inv in pEQ; eauto; desf.
× rewrite Hsim_sym in RELsim; eapply Hsim_alloc_label in RELsim; eauto; desf.
apply exact_label_hplus_dist in TRANout; desf.
exploit label_is_consistent_with_exact_label_spec; eauto; ins; desf.
apply hplus_not_undef_r, hdef_alt in DEF; desf; rewrite DEF in ×.
eapply hplus_preserves_label in rOutEQ; eauto; desf.
by red in RELlabel; desf;
exploit label_is_consistent_with_exact_label_spec; try exact RELlabel; try exact RELlabel1; eauto.
× apply hplus_not_undef_l, hdef_alt in DEF; desf; rewrite DEF in ×.
eexists (hb_sb b _ ), _, _; do 3 (split; try edone).
rewrite !(hplusAC (Hdef hf'0 _)) in qEQ.
eapply hplus_preserves_label in qEQ; ins; desf; eauto.
}
{
RMWin_def.
apply hplus_not_undef_r, hdef_alt in DEFin; desf; rewrite DEFin in ×.
symmetry in DEFin; eapply hsum_preserves_label in DEFin; eauto; desf.
2: by repeat (rewrite In_map in *; eexists; split; try edone); apply rfsInOK.
symmetry in rInEQ; eapply hplus_preserves_label_inv in rInEQ; eauto; desf.
× apply hplus_not_undef_l, hdef_alt in DEF; desf; rewrite DEF in ×.
eexists (hb_sb b _ ), _, _; do 3 (split; try edone).
rewrite Hsim_sym in ACQsim; eapply Hsim_alloc_label in ACQsim; eauto; desf.
by red in ACQlabel; desf; exploit label_is_consistent_with_exact_label_spec;
try exact ACQlabel; try exact ACQlabel1; eauto; ins; desf;
rewrite Heq; rewrite hplusAC in qEQ;
eapply hplus_preserves_label in qEQ; eauto; ins; desf; eauto 8.
× apply hplus_not_undef_r, hdef_alt in DEF; desf; rewrite DEF in ×.
rewrite hplusAC in rOutEQ; eapply hplus_preserves_label in rOutEQ; eauto; desf.
eapply hplus_preserves_label_inv in DEF; eauto; desf.
+ symmetry in DEF; eapply hsum_preserves_label_inv in DEF; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_rf b _), _, _; ins; rewrite Heq; ins; repeat split; eauto 8.
by apply rfsOutOK.
+ eexists (hb_sink b), _, _; ins; rewrite Heq; ins; repeat split; eauto 8.
by red; rewrite Heq.
}
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
eexists (hb_sb b _), _, _; do 3 (split; try edone).
symmetry in pEQ; eapply hplus_preserves_label_inv in pEQ; eauto; desf.
by eapply hplus_preserves_label in qEQ; eauto; desf; eauto.
eapply hplus_preserves_label_inv in pEQ; eauto; desf.
by exploit label_is_consistent_with_exact_label_spec; eauto; ins.
rewrite Hsim_sym in ACQsim; eapply Hsim_alloc_label in ACQsim; eauto; desf.
exploit label_is_consistent_with_exact_label_spec; eauto; ins; desf.
rewrite !(hplusAC (Hdef _ _)) in qEQ; eapply hplus_preserves_label in qEQ; eauto; desf.
split; try done.
rewrite Heq; ins; desf; eauto 8.
specialize (REL eq_refl); inv REL.
}
Qed.
Lemma take_sync_step PS PSg:
∀ lab sb rf mo hmap ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
edge (EV: edge_valid lab sb rf (fst edge)) b (B: hb_snd (fst edge) = Some b)
(VALID: hmap_valid lab sb rf hmap ga b) hf g (MAP: hmap (fst edge) = Hdef hf g)
l (LAB: HVlabeled (hf l) (snd edge)) (ALL: hf l ≠ @HVnone PS PSg),
∃ edge' hf' g', << VALID: edge_valid lab sb rf (fst edge') >> ∧
<< MAP': hmap (fst edge') = Hdef hf' g' >> ∧
<< ALL': hf' l ≠ @HVnone PS PSg >> ∧ << LAB': HVlabeled (hf' l) (snd edge') >> ∧
<< SYNC: sync_step lab edge edge' >>.
Proof.
ins; destruct edge as [edg lbl]; ins; destruct lbl;
[exploit step_from_normal | exploit step_from_triangle | exploit step_from_nabla];
eauto; ins; desf; solve [
eexists (edge2, HLnormal), _, _; repeat split; ins; eauto; red; tauto |
eexists (edge2, HLtriangle), _, _; repeat split; ins; eauto; red; tauto |
eexists (edge2, HLnabla), _, _; repeat split; ins; eauto; red; tauto ].
Qed.
Lemma extend_tracking_path_right PS PSg :
∀ lab sb rf mo hmap ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
path (NEMP: path ≠ nil) a b (CON: hbpath_connects lab sb rf path a b)
(VALID: @hmap_valid PS PSg lab sb rf hmap ga b) l (TRACK: tracking_path hmap path l),
∃ edge, << WFP: hbpath_wf lab sb rf (path ++ edge :: nil) >> ∧
<< TRACK: tracking_path hmap (path ++ edge :: nil) l >>.
Proof.
ins.
des_list_tail path path' edge; ins.
assert (B: hb_snd (fst edge) = Some b).
by red in CON; desf; destruct path'; ins; desf; rewrite last_app in OMEGA; ins; desf.
exploit (hmap_defined_in (ga := ga) (hmap := hmap) CONS_RF (fst edge)); eauto.
by apply (proj2 (connects_implies_wf CON)); find_in_list.
ins; desf.
exploit (take_sync_step (ga := ga) (hmap := hmap) CONS_RF edge); eauto.
by apply (proj2 (connects_implies_wf CON)); find_in_list.
by eapply TRACK; eauto; find_in_list.
by eapply TRACK; eauto; find_in_list.
ins; desf.
∃ edge'; split.
× eapply extend_path_right; eauto.
eby eapply connects_implies_wf.
by destruct path'; ins; desf; rewrite last_app; ins; desf.
× red; red; ins.
rewrite In_app in IN; desf.
eby eapply TRACK.
ins; desf.
rewrite MAP in MAP'; desf.
Qed.
This page has been generated by coqdoc