Experimental concurrency support #730
Conversation
for concurrency in crucible/crux based tools.
crucible::concurrency. Exposes a feature to control the fidelity of the translation, and allows the user to select this feature in `translate_libs.sh`. This initial support is highly experimental.
Co-authored-by: Ryan Scott <[email protected]>
There was a problem hiding this comment.
I guess it's the plural of crucible (multiple threads, etc...).
Gotcha. I suppose my confusion was rooted in that I kept trying to interpret "Crucibles" as "multiple instances of Crucible" rather than as a separate name altogether. For whatever reason, I didn't seem to have the same issue with Crux versus Cruces—I guess the use of Spanish/Latin adds its own distinct flair :)
In any case, I appreciate the footnote you've added to the README.
refers to this package.
…e switching to Crux.)
There was a problem hiding this comment.
This is really an impressive bit of work! I appreciate the design notes and the number of tests and benchmarks you included. I didn't deeply review most of the Haskell code, since a lot of it implements algorithms I'm not very familiar with, but it looks good from what I can tell (though I did notice a few bits of commented-out code that could probably be removed).
| const fn new() { | ||
| AtomicBool { | ||
| //... | ||
| id: crucible::concurrency::nonce(), //Not allowed in a const context |
There was a problem hiding this comment.
One option if you need to work around this is to change the field to id: Cell<Option<usize>> and assign a nonce on first use. I'm not sure whether this fits with the requirement that "the same resource has the same name across several executions", since I think it would make the naming depend on what order the first access to each variable happens in, which could depend on what order threads start up in.
Another option is to use a hack to run code on initialization, like we do for Bv: Rust side, Haskell side. The idea would be to define struct Nonce(u64); with an initializer containing a marker value like const NONCE_INIT: Nonce = Nonce(0xffff_ffff_ffff_ffff). Then recognize the nonce type and marker value in transConstVal and replace it with Crucible code to generate a fresh nonce (this might require a custom Crucible instruction). I'm not 100% sure whether this trick would work here, since for Nonce (unlike for Bv) it actually matters how many times the constant gets evaluated.
|
I only looked at the crux-mir parts, but overall those parts look good. My only real worry is the |
symbolic of course).
This is explained by some additional notes related to using `MirReferece`s as the basis for resource names.
…due to the usual state explosion issues.
Also adapt `cabal.project`.
Also adapt `cabal.project`.
Also add new packages to `cabal.project`. Also update megaparsec version in freeze files to make `crucible-syntax` happy.
The main purpose of this PR is to:
crucible-concurrency, a library used to add concurrency support for crucible-based tools. Notes on designs, limitations, future work, etc are included inDesignNotes.mdin thecrucible-concurrencysubdirectory.crux-mirusing the above. Notes on this implementation are included inConcurrency.mdin thecrux-mirsubdirectory. The changes broadly consist of a new moduleMir.Concurrency, as well as some changes to the Rust libraries shipped with the tool (i.e., those underlib).crucible-concurrencyships with an implementation forcrucible-syntax: hence, this PR also includes some minor changes tocrucible-syntaxto make it a bit more useful as a library, and also to fix a small issue with its entry block construction.