-
Notifications
You must be signed in to change notification settings - Fork 12.7k
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
Concurrency primitives in sync.rs with static enforcement. #3145
Comments
Regarding the immutability properties, I believe this scheme will work. |
It looks like both the condvar and the downgrade token can have a region pointer inside and thus be prevented from escaping. 904a74e (sync-cond-shouldnt-escape.rs) demonstrates this. |
This is done. It should go without saying that pipes are still the preferred communication mechanism when they will suffice - after all, these are implemented on top of pipes. |
CI: only run unit tests for `crater`
give some more help for the unusual data races Fixes rust-lang/miri#3142
Prior to this commit, errors thrown when evaluating the text of a benchcomp extra column would crash benchcomp. This could happen, for example, if a column tries to compare an old variant with a new one, but no data for the old variant exists, as seen in this run: https://github.com/model-checking/kani/actions/runs/8700040930/job/23859607740 Forcing the user to do error handling in the column text would make the text even more unwieldy than it already is, so this commit makes the column text evaluate to **<ERROR>** if an exception is raised during evaluation. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
These will serve as enhanced versions of
arc::exclusive
. The plan is formutex_arc
to be the same asexclusive
, but scheduler enabled, and come equipped with a working condition variable. It is marked unsafe because you can still create cycles with it (benefit: you can nest them).rw_arc
is somewhat more advanced, and notably more safe. Theconst
serves two purposes - it allows handing out immutable references while in read mode (just likearc::arc
does today), and it also prevents nesting them inside each other, since they won't be const themselves.I am also thinking of exposing semaphores, with
acquire
andrelease
and potentially alsocond_wait
andcond_signal
. These wouldn't protect anything themselves, but could perhaps be used to synchronise beyond-rust shared resources, such as the filesystem.Proposed interface:
A couple points:
rust_cond_lock
very-unsafely provided in the past.cvar example:
read_mode
andwrite_mode
are linear tokens that allow you to access the state, and downgrade consumes the write mode. This allows you atomically downgrade without releasing the lock, while statically enforcing no mutation after the downgrade.Downgrade example:
In particular, I would like confirmation that my understanding of region pointers will enforce the im/mutability properties.
The text was updated successfully, but these errors were encountered: