Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Fix bounds on Send and Sync impls for lock guards #262

Merged
merged 1 commit into from
Nov 17, 2020
Merged

Conversation

Amanieu
Copy link
Owner

@Amanieu Amanieu commented Nov 17, 2020

Fixes #258
Fixes #259

@Amanieu Amanieu merged commit 7de94f9 into master Nov 17, 2020
@Amanieu Amanieu deleted the guard_sync branch November 17, 2020 23:39
@ammaraskar
Copy link

Thank you! ❤️

@RalfJung
Copy link
Contributor

RalfJung commented Nov 21, 2020

I have looked at this in our formal soundness proof of (idealized) Mutex and RwLock implementations. I can confirm that T: Send implies MutexGuard<T>: Send.

However, for RwLock, things are more tricky. The way we have set up the proofs, we need both T: Send and T: Sync to show that either of the guards is Send. However, I think that is just an artifact of out proof -- I agree that these ought to be sound.

@jhjourdan
Copy link

I had a more precise look on the formal proofs than @RalfJung did, and it turns out that indeed, it is safe to:

  • make the read guard both Send and Sync as soon as T : Sync,
  • make the write guard Send as soon as T : Send,
  • make the write guard Sync as soon as T : Sync.

@RalfJung
Copy link
Contributor

IOW, the read guard behaves like a shared reference and the write guard behaves like a mutable reference. Exactly what one would expect. Thanks @jhjourdan!

@ammaraskar
Copy link

Thanks for double-checking and formally proving this Ralf and Jacques. Good to see that this matches the intuition from #258 (comment)

# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
4 participants