From 1b16dbbeae627df2efd70da988aec64ceb5a55ea Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 28 Apr 2017 16:44:02 +0200
Subject: [PATCH] refine comments
---
theories/typing/lib/rwlock/rwlockreadguard.v | 6 +++---
theories/typing/lib/rwlock/rwlockwriteguard.v | 6 +++---
2 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 64ae740d..1eb2b274 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -119,9 +119,9 @@ Section rwlockreadguard.
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. *)
+ (* 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 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 b439613c..04b3c8c4 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -123,9 +123,9 @@ Section rwlockwriteguard.
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. *)
+ (* 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 rwlockwriteguard.
Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.
--
GitLab