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

crux-mir: Restore --no-model-internal-atomics #1148

Open
RyanGlScott opened this issue Dec 5, 2023 · 0 comments
Open

crux-mir: Restore --no-model-internal-atomics #1148

RyanGlScott opened this issue Dec 5, 2023 · 0 comments
Labels
crucible-concurrency Issues related to crucible-concurrency or cruces crux enhancement MIR Issues relating to Rust/MIR support testing

Comments

@RyanGlScott
Copy link
Contributor

#730 originally added a flag to crux-mir's translate_libs.sh script to build it in a way such that different thread interleavings are not modeled:

Some library types, such as `std::sync::Arc`, use atomic primitives internally.
Naively exploring all thread interleavings due to executing these atomic load
and store instructions (currently) introduces a significiant performance
penalty, as the number of thread interleavings explodes. To avoid exploring
these interleavings (which should generally be unobservable), we can generate a
version of the libraries where these particular atomics are not modeled via:
$ ./translate_libs.sh --no-model-internal-atomics

Unfortunately, I overlooked the existence of this --no-model-internal-atomics flag when I worked on #1096, and as such, #1096 accidentally removed the flag altogether. What's more, I was not aware of this because the concurrency-related parts of crux-mir are not extensively tested in the CI. We should:

  1. Restore the flag, and
  2. Add some test cases that demonstrate it.
@RyanGlScott RyanGlScott added enhancement crux testing MIR Issues relating to Rust/MIR support crucible-concurrency Issues related to crucible-concurrency or cruces labels Dec 5, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
crucible-concurrency Issues related to crucible-concurrency or cruces crux enhancement MIR Issues relating to Rust/MIR support testing
Projects
None yet
Development

No branches or pull requests

1 participant