Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import permission.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslassnsem fslmodel fslassnlemmas.
Require Import fslhmap path.
Set Implicit Arguments.
Lemma step_back_from_normal PS PSg:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
edge (EV: edge_valid lab sb rf edge)
hmap ga (VALID: hmap_valid lab sb rf hmap ga (hb_fst edge))
hf g (MAP: hmap edge = Hdef hf g) l (LAB: HVlabeled (hf l) HLnormal) (ALL: hf l ≠ @HVnone PS PSg),
<< ALLOC: lab (hb_fst edge) = Aalloc l >> ∨
∃ edge' hf' g', << CON: hb_snd edge' = Some (hb_fst edge) >> ∧
<< EV': edge_valid lab sb rf edge' >> ∧
<< MAP': hmap edge' = Hdef hf' g' >> ∧
<< ALL': hf' l ≠ @HVnone PS PSg >> ∧
<< SB: ¬ is_rf edge >> ∧
(<< SB': is_sb edge' >> ∧ << LAB': HVlabeled (hf' l) HLnormal >> ∨
<< SB': is_sb edge' >> ∧ << LAB': HVlabeled (hf' l) HLnabla >> ∧
<< ACQ: is_acquire_fence (lab (hb_fst edge)) >> ∧
<< reallySB: is_sb edge >> ∨
<< RF': is_rf edge' >> ∧ << LAB': HVlabeled (hf' l) HLnabla >> ∧
<< ACQ: is_acquire_read (lab (hb_fst edge)) >>).
Proof.
ins; unnw.
assert (notRF: ¬ is_rf edge).
{
destruct edge; ins.
exploit no_normals_on_rf; eauto.
}
unfold hmap_valid, unique in VALID.
desfh; desc; try (destruct DISJ; desc); destruct edge; ins; try revert TYP; desfh;
try (by red in EV; rewrite Heq in EV);
try (by specialize (CONS_RF e'); desfh; desfh; rewrite Heq in *; desfh);
rewrite ?(qU0 _ EV), ?MAP in *; desfh;
try (by inv sEQ);
try (by rewrite rEQ in MAP; inv MAP).
{
right.
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
assert (D := hplus_def_inv_l _ _ DEF); desf; rewrite D in ×.
symmetry in D; eapply hsum_preserves_label in D; eauto; desfh.
2: by repeat (rewrite In_map; eexists; split; eauto); apply qOK.
symmetry in DEF; eapply hplus_preserves_label in DEF; eauto; desfh.
eapply hplus_preserves_label_inv in EQ; eauto; desf.
symmetry in EQ; eapply hsum_preserves_label_inv in EQ; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
by apply pOK.
}
{
right.
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
symmetry in DEF; rewrite hplusC in DEF; eapply hplus_preserves_label in DEF; eauto; desfh.
eapply hplus_preserves_label_inv in EQ; eauto; desf.
symmetry in EQ; eapply hsum_preserves_label_inv in EQ; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
by apply pOK.
}
{
destruct (classic (l = l0)); eauto.
apply hplus_gheap in qEQ.
right; eexists (hb_sb _ e), _, _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto.
}
{
destruct (classic (l = l0)); eauto.
apply hplus_gheap in qEQ.
right; eexists (hb_sb _ e), _, _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto.
}
{
right.
rewrite pEQ in qEQ; apply hplus_gheap in qEQ; desfh.
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
}
{
right; revert TYP.
symmetry in qEQ; eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
× unfold hupd in qEQ0, qEQ1; desfh; desfh.
symmetry in pEQ'; eapply hplus_preserves_label in pEQ'; rewrite ?hupds; try by eauto.
desfh; eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
× eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
+ red in TRAN; desfh.
rewrite TRAN in ×.
assert (A := Hsim_alloc l rfsSIM qEQ3); desfh.
red in rfsSIM; desfh.
specialize (rfsSIM1 l).
rewrite HVsim_sym in rfsSIM1; eapply label_sim in rfsSIM1; eauto; desfh.
specialize (TRAN3 l).
exploit label_is_consistent_with_exact_label; eauto; intro; desfh.
symmetry in TRAN; eapply hsum_preserves_label_inv in TRAN; eauto; desfh.
repeat (rewrite In_map in *; desfh).
eexists (hb_rf _ e), _, _; ins; repeat split; eauto.
by apply rfsOK.
repeat right; repeat split; desfh.
- red in TYP; desfh; specialize (TYP0 l).
exfalso; clear - TYP0 qEQ2 qEQ3.
by exploit label_is_consistent_with_exact_label; eauto.
- desf.
+ eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
symmetry in pEQ'; rewrite hplusC in pEQ'; eapply hplus_preserves_label in pEQ'; eauto; desfh.
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
}
{
right; clear TYP.
unfold hupd in ALL; desfh; desfh.
symmetry in pEQ'; eapply hplus_preserves_label in pEQ'; rewrite ?hupds; simpls; desfh.
2: by instantiate (1 := HLnormal); vauto.
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
}
{
apply hplus_gheap in qEQ; desfh.
right; eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
× unfold hupd in ALL; desf; desf.
by intro N; rewrite N in IV; ins.
× left; repeat split.
unfold hupd in LAB; desf; desf.
red; desf; ins; desf.
by apply Pfull_is_not_Pzero.
}
{
right; clear TYP.
destruct (classic (l = l0)).
× subst l0.
symmetry in qEQ; eapply hplus_ra_lD in qEQ.
2: eby rewrite hupds.
desf.
+ symmetry in UPD; eapply hplus_ra_lD in UPD; eauto; desfh; try (by rewrite hupds);
apply initialize_eq_raD in UPD; desf;
eexists (hb_sb _ e), _, _; repeat split; ins; eauto; instantiate; rewrite UPD;
ins; clear; desf; unfold is_normal; eauto 7.
+ destruct isrmw'.
by symmetry in UPD; eapply hplus_ra_lD in UPD; eauto; desfh; try (by rewrite hupds);
apply initialize_eq_raD in UPD; desfh;
eexists (hb_sb _ e), _, _; repeat split; ins; eauto; instantiate; rewrite UPD;
ins; clear; desf; ins; desf; unfold is_normal; eauto 7.
by symmetry in UPD; eapply hplus_ra_lD in UPD; eauto; desf; try (by rewrite hupds);
apply initialize_eq_raD in UPD; desf;
eexists (hb_sb _ e), _, _; repeat split; ins; eauto; instantiate; rewrite UPD;
ins; clear; desf; ins; desf; unfold is_normal; eauto 7.
× symmetry in UPD; rewrite <- hplusA in UPD, qEQ.
assert (D := hplus_def_inv_l _ _ UPD); desfh; rewrite D in ×.
apply hplus_eq_gheap in ghostEQ; desf.
apply hplus_gheap in qEQ; desfh.
symmetry in UPD; eapply hplus_preserves_label in UPD; eauto; desfh.
rewrite <- initialize_alloc in UPD.
unfold initialize, hupd in UPD0; desfh.
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
}
{
exfalso.
red in TRAN; desfh.
symmetry in TRAN; rewrite hplusC in TRAN; eapply hplus_preserves_label in TRAN; eauto; desf.
specialize (TRAN3 l).
by exploit label_is_consistent_with_exact_label; eauto.
}
{
right.
exploit RMWinDEF; try eassumption; try (eby rewrite <- MAP in *); rewrite <- hdef_alt; intro D; desfh.
symmetry in qEQ; eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
× unfold hupd in qEQ1; desfh; desfh.
eapply hplus_not_undef_l, hdef_alt in D; desfh; rewrite D in ×.
eapply hplus_preserves_label in pEQ; eauto; desfh.
eexists (hb_sb pre e), _, _; ins; repeat split; eauto.
by rewrite hupds.
× eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
+ eapply Hsim_alloc_label in ACQsim; eauto; desfh.
rewrite <- rInEQ in TRANin.
apply hplus_not_undef_r, hdef_alt in D; desfh; rewrite D in rInEQ.
eapply hplus_preserves_label in rInEQ; try exact ACQsim1; eauto; desfh.
symmetry in D; assert (R := hsum_preserves_label_inv _ _ _ D rInEQ0 rInEQ); desfh.
repeat (rewrite In_map in *; desfh).
eexists (hb_rf _ _), _, _; repeat split; try eassumption; ins.
by apply rfsInOK.
repeat right; repeat split; try done.
- eapply exact_label_hsum_dist in TRANin.
2: by repeat (rewrite In_map; eexists; split; try edone); apply rfsInOK.
exploit label_is_consistent_with_exact_label_spec; try exact R0; eauto.
congruence.
- red in ACQlabel; desfh; try by desf.
by exploit label_is_consistent_with_exact_label_spec; try exact ACQlabel; eauto.
+ eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
- apply hplus_not_undef_l, hdef_alt in D; desfh; rewrite D in ×.
rewrite hplusC, hplusA, hplusAC in pEQ; eapply hplus_preserves_label in pEQ; eauto; desfh.
eexists (hb_sb pre e), _, _; ins; repeat split; eauto.
- apply hplus_eq_gheap in ghostEQ; desf.
}
{
exfalso.
apply hplus_not_undef_r, hdef_alt in DEF; desf; rewrite DEF in ×.
rewrite hplusC in DEF; symmetry in DEF; eapply hplus_preserves_label in DEF; eauto; desf.
apply hplus_eq_gheap in ghostEQ; desf.
rewrite <- hplusA in rOutEQ; symmetry in rOutEQ.
eapply hplus_preserves_label_inv in rOutEQ; eauto; desf.
by rewrite rOutEQ in *; exploit label_is_consistent_with_exact_label_spec; eauto.
}
{
exploit FenceInDEF; try eassumption; try (eby rewrite <- MAP in *); rewrite <- hdef_alt; intro D; desfh.
rewrite hdef_alt in D; desfh; rewrite D in ×.
right; eexists (hb_sb _ e), _, _; do 3 (split; eauto).
symmetry in qEQ; eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
by eapply hplus_preserves_label in pEQ; eauto; desfh; ins; intuition.
eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
× exfalso; red in RELlabel'; desf.
specialize (RELlabel'0 l).
by exploit label_is_consistent_with_exact_label; eauto.
× eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
red in ACQsim; desfh.
specialize (ACQsim1 l).
rewrite <- HVsim_alloc in qEQ5; eauto.
rewrite HVsim_sym in ACQsim1.
eapply label_sim in ACQsim1; eauto; desfh.
red in ACQlabel; desfh.
specialize (ACQlabel0 l).
exploit label_is_consistent_with_exact_label; eauto; ins; desfh.
rewrite <- hplusA, hplusC in pEQ.
eapply hplus_preserves_label in pEQ; eauto; desfh; repeat split; try done.
right; left; repeat split; try done; desf.
exploit REL; try done.
intro H; inv H.
}
Qed.
Lemma step_back_from_nabla PS PSg:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
edge (EV: edge_valid lab sb rf edge)
hmap ga (VALID: hmap_valid lab sb rf hmap ga (hb_fst edge))
hf g (MAP: hmap edge = Hdef hf g) l (LAB: HVlabeled (hf l) HLnabla) (ALL: hf l ≠ @HVnone PS PSg),
∃ edge' hf' g',
<< CON: hb_snd edge' = Some (hb_fst edge) >> ∧ << EV': edge_valid lab sb rf edge' >> ∧
<< MAP': hmap edge' = Hdef hf' g' >> ∧ << ALL': hf' l ≠ @HVnone PS PSg >> ∧
(<< SB: ¬ is_rf edge >> ∧ << SB': is_sb edge' >> ∧ << LAB': HVlabeled (hf' l) HLnabla >> ∨
<< SB: ¬ is_rf edge >> ∧ << RF': is_rf edge' >> ∧ << LAB': HVlabeled (hf' l) HLnabla >> ∨
<< RF: ¬ is_sb edge >> ∧ << SB': is_sb edge' >> ∧ << LAB': HVlabeled (hf' l) HLtriangle >> ∨
<< RF: ¬ is_sb edge >> ∧ << SB': is_sb edge' >> ∧ << LAB': HVlabeled (hf' l) HLnormal >> ∧
<< REL: is_release_write (lab (hb_fst edge)) >> ∨
<< RF: ¬ is_sb edge >> ∧ << RF': is_rf edge' >> ∧ << LAB': HVlabeled (hf' l) HLnabla >> ∧
<< RMW: is_rmw (lab (hb_fst edge)) >>).
Proof.
ins; unnw.
unfold hmap_valid, unique in VALID.
desfh; desc; try (destruct DISJ; desc); destruct edge; ins; try revert TYP; desfh;
try (by red in EV; rewrite Heq in EV);
try (by specialize (CONS_RF e'); desfh; desfh; rewrite Heq in *; desfh);
rewrite ?(qU0 _ EV), ?MAP in *; desfh;
try (by inv sEQ);
try (by rewrite rEQ in MAP; inv MAP).
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
assert (D := hplus_def_inv_l _ _ DEF); desf; rewrite D in ×.
symmetry in D; eapply hsum_preserves_label in D; eauto; desfh.
2: by repeat (rewrite In_map; eexists; split; eauto); apply qOK.
symmetry in DEF; eapply hplus_preserves_label in DEF; eauto; desfh.
eapply hplus_preserves_label_inv in EQ; eauto; desf.
symmetry in EQ; eapply hsum_preserves_label_inv in EQ; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
by apply pOK.
}
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
symmetry in DEF; rewrite hplusC in DEF; eapply hplus_preserves_label in DEF; eauto; desfh.
eapply hplus_preserves_label_inv in EQ; eauto; desf.
symmetry in EQ; eapply hsum_preserves_label_inv in EQ; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
by apply pOK.
}
{
apply hplus_gheap in qEQ; desfh.
eexists (hb_sb _ e), _, _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto.
}
{
apply hplus_gheap in qEQ; desfh.
eexists (hb_sb _ e), _, _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto;
ins; unfold is_nabla in LAB; desf.
}
{
rewrite pEQ in qEQ; apply hplus_gheap in qEQ; desfh.
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
}
{
symmetry in qEQ; eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
× exfalso.
unfold hupd in qEQ0, qEQ1; desf; ins; desfh.
unfold is_nabla in qEQ0; desf.
× eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
+ red in TRAN; desfh.
rewrite TRAN in ×.
assert (A := Hsim_alloc l rfsSIM qEQ3); desfh.
red in rfsSIM; desfh.
specialize (rfsSIM1 l).
rewrite HVsim_sym in rfsSIM1; eapply label_sim in rfsSIM1; eauto; desfh.
specialize (TRAN3 l).
exploit label_is_consistent_with_exact_label; eauto; intro; desfh.
symmetry in TRAN; eapply hsum_preserves_label_inv in TRAN; eauto; desfh.
repeat (rewrite In_map in *; desfh).
eexists (hb_rf _ e), _, _; ins; repeat split; eauto 6.
by apply rfsOK.
+ eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
symmetry in pEQ'; rewrite hplusC in pEQ'; eapply hplus_preserves_label in pEQ'; eauto; desfh.
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
}
{
exfalso.
unfold hupd in *; desf; desf; eauto; ins; unfold is_nabla in LAB; desf.
}
{
apply hplus_gheap in qEQ; desfh.
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
× unfold hupd in ALL; desf; desf.
by intro N; rewrite N in IV; ins.
× left; repeat split; try done.
unfold hupd in LAB; desf; desf.
}
{
symmetry in UPD; rewrite <- hplusA in UPD, qEQ.
assert (D := hplus_def_inv_l _ _ UPD); desfh; rewrite D in ×.
apply hplus_eq_gheap in ghostEQ; desfh.
apply hplus_gheap in qEQ; desfh.
symmetry in UPD; eapply hplus_preserves_label in UPD; eauto; desfh.
rewrite <- initialize_alloc in UPD.
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
clear TYP; left; repeat split; try done.
by eapply initialize_not_normal; eauto.
}
{
eexists (hb_sb _ e), _, _; do 3 (split; eauto).
revert TYP.
red in TRAN; desfh.
rewrite TRAN in ×.
assert (R := hplus_def_inv_l _ _ TRAN); desfh.
rewrite R in ×.
symmetry in R; eapply hsum_preserves_label in R; eauto; desfh.
2: by repeat (rewrite In_map; eexists; split; eauto); apply rfsOK.
symmetry in TRAN; eapply hplus_preserves_label in TRAN; eauto; desfh.
rewrite Hsim_sym in rfsSIM; eapply Hsim_alloc_label in rfsSIM; eauto; desfh.
apply hplus_eq_gheap in ghostEQ; desfh.
eapply hplus_preserves_label_inv in rfsSIM; eauto; desfh.
assert (UPDcopy := UPD).
rewrite <- hplusA, hplusC in UPD; eapply hplus_preserves_label in UPD; eauto; desfh.
rewrite <- initialize_alloc in UPD.
ins; desfh.
× red in TYP; desfh.
exploit label_is_consistent_with_exact_label; try exact (TYP0 l); eauto; intro; desfh.
repeat split; try done.
right; right; left; repeat split; try done.
by eapply initialize_not_normal; eauto.
× red in TYP1; desfh.
exploit label_is_consistent_with_exact_label; try exact (TYP2 l); eauto; intro; desfh.
repeat split; try done.
do 3 right; left; repeat split; try done; desf; repeat split; try done.
destruct (classic (l = l0)).
+ subst l0.
symmetry in UPDcopy; eapply hplus_ra_lD in UPDcopy.
2: eby rewrite hupds.
by desf; apply initialize_eq_raD in UPDcopy; desf;
rewrite UPDcopy; clear; ins;unfold is_normal; desf; eauto.
+ by unfold initialize, hupd in UPD0; ins; desf.
}
{
eexists (hb_sb _ e), _, _; do 3 (split; eauto).
revert TYP.
red in TRAN; desfh.
rewrite TRAN in ×.
symmetry in TRAN; rewrite hplusC in TRAN; eapply hplus_preserves_label in TRAN; eauto; desfh.
rewrite Hsim_sym in rfsSIM; eapply Hsim_alloc_label in rfsSIM; eauto; desfh.
apply hplus_eq_gheap in ghostEQ; desfh.
eapply hplus_preserves_label_inv in rfsSIM; eauto; desfh.
assert (UPDcopy := UPD).
rewrite <- hplusA, hplusC in UPD; eapply hplus_preserves_label in UPD; eauto; desfh.
rewrite <- initialize_alloc in UPD.
ins; desfh.
× red in TYP; desfh.
exploit label_is_consistent_with_exact_label; try exact (TYP0 l); eauto; intro; desfh.
repeat split; try done.
right; right; left; repeat split; try done.
by eapply initialize_not_normal; eauto.
× red in TYP1; desfh.
exploit label_is_consistent_with_exact_label; try exact (TYP2 l); eauto; intro; desfh.
repeat split; try done.
do 3 right; left; repeat split; try done; desf; repeat split; try done.
destruct (classic (l = l0)).
+ subst l0.
symmetry in UPDcopy; eapply hplus_ra_lD in UPDcopy.
2: eby rewrite hupds.
by desf; apply initialize_eq_raD in UPDcopy; desf;
rewrite UPDcopy; clear; ins;unfold is_normal; desf; eauto.
+ by unfold initialize, hupd in UPD0; ins; desf.
}
{
exploit RMWinDEF; try eassumption; try (eby rewrite <- MAP in *); rewrite <- hdef_alt; intro D; desfh.
symmetry in qEQ; eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
by unfold hupd in qEQ0, qEQ1; desfh; desfh; ins; unfold is_nabla in qEQ0; desfh.
eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
× eapply Hsim_alloc_label in ACQsim; eauto; desfh.
apply exact_label_hplus_dist in TRANin; desfh.
exploit label_is_consistent_with_exact_label_spec; try exact ACQsim1; eauto.
ins; subst.
apply hplus_not_undef_r, hdef_alt in D; desfh; rewrite D in ×.
eapply hplus_preserves_label in rInEQ; eauto; desfh.
symmetry in D; eapply hsum_preserves_label_inv in D; eauto; desfh.
repeat (rewrite In_map in *; desfh).
eexists (hb_rf _ _), _, _; repeat split; eauto; ins.
by apply rfsInOK.
by right; left; repeat split.
× apply hplus_eq_gheap in ghostEQ; desfh.
eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
apply hplus_not_undef_l, hdef_alt in D; desfh; rewrite D in ×.
rewrite hplusC, hplusA, hplusAC in pEQ.
eapply hplus_preserves_label in pEQ; eauto; desfh.
eexists (hb_sb _ e), _, _; repeat split; eauto.
by left; repeat split.
}
{
exploit RMWinDEF; try eassumption; try (eby rewrite <- MAP in *); rewrite <- hdef_alt; intro D; desfh.
red in TRANout; desfh; rewrite <- hplusA, TRANout in rOutEQ.
apply hplus_not_undef_r, hdef_alt in DEF; desfh; rewrite DEF in ×.
assert (R := hplus_def_inv_l _ _ DEF); desfh; rewrite R in ×.
symmetry in R; eapply hsum_preserves_label in R; eauto; desfh.
2: by repeat (rewrite In_map; eexists; split; try edone); apply rfsOutOK.
symmetry in DEF; eapply hplus_preserves_label in DEF; eauto; desfh.
apply hplus_eq_gheap in ghostEQ; desfh.
symmetry in rOutEQ; eapply hplus_preserves_label_inv in rOutEQ; eauto; desfh.
eapply hplus_preserves_label_inv in TRANout; eauto; desfh.
× eexists (hb_sb _ e).
eapply Hsim_alloc_label in RELsim; eauto; desfh.
apply hplus_not_undef_l, hdef_alt in D; desfh; rewrite D in ×.
rewrite hplusAC in pEQ; eapply hplus_preserves_label in pEQ; eauto; desfh.
eexists _, _; repeat split; eauto.
red in RELlabel; desfh; exploit label_is_consistent_with_exact_label_spec;
try exact RELsim1; eauto; ins; subst lbl'.
by right; right; left; repeat split.
by do 3 right; left; repeat split; desf.
× apply hplus_not_undef_r, hdef_alt in D; desfh; rewrite D in ×.
rewrite hplusC in rInEQ; eapply hplus_preserves_label in rInEQ; eauto; desfh.
symmetry in D; eapply hsum_preserves_label_inv in D; eauto; desfh.
repeat (rewrite In_map in *; desfh).
eexists (hb_rf _ _), _, _; repeat split; eauto; ins.
by apply rfsInOK.
by repeat right; repeat split.
}
{
exploit RMWinDEF; try exact pEQ; try eassumption; try (eby rewrite <- MAP in *);
rewrite <- hdef_alt; intro D; desfh.
red in TRANout; desfh; rewrite <- hplusA, TRANout in rOutEQ.
apply hplus_not_undef_r, hdef_alt in DEF; desfh; rewrite DEF in ×.
symmetry in DEF; rewrite hplusC in DEF; eapply hplus_preserves_label in DEF; eauto; desfh.
apply hplus_eq_gheap in ghostEQ; desfh.
symmetry in rOutEQ; rewrite hplusC in rOutEQ; eapply hplus_preserves_label_inv in rOutEQ; eauto; desfh.
eapply hplus_preserves_label_inv in TRANout; eauto; desfh.
× eexists (hb_sb _ e).
eapply Hsim_alloc_label in RELsim; eauto; desfh.
apply hplus_not_undef_l, hdef_alt in D; desfh; rewrite D in ×.
rewrite hplusAC in pEQ; eapply hplus_preserves_label in pEQ; eauto; desfh.
eexists _, _; repeat split; eauto.
red in RELlabel; desfh; exploit label_is_consistent_with_exact_label_spec;
try exact RELsim1; eauto; ins; subst lbl'.
by right; right; left; repeat split.
by do 3 right; left; repeat split; desf.
× apply hplus_not_undef_r, hdef_alt in D; desfh; rewrite D in ×.
rewrite hplusC in rInEQ; eapply hplus_preserves_label in rInEQ; eauto; desfh.
symmetry in D; eapply hsum_preserves_label_inv in D; eauto; desfh.
repeat (rewrite In_map in *; desfh).
eexists (hb_rf _ _), _, _; repeat split; eauto; ins.
by apply rfsInOK.
by repeat right; repeat split.
}
{
exploit FenceInDEF; try eassumption; try (eby rewrite <- MAP in *); intro D; desfh; rewrite D in ×.
eexists (hb_sb _ e), _, _; do 3 (split; eauto).
symmetry in qEQ; eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
by eapply hplus_preserves_label in pEQ; eauto; desfh; ins; intuition.
eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
× exfalso; red in RELlabel'; desf.
specialize (RELlabel'0 l).
by exploit label_is_consistent_with_exact_label; eauto.
× eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
exfalso; red in ACQlabel'; desf.
specialize (ACQlabel'0 l).
by exploit label_is_consistent_with_exact_label; eauto.
}
Qed.
Lemma step_back_from_triangle PS PSg:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
edge (EV: edge_valid lab sb rf edge)
hmap ga (VALID: hmap_valid lab sb rf hmap ga (hb_fst edge))
hf g (MAP: hmap edge = Hdef hf g) l (LAB: HVlabeled (hf l) HLtriangle) (ALL: hf l ≠ @HVnone PS PSg),
∃ edge' hf' g',
<< CON: hb_snd edge' = Some (hb_fst edge) >> ∧ << EV': edge_valid lab sb rf edge' >> ∧
<< MAP': hmap edge' = Hdef hf' g' >> ∧ << ALL': hf' l ≠ @HVnone PS PSg >> ∧
<< SB: ¬ is_rf edge >> ∧ << SB': is_sb edge' >> ∧
(<< LAB': HVlabeled (hf' l) HLtriangle >> ∨
<< LAB': HVlabeled (hf' l) HLnormal >> ∧ << REL: is_release_fence (lab (hb_fst edge)) >>
∧ << reallySB: is_sb edge >>).
Proof.
ins; unnw.
assert (notRF: ¬ is_rf edge).
{
destruct edge; ins.
eby exploit triangles_never_on_rf; eauto; ins; desf.
}
unfold hmap_valid, unique in VALID.
desfh; desc; try (destruct DISJ; desc); destruct edge; ins; try revert TYP; desfh;
try (by red in EV; rewrite Heq in EV);
try (by specialize (CONS_RF e'); desfh; desfh; rewrite Heq in *; desfh);
rewrite ?(qU0 _ EV), ?MAP in *; desfh;
try (by inv sEQ);
try (by rewrite rEQ in MAP; inv MAP).
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
assert (D := hplus_def_inv_l _ _ DEF); desf; rewrite D in ×.
symmetry in D; eapply hsum_preserves_label in D; eauto; desfh.
2: by repeat (rewrite In_map; eexists; split; eauto); apply qOK.
symmetry in DEF; eapply hplus_preserves_label in DEF; eauto; desfh.
eapply hplus_preserves_label_inv in EQ; eauto; desf.
symmetry in EQ; eapply hsum_preserves_label_inv in EQ; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
by apply pOK.
}
{
rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
symmetry in DEF; rewrite hplusC in DEF; eapply hplus_preserves_label in DEF; eauto; desfh.
eapply hplus_preserves_label_inv in EQ; eauto; desf.
symmetry in EQ; eapply hsum_preserves_label_inv in EQ; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
by apply pOK.
}
{
apply hplus_gheap in qEQ; desfh.
eexists (hb_sb _ e), _, _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto.
}
{
apply hplus_gheap in qEQ; desfh.
eexists (hb_sb _ e), _, _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto;
ins; unfold is_triangle in LAB; desf.
}
{
rewrite pEQ in qEQ; apply hplus_gheap in qEQ; desfh.
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
}
{
symmetry in qEQ; eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
× exfalso.
unfold hupd in qEQ0, qEQ1; desf; ins; desfh.
unfold is_triangle in qEQ0; desf.
× eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
+ ins; exfalso.
assert (L: ∃ lbl, HlabeledExact (Hdef hf'0 g'0) lbl ∧ lbl ≠ HLtriangle).
by desf; eexists; split; eauto.
clear TYP; desf.
red in L; desf.
specialize (L1 l); exploit label_is_consistent_with_exact_label; eauto; intro; desf.
+ eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
symmetry in pEQ'; rewrite hplusC in pEQ'; eapply hplus_preserves_label in pEQ'; eauto; desfh.
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
}
{
exfalso.
unfold hupd in *; desf; desf; eauto; ins; unfold is_triangle in LAB; desf.
}
{
apply hplus_gheap in qEQ; desfh.
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
× unfold hupd in ALL; desf; desf.
by intro N; rewrite N in IV; ins.
× left; repeat split; try done.
unfold hupd in LAB; desf; desf.
}
{
symmetry in UPD; rewrite <- hplusA in UPD, qEQ.
assert (D := hplus_def_inv_l _ _ UPD); desfh; rewrite D in ×.
apply hplus_eq_gheap in ghostEQ; desfh.
apply hplus_gheap in qEQ; desfh.
symmetry in UPD; eapply hplus_preserves_label in UPD; eauto; desfh.
rewrite <- initialize_alloc in UPD.
eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
clear TYP; left; repeat split; try done.
by eapply initialize_not_normal; eauto.
}
{
exfalso.
red in TRAN; desfh.
symmetry in TRAN; rewrite hplusC in TRAN; eapply hplus_preserves_label in TRAN; eauto; desf.
specialize (TRAN3 l); exploit label_is_consistent_with_exact_label; eauto; intro; desf.
}
{
exploit RMWinDEF; try eassumption; try (eby rewrite <- MAP in *); rewrite <- hdef_alt; intro D; desfh.
symmetry in qEQ; eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
by unfold hupd in qEQ0, qEQ1; desfh; desfh; ins; unfold is_triangle in qEQ0; desfh.
eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
by red in ACQlabel; desfh; exploit label_is_consistent_with_exact_label_spec; try exact qEQ2; eauto; ins.
apply hplus_eq_gheap in ghostEQ; desfh.
eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
apply hplus_not_undef_l, hdef_alt in D; desfh; rewrite D in ×.
rewrite hplusC, hplusA, hplusAC in pEQ.
eapply hplus_preserves_label in pEQ; eauto; desfh.
eexists (hb_sb _ e), _, _; repeat split; eauto.
}
{
exfalso.
apply hplus_not_undef_r, hdef_alt in DEF; desf; rewrite DEF in ×.
rewrite hplusC in DEF; symmetry in DEF; eapply hplus_preserves_label in DEF; eauto; desf.
apply hplus_eq_gheap in ghostEQ; desf.
rewrite <- hplusA in rOutEQ; symmetry in rOutEQ.
eapply hplus_preserves_label_inv in rOutEQ; eauto; desf.
by rewrite rOutEQ in *; exploit label_is_consistent_with_exact_label_spec; eauto.
}
{
exploit FenceInDEF; try eassumption; try (eby rewrite <- MAP in *); intro D; desfh; rewrite D in ×.
eexists (hb_sb _ e), _, _; do 3 (split; eauto).
symmetry in qEQ; eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
by eapply hplus_preserves_label in pEQ; eauto; desfh; ins; intuition.
eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
× red in RELsim; desfh.
specialize (RELsim1 l).
rewrite <- HVsim_alloc in qEQ3; eauto.
apply HVsim_sym in RELsim1; eapply label_sim in qEQ2; eauto; desfh.
red in RELlabel; desfh.
specialize (RELlabel0 l); exploit label_is_consistent_with_exact_label; eauto; desfh.
rewrite hplusAC in pEQ; eapply hplus_preserves_label in pEQ; eauto; ins; desfh; repeat split; try done.
right; repeat split; try done; desf.
exploit ACQ; try done.
intro H; inv H.
× eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
exfalso; red in ACQlabel'; desf.
specialize (ACQlabel'0 l).
by exploit label_is_consistent_with_exact_label; eauto.
}
Qed.
Lemma take_sync_step_back 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)) (VALID: hmap_valid lab sb rf hmap ga (hb_fst (fst edge)))
hf g (MAP: hmap (fst edge) = Hdef hf g) l (LAB: HVlabeled (hf l) (snd edge)) (ALL: hf l ≠ @HVnone PS PSg)
(NALL: lab (hb_fst (fst edge)) ≠ Aalloc l),
∃ 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_back_from_normal | exploit step_back_from_triangle | exploit step_back_from_nabla];
eauto; ins; desf; try solve [
eexists (edge', HLnormal), _, _; repeat split; ins; eauto; red; tauto |
eexists (edge', HLtriangle), _, _; repeat split; ins; eauto; red; tauto |
eexists (edge', HLnabla), _, _; repeat split; ins; eauto; red; tauto ].
eexists (edge', HLtriangle), _, _; repeat split; ins; eauto; red.
right; left; repeat split; try done; right.
destruct edg; ins; eauto.
specialize (CONS_RF e'); rewrite EV in CONS_RF; desf.
red in CONS_RF0; desf; ins; eauto.
Qed.
Lemma extend_tracking_path_left 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 a) l (TRACK: tracking_path hmap path l)
(NALL: lab a ≠ Aalloc l),
∃ edge, << WFP: hbpath_wf lab sb rf (edge :: path) >> ∧
<< TRACK: tracking_path hmap (edge :: path) l >>.
Proof.
ins.
destruct path as [ | edge path']; ins.
assert (A: hb_fst (fst edge) = a) by (red in CON; desf; ins; desf).
exploit hmap_defined_out; eauto.
by apply (proj2 (connects_implies_wf CON)); find_in_list.
ins; desf.
exploit (take_sync_step_back (hmap := hmap) (ga := ga) 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_left; eauto; ins.
by exact (connects_implies_wf CON).
× red; red; ins; desf.
by rewrite MAP in MAP'; desf; split.
eby eapply TRACK; try find_in_list.
by eapply TRACK; try find_in_list.
Qed.
This page has been generated by coqdoc