From fb244ed311c652a2607959748f808610462cf7da Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 29 Apr 2017 00:25:46 +0200
Subject: [PATCH] MutexGuard Sync bound

---
 theories/typing/lib/mutex/mutexguard.v | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index a150166d..d3f1762e 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -88,9 +88,18 @@ Section mguard.
   Global Instance mutexguard_ne α : NonExpansive (mutexguard α).
   Proof. apply type_contractive_ne, _. Qed.
 
-  (* TODO: compat with lft_incl and eqtype.
-     MutexGuard is Sync if T is Send. *)
+  (* TODO: compat with lft_incl and eqtype. *)
 
+  Global Instance mutexguard_sync α ty :
+    Sync ty → Sync (mutexguard α ty).
+  Proof.
+    move=>?????/=. apply uPred.exist_mono=>?. do 6 f_equiv.
+    by rewrite sync_change_tid.
+  Qed.
+
+  (* POSIX requires the unlock to occur from the thread that acquired
+     the lock, so Rust does not implement Send for RwLockWriteGuard. We could
+     prove this. *)
 End mguard.
 
 Section code.
-- 
GitLab