Autoharness: verify harnesses in parallel by default

[tautschnig]

Description

Autoharness typically generates hundreds of harnesses, for which the sequential default of the harness runner is a poor fit. In a top-100 crates.io evaluation (tracking issue #3832), 12 crates hit a 30-minute wall-clock cap; with -j 16 --output-format=terse, num-traits alone went from timing out at 1800s to completing all 1,983 generated harnesses in 330s.

Kani already has the machinery (--jobs, whose rayon pool covers the full per-harness pipeline: goto-instrument, loop-contract synthesis, CBMC). This PR makes autoharness use it by default.

To distinguish an explicit --output-format=regular from the clap default, output_format becomes Option<OutputFormat> with an accessor defaulting to Regular.

Defaulting rules (apply_autoharness_parallel_defaults), applied for the autoharness subcommand only:

• --output-format is defaulted to terse when the user did not pass it.
• --jobs is defaulted to -j (the thread pool's default thread count) when the user did not pass it and the resulting format is terse.

So:

invocation	effective
autoharness	-j + terse
autoharness --jobs=N	-j N + terse
autoharness --output-format=terse	-j + terse
autoharness --jobs=1	sequential + terse
autoharness --output-format=regular (or old)	sequential, format as asked
autoharness --jobs=N --output-format=regular	error (as before)
plain kani / cargo kani	unchanged: sequential + regular; --jobs still requires --output-format=terse

The defaults are applied in main immediately after parsing and before validation, so validation sees the options the run will actually use. Otherwise a bare --jobs=N would be rejected for lacking --output-format=terse even though autoharness supplies exactly that default — i.e. the documented "pass -j <N> to control the number of threads" would not have worked. The call is idempotent and is repeated in setup_session so a session is configured correctly however it was constructed.

Note on memory: each thread runs its own CBMC process, so peak memory grows with the thread count, and the default is one thread per logical CPU. The docs call this out and point at --jobs=<N> as the knob.

Results themselves stay deterministic: harness_runner collects with rayon's indexed collect::<Result<Vec<_>>>(), which preserves input order, so the summary table, --sarif, and --export-json are unaffected by execution order. Only live stdout ordering varies, which is what the Thread N: prefix and the terse requirement address.

Testing

• New cargo_autoharness_parallel test pins both halves of the default with order-independent assertions: terse output (absence of per-check detail, independent of the CPU count), thread prefixes (skipped in a single-CPU environment rather than failing spuriously), the sorted per-function summary lines, and the totals line.
• New kani-driver unit tests: check_autoharness_parallel_defaults covers every combination in the table above plus "plain verification unaffected"; check_jobs_still_requires_terse pins that an explicit non-terse format with --jobs remains an error for both autoharness and plain verification.
• Existing autoharness tests that assert on per-check detail (Status:/Description:/Check N:), which only --output-format=regular prints, now pass that flag — this also covers the opt-out path. That is 12 tests, including cargo_autoharness_bounded, cargo_autoharness_slices and cargo_autoharness_smart_pointers, which were added after this PR was opened.
• The remaining autoharness tests (assume_invariant, fmt_impls, generics, list, raw_pointers, exclude_precedence) deliberately keep the new default, so CI exercises the parallel/terse path beyond the dedicated test. Their expected output only references the sorted summary/skipped tables and totals, and compiletest matches expected lines independently of order.
• Full script-based-pre suite (66 tests), ui suite, cargo test -p kani-driver (81 tests), clippy --all-targets, and kani-fmt --check pass.
• Manually verified every row of the table above, plus that plain kani/cargo kani output is unchanged.

Towards #3832 (evaluation throughput).

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.

[Copilot]

Pull request overview

Copilot reviewed 27 out of 27 changed files in this pull request and generated 2 comments.

[feliperodri]

Both addressed.

parallel.sh CPU detection: correct, and the guard was wrong in exactly the environment it was supposed to protect: getconf _NPROCESSORS_ONLN reports host-online CPUs, whereas rayon derives its default from available_parallelism (affinity/cgroup aware). Replaced the guard with RAYON_NUM_THREADS=2 on the invocation and made the thread-prefix assertion unconditional. This still discriminates the default rather than just pinning the pool size: rayon only consults RAYON_NUM_THREADS when the thread count is left unset, which is what the defaulted --jobs does — sequential verification passes an explicit num_threads(1) that overrides it. Verified both ways: with RAYON_NUM_THREADS=2 the default run emits Thread 0:/Thread 1:, while --output-format=regular emits no thread prefixes at all.

Docs example: also a real defect. The example now passes --output-format=regular, with a pointer to the Parallel verification section explaining why, so the command and the per-check Check/Status/Description output shown below it agree.