Skip to content
New issue

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

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

Already on GitHub? Sign in 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)

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