Require Import Vbase Varith.
Require Import Relations Wellfounded Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslmodel fslassnlemmas fslhmap.
Require Import ihc initread.
Set Implicit Arguments.
Lemma go_back_one_acq :
∀ acts lab sb mo rf
(FIN : ExecutionFinite acts lab sb)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(CONS_A : ConsistentAlloc lab) hmap V
(HC : hist_closed sb rf V) e
(VALID : hmap_valid lab sb rf hmap e)
(INe : In e V) hFR l
(NALLOC : lab e ≠ Aalloc l)
(ALLOC : ∀ hf loc,
hFR = Hdef hf → hf loc ≠ HVnone →
∃ c : actid, lab c = Aalloc loc ∧ c ≠ 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
(EQ: hsum (map hmap (map (hb_sb^~ e) pres_sb)) +!+
hsum (map hmap (map (hb_rf^~ e) pres_rf)) +!+ hFR =
Hdef h),
let hS := if excluded_middle_informative (ann_sink lab e) then hmap (hb_sink e) else hemp in
∃ h0 : val → HeapVal,
hsum (map hmap (map (hb_sb e) posts_sb)) +!+
hsum (map hmap (map (hb_rf e) posts_rf)) +!+ hS +!+ hFR =
Hdef h0 ∧
∀ PP´ QQ´ isrmw´ perm´ init´ (LA: h0 l = HVra PP´ QQ´ isrmw´ perm´ init´),
hvplus_ra_ret (h l) QQ´).
Proof.
unfold hmap_valid, unique; 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, <- qEQ.
rewrite pEQ in EQ.
eexists,; try edone.
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,; try edone; ins.
by 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 qEQ, sEQ, !hplusA, (hplusAC hr), (hplusAC _ hF), <- (hplusA (hsingl _ _)), (hplusC (hsingl _ _)),
hplus_init1; ins.
rewrite hplusAC, pEQ, <- pEQ´, !hplusA in EQ.
assert (SIM: Hsim (Hdef h)
(hr +!+ hsingl l0 (HVra Wemp (hupd Remp v P) false None (Some HLCnormal)) +!+ hF +!+ hFR)).
{
rewrite <- EQ; apply hplus_sim; try congruence.
by apply Hsim_refl; intro U; rewrite U, hplus_undef_r in ×.
}
clear - SIM; red in SIM; desf.
eexists,; try edone.
ins; specialize (SIM1 l).
rewrite LA in SIM1; red in SIM1; 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 ?hsum_one in *; eauto.
by specialize (CONS_RF e); 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 sEQ, RFemp, hsum_nil, !hplus_emp_l, pEQ, qEQ in ×.
exploit hdef_upd_alloc2; eauto.
instantiate (2 := v); instantiate (1 := HLnormal); intro A; desf.
repeat (eexists; try edone); intros.
rewrite <- A0, LA; [by eexists; vauto|].
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 ×.
assert (SIM: Hsim (hmap (hb_sb e post) +!+ hsum (map hmap (map (hb_rf e) rfs)) +!+ hmap (hb_sink e) +!+ hFR)
(Hdef (initialize h l0))).
{
exploit (hplus_propagate_initialize hf l0); eauto.
{ rewrite qEQ, hplusA in UPD; clear - UPD; symmetry in UPD; eapply hplus_def_inv in UPD; desf.
specialize (DEFv l0); specialize (PLUSv l0).
unfold initialize in PLUSv; rewrite !hupds in *; ins; desf.
}
intro Ieq.
rewrite UPD, hplusA, hplusAC in Ieq.
do 2 rewrite (hplusAC _ (_ (hb_sb _ _))); rewrite <- hplusA, <- Ieq, Hsim_sym.
apply hplus_sim; try congruence.
by apply Hsim_sym.
by apply Hsim_refl; intro U; rewrite U, hplus_undef_r in ×.
}
red in SIM; desf.
eexists,; try edone.
clear - SIM1; ins.
specialize (SIM1 l); rewrite LA in SIM1; ins; desf; desf.
unfold initialize, hupd in Heq; desf; desf.
by rewrite Heq1.
by rewrite Heq.
}
Case Aalloc.
{
∃ (pre :: nil), nil, (post :: nil), nil; repeat (split; ins; desf);
rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto;
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).
{
rewrite pEQ, qEQ in *; destruct hFR; ins.
rewrite hplus_unfold in *; desf; vauto.
{ eexists,; ins; instantiate; ins.
unfold hupd in LA; desf; desf; repeat (eexists; try edone).
by rewrite LA; eexists; vauto.
}
destruct n0; intro l´; specialize (h0 l´).
unfold hupd in *; desf; desf.
specialize (ALLOC _ l0 eq_refl).
destruct (hf0 l0); desf; destruct ALLOC; desf;
by edestruct H0; eapply CONS_A; rewrite ?H, ?Heq.
}
{
rewrite pEQ, qEQ in *; destruct hFR; ins.
rewrite hplus_unfold in *; desf; vauto.
{ eexists,; ins; instantiate; ins.
unfold hupd in LA; desf; desf; repeat (eexists; try edone).
by rewrite LA; eexists; vauto.
}
destruct n0; intro l´; specialize (h0 l´).
unfold hupd in *; desf; desf.
specialize (ALLOC _ l0 eq_refl).
destruct (hf0 l0); desf; destruct ALLOC; desf;
by edestruct H0; eapply CONS_A; rewrite ?H, ?Heq.
}
}
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.
assert (SIM: Hsim (hmap (hb_sb e post) +!+ hFR) (Hdef h)).
{
rewrite <- EQ, Hsim_sym.
apply hplus_sim; try congruence.
2: by apply Hsim_refl; intro U; rewrite U, hplus_undef_r in ×.
rewrite pEQ, qEQ.
apply hplus_sim; try congruence.
by apply Hsim_refl; intro U; rewrite U, !hplus_undef_l in ×.
apply hplus_sim; try congruence.
by intro U; rewrite U, hplus_undef_r in ×.
}
clear - SIM; red in SIM; desf.
eexists,; try edone; ins.
specialize (SIM1 l); rewrite LA in SIM1; ins; desf; desf.
}
Qed.
Lemma go_back_one_rel :
∀ lab sb rf mo hmap edge
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(VAL: hmap_valid lab sb rf hmap (hb_fst edge))
(EV : edge_valid lab sb rf edge) hf
(GET: hmap edge = Hdef hf) l PP QQ isrmw perm init v
(LA : hf l = HVra PP QQ isrmw perm init)
(NA : lab (hb_fst edge) ≠ Aalloc l),
∃ edge´ hf´,
edge_valid lab sb rf edge´ ∧
hb_snd edge´ = Some (hb_fst edge) ∧
hmap edge´ = Hdef hf´ ∧
∃ 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.
× symmetry in qEQ; assert (X := hplus_def_inv _ _ qEQ); desf; rewrite X in ×.
eapply hsum_raD in X; eauto; desf; desf.
2: by rewrite <- GET; eapply In_mapI, In_mapI, qOK.
destruct isrmw´.
+ eapply hplus_ram_lD in qEQ; try edone; desc; clear qEQ2; desf.
eapply hsum_eq_raD with (v:=v) in pEQ; eauto.
desf; repeat (rewrite In_map in *; desf); eapply pOK in pEQ3.
by unfold implies; repeat (eexists; try edone); ins; apply pEQ1, qEQ0, X4.
+ eapply hplus_ra_lD in qEQ; try edone; desc; clear qEQ2; desf.
eapply hsum_eq_raD with (v:=v) in pEQ; eauto.
desf; repeat (rewrite In_map in *; desf); eapply pOK in pEQ3.
by unfold implies; repeat (eexists; try edone); ins; apply pEQ1, qEQ0, X4.
× by specialize (CONS_RF e´); rewrite EV, Heq in CONS_RF; desf.
× symmetry in qEQ; rewrite GET in qEQ.
destruct isrmw.
+ eapply hplus_ram_rD in qEQ; try edone; desc; clear qEQ2; desf.
eapply hsum_eq_raD with (v:=v) in pEQ; eauto.
desf; repeat (rewrite In_map in *; desf); eapply pOK in pEQ3.
by unfold implies; repeat (eexists; try edone); ins; apply pEQ1, qEQ0.
+ eapply hplus_ra_rD in qEQ; try edone; desc; clear qEQ2; desf.
eapply hsum_eq_raD with (v:=v) in pEQ; eauto.
desf; repeat (rewrite In_map in *; desf); eapply pOK in pEQ3.
by unfold implies; repeat (eexists; try edone); ins; apply pEQ1, qEQ0.
}
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;
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.
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.
- ∃ (hb_sb pre e); eexists; repeat split; try edone.
destruct isrmw´0.
eapply hplus_ram_rD in pEQ´; eauto; desc; clarify.
by unfold implies; repeat eexists; try edone; intros; apply pEQ´0, qEQ3, qEQ1.
eapply hplus_ra_rD in pEQ´; eauto; desc; clarify.
by unfold implies; repeat eexists; try edone; intros; apply pEQ´0, 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 hh 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.
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 ×.
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, hsum (map hmap (map (hb_rf e) rfs)) +!+ hmap (hb_sink e) = Hdef h ∧
∃ PP´ QQ´ isrmw´ perm´ init´,
h l = HVra PP´ QQ´ isrmw´ perm´ init´ ∧
(∀ h : heap, assn_sem (sval (PP v)) h → assn_sem (sval (PP´ v)) h)).
{
red in rfsSIM; desf.
eexists,; try edone.
apply hplus_def_inv in rfsSIM; desf.
exploit hsum_raD; eauto.
by rewrite <- GET; eapply In_mapI, In_mapI, 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.
destruct isrmwflag.
+ eapply hplus_ram_rD in UPD; eauto; desc.
eapply initialize_eq_raD in UPD; desc.
repeat eexists; try edone.
unfold implies; intuition.
+ eapply hplus_ra_rD in UPD; eauto; desc.
eapply initialize_eq_raD in UPD; desc.
repeat eexists; try edone.
unfold implies; intuition.
× assert (RF: ∃ h, hsum (map hmap (map (hb_rf e) rfs)) +!+ hmap (hb_sink e) = Hdef h ∧
∃ 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,; 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.
destruct isrmwflag.
+ eapply hplus_ram_rD in UPD; eauto; desc.
eapply initialize_eq_raD in UPD; desc.
repeat eexists; try edone.
unfold implies; intuition.
+ eapply hplus_ra_rD in UPD; eauto; desc.
eapply initialize_eq_raD in UPD; desc.
repeat eexists; try edone.
unfold implies; intuition.
}
Case Afence.
{
cut (Hsim (hmap (hb_sb pre (hb_fst edge))) (hmap (hb_sb (hb_fst edge) post))).
{
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 pEQ, qEQ.
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 :
∀ 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 (GET: hmap edge = Hdef h) l PP QQ isrmw perm init
(LA: h l = HVra PP QQ isrmw perm init),
∃ cpre c hf PP´ QQ´ isrmw´ perm´ init´,
sb cpre c ∧
lab cpre = Aalloc l ∧
hmap (hb_sb cpre c) = Hdef hf ∧
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.
generalize (VALID _ 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 :
∀ 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 (GET: hmap edge = Hdef h) l PP QQ isrmw perm init
(LA: h l = HVra PP QQ isrmw perm init),
∃ cpre c hf PP´ QQ´ isrmw´,
sb cpre c ∧
lab cpre = Aalloc l ∧
hmap (hb_sb cpre c) = Hdef hf ∧
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.
instantiate (1 := v); intro ALL; desc.
assert (cpreVALID: hmap_valid lab sb rf hmap cpre).
{
apply VALID; desf.
eapply hist_closedD; eauto.
}
red in cpreVALID; rewrite ALL0 in cpreVALID; desc.
rewrite ((proj2 qU) _ ALL), ALL1 in ×.
revert ALL3; desf.
by rewrite hupds in ALL2.
rewrite hupds in ALL2; desf.
repeat eexists; eauto using hupds.
Qed.
Lemma go_back_one_rmwacq :
∀ lab sb rf mo hmap edge
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(VAL: hmap_valid lab sb rf hmap (hb_fst edge))
(EV : edge_valid lab sb rf edge) hf
(GET: hmap edge = Hdef hf) l PP QQ perm init
(LA : hf l = HVra PP QQ true perm init)
(NA : lab (hb_fst edge) ≠ Aalloc l),
∃ edge´ hf´,
edge_valid lab sb rf edge´ ∧
hb_snd edge´ = Some (hb_fst edge) ∧
hmap edge´ = Hdef hf´ ∧
∃ PP´ QQ´ perm´ init´, hf´ l = HVra PP´ QQ´ true perm´ init´.
Proof.
unfold hmap_valid, unique; ins; desf; desc; try (destruct DISJ; desc); try clear TYP.
Case Askip.
{
symmetry in qEQ; destruct edge; ins; subst.
× assert (X := hplus_def_inv _ _ qEQ); desf; rewrite X in ×.
eapply hsum_raD in X; eauto; desf; desf.
2: by rewrite <- GET; eapply In_mapI, In_mapI, qOK.
rewrite X2 in *; ins.
eapply hplus_ram_lD in qEQ; try edone; desc; clear qEQ2; desf.
eapply hsum_eq_ra_rmwD in pEQ; 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 GET in qEQ.
eapply hplus_ram_rD in qEQ; try edone; desc; clear qEQ2; desf.
eapply hsum_eq_ra_rmwD in pEQ; eauto.
desf; repeat (rewrite In_map in *; desf); rewrite pOK in ×.
by repeat (eexists; try edone).
}
Case Aalloc.
{
destruct edge; ins; subst;
try (by specialize (CONS_RF e´); rewrite EV, Heq in CONS_RF; desf);
try (by red in EV; rewrite Heq in *; desf);
apply qU0 in EV; subst e´; rewrite GET in *; desf;
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.
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_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 *; desf.
unfold hupd in LA; desf; desf.
by ∃ (hb_sb pre e); repeat (eexists; try edone).
}
Case Astore .
{
eexists (hb_sb _ _), _; repeat split; try edone.
symmetry in UPD; destruct edge; ins.
× rewrite (qU0 _ EV), GET in ×.
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 rfsSIM; desf.
eapply hsum_raD in rfsSIM; eauto; desf.
2: by rewrite <- GET; eapply In_mapI, In_mapI, rfsOK.
assert (EQ: ∃ PP QQ perm init, hf1 l = HVra PP QQ true perm init).
eby generalize (PLUSv l); rewrite rfsSIM, rfsSIM3; clear; ins; desf; repeat eexists.
desf.
specialize (rfsSIM1 l); rewrite EQ in rfsSIM1; red in rfsSIM1; desf; desf.
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.
eapply hplus_ram_rD in rfsSIM; eauto; desc.
clear rfsSIM3; specialize (rfsSIM1 l); rewrite rfsSIM in rfsSIM1; red in rfsSIM1; desf; desf.
eapply hplus_ram_rD in UPD; eauto; desc.
eapply initialize_eq_raD in UPD; desc.
eby repeat eexists.
}
Case Afence.
{
cut (Hsim (hmap (hb_sb pre (hb_fst edge))) (hmap (hb_sb (hb_fst edge) post))).
{
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 pEQ, qEQ.
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 :
∀ 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 (GET: hmap edge = Hdef h) l PP QQ perm init
(LA: h l = HVra PP QQ true perm init),
∃ cpre c hf PP´ QQ´ perm´ init´,
sb cpre c ∧
lab cpre = Aalloc l ∧
hmap (hb_sb cpre c) = Hdef hf ∧
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.
generalize (VALID _ 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 :
∀ lab sb rf mo hmap edge
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(VAL: hmap_valid lab sb rf hmap (hb_fst edge))
(EV : edge_valid lab sb rf edge) hf
(GET: hmap edge = Hdef hf) l PP QQ perm init
(LA : hf l = HVra 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´,
edge_valid lab sb rf edge´ ∧
hb_snd edge´ = Some (hb_fst edge) ∧
hmap edge´ = Hdef hf´ ∧
∃ 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.
{
symmetry in qEQ; destruct edge; ins; subst.
× assert (X := hplus_def_inv _ _ qEQ); desf; rewrite X in ×.
eapply hsum_has_ra_own in X; eauto; desf; desf.
2: by rewrite <- GET; eapply In_mapI, In_mapI, qOK.
eapply hplus_ra_own_l in qEQ; try edone; desc.
eapply hsum_eq_ra_ownD with (v:=v) in pEQ; 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 GET in qEQ.
eapply hplus_ra_own_r in qEQ; try edone; desc.
eapply hsum_eq_ra_ownD in pEQ; eauto.
desf; repeat (rewrite In_map in *; desf); rewrite pOK in ×.
by repeat (eexists; try edone).
}
Case Aalloc.
{
destruct edge; ins; subst;
try (by specialize (CONS_RF e´); rewrite EV, Heq in CONS_RF; desf);
try (by red in EV; rewrite Heq in *; desf);
apply qU0 in EV; subst e´; rewrite GET in *; desf;
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.
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_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.
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.
destruct edge; ins.
× rewrite (qU0 _ EV), GET in ×.
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 rewrite <- GET; eapply In_mapI, In_mapI, rfsOK.
eapply hplus_ra_own_l in rfsSIM; eauto; desf.
specialize (rfsSIM1 l); rewrite rfsSIM in rfsSIM1; red in rfsSIM1; desf; desf.
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.
eapply hplus_ra_own_r in rfsSIM; eauto; desf.
specialize (rfsSIM1 l); rewrite rfsSIM in rfsSIM1; red in rfsSIM1; desf; desf.
eapply hplus_ra_own_r in UPD; eauto; desf.
eapply initialize_eq_raD in UPD; desc.
eby repeat eexists.
}
Case Afence.
{
cut (Hsim (hmap (hb_sb pre (hb_fst edge))) (hmap (hb_sb (hb_fst edge) post))).
{
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 pEQ, qEQ.
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 :
∀ 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 (GET: hmap edge = Hdef h) 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 PP´ QQ´ perm´ init´,
sb cpre c ∧
lab cpre = Aalloc l ∧
hmap (hb_sb cpre c) = Hdef hf ∧
(cpre = hb_fst edge ∨ happens_before_union_rf sb rf cpre (hb_fst edge)) ∧
hf l = HVra PP´ QQ´ false perm´ init´.
Proof.
intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
clear edge EV IN; intros.
generalize (VALID _ 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 :
∀ 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 (GET: hmap edge = Hdef h) l PP QQ perm init (LA: h l = HVra PP QQ true perm init)
h´ (GET: hmap edge´ = Hdef h´) 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.
eapply VALID in INN; red in INN; desf; desc.
eapply qU in LA; eapply qU in LA´; congruence.
Qed.
Lemma wellformed :
∀ 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
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)
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 (MAPt: hsum (map hmap T) = Hdef hT)
PT QT isrmwT permT initT (HT: hT l = HVra PT QT isrmwT permT initT),
implies (proj1_sig (PW v)) (Astar (proj1_sig (QT v)) Atrue).
Proof.
intros until T.
assert (∃ cpre c hf PP´ QQ´ isrmw´ perm´ init´,
<< SBc: sb cpre c >> ∧
<< LABcpre: lab cpre = Aalloc l >> ∧
<< MAPc: hmap (hb_sb cpre c) = Hdef hf >> ∧
<< 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.
assert (cpreVALID := VALID _ 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; rewrite hupds in *; desf.
}
assert (AT: ∀ edge (IN: In edge T) hf (MAP: hmap edge = Hdef hf), 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 (h l); rewrite Heq in h; 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.
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, 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 ∧
∃ 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.
apply (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.
assert (ALLOC: ∀ hf loc,
hsum (map hmap (filter (fun x ⇒ hb_fst x != hb_fst edge) T)) = Hdef hf →
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.
intro ALL; desf.
eexists,; 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 := VALID _ 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.
}
red in VALID; desc.
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) | eby split].
intro DEF; desc.
eexists,; try edone.
rewrite !map_app, !hsum_app in DEF.
apply PRES7 in DEF; clear PRES7; desc.
assert (DECOMP: ∃ hrest, Hdef h0 = Hdef hT +!+ Hdef hrest).
{
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 :
∀ 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 (MAPw: hmap (hb_sb wpre w) = Hdef hw)
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 (MAPt: hsum (map hmap T) = Hdef hT)
PT QT isrmwT permT initT (HT: hT l = HVra 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.
by ins; rewrite hsum_nil, hplus_emp_r.
Qed.
Lemma wellformed_one :
∀ 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
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)
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 (MAPt: hmap (hb_sb rpre r) = Hdef hT)
PT QT isrmwT permT initT (HT: hT l = HVra 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.
by rewrite hsum_one.
Qed.
Lemma wellformed_one_w :
∀ 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
(MAPw: hmap (hb_sb wpre w) = Hdef hw)
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 (MAPt: hmap (hb_sb rpre r) = Hdef hT)
PT QT isrmwT permT initT (HT: hT l = HVra 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.
by ins; rewrite hsum_nil, hplus_emp_r.
Qed.
This page has been generated by coqdoc