Skip to content

Introduce (experimental, unstable) parallel runner for proof harnesses #1726

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.

Sign up for GitHub

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

Merged
merged 2 commits into from
Sep 28, 2022
Merged

Introduce (experimental, unstable) parallel runner for proof harnesses #1726

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8291750
Introduce (experimental, unstable) parallel runner for proof harnesses
tedinski Sep 16, 2022
2b70065
fix new argument documentation
tedinski Sep 28, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
89 changes: 89 additions & 0 deletions Cargo.lock
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -242,6 +242,51 @@ dependencies = [
"cfg-if",
]

[[package]]
name = "crossbeam-channel"
version = "0.5.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "c2dd04ddaf88237dc3b8d8f9a3c1004b506b54b3313403944054d23c0870c521"
dependencies = [
"cfg-if",
"crossbeam-utils",
]

[[package]]
name = "crossbeam-deque"
version = "0.8.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "715e8152b692bba2d374b53d4875445368fdf21a94751410af607a5ac677d1fc"
dependencies = [
"cfg-if",
"crossbeam-epoch",
"crossbeam-utils",
]

[[package]]
name = "crossbeam-epoch"
version = "0.9.10"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "045ebe27666471bb549370b4b0b3e51b07f56325befa4284db65fc89c02511b1"
dependencies = [
"autocfg",
"cfg-if",
"crossbeam-utils",
"memoffset",
"once_cell",
"scopeguard",
]

[[package]]
name = "crossbeam-utils"
version = "0.8.11"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "51887d4adc7b564537b15adcfb307936f8075dfcd5f00dde9a9f1d29383682bc"
dependencies = [
"cfg-if",
"once_cell",
]

[[package]]
name = "either"
version = "1.8.0"
Expand Down Expand Up @@ -392,6 +437,7 @@ dependencies = [
"kani_metadata",
"once_cell",
"pathdiff",
"rayon",
"regex",
"rustc-demangle",
"serde",
Expand Down Expand Up @@ -490,6 +536,15 @@ version = "2.5.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d"

[[package]]
name = "memoffset"
version = "0.6.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5aa361d4faea93603064a027415f07bd8e1d5c88c9fbf68bf56a285428fd79ce"
dependencies = [
"autocfg",
]

[[package]]
name = "num"
version = "0.4.0"
Expand Down Expand Up @@ -566,6 +621,16 @@ dependencies = [
"autocfg",
]

[[package]]
name = "num_cpus"
version = "1.13.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "19e64526ebdee182341572e50e9ad03965aa510cd94427a4549448f285e957a1"
dependencies = [
"hermit-abi",
"libc",
]

[[package]]
name = "object"
version = "0.29.0"
Expand Down Expand Up @@ -688,6 +753,30 @@ dependencies = [
"proc-macro2",
]

[[package]]
name = "rayon"
version = "1.5.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "bd99e5772ead8baa5215278c9b15bf92087709e9c1b2d1f97cdb5a183c933a7d"
dependencies = [
"autocfg",
"crossbeam-deque",
"either",
"rayon-core",
]

[[package]]
name = "rayon-core"
version = "1.9.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "258bcdb5ac6dad48491bb2992db6b7cf74878b0384908af124823d118c99683f"
dependencies = [
"crossbeam-channel",
"crossbeam-deque",
"crossbeam-utils",
"num_cpus",
]

[[package]]
name = "redox_syscall"
version = "0.2.16"
Expand Down
1 change: 1 addition & 0 deletions kani-driver/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ toml = "0.5"
regex = "1.6"
rustc-demangle = "0.1.21"
pathdiff = "0.2.1"
rayon = "1.5.3"

# A good set of suggested dependencies can be found in rustup:
# https://github.com/rust-lang/rustup/blob/master/Cargo.toml
Expand Down
58 changes: 44 additions & 14 deletions kani-driver/src/args.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -148,6 +148,10 @@ pub struct KaniArgs {
// consumes everything
pub cbmc_args: Vec<OsString>,

#[structopt(short, long, requires("enable-unstable"))]
// consumes everything
pub jobs: Option<Option<usize>>,

// Hide option till https://github.com/model-checking/kani/issues/697 is
// fixed.
/// Use abstractions for the standard library.
Expand Down Expand Up @@ -226,6 +230,15 @@ impl KaniArgs {
Some(DEFAULT_OBJECT_BITS)
}
}

/// Computes how many threads should be used to verify harnesses.
pub fn jobs(&self) -> Option<usize> {
match self.jobs {
None => Some(1), // no argument, default 1
Some(None) => None, // -j
Some(Some(x)) => Some(x), // -j=x
Comment on lines +236 to +239
Copy link
Contributor

@adpaco-aws adpaco-aws Sep 28, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't it worth to create an enum for all these options? Something like:

enum JobParalellism {
    Single,
    Multiple(Option<u32>),
}

Copy link
Contributor Author

@tedinski tedinski Sep 28, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

}
}
}

arg_enum! {
Expand Down Expand Up @@ -365,7 +378,6 @@ impl KaniArgs {
String::new()
};

// `tracing` is not a dependency of `kani-driver`, so we println! here instead.
println!(
"Using concrete playback with --randomize-layout.\n\
The produced tests will have to be played with the same rustc arguments:\n\
Expand All @@ -377,29 +389,47 @@ impl KaniArgs {
// TODO: these conflicting flags reflect what's necessary to pass current tests unmodified.
// We should consider improving the error messages slightly in a later pull request.
if natives_unwind && extra_unwind {
Err(Error::with_description(
return Err(Error::with_description(
"Conflicting flags: unwind flags provided to kani and in --cbmc-args.",
ErrorKind::ArgumentConflict,
))
} else if self.cbmc_args.contains(&OsString::from("--function")) {
Err(Error::with_description(
));
}
if self.cbmc_args.contains(&OsString::from("--function")) {
return Err(Error::with_description(
"Invalid flag: --function should be provided to Kani directly, not via --cbmc-args.",
ErrorKind::ArgumentConflict,
))
} else if self.quiet && self.concrete_playback == Some(ConcretePlaybackMode::Print) {
Err(Error::with_description(
));
}
if self.quiet && self.concrete_playback == Some(ConcretePlaybackMode::Print) {
return Err(Error::with_description(
"Conflicting options: --concrete-playback=print and --quiet.",
ErrorKind::ArgumentConflict,
))
} else if self.concrete_playback.is_some() && self.output_format == OutputFormat::Old {
Err(Error::with_description(
));
}
if self.concrete_playback.is_some() && self.output_format == OutputFormat::Old {
return Err(Error::with_description(
"Conflicting options: --concrete-playback isn't compatible with \
--output-format=old.",
ErrorKind::ArgumentConflict,
))
} else {
Ok(())
));
}
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,
));
Comment on lines +416 to +421
Copy link
Contributor

@adpaco-aws adpaco-aws Sep 28, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can't these conflicts be specified as an annotation in KaniArgs fields? Not clear to me why we handle them here.

Copy link
Contributor Author

@tedinski tedinski Sep 28, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.)

}
if self.jobs.is_some() && self.output_format != OutputFormat::Terse {
Copy link
Contributor

@zhassan-aws zhassan-aws Sep 28, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be more convenient to automatically switch to terse mode (which we want to switch to anyway) when jobs is specified.

Copy link
Contributor Author

@tedinski tedinski Sep 28, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I thought about it, but:

  1. The real problem is there's nowhere to put that code. e.g. this function doesn't take &mut and shouldn't.
  2. 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.

Copy link
Contributor

@zhassan-aws zhassan-aws Sep 28, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK.

// More verbose output formats make it hard to interpret output right now when run in parallel.
// This can be removed when we change up how results are printed.
return Err(Error::with_description(
"Conflicting options: --jobs requires `--output-format=terse`",
ErrorKind::ArgumentConflict,
));
}

Ok(())
}
}

Expand Down
7 changes: 1 addition & 6 deletions kani-driver/src/call_cbmc_viewer.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,12 +23,7 @@ impl KaniSession {
let coverage_filename = alter_extension(file, "coverage.xml");
let property_filename = alter_extension(file, "property.xml");

{
let mut temps = self.temporaries.borrow_mut();
temps.push(results_filename.clone());
temps.push(coverage_filename.clone());
temps.push(property_filename.clone());
}
self.record_temporary_files(&[&results_filename, &coverage_filename, &property_filename]);

self.cbmc_variant(file, &["--xml-ui", "--trace"], &results_filename, harness_metadata)?;
self.cbmc_variant(
Expand Down
5 changes: 1 addition & 4 deletions kani-driver/src/call_goto_instrument.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,10 +64,7 @@ impl KaniSession {
pub fn apply_vtable_restrictions(&self, file: &Path, source: &Path) -> Result<()> {
let linked_restrictions = alter_extension(file, "linked-restrictions.json");

{
let mut temps = self.temporaries.borrow_mut();
temps.push(linked_restrictions.clone());
}
self.record_temporary_files(&[&linked_restrictions]);

collect_and_link_function_pointer_restrictions(source, &linked_restrictions)?;

Expand Down
17 changes: 8 additions & 9 deletions kani-driver/src/call_single_file.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,15 +33,14 @@ impl KaniSession {
let restrictions_filename = alter_extension(file, "restrictions.json");
let rlib_filename = guess_rlib_name(file);

{
let mut temps = self.temporaries.borrow_mut();
temps.push(rlib_filename);
temps.push(output_filename.clone());
temps.push(typemap_filename);
temps.push(metadata_filename.clone());
if self.args.restrict_vtable() {
temps.push(restrictions_filename.clone());
}
self.record_temporary_files(&[
&rlib_filename,
&output_filename,
&typemap_filename,
&metadata_filename,
]);
if self.args.restrict_vtable() {
self.record_temporary_files(&[&restrictions_filename]);
}

let mut kani_args = self.kani_specific_flags();
Expand Down
5 changes: 1 addition & 4 deletions kani-driver/src/call_symtab.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,7 @@ impl KaniSession {
pub fn symbol_table_to_gotoc(&self, file: &Path) -> Result<PathBuf> {
let output_filename = file.with_extension("out");

{
let mut temps = self.temporaries.borrow_mut();
temps.push(output_filename.clone());
}
self.record_temporary_files(&[&output_filename]);

let args = vec![
file.to_owned().into_os_string(),
Expand Down
50 changes: 31 additions & 19 deletions kani-driver/src/harness_runner.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@

use anyhow::Result;
use kani_metadata::HarnessMetadata;
use rayon::prelude::*;
use std::path::{Path, PathBuf};

use crate::call_cbmc::VerificationStatus;
Expand Down Expand Up @@ -45,26 +46,37 @@ impl<'sess> HarnessRunner<'sess> {
) -> Result<Vec<HarnessResult<'a>>> {
let sorted_harnesses = crate::metadata::sort_harnesses_by_loc(harnesses);

let mut results = vec![];

for harness in &sorted_harnesses {
let harness_filename = harness.pretty_name.replace("::", "-");
let report_dir = self.report_base.join(format!("report-{}", harness_filename));
let specialized_obj = specialized_harness_name(self.linked_obj, &harness_filename);
if !self.retain_specialized_harnesses {
let mut temps = self.sess.temporaries.borrow_mut();
temps.push(specialized_obj.to_owned());
let pool = {
let mut builder = rayon::ThreadPoolBuilder::new();
if let Some(x) = self.sess.args.jobs() {
builder = builder.num_threads(x);
}
self.sess.run_goto_instrument(
self.linked_obj,
&specialized_obj,
self.symtabs,
&harness.mangled_name,
)?;

let result = self.sess.check_harness(&specialized_obj, &report_dir, harness)?;
results.push(HarnessResult { harness, result });
}
builder.build()?
};

let results = pool.install(|| -> Result<Vec<HarnessResult<'a>>> {
sorted_harnesses
.par_iter()
.map(|harness| -> Result<HarnessResult<'a>> {
let harness_filename = harness.pretty_name.replace("::", "-");
let report_dir = self.report_base.join(format!("report-{}", harness_filename));
let specialized_obj =
specialized_harness_name(self.linked_obj, &harness_filename);
if !self.retain_specialized_harnesses {
self.sess.record_temporary_files(&[&specialized_obj]);
}
self.sess.run_goto_instrument(
self.linked_obj,
&specialized_obj,
self.symtabs,
&harness.mangled_name,
)?;

let result = self.sess.check_harness(&specialized_obj, &report_dir, harness)?;
Ok(HarnessResult { harness, result })
})
.collect::<Result<Vec<_>>>()
})?;

Ok(results)
}
Expand Down
5 changes: 1 addition & 4 deletions kani-driver/src/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,10 +88,7 @@ fn standalone_main() -> Result<()> {
}

let linked_obj = util::alter_extension(&args.input, "out");
{
let mut temps = ctx.temporaries.borrow_mut();
temps.push(linked_obj.to_owned());
}
ctx.record_temporary_files(&[&linked_obj]);
ctx.link_goto_binary(&[goto_obj], &linked_obj)?;
if let Some(restriction) = outputs.restrictions {
ctx.apply_vtable_restrictions(&linked_obj, &restriction)?;
Expand Down
Loading