From 3fd612a963f81bd39477285e657c19e663fb23d2 Mon Sep 17 00:00:00 2001
From: Zhen Zhang <izgzhen@gmail.com>
Date: Thu, 22 Dec 2016 20:19:32 +0800
Subject: [PATCH] Simplify and update
- evmap is dropped
- per-item invariant is implemented with inv-in-inv
- peritem.v is simplified by proving an ad-hoc iter spec
- update to latest iris
- related fixes
---
_CoqProject | 1 -
opam.pins | 2 +-
theories/evmap.v | 134 --------------
theories/flat.v | 439 +++++++++++++++++----------------------------
theories/peritem.v | 194 +++++---------------
5 files changed, 209 insertions(+), 561 deletions(-)
delete mode 100644 theories/evmap.v
diff --git a/_CoqProject b/_CoqProject
index aa97415..69fa428 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -7,6 +7,5 @@ theories/flat.v
theories/atomic_sync.v
theories/treiber.v
theories/misc.v
-theories/evmap.v
theories/peritem.v
theories/atomic_pcas.v
diff --git a/opam.pins b/opam.pins
index ce27694..0b7c841 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 766dbcd2415df9256f197dc562a0a15f9b0ddeac
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 2e3a9be08487e50bfc4bba911da6a11a4b715d36
diff --git a/theories/evmap.v b/theories/evmap.v
deleted file mode 100644
index 22e6677..0000000
--- a/theories/evmap.v
+++ /dev/null
@@ -1,134 +0,0 @@
-(* evmap.v -- generalized heap-like monoid composite *)
-From iris.base_logic Require Export invariants.
-From iris.program_logic Require Export weakestpre.
-From iris.algebra Require Export auth frac gmap.
-From iris.algebra Require deprecated.
-From iris.proofmode Require Import tactics.
-
-Export deprecated.dec_agree.
-(* Porting this to algebra.agree does not really work well because the
- map from K to (Q * agree A) is part of the interface of this file.
- This file should either be ditched or raised to a higher level
- of abstraction, i.e., work on a map from K to A and use fmap
- for the thing that's owned. *)
-
-Section evmap.
- Context (K A: Type) (Q: cmraT) `{Countable K, EqDecision A}.
- Definition evkR := prodR Q (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.
-
- (* Some basic supporting lemmas *)
- Lemma map_agree_eq m m' (hd: K) (p q: Q) (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: Q) (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: Q) (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.
-End evmap.
-
-Section evmapR.
- Context (K A: Type) `{Countable K, EqDecision A}.
- Context `{!inG Σ (authR (evmapR K A unitR))}.
-
- (* Evidence that k immutably maps to some fixed v *)
- Definition ev γm (k : K) (v: A) := own γm (◯ {[ k := ((), DecAgree v) ]})%I.
-
- Global Instance persistent_ev γm k v : PersistentP (ev γm k v).
- Proof. apply _. Qed.
-
- (* Alloc a new mapsto *)
- Lemma evmap_alloc γm m k v:
- m !! k = None →
- own γm (◠m) ⊢ |==> own γm (◠(<[ k := ((), DecAgree v) ]> m) ⋅ ◯ {[ k := ((), DecAgree v) ]}).
- Proof.
- iIntros (?) "Hm".
- iDestruct (own_update with "Hm") as "?"; last by iAssumption.
- apply auth_update_alloc. apply alloc_singleton_local_update=>//.
- Qed.
-
- (* Some other supporting lemmas *)
- Lemma map_agree_none' γm (m: evmapR K A unitR) hd x:
- m !! hd = None →
- own γm (◠m) ∗ ev γm hd x ⊢ False.
- Proof.
- iIntros (?) "[Hom Hev]".
- iCombine "Hom" "Hev" as "Hauth".
- iDestruct (own_valid 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 x agy:
- m !! hd = Some ((), agy) →
- ev γm hd x ∗ own γm (â— m) ⊢ ⌜DecAgree x = agyâŒ.
- Proof.
- iIntros (?) "[#Hev Hom]".
- iCombine "Hom" "Hev" 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.
- iPureIntro. apply f_equal.
- eapply (map_agree_eq _ _ _ m)=>//.
- - iAssert (✓ m)%I as "H"=>//. rewrite (gmap_validI m).
- iDestruct ("H" $! hd) as "%".
- exfalso. subst. rewrite H0 in H1.
- by destruct H1 as [? ?].
- Qed.
-
- (* Evidence is the witness of membership *)
- Lemma ev_map_witness γm m hd x:
- ev γm hd x ∗ own γm (â— m) ⊢ ⌜m !! hd = Some (∅, DecAgree x)âŒ.
- Proof.
- iIntros "[#Hev Hom]".
- destruct (m !! hd) as [[[] agy]|] eqn:Heqn.
- - iDestruct (map_agree_eq' with "[-]") as %H'=>//; first by iFrame. by subst.
- - iExFalso. iApply map_agree_none'=>//. by iFrame.
- Qed.
-
- (* Two evidences coincides *)
- Lemma evmap_frag_agree_split γm p (a1 a2: A):
- ev γm p a1 ∗ ev γm p a2 ⊢ ⌜a1 = a2âŒ.
- Proof.
- iIntros "[Ho Ho']".
- destruct (decide (a1 = a2)) as [->|Hneq].
- - by iFrame.
- - iCombine "Ho" "Ho'" as "Ho".
- rewrite -(@auth_frag_op (evmapR K A unitR) {[p := (_, DecAgree a1)]} {[p := (_, DecAgree a2)]}).
- iDestruct (own_valid with "Ho") as %Hvalid.
- exfalso. 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.
-End evmapR.
diff --git a/theories/flat.v b/theories/flat.v
index 195a3ff..9850ce9 100644
--- a/theories/flat.v
+++ b/theories/flat.v
@@ -1,12 +1,11 @@
(* Flat Combiner *)
-
From iris.program_logic Require Export weakestpre.
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 frac agree excl agree gset gmap.
From iris.base_logic Require Import big_op saved_prop.
-From iris_atomic Require Import misc peritem sync evmap.
+From iris_atomic Require Import misc peritem sync.
Definition doOp : val :=
λ: "p",
@@ -49,24 +48,20 @@ Definition mk_flat : val :=
Definition reqR := prodR fracR (agreeR valC). (* request x should be kept same *)
Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *)
-Definition tokmR : ucmraT := evmapR loc toks unitR. (* tie each slot to tokens *)
Class flatG Σ := FlatG {
req_G :> inG Σ reqR;
- tok_G :> inG Σ (authR tokmR);
sp_G :> savedPropG Σ (ofe_funCF val idCF)
}.
Definition flatΣ : gFunctors :=
#[ GFunctor (constRF reqR);
- GFunctor (constRF (authR tokmR));
- savedPropΣ (ofe_funCF val idCF)
- ].
+ savedPropΣ (ofe_funCF val idCF) ].
Instance subG_flatΣ {Σ} : subG flatΣ Σ → flatG Σ.
-Proof. intros [?%subG_inG [?%subG_inG [? _]%subG_inv]%subG_inv]%subG_inv. split; apply _. Qed.
+Proof. intros [?%subG_inG [? _]%subG_inv]%subG_inv. split; apply _. Qed.
Section proof.
- Context `{!heapG Σ, !lockG Σ, !evidenceG loc val unitR Σ, !flatG Σ} (N : namespace).
+ Context `{!heapG Σ, !lockG Σ, !flatG Σ} (N: namespace).
Definition init_s (ts: toks) :=
let '(_, γ1, γ3, _, _) := ts in (own γ1 (Excl ()) ∗ own γ3 (Excl ()))%I.
@@ -86,61 +81,32 @@ Section proof.
(∃ Q: val → val → iProp Σ,
own γx ((1/2)%Qp, to_agree x) ∗ saved_prop_own γq (Q x) ∗
Q x y ∗ own γ1 (Excl ()) ∗ own γ4 (Excl ()))%I.
-
- Definition evm := ev loc toks.
- (* p slot invariant *)
- Definition p_inv R (γm γr: gname) (v: val) :=
- (∃ (ts: toks) (p : loc),
- ⌜v = #p⌠∗ evm γm p ts ∗
- ((* INIT *)
- (∃ y: val, p ↦{1/2} InjRV y ∗ init_s ts)∨
- (* INSTALLED *)
- (∃ f x: val, p ↦{1/2} InjLV (f, x) ∗ installed_s R ts f x) ∨
- (* RECEIVED *)
- (∃ f x: val, p ↦{1/2} InjLV (f, x) ∗ received_s ts x γr) ∨
- (* FINISHED *)
- (∃ x y: val, p ↦{1/2} InjRV y ∗ finished_s ts x y)))%I.
-
- Definition srv_stack_inv R γs γm γr s := (∃ xs, is_stack' (p_inv R γm γr) γs xs s)%I.
+ Definition p_inv R (γm γr: gname) (ts: toks) (p : loc) :=
+ ( (* INIT *)
+ (∃ y: val, p ↦ InjRV y ∗ init_s ts) ∨
+ (* INSTALLED *)
+ (∃ f x: val, p ↦ InjLV (f, x) ∗ installed_s R ts f x) ∨
+ (* RECEIVED *)
+ (∃ f x: val, p ↦ InjLV (f, x) ∗ received_s ts x γr) ∨
+ (* FINISHED *)
+ (∃ x y: val, p ↦ InjRV y ∗ finished_s ts x y))%I.
- Definition srv_tokm_inv γm := (∃ m : tokmR, own γm (◠m) ∗ [∗ map] p ↦ _ ∈ m, ∃ v, p ↦{1/2} v)%I.
+ Definition p_inv' R γm γr : val → iProp Σ :=
+ (λ v: val, ∃ ts (p: loc), ⌜v = #p⌠∗ inv N (p_inv R γm γr ts p))%I.
- Lemma install_push_spec R
- (p: loc) (γs γm γr: gname) (ts: toks)
- (s: loc) (f x: val) (Φ: val → iProp Σ) :
- inv N (srv_stack_inv R γs γm γr s ∗ srv_tokm_inv γm) ∗
- evm γm p ts ∗ installed_s R ts f x ∗
- p ↦{1/2} InjLV (f, x) ∗ ((∃ hd, evs γs hd #p) -∗ Φ #())
- ⊢ WP push #s #p {{ Φ }}.
- Proof.
- iIntros "(#? & Hpm & Hs & Hp & HΦ)".
- rewrite /srv_stack_inv.
- iDestruct (push_spec N (p_inv R γm γr) (fun v => (∃ hd, evs γs hd #p) ∗ ⌜v = #()âŒ)%I
- with "[-HΦ]") as "Hpush"=>//.
- - iSplitL "Hp Hs Hpm"; last eauto.
- iExists ts. iExists p. iSplit=>//. iFrame "Hpm".
- iRight. iLeft. iExists f, x. iFrame.
- - iApply wp_wand_r.
- iSplitL "Hpush"; first done.
- iIntros (?) "[? %]". subst.
- by iApply "HΦ".
- Qed.
+ Definition srv_bag R γm γr s := (∃ xs, is_bag_R N (p_inv' R γm γr) xs s)%I.
Definition installed_recp (ts: toks) (x: val) (Q: val → iProp Σ) :=
let '(γx, _, γ3, _, γq) := ts in
(own γ3 (Excl ()) ∗ own γx ((1/2)%Qp, to_agree x) ∗ saved_prop_own γq Q)%I.
- Lemma install_spec
- R P Q
- (f x: val) (γs γm γr: gname) (s: loc)
- (Φ: val → iProp Σ):
- inv N (srv_stack_inv R γs γm γr s ∗ srv_tokm_inv γm) ∗
- P ∗ ({{ R ∗ P }} f x {{ v, R ∗ Q v }}) ∗
- (∀ (p: loc) (ts: toks), installed_recp ts x Q -∗ evm γm p ts -∗(∃ hd, evs γs hd #p) -∗ Φ #p)
- ⊢ WP install f x #s {{ Φ }}.
+ Lemma install_spec R P Q (f x: val) (γm γr: gname) (s: loc):
+ {{{ inv N (srv_bag R γm γr s) ∗ P ∗ ({{ R ∗ P }} f x {{ v, R ∗ Q v }}) }}}
+ install f x #s
+ {{{ p ts, RET #p; installed_recp ts x Q ∗ inv N (p_inv R γm γr ts p) }}}.
Proof.
- iIntros "(#? & Hpx & Hf & HΦ)".
+ iIntros (Φ) "(#? & HP & Hf) HΦ".
wp_seq. wp_let. wp_let. wp_alloc p as "Hl".
iApply fupd_wp.
iMod (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
@@ -148,145 +114,73 @@ Section proof.
iMod (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
iMod (own_alloc (1%Qp, to_agree x)) as (γx) "Hx"; first done.
iMod (saved_prop_alloc (F:=(ofe_funCF val idCF)) Q) as (γq) "#?".
- iInv N as "[Hrs >Hm]" "Hclose".
- iDestruct "Hm" as (m) "[Hm HRm]".
- destruct (m !! p) eqn:Heqn.
- - (* old name *)
- iDestruct (big_sepM_delete (fun p _ => ∃ v : val, p ↦{1 / 2} v)%I m with "HRm") as "[Hp HRm]"=>//.
- iDestruct "Hp" as (?) "Hp". iExFalso. iApply bogus_heap; last by iFrame "Hl Hp". auto.
- - (* fresh name *)
- iDestruct (evmap_alloc _ _ _ m p (γx, γ1, γ3, γ4, γq) with "[Hm]") as ">[Hm1 #Hm2]"=>//.
- iDestruct "Hl" as "[Hl1 Hl2]".
- iMod ("Hclose" with "[HRm Hm1 Hl1 Hrs]").
- + iNext. iFrame. iExists (<[p := (∅, DecAgree (γx, γ1, γ3, γ4, γq))]> m). iFrame.
- iDestruct (big_sepM_insert _ m with "[-]") as "H"=>//.
- iSplitL "Hl1"; last by iAssumption. eauto.
- + iDestruct (own_update with "Hx") as ">[Hx1 Hx2]"; first by apply pair_l_frac_op_1'.
- iModIntro. wp_let. wp_bind ((push _) _).
- iApply install_push_spec=>//.
- iFrame "#". rewrite /evm /installed_s. iFrame.
- iSplitL "Hpx Hf".
- { (* TODO: Something somewhere can be simplified so that we don't have
- to add these dummy arguments any more. *)
- iExists (fun _ => P), (fun _ => Q). by iFrame. }
- iIntros "Hhd". wp_seq.
- iSpecialize ("HΦ" $! p (γx, γ1, γ3, γ4, γq) with "[-Hhd]")=>//.
- { rewrite /installed_recp. iFrame. iFrame "#". }
- by iApply ("HΦ" with "[]").
+ iDestruct (own_update with "Hx") as ">[Hx1 Hx2]"; first by apply pair_l_frac_op_1'.
+ iModIntro. wp_let. wp_bind (push _ _).
+ iMod (inv_alloc N _ (p_inv R γm γr (γx, γ1, γ3, γ4, γq) p)
+ with "[-HΦ Hx2 Ho3]") as "#HRx"; first eauto.
+ { iNext. iRight. iLeft. iExists f, x. iFrame.
+ iExists (λ _, P), (λ _ v, Q v).
+ iFrame. iFrame "#". }
+ iApply (push_spec N (p_inv' R γm γr) s #p
+ with "[-HΦ Hx2 Ho3]")=>//.
+ { iFrame "#". iExists (γx, γ1, γ3, γ4, γq), p.
+ iSplitR; first done. iFrame "#". }
+ iNext. iIntros "?".
+ wp_seq. iApply ("HΦ" $! p (γx, γ1, γ3, γ4, γq)).
+ iFrame. iFrame "#".
Qed.
- Lemma loop_iter_doOp_spec R (s hd: loc) (γs γm γr: gname) xs Φ:
- inv N (srv_stack_inv R γs γm γr s ∗ srv_tokm_inv γm) ∗ own γr (Excl ()) ∗ R ∗
- is_list' γs hd xs ∗ (own γr (Excl ()) -∗ R -∗ Φ #())
- ⊢ WP iter #hd doOp {{ Φ }}.
+ Definition f_spec (R: iProp Σ) (f: val) (Rf: iProp Σ) x :=
+ {{{ inv N R ∗ Rf }}}
+ f x
+ {{{ RET #(); Rf }}}.
+
+ Lemma doOp_f_spec R γm γr (p: loc) ts:
+ f_spec (p_inv R γm γr ts p) doOp (own γr (Excl ()) ∗ R)%I #p.
Proof.
- iIntros "(#? & Ho2 & HR & Hlist' & HΦ)".
- iApply (iter_spec N (p_inv R γm γr) Φ
- (* (fun v => v = #() ∗ own γr (Excl ()) ∗ R)%I *)
- γs s (own γr (Excl ()) ∗ R)%I (srv_tokm_inv γm) xs hd doOp doOp
- with "[-]")=>//.
- - rewrite /f_spec.
- iIntros (Φ' x) "(#? & Hev & [Hor HR] & HΦ')".
- iDestruct "Hev" as (xhd) "#Hev".
- wp_rec. wp_bind (! _)%E. iInv N as "[Hs >Hm]" "Hclose".
- iDestruct "Hs" as (gxs ghd) "[>Hghd [>Hgxs HRs]]". (* global xs, hd *)
- iDestruct "HRs" as (m) "[>Hom HRs]".
- (* acccess *)
- iDestruct (ev_map_witness _ _ _ m with "[Hev Hom]") as %H'; first by iFrame.
- iDestruct (big_sepM_delete_later (perR _) m with "HRs") as "[Hp HRm]"=>//.
- iDestruct "Hp" as (v') "[>% [Hpinv' >Hahd]]". inversion H. subst.
- iDestruct "Hpinv'" as (ts p'') "[>% [>#Hevm [Hp | [Hp | [Hp | Hp]]]]]"; subst.
- + iDestruct "Hp" as (y) "(>Hp & Hs)".
- wp_load. iMod ("Hclose" with "[-Hor HR Hev HΦ']").
- { iNext. iFrame. iExists gxs, ghd.
- iFrame "Hghd Hgxs". iExists m.
- iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
- iFrame. iExists #p''. iSplitR; first done. iExists ts, p''.
- iSplitR; first done. iFrame "#". iLeft. iExists y. iFrame. }
- iModIntro. wp_match. iApply ("HΦ'" with "[Hor HR]"). iFrame.
- + iDestruct "Hp" as (f' x') "(Hp & Hs)".
- wp_load. destruct ts as [[[[γx γ1] γ3] γ4] γq].
- iDestruct "Hs" as (P Q) "(Hx & Hpx & Hf' & HoQ & Ho1 & Ho4)".
- iAssert (|==> own γx (((1/2/2)%Qp, to_agree x') ⋅
- ((1/2/2)%Qp, to_agree x')))%I with "[Hx]" as ">[Hx1 Hx2]".
- { iDestruct (own_update with "Hx") as "?"; last by iAssumption.
- rewrite -{1}(Qp_div_2 (1/2)%Qp).
- by apply pair_l_frac_op'. }
- iMod ("Hclose" with "[-Hf' Ho1 Hx2 HR HoQ HΦ' Hpx]").
- { iNext. iFrame. iExists gxs, ghd.
- iFrame "Hghd Hgxs". iExists m.
- iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
- simpl. iFrame. iExists #p''. iSplitR; auto. rewrite /allocated.
- iExists (γx, γ1, γ3, γ4, γq), p''. iSplitR; auto.
- iFrame "#". iRight. iRight. iLeft. iExists f', x'. iFrame. }
- iModIntro. wp_match.
- wp_proj. wp_proj.
- wp_bind (f' _). iApply wp_wand_r. iSplitL "Hpx Hf' HR".
- { iApply "Hf'". iFrame. }
- iIntros (v) "[HR HQ]".
- wp_value. iInv N as "[Hs >Hm]" "Hclose".
- iDestruct "Hs" as (xs'' hd''') "[>Hhd [>Hxs HRs]]".
- iDestruct "HRs" as (m') "[>Hom HRs]".
- iDestruct (ev_map_witness _ _ _ m' with "[Hevm Hom]") as %?; first by iFrame.
- iDestruct (big_sepM_delete_later (perR _) m' with "HRs") as "[Hp HRm]"=>//.
- iDestruct "Hp" as (v'') "[>% [Hpinv' >Hhd'']]". inversion H1. subst.
- iDestruct "Hpinv'" as ([[[[γx' γ1'] γ3'] γ4'] γq'] p'''') "[>% [>#Hevm2 Hps]]".
- inversion H2. subst.
- destruct (decide (γ1 = γ1' ∧ γx = γx' ∧ γ3 = γ3' ∧ γ4 = γ4' ∧ γq = γq'))
- as [[? [? [? [? ?]]]]|Hneq]; subst.
- {
- iDestruct "Hps" as "[Hp | [Hp | [Hp | Hp]]]".
- * iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
- iApply excl_falso. iFrame.
- * iDestruct "Hp" as (? ?) "[>? Hs]". iDestruct "Hs" as (? ?) "(_ & _ & _ & _ & >Ho1' & _)".
- iApply excl_falso. iFrame.
- * iDestruct "Hp" as (? x5) ">(Hp & Hx & Hor & Ho4)".
- iDestruct "Hm" as (m2) "[Hom2 HRp]".
- iDestruct (ev_map_witness _ _ _ m2 with "[Hevm Hom2]") as %?; first by iFrame.
- iDestruct (big_sepM_delete _ m2 with "HRp") as "[HRk HRp]"=>//.
- iDestruct "HRk" as (?) "HRk".
- iDestruct (@mapsto_agree with "[$HRk $Hp]") as %->.
- iCombine "HRk" "Hp" as "Hp". wp_store.
- (* now close the invariant *)
- iDestruct (m_frag_agree' with "[Hx Hx2]") as "[Hx %]"; first iFrame.
- subst. rewrite Qp_div_2. iMod ("Hclose" with "[-HR Hor HΦ']").
- { iNext. iDestruct "Hp" as "[Hp1 Hp2]".
- iAssert (srv_tokm_inv γm) with "[Hp1 HRp Hom2]" as "HRp".
- { iExists m2. iFrame. iApply (big_sepM_delete _ m2)=>//.
- iFrame. eauto. }
- (* FIXME: These iFrame are really slow. *)
- iFrame. iExists xs''. iFrame. iExists hd'''. iFrame.
- iExists m'. iFrame.
- iDestruct (big_sepM_delete _ m' with "[-]") as "?"=>//.
- { simpl. iFrame. iExists #p''''.
- iSplitR; first auto. iExists (γx', γ1', γ3', γ4', γq'), p''''.
- iSplitR; first auto. iFrame "Hevm". iRight. iRight.
- iRight. iExists x5, v. iFrame.
- iExists Q. iFrame.
- }
- }
- iApply "HΦ'". iFrame.
- * iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
- iApply excl_falso. iFrame.
- }
- { iDestruct (evmap_frag_agree_split with "[]") as "%"; first iFrame "Hevm Hevm2".
- inversion H3. subst. by contradiction Hneq. }
- + destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (? x) "(_ & _ & >Ho2' & _)".
+ iIntros (Φ) "(#H1 & Hor & HR) HΦ".
+ wp_rec. wp_bind (! _)%E.
+ iInv N as "Hp" "Hclose".
+ iDestruct "Hp" as "[Hp | [Hp | [Hp | Hp]]]"; subst.
+ - iDestruct "Hp" as (y) "[>Hp Hts]".
+ wp_load. iMod ("Hclose" with "[-Hor HR HΦ]").
+ { iNext. iFrame "#". iLeft. iExists y. iFrame. }
+ iModIntro. wp_match. iApply ("HΦ" with "[Hor HR]"). iFrame.
+ - destruct ts as [[[[γx γ1] γ3] γ4] γq].
+ iDestruct "Hp" as (f x) "(>Hp & Hts)".
+ iDestruct "Hts" as (P Q) "(>Hx & Hpx & Hf' & HoQ & >Ho1 & >Ho4)".
+ iAssert (|==> own γx (((1/2/2)%Qp, to_agree x) ⋅
+ ((1/2/2)%Qp, to_agree x)))%I with "[Hx]" as ">[Hx1 Hx2]".
+ { iDestruct (own_update with "Hx") as "?"; last by iAssumption.
+ rewrite -{1}(Qp_div_2 (1/2)%Qp).
+ by apply pair_l_frac_op'. }
+ wp_load. iMod ("Hclose" with "[-Hf' Ho1 Hx2 HoQ HR HΦ Hpx]").
+ { iNext. iFrame. iFrame "#". iRight. iRight. iLeft. iExists f, x. iFrame. }
+ iModIntro. wp_match. wp_proj. wp_proj.
+ wp_bind (f _). iApply wp_wand_r. iSplitL "Hpx Hf' HR".
+ { iApply "Hf'". iFrame. }
+ iIntros (v) "[HR HQ]". wp_value.
+ iInv N as "Hx" "Hclose".
+ iDestruct "Hx" as "[Hp | [Hp | [Hp | Hp]]]"; subst.
+ * iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
iApply excl_falso. iFrame.
- + destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (x' y) "[Hp Hs]".
+ * iDestruct "Hp" as (? ?) "[>? Hs]". iDestruct "Hs" as (? ?) "(_ & _ & _ & _ & >Ho1' & _)".
+ iApply excl_falso. iFrame.
+ * iDestruct "Hp" as (? x5) ">(Hp & Hx & Hor & Ho4)".
+ wp_store. iDestruct (m_frag_agree' with "[Hx Hx2]") as "[Hx %]"; first iFrame.
+ subst. rewrite Qp_div_2. iMod ("Hclose" with "[-HR Hor HΦ]").
+ { iNext. iDestruct "Hp" as "[Hp1 Hp2]". iRight. iRight.
+ iRight. iExists x5, v. iFrame. iExists Q. iFrame. }
+ iApply "HΦ". iFrame.
+ * iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
+ iApply excl_falso. iFrame.
+ - destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (? x) "(_ & _ & >Ho2' & _)".
+ iApply excl_falso. iFrame.
+ - destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (x' y) "[Hp Hs]".
iDestruct "Hs" as (Q) "(>Hx & HoQ & HQxy & >Ho1 & >Ho4)".
- wp_load. iMod ("Hclose" with "[-HΦ' HR Hor]").
- { iNext. iFrame. iExists gxs, ghd.
- iFrame "Hghd Hgxs". iExists m.
- iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
- iFrame. iExists #p''. iSplitR; first auto. iExists (γx, γ1, γ3, γ4, γq), p''.
- iSplitR; auto. iFrame "#". iRight. iRight. iRight. iExists x', y. iFrame.
- iExists Q. iFrame. }
- iModIntro. wp_match.
- iApply "HΦ'". iFrame.
- - apply to_of_val.
- - iFrame "#". iFrame. iIntros "[Hor HR]".
- iApply ("HΦ" with "Hor HR").
+ wp_load. iMod ("Hclose" with "[-HΦ HR Hor]").
+ { iNext. iRight. iRight. iRight. iExists x', y. iFrame. iExists Q. iFrame. }
+ iModIntro. wp_match. iApply "HΦ". iFrame.
Qed.
Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()).
@@ -294,122 +188,111 @@ Section proof.
let '(γx, _, _, _, γq) := ts in
(∃ Q, own γx ((1 / 2)%Qp, to_agree x) ∗ saved_prop_own γq (Q x) ∗ Q x y)%I.
- Lemma try_srv_spec R (s: loc) (lk: val) (γs γr γm γlk: gname) Φ :
- inv N (srv_stack_inv R γs γm γr s ∗ srv_tokm_inv γm) ∗
+ Lemma loop_iter_doOp_spec R (γm γr: gname) xs:
+ ∀ (hd: loc),
+ {{{ is_list_R N (p_inv' R γm γr) hd xs ∗ own γr (Excl ()) ∗ R }}}
+ iter #hd doOp
+ {{{ RET #(); own γr (Excl ()) ∗ R }}}.
+ Proof.
+ induction xs as [|x xs' IHxs].
+ - iIntros (hd Φ) "[Hxs ?] HΦ".
+ simpl. wp_rec. wp_value. wp_let.
+ iDestruct "Hxs" as (?) "Hhd".
+ wp_load. wp_match. by iApply "HΦ".
+ - iIntros (hd Φ) "[Hxs HRf] HΦ". simpl.
+ iDestruct "Hxs" as (hd' ?) "(Hhd & #Hinv & Hxs')".
+ wp_rec. wp_value. wp_let. wp_bind (! _)%E.
+ iInv N as "H" "Hclose".
+ iDestruct "H" as (ts p) "[>% #?]". subst.
+ wp_load. iMod ("Hclose" with "[]").
+ { iNext. iExists ts, p. eauto. }
+ iModIntro. wp_match. wp_proj. wp_bind (doOp _).
+ iDestruct (doOp_f_spec R γm γr p ts) as "Hf".
+ iApply ("Hf" with "[HRf]").
+ { iFrame. iFrame "#". }
+ iNext. iIntros "HRf".
+ wp_seq. wp_proj. iApply (IHxs with "[-HΦ]")=>//.
+ iFrame "#"; first by iFrame. eauto.
+ Qed.
+
+ Lemma try_srv_spec R (s: loc) (lk: val) (γr γm γlk: gname) Φ :
+ inv N (srv_bag R γm γr s) ∗
is_lock N γlk lk (own γr (Excl ()) ∗ R) ∗ Φ #()
⊢ WP try_srv lk #s {{ Φ }}.
Proof.
- iIntros "(#? & #? & HΦ)".
- wp_seq. wp_let.
+ iIntros "(#? & #? & HΦ)". wp_seq. wp_let.
wp_bind (try_acquire _). iApply (try_acquire_spec with "[]"); first done.
iNext. iIntros ([]); last by (iIntros; wp_if).
- (* acquired the lock *)
iIntros "[Hlocked [Ho2 HR]]".
wp_if. wp_bind (! _)%E.
- iInv N as "[H >Hm]" "Hclose".
- iDestruct "H" as (xs' hd') "[>Hs [>Hxs HRs]]".
- wp_load. iDestruct (dup_is_list' with "[Hxs]") as ">[Hxs1 Hxs2]"; first by iFrame.
- iMod ("Hclose" with "[Hs Hxs1 HRs Hm]").
+ iInv N as "H" "Hclose".
+ iDestruct "H" as (xs' hd') "[>Hs Hxs]".
+ wp_load. iDestruct (dup_is_list_R with "[Hxs]") as ">[Hxs1 Hxs2]"; first by iFrame.
+ iMod ("Hclose" with "[Hs Hxs1]").
{ iNext. iFrame. iExists xs', hd'. by iFrame. }
- iModIntro. wp_let.
- wp_bind (iter _ _).
+ iModIntro. wp_let. wp_bind (iter _ _).
iApply wp_wand_r. iSplitL "HR Ho2 Hxs2".
- { iApply (loop_iter_doOp_spec R _ _ _ _ _ _ (fun v => own γr (Excl ()) ∗ R ∗ ⌜v = #()âŒ))%I=>//.
- iFrame "#". iFrame. iIntros "? ?". by iFrame. }
- iIntros (f') "[Ho [HR %]]". subst.
- wp_let. iApply (release_spec with "[Hlocked Ho HR]"); first iFrame "#∗".
+ { iApply (loop_iter_doOp_spec R _ _ _ _ (λ _, own γr (Excl ()) ∗ R)%I with "[-]")=>//.
+ iFrame "#". iFrame. eauto. }
+ iIntros (f') "[Ho HR]". wp_seq.
+ iApply (release_spec with "[Hlocked Ho HR]"); first iFrame "#∗".
iNext. iIntros. done.
Qed.
Lemma loop_spec R (p s: loc) (lk: val)
- (γs γr γm γlk: gname) (ts: toks) Φ:
- inv N (srv_stack_inv R γs γm γr s ∗ srv_tokm_inv γm) ∗
- is_lock N γlk lk (own γr (Excl ()) ∗ R) ∗
- own_γ3 ts ∗ evm γm p ts ∗
- (∃ hd, evs γs hd #p) ∗ (∀ x y, finished_recp ts x y -∗ Φ y)
- ⊢ WP loop #p #s lk {{ Φ }}.
+ (γs γr γm γlk: gname) (ts: toks):
+ {{{ inv N (srv_bag R γm γr s) ∗ inv N (p_inv R γm γr ts p) ∗
+ is_lock N γlk lk (own γr (Excl ()) ∗ R) ∗ own_γ3 ts }}}
+ loop #p #s lk
+ {{{ x y, RET y; finished_recp ts x y }}}.
Proof.
- iIntros "(#? & #? & Ho3 & #Hev & Hhd & HΦ)".
+ iIntros (Φ) "(#? & #? & #? & Ho3) HΦ".
iLöb as "IH". wp_rec. repeat wp_let.
- wp_bind (! _)%E. iInv N as "[Hinv >?]" "Hclose".
- iDestruct "Hinv" as (xs hd) "[>Hs [>Hxs HRs]]".
- iDestruct "HRs" as (m) "[>Hom HRs]".
- iDestruct "Hhd" as (hdp) "Hhd".
- destruct (m !! hdp) eqn:Heqn.
- - iDestruct (big_sepM_delete_later _ m with "HRs") as "[Hp Hrs]"=>//.
- iDestruct "Hp" as (?) "[>% [Hpr ?]]"; subst.
- iDestruct "Hpr" as (ts' p') "(>% & >Hp' & Hp)".
- subst. iDestruct (ev_map_witness _ _ _ m with "[Hom Hhd]") as %H=>//; first iFrame.
- rewrite Heqn in H. inversion H. subst.
- iDestruct (evmap_frag_agree_split with "[Hp']") as "%"; first iFrame "Hev Hp'". subst.
- destruct ts' as [[[[γx γ1] γ3] γ4] γq].
- iDestruct "Hp" as "[Hp | [Hp | [ Hp | Hp]]]".
- + iDestruct "Hp" as (?) "(_ & _ & >Ho3')".
- iApply excl_falso. iFrame.
- + iDestruct "Hp" as (f x) "(>Hp & Hs')".
- wp_load. iMod ("Hclose" with "[-Ho3 HΦ Hhd]").
- { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
- iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
- iFrame. iExists #p. iSplitR; first auto. iExists (γx, γ1, γ3, γ4, γq), p.
- iSplitR; first auto. iFrame.
- iRight. iLeft. iExists f, x. iFrame. }
- iModIntro. wp_match.
- wp_bind (try_srv _ _). iApply try_srv_spec=>//.
- iFrame "#". wp_seq.
- iAssert (∃ hd, evs γs hd #p)%I with "[Hhd]" as "Hhd"; eauto.
- by iApply ("IH" with "Ho3 Hhd").
- + iDestruct "Hp" as (f x) "(Hp & Hx & Ho2 & Ho4)".
- wp_load.
- iMod ("Hclose" with "[-Ho3 HΦ Hhd]").
- { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
- iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
- iFrame. iExists #p. iSplitR; auto. iExists (γx, γ1, γ3, γ4, γq), p.
- iSplitR; first auto. iFrame.
- iRight. iRight. iLeft. iExists f, x. iFrame. }
- iModIntro. wp_match.
- wp_bind (try_srv _ _). iApply try_srv_spec=>//.
- iFrame "#". wp_seq.
- iAssert (∃ hd, evs γs hd #p)%I with "[Hhd]" as "Hhd"; eauto.
- by iApply ("IH" with "Ho3 Hhd").
- + iDestruct "Hp" as (x y) "[>Hp Hs']". iDestruct "Hs'" as (Q) "(>Hx & HoQ & HQ & >Ho1 & >Ho4)".
- wp_load. iMod ("Hclose" with "[-Ho4 HΦ Hx HoQ HQ]").
- { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
- iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
- iFrame. iExists #p. iSplitR; auto. iExists (γx, γ1, γ3, γ4, γq), p.
- iSplitR; first auto. iFrame.
- iLeft. iExists y. iFrame. }
- iModIntro. wp_match. iApply ("HΦ" with "[-]"). iFrame.
- iExists Q. iFrame.
- - iExFalso. iApply (map_agree_none' _ _ _ m)=>//. iFrame "Hom".
- rewrite /ev. eauto.
+ wp_bind (! _)%E. iInv N as "Hp" "Hclose".
+ destruct ts as [[[[γx γ1] γ3] γ4] γq].
+ iDestruct "Hp" as "[Hp | [Hp | [ Hp | Hp]]]".
+ + iDestruct "Hp" as (?) "(_ & _ & >Ho3')".
+ iApply excl_falso. iFrame.
+ + iDestruct "Hp" as (f x) "(>Hp & Hs')".
+ wp_load. iMod ("Hclose" with "[Hp Hs']").
+ { iNext. iFrame. iRight. iLeft. iExists f, x. iFrame. }
+ iModIntro. wp_match. wp_bind (try_srv _ _). iApply try_srv_spec=>//.
+ iFrame "#". wp_seq. iApply ("IH" with "Ho3"); eauto.
+ + iDestruct "Hp" as (f x) "(Hp & Hx & Ho2 & Ho4)".
+ wp_load. iMod ("Hclose" with "[-Ho3 HΦ]").
+ { iNext. iFrame. iRight. iRight. iLeft. iExists f, x. iFrame. }
+ iModIntro. wp_match.
+ wp_bind (try_srv _ _). iApply try_srv_spec=>//.
+ iFrame "#". wp_seq. iApply ("IH" with "Ho3"); eauto.
+ + iDestruct "Hp" as (x y) "[>Hp Hs']".
+ iDestruct "Hs'" as (Q) "(>Hx & HoQ & HQ & >Ho1 & >Ho4)".
+ wp_load. iMod ("Hclose" with "[-Ho4 HΦ Hx HoQ HQ]").
+ { iNext. iFrame. iLeft. iExists y. iFrame. }
+ iModIntro. wp_match. iApply ("HΦ" with "[-]"). iFrame.
+ iExists Q. iFrame.
Qed.
- Lemma mk_flat_spec: mk_syncer_spec mk_flat.
+ Lemma mk_flat_spec (γm: gname): mk_syncer_spec mk_flat.
Proof.
iIntros (R Φ) "HR HΦ".
iMod (own_alloc (Excl ())) as (γr) "Ho2"; first done.
- iMod (own_alloc (◠(∅: tokmR) ⋅ ◯ ∅)) as (γm) "[Hm _]"; first by rewrite -auth_both_op.
- iAssert (srv_tokm_inv γm) with "[Hm]" as "Hm"; first eauto.
- { iExists ∅. iFrame. by rewrite big_sepM_empty. }
wp_seq. wp_bind (newlock _).
iApply (newlock_spec _ (own γr (Excl ()) ∗ R)%I with "[$Ho2 $HR]")=>//.
iNext. iIntros (lk γlk) "#Hlk".
wp_let. wp_bind (new_stack _).
- iApply (new_stack_spec' _ (p_inv _ γm γr))=>//.
- iFrame "Hm". iIntros (γ s) "#Hss".
+ iApply (new_bag_spec N (p_inv' R γm γr))=>//.
+ iNext. iIntros (s) "#Hss".
wp_let. iApply "HΦ". rewrite /synced.
- iAlways.
- iIntros (f). wp_let. iAlways.
+ iAlways. iIntros (f). wp_let. iAlways.
iIntros (P Q x) "#Hf".
- iIntros "!# Hp". wp_let.
- wp_bind (install _ _ _).
- iApply (install_spec R P Q)=>//.
- iFrame "#". iFrame "Hp". iSplitR; first iApply "Hf".
- iIntros (p [[[[γx γ1] γ3] γ4] γq]) "(Ho3 & Hx & HoQ) Hev Hhd".
+ iIntros "!# Hp". wp_let. wp_bind (install _ _ _).
+ iApply (install_spec R P Q f x γm γr s with "[-]")=>//.
+ { iFrame. iFrame "#". eauto. }
+ iNext. iIntros (p [[[[γx γ1] γ3] γ4] γq]) "[(Ho3 & Hx & HoQ) #?]".
wp_let. wp_bind (loop _ _ _).
- iApply loop_spec=>//.
- iFrame "#". iFrame.
- iIntros (? ?) "Hs".
+ iApply (loop_spec with "[-Hx HoQ]")=>//.
+ { iFrame "#". iFrame. }
+ iNext. iIntros (? ?) "Hs".
iDestruct "Hs" as (Q') "(Hx' & HoQ' & HQ')".
destruct (decide (x = a)) as [->|Hneq].
- iDestruct (saved_prop_agree with "[HoQ HoQ']") as "Heq"; first by iFrame.
diff --git a/theories/peritem.v b/theories/peritem.v
index 47abaac..dee70a5 100644
--- a/theories/peritem.v
+++ b/theories/peritem.v
@@ -1,183 +1,83 @@
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
+From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth gmap csum.
From iris.base_logic Require Import big_op.
-From iris_atomic Require Export treiber misc evmap.
+From iris_atomic Require Export treiber misc.
+From iris.base_logic.lib Require Import invariants namespaces.
Section defs.
- Context `{heapG Σ, !evidenceG loc val unitR Σ} (N: namespace).
+ Context `{heapG Σ} (N: namespace).
Context (R: val → iProp Σ) `{∀ x, TimelessP (R x)}.
- Definition allocated hd := (∃ q v, hd ↦{q} v)%I.
-
- Definition evs (γ: gname) := ev loc val γ.
-
- Fixpoint is_list' (γ: gname) (hd: loc) (xs: list val) : iProp Σ :=
+ Fixpoint is_list_R (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
+ | x :: xs => (∃ (hd': loc) q, hd ↦{q} SOMEV (x, #hd') ∗ inv N (R x) ∗ is_list_R 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_bag_R xs s := (∃ hd: loc, s ↦ #hd ∗ is_list_R hd xs)%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,
- is_list' γ hd xs ⊢ |==> is_list' γ hd xs ∗ is_list' γ hd xs.
+ Lemma dup_is_list_R : ∀ xs hd,
+ is_list_R hd xs ⊢ |==> is_list_R hd xs ∗ is_list_R 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 "Hs" as (hd' q) "([Hhd Hhd'] & #Hinv & Hs')".
iDestruct (IHxs' with "[Hs']") as ">[Hs1 Hs2]"; first by iFrame.
iModIntro. iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
Qed.
-
- Lemma extract_is_list γ : ∀ xs hd,
- 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'] & Hev & Hs')".
- iDestruct (IHxs' with "[Hs']") as ">[Hs1 Hs2]"; first by iFrame.
- iModIntro. 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),
- inv N ((∃ xs, is_stack' γ xs s) ∗ RI) ∗ (∃ hd, evs γ hd x) ∗
- Rf ∗ (Rf -∗ Φ #())
- ⊢ WP f x {{ Φ }}.
End defs.
Section proofs.
- Context `{heapG Σ, !evidenceG loc val unitR Σ} (N: namespace).
+ Context `{heapG Σ} (N: namespace).
Context (R: val → iProp Σ).
-Lemma new_stack_spec' Φ RI:
- RI ∗ (∀ γ s : loc, inv N ((∃ xs, is_stack' R γ xs s) ∗ RI) -∗ Φ #s)
- ⊢ WP new_stack #() {{ Φ }}.
+ Definition bag_inv s: iProp Σ := inv N (∃ xs, is_bag_R N R xs s)%I.
+
+ Lemma new_bag_spec:
+ {{{ True }}} new_stack #() {{{ s, RET #s; bag_inv s }}}.
Proof.
- iIntros "(HR & HΦ)". iApply wp_fupd.
- iMod (own_alloc (◠(∅: evmapR loc val unitR) ⋅ ◯ ∅)) as (γ) "[Hm Hm']".
- { apply auth_valid_discrete_2. done. }
+ iIntros (Φ) "HΦ". iApply wp_fupd.
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)). }
- iMod (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),
- f_spec N R γ xs s f' Rf RI → to_val f = Some f' →
- 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' ? ?) "(#? & Hxs1 & HRf & HΦ)".
- iDestruct "Hxs1" as (q) "Hhd".
- wp_rec. wp_value. wp_let. wp_load. wp_match. by iApply "HΦ".
- - simpl. iIntros (hd f f' Hf ?) "(#? & Hxs1 & HRf & HΦ)".
- iDestruct "Hxs1" as (hd2 q) "(Hhd & Hev & Hhd2)".
- wp_rec. wp_value. wp_let. wp_load. wp_match. wp_proj.
- wp_bind (f' _). iApply Hf=>//. iFrame "#".
- iSplitL "Hev"; first eauto. iFrame. iIntros "HRf".
- wp_seq. wp_proj. iApply (IHxs' with "[-]")=>//.
- + apply to_of_val.
- + iFrame "#". by iFrame.
+ iAssert ((∃ xs, is_bag_R N R xs s))%I with "[-HΦ]" as "Hxs".
+ { iFrame. iExists [], l.
+ iFrame. simpl. eauto. }
+ iMod (inv_alloc N _ (∃ xs : list val, is_bag_R N R xs s)%I with "[-HΦ]") as "#?"; first eauto.
+ iApply "HΦ". iFrame "#".
Qed.
- Lemma push_spec Φ γ (s: loc) (x: val) RI:
- R x ∗ inv N ((∃ xs, is_stack' R γ xs s) ∗ RI) ∗ ((∃ hd, evs γ hd x) -∗ Φ #())
- ⊢ WP push #s x {{ Φ }}.
+ Lemma push_spec (s: loc) (x: val):
+ {{{ R x ∗ bag_inv s }}} push #s x {{{ RET #() ; inv N (R x) }}}.
Proof.
- iIntros "(HRx & #? & HΦ)".
- iDestruct (push_atomic_spec s x) 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 *)
- iMod (fupd_intro_mask' (⊤ ∖ nclose N) ∅) as "Hvs"; first set_solver.
- iModIntro. iExists (xs, hd).
- iFrame "Hs Hxs'1". iSplit.
- + (* provide a way to rollback *)
- iIntros "[Hs Hl']".
- iMod "Hvs". iMod ("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.
- iMod "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'')".
- iCombine "Hhd'1" "Hhd'2" as "Hhd".
- 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.
- }
- iMod ("Hclose" with "[-]").
- { iNext. iFrame. iExists (x::xs).
- iExists hd'. iFrame.
- iExists hd, (1/2)%Qp. by iFrame.
- }
- iModIntro. iSplitL; last auto. by iExists hd'.
- - iApply wp_wand_r. iSplitL "HRx Hpush".
- + by iApply "Hpush".
- + iIntros (?) "[? %]". subst.
- by iApply "HΦ".
+ iIntros (Φ) "(HRx & #?) HΦ".
+ iLöb as "IH". wp_rec. wp_let.
+ wp_bind (! _)%E.
+ iInv N as "H1" "Hclose".
+ iDestruct "H1" as (xs hd) "[>Hs H1]".
+ wp_load. iMod ("Hclose" with "[Hs H1]").
+ { iNext. iFrame. iExists xs, hd. iFrame. }
+ iModIntro. wp_let. wp_alloc l as "Hl".
+ wp_let. wp_bind (CAS _ _ _)%E.
+ iInv N as "H1" "Hclose".
+ iDestruct "H1" as (xs' hd') "[>Hs H1]".
+ destruct (decide (hd = hd')) as [->|Hneq].
+ - wp_cas_suc.
+ iMod (inv_alloc N _ (R x) with "[HRx]") as "#HRx"; first eauto.
+ iMod ("Hclose" with "[Hs Hl H1]").
+ { iNext. iFrame. iExists (x::xs'), l.
+ iFrame. simpl. iExists hd', 1%Qp. iFrame.
+ by iFrame "#". }
+ iModIntro. wp_if. by iApply "HΦ".
+ - wp_cas_fail.
+ iMod ("Hclose" with "[Hs H1]").
+ { iNext. iFrame. iExists (xs'), hd'. iFrame. }
+ iModIntro. wp_if. iApply ("IH" with "HRx").
+ by iNext.
Qed.
End proofs.
--
GitLab