WIP: rwlock code

_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

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

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

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