Require Import Vbase Varith.
Require Import Relations Wellfounded Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslassnsem fslmodel fslassnlemmas fslhmap.
Require Import ihc initread.
Require Import GpsSepAlg.
Set Implicit Arguments.
Lemma go_back_one_acq PS PSg :
∀ acts lab sb mo rf
(FIN : ExecutionFinite acts lab sb)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(CONS_A : ConsistentAlloc lab) hmap ga V
(HC : hist_closed sb rf V) e
(VALID : hmap_valid lab sb rf hmap ga e)
(INe : In e V) hFR l
(NALLOC : lab e ≠ Aalloc l)
(ALLOC : ∀ hf g loc,
hFR = Hdef hf g → hf loc ≠ @HVnone PS PSg →
∃ c : actid, lab c = Aalloc loc ∧ c ≠ e)
(GHOSTS: ∀ hf g loc,
hFR = Hdef hf g → g loc ≠ None →
ga loc ≠ Some e),
∃ pres_sb pres_rf posts_sb posts_rf,
NoDup pres_sb ∧
NoDup pres_rf ∧
NoDup posts_sb ∧
NoDup posts_rf ∧
(∀ x : actid, In x pres_sb ↔ sb x e) ∧
(∀ x : actid, In x pres_rf ↔ rf e = Some x) ∧
(∀ x : actid, In x posts_sb ↔ sb e x) ∧
(∀ x : actid, In x posts_rf ↔ rf x = Some e) ∧
(∀ h g
(EQ: hsum (map hmap (map (hb_sb^~ e) pres_sb)) +!+
hsum (map hmap (map (hb_rf^~ e) pres_rf)) +!+ hFR =
Hdef h g),
let hS := if excluded_middle_informative (ann_sink lab e) then hmap (hb_sink e) else hemp in
∃ h0 g0,
hsum (map hmap (map (hb_sb e) posts_sb)) +!+
hsum (map hmap (map (hb_rf e) posts_rf)) +!+ hS +!+ hFR = Hdef h0 g0 ∧
∀ PP' QQ' isrmw' perm' init' (LA: h0 l = HVra PP' QQ' isrmw' perm' init'),
hvplus_ra_ret (h l) QQ').
Proof.
unfold hmap_valid; ins; desc.
assert (GHOSTS': ∀ hf' g' loc, hFR = Hdef hf' g' → g' loc ≠ None → gnew loc = None).
{
ins.
eapply GHOSTS in H0; eauto.
apply NNPP; intro C; destruct H0.
by apply NG.
}
unfold unique in *; ins; desf; desc; try (destruct DISJ; desc); try clear TYP;
try (by red in a; rewrite Heq in a);
try (by destruct n; red; rewrite Heq).
Case Askip.
{
∃ pres, nil, posts, nil; repeat (split; ins).
by specialize (CONS_RF e); rewrite H, Heq in CONS_RF; desf.
by specialize (CONS_RF x); rewrite H, Heq in CONS_RF; desf.
rewrite hsum_nil, hplus_emp_l in ×.
rewrite <- hplusA, <- EQ, hplusA.
eexists _, _; split.
by apply new_ghosts_are_ok; eauto; congruence.
by ins; rewrite LA.
}
Case Aload .
{
pose proof (has_rf_pres e FIN CONS_RF); desc.
∃ (pre :: nil), rfs, (post :: nil), nil; ins; repeat (split; ins; desf); rewrite ?hsum_one in *; eauto.
by specialize (CONS_RF x); rewrite H, Heq in CONS_RF; desf.
assert (RFemp: hsum (map hmap (map (hb_rf^~ e) rfs)) = hemp).
by rewrite hsum_eq_emp; ins; repeat (rewrite In_map in *; desf); rewrite rEQ.
rewrite qEQ, sEQ, RFemp, hsum_nil, ?hplus_emp_l in ×.
eexists _, _; split.
by rewrite hplusA; apply new_ghosts_are_ok; eauto; congruence.
by ins; rewrite LA.
}
Case Aload .
{
∃ (pre :: nil), rfs, (post :: nil), nil; ins; repeat (split; ins; desf);
rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
by specialize (CONS_RF x); rewrite H, Heq in CONS_RF; desf.
rewrite sEQ in ×.
rewrite qEQ, !hplusA; do 4 rewrite (hplusAC (hsingl _ _ _ _));
rewrite <- hplusA, hplus_init1, !(hplusAC hr); ins.
rewrite pEQ, <- pEQ', hplusA, !(hplusAC (hsum _)) in EQ.
eapply hplus_sim_def_strong in EQ; try eassumption; desf.
eexists _, _; split.
{
do 2 rewrite <- hplusA; eapply new_ghosts_are_ok; rewrite ?hplusA; try edone.
rewrite hplusAC, <- (hplusA hr).
rewrite <- !hplusA in EQ; apply hplus_def_inv_l in EQ; desf; rewrite !hplusA, hplusAC in EQ.
rewrite hdef_alt; eexists _, _.
apply hsingl_with_ghosts_is_ok; try edone.
by rewrite hplusA; intro U; rewrite U, ?hplus_undef_l, hplus_undef_r in ×.
}
ins; specialize (EQ0 l); rewrite LA, HVsim_sym in EQ0; ins; desf; desf.
}
Case Astore .
{
pose proof (has_rf_succs e FIN CONS_RF); desc.
∃ (pre :: nil), nil, (post :: nil), rfs; ins; repeat (split; ins; desf);
rewrite ?sEQ, ?hsum_one, ?hplus_emp_l in *; eauto.
by specialize (CONS_RF e); rewrite H, Heq in CONS_RF; desf.
assert (M: hsum (map hmap (map (hb_rf e) rfs)) = hemp).
{
generalize (fun x ⇒ proj1 (INrfs x)); clear - rEQ.
by induction rfs; ins; rewrite hsum_cons, IHrfs, hplus_emp_r; eauto.
}
rewrite M, hplus_emp_l in ×.
rewrite pEQ, qEQ in ×.
exploit hdef_upd_alloc2; eauto; []; intro A; desf.
eexists _, _; split.
eby rewrite hplusA; apply new_ghosts_are_ok.
ins; rewrite <- A0, LA; try done.
by intro; subst; desf; clear - A LA;
eapply hplus_raD in A; eauto; desc;
clear N R; unfold hupd in *; desf; desf.
}
Case Astore .
{
∃ (pre :: nil), nil, (post :: nil), rfs; ins; repeat (split; ins; desf);
rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
by specialize (CONS_RF e); rewrite H, Heq in CONS_RF; desf.
rewrite pEQ in EQ.
destruct hFR as [|hFR gFR]; ins.
assert (gPLUS: gres_plus g gFR = Some g0).
{
clear - EQ.
rewrite hplus_unfold in EQ; desf; desf.
unfold gres_plus_total; desf.
}
eapply hplus_propagate_initialize in EQ.
Focus 2.
symmetry in UPD; eapply hplus_has_atomic_l in UPD; ins; desf; try by rewrite hupds.
eby eapply initialize_is_atomic.
rewrite UPD, !hplusA in EQ.
rewrite !(hplusAC hr) in EQ.
apply (f_equal (hplus (gheap _ _ gnew))) in EQ.
rewrite <- ghostEQ in EQ at 1.
rewrite hplusA, hplusAC, !(hplusAC hr), <- hplusA in EQ.
assert (G := hplus_eq_gheap _ _ ghostEQ); desf.
rewrite hplus_unfold in EQ; desf.
× rewrite Hsim_sym in rfsSIM; eapply hplus_sim_def_strong in EQ; eauto; desf.
rewrite !hplusA in EQ.
rewrite qEQ, !hplusA, !(hplusAC (gheap _ _ _)), !(hplusAC (hmap _)), !(hplusAC (hsum _)).
eexists _, _; split; try edone.
ins; specialize (EQ0 l).
rewrite LA, HVsim_sym in EQ0; clear - EQ0.
rewrite hvplus_ra_ret_initialize.
instantiate (1 := l0).
ins; desf; desf.
× destruct n; split; ins.
assert (GD: gres_plus g gnew ≠ None).
{
rewrite hplusC, qEQ in DEF.
eapply hplus_sim_def in DEF.
2: by exact rfsSIM.
rewrite !hplusA in DEF.
rewrite (hplusC hF), !(hplusAC (gheap _ _ g1)), <- !(hplusAC hr), (hplusC hr), <- UPD,
<- hplusA, ghostEQ, hplus_unfold in DEF; clear - DEF; desf; desf.
by rewrite gres_plusC.
}
clear - GHOSTS' gPLUS GD.
unfold gres_plus; des_eqrefl; try done.
inv_lplus2 l.
destruct (classic (gnew l = None)).
by rewrite H in ×.
assert (gFR l = None) by (by apply NNPP; intro N; specialize (GHOSTS' _ _ _ eq_refl N)).
unfold gres_plus in gPLUS; des_eqrefl; try done; desf; ins.
inv_lplus l; rewrite H0 in ×.
rewrite olift_plusC in EQ0; ins; desf.
2: by ins; rewrite plift_plusC; ins; rewrite salg_plusC.
rewrite <- H2 in EQ; clear H2.
destruct GD; rewrite gres_plusC; unfold gres_plus; des_eqrefl; try done.
exfalso; inv_lplus l; congruence.
}
Case Armw.
{
∃ (pre :: nil), rfsIn, (post :: nil), rfsOut; repeat (split; ins; desc); eauto; try by desf.
rewrite hsum_one in ×.
rewrite pEQ, rInEQ, !hplusA in EQ.
rewrite qEQ, <- (hplusA _ _ hFR), rOutEQ, !hplusA.
rewrite hplusAC in EQ; eapply hplus_sim_def_strong in EQ; eauto; desf.
rewrite !(hplusAC hacq) in EQ; eapply hplus_sim_def_strong in EQ; eauto; desf.
rewrite !(hplusAC hrel'), !(hplusAC hacq'); rewrite (hplusAC ht).
eexists _, _; split.
{
rewrite <- (hplusA sbg), ghostEQ; do 4 rewrite <- hplusA.
apply new_ghosts_are_ok; rewrite ?hplusA; try edone.
by rewrite qEQ, rOutEQ, !hplusA, !(hplusAC hrel'), !(hplusAC hacq'), (hplusAC ht), ghostEQ in DEF.
}
clear - EQ0 EQ1.
ins; specialize (EQ0 l); specialize (EQ1 l).
rewrite LA, HVsim_sym in *; ins; desf; desf; ins; desf; desf.
}
Case Aalloc.
{
∃ (pre :: nil), nil, (post :: nil), nil; repeat (split; ins; desc);
rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto; clear n;
try (by desf);
try (by specialize (CONS_RF e); rewrite H, Heq in CONS_RF; desf);
try (by specialize (CONS_RF x); rewrite H, Heq in CONS_RF; desf).
desf; rewrite pEQ, qEQ, hplusA in *; destruct hFR; ins.
{
eexists _, _; split.
{
apply new_ghosts_are_ok; try edone.
rewrite hplus_unfold in *; desf; desf; vauto.
destruct n; split; try done.
intro l'; specialize (HEAPcompat l').
unfold hupd in *; desf; desf.
specialize (ALLOC _ _ l0 eq_refl).
destruct (hf0 l0); desf; ins; destruct ALLOC; desf;
by edestruct H0; eapply CONS_A; rewrite ?H, ?Heq.
}
ins; rewrite hplus_unfold in *; desf; vauto.
unfold hupd in LA; desf; desf.
by rewrite LA.
}
{
eexists _, _; split.
{
apply new_ghosts_are_ok; try edone.
rewrite hplus_unfold in *; desf; desf; vauto.
destruct n; split; try done.
intro l'; specialize (HEAPcompat l').
unfold hupd in *; desf; desf.
specialize (ALLOC _ _ l0 eq_refl).
destruct (hf0 l0); desf; ins; destruct ALLOC; desf;
by edestruct H0; eapply CONS_A; rewrite ?H, ?Heq.
}
ins; rewrite hplus_unfold in *; desf; vauto.
unfold hupd in LA; desf; desf.
by rewrite LA.
}
}
Case Afence.
{
∃ (pre :: nil), nil, (post :: nil), nil; repeat (split; ins; desf);
rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
by specialize (CONS_RF e); rewrite H, Heq in CONS_RF; desf.
by specialize (CONS_RF x); rewrite H, Heq in CONS_RF; desf.
rewrite pEQ, qEQ, !hplusA in ×.
rewrite hplusAC in EQ; eapply hplus_sim_def_strong in EQ; eauto; desf.
rewrite !(hplusAC hacq) in EQ; eapply hplus_sim_def_strong in EQ; eauto; desf.
rewrite hplusAC, !(hplusAC hacq'), <- hplusA, <- hplusA.
eexists _, _; split.
{
apply new_ghosts_are_ok; rewrite ?hplusA; try edone.
by rewrite hplusAC, !(hplusAC hacq') in DEF.
}
clear - EQ0 EQ1; ins; specialize (EQ0 l); specialize (EQ1 l).
rewrite LA, HVsim_sym in *; ins; desf; desf; ins; desf; desf.
}
Qed.
Lemma go_back_one_rel PS PSg :
∀ lab sb rf mo hmap ga edge
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(VAL: hmap_valid lab sb rf hmap ga (hb_fst edge))
(EV : edge_valid lab sb rf edge) hf g
(GET: hmap edge = Hdef hf g) l PP QQ isrmw perm init v
(LA : hf l = @HVra PS PSg PP QQ isrmw perm init)
(NA : lab (hb_fst edge) ≠ Aalloc l),
∃ edge' hf' g',
edge_valid lab sb rf edge' ∧
hb_snd edge' = Some (hb_fst edge) ∧
hmap edge' = Hdef hf' g' ∧
∃ PP' QQ' isrmw' perm' init',
hf' l = HVra PP' QQ' isrmw' perm' init' ∧ implies (sval (PP v)) (sval (PP' v)).
Proof.
unfold hmap_valid, unique; ins; desf; desc; try (destruct DISJ; desc); try clear TYP.
Case Askip.
{
destruct edge; ins; subst.
× rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
assert (X := hplus_def_inv _ _ DEF); desf; rewrite X in ×.
eapply hsum_raD in X; eauto; desf; desf.
2: eby repeat (rewrite In_map; eexists; split; try edone); apply qOK.
destruct isrmw'.
+ eapply hplus_ram_lD in DEF; try edone; desc; clear DEF2; desf.
eapply hplus_eq_raD with (v:=v) in EQ; eauto; desf.
eapply hsum_eq_raD with (v:=v) in EQ; eauto; desf.
repeat (rewrite In_map in *; desf).
eapply pOK in EQ5.
unfold implies; repeat (eexists; try edone); ins.
by apply EQ3, EQ1, DEF0, X4.
+ eapply hplus_ra_lD in DEF; try edone; desc; clear DEF2; desf.
eapply hplus_eq_raD with (v:=v) in EQ; eauto; desf.
eapply hsum_eq_raD with (v:=v) in EQ; eauto; desf.
repeat (rewrite In_map in *; desf).
eapply pOK in EQ5.
unfold implies; repeat (eexists; try edone); ins.
by apply EQ3, EQ1, DEF0, X4.
× by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf.
× rewrite hdef_alt in DEF; desf; rewrite DEF in *; rewrite GET in DEF.
destruct isrmw.
+ eapply hplus_ram_rD in DEF; try edone; desc; clear DEF2; desf.
eapply hplus_eq_raD with (v:=v) in EQ; eauto; desf.
eapply hsum_eq_raD with (v:=v) in EQ; eauto; desf.
repeat (rewrite In_map in *; desf).
eapply pOK in EQ5.
unfold implies; repeat (eexists; try edone); ins.
by apply EQ3, EQ1, DEF0.
+ eapply hplus_ra_rD in DEF; try edone; desc; clear DEF2; desf.
eapply hplus_eq_raD with (v:=v) in EQ; eauto; desf.
eapply hsum_eq_raD with (v:=v) in EQ; eauto; desf.
repeat (rewrite In_map in *; desf).
eapply pOK in EQ5.
unfold implies; repeat (eexists; try edone); ins.
by apply EQ3, EQ1, DEF0.
}
Case Aalloc.
{
destruct edge; ins; subst;
try (by red in EV; rewrite Heq in *; desf);
try (by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf); [].
apply qU0 in EV; subst e'; rewrite GET in *; desf;
apply hplus_gheap in qEQ; subst;
unfold hupd in *; desf; desf;
by ∃ (hb_sb pre e); repeat (eexists; try edone).
}
Case Aload .
{
destruct edge; ins; subst.
× apply qU0 in EV; subst e'; rewrite GET in *; desf.
rewrite pEQ in *; desf.
apply hplus_gheap in qEQ; subst.
by ∃ (hb_sb pre e); repeat (eexists; try edone).
× by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf.
× rewrite sEQ in GET; inv GET.
}
Case Aload .
{
destruct edge; ins; subst.
× apply qU0 in EV; subst e'; rewrite GET in *; desf.
symmetry in qEQ; eapply hplus_eq_raD with (v:=v) in qEQ; eauto; desf.
+ unfold hupd in qEQ0; desf; desf.
∃ (hb_sb pre e); eapply hplus_def_inv in pEQ'; desf.
specialize (PLUSv l0); rewrite hupds in *; simpls.
by desf; unfold implies; repeat (eexists; try edone); ins; try eapply qEQ1 in H.
+ eapply hplus_eq_raD with (v:=v) in qEQ; eauto; desf.
- red in rfsSIM; desf.
specialize (rfsSIM1 l); rewrite qEQ2 in rfsSIM1; red in rfsSIM1; desf; desf.
eapply hsum_eq_raD with (v:=v) in rfsSIM; eauto; desc.
repeat (rewrite In_map in *; desf); rewrite rfsOK in ×.
repeat (eexists; try edone); ins; eauto.
red; ins.
generalize (qEQ1 h), (qEQ3 h), (rfsSIM1 h); clear - H; tauto.
- eapply hplus_eq_raD with (v:=v) in qEQ; eauto; desf.
∃ (hb_sb pre e); eexists _, _; repeat split; try edone.
destruct isrmw'1.
eapply hplus_ram_rD in pEQ'; eauto; desc; clarify.
unfold implies; repeat eexists; try edone; intros.
by apply pEQ'0, qEQ5, qEQ3, qEQ1.
eapply hplus_ra_rD in pEQ'; eauto; desc; clarify.
by unfold implies; repeat eexists; try edone; intros; apply pEQ'0, qEQ5, qEQ3, qEQ1.
× by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf.
× ∃ (hb_sb pre e); eexists _, _; repeat split; try edone.
rewrite sEQ in GET; inv GET.
unfold hupd in LA; desf; desf.
eapply hplus_has_atomic_l in pEQ'.
2: by intros ? ? X; inv X; rewrite hupds.
unfold is_atomic in pEQ'; desf.
repeat eexists; try edone.
}
Case Astore .
{
destruct edge; ins; subst; try (by rewrite ?sEQ, ?rEQ in GET; inv GET).
apply qU0 in EV; subst e'; rewrite GET in *; desf.
apply hplus_gheap in qEQ; subst.
unfold hupd in LA; desf; desf.
by ∃ (hb_sb pre e); repeat (eexists; try edone).
}
Case Astore .
{
eexists (hb_sb pre (hb_fst edge)), _, _; repeat split; try edone.
symmetry in UPD.
destruct edge; ins.
× rewrite (qU0 _ EV), GET in ×.
rewrite <- hplusA in qEQ; symmetry in qEQ; assert (D := hplus_def_inv _ _ qEQ); desf.
rewrite <- hplusA in UPD; rewrite D in ×.
apply hplus_eq_gheap in ghostEQ; desf.
symmetry in qEQ; apply hplus_gheap in qEQ; subst.
destruct isrmw.
+ eapply hplus_ram_lD in UPD; eauto; desc.
eapply initialize_eq_raD in UPD; desc.
repeat eexists; try edone.
by unfold implies; apply UPD0.
+ eapply hplus_ra_lD in UPD; eauto; desc.
eapply initialize_eq_raD in UPD; desc.
repeat eexists; try edone.
by unfold implies; apply UPD0.
× assert (RF: ∃ h g, hsum (map hmap (map (hb_rf e) rfs)) +!+ hmap (hb_sink e) = Hdef h g ∧
∃ PP' QQ' isrmw' perm' init',
h l = HVra PP' QQ' isrmw' perm' init' ∧
(∀ h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h)).
{
red in rfsSIM; desf.
eexists _, _; split; try edone.
apply hplus_def_inv in rfsSIM; desf.
exploit hsum_raD; eauto.
by repeat (rewrite In_map; eexists; split; try edone); apply rfsOK.
intro RF; desf.
by specialize (DEFv l); specialize (PLUSv l); rewrite RF in *; ins; desf;
repeat eexists; try edone; desf; intuition;
specialize (RF3 _ _ H0); rewrite e0 in RF3.
}
desf; rewrite RF in ×.
red in rfsSIM; desf.
specialize (rfsSIM1 l); rewrite RF0 in rfsSIM1; ins; desf; desf.
apply hplus_eq_gheap in ghostEQ; desf.
eapply hplus_eq_raD in rfsSIM0; eauto; desf.
destruct isrmw'.
+ rewrite <- hplusA in UPD; eapply hplus_ram_rD in UPD; eauto; desc.
eapply initialize_eq_raD in UPD; desc.
repeat eexists; try edone.
by red; ins; apply UPD0, rfsSIM2, RF1.
+ rewrite <- hplusA in UPD; eapply hplus_ra_rD in UPD; eauto; desc.
eapply initialize_eq_raD in UPD; desc.
repeat eexists; try edone.
by red; ins; apply UPD0, rfsSIM2, RF1.
× assert (RF: ∃ h g, hsum (map hmap (map (hb_rf e) rfs)) +!+ hmap (hb_sink e) = Hdef h g ∧
∃ PP' QQ' isrmw' perm' init',
h l = HVra PP' QQ' isrmw' perm' init' ∧
implies (sval (PP v)) (sval (PP' v))).
{
red in rfsSIM; desf.
eexists _, _; split; try edone.
rewrite GET in ×.
destruct isrmw; [eapply hplus_ram_rD in rfsSIM | eapply hplus_ra_rD in rfsSIM]; eauto; desc;
repeat eexists; try edone; unfold implies; intuition.
}
desf; rewrite RF in ×.
red in rfsSIM; desf.
specialize (rfsSIM1 l); rewrite RF0 in rfsSIM1; ins; desf; desf.
apply hplus_eq_gheap in ghostEQ; desf.
eapply hplus_eq_raD in rfsSIM0; eauto; desf.
destruct isrmw'.
+ rewrite <- hplusA in UPD; eapply hplus_ram_rD in UPD; eauto; desc.
eapply initialize_eq_raD in UPD; desc.
repeat eexists; try edone.
by red; ins; apply UPD0, rfsSIM2, RF1.
+ rewrite <- hplusA in UPD; eapply hplus_ra_rD in UPD; eauto; desc.
eapply initialize_eq_raD in UPD; desc.
repeat eexists; try edone.
by red; ins; apply UPD0, rfsSIM2, RF1.
}
Case Armw.
{
RMWin_heap.
assert (H: ∃ PP' QQ' isrmw' perm' init', hf0 l = HVra PP' QQ' isrmw' perm' init' ∧
implies (sval (PP v)) (sval (PP' v))).
{
rewrite hdef_alt in DEF; desf; assert (DEF' := DEF).
rewrite qEQ, rOutEQ, !hplusA, <- !(hplusAC sbg), ghostEQ, (hplusC _ (gheap _ _ _)),
!(hplusAC (gheap _ _ _)) in DEF; desf.
assert (D := hplus_def_inv_r _ _ DEF); desf; rewrite D in ×.
symmetry in DEF; rewrite hplusC in DEF; apply hplus_gheap in DEF; subst.
cut (Hsim (Hdef h3 g3) (Hdef hf0 g0)).
{
intro SIM; red in SIM; desf.
specialize (SIM1 l).
destruct edge; ins.
× rewrite (qU0 _ EV), GET in ×.
destruct isrmw; [eapply hplus_ram_lD in DEF' | eapply hplus_ra_lD in DEF']; eauto; desc;
rewrite DEF' in SIM1; red in SIM1; des_if; desc; subst;
repeat eexists; try edone; red; ins; intuition.
× assert (R := hplus_def_inv_r _ _ DEF'); desf.
apply hplus_def_inv_l in R; desf.
rewrite R, hplusAC in DEF'.
eapply hsum_raD in R; eauto; desc.
2: by repeat (rewrite In_map; eexists; split; try edone); apply rfsOutOK.
destruct isrmw'; [eapply hplus_ram_lD in DEF' | eapply hplus_ra_lD in DEF']; eauto; desc;
rewrite DEF' in SIM1; red in SIM1; des_if; desc; subst;
repeat eexists; try edone; red; ins; intuition.
× rewrite GET, <- hplusA in DEF'.
destruct isrmw; [eapply hplus_ram_rD in DEF' | eapply hplus_ra_rD in DEF']; eauto; desc;
rewrite DEF' in SIM1; red in SIM1; des_if; desc; subst;
repeat eexists; try edone; red; ins; intuition.
}
{
rewrite pEQ, rInEQ, !hplusA in DEFin.
rewrite qEQ, rOutEQ, !hplusA, (hplusAC hrel'), (hplusAC hrel'), <- (hplusAC hacq'),
(hplusAC ht), ghostEQ in DEF'.
rewrite <- D, <- DEFin.
do 2 rewrite (hplusAC hacq).
rewrite <- (hplusAC hrel).
by repeat (apply hplus_sim; try apply Hsim_refl;
try by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in D);
rewrite Hsim_sym.
}
}
desf.
eapply hplus_eq_raD in DEFin; eauto; desf.
× eexists (hb_sb _ _), _, _; repeat split; eauto.
repeat eexists; eauto.
by red; ins; apply DEFin1, H0.
× eapply hsum_eq_raD in DEFin; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_rf _ _), _, _; repeat split; eauto.
by ins; apply rfsInOK.
repeat eexists; eauto.
by red; ins; apply DEFin3, DEFin1, H0.
}
Case Afence.
{
exploit FenceInDEF; eauto.
rewrite hdef_alt in DEF; intro DEFin; desf; rewrite DEF, DEFin in ×.
rewrite <- !hplusA in qEQ. symmetry in qEQ;
assert (D := hplus_def_inv_l _ _ qEQ); desf; rewrite D in ×.
symmetry in qEQ; apply hplus_gheap in qEQ; subst.
cut (Hsim (Hdef h3 g3) (Hdef hf0 g0)).
{
intro SIM.
red in SIM; desf.
eexists (hb_sb _ _), _, _; repeat split; eauto.
destruct edge; ins; try (by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf);
try (by red in EV; rewrite Heq in *; desf).
rewrite (qU0 _ EV), GET in *; desf.
specialize (SIM1 l); rewrite LA in SIM1; red in SIM1; desf; desf.
eby repeat eexists.
}
{
rewrite hplusA in D.
rewrite Hsim_sym, pEQ, <- D.
apply hplus_sim; try congruence.
by apply Hsim_refl; intro U; rewrite U, !hplus_undef_l in ×.
apply hplus_sim; try done.
by intro U; rewrite U, hplus_undef_r in ×.
}
}
Qed.
Lemma heap_loc_rel_allocated PS PSg :
∀ lab sb rf mo hmap V v
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_A: ConsistentAlloc lab)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(HC: hist_closed sb rf V)
(VALID: hmap_valids lab sb rf hmap V)
edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
h g (GET: hmap edge = Hdef h g) l PP QQ isrmw perm init
(LA: h l = @HVra PS PSg PP QQ isrmw perm init),
∃ cpre c hf g' PP' QQ' isrmw' perm' init',
sb cpre c ∧
lab cpre = Aalloc l ∧
hmap (hb_sb cpre c) = Hdef hf g' ∧
hf l = HVra PP' QQ' isrmw' perm' init' ∧
(cpre = hb_fst edge ∨ happens_before_union_rf sb rf cpre (hb_fst edge)) ∧
implies (sval (PP v)) (sval (PP' v)).
Proof.
intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
clear edge EV IN; intros.
red in VALID; desf.
generalize (VLD _ IN).
destruct (classic (lab (hb_fst edge) = Aalloc l)) as [|NEQ]; eauto.
× ins; destruct edge; ins.
by repeat (eexists; try edone); vauto.
by specialize (CONS_RF e'); rewrite EV, H in CONS_RF; desf.
by red in EV; rewrite H in EV.
× intros; exploit go_back_one_rel; eauto; ins; desf.
assert (HB: happens_before_union_rf sb rf (hb_fst edge') (hb_fst edge)).
by destruct edge'; ins; desf; eauto with hb.
exploit (IH edge'); eauto.
intro; desf; repeat eexists; eauto using implies_trans with hb ; ins; desf; eauto.
Qed.
Lemma heap_loc_rel_allocated_strong PS PSg :
∀ lab sb rf mo hmap V v
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_A: ConsistentAlloc lab)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(HC: hist_closed sb rf V)
(VALID: hmap_valids lab sb rf hmap V)
edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
h g (GET: hmap edge = Hdef h g) l PP QQ isrmw perm init
(LA: h l = @HVra PS PSg PP QQ isrmw perm init),
∃ cpre c hf g' PP' QQ' isrmw',
sb cpre c ∧
lab cpre = Aalloc l ∧
hmap (hb_sb cpre c) = Hdef hf g' ∧
hf l = HVra PP' QQ' isrmw' (Some HLCnormal) None ∧
(cpre = hb_fst edge ∨ happens_before_union_rf sb rf cpre (hb_fst edge)) ∧
implies (sval (PP v)) (sval (PP' v)).
Proof.
ins.
exploit heap_loc_rel_allocated; eauto.
red in VALID; desc.
instantiate (1 := v); intro ALL; desc.
assert (cpreVALID: hmap_valid lab sb rf hmap ga cpre).
{
apply VLD; desf.
eapply hist_closedD; eauto.
}
red in cpreVALID; rewrite ALL0 in cpreVALID; desc.
rewrite ((proj2 qU) _ ALL), ALL1 in ×.
revert ALL3; desf; apply hplus_gheap in qEQ; subst.
by rewrite hupds in ALL2.
rewrite hupds in ALL2; desf.
repeat eexists; eauto using hupds.
Qed.
Lemma heap_loc_allocated_atomic PS PSg :
∀ lab sb rf mo hmap V
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_A: ConsistentAlloc lab)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(HC: hist_closed sb rf V)
(VALID: hmap_valids lab sb rf hmap V)
edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
h g (GET: hmap edge = @Hdef PS PSg h g) l
(LA: is_atomic (h l)),
∃ cpre c hf g',
sb cpre c ∧
lab cpre = Aalloc l ∧
hmap (hb_sb cpre c) = Hdef hf g' ∧
is_atomic (hf l) ∧
(cpre = hb_fst edge ∨ happens_before_union_rf sb rf cpre (hb_fst edge)).
Proof.
ins; unfold is_atomic in LA; desf.
exploit heap_loc_rel_allocated; eauto; ins; desc.
repeat eexists; eauto.
by rewrite x3.
Grab Existential Variables. done.
Qed.
Lemma go_back_one_rmwacq PS PSg :
∀ lab sb rf mo hmap ga edge
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(VAL: hmap_valid lab sb rf hmap ga (hb_fst edge))
(EV : edge_valid lab sb rf edge) hf g
(GET: hmap edge = Hdef hf g) l PP QQ perm init
(LA : hf l = HVra PP QQ true perm init)
(NA : lab (hb_fst edge) ≠ Aalloc l),
∃ edge' hf' g',
edge_valid lab sb rf edge' ∧
hb_snd edge' = Some (hb_fst edge) ∧
hmap edge' = Hdef hf' g' ∧
∃ PP' QQ' perm' init', hf' l = @HVra PS PSg PP' QQ' true perm' init'.
Proof.
unfold hmap_valid, unique; ins; desf; desc; try (destruct DISJ; desc); try clear TYP.
Case Askip.
{
destruct edge; ins; subst.
× rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
assert (X := hplus_def_inv _ _ DEF); desf; rewrite X in ×.
eapply hsum_raD in X; eauto; desf; desf.
2: by repeat (rewrite In_map; eexists; split; try edone); eapply qOK.
rewrite X2 in *; ins.
eapply hplus_ram_lD in DEF; try edone; desc; clear DEF2; desf.
eapply hplus_eq_ra_rmwD in EQ; eauto; desf.
eapply hsum_eq_ra_rmwD in EQ; eauto; desf.
repeat (rewrite In_map in *; desf); rewrite pOK in ×.
by repeat (eexists; try edone).
× by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf.
× rewrite hdef_alt in DEF; desf; rewrite GET, DEF in ×.
eapply hplus_ram_rD in DEF; try edone; desc; clear DEF2; desf.
eapply hplus_eq_ra_rmwD in EQ; eauto; desf.
eapply hsum_eq_ra_rmwD in EQ; eauto; desf.
repeat (rewrite In_map in *; desf); rewrite pOK in ×.
by repeat (eexists; try edone).
}
Case Aalloc.
{
destruct edge; ins; subst;
try (by red in EV; rewrite Heq in *; desf);
try (by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf); [].
apply qU0 in EV; subst e'; rewrite GET in *; desf;
apply hplus_gheap in qEQ; subst;
unfold hupd in *; desf; desf;
by ∃ (hb_sb pre e); repeat (eexists; try edone).
}
Case Aload .
{
destruct edge; ins; subst.
× apply qU0 in EV; subst e'; rewrite GET in *; desf.
rewrite pEQ in ×.
apply hplus_gheap in qEQ; subst.
by ∃ (hb_sb pre e); repeat (eexists; try edone).
× by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf.
× rewrite sEQ in GET; inv GET.
}
Case Aload .
{
symmetry in qEQ; destruct edge; ins; subst.
× apply qU0 in EV; subst e'; rewrite GET in *; desf.
eapply hplus_eq_ra_rmwD in qEQ; eauto.
desf; [by unfold hupd in qEQ0; desf; desf|].
eapply hplus_eq_ra_rmwD in qEQ; eauto; desf.
+ red in rfsSIM; desf.
specialize (rfsSIM1 l); rewrite qEQ1 in rfsSIM1; red in rfsSIM1; desf; desf.
eapply hsum_eq_ra_rmwD in rfsSIM; eauto; desc.
repeat (rewrite In_map in *; desf); rewrite rfsOK in ×.
by repeat (eexists; try edone); ins; eauto.
+ eexists (hb_sb _ _), _, _; repeat split; try edone.
eapply hplus_eq_ra_rmwD in qEQ; eauto; desf.
eapply hplus_ram_rD in pEQ'; eauto; desc.
by repeat eexists; try edone.
× by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf.
× rewrite sEQ in GET; inv GET.
unfold hupd in LA; desf; desf.
}
Case Astore .
{
destruct edge; ins; subst; try (by rewrite ?rEQ, ?sEQ in GET; inv GET); [].
apply qU0 in EV; subst e'; rewrite GET in ×.
apply hplus_gheap in qEQ; subst.
unfold hupd in LA; desf; desf.
by ∃ (hb_sb pre e); repeat (eexists; try edone).
}
Case Astore .
{
eexists (hb_sb _ _), _, _; repeat split; try edone.
apply hplus_eq_gheap in ghostEQ; desf.
symmetry in UPD; destruct edge; ins.
× rewrite (qU0 _ EV), GET in ×.
rewrite <- hplusA in qEQ; symmetry in qEQ; assert (D := hplus_def_inv _ _ qEQ); desf.
rewrite <- hplusA in UPD; rewrite D in ×.
symmetry in qEQ; apply hplus_gheap in qEQ; subst.
eapply hplus_ram_lD in UPD; eauto; desc.
eapply initialize_eq_raD in UPD; desc.
eby repeat eexists.
× red in rfsSIM; desf.
apply hplus_def_inv in rfsSIM0; desf.
apply hplus_def_inv in rfsSIM; desf.
eapply hsum_raD in rfsSIM; eauto; desf.
2: by repeat (rewrite In_map; eexists; split; try edone); apply rfsOK.
assert (EQ: ∃ PP QQ perm init, hf1 l = HVra PP QQ true perm init).
eby generalize (PLUSv0 l); rewrite rfsSIM, rfsSIM3; clear; ins; desf; repeat eexists.
desf.
specialize (rfsSIM1 l); rewrite EQ in rfsSIM1; red in rfsSIM1; desf; desf.
specialize (PLUSv l); rewrite hvplusC in PLUSv; ins; desf.
rewrite PLUSv in ×.
rewrite <- hplusA in UPD; eapply hplus_ram_rD in UPD; eauto; desc.
eapply initialize_eq_raD in UPD; desc.
eby repeat eexists.
× rewrite GET in *; red in rfsSIM; desf.
generalize (hplus_def_inv_l _ _ rfsSIM0); ins; desf.
symmetry in rfsSIM0; apply hplus_gheap in rfsSIM0; desf.
eapply hplus_ram_rD in rfsSIM; eauto; desc.
clear rfsSIM3; specialize (rfsSIM1 l); rewrite rfsSIM in rfsSIM1; red in rfsSIM1; desf; desf.
rewrite <- hplusA in UPD; eapply hplus_ram_rD in UPD; eauto; desc.
eapply initialize_eq_raD in UPD; desc.
eby repeat eexists.
}
Case Armw.
{
RMWin_heap.
rewrite hdef_alt in DEF; desf; assert (DEF' := DEF).
rewrite qEQ, rOutEQ, !hplusA, <- !(hplusAC sbg), ghostEQ, (hplusC _ (gheap _ _ _)),
!(hplusAC (gheap _ _ _)) in DEF; desf.
assert (D := hplus_def_inv_r _ _ DEF); desf; rewrite D in ×.
symmetry in DEF; rewrite hplusC in DEF; apply hplus_gheap in DEF; subst.
assert (H: ∃ PP' QQ' perm' init', hf0 l = HVra PP' QQ' true perm' init').
{
cut (Hsim (Hdef h3 g3) (Hdef hf0 g0)).
{
intro SIM; red in SIM; desf.
specialize (SIM1 l).
destruct edge; ins.
× rewrite (qU0 _ EV), GET in ×.
eby eapply hplus_ram_lD in DEF'; eauto; desc;
rewrite DEF' in SIM1; red in SIM1; des_if; desc; subst;
repeat eexists.
× assert (R := hplus_def_inv_r _ _ DEF'); desf.
apply hplus_def_inv_l in R; desf.
rewrite R, hplusAC in DEF'.
eapply hsum_raD in R; eauto; desc.
2: by repeat (rewrite In_map; eexists; split; try edone); apply rfsOutOK.
rewrite R1 in *; ins.
eby eapply hplus_ram_lD in DEF'; eauto; desc;
rewrite DEF' in SIM1; red in SIM1; des_if; desc; subst;
repeat eexists.
× rewrite GET, <- hplusA in DEF'.
eby eapply hplus_ram_rD in DEF'; eauto; desc;
rewrite DEF' in SIM1; red in SIM1; des_if; desc; subst;
repeat eexists.
}
{
rewrite pEQ, rInEQ, !hplusA in DEFin.
rewrite qEQ, rOutEQ, !hplusA, (hplusAC hrel'), (hplusAC hrel'), <- (hplusAC hacq') in DEF'.
rewrite <- D, <- DEFin.
do 2 rewrite (hplusAC hacq).
rewrite <- (hplusAC hrel).
by repeat (apply hplus_sim; try apply Hsim_refl;
try by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in D);
rewrite Hsim_sym.
}
}
desf.
eapply hplus_eq_ra_rmwD in DEFin; eauto; desf.
× eexists (hb_sb _ _), _, _; repeat split; eauto.
× eapply hsum_eq_ra_rmwD in DEFin; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_rf _ _), _, _; repeat split; eauto.
by ins; apply rfsInOK.
}
Case Afence.
{
exploit FenceInDEF; eauto.
rewrite hdef_alt in DEF; intro DEFin; desf; rewrite DEF, DEFin in ×.
rewrite <- !hplusA in qEQ. symmetry in qEQ;
assert (D := hplus_def_inv_l _ _ qEQ); desf; rewrite D in ×.
symmetry in qEQ; apply hplus_gheap in qEQ; subst.
cut (Hsim (Hdef h3 g3) (Hdef hf0 g0)).
{
intro SIM.
red in SIM; desf.
eexists (hb_sb _ _), _, _; repeat split; eauto.
destruct edge; ins; try (by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf);
try (by red in EV; rewrite Heq in *; desf).
rewrite (qU0 _ EV), GET in *; desf.
specialize (SIM1 l); rewrite LA in SIM1; red in SIM1; desf; desf.
eby repeat eexists _, _.
}
{
rewrite hplusA in D.
rewrite Hsim_sym, pEQ, <- D.
apply hplus_sim; try congruence.
by apply Hsim_refl; intro U; rewrite U, !hplus_undef_l in ×.
apply hplus_sim; try done.
by intro U; rewrite U, hplus_undef_r in ×.
}
}
Qed.
Lemma heap_loc_rmwacq_allocated PS PSg :
∀ lab sb rf mo hmap V
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_A: ConsistentAlloc lab)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(HC: hist_closed sb rf V)
(VALID: hmap_valids lab sb rf hmap V)
edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
h g (GET: hmap edge = Hdef h g) l PP QQ perm init
(LA: h l = @HVra PS PSg PP QQ true perm init),
∃ cpre c hf g' PP' QQ' perm' init',
sb cpre c ∧
lab cpre = Aalloc l ∧
hmap (hb_sb cpre c) = Hdef hf g' ∧
hf l = HVra PP' QQ' true perm' init'.
Proof.
intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
clear edge EV IN; intros.
red in VALID; desc.
generalize (VLD _ IN).
destruct (classic (lab (hb_fst edge) = Aalloc l)) as [|NEQ]; eauto.
× ins; destruct edge; ins.
by repeat (eexists; try edone); vauto.
by specialize (CONS_RF e'); rewrite EV, H in CONS_RF; desf.
by red in EV; rewrite H in EV.
× intros; exploit go_back_one_rmwacq; eauto; ins; desf.
assert (HB: happens_before_union_rf sb rf (hb_fst edge') (hb_fst edge)).
by destruct edge'; ins; desf; eauto with hb.
exploit (IH edge'); eauto.
Qed.
Lemma go_back_one_acq3 PS PSg :
∀ lab sb rf mo hmap ga edge
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(VAL: hmap_valid lab sb rf hmap ga (hb_fst edge))
(EV : edge_valid lab sb rf edge) hf g
(GET: hmap edge = Hdef hf g) l PP QQ perm init
(LA : hf l = @HVra PS PSg PP QQ false perm init) v
(NE : sval (QQ v) ≠ Aemp)
(NE : sval (QQ v) ≠ Afalse)
(NA : lab (hb_fst edge) ≠ Aalloc l),
∃ edge' hf' g',
edge_valid lab sb rf edge' ∧
hb_snd edge' = Some (hb_fst edge) ∧
hmap edge' = Hdef hf' g' ∧
∃ PP' QQ' perm' init',
hf' l = HVra PP' QQ' false perm' init' ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof.
unfold hmap_valid, unique; ins; desf; desc; try (destruct DISJ; desc); try clear TYP.
Case Askip.
{
destruct edge; ins; subst.
× rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
assert (X := hplus_def_inv _ _ DEF); desf; rewrite X in ×.
eapply hsum_has_ra_own in X; eauto; desf; desf.
2: by repeat (rewrite In_map; eexists; split; try edone); eapply qOK.
eapply hplus_ra_own_l in DEF; try edone; desf.
eapply hplus_eq_ra_ownD in EQ; eauto; desf.
eapply hsum_eq_ra_ownD in EQ; eauto; desf.
repeat (rewrite In_map in *; desf); rewrite pOK in ×.
by repeat (eexists; try edone).
× by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf.
× rewrite hdef_alt in DEF; desf; rewrite GET, DEF in ×.
eapply hplus_ra_own_r in DEF; try edone; desf.
eapply hplus_eq_ra_ownD in EQ; eauto; desf.
eapply hsum_eq_ra_ownD in EQ; eauto; desf.
repeat (rewrite In_map in *; desf); rewrite pOK in ×.
by repeat (eexists; try edone).
}
Case Aalloc.
{
destruct edge; ins; subst;
try (by red in EV; rewrite Heq in *; desf);
try (by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf); [].
apply qU0 in EV; subst e'; rewrite GET in *; desf;
apply hplus_gheap in qEQ; subst;
unfold hupd in *; desf; desf;
by ∃ (hb_sb pre e); repeat (eexists; try edone).
}
Case Aload .
{
destruct edge; ins; subst.
× apply qU0 in EV; subst e'; rewrite GET in *; desf.
rewrite pEQ in ×.
apply hplus_gheap in qEQ; subst.
by ∃ (hb_sb pre e); repeat (eexists; try edone).
× by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf.
× rewrite sEQ in GET; inv GET.
}
Case Aload .
{
symmetry in qEQ; destruct edge; ins; subst.
× apply qU0 in EV; subst e'; rewrite GET in *; desf.
eapply hplus_eq_ra_ownD in qEQ; eauto; desf.
by unfold hupd in qEQ0; desf; desf.
eapply hplus_eq_ra_ownD in qEQ; eauto; desf.
+ red in rfsSIM; desf.
specialize (rfsSIM1 l); rewrite qEQ3 in rfsSIM1; red in rfsSIM1; desf; desf.
eapply hsum_eq_ra_ownD in rfsSIM; eauto; desc.
repeat (rewrite In_map in *; desf); rewrite rfsOK in ×.
by repeat (eexists; try edone); ins; eauto.
+ eapply hplus_eq_ra_ownD in qEQ; eauto; desf.
eapply hplus_ra_own_r in pEQ'; eauto; desf.
eexists (hb_sb _ e); repeat (eexists; try edone).
× by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf.
× rewrite sEQ in GET; inv GET.
unfold hupd in LA; desf; desf; desf.
eapply hplus_ra_own_l in pEQ'; try by rewrite hupds.
desf; eexists (hb_sb _ e); repeat (eexists; try edone).
}
Case Astore .
{
destruct edge; ins; subst; try by (rewrite ?sEQ, ?rEQ in GET; inv GET).
apply qU0 in EV; subst e'; rewrite GET in *; desf.
apply hplus_gheap in qEQ; subst.
unfold hupd in LA; desf; desf.
by ∃ (hb_sb pre e); repeat (eexists; try edone).
}
Case Astore .
{
symmetry in UPD; eexists (hb_sb pre (hb_fst edge)), _, _; repeat split; ins; eauto.
apply hplus_eq_gheap in ghostEQ; desf.
destruct edge; ins.
× rewrite (qU0 _ EV), GET in ×.
rewrite <- hplusA in qEQ; symmetry in qEQ; assert (D := hplus_def_inv _ _ qEQ); desf.
rewrite <- hplusA in UPD; rewrite D in ×.
symmetry in qEQ; apply hplus_gheap in qEQ; subst.
eapply hplus_ra_own_l in UPD; eauto; desc.
eapply initialize_eq_raD in UPD; desc.
by repeat (eexists; try edone).
× red in rfsSIM; desf.
assert (RF := (hplus_def_inv_l _ _ rfsSIM)); desf; rewrite RF in ×.
eapply hsum_has_ra_own in RF; eauto; desf.
2: by repeat (rewrite In_map; eexists; split; try edone); eapply rfsOK.
eapply hplus_ra_own_l in rfsSIM; eauto; desf.
specialize (rfsSIM1 l); rewrite rfsSIM in rfsSIM1; red in rfsSIM1; desf; desf.
generalize (hplus_def_inv _ _ rfsSIM0); ins; desf.
symmetry in rfsSIM0; apply hplus_gheap in rfsSIM0; desf.
rewrite <- hplusA in UPD; eapply hplus_ra_own_r in UPD; eauto; desf.
eapply initialize_eq_raD in UPD; desc.
eby repeat eexists.
× rewrite GET in ×.
red in rfsSIM; desf.
generalize (hplus_def_inv _ _ rfsSIM0); ins; desf.
symmetry in rfsSIM0; apply hplus_gheap in rfsSIM0; desf.
eapply hplus_ra_own_r in rfsSIM; eauto; desf.
specialize (rfsSIM1 l); rewrite rfsSIM in rfsSIM1; red in rfsSIM1; desf; desf.
rewrite <- hplusA in UPD; eapply hplus_ra_own_r in UPD; eauto; desf.
eapply initialize_eq_raD in UPD; desc.
eby repeat eexists.
}
Case Armw.
{
RMWin_heap.
rewrite hdef_alt in DEF; desf; assert (DEF' := DEF).
rewrite qEQ, rOutEQ, !hplusA, <- !(hplusAC sbg), ghostEQ, (hplusC _ (gheap _ _ _)),
!(hplusAC (gheap _ _ _)) in DEF; desf.
assert (D := hplus_def_inv_r _ _ DEF); desf; rewrite D in ×.
symmetry in DEF; rewrite hplusC in DEF; apply hplus_gheap in DEF; subst.
assert (H: ∃ PP' QQ' perm' init', hf0 l = HVra PP' QQ' false perm' init' ∧
sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse).
{
cut (Hsim (Hdef h3 g3) (Hdef hf0 g0)).
{
intro SIM; red in SIM; desf.
specialize (SIM1 l).
destruct edge; ins.
× rewrite (qU0 _ EV), GET in ×.
eby eapply hplus_ra_own_l in DEF'; eauto; desc;
rewrite DEF' in SIM1; red in SIM1; des_if; desc; subst;
repeat eexists.
× assert (R := hplus_def_inv_r _ _ DEF'); desf.
apply hplus_def_inv_l in R; desf.
rewrite R, hplusAC in DEF'.
eapply hsum_has_ra_own in R; eauto; desc.
2: by repeat (rewrite In_map; eexists; split; try edone); apply rfsOutOK.
eby eapply hplus_ra_own_l in DEF'; eauto; desc;
rewrite DEF' in SIM1; red in SIM1; des_if; desc; subst;
repeat eexists.
× rewrite GET, <- hplusA in DEF'.
eby eapply hplus_ra_own_r in DEF'; eauto; desc;
rewrite DEF' in SIM1; red in SIM1; des_if; desc; subst;
repeat eexists.
}
{
rewrite pEQ, rInEQ, !hplusA in DEFin.
rewrite qEQ, rOutEQ, !hplusA, (hplusAC hrel'), (hplusAC hrel'), <- (hplusAC hacq') in DEF'.
rewrite <- D, <- DEFin.
do 2 rewrite (hplusAC hacq).
rewrite <- (hplusAC hrel).
by repeat (apply hplus_sim; try apply Hsim_refl;
try by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in D);
rewrite Hsim_sym.
}
}
desf.
eapply hplus_eq_ra_ownD in DEFin; eauto; desf.
× eexists (hb_sb _ _), _, _; repeat split; eauto.
eby repeat eexists.
× eapply hsum_eq_ra_ownD in DEFin; eauto; desf.
repeat (rewrite In_map in *; desf).
eexists (hb_rf _ _), _, _; repeat split; eauto.
by ins; apply rfsInOK.
eby repeat eexists.
}
Case Afence.
{
exploit FenceInDEF; eauto.
rewrite hdef_alt in DEF; intro DEFin; desf; rewrite DEF, DEFin in ×.
rewrite <- !hplusA in qEQ. symmetry in qEQ;
assert (D := hplus_def_inv_l _ _ qEQ); desf; rewrite D in ×.
symmetry in qEQ; apply hplus_gheap in qEQ; subst.
cut (Hsim (Hdef h3 g3) (Hdef hf0 g0)).
{
intro SIM.
red in SIM; desf.
eexists (hb_sb _ _), _, _; repeat split; eauto.
destruct edge; ins; try (by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf);
try (by red in EV; rewrite Heq in *; desf).
rewrite (qU0 _ EV), GET in *; desf.
specialize (SIM1 l); rewrite LA in SIM1; red in SIM1; desf; desf.
eby repeat eexists _, _.
}
{
rewrite hplusA in D.
rewrite Hsim_sym, pEQ, <- D.
apply hplus_sim; try congruence.
by apply Hsim_refl; intro U; rewrite U, !hplus_undef_l in ×.
apply hplus_sim; try done.
by intro U; rewrite U, hplus_undef_r in ×.
}
}
Qed.
Lemma heap_loc_ra_own_allocated PS PSg :
∀ lab sb rf mo hmap V v
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_A: ConsistentAlloc lab)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(HC: hist_closed sb rf V)
(VALID: hmap_valids lab sb rf hmap V)
edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
h g (GET: hmap edge = Hdef h g) l PP QQ perm init
(LA: h l = HVra PP QQ false perm init)
(ALL: sval (QQ v) ≠ Aemp)
(NF: sval (QQ v) ≠ Afalse),
∃ cpre c hf g' PP' QQ' perm' init',
sb cpre c ∧
lab cpre = Aalloc l ∧
hmap (hb_sb cpre c) = Hdef hf g' ∧
(cpre = hb_fst edge ∨ happens_before_union_rf sb rf cpre (hb_fst edge)) ∧
hf l = @HVra PS PSg PP' QQ' false perm' init'.
Proof.
intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
clear edge EV IN; intros.
red in VALID; desc.
generalize (VLD _ IN).
destruct (classic (lab (hb_fst edge) = Aalloc l)) as [|NEQ]; eauto.
× ins; destruct edge; ins.
by repeat (eexists; try edone); vauto.
by specialize (CONS_RF e'); rewrite EV, H in CONS_RF; desf.
by red in EV; rewrite H in EV.
× intros; exploit go_back_one_acq3; eauto; ins; desf.
assert (HB: happens_before_union_rf sb rf (hb_fst edge') (hb_fst edge)).
by destruct edge'; ins; desf; eauto with hb.
exploit (IH edge'); ins; desf; repeat (eexists; try edone); eauto with hb.
Qed.
Lemma heap_loc_ra_no_own PS PSg :
∀ lab sb rf mo hmap V v
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_A: ConsistentAlloc lab)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(HC: hist_closed sb rf V)
(VALID: hmap_valids lab sb rf hmap V)
edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
edge' (EV: edge_valid lab sb rf edge') (IN': In (hb_fst edge') V)
h g (GET: hmap edge = Hdef h g) l PP QQ perm init (LA: h l = @HVra PS PSg PP QQ true perm init)
h' g' (GET: hmap edge' = Hdef h' g') PP' QQ' perm' init' (LA': h' l = HVra PP' QQ' false perm' init'),
sval (QQ' v) = Aemp ∨ sval (QQ' v) = Afalse.
Proof.
intros; apply NNPP; intro.
eapply heap_loc_ra_own_allocated with (edge:=edge') in LA'; eauto.
eapply heap_loc_rmwacq_allocated with (edge:=edge) in LA; eauto.
desc; pose proof (CONS_A _ _ LA0 _ LA'0); subst; desc.
assert (INN: In cpre0 V) by (desf; eauto with hb); clear LA'2.
red in VALID; desc.
eapply VLD in INN; red in INN; desf; desc.
eapply qU in LA; eapply qU in LA'; congruence.
Qed.
Lemma wellformed PS PSg :
∀ acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_A: ConsistentAlloc lab)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(HC: hist_closed sb rf V)
(VALID: hmap_valids lab sb rf hmap V)
wpre w (INw: In w V)
l v (LAB: is_writeLV (lab w) l v)
(SBw: sb wpre w) hw gw
rfw (rfwOK: ∀ x, In x rfw ↔ rf w = Some x) (rfwND: NoDup rfw)
(MAPw: hmap (hb_sb wpre w) +!+ hsum (map hmap (map (hb_rf^~ w) rfw)) = Hdef hw gw)
PW QW isrmwW permW initW
(HW: hw l = HVra PW QW isrmwW permW initW)
T (NDt: NoDup T)
(ST: ∀ edge (IN: In edge T), In (hb_fst edge) V)
(TT: ∀ edge (IN: In edge T), edge_valid lab sb rf edge)
(INDEP: independent sb rf T)
hT gT (MAPt: hsum (map hmap T) = Hdef hT gT)
PT QT isrmwT permT initT (HT: hT l = @HVra PS PSg PT QT isrmwT permT initT),
implies (proj1_sig (PW v)) (Astar (proj1_sig (QT v)) Atrue).
Proof.
intros until T.
assert (∃ cpre c hf g PP' QQ' isrmw' perm' init',
<< SBc: sb cpre c >> ∧
<< LABcpre: lab cpre = Aalloc l >> ∧
<< MAPc: hmap (hb_sb cpre c) = Hdef hf g >> ∧
<< HFc: hf l = HVra PP' QQ' isrmw' perm' init' >> ∧
<< HBc: happens_before_union_rf sb rf cpre w >> ∧
<< IMPc: implies (sval (PW v)) (sval (PP' v)) >>).
{
unnw.
eapply hplus_eq_raD with (v:=v) in MAPw; eauto; desf.
× exploit heap_loc_rel_allocated; eauto; ins.
by eapply HC; vauto.
desc; repeat (eexists; try edone); ins; desc.
by desf; eauto with hb.
by eapply implies_trans; split; eauto; red; apply MAPw1.
× eapply hsum_eq_raD with (v:=v) in MAPw; eauto; desc.
repeat (rewrite In_map in *; desf); rewrite rfwOK in ×.
exploit heap_loc_rel_allocated; eauto; ins.
by eapply HC; vauto.
desc; repeat (eexists; try edone); ins; desc.
by desf; eauto with hb.
by eapply implies_trans; split; eauto; red; ins; apply MAPw3, MAPw1.
}
desc.
assert (cpreV: In cpre V) by (eapply hist_closedD; eauto).
induction T using
(well_founded_ind (wf_ltof (fun T ⇒ depth_metric (happens_before_union_rf sb rf) V (map hb_fst T)))).
rename H into IH.
case_eq (depth_metric (happens_before_union_rf sb rf) V (map hb_fst T)) as D; ins.
{
clear IH.
destruct T as [ | edge T]; unfold depth_metric in *; ins; vauto.
by rewrite hsum_nil in MAPt; inv MAPt.
rewrite count_eq_0 in D.
exploit (ST edge); ins; eauto.
destruct (D _ x0).
unfold is_pred, has, mydec.
apply Bool.orb_true_intro; left.
desf; destruct n; vauto.
}
exploit (get_deepest ACYCLIC HC (T:=T)); try done.
by intro; subst; clear - D; induction V; ins.
intro; desc.
destruct (classic (In (hb_sb cpre c) T)) as [ALLOC | NALLOC].
{
clear IH.
red in VALID; desc.
assert (cpreVALID := VLD _ cpreV).
assert (PP' = QQ').
{
clear - cpreVALID SBc LABcpre MAPc HFc.
red in cpreVALID; rewrite LABcpre in cpreVALID; desc.
apply qU in SBc; subst.
rewrite MAPc in *; desf; apply hplus_gheap in qEQ; subst; rewrite hupds in *; desf.
}
assert (AT: ∀ edge (IN: In edge T) hf g (MAP: hmap edge = Hdef hf g),
hf l = HVnone ∨ is_atomic (hf l)).
{
clear - HT MAPt NDt; ins.
exploit hsum_is_atomic; eauto.
by instantiate (1 := l); rewrite HT.
intro AT; desf.
rewrite In_map in AT; desf.
destruct (classic (x = edge)) as [EQ|NEQ]; desf.
by right; congruence.
apply In_implies_perm in AT1 as [T' PERM].
exploit Permutation_in; eauto.
intro IN'; ins; desf.
apply In_split in IN'; desf.
rewrite (hsum_perm (map_perm _ PERM)) in MAPt; ins.
rewrite map_app in MAPt; ins.
rewrite hsum_cons, hsum_app, hsum_cons, (hplusAC (hmap edge)), <- (hplusA (hmap x)), MAP, AT in MAPt.
apply hplus_def_inv_l in MAPt; desf.
rewrite hplus_unfold in MAPt; desf.
unfold is_atomic in AT0; desf.
specialize (HEAPcompat l); rewrite Heq in HEAPcompat; ins; desf; ins; eauto.
}
subst.
apply In_implies_perm in ALLOC as [T' ALLOC]; desf.
rewrite (hsum_perm (map_perm _ ALLOC)), !map_cons, hsum_cons, MAPc in MAPt.
apply hplus_def_inv in MAPt; desf.
specialize (PLUSv l).
assert (HZ: hz l = HVnone).
{
eapply hsum_none; eauto.
ins.
repeat (rewrite In_map in *; desf).
assert (INx: In x T).
{
apply In_implies_perm in IN1 as [T'' PERM].
apply perm_skip with (x := hb_sb cpre c) in PERM.
assert (PERM' := (Permutation_sym (perm_trans ALLOC PERM))).
by eapply Permutation_in with (l := _ :: x :: T''); vauto.
}
specialize (ST _ INx); specialize (TT _ INx).
assert (X: hb_fst x ≠ cpre).
{
intro EQ.
destruct x; ins; subst.
× red in cpreVALID; rewrite LABcpre in cpreVALID; desc.
apply qU in SBc; subst.
apply qU in TT; subst.
apply In_implies_perm in IN1 as [T'' PERM].
apply (Permutation_NoDup (perm_trans ALLOC (perm_skip _ PERM))) in NDt.
by apply NoDup_neq in NDt.
× by specialize (CONS_RF e'); desf; rewrite LABcpre in CONS_RF; desf.
× by red in TT; rewrite LABcpre in TT.
}
apply NNPP; intro NEQ.
exploit (AT x); eauto.
intro A; desf.
unfold is_atomic in A; desf.
exploit heap_loc_rel_allocated; eauto.
by eexists; split; eauto.
instantiate (1 := v).
intro CONTRA; desf; specialize (CONS_A _ _ CONTRA0 _ LABcpre);
rewrite CONS_A in *; try congruence.
apply Permutation_sym in ALLOC.
apply Permutation_in with (x := hb_sb cpre c) in ALLOC; vauto.
apply (INDEP _ ALLOC _ INx).
eexists; repeat split; eauto.
apply clos_trans_t1n in CONTRA3.
inv CONTRA3.
× inv H.
+ red in cpreVALID; rewrite LABcpre in cpreVALID; desc.
apply qU in SBc; subst.
apply qU in HB_SB; subst.
by left.
+ exfalso; clear - HB_RF CONTRA0 CONS_RF.
specialize (CONS_RF (hb_fst x)); desf.
by rewrite CONTRA0 in CONS_RF; desf.
× inv H.
+ red in cpreVALID; rewrite LABcpre in cpreVALID; desc.
apply qU in SBc; subst.
apply qU in HB_SB; subst.
by right; apply clos_t1n_trans.
+ exfalso; clear - HB_RF CONTRA0 CONS_RF.
specialize (CONS_RF y); desf.
by rewrite CONTRA0 in CONS_RF; desf.
}
rewrite HZ in *; unfold hvplus in PLUSv; desf; try congruence.
rewrite PLUSv in HT; desf.
eapply implies_trans; split; eauto.
clear; red; ins.
∃ h, hemp; repeat split; try done.
eby eapply assn_sem_def.
by apply hplus_emp_r.
}
{
exploit get_pres; eauto; ins; desf.
cut (∃ hT gT, hsum (map hmap
(map (hb_sb^~ (hb_fst edge)) pres_sb ++
map (hb_rf^~ (hb_fst edge)) pres_rf ++
filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T)) = Hdef hT gT ∧
∃ PT' QT' isrmwT' permT' initT',
hT l = HVra PT' QT' isrmwT' permT' initT' ∧
implies (sval (QT' v)) (Astar (sval (QT v)) Atrue)).
{ intro PRES; desf.
rewrite D in METR.
eapply (IH _ METR ND') in PRES0; eauto.
eapply implies_trans; split; eauto.
apply implies_frame with (F := Atrue) in PRES1.
eapply implies_trans; split; eauto.
clear; unfold implies; ins; desf.
by rewrite !hplusA in *; eexists _, _; repeat split; eauto.
}
clear IH D n.
red in VALID; desc.
assert (GHOSTS: ∀ hf g loc,
hsum (map hmap (filter (fun x ⇒ hb_fst x != hb_fst edge) T)) = Hdef hf g →
g loc ≠ None → ga loc ≠ Some (hb_fst edge)).
{
intros ? gg ? SUM ALL GALL.
eapply hsum_galloc in SUM; eauto; desf.
rewrite In_map in SUM; desf.
rewrite In_filter in SUM1; desf.
exploit ghost_allocated; eauto; try by intuition.
intro C; desf.
eby rewrite H0 in *; eapply neq_contra.
eby rewrite H0 in *; eapply DEEP.
}
assert (ALLOC: ∀ hf g loc,
hsum (map hmap (filter (fun x ⇒ hb_fst x != hb_fst edge) T)) = Hdef hf g →
hf loc ≠ HVnone →
∃ c, lab c = Aalloc loc ∧ c ≠ hb_fst edge).
{
ins.
eapply hsum_alloc in H; eauto; desf.
repeat (rewrite In_map in *; desf).
rewrite In_filter in H2; desf.
exploit heap_loc_allocated; try (exact H); try (exact H1); eauto.
eby eexists; split; eauto.
intro ALL; desf.
eexists; split; try edone.
intro; subst c0.
apply clos_refl_trans_hbUrfE in ALL0; desf.
eby eapply DEEP.
eby rewrite ALL0 in H3; eapply neq_contra.
}
assert (NALLOCl: lab (hb_fst edge) ≠ Aalloc l).
{
intro A.
cut (edge = hb_sb cpre c); [ ins; congruence | ].
assert (eVALID := VLD _ INe).
red in eVALID; rewrite A in eVALID; desc.
specialize (TT _ IN).
destruct edge; ins.
× rewrite (CONS_A _ _ LABcpre _ A) in ×.
by rewrite <- ((proj2 qU) _ SBc), <- ((proj2 qU) _ TT).
× specialize (CONS_RF e'); rewrite TT, A in CONS_RF; desf.
× by red in TT; rewrite A in TT.
}
exploit go_back_one_acq; eauto.
intro PRES; desc.
assert (<< PERMsb: Permutation pres_sb0 pres_sb >> ∧ << PERMrf: Permutation pres_rf0 pres_rf >>).
{
repeat split; apply NoDup_Permutation; ins.
by rewrite PRES3, Pb.
by rewrite PRES4, Pr.
}
desc.
rewrite (hsum_perm (map_perm _ (map_perm _ PERMsb))),
(hsum_perm (map_perm _ (map_perm _ PERMrf))) in PRES7.
clear PRES PRES0 PRES3 PRES4 PERMsb PERMrf pres_sb0 pres_rf0.
exploit independent_heap_compat; eauto;
try solve [ins; apply (INCL' _ IN0) | ins; apply (EVS' _ IN0) | eexists; split; eauto].
intro DEF; desc.
eexists _, _; split; try edone.
rewrite !map_app, !hsum_app in DEF.
apply PRES7 in DEF; clear PRES7; desc.
assert (DECOMP: ∃ hrest grest, Hdef h0 g1 = Hdef hT gT +!+ Hdef hrest grest).
{
clear - TT NDt MAPt IN ND' Pb Pr DEF PRES1 PRES2 PRES5 PRES6.
desf; ins.
× rewrite <- hsum_cons, <- !map_cons, <- !hsum_app, <- !map_app in DEF.
assert (SUBSET: ∀ a, In a T → In a (map (hb_sb (hb_fst edge)) posts_sb ++
map (hb_rf (hb_fst edge)) posts_rf ++
hb_sink (hb_fst edge) ::
filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T)).
{
ins.
assert (DECOMPt := (helper_perm_filter_post (hb_fst edge) T)); desf.
assert (AV := (TT _ H)).
apply (Permutation_in _ DECOMPt) in H.
repeat (apply In_app in H; desf).
× repeat (apply In_app; right).
apply (Permutation_in _ (helper_filter_decide_sink _ NDt)) in H.
desf; find_in_list.
× apply In_app; left.
rewrite In_map in H; desf; simpls.
rewrite <- PRES5 in AV.
rewrite In_map.
by eexists; split; eauto.
× apply In_app; right; apply In_app; left.
rewrite In_map in H; desf; simpls.
rewrite <- PRES6 in AV.
rewrite In_map.
by eexists; split; eauto.
}
exploit (@subset_perm hbcase); try exact SUBSET; try done.
{
apply nodup_app; repeat split; try (apply nodup_map; ins; congruence).
{ apply nodup_app; repeat split; try (apply nodup_map; ins; congruence).
{ apply NoDup_cons.
by rewrite In_filter; ins; apply or_not_and; eauto using neq_contra.
by apply NoDup_filter.
}
{ red; ins.
rewrite In_map in IN1; desf.
rewrite In_filter in IN2; desf.
eby ins; eapply neq_contra.
}
}
{ red; ins.
rewrite In_map in IN1; desf.
rewrite In_app in IN2; ins; desf.
by rewrite In_map in IN2; desf.
eby rewrite In_filter in IN2; ins; desf; eapply neq_contra.
}
}
intro PERM; desf.
rewrite (hsum_perm (map_perm _ PERM)), !map_app, hsum_app in DEF.
assert (REST := (hplus_def_inv_r _ _ DEF)); desf.
rewrite MAPt, REST in DEF.
by eexists _, _; symmetry; eauto.
× rewrite hplus_emp_l, <- !hsum_app, <- !map_app in DEF.
assert (SUBSET: ∀ a, In a T → In a (map (hb_sb (hb_fst edge)) posts_sb ++
map (hb_rf (hb_fst edge)) posts_rf ++
filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T)).
{
ins.
assert (DECOMPt := (helper_perm_filter_post (hb_fst edge) T)); desf.
assert (AV := (TT _ H)).
apply (Permutation_in _ DECOMPt) in H.
repeat (apply In_app in H; desf).
× repeat (apply In_app; right).
apply (Permutation_in _ (helper_filter_decide_sink _ NDt)) in H; desf.
specialize (TT _ i); desf.
× apply In_app; left.
rewrite In_map in H; desf; simpls.
rewrite <- PRES5 in AV.
rewrite In_map.
by eexists; split; eauto.
× apply In_app; right; apply In_app; left.
rewrite In_map in H; desf; simpls.
rewrite <- PRES6 in AV.
rewrite In_map.
by eexists; split; eauto.
}
exploit (@subset_perm hbcase); try exact SUBSET; try done.
{
apply nodup_app; repeat split; try (apply nodup_map; ins; congruence).
{ apply nodup_app; repeat split; try (apply nodup_map; ins; congruence).
by apply NoDup_filter.
red; ins.
rewrite In_map in IN1; desf.
eby rewrite In_filter in IN2; ins; desf; eapply neq_contra.
}
{ red; ins.
rewrite In_map in IN1; desf.
rewrite In_app in IN2; desf.
by rewrite In_map in IN2; desf.
eby rewrite In_filter in IN2; ins; desf; eapply neq_contra.
}
}
intro PERM; desf.
rewrite (hsum_perm (map_perm _ PERM)), !map_app, hsum_app in DEF.
assert (REST := (hplus_def_inv_r _ _ DEF)); desf.
rewrite MAPt, REST in DEF.
by eexists _, _; symmetry; eauto.
}
clear - DECOMP HT DEF0; desf.
symmetry in DECOMP; apply hplus_def_inv in DECOMP; desf.
specialize (DEFv l); specialize (PLUSv l); rewrite HT in *; clear HT.
ins; desf.
× apply DEF0 in PLUSv.
red in PLUSv; desf.
do 5 eexists; split; eauto.
clear; red; ins.
∃ h, hemp; repeat split; try done.
eby eapply assn_sem_def.
by rewrite hplus_emp_r.
× apply DEF0 in PLUSv.
red in PLUSv; desf.
do 5 eexists; split; eauto.
clear; red; ins.
∃ h, hemp; repeat split; try done.
eby eapply assn_sem_def.
by rewrite hplus_emp_r.
× apply DEF0 in PLUSv.
red in PLUSv; desf.
clear - DEFv.
specialize (DEFv v); red in DEFv; desf.
+ unfold hv_rval in DEFv.
rewrite DEFv.
do 5 eexists; split; eauto.
clear; red; ins.
∃ hemp, h; repeat split; try done.
eby eapply assn_sem_def.
by rewrite hplus_emp_l.
eby eapply assn_sem_def.
+ do 5 eexists; split; eauto.
rewrite DEFv, DEFv0.
by clear; red; ins.
× apply DEF0 in PLUSv.
red in PLUSv; desf.
do 5 eexists; split; eauto.
clear; red; ins.
rewrite assn_sem_assn_norm in H.
simpls.
desf.
repeat (eexists; try done).
eby eapply assn_sem_def.
}
Qed.
Lemma wellformed_w PS PSg :
∀ acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_A: ConsistentAlloc lab)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(HC: hist_closed sb rf V)
(VALID: hmap_valids lab sb rf hmap V)
wpre w (INw: In w V)
typ l v (LAB: lab w = Astore typ l v)
(SBw: sb wpre w) hw gw (MAPw: hmap (hb_sb wpre w) = Hdef hw gw)
PW QW isrmwW permW initW
(HW: hw l = HVra PW QW isrmwW permW initW)
T (NDt: NoDup T)
(ST: ∀ edge (IN: In edge T), In (hb_fst edge) V)
(TT: ∀ edge (IN: In edge T), edge_valid lab sb rf edge)
(INDEP: independent sb rf T)
hT gT (MAPt: hsum (map hmap T) = Hdef hT gT)
PT QT isrmwT permT initT (HT: hT l = @HVra PS PSg PT QT isrmwT permT initT),
implies (proj1_sig (PW v)) (Astar (proj1_sig (QT v)) Atrue).
Proof.
ins; eapply wellformed with (w := w) (rfw := nil); eauto; ins.
by rewrite LAB.
by split; ins; specialize (CONS_RF w); rewrite H, LAB in CONS_RF; desf.
eby rewrite hsum_nil, hplus_emp_r.
Qed.
Lemma wellformed_one PS PSg :
∀ acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_A: ConsistentAlloc lab)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(HC: hist_closed sb rf V)
(VALID: hmap_valids lab sb rf hmap V)
wpre w (INw: In w V)
l v (LAB: is_writeLV (lab w) l v)
(SBw: sb wpre w) hw gw
rfw (rfwOK: ∀ x, In x rfw ↔ rf w = Some x) (rfwND: NoDup rfw)
(MAPw: hmap (hb_sb wpre w) +!+ hsum (map hmap (map (hb_rf^~ w) rfw)) = Hdef hw gw)
PW QW isrmwW permW initW
(HW: hw l = HVra PW QW isrmwW permW initW)
rpre r (ST: In rpre V) (TT: sb rpre r)
(NIN: ¬ In r V)
hT gT (MAPt: hmap (hb_sb rpre r) = Hdef hT gT)
PT QT isrmwT permT initT (HT: hT l = @HVra PS PSg PT QT isrmwT permT initT),
implies (sval (PW v)) (Astar (sval (QT v)) Atrue).
Proof.
intros; eapply wellformed with (w := w) (T := hb_sb rpre r :: nil); eauto; ins; desf.
by red; ins; desf; ins; desf; eapply ACYCLIC, happens_before_union_rf_trans; vauto.
eby rewrite hsum_one.
Qed.
Lemma wellformed_one_w PS PSg :
∀ acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_A: ConsistentAlloc lab)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(HC: hist_closed sb rf V)
(VALID: hmap_valids lab sb rf hmap V)
wpre w (INw: In w V)
typ l v (LAB: lab w = Astore typ l v)
(SBw: sb wpre w) hw gw
(MAPw: hmap (hb_sb wpre w) = Hdef hw gw)
PW QW isrmwW permW initW
(HW: hw l = HVra PW QW isrmwW permW initW)
rpre r (ST: In rpre V) (TT: sb rpre r)
(NIN: ¬ In r V)
hT gT (MAPt: hmap (hb_sb rpre r) = Hdef hT gT)
PT QT isrmwT permT initT (HT: hT l = @HVra PS PSg PT QT isrmwT permT initT),
implies (proj1_sig (PW v)) (Astar (proj1_sig (QT v)) Atrue).
Proof.
ins; eapply wellformed_one with (w := w) (rfw := nil); eauto; ins.
by rewrite LAB.
by split; ins; specialize (CONS_RF w); rewrite H, LAB in CONS_RF; desf.
eby rewrite hsum_nil, hplus_emp_r.
Qed.
This page has been generated by coqdoc