diff --git a/Cargo.lock b/Cargo.lock index 23500d2ee906..9cdf4ed56745 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -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" @@ -392,6 +437,7 @@ dependencies = [ "kani_metadata", "once_cell", "pathdiff", + "rayon", "regex", "rustc-demangle", "serde", @@ -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" @@ -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" @@ -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" diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 737eed3651a0..6a85b285d2ef 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -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 diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs index f0cdf9d97f2f..6a102195bea0 100644 --- a/kani-driver/src/args.rs +++ b/kani-driver/src/args.rs @@ -148,6 +148,10 @@ pub struct KaniArgs { // consumes everything pub cbmc_args: Vec, + /// Number of parallel jobs, defaults to 1 + #[structopt(short, long, hidden = true, requires("enable-unstable"))] + pub jobs: Option>, + // Hide option till https://github.com/model-checking/kani/issues/697 is // fixed. /// Use abstractions for the standard library. @@ -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 { + match self.jobs { + None => Some(1), // no argument, default 1 + Some(None) => None, // -j + Some(Some(x)) => Some(x), // -j=x + } + } } arg_enum! { @@ -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\ @@ -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, + )); } + if self.jobs.is_some() && self.output_format != OutputFormat::Terse { + // 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(()) } } diff --git a/kani-driver/src/call_cbmc_viewer.rs b/kani-driver/src/call_cbmc_viewer.rs index f8a61d24831f..1a4b3061778b 100644 --- a/kani-driver/src/call_cbmc_viewer.rs +++ b/kani-driver/src/call_cbmc_viewer.rs @@ -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( diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index e853fdf9abe9..d440482e7054 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -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)?; diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index a72d49933247..2a99b6ba8fb5 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -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(); diff --git a/kani-driver/src/call_symtab.rs b/kani-driver/src/call_symtab.rs index a9b427a168e1..802474c97641 100644 --- a/kani-driver/src/call_symtab.rs +++ b/kani-driver/src/call_symtab.rs @@ -12,10 +12,7 @@ impl KaniSession { pub fn symbol_table_to_gotoc(&self, file: &Path) -> Result { 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(), diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index de055b3ee09b..af6487ed53eb 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -3,6 +3,7 @@ use anyhow::Result; use kani_metadata::HarnessMetadata; +use rayon::prelude::*; use std::path::{Path, PathBuf}; use crate::call_cbmc::VerificationStatus; @@ -45,26 +46,37 @@ impl<'sess> HarnessRunner<'sess> { ) -> Result>> { 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>> { + sorted_harnesses + .par_iter() + .map(|harness| -> Result> { + 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::>>() + })?; Ok(results) } diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index ab3a0f776e23..41eecfc5bceb 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -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)?; diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index bc27c244563c..b742eca19161 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -4,10 +4,10 @@ use crate::args::KaniArgs; use crate::util::render_command; use anyhow::{bail, Context, Result}; -use std::cell::RefCell; use std::io::Write; use std::path::{Path, PathBuf}; use std::process::{Child, Command, ExitStatus, Stdio}; +use std::sync::Mutex; /// Contains information about the execution environment and arguments that affect operations pub struct KaniSession { @@ -22,7 +22,7 @@ pub struct KaniSession { pub kani_c_stubs: PathBuf, /// The temporary files we littered that need to be cleaned up at the end of execution - pub temporaries: RefCell>, + pub temporaries: Mutex>, } /// Represents where we detected Kani, with helper methods for using that information to find critical paths @@ -44,15 +44,22 @@ impl KaniSession { kani_compiler: install.kani_compiler()?, kani_lib_c: install.kani_lib_c()?, kani_c_stubs: install.kani_c_stubs()?, - temporaries: RefCell::new(vec![]), + temporaries: Mutex::new(vec![]), }) } + + pub fn record_temporary_files(&self, temps: &[&Path]) { + // unwrap safety: will panic this thread if another thread panicked *while holding the lock.* + // This is vanishingly unlikely, and even then probably the right thing to do + let mut t = self.temporaries.lock().unwrap(); + t.extend(temps.iter().map(|p| (*p).to_owned())); + } } impl Drop for KaniSession { fn drop(&mut self) { if !self.args.keep_temps && !self.args.dry_run { - let temporaries = self.temporaries.borrow(); + let temporaries = self.temporaries.lock().unwrap(); for file in temporaries.iter() { // If it fails, we don't care, skip it