From dbe8fbd79cdce0f3fcc2b8c79acc1d9b3964a0fc Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Thu, 7 Jun 2018 00:22:56 +0200
Subject: [PATCH] almost finish rwlock, only rwlockreadguard drop code left
---
_CoqProject | 1 +
theories/typing/lib/rwlock/rwlock.v | 47 ++++++--
theories/typing/lib/rwlock/rwlock_code.v | 23 ++--
.../typing/lib/rwlock/rwlockreadguard_code.v | 114 ++++++++----------
4 files changed, 102 insertions(+), 83 deletions(-)
diff --git a/_CoqProject b/_CoqProject
index 929cc6a4..75aca45b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -66,6 +66,7 @@ theories/typing/lib/refcell/ref.v
theories/typing/lib/rwlock/rwlock.v
theories/typing/lib/rwlock/rwlockreadguard.v
theories/typing/lib/rwlock/rwlockwriteguard.v
+theories/typing/lib/rwlock/rwlock_code.v
theories/typing/lib/rwlock/rwlockwriteguard_code.v
theories/typing/examples/get_x.v
theories/typing/examples/rebor.v
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index db68ab5f..601fee93 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -1,3 +1,4 @@
+From Coq.QArith Require Import Qcanon.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth csum frac agree.
From iris.bi Require Import fractional.
@@ -99,8 +100,10 @@ Section rwlock_inv.
Qed.
Lemma rwown_global_reading_st st q ν γs:
- rwown γs (st_global st) -∗ rwown γs (reading_st q ν) -∗
- ⌜∃ q' n, st = Some (inr (ν,q',n))⌝.
+ rwown γs (st_global st) -∗ rwown γs (reading_st q ν) -∗
+ ⌜∃ q' n, st = Some (inr (ν,q',n))
+ ∧ ( q' = q ∧ n = 1%positive
+ ∨ (∃ q0, q' = (q + q0)%Qp) ∧ n = (1 + Pos.pred n)%positive)⌝.
Proof.
iIntros "m r". iCombine "m" "r" as "mr".
iDestruct (own_valid with "mr") as %[INCL VAL]%auth_valid_discrete_2.
@@ -112,13 +115,40 @@ Section rwlock_inv.
/Some_included [Eq|/csum_included [//|[[?[?[??//]]]|[a[b[Eqa[Eqb INCL]]]]]]].
+ inversion Eq as [| ?? Eq1 |]. inversion Eq1 as [Eq2].
inversion Eq2 as [Eq3 ]. simpl in Eq3. apply to_agree_inj in Eq3.
- inversion Eq3. by do 2 eexists.
+ inversion Eq3. simpl in *. subst. do 2 eexists.
+ split; [done|by left].
+ inversion Eqa. inversion Eqb. subst a b.
- apply prod_included in INCL as [[INCL%to_agree_included _]%prod_included _].
- inversion INCL. by do 2 eexists.
+ apply prod_included in INCL as
+ [[INCL%to_agree_included LE1]%prod_included LE2%pos_included].
+ inversion INCL. do 2 eexists. split; [done|]. right. split.
+ * rewrite /= in LE1. destruct LE1 as [q1 LE1]. exists q1. by rewrite -frac_op'.
+ * rewrite -Pplus_one_succ_l Pos.succ_pred => //?. by subst.
- by apply option_included in INCL as [?|[?[?[?[??]]]]].
Qed.
+ Lemma rwown_update_read_dealloc_1 γs ν q:
+ rwown γs (st_global (Some (inr (ν,q,1%positive)))) -∗ rwown γs (reading_st q ν)
+ ==∗ rwown γs (st_global None).
+ Proof.
+ iIntros "m r". iCombine "m" "r" as "mr".
+ iMod (own_update with "mr") as "$"; [|done].
+ apply auth_update_dealloc.
+ rewrite /= -(right_id None op (Some _)). apply cancel_local_update_unit, _.
+ Qed.
+
+ Lemma rwown_update_read_dealloc γs ν q q' n:
+ rwown γs (st_global (Some (inr (ν,(q + q')%Qp,(1 + n)%positive))))
+ -∗ rwown γs (reading_st q' ν)
+ ==∗ rwown γs (st_global (Some (inr (ν,q,n)))).
+ Proof.
+ iIntros "m r". iCombine "m" "r" as "mr".
+ iMod (own_update with "mr") as "$"; [|done].
+ apply auth_update_dealloc.
+ rewrite -frac_op' -pos_op_plus /= (cmra_comm_L q)
+ -{1}(agree_idemp (to_agree _)) -2!pair_op -Cinr_op Some_op.
+ by apply (cancel_local_update_unit (Some _)), _.
+ Qed.
+
Lemma rwown_global_writing_st st γs:
rwown γs (st_global st) -∗ rwown γs writing_st -∗
⌜st = (Some (inl tt))⌝.
@@ -145,10 +175,11 @@ Section rwlock_inv.
GPS_SWSharedWriter l () #0 γ ∗
(∃ n', GPS_SWSharedReader l () #n' 1%Qp γ)
| Some (inr (ν, q, n)) => (* Locked for read. *)
+ GPS_SWSharedWriter l () #(Z.pos n) γ ∗
∃ q', □ (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
([†ν] ={↑lftN ∪ ↑histN}=∗ &{α}tyO) ∗
- (□ tyS (α ⊓ ν)) ∗ ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν] ∗
- GPS_SWSharedWriter l () #(Z.pos n) γ ∗
+ (□ tyS (α ⊓ ν)) ∗ ⌜(q + q')%Qp = 1%Qp⌝ ∗
+ q'.[ν] ∗
(∃ n', GPS_SWSharedReader l () #n' q' γ)
| _ => (* Locked for write. *) True
end
@@ -263,8 +294,8 @@ Section rwlock_inv.
{ iIntros (?) "W". iDestruct (GPS_SWRawWriter_RawReader with "W") as "#$".
iSplitR ""; iExists (Some $ inr (ν, (1/2)%Qp, n)); [|by iFrame "Share"].
iModIntro. iSplitL ""; [done|]. iFrame "Hst".
- iExists _. iFrame "Hshr Htok2 Hhν".
iDestruct (GPS_SWRawWriter_shared with "W") as "[$ [R ?]]".
+ iExists _. iFrame "Hshr Htok2 Hhν".
iSplitR "R"; last iSplitL ""; [|by rewrite Qp_div_2|by iExists _].
iIntros "!> Hν". iDestruct (lft_tok_dead with "Htok Hν") as "[]". }
iExists γ, γs, tyO, tyS. iModIntro. iFrame "inv EqO EqS". by iExists _.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 92d1b879..0e440d8f 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -251,8 +251,8 @@ Section rwlock_functions.
iDestruct "Eqst" as %Eqst. inversion Eqst as [Eqst2]. clear Eqst.
destruct st2 as [[[]|[[ν q] n]]|]; simpl in Eqst2.
+ exfalso. clear -Eqst2 Hm1. rewrite Eqst2 in Hm1. omega.
- + iDestruct 1 as (?) "[_ #Share]".
- iDestruct "INT" as (q') "(#H† & Hh & #Hshr & Hqq' & Hν & W & Rs)".
+ + iDestruct 1 as (?) "[_ #Share]". iDestruct "INT" as "[W INT]".
+ iDestruct "INT" as (q') "(#H† & Hh & #Hshr & Hqq' & Hν & Rs)".
iDestruct "Hqq'" as %Hqq'.
iMod (rwown_update_read ν n q q' γs Hqq' with "g") as "[g rst]".
iModIntro. iExists (). iSplitL ""; [done|].
@@ -285,7 +285,7 @@ Section rwlock_functions.
iSplitL "Htok2 rst R1"; last iSplitR "".
* iExists _, _. iFrame "Htok2 Hshr rst H†". simpl. by iExists _.
* iExists st2. subst st2. rewrite /= -Eqst. iSplitL ""; [done|].
- iFrame "g". iExists _. iFrame "H† Hh Hshr Htok1 W".
+ iFrame "g W". iExists _. iFrame "H† Hh Hshr Htok1".
rewrite -Qp_plus_assoc Qp_div_2. iSplitL ""; [done|by iExists _].
* iExists st2. subst st2. rewrite /= -Eqst. by iFrame "Share".
+ iDestruct "R" as (vR') "[R1 R2]".
@@ -293,7 +293,7 @@ Section rwlock_functions.
subst q'. rewrite -Eqst /=. iSplitL "Htok2 rst R1"; last iSplitR "".
* iExists _, _. iFrame "Htok2 Hshr rst H†". simpl. by iExists _.
* iExists st2. subst st2. simpl. iSplitL ""; [done|].
- iFrame "g". iExists _. iFrame "H† Hshr Htok1 W".
+ iFrame "g W". iExists _. iFrame "H† Hshr Htok1".
iSplitL "Hh". { iIntros "Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
rewrite Qp_div_2. iSplitL ""; [done|by iExists _].
* iExists st2. subst st2. rewrite /=. by iFrame "Share". }
@@ -409,10 +409,11 @@ Section rwlock_functions.
iNext. simpl.
iIntros (b v' [])
- "(INV & _ &[([%%] &_& mst & sst & Hβ & wst) | ([% Neq] & _ & _ & P)])".
+ "(INV & _ &[([%%] &_& Hβ & wst & W & R') | ([% Neq] & R' & _ & _)])".
- subst b v'.
- iMod ("Hclose''" with "[mst INV]") as "Hβtok".
- { iIntros "Vb'". iDestruct ("INV" with "Vb'") as "$". by iExists _. }
+ iDestruct "R'" as (?) "R'".
+ iMod (GPS_SWSharedWriter_revert with "W R' INV") as "[W INV]".
+ iMod ("Hclose''" with "INV") as "Hβtok".
iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iModIntro. wp_case.
iApply (type_type _ _ _
@@ -422,15 +423,11 @@ Section rwlock_functions.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
tctx_hasty_val' //. iFrame "Hx Hr".
iExists γs, β. iSplitL "Hβ"; [by iApply (bor_iff with "[$EqO] Hβ")|].
- iFrame "Hαβ wst sst".
- iExists _,_,_. iFrame "EqO EqS Hinv". by iExists _. }
+ iFrame "Hαβ wst". iExists _,_,_. iFrame "W EqO EqS Hinv". by iExists _. }
iApply (type_sum_assign (option $ rwlockwriteguard α ty)); [solve_typing..|].
simpl. iApply type_jump; solve_typing.
- subst b.
- iDestruct (rel_exist with "P") as (st') "mst".
- iDestruct (rel_embed_elim with "mst") as "mst".
- iMod ("Hclose''" with "[INV mst]") as "Hβtok".
- { iIntros "Vb'". iDestruct ("INV" with "Vb'") as "$". by iExists _. }
+ iMod ("Hclose''" with "INV") as "Hβtok".
iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iModIntro. wp_case.
iApply (type_type _ _ _
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 4f23176e..5c83eb43 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -5,7 +5,7 @@ From iris.bi Require Import fractional.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import typing.
From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard.
-From gpfsl.gps Require Import middleware.
+From gpfsl.gps Require Import middleware protocols.
Set Default Proof Using "Type".
Section rwlockreadguard_functions.
@@ -74,7 +74,7 @@ Section rwlockreadguard_functions.
iDestruct "HT" as "[Hx Hx']".
destruct x' as [[|lx'|]|]; try done. simpl.
iDestruct "Hx'" as (ν q γs β) "(Hx' & #Hαβ & Hν & H◯ & H† & Hinv)".
- iDestruct "Hinv" as (γ tyO tyS) "(R & (EqO & EqS) & #Hinv)".
+ iDestruct "Hinv" as (γ tyO tyS) "(R & (EqO & EqS & _) & #Hinv)".
iDestruct "R" as (vR) "R".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
@@ -94,12 +94,20 @@ Section rwlockreadguard_functions.
set Q : () → vProp Σ := (λ _, True)%I.
set R : () → lit → vProp Σ := (λ _ _, True)%I.
set T : () → () → vProp Σ :=
- (λ _ _,
+ (λ _ _, (q).[ν] ∗
□ (∀ κ q0 E0, ⌜lftE ⊆ E0⌝ -∗ &{κ} tyO -∗ (q0).[κ] ={E0}=∗ □ tyS κ ∗ (q0).[κ]) ∗
- ∃ ν q' st2, (q').[ν] ∗
- rwown γs (st_global st2) ∗
- □ tyS (β ⊓ ν) ∗
- □ ((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]))%I.
+ rwown γs (reading_st q ν) ∗
+ ∃ q' n,
+ ⌜Z_of_rwlock_st st2 = Z.pos n ∧
+ (q' = q ∧ n = 1%positive ∨
+ (∃ q0 : Qp, q' = (q + q0)%Qp) ∧ n = (1 + Pos.pred n)%positive)⌝ ∗
+ rwown γs (st_global (Some (inr (ν,q',n)))) ∗
+ (∃ qr, □ ((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
+ ([†ν] ={↑lftN ∪ ↑histN}=∗ &{β} tyO) ∗
+ □ tyS (β ⊓ ν) ∗
+ ⌜(q' + qr)%Qp = 1%Qp⌝ ∗
+ (qr).[ν] ∗
+ (∃ n', GPS_SWSharedReader lx' ((): unitProtocol) #n' qr γ)))%I.
iApply (GPS_SWSharedWriter_CAS_int_strong (rwlock_interp γs β tyO tyS) _
rwlock_noCAS _ _ _ _ #(Z_of_rwlock_st st2 - 1) () _ _ _
P T Q R _ Vb' _ (⊤ ∖ ↑rwlockN)
@@ -109,60 +117,40 @@ Section rwlockreadguard_functions.
{ iIntros "!> !>" (???). by iApply rwlock_interp_duplicable. }
{ simpl. iSplitR "H◯ Hν"; last iFrame "∗".
iNext. iIntros ([] _). iSplit; [|by iIntros (?) "_ _"]. iSplitL "".
- - iIntros "(H◯ & Hν)". iDestruct 1 as (st2') "[Eqst [g INT]]".
+ - iIntros "(H◯ & Hν)". iDestruct 1 as (st2') "[Eqst [H● INT]]".
iDestruct "Eqst" as %Eqst.
- iDestruct (rwown_global_reading_st with "g H◯") as %[q' [n Eqst2']].
- subst st2'. iDestruct 1 as (?) "[_ #Share]".
+ iDestruct (rwown_global_reading_st with "H● H◯") as %[q' [n [Eqst2' CASE]]].
+ subst st2'. simpl in Eqst. iDestruct 1 as (?) "[_ #Share]". iModIntro.
iExists (). rewrite Eqst /=. iSplitL ""; [done|].
- admit.
- - iIntros ([] _) "T W R". iSplitL ""; [done|].
+ iDestruct "INT" as "[$ INT]". rewrite /T. iFrame "Hν Share H◯".
+ iExists _,_. iFrame "H●". iSplitL""; [by inversion Eqst|]. iFrame "INT".
+ - iIntros ([] _) "(Hν & #Share & H◯ & T) W R". iSplitL ""; [done|].
+ iDestruct "T" as (q' n [Eqst Eq']) "[H● T]".
+ iDestruct "T" as (qr) "(#H† & Hh & #Hshr & Hqrq' & Hqr & Rm)".
+ iDestruct "Hqrq'" as %Hqrq'.
+ iDestruct "Rm" as (?) "Rm".
+ iDestruct (GPS_SWSharedReaders_join with "R Rm") as "R".
+ iCombine "Hν" "Hqr" as "Hν".
+ destruct Eq' as [[??]|[[q0 ?] Eqn]]; [subst q' n|subst q'].
+ + rewrite Hqrq'.
+ iMod (rwown_update_read_dealloc_1 with "H● H◯") as "H●". iModIntro.
+ rewrite Eqst /=. iSplitR ""; iExists None; [|by iFrame "Share"].
+ iSplitL ""; [done|]. iFrame "H● W". iSplitR "R"; [|by iExists _].
+ admit.
+ (* iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
+ iMod ("Hh" with "H†") as "Hb". iIntros "!> Hlx". iExists None. iFrame. *)
+ + rewrite Eqn Qp_plus_comm Eqst.
+ iMod (rwown_update_read_dealloc with "H● H◯") as "H●". iModIntro.
+ have Eqn': (Z.pos n - 1) = Z.pos (Pos.pred n).
+ { rewrite Pos2Z.inj_pred => // ?. by subst n. } rewrite Eqn'.
+ iSplitR ""; iExists (Some (inr (ν, q0, Pos.pred n))); [|by iFrame "Share"].
+ iSplitL ""; [done|]. iFrame "H● W".
+ iExists (q + qr)%Qp. iFrame "H† Hh Hshr Hν". iSplitR "R"; [|by iExists _].
+ by rewrite Qp_plus_assoc (Qp_plus_comm q0). }
-
- wp_read.
- iMod ("Hcloseβ" with "[H↦ INV]") as "Hβ"; first by iExists _; iFrame.
- iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _).
- iMod (at_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
- iDestruct "INV" as (st') "(Hlx & >H● & Hst)".
- destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?].
- + iAssert (|={⊤ ∖ ↑rwlockN,⊤ ∖ ↑rwlockN ∖ ↑lftN}▷=>
- (lx' ↦ #(Z_of_rwlock_st st'-1) ==∗ rwlock_inv tid lx' γ β ty))%I
- with "[H● H◯ Hx' Hν Hst H†]" as "INV".
- { iDestruct (own_valid_2 with "H● H◯") as %[[[=]| (? & st0 & [=<-] & -> & [Heq|Hle])]
- %option_included Hv]%auth_valid_discrete_2.
- - destruct st0 as [|[[agν q']n]|]; try by inversion Heq. revert Heq. simpl.
- intros [[EQ <-%leibniz_equiv]%(inj2 pair) <-%leibniz_equiv]
- %(inj Cinr)%(inj2 pair).
- iDestruct "Hst" as (ν' q') "(>EQν & _ & Hh & _ & >Hq & >Hν')".
- rewrite -EQ. iDestruct "EQν" as %<-%(inj to_agree)%leibniz_equiv.
- iCombine "Hν" "Hν'" as "Hν". iDestruct "Hq" as %->.
- iApply (step_fupd_mask_mono (↑lftN ∪ (⊤ ∖ ↑rwlockN ∖ ↑lftN)));
- last iApply (step_fupd_mask_frame_r _ ∅); [try set_solver..|];
- [apply union_least; solve_ndisj|].
- iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
- iMod ("Hh" with "H†") as "Hb". iIntros "!> Hlx". iExists None. iFrame.
- iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
- rewrite -(right_id None op (Some _)). apply cancel_local_update_unit, _.
- - iApply step_fupd_intro. set_solver. iNext. iIntros "Hlx".
- apply csum_included in Hle.
- destruct Hle as [|[(?&?&[=]&?)|(?&[[agν q']n]&[=<-]&->&Hle%prod_included)]];
- [by subst|].
- destruct Hle as [[Hag [q0 Hq]]%prod_included Hn%pos_included].
- iDestruct "Hst" as (ν' q'') "(EQν & H†' & Hh & Hshr & Hq & Hν')".
- iDestruct "EQν" as %EQν. revert Hag Hq. rewrite /= EQν to_agree_included.
- intros <-%leibniz_equiv ->%leibniz_equiv.
- iExists (Some (Cinr (to_agree ν, q0, Pos.pred n))).
- iSplitL "Hlx"; first by destruct n.
- replace (q ⋅ q0 + q'')%Qp with (q0 + (q + q''))%Qp by
- by rewrite (comm _ q q0) assoc. iCombine "Hν" "Hν'" as "Hν".
- iSplitL "H● H◯"; last by eauto with iFrame.
- iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
- assert (n = 1%positive ⋅ Pos.pred n) as EQn.
- { rewrite pos_op_plus -Pplus_one_succ_l Pos.succ_pred // =>?. by subst. }
- rewrite {1}EQn -{1}(agree_idemp (to_agree _)) -2!pair_op -Cinr_op Some_op.
- apply (cancel_local_update_unit (reading_st q ν)) , _. }
- iApply (wp_step_fupd with "INV"). done. set_solver.
- iApply (wp_cas_int_suc with "Hlx"); try done. iNext. iIntros "Hlx INV !>".
- iMod ("INV" with "Hlx") as "INV". iMod ("Hcloseβ" with "[$INV]") as "Hβ".
+ iNext. iIntros (b v' []) "(INV & _ & CASE)".
+ iDestruct "CASE" as "[[[% %] _]|[[% NE] [R' [_ [H◯ Hν]]]]]".
+ - subst b v'. iMod ("Hcloseβ" with "INV") as "Hβ".
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iModIntro. wp_if.
iApply (type_type _ _ _ [ x ◁ box (uninit 1)]
@@ -171,14 +159,16 @@ Section rwlockreadguard_functions.
iApply type_delete; [solve_typing..|].
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_jump; solve_typing.
- + iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
- iMod ("Hcloseβ" with "[Hlx H● Hst]") as "Hβ". by iExists _; iFrame.
+ - subst b. iMod ("Hcloseβ" with "INV") as "Hβ".
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iModIntro. wp_if.
iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lx' ◁ rwlockreadguard α ty]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val
- tctx_hasty_val' //=; simpl. auto 10 with iFrame. }
+ tctx_hasty_val' //=; simpl.
+ iFrame "Hx". iExists _,_,_,_. iFrame "Hx' Hαβ Hν H◯ H†".
+ iExists _,_,_. iSplitL "R'"; [by iExists _|]. iFrame "EqO EqS Hinv".
+ iExists _. by iFrame "RR". }
iApply type_jump; solve_typing.
- Qed.
+ Admitted.
End rwlockreadguard_functions.
--
GitLab