Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps fslassn fslassnlemmas fslmodel fslhmap.
Set Implicit Arguments.
We develop the following helper lemma in order to simplify the proofs of
various RSL proof rules.
Lemma triple_helper_start P e QQ :
(∀ 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 Model_hb_rf_acyclic)
(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 sb rf V)
hmap
(VALID : hmap_valids_strong lab sb rf hmap V)
(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 sb rf (fst :: V))
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst),
∃ hmap´,
agrees sb rf V hmap hmap´ ∧
(hmap_valids_strong lab sb rf hmap´ (fst :: V)) ∧
safe acts_cmd acts_ctx lab sb rf n (fst :: V) hmap´ lst
(with_opt res
(fun res h ⇒ ∃ hFR´ hq, h ≠ Hundef ∧ h = hq +!+ hFR +!+ hFR´
∧ assn_sem (QQ res) hq))) →
triple P e QQ.
Proof.
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).
{
ins; subst; eapply H; 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´) acts lab sb rf n V hmap lst Q,
safe l acts lab sb rf n V hmap lst Q →
safe l´ acts lab sb rf 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.
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 valid_ext :
∀ lab sb rf hmap e V
(VAL : hmap_valid lab sb rf hmap e) (IN: In e V)
(HC : hist_closed sb rf 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; desc;
try (destruct DISJ; desc); try revert TYP; 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).
{
∃ pres, posts, hf; repeat (split; try done).
by rewrite map_upd_irr; ins; red; intros; desf; eapply pOK in H; eauto with hb.
rewrite map_upd_irr; ins.
intro; desf.
}
{
ins.
∃ pre, post, hf; repeat (split; try done).
by clear TYP; unfold mupd; desf; desf; exfalso; eauto with hb.
right; split; eauto.
∃ rfs, hr, hF, P; repeat (split; try done);
try (∃ h´; repeat (split; try done));
solve [by rewrite map_upd_irr | clear TYP; unfold mupd; desf; desf].
}
{
ins.
∃ pre, post, hf; repeat (split; try done).
by clear TYP; unfold mupd; desf; desf; exfalso; eauto with hb.
right; split; try done.
∃ rfs, hr, hF, P; repeat (split; try done);
try (∃ h´; repeat (split; try done));
solve [by rewrite map_upd_irr | clear TYP; unfold mupd; desf; desf].
}
{
∃ pre, post; repeat (split; try done).
by unfold mupd; desf; desf; exfalso; eauto with hb.
∃ hF, hrel, hrel´, hacq, hacq´; repeat (split; try done);
by unfold mupd; desf; desf; exfalso; eauto with hb.
}
Qed.
Lemma valid_ext_sink :
∀ lab sb rf hmap e V
(VAL : hmap_valid lab sb rf hmap e) (IN: In e V)
(HC : hist_closed sb rf V) a (NIN: ¬ In a V) h,
hmap_valid lab sb rf (mupd hmap (hb_sink a) h) e.
Proof.
ins.
assert (EQ: mupd hmap (hb_sink a) h (hb_sink e) = hmap (hb_sink e)) by (unfold mupd; desf; desf).
unfold hmap_valid, unique in *; ins; desf; desc;
try (destruct DISJ; desc); try revert TYP; 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).
{
∃ pres, posts, hf; repeat (split; try done).
by rewrite map_upd_irr; ins; red; intros; desf; eapply pOK in H; eauto with hb.
rewrite map_upd_irr; ins; congruence.
}
{
ins.
∃ pre, post, hf; repeat (split; try done).
right; split; eauto.
∃ rfs, hr, hF, P; repeat (split; try done); try (∃ h´; repeat (split; try done));
try (by rewrite map_upd_irr); clear TYP; unfold mupd; desf; desf.
}
{
ins.
∃ pre, post, hf; repeat (split; try done).
right; split; try done.
by ∃ rfs, hr, hF, P; repeat (split; try done); try (∃ h´; repeat (split; try done));
rewrite map_upd_irr, EQ.
}
Qed.
Lemma hmap_irr_change_valid:
∀ lab sb rf hmap hmap´ e
(VALID: hmap_valid lab sb rf hmap e)
(IRR: ∀ edge, hb_fst edge = e ∨ hb_snd edge = Some e → hmap´ edge = hmap edge),
hmap_valid lab sb rf hmap´ e.
Proof.
ins; red; desf; red in VALID; rewrite Heq in VALID; desc.
{
∃ pres, posts, hf; unfold NW; repeat (split; try done).
× rewrite <- pEQ; f_equal.
apply map_eq; ins.
rewrite In_map in IN; desf.
apply IRR; eauto.
× rewrite qEQ; f_equal.
2: by symmetry; apply IRR; eauto.
f_equal.
apply map_eq; ins.
rewrite In_map in IN; desf.
symmetry; apply IRR; eauto.
}
{
∃ pre, post, hf; unfold NW; repeat (split; try done).
by rewrite <- pEQ; apply IRR; eauto.
desf; [left | right; ∃ QQ, isrmw]; rewrite <- qEQ; apply IRR; eauto.
}
{
assert (OK: hmap´ (hb_sb pre e) = hmap (hb_sb pre e) ∧ hmap´ (hb_sb e post) = hmap (hb_sb e post)).
by split; apply IRR; eauto.
desc.
∃ pre, post, hf; unfold NW; repeat (split; try done); try congruence.
destruct DISJ; desc.
{
left; repeat split; try done; try congruence.
by ins; erewrite <- ?rEQ; apply IRR; eauto.
by ins; erewrite <- ?sEQ; apply IRR; eauto.
}
{
assert(rOK: hsum (map hmap´ (map (hb_rf^~ e) rfs)) = hsum (map hmap (map (hb_rf^~ e) rfs))).
by clear TYP; f_equal; apply map_eq; ins; apply In_map in IN; desf; apply IRR; eauto.
right; repeat split; try done; try congruence.
∃ rfs, hr, hF, P; repeat (split; try done); try congruence; rewrite ?rOK; ins; desc; try done.
eby eexists; repeat split.
by ins; rewrite <- ?sEQ; apply IRR; eauto.
}
}
{
assert (OK: hmap´ (hb_sb pre e) = hmap (hb_sb pre e) ∧ hmap´ (hb_sb e post) = hmap (hb_sb e post)).
by split; apply IRR; eauto.
desc.
∃ pre, post, hf; unfold NW; repeat (split; try done); try congruence.
destruct DISJ; desc.
{
left; repeat split; try done; try congruence.
by ins; erewrite <- ?rEQ; apply IRR; eauto.
by ins; erewrite <- ?sEQ; apply IRR; eauto.
}
{
assert (rOK: hsum (map hmap´ (map (hb_rf e) rfs)) = hsum (map hmap (map (hb_rf e) rfs))).
by clear TYP; f_equal; apply map_eq; ins; apply In_map in IN; desf; apply IRR; eauto.
assert (sOK: hmap´ (hb_sink e) = hmap (hb_sink e)) by (apply IRR; eauto).
right; repeat split; try done; try congruence.
∃ rfs, hr, hF, P; repeat (split; try done); try congruence; rewrite ?rOK, ?sOK; ins; desc; try done.
eby eexists; repeat split.
}
}
{
done.
}
{
assert (OK: hmap´ (hb_sb pre e) = hmap (hb_sb pre e) ∧ hmap´ (hb_sb e post) = hmap (hb_sb e post)).
by split; apply IRR; eauto.
desc.
∃ pre, post; unfold NW; repeat (split; try done); try congruence.
∃ hF, hrel, hrel´, hacq, hacq´; repeat (split; try done); congruence.
}
Qed.
Lemma safe_mod :
∀ acts_cmd acts_ctx lab sb rf n V hmap lst QQ
(H : safe acts_cmd acts_ctx lab sb rf 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 acts_cmd´ acts_ctx´ lab sb rf 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 :
∀ acts_cmd acts_ctx lab sb rf lst
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
V Q n hmap
(HC: hist_closed sb rf (lst :: V))
(VALID: hmap_valids_strong lab sb rf hmap (lst :: V))
(POST: ∀ next (SB: sb lst next), Q (hmap (hb_sb lst next)) : Prop),
safe acts_cmd acts_ctx lab sb rf 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 :
∀ acts_cmd acts_ctx lab sb 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 sb rf V)
(HC´: hist_closed sb rf (lst :: V))
(VALID: hmap_valids_strong lab sb rf hmap V)
(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 sb rf V hmap hmap´ ∧
hmap_valids_strong lab sb rf hmap´ (lst :: V) ∧
safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap´ lst Q.
Proof.
ins; ∃ (mupd hmap (hb_sb lst next) h).
assert (A: agrees sb rf V hmap (mupd hmap (hb_sb lst next) h)).
by split; unfold mupd; desf; desf.
assert (HV: hmap_valids_strong lab sb rf (mupd hmap (hb_sb lst next) h) (lst :: V)).
{
split.
by unnw; red; ins; desf; eapply valid_ext; eauto; apply (proj1 VALID).
unnw; ins.
apply not_or_and in NIN0; unfold mupd; desf; desf.
× eapply (proj2 VALID); eauto.
× ins; desf; destruct H0; red; ins; eauto.
× eapply (proj2 VALID); eauto.
right; split; try done.
intro SB; destruct H0; clear - SB.
red in SB; split; desf; find_in_list.
}
repeat (split; try done).
eapply safe_final1; ins; unfold mupd; desf; eauto.
eapply LST in SB; congruence.
Qed.
Lemma safe_final_plain2 :
∀ acts_cmd acts_ctx lab sb 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 sb rf V)
(HC´: hist_closed sb rf (lst :: V))
(VALID: hmap_valids_strong lab sb rf hmap V)
(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 sb rf V hmap hmap´ ∧
hmap_valids_strong lab sb rf hmap´ (lst :: V) ∧
safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap´ lst Q.
Proof.
ins; pose (hmap´ := (mupd hmap (hb_sb lst next) h)).
ins; ∃ hmap´.
assert (A: agrees sb rf V hmap hmap´).
by unfold hmap´; split; unfold mupd; desf; desf.
assert (HV: hmap_valids_strong lab sb rf hmap´ (lst :: V)).
{
split; subst hmap´.
by unnw; red; ins; desf; eapply valid_ext; eauto; apply (proj1 VALID).
unnw; unfold mupd; desf; ins; desf; desf; ins.
× by destruct NIN0; eauto.
× eapply (proj2 VALID (hb_fst edge)); eauto.
× desf; destruct H0; vauto.
× eapply (proj2 VALID e); eauto.
right; split; eauto.
intro; destruct H0; unfold is_sb_out in *; desf; vauto.
}
repeat (split; try done).
eapply safe_final1; ins; unfold hmap´, mupd; desf; eauto;
eapply LST in SB; congruence.
Qed.
Lemma safe_final3 :
∀ acts_cmd acts_ctx lab sb 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 sb rf V)
(HC´: hist_closed sb rf (lst :: V))
(VALID: hmap_valids_strong lab sb rf hmap V)
(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 sb rf V hmap hmap´ ∧
hmap_valids_strong lab sb rf hmap´ (lst :: V) ∧
safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap´ lst Q.
Proof.
ins; ∃ (mupd hmap (hb_sb lst next) h).
assert (A: agrees sb rf V hmap (mupd hmap (hb_sb lst next) h)).
by split; unfold mupd; desf; desf.
assert (HV: hmap_valids_strong lab sb rf (mupd hmap (hb_sb lst next) h) (lst :: V)).
{
split; unnw; try red; ins.
× desf; eapply valid_ext; eauto.
by apply (proj1 VALID).
× unfold mupd; des_if.
+ subst; simpls; desf.
by destruct NIN0; eauto.
by destruct H0.
+ apply (proj2 VALID e).
by intro; destruct NIN0; eauto.
desf; eauto.
right; split; eauto.
intro SB; destruct H0.
unfold is_sb_out in *; split; desf; vauto.
}
repeat (split; try done).
eapply safe_final1; ins; unfold mupd; desf; eauto.
eapply LST in SB; congruence.
Qed.
Lemma safe_final3s :
∀ acts_cmd acts_ctx lab sb rf n V lst hmap Q next h hs
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed sb rf V)
(HC´: hist_closed sb rf (lst :: V))
(VALID: hmap_valids_strong lab sb rf hmap V)
(LST: unique (fun x ⇒ sb lst x) next)
(POST: Q h : Prop)
(VALID´: hmap_valid lab sb rf (mupd (mupd hmap (hb_sb lst next) h) (hb_sink lst) hs) lst)
(NIN: ¬ In lst V),
∃ hmap´,
agrees sb rf V hmap hmap´ ∧
hmap_valids_strong lab sb rf hmap´ (lst :: V) ∧
safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap´ lst Q.
Proof.
ins; pose (hmap´ := mupd (mupd hmap (hb_sb lst next) h) (hb_sink lst) hs).
∃ hmap´.
assert (A: agrees sb rf V hmap hmap´).
by subst hmap´; split; unfold mupd; desf; desf.
assert (HV: hmap_valids_strong lab sb rf hmap´ (lst :: V)).
{
subst hmap´; split; unnw; try red; ins.
× desf; eapply valid_ext_sink; eauto.
eapply valid_ext; eauto.
by apply (proj1 VALID).
× unfold mupd; des_if.
+ subst; simpls; desf.
by destruct NIN0; eauto.
+ desf.
by destruct NIN0; eauto.
by destruct H0.
+ apply (proj2 VALID e).
by intro; destruct NIN0; eauto.
desf; eauto.
right; split; eauto.
intro SB; destruct H0.
unfold is_sb_out in *; split; desf; vauto.
}
repeat (split; try done).
eapply safe_final1; ins; unfold mupd; desf; eauto.
subst hmap´; eapply LST in SB; unfold mupd; desf; desf.
Qed.
Lemma safe_final4a :
∀ acts_cmd acts_ctx lab sb rf n V lst hmap Q wri next hr hsinkw h hs
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed sb rf V)
(HC´: hist_closed sb rf (lst :: V))
(VALID: hmap_valids_strong lab sb rf hmap V)
(LST: unique (fun x ⇒ sb lst x) next)
(RF: rf lst = Some wri)
(POST: Q h : Prop)
(VALID´: hmap_valid lab sb rf (mupd
(mupd
(mupd
(mupd
hmap
(hb_rf wri lst) hr)
(hb_sink wri) hsinkw)
(hb_sb lst next) h)
(hb_sink lst) hs)
lst)
(VALID´´: hmap_valid lab sb rf (mupd (mupd hmap (hb_rf wri lst) hr) (hb_sink wri) hsinkw) wri)
(NIN: ¬ In lst V),
∃ hmap´,
agrees sb rf V hmap hmap´ ∧
hmap_valids_strong lab sb rf hmap´ (lst :: V) ∧
safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap´ lst Q.
Proof.
ins; pose (hmap´ := mupd
(mupd
(mupd
(mupd
hmap
(hb_rf wri lst) hr)
(hb_sink wri) hsinkw)
(hb_sb lst next) h)
(hb_sink lst) hs).
∃ hmap´.
assert (A: agrees sb rf V hmap hmap´).
by subst hmap´; split; unfold mupd; desf; desf.
assert (HV: hmap_valids_strong lab sb rf hmap´ (lst :: V)).
{
subst hmap´; split; unnw; try red; ins.
× desf; eapply valid_ext_sink; eauto.
eapply valid_ext; eauto.
destruct (classic (e = wri)) as [EQ|NEQ]; desf.
apply hmap_irr_change_valid with (hmap := hmap).
by apply VALID.
destruct edge; unfold mupd; desf; desf; ins; desf.
× unfold mupd; des_if.
+ subst; simpls; desf.
by destruct NIN0; eauto.
+ subst; ins; desf.
by destruct NIN0; eauto.
by destruct H0; red; ins; eauto.
+ subst; ins; desf.
destruct NIN0.
apply (HC´ lst); vauto.
+ subst; ins; desf.
- destruct NIN0.
apply (HC´ lst); vauto.
- destruct NIN0; eauto.
+ apply (proj2 VALID e).
by intro; destruct NIN0; eauto.
desf; eauto.
right; split; eauto.
intro SB; destruct H0.
unfold is_sb_out in *; split; desf; vauto.
}
repeat (split; try done).
eapply safe_final1; ins; unfold hmap´, mupd; desf; eauto;
eapply LST in SB; congruence.
Qed.
This page has been generated by coqdoc