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

tedinski · web-flow · commit 21ceaa2d4a38 · 2022-09-28T14:16:11.000-05:00
diff --git 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
@@ -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
@@ -148,6 +148,10 @@ pub struct KaniArgs {
     // consumes everything
     pub cbmc_args: Vec<OsString>,
 
+    /// Number of parallel jobs, defaults to 1
+    #[structopt(short, long, hidden = true, requires("enable-unstable"))]
+    pub jobs: Option<Option<usize>>,
+
     // 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<usize> {
+        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
@@ -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
@@ -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
@@ -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
@@ -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(),
diff --git 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<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)
     }
diff --git 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
