Simplify the model of mutexes by removing the exclusive token.

theories/lang/lib/lock.v

@@ -15,42 +15,24 @@ Definition release : val := λ: ["l"], "l" <-ˢᶜ #false.
    protocol into shared borrows.  Cancellable invariants don't work because
    their cancelling view shift has a non-empty mask, and it would have to be
    executed in the consequence view shift of a borrow. *)
-
-(** The CMRA we need. *)
-(* Not bundling heapG, as it may be shared with other users. *)
-Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
-Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
-
-Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
-Proof. solve_inG. Qed.
-
 Section proof.
-  Context `{!lrustG Σ, !lockG Σ}.
+  Context `{!lrustG Σ}.
 
-  Definition lock_proto (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
-    (∃ b : bool, l ↦ #b ∗ if b then True else own γ (Excl ()) ∗ R)%I.
+  Definition lock_proto (l : loc) (R : iProp Σ) : iProp Σ :=
+    (∃ b : bool, l ↦ #b ∗ if b then True else R)%I.
 
-  Definition locked (γ : gname): iProp Σ := own γ (Excl ()).
-
-  Global Instance lock_proto_ne γ l : NonExpansive (lock_proto γ l).
+  Global Instance lock_proto_ne l : NonExpansive (lock_proto l).
   Proof. solve_proper. Qed.
 
-  Global Instance locked_timeless γ : TimelessP (locked γ).
-  Proof. apply _. Qed.
-
-  Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
-  Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
-
-  Lemma lock_proto_iff γ l R R' :
-    □ (R ↔ R') -∗ lock_proto γ l R -∗ lock_proto γ l R'.
+  Lemma lock_proto_iff l R R' :
+    □ (R ↔ R') -∗ lock_proto l R -∗ lock_proto l R'.
   Proof.
     iIntros "#HRR' Hlck". iDestruct "Hlck" as (b) "[Hl HR]". iExists b.
-    iFrame "Hl". destruct b; first done. iDestruct "HR" as "[$ HR]".
-    by iApply "HRR'".
+    iFrame "Hl". destruct b; first done. by iApply "HRR'".
   Qed.
 
-  Lemma lock_proto_iff_proper γ l R R' :
-    □ (R ↔ R') -∗ □ (lock_proto γ l R ↔ lock_proto γ l R').
+  Lemma lock_proto_iff_proper l R R' :
+    □ (R ↔ R') -∗ □ (lock_proto l R ↔ lock_proto l R').
   Proof.
     iIntros "#HR !#". iSplit; iIntros "Hlck"; iApply (lock_proto_iff with "[HR] Hlck").
     - done.
@@ -59,43 +41,39 @@ Section proof.
 
   (** The main proofs. *)
   Lemma lock_proto_create (R : iProp Σ) l (b : bool) :
-    l ↦ #b -∗ (if b then True else ▷ R) ==∗ ∃ γ, ▷ lock_proto γ l R.
+    l ↦ #b -∗ (if b then True else ▷ R) ==∗ ▷ lock_proto l R.
   Proof.
-    iIntros "Hl HR".
-    iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
-    iExists _, _. iFrame "Hl". destruct b; first done. by iFrame.
+    iIntros "Hl HR". iExists _. iFrame "Hl". destruct b; first done. by iFrame.
   Qed.
 
-  Lemma lock_proto_destroy γ l R :
-    lock_proto γ l R -∗ ∃ (b : bool), l ↦ #b ∗ if b then True else R.
+  Lemma lock_proto_destroy l R :
+    lock_proto l R -∗ ∃ (b : bool), l ↦ #b ∗ if b then True else R.
   Proof.
-    iIntros "Hlck". iDestruct "Hlck" as (b) "[Hl HR]".
-    iExists b. iFrame "Hl". destruct b; first done.
-    iDestruct "HR" as "[_ $]".
+    iIntros "Hlck". iDestruct "Hlck" as (b) "[Hl HR]". auto with iFrame.
   Qed.
 
   Lemma mklock_unlocked_spec (R : iProp Σ) (l : loc) v :
-    {{{ l ↦ v ∗ ▷ R }}} mklock_unlocked [ #l ] {{{ γ, RET #(); ▷ lock_proto γ l R }}}.
+    {{{ l ↦ v ∗ ▷ R }}} mklock_unlocked [ #l ] {{{ RET #(); ▷ lock_proto l R }}}.
   Proof.
     iIntros (Φ) "[Hl HR] HΦ". wp_lam. rewrite -wp_fupd. wp_write.
-    iMod (lock_proto_create with "Hl HR") as (γ) "Hproto".
+    iMod (lock_proto_create with "Hl HR") as "Hproto".
     iApply "HΦ". by iFrame.
   Qed.
 
   Lemma mklock_locked_spec (R : iProp Σ) (l : loc) v :
-    {{{ l ↦ v }}} mklock_locked [ #l ] {{{ γ, RET #(); ▷ lock_proto γ l R }}}.
+    {{{ l ↦ v }}} mklock_locked [ #l ] {{{ RET #(); ▷ lock_proto l R }}}.
   Proof.
     iIntros (Φ) "Hl HΦ". wp_lam. rewrite -wp_fupd. wp_write.
-    iMod (lock_proto_create with "Hl [//]") as (γ) "Hproto".
+    iMod (lock_proto_create with "Hl [//]") as "Hproto".
     iApply "HΦ". by iFrame.
   Qed.
 
   (* At this point, it'd be really nice to have some sugar for symmetric
      accessors. *)
-  Lemma try_acquire_spec E γ l R P :
-    □ (P ={E,∅}=∗ ▷ lock_proto γ l R ∗ (▷ lock_proto γ l R ={∅,E}=∗ P)) -∗
+  Lemma try_acquire_spec E l R P :
+    □ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
     {{{ P }}} try_acquire [ #l ] @ E
-    {{{ b, RET #b; (if b is true then locked γ ∗ ▷ R else True) ∗ P }}}.
+    {{{ b, RET #b; (if b is true then ▷ R else True) ∗ P }}}.
   Proof.
     iIntros "#Hproto !# * HP HΦ".
     wp_rec. iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
@@ -104,30 +82,29 @@ Section proof.
       iMod ("Hclose" with "[Hl]"); first (iExists true; by eauto).
       iModIntro. iApply ("HΦ" $! false). auto.
     - wp_apply (wp_cas_int_suc with "Hl"); [done..|]. iIntros "Hl".
-      iDestruct "HR" as "[Hγ HR]".
       iMod ("Hclose" with "[Hl]") as "HP"; first (iExists true; by eauto).
-      iModIntro. rewrite /locked. iApply ("HΦ" $! true with "[$Hγ $HR $HP]").
+      iModIntro. iApply ("HΦ" $! true); iFrame.
   Qed.
 
-  Lemma acquire_spec E γ l R P :
-    □ (P ={E,∅}=∗ ▷ lock_proto γ l R ∗ (▷ lock_proto γ l R ={∅,E}=∗ P)) -∗
-    {{{ P }}} acquire [ #l ] @ E {{{ RET #(); locked γ ∗ ▷ R ∗ P }}}.
+  Lemma acquire_spec E l R P :
+    □ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
+    {{{ P }}} acquire [ #l ] @ E {{{ RET #(); ▷ R ∗ P }}}.
   Proof.
     iIntros "#Hproto !# * HP HΦ". iLöb as "IH". wp_rec.
     wp_apply (try_acquire_spec with "Hproto HP"). iIntros ([]).
-    - iIntros "[[Hlked HR] Hown]". wp_if. iApply "HΦ"; iFrame.
+    - iIntros "[HR Hown]". wp_if. iApply "HΦ"; iFrame.
     - iIntros "[_ Hown]". wp_if. iApply ("IH" with "Hown HΦ").
   Qed.
 
-  Lemma release_spec E γ l R P :
-    □ (P ={E,∅}=∗ ▷ lock_proto γ l R ∗ (▷ lock_proto γ l R ={∅,E}=∗ P)) -∗
-    {{{ locked γ ∗ R ∗ P }}} release [ #l ] @ E {{{ RET #(); P }}}.
+  Lemma release_spec E l R P :
+    □ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
+    {{{ R ∗ P }}} release [ #l ] @ E {{{ RET #(); P }}}.
   Proof.
-    iIntros "#Hproto !# * (Hlocked & HR & HP) HΦ". wp_let.
+    iIntros "#Hproto !# * (HR & HP) HΦ". wp_let.
     iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
     iDestruct "Hinv" as (b) "[? _]". wp_write. iApply "HΦ".
     iApply "Hclose". iExists false. by iFrame.
   Qed.
 End proof.
 
-Typeclasses Opaque lock_proto locked.
+Typeclasses Opaque lock_proto.

theories/typing/lib/mutex/mutex.v

@@ -11,7 +11,7 @@ Set Default Proof Using "Type".
 Definition mutexN := lrustN .@ "mutex".
 
 Section mutex.
-  Context `{!typeG Σ, !lockG Σ}.
+  Context `{!typeG Σ}.
 
   (*
     pub struct Mutex<T: ?Sized> {
@@ -33,9 +33,8 @@ Section mutex.
          | #(LitInt z) :: vl' =>
            ⌜∃ b, z = Z_of_bool b⌝ ∗ ty.(ty_own) tid vl'
          | _ => False end;
-       ty_shr κ tid l :=
-         ∃ γ κ',
-           &at{κ, mutexN} (lock_proto γ l (&{κ'} shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗ κ ⊑ κ'
+       ty_shr κ tid l := ∃ κ', κ ⊑ κ' ∗
+           &at{κ, mutexN} (lock_proto l (&{κ'} shift_loc l 1 ↦∗: ty.(ty_own) tid))
     |}%I.
   Next Obligation.
     iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq.
@@ -59,20 +58,20 @@ Section mutex.
     clear b vl. iMod (bor_sep with "LFT Hbor") as "[Hl Hbor]"; first done.
     iMod (bor_acc_cons with "LFT Hl Htok") as "[>Hl Hclose]"; first done.
     iDestruct "Hl" as (b) "Hl".
-    iMod (lock_proto_create with "Hl [Hbor]") as (γ) "Hproto".
+    iMod (lock_proto_create with "Hl [Hbor]") as "Hproto".
     { destruct b; last by iExact "Hbor". done. }
     iMod ("Hclose" with "[] Hproto") as "[Hl Htok]".
-    { clear b. iIntros "!> Hproto !>". iDestruct (lock_proto_destroy with "Hproto") as (b) "[Hl _]".
-      iNext. eauto with iFrame. }
-    iFrame "Htok". iExists γ, κ.
+    { clear b. iIntros "!> Hproto !>".
+      iDestruct (lock_proto_destroy with "Hproto") as (b) "[Hl _]".
+      eauto 10 with iFrame. }
+    iFrame "Htok". iExists κ.
     iMod (bor_share with "Hl") as "$"; [solve_ndisj..|].
     iApply lft_incl_refl.
   Qed.
   Next Obligation.
     iIntros (ty κ κ' tid l) "#Hincl H".
-    iDestruct "H" as (γ κ'') "(#Hlck & #Hlft)".
-    iExists _, _. iSplit; first by iApply at_bor_shorten.
-    iApply lft_incl_trans; done.
+    iDestruct "H" as (κ'') "(#Hlft & #Hlck)".
+    iExists _. by iSplit; [iApply lft_incl_trans|iApply at_bor_shorten].
   Qed.
 
   Global Instance mutex_wf ty `{!TyWf ty} : TyWf (mutex ty) :=
@@ -99,8 +98,8 @@ Section mutex.
     - simpl. iPureIntro. f_equiv. done.
     - iIntros "!# * Hvl". destruct vl as [|[[| |n]|]vl]; try done.
       simpl. iDestruct "Hvl" as "[$ Hvl]". by iApply "Howni".
-    - iIntros "!# * Hshr". iDestruct "Hshr" as (γ κ') "[Hshr Hincl]".
-      iExists _, _. iFrame "Hincl". iApply (at_bor_iff with "[] Hshr"). iNext.
+    - iIntros "!# * Hshr". iDestruct "Hshr" as (κ') "[Hincl Hshr]".
+      iExists _. iFrame "Hincl". iApply (at_bor_iff with "[] Hshr"). iNext.
       iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
       iApply heap_mapsto_pred_iff_proper.
       iAlways; iIntros; iSplit; iIntros; by iApply "Howni".
@@ -120,8 +119,8 @@ Section mutex.
   Global Instance mutex_sync ty :
     Send ty → Sync (mutex ty).
   Proof.
-    iIntros (???? l) "Hshr". iDestruct "Hshr" as (γ κ') "[Hshr Hincl]".
-    iExists _, _. iFrame "Hincl". iApply (at_bor_iff with "[] Hshr"). iNext.
+    iIntros (???? l) "Hshr". iDestruct "Hshr" as (κ') "[Hincl Hshr]".
+    iExists _. iFrame "Hincl". iApply (at_bor_iff with "[] Hshr"). iNext.
     iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
     iApply heap_mapsto_pred_iff_proper.
     iAlways; iIntros; iSplit; iIntros; by iApply send_change_tid.
@@ -130,7 +129,7 @@ Section mutex.
 End mutex.
 
 Section code.
-  Context `{!typeG Σ, !lockG Σ}.
+  Context `{!typeG Σ}.
 
   Definition mutex_new ty : val :=
     funrec: <> ["x"] :=
@@ -247,5 +246,4 @@ Section code.
     iApply type_assign; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
-
 End code.

theories/typing/lib/mutex/mutexguard.v

@@ -18,7 +18,7 @@ Set Default Proof Using "Type".
 *)
 
 Section mguard.
-  Context `{!typeG Σ, !lockG Σ}.
+  Context `{!typeG Σ}.
 
   (*
     pub struct MutexGuard<'a, T: ?Sized + 'a> {
@@ -34,8 +34,8 @@ Section mguard.
        ty_own tid vl :=
          match vl return _ with
          | [ #(LitLoc l) ] =>
-           ∃ γ β, locked γ ∗ α ⊑ β ∗
-             &at{α, mutexN} (lock_proto γ l (&{β} shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
+           ∃ β, α ⊑ β ∗
+             &at{α, mutexN} (lock_proto l (&{β} shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
              &{β} (shift_loc l 1 ↦∗: ty.(ty_own) tid)
          | _ => False end;
        ty_shr κ tid l :=
@@ -53,10 +53,8 @@ Section mguard.
     destruct vl as [|[[|l'|]|][]];
       try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
     setoid_rewrite heap_mapsto_vec_singleton.
-    iMod (bor_exists with "LFT Hb") as (γ) "Hb"; first done.
     iMod (bor_exists with "LFT Hb") as (β) "Hb"; first done.
-    iMod (bor_sep with "LFT Hb") as "[Hlcked H]"; first done.
-    iMod (bor_sep with "LFT H") as "[Hαβ H]"; first done.
+    iMod (bor_sep with "LFT Hb") as "[Hαβ H]"; first done.
     iMod (bor_sep with "LFT H") as "[_ H]"; first done.
     iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]"; first done.
     iExists _. iFrame "H↦". iApply delay_sharing_nested; try done.
@@ -96,8 +94,8 @@ Section mguard.
     iIntros "!# #HE". iDestruct ("Hα" with "HE") as "{Hα} Hα".
     iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs) {HE Hty}". iSplit; [done|iSplit; iAlways].
     - iIntros (tid [|[[]|][]]) "H"; try done. simpl.
-      iDestruct "H" as (γ β) "(Hcl & #H⊑ & #Hinv & Hown)".
-      iExists γ, β. iFrame. iSplit; last iSplit.
+      iDestruct "H" as (β) "(#H⊑ & #Hinv & Hown)".
+      iExists β. iFrame. iSplit; last iSplit.
       + by iApply lft_incl_trans.
       + iApply (at_bor_shorten with "Hα").
         iApply (at_bor_iff with "[] Hinv"). iNext.
@@ -134,13 +132,13 @@ Section mguard.
 End mguard.
 
 Section code.
-  Context `{!typeG Σ, !lockG Σ}.
+  Context `{!typeG Σ}.
 
-  Lemma mutex_acc E γ l ty tid q α κ :
+  Lemma mutex_acc E l ty tid q α κ :
     ↑lftN ⊆ E → ↑mutexN ⊆ E →
     let R := (&{κ} shift_loc l 1 ↦∗: ty_own ty tid)%I in
-    lft_ctx -∗ &at{α,mutexN} lock_proto γ l R -∗ α ⊑ κ -∗
-    □ ((q).[α] ={E,∅}=∗ ▷ lock_proto γ l R ∗ (▷ lock_proto γ l R ={∅,E}=∗ (q).[α])).
+    lft_ctx -∗ &at{α,mutexN} lock_proto l R -∗ α ⊑ κ -∗
+    □ ((q).[α] ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ (q).[α])).
   Proof.
     (* FIXME: This should work: iIntros (?? R). *) intros ?? R.
     iIntros "#LFT #Hshr #Hlincl !# Htok".
@@ -168,13 +166,13 @@ Section code.
     (* Switch to Iris. *)
     iIntros (tid) "#LFT #HE Hna HL Hk [Hg [Hx [Hm _]]]".
     rewrite !tctx_hasty_val [[x]]lock /=.
-    destruct m as [[|lm|]|]; try done. iDestruct "Hm" as (γ κ') "[#Hshr #Hακ']".
+    destruct m as [[|lm|]|]; try done. iDestruct "Hm" as (κ') "[#Hακ' #Hshr]".
     iDestruct (ownptr_uninit_own with "Hg") as (lg vlg) "(% & Hg & Hg†)".
     subst g. inv_vec vlg=>g. rewrite heap_mapsto_vec_singleton.
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & HL & Hclose1)"; [solve_typing..|].
     wp_apply (acquire_spec with "[] Hα"); first by iApply (mutex_acc with "LFT Hshr Hακ'").
-    iIntros "[Hlocked [Hcont Htok]]". wp_seq. wp_op. rewrite shift_loc_0. wp_write.
+    iIntros "[Hcont Htok]". wp_seq. wp_op. rewrite shift_loc_0. wp_write.
     iMod ("Hclose1" with "Htok HL") as "HL".
     (* Switch back to typing mode. *)
     iApply (type_type _ _ _ [ x ◁ own_ptr _ _; #lg ◁ box (mutexguard α ty)]
@@ -182,7 +180,7 @@ Section code.
     (* TODO: It would be nice to say [{#}] as the last spec pattern to clear the context in there. *)
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hg".
-      iExists _, _. iFrame "#∗". }
+      iExists _. iFrame "#∗". }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -212,9 +210,7 @@ Section code.
     destruct vl as [|[[|lm|]|] [|]]; simpl;
       try by iMod (bor_persistent_tok with "LFT Hprot Hα") as "[>[] _]".
     rewrite heap_mapsto_vec_singleton.
-    iMod (bor_exists with "LFT Hprot") as (γ) "Hprot"; first done.
     iMod (bor_exists with "LFT Hprot") as (κ) "Hprot"; first done.
-    iMod (bor_sep with "LFT Hprot") as "[_ Hprot]"; first done.
     iMod (bor_sep with "LFT Hprot") as "[Hβκ Hprot]"; first done.
     iMod (bor_sep with "LFT Hprot") as "[_ Hlm]"; first done.
     iMod (bor_persistent_tok with "LFT Hβκ Hα") as "[#Hβκ Hα]"; first done.
@@ -291,11 +287,11 @@ Section code.
     (* Switch to Iris. *)
     iIntros (tid) "#LFT #HE Hna HL Hk [Hg [Hm _]]".
     rewrite !tctx_hasty_val [[g]]lock /=.
-    destruct m as [[|lm|]|]; try done. iDestruct "Hm" as (γ β) "(Hlcked & #Hαβ & #Hshr & Hcnt)".
+    destruct m as [[|lm|]|]; try done. iDestruct "Hm" as (β) "(#Hαβ & #Hshr & Hcnt)".
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & HL & Hclose1)"; [solve_typing..|].
-    wp_apply (release_spec with "[] [Hα $Hlcked Hcnt]"); first by iApply (mutex_acc with "LFT Hshr Hαβ").
-    { by iFrame. }
+    wp_apply (release_spec with "[] [Hα Hcnt]");
+      [by iApply (mutex_acc with "LFT Hshr Hαβ")|by iFrame|].
     iIntros "Htok". wp_seq. iMod ("Hclose1" with "Htok HL") as "HL".
     (* Switch back to typing mode. *)
     iApply (type_type _ _ _ [ g ◁ own_ptr _ _ ]