From 18d3574ae4e319366a8a0dd89dfd7e3b77428f58 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 26 Apr 2017 14:06:14 +0200
Subject: [PATCH] rc_strong_count, rc_weak_count.
---
theories/typing/lib/rc/rc.v | 118 +++++++++++++++++++++++++++++++++++-
1 file changed, 115 insertions(+), 3 deletions(-)
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 25ba131d..9efa17bb 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -8,8 +8,6 @@ From lrust.typing Require Export type.
From lrust.typing Require Import typing option.
Set Default Proof Using "Type".
-(* TODO : weak_count strong_count *)
-
Definition rc_stR :=
prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitC))) natUR.
Class rcG Σ :=
@@ -346,6 +344,120 @@ Section code.
destruct strong=>//=. by rewrite Pos.pred_double_succ.
Qed.
+ Definition rc_strong_count : val :=
+ funrec: <> ["rc"] :=
+ let: "r" := new [ #1 ] in
+ let: "rc'" := !"rc" in
+ let: "rc''" := !"rc'" in
+ let: "strong" := !("rc''" +ₗ #0) in
+ "r" <- "strong";;
+ delete [ #1; "rc" ];; return: ["r"].
+
+ Lemma rc_strong_count_type ty `{!TyWf ty} :
+ typed_val rc_strong_count (fn(∀ α, ∅; &shr{α} rc ty) → int).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+ iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
+ iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+ rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
+ destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
+ (* All right, we are done preparing our context. Let's get going. *)
+ iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
+ wp_bind (!_)%E.
+ iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_step_fupd with "Hshr"); [done..|].
+ iMod (frac_bor_acc with "LFT Hlrc Hα2") as (q') "[Hlrc↦ Hclose]"; first solve_ndisj.
+ iApply wp_fupd. wp_read.
+ iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". iIntros "!> [Hα1 Hproto]".
+ iDestruct "Hproto" as (γ ν q'') "#(Hαν & Hpersist & Hrctokb)".
+ iModIntro. wp_let. wp_op. rewrite shift_loc_0.
+ (* Finally, finally... opening the thread-local Rc protocol. *)
+ iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)".
+ iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
+ iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
+ iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
+ iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
+ %option_included _]%prod_included [Hval _]]%auth_valid_discrete_2;
+ setoid_subst; try done; last first.
+ { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
+ apply csum_included in Hincl. naive_solver. }
+ iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'† & >% & Hνtok & Hν†)".
+ wp_read. wp_let.
+ (* And closing it again. *)
+ iMod ("Hclose3" with "[$Hrctok] Hna") as "[Hα1 Hna]".
+ iMod ("Hclose2" with "[Hrc● Hl'1 Hl'2 Hl'† Hνtok Hν† $Hna]") as "Hna".
+ { iExists _. iFrame "Hrc●". iExists _. auto with iFrame. }
+ iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+ (* Finish up the proof. *)
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); r ◁ box (uninit 1);
+ #(Z.pos s0) ◁ int ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { unlock.
+ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+ iFrame. }
+ iApply type_assign; [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+
+ Definition rc_weak_count : val :=
+ funrec: <> ["rc"] :=
+ let: "r" := new [ #1 ] in
+ let: "rc'" := !"rc" in
+ let: "rc''" := !"rc'" in
+ let: "strong" := !("rc''" +ₗ #1) in
+ "r" <- "strong";;
+ delete [ #1; "rc" ];; return: ["r"].
+
+ Lemma rc_weak_count_type ty `{!TyWf ty} :
+ typed_val rc_weak_count (fn(∀ α, ∅; &shr{α} rc ty) → int).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+ iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
+ iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+ rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
+ destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
+ (* All right, we are done preparing our context. Let's get going. *)
+ iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
+ wp_bind (!_)%E.
+ iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_step_fupd with "Hshr"); [done..|].
+ iMod (frac_bor_acc with "LFT Hlrc Hα2") as (q') "[Hlrc↦ Hclose]"; first solve_ndisj.
+ iApply wp_fupd. wp_read.
+ iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". iIntros "!> [Hα1 Hproto]".
+ iDestruct "Hproto" as (γ ν q'') "#(Hαν & Hpersist & Hrctokb)".
+ iModIntro. wp_let. wp_op.
+ (* Finally, finally... opening the thread-local Rc protocol. *)
+ iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)".
+ iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
+ iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
+ iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
+ iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
+ %option_included _]%prod_included [Hval _]]%auth_valid_discrete_2;
+ setoid_subst; try done; last first.
+ { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
+ apply csum_included in Hincl. naive_solver. }
+ iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'† & >% & Hνtok & Hν†)".
+ wp_read. wp_let.
+ (* And closing it again. *)
+ iMod ("Hclose3" with "[$Hrctok] Hna") as "[Hα1 Hna]".
+ iMod ("Hclose2" with "[Hrc● Hl'1 Hl'2 Hl'† Hνtok Hν† $Hna]") as "Hna".
+ { iExists _. iFrame "Hrc●". iExists _. auto with iFrame. }
+ iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+ (* Finish up the proof. *)
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); r ◁ box (uninit 1);
+ #(S weak) ◁ int ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { unlock.
+ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+ iFrame. }
+ iApply type_assign; [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+
Definition rc_new ty : val :=
funrec: <> ["x"] :=
let: "rcbox" := new [ #(2 + ty.(ty_size))%nat ] in
@@ -425,7 +537,7 @@ Section code.
iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
- iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
+ iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
%option_included _]%prod_included [Hval _]]%auth_valid_discrete_2;
setoid_subst; try done; last first.
{ exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
--
GitLab