From f4a672cf66e473034f25bb4400fd05cf7cb4df53 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 28 Apr 2017 17:05:41 +0200
Subject: [PATCH] Mutex: Send+Sync

---
 theories/lang/heap.v              |  7 +++++++
 theories/lang/lib/lock.v          |  8 ++++++++
 theories/typing/lib/mutex/mutex.v | 19 ++++++++++++++++++-
 3 files changed, 33 insertions(+), 1 deletion(-)

diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 65b01d93..58df7d54 100644
--- a/theories/lang/heap.v
+++ b/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,
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index 74c6b1c9..9e0eaa53 100644
--- a/theories/lang/lib/lock.v
+++ b/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.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 8d83630d..cd9a1409 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/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.
 
-- 
GitLab