Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps rslassn rslassnlemmas rslmodel.
Require Import rslhmap rslhmapna rslhmapa rsltriple rsltriple2.
Set Implicit Arguments.
Definition prg_sem e res acts lab sb rf mo sc mt :=
∃ fst lst pre post acts',
acts = pre :: acts' ∧
<< pNIN: ¬ In pre acts' >> ∧
<< qNIN: ¬ In post acts' >> ∧
<< NEQ : pre ≠ post >> ∧
<< ESEM: exp_sem e res acts' lab sb fst lst >> ∧
<< CONS: Consistent (post :: acts) lab sb rf mo sc mt >> ∧
<< pSB1: ∀ x, ¬ sb x pre >> ∧
<< pSB2: ∀ x, sb pre x → x = fst >> ∧
<< pSB : unique (sb^~ fst) pre >> ∧ << pL : lab pre = Askip >> ∧
<< qSB : unique (sb lst) post >> ∧ << qL : lab post = Askip >>.
Adequacy states that all consistent executions of closed programs, e,
satisfying the triple {Atrue} e {y. QQ y}, are memory safe and race free.
Moreover, the programs never read from uninitialized locations, and their
return value satisfies the post-condition.
Theorem adequacy :
∀ mt e QQ (T: triple mt Atrue e QQ) reso acts lab sb rf mo sc
(SEM : prg_sem e reso acts lab sb rf mo sc mt),
mem_safe acts lab sb rf mo ∧
race_free acts lab sb rf mo ∧
initialized_reads acts lab rf ∧
(∀ res, reso = Some res → ∃ h, assn_sem (QQ res) h).
Proof.
ins; red in SEM; unfold unique in *; desf; red in CONS; desf.
assert (HC: hist_closed mt lab sb rf mo (pre :: acts')).
assert (hist_closed mt lab sb rf mo (post :: pre :: acts')).
red; intros; destruct HB as [HB|[HB _]|HB].
by eapply FIN, proj1 in HB.
by eapply (proj1 FIN); intro X; rewrite X in ×.
by specialize (Crf a); rewrite HB in *; desc;
eapply (proj1 FIN); intro X; rewrite X in ×.
red; intros; generalize HB; eapply H in HB; eauto using In_cons.
destruct HB; try done; subst.
destruct 1; [|by red in HB_SW; rewrite qL in *; desf
|by specialize (Crf a); rewrite HB_RF, qL in Crf; desf].
ins; desf; [eby edestruct pSB1|].
by destruct (exp_sem_pre_closed _ _ _ _ _ _ _ ESEM _ _ HB_SB); desf; eauto.
assert (ND: NoDup (post :: pre :: acts')).
by repeat constructor; eauto using exp_sem_nodup; ins; intuition.
assert (∃ hmap, hmap_valids lab sb rf hmap (pre :: (acts' ++ nil))
∧ with_opt reso (fun res ⇒ assn_sem (QQ res)) (hmap (hb_sb lst post))).
{
assert (VAL: hmap_valids lab sb rf (fun _ : hbcase ⇒ hemp) (pre :: nil)).
red; ins; desf; red; rewrite pL; unfold not in ×.
∃ nil, (fst :: nil), (fun _ ⇒ HVnone), hemp; repeat (split; ins);
desf; eauto using eq_sym.
by rewrite hplus_emp_r, hsum_one; apply vshift_refl.
assert (HC': hist_closed mt lab sb rf mo (pre :: nil)).
red; ins; desf; unfold not in *; destruct HB as [|[? [? ?]]|RF];
rewrite ?pL in *; eauto.
by specialize (Crf a); rewrite RF, pL in *; desf.
cut (safe mt acts' (post :: pre :: nil) lab sb rf mo (S (length acts'))
(pre :: nil) (fun _ ⇒ hemp) lst
(with_opt reso (fun res h ⇒ ∃ hq, h ≠ Hundef ∧ h = hq +!+ hemp
∧ assn_sem (QQ res) hq))).
assert (INlst: In lst acts') by eauto using exp_sem_lst.
revert ND HC HC' VAL INlst.
change (pre :: acts') with ((pre :: nil) ++ acts').
rewrite <- (appl0 acts') at 3 4.
change (pre :: nil) with (nil ++ pre :: nil) at 6.
generalize (@nil actid) at 1 2 3 4 5 6 8 10 as V.
clear - qSB IRR Crf' Cna.
remember (S (length acts')) as n; revert Heqn.
generalize (fun _ : hbcase ⇒ hemp) as hmap, acts' as acts.
induction n; ins; desf.
destruct (classic (acts = nil)); subst; ins.
∃ hmap; split; ins; desf.
exploit POST; clear POST RELY GUAR; eauto using In_appI1.
by clear; destruct reso; ins; desf; rewrite hplus_emp_r in *; desf.
clear POST RELY.
eapply get_shallow with (V := pre :: V) in H4; try edone; desc;
try (by destruct mt).
exploit (GUAR e); clear GUAR; eauto using In_appI1.
by clear - IN H; rewrite ?nodup_cons, ?nodup_app, In_app in *;
ins; intro; desf; eauto.
by eapply Permutation_hist_closed, HC;
eauto using Permutation_cons_append.
intro M; desc.
eapply In_implies_perm in IN; desc.
assert (P' : Permutation (V ++ acts) (e :: V ++ l')).
clear - IN; simpl; etransitivity.
by eapply Permutation_app, IN; apply Permutation_refl.
by auto using Permutation_sym, Permutation_cons_app.
specialize (IHn hmap' l').
rewrite (Permutation_length IN) in IHn.
specialize (IHn eq_refl (e :: V)).
exploit IHn; clear IHn;
eauto using Permutation_NoDup, Permutation_hist_closed.
by eapply Permutation_hist_closed, HC; vauto.
by clear -VALID; red; ins; eapply VALID; rewrite In_app; ins; desf; eauto.
by ins; desf;
rewrite In_app in H3; des; try eapply (Permutation_in _ IN) in H3;
ins; desf; eauto using In_appI1, In_appI2, In_eq, In_cons.
rewrite (Permutation_length (Permutation_sym IN)); simpl.
eapply Permutation_safe1, SAFE.
change (e :: V) with ((e :: nil) ++ V); rewrite <- appA.
by eauto using Permutation_app, Permutation_trans,
Permutation_cons_append.
clear - IN; intro M; desf; eexists; split; try edone.
eapply Permutation_hmap_valids, M.
constructor; change (e :: V) with ((e :: nil) ++ V); rewrite <- appA.
apply Permutation_sym, Permutation_app;
eauto using Permutation_trans, Permutation_cons_append.
by destruct mt; ins; clear - Cna IRR; intros x H; apply (IRR x);
revert H; generalize x at 1 3; induction 1; desf; eauto with hb;
eapply Cna; eauto.
{
eapply T in ESEM; desc; eapply ESEM with (rf := rf) (sc := sc) (mo := mo);
clear ESEM T; vauto.
eapply ConsistentWeaken2, Consistent_perm; try edone.
2: by rewrite perm_eq_sym, perm_appC; apply perm_eq_refl.
by repeat (split; try done).
by eapply Permutation_NoDup; try apply Permutation_app_comm.
by rewrite hplus_emp_r.
done.
revert ESEM0; unfold with_mt, no_rlx_writes, no_rlx_writes_global.
ins; desf; ins; intro; eapply ESEM0; eauto.
eapply proj1 in FIN; specialize (FIN x).
unfold is_rlx_write in H; desf;
destruct FIN as [|[]]; congruence.
}
}
desc; rewrite appl0 in ×.
repeat split; eauto using valid_implies_mem_safe, valid_implies_race_free.
2: by ins; vauto.
red; ins; intro RF; assert (X := H _ IN).
specialize (Crf a); rewrite RF in Crf.
desf; try rewrite pL in *; ins.
red in X; desf; desf; ins; desf.
destruct pU; exploit heap_loc_na_initialized2; eauto; try done.
by eapply HC; eauto using In_cons; vauto.
intro M; desc.
eapply Crf; eauto using conj, eq_refl, is_write_weaken with nocore.
by ins; destruct M3; subst; eauto with hb.
assert (∃ PP QQ isrmw, hf l = HVra PP QQ isrmw true).
by eapply hplus_ra_lD with (l:=l) in pEQ'; auto using hupds; desf; eauto.
desc; destruct pU; exploit heap_loc_ra_initialized; eauto; try done.
by eapply HC; eauto using In_cons; vauto.
by ins; desf; eauto with hb.
desc; destruct pU; exploit heap_loc_ra_initialized; eauto; try done.
by eapply HC; eauto using In_cons; vauto.
by ins; desf; eauto with hb.
Qed.
Soundness of the proof rules
Frame
Theorem rule_frame :
∀ mt P E QQ (T: triple mt P E QQ) F,
triple mt (Astar P F) E (fun y ⇒ Astar (QQ y) F).
Proof.
split; apply T in SEM; desc; try done.
clear T SEM0; ins; desf; rewrite hplusA in ×.
exploit SEM; try edone.
instantiate (1 := n); clear - pSAT2; revert hmap V.
induction n; ins; desc; unfold NW; repeat split; ins; eauto.
specialize (POST IN _ SB); clear - POST pSAT2; desf.
destruct res; ins; desf; rewrite <- hplusA in *; repeat (eexists; try edone).
by rewrite POST0 in *; eauto.
specialize (GUAR _ INcmd NIN HC'); clear - GUAR IHn; desf; eauto.
Qed.
Theorem rule_conseq :
∀ mt P E QQ (T: triple mt P E QQ)
P' (PI: implies P' P)
QQ' (QI: ∀ y, implies (QQ y) (QQ' y)),
triple mt P' E QQ'.
Proof.
split; apply T in SEM; desc; try done.
clear T SEM0; ins; desf.
exploit SEM; try apply PI; try edone.
instantiate (1 := n); clear - QI; revert hmap V.
induction n; ins; desc; unfold NW; repeat split; ins; eauto.
specialize (POST IN _ SB); clear - POST QI; desf.
by destruct res; ins; desf; repeat (eexists; try edone); apply QI.
specialize (GUAR _ INcmd NIN HC'); clear - GUAR IHn; desf; eauto.
Qed.
Theorem rule_disj :
∀ mt P1 E QQ (T1: triple mt P1 E QQ)
P2 (T2: triple mt P2 E QQ),
triple mt (Adisj P1 P2) E QQ.
Proof.
split; [|by apply T1 in SEM; desc].
intros; rewrite assn_sem_disj in *; desf; [ eapply T1 | eapply T2 ]; eauto.
Qed.
Theorem rule_exists :
∀ mt PP E QQ (T: ∀ x, triple mt (PP x) E QQ),
triple mt (Aexists PP) E QQ.
Proof.
split; [|by apply (T 0) in SEM; desc].
by intros; rewrite assn_sem_exists in *; desc; eapply T; eauto.
Qed.
Theorem rule_value mt v QQ :
triple mt (QQ v) (Evalue v) QQ.
Proof.
eapply triple_helper_start; ins; desf; ins; desf.
by rewrite SEM1 in ×.
eapply safe_final_plain; eauto.
red; ins; desf; unfold NW.
unfold unique in *; desf.
eapply assn_sem_satD in pSAT; desf.
rewrite pEQ in *; eapply hdef_alt in pDEF; desf.
eexists (prev :: nil),(next :: nil),hf0, hemp; rewrite hplus_emp_r.
ins; rewrite !hsum_one; repeat (split; ins; desf); eauto;
unfold mupd; desf; try congruence.
rewrite pDEF; auto using vshift_refl.
Qed.
Theorem rule_let :
∀ mt P e QQ (T1: triple mt P e QQ)
RR e' (T2: ∀ x, triple mt (QQ x) (e' x) RR),
triple mt P (Elet e e') RR.
Proof.
split; ins; desf.
by eapply T1, proj1 in SEM0; exploit SEM0; eauto.
2: eby eapply T1.
2: by eapply T1, proj2 in ESEM1; eapply T2, proj2 in ESEM2;
unfold with_mt, no_rlx_writes in *; desf; ins;
rewrite In_app in *; desf; eauto.
rewrite appA in ×.
assert (UU1: unique (sb lst1) fst2) by (ins; desf; red; eauto using eq_sym).
generalize (proj1 (T1 _ _ _ _ _ _ ESEM1) _ _ _ _ CONS UNIQ _ FST _ UU1
n V V_PREV (fun x H ⇒ In_appI2 (V_CTX x H) _)
HC hmap VALID pDEF _ _ pEQ pSAT NOREL); clear T1; intro T1.
assert (CONS': weakConsistent (acts2 ++ acts1 ++ acts_ctx) lab sb rf mo sc mt).
eapply weakConsistent_perm; eauto.
by rewrite perm_appCA, perm_eq_refl.
assert (UNIQ': NoDup (acts2 ++ acts1 ++ acts_ctx)).
eapply nodup_perm; eauto.
by rewrite perm_appCA, perm_eq_refl.
assert (UU2: unique (sb^~ fst2) lst1) by (red; eauto using eq_sym).
specialize (proj1 (T2 _ _ _ _ _ _ _ ESEM2) _ _ _ _ CONS' UNIQ' _ UU2 _ LST);
clear T2; intro T2.
clear UU1 CONS' UNIQ' UU2.
assert (RNG: ∀ x, In x V → In x (acts1 ++ acts_ctx))
by eauto using In_appI2.
clear V_PREV V_CTX pEQ pDEF pSAT.
revert hmap V HC T1 VALID RNG ; induction n; ins; unfold NW.
ins; desf; repeat split; ins.
exfalso; eapply RNG in IN; rewrite In_app in *; desf;
eauto using exp_sem_lst.
by rewrite !nodup_app in *; desf; eauto using exp_sem_lst.
clear NOREL.
eapply IHn; eauto using In_appI2; unfold not; ins; desf;
eauto using In_appI2.
rewrite In_app in *; desf.
exploit GUAR; eauto; ins; desf.
∃ hmap'; repeat (split; try done).
eapply IHn; ins; unfold not; ins; desf; eauto using In_appI1.
clear IHn RELY GUAR.
assert (In fst2 (a :: V)).
by eapply (hist_closed_trans HC'); eauto using exp_sem_fst_reach, In_eq.
assert (¬ In fst2 V).
intro M; eapply RNG in M; rewrite In_app in *; desf; eauto using exp_sem_fst.
by rewrite !nodup_app in *; desf; eauto using exp_sem_fst.
ins; desf.
assert (In lst1 V).
exploit HC'; eauto using In_eq; ins; desf; vauto.
by subst lst1; exfalso; eauto using exp_sem_lst.
exploit POST; eauto; intro M; desf.
exploit (T2 (S n) V); eauto; []; intros (_ & _ & G).
exploit G; clear G; eauto; []; intro; desf.
∃ hmap'; repeat (split; ins); eapply safe_mod; eauto;
ins; rewrite In_app in *; desf; eauto.
by destruct NIN0; right; eapply hist_closed_trans;
eauto using exp_sem_lst_reach.
Qed.
Theorem rule_par :
∀ mt P1 e1 QQ1 (T1: triple mt P1 e1 QQ1)
P2 e2 Q2 (T2: triple mt P2 e2 (fun x ⇒ Q2)),
triple mt (Astar P1 P2) (Epar e1 e2) (fun x ⇒ Astar (QQ1 x) Q2).
Proof.
ins; eapply triple_helper_start; ins; desf; ins.
{ rewrite In_app in *; desf.
by rewrite LABF in ×.
by rewrite LABL in ×.
eby eapply T1.
eby eapply T2. }
assert (NEQf: fst1 ≠ fst2).
by intro; ins; rewrite !nodup_cons, nodup_app in NODUP;
desf; eauto using exp_sem_fst.
assert (NEQl: lst1 ≠ lst2).
by intro; ins; rewrite !nodup_cons, nodup_app in NODUP;
desf; eauto using exp_sem_lst.
assert (∃ hmap',
<< AGR: agrees lab sb rf V hmap hmap' >> ∧
<< VALID: ∀ e (IN: In e (fst::V)), hmap_valid lab sb rf hmap' e >> ∧
hmap' (hb_sb fst fst1) = h1 ∧
hmap' (hb_sb fst fst2) = h2 +!+ hFR ∧
hmap' (hb_sb fst fst2) ≠ Hundef).
∃ (mupd (mupd hmap (hb_sb fst fst1) h1) (hb_sb fst fst2) (h2 +!+ hFR)).
unfold NW; repeat split; ins; desf; eauto using valid_ext;
unfold mupd; desf; desf; red; ins; desf.
2: by eapply pDEF; rewrite pEQ, hplusA, H, hplusC.
eapply hdef_alt in pDEF; desf; unfold NW.
∃ (prev :: nil),(fst1 :: fst2 :: nil),hf,hemp; rewrite hplus_emp_r.
ins; rewrite hsum_one, hsum_two; desf; desf.
unfold unique in *; des.
repeat split; ins; des; subst; try done; eauto.
by repeat econstructor; red; ins; desf.
by eapply UF0 in H; desf; vauto.
by rewrite <- pDEF, pEQ, hplusA; apply vshift_refl.
clear pEQ pSAT pDEF VALID HC; desf.
∃ hmap'; repeat (split; try done); clear hmap AGR.
assert (PERM : perm_eq (fst :: lst :: (acts1 ++ acts2) ++ acts_ctx)
(acts1 ++ fst :: lst :: acts2 ++ acts_ctx)).
rewrite appA, perm_appCA with
(s1 := fst :: lst :: nil) (s2 := acts1)
(s3 := acts2 ++ acts_ctx); simpl.
by rewrite perm_eq_refl.
assert (UUF: unique (sb^~ fst1) fst) by (red; eauto using eq_sym).
assert (UUL: unique (sb lst1) lst) by (split; ins; desf; eauto using eq_sym).
assert (S1: safe mt acts1 (fst :: lst :: acts2 ++ acts_ctx) lab sb rf mo n
(fst :: V) hmap' lst1
(with_opt res1 (fun res h ⇒ ∃ hq, h ≠ Hundef ∧ h = hq +!+ hemp
∧ assn_sem (QQ1 res) hq))).
eapply T1; ins; desf; eauto using In_appI2, In_eq, weakConsistent_perm.
by eapply (nodup_perm _ _ _ PERM).
eby eapply assn_sem_def.
by rewrite hplus_emp_r.
clear PERM UUF UUL.
assert (PERM : perm_eq (fst :: lst :: (acts1 ++ acts2) ++ acts_ctx)
(acts2 ++ fst :: lst :: acts1 ++ acts_ctx)).
by rewrite perm_eq_sym, <- perm_appCA with
(s1 := fst :: lst :: acts1) (s2 := acts2)
(s3 := acts_ctx), appA, perm_eq_refl.
assert (UUF: unique (sb^~ fst2) fst) by (red; eauto using eq_sym).
assert (UUL: unique (sb lst2) lst) by (split; ins; desf; eauto using eq_sym).
assert (S2: safe mt acts2 (fst :: lst :: acts1 ++ acts_ctx) lab sb rf mo n
(fst :: V) hmap' lst2
(with_opt res2 (fun _ h ⇒ ∃ hq, h ≠ Hundef ∧ h = hq +!+ hFR
∧ assn_sem Q2 hq))).
eapply T2; ins; desf; eauto using In_appI2, weakConsistent_perm.
by eapply (nodup_perm _ _ _ PERM).
clear PERM UUF UUL.
revert S1 S2.
assert (RNG: ∀ x, In x (fst :: V) →
In x (fst :: acts1 ++ acts2 ++ acts_ctx)).
by ins; desf; eauto using In_appI2.
generalize (In_eq fst V) as INfst.
clear H0 H2 pSAT1 T1 T2 NEQf FST UF0 UF1 UF2 SBF1 SBF2 LABF.
revert RNG VALID HC0.
generalize (fst :: V); clear V V_PREV NIN V_CTX; intro V; revert V;
rename hmap' into hmap; revert hmap.
induction n; ins; desf; unfold NW; repeat (split; ins); eauto using In_cons.
by exfalso; rewrite !appA, !nodup_cons in *; apply RNG in IN; ins; desf; eauto.
eapply IHn; eauto using In_appI2, In_cons.
by ins; desf; rewrite !nodup_cons in UNIQ; desf; eauto using In_appI2.
rewrite In_app in INcmd; desf.
assert (ACYC: IrreflexiveHB lab sb rf mo) by (red in CONS; desf).
assert (NEQ1 : lst1 ≠ a).
by intro; subst; rewrite !nodup_cons, !In_app in UNIQ; desf; eauto using exp_sem_lst.
assert (NEQ2 : lst2 ≠ a).
by intro; subst; rewrite !nodup_cons, !In_app in UNIQ; desf; eauto using exp_sem_lst.
assert (IN1: In lst1 V)
by (assert (In lst1 (a :: V)); eauto using In_eq with hb; ins; desf).
assert (IN2: In lst2 V)
by (assert (In lst2 (a :: V)); eauto using In_eq with hb; ins; desf).
clear RELY GUAR RELY0 GUAR0.
assert (∃ hf, hmap (hb_sb lst1 a) +!+ hmap (hb_sb lst2 a) = Hdef hf).
{ clear IHn.
rewrite <- hsum_two.
change (hmap (hb_sb lst1 a) :: hmap (hb_sb lst2 a) :: nil) with
(map hmap (hb_sb lst1 a :: hb_sb lst2 a :: nil)).
eapply independent_heap_compat with (V := V); eauto; ins; desf; eauto.
eby red in CONS; desf.
by red in CONS; desf.
by constructor; ins; intro; desf.
by red; ins; desf; ins; desf;
eapply ACYC, happens_before_trans, HB; auto with hb.
}
desf.
eapply safe_final_plain with (h := hmap (hb_sb lst1 a) +!+ hmap (hb_sb lst2 a));
ins; desf; eauto.
eapply POST in IN2; eauto.
eapply POST0 in IN1; eauto.
clear - CVAL IN1 IN2 H; desf.
destruct res; ins; desf; destruct res2; ins; desf.
rewrite hplus_emp_r in ×.
∃ (hq +!+ hq0); rewrite hplusA; repeat (eexists; try edone); try congruence.
by intro X; rewrite IN0, IN4, <- hplusA, X in ×.
red; ins; desf; destruct LST; unfold NW.
∃ (lst1 :: lst2 :: nil),(next :: nil),hf,hemp; simpl;rewrite hplus_emp_r.
rewrite hsum_one, hsum_two; unfold mupd; desf; desf.
repeat split; ins; desf; eauto.
by repeat econstructor; red; ins; desf.
by edestruct UL0; desf; eauto.
by rewrite H; eauto using vshift_refl.
specialize (GUAR0 _ INcmd NIN HC'); desf.
repeat (eexists; try edone); eapply IHn; eauto using In_appI1, In_cons.
by ins; desf; rewrite !nodup_cons in UNIQ; desf; eauto using In_appI1, In_appI2.
specialize (GUAR _ INcmd NIN HC'); desf.
repeat (eexists; try edone); eapply IHn; eauto using In_appI1, In_cons.
by ins; desf; rewrite !nodup_cons in UNIQ; desf; eauto using In_appI1, In_appI2.
Qed.
Theorem rule_repeat :
∀ mt P e QQ (T: triple mt P e QQ) (IMP: implies (QQ 0) P),
triple mt P (Erepeat e) (fun x ⇒ if x == 0 then Afalse else QQ x).
Proof.
split.
2: by ins; desf; destruct mt; ins; intros a IN WRI;
rewrite In_flatten in *; desf; rewrite In_map in *; desf;
destruct x as [[[r acts]f]l]; ins;
apply ESEM, T, proj2 in IN1; apply IN1 in IN.
simpls; desf; clear NODUP.
revert fst resI actsI lstI GET_F ESEM REP GET_I.
induction sems; ins; desf; ins.
rewrite flatten_cons, appA in ×.
assert (N : ∃! next, sb lstI next).
clear IHsems CONS UNIQ.
destruct sems as [|[[[??]?]?]]; ins; desf; eauto.
by exploit (REP nil); ins; desf; eexists; split; eauto using eq_sym.
destruct N as [next' N].
assert (RNG: ∀ x, In x V → In x (actsI ++ acts_ctx))
by eauto using In_appI2.
assert (S := ESEM _ _ _ _ (In_eq _ _)); apply T, proj1 in S.
exploit S; clear S; eauto using In_appI2.
instantiate (1 := n).
clear prev FST V_PREV pDEF pEQ V_CTX.
revert V hmap HC VALID RNG .
induction n; ins; desf; unfold NW; repeat split; ins.
clear RELY GUAR IHn IHsems CONS.
assert (lstI = lst ∧ res = resI).
destruct (lastP sems); ins; desf.
rewrite last_snoc in *; desf.
rewrite snocE, map_app, !map_cons, flatten_app, flatten_cons in UNIQ; ins.
rewrite snocE in ×.
assert (M := ESEM _ _ _ _ (In_cons _ (In_appI2 (In_eq _ _) s))).
apply exp_sem_lst in M; apply RNG in IN.
exfalso; clear -IN UNIQ M.
by rewrite ?nodup_app, ?In_app in *; desf; eauto using In_appI1, In_appI2.
by subst; destruct res; ins; desf; subst; ins; apply POST.
by eapply IHn, RELY; ins; desf; eauto using In_appI2.
rewrite In_app in INcmd; desf.
by exploit GUAR; eauto; ins; desf; repeat (eexists; try edone);
eapply IHn; ins; desf; eauto using In_appI1.
clear RELY GUAR IHn.
destruct sems as [|[[[resJ actsJ]fstJ]lstJ]]; ins.
rewrite flatten_cons in ×.
eapply weakConsistent_Permutation in CONS; [|apply Permutation_app_comm].
rewrite appA in UNIQ; eapply Permutation_NoDup in UNIQ; [|apply Permutation_app_comm].
rewrite !appA in ×.
exploit (REP nil); ins; desf.
clear next' N.
rewrite H0 in *; clear H0.
specialize (IHsems fstJ resJ actsJ lstJ eq_refl).
assert (ESEM0 := (ESEM _ _ _ _ (or_introl eq_refl))).
specialize (fun r a f l H ⇒ ESEM r a f l (or_intror H)).
assert (a = fstJ); subst.
assert (clos_refl_trans _ sb fstJ a).
clear - REP INcmd ESEM.
rewrite In_app in *; desf; eauto using exp_sem_fst_reach.
assert (R := (ESEM _ _ _ _ (or_introl eq_refl))).
eapply exp_sem_fst_reach in R; [|by eapply exp_sem_lst, R].
specialize (fun r a f l H ⇒ ESEM r a f l (or_intror H)).
specialize (fun p r1 a1 f1 l1 r2 a2 f2 l2 s H ⇒
REP (_ :: p) r1 a1 f1 l1 r2 a2 f2 l2 s (f_equal (cons _) H)); simpls.
eapply rt_trans; eauto; clear R.
revert resJ actsJ fstJ lstJ REP; induction sems as [|[[[r a']f]l]]; ins.
rewrite flatten_cons, In_app in *; desf.
exploit (REP nil); ins; desf.
by eapply rt_trans with f; eauto using exp_sem_fst_reach, rt_step.
exploit (REP nil); ins; desf.
eapply rt_trans with f; eauto using exp_sem_fst_reach, rt_step.
eapply rt_trans with l; eauto 7 using exp_sem_fst_reach, exp_sem_lst.
eapply IHsems; ins; eauto.
by eapply (REP (_ :: _)); ins; f_equal; apply H.
assert (In fstJ actsJ) by eauto using exp_sem_fst.
assert (Z: In fstJ (a :: V)) by eauto using hist_closed_trans, In_eq.
ins; desf; apply RNG, In_app in Z.
exfalso; clear - H0 Z UNIQ; rewrite nodup_app in UNIQ.
by desf; eauto using In_appI1, In_appI2.
assert (In lstI V).
assert (In lstI (fstJ :: V)) by eauto using In_eq with hb.
by ins; desf; exfalso; clear - CONS SB; red in CONS; desc; eauto with hb.
exploit POST; clear POST; try edone; ins; desf.
exploit IHsems; clear IHsems; rewrite ?appA; eauto using f_equal.
eby ins; eapply (REP (_ :: prefix)); ins; f_equal.
by split; eauto using eq_sym.
by clear - RNG; intros ? X; eapply RNG in X; rewrite In_app in *; tauto.
instantiate (1 := S n); ins; desf.
exploit (GUAR fstJ); clear POST RELY GUAR; ins; desf.
∃ hmap'; split; try done; split; try done.
eapply safe_mod; try exact SAFE; eauto using In_appI1.
ins; rewrite In_app in IN; desf.
destruct NIN0; right; eauto using exp_sem_lst_reach, hist_closed_trans.
Qed.
Theorem rule_alloc_na mt :
triple mt (Aemp) (Ealloc) (fun x ⇒ Aptu x).
Proof.
eapply triple_helper_start; ins; desf; ins.
by desf; ins; desf; rewrite SEM1 in ×.
destruct hFR as [|hFR]; [by rewrite pEQ, hplusC in pDEF|].
rewrite hplus_emp_l in ×.
assert (hFR l = HVnone). {
apply NNPP; intro NEQ.
red in CONS; desc.
eapply (heap_loc_allocated IRR HC VALID (hb_sb _ _) (proj1 FST)) in NEQ;
ins; desc.
assert (c = fst) by eauto; subst.
by apply clos_refl_trans_hbE in NEQ0; desf; eauto with hb.
}
eapply safe_final_plain with (h := Hdef (hupd hFR l (HVuval))); eauto.
repeat eexists; try edone.
rewrite hplus_unfold; desf; ins.
by f_equal; extensionality y; unfold hupd; desf; ins; desf.
by destruct n0; intro; unfold hupd; desf; ins; desf.
red; rewrite SEM1.
eexists _, _, hFR; repeat (split; try edone); auto using mupds; unfold NW.
rewrite mupdo; try red; ins; desf.
Qed.
Non-atomic stores
Theorem rule_store_na1 :
∀ mt typ E E' E'' (TYP: with_mt mt (typ ≠ ATrlx ∧ typ ≠ ATacq) True),
triple mt (Apt E E') (Estore typ E E'') (fun x ⇒ Apt E E'').
Proof.
intros; eapply triple_helper_start; ins; desf; ins.
by desf; ins; desf; rewrite SEM1 in *; ins; desf.
destruct hFR as [|hFR]; [by rewrite pEQ, hplusC in pDEF|].
assert (EQ: hsingl E (HVval E') +!+ Hdef hFR = Hdef (hupd hFR E (HVval E'))).
clear - pDEF pEQ; rewrite hplus_unfold in *; desf.
by f_equal; extensionality y; specialize (h y); clear pEQ;
unfold hupd in *; desf; ins; desf.
eapply safe_final3 with (exn := nil) (h := Hdef (hupd hFR E (HVval E'')));
eauto.
repeat eexists; try edone.
symmetry; revert EQ; clear; rewrite !hplus_unfold; ins; desf.
f_equal; extensionality y; specialize (h y); specialize (h0 y).
by apply (f_equal (fun f ⇒ f y)) in H0; unfold hupd in *; desf; ins; desf.
destruct n; intro y; specialize (h y).
by apply (f_equal (fun f ⇒ f y)) in H0; unfold hupd in *; desf; ins; desf.
red; ins; desf; unfold NW.
eexists prev, next,(hupd hFR E (HVval E')).
repeat split; try done; try (by apply LST); try (by apply FST);
try left; repeat split; unfold mupd, hupd; ins; desf; desf.
by rewrite pEQ, EQ; f_equal; extensionality y; desf; desf.
by f_equal; extensionality y; desf; desf.
Qed.
Theorem rule_store_na2 :
∀ mt typ E E'' (TYP: with_mt mt (typ ≠ ATrlx ∧ typ ≠ ATacq) True),
triple mt (Aptu E) (Estore typ E E'') (fun x ⇒ Apt E E'').
Proof.
intros; eapply triple_helper_start; ins; desf; ins.
by desf; ins; desf; rewrite SEM1 in *; ins; desf.
destruct hFR as [|hFR]; [by rewrite pEQ, hplusC in pDEF|].
assert (EQ: hsingl E HVuval +!+ Hdef hFR = Hdef (hupd hFR E HVuval)).
clear - pDEF pEQ; rewrite hplus_unfold in *; desf.
by f_equal; extensionality y; specialize (h y); clear pEQ;
unfold hupd in *; desf; ins; desf.
eapply safe_final3 with (exn := nil) (h := Hdef (hupd hFR E (HVval E'')));
eauto.
repeat eexists; try edone.
symmetry; revert EQ; clear; rewrite !hplus_unfold; ins; desf.
f_equal; extensionality y; specialize (h y); specialize (h0 y).
by apply (f_equal (fun f ⇒ f y)) in H0; unfold hupd in *; desf; ins; desf.
destruct n; intro y; specialize (h y).
by apply (f_equal (fun f ⇒ f y)) in H0; unfold hupd in *; desf; ins; desf.
red; ins; desf; unfold NW.
eexists prev, next,(hupd hFR E HVuval).
repeat split; try done; try (by apply LST); try (by apply FST);
try left; repeat split; unfold mupd, hupd; ins; desf; desf.
by rewrite pEQ, EQ; f_equal; extensionality y; desf; desf.
by f_equal; extensionality y; desf; desf.
Qed.
Non-atomic loads
Theorem rule_load_na :
∀ mt typ E E' (TYP: with_mt mt (typ ≠ ATrlx ∧ typ ≠ ATrel) True),
triple mt (Apt E E') (Eload typ E)
(fun x ⇒ if x == E' then Apt E E' else Afalse).
Proof.
intros; eapply triple_helper_start; ins; subst.
by desf; ins; desf; rewrite SEM1 in ×.
destruct hFR as [|hFR]; [by rewrite pEQ, hplusC in pDEF|].
assert (EQ: hsingl E (HVval E') +!+ Hdef hFR = Hdef (hupd hFR E (HVval E'))).
clear - pDEF pEQ; rewrite hplus_unfold in *; desf.
by f_equal; extensionality y; specialize (h y); clear pEQ;
unfold hupd in *; desf; ins; desf.
rewrite EQ in *; desf.
assert (M: v = E'); desf; ins.
exploit heap_loc_na_initialized2; try exact HC; eauto using hupds;
ins; try eapply FST; try (eby red in CONS; desc); desc.
red in CONS; desc.
specialize (Crf fst); des_if; desc.
{
rewrite SEM1 in *; ins; desc; subst.
cut (a = c);
[by intro; subst; clear - Crf0 x1; destruct (lab c); ins; desf |].
assert (INa: In a V).
destruct mt.
2: by destruct (HC0 _ (In_eq _ _) a); clarify; auto using hc_edge;
edestruct ACYC; eauto with hb.
cut (is_na (lab fst) ∨ is_na (lab a)
∨ synchronizes_with lab sb rf mo a fst).
by intro; desf; destruct (HC0 _ (In_eq _ _) a); clarify;
auto using hc_edge; edestruct ACYC; eauto with hb.
cut (is_na (lab fst) ∨ is_na (lab a)
∨ is_release (lab a) ∧ is_acquire (lab fst)).
by clear -SEM1 Heq; ins; desf; eauto; do 2 right;
repeat split; try done; ∃ a; split; [left|].
by rewrite SEM1; clear -NOREL Crf0 TYP; ins; desf; vauto; right;
specialize (NOREL a); simpls; desc; unfold is_na; desf; ins; vauto.
destruct (valid_accessD _ _ _ _ _ (VALID _ INa)) as [aprev AA];
eauto; desc.
replace (loc (lab a)) with l in × by (destruct (lab a); ins; desf).
assert (HBa: a = prev ∨ happens_before lab sb rf mo a prev).
clear x4.
apply NNPP; intro NHB; unfold unique in *; apply not_or_and in NHB; desc.
assert (IND: independent lab sb rf mo (hb_sb aprev a :: hb_sb prev fst :: nil)).
by apply independent_two; ins; eauto; intro; desc; clarify; eauto with hb.
eapply independent_heap_compat in IND; try exact HC; eauto;
try (by ins; desf; eauto with hb).
desc; ins; rewrite hsum_two, AA0, pEQ, hplusC, hplus_unfold in IND;
des_if; clarify.
by specialize (h0 l); rewrite hupds in *; simpls; desf.
by constructor; ins; intro; desf.
assert (HBc: happens_before lab sb rf mo c fst)
by (destruct FST; desf; eauto with hb).
edestruct (two_access_cases (mt:=mt) cpre c a) with (V := V); eauto;
try (by desf; eauto using hist_closedD).
by destruct (lab c); ins; desc; congruence.
by destruct (lab a), (lab c); ins; desc; congruence.
unfold not in *; destruct H; exfalso; [by desf; eauto|].
eapply (Cwr c); try apply Heq; try by desf; eauto with hb.
by rewrite SEM1; destruct (lab c); ins; desf.
by eapply Cmo; eauto.
}
edestruct (Crf c); try rewrite SEM1; ins; instantiate;
try rewrite addn0; eauto.
by destruct FST; desf; eauto with hb.
eapply safe_final_plain2; eauto.
instantiate (1 := Hdef (hupd hFR E (HVval E'))).
by rewrite eqxx; repeat eexists; try done.
red; ins; desf; unfold NW.
eexists prev, next,(hupd hFR E (HVval E')).
repeat split; try done; try (by apply LST); try (by apply FST);
unfold mupd; desf; desf.
left; repeat (eexists; try edone); unfold hupd; ins; desf; desf.
Qed.
Theorem rule_alloc_atom_acq mt QQ :
triple mt (Aemp) (Ealloc) (fun x ⇒ Astar (Arel x QQ) (Aacq x QQ)).
Proof.
eapply triple_helper_start; ins; desf; ins.
by desf; ins; desf; rewrite SEM1 in ×.
destruct hFR as [|hFR]; [by rewrite pEQ, hplusC in pDEF|].
rewrite hplus_emp_l in ×.
assert (hFR l = HVnone). {
apply NNPP; intro NEQ.
red in CONS; desc.
eapply (heap_loc_allocated IRR HC VALID (hb_sb _ _) (proj1 FST)) in NEQ;
ins; desc.
assert (c = fst) by (eby eapply Ca).
by apply clos_refl_trans_hbE in NEQ0; desf; eauto with hb.
}
pose (QQ' := fun x ⇒ mk_assn_mod (QQ x)).
assert (EQ : ∀ isrmw,
hsingl l (HVra QQ' Remp false false) +!+
hsingl l (HVra Wemp QQ' isrmw false) =
hsingl l (HVra QQ' QQ' isrmw false)).
intro; rewrite hplus_unfold; desf.
f_equal; extensionality y; specialize (h y); unfold hupd in *; desf; ins; desf; ins.
by f_equal; extensionality v; desf; specialize (h v); desf; ins;
eapply assn_mod_eqI1; ins; try rewrite e; Asim_simpl.
by f_equal; extensionality v; desf; specialize (h v); desf; ins;
eapply assn_mod_eqI; ins; try rewrite e; Asim_simpl.
by destruct n0; intro; unfold hupd; desf; split; ins; vauto; destruct isrmw; vauto.
eapply safe_final_plain with (h := Hdef (hupd hFR l (HVra QQ' QQ' false false))); eauto.
subst QQ'; repeat eexists; try edone; instantiate; rewrite EQ; try done.
rewrite hplus_unfold; desf; ins.
by f_equal; extensionality y; unfold hupd; desf; ins; desf.
by destruct n0; intro; unfold hupd; desf; ins; desf.
red; rewrite SEM1.
eexists _, _, hFR; repeat (split; try edone); eauto using mupds; unfold NW.
rewrite mupdo; try red; ins; desf.
Qed.
Theorem rule_alloc_atom_rmwacq mt QQ :
triple mt (Aemp) (Ealloc) (fun x ⇒ Astar (Arel x QQ) (Armwacq x QQ)).
Proof.
eapply triple_helper_start; ins; desf; ins.
by desf; ins; desf; rewrite SEM1 in ×.
destruct hFR as [|hFR]; [by rewrite pEQ, hplusC in pDEF|].
rewrite hplus_emp_l in ×.
assert (hFR l = HVnone). {
apply NNPP; intro NEQ.
red in CONS; desc.
eapply (heap_loc_allocated IRR HC VALID (hb_sb _ _) (proj1 FST)) in NEQ;
ins; desc.
assert (c = fst) by (eby eapply Ca).
by apply clos_refl_trans_hbE in NEQ0; desf; eauto with hb.
}
pose (QQ' := fun x ⇒ mk_assn_mod (QQ x)).
assert (EQ : ∀ isrmw,
hsingl l (HVra QQ' Remp false false) +!+
hsingl l (HVra Wemp QQ' isrmw false) =
hsingl l (HVra QQ' QQ' isrmw false)).
intro; rewrite hplus_unfold; desf.
f_equal; extensionality y; specialize (h y); unfold hupd in *; desf; ins; desf; ins.
by f_equal; extensionality v; desf; specialize (h v); desf; ins;
eapply assn_mod_eqI1; ins; try rewrite e; Asim_simpl.
by f_equal; extensionality v; desf; specialize (h v); desf; ins;
eapply assn_mod_eqI; ins; try rewrite e; Asim_simpl.
by destruct n0; intro; unfold hupd; desf; split; ins; vauto; destruct isrmw; vauto.
eapply safe_final_plain with (h := Hdef (hupd hFR l (HVra QQ' QQ' true false))); eauto.
subst QQ'; repeat eexists; try edone; instantiate; rewrite EQ; try done.
rewrite hplus_unfold; desf; ins.
by f_equal; extensionality y; unfold hupd; desf; ins; desf.
by destruct n0; intro; unfold hupd; desf; ins; desf.
red; rewrite SEM1.
eexists _, _, hFR; repeat (split; try edone); eauto using mupds; unfold NW.
rewrite mupdo; try red; ins; desf.
Qed.
Definition release_typ typ := typ = ATrel ∨ typ = ATsc.
Theorem rule_store_rel mt typ E E' P (TYP : release_typ typ) :
triple mt (Astar (Arel E (mupd (fun _ ⇒ Afalse) E' P)) P)
(Estore typ E E')
(fun _ ⇒ Arainit E).
Proof.
eapply triple_helper_start; ins; desf; ins; subst.
by destruct TYP; desf; ins; desf; rewrite SEM1 in ×.
eapply safe_final3 with (h := _ +!+ hFR); eauto.
repeat eexists; try edone.
revert pDEF; rewrite pEQ.
rewrite hplusA, hplusAC; clear; intro X; eapply hplus_not_undef_r in X.
destruct hFR; ins.
rewrite hplus_unfold in *; desf; destruct n; intro v.
by specialize (h v); unfold hupd in *; desf; ins; desf; split;
vauto; destruct isrmwflag; vauto.
pose proof (has_sw_succs rf fst (proj1 CONS)); desc; red; ins; desf;
unfold NW.
eapply hdef_alt in pDEF; desf.
eexists prev, next.
unfold mclearw at 1 2 3, mupd at 1 2 3; desf; desf.
repeat (eexists; try edone).
right; split; [by destruct TYP; desf|].
eexists h2,(mk_assn_mod P),sws,_; repeat (split; simpl; vauto); try (by ins; desf).
2: by eapply sim_assn_sem, pSAT2; Asim_simpl.
2: by rewrite map_upd_irr, map_clearw_sws, hplus_emp_l; try done.
2: by destruct TYP; ins; desf.
rewrite map_upd_irr, map_clearw_sws, hplus_emp_l; ins.
unfold mupd; desf; desf.
eapply vshift_eqI.
revert pDEF; rewrite pEQ; clear; destruct h2; ins.
rewrite hplusA in pDEF.
generalize pDEF; eapply hplus_ra_lD with (l := E) in pDEF; eauto using hupds.
ins; desc; clarify; erewrite hdef_initializeE; eauto.
rewrite <- pDEF0.
rewrite !hplusA, !(hplusAC hFR); f_equal.
symmetry; rewrite hplusC, !hplusA, !(hplusAC (Hdef hf0)); f_equal.
rewrite hplusC, !hplus_init1.
by do 4 f_equal; extensionality y; unfold mupd, hupd; desf; ins.
Qed.
Relaxed stores
Theorem rule_store_rlx E E' :
triple Model_hb_rf_acyclic
(Arel E (mupd (fun _ ⇒ Afalse) E' Aemp))
(Estore ATrlx E E')
(fun _ ⇒ Arainit E).
Proof.
eapply triple_helper_start; ins; desf; ins; subst.
assert (DEF: hsingl E (HVra Wemp Remp false true) +!+ hFR ≠ Hundef).
revert pDEF; rewrite pEQ.
clear; intro X.
destruct hFR; ins.
rewrite hplus_unfold in *; desf; destruct n; intro v.
specialize (h v); unfold hupd in *; desf; ins; desf; split; vauto.
by destruct isrmwflag; vauto.
eapply safe_final_plain2 with (h := _ +!+ hFR); eauto.
repeat eexists; try edone.
eapply hdef_alt in pDEF; desc.
red; rewrite SEM1; ∃ prev, next, hf; unfold NW.
repeat (eexists; try edone).
by rewrite mupdo; ins; intro; desf.
right; split; try done.
eexists hemp, (mk_assn_mod Aemp), nil,_; ins.
rewrite assn_norm_emp; repeat (split; try done; try apply hplus_emp_l).
eapply vshift_eqI; rewrite pEQ in ×.
rewrite mupds, hplus_emp_l, hplus_emp_r, <- hplusA, hplus_init1.
assert (∃ PP QQ rmw init, hf E = HVra PP QQ rmw init); desc.
by eapply hplus_ra_lD in pDEF; [|apply hupds]; desc; eauto.
erewrite hdef_initializeE; eauto.
rewrite <- pDEF, hplusC, hplusAC, <- hplusA, hplus_init1.
by do 4 f_equal; clear; extensionality l; unfold mupd, hupd; desf.
by unfold ann_sw; rewrite SEM1; ins; desf.
Qed.
Relaxed loads
Theorem rule_load_rlx mt E :
triple mt
(Arainit E)
(Eload ATrlx E)
(fun _ ⇒ Arainit E).
Proof.
eapply triple_helper_start; ins; desf; ins; desf; subst.
by desf; ins; desf; rewrite SEM1 in ×.
eapply safe_final_plain with (h := _ +!+ hFR); eauto.
repeat eexists; try edone; congruence.
eapply hdef_alt in pDEF; desc.
red; rewrite SEM1; ∃ prev, next, hf; unfold NW.
repeat (eexists; try edone).
by rewrite mupdo; ins; intro; desf.
right; split; try done.
eexists nil, (fun _ ⇒ HVnone), hFR, (mk_assn_mod Aemp); ins.
rewrite mupds, assn_norm_emp, hplus_emp_l.
repeat (split; try done); try congruence.
by unfold ann_sw; rewrite SEM1; ins; desf.
rewrite <- pDEF, pEQ; do 4 f_equal.
by clear; extensionality l; unfold hupd; desf.
Qed.
Second, we have a stronger rule asserting that the value read was once
written. Note that this stronger rule is valid only in Model_hb_rf_acyclic.
Theorem rule_load_rlx2 E QQ :
triple Model_hb_rf_acyclic
(Astar (Aacq E QQ) (Arainit E))
(Eload ATrlx E)
(fun v ⇒ if (excluded_middle_informative (∃ h, assn_sem (QQ v) h)) then
Astar (Aacq E QQ) (Arainit E)
else Afalse).
Proof.
eapply triple_helper_start; ins; desf; ins; desf.
{
eapply safe_final_plain with (h := _ +!+ hFR); eauto.
repeat eexists; try edone; congruence.
eapply hdef_alt in pDEF; desc.
red; rewrite SEM1; ∃ prev, next, hf; unfold NW.
repeat (eexists; try edone).
by rewrite mupdo; ins; intro; desf.
right; split; try done.
eexists nil, (fun _ ⇒ HVnone), (Hdef hf), (mk_assn_mod Aemp); ins.
rewrite mupds, assn_norm_emp, hplus_emp_l.
rewrite hplus_init1 in ×.
assert (M: hupd Remp v (mk_assn_mod Aemp) = Remp)
by (by clear; extensionality y; unfold hupd; desf).
rewrite M, <- pDEF, pEQ, hplusAC, <- hplusA, hplus_init1.
repeat (split; try done); try congruence.
by unfold ann_sw; rewrite SEM1; ins; desf.
}
destruct n0.
rewrite hplus_init1 in ×.
assert (Z : ∃ hoo PP QQ0 isrmw, hmap (hb_sb prev fst) = Hdef hoo
∧ hoo E = HVra PP (fun x ⇒ mk_assn_mod (Astar (QQ x) (QQ0 x))) isrmw true).
rewrite pEQ in *; clear -pDEF.
destruct hFR; ins; rewrite hplus_unfold in *; desf.
specialize (h E); rewrite hupds in *; ins; desf; try destruct isrmwflag; desf;
repeat (eexists; try edone); instantiate; simpl; rewrite hupds; simpl;
rewrite Heq; f_equal; try done; extensionality y; apply assn_mod_eqI; simpl.
by instantiate (1 := fun v ⇒ Aemp); ins; Asim_simpl.
by instantiate (1 := fun v ⇒ (sval (QQ0 v))); ins; Asim_simpl;
generalize (Asim_assn_norm (QQ y));
destruct (h y) as [X|[X ->]]; simpls; rewrite X;
clear; eauto using Asim.
by instantiate (1 := fun v ⇒ (sval (QQ0 v))); ins; Asim_simpl.
desc.
assert (∃ wri, << RF : rf fst = Some wri >> ∧
<< WRI: is_writeLV (lab wri) E v >>).
{
red in CONS; desc; specialize (Crf fst); desf.
repeat eexists; desf; simpls.
by rewrite SEM1 in *; ins; desf.
exploit (heap_loc_ra_initialized FIN IRR Ca HC VALID (hb_sb prev fst));
eauto; try eapply FST; ins.
exfalso; desc; destruct FST.
eapply (Crf c); eauto; [by desf; eauto with hb|by rewrite SEM1 in *].
}
desf.
assert (INwri: In wri V). {
exploit HC0; eauto using In_eq; vauto.
by ins; red in CONS; desf; exfalso; eauto with hb.
}
generalize (VALID _ INwri); intro M.
eapply valid_ext_clearw2 with (w := wri) (V := V) in M; eauto;
try by (red in CONS; desc).
red in M; destruct (lab wri) eqn: EQ; ins; desc; [subst l v0|subst l v'];
assert (WRI: is_writeLV (lab wri) E v) by (rewrite EQ; done).
des; subst; try done.
{
rewrite eqxx in *; red in CONS; desc.
edestruct (no_acq_reads_from_na_one FIN IRR Ca HC VALID pre _ INwri _ _
WRI (proj1 pU) pEQ0 DISJ prev fst V_PREV (proj1 FST) NIN);
eauto using hupds.
}
{
red in CONS; desc.
assert (XXX: ∃ PW QW isrmwW initW, hf E = HVra PW QW isrmwW initW ∧
(∀ h, assn_sem (sval P) h → assn_sem (sval (PW v)) h)); desf.
{
assert (D := vshift_def UPD); desf; rewrite D in ×.
eapply hplus_ra_lD in D; [|by apply hupds]; desc.
eapply vshift_ra in UPD; try edone.
clear D2; desf.
unfold initialize in *; rewrite hupds in UPD; desf.
by repeat eexists; ins; apply UPD0, D0; rewrite hupds.
}
pose proof (read_loses_perm1 hmap lab sb rf E v V swsND); desc.
exploit (wellformed_one_w FIN IRR Ca HC VALID pre INwri EQ (proj1 pU)
pEQ0 XXX prev fst V_PREV (proj1 FST) NIN l); eauto using hupds.
by ins; eapply EQl in IN; desc.
by ins; eapply swsOK; eapply EQl in IN; desc.
by ins; eapply EQl in IN; desc.
simpl; intro S; desf.
eapply sim_assn_sem in S1; try eapply Asim_assn_norm.
destruct S1 as (ha & hb & DEF & <- & S1 & _); vauto.
}
{
red in CONS; desc.
assert (XXX: ∃ PI QI isrmwI initI, hi E = HVra PI QI isrmwI initI ∧
(∀ h, assn_sem (sval (PP' v)) h → assn_sem (sval (PI v)) h)); desf.
{
assert (D := vshift_def UPD); desf; rewrite D in ×.
eapply hplus_ra_lD in D; [|by apply hupds]; desc.
eapply vshift_ra in UPD; try edone.
clear D2; desf; rewrite UPD in ×.
by repeat eexists; ins; apply UPD0, D0.
}
rewrite map_clearw_irr in iEQ; ins; desf.
pose proof (read_loses_perm1 hmap lab sb rf E v V swsOutND); desc.
exploit (wellformed_one FIN IRR Ca HC VALID pre INwri WRI (proj1 pU)
swsInOK swsInND iEQ XXX prev fst V_PREV (proj1 FST) NIN l); eauto using hupds.
by ins; eapply EQl in IN; desc.
by ins; eapply swsOutOK; eapply EQl in IN; desc.
by ins; eapply EQl in IN; desc.
simpl; intro S; desf.
eapply sim_assn_sem in S1; try eapply Asim_assn_norm.
destruct S1 as (ha & hb & DEF & <- & S1 & _); vauto.
}
Qed.
Definition acquire_typ typ := typ = ATacq ∨ typ = ATsc.
Theorem rule_load_acq mt typ E QQ (PREC: ∀ v, precise (QQ v))
(TYP : acquire_typ typ) :
triple mt
(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.
by desf; ins; desf; rewrite SEM1 in ×.
rewrite hplus_init1 in ×.
assert (Z : ∃ hoo PP QQ0 isrmw, hmap (hb_sb prev fst) = Hdef hoo
∧ hoo E = HVra PP (fun x ⇒ mk_assn_mod (Astar (QQ x) (QQ0 x))) isrmw true
∧ (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.
specialize (h E); rewrite hupds in *; ins; desf; desf; try destruct isrmwflag; ins;
(do 5 eexists; [done|]); instantiate; simpl;
rewrite hupds; simpl; rewrite Heq;
(split; [f_equal; try done; extensionality y; apply assn_mod_eqI; simpl|]); ins.
by instantiate (1 := fun v ⇒ Aemp); ins; Asim_simpl.
by instantiate (1 := fun v ⇒ (sval (QQ0 v))); ins; Asim_simpl;
generalize (Asim_assn_norm (QQ y));
destruct (h y) as [X|[X ->]]; simpls; rewrite X;
clear; eauto using Asim.
by destruct (h x) as [X|[X _]]; simpls; rewrite X;
clear; eauto using Asim.
by instantiate (1 := fun v ⇒ (sval (QQ0 v))); ins; Asim_simpl.
desc.
assert (∃ wri, << RF : rf fst = Some wri >> ∧
<< WRI: is_writeLV (lab wri) E v >> ∧
<< HB : hc_edge mt lab sb rf mo wri fst >>).
{
red in CONS; desc; specialize (Crf fst); desf.
repeat eexists; desf; simpls.
by rewrite SEM1 in *; ins; desf.
destruct mt; [|by vauto]; case_eq (is_release (lab a)).
by destruct TYP; desf; econstructor 2;
repeat (eexists; try edone); rewrite ?SEM1; vauto.
by specialize (NOREL a); econstructor 3; destruct (lab a); ins; desf; vauto.
exploit (heap_loc_ra_initialized FIN IRR Ca HC VALID (hb_sb prev fst));
eauto; try eapply FST; ins.
exfalso; desc; destruct FST.
eapply (Crf c); eauto; [by desf; eauto with hb|by rewrite SEM1 in *].
}
desf.
assert (INwri: In wri V). {
exploit HC0; eauto using In_eq; ins; desf; vauto.
eby eapply hc_edge_irr in HB.
}
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.
assert (DEF: (hsingl E (HVra Wemp (fun x ⇒ mk_assn_mod (hupd QQ v Aemp x))
false false) +!+
hsingl E (HVra Wemp Remp false true) +!+ hemp) +!+ hFR ≠ Hundef).
by rewrite hplus_emp_r, hplus_init1, T, <- pEQ.
eapply safe_final5 with (h := _ +!+ hFR); eauto;
try (by red in CONS; desc).
repeat eexists; repeat split; eauto.
by eapply sim_assn_sem; [by apply Asim_assn_norm|]; instantiate; rewrite EMP.
eapply hdef_alt in pDEF; desc.
red; rewrite SEM1; eexists prev, next, hf; unfold NW.
repeat (eexists; try edone).
by rewrite mupdo; ins; intro; desf.
right; split; try done; [by inv TYP|].
assert (M: hupd Remp v (mk_assn_mod Aemp) = Remp)
by (by clear; extensionality y; unfold hupd; desf).
eexists (if is_release (lab wri) then wri :: nil else nil),
(fun _ ⇒ HVnone), (hsingl _ _ +!+ hFR), (mk_assn_mod Aemp); ins.
rewrite mupds, assn_norm_emp, hplus_emp_l, T, hplus_emp_r, hplus_init1, M.
rewrite hplusAC, <- hplusA, hplus_init1.
rewrite ?hplus_emp_r, ?hplus_init1 in ×.
repeat apply conj; try edone; instantiate; try congruence.
by desf.
ins; desf; unfold ann_sw; split; ins; desf; repeat split; try done; eauto.
by rewrite SEM1; inv TYP.
by rewrite map_upd_irr; ins; desf; ins; rewrite !eqxx, hsum_one; desf.
}
generalize (VALID _ INwri); intro M.
eapply valid_ext_clearw2 with (w := wri) (V := V) in M; eauto;
try by (red in CONS; desc).
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).
des; subst; try done.
{
rewrite eqxx in *; red in CONS; desc.
edestruct (no_acq_reads_from_na_one FIN IRR Ca HC VALID pre _ INwri _ _
WRI (proj1 pU) pEQ0 DISJ prev fst V_PREV (proj1 FST) NIN);
eauto using hupds.
}
assert (Y: ∃ h1 hsink', hsink = h1 +!+ hsink' ∧ assn_sem (QQ v0) h1).
destruct isrmw.
destruct (Z1 eq_refl v0) as [MM|MM]; try done.
assert (XXX: ∃ PW QW isrmwW initW, hf E = HVra PW QW isrmwW initW ∧ PW v0 = P).
{
rewrite vshift_hack in UPD.
symmetry in UPD; apply hplus_def_inv in UPD; desf.
generalize (PLUSv E), (DEFv E); unfold initialize; rewrite !hupds;
clear - TRAN.
ins; desf; repeat eexists; instantiate; ins; rewrite ?hupds; desf;
by rewrite e in TRAN; ins.
}
desc; subst; red in CONS; desc.
assert (WWW := wellformed_one_w); red in WWW.
destruct FST, pU, qU; eapply WWW with (R:=nil) in TRAN; clear WWW;
try exact HC; try exact Z0; try exact XXX; try exact Z; ins; eauto; [].
desc; apply (sim_assn_sem (Asim_assn_norm _)) in TRAN1; ins; desc.
by apply (sim_assn_sem (Asim_assn_norm _)) in TRAN5; rewrite MM in ×.
eby eapply load_helper1 with (V:=V); try exact CONS; try exact Z0;
try exact pEQ0; try exact Z.
desf.
{
assert (IMP2: is_release (lab wri) = false → sws = nil).
clear -swsOK; intro; destruct sws; ins.
by destruct (proj1 (swsOK _) (In_eq _ _)); clarify.
assert (IMP: is_release (lab wri) = false → h1 = hemp).
ins; rewrite IMP2 in *; ins.
rewrite RLX in TRAN; ins.
2: by rewrite EQ in *; ins; desf; vauto.
rewrite hsum_nil, hplus_emp_l in *; ins.
by eapply hplus_eq_emp in TRAN; desc.
assert (WOK: hmap_valid lab sb rf (mupd_sw (mclearw hmap wri V) wri fst h1) wri).
{
red; rewrite EQ.
do 3 eexists; repeat (split; try edone); right; split; try done.
unfold NW; eexists ( hsum (map (mupd_sw (mclearw hmap wri V) wri fst h1) (map (hb_sw wri) sws)) +!+
hsink'),P,sws,hsink'.
case_eq (is_release (lab wri)) as REL.
2: by rewrite IMP, IMP2, !hplus_emp_l in *; ins.
assert (IN: In fst sws).
by destruct TYP; desf; eapply swsOK; repeat split; try done; rewrite SEM1.
rewrite map_upd_sw_same3, hplusA; ins; vauto.
2: by desf; desf; apply/inP in Heq0.
by revert UPD TRAN; rewrite !(hplusAC h1).
}
assert (FOO: ∀ e, In e V →
hmap_valid lab sb rf (mupd_sw (mclearw hmap wri V) wri fst h1) e).
intros; destruct (eqP e wri); desf.
by red in CONS; desc; eapply valid_ext_sw; try eapply valid_ext_clearw2; eauto.
desf.
assert (DEF:
hsingl E (HVra Wemp (fun x ⇒ mk_assn_mod (hupd QQ v0 Aemp x)) false false) +!+
hsingl E (HVra Wemp Remp false true) +!+ h1 +!+ hFR ≠ Hundef).
{
red in CONS; desc.
assert (M: ∃ h, hsum (h1 :: hmap (hb_sb prev fst) :: nil) = Hdef h).
case_eq (is_release (lab wri)) as REL.
2: by rewrite hsum_cons, hsum_one, IMP, hplus_emp_l; ins; apply hdef_alt.
exploit (independent_heap_compat FIN IRR Ca HC FOO
(T := hb_sw wri fst :: hb_sb prev fst :: nil));
simpl; rewrite ?eqxx; try done.
by constructor; vauto; intro; ins; desf.
by ins; desf.
by ins; desf.
by destruct FST; ins; desf.
by destruct TYP; ins; desf; repeat split; try done; rewrite SEM1.
eapply independent_two; ins; eauto; try by intro; subst; eauto with hb.
by destruct TYP; desf; repeat eexists; try rewrite SEM1.
by destruct FST.
rewrite <- hplusA, hplus_init1; desc; revert M.
rewrite hsum_cons, hsum_one, pEQ, hplusAC; clear.
destruct (h1 +!+ hFR); ins.
rewrite hplus_unfold in *; desf.
by destruct n; intro v; specialize (h0 v); unfold hupd in *; desf; ins; desf;
split; ins; desf; ins; destruct isrmwflag; vauto.
}
eapply safe_final4a
with (wri := wri) (h := Hdef _ +!+ Hdef _ +!+ h1 +!+ hFR)
(h' := h1);
eauto.
by red in CONS; desc.
eexists; split; try edone.
split; [by rewrite <- !hplusA | ]; instantiate; rewrite hplusA.
repeat (eexists; try edone).
by clear -DEF; rewrite <- !hplusA in *; eauto.
by clear -DEF; apply hplus_not_undef_r in DEF; rewrite <- hplusA in DEF; eauto.
{
red; rewrite SEM1; unfold NW.
repeat (eexists; try edone).
unfold mupd, mclearw; desf; [exfalso|]; desf.
unfold mupd_sw; desf; try edone.
right; split; [by destruct TYP; desf|].
unfold mupd at 1 2; rewrite !eqxx; desf; desf.
assert (
hsingl E (HVra Wemp (fun x ⇒ mk_assn_mod (QQ x)) false true) =
hsingl E (HVra Wemp (hupd Remp v0 (mk_assn_mod (QQ v0))) false true) +!+
hsingl E (HVra Wemp (fun x ⇒ mk_assn_mod (hupd QQ v0 Aemp x)) false false)).
clear.
rewrite hplus_unfold; desf.
f_equal; extensionality v; unfold hupd, hvplus; desf; desf; simpl.
f_equal; extensionality v; desf; desf; simpl; eapply AsimD;
eauto using Asim, Asim_assn_norm.
by destruct n; intros; unfold hvplusDEF, hupd; desf; desf; simpl; vauto.
destruct (assn_sem_satD _ _ Y0) as [hw ->].
case_eq (is_release (lab wri)) as REL.
eexists (wri :: nil), hw,
(hsingl E (HVra Wemp (fun x ⇒ mk_assn_mod (hupd QQ v0 Aemp x)) false false) +!+ hFR),
(mk_assn_mod (QQ v0)).
repeat (apply conj; try done).
by destruct TYP; desf; ins; split; ins; desf; repeat split; rewrite ?SEM1; try done;
left; red in H0; rewrite RF in *; desf.
by ins; rewrite !eqxx, hsum_one.
by rewrite <- Z, pEQ, <- hplusA; f_equal.
by rewrite mupds, hplusC, !hplusA; do 2 f_equal; rewrite hplusC.
by simpl; eapply sim_assn_sem, Y0; Asim_simpl.
by clear - PREC; intros until 2; apply (PREC v0);
eapply sim_assn_sem; try edone; Asim_simpl.
eexists nil, hw,
(hsingl E (HVra Wemp (fun x ⇒ mk_assn_mod (hupd QQ v0 Aemp x)) false false) +!+ hFR),
(mk_assn_mod (QQ v0)).
rewrite IMP, IMP2 in *; try reflexivity; ins.
repeat (apply conj; try done).
by unfold ann_sw; split; ins; desf; congruence.
by rewrite <- Z, pEQ, <- hplusA; f_equal.
by rewrite mupds, hplusC, !hplusA; do 2 f_equal; rewrite hplusC.
by simpl; eapply sim_assn_sem, Y0; Asim_simpl.
by clear - PREC; intros until 2; apply (PREC v0);
eapply sim_assn_sem; try edone; Asim_simpl.
}
}
{
assert (CONTRA: sval (mk_assn_mod (Astar (QQ v') (QQ0 v'))) ≠ Aemp).
by simpl; intro H; apply assn_norm_star_eq_emp in H; desf.
assert (CONTRA': assn_norm (QQ v') ≠ Afalse).
assert (XXX: ∃ PW QW isrmwW initW, hi E = HVra PW QW isrmwW initW
∧ PW v' = PP' v').
{
rewrite vshift_hack in UPD.
symmetry in UPD; apply hplus_def_inv in UPD; desf.
rewrite (PLUSv E); generalize (DEFv E); unfold initialize; rewrite !hupds;
clear - TRAN'.
ins; desf; desf; eauto; repeat eexists; instantiate; ins; desf;
by rewrite e in TRAN'; ins.
}
desc; rewrite <- XXX0 in *; red in CONS; desc.
assert (WWW := wellformed_one); red in WWW.
destruct FST, pU, qU;
eapply WWW with (R:=nil) (hmap := mclearw hmap wri V) in TRAN'; clear WWW;
try exact HC; try exact Z0; try exact XXX; try exact Z; ins; eauto; [| |].
2: by red; ins; eapply valid_ext_clearw2; eauto.
2: by rewrite EQ.
desc; apply (sim_assn_sem (Asim_assn_norm _)) in TRAN'1; ins; desc.
by intro MM; apply (sim_assn_sem (Asim_assn_norm _)) in TRAN'5;
rewrite MM in ×.
destruct CONTRA, FST, pU; red in CONS; desc.
destruct isrmw.
by destruct (Z1 eq_refl v') as [MM|MM]; rewrite MM in ×.
eapply heap_loc_ra_no_own with (v:=v') (V:=V) in Z0;
eauto; ins; destruct Z0; eauto with hb; ins.
by eapply assn_norm_star_eq_false in H3; ins; desf.
}
Grab Existential Variables.
exact true.
Qed.
Theorem rule_cas :
∀ mt P typ1 typ2 E E' E'' RR QQ QQ'
(NA: typ1 ≠ ATna)
(NOT0: typ1 = ATrlx ∨ typ1 = ATrel ∨ typ1 = ATacq →
mt = Model_hb_rf_acyclic)
(NOT1: typ1 = ATrlx ∨ typ1 = ATrel → QQ E' = Aemp)
(NOT2: typ1 = ATrlx ∨ typ1 = ATacq → QQ' E'' = Aemp)
(IMP1: implies P (Astar (Astar (Armwacq E QQ) (Arainit E)) Atrue))
(IMP2: implies (Astar (QQ E') P)
(Astar (Astar (Arel E QQ') (QQ' E'')) (RR E')))
(T2: triple mt P (Eload typ2 E) (fun x ⇒ if x == E' then Atrue else RR x)),
triple mt P (Ecas typ1 typ2 E E' E'') RR.
Proof.
ins; eapply triple_helper_start; ins; desf; ins; desf.
by desf; ins; desf; rewrite SEM1 in *; ins; desf; exploit NOT0; vauto.
by desf; ins; desf; rewrite SEM1 in *; ins; desf; exploit NOT0; vauto.
2: by specialize (T2 (fst :: nil) (Some v') lab sb fst fst);
eapply proj1 in T2; ins; eauto;
exploit T2; clear T2; eauto 7; instantiate;
instantiate (1 := S n); ins; desf; desf;
exploit GUAR; clear POST RELY GUAR; try eassumption; eauto.
clear T2.
exploit IMP1; clear IMP1; eauto; intro X; ins; desf; clear X1 X2 X3.
rewrite hplus_init1, ?hplusA in ×.
assert (Z : ∃ hoo PP, hmap (hb_sb prev fst) = Hdef hoo
∧ hoo E = HVra PP (fun x ⇒ mk_assn_mod (QQ x)) true true).
rewrite pEQ in *; clear -pDEF.
destruct (h2 +!+ hFR); ins; rewrite hplus_unfold in *; desf.
by specialize (h E); rewrite hupds in *; ins; desf; desf;
try destruct isrmwflag; ins;
(do 3 eexists; [done|]); instantiate; simpl;
rewrite hupds; simpl; rewrite Heq;
f_equal; try done; extensionality y; apply assn_mod_eqI; simpl.
desc.
assert (∃ wri, << RF : rf fst = Some wri >> ∧
<< WRI: is_writeLV (lab wri) E E' >> ∧
<< HB : hc_edge mt lab sb rf mo wri fst >>).
{
red in CONS; desc; specialize (Crf fst); desf.
repeat eexists; desf; simpls.
by rewrite SEM1 in *; ins; desf.
destruct mt; [|by vauto]; case_eq (is_acquire (lab fst)) as ACQ.
case_eq (is_release (lab a)).
by econstructor 2; repeat (eexists; try edone); rewrite ?SEM1; vauto.
by specialize (NOREL a); econstructor 3; destruct (lab a); ins; desf;
vauto.
by exploit NOT0; try done; clear - NA SEM1 ACQ;
rewrite SEM1 in *; ins; desf; vauto.
exploit (heap_loc_ra_initialized FIN IRR Ca HC VALID (hb_sb prev fst));
eauto; try eapply FST; ins.
exfalso; desc; destruct FST.
eapply (Crf c); eauto; [by desf; eauto with hb|by rewrite SEM1 in *].
}
clear NOT0; desf.
assert (INwri: In wri V). {
exploit HC0; eauto using In_eq; ins; desf; vauto.
eby eapply hc_edge_irr in HB.
}
generalize (VALID _ INwri); intro M.
eapply valid_ext_clearw2 with (w := wri) (V := V) in M; eauto;
try by (red in CONS; desc).
red in M; destruct (lab wri) eqn: EQ; ins; desc; subst.
assert (WRI: is_writeLV (lab wri) E E') by (rewrite EQ; done).
des; subst; try done.
{
rewrite eqxx in *; red in CONS; desc.
edestruct (no_acq_reads_from_na_one FIN IRR Ca HC VALID pre _ INwri _ _
WRI (proj1 pU) pEQ0 DISJ prev fst V_PREV (proj1 FST) NIN);
eauto using hupds.
}
{
assert (K: hsum (map (mclearw hmap wri V) (map (hb_sw wri) sws)) = hemp).
by eapply rmw_helper0, swsOK; eauto.
rewrite K, hplus_emp_l in ×.
assert (Y: ∃ h1 hsink', hsink = h1 +!+ hsink' ∧ assn_sem (QQ E') h1).
by eapply rmw_helper1 with (V:=V); try exact Z0; try exact pEQ0;
try exact Z; eauto.
desf.
red in CONS; desc.
destruct (classic (ann_sw lab rf wri fst)) as [SW|NSW].
{
destruct FST.
assert (VAL': hmap_valids lab sb rf (mupd_sw (mclearw hmap wri V) wri fst h1) V).
red; ins; destruct (eqP e wri); subst.
2: by eapply valid_ext_sw; try eapply valid_ext_clearw2; eauto.
red; rewrite EQ; simpl; repeat (eexists; try edone); right.
split; try done; unfold NW.
eexists _,P0,sws; rewrite map_upd_sw_same3,K,hplus_emp_r; ins;
repeat (eexists; try edone).
by apply swsOK.
by rewrite eqxx; desf; apply/inP in Heq.
assert (IND: independent lab sb rf mo (hb_sw wri fst :: hb_sb prev fst :: nil)).
by apply independent_two; ins; eauto; intro; subst; eauto with hb.
eapply independent_heap_compat with (V:=V) in IND; try exact VAL';
eauto; ins; desf; desf.
2: by constructor; ins; intro; desf; desf.
rewrite hsum_two, pEQ, <- !hplusA in IND; ins.
exploit hplus_def_inv; try edone; intro M; desc; subst.
rewrite !hplusA in ×.
exploit (IMP2 (Hdef hy)); [by repeat (eexists; try edone)|].
simpl; intro ZZ; desf.
eapply safe_final4b
with (wri := wri) (h := h3 +!+ Hdef hz) (h' := h1); eauto.
repeat (eexists; try edone).
by intro AA; rewrite <- !hplusA in *;
rewrite M, <- ZZ0, !hplusA, AA, hplusC, hplusA, hplusAC in IND.
red; rewrite SEM1; simpl.
destruct (has_sw_succs rf fst FIN) as [swsOut ?]; desc.
∃ prev,next,(wri::nil),swsOut;
repeat (split; try intros [?|?]; subst; try done).
unfold ann_sw; ins; desc; left; congruence.
simpl; desf; desf.
rewrite !map_clearw_sws, !mupds, !mupdo; try solve [intro; desf].
simpl; rewrite !hsum_one; desf; desf.
unfold NW.
eexists _,_, (fun x ⇒ mk_assn_mod (QQ' x)),_,_,_; rewrite hplus_emp_l;
repeat (eexists; try edone); ins; eauto;
try (eby eapply sim_assn_sem; [apply Asim_sym, Asim_assn_norm|]).
eby rewrite hplusC, pEQ.
2: by rewrite NOT2.
eapply vshift_eqI; rewrite <- IND.
rewrite (hplusC (h3 +!+ _)), <- !hplusA.
f_equal.
by rewrite !hplusA, M, <- ZZ0, !hplusA.
}
{
assert (h1 = hemp).
unfold ann_sw in NSW; rewrite SEM1, EQ in NSW.
clear - TRAN Y0 NOT1 NSW RLX RF NA NA0; ins; desf;
solve [by destruct NSW | rewrite NOT1 in *; ins; auto 2 |
by rewrite RLX in *; ins; auto 2;
apply hplus_eq_emp, proj1 in TRAN].
subst; rewrite hplus_emp_l in ×.
exploit (IMP2).
by eexists hemp,_; rewrite hplus_emp_l; repeat (eexists; try edone).
simpl; intro ZZ; desf.
eapply safe_final3 with (h := h0 +!+ hFR) (exn := nil); eauto.
repeat (eexists; try edone).
by intro AA; rewrite <- !hplusA in *;
rewrite pEQ, <- ZZ0, !hplusA, AA, hplusC, hplusA, hplusAC in pDEF.
red; rewrite SEM1; simpl.
destruct (has_sw_succs rf fst FIN) as [swsOut ?]; desc.
∃ prev,next,nil,swsOut; repeat (split; try intros [?|?]; subst; try done).
by unfold ann_sw in *; ins; desf; destruct NSW.
simpl; desf; desf.
rewrite !mupds, !mupdo; try solve [intro; desf]; simpl.
rewrite !map_upd_irr, map_clearw_sws; ins.
rewrite !hsum_nil, hplus_emp_r.
unfold NW.
eexists _,_,(fun x ⇒ mk_assn_mod (QQ' x)),_,_,_; rewrite hplus_emp_l;
repeat (eexists; try edone); ins; eauto;
try (eby eapply sim_assn_sem; [apply Asim_sym, Asim_assn_norm|]).
2: by rewrite NOT2.
eapply vshift_eqI.
rewrite <- Z, pEQ, <- !hplusA, (hplusC _ h4), <- !hplusA; f_equal.
by rewrite hplusA in *; rewrite hplusAC, <- ZZ0.
}
}
{
assert (K: hsum (map (mclearw hmap wri V) (map (hb_sw wri) swsOut)) = hemp).
by eapply rmw_helper0, swsOutOK; eauto.
rewrite K, hplus_emp_l in ×.
assert (Y: ∃ h1 hsink', hsink = h1 +!+ hsink' ∧ assn_sem (QQ E') h1).
eapply rmw_helper2 with (V:=V); try exact UPD; try exact Z0; try exact pEQ0;
try exact Z; eauto.
by rewrite EQ.
desf.
red in CONS; desc.
destruct (classic (ann_sw lab rf wri fst)) as [SW|NSW].
{
destruct FST.
assert (VAL': hmap_valids lab sb rf (mupd_sw (mclearw hmap wri V) wri fst h1) V).
red; ins; destruct (eqP e wri); subst.
2: by eapply valid_ext_sw; try eapply valid_ext_clearw2; eauto.
red; rewrite EQ; simpl.
do 4 eexists; repeat (split; try edone); unfold NW.
eexists _, _,PP',_,_,hsink'.
rewrite map_upd_sw_same3,K,hplus_emp_r,map_upd_sw_irr; ins;
try solve[ intro; desf]; repeat (eexists; try edone); instantiate;
try rewrite swsOutOK in *; ins; try (by desf); eauto.
by rewrite eqxx; desf; apply/inP in Heq.
assert (IND: independent lab sb rf mo (hb_sw wri fst :: hb_sb prev fst :: nil)).
by apply independent_two; ins; eauto; intro; subst; eauto with hb.
eapply independent_heap_compat with (V:=V) in IND; try exact VAL';
eauto; ins; desf; desf.
2: by constructor; ins; intro; desf; desf.
rewrite hsum_two, pEQ, <- !hplusA in IND; ins.
exploit hplus_def_inv; try edone; intro M; desc; subst.
rewrite !hplusA in ×.
exploit (IMP2 (Hdef hy)); [by repeat (eexists; try edone)|].
simpl; intro ZZ; desf.
eapply safe_final4b
with (wri := wri) (h := h3 +!+ Hdef hz) (h' := h1); eauto.
repeat (eexists; try edone).
by intro AA; rewrite <- !hplusA in *;
rewrite M, <- ZZ0, !hplusA, AA, hplusC, hplusA, hplusAC in IND.
red; rewrite SEM1; simpl.
destruct (has_sw_succs rf fst FIN) as [swsOut' ?]; desc.
∃ prev,next,(wri::nil),swsOut';
repeat (split; try intros [?|?]; subst; try done).
unfold ann_sw; ins; desc; left; congruence.
simpl; desf; desf.
rewrite !map_clearw_sws, !mupds, !mupdo; try solve [intro; desf].
simpl; rewrite !hsum_one; desf; desf.
unfold NW.
eexists _,_,(fun x ⇒ mk_assn_mod (QQ' x)),_,_,_; rewrite hplus_emp_l;
repeat (eexists; try edone); ins; eauto;
try (eby eapply sim_assn_sem; [apply Asim_sym, Asim_assn_norm|]).
eby rewrite hplusC, pEQ.
2: by rewrite NOT2.
eapply vshift_eqI; rewrite <- IND.
rewrite (hplusC (h3 +!+ _)), <- !hplusA.
by f_equal; rewrite !hplusA, M, <- ZZ0, hplusA.
}
{
assert (h1 = hemp).
unfold ann_sw in NSW; rewrite SEM1, EQ in NSW.
clear - TRAN' Y0 NOT1 NSW RLX RF NA NA0; ins; desf;
solve [by destruct NSW | rewrite NOT1 in *; ins; auto 2 |
by rewrite RLX in *; ins; auto 2;
apply hplus_eq_emp, proj1 in TRAN'].
subst; rewrite hplus_emp_l in ×.
exploit (IMP2).
by eexists hemp,_; rewrite hplus_emp_l; repeat (eexists; try edone).
simpl; intro ZZ; desf.
eapply safe_final3 with (h := h0 +!+ hFR) (exn := nil); eauto.
repeat (eexists; try edone).
by intro AA; rewrite <- !hplusA in *;
rewrite pEQ, <- ZZ0, !hplusA, AA, hplusC, hplusA, hplusAC in pDEF.
red; rewrite SEM1; simpl.
destruct (has_sw_succs rf fst FIN) as [swsOut' ?]; desc.
∃ prev,next,nil,swsOut'; repeat (split; try intros [?|?]; subst; try done).
by unfold ann_sw in *; ins; desf; destruct NSW.
simpl; desf; desf.
rewrite !mupds, !mupdo; try solve [intro; desf]; simpl.
rewrite !map_upd_irr, map_clearw_sws; ins.
rewrite !hsum_nil, hplus_emp_r.
unfold NW.
eexists _,_,(fun x ⇒ mk_assn_mod (QQ' x)),_,_,_; rewrite hplus_emp_l;
repeat (eexists; try edone); ins; eauto;
try (eby eapply sim_assn_sem; [apply Asim_sym, Asim_assn_norm|]).
2: by rewrite NOT2.
eapply vshift_eqI.
rewrite <- Z, pEQ, <- !hplusA, (hplusC _ h4), <- !hplusA; f_equal.
by rewrite hplusA in *; rewrite hplusAC, <- ZZ0.
}
}
Qed.
This page has been generated by coqdoc Imprint | Data protection