WIP: rwlock code read lock acquire

opam

@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2018-06-03.1.8d7b204c") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2018-06-04.0.f12ff24c") | (= "dev") }
 ]

theories/lang/lock.v

@@ -136,17 +136,17 @@ Section proof.
     iIntros (??) "#Hproto !# * HP HΦ".
     wp_rec. iMod ("Hproto" with "HP") as (γ R0 Vb) "(#[Eq lc] & inv & Hclose)".
     iDestruct "lc" as (?) "lc".
-    iMod (rel_True_intro True%I tid with "[//]") as "rTrue".
+    iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
     iApply (GPS_PPRaw_CAS_int_simple (lock_interp R0) _ _ _ _ _
-                (Z_of_bool false) #true () (λ _, R0)%I (λ _ _, True)%I
-            with "[$lc $inv rTrue]");[done|by left|done|by right|by left|..].
+                (Z_of_bool false) #true () True%I (λ _, R0)%I (λ _ _, True)%I
+        with "[$lc $inv]");[done|by left|done|by right|by left|..].
     { iSplitL ""; [|iSplitL ""]; [iNext; iModIntro..|].
       - iIntros (?? _). by iApply lock_interp_comparable.
       - by iIntros (??)"_ #$".
-      - iNext. rewrite /= -(bi.True_sep' (∀ _, _)%I).
+      - iFrame "rTrue". iNext. rewrite /= -(bi.True_sep' (∀ _, _)%I).
         iApply (rel_sep_objectively with "[$rTrue]").
         iModIntro. iIntros ([] _). iSplit; [|by iIntros (?) "??"].
-        iIntros "F _". iModIntro. rewrite /lock_interp /=.
+        iIntros "_ F _". iModIntro. rewrite /lock_interp /=.
         iExists (). iSplitL ""; [done|]. iDestruct "F" as (b) "[Eq R0]".
         iDestruct "Eq" as %Eq. destruct b; [by inversion Eq|].
         iFrame "R0". iSplit; by iExists true. }

theories/typing/lib/rwlock/rwlock_code.v

@@ -193,27 +193,32 @@ Section rwlock_functions.
     - 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".
+      iDestruct (bi.later_exist_2 with "mst") as ">mst".
       set Q : () → vProp Σ :=
-        (λ _, (∃ st, ▷ rwown γs (main_st st)) ∗
+        (λ _, (∃ st, rwown γs (main_st st)) ∗
               (qβ / 2).[β] ∗
               (∃ qν ν, (qν).[ν] ∗
                  tyS (β ⊓ ν) ∗
                  rwown γs (reading_st qν ν) ∗
                  ((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν])))%I.
-      set R : () → lit → vProp Σ :=
-        (λ _ _, (∃ st, ▷ rwown γs (main_st st)) ∗ (qβ / 2).[β])%I.
-      iMod (rel_True_intro True%I tid with "[//]") as "rTrue".
+      set R : () → lit → vProp Σ := (λ _ _, True)%I.
+      set P : vProp Σ := ((∃ st, rwown γs (main_st st)) ∗ <obj> (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) () Q R _ _ Vb'
+                  (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 ""|..].
       { iIntros "!> !>" (???). by iApply rwlock_interp_comparable. }
       { iIntros "!> !>" (???). by iApply rwlock_interp_duplicable. }
-      { simpl. iNext. rewrite /= -(bi.True_sep' (∀ _ : (), _)%I).
-        iApply (rel_sep_objectively with "[$rTrue mst Hβtok2]").
-        iModIntro. iDestruct (monPred_objectively_elim with "Hβtok2") as "Hβtok2".
-        iIntros ([] _). iSplit; [|iIntros (?) "_ _"; iFrame "Hβtok2"; by iExists _].
+      { simpl. iSplitL ""; last first.
+        { rewrite -(bi.True_sep' P).
+          iApply (rel_sep_objectively with "[$rTrue mst Hβtok2]").
+          iModIntro. by iFrame. }
+        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].
@@ -241,7 +246,8 @@ Section rwlock_functions.
           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.
+          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.
@@ -257,7 +263,7 @@ Section rwlock_functions.
 
       iNext. simpl.
       iIntros (b v' [])
-              "(INV & _ &[([%%] & _ & mst & Hβtok2 & Hβ) | ([% Neq] & PP' & R)])".
+              "(INV & _ &[([%%] & _ & mst & Hβtok2 & Hβ) | ([% Neq] & _ & _ & P)])".
       + 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".
@@ -279,15 +285,20 @@ Section rwlock_functions.
         iApply (type_sum_assign (option $ rwlockreadguard α ty)); [solve_typing..|].
         simpl. iApply type_jump; solve_typing.
       + 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.
+        iDestruct (rel_sep_elim with "P") as "[mst Hβtok2]".
+        iDestruct (rel_exist with "mst") as (st') "mst".
+        iDestruct (rel_embed_elim with "mst") as "mst".
+        iDestruct (rel_objectively_elim with "Hβtok2") as "Hβtok2".
+        iDestruct (monPred_objectively_elim with "Hβtok2") as "Hβtok2".
+        iMod ("Hclose''" with "[INV mst]") as "Hβtok1".
+        { iIntros "Vb'". iDestruct ("INV" with "Vb'") as "$". by iExists _. }
         iModIntro. wp_case. iMod ("Hclose'" with "[$]") as "Hα".
         iMod ("Hclose" with "Hα HL") as "HL".
         iSpecialize ("Hk" with "[]"); first solve_typing.
         iApply ("Hk" $! [#] with "Hna HL").
         rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
-        iExists _. iSplit. done. simpl. eauto.
+        iExists _. iSplit. done. iExists _. iFrame "Hαβ". 
+        iExists _,_,_,_. iFrame "EqO EqS Hinv". by iExists _.
   Qed.
 
   (* Acquiring a write lock. *)