From b6760d1c4c8e4f7eae69e6e2fce5bf2e7f5b2bf4 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 6 Jun 2018 01:17:48 +0200
Subject: [PATCH] bump gpfsl and WIP rwlock code
---
_CoqProject | 2 -
opam | 2 +-
theories/lang/spawn.v | 13 +-
theories/typing/lib/rwlock/rwlock.v | 214 ++++++------------
theories/typing/lib/rwlock/rwlockreadguard.v | 9 +-
.../typing/lib/rwlock/rwlockreadguard_code.v | 45 ++--
theories/typing/lib/rwlock/rwlockwriteguard.v | 15 +-
7 files changed, 115 insertions(+), 185 deletions(-)
diff --git a/_CoqProject b/_CoqProject
index 75aca45b..c03b2e2b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -66,8 +66,6 @@ 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
theories/typing/examples/unbox.v
diff --git a/opam b/opam
index f11f39ad..96ec01e2 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
- "coq-gpfsl" { (= "dev.2018-06-04.0.f12ff24c") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2018-06-05.0.a660e9c0") | (= "dev") }
]
diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v
index 5a3db296..1b51e66b 100644
--- a/theories/lang/spawn.v
+++ b/theories/lang/spawn.v
@@ -61,7 +61,8 @@ Definition spawn_interp γe γf Ψ : interpC Σ unitProtocol :=
(* Accessor content for the GPS invariant *)
Definition spawn_inv γc γe γf γj c Ψ :=
- (tok γf ∗ tok γj ∨ (∃ V, GPS_INV (spawn_interp γe γf Ψ) c γc V))%I.
+ (tok γf ∗ tok γj
+ ∨ (∃ V, GPS_INV (spawn_interp γe γf Ψ) c (λ _ _ _, True : Prop) γc V))%I.
Definition finish_handle γc γe c Ψ : vProp :=
(∃ γf γj v, (c >> 1) ↦ v ∗ GPS_SWRawWriter c () #0 γc
@@ -111,7 +112,7 @@ Proof.
iMod (own_alloc (Excl ())) as (γe) "Hγe"; first done.
rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
iDestruct "Hl" as "[Hc Hd]". wp_write.
- iMod (GPS_SWRaw_Init_vs (spawn_interp γe γf Ψ) _ false _ () with "Hc []")
+ iMod (GPS_SWRaw_Init_vs (spawn_interp γe γf Ψ) _ _ false _ () with "Hc []")
as (γc) "[SW gpsI]".
{ iIntros (?). rewrite /spawn_interp /=. by iSplit; iExists false. }
iDestruct (GPS_SWRawWriter_RawReader with "SW") as "#R". simpl.
@@ -138,8 +139,8 @@ Proof.
auto. }
iDestruct "Hinv" as (Vb) "HInv".
iApply (GPS_SWRawWriter_rel_write (spawn_interp γe γf Ψ)
- _ True%I () () _ #1 _ _ Vb
- with "[$SW HInv Hf HΨ Hd]"); [done|solve_ndisj|..].
+ _ (λ _ _ _, True : Prop) True%I () () _ #1 _ _ Vb
+ with "[$SW HInv Hf HΨ Hd]"); [done|solve_ndisj|done|..].
{ iSplitL "HInv".
- iIntros "mb". iNext. by iApply (monPred_in_elim with "mb HInv").
- iNext. iIntros "_ SW". iSplitL ""; [done|].
@@ -163,7 +164,7 @@ Proof.
{ iExFalso. iCombine "Hj" "Hj'" as "Hj". iDestruct (own_valid with "Hj") as "%".
auto. }
iDestruct "Hinv" as (Vb) "HInv".
- iApply (GPS_SWRawReader_read (spawn_interp γe γf Ψ') _ _ () _ _ _ Vb
+ iApply (GPS_SWRawReader_read (spawn_interp γe γf Ψ') _ _ _ () _ _ _ Vb
with "[$R HInv]"); [solve_ndisj|by right|..].
{ iSplitL "HInv".
- iIntros "mb". iNext. by iApply (monPred_in_elim with "mb HInv").
@@ -181,7 +182,7 @@ Proof.
iMod ("Hclose" with "[Hj Hf]") as "_". { iNext. iLeft. iFrame. }
iModIntro. wp_if. wp_op. wp_read. wp_let.
iApply (wp_hist_inv); [done|]. iIntros "Hist".
- iMod (GPS_SWRawWriter_dealloc _ _ true with "Hist HInv SW") as "[Hc _]";
+ iMod (GPS_SWRawWriter_dealloc _ _ _ true with "Hist HInv SW") as "[Hc _]";
[done|].
iAssert (c ↦∗ [ #1 ; v])%I with "[Hc Hd]" as "Hc".
{ rewrite own_loc_na_vec_cons own_loc_na_vec_singleton. iFrame. }
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index d36f06a2..462e7ed3 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -10,18 +10,13 @@ Definition rwlock_st := option (() + lft * frac * positive).
Definition rwlock_stR :=
optionUR (csumR (exclR unitC) (prodR (prodR (agreeR lftC) fracR) positiveR)).
-Definition rwlock_stAgreeR :=
- optionUR (prodR (exclR unitC) (agreeR (leibnizC rwlock_st))).
-Definition rwlockR :=
- prodR (authR rwlock_stR) (authR rwlock_stAgreeR).
+Definition rwlockR := authR rwlock_stR.
Class rwlockG Σ := RwLockG {
rwlock_stateG :> inG Σ rwlockR ;
rwlock_gpsG :> gpsG Σ unitProtocol;
- rwlock_gpsExAgG :> gpsExAgG Σ;
}.
-Definition rwlockΣ : gFunctors :=
- #[GFunctor rwlockR; gpsΣ unitProtocol; GFunctor (agreeR (leibnizC Qp))].
+Definition rwlockΣ : gFunctors := #[GFunctor rwlockR; gpsΣ unitProtocol].
Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
Proof. solve_inG. Qed.
@@ -42,12 +37,9 @@ Definition Z_of_rwlock_st (st : rwlock_st) : Z :=
Definition rwlockN := lrustN .@ "rwlock".
Notation rwown γs st := (⎡ own γs (st : rwlockR) ⎤ : vProp _)%I.
-Notation st_agree st := (Some (Excl (), to_agree st)).
-Notation st_full st := (● rwlock_to_st st ⋅ ◯ rwlock_to_st st,
- ● st_agree st ⋅ ◯ st_agree st).
-Notation st_global st:= (● rwlock_to_st st,
- ● st_agree st ⋅ ◯ st_agree st).
-Notation st_local st := (◯ (rwlock_to_st st), ε).
+Notation st_full st := (● rwlock_to_st st ⋅ ◯ rwlock_to_st st).
+Notation st_global st:= (● rwlock_to_st st).
+Notation st_local st := (◯ rwlock_to_st st).
Section rwlock_inv.
Context `{typeG Σ, rwlockG Σ}.
@@ -56,78 +48,28 @@ Section rwlock_inv.
(* Cmra operations *)
Definition reading_st (q : frac) (ν : lft) : rwlockR
:= st_local (Some $ inr (ν, q, xH)).
- Definition writing_st : rwlockR := st_local (Some $ inl ()).
- Definition main_st (st: rwlock_st): rwlockR := (● rwlock_to_st st, ● st_agree st).
- Definition sub_st (st: rwlock_st) : rwlockR := (ε, ◯ st_agree st).
-
- Lemma rwown_main_sub_agree st1 st2 γs :
- rwown γs (main_st st1) -∗ rwown γs (sub_st st2) -∗ ⌜st1 = st2⌝.
- Proof.
- iIntros "m s". iCombine "m" "s" as "ms".
- rewrite pair_op right_id.
- iDestruct (own_valid with "ms")
- as %[_ [INCL VAL]%(auth_valid_discrete_2 (A:= rwlock_stAgreeR))].
- iPureIntro.
- destruct (@Some_included_exclusive _ _
- (pair_exclusive_l _ _ (excl_exclusive _)) _ INCL VAL)
- as [_ Eq2%(to_agree_inj (A:= leibnizC _))]. done.
- Qed.
-
- Lemma rwown_st_global_main_sub st γs :
- rwown γs (st_global st) ⊣⊢ rwown γs (main_st st) ∗ rwown γs (sub_st st).
- Proof.
- by rewrite /main_st /sub_st -embed_sep -own_op pair_op right_id.
- Qed.
-
- Lemma rwown_full_global_local st γs :
- rwown γs (st_full st) ⊣⊢ rwown γs (st_local st) ∗ rwown γs (st_global st).
- Proof.
- by rewrite -embed_sep -own_op pair_op left_id.
- Qed.
-
- Lemma rwown_full_split st γs :
- rwown γs (st_full st)
- ⊣⊢ rwown γs (st_local st) ∗ rwown γs (main_st st) ∗ rwown γs (sub_st st).
- Proof. by rewrite rwown_full_global_local rwown_st_global_main_sub. Qed.
-
- Lemma rwown_agree_update (st st': rwlock_st) :
- ● (st_agree st : rwlock_stAgreeR) ⋅ ◯ st_agree st
- ~~> ● st_agree st' ⋅ ◯ st_agree st'.
- Proof.
- apply (auth_update (A:=rwlock_stAgreeR)).
- apply (option_local_update (A:= prodR _ (agreeR (leibnizC _)))).
- eapply (exclusive_local_update (A:= prodR _ (agreeR (leibnizC _)))). done.
- Unshelve. by apply (pair_exclusive_l(B:=agreeR (leibnizC _))), excl_exclusive.
- Qed.
+ Definition writing_st : rwlockR := st_local (Some $ inl ()).
Lemma rwown_update_write_read ν γs :
let st' : rwlock_st := Some (inr (ν, (1/2)%Qp, 1%positive)) in
- rwown γs (main_st None) -∗ rwown γs (sub_st None)
- ==∗ rwown γs (main_st st') ∗ rwown γs (sub_st st') ∗ rwown γs (reading_st (1/2)%Qp ν).
+ rwown γs (st_global None)
+ ==∗ rwown γs (st_global st') ∗ rwown γs (reading_st (1/2)%Qp ν).
Proof.
- iIntros (st') "m s".
- rewrite bi.sep_assoc -rwown_st_global_main_sub -embed_sep -own_op pair_op right_id.
- iDestruct (rwown_st_global_main_sub with "[$m $s]") as "ms".
- iMod (own_update (A:=rwlockR) with "ms") as "$"; [|done].
- apply prod_update; simpl; [|by apply rwown_agree_update].
- apply auth_update_alloc.
- rewrite -(right_id None op (Some _)). by apply op_local_update_discrete.
+ iIntros (st') "g". rewrite -embed_sep -own_op.
+ iMod (own_update with "g") as "$"; [|done]. apply auth_update_alloc.
+ rewrite /= -(right_id None op (Some _)). by apply op_local_update_discrete.
Qed.
Lemma rwown_update_read ν (n: positive) (q q': frac) γs
(Hqq' : (q + q')%Qp = 1%Qp) :
let st : rwlock_st := (Some (inr (ν, q, n))) in
let st': rwlock_st := Some (inr (ν, (q + (q'/2)%Qp)%Qp, (n + 1)%positive)) in
- rwown γs (main_st st) -∗ rwown γs (sub_st st)
- ==∗ rwown γs (main_st st') ∗ rwown γs (sub_st st') ∗ rwown γs (reading_st (q'/2)%Qp ν).
+ rwown γs (st_global st)
+ ==∗ rwown γs (st_global st') ∗ rwown γs (reading_st (q'/2)%Qp ν).
Proof.
- iIntros (st') "m s".
- rewrite bi.sep_assoc -rwown_st_global_main_sub -embed_sep -own_op pair_op right_id.
- iDestruct (rwown_st_global_main_sub with "[$m $s]") as "ms".
- iMod (own_update (A:=rwlockR) with "ms") as "$"; [|done].
- apply prod_update; simpl; [|by apply rwown_agree_update].
- apply auth_update_alloc.
- rewrite Pos.add_comm Qp_plus_comm -pos_op_plus
+ iIntros (st') "g". rewrite -embed_sep -own_op.
+ iMod (own_update with "g") as "$"; [|done]. apply auth_update_alloc.
+ rewrite Pos.add_comm Qp_plus_comm -pos_op_plus /=
-{2}(agree_idemp (to_agree _)) -frac_op'
-2!pair_op -Cinr_op Some_op.
rewrite -{2}(right_id None op (Some (Cinr (_, (q' /2)%Qp, _)))).
@@ -140,39 +82,28 @@ Section rwlock_inv.
Lemma rwown_update_write γs :
let st' : rwlock_st := Some (inl ()) in
- rwown γs (main_st None) -∗ rwown γs (sub_st None)
- ==∗ rwown γs (main_st st') ∗ rwown γs (sub_st st') ∗ rwown γs writing_st.
+ rwown γs (st_global None) ==∗ rwown γs (st_global st') ∗ rwown γs writing_st.
Proof.
- iIntros (st') "m s".
- rewrite bi.sep_assoc -rwown_st_global_main_sub -embed_sep -own_op pair_op right_id.
- iDestruct (rwown_st_global_main_sub with "[$m $s]") as "ms".
- iMod (own_update (A:=rwlockR) with "ms") as "$"; [|done].
- apply prod_update; simpl; [|by apply rwown_agree_update].
- apply auth_update_alloc.
- rewrite -(right_id None op (Some _)). by apply op_local_update_discrete.
+ iIntros (st') "g". rewrite -embed_sep -own_op.
+ iMod (own_update with "g") as "$"; [|done]. apply auth_update_alloc.
+ rewrite /= -(right_id None op (Some _)). by apply op_local_update_discrete.
Qed.
Lemma rwown_update_write_dealloc γs :
let st : rwlock_st := Some (inl ()) in
- rwown γs (main_st st) -∗ rwown γs (sub_st st) -∗ rwown γs writing_st
- ==∗ rwown γs (main_st None) ∗ rwown γs (sub_st None).
+ rwown γs (st_global st) -∗ rwown γs writing_st ==∗ rwown γs (st_global None).
Proof.
- iIntros (st) "m s w".
- rewrite -rwown_st_global_main_sub.
- iDestruct (rwown_st_global_main_sub with "[$m $s]") as "ms".
- iCombine "ms" "w" as "msw".
- iMod (own_update (A:=rwlockR) with "msw") as "$"; [|done].
- apply prod_update; simpl; [|by apply rwown_agree_update].
- apply auth_update_dealloc.
- rewrite -(right_id None op (Some _)). by apply cancel_local_update_unit, _.
+ iIntros (st) "g w". iCombine "g" "w" as "gw".
+ iMod (own_update with "gw") as "$"; [|done]. apply auth_update_dealloc.
+ rewrite /= -(right_id None op (Some _)). by apply cancel_local_update_unit, _.
Qed.
- Lemma rown_main_reading_st st q ν γs:
- rwown γs (main_st st) -∗ rwown γs (reading_st q ν) -∗
+ Lemma rown_global_reading_st st q ν γs:
+ rwown γs (st_global st) -∗ rwown γs (reading_st q ν) -∗
⌜∃ q' n, st = Some (inr (ν,q',n))⌝.
Proof.
iIntros "m r". iCombine "m" "r" as "mr".
- iDestruct (own_valid with "mr") as %[[INCL VAL]%auth_valid_discrete_2 ?].
+ iDestruct (own_valid with "mr") as %[INCL VAL]%auth_valid_discrete_2.
iPureIntro. destruct st as [[[]|[[]]]|].
- move : INCL =>
/Some_included [Eq|/csum_included [//|[[?[?[??//]]]|[?[?[?[??//]]]]]]].
@@ -192,26 +123,31 @@ Section rwlock_inv.
Definition rwlock_interp
(γs: gname) (α : lft) (tyO: vProp) (tyS: lft → vProp)
: interpC Σ unitProtocol :=
- (λ pb l _ _ vs, ∃ st, ⌜vs = #(Z_of_rwlock_st st)⌝ ∗
+ (λ pb l γ _ vs, ∃ st, ⌜vs = #(Z_of_rwlock_st st)⌝ ∗
if pb
- then match st return _ with
+ then rwown γs (st_global st) ∗
+ match st return _ with
| None => (* Not locked. *)
- rwown γs (sub_st st) ∗ &{α}tyO
+ &{α}tyO ∗
+ GPS_SWSharedWriter l () #0 γ ∗
+ GPS_SWSharedReader l () #0 1%Qp γ
| Some (inr (ν, q, n)) => (* Locked for read. *)
- rwown γs (sub_st st) ∗
∃ q', □ (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
([†ν] ={↑lftN ∪ ↑histN}=∗ &{α}tyO) ∗
- (□ tyS (α ⊓ ν)) ∗ ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]
+ (□ tyS (α ⊓ ν)) ∗ ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν] ∗
+ GPS_SWSharedWriter l () #(Z.pos n) γ ∗
+ GPS_SWSharedReader l () #(Z.pos n) q' γ
| _ => (* Locked for write. *) True
end
else □ (∀ κ q E, ⌜lftE ⊆ E⌝ -∗ &{κ}tyO -∗ q.[κ] ={E}=∗ (□ tyS κ) ∗ q.[κ]))%I.
+ Definition rwlock_noCAS (l: loc) (s : unitProtocol) (v: val) : Prop := v = #(-1).
Definition rwlock_proto_inv l γ γs α tyO tyS : vProp :=
- ((∃ st, rwown γs (main_st st)) ∗ GPS_PPInv (rwlock_interp γs α tyO tyS) l γ)%I.
+ GPS_INV (rwlock_interp γs α tyO tyS) l rwlock_noCAS γ.
Definition rwlock_proto_lc l γ (tyO: vProp) (tyS: lft → vProp) tid ty: vProp :=
((▷ □ (tyO ↔ (l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
(▷ □ (∀ α, tyS α ↔ ty.(ty_shr) α tid (l +ₗ 1))) ∗
- (∃ v, GPS_PPRaw l () v γ))%I.
+ (∃ v, GPS_SWRawReader l () v γ))%I.
Lemma rwlock_interp_comparable γs α tyO tyS l γ s v (n: Z):
rwlock_interp γs α tyO tyS false l γ s v
@@ -291,47 +227,51 @@ Section rwlock_inv.
{ iIntros "!#" (????) "tyO tok". by iMod (ty_share with "LFT tyO tok") as "[#? $]". }
iDestruct "H" as ([|n|[]]) "[>Hn >%]"; try lia.
- iFrame "Htok".
- iMod (own_alloc (st_full None : rwlockR)) as (γs) "Hst". done.
- iDestruct (rwown_full_split with "Hst") as "(lst & mst & sst)".
- iMod (GPS_PPRaw_Init_vs (rwlock_interp γs α tyO tyS) _ true _ ()
- with "Hn [Hvl sst]") as (γ) "[R inv]".
- { iIntros (?). iSplitR ""; iExists None; by [iFrame "Hvl sst"|iFrame "Share"]. }
- iExists γ, γs, tyO, tyS.
- iModIntro. iFrame "inv EqO EqS". iSplitL "R"; by iExists _.
+ iMod (own_alloc (st_global None : rwlockR)) as (γs) "Hst". done.
+ iMod (GPS_SWRaw_Init_vs_strong (rwlock_interp γs α tyO tyS) _ rwlock_noCAS
+ true _ () (GPS_SWRawReader l ((): unitProtocol) #0)%I
+ with "Hn [Hvl Hst]") as (γ) "[inv R]".
+ { iIntros (?) "W". iDestruct (GPS_SWRawWriter_RawReader with "W") as "#$".
+ iSplitR ""; iExists None; [|by iFrame "Share"]. iModIntro. iSplit; [done|].
+ iFrame "Hvl Hst". by iDestruct (GPS_SWRawWriter_shared with "W") as "[$$]". }
+ iExists γ, γs, tyO, tyS. iModIntro. iFrame "inv EqO EqS". by iExists _.
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
- iMod (own_alloc (st_full (Some $ inr (ν, (1/2)%Qp, n)) : rwlockR))
- as (γs) "Hst". done.
- iDestruct (rwown_full_split with "Hst") as "(lst & mst & sst)".
+ iMod (own_alloc (st_global (Some $ inr (ν, (1/2)%Qp, n)))) as (γs) "Hst".
+ { by apply auth_auth_valid. }
iMod (rebor _ _ (α ⊓ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
{ iApply lft_intersect_incl_l. }
iDestruct (lft_intersect_acc with "Htok Htok1") as (q') "[Htok Hclose]".
iMod (ty_share with "LFT Hvl Htok") as "[#Hshr Htok]". done.
iDestruct ("Hclose" with "Htok") as "[$ Htok]".
- iMod (GPS_PPRaw_Init_vs (rwlock_interp γs α tyO tyS) _ true _ ()
- with "Hn [-mst]") as (γ) "[R inv]".
- { iIntros (?).
+ iMod (GPS_SWRaw_Init_vs_strong (rwlock_interp γs α tyO tyS) _ rwlock_noCAS
+ true _ () (GPS_SWRawReader l (() : unitProtocol) #(Z.pos n))%I
+ with "Hn [-]") as (γ) "[inv R]".
+ { iIntros (?) "W". iDestruct (GPS_SWRawWriter_RawReader with "W") as "#$".
iSplitR ""; iExists (Some $ inr (ν, (1/2)%Qp, n)); [|by iFrame "Share"].
- iSplitL ""; [done|]. iFrame "sst".
- iExists _. iFrame "Hshr Htok2 Hhν". iSplitR ""; [|by rewrite Qp_div_2].
+ iModIntro. iSplitL ""; [done|]. iFrame "Hst".
+ iExists _. iFrame "Hshr Htok2 Hhν".
+ iDestruct (GPS_SWRawWriter_shared with "W") as "[$ [$ ?]]".
+ iSplitR ""; [|by rewrite Qp_div_2].
iIntros "!> Hν". iDestruct (lft_tok_dead with "Htok Hν") as "[]". }
- iExists γ, γs, tyO, tyS.
- iModIntro. iFrame "inv EqO EqS". iSplitL "R"; by iExists _.
- - iMod (own_alloc (st_full (Some $ inl ()) : rwlockR)) as (γs) "Hst". done.
+ iExists γ, γs, tyO, tyS. iModIntro. iFrame "inv EqO EqS". by iExists _.
+ - iMod (own_alloc (st_global (Some $ inl ()))) as (γs) "Hst".
+ { by apply auth_auth_valid. }
iFrame "Htok".
- iDestruct (rwown_full_split with "Hst") as "(lst & mst & sst)".
- iMod (GPS_PPRaw_Init_vs (rwlock_interp γs α tyO tyS) _ true _ ()
- with "Hn [Hvl]") as (γ) "[R inv]".
- { iIntros (?). iSplitR ""; iExists (Some $ inl ()); by [|iFrame "Share"]. }
- iExists γ, γs, tyO, tyS.
- iModIntro. iFrame "inv EqO EqS". iSplitL "R"; by iExists _.
+ iMod (GPS_SWRaw_Init_vs_strong (rwlock_interp γs α tyO tyS) _ rwlock_noCAS
+ true _ () (GPS_SWRawWriter l (() : unitProtocol) #(-1))%I
+ with "Hn [Hvl Hst]") as (γ) "[inv W]".
+ { iIntros (?) "$". iModIntro. iSplitR ""; iExists (Some $ inl ());
+ by [iFrame "Hst"|iFrame "Share"]. }
+ iExists γ, γs, tyO, tyS. iModIntro. iFrame "inv EqO EqS". iExists _.
+ by iDestruct (GPS_SWRawWriter_RawReader with "W") as "#$".
Qed.
Lemma rwlock_proto_destroy b l γ γs α tyO tyS :
⎡ hist_inv ⎤ -∗ ▷?b rwlock_proto_inv l γ γs α tyO tyS
={↑histN}=∗ ∃ (z : Z), l ↦ #z ∗ ⌜-1 ≤ z⌝.
Proof.
- iIntros "#hInv [mst inv]".
- iMod (GPS_PPInv_dealloc with "hInv inv") as (s v) "(Hl & F & _)"; [done|].
+ iIntros "#hInv inv".
+ iMod (GPS_INV_dealloc with "hInv inv") as (s v) "(Hl & F & _)"; [done|].
iDestruct "F" as (st) "[>% _]". subst v. iExists _. iFrame "Hl".
iPureIntro. destruct st as [[|[[??]?]]| ]; simpl; try omega. lia.
Qed.
@@ -370,20 +310,6 @@ Section rwlock_inv.
- iIntros (V'' ??). by iFrame.
Qed.
- Lemma rwlock_proto_inv_split l γ γs β tid ty Vb:
- (monPred_in Vb
- → ▷ ((∃ st, rwown γs (main_st st)) ∗ GPS_PPInv (rwlock_interp γs tid β ty) l γ))
- ⊣⊢ ((∃ st, ▷ rwown γs (main_st st))
- ∗ (monPred_in Vb → ▷ GPS_PPInv (rwlock_interp γs tid β ty) l γ)).
- Proof.
- rewrite /rwlock_proto_inv bi.later_sep bi.later_exist monPred_in_sep.
- iSplit; iIntros "[mst $]".
- - rewrite monPred_in_exist. iDestruct "mst" as (st) "mst".
- iExists st. by rewrite -embed_later monPred_in_embed.
- - iDestruct "mst" as (st) "mst". rewrite monPred_in_exist.
- iExists st. by rewrite -embed_later monPred_in_embed.
- Qed.
-
Lemma rwlock_interp_read_acq l s v γ γs α tyO tyS tid:
(▽{tid} rwlock_interp γs α tyO tyS false l γ s v : vProp) -∗
∃ st, ⌜v = #(Z_of_rwlock_st st)⌝.
@@ -459,7 +385,7 @@ Section rwlock.
Global Instance rwlock_type_ne : TypeNonExpansive rwlock.
Proof.
constructor;
- solve_proper_core ltac:(fun _ => exact: type_dist2_S
+ solve_proper_core ltac:(fun _ => exact: type_dist2_S
|| (eapply rwlock_proto_lc_type_ne; try reflexivity)
|| f_type_equiv || f_equiv).
Qed.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 58a03611..a53141f6 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -24,8 +24,9 @@ Section rwlockreadguard.
∃ ν q γs β, ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
α ⊑ β ∗ q.[ν] ∗ rwown γs (reading_st q ν) ∗
(1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
- (∃ γ tyO tyS, rwlock_proto_lc l γ tyO tyS tid ty ∗
- &at{β,rwlockN}(rwlock_proto_inv l γ γs β tyO tyS))
+ (∃ γ tyO tyS, (∃ n, GPS_SWSharedReader l () #(Z.pos n) q γ) ∗
+ rwlock_proto_lc l γ tyO tyS tid ty ∗
+ &at{β,rwlockN}(rwlock_proto_inv l γ γs β tyO tyS))
| _ => False
end;
ty_shr κ tid l :=
@@ -90,8 +91,8 @@ Section rwlockreadguard.
+ iApply ty_shr_mono; last by iApply "Hs".
iApply lft_intersect_mono. done. iApply lft_incl_refl.
+ by iApply lft_incl_trans.
- + iDestruct "Hinv" as (γ tyO tyS) "(lc & inv)".
- iExists γ, tyO, tyS. iFrame "inv". by iApply ("Hty1ty2" with "HE lc").
+ + iDestruct "Hinv" as (γ tyO tyS) "(R & lc & inv)".
+ iExists γ, tyO, tyS. iFrame "R inv". by iApply ("Hty1ty2" with "HE lc").
- iIntros (κ tid l) "H". iDestruct "H" as (l') "[Hf Hshr]". iExists l'.
iFrame. iApply ty_shr_mono; last by iApply "Hs".
iApply lft_intersect_mono. done. iApply lft_incl_refl.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 2100479f..31e66639 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -73,40 +73,43 @@ Section rwlockreadguard_functions.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
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) "((EqO & EqS & PP) & Hinv)".
- iDestruct "PP" as (vP) "PP".
+ iDestruct "Hx'" as (ν q γs β) "(Hx' & #Hαβ & Hν & H◯ & H† & 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.
wp_bind (!ʳˡˣ#lx')%E.
iMod (at_bor_acc with "LFT Hinv Hβ") as (Vb) "[INV Hcloseβ]"; [done..|].
- iDestruct (rwlock_proto_inv_split with "INV") as "[mst INV]".
- iDestruct "mst" as (st1) ">mst".
- iApply (GPS_PPRaw_read with "[$PP $INV]"); [solve_ndisj|by left|..].
+ iDestruct (GPS_SWSharedReader_RawReader with "R") as "#RR".
+ iApply (GPS_SWRawReader_read with "[$RR $INV]"); [solve_ndisj|by left|..].
{ iNext. iIntros (? _). iLeft.
iIntros "!>" (?). by iApply rwlock_interp_duplicable. }
iNext. iIntros ([] v') "(_ & _ & INV & Int)".
iDestruct (rwlock_interp_read_acq with "Int") as (st2) "Int".
iDestruct "Int" as %?. subst v'.
- iMod ("Hcloseβ" with "[mst INV]") as "Hβ".
- { rewrite rwlock_proto_inv_split. iFrame "INV". by iExists _. }
+ iMod ("Hcloseβ" with "INV") as "Hβ".
iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _ _ _ _).
iMod (at_bor_acc with "LFT Hinv Hβ") as (Vb') "[INV Hcloseβ]"; [done..|].
- iDestruct (rwlock_proto_inv_split with "INV") as "[mst INV]".
- iDestruct (bi.later_exist_2 with "mst") as ">mst".
- set Q : () → vProp Σ := (λ _, (∃ st, rwown γs (main_st st)))%I.
- set R : () → lit → vProp Σ := (λ _ _, (∃ st, rwown γs (main_st st)))%I.
- iApply (GPS_PPRaw_CAS_int_simple (rwlock_interp γs β tyO tyS) _ _ _ _ _
- _ #(Z_of_rwlock_st st2 - 1) () True%I Q R _ _ Vb'
- with "[$PP $INV mst H◯ Hx' Hν H†]");
- [solve_ndisj|by left|done|by left|by right|iSplitL ""; last iSplitL ""|..].
+ set P : vProp Σ := (rwown γs (reading_st q ν) ∗ (q).[ν])%I.
+ set Q : () → vProp Σ := (λ _, True)%I.
+ set R : () → lit → vProp Σ := (λ _ _, True)%I.
+ set T : () → () → vProp Σ := (λ _ _, True)%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)
+ with "[$R $INV H◯ Hν]");
+ [done|solve_ndisj|by left|done|by left|by right|iSplitL ""; last iSplitL ""|..].
{ iIntros "!> !>" (???). by iApply rwlock_interp_comparable. }
{ iIntros "!> !>" (???). by iApply rwlock_interp_duplicable. }
- { simpl. iSplitR ""; last done.
- iNext. iIntros ([] _). iSplit; [|by iIntros (?) "_ _"].
- iDestruct "mst" as (st3) "mst". iIntros "_".
- iDestruct 1 as (st2') "[Eqst INT]". iDestruct "Eqst" as %Eqst.
- destruct st2' as [[[]|[[ν' q'] n]]|].
+ { simpl. iSplitR "H◯ Hν"; last iFrame "∗".
+ iNext. iIntros ([] _). iSplit; [|by iIntros (?) "_ _"]. iSplitL "".
+ - iIntros "(H◯ & Hν)". iDestruct 1 as (st2') "[Eqst [g INT]]".
+ iDestruct "Eqst" as %Eqst.
+ iDestruct (rown_global_reading_st with "g H◯") as %[q' [n Eqst2']].
+ subst st2'. iDestruct 1 as (?) "[_ #Share]".
+ iExists (). rewrite Eqst /=. iSplitL ""; [done|].
+ admit.
+ - iIntros ([] _) "T W".
wp_read.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 4094aecb..cee094bd 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -23,9 +23,10 @@ Section rwlockwriteguard.
match vl return _ with
| [ #(LitLoc l) ] =>
∃ γs β, &{β}((l +ₗ 1) ↦∗: ty.(ty_own) tid) ∗
- α ⊑ β ∗ rwown γs writing_st ∗ rwown γs (sub_st (Some (inl ()))) ∗
- (∃ γ tyO tyS, rwlock_proto_lc l γ tyO tyS tid ty ∗
- &at{β,rwlockN}(rwlock_proto_inv l γ γs β tyO tyS))
+ α ⊑ β ∗ rwown γs writing_st ∗
+ (∃ γ tyO tyS, GPS_SWRawWriter l () #(-1) γ ∗
+ rwlock_proto_lc l γ tyO tyS tid ty ∗
+ &at{β,rwlockN}(rwlock_proto_inv l γ γs β tyO tyS))
| _ => False
end;
ty_shr κ tid l :=
@@ -84,14 +85,14 @@ Section rwlockwriteguard.
iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [done|iSplit; iAlways].
- iIntros (tid [|[[]|][]]) "H"; try done.
- iDestruct "H" as (γs β) "(Hb & #H⊑ & Hown & Hsst & Hinv)".
- iExists γs, β. iFrame "Hown Hsst". iSplit; last iSplit.
+ iDestruct "H" as (γs β) "(Hb & #H⊑ & Hown & Hinv)".
+ iExists γs, β. iFrame "Hown". iSplitL "Hb"; last iSplitR "Hinv".
+ iApply bor_iff; last done.
iIntros "!>!#". iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
iExists vl; iFrame; by iApply "Ho".
+ by iApply lft_incl_trans.
- + iDestruct "Hinv" as (γ tyO tyS) "(lc & inv)".
- iExists γ, tyO, tyS. iFrame "inv". by iApply ("Hty1ty2" with "HE lc").
+ + iDestruct "Hinv" as (γ tyO tyS) "(W & lc & inv)".
+ iExists γ, tyO, tyS. iFrame "W inv". by iApply ("Hty1ty2" with "HE lc").
- iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
--
GitLab