diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 097275062583d9aeeaebb1d6e0698d25ff9aba5e..be7d944a05055c28ce94f77ad80de5b091b07453 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -22,7 +22,11 @@ Definition clone_weak : val :=
Definition downgrade : val :=
rec: "downgrade" ["l"] :=
let: "weak" := !ˢᶜ("l" +ₗ #1) in
- if: CAS ("l" +ₗ #1) "weak" ("weak" + #1) then #() else "downgrade" ["l"].
+ if: "weak" = #(-1) then
+ "downgrade" ["l"]
+ else
+ if: CAS ("l" +ₗ #1) "weak" ("weak" + #1) then #()
+ else "downgrade" ["l"].
Definition upgrade : val :=
rec: "upgrade" ["l"] :=
@@ -59,10 +63,25 @@ Definition try_unwrap_full : val :=
else "l" <- #1;; #1
else #2.
+Definition is_unique : val :=
+ λ: ["l"],
+ if: CAS ("l" +ₗ #1) #1 #(-1) then
+ let: "strong" := !ˢᶜ"l" in
+ let: "unique" := "strong" = #1 in
+ "l" +ₗ #1 <-ˢᶜ #1;;
+ "unique"
+ else
+ #false.
+
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
+
+(* See rc.v for understanding the structure of this CMRA.
+ The only additional thing is the [optionR (exclR unitC))], used to handle
+ properly the locking mechanisme for the weak count. *)
Definition arc_stR :=
- prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitC))) natUR.
+ prodUR (optionUR (csumR (prodR (prodR fracR positiveR) (optionR (exclR unitC)))
+ (exclR unitC))) natUR.
Class arcG Σ :=
RcG :> inG Σ (authR arc_stR).
Definition arcΣ : gFunctors := #[GFunctor (authR arc_stR)].
@@ -73,7 +92,7 @@ Section def.
Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) (P2 : iProp Σ) (N : namespace).
Definition arc_tok γ q : iProp Σ :=
- own γ (◯ (Some $ Cinl (q, 1%positive), 0%nat)).
+ own γ (◯ (Some $ Cinl (q, 1%positive, None), 0%nat)).
Definition weak_tok γ : iProp Σ :=
own γ (◯ (None, 1%nat)).
@@ -83,9 +102,10 @@ Section def.
Definition arc_inv (γ : gname) (l : loc) : iProp Σ :=
(∃ st : arc_stR, own γ (● st) ∗
match st with
- | (Some (Cinl (q, strong)), weak) => ∃ q',
- l ↦ #(Zpos strong) ∗ shift_loc l 1 ↦ #(S weak) ∗
- ⌜(q + q')%Qp = 1%Qp⌝ ∗ P1 q'
+ | (Some (Cinl (q, strong, wlock)), weak) =>
+ ∃ q', ⌜(q + q')%Qp = 1%Qp⌝ ∗ P1 q' ∗ l ↦ #(Zpos strong) ∗
+ if wlock then shift_loc l 1 ↦ #(-1) ∗ ⌜weak = 0%nat⌝
+ else shift_loc l 1 ↦ #(S weak)
| (Some (Cinr _), weak) =>
l ↦ #0 ∗ shift_loc l 1 ↦ #(S weak)
| (None, (S _) as weak) =>
@@ -141,8 +161,9 @@ Section arc.
∃ γ q, is_arc P1 P2 N γ l ∗ P1 q ∗ arc_tok γ q.
Proof using HP1.
iIntros "Hl1 Hl2 [HP1 HP1']".
- iMod (own_alloc ((● (Some $ Cinl ((1/2)%Qp, xH), O) ⋅
- ◯ (Some $ Cinl ((1/2)%Qp, xH), O)))) as (γ) "[H● H◯]"; first done.
+ iMod (own_alloc ((● (Some $ Cinl ((1/2)%Qp, xH, None), O) ⋅
+ ◯ (Some $ Cinl ((1/2)%Qp, xH, None), O))))
+ as (γ) "[H● H◯]"; first done.
iExists _, _. iFrame. iApply inv_alloc. iExists _. iFrame. iExists _. iFrame.
rewrite Qp_div_2. auto.
Qed.
@@ -157,19 +178,18 @@ Section arc.
Lemma arc_tok_auth_val st γ q :
own γ (● st) -∗ arc_tok γ q -∗
- ⌜∃ q' strong weak, st = (Some $ Cinl (q', strong), weak) ∧
- if decide (strong = xH) then q = q'
- else ∃ q'', q' = (q + q'')%Qp⌝.
+ ⌜∃ q' strong wlock weak, st = (Some $ Cinl (q', strong, wlock), weak) ∧
+ if decide (strong = xH) then q = q' ∧ wlock = None
+ else ∃ q'', q' = (q + q'')%Qp⌝.
Proof.
iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
%[[Hincl%option_included _]%prod_included [Hval _]]%auth_valid_discrete_2.
destruct st, Hincl as [[=]|(?&?&[= <-]&?&[Hincl|Hincl%csum_included])];
simpl in *; subst.
- - setoid_subst. iExists _, _, _. by iSplit.
- - destruct Hincl as [->|[(?&[]&[=<-]&->&
- [[??]%frac_included%Qp_lt_sum ?%pos_included]%prod_included)|
- (?&?&[=]&?)]]; first done.
- iExists _, _, _. iSplit=>//. simpl in *. destruct decide; [subst;lia|eauto].
+ - setoid_subst. iExists _, _, _, _. by iSplit.
+ - destruct Hincl as [->|[(?&[[??]?]&[=<-]&->&[[[??]%frac_included%Qp_lt_sum
+ ?%pos_included]%prod_included _]%prod_included)|(?&?&[=]&?)]]; first done.
+ iExists _, _, _, _. iSplit=>//. simpl in *. destruct decide; [subst;lia|eauto].
Qed.
Lemma clone_arc_spec (γ : gname) (l : loc) (P : iProp Σ) :
@@ -180,30 +200,31 @@ Section arc.
iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
- iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &?&[-> _]).
- iDestruct "H" as (?) "[H H']". wp_read. iMod ("Hclose2" with "Hown") as "HP".
- iModIntro. iMod ("Hclose1" with "[H H' H●]") as "_".
- { iExists _. auto with iFrame. }
+ iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &?&?&[-> _]).
+ iDestruct "H" as (?) "(Hq & HP1 & H↦ & Hw)". wp_read.
+ iMod ("Hclose2" with "Hown") as "HP". iModIntro.
+ iMod ("Hclose1" with "[-HP HΦ]") as "_"; [iExists _; auto with iFrame|].
iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
- iDestruct (arc_tok_auth_val with "H● Hown") as %(?&strong'&?&[-> _]).
- iDestruct "H" as (q) "(Hl & Hl1 & >Heq & [HP1 HP1'])". iDestruct "Heq" as %Heq.
+ iDestruct (arc_tok_auth_val with "H● Hown") as %(?&strong'&?&?&[-> _]).
+ iDestruct "H" as (q) "(>#Hq & [HP1 HP1'] & Hl & Hw)". iDestruct "Hq" as %Hq.
destruct (decide (strong = strong')) as [->|?].
- wp_apply (wp_cas_int_suc with "Hl"); first done. iIntros "Hl".
iMod (own_update with "H●") as "[H● Hown']".
{ apply auth_update_alloc, prod_local_update_1,
- (op_local_update_discrete _ _ (Some (Cinl ((q/2)%Qp, 1%positive))))=>-[/= Hqa _].
- split; simpl; last done. apply frac_valid'. rewrite -Heq comm_L -{2}(Qp_div_2 q).
+ (op_local_update_discrete _ _ (Some (Cinl ((q/2)%Qp, 1%positive, None))))
+ =>-[/= Hqa ?]. split;[split|]=>//=; last by rewrite left_id.
+ apply frac_valid'. rewrite -Hq comm_L -{2}(Qp_div_2 q).
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0. }
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
- iMod ("Hclose1" with "[Hl Hl1 H● HP1']") as "_".
+ iMod ("Hclose1" with "[Hl Hw H● HP1']") as "_".
{ iExists _. iFrame. iExists _. rewrite /= [xH ⋅ _]comm_L. iFrame.
- rewrite [(q / 2)%Qp ⋅ _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2. auto. }
+ rewrite [(q / 2)%Qp ⋅ _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
iModIntro. wp_apply (wp_if _ true). wp_value. iApply "HΦ". iFrame.
- wp_apply (wp_cas_int_fail with "Hl"); [done|congruence|]. iIntros "Hl".
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
- iMod ("Hclose1" with "[Hl Hl1 HP1 HP1' H●]") as "_".
+ iMod ("Hclose1" with "[-HP HΦ]") as "_".
{ iExists _. iFrame. iExists q. auto with iFrame. }
iModIntro. wp_apply (wp_if _ false). iApply ("IH" with "HP HΦ").
Qed.
@@ -214,32 +235,40 @@ Section arc.
Proof.
iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
iInv N as (st) "[>H● H]" "Hclose1".
- iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
- iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& weak &[-> _]).
- iDestruct "H" as (?) "(H & H' & H'')". wp_read. iMod ("Hclose2" with "Hown") as "HP".
- iModIntro. iMod ("Hclose1" with "[H H' H'' H●]") as "_".
- { iExists _. auto with iFrame. }
- iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). wp_op.
+ iApply fupd_wp. iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
+ iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& wlock & weak &[-> _]).
+ iMod ("Hclose2" with "Hown") as "HP". iModIntro.
+ iDestruct "H" as (?) "(? & ? & ? & Hw)". destruct wlock.
+ { iDestruct "Hw" as "(Hw & >%)". subst. wp_read.
+ iMod ("Hclose1" with "[-HP HΦ]") as "_"; first by iExists _; auto with iFrame.
+ iModIntro. wp_let. wp_op=>[_|//]. wp_if. iApply ("IH" with "HP HΦ"). }
+ wp_read. iMod ("Hclose1" with "[-HP HΦ]") as "_"; first by iExists _; auto with iFrame.
+ iModIntro. wp_let. wp_op=>[//|_]. wp_if. wp_op. wp_op. wp_bind (CAS _ _ _).
iInv N as (st) "[>H● H]" "Hclose1".
- iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
- iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& weak' &[-> _]).
- iDestruct "H" as (q) "(Hl & Hl1 & >Heq & HP1)". iDestruct "Heq" as %Heq.
- destruct (decide (weak = weak')) as [<-|Hw].
+ iApply fupd_wp. iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
+ iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& wlock & weak' &[-> _]).
+ iMod ("Hclose2" with "Hown") as "HP". iModIntro.
+ iDestruct "H" as (q) "(>Heq & HP1 & Hl & Hl1)". iDestruct "Heq" as %Heq.
+ destruct (decide (weak = weak' ∧ wlock = None)) as [[<- ->]|Hw].
- wp_apply (wp_cas_int_suc with "Hl1"); first done. iIntros "Hl1".
iMod (own_update with "H●") as "[H● Hown']".
{ by apply auth_update_alloc, prod_local_update_2,
(op_local_update_discrete _ _ (1%nat)). }
- iMod ("Hclose2" with "Hown") as "HP". iModIntro.
- iMod ("Hclose1" with "[Hl Hl1 H● HP1]") as "_".
+ iMod ("Hclose1" with "[-Hown' HP HΦ]") as "_".
{ iExists _. iFrame. iExists _.
rewrite Z.add_comm (Nat2Z.inj_add 1). auto with iFrame. }
iModIntro. wp_apply (wp_if _ true). wp_value. iApply "HΦ". iFrame.
- - wp_apply (wp_cas_int_fail with "Hl1"); [done| |].
- { contradict Hw. apply SuccNat2Pos.inj. lia. }
- iMod ("Hclose2" with "Hown") as "HP". iIntros "Hl1 !>".
- iMod ("Hclose1" with "[Hl Hl1 HP1 H●]") as "_".
- { iExists _. auto with iFrame. }
- iModIntro. wp_apply (wp_if _ false). iApply ("IH" with "HP HΦ").
+ - destruct wlock.
+ + iDestruct "Hl1" as "[Hl1 >%]". subst.
+ wp_apply (wp_cas_int_fail with "Hl1"); [done..|].
+ iIntros "Hl1". iMod ("Hclose1" with "[-HP HΦ]") as "_".
+ { iExists _. auto with iFrame. }
+ iModIntro. wp_apply (wp_if _ false). iApply ("IH" with "HP HΦ").
+ + wp_apply (wp_cas_int_fail with "Hl1"); [done| |].
+ { contradict Hw. split=>//. apply SuccNat2Pos.inj. lia. }
+ iIntros "Hl1". iMod ("Hclose1" with "[-HP HΦ]") as "_".
+ { iExists _. auto with iFrame. }
+ iModIntro. wp_apply (wp_if _ false). iApply ("IH" with "HP HΦ").
Qed.
Lemma weak_tok_auth_val γ st :
@@ -256,31 +285,30 @@ Section arc.
{{{ P }}} clone_weak [ #l] {{{ RET #(); P ∗ weak_tok γ }}}.
Proof.
iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
- iAssert (□ (P ={⊤,∅}=∗ ∃ w : Z, shift_loc l 1 ↦ #w ∗
- (shift_loc l 1 ↦ #(w + 1) ={∅,⊤}=∗ P ∗ weak_tok γ) ∧
- (shift_loc l 1 ↦ #w ={∅,⊤}=∗ P)))%I as "#Hproto".
+ iAssert (□ (P ={⊤,⊤∖↑N}=∗ ∃ w : Z, shift_loc l 1 ↦ #w ∗
+ (shift_loc l 1 ↦ #(w + 1) ={⊤∖↑N,⊤}=∗ P ∗ weak_tok γ) ∧
+ (shift_loc l 1 ↦ #w ={⊤∖↑N,⊤}=∗ P)))%I as "#Hproto".
{ iIntros "!# HP". iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as "[Hown Hclose2]".
iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
- destruct st' as [[[]| |]|]; try done; iExists _.
- - iDestruct "H" as (?) "(? & >$ & ?)". iIntros "!>"; iSplit; iIntros "?";
- iMod ("Hclose2" with "Hown") as "HP".
+ iMod ("Hclose2" with "Hown") as "HP".
+ destruct st' as [[[[??][?|]]| |]|]; try done; [|iExists _..].
+ - by iDestruct "H" as (?) "(_ & _ & _ & _ & >%)".
+ - iDestruct "H" as (?) "(? & ? & ? & >$)". iIntros "!>"; iSplit; iIntros "?".
+ iMod (own_update with "H●") as "[H● $]".
{ by apply auth_update_alloc, prod_local_update_2,
(op_local_update_discrete _ _ (1%nat)). }
rewrite Z.add_comm -(Nat2Z.inj_add 1). iFrame.
iApply "Hclose1". iExists _. auto with iFrame.
+ iFrame. iApply ("Hclose1" with "[-]"). iExists _. auto with iFrame.
- - iDestruct "H" as "[? >$]". iIntros "!>"; iSplit; iIntros "?";
- iMod ("Hclose2" with "Hown") as "HP".
+ - iDestruct "H" as "[? >$]". iIntros "!>"; iSplit; iIntros "?".
+ iMod (own_update with "H●") as "[H● $]".
{ by apply auth_update_alloc, prod_local_update_2,
(op_local_update_discrete _ _ (1%nat)). }
rewrite Z.add_comm -(Nat2Z.inj_add 1). iFrame. iApply "Hclose1".
iExists _. auto with iFrame.
+ iFrame. iApply ("Hclose1" with "[-]"). iExists _. auto with iFrame.
- - iDestruct "H" as "(? & >$ & ?)". iIntros "!>"; iSplit; iIntros "?";
- iMod ("Hclose2" with "Hown") as "HP".
+ - iDestruct "H" as "(? & >$ & ?)". iIntros "!>"; iSplit; iIntros "?".
+ iMod (own_update with "H●") as "[H● $]".
{ by apply auth_update_alloc, prod_local_update_2,
(op_local_update_discrete _ _ (1%nat)). }
@@ -311,18 +339,19 @@ Section arc.
{ iIntros "!# HP". iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as "[Hown Hclose2]".
iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
- destruct st' as [[[]| |]|]; try done; iExists _.
- - iDestruct "H" as (q) "(>$ & ? & >Heq & [HP1 HP1'])". iDestruct "Heq" as %Heq.
+ destruct st' as [[[[??]?]| |]|]; try done; iExists _.
+ - iDestruct "H" as (q) "(>Heq & [HP1 HP1'] & >$ & ?)". iDestruct "Heq" as %Heq.
iIntros "!>"; iSplit; iMod ("Hclose2" with "Hown") as "HP".
+ iIntros "_ Hl". iExists (q/2)%Qp. iMod (own_update with "H●") as "[H● $]".
{ apply auth_update_alloc. rewrite -[(_,0%nat)]right_id.
- apply op_local_update_discrete. constructor; last done. split; last done.
+ apply op_local_update_discrete=>Hv. constructor; last done.
+ split; last by rewrite /= left_id; apply Hv. split=>[|//].
apply frac_valid'. rewrite -Heq comm_L -{2}(Qp_div_2 q).
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0. }
iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame.
rewrite /= [xH ⋅ _]comm_L frac_op' [(_ + c)%Qp]comm -[(_ + _)%Qp]assoc
- Qp_div_2. auto with iFrame.
+ Qp_div_2 left_id_L. auto with iFrame.
+ iIntros "Hl". iFrame. iApply ("Hclose1" with "[-]"). iExists _. iFrame.
iExists q. auto with iFrame.
- iDestruct "H" as "[>$ ?]". iIntros "!>"; iSplit; first by auto with congruence.
@@ -357,8 +386,9 @@ Section arc.
(shift_loc l 1 ↦ #w ={⊤ ∖ ↑N,⊤}=∗ weak_tok γ)))%I as "#Hproto".
{ iIntros "!# Hown". iInv N as (st) "[>H● H]" "Hclose1".
iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
- destruct st' as [[[]| |]|]; try done; iExists _.
- - iDestruct "H" as (q) "(? & >$ & >Heq & HP1)". iIntros "!>"; iSplit; iIntros "Hl1".
+ destruct st' as [[[[??][?|]]| |]|]; try done; [|iExists _..].
+ - by iDestruct "H" as (?) "(_ & _ & _ & _ & >%)".
+ - iDestruct "H" as (q) "(>Heq & HP1 & ? & >$)". iIntros "!>"; iSplit; iIntros "Hl1".
+ iMod ("Hclose1" with "[>-]") as "_"; last iLeft; auto with lia.
iExists _. iMod (own_update_2 with "H● Hown") as "$".
{ apply auth_update_dealloc, prod_local_update_2,
@@ -377,7 +407,7 @@ Section arc.
{ apply auth_update_dealloc, prod_local_update_2,
(cancel_local_update_empty 1%nat), _. }
destruct weak as [|weak].
- * iMod ("Hclose1" with "[-HP2 H Hl1]") as "_"; last by auto with iFrame.
+ * iMod ("Hclose1" with "[H●]") as "_"; last by auto with iFrame.
iExists _. iFrame.
* iMod ("Hclose1" with "[>-]") as "_"; last iLeft; auto with lia.
iExists _. iFrame. by replace (S (S weak) - 1) with (S weak:Z) by lia.
@@ -403,17 +433,17 @@ Section arc.
Proof using HP1.
iIntros "#INV #Hdrop #Hdealloc !# * (HP & Hown & HP1) HΦ". iLöb as "IH".
wp_rec. wp_bind (!ˢᶜ_)%E. iInv N as (st) "[>H● H]" "Hclose".
- iDestruct (arc_tok_auth_val with "H● Hown") as %(?& s &?&[-> _]).
- iDestruct "H" as (?) "[H H']". wp_read. iMod ("Hclose" with "[H H' H●]") as "_".
- { iExists _. auto with iFrame. }
+ iDestruct (arc_tok_auth_val with "H● Hown") as %(?& s &?&?&[-> _]).
+ iDestruct "H" as (?) "(? & ? & ? & ?)". wp_read.
+ iMod ("Hclose" with "[-HP Hown HP1 HΦ]") as "_". { iExists _. auto with iFrame. }
iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _).
iInv N as (st) "[>H● H]" "Hclose".
- iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s' & w &[-> Hqq']).
- iDestruct "H" as (q'') "(Hs & Hw & >Hq'' & HP1')". iDestruct "Hq''" as %Hq''.
+ iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s' & wl & w &[-> Hqq']).
+ iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
destruct (decide (s = s')) as [<-|?].
- wp_apply (wp_cas_int_suc with "Hs"); first done. iIntros "Hs".
destruct decide as [->|?].
- + revert Hq''. rewrite -Hqq' // => Hq''.
+ + destruct Hqq' as [<- ->].
iMod (own_update_2 with "H● Hown") as "[H● H◯]".
{ apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
etrans; first apply cancel_local_update_empty, _.
@@ -432,11 +462,12 @@ Section arc.
apply delete_option_local_update, _. }
iFrame. iApply "Hclose". iExists _. by iFrame.
+ destruct Hqq' as [? ->].
- rewrite -[in (_, _)](Pos.succ_pred s) // -Pos.add_1_l -pair_op -Cinl_op Some_op.
+ rewrite -[in (_, _)](Pos.succ_pred s) // -[wl in Cinl (_, wl)]left_id
+ -Pos.add_1_l -2!pair_op -Cinl_op Some_op.
iMod (own_update_2 _ _ _ _ with "H● Hown") as "H●".
{ apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_empty, _. }
iMod ("Hclose" with "[- HΦ HP]") as "_".
- { iExists _. iFrame. iExists (q + q'')%Qp. iFrame. iSplit; first by destruct s.
+ { iExists _. iFrame. iExists (q + q'')%Qp. iFrame. iSplit; last by destruct s.
iIntros "!> !%". rewrite assoc -Hq''. f_equal. apply comm, _. }
iModIntro. wp_apply (wp_if _ true). wp_op. by intros [=->]. intros _.
wp_if. by iApply "HΦ".
@@ -453,12 +484,11 @@ Section arc.
if b then P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ) else arc_tok γ q ∗ P1 q }}}.
Proof using HP1.
iIntros "#INV !# * [Hown HP1] HΦ". wp_rec. iInv N as (st) "[>H● H]" "Hclose".
- iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s & w &[-> Hqq']).
- iDestruct "H" as (q'') "(Hs & Hw & >Hq'' & HP1')". iDestruct "Hq''" as %Hq''.
+ iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s & wl & w &[-> Hqq']).
+ iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
destruct (decide (s = xH)) as [->|?].
- wp_apply (wp_cas_int_suc with "Hs"); first done. iIntros "Hs".
- revert Hq''. rewrite -Hqq' // => Hq''.
- iMod (own_update_2 with "H● Hown") as "[H● H◯]".
+ destruct Hqq' as [<- ->]. iMod (own_update_2 with "H● Hown") as "[H● H◯]".
{ apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
etrans; first apply cancel_local_update_empty, _.
by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
@@ -474,18 +504,70 @@ Section arc.
apply delete_option_local_update, _. }
iApply "Hclose". iExists _. by iFrame.
- wp_apply (wp_cas_int_fail with "Hs"); [done|congruence|]. iIntros "Hs".
- iMod ("Hclose" with "[Hs Hw HP1' H●]") as "_"; first by iExists _; auto with iFrame.
+ iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_"; first by iExists _; auto with iFrame.
iApply ("HΦ" $! false). by iFrame.
Qed.
- (* Lemma try_unwrap_spec (γ : gname) (q: Qp) (l : loc) : *)
- (* is_arc γ l -∗ *)
- (* {{{ own γ (arc_tok q) ∗ P1 q }}} get_mut [ #l] *)
- (* {{{ (b : bool), RET #b ; *)
- (* if b then P1 1 ∗ (P1 1 ={⊤}=∗ ∃ γ' q', own γ' (arc_tok q') ∗ P1 q') *)
- (* else own γ (arc_tok q) ∗ P1 q }}}. *)
- (* Proof. *)
-
+ Lemma is_unique_spec (γ : gname) (q: Qp) (l : loc) :
+ is_arc P1 P2 N γ l -∗
+ {{{ arc_tok γ q ∗ P1 q }}} is_unique [ #l]
+ {{{ (b : bool), RET #b ;
+ if b then l ↦ #1 ∗ shift_loc l 1 ↦ #1 ∗ P1 1
+ else arc_tok γ q ∗ P1 q }}}.
+ Proof using HP1.
+ iIntros "#INV !# * [Hown HP1] HΦ". wp_rec. wp_bind (CAS _ _ _). wp_op.
+ iInv N as (st) "[>H● H]" "Hclose".
+ iDestruct (arc_tok_auth_val with "H● Hown") as %(? & ? & wl & w &[-> _]).
+ iDestruct "H" as (?) "(>Hq'' & HP1' & >Hs & >Hw)".
+ destruct wl; last (destruct w; last first).
+ - iDestruct "Hw" as "[Hw %]". subst.
+ iApply (wp_cas_int_fail with "Hw")=>//. iNext. iIntros "Hw".
+ iMod ("Hclose" with "[-HΦ Hown HP1]") as "_"; first by iExists _; eauto with iFrame.
+ iModIntro. iApply (wp_if _ false). iModIntro. wp_value. iApply "HΦ". iFrame.
+ - iApply (wp_cas_int_fail with "Hw"); [done|lia|]. iNext. iIntros "Hw".
+ iMod ("Hclose" with "[-HΦ Hown HP1]") as "_"; first by iExists _; eauto with iFrame.
+ iModIntro. iApply (wp_if _ false). iModIntro. wp_value. iApply "HΦ". iFrame.
+ - iApply (wp_cas_int_suc with "Hw")=>//. iNext. iIntros "Hw".
+ iMod (own_update_2 with "H● Hown") as "[H● H◯]".
+ { by apply auth_update, prod_local_update_1, option_local_update,
+ csum_local_update_l, prod_local_update_2,
+ (alloc_option_local_update (Excl ())). }
+ iMod ("Hclose" with "[-HΦ HP1 H◯]") as "_"; first by iExists _; eauto with iFrame.
+ iModIntro. iApply (wp_if _ true). iNext. wp_bind (!ˢᶜ_)%E.
+ iInv N as ([st ?]) "[>H● H]" "Hclose".
+ iDestruct (own_valid_2 with "H● H◯") as
+ %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_valid_discrete_2.
+ simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & [|Hincl]); last first.
+ + apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
+ destruct Hincl as (?&[[??]?]&[=<-]&->&[[_ Hlt]%prod_included _]%prod_included).
+ simpl in Hlt. apply pos_included in Hlt.
+ iDestruct "H" as (?) "(? & ? & ? & ?)". wp_read.
+ iMod ("Hclose" with "[-HΦ H◯ HP1]") as "_"; first by iExists _; auto with iFrame.
+ iModIntro. wp_let. wp_op; [lia|intros _]. wp_let. wp_op. wp_bind (_ <-ˢᶜ _)%E.
+ iInv N as ([st w]) "[>H● H]" "Hclose".
+ iDestruct (own_valid_2 with "H● H◯") as
+ %[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_valid_discrete_2.
+ simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & Hincl); last first.
+ assert (∃ q p, x2 = Cinl (q, p, Excl' ())) as (? & ? & ->).
+ { destruct Hincl as [|Hincl]; first by setoid_subst; eauto.
+ apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
+ destruct Hincl as (?&[[??]?]&[=<-]&->&[_ Hincl%option_included]%prod_included).
+ simpl in Hincl. destruct Hincl as [[=]|(?&?&[=<-]&->&[?|[]%exclusive_included])];
+ [|by apply _|by apply Hval]. setoid_subst. eauto. }
+ iDestruct "H" as (?) "(? & ? & ? & >? & >%)". subst. wp_write.
+ iMod (own_update_2 with "H● H◯") as "[H● H◯]".
+ { apply auth_update, prod_local_update_1, option_local_update,
+ csum_local_update_l, prod_local_update_2, delete_option_local_update, _. }
+ iMod ("Hclose" with "[-HΦ H◯ HP1]") as "_"; first by iExists _; auto with iFrame.
+ iModIntro. wp_seq. iApply "HΦ". iFrame.
+ + setoid_subst. iDestruct "H" as (?) "(Hq & ? & ? & >? & >%)". subst. wp_read.
+ iMod (own_update_2 with "H● H◯") as "H●".
+ { apply auth_update_dealloc. rewrite -{1}[(_, 0%nat)]right_id.
+ apply cancel_local_update_empty, _. }
+ iMod ("Hclose" with "[H●]") as "_"; first by iExists _; iFrame.
+ iModIntro. wp_seq. wp_op=>[_|//]. wp_let. wp_op. wp_write. iApply "HΦ".
+ iDestruct "Hq" as %<-. iFrame.
+ Qed.
End arc.
Typeclasses Opaque is_arc arc_tok weak_tok.
\ No newline at end of file