Skip to content
Snippets Groups Projects
Commit de90bc2d authored by Hai Dang's avatar Hai Dang
Browse files

rwlock typing

parent 371c8990
Branches
Tags
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
_CoqProject
+ 3
− 2
View file @ de90bc2d
......@@ -53,16 +53,17 @@ theories/typing/lib/swap.v
theories/typing/lib/take_mut.v
theories/typing/lib/spawn.v
theories/typing/lib/join.v
theories/typing/lib/rc/rc.v
theories/typing/lib/rc/weak.v
theories/typing/lib/mutex/mutex.v
theories/typing/lib/mutex/mutexguard.v
theories/typing/lib/rc/rc.v
theories/typing/lib/rc/weak.v
theories/typing/lib/refcell/refcell_code.v
theories/typing/lib/refcell/refcell.v
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/examples/get_x.v
theories/typing/examples/rebor.v
theories/typing/examples/unbox.v
......
theories/typing/lib/rwlock/rwlock.v
+ 144
− 99
View file @ de90bc2d
......@@ -11,10 +11,9 @@ Definition rwlock_stR :=
Class rwlockG Σ := RwLockG {
rwlock_stateG :> inG Σ (authR rwlock_stR);
rwlock_gpsG :> gpsG Σ unitProtocol;
rwlock_gpsExAgG :> gpsExAgG Σ;
}.
Definition rwlockΣ : gFunctors :=
#[GFunctor (authR rwlock_stR);gpsΣ unitProtocol; GFunctor (agreeR (leibnizC Qp))].
#[GFunctor (authR rwlock_stR); gpsΣ unitProtocol].
Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
Proof. solve_inG. Qed.
......@@ -30,58 +29,110 @@ Definition reading_st (q : frac) (ν : lft) : rwlock_stR :=
Definition writing_st : rwlock_stR :=
Some (Cinl (Excl ())).
Lemma rwlock_st_positive (st : rwlock_stR) :
0 < Z_of_rwlock_st st
→ ∃ v (q: frac) (n: positive), st = Some (Cinr (v, q, n)).
Proof.
destruct st as [[|[[v q] n] |]| ]; simpl; [omega| |omega..].
move => ?. by do 3 eexists.
Qed.
Definition rwlockN := lrustN .@ "rwlock".
Section rwlock_inv.
Context `{typeG Σ, rwlockG Σ}.
Local Notation vProp := (vProp Σ).
Definition rwlock_interp (γs: gname) tid (α : lft) ty
(* Rown: list val → vProp) ty.(ty_own) tid *)
Definition rwlock_interp
(γs: gname) (α : lft) (tyOwn: list val → vProp) (tyShr: lft → loc → 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 (⎡ own γs (● st) ⎤ ∗
match st return _ with
| None => (* Not locked. *)
⎡ own γs (● st) ⎤ ∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)
&{α}((l +ₗ 1) ↦∗: tyOwn) ∗
GPS_SWSharedWriter l () vs γ ∗
GPS_SWSharedReader l () vs 1%Qp γ
| Some (Cinr (agν, q, n)) => (* Locked for read. *)
⎡ own γs (● st) ⎤ ∗
∃ (ν : lft) q', agν ≡ to_agree ν ∗
□ (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
([†ν] ={↑lftN ∪ ↑histN}=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]
([†ν] ={↑lftN ∪ ↑histN}=∗ &{α}((l +ₗ 1) ↦∗: tyOwn)) ∗
tyShr (α ⊓ ν) (l +ₗ 1) ∗
⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν] ∗
GPS_SWSharedWriter l () vs γ ∗ GPS_SWSharedReader l () vs q' γ
| _ => (* Locked for write. *) True
end)
else True)%I.
Definition rwlock_proto_inv l (γ γs: gname) tid α ty : vProp :=
(GPS_PPInv (rwlock_interp γs tid α ty) l γ)%I.
Definition rwlock_proto_lc l (γ: gname) : vProp :=
(∃ v, GPS_PPRaw l () v γ)%I.
Definition rwlock_proto_inv l γ γs α tyOwn tyShr : vProp :=
(GPS_INV (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_SWRawReader l () v γ))%I.
Global Instance rwlock_proto_lc_persistent:
Persistent (rwlock_proto_lc l γ tyO tyS tid ty) := _.
Global Instance rwlock_proto_lc_type_ne n l γ tyO tyS tid :
Proper (type_dist2 n ==> dist n) (rwlock_proto_lc l γ tyO tyS tid).
Proof.
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.forall_ne => ?.
apply bi.iff_ne; [done|apply ty_shr_type_dist]; [by apply type_dist2_S|done..].
Qed.
Global Instance rwlock_proto_lc_ne l γ tyO tyS tid :
NonExpansive (rwlock_proto_lc l γ tyO tyS tid).
Proof.
intros n ???. eapply rwlock_proto_lc_type_ne, type_dist_dist2. done.
Qed.
Lemma rwlock_proto_lc_proper E L ty1 ty2 q :
eqtype E L ty1 ty2 →
llctx_interp L q -∗ ∀ l γ tyO tyS tid, □ (elctx_interp E -∗
rwlock_proto_lc l γ tyO tyS tid ty1 -∗ rwlock_proto_lc l γ tyO tyS tid ty2).
Proof.
(* TODO : this proof is essentially [solve_proper], but within the logic.
It would easily gain from some automation. *)
rewrite eqtype_unfold. iIntros (Hty) "HL".
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 "?".
+ iApply "Hshr". by iApply "EqS".
+ iApply "EqS". by iApply "Hshr".
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, rwlock_proto_lc l γ ∗ ▷ rwlock_proto_inv l γ γs tid α ty).
(q / 2).[α] ∗
(∃ γ γs tyO tyS, rwlock_proto_lc l γ tyO tyS tid ty
∗ ▷ 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 "?". }
iDestruct "H" as ([|n|[]]) "[>Hn >%]"; try lia.
- iFrame. iMod (own_alloc (● None)) as (γs) "Hst". done.
iMod (GPS_PPRaw_Init_vs (rwlock_interp γs tid α ty) _ true _ ()
with "Hn [Hvl Hst]") as (γ) "[lc inv]".
{ iIntros (?). rewrite /rwlock_interp /=.
iSplitR ""; iExists None; [|done]. iSplit; [done|]. iFrame. }
iExists γ, γs. iFrame. by iExists _.
iMod (GPS_SWRaw_Init_vs_strong (rwlock_interp γs α tyOwn tyShr) _ true
_ () (GPS_SWRawReader l ((): unitProtocol) #0)%I
with "Hn [Hvl Hst]") as (γ) "[inv R]".
{ iIntros (?) "W". rewrite /rwlock_interp /=.
iDestruct (GPS_SWRawWriter_RawReader with "W") as "#$".
iSplitR ""; iExists None; [|done]. iModIntro. iSplit; [done|].
iFrame "Hvl Hst". by iDestruct (GPS_SWRawWriter_shared with "W") as "[$ $]". }
iExists γ, γs, tyOwn, tyShr. iFrame "inv".
iSplitL ""; [done|]. iSplitL ""; [done|]. by iExists _.
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
iMod (own_alloc (● Some (Cinr (to_agree ν, (1/2)%Qp, n)))) as (γs) "Hst".
{ by apply auth_auth_valid. }
......@@ -90,71 +141,58 @@ Section rwlock_inv.
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 tid α ty) _ true _ ()
with "Hn [-]") as (γ) "[lc inv]".
{ iIntros (?). rewrite /rwlock_interp /=.
iMod (GPS_SWRaw_Init_vs_strong (rwlock_interp γs α tyOwn tyShr) _ true
_ () (GPS_SWRawReader l ((): unitProtocol) #(Z.pos n))%I
with "Hn [-]") as (γ) "[inv R]".
{ iIntros (?) "W". rewrite /rwlock_interp /=.
iDestruct (GPS_SWRawWriter_RawReader with "W") as "#$".
iSplitR ""; iExists (Some (Cinr (to_agree ν, (1/2)%Qp, n))); [|done].
iSplit; [done|]. iFrame "Hst".
iModIntro. iNext. iSplit; [done|]. iFrame "Hst".
iExists _, _. iIntros "{$Hshr}".
iSplitR; first by auto. iFrame "Htok2 Hhν".
rewrite Qp_div_2. iSplitL; last by auto.
iIntros "!> Hν". iDestruct (lft_tok_dead with "Htok Hν") as "[]". }
iExists γ, γs. iFrame. by iExists _.
iDestruct (GPS_SWRawWriter_shared with "W") as "[$ R]".
rewrite Qp_div_2. iSplitR "R"; last (iSplit; first by auto).
- iIntros "Hν". iDestruct (lft_tok_dead with "Htok Hν") as "[]".
- rewrite -{2}(Qp_div_2 1). iDestruct "R" as "[$ ?]". }
iExists γ, γs, tyOwn, tyShr. iModIntro. iFrame "inv".
iSplitL ""; [done|]. iSplitL ""; [done|]. by iExists _.
- iMod (own_alloc (● writing_st)) as (γs) "Hst". { by apply auth_auth_valid. }
iFrame "Htok".
iMod (GPS_PPRaw_Init_vs (rwlock_interp γs tid α ty) _ true _ ()
with "Hn []") as (γ) "[lc inv]".
{ iIntros (?). rewrite /rwlock_interp /=.
iSplitR ""; iExists writing_st; done. }
iExists γ, γs. iFrame. by iExists _.
iMod (GPS_SWRaw_Init_vs_strong (rwlock_interp γs α tyOwn tyShr) _ true
_ () (GPS_SWRawWriter l ((): unitProtocol) #(-1))%I
with "Hn [Hvl Hst]") as (γ) "[inv W]".
{ iIntros (?) "W". rewrite /rwlock_interp /=. iFrame "W". iModIntro.
iSplitR ""; iExists writing_st; [|done]. iSplit; [done|]. by iFrame "Hst". }
iExists γ, γs, tyOwn, tyShr. iFrame "inv".
iSplitL ""; [done|]. iSplitL ""; [done|]. iExists _.
by iDestruct (GPS_SWRawWriter_RawReader with "W") as "#$".
Qed.
Lemma rwlock_proto_destroy b l γ γs tid α ty :
⎡ hist_inv ⎤ -∗ ▷?b rwlock_proto_inv l γ γs tid α ty
Lemma rwlock_proto_destroy b l γ γs α tyOwn tyShr :
⎡ hist_inv ⎤ -∗ ▷?b rwlock_proto_inv l γ γs α tyOwn tyShr
={↑histN}=∗ ∃ (z : Z), l ↦ #z ∗ ⌜-1 ≤ z⌝.
Proof.
iIntros "#hInv inv".
iMod (GPS_PPInv_dealloc with "hInv inv") as (s v) "(Hl & F & _)"; [done|].
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 [[|[[??] n] |]| ]; simpl; try omega. lia.
Qed.
Global Instance rwlock_proto_inv_type_ne n l γ γs tid α :
Proper (type_dist2 n ==> dist n) (rwlock_proto_inv l γ γs tid α).
Lemma rwlock_interp_comparable γs α tyO tyS l γ s v:
rwlock_interp γs α tyO tyS false l γ s v
-∗ ⌜∃ vl : lit, v = #vl ∧ lit_comparable (Z_of_bool false) vl⌝.
Proof.
move => ???. apply GPS_PPInv_ne.
solve_proper_core
ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
iDestruct 1 as (st) "[% _]". subst v.
destruct st as [[|[[??] n] |]| ]; simpl;
iExists _; iPureIntro ;(split; [done|by constructor]).
Qed.
Global Instance rwlock_proto_inv_ne l γ γs tid α :
NonExpansive (rwlock_proto_inv l γ γs tid α).
Proof.
intros n ???. eapply rwlock_proto_inv_type_ne, type_dist_dist2. done.
Qed.
(*
Lemma rwlock_proto_inv_proper E L ty1 ty2 q :
eqtype E L ty1 ty2 →
llctx_interp L q -∗ ∀ l γ γs tid α, □ (elctx_interp E -∗
rwlock_proto_inv l γ γs tid α ty1 -∗ rwlock_proto_inv l γ γs tid α ty2).
Proof.
(* TODO : this proof is essentially [solve_proper], but within the logic.
It would easily gain from some automation. *)
rewrite eqtype_unfold. iIntros (Hty) "HL".
iDestruct (Hty with "HL") as "#Hty". iIntros "* !# #HE H".
iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
iAssert (□ (&{α}((l +ₗ 1) ↦∗: ty_own ty1 tid) -∗
&{α}((l +ₗ 1) ↦∗: ty_own ty2 tid)))%I as "#Hb".
{ iIntros "!# H". iApply bor_iff; last done.
iIntros "!>!#"; iSplit; iDestruct 1 as (vl) "[Hf H]"; iExists vl;
iFrame; by iApply "Hown". }
iDestruct "H" as (st) "H"; iExists st;
iDestruct "H" as "($&$&H)"; destruct st as [[|[[agν ?]?]|]|]; try done;
last by iApply "Hb".
iDestruct "H" as (ν q') "(Hag & #Hend & Hh & ? & ? & ?)". iExists ν, q'.
iFrame. iSplitR. done. iSplitL "Hh"; last by iApply "Hshr".
iIntros "Hν". iApply "Hb". iApply ("Hh" with "Hν").
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.
End rwlock_inv.
Section rwlock.
......@@ -177,8 +215,8 @@ Section rwlock.
end)%I;
ty_shr κ tid l :=
(∃ α, κ ⊑ α
∗ ∃ γ γs, rwlock_proto_lc l γ
∗ &at{α,rwlockN}(rwlock_proto_inv l γ γs tid α ty))%I |}.
∗ ∃ γ γs tyOwn tyShr, rwlock_proto_lc l γ tyOwn tyShr tid ty
∗ &at{α,rwlockN}(rwlock_proto_inv l γ γs α tyOwn tyShr))%I |}.
Next Obligation.
iIntros (??[|[[]|]]); try iIntros "[? []]". rewrite ty_size_eq.
iIntros "[_ [_ %]] !% /=". congruence.
......@@ -197,16 +235,17 @@ Section rwlock.
iSplitL "Hn"; [eauto|iExists _; iFrame]. }
iMod (bor_sep with "LFT H") as "[Hn Hvl]". done.
iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]". done.
iAssert ((q / 2).[κ] ∗ ∃ γ γs, rwlock_proto_lc l γ
∗ ▷ rwlock_proto_inv l γ γs tid κ ty)%I with "[> -Hclose]"
iAssert ((q / 2).[κ] ∗
∃ γ γs tyO tyS, rwlock_proto_lc l γ tyO tyS tid ty
∗ ▷ rwlock_proto_inv l γ γs κ tyO tyS)%I with "[> -Hclose]"
as "[$ HQ]"; last first.
{ iDestruct "HQ" as (γ γs) "[lc HQ]".
{ iDestruct "HQ" as (γ γs tyO tyS) "[lc HQ]".
iMod ("Hclose" with "[] HQ") as "[Hb $]".
- iIntros "!> H".
iMod (rwlock_proto_destroy true with "hInv H") as (n') "[Hl ?]".
iExists _. by iFrame.
- iExists κ. iSplitR. by iApply lft_incl_refl.
iExists γ, γs. iFrame "lc". iApply bor_share; try done.
iExists γ, γs, tyO, tyS. iFrame "lc". iApply bor_share; try done.
solve_ndisj. }
by iApply (rwlock_proto_create with "LFT Htok' Hvl H").
Qed.
......@@ -221,31 +260,34 @@ Section rwlock.
Global Instance rwlock_type_ne : TypeNonExpansive rwlock.
Proof.
constructor;
solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_proto_inv_type_ne; try reflexivity) ||
f_type_equiv || f_contractive || f_equiv).
solve_proper_core ltac:(fun _ => exact: type_dist2_S
|| (eapply rwlock_proto_lc_type_ne; try reflexivity)
|| f_type_equiv || f_equiv).
Qed.
Global Instance rwlock_ne : NonExpansive rwlock.
Proof.
constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
constructor;
solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity)
|| f_equiv).
Qed.
(*
Global Instance rwlock_mono E L : Proper (eqtype E L ==> subtype E L) rwlock.
Proof.
(* TODO : this proof is essentially [solve_proper], but within the logic.
It would easily gain from some automation. *)
iIntros (ty1 ty2 EQ qL) "HL". generalize EQ. rewrite eqtype_unfold=>EQ'.
iDestruct (EQ' with "HL") as "#EQ'".
iDestruct (rwlock_inv_proper with "HL") as "#Hty1ty2"; first done.
iDestruct (rwlock_inv_proper with "HL") as "#Hty2ty1"; first by symmetry.
iDestruct (rwlock_proto_lc_proper with "HL") as "#Hty1ty2"; first done.
iIntros "!# #HE". iDestruct ("EQ'" with "HE") as "(% & #Hown & #Hshr)".
iSplit; [|iSplit; iIntros "!# * H"].
- iPureIntro. simpl. congruence.
- destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown".
- iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
iApply at_bor_iff; last done. iSplit; iIntros "!>!# H".
by iApply "Hty1ty2". by iApply "Hty2ty1".
- destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ [$ H]]".
by iApply "Hown".
- iDestruct "H" as (α) "[Ha H]". iExists α. iFrame "Ha".
iDestruct "H" as (γ γs tyO tyS) "[lc H]".
iExists γ, γs, tyO, tyS. iFrame "H".
by iApply ("Hty1ty2" with "HE lc").
Qed.
Lemma rwlock_mono' E L ty1 ty2 :
eqtype E L ty1 ty2 → subtype E L (rwlock ty1) (rwlock ty2).
......@@ -254,7 +296,7 @@ Section rwlock.
Proof. by split; apply rwlock_mono. Qed.
Lemma rwlock_proper' E L ty1 ty2 :
eqtype E L ty1 ty2 → eqtype E L (rwlock ty1) (rwlock ty2).
Proof. eapply rwlock_proper. Qed. *)
Proof. eapply rwlock_proper. Qed.
(* Apparently, we don't need to require ty to be sync,
contrarily to Rust's implementation. *)
......@@ -266,12 +308,15 @@ Section rwlock.
Send ty → Sync ty → Sync (rwlock ty).
Proof.
move=>???????/=. apply bi.exist_mono=>?. apply bi.sep_mono_r.
do 2 apply bi.exist_mono=>?. apply bi.sep_mono_r.
iApply at_bor_iff. iIntros "!> !#". iApply bi.equiv_iff.
apply uPred.exist_proper=>?; do 7 f_equiv; first do 7 f_equiv.
- do 5 f_equiv. apply uPred.equiv_spec; split; iApply send_change_tid.
- apply uPred.equiv_spec; split; iApply sync_change_tid.
- apply uPred.equiv_spec; split; iApply send_change_tid.
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 "?".
+ iApply sync_change_tid. by iApply "H".
+ iApply "H". by iApply sync_change_tid.
Qed.
End rwlock.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment