search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.21k stars 89 forks source link

`assess scan` execution could be parallelized #2294

Open adpaco-aws opened 1 year ago

adpaco-aws commented 1 year ago

Goto binary serialization (introduced in #2205) showed significant time/memory improvements. It's not unreasonable to think that these improvements could allow us to parallelize the assess scan feature so its execution on a set of workspaces can be done in parallel.

With this change, we would get better runtimes for assess scan (currently takes >1hr? to run the top-100 crates experiments).

celinval commented 1 year ago

You might want to be careful when we are executing the entire assess flow (i.e.: without --only-codegen). I believe assess already tries to run the test harnesses in parallel. So if scan also invokes assess using threads, we should factor in how we compute the number of threads used to run the test harnesses (or maybe disable it).

In the long run, we could leverage tokio or some thread pool to do this work and not worry about the load.