complete rwlock write code, WIP: rwlock code

_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

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)

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' [])

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.

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)]