From 61f3af14d6cd5e6b0662f384d8fa59547b434e22 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 3 Jul 2019 11:46:03 +0200
Subject: [PATCH] Clean up the stack helping proof.
---
theories/experimental/helping/helping_stack.v | 482 ++++++++----------
1 file changed, 220 insertions(+), 262 deletions(-)
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index ed19fff..e0a3b69 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -1,20 +1,22 @@
(* ReLoC -- Relational logic for fine-grained concurrency *)
(** Fine-grained stack with helping.
Based on the case study <https://iris-project.org/pdfs/2017-case-study-concurrent-stacks-with-helping.pdf> *)
-(* It demonstrates how to do _helping_ in Iris. Note that for this
+(** This demonstrates how to do _helping_ in ReLoC/Iris. Note that for this
proof we cannot stay inside the ReLoC and we have to unfold some stuff
to get to the actual model of logical relations. The initial version
of this code was written togethe witr Amin Timany around 2017 *)
-(* TODO: get rid of the rec_unfold's here *)
From iris.algebra Require Import auth gmap agree list excl.
From iris.base_logic.lib Require Import auth.
-From reloc Require Export reloc experimental.helping.mailbox examples.stack.CG_stack lib.list.
+From reloc Require Export reloc experimental.helping.mailbox.
+From reloc Require Import examples.stack.CG_stack lib.list.
+(** * Source code *)
+(** All the operations are paramaterized by a mailbox, see mailbox.v for details *)
Definition pop_st : val := rec: "pop" "r" "get" :=
match: "get" #() with
NONE =>
- (match: rec_unfold !"r" with
+ (match: !"r" with
NONE => NONE
| SOME "l" =>
let: "pair" := !"l" in
@@ -46,13 +48,15 @@ Definition mk_stack : val := λ: "_",
(λ: <>, pop_st "r" (λ: <>, "get" "mb"),
λ: "x", push_st "r" (λ: "n", "put" "mb" "n") "x").
+(** The coarse-grained version *)
Definition CG_mkstack : val := λ: "_",
let: "st" := CG_new_stack #() in
(λ: <>, CG_locked_pop "st", λ: "x", CG_locked_push "st" "x").
-(** Algebras needed for the refinement *)
+(** * Algebras needed for the refinement *)
Canonical Structure ectx_itemO := leibnizO ectx_item.
+(** An offer registry associates with each offer (loc), a value that is being offered, and a potential thread (gname, nat, ectx) that accepts the offer, if it is present. *)
Definition offerReg := gmap loc (val * gname * nat * (list ectx_item)).
Definition offerRegR :=
@@ -63,54 +67,30 @@ Class offerRegPreG Σ := OfferRegPreG {
offerReg_inG :> authG Σ offerRegR
}.
-Section refinement.
- Context `{!relocG Σ,!offerRegPreG Σ, !channelG Σ}.
+(** ** Definitions concerning offers *)
+Definition offerize (x : (val * gname * nat * (list ectx_item))) :
+ (agreeR (prodO valO (prodO gnameO (prodO natO (listO ectx_itemO))))) :=
+ match x with
+ | (v, γ, n, K) => to_agree (v, (γ, (n, K)))
+ end.
- Definition offerize (x : (val * gname * nat * (list ectx_item))) :
- (agreeR (prodO valO (prodO gnameO (prodO natO (listO ectx_itemO))))) :=
- match x with
- | (v, γ, n, K) => to_agree (v, (γ, (n, K)))
- end.
- 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.
- Qed.
+Definition to_offer_reg : offerReg -> offerRegR := fmap offerize.
- Definition stackN := nroot .@ "stacked".
+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.
+Qed.
- Definition offerInv (N : offerReg) (st' : val) : iProp Σ :=
- ([∗ map] l ↦ w ∈ N,
- match w with
- | (v,γ,j,K) => ∃ (c : nat),
- l ↦ #c ∗
- (⌜c = 0⌠∗ j ⤇ fill K (CG_locked_push st' (of_val v))%E
- ∨ ⌜c = 1⌠∗ (j ⤇ fill K #() ∨ own γ (Excl ()))
- ∨ ⌜c = 2⌠∗ own γ (Excl ()))%nat
- end)%I.
+(** * Refinement proof *)
+Section refinement.
+ Context `{!relocG Σ, !offerRegPreG Σ, !channelG Σ}.
- Lemma offerInv_empty (st' : val) :
- offerInv ∅ st'.
- Proof. by rewrite /offerInv big_sepM_empty. Qed.
+ Implicit Type A : lrel Σ.
- Lemma offerInv_excl (N : offerReg) (st' : val) (o : loc) (v : val) :
- offerInv N st' -∗ o ↦ v -∗ ⌜N !! o = NoneâŒ.
- Proof.
- rewrite /offerInv.
- iIntros "HN Ho".
- iAssert (⌜is_Some (N !! o)⌠→ False)%I as %Hbaz.
- {
- iIntros ([[[[? ?] ?] ?] HNo]).
- rewrite (big_sepM_lookup _ N o _ HNo).
- iDestruct "HN" as (c) "[HNo ?]".
- iDestruct (gen_heap.mapsto_valid_2 with "Ho HNo") as %Hfoo.
- compute in Hfoo. contradiction.
- }
- iPureIntro.
- destruct (N !! o); eauto. exfalso. apply Hbaz; eauto.
- Qed.
+ Definition stackN := nroot .@ "stacked".
+ (** ** Lemmas for modifying the offer registery *)
Lemma offerReg_alloc (o : loc) (v : val) (γ : gname)
(j : nat) (K : list ectx_item) (γo : gname) (N : offerReg) :
N !! o = None →
@@ -197,43 +177,39 @@ Section refinement.
by rewrite Hfoo.
Qed.
- Definition stackRel (v1 v2 : val) : iProp Σ :=
- lrel_list lrel_int v1 v2.
- Instance stackRel_persistent v1 v2 : Persistent (stackRel v1 v2).
- Proof. apply _. Qed.
- Lemma stackRel_empty : stackRel (InjLV #()) (InjLV #()).
- Proof. apply lrel_list_nil. Qed.
- Hint Resolve stackRel_empty.
- Lemma stackRel_cons (n : Z) t1 t2 :
- ▷ stackRel t1 t2 -∗ stackRel (InjRV (#n, t1)) (InjRV (#n, t2)).
- Proof.
- iIntros "#Hs".
- iApply (lrel_list_cons with "[] Hs").
- iNext. iExists _. iSplit; eauto.
- Qed.
- Lemma stackRel_unfold v1 v2 :
- stackRel v1 v2
- ⊣⊢
- (â–· ((⌜v1 = (InjLV #())⌠∧ ⌜v2 = (InjLV #())âŒ)
- ∨ ∃ (n : Z) t1 t2, ⌜v1 = (InjRV (#n, t1))âŒ
- ∧ ⌜v2 = (InjRV (#n, t2))âŒ
- ∧ stackRel t1 t2))%I.
+ (** ** The offer invariant *)
+ Definition offerInv (N : offerReg) (st' : val) : iProp Σ :=
+ ([∗ map] l ↦ w ∈ N,
+ match w with
+ | (v,γ,j,K) => ∃ (c : nat),
+ l ↦ #c ∗
+ (⌜c = 0⌠∗ j ⤇ fill K (CG_locked_push st' (of_val v))%E
+ ∨ ⌜c = 1⌠∗ (j ⤇ fill K #() ∨ own γ (Excl ()))
+ ∨ ⌜c = 2⌠∗ own γ (Excl ()))%nat
+ end)%I.
+
+ Lemma offerInv_empty (st' : val) :
+ offerInv ∅ st'.
+ Proof. by rewrite /offerInv big_sepM_empty. Qed.
+
+ Lemma offerInv_excl (N : offerReg) (st' : val) (o : loc) (v : val) :
+ offerInv N st' -∗ o ↦ v -∗ ⌜N !! o = NoneâŒ.
Proof.
- rewrite /stackRel /=.
- rewrite lrel_list_unfold.
- iSplit.
- - iIntros "H". iNext.
- iDestruct "H" as "[H|H]"; first by iLeft.
- iRight. iDestruct "H" as (w1 w2 t1 t2) "(-> & -> & Hw & Ht)".
- iDestruct "Hw" as (n) "[-> ->]".
- iExists n,_,_. eauto with iFrame.
- - iIntros "H". iNext.
- iDestruct "H" as "[H|H]"; first by iLeft.
- iRight. iDestruct "H" as (n t1 t2) "(->&->&Hl)".
- iExists #n,#n,_,_. repeat iSplit; eauto with iFrame.
+ rewrite /offerInv.
+ iIntros "HN Ho".
+ iAssert (⌜is_Some (N !! o)⌠→ False)%I as %Hbaz.
+ {
+ iIntros ([[[[? ?] ?] ?] HNo]).
+ rewrite (big_sepM_lookup _ N o _ HNo).
+ iDestruct "HN" as (c) "[HNo ?]".
+ iDestruct (gen_heap.mapsto_valid_2 with "Ho HNo") as %Hfoo.
+ compute in Hfoo. contradiction.
+ }
+ iPureIntro.
+ destruct (N !! o); eauto. exfalso. apply Hbaz; eauto.
Qed.
-
+ (** Linking two contents of the two stacks together. *)
Definition oloc_to_val (ol: option loc) : val :=
match ol with
| None => NONEV
@@ -245,92 +221,67 @@ Section refinement.
Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
Proof. intros [|][|]; simpl; congruence. Qed.
- Notation D := (olocO -d> valO -d> iProp Σ).
+ Local Notation D := (olocO -d> valO -d> iProp Σ).
- Definition stack_link_pre : D → D := λ S ol v2,
+ Definition stack_link_pre (A : lrel Σ) : D → D := λ S ol v2,
match ol return _ with
| None => ⌜v2 = NONEVâŒ
| Some l => ∃ (h : val) (t : option loc) (h' t' : val),
⌜v2 = SOMEV (h', t')âŒ
∗ (∃ q, l ↦{q} (h, oloc_to_val t))
- ∗ lrel_int h h' ∗ ▷ S t t'
+ ∗ A h h' ∗ ▷ S t t'
end%I.
- Global Instance stack_link_pre_contractive : Contractive stack_link_pre.
+ Global Instance stack_link_pre_contractive A : Contractive (stack_link_pre A).
Proof.
intros n S1 S2 HS. solve_proper_prepare.
repeat (first [apply HS | f_contractive | f_equiv]).
Qed.
- Definition stack_link := fixpoint stack_link_pre.
- Lemma stack_link_unfold ol v2 :
- stack_link ol v2 ≡
+ Definition stack_link A := fixpoint (stack_link_pre A).
+
+ Lemma stack_link_unfold A ol v2 :
+ stack_link A ol v2 ≡
(match ol with
| None => ⌜v2 = NONEVâŒ
| Some l => ∃ (h : val) (t : option loc) (h' t' : val),
⌜v2 = SOMEV (h', t')âŒ
∗ (∃ q, l ↦{q} (h, oloc_to_val t))
- ∗ lrel_int h h' ∗ ▷ stack_link t t'
+ ∗ A h h' ∗ ▷ stack_link A t t'
end%I).
- Proof. apply (fixpoint_unfold stack_link_pre). Qed.
+ Proof. apply (fixpoint_unfold (stack_link_pre A)). Qed.
- Lemma stack_link_empty : stack_link None NILV.
+ Lemma stack_link_empty A : stack_link A None NILV.
Proof. rewrite stack_link_unfold; by iPureIntro. Qed.
- Lemma stack_link_cons l h h' t t' q :
- lrel_int h h' -∗
- ▷ stack_link t t' -∗
+ Lemma stack_link_cons A l h h' t t' q :
+ A h h' -∗
+ ▷ stack_link A t t' -∗
l ↦{q} (h, oloc_to_val t) -∗
- stack_link (Some l) (CONSV h' t').
+ stack_link A (Some l) (CONSV h' t').
Proof.
iIntros "Hh Ht Hl".
- rewrite (stack_link_unfold (Some _)).
+ rewrite (stack_link_unfold A (Some _)).
iExists _,_,_,_. iFrame "Hh Ht". iSplit; eauto with iFrame.
Qed.
- (* Fixpoint is_list xs v : iProp Σ := *)
- (* (match xs, v with *)
- (* | [], None => True *)
- (* | x :: xs, Some l => ∃ t q, l ↦{q} (x, oloc_to_val t)%V ∗ is_list xs t *)
- (* | _, _ => False *)
- (* end)%I. *)
-
- (* Lemma is_list_dup xs v : *)
- (* is_list xs v -∗ is_list xs v ∗ match v with *)
- (* | None => True *)
- (* | Some l => ∃ h t q, l ↦{q} (h, oloc_to_val t)%V *)
- (* end. *)
- (* Proof. *)
- (* destruct xs, v; simpl; auto; first by iIntros "[]". *)
- (* iIntros "H"; iDestruct "H" as (t q) "(Hl & Hstack)". *)
- (* iDestruct "Hl" as "[Hl1 Hl2]". *)
- (* iSplitR "Hl2"; first by (iExists _,_; iFrame). by iExists _, _, _. *)
- (* Qed. *)
-
- (* Lemma is_list_empty xs : *)
- (* is_list xs None -∗ ⌜xs = []âŒ. *)
- (* Proof. *)
- (* destruct xs; iIntros "Hstack"; auto. *)
- (* Qed. *)
-
- (* Lemma is_list_cons xs l h t q : *)
- (* l ↦{q} (h, t)%V -∗ *)
- (* is_list xs (Some l) -∗ *)
- (* ∃ ys, ⌜xs = h :: ysâŒ. *)
- (* Proof. *)
- (* destruct xs; first by iIntros "? %". *)
- (* iIntros "Hl Hstack"; iDestruct "Hstack" as (t' q') "(Hl' & Hrest)". *)
- (* iDestruct (gen_heap.mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto. *)
- (* Qed. *)
-
- Definition stackInv oname (st st' mb : loc) (lc : val) : iProp Σ :=
- (∃ ol v2 (N : offerReg), is_locked_r lc false ∗ st ↦ oloc_to_val ol ∗ st' ↦ₛ v2
- ∗ stack_link ol v2
- ∗ (mb ↦ NONEV
- ∨ (∃ (l : loc) (n : Z) γ j K, mb ↦ SOMEV (#n, #l) ∗ ⌜N !! l = Some (#n, γ, j, K)âŒ))
+ (** ** The main invariant *)
+ Definition stackInv A oname (st st' mb : loc) (lc : val) : iProp Σ :=
+ (∃ ol v2 (N : offerReg),
+ is_locked_r lc false
+ ∗ st ↦ oloc_to_val ol
+ ∗ st' ↦ₛ v2
+ ∗ stack_link A ol v2
+ ∗ (mb ↦ NONEV (* the mailbox is either empty or contains an offer that is in the registry *)
+ ∨ (∃ (l : loc) v1 v2 γ j K, A v1 v2
+ ∗ mb ↦ SOMEV (v1, #l)
+ ∗ ⌜N !! l = Some (v2, γ, j, K)âŒ))
∗ own oname (◠to_offer_reg N)
∗ offerInv N (#st', lc))%I.
+
+ (** ** The proof itself *)
+ (* Helper instances *)
Local Instance ro_pointsto_fromand (l : loc) (w : val) :
FromSep (∃ q, l ↦{q} w) (∃ q, l ↦{q} w) (∃ q, l ↦{q} w).
Proof.
@@ -343,12 +294,12 @@ Section refinement.
iSplitL "H1"; eauto with iFrame.
Qed.
- Lemma pop_no_helping_refinement γo st st' mb lk :
- inv stackN (stackInv γo st st' mb lk) -∗
+ Lemma pop_no_helping_refinement A γo st st' mb lk :
+ inv stackN (stackInv A γo st st' mb lk) -∗
□ (REL (pop_st #st) (λ: <>, get_mail #mb)%V
<<
- CG_locked_pop (#st', lk)%V : () + lrel_int) -∗
- REL match: rec_unfold ! #st with
+ CG_locked_pop (#st', lk)%V : () + A) -∗
+ REL match: ! #st with
InjL <> => InjL #()
| InjR "l" =>
let: "pair" := ! "l" in
@@ -357,17 +308,17 @@ Section refinement.
else (pop_st #st) (λ: <>, get_mail #mb)%V
end
<<
- CG_locked_pop (#st', lk)%V : () + lrel_int.
+ CG_locked_pop (#st', lk)%V : () + A.
Proof.
iIntros "#Hinv IH".
rel_load_l_atomic.
- iInv stackN as (s1 s2 N) "(Hlk & Hst1 & Hst2 & Hrel & >Hmb & HNown & HN)" "Hcl".
+ iInv stackN as (s1 s2 N) "(Hlk & Hst1 & Hst2 & Hrel & Hmb & HNown & HN)" "Hcl".
iModIntro. iExists _; iFrame. iNext. iIntros "Hst1".
rewrite stack_link_unfold.
destruct s1 as [l|]; last first.
- (* Stack is empty *)
iDestruct "Hrel" as "->". iSimpl.
- rel_rec_l. rel_pures_l.
+ rel_pures_l.
rel_apply_r (refines_CG_pop_fail_r with "Hst2 Hlk").
iIntros "Hst' Hlk".
iMod ("Hcl" with "[-]") as "_".
@@ -376,7 +327,7 @@ Section refinement.
rel_values. iModIntro. iExists #(),#().
iLeft; repeat iSplit; eauto with iFrame.
- iDestruct "Hrel" as (h t h' t' ->) "(Hl & #Hh & Ht)". iSimpl.
- rel_rec_l. rel_pures_l.
+ rel_pures_l.
iDestruct "Hl" as "[Hl Hl2]".
iMod ("Hcl" with "[-IH Hl]") as "_".
{ iNext. iExists _,_,_. iFrame.
@@ -385,7 +336,7 @@ Section refinement.
iDestruct "Hl" as (q) "Hl".
rel_load_l. rel_pures_l.
rel_cmpxchg_l_atomic.
- iInv stackN as (s1 s2 N') "(Hlk & Hst1 & Hst2 & Hrel & >Hmb & HNown & HN)" "Hcl".
+ iInv stackN as (s1 s2 N') "(Hlk & Hst1 & Hst2 & Hrel & Hmb & HNown & HN)" "Hcl".
iModIntro. iExists _; iFrame "Hst1". iSplit.
+ (* Going to retry *)
iIntros (Hs1). iNext. iIntros "Hst1".
@@ -411,28 +362,134 @@ Section refinement.
iRight. repeat iSplit; eauto with iFrame.
Qed.
- Lemma push_refinement γo st st' mb lk h1 h2 :
- inv stackN (stackInv γo st st' mb lk) -∗
- lrel_int h1 h2 -∗
+ Lemma pop_refinement A γo st st' mb lk :
+ inv stackN (stackInv A γo st st' mb lk) -∗
+ REL (pop_st #st) (λ: <>, get_mail #mb)%V
+ <<
+ CG_locked_pop (#st', lk)%V : () + A.
+ Proof.
+ iIntros "#Hinv".
+ iLöb as "IH".
+ rel_rec_l. rel_pures_l.
+ rel_rec_l.
+ rel_load_l_atomic.
+ iInv stackN as (s1 s2 N) "(>Hl & >Hst1 & >Hst2 & Hrel & Hmb & HNown & HN)" "Hcl"; simplify_eq.
+ iDestruct "Hmb" as "[Hmb | Hmb]".
+ - (* NO OFFER *)
+ iModIntro. iExists _; iFrame.
+ iNext. iIntros "Hmb".
+ rel_pures_l.
+ iMod ("Hcl" with "[-]") as "_".
+ { iNext. iExists _, _, _; iFrame. }
+ iApply (pop_no_helping_refinement with "Hinv IH").
+ - (* YES OFFER *)
+ iDestruct "Hmb" as (l v1 v2 γ j K) "(#Hv & Hmb & >HNl)".
+ iDestruct "HNl" as %HNl.
+ rewrite /offerInv big_sepM_lookup_acc; eauto.
+ iDestruct "HN" as "[HNl HN]".
+ simpl. iMod "HNown".
+ iMod (offerReg_lookup_frag with "HNown") as "[#Hlown HNown]"; eauto.
+ iModIntro. iExists _; iFrame.
+ iNext. iIntros "Hmb".
+ iMod ("Hcl" with "[-Hlown IH]") as "_".
+ { iNext. iExists _, _, _; iFrame.
+ iSplitL "Hmb".
+ - iRight. iExists _, _, _, _, _, _.
+ eauto with iFrame.
+ - by iApply "HN". }
+ rel_pures_l. rel_rec_l. rel_pures_l.
+ (* Trying to take upon the offer *)
+ rel_cmpxchg_l_atomic.
+ iInv stackN as (s1' s2' N') "(>Hl & >Hst1 & >Hst2 & Hrel & Hmb & HNown & HN)" "Hcl"; simplify_eq.
+ iMod "HNown".
+ iDestruct (offerReg_frag_lookup with "HNown Hlown") as %?.
+ rewrite /offerInv (big_sepM_lookup_acc _ _ l); eauto.
+ iDestruct "HN" as "[HNl HN]".
+ iDestruct "HNl" as (c) "[>HNl Hc]".
+ iModIntro. iExists _; iFrame.
+ iSplit; last first.
+ + (* CAS suc *)
+ iIntros (Hc); simplify_eq/=. iNext.
+ assert (c = 0%nat) as -> by lia. (* :) *)
+ iIntros "HNl".
+ rel_pures_l.
+ iDestruct "Hc" as "[[% Hj] | [[% ?] | [% ?]]]"; [| congruence..].
+ unlock {1}CG_locked_push.
+ unlock {1}acquire {1}release.
+ (* THIS IS COPY PASTED :-) *)
+ tp_pure j (App _ (_,_)%V). iSimpl in "Hj".
+ tp_pure j (Rec _ _ _). iSimpl in "Hj".
+ repeat (tp_pure j _; iSimpl in "Hj").
+ tp_pure j (Snd _). iSimpl in "Hj".
+ unlock acquire. tp_pure j (App _ lk). iSimpl in "Hj".
+ unlock is_locked_r. iDestruct "Hl" as (lk' ->) "Hl".
+ (* TODO: make all the tp_ tactics work without the need for an explicit Fupd *)
+ iApply refines_spec_ctx.
+ iDestruct 1 as (Ï) "#HÏ".
+ iApply fupd_refines.
+ (* because we manually applied `fupd_refines`, the tactical `with_spec_ctx` doesn't work anymore *)
+ tp_cmpxchg_suc j. iSimpl in "Hj".
+ tp_pure j (Snd _). iSimpl in "Hj".
+ tp_if j. iSimpl in "Hj".
+ tp_pure j (Rec _ _ _). iSimpl in "Hj".
+ tp_rec j. iSimpl in "Hj".
+
+ unlock CG_push.
+ tp_pure j (Fst _). iSimpl in "Hj".
+ tp_pure j (App _ #st'). iSimpl in "Hj".
+ tp_pure j (Rec _ _ _). iSimpl in "Hj".
+ tp_pure j (App _ v2). iSimpl in "Hj".
+ tp_load j. iSimpl in "Hj".
+ tp_pure j (Pair _ _).
+ tp_pure j (InjR _).
+ tp_store j. iSimpl in "Hj".
+ tp_pure j (Rec _ _ _).
+ tp_rec j. iSimpl in "Hj".
+ tp_pure j (Snd _). unlock release.
+ tp_rec j. tp_store j.
+ iClear "HÏ". clear Ï. iModIntro.
+
+ rel_apply_r (refines_CG_pop_suc_r with "Hst2 [Hl]").
+ { iExists _. by iFrame "Hl". }
+ iIntros "Hst2 Hl".
+ iMod ("Hcl" with "[-]") as "_".
+ { iNext. iExists _,_,_. iFrame.
+ iApply "HN".
+ iExists 1%nat. iFrame "HNl".
+ iRight. iLeft. eauto with iFrame. }
+ rel_values. iModIntro. iExists v1,v2.
+ iRight. repeat iSplit; eauto with iFrame.
+ + (* CAS FAILS *)
+ iIntros (Hc). iNext.
+ iIntros "HNl".
+ iMod ("Hcl" with "[-IH]") as "_".
+ { iNext. iExists _,_,_. iFrame.
+ iApply "HN". iExists _. iFrame. }
+ rel_pures_l.
+ iApply (pop_no_helping_refinement with "Hinv IH").
+ Qed.
+
+ Lemma push_refinement A γo st st' mb lk h1 h2 :
+ inv stackN (stackInv A γo st st' mb lk) -∗
+ A h1 h2 -∗
REL ((push_st #st) (λ: "n", (put_mail #mb) "n")%V) h1
<<
(CG_locked_push (#st', lk)%V) h2 : ().
Proof.
- iIntros "#Hinv Hh".
- iDestruct "Hh" as (n) "[% %]"; simplify_eq/=.
+ iIntros "#Hinv #Hh".
iLöb as "IH".
rel_rec_l.
rel_pures_l.
rel_rec_l. rel_pures_l. rel_rec_l.
rel_alloc_l o as "Ho". rel_pures_l.
rel_store_l_atomic.
- iInv stackN as (s1 s2 N) "(Hl & Hst1 & Hst2 & Hrel & >Hmb & HNown & HN)" "Hcl".
+ iInv stackN as (s1 s2 N) "(Hl & Hst1 & Hst2 & Hrel & Hmb & HNown & HN)" "Hcl".
iModIntro.
iAssert (∃ v, ▷ mb ↦ v)%I with "[Hmb]" as (v) "Hmb".
{ iDestruct "Hmb" as "[Hmb | Hmb]".
- iExists (InjLV #()); eauto.
- - iDestruct "Hmb" as (l m γ j K) "[Hmb ?]".
- iExists (InjRV (#m, #l)); eauto. }
+ - iDestruct "Hmb" as (l m1 m2 γ j K) "(Hm & Hmb & ?)".
+ iExists (InjRV (m1, #l)); eauto. }
iExists _; iFrame; iNext.
iIntros "Hmb".
rel_pures_l.
@@ -442,11 +499,11 @@ Section refinement.
rewrite {2}refines_eq /refines_def.
iIntros (Ï) "#Hs".
iIntros (j K) "Hj".
- iMod (offerReg_alloc o #n γ j K with "HNown") as "[HNown Hfrag]"; eauto.
+ iMod (offerReg_alloc o h2 γ j K with "HNown") as "[HNown Hfrag]"; eauto.
iMod ("Hcl" with "[-Hfrag Hγ]") as "_".
{ iNext. iExists _,_,_; iFrame.
iSplitL "Hmb".
- - iRight. iExists o, n, _, _, _. iFrame "Hmb".
+ - iRight. iExists o, h1, h2, _, _, _. iFrame "Hmb Hh".
iPureIntro. by rewrite lookup_insert.
- rewrite /offerInv big_sepM_insert; eauto.
iFrame.
@@ -454,7 +511,7 @@ Section refinement.
iLeft. unlock CG_locked_push. iFrame "Hj". eauto. }
iModIntro. wp_proj.
wp_bind (CmpXchg _ _ _).
- iInv stackN as (s1' s2' N') "(Hl & Hst1 & Hst2 & Hrel & >Hmb & >HNown & HN)" "Hcl".
+ iInv stackN as (s1' s2' N') "(Hl & Hst1 & Hst2 & Hrel & Hmb & >HNown & HN)" "Hcl".
iDestruct (offerReg_frag_lookup with "HNown Hfrag") as %Hfoo.
rewrite /offerInv.
rewrite (big_sepM_lookup_acc _ N'); eauto.
@@ -497,7 +554,7 @@ Section refinement.
tp_pure j (Fst _). iSimpl in "Hj".
tp_pure j (App _ #st'). iSimpl in "Hj".
tp_pure j (Rec _ _ _). iSimpl in "Hj".
- tp_pure j (App _ #n). iSimpl in "Hj".
+ tp_pure j (App _ h2). iSimpl in "Hj".
tp_load j. iSimpl in "Hj".
tp_pure j (Pair _ _).
tp_pure j (InjR _).
@@ -506,9 +563,8 @@ Section refinement.
tp_rec j. iSimpl in "Hj".
tp_pure j (Snd _). unlock release.
tp_rec j. tp_store j.
- iDestruct (stack_link_cons hd #n #n
- with "[] Hrel Hhd") as "Hrel".
- { iExists n. eauto with iFrame. }
+ iDestruct (stack_link_cons _ hd h1 h2
+ with "Hh Hrel Hhd") as "Hrel".
iMod ("Hcl" with "[-Hj]").
{ iNext. iExists _,_,_; subst; iFrame.
iExists _; by iFrame "Hl". }
@@ -542,9 +598,9 @@ Section refinement.
iExists #(); eauto.
Qed.
- Lemma refinement :
+ Lemma refinement A :
REL mk_stack #() << CG_mkstack #() :
- (() → () + lrel_int) * (lrel_int → ()).
+ (() → () + A) * (A → ()).
Proof.
rel_rec_r. rel_pures_r. rel_rec_r.
rel_apply_r refines_newlock_r. iIntros (lk) "Hlk".
@@ -557,7 +613,7 @@ Section refinement.
rel_alloc_l st as "Hst". rel_pure_l. rel_pure_l. rel_pure_l. rel_pure_l.
iMod (own_alloc (◠to_offer_reg ∅ : authR offerRegR)) as (γo) "Hor".
{ apply auth_auth_valid. apply to_offer_reg_valid. }
- iMod (inv_alloc stackN _ (stackInv γo st st' mb lk) with "[-]") as "#Hinv".
+ iMod (inv_alloc stackN _ (stackInv _ γo st st' mb lk) with "[-]") as "#Hinv".
{ iNext. unfold stackInv.
iExists None, _, _. iFrame.
iSplit; eauto.
@@ -571,105 +627,7 @@ Section refinement.
(* * Pop refinement *)
{ rel_arrow_val. iIntros (? ?) "[% %]"; simplify_eq/=.
rel_pures_l. rel_pures_r.
- iLöb as "IH".
- rel_rec_l. rel_pures_l.
- rel_rec_l.
- rel_load_l_atomic.
- iInv stackN as (s1 s2 N) "(>Hl & >Hst1 & >Hst2 & Hrel & Hmb & HNown & HN)" "Hcl"; simplify_eq.
- iDestruct "Hmb" as "[Hmb | Hmb]".
- - (* NO OFFER *)
- iModIntro. iExists _; iFrame.
- iNext. iIntros "Hmb".
- rel_pures_l.
- iMod ("Hcl" with "[-]") as "_".
- { iNext. iExists _, _, _; iFrame. }
- iApply (pop_no_helping_refinement with "Hinv IH").
- - (* YES OFFER *)
- iDestruct "Hmb" as (l v γ j K) "[Hmb >HNl]".
- iDestruct "HNl" as %HNl.
- rewrite /offerInv big_sepM_lookup_acc; eauto.
- iDestruct "HN" as "[HNl HN]".
- simpl. iMod "HNown".
- iMod (offerReg_lookup_frag with "HNown") as "[#Hlown HNown]"; eauto.
- iModIntro. iExists _; iFrame.
- iNext. iIntros "Hmb".
- iMod ("Hcl" with "[-Hlown IH]") as "_".
- { iNext. iExists _, _, _; iFrame.
- iSplitL "Hmb".
- iRight. iExists _, _. iFrame.
- iPureIntro. do 3 eexists; eauto.
- by iApply "HN". }
- rel_pures_l. rel_rec_l. rel_pures_l.
- (* Trying to take upon the offer *)
- rel_cmpxchg_l_atomic.
- iInv stackN as (s1' s2' N') "(>Hl & >Hst1 & >Hst2 & Hrel & Hmb & HNown & HN)" "Hcl"; simplify_eq.
- iMod "HNown".
- iDestruct (offerReg_frag_lookup with "HNown Hlown") as %?.
- rewrite /offerInv (big_sepM_lookup_acc _ _ l); eauto.
- iDestruct "HN" as "[HNl HN]".
- iDestruct "HNl" as (c) "[>HNl Hc]".
- iModIntro. iExists _; iFrame.
- iSplit; last first.
- + (* CAS suc *)
- iIntros (Hc); simplify_eq/=. iNext.
- assert (c = 0%nat) as -> by lia. (* :) *)
- iIntros "HNl".
- rel_pures_l.
- iDestruct "Hc" as "[[% Hj] | [[% ?] | [% ?]]]"; [| congruence..].
- unlock {1}CG_locked_push.
- unlock {1}acquire {1}release.
- (* THIS IS COPY PASTED :-) *)
- tp_pure j (App _ (_,_)%V). iSimpl in "Hj".
- tp_pure j (Rec _ _ _). iSimpl in "Hj".
- repeat (tp_pure j _; iSimpl in "Hj").
- tp_pure j (Snd _). iSimpl in "Hj".
- unlock acquire. tp_pure j (App _ lk). iSimpl in "Hj".
- unlock is_locked_r. iDestruct "Hl" as (lk' ->) "Hl".
- (* TODO: make all the tp_ tactics work without the need for an explicit Fupd *)
- iApply refines_spec_ctx.
- iDestruct 1 as (Ï) "#HÏ".
- iApply fupd_refines.
- (* because we manually applied `fupd_refines`, the tactical `with_spec_ctx` doesn't work anymore *)
- tp_cmpxchg_suc j. iSimpl in "Hj".
- tp_pure j (Snd _). iSimpl in "Hj".
- tp_if j. iSimpl in "Hj".
- tp_pure j (Rec _ _ _). iSimpl in "Hj".
- tp_rec j. iSimpl in "Hj".
-
- unlock CG_push.
- tp_pure j (Fst _). iSimpl in "Hj".
- tp_pure j (App _ #st'). iSimpl in "Hj".
- tp_pure j (Rec _ _ _). iSimpl in "Hj".
- tp_pure j (App _ #v). iSimpl in "Hj".
- tp_load j. iSimpl in "Hj".
- tp_pure j (Pair _ _).
- tp_pure j (InjR _).
- tp_store j. iSimpl in "Hj".
- tp_pure j (Rec _ _ _).
- tp_rec j. iSimpl in "Hj".
- tp_pure j (Snd _). unlock release.
- tp_rec j. tp_store j.
- iClear "HÏ". clear Ï. iModIntro.
-
- rel_apply_r (refines_CG_pop_suc_r with "Hst2 [Hl]").
- { iExists _. by iFrame "Hl". }
- iIntros "Hst2 Hl".
- iMod ("Hcl" with "[-]") as "_".
- { iNext. iExists _,_,_. iFrame.
- iApply "HN".
- iExists 1%nat. iFrame "HNl".
- iRight. iLeft. eauto with iFrame. }
- rel_values. iModIntro. iExists #v,#v.
- iRight. repeat iSplit; eauto with iFrame.
- + (* CAS FAILS *)
- iIntros (Hc). iNext.
- iIntros "HNl".
- iMod ("Hcl" with "[-IH]") as "_".
- { iNext. iExists _,_,_. iFrame.
- iApply "HN". iExists _. iFrame. }
- rel_pures_l.
- iApply (pop_no_helping_refinement with "Hinv IH"). }
+ iApply (pop_refinement with "Hinv"). }
Qed.
-
End refinement.
--
GitLab