Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps rslassn rslassnlemmas rslmodel rslhmap.
Set Implicit Arguments.
We develop the following helper lemma in order to simplify the proofs of
various RSL proof rules.
Lemma triple_helper_start mt P e QQ :
(∀ res acts_cmd lab sb fst lst
(SEM : exp_sem e res acts_cmd lab sb fst lst) a
(MT : mt = Model_standard_c11)
(IN : In a acts_cmd) (RW : is_rlx_write (lab a)), False) →
(∀ res acts_cmd lab sb fst lst
(SEM : exp_sem e res acts_cmd lab sb fst lst) acts_ctx rf mo sc
(CONS : weakConsistent (acts_cmd ++ acts_ctx) lab sb rf mo sc mt)
(UNIQ : NoDup (acts_cmd ++ acts_ctx))
prev (FST : unique (sb^~ fst) prev)
next (LST : unique (sb lst) next)
n V (V_PREV : In prev V)
(V_CTX : ∀ x : actid, In x V → In x acts_ctx)
(HC : hist_closed mt lab sb rf mo V)
hmap
(VALID : ∀ e, In e V → hmap_valid lab sb rf hmap e)
(pDEF : hmap (hb_sb prev fst) ≠ Hundef) hp hFR
(pEQ : hmap (hb_sb prev fst) = hp +!+ hFR)
(pSAT : assn_sem P hp)
(NIN : ¬ In fst V)
(HC : hist_closed mt lab sb rf mo (fst :: V))
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(NOREL : with_mt mt (no_rlx_writes_global lab) True),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (fst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (fst :: V) hmap' lst
(with_opt res
(fun res h ⇒ ∃ hq, h ≠ Hundef ∧ h = hq +!+ hFR
∧ assn_sem (QQ res) hq))) →
triple mt P e QQ.
Proof.
split; [|by ins; red; desf; red; eauto].
induction n; ins; unfold NW; repeat split; ins; desf.
× by exfalso; rewrite nodup_app in UNIQ; desf; eauto using exp_sem_lst.
× eapply IHn; eauto using In_cons; [by ins; desf; eauto| |];
destruct FST; rewrite (proj1 (HEQ _ V_PREV _)) in pDEF, pEQ; eauto.
× cut (a = fst).
by ins; eapply H0; ins; subst; eauto using exp_sem_lst_reach.
assert (M: In fst (a :: V)).
by eapply (hist_closed_trans HC'); eauto using exp_sem_fst_reach, In_eq.
ins; desf; apply V_CTX in M; ins.
by exfalso; rewrite !nodup_app in *; desf; eauto using exp_sem_fst.
Qed.
Configuration safety is invariant over Permutations of acts_cmd.
Lemma Permutation_safe1 :
∀ l l' (P : Permutation l l') mt acts lab sb rf mo n V hmap lst Q,
safe mt l acts lab sb rf mo n V hmap lst Q →
safe mt l' acts lab sb rf mo n V hmap lst Q.
Proof.
induction n; ins; desc; repeat split; unfold NW; ins; eauto.
edestruct GUAR; desc; eauto.
eby eapply Permutation_in; try eapply Permutation_sym.
Qed.
We now develop a number of lemmas for establishing configuration safety of
final configurations.
Definition mclearw h x (exn : list actid) := fun y ⇒
match y with
| hb_sw a b ⇒ if a == x then if b \in exn then h y else hemp else h y
| hb_sb _ _ ⇒ h y
end.
Definition mclears h x := fun y ⇒
match y with
| hb_sw _ _ ⇒ h y
| hb_sb a b ⇒ if a == x then hemp else h y
end.
Definition mupd_sw h x y z := fun t ⇒
match t with
| hb_sw a b ⇒ if b == y then if a == x then z else hemp else h t
| hb_sb _ _ ⇒ h t
end.
Lemma map_upd_irr (A: eqType) B C (hmap : A → B) x y f (l : list C) :
(∀ a, In a l → f a ≠ x) →
map (mupd hmap x y) (map f l) = map hmap (map f l).
Proof.
unfold mupd; induction l; ins; desf; f_equal; eauto.
exfalso; intuition eauto.
Qed.
Lemma map_clearw_irr A hmap x exn f (l : list A) :
(∀ a b, In a l → f a = hb_sw x b → In b exn) →
map (mclearw hmap x exn) (map f l) = map hmap (map f l).
Proof.
unfold mclearw; induction l; ins; desf; desf; f_equal; eauto.
apply/inP in Heq1.
exfalso; subst; intuition eauto.
Qed.
Lemma map_clears_irr A hmap x f (l : list A) :
(∀ a b, In a l → f a = hb_sb x b → False) →
map (mclears hmap x) (map f l) = map hmap (map f l).
Proof.
unfold mclears; induction l; ins; desf; desf; f_equal; eauto.
exfalso; subst; intuition eauto.
Qed.
Lemma map_upd_sw_irr C hmap x y z f (l : list C) :
(∀ a b, In a l → f a ≠ hb_sw b y) →
map (mupd_sw hmap x y z) (map f l) = map hmap (map f l).
Proof.
unfold mupd_sw; induction l; ins; desf; f_equal; subst; eauto;
exfalso; intuition eauto.
Qed.
Lemma map_upd_sw_same hmap a b h l :
NoDup l →
In a l →
hsum (map (mupd_sw hmap a b h) (map (hb_sw^~ b) l)) = h.
Proof.
induction l; ins; desf; desf; inv H; rewrite hsum_cons, ?hplus_emp_l; eauto.
rewrite <- (hplus_emp_r h) at 3; f_equal.
clear -H2; induction l; ins; desf; desf; rewrite hsum_cons, ?hplus_emp_l; eauto.
exfalso; eauto.
Qed.
Lemma map_upd_sw_same2 hmap a b h l :
NoDup l →
In b l →
hsum (map (mupd_sw hmap a b h) (map (hb_sw a) l)) =
h +!+ hsum (map (mupd hmap (hb_sw a b) hemp) (map (hb_sw a) l)).
Proof.
induction l; ins; desf; desf; inv H; rewrite !hsum_cons, ?hplus_emp_l; eauto.
rewrite map_upd_sw_irr, map_upd_irr; try red; ins; desf.
by unfold mupd; desf; desf; rewrite hplus_emp_l.
rewrite hplusAC; f_equal; eauto; unfold mupd; desf; desf.
Qed.
Lemma map_upd_sw_same3 hmap a b h l :
NoDup l →
In b l →
hmap (hb_sw a b) = hemp →
hsum (map (mupd_sw hmap a b h) (map (hb_sw a) l)) =
h +!+ hsum (map hmap (map (hb_sw a) l)).
Proof.
ins; rewrite map_upd_sw_same2; ins; f_equal.
clear H0; induction l; ins; rewrite !hsum_cons.
inv H; f_equal; auto; unfold mupd; desf; desf.
Qed.
Lemma map_clearw_sws :
∀ hmap x l, hsum (map (mclearw hmap x nil) (map (hb_sw x) l)) = hemp.
Proof.
induction l; ins; desf; desf.
by rewrite hsum_cons, hplus_emp_l.
Qed.
Lemma map_clears_edges :
∀ hmap x l, hsum (map (mclears hmap x) (map (hb_sb x) l)) = hemp.
Proof.
induction l; ins; desf; desf.
by rewrite hsum_cons, hplus_emp_l.
Qed.
Lemma valid_ext :
∀ mt lab sb rf mo hmap e V
(VAL : hmap_valid lab sb rf hmap e) (IN: In e V)
(HC : hist_closed mt lab sb rf mo V) a (NIN: ¬ In a V) b h,
hmap_valid lab sb rf (mupd hmap (hb_sb a b) h) e.
Proof.
unfold hmap_valid, unique; ins; desf; desf; unfold NW;
try by (repeat (eexists; try edone); unfold mupd; desf; desf; eauto 8;
try (by exfalso; eauto with hb);
right; repeat (eexists; try edone); unfold mupd; desf; desf;
eauto 8 using map_upd_irr;
f_equal; clear; induction sws; ins; desf; desf; congruence).
∃ pres, posts, hf, hsink; unfold NW; repeat (split; try done).
by rewrite map_upd_irr; ins; red; intros; desf; eapply pOK in H; eauto with hb.
eapply vshift_trans; eauto; rewrite map_upd_irr; ins;
auto using vshift_refl; intro; desf.
∃ pre, post, hf; repeat (split; try done).
unfold mupd; desf; desf; try (by exfalso; eauto with hb).
right; repeat (eexists; try edone); try rewrite map_upd_irr; eauto;
unfold mupd; desf; desf; try rewrite map_upd_irr; eauto 8;
try (by exfalso; eauto with hb).
∃ pre, post, hf; repeat (split; try done).
unfold mupd; desf; desf; try (by exfalso; eauto with hb).
right; repeat (eexists; try edone); try rewrite map_upd_irr; eauto;
unfold mupd; desf; desf; try rewrite map_upd_irr; eauto 8;
try (by exfalso; eauto with hb).
∃ pre, post, swsIn, swsOut; repeat (split; try done).
unfold mupd at 1 2 4; desf; desf; try (by exfalso; eauto with hb).
do 7 eexists; repeat (split; try edone); try rewrite map_upd_irr; eauto;
desf; desf; try (by exfalso; eauto with hb).
Qed.
Lemma valid_ext_sw_helper :
∀ hmap a b h e l hsink (NEQ: e ≠ a),
∃ hsink' : heap,
hsum (map (mupd_sw hmap a b h) (map (hb_sw e) l)) +!+ hsink' =
hsum (map hmap (map (hb_sw e) l)) +!+ hsink.
Proof.
intros; induction l; ins; vauto; rewrite !hsum_cons; desf; desf.
by eexists (hmap (hb_sw e b) +!+ hsink');
rewrite hplus_emp_l, hplusA, hplusAC; f_equal.
by ∃ hsink'; rewrite !hplusA; f_equal.
Qed.
Lemma valid_ext_sw :
∀ mt lab sb rf mo hmap e V
(VAL: hmap_valid lab sb rf hmap e) (IN: In e V)
(HC : hist_closed mt lab sb rf mo V) b
(NIN: ¬ In b V) a (NEQ': e ≠ a) h,
hmap_valid lab sb rf (mupd_sw hmap a b h) e.
Proof.
unfold hmap_valid; ins; desf; desf; unfold NW;
try solve [repeat (eexists; try edone); left;
repeat (eexists; try edone); ins; desf; eauto].
by ∃ pres, posts, hf, hsink; repeat (split; try done);
rewrite map_upd_sw_irr.
{
repeat (eexists; try edone).
right; repeat (eexists; try edone).
rewrite map_upd_sw_irr; ins; intro; desf.
}
{
repeat (eexists; try edone).
right; split; try done.
assert (X: ∃ hsink',
hsum (map (mupd_sw hmap a b h) (map (hb_sw e) sws)) +!+ hsink'
= hsum (map hmap (map (hb_sw e) sws)) +!+ hsink).
by eapply valid_ext_sw_helper.
desf; rewrite <- X in *; repeat (eexists; try edone).
}
{
assert (X: ∃ hsink',
hsum (map (mupd_sw hmap a b h) (map (hb_sw e) swsOut)) +!+ hsink'
= hsum (map hmap (map (hb_sw e) swsOut)) +!+ hsink).
by eapply valid_ext_sw_helper.
desf; rewrite <- X in ×.
repeat (eexists; try edone); instantiate; rewrite map_upd_sw_irr;
try edone; ins; intro; desf; desf.
}
Qed.
Lemma valid_ext_clearw :
∀ mt lab sb rf mo hmap e V
(VAL : hmap_valid lab sb rf hmap e)
(HC : hist_closed mt lab sb rf mo V) a (NIN: ¬ In a V) (IN: In e V) exn,
hmap_valid lab sb rf (mclearw hmap a exn) e.
Proof.
unfold hmap_valid; ins; desf; desf; unfold NW;
try solve [repeat (eexists; try edone); left;
repeat (eexists; try edone); ins; desf; eauto];
try (repeat (eexists; try edone); right;
repeat (eexists; try edone); ins; desf; eauto);
try apply/inP in Heq0.
by eexists pres, posts; repeat (split; try done);
rewrite !map_clearw_irr; ins; vauto.
by rewrite map_clearw_irr; ins; desf.
rewrite !map_clearw_irr; ins; desf.
by exfalso; desf; rewrite swsOK in *; eauto using hist_closedD with hb.
by rewrite !map_clearw_irr; ins; vauto.
by rewrite !map_clearw_irr; ins; desf.
∃ pre, post, swsIn, swsOut; repeat (split; try done).
do 6 eexists; repeat (split; try edone); rewrite map_clearw_irr; eauto;
ins; desf; desf; rewrite swsInOK in *; try (by destruct NIN; eauto with hb).
Qed.
Lemma valid_ext_clearw_helper :
∀ hmap a V e l hsink,
∃ hsink' : heap,
hsum (map (mclearw hmap a V) (map (hb_sw e) l)) +!+ hsink' =
hsum (map hmap (map (hb_sw e) l)) +!+ hsink.
Proof.
intros; induction l; ins; vauto; rewrite !hsum_cons; desf; desf.
by ∃ hsink'; rewrite !hplusA; f_equal.
by eexists (hmap (hb_sw a a0) +!+ hsink');
rewrite hplus_emp_l, hplusA, hplusAC; f_equal.
by ∃ hsink'; rewrite !hplusA; f_equal.
Qed.
Lemma valid_ext_clearw2 :
∀ mt lab sb rf mo hmap w e V
(ACYC: IrreflexiveHB lab sb rf mo)
(VAL : hmap_valid lab sb rf hmap e) (IN : In e V)
(HC : hist_closed mt lab sb rf mo V),
hmap_valid lab sb rf (mclearw hmap w V) e.
Proof.
unfold hmap_valid; ins; desf; desf; unfold NW; try apply/inP in Heq0; try done;
try solve [repeat (eexists; try edone); left;
repeat (eexists; try edone); unfold mupd; ins; desf; eauto].
{ ∃ pres, posts, hf; repeat (split; try done);
rewrite !map_clearw_irr; ins; vauto. }
{ repeat (eexists; try edone).
right; repeat (eexists; try edone); ins; desf.
rewrite map_clearw_irr; ins; desf. }
{ repeat (eexists; try edone).
right; split; try done.
assert (X: ∃ hsink',
hsum (map (mclearw hmap w V) (map (hb_sw w) sws)) +!+ hsink'
= hsum (map hmap (map (hb_sw w) sws)) +!+ hsink).
by apply valid_ext_clearw_helper.
desc; rewrite <- X in *; repeat (eexists; try edone).
}
{ repeat (eexists; try edone).
right; split; try done.
assert (X: ∃ hsink',
hsum (map (mclearw hmap w V) (map (hb_sw e) sws)) +!+ hsink'
= hsum (map hmap (map (hb_sw e) sws)) +!+ hsink).
by apply valid_ext_clearw_helper.
desc; rewrite <- X in *; repeat (eexists; try edone).
}
{ assert (X: ∃ hsink',
hsum (map (mclearw hmap w V) (map (hb_sw e) swsOut)) +!+ hsink'
= hsum (map hmap (map (hb_sw e) swsOut)) +!+ hsink).
by apply valid_ext_clearw_helper.
desc; rewrite <- X in *; repeat (eexists; try edone);
rewrite map_clearw_irr; ins; desf.
}
Qed.
Lemma valid_ext_clears :
∀ mt lab sb rf mo hmap e V
(VAL : hmap_valid lab sb rf hmap e)
(HC : hist_closed mt lab sb rf mo V) (IN: In e V) a (NIN: ¬ In a V),
hmap_valid lab sb rf (mclears hmap a) e.
Proof.
unfold hmap_valid, unique; ins; desf; desf; unfold NW;
try (by rewrite NEQ in *); desf;
try solve [repeat (eexists; try edone); desf; desf; try solve [exfalso; eauto with hb];
left; repeat (eexists; try edone); ins; desf; eauto];
try (repeat (eexists; try edone); desf; desf; try solve [exfalso; eauto with hb];
right; repeat (eexists; try edone); ins; desf; eauto).
eexists pres, posts,hf,hsink; repeat (split; try done);
rewrite !map_clears_irr; ins; desf; rewrite ?pOK in *; eauto with hb.
∃ pre, post, hf; repeat (eexists; try edone); desf; desf;
try solve [exfalso; eauto with hb].
left; repeat (eexists; try edone); ins; desf; eauto.
∃ pre, post, hf; repeat (eexists; try edone); desf; desf;
try solve [exfalso; eauto with hb].
right; repeat (eexists; try edone); ins; desf; eauto.
by rewrite map_clears_irr; ins; desf.
∃ pre, post, hf; repeat (eexists; try edone); desf; desf;
try solve [exfalso; eauto with hb].
left; repeat (eexists; try edone); ins; desf; eauto.
∃ pre, post, hf; repeat (eexists; try edone); desf; desf;
try solve [exfalso; eauto with hb].
right; repeat (eexists; try edone); ins; desf; eauto.
eby rewrite !map_clears_irr; ins; desf.
by rewrite !map_clears_irr; ins; desf.
∃ pre, post, swsIn, swsOut; repeat (split; try done).
desf; desf; try (by exfalso; eauto with hb).
do 7 eexists; repeat (split; try edone); rewrite ?map_clears_irr; eauto;
ins; desf; desf.
Qed.
Lemma safe_mod :
∀ mt acts_cmd acts_ctx lab sb rf mo n V hmap lst QQ
(H : safe mt acts_cmd acts_ctx lab sb rf mo n V hmap lst QQ)
acts_cmd' (E1: ∀ x (NIN: ¬ In x V) (IN: In x acts_cmd'), In x acts_cmd)
acts_ctx' (E2: ∀ x (NIN: ¬ In x V) (IN: In x acts_ctx'), In x acts_ctx),
safe mt acts_cmd' acts_ctx' lab sb rf mo n V hmap lst QQ.
Proof.
induction n; ins; desf; unfold NW; repeat (split; ins).
by eapply IHn; ins; desf; eauto; eapply RELY; eauto; eapply E2.
exploit GUAR; eauto; intro; desf.
∃ hmap'; intuition.
Qed.
Lemma safe_final1 :
∀ mt acts_cmd acts_ctx lab sb rf mo lst
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
V Q n hmap
(HC: hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap e)
(POST: ∀ next (SB: sb lst next), Q (hmap (hb_sb lst next)) : Prop),
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap lst Q.
Proof.
intros until n.
generalize (lst :: V), (In_eq lst V); clear -LR; induction n; ins.
unfold NW; intuition (desf; eauto).
by eapply IHn; eauto using In_cons; ins;
rewrite <- (proj1 (HEQ _ H next)); eauto.
by destruct NIN; generalize (LR _ INcmd), H, HC; clear;
induction 1; ins; eauto with hb.
Qed.
Lemma safe_final_plain :
∀ mt acts_cmd acts_ctx lab sb rf mo n V lst hmap Q next h
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed mt lab sb rf mo V)
(HC': hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(LST: unique (fun x ⇒ sb lst x) next)
(POST: Q h : Prop)
(VALID': hmap_valid lab sb rf (mupd hmap (hb_sb lst next) h) lst)
(NIN: ¬ In lst V),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap' lst Q.
Proof.
ins; ∃ (mupd hmap (hb_sb lst next) h).
assert (A: agrees lab sb rf V hmap (mupd hmap (hb_sb lst next) h)).
by split; unfold mupd; desf; desf.
assert (HV: hmap_valids lab sb rf (mupd hmap (hb_sb lst next) h) (lst :: V)).
by red; ins; desf; eapply valid_ext; eauto.
repeat (split; try done).
eapply safe_final1; ins; unfold mupd; desf; eauto.
eapply LST in SB; congruence.
Qed.
Lemma safe_final_plain2 :
∀ mt acts_cmd acts_ctx lab sb mo rf n V lst hmap Q next h
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed mt lab sb rf mo V)
(HC': hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(LST: unique (fun x ⇒ sb lst x) next)
(POST: Q h : Prop)
(VALID': hmap_valid lab sb rf (mupd (mupd_sw hmap lst lst hemp)
(hb_sb lst next) h) lst)
(NIN: ¬ In lst V),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap' lst Q.
Proof.
ins; pose (hmap' := (mupd (mupd_sw hmap lst lst hemp) (hb_sb lst next) h)).
ins; ∃ hmap'.
assert (A: agrees lab sb rf V hmap hmap').
by unfold hmap'; split; unfold mupd, mupd_sw; desf; desf.
assert (HV: hmap_valids lab sb rf hmap' (lst :: V)).
subst hmap'; red; ins; desf; eapply valid_ext; eauto.
by eapply valid_ext_sw; eauto; intro; desf.
repeat (split; try done).
eapply safe_final1; ins; unfold hmap', mupd; desf; eauto;
eapply LST in SB; congruence.
Qed.
Lemma safe_final3 :
∀ mt exn acts_cmd acts_ctx lab sb rf mo n V lst hmap Q next h
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed mt lab sb rf mo V)
(HC': hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(LST: unique (fun x ⇒ sb lst x) next)
(POST: Q h : Prop)
(VALID': hmap_valid lab sb rf (mupd (mclearw hmap lst exn) (hb_sb lst next) h) lst)
(NIN: ¬ In lst V),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap' lst Q.
Proof.
ins; ∃ (mupd (mclearw hmap lst exn) (hb_sb lst next) h).
assert (A: agrees lab sb rf V hmap
(mupd (mclearw hmap lst exn) (hb_sb lst next) h)).
split; unfold mupd, mclearw; desf; desf.
by intros; exfalso; eauto using hist_closedD with hb.
assert (HV: hmap_valids lab sb rf
(mupd (mclearw hmap lst exn) (hb_sb lst next) h)
(lst :: V)).
red; ins; desf; eapply valid_ext; eauto.
by eapply valid_ext_clearw, IN; eauto.
repeat (split; try done).
eapply safe_final1; ins; unfold mupd; desf; eauto.
eapply LST in SB; congruence.
Qed.
Lemma safe_final4a :
∀ mt acts_cmd acts_ctx lab sb rf mo n V lst hmap Q wri next h h'
(ACYC: IrreflexiveHB lab sb rf mo)
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed mt lab sb rf mo V)
(HC': hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(LST: unique (fun x ⇒ sb lst x) next)
(POST: Q h : Prop)
(VALID': hmap_valid lab sb rf (mupd (mupd_sw
(mclearw hmap wri V) wri lst h')
(hb_sb lst next) h) lst)
(VALID'': hmap_valid lab sb rf (mupd_sw (mclearw hmap wri V) wri lst h') wri)
(NIN: ¬ In lst V),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap' lst Q.
Proof.
ins; pose (hmap' := (mupd (mupd_sw (mclearw hmap wri V) wri lst h') (hb_sb lst next) h)).
ins; ∃ hmap'.
assert (A: agrees lab sb rf V hmap hmap').
unfold hmap'; split; unfold mupd, mclearw, mupd_sw; desf; desf.
by apply/inP in Heq2.
assert (HV: hmap_valids lab sb rf hmap' (lst :: V)).
subst hmap'; red; ins; desf; eapply valid_ext; eauto.
destruct (eqP e wri); desf; eapply valid_ext_sw; eauto.
by eapply valid_ext_clearw2; eauto.
repeat (split; try done).
eapply safe_final1; ins; unfold hmap', mupd; desf; eauto;
eapply LST in SB; congruence.
Qed.
Lemma safe_final4b :
∀ mt acts_cmd acts_ctx lab sb rf mo n V lst hmap Q wri next h h'
(ACYC: IrreflexiveHB lab sb rf mo)
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed mt lab sb rf mo V)
(HC': hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(LST: unique (fun x ⇒ sb lst x) next)
(POST: Q h : Prop)
(VALID': hmap_valid lab sb rf (mclearw (mupd (mupd_sw
(mclearw hmap wri V) wri lst h')
(hb_sb lst next) h) lst nil) lst)
(VALID'': hmap_valid lab sb rf (mupd_sw (mclearw hmap wri V) wri lst h') wri)
(NIN: ¬ In lst V),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap' lst Q.
Proof.
ins; pose (hmap' := (mclearw (mupd (mupd_sw (mclearw hmap wri V) wri lst h') (hb_sb lst next) h) lst nil)).
ins; ∃ hmap'.
assert (A: agrees lab sb rf V hmap hmap').
unfold hmap'; split; unfold mupd, mclearw, mupd_sw; desf; desf.
by intro; exfalso; eauto with hb.
by apply/inP in Heq3.
assert (HV: hmap_valids lab sb rf hmap' (lst :: V)).
subst hmap'; red; ins; desf.
eapply valid_ext_clearw with (V:=V); eauto.
eapply valid_ext; eauto.
destruct (eqP e wri); desf; eapply valid_ext_sw; eauto.
by eapply valid_ext_clearw2; eauto.
repeat (split; try done).
eapply safe_final1; ins; unfold hmap', mupd; desf; eauto;
eapply LST in SB; congruence.
Qed.
Lemma safe_final4 :
∀ mt acts_cmd acts_ctx lab sb rf mo n V lst hmap Q wri next h h'
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed mt lab sb rf mo V)
(HC': hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(LST: unique (fun x ⇒ sb lst x) next)
(POST: Q h : Prop)
(VALID': hmap_valid lab sb rf (mupd (mupd_sw hmap wri lst h')
(hb_sb lst next) h) lst)
(VALID': hmap_valid lab sb rf (mupd_sw hmap wri lst h') wri)
(NIN: ¬ In lst V),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap' lst Q.
Proof.
ins; pose (hmap' := (mupd (mupd_sw hmap wri lst h') (hb_sb lst next) h)).
ins; ∃ hmap'.
assert (A: agrees lab sb rf V hmap hmap').
by unfold hmap'; split; unfold mupd, mupd_sw; desf; desf.
assert (HV: hmap_valids lab sb rf hmap' (lst :: V)).
subst hmap'; red; ins; desf; eapply valid_ext; eauto.
by destruct (eqP e wri); desf; eapply valid_ext_sw; eauto.
repeat (split; try done).
eapply safe_final1; ins; unfold hmap', mupd; desf; eauto;
eapply LST in SB; congruence.
Qed.
Lemma safe_final5 :
∀ mt acts_cmd acts_ctx lab sb mo rf n V lst hmap Q next h
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed mt lab sb rf mo V)
(HC': hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(LST: unique (fun x ⇒ sb lst x) next)
(POST: Q h : Prop)
(VALID': hmap_valid lab sb rf (mupd (mupd_sw hmap lst lst hemp)
(hb_sb lst next) h) lst)
(NIN: ¬ In lst V),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap' lst Q.
Proof.
ins; pose (hmap' := (mupd (mupd_sw hmap lst lst hemp) (hb_sb lst next) h)).
ins; ∃ hmap'.
assert (A: agrees lab sb rf V hmap hmap').
by unfold hmap'; split; unfold mupd, mupd_sw; desf; desf.
assert (HV: hmap_valids lab sb rf hmap' (lst :: V)).
subst hmap'; red; ins; desf; eapply valid_ext; eauto.
by eapply valid_ext_sw; eauto; intro; desf.
repeat (split; try done).
eapply safe_final1; ins; unfold hmap', mupd; desf; eauto;
eapply LST in SB; congruence.
Qed.
Lemma has_sb_succs acts lab sb a :
ExecutionFinite acts lab sb →
∃ posts,
<< qND: NoDup posts >> ∧
<< qIN: ∀ x, In x posts ↔ sb a x >>.
Proof.
∃ (undup (filter (fun x ⇒ mydec (sb a x)) acts)).
unfold NW; split; [by apply/uniqP; apply undup_uniq|].
intros; rewrite (In_mem_eq (mem_undup (T:=nat_eqType) _)), In_filter.
unfold mydec; desf; split; ins; desf; eauto.
split; try done; eapply H in H0; desf.
Qed.
Lemma safe_nt :
∀ mt acts_cmd acts_ctx lab sb mo rf n V lst hmap
(FIN: ExecutionFinite (acts_cmd ++ acts_ctx) lab sb)
(IRR: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed mt lab sb rf mo V)
(HC': hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(LAB: lab lst = Askip)
(NIN: ¬ In lst V),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap' lst (fun _ ⇒ True).
Proof.
ins; pose (hmap' := mclears hmap lst).
ins; ∃ hmap'.
assert (A: agrees lab sb rf V hmap hmap').
by unfold hmap'; split; unfold mclears; desf; desf.
cut (hmap_valids lab sb rf hmap' (lst :: V)).
by intro; repeat (split; try done); apply safe_final1.
subst hmap'; red; ins; desf; eauto using valid_ext_clears.
red; rewrite LAB.
assert (X:= get_pres_aux _ HC' (In_eq _ _)); desf.
assert (X:= has_sb_succs e FIN); desf.
assert (IND: independent lab sb rf mo (map (hb_sb^~e) pres_sb)).
by red; ins; rewrite In_map in *; desc; clarify; ins;
rewrite Pb in *; desf; eauto with hb.
specialize (HC' _ (In_eq _ _)).
eapply independent_heap_compat with (V:=V) in IND; eauto;
try (by ins; rewrite In_map in *; desf; rewrite ?Pb in *; ins).
desf; ∃ pres_sb, posts, h, (Hdef h).
rewrite map_clears_edges, hplus_emp_l, map_clears_irr; ins; desf;
rewrite ?Pb in *; eauto with hb.
by repeat (split; try done); apply vshift_refl.
by eapply nodup_map; ins; intro; desf.
ins; rewrite In_map in *; desf; rewrite Pb in ×.
destruct (HC' _ (hc_edge_sb _ _ _ _ _ _ _ IN0)); desf.
exfalso; eauto with hb.
Qed.
This page has been generated by coqdoc Imprint | Data protection