Require Import Vbase Varith.
Require Import Relations Wellfounded Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 rslassn rslmodel rslassnlemmas rslhmap.
Set Implicit Arguments.
Lemma hplus_eq_ra_rmwD h h1 h2 l PP QQ init :
hplus h1 h2 = Hdef h →
h l = HVra PP QQ true init →
∃ hf PP' QQ' init',
(h1 = Hdef hf ∨ h2 = Hdef hf) ∧ hf l = HVra PP' QQ' true init'.
Proof.
ins; eapply hplus_def_inv in H; desf.
specialize (DEFv l); rewrite PLUSv in *; clear PLUSv.
red in DEFv; desf; ins; desf; try destruct isrmwflag; ins; desf;
repeat eexists; try edone; eauto.
Qed.
Lemma hsum_eq_ra_rmwD:
∀ h' hs l PP QQ init,
hsum hs = Hdef h' →
h' l = HVra PP QQ true init →
∃ h'' PP' QQ' init', In (Hdef h'') hs ∧ h'' l = HVra PP' QQ' true init'.
Proof.
intros until 0; induction[h' PP QQ init] hs; ins; [by inv H|].
rewrite hsum_cons in *; eapply hplus_eq_ra_rmwD in H; eauto.
desf; eauto 8; exploit IHhs; eauto; ins; desf; eauto 8.
Qed.
Lemma hplus_eq_ra_ownD h h1 h2 l PP QQ init v :
hplus h1 h2 = Hdef h →
h l = HVra PP QQ false init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ hf PP' QQ' init',
(h1 = Hdef hf ∨ h2 = Hdef hf) ∧ hf l = HVra PP' QQ' false init'
∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof.
ins; eapply hplus_def_inv in H; desf.
specialize (DEFv l); rewrite PLUSv in *; clear PLUSv.
red in DEFv; desf; ins; desf; try destruct isrmwflag; ins; desf;
try solve [repeat (eexists; try eassumption); eauto].
case_eq (sval (QQ0 v)); ins;
try solve [clear Heq0; repeat (eexists; try eassumption); eauto;
instantiate; congruence].
case_eq (sval (QQ1 v)); ins;
try solve [clear Heq; repeat (eexists; try eassumption); eauto;
instantiate; congruence].
by rewrite H, H0, assn_norm_star_false in ×.
by rewrite H, H0, assn_norm_star_emp_r in ×.
clear Heq; repeat (eexists; try eassumption); eauto.
by intro H0; apply H1; rewrite H, H0, assn_norm_star_emp, assn_norm_emp.
by intro H0; apply H2; rewrite H, H0, assn_norm_star_emp.
Qed.
Lemma hsum_eq_ra_ownD:
∀ h' hs l PP QQ init v,
hsum hs = Hdef h' →
h' l = HVra PP QQ false init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ h'' PP' QQ' init',
In (Hdef h'') hs ∧ h'' l = HVra PP' QQ' false init'
∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof.
intros until 0; induction[h' PP QQ init] hs; ins; [by inv H|].
rewrite hsum_cons in *; eapply hplus_eq_ra_ownD in H; eauto.
desf; eauto 10; exploit IHhs; eauto; ins; desf; eauto 12.
Qed.
Lemma hplus_ra_own_l h h1 h2 l PP QQ init v :
hplus (Hdef h1) h2 = Hdef h →
h1 l = HVra PP QQ false init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ PP' QQ' init',
h l = HVra PP' QQ' false init' ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof.
ins; eapply hplus_def_inv in H; desf.
specialize (DEFv l); rewrite PLUSv in *; clear PLUSv;
red in DEFv; desf; ins; desf; try destruct isrmwflag; ins; desf;
try solve [repeat eexists; eauto].
by exfalso; destruct (DEFv v); desf.
repeat eexists; ins; intro; [
apply assn_norm_star_eq_emp in H |
apply assn_norm_star_eq_false in H ]; desf; auto;
eapply H1; destruct (QQ v); ins; congruence.
Qed.
Lemma hplus_ra_own_r h h1 h2 l PP QQ init v :
hplus h1 (Hdef h2) = Hdef h →
h2 l = HVra PP QQ false init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ PP' QQ' init',
h l = HVra PP' QQ' false init' ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof. by rewrite hplusC; apply hplus_ra_own_l. Qed.
Lemma hsum_has_ra_own h hs hf l PP QQ init v :
hsum hs = Hdef h →
In (Hdef hf) hs →
hf l = HVra PP QQ false init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ PP' QQ' init',
h l = HVra PP' QQ' false init' ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof.
induction[h PP QQ init] hs; ins.
rewrite hsum_cons in *; desf.
eapply hplus_ra_own_l; eauto.
exploit hplus_def_inv; eauto; ins; desf.
exploit IHhs; eauto; intro; desf.
rewrite x1 in *; eapply hplus_ra_own_r; eauto.
Qed.
Lemma go_back_one_acq :
∀ mt acts lab sb mo rf
(FIN : ExecutionFinite acts lab sb)
(CONS_A : ConsistentAlloc lab) hmap V
(HC : hist_closed mt lab sb rf mo 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_sw posts_sb posts_sw,
NoDup pres_sb ∧
NoDup pres_sw ∧
NoDup posts_sb ∧
NoDup posts_sw ∧
(∀ x : actid, In x pres_sb ↔ sb x e) ∧
(∀ x : actid, In x pres_sw ↔ ann_sw lab rf x e) ∧
(∀ x : actid, In x posts_sb ↔ sb e x) ∧
(∀ x : actid, In x posts_sw ↔ ann_sw lab rf e x) ∧
(∀ h
(EQ: hsum (map hmap (map (hb_sb^~ e) pres_sb)) +!+
hsum (map hmap (map (hb_sw^~ e) pres_sw)) +!+ hFR =
Hdef h),
∃ h0 : val → HeapVal,
hsum (map hmap (map (hb_sb e) posts_sb)) +!+
hsum (map hmap (map (hb_sw e) posts_sw)) +!+ hFR =
Hdef h0 ∧
∀ PP' QQ' isrmw' init' (LA: h0 l = HVra PP' QQ' isrmw' init'),
hvplus_ra2_ret (h l) QQ').
Proof.
unfold hmap_valid, unique; ins; desf; desf.
Case Askip.
∃ pres, nil, posts, nil; repeat (split; ins).
by red in H; desf; rewrite Heq in ×.
by red in H; desf; rewrite Heq in ×.
eapply vshift_hack in qEQ.
rewrite pEQ, qEQ, hplusA, hplusAC, hplusC in EQ.
eapply hplus_def_inv in EQ; desf.
repeat (eexists; try edone).
eby rewrite PLUSv; intros; eapply hvplus_ra2.
Case Aalloc.
∃ (pre :: nil), nil, (post :: nil), nil; repeat (split; ins; desf);
rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
by red in H; desf; rewrite Heq in ×.
by red in H; desf; rewrite Heq in ×.
rewrite pEQ, qEQ in *; destruct hFR; ins.
rewrite hplus_unfold in *; desf; vauto.
eexists; split; ins; instantiate; ins.
unfold hupd in LA; desf; desf; repeat (eexists; try edone).
by rewrite LA; eexists; vauto.
destruct n; 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 Aalloc .
∃ (pre :: nil), nil, (post :: nil), nil; repeat (split; ins; desf);
rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
by red in H; desf; rewrite Heq in ×.
by red in H; desf; rewrite Heq in ×.
rewrite pEQ, qEQ in *; destruct hFR; ins.
rewrite hplus_unfold in *; desf; vauto.
eexists; split; ins; instantiate; ins.
unfold hupd in LA; desf; desf; repeat (eexists; try edone).
by rewrite LA; eexists; vauto.
destruct n; 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 Aload .
pose proof (has_sw_pres rf e FIN); desc.
∃ (pre :: nil), sws, (post :: nil), nil; ins; repeat (split; ins; desf);
rewrite ?hsum_one in *; eauto.
by red in H; desf; rewrite Heq in ×.
rewrite qEQ, hsum_nil, hplus_emp_l;
rewrite (hplusC _ hFR), <- hplusA in EQ.
exploit hplus_def_inv; try eapply EQ; ins; desf.
eexists; split; try edone; ins.
rewrite PLUSv; eapply hvplus_ra2; eauto.
Case Aload .
∃ (pre :: nil), sws, (post :: nil), nil; ins; repeat (split; ins; desf);
rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
by red in H; desf; rewrite Heq in ×.
rewrite pEQ, swsEQ, <- pEQ', hplusA, (hplusAC _ hF),
<- hplus_init1 with (init := true), hplusA,
<- (hplusA _ hF), <- (hplusA _ (hplus _ hF)), <- qEQ, hplusC in EQ.
eapply hplus_def_inv in EQ; ins; desf.
repeat (eexists; try edone).
intros; rewrite PLUSv; eapply hvplus_ra2; eauto.
Case Astore .
pose proof (has_sw_succs rf e FIN); desc.
∃ (pre :: nil), nil, (post :: nil), sws; ins; repeat (split; ins; desf);
rewrite ?hsum_one in *; eauto.
by red in H; desf; rewrite Heq in ×.
assert (M: hsum (map hmap (map (hb_sw e) sws)) = hemp).
generalize (fun x ⇒ proj1 (INsws x)); clear - wEQ.
by induction sws; ins; rewrite hsum_cons, IHsws, hplus_emp_r; eauto.
rewrite M; rewrite hsum_nil, pEQ, qEQ in ×.
exploit (hdef_upd_alloc2); eauto.
instantiate (1 := v); 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), sws; ins; repeat (split; ins; desf);
rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
by red in H; desf; rewrite Heq in ×.
rewrite pEQ in ×.
eapply vshift_hack in UPD.
assert (∃ RR QQ isrmw init, hf l0 = HVra RR QQ isrmw init).
clear - UPD; symmetry in UPD; eapply hplus_def_inv in UPD; desf.
specialize (DEFv l0); eapply hvplus_ra2 in DEFv; eauto using hupds.
rewrite <- PLUSv in DEFv; clear - DEFv.
by unfold initialize in *; rewrite hupds in *; desf; eauto.
desf.
exploit (hplus_init_def2 _ l0 _ EQ); [congruence|intro X].
generalize X; intro Z.
rewrite UPD in X.
rewrite !hplusA, !(hplusAC hsink), <- hplusA, hplusC in X.
generalize X; intro Y.
eapply hplus_def_inv in X; desf.
repeat (eexists; try edone).
ins; cut (hvplus_ra2_ret (initialize h l0 l) QQ').
by clear; unfold initialize, hupd; desf; try rewrite Heq0.
by rewrite PLUSv; eapply hvplus_ra2; eauto.
Case Armw.
∃ (pre :: nil), swsIn, (post :: nil), swsOut; ins; repeat (split; ins; desf);
rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
rewrite pEQ in ×.
eapply vshift_hack in UPD.
assert (∃ RR QQ isrmw init, hi l0 = HVra RR QQ isrmw init).
clear - UPD; symmetry in UPD; eapply hplus_def_inv in UPD; desf.
specialize (DEFv l0); eapply hvplus_ra2 in DEFv; eauto using hupds.
rewrite <- PLUSv in DEFv; clear - DEFv.
by destruct (hi l0); eauto.
desf.
rewrite <- hplusA, iEQ, UPD, !hplusA, !(hplusAC hsink), <- hplusA, hplusC in EQ.
eapply hplus_def_inv in EQ; desc.
eexists; split; try edone; ins.
by rewrite PLUSv; eapply hvplus_ra2; eauto.
Qed.
Lemma go_back_one_acq2 :
∀ acts lab sb rf
(FIN : ExecutionFinite acts lab sb)
(CONS_A : ConsistentAlloc lab) hmap a
(VALID : hmap_valid lab sb rf hmap a)
hFR typ l v pre post sws
(LL: lab a = Aload typ l v)
(Lp: unique (sb^~ a) pre)
(Lq: unique (sb a) post)
(LwND: NoDup sws)
(LwOK: ∀ x, In x sws ↔ ann_sw lab rf x a)
hp hq hw PP QQ PP' QQ'
(Ep: hmap (hb_sb pre a) = Hdef hp)
(Eq: hmap (hb_sb a post) = Hdef hq)
(Ew: hsum (map hmap (map (hb_sw^~ a) sws)) = Hdef hw)
(Gp: hp l = HVra PP QQ false true)
(Gq: hq l = HVra PP' QQ' false true) Q
(NF: ¬ Asim Q Afalse)
(L: << Gw : hw l = HVnone >> ∧
<< ASIM: Asim (sval (QQ v)) (Astar (sval (QQ' v)) Q) >>
∨ ∃ Pw' Qw' initw',
<< Gw : hw l = HVra Pw' Qw' false initw' >> ∧
<< ASIM: Asim (Astar (sval (QQ v)) (sval (Qw' v))) (Astar (sval (QQ' v)) Q) >>)
(ALLOC : ∀ hf loc,
hFR = Hdef hf →
hf loc ≠ HVnone → ∃ c : actid, lab c = Aalloc loc ∧ c ≠ a) h
(EQ: hmap (hb_sb pre a) +!+
hsum (map hmap (map (hb_sw^~ a) sws)) +!+ hFR =
Hdef h),
∃ h0 : val → HeapVal,
hmap (hb_sb a post) +!+ hFR =
Hdef h0 ∧
∀ PP' QQ' isrmw' (LA: h0 l = HVra PP' QQ' isrmw' true),
∃ PP0 QQ0, h l = HVra PP0 QQ0 isrmw' true ∧
Asim (sval (QQ0 v)) (Astar (sval (QQ' v)) Q).
Proof.
intros; unfold hmap_valid, unique in VALID; ins; rewrite LL in *; desc.
eapply Lp in pU; eapply Lq in qU; subst pre0 post0; clear pU0 qU0.
rewrite pEQ in *; clarify.
destruct DISJ; desc.
rewrite qEQ; rewrite (hplusC _ hFR), <- hplusA in EQ.
exploit hplus_def_inv; try eapply EQ; ins; desc.
eexists; split; try edone; ins.
exfalso; eapply hplus_raD in x0; eauto; clear L; desf; congruence.
assert (PRM: Permutation sws0 sws).
by apply NoDup_Permutation; ins; rewrite swsOK, LwOK.
assert (Hdef hw0 = Hdef hw); clarify.
by rewrite <- swsEQ, <- Ew,
(hsum_perm (Permutation_map _ (Permutation_map _ PRM))).
simpls; rewrite Ew in *; clarify.
rewrite <- pEQ', hplusA, (hplusAC _ hF),
<- hplus_init1 with (init := true), hplusA,
<- (hplusA _ hF), <- (hplusA _ (hplus _ hF)), <- qEQ, hplusC in EQ.
eapply hplus_def_inv in EQ; ins; desc.
eexists; split; try edone; ins.
rewrite PLUSv, LA in *; rename DEFv into DDD; specialize (DDD l); clear PLUSv; desc; clarify.
rewrite hupds, qEQ in ×.
eapply hplus_def_inv in EQ; desc; clarify.
rewrite EQ, PLUSv in *; desc; clarify.
eapply hplus_def_inv in EQ; desc; clarify.
specialize (DEFv0 l); specialize (DEFv l).
rewrite PLUSv0 in ×.
eapply hplus_def_inv in pEQ'; desc; clarify.
specialize (DEFv1 l).
rewrite hupds, PLUSv1 in *; clear hp PLUSv1 PLUSv hq PLUSv0 qEQ pEQ qD.
eapply hplus_def_inv in EQ0; desc; clarify.
simpl; do 2 eexists; split;f_equal; ins; auto using orbF.
destruct isrmw'.
{ cut (Asim Aemp Q).
by clear; intros H; eapply Asim_trans, Asim_star, H;
eauto using Asim.
specialize (DEFv2 l); rewrite PLUSv in *; des; rewrite Gw in *; ins;
rewrite !hupds in *; ins; desf; rewrite hupds in *; ins; clarify; ins;
desf; ins; desc; specialize (DDD v); rewrite hupds in *;
red in DDD; ins; desf; rewrite ?DDD1 in *; ins; rewrite <- DDD in *; Asim_simpl_asm ASIM; try apply Asim1 in ASIM; desf; eauto using Asim.
eapply Asim_trans in ASIM; [|eapply Asim_starC]; apply Asim1 in ASIM; desf; eauto using Asim.
}
specialize (DEFv2 l); rewrite PLUSv in *; des; rewrite Gw in *; ins;
destruct (hz2 l); ins; clarify; ins; rewrite hupds in *; ins;
destruct (hz l); ins; clarify; rewrite hupds in *;
rewrite ?assn_norm_emp, ?Asim_norm_l, ?Asim_norm_r in *; simpls;
Asim_simpl_asm ASIM; instantiate; Asim_simpl.
by eauto using Asim.
by eauto using Asim.
by apply Asim_rem2; eauto using Asim.
by eauto using Asim.
by apply Asim_rem2; eauto using Asim.
by eauto using Asim.
by apply Asim_rem2; eauto using Asim.
Qed.
Lemma go_back_one_rel :
∀ lab sb rf hmap edge
(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 init v
(LA : hf l = HVra PP QQ isrmw init)
(NA : lab (hb_fst edge) ≠ Aalloc l),
∃ edge' hf',
edge_valid lab sb rf edge' ∧
hb_snd edge' = hb_fst edge ∧
hmap edge' = Hdef hf' ∧
∃ PP' QQ' isrmw' init',
hf' l = HVra PP' QQ' isrmw' init' ∧
(∀ h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h).
Proof.
unfold hmap_valid, unique; ins; desf; desf.
Case Askip.
destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
eapply vshift_hack in qEQ.
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 repeat (eexists; try edone); ins; apply pEQ1, qEQ0, X2.
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 repeat (eexists; try edone); ins; apply pEQ1, qEQ0, X2.
Case Aalloc.
destruct edge; ins; subst; 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 Aalloc.
destruct edge; ins; subst; 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; try (by red in EV; rewrite Heq in *; desf); [].
apply qU0 in EV; subst e'; rewrite GET in *; desf.
rewrite pEQ in *; desf.
by ∃ (hb_sb pre e); repeat (eexists; try edone).
Case Aload .
destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
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; repeat (eexists; try edone); ins; try eapply qEQ1 in H.
eapply hplus_eq_raD with (v:=v) in qEQ; eauto.
desf.
eapply hsum_eq_raD with (v:=v) in swsEQ; eauto; desc.
repeat (rewrite In_map in *; desf); rewrite swsOK in ×.
repeat (eexists; try edone); ins; eauto.
generalize (qEQ1 h), (qEQ3 h), (swsEQ1 h); clear - H; tauto.
∃ (hb_sb pre e); destruct (hmap (hb_sb pre e)); try done.
eexists; repeat split; ins.
destruct isrmw'0.
eapply hplus_ram_rD in pEQ'; eauto; desc; clarify.
by repeat eexists; try edone; intros; apply pEQ'0, qEQ3, qEQ1.
eapply hplus_ra_rD in pEQ'; eauto; desc; clarify.
by repeat eexists; try edone; intros; apply pEQ'0, qEQ3, qEQ1.
Case Astore .
destruct edge; ins; subst; try (by rewrite wEQ in GET; try done; 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 .
∃ (hb_sb pre (hb_fst edge)); destruct (hmap (hb_sb pre (hb_fst edge))); try done.
eexists; repeat split; ins.
eapply vshift_hack in UPD.
destruct edge; ins.
symmetry in UPD.
rewrite !(hplusAC (hsum _)) in UPD.
exploit hplus_def_inv_l; eauto; intro Z; desf.
exploit hsum_raD; eauto; [|intro W; desf].
by rewrite <- GET; eapply In_mapI, In_mapI, swsOK.
destruct isrmw'.
rewrite Z in *; eapply hplus_ram_lD in UPD; eauto; desc; clarify.
eapply initialize_eq_raD in UPD; desc.
by repeat eexists; try edone; intros; apply UPD0; eauto.
rewrite Z in *; eapply hplus_ra_lD in UPD; eauto; desc; clarify.
eapply initialize_eq_raD in UPD; desc.
by repeat eexists; try edone; intros; apply UPD0; eauto.
apply qU0 in EV; subst e'; rewrite GET in *; desf.
destruct isrmw.
symmetry in UPD; rewrite hplusAC in UPD.
eapply hplus_ram_lD in UPD; eauto; desc; clarify.
eapply initialize_eq_raD in UPD; desc.
by repeat eexists; try edone; intros; apply UPD0; eauto.
symmetry in UPD; rewrite hplusAC in UPD.
eapply hplus_ra_lD in UPD; eauto; desc; clarify.
eapply initialize_eq_raD in UPD; desc.
by repeat eexists; try edone; intros; apply UPD0; eauto.
Case Armw.
eapply vshift_hack in UPD.
assert (X: ∃ PP' QQ' isrmw' init',
hi l = HVra PP' QQ' isrmw' init' ∧
(∀ h0, assn_sem (sval (PP v)) h0 → assn_sem (sval (PP' v)) h0)).
{
destruct edge; ins.
rewrite !(hplusAC (hsum _)) in UPD.
symmetry in UPD; exploit hplus_def_inv_l; eauto.
intro Z; desf; exploit hsum_raD; eauto; [|intro W; desf].
by rewrite <- GET; eapply In_mapI, In_mapI, swsOutOK.
destruct isrmw'.
rewrite Z in *; eapply hplus_ram_lD in UPD; eauto; desc; clarify.
by repeat eexists; try edone; intros; apply UPD0; eauto.
rewrite Z in *; eapply hplus_ra_lD in UPD; eauto; desc; clarify.
by repeat eexists; try edone; intros; apply UPD0; eauto.
apply qU0 in EV; subst e'; rewrite GET in *; desf.
rewrite hplusAC in UPD.
destruct isrmw.
symmetry in UPD; eapply hplus_ram_lD in UPD; eauto; desc; clarify.
by repeat eexists; try edone; intros; apply UPD0; eauto.
symmetry in UPD; eapply hplus_ra_lD in UPD; eauto; desc; clarify.
by repeat eexists; try edone; intros; apply UPD0; eauto.
}
desc.
eapply hplus_eq_raD with (v:=v) in iEQ; eauto; desf.
eexists (hb_sb pre _), _; ins; repeat (split; try edone); ins; eauto.
by repeat eexists; try edone; intros; apply iEQ1; auto.
eapply hsum_eq_raD with (v:=v) in iEQ; eauto; desf.
repeat (rewrite In_map in *; desf); rewrite swsInOK in ×.
eexists (hb_sw _ _); ins; repeat (eexists; try edone); ins; eauto.
generalize (iEQ1 h), (iEQ3 h), (X0 h); clear - H; tauto.
Qed.
Lemma heap_loc_rel_allocated :
∀ mt lab sb rf mo hmap V v
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo 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 init
(LA: h l = HVra PP QQ isrmw init),
∃ cpre c hf PP' QQ' isrmw' init',
sb cpre c ∧
lab cpre = Aalloc l ∧
hmap (hb_sb cpre c) = Hdef hf ∧
hf l = HVra PP' QQ' isrmw' init' ∧
(cpre = hb_fst edge ∨ happens_before lab sb rf mo cpre (hb_fst edge)) ∧
(∀ h, assn_sem (proj1_sig (PP v)) h → assn_sem (proj1_sig (PP' v)) h).
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; try (by red in EV; rewrite H in *; desf); [].
repeat (eexists; try edone); vauto.
}
intros; exploit go_back_one_rel; eauto; ins; desf.
assert (HB: happens_before lab sb rf mo (hb_fst edge') (hb_fst edge)).
by destruct edge'; ins; subst; eauto with hb.
exploit (IH edge'); eauto.
intro; desf; repeat eexists; eauto with hb; ins; desf; eauto.
Qed.
Lemma go_back_one_rmwacq :
∀ lab sb rf hmap edge
(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 init
(LA : hf l = HVra PP QQ true init)
(NA : lab (hb_fst edge) ≠ Aalloc l),
∃ edge' hf',
edge_valid lab sb rf edge' ∧
hb_snd edge' = hb_fst edge ∧
hmap edge' = Hdef hf' ∧
∃ PP' QQ' init', hf' l = HVra PP' QQ' true init'.
Proof.
unfold hmap_valid, unique; ins; desf; desf.
Case Askip.
destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
eapply vshift_hack in qEQ.
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.
rewrite X1 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).
Case Aalloc.
destruct edge; ins; subst; 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 Aalloc.
destruct edge; ins; subst; 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; try (by red in EV; rewrite Heq in *; desf); [].
apply qU0 in EV; subst e'; rewrite GET in *; desf.
rewrite pEQ in *; desf.
by ∃ (hb_sb pre e); repeat (eexists; try edone).
Case Aload .
destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
apply qU0 in EV; subst e'; rewrite GET in *; desf.
symmetry in qEQ; 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.
eapply hsum_eq_ra_rmwD in swsEQ; eauto; desc.
repeat (rewrite In_map in *; desf); rewrite swsOK in ×.
by repeat (eexists; try edone); ins; eauto.
∃ (hb_sb pre e); destruct (hmap (hb_sb pre e)); try done.
eexists; repeat split; ins.
eapply hplus_ram_rD in pEQ'; eauto; desc; clarify.
by repeat eexists; try edone.
Case Astore .
destruct edge; ins; subst; try (by rewrite wEQ in GET; try done; 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 .
∃ (hb_sb pre (hb_fst edge)); destruct (hmap (hb_sb pre (hb_fst edge))); try done.
eexists; repeat split; ins.
eapply vshift_hack in UPD.
destruct edge; ins.
rewrite !(hplusAC (hsum _)) in UPD.
symmetry in UPD; exploit hplus_def_inv_l; eauto.
intro Z; desf; exploit hsum_raD; eauto; [|intro W; desf].
by rewrite <- GET; eapply In_mapI, In_mapI, swsOK.
rewrite W1 in *; ins.
rewrite Z in *; eapply hplus_ram_lD in UPD; eauto; desc; clarify.
eapply initialize_eq_raD in UPD; desc.
by repeat eexists; try edone.
apply qU0 in EV; subst e'; rewrite GET in *; desf.
symmetry in UPD; rewrite hplusAC in UPD.
eapply hplus_ram_lD in UPD; eauto; desc; clarify.
eapply initialize_eq_raD in UPD; desc.
by repeat eexists; try edone; intros; apply UPD0; eauto.
Case Armw.
eapply vshift_hack in UPD.
assert (X: ∃ PP' QQ' init', hi l = HVra PP' QQ' true init').
{
destruct edge; ins.
rewrite !(hplusAC (hsum _)) in UPD.
symmetry in UPD; exploit hplus_def_inv_l; eauto.
intro Z; desf; exploit hsum_raD; eauto; [|intro W; desf].
by rewrite <- GET; eapply In_mapI, In_mapI, swsOutOK.
rewrite W1 in *; ins.
rewrite Z in *; eapply hplus_ram_lD in UPD; eauto; desc; clarify.
by repeat eexists; try edone.
rewrite hplusAC in UPD.
apply qU0 in EV; subst e'; rewrite GET in *; desf.
symmetry in UPD; eapply hplus_ram_lD in UPD; eauto; desc; clarify.
by repeat eexists; try edone.
}
desc.
eapply hplus_eq_ra_rmwD in iEQ; eauto; desf.
by eexists (hb_sb pre _), _; ins; repeat (split; try edone); ins; eauto.
eapply hsum_eq_ra_rmwD in iEQ; eauto; desf.
repeat (rewrite In_map in *; desf); rewrite swsInOK in ×.
by eexists (hb_sw _ _); ins; repeat (eexists; try edone); ins; eauto.
Qed.
Lemma heap_loc_rmwacq_allocated :
∀ mt lab sb rf mo hmap V
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo 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 init
(LA: h l = HVra PP QQ true init),
∃ cpre c hf PP' QQ' init',
sb cpre c ∧
lab cpre = Aalloc l ∧
hmap (hb_sb cpre c) = Hdef hf ∧
hf l = HVra PP' QQ' true 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; try (by red in EV; rewrite H in *; desf); [].
repeat (eexists; try edone); vauto.
}
intros; exploit go_back_one_rmwacq; eauto; ins; desf.
assert (HB: happens_before lab sb rf mo (hb_fst edge') (hb_fst edge)).
by destruct edge'; ins; subst; eauto with hb.
exploit (IH edge'); eauto.
Qed.
Lemma go_back_one_acq3 :
∀ lab sb rf hmap edge
(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 init
(LA : hf l = HVra PP QQ false 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' = hb_fst edge ∧
hmap edge' = Hdef hf' ∧
∃ PP' QQ' init',
hf' l = HVra PP' QQ' false init' ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof.
unfold hmap_valid, unique; ins; desf; desf.
Case Askip.
destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
eapply vshift_hack in qEQ.
symmetry in qEQ.
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); eauto.
Case Aalloc.
destruct edge; ins; subst; 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 Aalloc.
destruct edge; ins; subst; 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; try (by red in EV; rewrite Heq in *; desf); [].
apply qU0 in EV; subst e'; rewrite GET in *; desf.
rewrite pEQ in *; desf.
by ∃ (hb_sb pre e); repeat (eexists; try edone).
Case Aload .
destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
apply qU0 in EV; subst e'; rewrite GET in *; desf.
rewrite hplusAC in qEQ.
symmetry in qEQ; eapply hplus_eq_ra_ownD in qEQ; eauto.
desf.
eapply hsum_eq_ra_ownD in swsEQ; eauto; desc.
repeat (rewrite In_map in *; desf); rewrite swsOK in ×.
by repeat (eexists; try edone); ins; eauto.
eexists (hb_sb pre e), _; repeat split; eauto.
eapply hplus_eq_ra_ownD in qEQ; eauto; desf.
by unfold hupd in qEQ3; desf; desf; ins.
by eapply hplus_ra_own_r in pEQ'; eauto.
Case Astore .
destruct edge; ins; subst; try (by rewrite wEQ in GET; try done; 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 .
∃ (hb_sb pre (hb_fst edge)); destruct (hmap (hb_sb pre (hb_fst edge))); try done.
eexists; repeat split; ins.
eapply vshift_hack in UPD.
destruct edge; ins.
rewrite !(hplusAC (hsum _)) in UPD.
symmetry in UPD; exploit hplus_def_inv_l; eauto.
intro Z; desf; exploit hsum_has_ra_own; eauto; [|intro W; desf].
by rewrite <- GET; eapply In_mapI, In_mapI, swsOK.
rewrite Z in *; eapply hplus_ra_own_l in UPD; eauto; desc; clarify.
eapply initialize_eq_raD in UPD; desc.
by repeat (eexists; try edone).
apply qU0 in EV; subst e'; rewrite GET in *; desf.
symmetry in UPD; rewrite hplusAC in UPD.
eapply hplus_ra_own_l in UPD; eauto; desc; clarify.
eapply initialize_eq_raD in UPD; desc.
by repeat (eexists; try edone).
Case Armw.
eapply vshift_hack in UPD.
assert (X: ∃ PP' QQ' init',
hi l = HVra PP' QQ' false init' ∧
sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse).
{
destruct edge; ins.
rewrite !(hplusAC (hsum _)) in UPD.
symmetry in UPD; exploit hplus_def_inv_l; eauto.
intro Z; desf; exploit hsum_has_ra_own; eauto; [|intro W; desf].
by rewrite <- GET; eapply In_mapI, In_mapI, swsOutOK.
by rewrite Z in *; eapply hplus_ra_own_l in UPD; eauto; desc; clarify.
rewrite hplusAC in UPD.
apply qU0 in EV; subst e'; rewrite GET in *; desf.
by symmetry in UPD; eapply hplus_ra_own_l in UPD; eauto; desc; clarify.
}
desc.
eapply hplus_eq_ra_ownD with (v := v) in iEQ; eauto; desf.
by eexists (hb_sb pre _); ins; repeat (eexists; try edone).
eapply hsum_eq_ra_ownD in iEQ; eauto; desf.
repeat (rewrite In_map in *; desf); rewrite swsInOK in ×.
by eexists (hb_sw _ _); ins; repeat (eexists; try edone).
Qed.
Lemma heap_loc_ra_own_allocated :
∀ mt lab sb rf mo hmap V v
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo 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 init
(LA: h l = HVra PP QQ false init)
(ALL: sval (QQ v) ≠ Aemp)
(NF: sval (QQ v) ≠ Afalse),
∃ cpre c hf PP' QQ' init',
sb cpre c ∧
lab cpre = Aalloc l ∧
hmap (hb_sb cpre c) = Hdef hf ∧
(cpre = hb_fst edge ∨ happens_before lab sb rf mo cpre (hb_fst edge)) ∧
hf l = HVra PP' QQ' false 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; try (by red in EV; rewrite H in *; desf); [].
repeat (eexists; try edone); vauto.
}
intros; exploit go_back_one_acq3; eauto; ins; desc.
assert (HB: happens_before lab sb rf mo (hb_fst edge') (hb_fst edge)).
by destruct edge'; ins; subst; eauto with hb.
exploit (IH edge'); ins; desf; repeat (eexists; try edone); eauto with hb.
Qed.
Lemma heap_loc_ra_no_own :
∀ mt lab sb rf mo hmap V v
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo 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 init (LA: h l = HVra PP QQ true init)
h' (GET: hmap edge' = Hdef h') PP' QQ' init' (LA': h' l = HVra PP' QQ' false 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 hb_helper1 lab sb rf mo e e' a :
unique (sb e) e' →
(∀ x, ¬ synchronizes_with lab sb rf mo e x) →
happens_before lab sb rf mo e a →
happens_before lab sb rf mo e' a ∨ e' = a.
Proof.
unfold happens_before; intros.
apply clos_trans_t1n in H1.
inv H1; red in H2; desf; try apply H in H2; try apply H0 in H2;
vauto; eauto using clos_t1n_trans.
Qed.
Lemma helper_acyclic_last :
∀ A (r: A → A → Prop)
(ACYCL: acyclic r) e i
(MHB: clos_refl_trans _ r e i) R,
∃ b,
<< PRM: In b (i :: R) >> ∧
<< BEFORE: clos_refl_trans _ r e b >> ∧
<< NAFTER: ∀ c, In c (i :: R) → ¬ clos_trans _ r b c >>.
Proof.
unfold not; induction R; ins; unfold NW.
by repeat eexists; eauto; ins; desf; subst; eauto using t_step, clos_refl_trans.
desc; destruct (classic (clos_trans _ r b a)).
∃ a; repeat split; eauto.
by clear -BEFORE H; rewrite clos_refl_transE in *; desf; eauto using clos_trans.
by intros ? [IN|[IN|IN]] HB; subst; eauto using clos_trans.
∃ b; repeat split; try tauto.
by intros ? [IN|[IN|IN]] HB; subst; eauto using clos_trans.
Qed.
Lemma helper_hb_last :
∀ A lab sb rf mo
(ACYCL: IrreflexiveHB lab sb rf mo) b (Q: A) R (IN: In (b, Q) R) e
(MHB: e = b ∨ happens_before lab sb rf mo e b),
∃ b Q,
<< PRM: In (b, Q) R >> ∧
<< BEFORE: e = b ∨ happens_before lab sb rf mo e b >> ∧
<< NAFTER: ∀ b' Q',
In (b', Q') R →
¬ happens_before lab sb rf mo b b' >>.
Proof.
intros; desc.
eapply In_implies_perm in IN; desc.
assert (MHB': clos_refl_trans actid (imm_happens_before lab sb rf mo) e b).
by clear -MHB; desf; [|induction MHB]; eauto using clos_refl_trans.
pose proof (helper_acyclic_last ACYCL MHB' (map (@fst _ _) l')).
ins; desc.
assert (∃ Q, In (b0, Q) R).
destruct PRM; subst.
∃ Q; apply (Permutation_in _ (Permutation_sym IN)), In_eq.
apply In_map in H; destruct H as [[? Q'] [? ?]].
∃ Q'; apply (Permutation_in _ (Permutation_sym IN)); vauto.
desc; ∃ b0, Q0; repeat split; try edone.
by eapply clos_refl_transE in BEFORE; destruct BEFORE; vauto.
red; ins; eapply NAFTER.
apply (Permutation_in _ IN) in H0; ins; rewrite In_map in ×.
clear - H0; desf; vauto.
Qed.
Definition RTrel A lab sb rf mo V RT RT' :=
length (A:=A) (fst RT) < length (A:=A) (fst RT') ∨
length (fst RT) = length (fst RT') ∧
depth_metric (happens_before lab sb rf mo) V (map hb_fst (snd RT)) <
depth_metric (happens_before lab sb rf mo) V (map hb_fst (snd RT')).
Definition RTrelWF A lab sb rf mo V :
well_founded (RTrel (A:=A) lab sb rf mo V).
Proof.
red; intros [a b].
remember (existT (fun _ ⇒ list hbcase) (length a) b) as c; revert a b Heqc.
induction c using
(well_founded_ind
(wf_lexprod _ _ _ _
(wf_ltof (fun x ⇒ x))
(fun _ ⇒ wf_ltof (fun x ⇒
depth_metric (happens_before lab sb rf mo) V (map hb_fst x))))).
intros; desf; constructor; intros [m n] R; eapply H; ins.
red in R; desf; ins; try rewrite R in *; vauto.
Qed.
Definition read_loses_perm hmap lab sb rf a l v (Q: assn_mod) :=
∃ typ apre apost w,
<< LL: lab a = Aload typ l v >> ∧
<< Lp: unique (sb^~ a) apre >> ∧
<< Lq: unique (sb a) apost >> ∧
<< Lw: ann_sw lab rf w a >> ∧
∃ hp hq hw PP QQ PP' QQ',
<< Ep: hmap (hb_sb apre a) = Hdef hp >> ∧
<< Eq: hmap (hb_sb a apost) = Hdef hq >> ∧
<< Ew: hmap (hb_sw w a) = Hdef hw >> ∧
<< Gp: hp l = HVra PP QQ false true >> ∧
<< Gq: hq l = HVra PP' QQ' false true >> ∧
<< PREC: precise (sval Q) >> ∧
<< LSEM: assn_sem (sval Q) (Hdef hw) >> ∧
( << Gw : hw l = HVnone >> ∧
<< ASIM: Asim (sval (QQ v)) (Astar (sval (QQ' v)) (sval Q)) >>
∨ ∃ Pw' Qw' initw',
<< Gw : hw l = HVra Pw' Qw' false initw' >> ∧
<< ASIM: Asim (Astar (sval (QQ v)) (sval (Qw' v))) (Astar (sval (QQ' v)) (sval Q)) >>).
Definition ssnd (x : actid × assn_mod) := sval (snd x).
Lemma wellformed_only_reads_helper :
∀ (goal : assn_mod → Prop) mt acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo V)
(VALID: hmap_valids lab sb rf hmap V)
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)
(R: list (actid × assn_mod))
(NDr: NoDup (map (@fst _ _) R))
(SR: ∀ a Q (IN: In (a, Q) R), In a V) l v
(DEL: ∀ a Q (IN: In (a, Q) R), read_loses_perm hmap lab sb rf a l v Q)
(NHB: ∀ a (INt: In a T) b Q (INr: In (b,Q) R),
hb_snd a ≠ b ∧ ¬ happens_before lab sb rf mo (hb_snd a) b)
(INDEP: independent lab sb rf mo T)
hT (MAPt: hsum (map hmap T) = Hdef hT)
PT QT isrmwT initT (HT: hT l = HVra PT QT isrmwT initT)
(PROVE:
∀ h h' PP' QQ' isrmw' init'
(ALLOC: ∀ a apost (SB: sb a apost) (A: lab a = Aalloc l) h''
(D: hmap (hb_sb a apost) = Hdef h''), h'' l = h' l)
(VS: vshift (Hdef h) (Hdef h'))
(G : h l = HVuval ∨ ∃ isrmw QQ, h l = HVra QQ QQ isrmw false)
(G': h' l = HVra PP' QQ' isrmw' init'),
∃ FRAME, goal (mk_assn_mod (Astar (sval (QQ' v)) FRAME))),
∃ FRAME, goal (mk_assn_mod (Astar (sval (QT v)) (foldr Astar (map ssnd R) FRAME))).
Proof.
intros until R; revert NDt ST TT.
remember (R, T) as RT; revert R T HeqRT.
induction RT using (well_founded_ind (RTrelWF lab sb rf mo V)).
specialize (fun R' T' X ⇒ H (R',T') X _ _ eq_refl).
ins; desf.
exploit (get_deepest ACYCLIC HC (T:=T)); try done.
by intro; subst; clear - HT MAPt; inv MAPt.
intro; desc.
destruct (classic (∃ b Q, In (b, Q) R ∧
(hb_fst edge = b ∨ happens_before lab sb rf mo (hb_fst edge) b))).
{
desc.
pose proof (helper_hb_last ACYCLIC _ _ H0 H1).
clear b Q H0 H1; desc.
assert (LP := DEL _ _ PRM); red in LP; desc.
eapply In_implies_perm in PRM; desc.
destruct BEFORE as [BEFORE|BEFORE]; subst.
{
pose proof (get_pres ACYCLIC HC _ NDt IN ST TT DEEP INDEP); ins; desc.
clear METR.
ins.
assert (METR': RTrel lab sb rf mo V (l', map (hb_sb^~ (hb_fst edge)) pres_sb ++
map (hb_sw^~ (hb_fst edge)) pres_sw ++
filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T)
(R, T)).
by left; simpl; rewrite (Permutation_length PRM); ins.
specialize (H _ _ METR' ND' INCL' EVS').
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).
intros ? ? U NEQ; eapply hsum_alloc in U; eauto; desc.
rewrite In_map in *; desc; rewrite In_filter in *; desc.
exploit heap_loc_allocated; eauto; try (by destruct x; ins; eauto).
destruct (eqP (hb_fst x) (hb_fst edge)); ins; desc; eexists; split; eauto; intro; desc.
subst; desf; congruence.
assert (∃ hT',
hsum
(map hmap
(map (hb_sb^~ (hb_fst edge)) pres_sb ++
map (hb_sw^~ (hb_fst edge)) pres_sw ++
filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T)) =
Hdef hT' ∧
∃ PT' QT' isrmwT' initT',
hT' l = HVra PT' QT' isrmwT' initT' ∧
Asim (sval (QT' v)) (Astar (sval (QT v)) (sval Q))).
{
clear H; exploit independent_heap_compat; eauto;
try solve [by intros ? ? X; eapply INCL' in X|
by intros ? ? X; eapply EVS' in X].
intros [hhh M]; simpls; eexists; split; try edone.
rewrite !map_app, !hsum_app in ×.
clear METR' IND' EVS' ND' INCL'.
assert (IN' := IN).
eapply TT in IN'; destruct edge; ins;
[by red in IN'; rewrite LL in IN'; desc|].
eapply Lq in IN'; subst.
assert (J: Permutation T (hb_sb e e' :: filter (fun x : hbcase ⇒ hb_fst x != e) T)).
eapply NoDup_Permutation; eauto.
constructor; eauto using NoDup_filter.
by rewrite In_filter; simpl; rewrite eqxx; intro; desc.
clear LP0; split; ins; rewrite In_filter in *; desf; eauto.
case (eqP (hb_fst x) e); eauto.
left; eapply TT in H; destruct x; ins; subst;
[by red in H; rewrite LL in H; desc|].
by eapply Lq in H; subst.
clear IN.
assert (pres_sb = apre :: nil).
destruct Lp as [Lp Lp'].
destruct pres_sb as [|aa pres_sb]; ins; [by eapply Pb in Lp|].
(assert (apre = aa) by eapply Lp', Pb, In_eq); subst aa; f_equal.
destruct pres_sb; ins; inv NDb; destruct H1; left; symmetry.
by eapply Lp', Pb; vauto.
subst; ins; rewrite hsum_one, Ep in ×.
revert MAPt; rewrite (hsum_perm (map_perm _ J)); simpl.
rewrite hsum_cons, Eq; intro.
assert (P: pres_sw = w :: nil).
by apply NoDup_eq_one; clear - NDw Pw Lw; ins;
rewrite Pw in *; unfold ann_sw in *; desf.
rewrite <- Ep in M.
subst; simpls; rewrite hsum_one in ×.
exploit (go_back_one_acq2 (rf:=rf) FIN CONS_A hmap); try eapply LwND; eauto;
simpls; rewrite ?hsum_one; try edone.
by intro G; eapply sim_assn_sem in LSEM; [|apply Asim_sym, G].
intro K; desc.
rewrite Eq, MAPt in K; clarify.
eapply hplus_ra_lD in MAPt; eauto; desc; rewrite MAPt in *; desc; clarify.
assert (initT = true) by desf; subst; clear MAPt2.
specialize (K0 _ _ _ eq_refl); desc; rewrite K0.
do 4 eexists; try edone.
}
clear ND' INCL' EVS' METR' hT MAPt HT; desc.
cut (∃ FRAME,
goal
(mk_assn_mod
(Astar (sval (QT' v)) (foldr Astar (List.map ssnd l') FRAME)))).
clear -H2 PRM; intro M; desc.
∃ FRAME; erewrite AsimD; [eapply M|].
eapply Asim_trans.
by eapply (Asim_star (Asim_refl _)), (foldr_star_perm2 (Permutation_map _ PRM)).
eapply Asim_trans.
by simpl; eapply Asim_sym, Asim_starA.
by eapply Asim_star, Asim_refl; eapply Asim_sym, H2.
eapply H; eauto.
by eapply (Permutation_NoDup (Permutation_map _ PRM)) in NDr; inv NDr.
eby ins; eapply SR, Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].
eby ins; eapply DEL, Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].
{ clear LP0; intros; rewrite !In_app, !In_map, In_filter in *; desf; ins; eauto.
3: eapply NHB; eauto;
eby ins; eapply Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].
× split.
by intro; subst;
eapply (Permutation_NoDup (Permutation_map _ PRM)) in NDr;
inv NDr; destruct H5; rewrite In_map; vauto.
eby eapply NAFTER, Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].
× split.
by intro; subst;
eapply (Permutation_NoDup (Permutation_map _ PRM)) in NDr;
inv NDr; destruct H5; rewrite In_map; vauto.
eby eapply NAFTER, Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].
}
}
assert (METR': RTrel lab sb rf mo V (l', hb_sb apre b :: hb_sw w b :: T) (R, T)).
by left; simpl; rewrite (Permutation_length PRM); ins.
specialize (H _ _ METR').
assert (ND': NoDup (hb_sb apre b :: hb_sw w b :: T)).
clear LP0; constructor; try constructor; ins;
intro X; desf; eapply NHB in X.
2: by ins; eapply Permutation_in, In_eq; eapply (Permutation_sym PRM).
by ins; desf.
2: by ins; eapply Permutation_in, In_eq; eapply (Permutation_sym PRM).
by ins; desf.
assert (INDEP': independent lab sb rf mo (hb_sb apre b :: hb_sw w b :: T)).
{ clear LP0 H; destruct Lp, Lq.
red; ins; destruct IN1 as [|[|]], IN2 as [|[|]];
desc; subst; ins; try rewrite LwOK in *; eauto;
try solve[by desf; eauto with hb].
eapply NHB in H3.
2: by eapply Permutation_in, In_eq; eapply (Permutation_sym PRM).
by desf; eauto with hb.
eapply NHB in H3.
2: by eapply Permutation_in, In_eq; eapply (Permutation_sym PRM).
by desf; eauto with hb.
}
clear INDEP.
assert (INCL' : ∀ edge0,
In edge0 (hb_sb apre b :: hb_sw w b :: T) →
In (hb_fst edge0) V).
assert (In b V).
by ins; eapply SR, Permutation_in, In_eq; eapply (Permutation_sym PRM).
by destruct Lp; clear LP0; ins; desf; ins; try rewrite LwOK in *;
eauto using hist_closedD with hb.
assert (EV' : ∀ edge0,
In edge0 (hb_sb apre b :: hb_sw w b :: T) →
edge_valid lab sb rf edge0).
by destruct Lp; ins; clear BEFORE LP0; desf; ins; eauto.
assert (∃ hT',
hsum (hmap (hb_sb apre b) :: hmap (hb_sw w b) :: map hmap T) = Hdef hT' ∧
∃ PT' QT' isrmwT' initT',
hT' l = HVra PT' QT' isrmwT' initT' ∧
∃ R,
Asim (sval (QT' v)) (Astar (sval (QT v)) (Astar (sval Q) R))).
{ clear H; exploit independent_heap_compat; eauto;
try solve [by intros ? ? X; eapply INCL' in X|
by intros ? ? X; eapply EV' in X].
intros [hhh L]; simpls; eexists; split; try edone.
rewrite !hsum_cons, MAPt, Ep, Ew in L; desc.
revert HT LP0 Gp L; clear; do 2 (rewrite hplus_unfold; desf).
specialize (h l); specialize (h0 l).
intros; desc; clarify; rewrite Gp, HT in *; simpls.
destruct (hw l); ins; desf; do 5 eexists; try edone;
ins; ∃ (sval (QQ' v)); Asim_simpl; desf; try solve [exfalso; eauto];
(eapply Asim_sym, Asim_trans, Asim_sym in ASIM; [|apply Asim_starC]);
(eapply Asim_trans; [|repeat first [exact ASIM|apply Asim_star|idtac]; try apply Asim_refl]); eauto using Asim.
by destruct (h0 v); ins; desc; rewrite H, ?H0; eauto using Asim.
by destruct (h v), (h0 v); ins; desc; rewrite H, H0, ?H1, ?H2; eauto using Asim.
}
clear hT HT MAPt; desc.
cut (∃ FRAME,
goal
(mk_assn_mod
(Astar (sval (QT' v)) (foldr Astar (List.map ssnd l') FRAME)))).
clear -H2 PRM; intro M; desc.
∃ (Astar R0 FRAME); erewrite AsimD; [eapply M|].
eapply Asim_trans.
by eapply (Asim_star (Asim_refl _)), (foldr_star_perm2 (Permutation_map _ PRM)).
eapply Asim_trans.
by simpl; eapply Asim_sym, Asim_starA.
eapply Asim_trans, Asim_star, Asim_refl; [|apply Asim_sym, H2].
apply (Asim_trans (Asim_starA _ _ _)).
eapply Asim_trans, Asim_sym, Asim_starA.
apply Asim_star; [apply Asim_refl|].
eapply Asim_trans, Asim_sym, Asim_starA.
apply Asim_star, Asim_foldr_pull; apply Asim_refl.
eapply H; eauto.
× by eapply (Permutation_NoDup (Permutation_map _ PRM)) in NDr; inv NDr.
× eby ins; eapply SR, Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].
× eby ins; eapply DEL, Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].
× ins; eauto using Permutation_in, Permutation_map.
destruct INt as [|[INt|INt]]; desc; subst; ins.
3: eby eapply NHB, Permutation_in, In_cons; [|eapply (Permutation_sym PRM)|].
split.
by intro; subst;
eapply (Permutation_NoDup (Permutation_map _ PRM)) in NDr;
inv NDr; destruct H5; rewrite In_map; vauto.
eby eapply NAFTER, Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].
split.
by intro; subst;
eapply (Permutation_NoDup (Permutation_map _ PRM)) in NDr;
inv NDr; destruct H5; rewrite In_map; vauto.
eby eapply NAFTER, Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].
}
pose proof (get_pres ACYCLIC HC _ NDt IN ST TT DEEP INDEP); desf.
simpls; desf.
assert (NHB': ∀ a,
In a
(map (hb_sb^~ (hb_fst edge)) pres_sb ++
map (hb_sw^~ (hb_fst edge)) pres_sw ++
filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T) →
∀ b Q,
In (b, Q) R →
hb_snd a ≠ b ∧ ¬ happens_before lab sb rf mo (hb_snd a) b).
{ clear - H0 NHB; intros.
rewrite !In_app, !In_map, In_filter in *; desf; ins; eauto;
split; intro; desf; destruct H0; eauto. }
specialize (H R (map (hb_sb^~ (hb_fst edge)) pres_sb ++
map (hb_sw^~ (hb_fst edge)) pres_sw ++
filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T)
(or_intror (conj eq_refl METR)) ND' INCL' EVS'
NDr SR _ _ DEL NHB' IND').
clear NHB'.
exploit independent_heap_compat; try apply IND'; eauto;
try solve [by intros ? ? X; eapply INCL' in X|by intros ? ? X; eapply EVS' in X].
intro M; desf; rewrite M in ×.
specialize (H _ eq_refl).
clear IND' EVS' INCL' METR ND'.
assert (J := helper_perm_filter_post (hb_fst edge) T); desf.
revert MAPt.
rewrite (hsum_perm (map_perm _ J)).
rewrite !map_app, !hsum_app in ×.
rewrite hplusC, hplusA; ins.
assert (ALLOC: ∀ hf loc,
hsum (map hmap (filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T)) = Hdef hf →
hf loc ≠ HVnone →
∃ c, lab c = Aalloc loc ∧ c ≠ hb_fst edge).
intros ? ? U NEQ; eapply hsum_alloc in U; eauto; desf.
rewrite In_map in *; desf.
rewrite In_filter in *; desf.
exploit heap_loc_allocated; eauto; try (by destruct x; ins; eauto).
destruct (eqP (hb_fst x) (hb_fst edge)); ins; desf; eexists; split; eauto; intro; desf.
by apply clos_refl_trans_hbE in x0; desf; try congruence; eapply DEEP; eauto with hb.
clear INDEP.
destruct (classic (lab (hb_fst edge) = Aalloc l)) as [EQ|NEQ].
{
clear H.
destruct posts_sw; ins.
2: by exploit TT;
[by eapply Permutation_in, In_appI2, In_appI2, In_eq;
apply Permutation_sym, J|];
simpl; unfold ann_sw; rewrite EQ; ins; desf.
generalize (VALID _ (ST _ IN)); unfold hmap_valid; rewrite EQ.
generalize IN as IN'.
intros; desc; eapply TT in IN'; destruct edge; simpls;
[by red in IN'; rewrite EQ in *; desf|].
eapply qU in IN'; subst.
assert (posts_sb = e' :: nil).
{ eapply (Permutation_in _ J) in IN.
rewrite !In_app, In_map, In_filter, eqxx in *; ins.
clear qEQ; desf.
eapply (Permutation_NoDup J), nodup_append_right, nodup_append_left in NDt.
destruct (In_implies_perm _ _ IN0) as [l' Pl'].
cut (l' = nil).
symmetry in Pl'; eapply In_split in IN0; desf.
eapply Permutation_cons_app_inv in Pl'.
intros; subst; eapply Permutation_nil in Pl'.
by destruct l1; ins; destruct l2; ins.
apply (Permutation_NoDup (Permutation_map _ Pl')) in NDt.
ins; inv NDt.
destruct l' as [|e'' ?]; ins.
clear H3.
assert (e' ≠ e'') by (intro; subst; eauto).
destruct H.
exploit TT.
eapply (Permutation_in _ (Permutation_sym J)), In_appI2, In_appI1, In_mapI.
eapply (Permutation_in _ (Permutation_sym Pl')), In_cons, In_eq.
eapply qU.
}
subst; ins; rewrite hsum_nil, hsum_one, hplus_emp_l in ×.
assert (R = nil).
{
specialize (NHB _ IN).
destruct R as [|[]]; ins; []; exfalso.
specialize (SR _ _ (In_eq _ _)).
specialize (DEL _ _ (In_eq _ _)); red in DEL; desc; clear DEL0.
specialize (NHB _ _ (In_eq _ _)); desc.
assert (∃ hf', hmap (hb_sb e e') = Hdef hf' ∧ hf' l ≠ HVnone).
by clear -qEQ; desf; repeat eexists; try edone; rewrite hupds.
desc; clear qEQ IN.
exploit (heap_loc_allocated ACYCLIC HC VALID (hb_sb a apost));
try eapply Lq; simpl; eauto.
instantiate (1:=l); congruence.
intro M'; desc.
assert (c = e) by (eapply CONS_A; rewrite ?EQ, ?M'; ins); subst.
eapply clos_refl_trans_hbE in M'0; desf; try congruence.
desf; eauto using t_step with hb; try congruence.
eapply (@hb_helper1 lab sb rf) with (a := a) in qU;
try edone; desf; eauto with hb.
by unfold synchronizes_with; rewrite M'; red; ins; desf.
}
subst; ins.
clear - PROVE CONS_A qU qEQ MAPt ALLOC EQ HT.
eapply hplus_def_inv in MAPt; desc; subst; rewrite MAPt in ×.
assert (N: hT l = hy l).
desf; rewrite PLUSv, hupds; simpls; desf;
exfalso; assert (XXX: hz l ≠ HVnone) by congruence;
destruct (ALLOC _ _ MAPt0 XXX) as (c & Ac & []);
by eapply CONS_A; rewrite ?EQ, ?Ac.
eapply PROVE; eauto using vshift_refl.
intros; assert (a = e) by (eapply CONS_A; rewrite ?EQ, ?A; done); subst.
eapply qU in SB; congruence.
by desf; rewrite hupds in *; desf; eauto.
}
exploit go_back_one_acq; try eapply NEQ; eauto.
intro K; desf.
exploit (NoDup_Permutation K NDb); [by intro; rewrite Pb|].
exploit (NoDup_Permutation K0 NDw); [by intro; rewrite Pw|].
clear Pb Pw; intros Pb Pw.
rewrite (hsum_perm (map_perm _ (map_perm _ Pb))) in K7.
rewrite (hsum_perm (map_perm _ (map_perm _ Pw))) in K7.
specialize (K7 _ M); desf.
destruct (@perm_from_subset _ posts_sb0 posts_sb) as [rb Psb].
by eapply (Permutation_NoDup J) in NDt; rewrite !nodup_app in NDt;
desf; eauto using NoDup_mapD.
by symmetry in J; intros; apply K5, (TT (hb_sb _ _)), (Permutation_in _ J),
In_appI2, In_appI1, In_mapI.
destruct (@perm_from_subset _ posts_sw0 posts_sw) as [rw Psw].
by eapply (Permutation_NoDup J) in NDt; rewrite !nodup_app in NDt;
desf; eauto using NoDup_mapD.
by symmetry in J; intros; apply K6, (TT (hb_sw _ _)), (Permutation_in _ J),
In_appI2, In_appI2, In_mapI.
rewrite (hsum_perm (map_perm _ (map_perm _ Psb))) in K7.
rewrite (hsum_perm (map_perm _ (map_perm _ Psw))) in K7.
rewrite !map_app, !hsum_app, !hplusA in K7.
rewrite !(hplusAC (hsum (map hmap (map (hb_sb _) rb)))) in K7.
rewrite !(hplusAC (hsum (map hmap (map (hb_sw _) rw)))) in K7.
unfold actid in *; rewrite MAPt, <- hplusA, hplusC in K7.
eapply hplus_def_inv in K7; desf.
eapply hvplus_ra2 in HT; eauto.
rewrite <- PLUSv in HT; red in HT; desf.
specialize (K8 _ _ _ _ eq_refl); red in K8; desf.
specialize (H _ _ _ _ eq_refl PROVE); desf.
specialize (HT v); desf.
specialize (K8 v); desf.
∃ (Astar (Astar QR QR0) FRAME).
clear -H HT K8; erewrite AsimD; [edone|].
eapply Asim_trans.
by apply Asim_star, Asim_foldr_pull; apply Asim_refl.
eapply Asim_trans, (Asim_star (Asim_sym K8)), Asim_refl.
eapply Asim_trans, (Asim_star (Asim_star (Asim_sym HT) (Asim_refl _))), Asim_refl.
eapply Asim_trans, Asim_sym, Asim_starA.
eapply Asim_trans, Asim_sym, Asim_starA.
apply Asim_star, Asim_starA; apply Asim_refl.
Qed.
Lemma wellformed :
∀ mt acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo 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
sww (swwOK: ∀ x, In x sww ↔ ann_sw lab rf x w) (swwND: NoDup sww)
(MAPw: hmap (hb_sb wpre w) +!+ hsum (map hmap (map (hb_sw^~ w) sww)) = Hdef hw)
PW QW isrmwW initW
(HW: hw l = HVra PW QW isrmwW initW)
(R: list (actid × assn_mod))
(NDr: NoDup (map (@fst _ _) R))
(SR: ∀ a Q (IN: In (a, Q) R), In a V)
(TR: ∀ a Q (IN: In (a, Q) R), ann_sw lab rf w a)
(DEL: ∀ a Q (IN: In (a, Q) R), read_loses_perm hmap lab sb rf a l v Q)
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 lab sb rf mo T)
(NHB: ∀ a (INt: In a T) b Q (INr: In (b,Q) R),
hb_snd a ≠ b ∧ ¬ happens_before lab sb rf mo (hb_snd a) b)
hT (MAPt: hsum (map hmap T) = Hdef hT)
PT QT isrmwT initT (HT: hT l = HVra PT QT isrmwT initT),
implies (proj1_sig (PW v))
(Astar (proj1_sig (QT v))
(foldr Astar (map ssnd R) Atrue)).
Proof.
intros.
assert (N: ∃ cpre c hf PP' QQ' isrmw' init',
sb cpre c ∧
lab cpre = Aalloc l ∧
hmap (hb_sb cpre c) = Hdef hf ∧
hf l = HVra PP' QQ' isrmw' init' ∧
happens_before lab sb rf mo cpre w ∧
(∀ h, assn_sem (sval (PW v)) h → assn_sem (sval (PP' v)) h)).
eapply hplus_eq_raD with (v:=v) in MAPw; eauto; desf.
exploit (heap_loc_rel_allocated v ACYCLIC CONS_A HC VALID
(hb_sb wpre w) SBw); ins; eauto with hb.
by desc; repeat (eexists; try edone); ins; desf; eauto with hb; apply x5, MAPw1.
eapply hsum_eq_raD with (v:=v) in MAPw; eauto; desc; clarify.
repeat (rewrite In_map in *; desc); clarify; rewrite swwOK in ×.
exploit (heap_loc_rel_allocated v ACYCLIC CONS_A HC VALID
(hb_sw _ w) MAPw5); ins; eauto with hb.
by desc; repeat (eexists; try edone); ins; desf; eauto with hb; apply x6, MAPw3, MAPw1.
desc; intros.
assert (In cpre V) by (eauto with hb).
clear SBw INw MAPw HW.
edestruct (wellformed_only_reads_helper (fun A ⇒ implies (sval (PW v)) (sval A)));
eauto.
intros; eapply vshift_hack in VS; desf; rewrite G in *; desf.
erewrite ALLOC in N2; eauto; []; desf.
∃ Aemp; red; ins.
eapply sim_assn_sem, N4; eauto; Asim_simpl; vauto.
simpls.
red; intros.
eapply sim_assn_sem; [apply Asim_star, Asim_foldr_simpl; apply Asim_refl|].
apply H0 in H1.
eapply sim_assn_sem in H1; [|apply Asim_assn_norm].
eapply sim_assn_sem in H1;
[|apply Asim_star, Asim_sym, Asim_foldr_simpl; apply Asim_refl].
clear -H1; simpls; desf; repeat eexists; try edone.
by intro; desf; destruct h0; ins.
Qed.
Lemma wellformed_one :
∀ mt acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo 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
sww (swwOK: ∀ x, In x sww ↔ ann_sw lab rf x w) (swwND: NoDup sww)
(MAPw: hmap (hb_sb wpre w) +!+ hsum (map hmap (map (hb_sw^~ w) sww)) = Hdef hw)
PW QW isrmwW initW
(HW: hw l = HVra PW QW isrmwW initW)
rpre r (ST: In rpre V) (TT: sb rpre r)
(NIN: ¬ In r V)
(R: list (actid × assn_mod))
(NDr: NoDup (map (@fst _ _) R))
(SR: ∀ a Q (IN: In (a, Q) R), In a V)
(TR: ∀ a Q (IN: In (a, Q) R), ann_sw lab rf w a)
(DEL: ∀ a Q (IN: In (a, Q) R), read_loses_perm hmap lab sb rf a l v Q)
hT (MAPt: hmap (hb_sb rpre r) = Hdef hT)
PT QT isrmwT initT (HT: hT l = HVra PT QT isrmwT initT),
implies (proj1_sig (PW v))
(Astar (proj1_sig (QT v))
(foldr Astar (map ssnd R) Atrue)).
Proof.
intros; eapply wellformed with (w := w) (T := hb_sb rpre r :: nil);
eauto; ins; desf.
× by red; ins; desf; ins; desf; eauto using t_step with hb.
× by split; intro; desf; eauto using hist_closedD.
× by rewrite hsum_one.
Qed.
Lemma wellformed_one_w :
∀ mt acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo 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 initW
(HW: hw l = HVra PW QW isrmwW initW)
rpre r (ST: In rpre V) (TT: sb rpre r)
(NIN: ¬ In r V)
(R: list (actid × assn_mod))
(NDr: NoDup (map (@fst _ _) R))
(SR: ∀ a Q (IN: In (a, Q) R), In a V)
(TR: ∀ a Q (IN: In (a, Q) R), ann_sw lab rf w a)
(DEL: ∀ a Q (IN: In (a, Q) R), read_loses_perm hmap lab sb rf a l v Q)
hT (MAPt: hmap (hb_sb rpre r) = Hdef hT)
PT QT isrmwT initT (HT: hT l = HVra PT QT isrmwT initT),
implies (proj1_sig (PW v))
(Astar (proj1_sig (QT v))
(foldr Astar (map ssnd R) Atrue)).
Proof.
intros; eapply wellformed_one with (w := w) (sww := nil); eauto;
instantiate; ins; unfold ann_sw; try rewrite LAB; ins; try split; ins; desf.
by rewrite hsum_nil, hplus_emp_r.
Qed.
Lemmas about initialization
Lemma helper_ra_init :
∀ lab sb rf hmap edge
(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
(LA : hf l = HVra PP QQ isrmw true)
(NW : ¬ is_writeL (lab (hb_fst edge)) l),
∃ edge' hf',
edge_valid lab sb rf edge' ∧
hb_snd edge' = hb_fst edge ∧
hmap edge' = Hdef hf' ∧
∃ PP' QQ' isrmw',
hf' l = HVra PP' QQ' isrmw' true.
Proof.
unfold hmap_valid, unique; ins; desf; desf.
Case Askip.
destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
eapply vshift_hack in qEQ.
symmetry in qEQ.
assert (X := hplus_def_inv _ _ qEQ); desf; rewrite X in ×.
eapply hsum_raD in X; eauto; desf.
2: by rewrite <- GET; eapply In_mapI, In_mapI, qOK.
rewrite X0 in *; clear X0; try done.
destruct isrmw'.
eapply hplus_ram_lD in qEQ; try edone; desc; clarify.
assert (init'0 = true) by desf; clear qEQ2; subst.
eapply hsum_eq_ra_initD in pEQ; eauto.
desf; repeat (rewrite In_map in *; desf).
by apply pOK in pEQ2; repeat (eexists; try edone); ins.
eapply hplus_ra_lD in qEQ; try edone; desc; clarify.
assert (init'0 = true) by desf; clear qEQ2; subst.
eapply hsum_eq_ra_initD in pEQ; eauto.
desf; repeat (rewrite In_map in *; desf).
by apply pOK in pEQ2; repeat (eexists; try edone); ins.
Case Aalloc.
destruct edge; ins; subst; 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 Aalloc.
destruct edge; ins; subst; 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; try (by red in EV; rewrite Heq in *; desf); [].
apply qU0 in EV; subst e'; rewrite GET in *; desf.
rewrite pEQ in *; desf.
by ∃ (hb_sb pre e); repeat (eexists; try edone).
Case Aload .
destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
apply qU0 in EV; subst e'; rewrite GET in *; desf.
symmetry in qEQ; eapply hplus_eq_ra_initD in qEQ; eauto.
desf.
unfold hupd in qEQ0; desf; desf.
apply hplus_def_inv in pEQ'; desf.
specialize (PLUSv l0); rewrite hupds in *; simpls.
by desf; ∃ (hb_sb pre e); repeat (eexists; try edone).
eapply hplus_eq_ra_initD in qEQ; eauto.
desf.
eapply hsum_eq_ra_initD in swsEQ; eauto; desf.
repeat (rewrite In_map in *; desf); rewrite swsOK in ×.
repeat (eexists; try edone); ins; eauto.
∃ (hb_sb pre e); destruct (hmap (hb_sb pre e)); try done.
eexists; repeat split; ins.
destruct isrmw'0.
eapply hplus_ram_rD in pEQ'; eauto; desc; clarify.
by desf; repeat eexists; try edone.
eapply hplus_ra_rD in pEQ'; eauto; desc; clarify.
by desf; repeat eexists; try edone.
Case Astore .
destruct edge; ins; subst; try (by rewrite wEQ in GET; try done; 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 .
∃ (hb_sb pre (hb_fst edge)); destruct (hmap (hb_sb pre (hb_fst edge))); try done.
eexists; repeat split; ins.
eapply vshift_hack in UPD.
destruct edge; ins.
rewrite !(hplusAC (hsum _)) in UPD.
symmetry in UPD; exploit hplus_def_inv_l; eauto.
intro Z; desf; exploit hsum_raD; eauto; [|intro W; desf].
by rewrite <- GET; eapply In_mapI, In_mapI, swsOK.
rewrite W0 in *; try done; clear init' W0.
rewrite Z in *; destruct isrmw'.
eapply hplus_ram_lD in UPD; eauto; desc; clarify.
revert UPD; unfold initialize, hupd; case eqP; intro; subst; try done.
by desf; eauto.
eapply hplus_ra_lD in UPD; eauto; desc; clarify.
revert UPD; unfold initialize, hupd; case eqP; intro; subst; try done.
by desf; eauto.
apply qU0 in EV; subst e'; rewrite GET in *; desf.
symmetry in UPD; rewrite hplusAC in UPD.
destruct isrmw.
eapply hplus_ram_lD in UPD; eauto; desc; clarify.
revert UPD; unfold initialize, hupd; case eqP; intro; subst; try done.
by desf; eauto.
eapply hplus_ra_lD in UPD; eauto; desc; clarify.
revert UPD; unfold initialize, hupd; case eqP; intro; subst; try done.
by desf; eauto.
Case Armw.
eapply vshift_hack in UPD.
assert (∃ PP' QQ' isrmw', hi l = HVra PP' QQ' isrmw' true).
{ destruct edge; ins.
rewrite !(hplusAC (hsum _)) in UPD.
symmetry in UPD; exploit hplus_def_inv_l; eauto.
intro Z; desf; exploit hsum_raD; eauto; [|intro W; desf].
by rewrite <- GET; eapply In_mapI, In_mapI, swsOutOK.
rewrite W0 in *; try done; clear init' W0.
rewrite Z in *; destruct isrmw'.
eapply hplus_ram_lD in UPD; eauto; desc; clarify.
by revert UPD; unfold initialize, hupd; desf; eauto.
eapply hplus_ra_lD in UPD; eauto; desc; clarify.
by revert UPD; unfold initialize, hupd; desf; eauto.
rewrite hplusAC in UPD.
apply qU0 in EV; subst e'; rewrite GET in *; desf.
destruct isrmw.
symmetry in UPD; eapply hplus_ram_lD in UPD; eauto; desc; clarify.
by revert UPD; unfold initialize, hupd; desf; eauto.
symmetry in UPD; eapply hplus_ra_lD in UPD; eauto; desc; clarify.
by revert UPD; unfold initialize, hupd; desf; eauto. }
desc.
eapply hplus_eq_ra_initD in iEQ; eauto; desf.
by eexists (hb_sb pre _); repeat (eexists; try edone).
eapply hsum_eq_ra_initD in iEQ; eauto; desf.
repeat (rewrite In_map in *; desf); rewrite swsInOK in ×.
by eexists (hb_sw _ _); ins; repeat (eexists; try edone); ins; eauto.
Qed.
Lemma heap_loc_ra_initialized :
∀ mt acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo 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
(LA: h l = HVra PP QQ isrmw true),
∃ cpre c,
sb cpre c ∧
is_writeL (lab c) l ∧
(c = hb_fst edge ∨ happens_before lab sb rf mo c (hb_fst edge)).
Proof.
intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
clear edge EV IN; intros.
generalize (VALID _ IN).
destruct (classic (is_writeL (lab (hb_fst edge)) l)) as [|NEQ]; eauto.
{
ins; red in H0; unfold unique in *; desf; ins; desf;
∃ pre; repeat eexists; eauto; instantiate;
by rewrite Heq.
}
exploit helper_ra_init; eauto; ins; desf.
assert (HB: happens_before lab sb rf mo (hb_fst edge') (hb_fst edge)).
by destruct edge'; ins; subst; eauto with hb.
exploit (IH edge'); eauto.
intro; desf; repeat eexists; eauto with hb; ins; desf; eauto.
Qed.
Construction of the read_loses_perm list
Fixpoint map_pairo A B (f: A → option B) l :=
match l with
| nil ⇒ nil
| x :: l' ⇒
match f x with
| Some y ⇒ (x, y) :: map_pairo f l'
| None ⇒ map_pairo f l'
end
end.
Lemma In_map_pairo A B (f : A → option B) l x :
In x (map_pairo f l) ↔ In (fst x) l ∧ f (fst x) = Some (snd x).
Proof.
induction l; ins; try tauto.
case_eq (f a); ins; rewrite IHl; clear IHl;
ins; intuition; desf; ins; eauto.
Qed.
Lemma NoDup_map_fst_map_pairo A B (f : A → option B) l :
NoDup l → NoDup (map (@fst _ _) (map_pairo f l)).
Proof.
induction l; inversion 1; ins; desf; ins; eauto.
inv H; constructor; eauto.
rewrite In_map; intro; desf.
rewrite In_map_pairo in *; desf.
Qed.
Lemma read_loses_perm_uniq :
∀ hmap lab sb rf r E v P
(H: read_loses_perm hmap lab sb rf r E v P) P'
(H': read_loses_perm hmap lab sb rf r E v P'),
P = P'.
Proof.
unfold read_loses_perm, unique in *; ins; desc.
apply Lp2 in Lp; apply Lq2 in Lq; subst.
rewrite Ep0, Eq0 in *; clarify.
rewrite Gp0, Gq0 in *; clarify.
assert (w0 = w) by (unfold ann_sw in *; des; congruence); subst.
rewrite Ew0 in Ew; clarify.
assert (SIM: Asim (Astar (sval (QQ' v)) (sval P)) (Astar (sval (QQ' v)) (sval P'))).
by desf; rewrite Gw0 in *; clarify; eauto using Asim.
clear H0 H'0.
eapply assn_mod_eqI; eapply Asim_star_cancel in SIM.
desf;
try eapply (sim_assn_sem SIM) in LSEM;
try eapply (sim_assn_sem SIM) in LSEM0; ins; desf.
Qed.
Lemma read_loses_perm1 hmap lab sb rf E res sws V :
NoDup sws →
∃ l,
<< NDl: NoDup (map (@fst _ _) l) >> ∧
<< EQl: ∀ r P, In (r,P) l →
In r sws ∧ In r V ∧
read_loses_perm hmap lab sb rf r E res P >> ∧
<< EQl': ∀ r P,
In r sws → In r V →
read_loses_perm hmap lab sb rf r E res P →
In (r,P) l >>.
Proof.
eexists (map_pairo
(fun r ⇒
match (excluded_middle_informative
(∃! P, In r V ∧ read_loses_perm hmap lab sb rf r E res P)) with
| left pf ⇒
Some (sval (constructive_definite_description _ pf))
| _ ⇒ None
end) sws).
split; unfold NW.
by apply NoDup_map_fst_map_pairo.
split; intros.
rewrite In_map_pairo in *; simpls; desc.
split; try done; desf; desf; destruct e as (? & ? & ?); desc; ins.
split; try done.
by destruct (constructive_definite_description); ins; desf.
rewrite In_map_pairo; ins; split; try done; desf.
destruct e as (? & ? & M); desc; ins.
f_equal; destruct (constructive_definite_description); ins; desf.
by rewrite <- (M P), <- (M x0).
eby destruct n; ∃ P; split; ins; desf; eapply read_loses_perm_uniq.
Qed.
This page has been generated by coqdoc Imprint | Data protection