From 2d33ef8064c7902545adb1d6691e74630b2a9fe4 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 16 Nov 2020 12:14:22 +0100
Subject: [PATCH] fix helping_wrapper.v
---
_CoqProject | 1 +
.../experimental/helping/helping_wrapper.v | 104 ++++++++++--------
2 files changed, 57 insertions(+), 48 deletions(-)
diff --git a/_CoqProject b/_CoqProject
index e7a89a1..54ea159 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -57,6 +57,7 @@ theories/examples/coinflip.v
theories/experimental/helping/offers.v
theories/experimental/helping/helping_stack.v
+theories/experimental/helping/helping_wrapper.v
theories/experimental/hocap/counter.v
theories/experimental/hocap/ticket_lock.v
diff --git a/theories/experimental/helping/helping_wrapper.v b/theories/experimental/helping/helping_wrapper.v
index b197ef2..ffa9be5 100644
--- a/theories/experimental/helping/helping_wrapper.v
+++ b/theories/experimental/helping/helping_wrapper.v
@@ -46,19 +46,29 @@ Definition mk_helping : val := λ: "new_ds",
(λ: <>, wrap_pop "f1" "mb",
λ: "x", wrap_push "f2" "mb" "x").
+(** * Logical theory of an offer registry *)
+(** We will use an "offer registery". It associates for each offer a
+value that is being offered and a potential thread with the
+continuation that accepts the offer, if it is present. *)
+
Canonical Structure ectx_itemO := leibnizO ectx_item.
-Definition offerReg := gmap loc (val * gname * nat * (list ectx_item)).
+(* TODO: move !! *)
+Canonical Structure ref_idO := leibnizO ref_id.
+Global Instance ref_id_inhabited : Inhabited ref_id.
+Proof. split. apply (RefId 0 []). Qed.
+
+Definition offerReg := gmap loc (val * gname * ref_id).
Definition offerRegR :=
- gmapUR loc (agreeR (prodO valO (prodO gnameO (prodO natO (listO ectx_itemO))))).
+ gmapUR loc (agreeR (prodO valO (prodO gnameO ref_idO))).
Class offerRegPreG Σ := OfferRegPreG {
offerReg_inG :> authG Σ offerRegR
}.
-Definition offerize (x : (val * gname * nat * (list ectx_item))) :
- (agreeR (prodO valO (prodO gnameO (prodO natO (listO ectx_itemO))))) :=
+Definition offerize (x : (val * gname * ref_id)) :
+ (agreeR (prodO valO (prodO gnameO ref_idO))) :=
match x with
- | (v, γ, n, K) => to_agree (v, (γ, (n, K)))
+ | (v, γ, k) => to_agree (v, (γ, k))
end.
Definition to_offer_reg : offerReg -> offerRegR := fmap offerize.
@@ -66,32 +76,32 @@ Definition to_offer_reg : offerReg -> offerRegR := fmap offerize.
Lemma to_offer_reg_valid N : ✓ to_offer_reg N.
Proof.
intros l. rewrite lookup_fmap. case (N !! l); simpl; try done.
- intros [[[v γ] n] K]; simpl. done.
+ intros [[v γ] k]; simpl. done.
Qed.
Section offerReg_rules.
Context `{!offerRegPreG Σ, !offerG Σ}.
Lemma offerReg_alloc (o : loc) (v : val) (γ : gname)
- (j : nat) (K : list ectx_item) (γo : gname) (N : offerReg) :
+ (k : ref_id) (γo : gname) (N : offerReg) :
N !! o = None →
own γo (◠to_offer_reg N)
- ==∗ own γo (◠to_offer_reg (<[o:=(v, γ, j, K)]> N))
- ∗ own γo (◯ {[o := offerize (v, γ, j, K)]}).
+ ==∗ own γo (◠to_offer_reg (<[o:=(v, γ, k)]> N))
+ ∗ own γo (◯ {[o := offerize (v, γ, k)]}).
Proof.
iIntros (HNo) "HN".
iMod (own_update with "HN") as "[HN Hfrag]".
{ eapply auth_update_alloc.
- eapply (alloc_singleton_local_update _ o (to_agree (v, (γ, (j, K))))); try done.
+ eapply (alloc_singleton_local_update _ o (to_agree (v, (γ, k)))); try done.
by rewrite /to_offer_reg lookup_fmap HNo. }
iFrame. by rewrite /to_offer_reg fmap_insert.
Qed.
Lemma offerReg_frag_lookup (o : loc) (v : val) (γ : gname)
- (j : nat) (K : list ectx_item) (γo : gname) (N : offerReg) :
+ k (γo : gname) (N : offerReg) :
own γo (◠to_offer_reg N)
- -∗ own γo (◯ {[o := to_agree (v, (γ, (j, K)))]})
- -∗ ⌜N !! o = Some (v, γ, j, K)âŒ.
+ -∗ own γo (◯ {[o := to_agree (v, (γ, k))]})
+ -∗ ⌜N !! o = Some (v, γ, k)âŒ.
Proof.
iIntros "HN Hfrag".
iDestruct (own_valid_2 with "HN Hfrag") as %Hfoo.
@@ -110,23 +120,23 @@ Section offerReg_rules.
intros Hav.
rewrite -(inj Some _ _ Hav).
rewrite Some_included_total.
- destruct av' as [[[??]?]?]. simpl.
+ destruct av' as [[??]?]. simpl.
rewrite to_agree_included.
fold_leibniz.
intros. by simplify_eq.
Qed.
Lemma offerReg_lookup_frag (o : loc) (v : val) (γ : gname)
- (j : nat) (K : list ectx_item) (γo : gname) (N : offerReg) :
- N !! o = Some (v, γ, j, K) →
+ (k : ref_id) (γo : gname) (N : offerReg) :
+ N !! o = Some (v, γ, k) →
own γo (◠to_offer_reg N)
- ==∗ own γo (◯ {[o := to_agree (v, (γ, (j, K)))]})
+ ==∗ own γo (◯ {[o := to_agree (v, (γ, k))]})
∗ own γo (◠to_offer_reg N).
Proof.
iIntros (HNo) "Hown".
iMod (own_update with "[Hown]") as "Hown".
{ eapply (auth_update (to_offer_reg N) ∅).
- eapply (op_local_update_discrete _ ∅ {[o := to_agree (v, (γ, (j, K)))]}).
+ eapply (op_local_update_discrete _ ∅ {[o := to_agree (v, (γ, k))]}).
intros. intros i. destruct (decide (i = o)); subst; rewrite lookup_op.
+ rewrite lookup_singleton lookup_fmap HNo.
rewrite -Some_op.
@@ -142,7 +152,7 @@ Section offerReg_rules.
rewrite right_id. iFrame "Hown". }
iDestruct "Hown" as "[Ho Hown]".
rewrite right_id. iFrame.
- assert ({[o := to_agree (v, (γ, (j, K)))]} ⋅ to_offer_reg N ≡ to_offer_reg N) as Hfoo.
+ assert ({[o := to_agree (v, (γ, k))]} ⋅ to_offer_reg N ≡ to_offer_reg N) as Hfoo.
{ intro i.
rewrite /to_offer_reg lookup_merge !lookup_fmap.
destruct (decide (i = o)); subst.
@@ -160,9 +170,9 @@ Section offerReg_rules.
Definition offerInv `{!relocG Σ} (N : offerReg) (f : val) : iProp Σ :=
([∗ map] l ↦ w ∈ N,
match w with
- | (v,γ,j,K) => is_offer γ l
- (j ⤇ fill K (f (of_val v))%E)
- (j ⤇ fill K #())
+ | (v,γ,k) => is_offer γ l
+ (refines_right k (f (of_val v))%E)
+ (refines_right k #())
end)%I.
Lemma offerInv_empty `{!relocG Σ} (f : val) : ⊢ offerInv ∅ f.
@@ -174,7 +184,7 @@ Section offerReg_rules.
rewrite /offerInv. iIntros "HN Ho".
iAssert (⌜is_Some (N !! o)⌠→ False)%I as %Hbaz.
{
- iIntros ([[[[? ?] ?] ?] HNo]).
+ iIntros ([[[? ?] ?] HNo]).
rewrite (big_sepM_lookup _ N o _ HNo).
iApply (is_offer_exclusive with "HN Ho").
}
@@ -183,6 +193,7 @@ Section offerReg_rules.
End offerReg_rules.
+
(** * Refinement proof *)
Section refinement.
Context `{!relocG Σ, !offerRegPreG Σ, !offerG Σ}.
@@ -193,25 +204,27 @@ Section refinement.
This is also the only place where we need to unfold the definition of the refinement proposition. *)
Lemma revoke_offer_l γ off E K (v : val) e1 e2 A :
offer_token γ -∗
- (∀ j K', (j ⤇ fill K' e1) ={E, ⊤, E}▷=∗
- ▷ is_offer γ off (j ⤇ fill K' e1) (j ⤇ fill K' e2) ∗
- ▷ (is_offer γ off (j ⤇ fill K' e1) (j ⤇ fill K' e2) -∗
+ (∀ k, refines_right k e1 ={E}[⊤]▷=∗
+ ▷ is_offer γ off (refines_right k e1) (refines_right k e2) ∗
+ ▷ (is_offer γ off (refines_right k e1) (refines_right k e2) -∗
((REL fill K (of_val NONEV) << e2 @ E : A)
∧ (REL fill K (of_val $ SOMEV v) << e1 @ E : A)))) -∗
REL fill K (revoke_offer (v, #off)%V) << e1 @ E : A.
Proof.
iIntros "Hγ Hlog".
- rewrite {3}refines_eq /refines_def.
- iIntros (j K') "#Hs Hj".
- iMod ("Hlog" with "Hj") as "Hlog".
- iModIntro. iApply wp_bind. (* TODO: why do we have to use wp_bind here? *)
+ iApply refines_split.
+ iIntros (k) "Hk".
+ iMod ("Hlog" with "Hk") as "Hlog".
+ iApply refines_wp_l.
wp_apply (wp_revoke_offer with "Hγ [-]").
iNext. iMod "Hlog" as "[Hoff Hcont]". iModIntro.
iFrame "Hoff". iNext. iSplit.
- iIntros "Hoff". iDestruct ("Hcont" with "Hoff") as "[Hcont _]".
- rewrite refines_eq. by iApply "Hcont".
+ iIntros "Hk". iApply refines_left_fupd.
+ iApply (refines_combine with "Hcont Hk").
- iIntros "Hoff". iDestruct ("Hcont" with "Hoff") as "[_ Hcont]".
- rewrite refines_eq. by iApply "Hcont".
+ iIntros "Hk". iApply refines_left_fupd.
+ iApply (refines_combine with "Hcont Hk").
Qed.
(** We will also use the following instances for splitting and
@@ -234,17 +247,17 @@ Section refinement.
Definition I A oname (mb : loc) (push_f : val) : iProp Σ :=
(∃ (N : offerReg),
(mb ↦ NONEV (* the mailbox is either empty or contains an offer that is in the registry *)
- ∨ (∃ (l : loc) v1 v2 γ j K,
+ ∨ (∃ (l : loc) v1 v2 γ k,
A v1 v2
∗ mb ↦ SOMEV (v1, #l)
- ∗ ⌜N !! l = Some (v2, γ, j, K)âŒ))
+ ∗ ⌜N !! l = Some (v2, γ, k)âŒ))
∗ own oname (◠to_offer_reg N)
∗ offerInv N push_f)%I.
Lemma wrap_pop_refinement A (pop1 pop2 push2 : val) γo mb :
inv iN (I A γo mb push2) -∗
- (∀ e v2 j K, j ⤇ fill K (push2 (of_val v2)) -∗
- (j ⤇ fill K #() -∗ REL e << SOMEV v2 @ ⊤∖↑iN : () + A) -∗
+ (∀ e v2 k, refines_right k (push2 (of_val v2)) -∗
+ (refines_right k #() -∗ REL e << SOMEV v2 @ ⊤∖↑iN : () + A) -∗
REL e << pop2 #() @ ⊤∖↑iN : () + A) -∗
(REL pop1 << pop2 : () → () + A) -∗
REL wrap_pop pop1 #mb
@@ -265,7 +278,7 @@ Section refinement.
{ iNext. iExists N; by iFrame. }
iApply (refines_app with "Hpop"). by rel_values.
- (* YES OFFER *)
- iDestruct "Hmb" as (l v1 v2 γ j K) "(#Hv & Hmb & >HNl)".
+ iDestruct "Hmb" as (l v1 v2 γ k) "(#Hv & Hmb & >HNl)".
iDestruct "HNl" as %HNl.
rewrite /offerInv big_sepM_lookup_acc; eauto. iSimpl in "HN".
iDestruct "HN" as "[HNl HN]".
@@ -276,7 +289,7 @@ Section refinement.
iMod ("Hcl" with "[-Hlown IH Hpop HpopGhost]") as "_".
{ iNext. iExists _. iFrame.
iSplitL "Hmb".
- - iRight. iExists _, _, _, _, _, _.
+ - iRight. iExists _, _, _, _, _.
eauto with iFrame.
- by iApply "HN". }
@@ -328,20 +341,20 @@ Section refinement.
iAssert (∃ v, ▷ mb ↦ v)%I with "[Hmb]" as (v) "Hmb".
{ iDestruct "Hmb" as "[Hmb | Hmb]".
- iExists NONEV; eauto.
- - iDestruct "Hmb" as (l m1 m2 γ' j K) "(Hm & Hmb & ?)".
+ - iDestruct "Hmb" as (l m1 m2 γ' k) "(Hm & Hmb & ?)".
iExists (SOMEV (m1, #l)); eauto. }
iExists _; iFrame; iNext.
iIntros "Hmb".
rel_pures_l.
rel_apply_l (revoke_offer_l with "Htok").
- iIntros (j K') "Hj". iSpecialize ("Hoff" with "Hj").
+ iIntros (j) "Hj". iSpecialize ("Hoff" with "Hj").
iDestruct (offerInv_excl with "HN Hoff") as %?.
- iMod (offerReg_alloc off h2 γ j K' with "HNown") as "[HNown #Hfrag]"; eauto.
+ iMod (offerReg_alloc off h2 γ with "HNown") as "[HNown #Hfrag]"; eauto.
iMod ("Hcl" with "[-Hpush]") as "_".
{ iNext. iExists _. iFrame "HNown".
iSplitL "Hmb".
- - iRight. iExists off, h1, h2, _, _, _. iFrame "Hmb Hh".
+ - iRight. iExists off, h1, h2, _, _. iFrame "Hmb Hh".
iPureIntro. by rewrite lookup_insert.
- rewrite /offerInv big_sepM_insert; eauto with iFrame. }
iModIntro. iNext.
@@ -395,23 +408,18 @@ Section stack_example.
Proof.
iIntros "#Hinv #Hstack".
iApply (wrap_pop_refinement with "Hinv [] []").
- { iIntros (e v2 j K) "Hj Hcont".
+ { iIntros (e v2 j) "Hj Hcont".
rel_pures_r.
iDestruct "Hstack" as (st1l lk1 ->) "[#HstI #Hstack]".
iInv stackN as (ls1 ls2) "(Hst1 & >Hst2 & HA)" "Hcl".
iDestruct "Hst2" as (st2l lk2 ->) "[Hlk Hst2]".
tp_rec j. tp_pures j. tp_rec j. tp_pures j. tp_rec j.
unlock is_locked_r. iDestruct "Hlk" as (lk' ->) "Hl".
- (* TODO: make all the tp_ tactics work without the need for an explicit Fupd *)
- iApply refines_spec_ctx. iIntros "#HÏ".
- iApply fupd_refines.
- (* because we manually applied `fupd_refines`, the tactical `with_spec_ctx` doesn't work anymore *)
tp_cmpxchg_suc j.
tp_pures j. tp_rec j. tp_pures j.
tp_load j. tp_pures j.
tp_store j. tp_pures j.
tp_rec j. tp_store j.
- iClear "HÏ". iModIntro.
rel_apply_r (refines_CG_pop_suc_r with "[Hst2 Hl]").
{ iExists st2l,#lk'. rewrite /is_locked_r. by eauto with iFrame. }
iIntros "Hst2".
--
GitLab