Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps fslassn fslassnsem fslassnlemmas fslmodel.
Require Import fslhmap fslhmapna fslhmapa fsltriple fsltriple2.
Require Import ihc initread.
Require Import GpsSepAlg.
Set Implicit Arguments.
A helper lemma for establishing the soundness of the atomic load rules.
Definition preciseish PS PSg P :=
∀ hP (SEM: assn_sem P hP) hP' (SEM': assn_sem P hP')
hF (DEF: hplus hP hF ≠ @Hundef PS PSg) hF' (EQ: hplus hP hF = hplus hP' hF'),
hP = hP' ∧ Hsim hF hF'.
Lemma precise_nabla PS PSg (P: assn PS PSg): precise P → preciseish (Anabla P).
Proof.
red; ins; desf.
assert (EQ': h'0 = lupd hP HLnormal) by (by apply lupd_eq; [apply Hsim_sym | ]).
assert (EQ'': h' = lupd hP' HLnormal) by (by apply lupd_eq; [apply Hsim_sym | ]).
subst.
exploit (H _ SEM0 _ SEM'0 (lupd hF HLnormal)).
by rewrite <- lupd_hplus_dist; unfold lupd; desf.
by instantiate (1 := lupd hF' HLnormal); rewrite <- !lupd_hplus_dist, EQ.
intro LUPD; desf.
split.
× apply lupd_eq_lupd in LUPD.
eby eapply exact_label_sim.
eby eapply hplus_not_undef_l.
× eapply lupd_eq_lupd; try edone.
eby eapply hplus_not_undef_r.
Qed.
Theorem rule_load_acq PS PSg typ E QQ
(PREC: ∀ v, @precise PS PSg (QQ v))
(NORM: ∀ v, normalizable (QQ v))
(TYP : acquire_typ typ) :
triple (Astar (Aacq E QQ) (Arainit E))
(Eload typ E)
(fun v ⇒ Astar (Aacq E (hupd QQ v Aemp)) (Astar (Arainit E) (QQ v))).
Proof.
eapply triple_helper_start; ins; desc; clarify; ins.
rewrite hplus_init1 in *; ins.
assert (VALID' := VALID); red in VALID'; desc; red in VALIDS; desc.
assert (Z : ∃ hoo goo PP QQ0 isrmw labW labR, hmap (hb_sb prev fst) = Hdef hoo goo
∧ hoo E = HVra PP (fun x ⇒ mk_assn_mod (Astar (QQ x) (QQ0 x))) isrmw labW (ohlplus HLnormal labR)
∧ (isrmw → ∀ x, assn_norm (QQ x) = Aemp ∨ assn_norm (QQ x) = Afalse)).
{
rewrite pEQ in *; clear -pDEF.
destruct hFR; ins; rewrite hplus_unfold in *; desf; desf.
specialize (HEAPcompat E); rewrite hupds in *; ins; desf.
{
eexists _, _, Wemp, (fun _ ⇒ Aemp), false, None, None; split; [done | ].
ins; rewrite Heq, hupds, hvplusC; ins; split; ins.
f_equal; extensionality v; apply AsimD, Asim_sym, Asim_star_emp.
}
{ eexists _, _, RR, (fun v ⇒ sval (QQ0 v)), isrmwflag, permlbl, init; split; [done | ].
ins; rewrite Heq, hupds in *; ins; split.
× f_equal; [extensionality v | ]; desf.
+ extensionality v; generalize (HEAPcompat v); clear; ins.
unfold hv_acq_def, hv_rval in H; desf.
- apply assn_mod_eqI; Asim_simpl.
eapply Asim_trans.
by apply Asim_star_emp_l.
apply Asim_star; [ | by apply Asim_refl].
by rewrite <- H; apply Asim_sym, Asim_assn_norm.
- apply assn_mod_eqI; Asim_simpl.
rewrite H0; eapply Asim_trans.
by apply Asim_sym, Asim_star_false.
apply Asim_star; [ | by apply Asim_refl].
by rewrite <- H; apply Asim_sym, Asim_assn_norm.
+ by extensionality v; apply AsimD, Asim_star; [apply Asim_sym, Asim_assn_norm | apply Asim_refl].
× ins; desf; specialize (HEAPcompat x); unfold hv_acq_def, hv_rval in HEAPcompat; desf; eauto.
}
}
desc.
assert (∃ wri, << RF : rf fst = Some wri >> ∧ << WRI: is_writeLV (lab wri) E v >>).
{
red in CONS; desc; generalize (Crf fst); intro CrfFST; desf.
repeat eexists; desf; simpls.
by rewrite SEM1 in *; ins; desf.
exfalso.
exploit (initialization_always_before (AcyclicStrong_implies_IrreflexiveHBuRF ACYC)
Crf HC (proj1 VALID)); eauto.
by simpl; apply FST.
by simpl; exploit (HC0 fst); vauto; apply hc_edge_sb, FST.
by instantiate (2 := E); instantiate (1 := HLnormal);
rewrite Z0; clear; simpl; desf; red; eauto; inv Heq; eauto.
intro; desf.
eapply (CrfFST a); eauto.
2: eby rewrite SEM1.
red in FST; desc;clear - FST HB.
apply clos_refl_trans_hbE in HB; desf; eauto with hb.
}
desf.
assert (INwri: In wri V).
{
exploit (HC0 fst); vauto.
simpl; intro; desf.
exfalso; red in CONS; desc; eapply (AcyclicStrong_implies_IrreflexiveHBuRF ACYC); vauto.
}
destruct (eqP (assn_norm (QQ v)) Aemp) as [EMP|NEMP].
{
assert (T: (fun x : val ⇒ mk_assn_mod (hupd QQ v Aemp x)) =
(fun x : val ⇒ mk_assn_mod (QQ x))).
{
clear - EMP; exten; intro y; unfold hupd; desf; desf.
by apply assn_mod_eqI1; ins.
}
eapply safe_final3s with
(h := hsingl _ _ E (HVra Wemp (fun x ⇒ mk_assn_mod (hupd QQ v Aemp x)) false None HLnormal) +!+ hFR)
(hs := hsingl _ _ E (HVra Wemp Remp false None None))
(ga' := ga_clear ga fst); eauto.
by ins; apply ga_clear_agrees; congruence.
by eauto using ga_clear_fin.
× ∃ hemp; rewrite hplus_emp_r.
repeat eexists; repeat split; eauto; try done.
+ rewrite pEQ in pDEF; clear - pDEF EMP.
rewrite hdef_alt in pDEF; desf.
apply hplus_def_inv in pDEF; desf.
intro U; rewrite hplus_unfold in U; desf.
destruct n; unnw; rewrite gres_plusC, gres_plus_emp_r; split; ins.
specialize (DEFv v0).
unfold hupd; desf; ins; desf; rewrite ?hupds in DEFv; ins; desf.
split; ins; desf; desf.
rewrite assn_norm_emp.
by specialize (DEFv v); rewrite EMP in DEFv.
+ by instantiate (1 := hemp); rewrite hplus_emp_r, hplus_init1.
+ by rewrite hplus_emp_r.
+ by apply assn_sem_assn_norm; rewrite EMP.
× red; desf.
∃ gres_emp; split.
by unfold ga_clear; split; ins; desf.
eexists _ , _ , hoo, goo; repeat split; try (by apply FST); try by (apply LST).
by unfold mupd; desf; desf; rewrite pEQ, T in ×.
by unfold mupd; desf; desf.
right; split; [by destruct TYP; desf | ].
destruct hFR as [|hFR gFR]; try done.
eexists (wri :: nil), hemp,
(hsingl _ _ E (HVra Wemp (fun x : val ⇒ mk_assn_mod (QQ x)) false None HLnormal) +!+ Hdef hFR gFR),
(mk_assn_mod Aemp).
assert (RFemp: hmap (hb_rf wri fst) = hemp).
{
eapply RESTR; eauto.
right; split; ins.
clear; intro SB; red in SB; desf.
}
unnw; repeat (split; try by (clear Z0; ins; desf; vauto)); intros;
(try by ins; rewrite ?assn_norm_emp in *; ins; subst; rewrite ?hplus_emp_l in *).
+ clear Z0; ins; rewrite hsum_one; unfold mupd; desf; desf.
rewrite RFemp; vauto.
+ ∃ hemp; repeat split; try by vauto.
clear Z0; ins; rewrite hsum_one; unfold mupd; desf; desf.
by rewrite RFemp; apply Hsim_refl.
+ clear Z0; ins; rewrite hsum_one; unfold mupd; desf; desf.
by rewrite RFemp; apply Hsim_refl.
+ unfold mupd; desf; desf.
unnw; repeat f_equal.
clear - EMP; extensionality x.
unfold hupd; desf; desf.
+ rewrite Z in pEQ; clear - pEQ Z0.
assert (empEQ: hupd Remp v (mk_assn_mod Aemp) = @Remp PS PSg).
by extensionality x; unfold hupd; desf; desf.
rewrite empEQ, hplusAC, <- hplusA, hplus_init1, hplus_unfold; desf.
+ unfold mupd; desf; desf.
rewrite Z in pEQ; clear - T pEQ EMP.
by rewrite hplus_emp_r, hplus_emp_l, hplusAC, <- hplusA, hplus_init1; ins; repeat f_equal.
+ clear; left; repeat eexists.
}
generalize (VLD _ INwri); intro M.
red in M; desc; destruct (lab wri) eqn: EQ; ins; desc; subst l v.
assert (WRI: is_writeLV (lab wri) E v0) by (rewrite EQ; done).
desc; destruct DISJ; desc; subst; try done.
{
red in CONS; desc; ins.
edestruct (no_atomic_reads_from_na_one FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC)
Ca Crf HC (proj1 VALID) pre _ INwri _ _
WRI (proj1 pU) pEQ0 IV prev fst V_PREV (proj1 FST) NIN);
eauto using hupds.
}
assert (XXX: ∃ PW QW isrmwW permW initW, hf E = HVra PW QW isrmwW permW initW ∧ PW v0 = P).
{
symmetry in UPD; apply hplus_def_inv in UPD; desc.
inv UPD.
generalize (PLUSv E), (DEFv E); unfold initialize; rewrite !hupds.
clear - TRAN0.
ins; desf; repeat eexists; instantiate; ins; rewrite ?hupds; desf;
by rewrite e in TRAN0; ins.
}
{
assert (Y: ∃ h1 hsink, hmap (hb_sink wri) = h1 +!+ hsink ∧ assn_sem (Anabla (QQ v0)) h1).
{
destruct isrmw.
× exfalso. destruct (Z1 eq_refl v0) as [MM|MM]; try done.
desc; subst; red in CONS; desc.
assert (WWW := wellformed_one_w); red in WWW.
destruct FST, pU, qU; eapply WWW in TRAN0; clear WWW;
try exact HC; try exact Z0; try exact XXX; try exact Z; try exact (proj1 VALID); try eassumption; eauto; [].
ins; desc.
apply (sim_assn_sem (Asim_assn_norm _)) in TRAN4; ins; desc.
by apply (sim_assn_sem (Asim_assn_norm _)) in TRAN8; rewrite MM in ×.
× red in CONS; desc; ins.
exploit annotated_rfs_and_sinks; try exact HC; try eassumption; eauto.
by apply pU.
by rewrite XXX.
{
ins.
destruct (classic (In x V)) as [INx | NINx].
× exfalso.
assert (NEMP': assn_norm (Astar (QQ v0) (QQ0 v0)) ≠ Aemp).
by intro EMP; apply assn_norm_star_eq_emp in EMP; desc.
assert (NFALSE': assn_norm (Astar (QQ v0) (QQ0 v0)) ≠ Afalse).
{
revert Z0; clear TYP0.
red in WRI; desfh; desfh.
ins.
exploit wellformed_one_w; try exact HC; try exact Heq; try exact XXX; try exact V_PREV;
try eassumption; try (by unfold unique in *; desc; eauto with hb).
eby exact (proj1 VALID).
intro IMP; exploit (IMP V_PREV (proj1 FST)); try eassumption.
clear; intros NF F; ins; rewrite F in NF; desf.
}
assert (VALIDx := VLD _ INx).
revert Z0; clear TYP0; red in VALIDx; desfh; desfh.
RMWin_def.
assert (l = E).
{
rewrite rfsOK in IN.
clear - Crf IN EQ Heq.
specialize (Crf x); rewrite IN, EQ, Heq in Crf; ins; desf.
}
subst l.
apply hplus_not_undef_l, hdef_alt in DEFin; desc; rewrite DEFin in ×.
symmetry in pEQ1; eapply hplus_ram_lD in pEQ1; desc.
2: by rewrite hupds.
clear pEQ4; ins.
exploit heap_loc_ra_no_own; try exact pEQ1; try (intro X; specialize (X _ _ Z0));
try exact HC; try eassumption; ins; try (by unfold unique in *; desc; eauto with hb).
eby exact (proj1 VALID).
instantiate (1 := v0) in X; clear Z0; desf.
× eapply (proj2 VALID); try by exact NINx.
right; split; unfold is_sb_out; ins.
by intro; desc.
}
ins; desc.
destruct x0; desc.
{
unnw; subst ann_rfs; ins.
rewrite rfEQ, hsum_nil, hplus_emp_l in ×.
subst P.
exploit (wellformed_one_w FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC) Ca Crf HC (proj1 VALID)
pre wri INwri EQ (proj1 pU) pEQ0 XXX prev fst V_PREV (proj1 FST) NIN); eauto.
intro WF; ins; desc.
rewrite assn_sem_assn_norm in *; ins; desc.
subst h1; subst h'.
∃ (lupd h0 HLnabla), (lupd (h3 +!+ h2) HLnabla).
repeat (apply conj).
by rewrite <- lupd_hplus_dist, <- hplusA; apply lupd_eq.
by apply lupd_label; intro U; rewrite U, !hplus_undef_l in ×.
eexists; repeat (apply conj); try edone.
by apply Hsim_sym, lupd_sim; intro U; rewrite U, !hplus_undef_l in ×.
by repeat (apply exact_label_hplus_dist in TRAN2; desc).
}
{
remember (hb_sb prev fst :: map hb_sink ann_rfs) as T.
assert (NDt : NoDup T).
{
subst T; apply nodup_cons.
split.
by rewrite In_map; intro; desc.
apply nodup_map; ins.
clear Z0 TYP0; intro; desf.
}
assert (INt: ∀ edge : hbcase, In edge T → In (hb_fst edge) V).
{
clear TYP0 Z0; subst T; ins; desf.
rewrite In_map in *; desf; ins; intuition.
}
assert (VALIDt: ∀ edge : hbcase, In edge T → edge_valid lab sb rf edge).
{
clear TYP0 Z0; subst T; ins; desf.
by ins; apply FST.
rewrite In_map in *; desf; ins.
apply SUBSET, rfsOK in H0.
red; desf; specialize (Crf x); rewrite H0, Heq in Crf; ins; desf.
}
assert (INDEP: independent sb rf T).
{
clear Z0 TYP0; subst T; red; ins; desf; ins; rewrite ?In_map in *; desf; ins.
by destruct NIN; apply INann_rfs.
eby destruct NIN; eapply hist_closedD.
by destruct NIN; eapply hist_closedD; try edone; apply INann_rfs.
}
assert (HT: ∃ hT gT, hsum (map hmap T) = Hdef hT gT ∧
∃ PT QT isrmwT permT initT, hT E = HVra PT QT isrmwT permT initT ∧
QT v0 = mk_assn_mod (Astar (Astar (QQ v0) (QQ0 v0)) (sval QQread))).
{
clear TYP0; revert Z0; subst T.
exploit independent_heap_compat; try exact HC; try eassumption; eauto.
by exact (proj1 VALID).
by ins; desf; rewrite In_map in *; desf.
by ins; desf; rewrite In_map in *; desf.
by ins; desf; rewrite In_map in *; desf; intuition.
by ins; desf; [apply FST | rewrite In_map in *; desf].
by ins; desf; rewrite In_map in *; desf.
by ins; desf; exploit (VALIDt (hb_sink a)); ins; eauto.
intros SUM ?; desc.
eexists _, _; split; try edone.
ins; rewrite hsum_cons, Z, SINKS in SUM.
clear - SUM Z0.
apply hplus_def_inv in SUM; desc.
inv SUM.
generalize (PLUSv E); rewrite Z0, hupds; clear; ins.
repeat eexists; eauto.
clear; ins; apply AsimD.
apply Asim_star.
by apply Asim_sym, Asim_assn_norm.
by rewrite hupds; apply Asim_refl.
}
subst P; desc.
exploit (wellformed_w FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC) Ca Crf HC (proj1 VALID)
pre wri INwri EQ (proj1 pU) pEQ0 XXX NDt INt VALIDt INDEP HT HT0); try exact TRAN0.
rewrite HT1; intro WF; simpls; desc.
rewrite assn_sem_assn_norm in ×.
subst h'.
rewrite rfEQ in ×.
clear - PREC NORM PRECISE NORMALIZABLE rfsSIM TRAN TRAN0 TRAN1 TRAN2 TRAN READS READS0 READS1 READS2
WF WF1 WF2.
ins; desf.
assert (EQ: hsum (map hmap (map (hb_rf wri) ann_rfs)) +!+ hmap (hb_sink wri)
= lupd (h4 +!+ h5 +!+ h3 +!+ h2) HLnabla) by (by rewrite !hplusA in TRAN1; apply lupd_eq).
assert (EQ': hsum (map hmap (map (hb_rf wri) ann_rfs)) = lupd h'0 HLnabla) by (by apply lupd_eq).
rewrite EQ', !(hplusAC h3), !lupd_hplus_dist in EQ.
specialize (NORMALIZABLE _ WF4); desc.
subst h3.
rewrite lupd_hplus_dist, hplusA in EQ.
apply precise_nabla in PRECISE.
assert (SAT0: assn_sem (Anabla (sval QQread)) (lupd h'0 HLnabla)).
{
split.
eby eapply lupd_label, assn_sem_def.
∃ h'0; repeat (apply conj); try done.
eby eapply Hsim_sym, lupd_sim, assn_sem_def.
}
assert (SATn: assn_sem (Anabla (sval QQread)) (lupd hN HLnabla)).
{
split.
eby eapply lupd_label, assn_sem_def.
∃ hN; repeat (apply conj); try done.
eby eapply Hsim_sym, lupd_sim, assn_sem_def.
}
assert (DEF: lupd h'0 HLnabla +!+ hmap (hb_sink wri) ≠ Hundef).
{
rewrite EQ' in rfsSIM.
red in rfsSIM; desc; congruence.
}
exploit (PRECISE _ SAT0 _ SATn _ DEF).
by exact EQ.
intro DECOMP; desc.
apply exact_label_sim with (lbl := HLnabla) in DECOMP0.
2: by apply exact_label_hplus_dist in TRAN; desc.
2: by rewrite <- !lupd_hplus_dist in *; apply lupd_label;
red in DECOMP0; desc; intro U; rewrite U in ×.
specialize (NORM _ _ WF6); desc.
subst h4.
rewrite lupd_hplus_dist, hplusA, hplusAC in DECOMP0.
eexists _, _; split; [by exact DECOMP0 | ].
split; [by apply lupd_label; intro U; rewrite U, !hplus_undef_r in × | ].
eexists; repeat apply conj; try exact NORM; try edone.
eby eapply Hsim_sym, lupd_sim, assn_sem_def.
}
}
clear Z Z0 Z1; desc.
assert (WOK: hmap_valid lab sb rf (mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink)
(ga_clear ga fst) wri).
{
red; rewrite EQ.
∃ gnew; split.
{ red; ins; split.
by intro X; apply NG in X; unfold ga_clear; desf.
by ins; apply NG; unfold ga_clear in *; desf.
}
eexists _, _, _, _; repeat (split; try edone); right; split; try done.
∃ rfs, hr, hF, P, sbg, rfg.
assert(SAME: hsum (map (mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink) (map (hb_rf wri) rfs))
+!+ mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink (hb_sink wri)
= hsum (map hmap (map (hb_rf wri) rfs)) +!+ hmap (hb_sink wri)).
{
clear TYP0.
rewrite <- rfsOK in RF.
apply In_implies_perm in RF as [rfs' PERM].
rewrite !(hsum_perm (map_perm _ (map_perm _ PERM))); ins.
rewrite !hsum_cons.
rewrite !map_upd_irr; ins.
2: by intro; desf; apply Permutation_NoDup, nodup_cons in PERM; ins; desf.
unfold mupd; desf; desf.
desf.
symmetry; rewrite (hplusC h1), Y, !hplusA, <- hplus_emp_l.
f_equal.
eapply (proj2 VALID); eauto.
right; split; ins.
unfold is_sb_out; intro; desf.
}
rewrite <- SAME in *; unnw; repeat (split; try done).
eby eexists; split.
}
clear TYP0.
assert (FOO': ∀ e, In e V →
hmap_valid lab sb rf (mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink)
(ga_clear ga fst) e).
{
ins; destruct (eqP e wri); desf.
eapply hmap_irr_change_valid.
by apply VLD.
by apply ga_clear_agrees; congruence.
ins; unfold mupd; desf; desf; ins; desf.
}
assert (FOO: hmap_valids lab sb rf (mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink) V).
by eexists; split; try exact FOO'; eauto using ga_clear_fin.
ins; desc.
assert (DEF': hsingl _ _ E
(HVra Wemp (fun x : val ⇒ mk_assn_mod (hupd QQ v0 Aemp x)) false None (Some HLCnormal))
+!+ h'0 +!+ hFR ≠ Hundef).
{
red in CONS; desc; ins.
exploit (independent_heap_compat FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC) Crf Ca HC FOO
(T := hb_rf wri fst :: hb_sb prev fst :: nil));
try solve [ by rewrite NoDup_two | ins; desf; apply FST].
by eapply independent_two; ins; eauto; try (by apply FST); intro; desf; eauto with hb.
intro DEF'; desc.
ins; rewrite hsum_two in DEF'.
unfold mupd in DEF'; desf; desf.
pattern g0 in DEF'; eapply ex_intro in DEF';
pattern h in DEF'; eapply ex_intro in DEF'; rewrite <- hdef_alt, pEQ in DEF'.
apply (hplus_sim_def _ Y2) in DEF'.
assert (D: hsingl _ _ E (HVra Wemp (fun x : val ⇒ mk_assn_mod (QQ x)) false None (Some HLCnormal))
=
hsingl _ _ E (HVra Wemp (hupd Remp v0 (mk_assn_mod (QQ v0))) false None None)
+!+
hsingl _ _ E
(HVra Wemp (fun x : val ⇒ mk_assn_mod (hupd QQ v0 Aemp x)) false None (Some HLCnormal))).
{
clear; rewrite hplus_hsingl; simpl; vauto.
repeat f_equal; desf.
extensionality v.
apply AsimD.
unfold hupd; desf; desf; ins.
by rewrite assn_norm_emp; eapply Asim_trans; [apply Asim_assn_norm | apply Asim_star_emp_r].
by rewrite assn_norm_emp; eapply Asim_trans; [apply Asim_assn_norm | apply Asim_star_emp_l].
}
rewrite hplusAC, D, hplusA in DEF'.
by intro U; rewrite U, hplus_undef_r in DEF'.
}
eapply safe_final4a with
(h := hsingl _ _ E
(HVra Wemp (fun x : val ⇒ mk_assn_mod ((hupd QQ v0 Aemp) x)) false None (Some HLCnormal))
+!+ h'0 +!+ hFR)
(hs := hsingl _ _ E (HVra Wemp (hupd Remp v0 (mk_assn_mod (QQ v0))) false None None))
(ga' := ga_clear ga fst);
eauto.
by ins; apply ga_clear_agrees; congruence.
by eauto using ga_clear_fin.
{ ∃ hemp; rewrite hplus_emp_r.
eexists; repeat split; try done.
eby rewrite <- hplusA.
eexists _, (hsingl _ _ E (HVra Wemp Remp false None (Some HLCnormal)) +!+ h'0); repeat (split; try edone).
by intro U; rewrite <- hplusA, U, hplus_undef_l in DEF'.
by rewrite <- hplusA, hplus_init1.
eexists _, h'0; repeat (split; try edone).
rewrite <- ohlplus_none_l in DEF' at 1.
rewrite <- (ohlplus_none_l (Some HLCnormal)) in DEF'.
by intro U; rewrite <- hplus_init1, hplusA, <- (hplusA _ h'0), U, hplus_undef_l, hplus_undef_r in DEF'.
}
{ red; rewrite SEM1.
∃ gres_emp; split.
by unfold ga_clear; split; ins; desf.
rewrite hdef_alt in pDEF; desc.
eexists _, _, hf0, g0; repeat (split; try edone).
by unfold NW, mupd; desf; desf.
by unfold NW, mupd; desf; desf.
right.
split; [by red in TYP; desf | ].
eexists (wri :: nil), (lupd h1 HLnormal), _, (mk_assn_mod (QQ v0)).
repeat (apply conj; try edone); ins; rewrite ?hsum_one; unfold mupd; desf; desf.
× split; ins; desf; eauto.
× ∃ h'0; repeat split; try done.
by simpl; rewrite assn_sem_assn_norm.
× apply lupd_sim.
red in Y2; desf.
× instantiate (1 :=
hsingl _ _ E (HVra Wemp (fun x : val ⇒ mk_assn_mod (hupd QQ v0 Aemp x)) false None None) +!+ hFR).
rewrite <- hplusA, hplus_hsingl, <- pDEF, pEQ; vauto.
ins; unnw; repeat f_equal; extensionality v; desf.
clear; apply AsimD.
unfold hupd; desf; desf; ins.
by rewrite assn_norm_emp; eapply Asim_trans; apply Asim_sym;
[apply Asim_star_emp_r | apply Asim_assn_norm].
by rewrite assn_norm_emp; eapply Asim_trans; apply Asim_sym;
[apply Asim_star_emp_l | apply Asim_assn_norm].
× rewrite hplus_emp_r, (hplusAC h'0), (hplusAC (lupd _ _)).
rewrite <- (hplusA (hsingl _ _ _ _) (hsingl _ _ _ _)), (hplusC (hsingl _ _ _ _) (hsingl _ _ _ _)),
hplus_init1; simpl.
unnw; f_equal.
apply lupd_eq; try done.
by apply Hsim_sym.
× right; repeat split; try (by red in TYP; desf).
apply lupd_label.
red in Y2; desf.
× by unnw; rewrite <- precise_assn_norm.
× by unnw; rewrite <- normalizable_assn_norm.
}
}
{
exfalso. RMWin_def.
red in CONS; desc; ins.
assert (NEMP': assn_norm (Astar (QQ v') (QQ0 v')) ≠ Aemp).
by intro EMP; apply assn_norm_star_eq_emp in EMP; desc.
assert (SEM': ∃ h, assn_sem (assn_norm (Astar (QQ v') (QQ0 v'))) h).
{
rewrite hdef_alt in DEFin; desc.
assert (RMW := DEFin); rewrite pEQ0, !hplusA in RMW.
eapply hplus_ram_lD in RMW; desc.
2: by rewrite hupds.
clear RMW2.
destruct (classic (v0 = v')) as [ | VAL]; [subst v0 | ].
× exploit wellformed_one; try exact HC; try exact DEFin; try exact V_PREV; try eassumption;
try (by unfold unique in *; desc; eauto with hb).
eby exact (proj1 VALID).
eby rewrite EQ.
intro IMP; exploit IMP; try exact NIN; try exact (proj1 FST); rewrite ?addn0; eauto.
eby apply RMW0; rewrite hupds.
eby clear; ins; desf; eexists.
× exploit wellformed_one; try exact HC; try exact DEFin; try exact V_PREV; try eassumption;
try (by unfold unique in *; desc; eauto with hb).
eby exact (proj1 VALID).
eby rewrite EQ.
intro IMP; exploit IMP; try exact NIN; try exact (proj1 FST); rewrite ?addn0; eauto.
eby apply RMW0; unfold hupd; rewrite eqxx.
eby clear; ins; desf; eexists.
}
destruct isrmw.
×
exploit Z1; try done.
instantiate (1 := v'); clear - NEMP SEM'.
intro CONTRA; desf.
rewrite assn_norm_star_intro, assn_sem_assn_norm, CONTRA in SEM'.
ins; desf.
×
apply hplus_not_undef_l, hdef_alt in DEFin; desc; rewrite DEFin in ×.
symmetry in pEQ0; eapply hplus_ram_lD in pEQ0; desc.
2: by rewrite hupds.
clear pEQ3; ins.
exploit heap_loc_ra_no_own; try exact Z0; try exact pEQ0; try exact HC;
(try (intro X; specialize (X _ _ Z0))); try eassumption; ins;
try (by unfold unique in *; desc; eauto with hb).
eby exact (proj1 VALID).
instantiate (1 := v') in X; clear Z0; desf.
by rewrite X in SEM'.
}
Grab Existential Variables. done.
Qed.
Theorem rule_load_rlx PS PSg typ E QQ
(PREC: ∀ v, @precise PS PSg (QQ v))
(NORM: ∀ v, normalizable (QQ v))
(AT: typ ≠ ATna):
triple (Astar (Aacq E QQ) (Arainit E))
(Eload typ E)
(fun v ⇒ Astar (Aacq E (hupd QQ v Aemp)) (Astar (Arainit E) (Anabla (QQ v)))).
Proof.
eapply triple_helper_start; ins; desc; clarify; ins.
rewrite hplus_init1 in *; ins.
assert (VALID' := VALID); red in VALID'; desc; red in VALIDS; desc.
assert (Z : ∃ hoo goo PP QQ0 isrmw labW labR, hmap (hb_sb prev fst) = Hdef hoo goo
∧ hoo E = HVra PP (fun x ⇒ mk_assn_mod (Astar (QQ x) (QQ0 x))) isrmw labW (ohlplus HLnormal labR)
∧ (isrmw → ∀ x, assn_norm (QQ x) = Aemp ∨ assn_norm (QQ x) = Afalse)).
{
rewrite pEQ in *; clear -pDEF.
destruct hFR; ins; rewrite hplus_unfold in *; desf; desf.
specialize (HEAPcompat E); rewrite hupds in *; ins; desf.
{
eexists _, _, Wemp, (fun _ ⇒ Aemp), false, None, None; split; [done | ].
ins; rewrite Heq, hupds, hvplusC; ins; split; ins.
f_equal; extensionality v; apply AsimD, Asim_sym, Asim_star_emp.
}
{ eexists _, _, RR, (fun v ⇒ sval (QQ0 v)), isrmwflag, permlbl, init; split; [done | ].
ins; rewrite Heq, hupds in *; ins; split.
× f_equal; [extensionality v | ]; desf.
+ extensionality v; generalize (HEAPcompat v); clear; ins.
unfold hv_acq_def, hv_rval in H; desf.
- apply assn_mod_eqI; Asim_simpl.
eapply Asim_trans.
by apply Asim_star_emp_l.
apply Asim_star; [ | by apply Asim_refl].
by rewrite <- H; apply Asim_sym, Asim_assn_norm.
- apply assn_mod_eqI; Asim_simpl.
rewrite H0; eapply Asim_trans.
by apply Asim_sym, Asim_star_false.
apply Asim_star; [ | by apply Asim_refl].
by rewrite <- H; apply Asim_sym, Asim_assn_norm.
+ by extensionality v; apply AsimD, Asim_star; [apply Asim_sym, Asim_assn_norm | apply Asim_refl].
× ins; desf; specialize (HEAPcompat x); unfold hv_acq_def, hv_rval in HEAPcompat; desf; eauto.
}
}
desc.
assert (∃ wri, << RF : rf fst = Some wri >> ∧ << WRI: is_writeLV (lab wri) E v >>).
{
red in CONS; desc; generalize (Crf fst); intro CrfFST; desf.
repeat eexists; desf; simpls.
by rewrite SEM1 in *; ins; desf.
exfalso.
exploit (initialization_always_before (AcyclicStrong_implies_IrreflexiveHBuRF ACYC)
Crf HC (proj1 VALID)); eauto.
by simpl; apply FST.
by simpl; exploit (HC0 fst); vauto; apply hc_edge_sb, FST.
by instantiate (2 := E); instantiate (1 := HLnormal);
rewrite Z0; clear; simpl; desf; red; eauto; inv Heq; eauto.
intro; desf.
eapply (CrfFST a); eauto.
2: eby rewrite SEM1.
red in FST; desc;clear - FST HB.
apply clos_refl_trans_hbE in HB; desf; eauto with hb.
}
desf.
assert (INwri: In wri V).
{
exploit (HC0 fst); vauto.
simpl; intro; desf.
exfalso; red in CONS; desc; eapply (AcyclicStrong_implies_IrreflexiveHBuRF ACYC); vauto.
}
destruct (eqP (assn_norm (QQ v)) Aemp) as [EMP|NEMP].
{
assert (T: (fun x : val ⇒ mk_assn_mod (hupd QQ v Aemp x)) =
(fun x : val ⇒ mk_assn_mod (QQ x))).
{
clear - EMP; exten; intro y; unfold hupd; desf; desf.
by apply assn_mod_eqI1; ins.
}
eapply safe_final3s with
(h := hsingl _ _ E (HVra Wemp (fun x ⇒ mk_assn_mod (hupd QQ v Aemp x)) false None HLnormal) +!+ hFR)
(hs := hsingl _ _ E (HVra Wemp Remp false None None)) (ga' := ga_clear ga fst); eauto.
by ins; apply ga_clear_agrees; congruence.
by eauto using ga_clear_fin.
× ∃ hemp; rewrite hplus_emp_r.
repeat eexists; repeat split; eauto; try done.
+ rewrite pEQ in pDEF; clear - pDEF EMP.
rewrite hdef_alt in pDEF; desf.
apply hplus_def_inv in pDEF; desf.
intro U; rewrite hplus_unfold in U; desf.
destruct n; unnw; rewrite gres_plusC, gres_plus_emp_r; split; ins.
specialize (DEFv v0).
unfold hupd; desf; ins; desf; rewrite ?hupds in DEFv; ins; desf.
split; ins; desf; desf.
rewrite assn_norm_emp.
by specialize (DEFv v); rewrite EMP in DEFv.
+ by instantiate (1 := gres_emp); instantiate (1 := (fun _ : val ⇒ HVnone));
rewrite hplus_emp_r, hplus_init1.
+ by rewrite hplus_emp_r.
+ vauto.
+ by rewrite <- assn_sem_assn_norm, EMP.
+ vauto.
+ vauto.
× red; desf.
∃ gres_emp; split.
by unfold ga_clear; split; ins; desf.
eexists _, _,hoo,goo; repeat split; try (by apply FST); try by (apply LST).
by unfold mupd; desf; desf; rewrite pEQ, T in ×.
by unfold mupd; desf; desf.
right; split; [done | ].
destruct hFR as [|hFR gFR]; try done.
eexists (wri :: nil), hemp,
(hsingl _ _ E (HVra Wemp (fun x : val ⇒ mk_assn_mod (QQ x)) false None HLnormal) +!+ Hdef hFR gFR),
(mk_assn_mod Aemp).
assert (RFemp: hmap (hb_rf wri fst) = hemp).
{
eapply RESTR; eauto.
right; split; ins.
clear; intro SB; red in SB; desf.
}
unnw; repeat (split; try by (clear Z0; ins; desf; vauto)); intros;
try (by ins; rewrite ?assn_norm_emp in *; ins; subst; rewrite ?hplus_emp_l in *).
+ clear Z0; ins; rewrite hsum_one; unfold mupd; desf; desf.
rewrite RFemp; vauto.
+ ∃ hemp; repeat split; try by vauto.
clear Z0; ins; rewrite hsum_one; unfold mupd; desf; desf.
by rewrite RFemp; apply Hsim_refl.
+ clear Z0; ins; rewrite hsum_one; unfold mupd; desf; desf.
by rewrite RFemp; apply Hsim_refl.
+ unfold mupd; desf; desf.
unnw; repeat f_equal.
clear - EMP; extensionality x.
unfold hupd; desf; desf.
+ rewrite Z in pEQ; clear - pEQ Z0.
assert (empEQ: hupd Remp v (mk_assn_mod Aemp) = @Remp PS PSg).
by extensionality x; unfold hupd; desf; desf.
rewrite empEQ, hplusAC, <- hplusA, hplus_init1, hplus_unfold; desf.
+ unfold mupd; desf; desf.
rewrite Z in pEQ; clear - T pEQ EMP.
by rewrite hplus_emp_r, hplus_emp_l, hplusAC, <- hplusA, hplus_init1; ins; repeat f_equal.
+ clear; left; repeat eexists.
}
generalize (VLD _ INwri); intro M.
red in M; destruct (lab wri) eqn: EQ; ins; desc; subst l v.
assert (WRI: is_writeLV (lab wri) E v0) by (rewrite EQ; done).
desc; destruct DISJ; desc; subst; try done.
{
red in CONS; desc; ins.
edestruct (no_atomic_reads_from_na_one FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC)
Ca Crf HC (proj1 VALID) pre _ INwri _ _
WRI (proj1 pU) pEQ0 IV prev fst V_PREV (proj1 FST) NIN);
eauto using hupds.
}
assert (XXX: ∃ PW QW isrmwW permW initW, hf E = HVra PW QW isrmwW permW initW ∧ PW v0 = P).
{
symmetry in UPD; apply hplus_def_inv in UPD; desc.
inv UPD.
generalize (PLUSv E), (DEFv E); unfold initialize; rewrite !hupds.
clear - TRAN0.
ins; desf; repeat eexists; instantiate; ins; rewrite ?hupds; desf;
by rewrite e in TRAN0; ins.
}
{
assert (Y: ∃ h1 hsink, hmap (hb_sink wri) = h1 +!+ hsink ∧ assn_sem (Anabla (QQ v0)) h1).
{
destruct isrmw.
× exfalso. destruct (Z1 eq_refl v0) as [MM|MM]; try done.
desc; subst; red in CONS; desc.
assert (WWW := wellformed_one_w); red in WWW.
destruct FST, pU, qU; eapply WWW in TRAN0; clear WWW;
try exact HC; try exact Z0; try exact XXX; try exact Z; try exact (proj1 VALID); try eassumption; eauto; [].
ins; desc.
apply (sim_assn_sem (Asim_assn_norm _)) in TRAN4; ins; desc.
by apply (sim_assn_sem (Asim_assn_norm _)) in TRAN8; rewrite MM in ×.
× red in CONS; desc; ins.
exploit annotated_rfs_and_sinks; try exact HC; try eassumption; eauto.
by apply pU.
by rewrite XXX.
{
ins.
destruct (classic (In x V)) as [INx | NINx].
× exfalso.
assert (NEMP': assn_norm (Astar (QQ v0) (QQ0 v0)) ≠ Aemp).
by intro EMP; apply assn_norm_star_eq_emp in EMP; desc.
assert (NFALSE': assn_norm (Astar (QQ v0) (QQ0 v0)) ≠ Afalse).
{
revert Z0; clear TYP.
red in WRI; desfh; desfh.
ins.
exploit wellformed_one_w; try exact HC; try exact Heq; try exact XXX; try exact V_PREV;
try eassumption; try (by unfold unique in *; desc; eauto with hb).
eby exact (proj1 VALID).
intro IMP; exploit (IMP V_PREV (proj1 FST)); try eassumption.
clear; intros NF F; ins; rewrite F in NF; desf.
}
assert (VALIDx := VLD _ INx).
revert Z0; clear TYP; red in VALIDx; desfh; desfh.
RMWin_def.
assert (l = E).
{
rewrite rfsOK in IN.
clear - Crf IN EQ Heq.
specialize (Crf x); rewrite IN, EQ, Heq in Crf; ins; desf.
}
subst l.
apply hplus_not_undef_l, hdef_alt in DEFin; desc; rewrite DEFin in ×.
symmetry in pEQ1; eapply hplus_ram_lD in pEQ1; desc.
2: by rewrite hupds.
clear pEQ4; ins.
exploit heap_loc_ra_no_own; try exact pEQ1; try (intro X; specialize (X _ _ Z0));
try exact HC; try eassumption; ins; try (by unfold unique in *; desc; eauto with hb).
eby exact (proj1 VALID).
instantiate (1 := v0) in X; clear Z0; desf.
× eapply (proj2 VALID); try by exact NINx.
right; split; unfold is_sb_out; ins.
by intro; desc.
}
ins; desc.
destruct x0; desc.
{
unnw; subst ann_rfs; ins.
rewrite rfEQ, hsum_nil, hplus_emp_l in ×.
subst P.
exploit (wellformed_one_w FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC) Ca Crf HC (proj1 VALID)
pre wri INwri EQ (proj1 pU) pEQ0 XXX prev fst V_PREV (proj1 FST) NIN); eauto.
intro WF; ins; desc.
rewrite assn_sem_assn_norm in *; ins; desc.
subst h1; subst h'.
∃ (lupd h0 HLnabla), (lupd (h3 +!+ h2) HLnabla).
repeat (apply conj).
by rewrite <- lupd_hplus_dist, <- hplusA; apply lupd_eq.
by apply lupd_label; intro U; rewrite U, !hplus_undef_l in ×.
eexists; repeat (apply conj); try edone.
by apply Hsim_sym, lupd_sim; intro U; rewrite U, !hplus_undef_l in ×.
by repeat (apply exact_label_hplus_dist in TRAN2; desc).
}
{
remember (hb_sb prev fst :: map hb_sink ann_rfs) as T.
assert (NDt : NoDup T).
{
subst T; apply nodup_cons.
split.
by rewrite In_map; intro; desc.
apply nodup_map; ins.
clear Z0 TYP; intro; desf.
}
assert (INt: ∀ edge : hbcase, In edge T → In (hb_fst edge) V).
{
clear Z0 TYP; subst T; ins; desf.
rewrite In_map in *; desf; ins; intuition.
}
assert (VALIDt: ∀ edge : hbcase, In edge T → edge_valid lab sb rf edge).
{
clear TYP Z0; subst T; ins; desf.
by ins; apply FST.
rewrite In_map in *; desf; ins.
apply SUBSET, rfsOK in H0.
red; desf; specialize (Crf x); rewrite H0, Heq in Crf; ins; desf.
}
assert (INDEP: independent sb rf T).
{
clear Z0 TYP; subst T; red; ins; desf; ins; rewrite ?In_map in *; desf; ins.
by destruct NIN; apply INann_rfs.
eby destruct NIN; eapply hist_closedD.
by destruct NIN; eapply hist_closedD; try edone; apply INann_rfs.
}
assert (HT: ∃ hT gT, hsum (map hmap T) = Hdef hT gT ∧
∃ PT QT isrmwT permT initT, hT E = HVra PT QT isrmwT permT initT ∧
QT v0 = mk_assn_mod (Astar (Astar (QQ v0) (QQ0 v0)) (sval QQread))).
{
clear TYP; revert Z0; subst T.
exploit independent_heap_compat; try exact HC; try eassumption; eauto.
by exact (proj1 VALID).
by ins; desf; rewrite In_map in *; desf.
by ins; desf; rewrite In_map in *; desf.
by ins; desf; rewrite In_map in *; desf; intuition.
by ins; desf; [apply FST | rewrite In_map in *; desf].
by ins; desf; rewrite In_map in *; desf.
by ins; desf; exploit (VALIDt (hb_sink a)); ins; eauto.
intros SUM ?; desc.
eexists _, _; split; try edone.
ins; rewrite hsum_cons, Z, SINKS in SUM.
clear - SUM Z0.
apply hplus_def_inv in SUM; desc.
inv SUM.
generalize (PLUSv E); rewrite Z0, hupds; clear; ins.
repeat eexists; eauto.
clear; ins; apply AsimD.
apply Asim_star.
by apply Asim_sym, Asim_assn_norm.
by rewrite hupds; apply Asim_refl.
}
subst P; desc.
exploit (wellformed_w FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC) Ca Crf HC (proj1 VALID)
pre wri INwri EQ (proj1 pU) pEQ0 XXX NDt INt VALIDt INDEP HT HT0); try exact TRAN0.
rewrite HT1; intro WF; simpls; desc.
rewrite assn_sem_assn_norm in ×.
subst h'.
rewrite rfEQ in ×.
clear - PREC NORM PRECISE NORMALIZABLE rfsSIM TRAN TRAN0 TRAN1 TRAN2 TRAN READS READS0 READS1 READS2
WF WF1 WF2.
ins; desf.
assert (EQ: hsum (map hmap (map (hb_rf wri) ann_rfs)) +!+ hmap (hb_sink wri)
= lupd (h4 +!+ h5 +!+ h3 +!+ h2) HLnabla) by (by rewrite !hplusA in TRAN1; apply lupd_eq).
assert (EQ': hsum (map hmap (map (hb_rf wri) ann_rfs)) = lupd h'0 HLnabla) by (by apply lupd_eq).
rewrite EQ', !(hplusAC h3), !lupd_hplus_dist in EQ.
specialize (NORMALIZABLE _ WF4); desc.
subst h3.
rewrite lupd_hplus_dist, hplusA in EQ.
apply precise_nabla in PRECISE.
assert (SAT0: assn_sem (Anabla (sval QQread)) (lupd h'0 HLnabla)).
{
split.
eby eapply lupd_label, assn_sem_def.
∃ h'0; repeat (apply conj); try done.
eby eapply Hsim_sym, lupd_sim, assn_sem_def.
}
assert (SATn: assn_sem (Anabla (sval QQread)) (lupd hN HLnabla)).
{
split.
eby eapply lupd_label, assn_sem_def.
∃ hN; repeat (apply conj); try done.
eby eapply Hsim_sym, lupd_sim, assn_sem_def.
}
assert (DEF: lupd h'0 HLnabla +!+ hmap (hb_sink wri) ≠ Hundef).
{
rewrite EQ' in rfsSIM.
red in rfsSIM; desc; congruence.
}
exploit (PRECISE _ SAT0 _ SATn _ DEF).
by exact EQ.
intro DECOMP; desc.
apply exact_label_sim with (lbl := HLnabla) in DECOMP0.
2: by apply exact_label_hplus_dist in TRAN; desc.
2: by rewrite <- !lupd_hplus_dist in *; apply lupd_label;
red in DECOMP0; desc; intro U; rewrite U in ×.
specialize (NORM _ _ WF6); desc.
subst h4.
rewrite lupd_hplus_dist, hplusA, hplusAC in DECOMP0.
eexists _, _; split; [by exact DECOMP0 | ].
split; [by apply lupd_label; intro U; rewrite U, !hplus_undef_r in × | ].
eexists; repeat apply conj; try exact NORM; try edone.
eby eapply Hsim_sym, lupd_sim, assn_sem_def.
}
}
clear Z Z0 Z1; desc.
assert (WOK: hmap_valid lab sb rf (mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink)
(ga_clear ga fst) wri).
{
red; rewrite EQ.
∃ gnew; split.
{ red; ins; split.
by intro X; apply NG in X; unfold ga_clear; desf.
by ins; apply NG; unfold ga_clear in *; desf.
}
eexists _, _, _, _; repeat (split; try edone); right; split; try done.
∃ rfs, hr, hF, P, sbg, rfg.
assert(SAME: hsum (map (mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink) (map (hb_rf wri) rfs))
+!+ mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink (hb_sink wri)
= hsum (map hmap (map (hb_rf wri) rfs)) +!+ hmap (hb_sink wri)).
{
clear TYP.
rewrite <- rfsOK in RF.
apply In_implies_perm in RF as [rfs' PERM].
rewrite !(hsum_perm (map_perm _ (map_perm _ PERM))); ins.
rewrite !hsum_cons.
rewrite !map_upd_irr; ins.
2: by intro; desf; apply Permutation_NoDup, nodup_cons in PERM; ins; desf.
unfold mupd; desf; desf.
desf.
symmetry; rewrite (hplusC h1), Y, !hplusA, <- hplus_emp_l.
f_equal.
eapply (proj2 VALID); eauto.
right; split; ins.
unfold is_sb_out; intro; desf.
}
rewrite <- SAME in *; unnw; repeat (split; try done).
eby eexists; split.
}
clear TYP.
assert (FOO': ∀ e, In e V →
hmap_valid lab sb rf (mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink)
(ga_clear ga fst) e).
{
ins; destruct (eqP e wri); desf.
eapply hmap_irr_change_valid.
by apply VLD.
by apply ga_clear_agrees; congruence.
ins; unfold mupd; desf; desf; ins; desf.
}
assert (FOO: hmap_valids lab sb rf (mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink) V).
by eexists; split; try exact FOO'; eauto using ga_clear_fin.
ins; desc.
assert (DEF': hsingl _ _ E
(HVra Wemp (fun x : val ⇒ mk_assn_mod (hupd QQ v0 Aemp x)) false None (Some HLCnormal))
+!+ h'0 +!+ hFR ≠ Hundef).
{
red in CONS; desc; ins.
exploit (independent_heap_compat FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC) Crf Ca HC FOO
(T := hb_rf wri fst :: hb_sb prev fst :: nil));
try solve [ by rewrite NoDup_two | ins; desf; apply FST].
by eapply independent_two; ins; eauto; try (by apply FST); intro; desf; eauto with hb.
intro DEF'; desc.
ins; rewrite hsum_two in DEF'.
unfold mupd in DEF'; desf; desf.
pattern g0 in DEF'; eapply ex_intro in DEF';
pattern h in DEF'; eapply ex_intro in DEF'; rewrite <- hdef_alt, pEQ in DEF'.
apply (hplus_sim_def _ Y2) in DEF'.
assert (D: hsingl _ _ E (HVra Wemp (fun x : val ⇒ mk_assn_mod (QQ x)) false None (Some HLCnormal))
=
hsingl _ _ E (HVra Wemp (hupd Remp v0 (mk_assn_mod (QQ v0))) false None None)
+!+
hsingl _ _ E
(HVra Wemp (fun x : val ⇒ mk_assn_mod (hupd QQ v0 Aemp x)) false None (Some HLCnormal))).
{
clear; rewrite hplus_hsingl; simpl; vauto.
repeat f_equal; desf.
extensionality v.
apply AsimD.
unfold hupd; desf; desf; ins.
by rewrite assn_norm_emp; eapply Asim_trans; [apply Asim_assn_norm | apply Asim_star_emp_r].
by rewrite assn_norm_emp; eapply Asim_trans; [apply Asim_assn_norm | apply Asim_star_emp_l].
}
rewrite hplusAC, D, hplusA in DEF'.
by intro U; rewrite U, hplus_undef_r in DEF'.
}
eapply safe_final4a with
(h := hsingl _ _ E
(HVra Wemp (fun x : val ⇒ mk_assn_mod ((hupd QQ v0 Aemp) x)) false None (Some HLCnormal))
+!+ h1 +!+ hFR)
(hs := hsingl _ _ E (HVra Wemp (hupd Remp v0 (mk_assn_mod (QQ v0))) false None None))
(ga' := ga_clear ga fst);
eauto.
by ins; apply ga_clear_agrees; congruence.
by eauto using ga_clear_fin.
{ ∃ hemp; rewrite hplus_emp_r.
eexists; repeat split; try done.
× rewrite hplusAC; rewrite hplusAC in DEF'.
eapply hplus_sim_def; try exact DEF'.
by apply Hsim_sym.
× by rewrite <- hplusA.
× eexists _, (hsingl _ _ E (HVra Wemp Remp false None (Some HLCnormal)) +!+ h1); repeat (split; try edone).
rewrite <- hplusA in DEF'.
apply hplus_not_undef_l in DEF'.
rewrite hplusC; rewrite hplusC in DEF'.
eapply hplus_sim_def; try exact DEF'.
by apply Hsim_sym.
by rewrite <- hplusA, hplus_init1.
eexists _, h1; repeat (split; try edone).
+ rewrite <- ohlplus_none_l in DEF' at 1.
rewrite <- (ohlplus_none_l (Some HLCnormal)) in DEF'.
rewrite <- hplus_init1, hplusA, <- (hplusA _ h'0) in DEF'.
apply hplus_not_undef_r, hplus_not_undef_l in DEF'.
rewrite hplusC; rewrite hplusC in DEF'.
eapply hplus_sim_def; try exact DEF'.
by apply Hsim_sym.
+ eexists; repeat (apply conj); solve [exact Y1 | exact Y2 | exact Y3].
}
{ red; rewrite SEM1.
∃ gres_emp; split.
by unfold ga_clear; split; ins; desf.
rewrite hdef_alt in pDEF; desc.
eexists _, _, hf0, g0; repeat (split; try edone).
{ unfold NW, mupd; desf; desf.
rewrite hplusAC; eapply hplus_sim_def; eauto.
eby apply Hsim_sym.
by rewrite hplusAC.
}
by unfold NW, mupd; desf; desf.
right.
split; [done | ].
eexists (wri :: nil), h1, _, (mk_assn_mod (QQ v0)).
repeat (apply conj; try edone); ins; rewrite ?hsum_one; unfold mupd; desf; desf.
× split; ins; desf; eauto.
× ∃ h'0; repeat split; try done.
by simpl; rewrite assn_sem_assn_norm.
× apply Hsim_refl.
red in Y0; desf.
× instantiate
(1 := hsingl _ _ E (HVra Wemp (fun x : val ⇒ mk_assn_mod (hupd QQ v0 Aemp x)) false None None)
+!+ hFR).
rewrite <- hplusA, hplus_hsingl, <- pDEF, pEQ; vauto.
ins; unnw; repeat f_equal; extensionality v; desf.
clear; apply AsimD.
unfold hupd; desf; desf; ins.
by rewrite assn_norm_emp; eapply Asim_trans; apply Asim_sym;
[apply Asim_star_emp_r | apply Asim_assn_norm].
by rewrite assn_norm_emp; eapply Asim_trans; apply Asim_sym;
[apply Asim_star_emp_l | apply Asim_assn_norm].
× rewrite hplus_emp_r, !(hplusC h1), <- !hplusA.
unnw; repeat f_equal.
rewrite hplusC, hplus_init1; simpl.
unnw; f_equal.
× eauto.
× by unnw; rewrite <- precise_assn_norm.
× by unnw; rewrite <- normalizable_assn_norm.
}
}
{
exfalso. RMWin_def.
red in CONS; desc; ins.
assert (NEMP': assn_norm (Astar (QQ v') (QQ0 v')) ≠ Aemp).
by intro EMP; apply assn_norm_star_eq_emp in EMP; desc.
assert (SEM': ∃ h, assn_sem (assn_norm (Astar (QQ v') (QQ0 v'))) h).
{
rewrite hdef_alt in DEFin; desc.
assert (RMW := DEFin); rewrite pEQ0, !hplusA in RMW.
eapply hplus_ram_lD in RMW; desc.
2: by rewrite hupds.
clear RMW2.
destruct (classic (v0 = v')) as [ | VAL]; [subst v0 | ].
× exploit wellformed_one; try exact HC; try exact DEFin; try exact V_PREV; try eassumption;
try (by unfold unique in *; desc; eauto with hb).
eby exact (proj1 VALID).
eby rewrite EQ.
intro IMP; exploit IMP; try exact NIN; try exact (proj1 FST); rewrite ?addn0; eauto.
eby apply RMW0; rewrite hupds.
eby clear; ins; desf; eexists.
× exploit wellformed_one; try exact HC; try exact DEFin; try exact V_PREV; try eassumption;
try (by unfold unique in *; desc; eauto with hb).
eby exact (proj1 VALID).
eby rewrite EQ.
intro IMP; exploit IMP; try exact NIN; try exact (proj1 FST); rewrite ?addn0; eauto.
eby apply RMW0; unfold hupd; rewrite eqxx.
eby clear; ins; desf; eexists.
}
destruct isrmw.
×
exploit Z1; try done.
instantiate (1 := v'); clear - NEMP SEM'.
intro CONTRA; desf.
rewrite assn_norm_star_intro, assn_sem_assn_norm, CONTRA in SEM'.
ins; desf.
×
apply hplus_not_undef_l, hdef_alt in DEFin; desc; rewrite DEFin in ×.
symmetry in pEQ0; eapply hplus_ram_lD in pEQ0; desc.
2: by rewrite hupds.
clear pEQ3; ins.
exploit heap_loc_ra_no_own; try exact Z0; try exact pEQ0; try exact HC;
(try (intro X; specialize (X _ _ Z0))); try eassumption; ins;
try (by unfold unique in *; desc; eauto with hb).
eby exact (proj1 VALID).
instantiate (1 := v') in X; clear Z0; desf.
by rewrite X in SEM'.
}
Grab Existential Variables. done.
Qed.
This page has been generated by coqdoc