From f1983fc8b5e3abc854766282bc55351ab39e86b8 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 6 Jun 2018 11:03:11 +0200
Subject: [PATCH] complete rwlock write code, WIP: rwlock code
---
_CoqProject | 1 +
theories/typing/lib/rwlock/rwlock.v | 15 +-
theories/typing/lib/rwlock/rwlock_code.v | 141 +++++++++---------
.../typing/lib/rwlock/rwlockreadguard_code.v | 2 +-
.../typing/lib/rwlock/rwlockwriteguard_code.v | 32 ++--
5 files changed, 104 insertions(+), 87 deletions(-)
diff --git a/_CoqProject b/_CoqProject
index c03b2e2b..929cc6a4 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/rwlockwriteguard_code.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 462e7ed3..f5e552ac 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -98,7 +98,7 @@ Section rwlock_inv.
rewrite /= -(right_id None op (Some _)). by apply cancel_local_update_unit, _.
Qed.
- Lemma rown_global_reading_st st q ν γs:
+ 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))⌝.
Proof.
@@ -119,6 +119,19 @@ Section rwlock_inv.
- by apply option_included in INCL as [?|[?[?[?[??]]]]].
Qed.
+ Lemma rwown_global_writing_st st γs:
+ rwown γs (st_global st) -∗ rwown γs writing_st -∗
+ ⌜st = (Some (inl tt))⌝.
+ Proof.
+ iIntros "m w". iCombine "m" "w" as "mw".
+ iDestruct (own_valid with "mw") as %[INCL VAL]%auth_valid_discrete_2.
+ iPureIntro. destruct st as [[[]|[[]]]|]; [done|..].
+ - move : INCL =>
+ /Some_included [Eq|/csum_included [//|[[?[?[?[Eq _]]]]|[?[?[?[??//]]]]]]];
+ inversion Eq.
+ - move :INCL => /= /option_included [//|[?[? [? [? //]]]]].
+ Qed.
+
(* GPS protocol definitions *)
Definition rwlock_interp
(γs: gname) (α : lft) (tyO: vProp) (tyS: lft → vProp)
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 08a0ba9a..9a5c0c62 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -5,7 +5,7 @@ From lrust.lang Require Import memcpy.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import typing option.
From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard rwlockwriteguard.
-From gpfsl.gps Require Import middleware.
+From gpfsl.gps Require Import middleware protocols.
Set Default Proof Using "Type".
(** SYNCHRONIZATION CONDITIONS of rwlock *)
@@ -18,9 +18,7 @@ Set Default Proof Using "Type".
- write_unlock uses a release write
- read_lock uses an acquire CAS
- write_lock uses an acquire CAS
- - read_unlock uses a release CAS
- TODO: check if read_unlock can be a relaxed CAS, due to the release sequence
- or read-only accesses? *)
+ - read_unlock uses a release CAS *)
Section rwlock_functions.
Context `{typeG Σ, rwlockG Σ}.
@@ -180,20 +178,17 @@ Section rwlock_functions.
iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']". done.
iDestruct (lft_tok_split_unit (qβ/2) (qβ/2) β with "[Hβtok]")
as "[Hβtok1 Hβtok2]". { by rewrite Qp_div_2. }
- iDestruct "Hinv" as (γ γs tyO tyS) "((EqO & EqS & PP) & Hinv)".
- iDestruct "PP" as (vP) "PP".
+ iDestruct "Hinv" as (γ γs tyO tyS) "((EqO & EqS & R) & Hinv)".
+ iDestruct "R" as (vR) "R".
wp_bind (!ʳˡˣ(LitV lx))%E.
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 (st1) ">mst".
- iApply (GPS_PPRaw_read with "[$PP $INV]"); [solve_ndisj|by left|..].
+ iApply (GPS_SWRawReader_read with "[$R $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".
+ iNext. iIntros ([] v') "(_ & #R' & INV & Int)".
+ iDestruct (rwlock_interp_read_acq with "Int") as (st') "Int".
iDestruct "Int" as %?. subst v'.
- iMod ("Hclose''" with "[mst INV]") as "Hβtok1".
- { rewrite rwlock_proto_inv_split. iFrame "INV". by iExists _. }
+ iMod ("Hclose''" with "INV") as "Hβtok1".
iModIntro. wp_let. wp_op; case_bool_decide as Hm1; wp_if.
- iDestruct (monPred_objectively_elim with "Hβtok2") as "Hβtok2".
iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
@@ -206,74 +201,84 @@ Section rwlock_functions.
simpl. iApply type_jump; solve_typing.
- 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 (bi.later_exist_2 with "mst") as ">mst".
set Q : () → vProp Σ :=
- (λ _, (∃ st, rwown γs (main_st st)) ∗
- (qβ / 2).[β] ∗
+ (λ _, (qβ / 2).[β] ∗
(∃ qν ν, (qν).[ν] ∗
tyS (β ⊓ ν) ∗
rwown γs (reading_st qν ν) ∗
((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν])))%I.
set R : () → lit → vProp Σ := (λ _ _, True)%I.
- set P : vProp Σ := ((∃ st, rwown γs (main_st st)) ∗ <obj> (qβ / 2).[β])%I.
+ set P : vProp Σ := (<obj> (qβ / 2).[β])%I.
+ set T : () → () → vProp Σ :=
+ (λ _ _, (qβ / 2).[β] ∗
+ ∃ ν n q q',
+ ([†ν] ={↑lftN ∪ ↑histN}=∗ &{β} tyO) ∗
+ (q').[ν] ∗
+ GPS_SWSharedReader lx (() : unitProtocol) #(Z.pos n) q' γ ∗
+ rwown γs (st_global (Some (inr (ν, (q + q' / 2)%Qp, (n + 1)%positive)))) ∗
+ rwown γs (reading_st (q' / 2) ν))%I.
iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
- iApply (GPS_PPRaw_CAS_int_simple (rwlock_interp γs β tyO tyS) _ _ _ _ _
- (Z_of_rwlock_st st2) #(Z_of_rwlock_st st2 + 1) () P Q R _ _ Vb'
- with "[$PP $INV mst Hβtok2 rTrue]");
- [solve_ndisj|by left|done|by right|by left|iSplitL ""; last iSplitL ""|..].
+ iApply (GPS_SWSharedWriter_CAS_int (rwlock_interp γs β tyO tyS) _
+ rwlock_noCAS _ _ _ (Z_of_rwlock_st st') #(Z_of_rwlock_st st' + 1)
+ () _ _ P T Q R _ Vb' _ (⊤ ∖ ↑rwlockN)
+ with "[$R' $INV Hβtok2 rTrue]");
+ [done|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. iSplitL ""; last first.
- { rewrite -(bi.True_sep' P).
- iApply (rel_sep_objectively with "[$rTrue mst Hβtok2]").
- iModIntro. by iFrame. }
+ { rewrite -{2}(bi.True_sep' P).
+ iApply (rel_sep_objectively with "[$rTrue Hβtok2]"). by iModIntro. }
iNext. rewrite -(bi.True_sep' (∀ _ : (), _)%I).
iApply (rel_sep_objectively with "[$rTrue]"). iModIntro.
iIntros ([] _). iSplit; [|by iIntros (?) "_ _"].
- iIntros "[mst Hβtok2]". iDestruct "mst" as (st3) "mst".
- iDestruct (monPred_objectively_elim with "Hβtok2") as "Hβtok2".
- iDestruct 1 as (st2') "[Eqst INT]". iDestruct "Eqst" as %Eqst.
- destruct st2' as [[[]|[[ν q] n]]|].
- - exfalso. clear -Eqst Hm1. simpl in Eqst. inversion Eqst as [Eq1].
- rewrite Eq1 in Hm1. omega.
- - 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 "∗ 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 (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 ∪ ↑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. }
+ iSplit.
+ { rewrite /rwlock_noCAS. iIntros "_" (Eq) "_".
+ inversion Eq as [Eq1]. rewrite Eq1 in Hm1. exfalso. by apply Hm1. }
+ iSplitL "".
+ - iIntros "Hβtok2". iDestruct 1 as (st2) "[Eqst [g INT]]".
+ iDestruct (monPred_objectively_elim with "Hβtok2") as "Hβtok2".
+ iDestruct "Eqst" as %Eqst.
+ destruct st2 as [[[]|[[ν q] n]]|].
+ + exfalso. clear -Eqst Hm1. simpl in Eqst. inversion Eqst as [Eq1].
+ rewrite Eq1 in Hm1. omega.
+ + simpl in Eqst. iDestruct 1 as (?) "[_ #Share]".
+ iDestruct "INT" as (q') "(#H† & Hh & #Hshr & Hqq' & Hν & W & Rs)".
+ iDestruct "Hqq'" as %Hqq'. iExists (). iSplitL ""; [done|].
+ iMod (rwown_update_read ν n q q' γs Hqq' with "g") as "[g rst]".
+ have Eq: Z_of_rwlock_st st' + 1 = Z.pos (n + 1).
+ { clear -Eqst. inversion Eqst as [Eq]. by rewrite Eq. }
+ iModIntro. iFrame "Hβtok2". rewrite Eqst.
+ iFrame "W". iExists ν,n,q,q'. iFrame "Hh Hν Rs g rst".
+ +
+ 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 "∗ 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 (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 ∪ ↑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. }
iNext. simpl.
iIntros (b v' [])
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 31e66639..22382bf9 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -105,7 +105,7 @@ Section rwlockreadguard_functions.
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']].
+ iDestruct (rwown_global_reading_st with "g H◯") as %[q' [n Eqst2']].
subst st2'. iDestruct 1 as (?) "[_ #Share]".
iExists (). rewrite Eqst /=. iSplitL ""; [done|].
admit.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index d0fbe0f7..7069a0cb 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -118,34 +118,32 @@ Section rwlockwriteguard_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 (γs β) "(Hx' & #Hαβ & wst & Hsst & #Hinv)".
- iDestruct "Hinv" as (γ tyO tyS) "((EqO & EqS & PP) & Hinv)".
- iDestruct "PP" as (vP) "PP".
+ iDestruct "Hx'" as (γs β) "(Hx' & #Hαβ & wst & Hinv)".
+ iDestruct "Hinv" as (γ tyO tyS) "(W & (#EqO & #EqS & #R) & #Hinv)".
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' <-ʳᵉˡ #0)%E.
iMod (at_bor_acc with "LFT Hinv Hβ") as (Vb) "[INV Hcloseβ]"; [done..|].
- iDestruct (rwlock_proto_inv_split with "INV") as "[H● INV]".
- iDestruct "H●" as (st1) ">H●".
- iDestruct (rwown_main_sub_agree with "H● Hsst") as %?. subst st1.
- iMod (rwown_update_write_dealloc with "H● Hsst wst") as "(mst & sst)".
iAssert (▷ □ (∀ κ q' E', ⌜lftE ⊆ E'⌝ -∗ &{κ} tyO -∗
(q').[κ] ={E'}=∗ (□ tyS κ) ∗ (q').[κ]))%I as "#Share".
{ iIntros "!> !#" (κ???) "tyO tok".
iMod (ty_share with "LFT [tyO] tok") as "[#tyS $]" ;[done|..].
- iApply (bor_iff with "EqO tyO").
- iIntros "!> !#". by iApply "EqS". }
- iApply (GPS_PPRaw_write (rwlock_interp γs β tyO tyS) _ _ _ #0 _ ()
- with "[$PP $INV sst Hx']"); [done|solve_ndisj|by right|..].
- { simpl. iNext. iIntros "_ !>".
- iSplitL "sst Hx'"; iExists None; [|by iFrame "Share"].
- iSplitL ""; [done|]. iFrame "sst". iApply (bor_iff with "[] Hx'").
- iIntros "!> !#". by iApply (bi_iff_sym with "EqO"). }
- iNext. iIntros "[PP' INV]".
- iMod ("Hcloseβ" with "[INV mst]") as "Hβ".
- { iIntros "Vb'". iDestruct ("INV" with "Vb'") as "$". by iExists _. }
-
+ iApply (GPS_SWRawWriter_rel_write (rwlock_interp γs β tyO tyS) _
+ rwlock_noCAS True%I () () #(-1) #0 with "[$W $INV wst Hx']");
+ [done|solve_ndisj|done|..].
+ { simpl. iNext. iDestruct 1 as (st') "[_ [g INT]]". iIntros "W".
+ iDestruct (rwown_global_writing_st with "g wst") as %?. subst st'.
+ iMod (rwown_update_write_dealloc with "g wst") as "g". iModIntro.
+ iDestruct (GPS_SWRawWriter_shared with "W") as "[W Rs]".
+ iSplitL ""; [done|]. iSplitR ""; iExists None; [|by iFrame "Share"].
+ iSplitL ""; [done|]. iFrame "g W Rs".
+ iApply (bor_iff with "[] Hx'"). iIntros "!> !#". iApply bi_iff_sym.
+ by iApply "EqO". }
+ iNext. iIntros "(R' & INV & _)".
+ iMod ("Hcloseβ" with "INV") as "Hβ".
iModIntro. wp_seq. iMod ("Hcloseα" with "Hβ") as "Hα".
iMod ("Hclose" with "Hα HL") as "HL".
iApply (type_type _ _ _ [ x ◁ box (uninit 1)]
--
GitLab