Organize dependencies

Makefile.coq

@@ -97,12 +97,15 @@ endif
 ######################
 
 VFILES:=atomic.v\
+  sync.v\
+  atomic_incr.v\
   simple_sync.v\
   flat.v\
   atomic_sync.v\
   treiber.v\
   misc.v\
-  evmap.v
+  evmap.v\
+  peritem.v
 
 ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
 -include $(addsuffix .d,$(VFILES))

_CoqProject

 -Q . iris_atomic
 atomic.v
+sync.v
+atomic_incr.v
 simple_sync.v
 flat.v
 atomic_sync.v
 treiber.v
 misc.v
 evmap.v
+peritem.v

atomic.v

 From iris.program_logic Require Export hoare weakestpre pviewshifts ownership.
-From iris.algebra Require Import upred_big_op.
 From iris.prelude Require Export coPset.
-From iris.proofmode Require Import tactics.
 Import uPred.
 
 Section atomic.
@@ -23,108 +21,3 @@ Section atomic.
 
   Arguments atomic_triple {_} _ _ _ _.
 End atomic.
-
-From iris.heap_lang Require Export lang proofmode notation.
-
-Section incr.
-  Context `{!heapG Σ} (N : namespace).
-
-  Definition incr: val :=
-    rec: "incr" "l" :=
-       let: "oldv" := !"l" in
-       if: CAS "l" "oldv" ("oldv" + #1)
-         then "oldv" (* return old value if success *)
-         else "incr" "l".
-
-  Global Opaque incr.
-
-  (* TODO: Can we have a more WP-style definition and avoid the equality? *)
-  Definition incr_triple (l: loc) :=
-    atomic_triple _ (fun (v: Z) => l ↦ #v)%I
-                    (fun v ret => ret = #v ★ l ↦ #(v + 1))%I
-                    (nclose heapN)
-                    ⊤
-                    (incr #l).
-
-  Lemma incr_atomic_spec: ∀ (l: loc), heapN ⊥ N → heap_ctx ⊢ incr_triple l.
-  Proof.
-    iIntros (l HN) "#?".
-    rewrite /incr_triple.
-    rewrite /atomic_triple.
-    iIntros (P Q) "#Hvs".
-    iLöb as "IH".
-    iIntros "!# HP".
-    wp_rec.
-    wp_bind (! _)%E.
-    iVs ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
-    wp_load.
-    iVs ("Hvs'" with "Hl") as "HP".
-    iVsIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
-    iVs ("Hvs" with "HP") as (x') "[Hl Hvs']".
-    destruct (decide (x = x')).
-    - subst.
-      iDestruct "Hvs'" as "[_ Hvs']".
-      iSpecialize ("Hvs'" $! #x').
-      wp_cas_suc.
-      iVs ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
-      iVsIntro. wp_if. iVsIntro. by iExists x'.
-    - iDestruct "Hvs'" as "[Hvs' _]".
-      wp_cas_fail.
-      iVs ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
-      iVsIntro. wp_if. by iApply "IH".
-  Qed.
-End incr.
-
-From iris.heap_lang.lib Require Import par.
-
-Section user.
-  Context `{!heapG Σ, !spawnG Σ} (N : namespace).
-
-  Definition incr_2 : val :=
-    λ: "x",
-       let: "l" := ref "x" in
-       incr "l" || incr "l";;
-       !"l".
-
-  (* prove that incr is safe w.r.t. data race. TODO: prove a stronger post-condition *)
-  Lemma incr_2_safe:
-    ∀ (x: Z), heapN ⊥ N -> heap_ctx ⊢ WP incr_2 #x {{ _, True }}.
-  Proof.
-    iIntros (x HN) "#Hh".
-    rewrite /incr_2.
-    wp_let.
-    wp_alloc l as "Hl".
-    iVs (inv_alloc N _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; first eauto.
-    wp_let.
-    wp_bind (_ || _)%E.
-    iApply (wp_par (λ _, True%I) (λ _, True%I)).
-    iFrame "Hh".
-    (* prove worker triple *)
-    iDestruct (incr_atomic_spec N l with "Hh") as "Hincr"=>//.
-    rewrite /incr_triple /atomic_triple.
-    iSpecialize ("Hincr"  $! True%I (fun _ _ => True%I) with "[]").
-    - iIntros "!# _".
-      (* open the invariant *)
-      iInv N as (x') ">Hl'" "Hclose".
-      (* mask magic *)
-      iApply pvs_intro'.
-      { apply ndisj_subseteq_difference; auto. }
-      iIntros "Hvs".
-      iExists x'.
-      iFrame "Hl'".
-      iSplit.
-      + (* provide a way to rollback *)
-        iIntros "Hl'".
-        iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
-      + (* provide a way to commit *)
-        iIntros (v) "[Heq Hl']".
-        iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
-    - iDestruct "Hincr" as "#HIncr".
-      iSplitL; [|iSplitL]; try (iApply wp_wand_r;iSplitL; [by iApply "HIncr"|auto]).
-      iIntros (v1 v2) "_ !>".
-      wp_seq.
-      iInv N as (x') ">Hl" "Hclose".
-      wp_load.
-      iApply "Hclose". eauto.
-  Qed.
-End user.

atomic_incr.v

+From iris.heap_lang Require Export lang proofmode notation.
+From iris_atomic Require Import atomic.
+
+Section incr.
+  Context `{!heapG Σ} (N : namespace).
+
+  Definition incr: val :=
+    rec: "incr" "l" :=
+       let: "oldv" := !"l" in
+       if: CAS "l" "oldv" ("oldv" + #1)
+         then "oldv" (* return old value if success *)
+         else "incr" "l".
+
+  Global Opaque incr.
+
+  (* TODO: Can we have a more WP-style definition and avoid the equality? *)
+  Definition incr_triple (l: loc) :=
+    atomic_triple _ (fun (v: Z) => l ↦ #v)%I
+                    (fun v ret => ret = #v ★ l ↦ #(v + 1))%I
+                    (nclose heapN)
+                    ⊤
+                    (incr #l).
+
+  Lemma incr_atomic_spec: ∀ (l: loc), heapN ⊥ N → heap_ctx ⊢ incr_triple l.
+  Proof.
+    iIntros (l HN) "#?".
+    rewrite /incr_triple.
+    rewrite /atomic_triple.
+    iIntros (P Q) "#Hvs".
+    iLöb as "IH".
+    iIntros "!# HP".
+    wp_rec.
+    wp_bind (! _)%E.
+    iVs ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
+    wp_load.
+    iVs ("Hvs'" with "Hl") as "HP".
+    iVsIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
+    iVs ("Hvs" with "HP") as (x') "[Hl Hvs']".
+    destruct (decide (x = x')).
+    - subst.
+      iDestruct "Hvs'" as "[_ Hvs']".
+      iSpecialize ("Hvs'" $! #x').
+      wp_cas_suc.
+      iVs ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
+      iVsIntro. wp_if. iVsIntro. by iExists x'.
+    - iDestruct "Hvs'" as "[Hvs' _]".
+      wp_cas_fail.
+      iVs ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
+      iVsIntro. wp_if. by iApply "IH".
+  Qed.
+End incr.
+
+From iris.heap_lang.lib Require Import par.
+
+Section user.
+  Context `{!heapG Σ, !spawnG Σ} (N : namespace).
+
+  Definition incr_2 : val :=
+    λ: "x",
+       let: "l" := ref "x" in
+       incr "l" || incr "l";;
+       !"l".
+
+  (* prove that incr is safe w.r.t. data race. TODO: prove a stronger post-condition *)
+  Lemma incr_2_safe:
+    ∀ (x: Z), heapN ⊥ N -> heap_ctx ⊢ WP incr_2 #x {{ _, True }}.
+  Proof.
+    iIntros (x HN) "#Hh".
+    rewrite /incr_2.
+    wp_let.
+    wp_alloc l as "Hl".
+    iVs (inv_alloc N _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; first eauto.
+    wp_let.
+    wp_bind (_ || _)%E.
+    iApply (wp_par (λ _, True%I) (λ _, True%I)).
+    iFrame "Hh".
+    (* prove worker triple *)
+    iDestruct (incr_atomic_spec N l with "Hh") as "Hincr"=>//.
+    rewrite /incr_triple /atomic_triple.
+    iSpecialize ("Hincr"  $! True%I (fun _ _ => True%I) with "[]").
+    - iIntros "!# _".
+      (* open the invariant *)
+      iInv N as (x') ">Hl'" "Hclose".
+      (* mask magic *)
+      iApply pvs_intro'.
+      { apply ndisj_subseteq_difference; auto. }
+      iIntros "Hvs".
+      iExists x'.
+      iFrame "Hl'".
+      iSplit.
+      + (* provide a way to rollback *)
+        iIntros "Hl'".
+        iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
+      + (* provide a way to commit *)
+        iIntros (v) "[Heq Hl']".
+        iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
+    - iDestruct "Hincr" as "#HIncr".
+      iSplitL; [|iSplitL]; try (iApply wp_wand_r;iSplitL; [by iApply "HIncr"|auto]).
+      iIntros (v1 v2) "_ !>".
+      wp_seq.
+      iInv N as (x') ">Hl" "Hclose".
+      wp_load.
+      iApply "Hclose". eauto.
+  Qed.
+End user.

atomic_pcas.v

 From iris.program_logic Require Export weakestpre hoare.
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Export lang proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import dec_agree frac.
-From iris_atomic Require Import atomic atomic_sync.
+From iris_atomic Require Import atomic_pcas'.
 Import uPred.
 
 Section atomic_pair.

atomic_sync.v

@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import dec_agree frac.
-From iris_atomic Require Import atomic misc.
+From iris_atomic Require Import atomic sync misc.
 
 Definition syncR := prodR fracR (dec_agreeR val).
 Class syncG Σ := sync_tokG :> inG Σ syncR.
@@ -39,22 +39,11 @@ Section atomic_sync.
                                heap_ctx ★ ϕ l g ★ □ α x ★
                                (∀ (v: val) (g': A), ϕ l g' -★ β x g g' v -★ |={E}=> Φ v)
                                ⊢ WP f' x @ E {{ Φ }} )}}.
-
-  Definition synced R (f' f: val) :=
-    (□ ∀ P Q (x: val), ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) → ({{ P x }} f' x {{ v, Q x v }}))%I.
-
-  Definition is_syncer (R: iProp Σ) (s: val) :=
-    (∀ (f : val), WP s f {{ f', synced R f' f }})%I.
-
-  Definition mk_syncer_spec (mk_syncer: val) :=
-    ∀ (R: iProp Σ) (Φ: val -> iProp Σ),
-      heapN ⊥ N →
-      heap_ctx ★ R ★ (∀ s, □ (is_syncer R s) -★ Φ s) ⊢ WP mk_syncer #() {{ Φ }}.
   
   Lemma atomic_spec (mk_syncer f_seq l: val) (ϕ: val → A → iProp Σ) α β Ei:
       ∀ (g0: A),
         heapN ⊥ N → seq_spec f_seq ϕ α β ⊤ →
-        mk_syncer_spec mk_syncer →
+        mk_syncer_spec N mk_syncer →
         heap_ctx ★ ϕ l g0
         ⊢ WP (sync mk_syncer) f_seq l {{ f, ∃ γ, gHalf γ g0 ★ ∀ x, □ atomic_triple' α β Ei ⊤ f x γ  }}.
   Proof.

flat.v

@@ -3,12 +3,12 @@ From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import auth upred frac agree excl dec_agree upred_big_op gset gmap.
-From iris_atomic Require Import misc atomic treiber atomic_sync evmap.
+From iris_atomic Require Import misc peritem sync evmap.
 
 Definition doOp : val :=
   λ: "p",
      match: !"p" with
-      InjL "req" => "p" <- InjR ((Fst "req") (Snd "req"))
+       InjL "req" => "p" <- InjR ((Fst "req") (Snd "req"))
      | InjR "_" => #()
      end.
 

pcas.v

@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import excl.
-Require Import iris_atomic.atomic_sync.
+Require Import iris_atomic.simple_sync.
 Import uPred.
 
 (* CAS, load and store to pair of locations *)

peritem.v

+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+From iris.algebra Require Import frac auth upred gmap dec_agree upred_big_op csum.
+From iris_atomic Require Export treiber misc evmap.
+
+Section defs.
+  Context `{heapG Σ, !evidenceG loc val unitR Σ} (N: namespace).
+  Context (R: val → iProp Σ) (γ: gname) `{∀ x, TimelessP (R x)}.
+
+  Definition allocated hd := (∃ q v, hd ↦{q} v)%I.
+
+  Definition evs := ev loc val γ.
+
+  Fixpoint is_list' (hd: loc) (xs: list val) : iProp Σ :=
+    match xs with
+    | [] => (∃ q, hd ↦{ q } NONEV)%I
+    | x :: xs => (∃ (hd': loc) q, hd ↦{q} SOMEV (x, #hd') ★ evs hd x ★ is_list' hd' xs)%I
+    end.
+
+  Lemma in_list' x xs:
+    ∀ hd, x ∈ xs →
+          is_list' hd xs
+          ⊢ ∃ (hd' hd'': loc) q, hd' ↦{q} SOMEV (x, #hd'') ★ evs hd' x.
+  Proof.
+    induction xs as [|x' xs' IHxs'].
+    - intros ? Hin. inversion Hin.
+    - intros hd Hin. destruct (decide (x = x')) as [->|Hneq].
+      + iIntros "Hls". simpl.
+        iDestruct "Hls" as (hd' q) "(? & ? & ?)".
+        iExists hd, hd', q. iFrame.
+      + assert (x ∈ xs') as Hin'; first set_solver.
+        iIntros "Hls". simpl.
+        iDestruct "Hls" as (hd' q) "(? & ? & ?)".
+        iApply IHxs'=>//.
+  Qed.
+
+  Definition perR' hd v v' := (v = ((∅: unitR), DecAgree v') ★ R v' ★ allocated hd)%I.
+  Definition perR  hd v := (∃ v', perR' hd v v')%I.
+  
+  Definition allR := (∃ m : evmapR loc val unitR, own γ (● m) ★ [★ map] hd ↦ v ∈ m, perR hd v)%I.
+
+  Definition is_stack' xs s := (∃ hd: loc, s ↦ #hd ★ is_list' hd xs ★ allR)%I.
+
+  Global Instance is_list'_timeless hd xs: TimelessP (is_list' hd xs).
+  Proof. generalize hd. induction xs; apply _. Qed.
+
+  Global Instance is_stack'_timeless xs s: TimelessP (is_stack' xs s).
+  Proof. apply _. Qed.
+
+  Lemma dup_is_list': ∀ xs hd,
+    heap_ctx ★ is_list' hd xs ⊢ |=r=> is_list' hd xs ★ is_list' hd xs.
+  Proof.
+    induction xs as [|y xs' IHxs'].
+    - iIntros (hd) "(#? & Hs)".
+      simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
+    - iIntros (hd) "(#? & Hs)". simpl.
+      iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & #Hev & Hs')".
+      iDestruct (IHxs' with "[Hs']") as "==>[Hs1 Hs2]"; first by iFrame.
+      iVsIntro. iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
+  Qed.
+
+  Lemma extract_is_list: ∀ xs hd,
+    heap_ctx ★ is_list' hd xs ⊢ |=r=> is_list' hd xs ★ is_list hd xs.
+  Proof.
+    induction xs as [|y xs' IHxs'].
+    - iIntros (hd) "(#? & Hs)".
+      simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
+    - iIntros (hd) "(#? & Hs)". simpl.
+      iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & Hev & Hs')".
+      iDestruct (IHxs' with "[Hs']") as "==>[Hs1 Hs2]"; first by iFrame.
+      iVsIntro. iSplitL "Hhd Hs1 Hev"; iExists hd', (q / 2)%Qp; by iFrame.
+  Qed.
+
+  Definition f_spec (xs: list val) (s: loc) (f: val) (Rf RI: iProp Σ) := (* Rf, RI is some frame *)
+    ∀ Φ (x: val),
+      heapN ⊥ N → x ∈ xs →
+      heap_ctx ★ inv N ((∃ xs, is_stack' xs s) ★ RI) ★  Rf ★ (Rf -★ Φ #())
+      ⊢ WP f x {{ Φ }}.
+End defs.
+
+Section proofs.
+  Context `{heapG Σ, !evidenceG loc val unitR Σ} (N: namespace).
+  Context (R: val → iProp Σ).
+
+Lemma new_stack_spec' Φ RI:
+    heapN ⊥ N →
+    heap_ctx ★ RI ★ (∀ γ s : loc, inv N ((∃ xs, is_stack' R γ xs s) ★ RI) -★ Φ #s)
+    ⊢ WP new_stack #() {{ Φ }}.
+  Proof.
+    iIntros (HN) "(#Hh & HR & HΦ)".
+    iVs (own_alloc (● (∅: evmapR loc val unitR) ⋅ ◯ ∅)) as (γ) "[Hm Hm']".
+    { apply auth_valid_discrete_2. done. }
+    wp_seq. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
+    wp_alloc s as "Hs".
+    iAssert ((∃ xs : list val, is_stack' R γ xs s) ★ RI)%I with "[-HΦ Hm']" as "Hinv".
+    { iFrame. iExists [], l. iFrame. simpl. iSplitL "Hl".
+      - eauto.
+      - iExists ∅. iSplitL. iFrame. by iApply (big_sepM_empty (fun hd v => perR R hd v)). }
+    iVs (inv_alloc N _ ((∃ xs : list val, is_stack' R γ xs s) ★ RI)%I with "[-HΦ Hm']") as "#?"; first eauto.
+    by iApply "HΦ".
+  Qed.
+    
+  Lemma iter_spec Φ γ s (Rf RI: iProp Σ):
+    ∀ xs hd (f: expr) (f': val),
+      heapN ⊥ N → f_spec N R γ xs s f' Rf RI → to_val f = Some f' →
+      heap_ctx ★ inv N ((∃ xs, is_stack' R γ xs s) ★ RI) ★
+      is_list' γ hd xs ★ Rf ★ (Rf -★ Φ #())
+      ⊢ WP (iter #hd) f {{ v, Φ v }}.
+  Proof.
+    induction xs as [|x xs' IHxs'].
+    - simpl. iIntros (hd f f' HN ? ?) "(#Hh & #? & Hxs1 & HRf & HΦ)".
+      iDestruct "Hxs1" as (q) "Hhd".
+      wp_rec. wp_value. iVsIntro. wp_let. wp_load. wp_match. by iApply "HΦ".
+    - simpl. iIntros (hd f f' HN Hf ?) "(#Hh & #? & Hxs1 & HRf & HΦ)".
+      iDestruct "Hxs1" as (hd2 q) "(Hhd & Hev & Hhd2)".
+      wp_rec. wp_value. iVsIntro. wp_let. wp_load. wp_match. wp_proj.
+      wp_bind (f' _). iApply Hf=>//; first set_solver. iFrame "#". iFrame. iIntros "HRf".
+      wp_seq. wp_proj. iApply (IHxs' with "[-]")=>//.
+      + rewrite /f_spec. iIntros (? ? ? ?) "(#? & #? & ? & ?)".
+        iApply Hf=>//.
+        * set_solver.
+        * iFrame "#". by iFrame.
+      + apply to_of_val.
+      + iFrame "#". by iFrame.
+  Qed.
+  
+  Lemma push_spec Φ γ (s: loc) (x: val) RI:
+    heapN ⊥ N →
+    heap_ctx ★ R x ★ inv N ((∃ xs, is_stack' R γ xs s) ★ RI) ★ ((∃ hd, evs γ hd x) -★ Φ #())
+    ⊢ WP push #s x {{ Φ }}.
+  Proof.
+    iIntros (HN) "(#Hh & HRx & #? & HΦ)".
+    iDestruct (push_atomic_spec N s x with "Hh") as "Hpush"=>//.
+    iSpecialize ("Hpush" $! (R x) (fun _ ret => (∃ hd, evs γ hd x) ★ ret = #())%I with "[]").
+    - iIntros "!# Rx".
+      (* open the invariant *)
+      iInv N as "[IH1 ?]" "Hclose".
+      iDestruct "IH1" as (xs hd) "[>Hs [>Hxs HR]]".
+      iDestruct (extract_is_list with "[Hxs]") as "==>[Hxs Hxs']"; first by iFrame.
+      iDestruct (dup_is_list with "[Hxs']") as "[Hxs'1 Hxs'2]"; first by iFrame.
+      (* mask magic *)
+      iApply pvs_intro'.
+      { apply ndisj_subseteq_difference; auto. }
+      iIntros "Hvs".
+      iExists (xs, hd).
+      iFrame "Hs Hxs'1".
+      iSplit.
+      + (* provide a way to rollback *)
+        iIntros "[Hs Hl']".
+        iVs "Hvs". iVs ("Hclose" with "[-Rx]"); last done.
+        { iNext. iFrame. iExists xs. iExists hd. by iFrame. }
+      + (* provide a way to commit *)
+        iIntros (v) "Hs".
+        iDestruct "Hs" as (hd') "[% [Hs [[Hhd'1 Hhd'2] Hxs']]]". subst.
+        iVs "Hvs".
+        iDestruct "HR" as (m) "[>Hom HRm]".
+        destruct (m !! hd') eqn:Heqn.
+        * iDestruct (big_sepM_delete_later (perR R) m with "HRm") as "[Hx ?]"=>//.
+          iDestruct "Hx" as (?) "(_ & _ & >Hhd'')".
+          iDestruct (heap_mapsto_op_1 with "[Hhd'1 Hhd'2]") as "[_ Hhd]"; first iFrame.
+          rewrite Qp_div_2.
+          iDestruct "Hhd''" as (q v) "Hhd''". iExFalso.
+          iApply (bogus_heap hd' 1%Qp q); first apply Qp_not_plus_q_ge_1.
+          iFrame "#". iFrame.
+        * iAssert (evs γ hd' x ★ ▷ (allR R γ))%I
+                  with "==>[Rx Hom HRm Hhd'1]" as "[#Hox ?]".
+          {
+            iDestruct (evmap_alloc _ _ _ m with "[Hom]") as "==>[Hom Hox]"=>//.
+            iDestruct (big_sepM_insert_later (perR R) m) as "H"=>//.
+            iSplitL "Hox".
+            { rewrite /evs /ev. eauto. }
+            iExists (<[hd' := ((), DecAgree x)]> m).
+            iFrame. iApply "H". iFrame. iExists x.
+            iFrame. rewrite /allocated. iSplitR "Hhd'1"; auto.
+          }
+          iVs ("Hclose" with "[-]").
+          { iNext. iFrame. iExists (x::xs).
+            iExists hd'. iFrame.
+            iExists hd, (1/2)%Qp. by iFrame.
+          }
+        iVsIntro. iSplitL; last auto. by iExists hd'.
+    - iApply wp_wand_r. iSplitL "HRx Hpush".
+      + by iApply "Hpush".
+      + iIntros (?) "H". iDestruct "H" as (_) "[? %]". subst.
+        by iApply "HΦ".
+  Qed.
+
+  (* some helpers *)
+  Lemma access (γ: gname) (x: val) (xs: list val) (m: evmapR loc val unitR) :
+    ∀ hd: loc,
+    x ∈ xs  →
+    ▷ ([★ map] hd↦v ∈ m, perR R hd v) ★ own γ (● m) ★
+    is_list' γ hd xs
+    ⊢ ∃ hd', ▷ ([★ map] hd↦v ∈ delete hd' m, perR R hd v) ★
+             ▷ perR R hd' ((∅: unitR), DecAgree x) ★ m !! hd' = Some ((∅: unitR), DecAgree x) ★ own γ (● m).
+  Proof.
+    induction xs as [|x' xs' IHxs'].
+    - iIntros (? Habsurd). inversion Habsurd.
+    - destruct (decide (x = x')) as [->|Hneq].
+      + iIntros (hd _) "(HR & Hom & Hxs)".
+        simpl. iDestruct "Hxs" as (hd' q) "[Hhd [#Hev Hxs']]".
+        rewrite /ev. destruct (m !! hd) as [[q' [x|]]|] eqn:Heqn.
+        * iDestruct (big_sepM_delete_later (perR R) m with "HR") as "[Hp HRm]"=>//.
+          iDestruct (map_agree_eq' _ _ _ m with "[Hom]") as %H'=>//; first iFrame=>//.
+          subst. iExists hd. inversion H'. subst. destruct q'. by iFrame.
+        * iDestruct (big_sepM_delete_later (perR R) m with "HR") as "[Hp HRm]"=>//.
+          iDestruct (map_agree_eq' _ _ _ m with "[Hom]") as "%"=>//; first iFrame=>//.
+        * iExFalso. iApply (map_agree_none' _ _ _ m)=>//. iFrame=>//.
+      + iIntros (hd ?).
+        assert (x ∈ xs'); first set_solver.
+        iIntros "(HRs & Hom & Hxs')".
+        simpl. iDestruct "Hxs'" as (hd' q) "[Hhd [Hev Hxs']]".
+        iDestruct (IHxs' hd' with "[HRs Hxs' Hom]") as "?"=>//.
+        iFrame.
+  Qed.
+
+End proofs.

simple_sync.v

@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import dec_agree frac.
-From iris_atomic Require Import atomic atomic_sync.
+From iris_atomic Require Import sync.
 Import uPred.
 
 Definition mk_sync: val :=

sync.v

+From iris.program_logic Require Export weakestpre hoare.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+
+Section sync.
+  Context `{!heapG Σ} (N : namespace).
+  
+  Definition synced R (f' f: val) :=
+    (□ ∀ P Q (x: val), ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) → ({{ P x }} f' x {{ v, Q x v }}))%I.
+
+  Definition is_syncer (R: iProp Σ) (s: val) :=
+    (∀ (f : val), WP s f {{ f', synced R f' f }})%I.
+
+  Definition mk_syncer_spec (mk_syncer: val) :=
+    ∀ (R: iProp Σ) (Φ: val -> iProp Σ),
+      heapN ⊥ N →
+      heap_ctx ★ R ★ (∀ s, □ (is_syncer R s) -★ Φ s) ⊢ WP mk_syncer #() {{ Φ }}.
+End sync.

treiber.v

@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import frac auth upred gmap dec_agree upred_big_op csum.
-From iris_atomic Require Import atomic misc evmap.
+From iris_atomic Require Import atomic misc.
 
 Definition new_stack: val := λ: <>, ref (ref NONE).
 
@@ -198,216 +198,3 @@ Section proof.
 
 End proof.
 
-Section defs.
-  Context `{heapG Σ, !evidenceG loc val unitR Σ} (N: namespace).
-  Context (R: val → iProp Σ) (γ: gname) `{∀ x, TimelessP (R x)}.
-
-  Definition allocated hd := (∃ q v, hd ↦{q} v)%I.
-
-  Definition evs := ev loc val γ.
-
-  Fixpoint is_list' (hd: loc) (xs: list val) : iProp Σ :=
-    match xs with
-    | [] => (∃ q, hd ↦{ q } NONEV)%I
-    | x :: xs => (∃ (hd': loc) q, hd ↦{q} SOMEV (x, #hd') ★ evs hd x ★ is_list' hd' xs)%I
-    end.
-
-  Lemma in_list' x xs:
-    ∀ hd, x ∈ xs →
-          is_list' hd xs
-          ⊢ ∃ (hd' hd'': loc) q, hd' ↦{q} SOMEV (x, #hd'') ★ evs hd' x.
-  Proof.
-    induction xs as [|x' xs' IHxs'].
-    - intros ? Hin. inversion Hin.
-    - intros hd Hin. destruct (decide (x = x')) as [->|Hneq].
-      + iIntros "Hls". simpl.
-        iDestruct "Hls" as (hd' q) "(? & ? & ?)".
-        iExists hd, hd', q. iFrame.
-      + assert (x ∈ xs') as Hin'; first set_solver.
-        iIntros "Hls". simpl.
-        iDestruct "Hls" as (hd' q) "(? & ? & ?)".
-        iApply IHxs'=>//.
-  Qed.
-
-  Definition perR' hd v v' := (v = ((∅: unitR), DecAgree v') ★ R v' ★ allocated hd)%I.
-  Definition perR  hd v := (∃ v', perR' hd v v')%I.