Commit d1d67a37 by Ralf Jung

### turn CAS into compare-and-swap instead of compare-and-set: make it return the old value

parent 4a85888c
 ... ... @@ -15,7 +15,7 @@ Section tests. vals_cas_compare_safe v1 v1 → {{{ proph p vs ∗ ▷ l ↦ v1 }}} CAS_resolve #l v1 v2 #p v @ s; E {{{ RET #true ; ∃ vs', ⌜vs = (#true, v)::vs'⌝ ∗ proph p vs' ∗ l ↦ v2 }}}. {{{ RET v1 ; ∃ vs', ⌜vs = (v1, v)::vs'⌝ ∗ proph p vs' ∗ l ↦ v2 }}}. Proof. iIntros (Hcmp Φ) "[Hp Hl] HΦ". wp_apply (wp_resolve with "Hp"); first done. ... ... @@ -28,7 +28,7 @@ Section tests. val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 → {{{ proph p vs ∗ ▷ l ↦ v' }}} CAS_resolve #l v1 v2 #p v @ s; E {{{ RET #false ; ∃ vs', ⌜vs = (#false, v)::vs'⌝ ∗ proph p vs' ∗ l ↦ v' }}}. {{{ RET v' ; ∃ vs', ⌜vs = (v', v)::vs'⌝ ∗ proph p vs' ∗ l ↦ v' }}}. Proof. iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ". wp_apply (wp_resolve with "Hp"); first done. ... ... @@ -39,7 +39,7 @@ Section tests. Lemma test_resolve1 E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) : l ↦ #n -∗ proph p vs -∗ WP Resolve (CAS #l #n (#n + #1)) #p v @ E {{ v, ⌜v = #true⌝ ∗ ∃vs, proph p vs ∗ l ↦ #(n+1) }}%I. WP Resolve (CAS #l #n (#n + #1)) #p v @ E {{ v, ⌜v = #n⌝ ∗ ∃vs, proph p vs ∗ l ↦ #(n+1) }}%I. Proof. iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done. wp_cas_suc. iIntros (ws ->) "Hp". eauto with iFrame. ... ...
 ... ... @@ -121,7 +121,7 @@ Definition newcounter : val := λ: <>, ref #0. Definition incr : val := rec: "incr" "l" := let: "n" := !"l" in if: CAS "l" "n" (#1 + "n") then #() else "incr" "l". if: CAS "l" "n" (#1 + "n") = "n" then #() else "incr" "l". Definition read : val := λ: "l", !"l". (** The CMRA we need. *) ... ... @@ -231,10 +231,11 @@ Section counter_proof. rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]". wp_cas_suc. iSplitL "Hl Hγ". { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. } wp_if. rewrite {3}/C; eauto 10. - wp_cas_fail; first (intros [=]; abstract omega). wp_op. rewrite bool_decide_true //. wp_if. rewrite {3}/C; eauto 10. - assert (#c ≠ #c') by (intros [=]; abstract omega). wp_cas_fail. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|]. wp_if. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10. wp_op. rewrite bool_decide_false //. wp_if. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10. Qed. Check "read_spec". ... ...
 ... ... @@ -9,7 +9,7 @@ Set Default Proof Using "Type". Definition one_shot_example : val := λ: <>, let: "x" := ref NONE in ( (* tryset *) (λ: "n", CAS "x" NONE (SOME "n")), CAS "x" NONE (SOME "n") = NONE), (* check *) (λ: <>, let: "y" := !"x" in λ: <>, match: "y" with ... ... @@ -49,13 +49,15 @@ Proof. iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN". { iNext. iLeft. by iSplitL "Hl". } wp_pures. iModIntro. iApply "Hf"; iSplit. - iIntros (n) "!#". wp_lam. wp_pures. - iIntros (n) "!#". wp_lam. wp_pures. wp_bind (CAS _ _ _). iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]". + iMod (own_update with "Hγ") as "Hγ". { by apply cmra_update_exclusive with (y:=Shot n). } wp_cas_suc. iSplitL; last eauto. iModIntro. iNext; iRight; iExists n; by iFrame. + wp_cas_fail. iSplitL; last eauto. wp_cas_suc. iSplitL; iModIntro; last first. { wp_pures. eauto. } iNext; iRight; iExists n; by iFrame. + wp_cas_fail. iSplitL; iModIntro; last first. { wp_pures. eauto. } rewrite /one_shot_inv; eauto 10. - iIntros "!# /=". wp_lam. wp_bind (! _)%E. iInv N as ">Hγ". ... ...
 ... ... @@ -97,8 +97,8 @@ Inductive expr := | AllocN (e1 e2 : expr) (* array length (positive number), initial value *) | Load (e : expr) | Store (e1 : expr) (e2 : expr) | CAS (e0 : expr) (e1 : expr) (e2 : expr) | FAA (e1 : expr) (e2 : expr) | CAS (e0 : expr) (e1 : expr) (e2 : expr) (* Compare-and-swap (NOT compare-and-set!) *) | FAA (e1 : expr) (e2 : expr) (* Fetch-and-add *) (* Prophecy *) | NewProph | Resolve (e0 : expr) (e1 : expr) (e2 : expr) (* wrapped expr, proph, val *) ... ... @@ -518,6 +518,7 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit := Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val := if decide (op = EqOp) then (* Crucially, this compares the same way as [CAS]! *) Some \$ LitV \$ LitBool \$ bool_decide (val_for_compare v1 = val_for_compare v2) else match v1, v2 with ... ... @@ -633,19 +634,13 @@ Inductive head_step : expr → state → list observation → expr → state → [] (Val \$ LitV LitUnit) (state_upd_heap <[l:=v]> σ) [] | CasFailS l v1 v2 vl σ : | CasS l v1 v2 vl σ : vals_cas_compare_safe vl v1 → σ.(heap) !! l = Some vl → val_for_compare vl ≠ val_for_compare v1 → head_step (CAS (Val \$ LitV \$ LitLoc l) (Val v1) (Val v2)) σ [] (Val \$ LitV \$ LitBool false) σ [] | CasSucS l v1 v2 vl σ : vals_cas_compare_safe vl v1 → σ.(heap) !! l = Some vl → val_for_compare vl = val_for_compare v1 → head_step (CAS (Val \$ LitV \$ LitLoc l) (Val v1) (Val v2)) σ [] (Val \$ LitV \$ LitBool true) (state_upd_heap <[l:=v2]> σ) (* Crucially, this compares the same way as [EqOp]! *) (Val vl) (if decide (val_for_compare vl = val_for_compare v1) then state_upd_heap <[l:=v2]> σ else σ) [] | FaaS l i1 i2 σ : σ.(heap) !! l = Some (LitV (LitInt i1)) → ... ...
 ... ... @@ -36,7 +36,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap { val_is_unboxed w1 → <<< ∀ v, mapsto l 1 v >>> cas #l w1 w2 @ ⊤ <<< if decide (val_for_compare v = val_for_compare w1) then mapsto l 1 w2 else mapsto l 1 v, RET #(if decide (val_for_compare v = val_for_compare w1) then true else false) >>>; RET v >>>; }. Arguments atomic_heap _ {_}. ... ... @@ -100,7 +100,7 @@ Section proof. <<< ∀ (v : val), l ↦ v >>> primitive_cas #l w1 w2 @ ⊤ <<< if decide (val_for_compare v = val_for_compare w1) then l ↦ w2 else l ↦ v, RET #(if decide (val_for_compare v = val_for_compare w1) then true else false) >>>. RET v >>>. Proof. iIntros (? Φ) "AU". wp_lam. wp_let. wp_let. iMod "AU" as (v) "[H↦ [_ Hclose]]". ... ...
 ... ... @@ -9,7 +9,7 @@ Set Default Proof Using "Type". Definition newcounter : val := λ: <>, ref #0. Definition incr : val := rec: "incr" "l" := let: "n" := !"l" in if: CAS "l" "n" (#1 + "n") then #() else "incr" "l". if: CAS "l" "n" (#1 + "n") = "n" then #() else "incr" "l". Definition read : val := λ: "l", !"l". (** Monotone counter *) ... ... @@ -59,13 +59,16 @@ Section mono_proof. { apply auth_update, (mnat_local_update _ _ (S c)); auto. } wp_cas_suc. iModIntro. iSplitL "Hl Hγ". { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. } wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto. wp_op. rewrite bool_decide_true //. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto. iApply (own_mono with "Hγf"). (* FIXME: FIXME(Coq #6294): needs new unification *) apply: auth_frag_mono. by apply mnat_included, le_n_S. - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro. - assert (#c ≠ #c') by by intros [= ?%Nat2Z.inj]. wp_cas_fail. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|]. wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto. wp_op. rewrite bool_decide_false //. wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto. rewrite {3}/mcounter; eauto 10. Qed. ... ... @@ -136,10 +139,11 @@ Section contrib_spec. { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); lia. } wp_cas_suc. iModIntro. iSplitL "Hl Hγ". { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. } wp_if. by iApply "HΦ". - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). wp_op. rewrite bool_decide_true //. wp_if. by iApply "HΦ". - assert (#c ≠ #c') by by intros [= ?%Nat2Z.inj]. wp_cas_fail. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|]. wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto. wp_op. rewrite bool_decide_false //. wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto. Qed. Lemma read_contrib_spec γ l q n : ... ...
 ... ... @@ -16,7 +16,7 @@ Section increment_physical. Definition incr_phy : val := rec: "incr" "l" := let: "oldv" := !"l" in if: CAS "l" "oldv" ("oldv" + #1) if: CAS "l" "oldv" ("oldv" + #1) = "oldv" then "oldv" (* return old value if success *) else "incr" "l". ... ... @@ -29,9 +29,9 @@ Section increment_physical. wp_pures. wp_bind (CAS _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]". destruct (decide (#v = #w)) as [[= ->]|Hx]. - wp_cas_suc. iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ". iModIntro. wp_if. done. iModIntro. wp_op. rewrite bool_decide_true //. wp_if. done. - wp_cas_fail. iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU". iModIntro. wp_if. iApply "IH". done. iModIntro. wp_op. rewrite bool_decide_false //. wp_if. iApply "IH". done. Qed. End increment_physical. ... ... @@ -45,7 +45,7 @@ Section increment. Definition incr : val := rec: "incr" "l" := let: "oldv" := !"l" in if: CAS "l" "oldv" ("oldv" + #1) if: CAS "l" "oldv" ("oldv" + #1) = "oldv" then "oldv" (* return old value if success *) else "incr" "l". ... ... @@ -70,9 +70,9 @@ Section increment. { (* abort case *) iDestruct "Hclose" as "[? _]". done. } iIntros "Hl". simpl. destruct (decide (#w = #v)) as [[= ->]|Hx]. - iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ". iIntros "!>". wp_if. by iApply "HΦ". iIntros "!>". wp_op. rewrite bool_decide_true //. wp_if. by iApply "HΦ". - iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU". iIntros "!>". wp_if. iApply "IH". done. iIntros "!>". wp_op. rewrite bool_decide_false //. wp_if. iApply "IH". done. Qed. (** A proof of the incr specification that uses lemmas to avoid reasining ... ... @@ -94,9 +94,9 @@ Section increment. iIntros "H↦ !>". simpl. destruct (decide (#x' = #x)) as [[= ->]|Hx]. - iRight. iFrame. iIntros "HΦ !>". wp_if. by iApply "HΦ". wp_op. rewrite bool_decide_true //. wp_if. by iApply "HΦ". - iLeft. iFrame. iIntros "AU !>". wp_if. iApply "IH". done. wp_op. rewrite bool_decide_false //. wp_if. iApply "IH". done. Qed. (** A "weak increment": assumes that there is no race *) ... ...
 ... ... @@ -7,7 +7,7 @@ From iris.heap_lang.lib Require Import lock. Set Default Proof Using "Type". Definition newlock : val := λ: <>, ref #false. Definition try_acquire : val := λ: "l", CAS "l" #false #true. Definition try_acquire : val := λ: "l", CAS "l" #false #true = #false. Definition acquire : val := rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l". Definition release : val := λ: "l", "l" <- #false. ... ... @@ -61,12 +61,12 @@ Section proof. {{{ b, RET #b; if b is true then locked γ ∗ R else True }}}. Proof. iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv". wp_rec. iInv N as ([]) "[Hl HR]". wp_rec. wp_bind (CAS _ _ _). iInv N as ([]) "[Hl HR]". - wp_cas_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto). iApply ("HΦ" \$! false). done. wp_pures. iApply ("HΦ" \$! false). done. - wp_cas_suc. iDestruct "HR" as "[Hγ HR]". iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto). rewrite /locked. by iApply ("HΦ" \$! true with "[\$Hγ \$HR]"). rewrite /locked. wp_pures. by iApply ("HΦ" \$! true with "[\$Hγ \$HR]"). Qed. Lemma acquire_spec γ lk R : ... ...
 ... ... @@ -20,7 +20,7 @@ Definition newlock : val := Definition acquire : val := rec: "acquire" "lk" := let: "n" := !(Snd "lk") in if: CAS (Snd "lk") "n" ("n" + #1) if: CAS (Snd "lk") "n" ("n" + #1) = "n" then wait_loop "n" "lk" else "acquire" "lk". ... ... @@ -122,14 +122,14 @@ Section proof. wp_cas_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth". { iNext. iExists o', (S n). rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. } wp_if. wp_op. rewrite bool_decide_true //. wp_if. iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]"). + iFrame. rewrite /is_lock; eauto 10. + by iNext. - wp_cas_fail. iModIntro. iSplitL "Hlo' Hln' Hauth Haown". { iNext. iExists o', n'. by iFrame. } wp_if. by iApply "IH"; auto. wp_op. rewrite bool_decide_false //. wp_if. by iApply "IH"; auto. Qed. Lemma release_spec γ lk R : ... ...
 ... ... @@ -56,8 +56,7 @@ Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core (* [simpl apply] is too stupid, so we need extern hints here. *) Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core. Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS : core. Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS : core. Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasS : core. Local Hint Extern 0 (head_step (AllocN _ _) _ _ _ _ _) => apply alloc_fresh : core. Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : core. Local Hint Resolve to_of_val : core. ... ... @@ -378,7 +377,7 @@ Qed. Lemma wp_cas_fail s E l q v' v1 v2 : val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 → {{{ ▷ l ↦{q} v' }}} CAS (Val \$ LitV \$ LitLoc l) (Val v1) (Val v2) @ s; E {{{ RET LitV (LitBool false); l ↦{q} v' }}}. {{{ RET v'; l ↦{q} v' }}}. Proof. iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. ... ... @@ -388,7 +387,7 @@ Qed. Lemma twp_cas_fail s E l q v' v1 v2 : val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 → [[{ l ↦{q} v' }]] CAS (Val \$ LitV \$ LitLoc l) (Val v1) (Val v2) @ s; E [[{ RET LitV (LitBool false); l ↦{q} v' }]]. [[{ RET v'; l ↦{q} v' }]]. Proof. iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto. iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. ... ... @@ -399,7 +398,7 @@ Qed. Lemma wp_cas_suc s E l v1 v2 v' : val_for_compare v' = val_for_compare v1 → vals_cas_compare_safe v' v1 → {{{ ▷ l ↦ v' }}} CAS (Val \$ LitV \$ LitLoc l) (Val v1) (Val v2) @ s; E {{{ RET LitV (LitBool true); l ↦ v2 }}}. {{{ RET v'; l ↦ v2 }}}. Proof. iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. ... ... @@ -410,7 +409,7 @@ Qed. Lemma twp_cas_suc s E l v1 v2 v' : val_for_compare v' = val_for_compare v1 → vals_cas_compare_safe v' v1 → [[{ l ↦ v' }]] CAS (Val \$ LitV \$ LitLoc l) (Val v1) (Val v2) @ s; E [[{ RET LitV (LitBool true); l ↦ v2 }]]. [[{ RET v'; l ↦ v2 }]]. Proof. iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto. iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. ... ... @@ -578,7 +577,7 @@ Lemma wp_cas_suc_offset s E l off vs v' v1 v2 : vals_cas_compare_safe v' v1 → {{{ ▷ l ↦∗ vs }}} CAS #(l +ₗ off) v1 v2 @ s; E {{{ RET #true; l ↦∗ <[off:=v2]> vs }}}. {{{ RET v'; l ↦∗ <[off:=v2]> vs }}}. Proof. iIntros (Hlookup ?? Φ) "Hl HΦ". iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]". ... ... @@ -591,7 +590,7 @@ Lemma wp_cas_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 : vals_cas_compare_safe (vs !!! off) v1 → {{{ ▷ l ↦∗ vs }}} CAS #(l +ₗ off) v1 v2 @ s; E {{{ RET #true; l ↦∗ vinsert off v2 vs }}}. {{{ RET (vs !!! off); l ↦∗ vinsert off v2 vs }}}. Proof. intros. setoid_rewrite vec_to_list_insert. eapply wp_cas_suc_offset=> //. by apply vlookup_lookup. ... ... @@ -603,7 +602,7 @@ Lemma wp_cas_fail_offset s E l off vs v0 v1 v2 : vals_cas_compare_safe v0 v1 → {{{ ▷ l ↦∗ vs }}} CAS #(l +ₗ off) v1 v2 @ s; E {{{ RET #false; l ↦∗ vs }}}. {{{ RET v0; l ↦∗ vs }}}. Proof. iIntros (Hlookup HNEq Hcmp Φ) ">Hl HΦ". iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]". ... ... @@ -618,7 +617,7 @@ Lemma wp_cas_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 : vals_cas_compare_safe (vs !!! off) v1 → {{{ ▷ l ↦∗ vs }}} CAS #(l +ₗ off) v1 v2 @ s; E {{{ RET #false; l ↦∗ vs }}}. {{{ RET (vs !!! off); l ↦∗ vs }}}. Proof. intros. eapply wp_cas_fail_offset=> //. by apply vlookup_lookup. Qed. Lemma wp_faa_offset s E l off vs (i1 i2 : Z) : ... ...
 ... ... @@ -135,6 +135,7 @@ Proof. - unfold un_op_eval in *. repeat case_match; naive_solver. - eapply bin_op_eval_closed; eauto; naive_solver. - by apply heap_closed_alloc. - case_match; try apply map_Forall_insert_2; by naive_solver. Qed. (* Parallel substitution with maps of values indexed by strings *) ... ...
 ... ... @@ -284,9 +284,9 @@ Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v v1 v2 Φ : envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' → vals_cas_compare_safe v v1 → (val_for_compare v = val_for_compare v1 → envs_entails Δ'' (WP fill K (Val \$ LitV true) @ s; E {{ Φ }})) → envs_entails Δ'' (WP fill K (Val v) @ s; E {{ Φ }})) → (val_for_compare v ≠ val_for_compare v1 → envs_entails Δ' (WP fill K (Val \$ LitV false) @ s; E {{ Φ }})) → envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }})) → envs_entails Δ (WP fill K (CAS (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}). Proof. rewrite envs_entails_eq=> ???? Hsuc Hfail. ... ... @@ -305,9 +305,9 @@ Lemma tac_twp_cas Δ Δ' s E i K l v v1 v2 Φ : envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' → vals_cas_compare_safe v v1 → (val_for_compare v = val_for_compare v1 → envs_entails Δ' (WP fill K (Val \$ LitV true) @ s; E [{ Φ }])) → envs_entails Δ' (WP fill K (Val v) @ s; E [{ Φ }])) → (val_for_compare v ≠ val_for_compare v1 → envs_entails Δ (WP fill K (Val \$ LitV false) @ s; E [{ Φ }])) → envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }])) → envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]). Proof. rewrite envs_entails_eq=> ??? Hsuc Hfail. ... ... @@ -326,7 +326,7 @@ Lemma tac_wp_cas_fail Δ Δ' s E i K l q v v1 v2 Φ : MaybeIntoLaterNEnvs 1 Δ Δ' → envs_lookup i Δ' = Some (false, l ↦{q} v)%I → val_for_compare v ≠ val_for_compare v1 → vals_cas_compare_safe v v1 → envs_entails Δ' (WP fill K (Val \$ LitV false) @ s; E {{ Φ }}) → envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }}) → envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}). Proof. rewrite envs_entails_eq=> ?????. ... ... @@ -337,7 +337,7 @@ Qed. Lemma tac_twp_cas_fail Δ s E i K l q v v1 v2 Φ : envs_lookup i Δ = Some (false, l ↦{q} v)%I → val_for_compare v ≠ val_for_compare v1 → vals_cas_compare_safe v v1 → envs_entails Δ (WP fill K (Val \$ LitV false) @ s; E [{ Φ }]) → envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }]) → envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]). Proof. rewrite envs_entails_eq. intros. rewrite -twp_bind. ... ... @@ -350,7 +350,7 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ : envs_lookup i Δ' = Some (false, l ↦ v)%I → envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' → val_for_compare v = val_for_compare v1 → vals_cas_compare_safe v v1 → envs_entails Δ'' (WP fill K (Val \$ LitV true) @ s; E {{ Φ }}) → envs_entails Δ'' (WP fill K (Val v) @ s; E {{ Φ }}) → envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}). Proof. rewrite envs_entails_eq=> ??????; subst. ... ... @@ -363,7 +363,7 @@ Lemma tac_twp_cas_suc Δ Δ' s E i K l v v1 v2 Φ : envs_lookup i Δ = Some (false, l ↦ v)%I → envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' → val_for_compare v = val_for_compare v1 → vals_cas_compare_safe v v1 → envs_entails Δ' (WP fill K (Val \$ LitV true) @ s; E [{ Φ }]) → envs_entails Δ' (WP fill K (Val v) @ s; E [{ Φ }]) → envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]). Proof. rewrite envs_entails_eq=>?????; subst. ... ... @@ -627,7 +627,7 @@ Tactic Notation "wp_faa" := | |- envs_entails _ (wp ?s ?E ?e ?Q) => first [reshape_expr e ltac:(fun K e' => eapply (tac_wp_faa _ _ _ _ _ _ K)) |fail 1 "wp_faa: cannot find 'CAS' in" e]; |fail 1 "wp_faa: cannot find 'FAA' in" e]; [iSolveTC |solve_mapsto () |pm_reflexivity ... ... @@ -635,7 +635,7 @@ Tactic Notation "wp_faa" := | |- envs_entails _ (twp ?s ?E ?e ?Q) => first [reshape_expr e ltac:(fun K e' => eapply (tac_twp_faa _ _ _ _ _ K)) |fail 1 "wp_faa: cannot find 'CAS' in" e]; |fail 1 "wp_faa: cannot find 'FAA' in" e]; [solve_mapsto () |pm_reflexivity |wp_finish] ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment