complete rwlock acquire 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/rwlock_code.v
 theories/typing/examples/get_x.v
 theories/typing/examples/rebor.v
 theories/typing/examples/unbox.v

theories/typing/lib/rwlock/rwlock.v

@@ -142,6 +142,21 @@ Section rwlock_inv.
       apply Qcplus_le_mono_r, Qp_ge_0.
   Qed.
 
+  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.
+  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 (Cinl (Excl ())) = Some (Cinl (Excl ())) ⋅ ε);
+              [by apply op_local_update_discrete|by rewrite right_id_L].
+  Qed.
+
   (* GPS protocol definitions *)
   Definition rwlock_interp
     (γs: gname) (α : lft) (tyO: vProp) (tyS: lft → vProp)

theories/typing/lib/rwlock/rwlock_code.v

@@ -8,6 +8,20 @@ From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard rwlockwritegu
 From gpfsl.gps Require Import middleware.
 Set Default Proof Using "Type".
 
+(** SYNCHRONIZATION CONDITIONS of rwlock *)
+(*  ---> stands for Release-Acquire synchronization.
+  write_unlock  --->  read_lock
+  read_unlock   --->  read_lock
+  read_unlock   --->  write_lock
+
+  This leads to the following C11 implementation:
+  - 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? *)
+
 Section rwlock_functions.
   Context `{typeG Σ, rwlockG Σ}.
 
@@ -332,37 +346,75 @@ Section rwlock_functions.
     iIntros (x' tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
-    iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
+    iDestruct "Hx'" as (β) "#[Hαβ Hinv]".
+    iDestruct "Hinv" as (γ γs tyO tyS) "((EqO & EqS & PP) & Hinv)".
+    iDestruct "PP" as (vP) "PP".
     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βtok Hclose']". done.
-    wp_bind (CAS _ _ _).
-    iMod (at_bor_acc_tok with "LFT Hinv Hβtok") as "[INV Hclose'']"; try done.
-    iDestruct "INV" as (st) "(Hlx & >Hownst & Hst)". destruct st.
-    - iApply (wp_cas_int_fail with "Hlx"). by destruct c as [|[[]]|].
-      iNext. iIntros "Hlx".
-      iMod ("Hclose''" with "[Hlx Hownst Hst]") as "Hβtok"; first by iExists _; iFrame.
+    wp_bind (CAS _ _ _ _ _ _).
+    iMod (at_bor_acc with "LFT Hinv Hβtok") as (Vb) "[INV Hclose'']"; try 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) ∗ rwown γs (sub_st st)) ∗
+             &{β}tyO ∗ rwown γs writing_st)%I.
+    set R : () → lit → vProp Σ := (λ _ _, True)%I.
+    set P : vProp Σ := ((∃ st, rwown γs (main_st st)))%I.
+    iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
+    iApply (GPS_PPRaw_CAS_int_simple (rwlock_interp γs β tyO tyS) _ _ _ _ _
+                  0 #(-1) () P Q R _ _ Vb with "[$PP $INV mst 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. iSplitL ""; last first.
+      { rewrite -{2}(bi.True_sep' P).
+        iApply (rel_sep_objectively with "[$rTrue mst]"). iModIntro. by iFrame. }
+      iNext. rewrite -(bi.True_sep' (∀ _ : (), _)%I).
+      iApply (rel_sep_objectively with "[$rTrue]"). iModIntro.
+      iIntros ([] _). iSplit; [|by iIntros (?) "_ _"].
+      iDestruct 1 as (st) "mst".
+      iDestruct 1 as (st') "[Eqst INT]". iDestruct "Eqst" as %Eqst.
+      destruct st' as [[[]|[[ν q] n]]|]; [by inversion Eqst..|].
+      iDestruct "INT" as "[sst Hst]".
+      iDestruct 1 as (?) "[_ #Share]". iExists (). iSplitL ""; [done|].
+      iDestruct (rwown_main_sub_agree with "mst sst") as %Eqst2. subst st.
+      set st': rwlock_st := Some (inl ()).
+      iMod (rwown_update_write γs with "mst sst") as "(mst'&sst'&wst)".
+      iModIntro. iFrame "Hst wst". iSplitR ""; [iExists _; by iFrame|].
+      iSplitL ""; iExists st'; [done|by iFrame "Share"]. }
+
+    iNext. simpl.
+    iIntros (b v' [])
+            "(INV & _ &[([%%] & _ & mst & Hβ & wst) | ([% Neq] & _ & _ & P)])".
+    - subst b v'. iDestruct "mst" as (st2) "[mst sst]".
+      iMod ("Hclose''" with "[mst INV]") as "Hβtok".
+      { iIntros "Vb'". iDestruct ("INV" with "Vb'") as "$". by iExists st2. }
       iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
       iModIntro. wp_case.
-      iApply (type_type _ _ _
-              [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2) ]
-              with "[] LFT HE Hna HL Hk"); first last.
-      { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
-      iApply (type_sum_unit (option $ rwlockwriteguard α ty));
-        [solve_typing..|]; first last.
-      rewrite /option /=. iApply type_jump; solve_typing.
-    - iApply (wp_cas_int_suc with "Hlx"). iIntros "!> Hlx".
-      iMod (own_update with "Hownst") as "[Hownst ?]".
-      { by eapply auth_update_alloc, (op_local_update_discrete _ _ writing_st). }
-      iMod ("Hclose''" with "[Hlx Hownst]") as "Hβtok". { iExists _. iFrame. }
-      iModIntro. wp_case. iMod ("Hclose'" with "Hβtok") as "Hα".
-      iMod ("Hclose" with "Hα HL") as "HL".
       iApply (type_type  _ _ _
                    [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2);
                      #lx ◁ rwlockwriteguard α 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 "∗#". }
+                tctx_hasty_val' //. iFrame "Hx Hr".
+        iExists γs, β. iSplitL "Hβ"; [by iApply (bor_iff with "[$EqO] Hβ")|].
+        iFrame "Hαβ wst". iSplitL "sst"; [by iExists st2|].
+        iExists _,_,_. iFrame "EqO EqS Hinv". by iExists _. }
       iApply (type_sum_assign (option $ rwlockwriteguard α ty)); [solve_typing..|].
       simpl. iApply type_jump; solve_typing.
+    - subst b.
+      iDestruct (rel_exist with "P") as (st') "mst".
+      iDestruct (rel_embed_elim with "mst") as "mst".
+      iMod ("Hclose''" with "[INV mst]") as "Hβtok".
+      { iIntros "Vb'". iDestruct ("INV" with "Vb'") as "$". by iExists _. }
+      iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+      iModIntro. wp_case.
+      iApply (type_type _ _ _
+              [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2) ]
+              with "[] LFT HE Hna HL Hk"); first last.
+      { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+      iApply (type_sum_unit (option $ rwlockwriteguard α ty));
+        [solve_typing..|]; first last.
+      rewrite /option /=. iApply type_jump; solve_typing.
   Qed.
 End rwlock_functions.

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) ∗
-             α ⊑ β ∗ rwown γs writing_st ∗
+             α ⊑ β ∗ rwown γs writing_st ∗ (∃ st, rwown γs (sub_st st)) ∗
              (∃ γ tyO tyS, rwlock_proto_lc l γ tyO tyS tid ty ∗
                     &at{β,rwlockN}(rwlock_proto_inv l γ γs β tyO tyS))
          | _ => False
@@ -84,8 +84,8 @@ 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 & Hinv)".
-      iExists γs, β. iFrame "Hown". iSplit; last iSplit.
+      iDestruct "H" as (γs β) "(Hb & #H⊑ & Hown & Hsst & Hinv)".
+      iExists γs, β. iFrame "Hown Hsst". iSplit; last iSplit.
       + iApply bor_iff; last done.
         iIntros "!>!#". iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
         iExists vl; iFrame; by iApply "Ho".