From 917d7705c5345364a15d7a4383b0662c65b35582 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Mon, 24 Jun 2019 14:46:13 +0200
Subject: [PATCH] bump Iris for CmpXchg change, and port everyting
---
opam | 2 +-
.../concurrent_stacks/concurrent_stack1.v | 18 ++++-----
.../concurrent_stacks/concurrent_stack2.v | 34 ++++++++---------
.../concurrent_stacks/concurrent_stack3.v | 18 ++++-----
.../concurrent_stacks/concurrent_stack4.v | 36 +++++++++---------
theories/hocap/fg_bag.v | 20 +++++-----
theories/lecture_notes/coq_intro_example_2.v | 30 +++++++--------
theories/lecture_notes/lock.v | 10 +++--
theories/lecture_notes/lock_unary_spec.v | 16 +++++---
theories/lecture_notes/modular_incr.v | 10 ++---
theories/logatom/conditional_increment/cinc.v | 38 +++++++++----------
theories/logatom/flat_combiner/peritem.v | 10 ++---
theories/logatom/snapshot/atomic_snapshot.v | 10 ++---
theories/logatom/treiber.v | 20 +++++-----
theories/logatom/treiber2.v | 22 +++++------
theories/logrel_heaplang/ltyping.v | 7 ++--
theories/spanning_tree/spanning.v | 9 +++--
17 files changed, 159 insertions(+), 151 deletions(-)
diff --git a/opam b/opam
index 8d26d10..f0caf49 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
- "coq-iris" { (= "dev.2019-06-20.3.4f0c1046") | (= "dev") }
+ "coq-iris" { (= "dev.2019-06-24.3.5ef58527") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
diff --git a/theories/concurrent_stacks/concurrent_stack1.v b/theories/concurrent_stacks/concurrent_stack1.v
index ef69142..7fbdcc2 100644
--- a/theories/concurrent_stacks/concurrent_stack1.v
+++ b/theories/concurrent_stacks/concurrent_stack1.v
@@ -111,23 +111,23 @@ Section stacks.
wp_load.
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _, _; by iFrame. }
- iModIntro. wp_let. wp_alloc ℓ' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
+ iModIntro. wp_let. wp_alloc ℓ' as "Hl'". wp_pures. wp_bind (CmpXchg _ _ _).
iInv N as (ℓ'' v'') "(>% & >Hl & Hlist)" "Hclose"; simplify_eq.
destruct (decide (v' = v'')) as [->|Hne].
- - wp_cas_suc. { destruct v''; left; done. }
+ - wp_cmpxchg_suc. { destruct v''; left; done. }
iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
{ iNext; iExists _, (Some ℓ'); iFrame; iSplit; first done;
rewrite (is_list_unfold _ (Some _)). iExists _, _; iFrame; eauto. }
iModIntro.
- wp_if.
+ wp_pures.
by iApply "HΦ".
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
{ destruct v', v''; simpl; congruence. }
{ destruct v''; left; done. }
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _, _; by iFrame. }
iModIntro.
- wp_if.
+ wp_pures.
iApply ("IH" with "HP HΦ").
Qed.
@@ -153,25 +153,25 @@ Section stacks.
iMod ("Hclose" with "[Hl' Hlist]") as "_".
{ iNext; iExists _, _; by iFrame. }
iModIntro.
- wp_pures. wp_bind (CAS _ _ _).
+ wp_pures. wp_bind (CmpXchg _ _ _).
iInv N as (ℓ'' v'') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
destruct (decide (v'' = (Some l))) as [-> |].
* rewrite is_list_unfold.
iDestruct "Hlist" as (h' t') "(Hl'' & HP & Hlist)".
iDestruct "Hl''" as (q') "Hl''".
simpl.
- wp_cas_suc.
+ wp_cmpxchg_suc.
iDestruct (mapsto_agree with "Hl'' Hl") as %[= <- <-%oloc_to_val_inj].
iMod ("Hclose" with "[Hl' Hlist]") as "_".
{ iNext; iExists ℓ'', _; by iFrame. }
iModIntro.
wp_pures.
iApply ("HΦ" with "[HP]"); iRight; iExists _; by iFrame.
- * wp_cas_fail. { destruct v''; simpl; congruence. }
+ * wp_cmpxchg_fail. { destruct v''; simpl; congruence. }
iMod ("Hclose" with "[Hl' Hlist]") as "_".
{ iNext; iExists ℓ'', _; by iFrame. }
iModIntro.
- wp_if.
+ wp_pures.
iApply ("IH" with "HΦ").
Qed.
End stacks.
diff --git a/theories/concurrent_stacks/concurrent_stack2.v b/theories/concurrent_stacks/concurrent_stack2.v
index ae45ce8..0470370 100644
--- a/theories/concurrent_stacks/concurrent_stack2.v
+++ b/theories/concurrent_stacks/concurrent_stack2.v
@@ -97,22 +97,22 @@ Section side_channel.
{{{ v', RET v'; (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ P v'') ∨ ⌜v' = InjLV #()⌝ }}}.
Proof.
iIntros (Φ) "[Hinv Hγ] HΦ". iDestruct "Hinv" as (v' l) "[-> #Hinv]".
- wp_lam. wp_bind (CAS _ _ _). wp_pures.
+ wp_lam. wp_bind (CmpXchg _ _ _). wp_pures.
iInv N as "Hstages" "Hclose".
iDestruct "Hstages" as "[[Hl HP] | [H | [Hl H]]]".
- - wp_cas_suc.
+ - wp_cmpxchg_suc.
iMod ("Hclose" with "[Hl Hγ]") as "_".
{ iRight; iRight; iFrame. }
iModIntro.
wp_pures.
by iApply "HΦ"; iLeft; iExists _; iSplit.
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
iMod ("Hclose" with "[H]") as "_".
{ iRight; iLeft; auto. }
iModIntro.
wp_pures.
by iApply "HΦ"; iRight.
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
iDestruct (own_valid_2 with "H Hγ") as %[].
Qed.
@@ -123,22 +123,22 @@ Section side_channel.
{{{ v', RET v'; (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ P v'') ∨ ⌜v' = InjLV #()⌝ }}}.
Proof.
iIntros (Φ) "H HΦ"; iDestruct "H" as (v l) "[-> #Hinv]".
- wp_lam. wp_proj. wp_bind (CAS _ _ _).
+ wp_lam. wp_proj. wp_bind (CmpXchg _ _ _).
iInv N as "Hstages" "Hclose".
iDestruct "Hstages" as "[[H HP] | [H | [Hl Hγ]]]".
- - wp_cas_suc.
+ - wp_cmpxchg_suc.
iMod ("Hclose" with "[H]") as "_".
{ by iRight; iLeft. }
iModIntro.
wp_pures.
iApply "HΦ"; iLeft; auto.
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
iMod ("Hclose" with "[H]") as "_".
{ by iRight; iLeft. }
iModIntro.
wp_pures.
iApply "HΦ"; auto.
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
iMod ("Hclose" with "[Hl Hγ]").
{ iRight; iRight; iFrame. }
iModIntro.
@@ -326,23 +326,23 @@ Section stack_works.
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _; iFrame. }
iModIntro.
- wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
+ wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CmpXchg _ _ _).
iInv N as (list) "(Hl & Hlist)" "Hclose".
destruct (decide (v'' = list)) as [ -> |].
- * wp_cas_suc. { destruct list; left; done. }
+ * wp_cmpxchg_suc. { destruct list; left; done. }
iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
{ iNext; iExists (Some _); iFrame.
rewrite (is_list_unfold _ (Some _)). iExists _, _; iFrame; eauto. }
iModIntro.
- wp_if.
+ wp_pures.
by iApply "HΦ".
- * wp_cas_fail.
+ * wp_cmpxchg_fail.
{ destruct list, v''; simpl; congruence. }
{ destruct list; left; done. }
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _; by iFrame. }
iModIntro.
- wp_if.
+ wp_pures.
iApply ("IH" with "HP HΦ").
- wp_match.
by iApply "HΦ".
@@ -373,24 +373,24 @@ Section stack_works.
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _; by iFrame. }
iModIntro.
- wp_let. wp_proj. wp_bind (CAS _ _ _). wp_pures.
+ wp_let. wp_proj. wp_bind (CmpXchg _ _ _). wp_pures.
iInv N as (v'') "[Hl Hlist]" "Hclose".
destruct (decide (v'' = Some list)) as [-> |].
+ rewrite is_list_unfold.
iDestruct "Hlist" as (h' t') "(Hl'' & HP & Hlist)".
iDestruct "Hl''" as (q') "Hl''".
- wp_cas_suc.
+ wp_cmpxchg_suc.
iDestruct (mapsto_agree with "Hl'' Hl'") as "%"; simplify_eq.
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _; by iFrame. }
iModIntro.
wp_pures.
iApply ("HΦ" with "[HP]"); iRight; iExists _; by iFrame.
- + wp_cas_fail. { destruct v''; simpl; congruence. }
+ + wp_cmpxchg_fail. { destruct v''; simpl; congruence. }
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _; by iFrame. }
iModIntro.
- wp_if.
+ wp_pures.
iApply ("IH" with "HΦ").
- iDestruct "HSome" as (v) "[-> HP]".
wp_pures.
diff --git a/theories/concurrent_stacks/concurrent_stack3.v b/theories/concurrent_stacks/concurrent_stack3.v
index 4b51618..5a3506b 100644
--- a/theories/concurrent_stacks/concurrent_stack3.v
+++ b/theories/concurrent_stacks/concurrent_stack3.v
@@ -118,23 +118,23 @@ Section stack_works.
{ iNext; iExists _, _; iFrame. }
clear xs.
iModIntro.
- wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
+ wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CmpXchg _ _ _).
iInv N as (list' xs) "(Hl & Hlist & HP)" "Hclose".
destruct (decide (list = list')) as [ -> |].
- - wp_cas_suc. { destruct list'; left; done. }
+ - wp_cmpxchg_suc. { destruct list'; left; done. }
iMod ("Hupd" with "HP") as "[HP HΨ]".
iMod ("Hclose" with "[Hl Hl' HP Hlist]") as "_".
{ iNext; iExists (Some _), (v :: xs); iFrame; iExists _; iFrame; auto. }
iModIntro.
- wp_if.
+ wp_pures.
by iApply ("HΦ" with "HΨ").
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
{ destruct list, list'; simpl; congruence. }
{ destruct list'; left; done. }
iMod ("Hclose" with "[Hl HP Hlist]").
{ iExists _, _; iFrame. }
iModIntro.
- wp_if.
+ wp_pures.
iApply ("IH" with "Hupd HΦ").
Qed.
@@ -172,10 +172,10 @@ Section stack_works.
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
iModIntro.
- wp_let. wp_proj. wp_bind (CAS _ _ _). wp_pures.
+ wp_let. wp_proj. wp_bind (CmpXchg _ _ _). wp_pures.
iInv N as (v' xs'') "(Hl & Hlist & HP)" "Hclose".
destruct (decide (v' = (Some l'))) as [ -> |].
- * wp_cas_suc.
+ * wp_cmpxchg_suc.
iDestruct (is_list_cons with "[Hl'] Hlist") as (ys) "%"; first by iExists _.
simplify_eq.
iDestruct "Hupd" as "[Hupdcons _]".
@@ -188,11 +188,11 @@ Section stack_works.
iModIntro.
wp_pures.
iApply ("HΦ" with "HΨ").
- * wp_cas_fail. { destruct v'; simpl; congruence. }
+ * wp_cmpxchg_fail. { destruct v'; simpl; congruence. }
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
iModIntro.
- wp_if.
+ wp_pures.
iApply ("IH" with "Hupd HΦ").
Qed.
End stack_works.
diff --git a/theories/concurrent_stacks/concurrent_stack4.v b/theories/concurrent_stacks/concurrent_stack4.v
index e406b58..57af553 100644
--- a/theories/concurrent_stacks/concurrent_stack4.v
+++ b/theories/concurrent_stacks/concurrent_stack4.v
@@ -119,24 +119,24 @@ Section proofs.
{{{ v', RET v'; (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ can_push P Q v'') ∨ (⌜v' = InjLV #()⌝ ∗ (Q #())) }}}.
Proof.
iIntros (Φ) "[Hinv Hγ] HΦ". iDestruct "Hinv" as (v' l) "[-> #Hinv]".
- wp_lam. wp_pures. wp_bind (CAS _ _ _).
+ wp_lam. wp_pures. wp_bind (CmpXchg _ _ _).
iInv Nside_channel as "Hstages" "Hclose".
iDestruct "Hstages" as "[[Hl HP] | [[Hl HQ] | [[Hl H] | [Hl H]]]]".
- - wp_cas_suc.
+ - wp_cmpxchg_suc.
iMod ("Hclose" with "[Hl Hγ]") as "_".
{ iNext; iRight; iRight; iFrame. }
iModIntro.
wp_pures.
by iApply "HΦ"; iLeft; iExists _; iFrame.
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
iMod ("Hclose" with "[Hl Hγ]") as "_".
{ iNext; iRight; iRight; iLeft; iFrame. }
iModIntro.
wp_pures.
iApply ("HΦ" with "[HQ]"); iRight; auto.
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
iDestruct (own_valid_2 with "H Hγ") as %[].
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
iDestruct (own_valid_2 with "H Hγ") as %[].
Qed.
@@ -149,11 +149,11 @@ Section proofs.
(∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ Ψ v') ∨ (⌜v' = InjLV #()⌝ ∗ (do_pop ∧ Q')) }}}.
Proof.
simpl; iIntros (Φ) "[H [Hopener Hupd]] HΦ"; iDestruct "H" as (v l) "[-> #Hinv]".
- wp_lam. wp_proj. wp_bind (CAS _ _ _).
+ wp_lam. wp_proj. wp_bind (CmpXchg _ _ _).
iInv Nside_channel as "Hstages" "Hclose".
iDestruct "Hstages" as "[[Hl Hpush] | [[Hl HQ] | [[Hl Hγ] | [Hl Hγ]]]]".
- iMod "Hopener" as (xs) "[HP Hcloser]".
- wp_cas_suc.
+ wp_cmpxchg_suc.
iMod ("Hpush" with "HP") as "[HP HQ]".
iMod ("Hupd" with "HP") as "[HP HΨ]".
iMod ("Hcloser" with "HP") as "_".
@@ -162,19 +162,19 @@ Section proofs.
iApply fupd_intro_mask; first done.
wp_pures.
iApply "HΦ"; iLeft; auto.
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
iMod ("Hclose" with "[Hl HQ]") as "_".
{ iRight; iLeft; iFrame. }
iModIntro.
wp_pures.
iApply "HΦ"; auto.
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
iMod ("Hclose" with "[Hl Hγ]").
{ iRight; iRight; iFrame. }
iModIntro.
wp_pures.
iApply "HΦ"; auto.
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
iMod ("Hclose" with "[Hl Hγ]").
{ iRight; iRight; iFrame. }
iModIntro.
@@ -350,25 +350,25 @@ Section proofs.
{ iNext; iExists _, _; iFrame. }
clear xs.
iModIntro.
- wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
+ wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CmpXchg _ _ _).
iInv Nstack as (list' xs) "(Hl & Hlist & HP)" "Hclose".
destruct (decide (list = list')) as [ -> |].
- * wp_cas_suc. { destruct list'; left; done. }
+ * wp_cmpxchg_suc. { destruct list'; left; done. }
iMod (fupd_intro_mask' (⊤ ∖ ↑Nstack) inner_mask) as "Hupd'"; first solve_ndisj.
iMod ("Hupd" with "HP") as "[HP HΨ]".
iMod "Hupd'" as "_".
iMod ("Hclose" with "[Hl Hl' HP Hlist]") as "_".
{ iNext; iExists (Some _), (v' :: xs); iFrame; iExists _; iFrame; auto. }
iModIntro.
- wp_if.
+ wp_pures.
by iApply ("HΦ" with "HΨ").
- * wp_cas_fail.
+ * wp_cmpxchg_fail.
{ destruct list, list'; simpl; congruence. }
{ destruct list'; left; done. }
iMod ("Hclose" with "[Hl HP Hlist]").
{ iExists _, _; iFrame. }
iModIntro.
- wp_if.
+ wp_pures.
iApply ("IH" with "HΦ Hupd").
- wp_match. iApply ("HΦ" with "HΨ").
Qed.
@@ -426,10 +426,10 @@ Section proofs.
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
iModIntro.
- wp_pures. wp_bind (CAS _ _ _).
+ wp_pures. wp_bind (CmpXchg _ _ _).
iInv Nstack as (v' xs'') "(Hl & Hlist & HP)" "Hclose".
destruct (decide (v' = (Some l'))) as [ -> |].
- + wp_cas_suc.
+ + wp_cmpxchg_suc.
iDestruct (is_list_cons with "[Hl'] Hlist") as (ys) "%"; first by iExists _.
simplify_eq.
iMod (fupd_intro_mask' (⊤ ∖ ↑Nstack) inner_mask) as "Hupd'"; first solve_ndisj.
@@ -444,7 +444,7 @@ Section proofs.
iModIntro.
wp_pures.
iApply ("HΦ" with "HΨ").
- + wp_cas_fail. { destruct v'; simpl; congruence. }
+ + wp_cmpxchg_fail. { destruct v'; simpl; congruence. }
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
iModIntro.
diff --git a/theories/hocap/fg_bag.v b/theories/hocap/fg_bag.v
index b8c8c53..4f87bdd 100644
--- a/theories/hocap/fg_bag.v
+++ b/theories/hocap/fg_bag.v
@@ -162,21 +162,21 @@ Section proof.
{ iNext. iExists _,_. iFrame. } clear ls.
iModIntro.
wp_alloc n as "Hn".
- wp_pures. wp_bind (CAS _ _ _).
+ wp_pures. wp_bind (CmpXchg _ _ _).
iInv N as (o' ls) "[Ho [Hls >Hb]]" "Hcl".
destruct (decide (o = o')) as [->|?].
- - wp_cas_suc. { destruct o'; left; done. }
+ - wp_cmpxchg_suc. { destruct o'; left; done. }
iMod ("Hvs" with "[$Hb $HP]") as "[Hb HQ]".
iMod ("Hcl" with "[Ho Hn Hls Hb]") as "_".
{ iNext. iExists (Some _),(v::ls). iFrame "Ho Hb".
simpl. iExists _. iFrame. by iExists 1%Qp. }
- iModIntro. wp_if_true. by iApply "HΦ".
- - wp_cas_fail.
+ iModIntro. wp_pures. by iApply "HΦ".
+ - wp_cmpxchg_fail.
{ destruct o, o'; simpl; congruence. }
{ destruct o'; left; done. }
iMod ("Hcl" with "[Ho Hls Hb]") as "_".
{ iNext. iExists _,ls. by iFrame "Ho Hb". }
- iModIntro. wp_if_false.
+ iModIntro. wp_proj. wp_if.
by iApply ("IH" with "HP [HΦ]").
Qed.
@@ -214,11 +214,11 @@ Section proof.
iExists _; eauto. by iFrame. }
iModIntro. repeat wp_pure _.
iDestruct "Hhd'" as (q) "Hhd".
- wp_load. repeat wp_pure _.
- wp_bind (CAS _ _ _).
+ wp_load. wp_pures.
+ wp_bind (CmpXchg _ _ _).
iInv N as (o' ls') "[Ho [Hls >Hb]]" "Hcl".
destruct (decide (o' = (Some hd))) as [->|?].
- + wp_cas_suc.
+ + wp_cmpxchg_suc.
(* The list is still the same *)
rewrite (is_list_duplicate tl). iDestruct "Hls'" as "[Hls' Htl]".
iAssert (is_list (Some hd) (x::ls)) with "[Hhd Hls']" as "Hls'".
@@ -230,10 +230,10 @@ Section proof.
iMod ("Hcl" with "[Ho Htl Hb]") as "_".
{ iNext. iExists _,ls. by iFrame "Ho Hb". }
iModIntro. wp_pures. by iApply "HΦ".
- + wp_cas_fail. { destruct o'; simpl; congruence. }
+ + wp_cmpxchg_fail. { destruct o'; simpl; congruence. }
iMod ("Hcl" with "[Ho Hls Hb]") as "_".
{ iNext. iExists _,ls'. by iFrame "Ho Hb". }
- iModIntro. wp_if_false.
+ iModIntro. wp_proj. wp_if.
by iApply ("IH" with "HP [HΦ]").
Qed.
End proof.
diff --git a/theories/lecture_notes/coq_intro_example_2.v b/theories/lecture_notes/coq_intro_example_2.v
index 7d95642..253a2db 100644
--- a/theories/lecture_notes/coq_intro_example_2.v
+++ b/theories/lecture_notes/coq_intro_example_2.v
@@ -316,10 +316,10 @@ Section monotone_counter.
{ iNext; iExists m; iFrame. }
iModIntro.
wp_let; wp_op; wp_let.
- wp_bind (CAS _ _ _)%E.
+ wp_bind (CmpXchg _ _ _)%E.
iInv N as (k) ">[Hpt HOwnAuth]" "HClose".
destruct (decide (k = m)); subst.
- + wp_cas_suc.
+ + wp_cmpxchg_suc.
(* If the CAS succeeds we need to update our ghost state. This is achieved using the own_update rule/lemma.
The arguments are the ghost name and the ghost resources x from which and to which we are updating.
Finally we need to give up own γ x to get ownership of the new resources.
@@ -332,12 +332,12 @@ Section monotone_counter.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
{ iNext; iExists (1 + m)%nat.
rewrite Nat2Z.inj_succ Z.add_1_l; iFrame. }
- iModIntro; wp_if; iApply ("HCont" with "[HInv HOwnFrag]").
+ iModIntro; wp_pures; iApply ("HCont" with "[HInv HOwnFrag]").
iExists γ; iFrame "#"; iFrame.
- + wp_cas_fail; first intros ?; simplify_eq.
+ + wp_cmpxchg_fail; first intros ?; simplify_eq.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
- iExists k; iFrame.
- - iModIntro; wp_if.
+ - iModIntro. wp_proj. wp_if.
iApply ("IH" with "HOwnFrag HCont"); iFrame.
Qed.
End monotone_counter.
@@ -501,22 +501,22 @@ Section monotone_counter'.
{ iNext; iExists m; iFrame. }
iModIntro.
wp_let; wp_op; wp_let.
- wp_bind (CAS _ _ _)%E.
+ wp_bind (CmpXchg _ _ _)%E.
iInv N as (k) ">[Hpt HOwnAuth]" "HClose".
destruct (decide (k = m)); subst.
- + wp_cas_suc.
+ + wp_cmpxchg_suc.
iMod (own_update γ ((● m ⋅ ◯ n)) (● (S m : mnatUR) ⋅ (◯ (S n : mnatUR))) with "[HOwnFrag HOwnAuth]") as "[HOwnAuth HOwnFrag]".
{ apply mcounterRA_update'. }
{ rewrite own_op; iFrame. }
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
{ iNext; iExists (1 + m)%nat.
rewrite Nat2Z.inj_succ Z.add_1_l; iFrame. }
- iModIntro; wp_if; iApply ("HCont" with "[HInv HOwnFrag]").
+ iModIntro; wp_pures; iApply ("HCont" with "[HInv HOwnFrag]").
iExists γ; iFrame "#"; iFrame.
- + wp_cas_fail; first intros ?; simplify_eq.
+ + wp_cmpxchg_fail; first intros ?; simplify_eq.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
- iExists k; iFrame.
- - iModIntro; wp_if.
+ - iModIntro. wp_proj. wp_if.
iApply ("IH" with "HOwnFrag HCont"); iFrame.
Qed.
End monotone_counter'.
@@ -621,16 +621,16 @@ Section ccounter.
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hpt]" "Hclose".
wp_load. iMod ("Hclose" with "[Hpt Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iModIntro. wp_let. wp_op. wp_let.
- wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hpt]" "Hclose".
+ wp_bind (CmpXchg _ _ _). iInv N as (c') ">[Hγ Hpt]" "Hclose".
destruct (decide (c' = c)) as [->|].
- iMod (own_update_2 with "Hγ Hown") as "[Hγ Hown]".
{ apply ccounterRA_update. } (* We use the update lemma for our RA. *)
- wp_cas_suc. iMod ("Hclose" with "[Hpt Hγ]") as "_".
+ wp_cmpxchg_suc. iMod ("Hclose" with "[Hpt Hγ]") as "_".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
- iModIntro. wp_if. iApply "HΦ". by iFrame "Hinv".
- - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
+ iModIntro. wp_pures. iApply "HΦ". by iFrame "Hinv".
+ - wp_cmpxchg_fail; first (by intros [= ?%Nat2Z.inj]).
iMod ("Hclose" with "[Hpt Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
- iModIntro. wp_if. by iApply ("IH" with "[Hown] [HΦ]"); auto.
+ iModIntro. wp_pures. by iApply ("IH" with "[Hown] [HΦ]"); auto.
Qed.
Lemma read_contrib_spec γ ℓ q n :
diff --git a/theories/lecture_notes/lock.v b/theories/lecture_notes/lock.v
index 45450c3..9db80af 100644
--- a/theories/lecture_notes/lock.v
+++ b/theories/lecture_notes/lock.v
@@ -94,17 +94,19 @@ Section lock_spec.
iIntros (HE φ) "#Hi Hcont"; rewrite /acquire.
iLöb as "IH".
wp_rec.
- wp_bind (CAS _ _ _).
+ wp_bind (CmpXchg _ _ _).
iInv (lockN l) as "[(Hl & HP & Ht)|Hl]" "Hcl".
- - wp_cas_suc.
+ - wp_cmpxchg_suc.
iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
iModIntro.
+ wp_proj.
wp_if.
iApply "Hcont".
iFrame.
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
iModIntro.
+ wp_proj.
wp_if.
iApply ("IH" with "[$Hcont]").
Qed.
@@ -129,4 +131,4 @@ End lock_spec.
Typeclasses Opaque locked.
Global Opaque locked.
Typeclasses Opaque is_lock.
-Global Opaque is_lock.
\ No newline at end of file
+Global Opaque is_lock.
diff --git a/theories/lecture_notes/lock_unary_spec.v b/theories/lecture_notes/lock_unary_spec.v
index 85eb981..3f6dcb9 100644
--- a/theories/lecture_notes/lock_unary_spec.v
+++ b/theories/lecture_notes/lock_unary_spec.v
@@ -109,17 +109,19 @@ Section lock_spec.
iIntros (HE φ) "#Hi Hcont"; rewrite /acquire.
iLöb as "IH".
wp_rec.
- wp_bind (CAS _ _ _).
+ wp_bind (CmpXchg _ _ _).
iInv (lockN l) as "[(Hl & HP & Ht)|Hl]" "Hcl".
- - wp_cas_suc.
+ - wp_cmpxchg_suc.
iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
iModIntro.
+ wp_proj.
wp_if.
iApply "Hcont".
iFrame.
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
iModIntro.
+ wp_proj.
wp_if.
iApply ("IH" with "[$Hcont]").
Qed.
@@ -167,16 +169,18 @@ Section lock_spec.
iIntros (HE) "#Hi"; rewrite /acquire.
iLöb as "IH".
wp_rec.
- wp_bind (CAS _ _ _).
+ wp_bind (CmpXchg _ _ _).
iInv (lockN l) as "[(Hl & HP & Ht)|Hl]" "Hcl".
- - wp_cas_suc.
+ - wp_cmpxchg_suc.
iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
iModIntro.
+ wp_proj.
wp_if.
iFrame.
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
iModIntro.
+ wp_proj.
wp_if.
iApply "IH".
Qed.
diff --git a/theories/lecture_notes/modular_incr.v b/theories/lecture_notes/modular_incr.v
index 7b75637..dab089e 100644
--- a/theories/lecture_notes/modular_incr.v
+++ b/theories/lecture_notes/modular_incr.v
@@ -169,21 +169,21 @@ Section cnt_spec.
iModIntro.
wp_let.
wp_op.
- wp_bind (CAS _ _ _)%E.
+ wp_bind (CmpXchg _ _ _)%E.
iInv (N .@ "internal") as (m') "[>Hpt >Hown]" "HClose".
destruct (decide (m = m')); simplify_eq.
- - wp_cas_suc.
+ - wp_cmpxchg_suc.
iMod ("HVS" $! m' with "[Hown HP]") as "[Hown HQ]"; first iFrame.
iMod ("HClose" with "[Hpt Hown]") as "_".
{ iNext; iExists _; iFrame. }
iModIntro.
- wp_if.
+ wp_pures.
iApply "HCont"; by iFrame.
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
iMod ("HClose" with "[Hpt Hown]") as "_".
{ iNext; iExists _; iFrame. }
iModIntro.
- wp_if.
+ wp_pures.
iApply ("IH" with "HP HCont").
Qed.
diff --git a/theories/logatom/conditional_increment/cinc.v b/theories/logatom/conditional_increment/cinc.v
index d3bbb48..15cf972 100644
--- a/theories/logatom/conditional_increment/cinc.v
+++ b/theories/logatom/conditional_increment/cinc.v
@@ -23,7 +23,7 @@ Definition new_counter : val :=
(*
complete(c, f, x, n, p) :=
- Resolve CAS(c, x, ref (injL (if !f then n+1 else n))) p (ref ()) ;; ()
+ Resolve CmpXchg(c, x, ref (injL (if !f then n+1 else n))) p (ref ()) ;; ()
*)
Definition complete : val :=
λ: "c" "f" "x" "n" "p",
@@ -31,7 +31,7 @@ Definition complete : val :=
(* Compare with #true to make this a total operation that never
gets stuck, no matter the value stored in [f]. *)
let: "new_n" := if: !"f" = #true then "n" + #1 else "n" in
- Resolve (CAS "c" "x" (ref (InjL "new_n"))) "p" "l_ghost" ;; #().
+ Resolve (CmpXchg "c" "x" (ref (InjL "new_n"))) "p" "l_ghost" ;; #().
(*
get c :=
@@ -131,7 +131,7 @@ Section conditional_counter.
Fixpoint val_to_some_loc (vs : list (val * val)) : option loc :=
match vs with
- | (#true , LitV (LitLoc l)) :: _ => Some l
+ | ((_, #true)%V, LitV (LitLoc l)) :: _ => Some l
| _ :: vs => val_to_some_loc vs
| _ => None
end.
@@ -161,12 +161,12 @@ Section conditional_counter.
Definition accepted_state Q (proph_winner : option loc) (l_ghost_winner : loc) :=
(l_ghost_winner ↦{1/2} - ∗ match proph_winner with None => True | Some l => ⌜l = l_ghost_winner⌝ ∗ Q end)%I.
- (* The same thread then wins the CAS and moves from [accepted] to [done].
+ (* The same thread then wins the CmpXchg and moves from [accepted] to [done].
Then, the [γ_t] token guards the transition to take out [Q].
- Remember that the thread winning the CAS might be just helping. The token
+ Remember that the thread winning the CmpXchg might be just helping. The token
is owned by the thread whose request this is.
In this state, [l_ghost_winner] serves as a token to make sure that
- only the CAS winner can transition to here, and owning half of[l] serves as a
+ only the CmpXchg winner can transition to here, and owning half of[l] serves as a
"location" token to ensure there is no ABA going on. Notice how [counter_inv]
owns *more than* half of its [l], which means we know that the [l] there
and here cannot be the same. *)
@@ -264,7 +264,7 @@ Section conditional_counter.
(□(own_token γ_t ={⊤}=∗ ▷ Q) -∗ Φ #()) -∗
own γ_n (● Excl' n) -∗
l_new ↦ InjLV #n -∗
- WP Resolve (CAS #c_l #l #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
+ WP Resolve (CmpXchg #c_l #l #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
Proof.
iIntros "#InvC #InvS Hl_ghost HQ Hn● [Hl_new Hl_new']". wp_bind (Resolve _ _ _)%E.
iInv counterN as (l' q s) "(>Hc & >[Hl Hl'] & Hrest)".
@@ -286,9 +286,9 @@ Section conditional_counter.
while a [state] protocol is not [done], it owns enough of
the [counter] protocol to ensure that does not move anywhere else. *)
iDestruct (mapsto_agree with "Hc Hc'") as %[= ->].
- (* We perform the CAS. *)
+ (* We perform the CmpXchg. *)
iCombine "Hc Hc'" as "Hc".
- wp_apply (wp_resolve with "Hp"); first done; wp_cas_suc.
+ wp_apply (wp_resolve with "Hp"); first done; wp_cmpxchg_suc.
iIntros (vs' ->) "Hp'". simpl.
(* Update to Done. *)
iDestruct "Accepted" as "[Hl_ghost_inv [HEq Q]]".
@@ -313,19 +313,19 @@ Section conditional_counter.
inv stateN (state_inv P Q p m c_l l l_ghost_inv γ_n γ_t γ_s) -∗
(□(own_token γ_t ={⊤}=∗ ▷ Q) -∗ Φ #()) -∗
l_new ↦ InjLV #n -∗
- WP Resolve (CAS #c_l #l #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
+ WP Resolve (CmpXchg #c_l #l #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
Proof.
iIntros (Hnl) "#InvC #InvS HQ Hl_new". wp_bind (Resolve _ _ _)%E.
iInv counterN as (l' q s) "(>Hc & >[Hl Hl'] & Hrest)".
iInv stateN as (vs) "(>Hp & [NotDone | [#Hs Done]])".
{ (* If the [state] protocol is not done yet, we can show that it
- is the active protocol still (l = l'). But then the CAS would
+ is the active protocol still (l = l'). But then the CmpXchg would
succeed, and our prophecy would have told us that.
So here we can prove that the prophecy was wrong. *)
iDestruct "NotDone" as "(_ & >Hc' & State)".
iDestruct (mapsto_agree with "Hc Hc'") as %[=->].
iCombine "Hc Hc'" as "Hc".
- wp_apply (wp_resolve with "Hp"); first done; wp_cas_suc.
+ wp_apply (wp_resolve with "Hp"); first done; wp_cmpxchg_suc.
iIntros (vs' ->). iDestruct "State" as "[Pending | Accepted]".
+ iDestruct "Pending" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
+ iDestruct "Accepted" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs. }
@@ -339,8 +339,8 @@ Section conditional_counter.
iDestruct (mapsto_combine with "Hl Hl''") as "[Hl _]".
rewrite Qp_half_half. iDestruct (mapsto_valid_3 with "Hl Hl'") as "[]".
}
- (* The CAS fails. *)
- wp_apply (wp_resolve with "Hp"); first done. wp_cas_fail.
+ (* The CmpXchg fails. *)
+ wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_fail.
iIntros (vs' ->) "Hp". iModIntro.
iSplitL "Done Hp". { iNext. iExists _. iFrame "#∗". } iModIntro.
iSplitL "Hc Hrest Hl Hl'". { eauto 10 with iFrame. }
@@ -444,14 +444,14 @@ Section conditional_counter.
wp_let. wp_load. wp_match. wp_apply wp_new_proph; first done.
iIntros (l_ghost p') "Hp'".
wp_let. wp_alloc ly as "Hly".
- wp_let. wp_bind (CAS _ _ _)%E.
+ wp_let. wp_bind (CmpXchg _ _ _)%E.
(* open outer invariant again to CAS c_l *)
iInv counterN as (l'' q2 s) "(>Hc & >Hl & Hrest)".
destruct (decide (l' = l'')) as [<- | Hn].
+ (* CAS succeeds *)
iDestruct (mapsto_agree with "Hl' Hl") as %<-%state_to_val_inj.
iDestruct "Hrest" as ">[Hc' Hn●]". iCombine "Hc Hc'" as "Hc".
- wp_cas_suc.
+ wp_cmpxchg_suc.
(* Take a "peek" at [AU] and abort immediately to get [gc_is_gc f]. *)
iMod "AU" as (b' n') "[[CC Hf] [Hclose _]]".
iDestruct (gc_is_gc with "Hf") as "#Hgc".
@@ -470,13 +470,13 @@ Section conditional_counter.
(* close invariant *)
iNext. iExists _, _, (Updating f n p'). eauto 10 with iFrame.
}
- wp_if. wp_apply complete_spec; [done..|].
+ wp_pures. wp_apply complete_spec; [done..|].
iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_lam.
+ (* CAS fails: closing invariant and invoking IH *)
- wp_cas_fail.
+ wp_cmpxchg_fail.
iModIntro. iSplitR "AU".
{ iModIntro. iExists _, _, s. iFrame. }
- wp_if. by iApply "IH".
+ wp_pures. by iApply "IH".
- (* l' ↦ injR *)
iModIntro.
(* extract state invariant *)
diff --git a/theories/logatom/flat_combiner/peritem.v b/theories/logatom/flat_combiner/peritem.v
index 2ddcb83..44ee033 100644
--- a/theories/logatom/flat_combiner/peritem.v
+++ b/theories/logatom/flat_combiner/peritem.v
@@ -70,21 +70,21 @@ Section proofs.
wp_load. iMod ("Hclose" with "[Hs H1]").
{ iNext. iFrame. iExists xs, hd. iFrame. }
iModIntro. wp_let. wp_alloc l as "Hl".
- wp_let. wp_bind (CAS _ _ _)%E.
+ wp_let. wp_bind (CmpXchg _ _ _)%E.
iInv N as "H1" "Hclose".
iDestruct "H1" as (xs' hd') "[>Hs H1]".
destruct (decide (hd = hd')) as [->|Hneq].
- - wp_cas_suc.
+ - wp_cmpxchg_suc.
iMod (inv_alloc N _ (R x) with "[HRx]") as "#HRx"; first eauto.
iMod ("Hclose" with "[Hs Hl H1]").
{ iNext. iFrame. iExists (x::xs'), l.
iFrame. simpl. iExists hd', 1%Qp. iFrame.
by iFrame "#". }
- iModIntro. wp_if. by iApply "HΦ".
- - wp_cas_fail.
+ iModIntro. wp_pures. by iApply "HΦ".
+ - wp_cmpxchg_fail.
iMod ("Hclose" with "[Hs H1]").
{ iNext. iFrame. iExists (xs'), hd'. iFrame. }
- iModIntro. wp_if. iApply ("IH" with "HRx").
+ iModIntro. wp_pures. iApply ("IH" with "HRx").
by iNext.
Qed.
diff --git a/theories/logatom/snapshot/atomic_snapshot.v b/theories/logatom/snapshot/atomic_snapshot.v
index 278cff3..d7364c6 100644
--- a/theories/logatom/snapshot/atomic_snapshot.v
+++ b/theories/logatom/snapshot/atomic_snapshot.v
@@ -224,12 +224,12 @@ Section atomic_snapshot.
wp_load. wp_proj. wp_let. wp_op. wp_alloc l1'new as "Hl1'new".
wp_let.
(* CAS *)
- wp_bind (CAS _ _ _)%E.
+ wp_bind (CmpXchg _ _ _)%E.
(* open invariant *)
iInv N as (q' l1'' T x' v'') ">[Hl1 [Hl1'' [Hx⚫ [Ht● Ht]]]]".
iDestruct "Ht" as %[Ht Hvt].
destruct (decide (l1'' = l1')) as [-> | Hn].
- - wp_cas_suc.
+ - wp_cmpxchg_suc.
iDestruct (mapsto_agree with "Hl1'frac2 Hl1''") as %[= -> ->]. iClear "Hl1'frac2".
(* open AU *)
iMod "AU" as (xv) "[Hx [_ Hclose]]".
@@ -257,10 +257,10 @@ Section atomic_snapshot.
rewrite Hd in Hv. clear Hd. apply elem_of_union in Hv.
destruct Hv as [Hv%elem_of_singleton_1 | Hv]; first done.
specialize (Hvt _ Hv). lia.
- + wp_if. done.
- - wp_cas_fail. iModIntro. iSplitR "AU".
+ + wp_pures. done.
+ - wp_cmpxchg_fail. iModIntro. iSplitR "AU".
+ iNext. rewrite /snapshot_inv. eauto 10 with iFrame.
- + wp_if. iApply "IH"; last eauto. rewrite /is_snapshot. eauto.
+ + wp_pures. iApply "IH"; last eauto. rewrite /is_snapshot. eauto.
Qed.
Lemma read_spec γ p :
diff --git a/theories/logatom/treiber.v b/theories/logatom/treiber.v
index 3eae8c7..f69762a 100644
--- a/theories/logatom/treiber.v
+++ b/theories/logatom/treiber.v
@@ -108,18 +108,18 @@ Section proof.
iDestruct "Hxs" as (hd) "[Hs Hhd]".
wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by eauto with iFrame.
iModIntro. wp_let. wp_alloc l as "Hl". wp_let.
- wp_bind (CAS _ _ _)%E.
+ wp_bind (CmpXchg _ _ _)%E.
iMod "HP" as (xs') "[Hxs' Hvs']".
iDestruct "Hxs'" as (hd') "[Hs' Hhd']".
destruct (decide (hd = hd')) as [->|Hneq].
- * wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
+ * wp_cmpxchg_suc. iDestruct "Hvs'" as "[_ Hvs']".
iMod ("Hvs'" with "[-]") as "HQ".
{ simpl. by eauto 10 with iFrame. }
- iModIntro. wp_if. eauto.
- * wp_cas_fail.
+ iModIntro. wp_pures. eauto.
+ * wp_cmpxchg_fail.
iDestruct "Hvs'" as "[Hvs' _]".
iMod ("Hvs'" with "[-]") as "HP"; first by eauto with iFrame.
- iModIntro. wp_if. by iApply "IH".
+ iModIntro. wp_pures. by iApply "IH".
Qed.
Lemma pop_atomic_spec (s: loc) :
@@ -147,11 +147,11 @@ Section proof.
iMod ("Hvs'" with "[-Hhd1 Hhd2 Hxs1]") as "HP".
{ eauto with iFrame. }
iModIntro. wp_let. wp_load. wp_match. wp_proj.
- wp_bind (CAS _ _ _).
+ wp_bind (CmpXchg _ _ _).
iMod "HP" as (xs'') "[Hxs'' Hvs']".
iDestruct "Hxs''" as (hd'') "[Hs'' Hhd'']".
destruct (decide (hd = hd'')) as [->|Hneq].
- + wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
+ + wp_cmpxchg_suc. iDestruct "Hvs'" as "[_ Hvs']".
destruct xs'' as [|x'' xs''].
{ simpl. iDestruct "Hhd''" as (?) "H".
iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1] [$H]") as %?. }
@@ -159,9 +159,9 @@ Section proof.
iDestruct (@mapsto_agree with "[$Hhd1] [$Hhd'']") as %[=]. subst.
iMod ("Hvs'" with "[-]") as "HQ".
{ eauto with iFrame. }
- iModIntro. wp_if. wp_pures. eauto.
- + wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]".
+ iModIntro. wp_pures. eauto.
+ + wp_cmpxchg_fail. iDestruct "Hvs'" as "[Hvs' _]".
iMod ("Hvs'" with "[-]") as "HP"; first by eauto with iFrame.
- iModIntro. wp_if. by iApply "IH".
+ iModIntro. wp_pures. by iApply "IH".
Qed.
End proof.
diff --git a/theories/logatom/treiber2.v b/theories/logatom/treiber2.v
index 25d1181..50a2d61 100644
--- a/theories/logatom/treiber2.v
+++ b/theories/logatom/treiber2.v
@@ -260,13 +260,13 @@ Proof.
(* We can now perform the load, and get rid of the modality. *)
wp_load. iModIntro. iSplitL "Hl Hγ● HPhys"; first by eauto 10 with iFrame.
(* We then resume stepping through the program, and focus on the CAS. *)
- wp_alloc r as "Hr". wp_inj. wp_bind (CAS _ _ _)%E.
+ wp_alloc r as "Hr". wp_inj. wp_bind (CmpXchg _ _ _)%E.
(* Now, we need to use the invariant again to gain information on [ℓ]. *)
iInv "HInv" as (ys) ">[HPhys Hγ●]". iDestruct "HPhys" as (u) "[Hl HPhys]".
(* We now reason by case on the success/failure of the CAS. *)
destruct (decide (u = w)) as [[= ->]|NE].
- (* The CAS succeeded. *)
- wp_cas_suc. { case w; left; done. (* Administrative stuff. *) }
+ wp_cmpxchg_suc. { case w; left; done. (* Administrative stuff. *) }
(* This was the linearization point. We access the preconditon. *)
iMod "AU" as (zs) "[Hγ◯ [_ HClose]]".
(* Use agreement on ressource [γ] to learn [zs = ys]. *)
@@ -278,14 +278,14 @@ Proof.
(* We can eliminate the modality. *)
iModIntro. iSplitR "H"; first by eauto 10 with iFrame.
(* And conclude the proof easily, after some computation steps. *)
- wp_if. iExact "H".
+ wp_pures. iExact "H".
- (* The CAS failed. *)
- wp_cas_fail. { case u, w; simpl; congruence. }
+ wp_cmpxchg_fail. { case u, w; simpl; congruence. }
{ case u, w; simpl; eauto. (* Administrative stuff. *) }
(* We can eliminate the modality. *)
iModIntro. iSplitL "Hγ● Hl HPhys"; first by eauto 10 with iFrame.
(* And conclude the proof by induction hypothesis. *)
- wp_if. iApply "IH". iExact "AU".
+ wp_pures. iApply "IH". iExact "AU".
Qed.
(** As for [push_stack] the specification of [pop_stack] depends on a location
@@ -315,7 +315,7 @@ Proof.
iModIntro. iSplitL "Hl Hγ● HPhys1"; first by eauto 10 with iFrame.
(* We continue stepping through the program, and focus on the CAS. *)
wp_let. wp_match. iDestruct "HPhys2" as (r q) "[Hw HP]".
- wp_load. wp_let. wp_proj. wp_bind (CAS _ _ _)%E.
+ wp_load. wp_let. wp_proj. wp_bind (CmpXchg _ _ _)%E.
(* We need to use the invariant again to gain information on [ℓ]. *)
iInv "HInv" as (ys) ">[H Hγ●]".
unfold phys_stack. iDestruct "H" as (u) "[Hl HPhys]".
@@ -324,7 +324,7 @@ Proof.
(* We reason by case on the success/failure of the CAS. *)
destruct (decide (u = Some w)) as [[= ->]|Hx].
* (* The CAS succeeded, so this is the linearization point. *)
- wp_cas_suc.
+ wp_cmpxchg_suc.
(* The list [ys] must be non-empty, otherwise the proof is trivial. *)
destruct ys; first done.
(* We access the precondition, prior to performing an update. *)
@@ -341,13 +341,13 @@ Proof.
(* Eliminate the modality. *)
iModIntro. iSplitR "HΦ"; first by eauto 10 with iFrame.
(* And conclude the proof. *)
- wp_if. wp_proj. wp_inj. iExact "HΦ".
+ wp_pures. iExact "HΦ".
* (* The CAS failed. *)
- wp_cas_fail. { intro H. apply Hx. destruct u; inversion H; done. }
+ wp_cmpxchg_fail. { intro H. apply Hx. destruct u; inversion H; done. }
(* We can eliminate the modality. *)
iModIntro. iSplitR "AU"; first by eauto 10 with iFrame.
(* And conclude the proof using the induction hypothesis. *)
- wp_if. iApply "IH". iExact "AU".
+ wp_pures. iApply "IH". iExact "AU".
- (* The stack is empty, the load was the linearization point, we can hence
commit (without updating the stack). So we access the precondition. *)
iClear "HPhys1 HPhys2". iMod "AU" as (xs) "[Hγ◯ [_ HClose]]".
@@ -358,7 +358,7 @@ Proof.
(* We finally eliminate the modality and conclude the proof by taking some
computation steps, and using our hypothesis. *)
iModIntro. iSplitR "HΦ"; first by eauto 10 with iFrame.
- wp_let. wp_match. wp_inj. iExact "HΦ".
+ wp_pures. iExact "HΦ".
Qed.
End treiber_stack.
diff --git a/theories/logrel_heaplang/ltyping.v b/theories/logrel_heaplang/ltyping.v
index d260fe9..a442e29 100644
--- a/theories/logrel_heaplang/ltyping.v
+++ b/theories/logrel_heaplang/ltyping.v
@@ -374,15 +374,16 @@ Section types_properties.
iInv (tyN.@l) as (v) "[>Hl Hv]"; iDestruct "Hv" as (n') "> ->".
wp_faa. iModIntro. eauto 10.
Qed.
- Lemma ltyped_cas Γ A e1 e2 e3 :
+ Lemma ltyped_cmpxchg Γ A e1 e2 e3 :
LTyUnboxed A →
- (Γ ⊨ e1 : ref A) -∗ (Γ ⊨ e2 : A) -∗ (Γ ⊨ e3 : A) -∗ Γ ⊨ CAS e1 e2 e3 : lty_bool.
+ (Γ ⊨ e1 : ref A) -∗ (Γ ⊨ e2 : A) -∗ (Γ ⊨ e3 : A) -∗ Γ ⊨ CmpXchg e1 e2 e3 : A * lty_bool.
Proof.
intros. iIntros "#H1 #H2 #H3" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H3 [//])"); iIntros (w3) "HA3".
wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "HA2".
iDestruct (lty_unboxed with "HA2") as %?.
wp_apply (wp_wand with "(H1 [//])"); iIntros (w1); iDestruct 1 as (l ->) "#?".
- iInv (tyN.@l) as (v) "[>Hl Hv]". wp_cas as ?|?; eauto 10.
+ iInv (tyN.@l) as (v) "[>Hl #Hv]". wp_cmpxchg as ?|?; iModIntro;
+ (iSplitL; [by eauto 12 with iFrame | iExists _, _; eauto]).
Qed.
End types_properties.
diff --git a/theories/spanning_tree/spanning.v b/theories/spanning_tree/spanning.v
index 98a7f21..32e75bb 100644
--- a/theories/spanning_tree/spanning.v
+++ b/theories/spanning_tree/spanning.v
@@ -62,6 +62,7 @@ Section Helpers.
{ iNext. unfold graph_inv at 2. iExists _; iFrame; auto. }
iModIntro. wp_proj. wp_let.
destruct u as [u1 u2]; simpl.
+ wp_bind (CmpXchg _ _ _).
iMod (cinv_open _ graphN with "Hgr key")
as "(>Hinv & key & Hclose)"; first done.
unfold graph_inv at 2.
@@ -75,7 +76,7 @@ Section Helpers.
rewrite Hil2' in Hil2; inversion Hil2; subst.
iDestruct (auth_own_graph_valid with "Hi1") as %Hvl.
destruct u as [[] uch].
- - wp_cas_fail.
+ - wp_cmpxchg_fail.
iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3";
eauto.
{ iFrame. iExists _; eauto. iSplitR; eauto. by iExists _; iFrame. }
@@ -83,9 +84,9 @@ Section Helpers.
{ by eapply in_dom_of_graph. }
iMod ("Hclose" with "[Hi1 Hi2 Hi3]") as "_".
{ iNext. unfold graph_inv at 2. iExists _; iFrame; auto. }
- iModIntro. iFrame. iRight; by iFrame.
+ iModIntro. iFrame. wp_pures. iRight; by iFrame.
- (* CAS succeeds *)
- wp_cas_suc.
+ wp_cmpxchg_suc.
iMod (mark_graph _ _ x uch with "[Hi1 Hx]") as "[Hi1 Hx]"; try by iFrame.
{ apply (proj1 (not_elem_of_dom (D := gset loc) G' x)).
intros Hid. eapply in_dom_of_graph in Hid; eauto; tauto. }
@@ -100,7 +101,7 @@ Section Helpers.
rewrite dom_op dom_singleton_L ?gset_op_union (comm union); iFrame.
iPureIntro.
{ by apply mark_strict_subgraph. }
- + iModIntro. iLeft; iSplit; trivial. iExists _; iFrame.
+ + iModIntro. wp_pures. iLeft; iSplit; trivial. iExists _; iFrame.
iPureIntro; eapply of_graph_unmarked; eauto.
Qed.
--
GitLab