Merge branch 'master' of https://gitlab.mpi-sws.org/iris/examples

.gitlab-ci.yml

@@ -23,6 +23,7 @@ variables:
   except:
   - triggers
   - schedules
+  - api
 
 ## Build jobs
 
@@ -43,3 +44,4 @@ build-iris.dev:
   only:
   - triggers
   - schedules
+  - api

README.md

@@ -53,8 +53,11 @@ This repository contains the following case studies:
 * [logrel_heaplang](theories/logrel_heaplang): A unary logical relation for
   semantic typing of heap lang.
 * [logatom](theories/logrel_heaplang): Proofs of various logically atomic specifications:
-  - Elimination Stack
-  - Treiber Stack (by Zhen Zhang)
+  - Elimination Stack (by Ralf Jung)
+  - Conditional increment (inspired by [this paper](https://people.mpi-sws.org/~dreyer/papers/relcon/paper.pdf)) and RDCSS (as in [this paper](https://timharris.uk/papers/2002-disc.pdf)) (by Marianna Rapoport, Rodolphe Lepigre and Gaurav Parthasarathy)
+  - [Herlihy-Wing-Queue](https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf)
+  - Atomic Snapshot (by Marianna Rapoport)
+  - Treiber Stack (by Zhen Zhang, and another version by Rodolphe Lepigre)
   - Flat Combiner (by Zhen Zhang, also see [this archived documentation](https://gitlab.mpi-sws.org/FP/iris-atomic/tree/master/docs))
 * [spanning-tree](theories/spanning_tree): Proof of a concurrent spanning tree
   algorithm by Amin Timany.

_CoqProject

@@ -93,6 +93,7 @@ theories/hocap/lib/oneshot.v
 theories/hocap/concurrent_runners.v
 theories/hocap/parfib.v
 
+theories/logatom/lib/gc.v
 theories/logatom/treiber.v
 theories/logatom/treiber2.v
 theories/logatom/elimination_stack/hocap_spec.v
@@ -108,3 +109,8 @@ theories/logatom/snapshot/spec.v
 theories/logatom/snapshot/atomic_snapshot.v
 theories/logatom/conditional_increment/spec.v
 theories/logatom/conditional_increment/cinc.v
+theories/logatom/rdcss/rdcss.v
+theories/logatom/rdcss/spec.v
+theories/logatom/proph_erasure.v
+theories/logatom/herlihy_wing_queue/spec.v
+theories/logatom/herlihy_wing_queue/hwq.v

opam

 opam-version: "1.2"
 name: "coq-iris-examples"
 maintainer: "Ralf Jung <jung@mpi-sws.org>"
-authors: "The Iris Team"
+authors: "The Iris Team and Contributors"
 homepage: "http://iris-project.org/"
 bug-reports: "https://gitlab.mpi-sws.org/FP/iris-examples/issues"
 dev-repo: "https://gitlab.mpi-sws.org/FP/iris-examples.git"
@@ -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-11.8.a51fa3cf") | (= "dev") }
+  "coq-iris" { (= "dev.2019-08-14.0.ffccb508") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]

theories/barrier/example_joining_existentials.v

@@ -6,16 +6,16 @@ From iris.proofmode Require Import tactics.
 From iris_examples.barrier Require Import proof specification.
 Set Default Proof Using "Type".
 
-Definition one_shotR (Σ : gFunctors) (F : cFunctor) :=
-  csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ) _).
+Definition one_shotR (Σ : gFunctors) (F : oFunctor) :=
+  csumR (exclR unitO) (agreeR $ laterO $ F (iPreProp Σ) _).
 Definition Pending {Σ F} : one_shotR Σ F := Cinl (Excl ()).
-Definition Shot {Σ} {F : cFunctor} (x : F (iProp Σ) _) : one_shotR Σ F :=
-  Cinr $ to_agree $ Next $ cFunctor_map F (iProp_fold, iProp_unfold) x.
+Definition Shot {Σ} {F : oFunctor} (x : F (iProp Σ) _) : one_shotR Σ F :=
+  Cinr $ to_agree $ Next $ oFunctor_map F (iProp_fold, iProp_unfold) x.
 
-Class oneShotG (Σ : gFunctors) (F : cFunctor) :=
+Class oneShotG (Σ : gFunctors) (F : oFunctor) :=
   one_shot_inG :> inG Σ (one_shotR Σ F).
-Definition oneShotΣ (F : cFunctor) : gFunctors :=
-  #[ GFunctor (csumRF (exclRF unitC) (agreeRF (▶ F))) ].
+Definition oneShotΣ (F : oFunctor) : gFunctors :=
+  #[ GFunctor (csumRF (exclRF unitO) (agreeRF (▶ F))) ].
 Instance subG_oneShotΣ {Σ F} : subG (oneShotΣ F) Σ → oneShotG Σ F.
 Proof. solve_inG. Qed.
 
@@ -59,12 +59,12 @@ Proof.
   iAssert (▷ (x ≡ x'))%I as "Hxx".
   { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
     rewrite own_valid csum_validI /= agree_validI agree_equivI bi.later_equivI /=.
-    rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id.
-    assert (HF : cFunctor_map F (cid, cid) ≡ cFunctor_map F (iProp_fold (Σ:=Σ) ◎ iProp_unfold, iProp_fold (Σ:=Σ) ◎ iProp_unfold)).
+    rewrite -{2}[x]oFunctor_id -{2}[x']oFunctor_id.
+    assert (HF : oFunctor_map F (cid, cid) ≡ oFunctor_map F (iProp_fold (Σ:=Σ) ◎ iProp_unfold, iProp_fold (Σ:=Σ) ◎ iProp_unfold)).
     { apply ne_proper; first by apply _.
       by split; intro; simpl; symmetry; apply iProp_fold_unfold. }
     rewrite (HF x). rewrite (HF x').
-    rewrite !cFunctor_compose. iNext. by iRewrite "Hγ2". }
+    rewrite !oFunctor_compose. iNext. by iRewrite "Hγ2". }
   iNext. iRewrite -"Hxx" in "Hx'".
   iExists x; iFrame "Hγ". iApply (Ψ_join with "Hx Hx'").
 Qed.

theories/barrier/specification.v

@@ -18,7 +18,7 @@ Lemma barrier_spec (N : namespace) :
     (∀ l P Q, recv l (P ∗ Q) ={↑N}=> recv l P ∗ recv l Q) ∧
     (∀ l P Q, (P -∗ Q) -∗ recv l P -∗ recv l Q).
 Proof.
-  exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)).
+  exists (λ l, OfeMor (recv N l)), (λ l, OfeMor (send N l)).
   split_and?; simpl.
   - iIntros (P) "!# _". iApply (newbarrier_spec _ P with "[]"); [done..|].
     iNext. eauto.

theories/concurrent_stacks/concurrent_stack1.v

@@ -36,9 +36,19 @@ Section stacks.
     iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
   Qed.
 
-  Definition is_list_pre (P : val → iProp Σ) (F : val -c> iProp Σ) :
-     val -c> iProp Σ := λ v,
-    (v ≡ NONEV ∨ ∃ (l : loc) (h t : val), ⌜v ≡ SOMEV #l⌝ ∗ l ↦{-} (h, t)%V ∗ P h ∗ ▷ F t)%I.
+  Definition oloc_to_val (ol: option loc) : val :=
+    match ol with
+    | None => NONEV
+    | Some loc => SOMEV (#loc)
+    end.
+  Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
+  Proof. intros [|][|]; simpl; congruence. Qed.
+
+  Definition is_list_pre (P : val → iProp Σ) (F : option loc -d> iProp Σ) :
+     option loc -d> iProp Σ := λ v, match v with
+     | None => True
+     | Some l => ∃ (h : val) (t : option loc), l ↦{-} (h, oloc_to_val t)%V ∗ P h ∗ ▷ F t
+     end%I.
 
   Local Instance is_list_contr (P : val → iProp Σ) : Contractive (is_list_pre P).
   Proof.
@@ -58,28 +68,22 @@ Section stacks.
     rewrite is_list_eq. apply (fixpoint_unfold (is_list_pre P)).
   Qed.
 
-  (* TODO: shouldn't have to explicitly return is_list *)
-  Lemma is_list_unboxed (P : val → iProp Σ) v :
-      is_list P v -∗ ⌜val_is_unboxed v⌝ ∗ is_list P v.
-  Proof.
-    iIntros "Hstack"; iSplit; last done;
-    iDestruct (is_list_unfold with "Hstack") as "[->|Hstack]";
-    last iDestruct "Hstack" as (l h t) "(-> & _)"; done.
-  Qed.
-
-  Lemma is_list_disj (P : val → iProp Σ) v :
-    is_list P v -∗ is_list P v ∗ (⌜v ≡ NONEV⌝ ∨ ∃ (l : loc) h t, ⌜v ≡ SOMEV #l%V⌝ ∗ l ↦{-} (h, t)%V).
+  Lemma is_list_dup (P : val → iProp Σ) v :
+    is_list P v -∗ is_list P v ∗ match v with
+      | None => True
+      | Some l => ∃ h t, l ↦{-} (h, oloc_to_val t)%V
+      end.
   Proof.
-    iIntros "Hstack".
-    iDestruct (is_list_unfold with "Hstack") as "[%|Hstack]"; simplify_eq.
-    - rewrite is_list_unfold; iSplitR; [iLeft|]; eauto.
-    - iDestruct "Hstack" as (l h t) "(% & Hl & Hlist)".
-      iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]"; simplify_eq.
-      rewrite (is_list_unfold _ (InjRV _)); iSplitR "Hl2"; iRight; iExists _, _, _; by iFrame.
+    iIntros "Hstack". iDestruct (is_list_unfold with "Hstack") as "Hstack".
+    destruct v as [l|].
+    - iDestruct "Hstack" as (h t) "(Hl & Hlist)".
+      iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
+      rewrite (is_list_unfold _ (Some _)); iSplitR "Hl2"; iExists _, _; by iFrame.
+    - rewrite is_list_unfold; iSplitR; eauto.
   Qed.
 
   Definition stack_inv P v :=
-    (∃ l v', ⌜v = #l⌝ ∗ l ↦ v' ∗ is_list P v')%I.
+    (∃ l ol', ⌜v = #l⌝ ∗ l ↦ oloc_to_val ol' ∗ is_list P ol')%I.
 
   Definition is_stack (P : val → iProp Σ) v :=
     inv N (stack_inv P v).
@@ -92,8 +96,8 @@ Section stacks.
     wp_lam.
     wp_alloc ℓ as "Hl".
     iMod (inv_alloc N ⊤ (stack_inv P #ℓ) with "[Hl]") as "Hinv".
-    { iNext; iExists ℓ, NONEV; iFrame;
-      by iSplit; last (iApply is_list_unfold; iLeft). }
+    { iNext; iExists ℓ, None; iFrame;
+      by iSplit; last (iApply is_list_unfold). }
     by iApply "Hpost".
   Qed.
 
@@ -107,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 [ -> |].
-    - iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
-      wp_cas_suc.
+    destruct (decide (v' = v'')) as [->|Hne].
+    - wp_cmpxchg_suc. { destruct v''; left; done. }
       iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
-      { iNext; iExists _, (InjRV #ℓ'); iFrame; iSplit; first done;
-        rewrite (is_list_unfold _ (InjRV _)). iRight; iExists _, _, _; iFrame; eauto. }
+      { iNext; iExists _, (Some ℓ'); iFrame; iSplit; first done;
+        rewrite (is_list_unfold _ (Some _)). iExists _, _; iFrame; eauto. }
       iModIntro.
-      wp_if.
+      wp_pures.
       by iApply "HΦ".
-    - iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
-      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.
 
@@ -134,41 +138,40 @@ Section stacks.
     iLöb as "IH".
     wp_lam. wp_bind (Load _).
     iInv N as (ℓ v') "(>% & Hl & Hlist)" "Hclose"; subst.
+    iDestruct (is_list_dup with "Hlist") as "[Hlist Hlist2]".
     wp_load.
-    iDestruct (is_list_disj with "Hlist") as "[Hlist Hdisj]".
     iMod ("Hclose" with "[Hl Hlist]") as "_".
     { iNext; iExists _, _; by iFrame. }
     iModIntro.
-    iDestruct "Hdisj" as "[-> | Heq]".
+    destruct v' as [l|]; last first.
     - wp_match.
       iApply "HΦ"; by iLeft.
-    - iDestruct "Heq" as (l h t) "[-> Hl]".
-      wp_match. wp_bind (Load _).
+    - wp_match. wp_bind (Load _).
       iInv N as (ℓ' v') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
-      iDestruct "Hl" as (q) "Hl".
+      iDestruct "Hlist2" as (???) "Hl".
       wp_load.
       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'' = InjRV #l)) as [-> |].
+      destruct (decide (v'' = (Some l))) as [-> |].
       * rewrite is_list_unfold.
-        iDestruct "Hlist" as "[>% | H]"; first done.
-        iDestruct "H" as (ℓ''' h' t') "(>% & Hl'' & HP & Hlist)"; simplify_eq.
+        iDestruct "Hlist" as (h' t') "(Hl'' & HP & Hlist)".
         iDestruct "Hl''" as (q') "Hl''".
-        wp_cas_suc.
-        iDestruct (mapsto_agree with "Hl'' Hl") as "%"; simplify_eq.
+        simpl.
+        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 h; by iFrame.
-      * wp_cas_fail.
+        iApply ("HΦ" with "[HP]"); iRight; iExists _; by iFrame.
+      * 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.

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.
@@ -246,9 +246,19 @@ Section stack_works.
     iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
   Qed.
 
-  Definition is_list_pre (P : val → iProp Σ) (F : val -c> iProp Σ) :
-     val -c> iProp Σ := λ v,
-    (v ≡ NONEV ∨ ∃ (l : loc) (h t : val), ⌜v ≡ SOMEV #l⌝ ∗ l ↦{-} (h, t)%V ∗ P h ∗ ▷ F t)%I.
+  Definition oloc_to_val (ol: option loc) : val :=
+    match ol with
+    | None => NONEV
+    | Some loc => SOMEV (#loc)
+    end.
+  Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
+  Proof. intros [|][|]; simpl; congruence. Qed.
+
+  Definition is_list_pre (P : val → iProp Σ) (F : option loc -d> iProp Σ) :
+     option loc -d> iProp Σ := λ v, match v with
+     | None => True
+     | Some l => ∃ (h : val) (t : option loc), l ↦{-} (h, oloc_to_val t)%V ∗ P h ∗ ▷ F t
+     end%I.
 
   Local Instance is_list_contr (P : val → iProp Σ) : Contractive (is_list_pre P).
   Proof.
@@ -268,27 +278,21 @@ Section stack_works.
     rewrite is_list_eq. apply (fixpoint_unfold (is_list_pre P)).
   Qed.
 
-  (* TODO: shouldn't have to explicitly return is_list *)
-  Lemma is_list_unboxed (P : val → iProp Σ) v :
-      is_list P v -∗ ⌜val_is_unboxed v⌝ ∗ is_list P v.
-  Proof.
-    iIntros "Hstack"; iSplit; last done;
-    iDestruct (is_list_unfold with "Hstack") as "[->|Hstack]";
-    last iDestruct "Hstack" as (l h t) "(-> & _)"; done.
-  Qed.
-
-  Lemma is_list_disj (P : val → iProp Σ) v :
-    is_list P v -∗ is_list P v ∗ (⌜v ≡ NONEV⌝ ∨ ∃ (l : loc) h t, ⌜v ≡ SOMEV #l%V⌝ ∗ l ↦{-} (h, t)%V).
+  Lemma is_list_dup (P : val → iProp Σ) v :
+    is_list P v -∗ is_list P v ∗ match v with
+      | None => True
+      | Some l => ∃ h t, l ↦{-} (h, oloc_to_val t)%V
+      end.
   Proof.
-    iIntros "Hstack".
-    iDestruct (is_list_unfold with "Hstack") as "[%|Hstack]"; simplify_eq.
-    - rewrite is_list_unfold; iSplitR; [iLeft|]; eauto.
-    - iDestruct "Hstack" as (l h t) "(% & Hl & Hlist)".
-      iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]"; simplify_eq.
-      rewrite (is_list_unfold _ (InjRV _)); iSplitR "Hl2"; iRight; iExists _, _, _; by iFrame.
+    iIntros "Hstack". iDestruct (is_list_unfold with "Hstack") as "Hstack".
+    destruct v as [l|].
+    - iDestruct "Hstack" as (h t) "(Hl & Hlist)".
+      iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
+      rewrite (is_list_unfold _ (Some _)); iSplitR "Hl2"; iExists _, _; by iFrame.
+    - rewrite is_list_unfold; iSplitR; eauto.
   Qed.
 
-  Definition stack_inv P l := (∃ v, l ↦ v ∗ is_list P v)%I.
+  Definition stack_inv P l := (∃ v, l ↦ oloc_to_val v ∗ is_list P v)%I.
   Definition is_stack P v :=
     (∃ mailbox l, ⌜v = (mailbox, #l)%V⌝ ∗ is_mailbox Nmailbox P mailbox ∗ inv N (stack_inv P l))%I.
 
@@ -302,7 +306,7 @@ Section stack_works.
     wp_apply mk_mailbox_works; first done.
     iIntros (mailbox) "#Hmailbox".
     iMod (inv_alloc N _ (stack_inv P l) with "[Hl]") as "#Hinv".
-    { by iNext; iExists _; iFrame; rewrite is_list_unfold; iLeft. }
+    { iNext; iExists None; iFrame. rewrite is_list_unfold. done. }
     wp_pures; iModIntro; iApply "Hpost"; iExists _, _; auto.
   Qed.
 
@@ -322,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 [ -> |].
-      * iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
-        wp_cas_suc.
+      * wp_cmpxchg_suc. { destruct list; left; done. }
         iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
-        { iNext; iExists (SOMEV _); iFrame.
-          rewrite (is_list_unfold _ (InjRV _)). iRight; iExists _, _, _; iFrame; eauto. }
+        { iNext; iExists (Some _); iFrame.
+          rewrite (is_list_unfold _ (Some _)). iExists _, _; iFrame; eauto. }
         iModIntro.
-        wp_if.
+        wp_pures.
         by iApply "HΦ".
-      * iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
-        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Φ".
@@ -355,40 +359,38 @@ Section stack_works.
     - wp_match. wp_bind (Load _).
       iInv N as (list) "[Hl Hlist]" "Hclose".
       wp_load.
-      iDestruct (is_list_disj with "Hlist") as "[Hlist Hdisj]".
+      iDestruct (is_list_dup with "Hlist") as "[Hlist Hlist2]".
       iMod ("Hclose" with "[Hl Hlist]") as "_".
       { iNext; iExists _; by iFrame. }
       iModIntro.
-      iDestruct "Hdisj" as "[-> | Heq]".
+      destruct list as [list|]; last first.
       * wp_match.
         iApply "HΦ"; by iLeft.
-      * iDestruct "Heq" as (l' h t) "[-> Hl']".
-        wp_match. wp_bind (Load _).
+      * wp_match. wp_bind (Load _).
         iInv N as (v') "[>Hl Hlist]" "Hclose".
-        iDestruct "Hl'" as (q) "Hl'".
+        iDestruct "Hlist2" as (???) "Hl'".
         wp_load.
         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'' = InjRV #l')) as [-> |].
+        destruct (decide (v'' = Some list)) as [-> |].
         + rewrite is_list_unfold.
-          iDestruct "Hlist" as "[>% | H]"; first done.
-          iDestruct "H" as (l'' h' t') "(>% & Hl'' & HP & Hlist)"; simplify_eq.
+          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 h; by iFrame.
-        + wp_cas_fail.
+          iApply ("HΦ" with "[HP]"); iRight; iExists _; by iFrame.
+        + 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.

theories/concurrent_stacks/concurrent_stack3.v

@@ -44,47 +44,51 @@ Section stack_works.
     iApply (mapsto_agree with "H1 H2").
   Qed.
 
+  Definition oloc_to_val (ol: option loc) : val :=
+    match ol with
+    | None => NONEV
+    | Some loc => SOMEV (#loc)
+    end.
+  Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
+  Proof. intros [|][|]; simpl; congruence. Qed.
+
   Fixpoint is_list xs v : iProp Σ :=
-    (match xs with
-     | [] => ⌜v = NONEV⌝
-     | x :: xs => ∃ l (t : val), ⌜v = SOMEV #l%V⌝ ∗ l ↦{-} (x, t)%V ∗ is_list xs t
+    (match xs, v with
+     | [], None => True
+     | x :: xs, Some l => ∃ t, l ↦{-} (x, oloc_to_val t)%V ∗ is_list xs t
+     | _, _ => False
      end)%I.
 
-  Lemma is_list_disj xs v :
-    is_list xs v -∗ is_list xs v ∗ (⌜v = NONEV⌝ ∨ ∃ l (h t : val), ⌜v = SOMEV #l⌝ ∗ l ↦{-} (h, t)%V).
+  Lemma is_list_dup xs v :
+    is_list xs v -∗ is_list xs v ∗ match v with
+      | None => True
+      | Some l => ∃ h t, l ↦{-} (h, oloc_to_val t)%V
+      end.
   Proof.
-    destruct xs; auto.
-    iIntros "H"; iDestruct "H" as (l t) "(-> & Hl & Hstack)".
+    destruct xs, v; simpl; auto; first by iIntros "[]".
+    iIntros "H"; iDestruct "H" as (t) "(Hl & Hstack)".
     iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
-    iSplitR "Hl2"; first by (iExists _, _; iFrame). iRight; auto.
-  Qed.
-
-  Lemma