Mutex: Send+Sync

theories/lang/heap.v

@@ -202,6 +202,13 @@ Section heap.
     iFrame "Hm". by iApply "Hwand".
   Qed.
 
+  Lemma heap_mapsto_pred_iff_proper l q Φ1 Φ2 :
+    □ (∀ vl, Φ1 vl ↔ Φ2 vl) -∗ □ (l ↦∗{q}: Φ1 ↔ l ↦∗{q}: Φ2).
+  Proof.
+    iIntros "#HΦ !#". iSplit; iIntros; iApply (heap_mapsto_pred_wand with "[-]"); try done; [|];
+    iIntros; by iApply "HΦ".
+  Qed.
+
   Lemma heap_mapsto_vec_combine l q vl :
     vl ≠ [] →
     l ↦∗{q} vl ⊣⊢ own heap_name (◯ [^op list] i ↦ v ∈ vl,

theories/lang/lib/lock.v

@@ -44,6 +44,14 @@ Section proof.
     by iApply "HRR'".
   Qed.
 
+  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.
+    - iAlways; iSplit; iIntros; by iApply "HR".
+  Qed.
+
   (** The main proofs. *)
   Lemma lock_proto_create (R : iProp Σ) l (b : bool) :
     l ↦ #b -∗ (if b then True else ▷ R) ==∗ ∃ γ, ▷ lock_proto γ l R.

theories/typing/lib/mutex/mutex.v

@@ -99,7 +99,24 @@ Section mutex.
     constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
   Qed.
 
-  (* TODO: compat with eqtype, Send+Sync if ty is Send. *)
+  Global Instance mutex_send ty :
+    Send ty → Send (mutex ty).
+  Proof.
+    iIntros (??? [|[[| |n]|]vl]); try done. iIntros "[$ Hvl]".
+    by iApply send_change_tid.
+  Qed.
+
+  Global Instance mutex_sync ty :
+    Send ty → Sync (mutex ty).
+  Proof.
+    iIntros (???? l) "Hshr". iDestruct "Hshr" as (γ κ') "[Hshr Hincl]".
+    iExists _, _. iFrame "Hincl". iApply (shr_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.
+  Qed.
+
+  (* TODO: compat with eqtype. *)
 
 End mutex.