diff --git a/_CoqProject b/_CoqProject
index bd1908a6ca9c62e83da7c9d78f77f576df4bacbe..c03b2e2b60c556cb12f90154d5edf63677a55baa 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -63,6 +63,9 @@ theories/typing/lib/refcell/ref_code.v
theories/typing/lib/refcell/refmut_code.v
theories/typing/lib/refcell/refmut.v
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/examples/get_x.v
theories/typing/examples/rebor.v
theories/typing/examples/unbox.v
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 1a46ea0edcf136f05468f7d97e28f1c412d48c7b..1f3d82f33571f3890fef68c3d4b542cc18e537ac 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -41,50 +41,146 @@ 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), ε).
Section rwlock_inv.
Context `{typeG Σ, rwlockG Σ}.
Local Notation vProp := (vProp Σ).
- Definition reading_st (q : frac) (ν : lft) γs : vProp :=
- ⎡ own γs (◯ (rwlock_to_st $ Some $ inr (ν, q, xH)), ε) ⎤%I.
- Definition writing_st γs: vProp :=
- ⎡ own γs (◯ (rwlock_to_st $ Some $ inl ()), ε) ⎤%I.
- Definition main_st st γs: vProp :=
- ⎡ own γs ((● rwlock_to_st st, ● st_agree st) : rwlockR) ⎤%I.
- Definition sub_st (st: rwlock_st) γs : vProp :=
- ⎡ own γs ((ε, ◯ st_agree st) : rwlockR) ⎤%I.
+ (* 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.
+
+ 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 ν).
+ 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 (_: Some (Cinr (to_agree ν, (1/2)%Qp, 1%positive))
+ = Some (Cinr (to_agree ν, (1/2)%Qp, 1%positive)) ⋅ ε);
+ [by apply op_local_update_discrete|by rewrite right_id_L].
+ 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 ν).
+ 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
+ -{2}(agree_idemp (to_agree _)) -frac_op'
+ -2!pair_op -Cinr_op Some_op.
+ rewrite {2}(_: Some (Cinr (to_agree ν, (q' / 2)%Qp, 1%positive))
+ = Some (Cinr (to_agree ν, (q' / 2)%Qp, 1%positive)) ⋅ ε);
+ [|by rewrite right_id_L].
+ apply op_local_update_discrete =>-[Hagv _]. split; [split|done].
+ - by rewrite /= agree_idemp.
+ - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
+ apply Qcplus_le_mono_l. rewrite -{1}(Qcanon.Qcplus_0_l (q'/2)%Qp).
+ apply Qcplus_le_mono_r, Qp_ge_0.
+ Qed.
+
+ (* GPS protocol definitions *)
Definition rwlock_interp
- (γs: gname) (α : lft) (tyOwn: list val → vProp) (tyShr: lft → loc → vProp)
+ (γs: gname) (α : lft) (tyO: vProp) (tyS: lft → vProp)
: interpC Σ unitProtocol :=
(λ pb l _ _ vs, ∃ st, ⌜vs = #(Z_of_rwlock_st st)⌝ ∗
if pb
then match st return _ with
| None => (* Not locked. *)
- sub_st st γs ∗
- &{α}((l +ₗ 1) ↦∗: tyOwn)
+ rwown γs (sub_st st) ∗ &{α}tyO
| Some (inr (ν, q, n)) => (* Locked for read. *)
- sub_st st γs ∗
- ∃ q', □ (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
- ([†ν] ={↑lftN ∪ ↑histN}=∗ &{α}((l +ₗ 1) ↦∗: tyOwn)) ∗
- tyShr (α ⊓ ν) (l +ₗ 1) ∗
- ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]
+ rwown γs (sub_st st) ∗
+ ∃ q', □ (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
+ ([†ν] ={↑lftN ∪ ↑histN}=∗ &{α}tyO) ∗
+ (□ tyS (α ⊓ ν)) ∗ ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]
| _ => (* Locked for write. *) True
end
- else □ (∀ α' l', tyShr α' l' -∗ □ tyShr α' l'))%I.
+ else □ (∀ κ q E, ⌜lftE ⊆ E⌝ -∗ &{κ}tyO -∗ q.[κ] ={E}=∗ (□ tyS κ) ∗ q.[κ]))%I.
- Definition rwlock_proto_inv l γ γs α tyOwn tyShr : vProp :=
- ((∃ st, main_st st γs) ∗ GPS_PPInv (rwlock_interp γs α tyOwn tyShr) l γ)%I.
- Definition rwlock_proto_lc l γ
- (tyOwn: list val → vProp) (tyShr: lft → loc → vProp) tid ty : vProp :=
- ((▷ □ ∀ vl, tyOwn vl ↔ ty.(ty_own) tid vl) ∗
- (▷ □ ∀ α l', tyShr α l' ↔ ty.(ty_shr) α tid l') ∗
- (∃ v, GPS_PPRaw l () v γ))%I.
+ Definition rwlock_proto_inv l γ γs α tyO tyS : vProp :=
+ ((∃ st, rwown γs (main_st st)) ∗ GPS_PPInv (rwlock_interp γs α tyO tyS) l γ)%I.
+ 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.
+
+ Lemma rwlock_interp_comparable γs α tyO tyS l γ s v (n: Z):
+ rwlock_interp γs α tyO tyS false l γ s v
+ -∗ ⌜∃ vl : lit, v = #vl ∧ lit_comparable n vl⌝.
+ Proof.
+ iDestruct 1 as (st) "[% _]". subst v.
+ destruct st as [[|[[??]?]]|]; simpl;
+ iExists _; iPureIntro ;(split; [done|by constructor]).
+ Qed.
+
+ Lemma rwlock_interp_duplicable γs α tyO tyS l γ s v:
+ rwlock_interp γs α tyO tyS false l γ s v
+ -∗ rwlock_interp γs α tyO tyS false l γ s v ∗
+ rwlock_interp γs α tyO tyS false l γ s v.
+ Proof. by iIntros "#$". Qed.
Global Instance rwlock_proto_lc_persistent:
Persistent (rwlock_proto_lc l γ tyO tyS tid ty) := _.
@@ -95,8 +191,9 @@ Section rwlock_inv.
move => ???.
apply bi.sep_ne; [|apply bi.sep_ne]; [..|done];
apply bi.later_contractive; (destruct n; [done|]);
- apply bi.intuitionistically_ne; apply bi.forall_ne => ?.
- - apply bi.iff_ne; [done|]. by apply ty_own_type_dist.
+ apply bi.intuitionistically_ne.
+ - apply bi.iff_ne; [done|]. apply bi.exist_ne => ?.
+ apply bi.sep_ne; [done|by apply ty_own_type_dist].
- apply bi.forall_ne => ?.
apply bi.iff_ne; [done|apply ty_shr_type_dist]; [by apply type_dist2_S|done..].
Qed.
@@ -118,112 +215,73 @@ Section rwlock_inv.
iDestruct (Hty with "HL") as "#Hty". iIntros "* !# #HE H".
iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
iDestruct "H" as "(#EqO & #EqS & $)". iSplit; iIntros "!> !#".
- - iIntros (vl). iSplit; iIntros "H1".
- + iApply "Hown". by iApply "EqO".
- + iApply "EqO". by iApply "Hown".
- - iIntros (??). iSplit; iIntros "?".
+ - iSplit; iIntros "H1".
+ + iDestruct ("EqO" with "H1") as (?) "[? ?]".
+ iExists _. iFrame. by iApply "Hown".
+ + iDestruct "H1" as (?) "[? ?]". iApply "EqO".
+ iExists _. iFrame. by iApply "Hown".
+ - iIntros (?). iSplit; iIntros "?".
+ iApply "Hshr". by iApply "EqS".
+ iApply "EqS". by iApply "Hshr".
Qed.
- Lemma rwlock_main_sub_agree st1 st2 γs :
- main_st st1 γs -∗ sub_st st2 γs -∗ ⌜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 rwlock_main_sub_st st γs :
- ⎡ own γs ((● rwlock_to_st st, ● st_agree st ⋅ ◯ st_agree st) : rwlockR) ⎤
- ⊣⊢ main_st st γs ∗ sub_st st γs.
- Proof.
- by rewrite /main_st /sub_st -embed_sep -own_op pair_op right_id.
- Qed.
-
- Lemma rwlock_own_st st γs :
- ⎡ own γs (st_full st : rwlockR) ⎤
- ⊣⊢ ⎡ own γs (st_local st) ⎤%I ∗ main_st st γs ∗ sub_st st γs.
- Proof.
- by rewrite -rwlock_main_sub_st -embed_sep -own_op pair_op left_id.
- Qed.
-
- Lemma rwlock_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.
-
Lemma rwlock_proto_create l q tid α ty E (SUB: lftE ⊆ E):
⎡ lft_ctx ⎤ -∗
(q / 2).[α] -∗
&{α} ((l +ₗ 1) ↦∗{1}: ty_own ty tid)%I -∗
▷ (∃ n : Z, l ↦{1} #n ∗ ⌜-1 ≤ n⌝) ={E}=∗
(q / 2).[α] ∗ (∃ γ γs tyO tyS, rwlock_proto_lc l γ tyO tyS tid ty
- ∗ ▷ rwlock_proto_inv l γ γs α tyO tyS).
+ ∗ ▷ rwlock_proto_inv l γ γs α tyO tyS).
Proof.
iIntros "#LFT Htok Hvl H".
- set tyOwn := (ty.(ty_own) tid).
- set tyShr := (λ α l', ty.(ty_shr) α tid l').
- iAssert (□ (∀ vl, tyOwn vl ↔ ty_own ty tid vl))%I as "#EqO".
- { iIntros "!#" (?); iSplit; by iIntros "?". }
- iAssert (□ (∀ α' l', tyShr α' l' ↔ ty_shr ty α' tid l'))%I as "#EqS".
- { iIntros "!#" (??); iSplit; by iIntros "?". }
- iAssert (□ (∀ (α' : lft) (l' : loc), tyShr α' l' -∗ □ tyShr α' l'))%I as "#PerS".
- { iIntros "!#" (α' l') "tS". iDestruct ("EqS" with "tS") as "#$". }
+ set tyO : vProp := ((l +ₗ 1) ↦∗{1}: ty.(ty_own) tid)%I.
+ set tyS : lft → vProp := (λ α', ty.(ty_shr) α' tid (l +ₗ 1))%I.
+ iAssert (□ (tyO ↔ (l +ₗ 1) ↦∗{1}: ty.(ty_own) tid))%I as "#EqO".
+ { iIntros "!#". by iApply (bi.iff_refl True%I). }
+ iAssert (□ (∀ α', tyS α' ↔ ty.(ty_shr) α' tid (l +ₗ 1)))%I as "#EqS".
+ { iIntros "!#" (?). by iApply (bi.iff_refl True%I). }
+ iAssert (□ (∀ κ q' E', ⌜lftE ⊆ E'⌝ -∗ &{κ} tyO -∗
+ (q').[κ] ={E'}=∗ (□ tyS κ) ∗ (q').[κ]))%I as "#Share".
+ { 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 (rwlock_own_st with "Hst") as "(lst & mst & sst)".
- iMod (GPS_PPRaw_Init_vs (rwlock_interp γs α tyOwn tyShr) _ true _ ()
+ 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 (?). rewrite /rwlock_interp /=.
- iSplitR ""; iExists None; [by iFrame "Hvl sst"|by iFrame "PerS"]. }
- iExists γ, γs, tyOwn, tyShr. iModIntro. iFrame "inv".
- iSplitL "R"; [|by iExists _].
- iSplitL ""; [done|]. iSplitL ""; [done|]. by iExists _.
+ { iIntros (?). iSplitR ""; iExists None; by [iFrame "Hvl sst"|iFrame "Share"]. }
+ iExists γ, γs, tyO, tyS.
+ iModIntro. iFrame "inv EqO EqS". iSplitL "R"; 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 (rwlock_own_st with "Hst") as "(lst & mst & sst)".
+ iDestruct (rwown_full_split with "Hst") as "(lst & mst & sst)".
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.
+ 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 α tyOwn tyShr) _ true _ ()
+ iMod (GPS_PPRaw_Init_vs (rwlock_interp γs α tyO tyS) _ true _ ()
with "Hn [-mst]") as (γ) "[R inv]".
- { iIntros (?). rewrite /rwlock_interp /=.
- iSplitR ""; iExists (Some $ inr (ν, (1/2)%Qp, n)); [|by iFrame "PerS"].
+ { iIntros (?).
+ 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].
iIntros "!> Hν". iDestruct (lft_tok_dead with "Htok Hν") as "[]". }
- iExists γ, γs, tyOwn, tyShr. iModIntro. iFrame "inv".
- iSplitL "R"; [|by iExists _].
- iSplitL ""; [done|]. iSplitL ""; [done|]. by iExists _.
+ 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.
iFrame "Htok".
- iDestruct (rwlock_own_st with "Hst") as "(lst & mst & sst)".
- iMod (GPS_PPRaw_Init_vs (rwlock_interp γs α tyOwn tyShr) _ true _ ()
+ 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 (?). rewrite /rwlock_interp /=.
- iSplitR ""; iExists (Some $ inl ()); [done|by iFrame "PerS"]. }
- iExists γ, γs, tyOwn, tyShr. iFrame "inv".
- iSplitL "R"; [|by iExists _].
- iSplitL ""; [done|]. iSplitL ""; [done|]. by iExists _.
+ { iIntros (?). iSplitR ""; iExists (Some $ inl ()); by [|iFrame "Share"]. }
+ iExists γ, γs, tyO, tyS.
+ iModIntro. iFrame "inv EqO EqS". iSplitL "R"; by iExists _.
Qed.
- Lemma rwlock_proto_destroy b l γ γs α tyOwn tyShr :
- ⎡ hist_inv ⎤ -∗ ▷?b rwlock_proto_inv l γ γs α tyOwn tyShr
+ 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]".
@@ -232,21 +290,7 @@ Section rwlock_inv.
iPureIntro. destruct st as [[|[[??]?]]| ]; simpl; try omega. lia.
Qed.
- Lemma rwlock_interp_comparable γs α tyO tyS l γ s v (n: Z):
- rwlock_interp γs α tyO tyS false l γ s v
- -∗ ⌜∃ vl : lit, v = #vl ∧ lit_comparable n vl⌝.
- Proof.
- iDestruct 1 as (st) "[% _]". subst v.
- destruct st as [[|[[??]?]]|]; simpl;
- iExists _; iPureIntro ;(split; [done|by constructor]).
- Qed.
-
- Lemma rwlock_interp_duplicable γs α tyO tyS l γ s v:
- rwlock_interp γs α tyO tyS false l γ s v
- -∗ rwlock_interp γs α tyO tyS false l γ s v ∗
- rwlock_interp γs α tyO tyS false l γ s v.
- Proof. by iIntros "#$". Qed.
-
+ (* Lemmas to deal with views *)
(* TODO: move elsewhere *)
Lemma monPred_in_sep (P Q : vProp) V :
(monPred_in V → P ∗ Q) ⊣⊢ (monPred_in V → P) ∗ (monPred_in V → Q).
@@ -280,11 +324,11 @@ Section rwlock_inv.
- iIntros (V'' ??). by iFrame.
Qed.
- Lemma rwlock_proto_inv_split l γ γs β tyO tyS Vb:
+ Lemma rwlock_proto_inv_split l γ γs β tid ty Vb:
(monPred_in Vb
- → ▷ ((∃ st, main_st st γs) ∗ GPS_PPInv (rwlock_interp γs β tyO tyS) l γ))
- ⊣⊢ ((∃ st, ▷ main_st st γs)
- ∗ (monPred_in Vb → ▷ GPS_PPInv (rwlock_interp γs β tyO tyS) l γ)).
+ → ▷ ((∃ 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 $]".
@@ -294,8 +338,8 @@ Section rwlock_inv.
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) -∗
+ 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)⌝.
Proof.
iIntros "Int". iDestruct (acq_exist with "Int") as (?) "Int".
@@ -325,8 +369,8 @@ Section rwlock.
end)%I;
ty_shr κ tid l :=
(∃ α, κ ⊑ α
- ∗ ∃ γ γs tyOwn tyShr, rwlock_proto_lc l γ tyOwn tyShr tid ty
- ∗ &at{α,rwlockN}(rwlock_proto_inv l γ γs α tyOwn tyShr))%I |}.
+ ∗ ∃ γ γs tyO tyS, rwlock_proto_lc l γ tyO tyS tid ty
+ ∗ &at{α,rwlockN}(rwlock_proto_inv l γ γs α tyO tyS))%I |}.
Next Obligation.
iIntros (??[|[[]|]]); try iIntros "[? []]". rewrite ty_size_eq.
iIntros "[_ [_ %]] !% /=". congruence.
@@ -419,13 +463,16 @@ Section rwlock.
do 4 apply bi.exist_mono=>?.
apply bi.sep_mono_l, bi.sep_mono; last apply bi.sep_mono_l;
apply bi.later_mono; iIntros "#H !#".
- - iIntros (vl). iSpecialize ("H" $! vl). iSplit; iIntros "?".
- + iApply send_change_tid. by iApply "H".
- + iApply "H". by iApply send_change_tid.
- - iIntros (α l'). iSpecialize ("H" $! α l'). iSplit; iIntros "?".
+ - iSplit; iIntros "H1".
+ + iDestruct ("H" with "H1") as (?) "[??]".
+ iExists _. iFrame. by iApply send_change_tid.
+ + iApply "H". iDestruct "H1" as (?) "[??]".
+ iExists _. iFrame. by iApply send_change_tid.
+ - iIntros (α). iSpecialize ("H" $! α). iSplit; iIntros "H1".
+ iApply sync_change_tid. by iApply "H".
+ iApply "H". by iApply sync_change_tid.
Qed.
+
End rwlock.
Hint Resolve rwlock_mono' rwlock_proper' : lrust_typing.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 818053d763882ffc954ce7ff690442294e933cbc..2eb37366fdbb39aaf406c566afd61e965064b1f0 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -132,7 +132,7 @@ Section rwlock_functions.
"r" <-{Σ none} ();;
"k" []
else
- if: CAS "x'" "n" ("n" + #1) AcqRel Relaxed then
+ if: CAS "x'" "n" ("n" + #1) Relaxed AcqRel Relaxed then
"r" <-{Σ some} "x'";;
"k" []
else "loop" []
@@ -173,8 +173,9 @@ Section rwlock_functions.
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|..].
- { iNext. iIntros (? _). iLeft. iIntros "!>" (?). by iApply rwlock_interp_duplicable. }
- iNext. iIntros ([] v') "(_ & R' & INV & Int)".
+ { 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βtok1".
@@ -189,23 +190,24 @@ Section rwlock_functions.
iApply (type_sum_unit (option $ rwlockreadguard α ty));
[solve_typing..|]; first last.
simpl. iApply type_jump; solve_typing.
- - wp_op. wp_bind (CAS _ _ _ _ _).
+ - wp_op. wp_bind (CAS _ _ _ _ _ _).
iMod (at_bor_acc with "LFT Hinv Hβtok1") as (Vb') "[INV Hclose'']"; [done..|].
iDestruct (rwlock_proto_inv_split with "INV") as "[mst INV]".
iDestruct "mst" as (st3) ">mst".
set Q : () → vProp Σ :=
- (λ _, (∃ st, ▷ main_st st γs) ∗
+ (λ _, (∃ st, ▷ rwown γs (main_st st)) ∗
(qβ / 2).[β] ∗
(∃ qν ν, (qν).[ν] ∗
- tyS (β ⊓ ν) (lx +ₗ 1) ∗
- reading_st qν ν γs ∗
+ tyS (β ⊓ ν) ∗
+ rwown γs (reading_st qν ν) ∗
((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν])))%I.
- set R : () → lit → vProp Σ := (λ _ _, (∃ st, ▷ main_st st γs) ∗ (qβ / 2).[β])%I.
+ set R : () → lit → vProp Σ :=
+ (λ _ _, (∃ st, ▷ rwown γs (main_st st)) ∗ (qβ / 2).[β])%I.
iMod (rel_True_intro True%I tid with "[//]") as "rTrue".
- iApply (GPS_PPRaw_CAS_simple (rwlock_interp γs β tyO tyS) _ _ _ _
+ iApply (GPS_PPRaw_CAS_int_simple (rwlock_interp γs β tyO tyS) _ _ _ _ _
(Z_of_rwlock_st st2) #(Z_of_rwlock_st st2 + 1) () Q R _ _ Vb'
- with "[$PP $INV mst Hβtok2 rTrue]"); [solve_ndisj|by right|by left|..];
- [iSplitL ""; last iSplitL ""|].
+ with "[$PP $INV mst Hβtok2 rTrue]");
+ [solve_ndisj|by left|done|by right|by left|iSplitL ""; last iSplitL ""|..].
{ iIntros "!> !>" (???). by iApply rwlock_interp_comparable. }
{ iIntros "!> !>" (???). by iApply rwlock_interp_duplicable. }
{ simpl. iNext. rewrite /= -(bi.True_sep' (∀ _ : (), _)%I).
@@ -216,85 +218,69 @@ Section rwlock_functions.
destruct st2' as [[[]|[[ν q] n]]|].
- exfalso. clear -Eqst Hm1. simpl in Eqst. inversion Eqst as [Eq1].
rewrite Eq1 in Hm1. omega.
- - iDestruct "INT" as "[sub INT]".
- iDestruct (rwlock_main_sub_agree with "mst sub") as %Eqst2. subst st3.
- iDestruct 1 as (?) "[_ #PerS]".
- iDestruct "INT" as (q') "(#H† & Hh & Hshr' & Hqq' & [Hν1 Hν2])".
- iDestruct "Hqq'" as %Hqq'.
- iDestruct ("PerS" with "Hshr'") as "#Hshr". iClear "Hshr'".
- iExists (). iSplitL ""; [done|].
- iDestruct (rwlock_main_sub_st with "[$mst $sub]") as "ms".
- set st': rwlock_st := Some (inr (ν, (q + (q'/2)%Qp)%Qp, (n + 1)%positive)).
- iMod (own_update _ _
- ((● rwlock_to_st st' ⋅ ◯ (rwlock_to_st $ Some $ inr (ν, (q' / 2)%Qp, 1%positive)),
- ● st_agree st' ⋅ ◯ st_agree st') : rwlockR) with "ms") as "ms'".
- { apply prod_update; simpl; [|by apply rwlock_agree_update].
- 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}(_: Some (Cinr (to_agree ν, (q' / 2)%Qp, 1%positive))
- = Some (Cinr (to_agree ν, (q' / 2)%Qp, 1%positive)) ⋅ ε);
- [|by rewrite right_id_L].
- apply op_local_update_discrete =>-[Hagv _]. split; [split|done].
- - by rewrite /= agree_idemp.
- - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
- apply Qcplus_le_mono_l. rewrite -{1}(Qcanon.Qcplus_0_l (q'/2)%Qp).
- apply Qcplus_le_mono_r, Qp_ge_0. }
- iAssert (main_st st' γs ∗ sub_st st' γs ∗ reading_st (q' / 2)%Qp ν γs)%I
- with "[ms']" as "(mst' & sst' & rst)".
- { rewrite /main_st /sub_st /reading_st.
- by rewrite -2!embed_sep -2!own_op pair_op /= left_id right_id. }
+ - iDestruct "INT" as "[sst INT]".
+ iDestruct (rwown_main_sub_agree with "mst sst") as %Eqst2. subst st3.
+ iDestruct 1 as (?) "[_ #Share]".
+ iDestruct "INT" as (q') "(#H† & Hh & #Hshr & Hqq' & [Hν1 Hν2])".
+ iDestruct "Hqq'" as %Hqq'. iExists (). iSplitL ""; [done|].
+ iMod (rwown_update_read ν n q q' γs Hqq' with "mst sst") as "(mst'&sst'&rst)".
have Eq: Z_of_rwlock_st st2 + 1 = Z.pos (n + 1).
{ clear -Eqst. inversion Eqst as [Eq]. by rewrite Eq. }
iModIntro. iFrame "Hβtok2".
+ set st' : rwlock_st := (Some (inr (ν, (q + q' / 2)%Qp, (n + 1)%positive))).
iSplitL "mst' rst Hν2"; [iSplitL "mst'"; [by iExists _|]|iSplitR ""].
+ iExists _, _. by iFrame "∗#".
+ iExists st'. simpl. iFrame "sst'". iSplitL ""; [by rewrite Eq|].
- iExists (q' / 2)%Qp. iFrame "∗#". iPureIntro. by rewrite -Qp_plus_assoc Qp_div_2.
- + iExists st'. iFrame "PerS". by rewrite Eq.
- - iDestruct "INT" as "[sub Hst]".
- iDestruct (rwlock_main_sub_agree with "mst sub") as %Eqst2. subst st3.
- iDestruct 1 as (?) "[_ #PerS]".
- iExists (). iSplitL ""; [done|].
- iDestruct (rwlock_main_sub_st with "[$mst $sub]") as "ms".
+ iExists (q'/2)%Qp. iFrame "∗ H† Hshr".
+ iPureIntro. by rewrite -Qp_plus_assoc Qp_div_2.
+ + iExists st'. iFrame "Share". by rewrite Eq.
+ - iDestruct "INT" as "[sst Hst]".
+ iDestruct (rwown_main_sub_agree with "mst sst") as %Eqst2. subst st3.
+ iDestruct 1 as (?) "[_ #Share]". iExists (). iSplitL ""; [done|].
iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". solve_ndisj.
set st': rwlock_st := Some (inr (ν, (1/2)%Qp, 1%positive)).
- iMod (own_update _ _
- ((● rwlock_to_st st' ⋅ ◯ (rwlock_to_st $ Some $ inr (ν, (1/2)%Qp, 1%positive)),
- ● st_agree st' ⋅ ◯ st_agree st') : rwlockR) with "ms") as "ms'".
- { apply prod_update; simpl; [|by apply rwlock_agree_update].
- apply auth_update_alloc.
- rewrite (_: Some (Cinr (to_agree ν, (1/2)%Qp, 1%positive))
- = Some (Cinr (to_agree ν, (1/2)%Qp, 1%positive)) ⋅ ε);
- [by apply op_local_update_discrete|by rewrite right_id_L]. }
- iAssert (main_st st' γs ∗ sub_st st' γs ∗ reading_st (1/2)%Qp ν γs)%I
- with "[ms']" as "(mst' & sst' & rst)".
- { rewrite /main_st /sub_st /reading_st.
- by rewrite -2!embed_sep -2!own_op pair_op /= left_id right_id. }
+ iMod (rwown_update_write_read ν γs with "mst sst") as "(mst'&sst'& rst)".
iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
- iApply (fupd_mask_mono (↑lftN)). solve_ndisj.
- iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hst") as "[Hst Hh]". solve_ndisj.
- { iApply lft_intersect_incl_l. }
- iMod (ty_share with "LFT Hst Htok") as "[Hshr Htok]". solve_ndisj.
- iFrame "#". iDestruct ("Hclose" with "Htok") as "[$ Htok2]".
- iExists _. iFrame. iExists _, _. iSplitR; first done. iFrame "#∗".
- rewrite Qp_div_2. iSplitL; last done.
- iIntros "!> Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
+ iApply (fupd_mask_mono (↑lftN ∪ ↑histN)). apply union_subseteq; split; solve_ndisj.
+ iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hst") as "[Hst Hh]";
+ [apply union_subseteq_l|iApply lft_intersect_incl_l|].
+ iMod ("Share" with "[%] Hst Htok") as "[#Hshr Htok]". apply union_subseteq_l.
+ iDestruct ("Hclose" with "Htok") as "[$ Htok2]".
+ iModIntro. iSplitL "mst' rst Htok2".
+ { iSplitL "mst'"; [by iExists _|]. iExists _,_. by iFrame "Htok2 Hshr rst Hhν". }
+ rewrite (_: Z_of_rwlock_st st2 + 1 = 1); last first.
+ { clear -Eqst. inversion Eqst as [Eq]. by rewrite Eq. }
+ iSplitR ""; iExists st'; [|by iFrame "Share"]. iSplitL ""; [done|].
+ simpl. iFrame "sst'". iExists _. iFrame "Hhν Htok1 Hshr".
+ rewrite Qp_div_2. iSplitL; last done.
+ iIntros "Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
- iMod ("Hclose''" with "[$INV]") as "Hβtok1". iModIntro. wp_case.
+ iNext. simpl.
+ iIntros (b v' [])
+ "(INV & _ &[([%%] & _ & mst & Hβtok2 & Hβ) | ([% Neq] & PP' & R)])".
+ + subst b v'. iDestruct "Hβ" as (q' ν) "(Hν & Hshr & Hreading & H†)".
+ iMod ("Hclose''" with "[mst INV]") as "Hβtok1".
+ { iIntros "Vb'". iSpecialize ("INV" with "Vb'"). iFrame "INV".
+ iDestruct "mst" as (?) "?". by iExists _. }
+ iModIntro. wp_case.
iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iApply (type_type _ _ _
[ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2);
#lx ◁ rwlockreadguard α ty]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
- tctx_hasty_val' //. iFrame.
- iExists _, _, _, _. iFrame "∗#". iApply ty_shr_mono; last done.
- iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
+ tctx_hasty_val' //. iFrame "Hx Hr".
+ iExists _, _, _, _. iFrame "Hν Hreading H† Hαβ".
+ iDestruct ("EqS" with "Hshr") as "Hshr".
+ iSplitL "Hshr".
+ - iApply ty_shr_mono; last done.
+ iApply lft_intersect_mono; first done. iApply lft_incl_refl.
+ - iExists _,_,_. iFrame "EqO EqS Hinv". by iExists _. }
iApply (type_sum_assign (option $ rwlockreadguard α ty)); [solve_typing..|].
simpl. iApply type_jump; solve_typing.
- + iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
+ + subst b.
+ iDestruct (acq_sep_elim with "R") as "[mst Hβtok2]".
+ iDestruct (acq_embed_elim with "Hβtok2") as "Hβtok2".
iMod ("Hclose''" with "[Hlx Hownst Hst]") as "Hβtok1"; first by iExists _; iFrame.
iModIntro. wp_case. iMod ("Hclose'" with "[$]") as "Hα".
iMod ("Hclose" with "Hα HL") as "HL".
@@ -310,7 +296,7 @@ Section rwlock_functions.
withcont: "k":
let: "r" := new [ #2 ] in
let: "x'" := !"x" in
- if: CAS "x'" #0 #(-1) then
+ if: CAS "x'" #0 #(-1) Relaxed AcqRel Relaxed then
"r" <-{Σ some} "x'";;
"k" ["r"]
else
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 426edb8baf76f64fc86aaf4e233b6d4e9641b020..58a03611b88075ea6e8f70080c9cdf6318bd84c8 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -22,8 +22,8 @@ Section rwlockreadguard.
match vl return _ with
| [ #(LitLoc l) ] =>
∃ ν q γs β, ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
- α ⊑ β ∗ q.[ν] ∗ reading_st q ν γs ∗
- (1.[ν] ={↑lftN,∅}▷=∗ [†ν]) ∗
+ α ⊑ β ∗ 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))
| _ => False
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 85b30d53caece0580f575adcd571c36279ee1251..ad3d3ff839ea5f2ab39151fb81240a2723d15ea3 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -23,7 +23,7 @@ Section rwlockwriteguard.
match vl return _ with
| [ #(LitLoc l) ] =>
∃ γs β, &{β}((l +ₗ 1) ↦∗: ty.(ty_own) tid) ∗
- α ⊑ β ∗ writing_st γs ∗
+ α ⊑ β ∗ rwown γs writing_st ∗
(∃ γ tyO tyS, rwlock_proto_lc l γ tyO tyS tid ty ∗
&at{β,rwlockN}(rwlock_proto_inv l γ γs β tyO tyS))
| _ => False