Autoharness: verify harnesses in parallel by default

docs/src/reference/experimental/autoharness.md

@@ -79,16 +79,36 @@ Autoharness also accepts a `--list` argument, which runs the [list subcommand](.
 
 For a full list of options, run `kani autoharness --help`.
 
+### Parallel verification
+
+Since autoharness typically generates many harnesses, it verifies them in parallel by default,
+i.e. as if `--jobs` (the thread pool's default number of threads, normally one per logical CPU)
+and `--output-format=terse` had been passed. Note that plain `kani`/`cargo kani` verification is
+unaffected and remains sequential by default.
+
+To override the default:
+- `-j <N>` / `--jobs=<N>` caps the number of harnesses verified concurrently. Each thread runs
+  its own CBMC process, so peak memory grows with the number of threads; lower `<N>` if a run
+  exhausts the available memory. `--jobs=1` keeps the terse output but verifies sequentially.
+- `--output-format=regular` verifies harnesses sequentially, with Kani's default, more detailed
+  per-check output. (Parallel verification requires terse output, because interleaved detailed
+  output is hard to read; passing `--jobs` together with `--output-format=regular` is therefore
+  an error.)
+
+In parallel runs each harness result line is prefixed with the thread that produced it, and
+results arrive in nondeterministic order; the summary table printed at the end is always sorted.
+
 ## Example
 Using the `estimate_size` example from [First Steps](../../tutorial-first-steps.md) again:
 ```rust
 {{#include ../../tutorial/first-steps-v1/src/lib.rs:code}}
 ```
 
-We get:
+We get (passing `--output-format=regular` so that the per-check detail is shown, c.f.
+[Parallel verification](#parallel-verification)):
 
 ```
-# cargo kani autoharness -Z autoharness
+# cargo kani autoharness -Z autoharness --output-format=regular
 Autoharness: Checking function estimate_size against all possible inputs...
 RESULTS:
 Check 3: estimate_size.assertion.1

kani-driver/src/args/mod.rs

@@ -338,9 +338,11 @@ pub struct VerificationArgs {
     #[arg(long, hide_short_help = true)]
     pub only_codegen: bool,
 
-    /// Toggle between different styles of output
-    #[arg(long, default_value = "regular", ignore_case = true, value_enum)]
-    pub output_format: OutputFormat,
+    /// Toggle between different styles of output. Defaults to "regular", except for
+    /// `autoharness`, which defaults to "terse" (to support parallel harness verification,
+    /// c.f. `--jobs`) unless this option is passed explicitly.
+    #[arg(long, ignore_case = true, value_enum)]
+    pub output_format: Option<OutputFormat>,
 
     /// Write verification results into per-harness files, rather than to stdout
     #[arg(long, hide_short_help = true)]
@@ -499,6 +501,31 @@ impl VerificationArgs {
         }
     }
 
+    /// The output format, defaulting to `regular` when the user did not specify one.
+    pub fn output_format(&self) -> OutputFormat {
+        self.output_format.unwrap_or(OutputFormat::Regular)
+    }
+
+    /// Default to parallel harness verification with terse output for `autoharness`, which
+    /// typically generates hundreds of harnesses; sequential verification is a poor fit.
+    ///
+    /// Explicit user choices are preserved: `--output-format` is only defaulted when the user
+    /// did not pass it, and `--jobs` is only defaulted when the user did not pass it *and* the
+    /// resulting format is `terse` (parallel verification requires terse output, c.f.
+    /// `validate`). Consequently `--output-format=regular` (or `old`) opts back into sequential
+    /// verification, while a bare `--jobs=N` still gets the terse output it needs.
+    ///
+    /// This must run *before* argument validation, so that validation sees the options the run
+    /// will actually use; it is idempotent, so calling it again later is harmless.
+    pub fn apply_autoharness_parallel_defaults(&mut self) {
+        if self.output_format.is_none() {
+            self.output_format = Some(OutputFormat::Terse);
+        }
+        if self.jobs.is_none() && self.output_format() == OutputFormat::Terse {
+            self.jobs = Some(None); // `-j`: the thread pool's default thread count
+        }
+    }
+
     /// Computes how many threads should be used to verify harnesses.
     pub fn jobs(&self) -> NumThreads {
         match self.jobs {
@@ -528,7 +555,7 @@ pub enum ConcretePlaybackMode {
     InPlace,
 }
 
-#[derive(Clone, Debug, PartialEq, Eq, ValueEnum)]
+#[derive(Clone, Copy, Debug, PartialEq, Eq, ValueEnum)]
 pub enum OutputFormat {
     Regular,
     Terse,
@@ -796,14 +823,14 @@ impl ValidateArgs for VerificationArgs {
                     "Conflicting options: --concrete-playback=print and --quiet.",
                 ));
             }
-            if self.concrete_playback.is_some() && self.output_format == OutputFormat::Old {
+            if self.concrete_playback.is_some() && self.output_format() == OutputFormat::Old {
                 return Err(Error::raw(
                     ErrorKind::ArgumentConflict,
                     "Conflicting options: --concrete-playback isn't compatible with \
                 --output-format=old.",
                 ));
             }
-            if self.sarif.is_some() && self.output_format == OutputFormat::Old {
+            if self.sarif.is_some() && self.output_format() == OutputFormat::Old {
                 return Err(Error::raw(
                     ErrorKind::ArgumentConflict,
                     "Conflicting options: --sarif isn't compatible with --output-format=old.",
@@ -812,7 +839,7 @@ impl ValidateArgs for VerificationArgs {
             // `--output-format=old` bypasses CBMC's structured output entirely: `run_cbmc` mocks a
             // result with no properties, and treats a timeout as success. An export produced from
             // that would be indistinguishable from a real clean run.
-            if self.export_json.is_some() && self.output_format == OutputFormat::Old {
+            if self.export_json.is_some() && self.output_format() == OutputFormat::Old {
                 return Err(Error::raw(
                     ErrorKind::ArgumentConflict,
                     "Conflicting options: --export-json isn't compatible with --output-format=old.",
@@ -844,15 +871,15 @@ impl ValidateArgs for VerificationArgs {
                     ),
                 ));
             }
-            if self.jobs().will_multithread() && self.output_format != OutputFormat::Terse {
+            if self.jobs().will_multithread() && 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::raw(
                     ErrorKind::ArgumentConflict,
                     "Conflicting options: --jobs requires `--output-format=terse`",
                 ));
             }
-            if self.log_file.is_some() && self.output_format == OutputFormat::Old {
+            if self.log_file.is_some() && self.output_format() == OutputFormat::Old {
                 // `old` runs CBMC with inherited stdio instead of piping it, so neither
                 // `kani_cbmc_output_filter` nor `process_output` runs and nothing but the
                 // per-harness "Checking harness ..." lines reaches the log. Accepting the
@@ -1387,4 +1414,61 @@ mod tests {
         let err = StandaloneArgs::try_parse_from(args).unwrap().validate().unwrap_err();
         assert_eq!(err.kind(), ErrorKind::MissingRequiredArgument);
     }
+
+    /// `autoharness` verifies harnesses in parallel by default, which requires terse output.
+    /// Check each combination of explicitly passed / defaulted `--jobs` and `--output-format`.
+    #[test]
+    fn check_autoharness_parallel_defaults() {
+        let effective = |extra: &str| {
+            let args = format!("kani autoharness -Z autoharness {extra} input.rs");
+            let parsed = StandaloneArgs::try_parse_from(args.split_whitespace()).unwrap();
+            let Some(StandaloneSubcommand::Autoharness(mut autoharness)) = parsed.command else {
+                panic!("expected the autoharness subcommand");
+            };
+            autoharness.verify_opts.apply_autoharness_parallel_defaults();
+            (autoharness.verify_opts.jobs(), autoharness.verify_opts.output_format())
+        };
+
+        // Neither option passed: parallel with terse output.
+        assert_eq!(effective(""), (NumThreads::ThreadPoolDefault, OutputFormat::Terse));
+        // Only `--jobs`: the user's thread count, plus the terse output it requires.
+        assert_eq!(effective("--jobs=4"), (NumThreads::UserSpecified(4), OutputFormat::Terse));
+        // Only `--output-format=terse`: parallel, since terse is what parallel needs.
+        assert_eq!(
+            effective("--output-format=terse"),
+            (NumThreads::ThreadPoolDefault, OutputFormat::Terse)
+        );
+        // A more verbose format opts back into sequential verification.
+        assert_eq!(
+            effective("--output-format=regular"),
+            (NumThreads::NoMultithreading, OutputFormat::Regular)
+        );
+        assert_eq!(
+            effective("--output-format=old"),
+            (NumThreads::NoMultithreading, OutputFormat::Old)
+        );
+
+        // Applying the defaults is idempotent, and plain verification is unaffected.
+        let args = "kani input.rs".split_whitespace();
+        let parsed = StandaloneArgs::try_parse_from(args).unwrap();
+        assert_eq!(parsed.verify_opts.jobs(), NumThreads::NoMultithreading);
+        assert_eq!(parsed.verify_opts.output_format(), OutputFormat::Regular);
+    }
+
+    /// `--jobs` with an explicitly requested non-terse format stays an error, for `autoharness`
+    /// (where the defaults cannot silently override the user) as well as plain verification.
+    #[test]
+    fn check_jobs_still_requires_terse() {
+        for args in [
+            "kani autoharness -Z autoharness --jobs=4 --output-format=regular input.rs",
+            "kani --jobs=4 input.rs",
+        ] {
+            let mut parsed = StandaloneArgs::try_parse_from(args.split_whitespace()).unwrap();
+            if let Some(StandaloneSubcommand::Autoharness(autoharness)) = &mut parsed.command {
+                autoharness.verify_opts.apply_autoharness_parallel_defaults();
+            }
+            let err = parsed.validate().unwrap_err();
+            assert_eq!(err.kind(), ErrorKind::ArgumentConflict, "for `{args}`");
+        }
+    }
 }

kani-driver/src/autoharness/mod.rs

@@ -52,6 +52,10 @@ pub fn autoharness_standalone(args: StandaloneAutoharnessArgs) -> Result<()> {
 
 /// Execute autoharness-specific KaniSession configuration.
 fn setup_session(session: &mut KaniSession, common_autoharness_args: &CommonAutoharnessArgs) {
+    // `main` already applies these before validating the arguments (so that validation sees the
+    // options the run will actually use); repeat it here -- the call is idempotent -- so that the
+    // session is configured correctly regardless of how it was constructed.
+    session.args.apply_autoharness_parallel_defaults();
     session.enable_autoharness();
     session.add_default_bounds();
     session.add_auto_harness_args(

kani-driver/src/call_cbmc.rs

@@ -225,7 +225,7 @@ impl KaniSession {
         let mut cmd = TokioCommand::new("cbmc");
         cmd.args(args);
 
-        let verification_results = if self.args.output_format == crate::args::OutputFormat::Old {
+        let verification_results = if self.args.output_format() == crate::args::OutputFormat::Old {
             if self.run_terminal_timeout(cmd).is_err() {
                 VerificationResult::mock_failure()
             } else {
@@ -267,7 +267,7 @@ impl KaniSession {
                         i,
                         self.args.extra_pointer_checks,
                         self.args.common_args.quiet,
-                        &self.args.output_format,
+                        &self.args.output_format(),
                         self.args.log_file.as_ref(),
                     )
                 }),
@@ -279,7 +279,7 @@ impl KaniSession {
                     i,
                     self.args.extra_pointer_checks,
                     self.args.common_args.quiet,
-                    &self.args.output_format,
+                    &self.args.output_format(),
                     self.args.log_file.as_ref(),
                 )
             })

kani-driver/src/harness_runner.rs

@@ -174,7 +174,7 @@ impl KaniSession {
                 self.write_output_to_file(result, harness, thread_index);
             }
 
-            let output = result.render(&self.args.output_format, harness.attributes.should_panic);
+            let output = result.render(&self.args.output_format(), harness.attributes.should_panic);
 
             if rayon::current_num_threads() > 1 {
                 self.emit_line(&format!("Thread {thread_index}: {output}"));
@@ -200,7 +200,7 @@ impl KaniSession {
     }
 
     fn should_print_output(&self) -> bool {
-        !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old
+        !self.args.common_args.quiet && self.args.output_format() != OutputFormat::Old
     }
 
     fn write_output_to_file(

kani-driver/src/main.rs

@@ -82,7 +82,13 @@ fn main() -> ExitCode {
 /// The main function for the `cargo kani` command.
 fn cargokani_main(input_args: Vec<OsString>) -> Result<()> {
     let input_args = join_args(input_args)?;
-    let args = args::CargoKaniArgs::parse_from(&input_args);
+    let mut args = args::CargoKaniArgs::parse_from(&input_args);
+    // Apply the autoharness defaults before validating, so that validation sees the options the
+    // run will actually use (e.g. `--jobs=N` must not be rejected for lacking
+    // `--output-format=terse` when autoharness supplies exactly that default).
+    if let Some(CargoKaniSubcommand::Autoharness(autoharness_args)) = &mut args.command {
+        autoharness_args.verify_opts.apply_autoharness_parallel_defaults();
+    }
     check_is_valid(&args);
 
     // Handle version flag
@@ -117,7 +123,11 @@ fn cargokani_main(input_args: Vec<OsString>) -> Result<()> {
 
 /// The main function for the `kani` command.
 fn standalone_main() -> Result<()> {
-    let args = args::StandaloneArgs::parse();
+    let mut args = args::StandaloneArgs::parse();
+    // See the comment in `cargokani_main`.
+    if let Some(StandaloneSubcommand::Autoharness(autoharness_args)) = &mut args.command {
+        autoharness_args.verify_opts.apply_autoharness_parallel_defaults();
+    }
     check_is_valid(&args);
 
     // Handle version flag

tests/script-based-pre/autoderive_arbitrary_enums/enums.sh

@@ -2,4 +2,4 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-cargo kani autoharness -Z autoharness
+cargo kani autoharness -Z autoharness --output-format=regular

tests/script-based-pre/autoderive_arbitrary_structs/structs.sh

@@ -2,4 +2,4 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-cargo kani autoharness -Z autoharness
+cargo kani autoharness -Z autoharness --output-format=regular

tests/script-based-pre/autoharness-refs_immutable/run.sh

@@ -2,4 +2,4 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-kani autoharness -Z autoharness immutable.rs
+kani autoharness -Z autoharness --output-format=regular immutable.rs

tests/script-based-pre/autoharness-refs_mutable/run.sh

@@ -2,4 +2,4 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-kani autoharness -Z autoharness mutable.rs
+kani autoharness -Z autoharness --output-format=regular mutable.rs

tests/script-based-pre/cargo_autoharness_bounded/bounded.sh

@@ -15,4 +15,4 @@ echo "[with --bounded-arguments]"
 # `String`, which is expensive; on slower CI runners it can exceed the autoharness default
 # 60s harness timeout, so raise it here to keep these harnesses from spuriously timing out.
 # This run reports failures (`vec_first`/`string_first_byte`), so it exits non-zero (see config.yml).
-cargo kani autoharness -Z autoharness -Z unstable-options --bounded-arguments --harness-timeout 5m
+cargo kani autoharness -Z autoharness -Z unstable-options --output-format=regular --bounded-arguments --harness-timeout 5m

tests/script-based-pre/cargo_autoharness_contracts/contracts.sh

@@ -2,4 +2,4 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-cargo kani autoharness -Z autoharness
+cargo kani autoharness -Z autoharness --output-format=regular

tests/script-based-pre/cargo_autoharness_dependencies/dependencies.sh

@@ -2,4 +2,4 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-cargo kani autoharness -Z autoharness
+cargo kani autoharness -Z autoharness --output-format=regular

tests/script-based-pre/cargo_autoharness_exclude/exclude.sh

@@ -2,4 +2,4 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-cargo kani autoharness -Z autoharness --exclude-pattern exclude
+cargo kani autoharness -Z autoharness --output-format=regular --exclude-pattern exclude

tests/script-based-pre/cargo_autoharness_filter/filter.sh

@@ -2,4 +2,4 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-cargo kani autoharness -Z autoharness
+cargo kani autoharness -Z autoharness --output-format=regular

tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh

@@ -2,4 +2,4 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-cargo kani autoharness -Z autoharness
+cargo kani autoharness -Z autoharness --output-format=regular

tests/script-based-pre/cargo_autoharness_include/include.sh

@@ -2,4 +2,4 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-cargo kani autoharness -Z autoharness --include-pattern cargo_autoharness_include::include
+cargo kani autoharness -Z autoharness --output-format=regular --include-pattern cargo_autoharness_include::include

tests/script-based-pre/cargo_autoharness_parallel/Cargo.toml

@@ -0,0 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "cargo_autoharness_parallel"
+version = "0.1.0"
+edition = "2021"

tests/script-based-pre/cargo_autoharness_parallel/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: parallel.sh
+expected: parallel.expected

tests/script-based-pre/cargo_autoharness_parallel/parallel.expected

@@ -0,0 +1,7 @@
+TERSE: yes
+PARALLEL: yes
+| f1 | #[kani::proof] | Success
+| f2 | #[kani::proof] | Success
+| f3 | #[kani::proof] | Success
+| f4 | #[kani::proof] | Success
+Complete - 4 successfully verified functions, 0 failures, 4 total.