Pull dependencies back

647edcec · Zhen Zhang · b0f7bc5b · 647edcec · 647edcec · 647edcec
Commit 647edcec authored Oct 11, 2016 by Zhen Zhang
10 changed files
--- a/Makefile.coq
+++ b/Makefile.coq
@@ -50,11 +50,11 @@ vo_to_obj = $(addsuffix .o,\
 ##########################

 COQLIBS?=\
-  -Q "." flatcomb
+  -Q "." iris_atomic
 COQCHKLIBS?=\
-  -R "." flatcomb
+  -R "." iris_atomic
 COQDOCLIBS?=\
-  -R "." flatcomb
+  -R "." iris_atomic

 ##########################
 #                        #
@@ -96,12 +96,13 @@ endif
 #                    #
 ######################

-VFILES:=simple_sync.v\
-  pair_cas.v\
+VFILES:=atomic.v\
+  simple_sync.v\
  flat.v\
  atomic_pair.v\
  atomic_sync.v\
-  treiber.v
+  treiber.v\
+  misc.v

 ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
 -include $(addsuffix .d,$(VFILES))
@@ -191,22 +192,22 @@ userinstall:

 install:
 	cd "." && for i in $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES); do \
-	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/flatcomb/$$i`"; \
-	 install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/flatcomb/$$i; \
+	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/iris_atomic/$$i`"; \
+	 install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/iris_atomic/$$i; \
 	done

 install-doc:
-	install -d "$(DSTROOT)"$(COQDOCINSTALL)/flatcomb/html
+	install -d "$(DSTROOT)"$(COQDOCINSTALL)/iris_atomic/html
 	for i in html/*; do \
-	 install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/flatcomb/$$i;\
+	 install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/iris_atomic/$$i;\
 	done

 uninstall_me.sh: Makefile
 	echo '#!/bin/sh' > $@
-	printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/flatcomb && rm -f $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "flatcomb" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
-	printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/flatcomb \\\n' >> "$@"
+	printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/iris_atomic && rm -f $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "iris_atomic" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
+	printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/iris_atomic \\\n' >> "$@"
 	printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@"
-	printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find flatcomb/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
+	printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find iris_atomic/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
 	chmod +x $@

 uninstall: uninstall_me.sh

--- a/_CoqProject
+++ b/_CoqProject
-Q . flatcomb
+-Q . iris_atomic
+atomic.v
 simple_sync.v
-pair_cas.v
 flat.v
 atomic_pair.v
 atomic_sync.v
 treiber.v
-
+misc.v
--- a/atomic.v
+++ b/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.
+  Context `{irisG Λ Σ} {A: Type}.
+
+  (* logically atomic triple: <x, α> e @ E_i, E_o <v, β x v> *)
+  Definition atomic_triple
+             (α: A → iProp Σ)
+             (β: A → val _ → iProp Σ)
+             (Ei Eo: coPset)
+             (e: expr _) : iProp Σ :=
+    (∀ P Q, (P ={Eo, Ei}=> ∃ x:A,
+                                α x ★
+                                ((α x ={Ei, Eo}=★ P) ∧
+                                 (∀ v, β x v ={Ei, Eo}=★ Q x v))
+            ) -★ {{ P }} e @ ⊤ {{ v, (∃ x: A, Q x v) }})%I.
+
+  (* Weakest-pre version of the above one. Also weaker in some sense *)
+  Definition atomic_triple_wp
+             (α: A → iProp Σ)
+             (β: A → val _ → iProp Σ)
+             (Ei Eo: coPset)
+             (e: expr _) : iProp Σ :=
+    (∀ P Q, (P ={Eo, Ei}=> ∃ x,
+                              α x ★
+                              ((α x ={Ei, Eo}=★ P) ∧
+                               (∀ v, β x v ={Ei, Eo}=★ Q x v))
+            ) -★ P -★ WP e @ ⊤ {{ v, (∃ x, Q x v) }})%I.
+
+  Lemma atomic_triple_weaken α β Ei Eo e:
+    atomic_triple α β Ei Eo e ⊢ atomic_triple_wp α β Ei Eo e.
+  Proof.
+    iIntros "H". iIntros (P Q) "Hvs Hp".
+    by iApply ("H" $! P Q with "Hvs").
+  Qed.
+
+  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.
--- a/atomic_pair.v
+++ b/atomic_pair.v
@@ -2,10 +2,8 @@ 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.lib Require Import spin_lock.
-From iris.tests Require Import atomic.
 From iris.algebra Require Import dec_agree frac.
-From iris.program_logic Require Import auth.
-From flatcomb Require Import sync.
+From iris_atomic Require Import atomic sync.
 Import uPred.

 Section atomic_pair.

--- a/atomic_sync.v
+++ b/atomic_sync.v
@@ -2,9 +2,8 @@ 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.lib Require Import spin_lock.
-From iris.tests Require Import atomic misc.
 From iris.algebra Require Import dec_agree frac.
-From iris.program_logic Require Import auth.
+From iris_atomic Require Import atomic misc.

 Definition syncR := prodR fracR (dec_agreeR val).
 Class syncG Σ := sync_tokG :> inG Σ syncR.

--- a/flat.v
+++ b/flat.v
-From iris.program_logic Require Export auth weakestpre saved_prop.
+From iris.program_logic Require Export weakestpre saved_prop.
 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 upred frac agree excl dec_agree upred_big_op gset gmap.
-From iris.tests Require Import misc atomic treiber_stack.
-Require Import flatcomb.atomic_sync.
+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.

 Definition doOp : val :=
  λ: "f" "p",
@@ -168,8 +167,7 @@ Section proof.
      iDestruct (evmap_alloc _ _ _ m p (γx, γ1, γ3, γ4, γq) with "[Hm]") as "==>[Hm1 Hm2]"=>//.
      iDestruct "Hl" as "[Hl1 Hl2]".
      iVs ("Hclose" with "[HRm Hm1 Hl1 Hrs]").
-      + iNext. iFrame. iExists ({[p := (1%Qp, DecAgree (γx, γ1, γ3, γ4, γq))]} ⋅ m). iFrame.
-        rewrite <-(insert_singleton_op m)=>//.
+      + iNext. iFrame. iExists (<[p := (1%Qp, DecAgree (γx, γ1, γ3, γ4, γq))]> m). iFrame.
        iDestruct (big_sepM_insert _ m with "[-]") as "H"=>//.
        iSplitL "Hl1"; last by iAssumption. eauto.
      + iDestruct (pack_ev with "Hm2") as "Hev".

--- a/misc.v
+++ b/misc.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 auth frac gmap dec_agree upred_big_op.
+From iris.prelude Require Import countable.
+Import uPred.
+
+Section lemmas.
+  Lemma op_some: ∀ {A: cmraT} (a b: A), Some a ⋅ Some b = Some (a ⋅ b).
+  Proof. done. Qed.
+
+  Lemma invalid_plus: ∀ (q: Qp), ¬ ✓ (1 + q)%Qp.
+  Proof.
+    intros q H.
+    apply (Qp_not_plus_q_ge_1 q).
+    done.
+  Qed.
+
+  Lemma pair_l_frac_update (g g': val):
+    ((1 / 2)%Qp, DecAgree g) ⋅ ((1 / 2)%Qp, DecAgree g) ~~> ((1 / 2)%Qp, DecAgree g') ⋅ ((1 / 2)%Qp, DecAgree g').
+  Proof.
+    repeat rewrite pair_op dec_agree_idemp.
+    rewrite frac_op' Qp_div_2.
+    eapply cmra_update_exclusive.
+    done.
+  Qed.
+  
+  Lemma pair_l_frac_op (p q: Qp) (g g': val):
+    (((p, DecAgree g') ⋅ (q, DecAgree g'))) ~~> ((p + q)%Qp, DecAgree g').
+  Proof. by rewrite pair_op dec_agree_idemp frac_op'. Qed.
+
+  Lemma pair_l_frac_op' (p q: Qp) (g g': val):
+     ((p + q)%Qp, DecAgree g') ~~> (((p, DecAgree g') ⋅ (q, DecAgree g'))).
+  Proof. by rewrite pair_op dec_agree_idemp frac_op'. Qed.
+
+  Lemma pair_l_frac_op_1' (g g': val):
+     (1%Qp, DecAgree g') ~~> (((1/2)%Qp, DecAgree g') ⋅ ((1/2)%Qp, DecAgree g')).
+  Proof. by rewrite pair_op dec_agree_idemp frac_op' Qp_div_2. Qed.
+  
+End lemmas.
+
+Section excl.
+  Context `{!inG Σ (exclR unitC)}.
+  Lemma excl_falso γ Q':
+    own γ (Excl ()) ★ own γ (Excl ()) ⊢ Q'.
+  Proof.
+    iIntros "[Ho1 Ho2]". iCombine "Ho1" "Ho2" as "Ho".
+    iExFalso. by iDestruct (own_valid with "Ho") as "%".
+  Qed.
+End excl.
+
+Section pair.
+  Context `{EqDecision A, !inG Σ (prodR fracR (dec_agreeR A))}.
+  
+  Lemma m_frag_agree γm (q1 q2: Qp) (a1 a2: A):
+    own γm (q1, DecAgree a1) ★ own γm (q2, DecAgree a2)
+    ⊢ |=r=> own γm ((q1 + q2)%Qp, DecAgree a1) ★ (a1 = a2).
+  Proof.
+    iIntros "[Ho Ho']".
+    destruct (decide (a1 = a2)) as [->|Hneq].
+    - iSplitL=>//.
+      iCombine "Ho" "Ho'" as "Ho".
+      iDestruct (own_update with "Ho") as "?"; last by iAssumption.
+      by rewrite pair_op frac_op' dec_agree_idemp.
+    - iCombine "Ho" "Ho'" as "Ho".
+      iDestruct (own_valid with "Ho") as %Hvalid.
+      exfalso. destruct Hvalid as [_ Hvalid].
+      simpl in Hvalid. apply dec_agree_op_inv in Hvalid. inversion Hvalid. subst. auto.
+  Qed.
+End pair.
+
+Section evidence.  
+  Context (K A: Type) `{Countable K, EqDecision A}.
+  Definition evkR := prodR fracR (dec_agreeR A).
+  Definition evmapR := gmapUR K evkR.
+  Definition evidenceR := authR evmapR.
+  Class evidenceG Σ := EvidenceG { evidence_G :> inG Σ evidenceR }.
+  Definition evidenceΣ : gFunctors := #[ GFunctor (constRF evidenceR) ].
+
+  Instance subG_evidenceΣ {Σ} : subG evidenceΣ Σ → evidenceG Σ.
+  Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+
+  Lemma map_agree_eq m m' (hd: K) (p q: Qp) (x y: A):
+    m !! hd = Some (p, DecAgree y) →
+    m = {[hd := (q, DecAgree x)]} ⋅ m' → x = y.
+  Proof.
+    intros H1 H2.
+    destruct (decide (x = y)) as [->|Hneq]=>//.
+    exfalso.
+    subst. rewrite lookup_op lookup_singleton in H1.
+    destruct (m' !! hd) as [[b [c|]]|] eqn:Heqn; rewrite Heqn in H1; inversion H1=>//.
+    destruct (decide (x = c)) as [->|Hneq3]=>//.
+    - rewrite dec_agree_idemp in H3. by inversion H3.
+    - rewrite dec_agree_ne in H3=>//.
+  Qed.
+
+  Lemma map_agree_somebot m m' (hd: K) (p q: Qp) (x: A):
+    m !! hd = Some (p, DecAgreeBot) → m' !! hd = None →
+    m = {[hd := (q, DecAgree x)]} ⋅ m' → False.
+  Proof.
+    intros H1 H2 H3. subst. rewrite lookup_op lookup_singleton in H1.
+    destruct (m' !! hd) as [[b [c|]]|] eqn:Heqn; rewrite Heqn in H1; inversion H1=>//.
+  Qed.
+
+  Lemma map_agree_none m m' (hd: K) (q: Qp) (x: A):
+    m !! hd = None → m = {[hd := (q, DecAgree x)]} ⋅ m' → False.
+  Proof.
+    intros H1 H2. subst. rewrite lookup_op lookup_singleton in H1.
+    destruct (m' !! hd)=>//.
+  Qed.
+
+  Context `{!inG Σ (authR evmapR)}.
+
+  Definition ev γm (k : K) (v: A) := (∃ q, own γm (◯ {[ k := (q, DecAgree v) ]}))%I.
+
+  Lemma evmap_alloc γm m k v:
+    m !! k = None →
+    own γm (● m) ⊢ |=r=> own γm (● (<[ k := (1%Qp, DecAgree v) ]> m) ⋅ ◯ {[ k := (1%Qp, DecAgree v) ]}).
+  Proof.
+    iIntros (?) "Hm".
+    iDestruct (own_update with "Hm") as "?"; last by iAssumption.
+    apply auth_update_alloc, alloc_local_update=>//.
+  Qed.
+  
+  Lemma map_agree_none' γm m hd x:
+    m !! hd = None →
+    own γm (● m) ★ ev γm hd x ⊢ False.
+  Proof.
+    iIntros (?) "[Hom Hev]". iDestruct "Hev" as (?) "Hfrag".
+    iCombine "Hom" "Hfrag" as "Hauth".
+    iDestruct (own_valid γm (● m ⋅ ◯ {[hd := (_, DecAgree x)]})
+               with "[Hauth]") as %Hvalid=>//.
+    iPureIntro.
+    apply auth_valid_discrete_2 in Hvalid as [[af Compose%leibniz_equiv_iff] Valid].
+    eapply (map_agree_none m)=>//.
+  Qed.
+  
+  Lemma map_agree_eq' γm m hd p x agy:
+    m !! hd = Some (p, agy) →
+    own γm (● m) ★ ev γm hd x ⊢ own γm (● m) ★ ev γm hd x ★ DecAgree x = agy.
+  Proof.
+    iIntros (?) "[Hom Hev]". iDestruct "Hev" as (?) "Hfrag".
+    iCombine "Hom" "Hfrag" as "Hauth".
+    iDestruct (own_valid γm (● m ⋅ ◯ {[hd := (_, DecAgree x)]})
+               with "[Hauth]") as %Hvalid=>//.
+    apply auth_valid_discrete_2 in Hvalid as [[af Compose%leibniz_equiv_iff] Valid].
+    destruct agy as [y|].
+    - iDestruct "Hauth" as "[? ?]". iFrame. iSplitL.
+      { rewrite /ev. eauto. }
+      iPureIntro. destruct (decide (x = y)); try by subst.
+      exfalso. apply n. eapply (map_agree_eq m)=>//. (* XXX: Why it is uPred M *)
+    - iAssert (✓ m)%I as "H"=>//. rewrite (gmap_validI m).
+      iDestruct ("H" $! hd) as "%".
+      exfalso. subst. rewrite H0 in H2.
+      by destruct H2 as [? ?].
+  Qed.
+
+  Lemma pack_ev γm k v q:
+    own γm (◯ {[ k := (q, DecAgree v) ]}) ⊢ ev γm k v.
+  Proof. iIntros "?". rewrite /ev. eauto. Qed.
+  
+  Lemma dup_ev γm hd y:
+    ev γm hd y ⊢ |=r=> ev γm hd y ★ ev γm hd y.
+  Proof.
+    rewrite /ev. iIntros "Hev". iDestruct "Hev" as (q) "Hev".
+    iAssert (|=r=> own γm (◯ {[hd := ((q/2)%Qp, DecAgree y)]} ⋅
+                           ◯ {[hd := ((q/2)%Qp, DecAgree y)]}))%I with "[Hev]" as "==>[Hev1 Hev2]".
+    { iDestruct (own_update with "Hev") as "?"; last by iAssumption.
+      rewrite <- auth_frag_op.
+      by rewrite op_singleton pair_op dec_agree_idemp  frac_op' Qp_div_2. }
+    iSplitL "Hev1"; eauto.
+  Qed.
+
+  Lemma evmap_frag_agree_split γm p q1 q2 (a1 a2: A):
+    own γm (◯ {[p := (q1, DecAgree a1)]}) ★
+    own γm (◯ {[p := (q2, DecAgree a2)]})
+    ⊢ |=r=> own γm (◯ {[p := (q1, DecAgree a1)]}) ★
+            own γm (◯ {[p := (q2, DecAgree a1)]}) ★ (a1 = a2).
+  Proof.
+    iIntros "[Ho Ho']".
+    destruct (decide (a1 = a2)) as [->|Hneq].
+    - by iFrame.
+    - iCombine "Ho" "Ho'" as "Ho".
+      iDestruct (own_valid with "Ho") as %Hvalid.
+      exfalso. rewrite <-(@auth_frag_op evmapR) in Hvalid.
+      rewrite op_singleton in Hvalid.
+      apply auth_valid_discrete in Hvalid. simpl in Hvalid.
+      apply singleton_valid in Hvalid.
+      destruct Hvalid as [_ Hvalid].
+      apply dec_agree_op_inv in Hvalid. inversion Hvalid. subst. auto.
+  Qed.
+
+  Lemma evmap_frag_agree γm p q1 q2 (a1 a2: A):
+    own γm (◯ {[p := (q1, DecAgree a1)]}) ★
+    own γm (◯ {[p := (q2, DecAgree a2)]})
+    ⊢ |=r=> own γm (◯ {[p := ((q1 + q2)%Qp, DecAgree a1)]}) ★ (a1 = a2).
+  Proof.
+    iIntros "Hos".
+    iDestruct (evmap_frag_agree_split with "Hos") as "==>[Ho1 [Ho2 %]]".
+    iCombine "Ho1" "Ho2" as "Ho". iSplitL; auto.
+    iDestruct (own_update with "Ho") as "?"; last by iAssumption.
+    rewrite <-(@auth_frag_op evmapR {[p := (q1, DecAgree a1)]} {[p := (q2, DecAgree a1)]}).
+    by rewrite op_singleton pair_op frac_op' dec_agree_idemp.
+  Qed.
+
+  Lemma ev_agree γm k v1 v2:
+    ev γm k v1 ★ ev γm k v2 ⊢ |=r=> ev γm k v1 ★ ev γm k v1 ★ v1 = v2.
+  Proof.
+    iIntros "[Hev1 Hev2]".
+    iDestruct "Hev1" as (?) "Hev1". iDestruct "Hev2" as (?) "Hev2".
+    iDestruct (evmap_frag_agree_split with "[-]") as "==>[Hev1 [Hev2 %]]"; first iFrame.
+    subst. iSplitL "Hev1"; rewrite /ev; eauto.
+  Qed.
+
+End evidence.
+
+Section heap_extra.
+  Context `{heapG Σ}.
+
+  Lemma bogus_heap p (q1 q2: Qp) a b:
+    ~((q1 + q2)%Qp ≤ 1%Qp)%Qc →
+    heap_ctx ★ p ↦{q1} a ★ p ↦{q2} b ⊢ False.
+  Proof.
+    iIntros (?) "(#Hh & Hp1 & Hp2)".
+    iCombine "Hp1" "Hp2" as "Hp".
+    iDestruct (heap_mapsto_op_1 with "Hp") as "[_ Hp]".
+    rewrite heap_mapsto_eq. iDestruct (own_valid with "Hp") as %H'.
+    apply singleton_valid in H'. by destruct H' as [H' _].
+  Qed.
+  
+End heap_extra.
+
+Section big_op_later.
+  Context {M : ucmraT}.
+  Context `{Countable K} {A : Type}.
+  Implicit Types m : gmap K A.
+  Implicit Types Φ Ψ : K → A → uPred M. 
+
+  Lemma big_sepM_delete_later Φ m i x :
+    m !! i = Some x →
+    ▷ ([★ map] k↦y ∈ m, Φ k y) ⊣⊢ ▷ Φ i x ★ ▷ [★ map] k↦y ∈ delete i m, Φ k y.
+  Proof. intros ?. rewrite big_sepM_delete=>//. apply later_sep. Qed.
+
+  Lemma big_sepM_insert_later Φ m i x :
+    m !! i = None →
+    ▷ ([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ ▷ Φ i x ★ ▷ [★ map] k↦y ∈ m, Φ k y.
+  Proof. intros ?. rewrite big_sepM_insert=>//. apply later_sep. Qed.
+End big_op_later.
--- a/pair_cas.v
+++ b/pair_cas.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.
-From flatcomb Require Import sync.
+Require Import iris_atomic.atomic_sync.
 Import uPred.

 (* CAS, load and store to pair of locations *)

--- a/simple_sync.v
+++ b/simple_sync.v
@@ -2,10 +2,8 @@ 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.lib Require Import spin_lock.
-From iris.tests Require Import atomic misc.
 From iris.algebra Require Import dec_agree frac.
-From iris.program_logic Require Import auth.
-From flatcomb Require Import atomic_sync.
+From iris_atomic Require Import atomic atomic_sync.
 Import uPred.

 Definition mk_sync: val :=

--- a/treiber.v
+++ b/treiber.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 upred gmap dec_agree upred_big_op.
-From iris.program_logic Require Import auth.
-From iris.tests Require Import treiber_stack atomic misc.
+From iris.algebra Require Import auth upred gmap dec_agree upred_big_op.
+From iris_atomic Require Import atomic misc.
+
+Definition new_stack: val := λ: <>, ref (ref NONE).
+
+Definition push: val :=
+  rec: "push" "s" "x" :=
+      let: "hd" := !"s" in
+      let: "s'" := ref SOME ("x", "hd") in
+      if: CAS "s" "hd" "s'"
+        then #()
+        else "push" "s" "x".
+
+Definition pop: val :=
+  rec: "pop" "s" :=
+      let: "hd" := !"s" in
+      match: !"hd" with
+        SOME "cell" =>
+        if: CAS "s" "hd" (Snd "cell")
+          then SOME (Fst "cell")
+          else "pop" "s"
+      | NONE => NONE
+      end.
+
+Definition iter: val :=
+  rec: "iter" "hd" "f" :=
+      match: !"hd" with
+        NONE => #()
+      | SOME "cell" => "f" (Fst "cell") ;; "iter" (Snd "cell") "f"
+      end.
+
+Global Opaque new_stack push pop iter.
+
+Section proof.
+  Context `{!heapG Σ} (N: namespace).
+
+  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') ★ is_list hd' xs)%I
+    end.
+
+  Lemma dup_is_list : ∀ xs hd,
+    heap_ctx ★ is_list hd xs ⊢ 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'] & Hs')".
+      iDestruct (IHxs' with "[Hs']") as "[Hs1 Hs2]"; first by iFrame.
+      iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
+  Qed.
+
+  Lemma uniq_is_list:
+    ∀ xs ys hd, heap_ctx ★ is_list hd xs ★ is_list hd ys ⊢ xs = ys.
+  Proof.
+    induction xs as [|x xs' IHxs'].
+    - induction ys as [|y ys' IHys'].
+      + auto.
+      + iIntros (hd) "(#? & Hxs & Hys)".
+        simpl. iDestruct "Hys" as (hd' ?) "(Hhd & Hys')".
+        iExFalso. iDestruct "Hxs" as (?) "Hhd'".
+        iDestruct (heap_mapsto_op_1 with "[Hhd Hhd']") as "[% _]".
+        { iSplitL "Hhd"; done. }
+        done.
+    - induction ys as [|y ys' IHys'].
+      + iIntros (hd) "(#? & Hxs & Hys)".
+        simpl.
+        iExFalso. iDestruct "Hxs" as (? ?) "(Hhd & _)".
+        iDestruct "Hys" as (?) "Hhd'".
+        iDestruct (heap_mapsto_op_1 with "[Hhd Hhd']") as "[% _]".
+        { iSplitL "Hhd"; done. }
+        done.
+      + iIntros (hd) "(#? & Hxs & Hys)".
+        simpl. iDestruct "Hxs" as (? ?) "(Hhd & Hxs')".
+        iDestruct "Hys" as (? ?) "(Hhd' & Hys')".
+        iDestruct (heap_mapsto_op_1 with "[Hhd Hhd']") as "[% _]".
+        { iSplitL "Hhd"; done. }
+        inversion H3. (* FIXME: name *)
+        subst. iDestruct (IHxs' with "[Hxs' Hys']") as "%"; first by iFrame.
+        by subst.
+  Qed.
+
+  Definition is_stack (s: loc) xs: iProp Σ := (∃ hd: loc, s ↦ #hd ★ is_list hd xs)%I.
+
+  Global Instance is_list_timeless xs hd: TimelessP (is_list hd xs).
+  Proof. generalize hd. induction xs; apply _. Qed.
+
+  Global Instance is_stack_timeless xs hd: TimelessP (is_stack hd xs).
+  Proof. generalize hd. induction xs; apply _. Qed.
+
+  Lemma new_stack_spec:
+    ∀ (Φ: val → iProp Σ),
+      heapN ⊥ N →
+      heap_ctx ★ (∀ s, is_stack s [] -★ Φ #s) ⊢ WP new_stack #() {{ Φ }}.
+  Proof.
+    iIntros (Φ HN) "[#Hh HΦ]". wp_seq.
+    wp_bind (ref NONE)%E. wp_alloc l as "Hl".
+    wp_alloc l' as "Hl'".