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

Implement "many-seeds" mode directly in the driver? #3877

Open
RalfJung opened this issue Sep 10, 2024 · 1 comment
Open

Implement "many-seeds" mode directly in the driver? #3877

RalfJung opened this issue Sep 10, 2024 · 1 comment
Labels
A-driver Area: the Miri driver (the `miri` binary) C-cleanup Category: cleaning up our code

Comments

@RalfJung
Copy link
Member

Currently, ./miri run and cargo miri both have an independent implementation of "many-seeds" mode. The one in ./miri is concurrent, the one in cargo miri is not.

I wonder if we could avoid all that duplication by having this implemented directly in the driver instead, via something like -Zmiri-many-seeds? I can imagine two possible implementations:

  • Inside a single rustc driver session, we can spin up more than one interpreter instance -- all the relevant state is (should be) in the interpreter instance, so this will give us clean independent executions. They could even share the query cache this way. However, this would AFAIK have to be sequential -- or can we make use of "parallel rustc" support for this somehow?
  • Inside the miri binary, create multiple rustc driver sessions, each in a separate thread. I think that should be possible? Or does the rustc driver infrastructure assume that it is instantiated only once per process?

Cc @bjorn3 since you know a lot about this driver stuff, IIRC. :)
Cc @SparrowLii for parallel rustc know-how.

@oli-obk
Copy link
Contributor

oli-obk commented Sep 10, 2024

  • I think that should be possible? Or does the rustc driver infrastructure assume that it is instantiated only once per process?

Possible, we only use tls, no true globals.

But I'd prefer just using parallel rust logic to run everything in parallel. Tho that may run into the various issues parallel rustc still has

@RalfJung RalfJung added C-cleanup Category: cleaning up our code A-driver Area: the Miri driver (the `miri` binary) labels Sep 17, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-driver Area: the Miri driver (the `miri` binary) C-cleanup Category: cleaning up our code
Projects
None yet
Development

No branches or pull requests

2 participants