From 4a90389fcd0d201f639700772c25badfa3702ee2 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 28 Apr 2017 16:28:50 +0200
Subject: [PATCH] Guards for rwlock are sync.

---
 theories/typing/lib/rwlock/rwlockreadguard.v  | 10 +++++++++-
 theories/typing/lib/rwlock/rwlockwriteguard.v | 11 ++++++++++-
 2 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index e21b832d..64ae740d 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -113,7 +113,15 @@ Section rwlockreadguard.
     eqtype E L (rwlockreadguard α1 ty1) (rwlockreadguard α2 ty2).
   Proof. intros. by eapply rwlockreadguard_proper. Qed.
 
-  (* TODO: In Rust, the read guard is Sync if ty is Send+Sync. *)
+  Global Instance rwlockreadguard_sync α ty :
+    Sync ty → Sync (rwlockreadguard α ty).
+  Proof.
+    move=>?????/=. apply uPred.exist_mono=>?. by rewrite sync_change_tid.
+  Qed.
+
+  (* Probably for reasons related to the underlying representation,
+     Rust does not implement Send for RwLockWriteGuard. We could prove
+     this. *)
 End rwlockreadguard.
 
 Hint Resolve rwlockreadguard_mono' rwlockreadguard_proper' : lrust_typing.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 985ed87d..b439613c 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -116,7 +116,16 @@ Section rwlockwriteguard.
     eqtype E L (rwlockwriteguard α1 ty1) (rwlockwriteguard α2 ty2).
   Proof. intros. by eapply rwlockwriteguard_proper. Qed.
 
-  (* TODO: In Rust, the write guard is Sync if ty is Send+Sync. *)
+  Global Instance rwlockwriteguard_sync α ty :
+    Sync ty → Sync (rwlockwriteguard α ty).
+  Proof.
+    move=>?????/=. apply uPred.exist_mono=>?. do 6 f_equiv.
+    by rewrite sync_change_tid.
+  Qed.
+
+  (* Probably for reasons related to the underlying representation,
+     Rust does not implement Send for RwLockWriteGuard. We could prove
+     this. *)
 End rwlockwriteguard.
 
 Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.
-- 
GitLab