From 647edceca038974b85a3aa1843ece23a116f3ea9 Mon Sep 17 00:00:00 2001
From: Zhen Zhang <izgzhen@gmail.com>
Date: Tue, 11 Oct 2016 15:24:58 +0200
Subject: [PATCH] Pull dependencies back
---
Makefile.coq | 27 +++---
_CoqProject | 6 +-
atomic.v | 147 ++++++++++++++++++++++++++++++
atomic_pair.v | 4 +-
atomic_sync.v | 3 +-
flat.v | 10 +-
misc.v | 248 ++++++++++++++++++++++++++++++++++++++++++++++++++
pair_cas.v | 2 +-
simple_sync.v | 4 +-
treiber.v | 205 ++++++++++++++++++++++++++++++++++++++++-
10 files changed, 620 insertions(+), 36 deletions(-)
create mode 100644 atomic.v
create mode 100644 misc.v
diff --git a/Makefile.coq b/Makefile.coq
index 154f355..5f758bc 100644
--- 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
diff --git a/_CoqProject b/_CoqProject
index 5905c1f..0282886 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,8 +1,8 @@
--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
diff --git a/atomic.v b/atomic.v
new file mode 100644
index 0000000..0b978ba
--- /dev/null
+++ b/atomic.v
@@ -0,0 +1,147 @@
+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.
diff --git a/atomic_pair.v b/atomic_pair.v
index 9a6cca2..73b8fba 100644
--- 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.
diff --git a/atomic_sync.v b/atomic_sync.v
index c5f6f9d..89df35f 100644
--- 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.
diff --git a/flat.v b/flat.v
index 2cacbfa..ad4504b 100644
--- a/flat.v
+++ b/flat.v
@@ -1,10 +1,9 @@
-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".
diff --git a/misc.v b/misc.v
new file mode 100644
index 0000000..3a373dc
--- /dev/null
+++ b/misc.v
@@ -0,0 +1,248 @@
+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.
diff --git a/pair_cas.v b/pair_cas.v
index aa7b1ff..5ab3cd7 100644
--- 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 *)
diff --git a/simple_sync.v b/simple_sync.v
index de70675..d9859bb 100644
--- 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 :=
diff --git a/treiber.v b/treiber.v
index c2cbe7c..82dc587 100644
--- a/treiber.v
+++ b/treiber.v
@@ -1,9 +1,204 @@
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'".
+ iApply "HΦ". rewrite /is_stack. iExists l.
+ iFrame. by iExists 1%Qp.
+ Qed.
+
+ Definition push_triple (s: loc) (x: val) :=
+ atomic_triple (fun xs_hd: list val * loc =>
+ let '(xs, hd) := xs_hd in s ↦ #hd ★ is_list hd xs)%I
+ (fun xs_hd ret =>
+ let '(xs, hd) := xs_hd in
+ ∃ hd': loc,
+ ret = #() ★ s ↦ #hd' ★ hd' ↦ SOMEV (x, #hd) ★ is_list hd xs)%I
+ (nclose heapN)
+ ⊤
+ (push #s x).
+
+ Lemma push_atomic_spec (s: loc) (x: val) :
+ heapN ⊥ N → heap_ctx ⊢ push_triple s x.
+ Proof.
+ iIntros (HN) "#?". rewrite /push_triple /atomic_triple.
+ iIntros (P Q) "#Hvs".
+ iLöb as "IH". iIntros "!# HP". wp_rec.
+ wp_let. wp_bind (! _)%E.
+ iVs ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]".
+ wp_load. iVs ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame.
+ iVsIntro. wp_let. wp_alloc l as "Hl". wp_let.
+ wp_bind (CAS _ _ _)%E.
+ iVs ("Hvs" with "HP") as ([xs' hd']) "[[Hs Hhd'] Hvs']".
+ destruct (decide (hd = hd')) as [->|Hneq].
+ * wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
+ iVs ("Hvs'" $! #() with "[-]") as "HQ".
+ { iExists l. iSplitR; first done. by iFrame. }
+ iVsIntro. wp_if. iVsIntro. eauto.
+ * wp_cas_fail.
+ iDestruct "Hvs'" as "[Hvs' _]".
+ iVs ("Hvs'" with "[-]") as "HP"; first by iFrame.
+ iVsIntro. wp_if. by iApply "IH".
+ Qed.
+
+ Definition pop_triple (s: loc) :=
+ atomic_triple (fun xs_hd: list val * loc =>
+ let '(xs, hd) := xs_hd in s ↦ #hd ★ is_list hd xs)%I
+ (fun xs_hd ret =>
+ let '(xs, hd) := xs_hd in
+ (ret = NONEV ★ xs = [] ★ s ↦ #hd ★ is_list hd []) ∨
+ (∃ x q (hd': loc) xs', hd ↦{q} SOMEV (x, #hd') ★ ret = SOMEV x ★
+ xs = x :: xs' ★ s ↦ #hd' ★ is_list hd' xs'))%I
+ (nclose heapN)
+ ⊤
+ (pop #s).
+
+ Lemma pop_atomic_spec (s: loc):
+ heapN ⊥ N → heap_ctx ⊢ pop_triple s.
+ Proof.
+ iIntros (HN) "#?".
+ rewrite /pop_triple /atomic_triple.
+ iIntros (P Q) "#Hvs".
+ iLöb as "IH". iIntros "!# HP". wp_rec.
+ wp_bind (! _)%E.
+ iVs ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] Hvs']".
+ destruct xs as [|y' xs'].
+ - simpl. wp_load. iDestruct "Hvs'" as "[_ Hvs']".
+ iDestruct "Hhd" as (q) "[Hhd Hhd']".
+ iVs ("Hvs'" $! NONEV with "[-Hhd]") as "HQ".
+ { iLeft. iSplit=>//. iSplit=>//. iFrame. eauto. }
+ iVsIntro. wp_let. wp_load. wp_match.
+ iVsIntro. eauto.
+ - simpl. iDestruct "Hhd" as (hd' q) "([[Hhd1 Hhd2] Hhd'] & Hxs')".
+ iDestruct (dup_is_list with "[Hxs']") as "[Hxs1 Hxs2]"; first by iFrame.
+ wp_load. iDestruct "Hvs'" as "[Hvs' _]".
+ iVs ("Hvs'" with "[-Hhd1 Hhd2 Hxs1]") as "HP".
+ { iFrame. iExists hd', (q / 2)%Qp. by iFrame. }
+ iVsIntro. wp_let. wp_load. wp_match. wp_proj.
+ wp_bind (CAS _ _ _). iVs ("Hvs" with "HP") as ([xs hd'']) "[[Hs Hhd''] Hvs']".
+ destruct (decide (hd = hd'')) as [->|Hneq].
+ + wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
+ iVs ("Hvs'" $! (SOMEV y') with "[-]") as "HQ".
+ { iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'.
+ destruct xs as [|x' xs''].
+ - simpl. iDestruct "Hhd''" as (?) "H".
+ iExFalso. iDestruct (heap_mapsto_op_1 with "[Hhd1 H]") as "[% _]".
+ { iSplitL "Hhd1"; done. }
+ done.
+ - simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
+ iDestruct (heap_mapsto_op_1 with "[Hhd1 Hhd'']") as "[% _]".
+ { iSplitL "Hhd1"; done. }
+ inversion H0. (* FIXME: bad naming *) subst.
+ iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
+ repeat (iSplitR "Hxs1 Hs"; first done).
+ iFrame. }
+ iVsIntro. wp_if. wp_proj. eauto.
+ + wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]".
+ iVs ("Hvs'" with "[-]") as "HP"; first by iFrame.
+ iVsIntro. wp_if. by iApply "IH".
+ Qed.
+
+End proof.
+
+
Section defs.
Context `{heapG Σ, !evidenceG loc val Σ} (N: namespace).
@@ -174,8 +369,7 @@ Lemma new_stack_spec' Φ RI:
{ rewrite /ev. eauto. }
iFrame.
iDestruct (big_sepM_insert_later (perR R) m) as "H"=>//.
- rewrite (insert_singleton_op m)=>//.
- iExists ({[hd' := (1%Qp, DecAgree x)]} â‹… m).
+ iExists (<[hd' := (1%Qp, DecAgree x)]> m).
iFrame. iApply "H". iFrame. iExists x.
iFrame. rewrite /allocated. iSplitR "Hhd'1"; auto.
}
@@ -222,3 +416,4 @@ Lemma new_stack_spec' Φ RI:
Qed.
End proofs.
+
--
GitLab