https://github.com/GaloisInc/crucible/pull/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:
Unfortunately, I overlooked the existence of this --no-model-internal-atomics flag when I worked on https://github.com/GaloisInc/crucible/pull/1096, and as such, https://github.com/GaloisInc/crucible/pull/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:
https://github.com/GaloisInc/crucible/pull/730 originally added a flag to
crux-mir'stranslate_libs.shscript to build it in a way such that different thread interleavings are not modeled:https://github.com/GaloisInc/crucible/blob/a8839cda3f1570ff921237ce48606a006cd26e0a/crux-mir/Concurrency.md?plain=1#L15-L22
Unfortunately, I overlooked the existence of this
--no-model-internal-atomicsflag when I worked on https://github.com/GaloisInc/crucible/pull/1096, and as such, https://github.com/GaloisInc/crucible/pull/1096 accidentally removed the flag altogether. What's more, I was not aware of this because the concurrency-related parts ofcrux-mirare not extensively tested in the CI. We should: