-
Notifications
You must be signed in to change notification settings - Fork 13.4k
Is deadlock unsafe? #2821
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
Comments
Perhaps we could implement |
Also, I believe that the use of unsafe here is appropriate. It's not because the |
@pcwalton mentioned this morning that if we get message passing fast enough, we might be able to do mutable state as a task where all messages sent to it have a yield-to-target mode. It'd let us remove |
Exclusives will always be unsafe because putting exclusives inside of exclusives can result in exchange heap leaks. Yet exclusives-in-exclusives might be desirable in some cases, so even if we could use the type system to prevent it (which seems infeasible), we shouldn't. Conclusion: They stay unsafe. |
Update CBMC version to 5.94 and change our regression script to read the values from kani-dependencies instead of requiring us to keep two sources of truth.
arc::exclusive is marked unsafe because it can deadlock trivially. But it's not too hard to use comm::port to deadlock too, and marking our core communication mechanism as unsafe is probably unwise.
Before removing the unsafe tag from exclusive.with(), though, perhaps we should think up a way to use borrowck to enforce that you don't call with within a with on the same exclusive (or maybe make them support recursive locking!!). Of course we can't statically prevent multi-exclusive deadlock, but the trivial ones might be doable.
The text was updated successfully, but these errors were encountered: