Introduce (experimental, unstable) parallel runner for proof harnesses #1726
Conversation
zhassan-aws
left a comment
zhassan-aws
left a comment
There was a problem hiding this comment.
Nice! Just have a couple of comments.
| ErrorKind::ArgumentConflict, | ||
| )); | ||
| } | ||
| if self.jobs.is_some() && self.output_format != OutputFormat::Terse { |
There was a problem hiding this comment.
It would be more convenient to automatically switch to terse mode (which we want to switch to anyway) when jobs is specified.
There was a problem hiding this comment.
I thought about it, but:
- The real problem is there's nowhere to put that code. e.g. this function doesn't take
&mutand shouldn't. - But I also felt like being annoying for the moment is fine until we stabilize, and I'm planning on fixing this issue soon as well.
adpaco-aws
left a comment
adpaco-aws
left a comment
There was a problem hiding this comment.
Can you consider this couple of comments in your next PR?
| match self.jobs { | ||
| None => Some(1), // no argument, default 1 | ||
| Some(None) => None, // -j | ||
| Some(Some(x)) => Some(x), // -j=x |
There was a problem hiding this comment.
Isn't it worth to create an enum for all these options? Something like:
enum JobParalellism {
Single,
Multiple(Option<u32>),
}
There was a problem hiding this comment.
The double option in the args is a bit confusing imo, but is idiomatic there.
The option it returns exactly corresponds to calling num_threads on the thread pool (none means no, some means yes with this value), so I thought that was clear.
| if self.concrete_playback.is_some() && self.jobs() != Some(1) { | ||
| // Concrete playback currently embeds a lot of assumptions about the order in which harnesses get called. | ||
| return Err(Error::with_description( | ||
| "Conflicting options: --concrete-playback isn't compatible with --jobs.", | ||
| ErrorKind::ArgumentConflict, | ||
| )); |
There was a problem hiding this comment.
Can't these conflicts be specified as an annotation in KaniArgs fields? Not clear to me why we handle them here.
There was a problem hiding this comment.
Only partially. This allows -j1 to work fine for instance, and is more durable if we end up wanting to change the default to num_cpus later, but still need to require single threaded for concrete-playback. (Though hopefully we'll fix that first...)
(Basically this is a semantic check: note the () on self.jobs(), rather than just a syntactic check that conflicts would perform.)
3 participants
Description of changes:
What it says on the tin. :) Takes a 24s artificial benchmark down to under 4s to run.
cargo build:--jobsor-j. Default is 1. Default with just-jis num_cpus.--output-format=terse. And--enable-unstableof course.There is the problem of output. We actually don't have a huge problem with interleaving output because Adrian already wrote the renderer to print one big blob instead of multiple little ones. (Nice!) However, we do still have #1711 that this exacerbates, and the "verification time" isn't really paired with an output anymore. I think this is merge-able as-is, but I do plan on an independent PR to fix up that issue tomorrow, which it might be reasonable to want merged first.
Call-outs:
Changes include:
--jobsoption tokani-driverKaniSession'sRefCellwith aMutex(and addingrecord_temporary_files)fortorayonpar_iterand that's it! It's actually a pretty simple change now. Sweet.
Testing:
How is this change tested? existing ci: all lines of code actually run by default, just without setting
jhigher than 1Is this a refactor change? no
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.