Link independent harness models in parallel

[M00NLIG7]

Summary

Use Kani's existing verification job budget to link harness models concurrently only when every computed destination path is distinct. Shared or duplicate destinations, explicit serial settings, and single-link projects retain the existing serial path.

This also centralizes construction of the Rayon pool so linking and harness verification cannot interpret --jobs differently.

Motivation

Autoharness can produce many independent symbol-table models. Project::try_new currently invokes goto-cc for each model serially before the already-parallel harness pipeline starts. Local process profiling identified that sequence as a measurable preparation boundary.

The change is intentionally conservative: it removes that boundary where independence can be established, without changing formulas, solver behavior, verification defaults, or the number of workers selected by Kani.

Behavior and concurrency contract

• Canonicalize every model input and compute its final .out destination before starting any link.
• Use an indexed Rayon parallel iterator only when there is more than one link, the configured job setting permits parallelism, and all destination paths are unique.
• Fall back to a regular serial iterator if any destination is shared or uniqueness is otherwise not established.
• Preserve NumThreads exactly: omitted ordinary-Kani jobs remain serial, --jobs=1 remains serial, --jobs=N uses exactly N, and Rayon's existing default remains the autoharness default.
• Collect artifact groups in metadata order even when links complete out of order.
• Propagate any link error and abort project construction.

The link and verification phases use separate stage-local pools, both built from the same existing NumThreads selection; this PR does not add workers to that selection.

Correctness

Focused unit coverage exercises:

• a two-worker upper bound while proving indexed results match the serial order;
• both the ordinary serial setting and explicit --jobs=1 without entering a Rayon worker;
• duplicate destinations forcing the complete link set down the serial path;
• a failure from a parallel link reaching the caller.

The existing autoharness script regression now also runs with explicit --jobs=1 and compares normalized per-harness/final summaries with the parallel run.

Local validation on the current tree:

• cargo build-dev
• cargo test -p kani-driver (85 passed)
• cargo clippy --workspace --tests -- -D warnings
• RUSTFLAGS="--cfg=kani_sysroot" cargo clippy --workspace -- -D warnings
• ./scripts/kani-fmt.sh --check
• bash -n tests/script-based-pre/cargo_autoharness_parallel/parallel.sh

The end-to-end script could not run to completion locally because this host does not currently have goto-cc/CBMC on PATH; the script now fails immediately rather than accepting an empty comparison. The normal Linux regression job supplies those dependencies.

Benchmarks

These are end-to-end cargo kani autoharness measurements comparing current upstream behavior (U) with only independent linking added (L). Each cell is steady median seconds [min–max] / maximum aggregate process-tree RSS MiB. Control has seven retained steady samples; the other workloads have three. All samples were retained.

Workload	U	L	Median change
24-proof control	54.668 [43.952–56.363] / 346.5	51.633 [42.812–55.823] / 351.0	−5.6%
Heterogeneous medium, 22 jobs	20.419 [18.610–22.240] / 200.4	17.724 [16.292–18.018] / 184.5	−13.2%
Memory-heavy formatting, 13 jobs	19.880 [18.098–21.500] / 3,037.2	16.684 [15.654–17.113] / 3,050.5	−16.1%
num-traits 0.2.19 constructor subset, 30 jobs	6.854 [5.999–7.164] / 93.7	3.130 [2.776–3.612] / 110.7	−54.3%

Artifact-cold U→L samples were also directionally positive: control 53.296→46.162 s, medium 23.168→21.139 s, heavy 23.248→20.686 s, and the real subset 8.924→5.642 s. “Artifact-cold” means deleting the workload target, not flushing the macOS filesystem cache.

Common command (the real subset additionally used the shown include filter):

RAYON_NUM_THREADS=12 \
RUSTUP_TOOLCHAIN=nightly-2026-04-01-aarch64-apple-darwin \
PATH="<exact-state>/scripts:<cbmc-6.10.0-bin>:$PATH" \
cargo kani autoharness -Z autoharness -Z unstable-options \
  --solver cadical --output-format=terse --quiet \
  --harness-timeout 120s \
  [--include-pattern '::(zero|one)$'] \
  --export-json '<fresh-run-dir>/results.json'

The benchmark host was an Apple M3 Pro (Mac15,7), 12 cores (6 performance + 6 efficiency), 36 GiB RAM, macOS 26.5.2 arm64, CBMC 6.10.0/CaDiCaL, on battery and shared with other work. The new matrix interleaved states and used one cold plus three steady samples per state/workload.

All 60 new formal matrix runs exited successfully with fresh exports and equivalent structured output. No run timed out or hit its RSS stop, and no newly observed swapout or throttling occurred. The control exports covered 24/24 harnesses and 432/432 successful properties; medium covered 22/22 and 342/342; heavy covered 13/13 with all 29,003 property records identical; the real subset covered 30/30 constructors.

Resource impact

The memory-heavy U→L maximum changed by +0.4% (+13.3 MiB), while medium decreased by 7.9%. The largest relative increase was the tiny real constructor subset (+18.1%), but that was +17.0 MiB absolute (93.7→110.7 MiB). Control increased by 4.5 MiB.

This does not increase Kani's configured worker budget. Concurrent linker processes can raise short-lived preparation RSS relative to serial linking, but measured heavy-workload memory remained dominated by solver processes.

Non-goals

• No implicit worker oversubscription or default worker-count change.
• No fixed CPU-derived memory policy or memory-budget mechanism.
• No solver scheduling, solver selection, formula, unwind, or property change.
• No change to explicit --jobs semantics.

Limitations

• Measurements are from one noisy, heterogeneous-core arm64 macOS host, not representative Linux x86_64 hardware. No non-emulated Linux x86_64 benchmark facility was available locally; I did not use architecture emulation. The PR CI is the available upstream-supported Linux x86_64 validation.
• The 5.6% control effect is modest and its ranges overlap substantially.
• The 54.3% num-traits result is a limited 30-constructor, link-dominated subset, not a full-crate result. Those constructors produced no property records. A full unfiltered num-traits --list attempt was stopped safely at 300.057 s and 909,392 KiB before a harness list appeared, so full-crate behavior remains unknown.
• No additional high-harness public crate was genuinely available within the bounded local setup.
• Medium/heavy/real series have three steady repetitions; RSS is sampled aggregate resident memory rather than proportional set size; swap counters are system-wide.
• The benchmark did not inject duplicate destinations or link failures; the new focused unit tests cover both paths.

Reviewer question

Is the existing verification --jobs budget the right authority for linker concurrency, or should linking eventually have a separate explicit budget?

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

[feliperodri]

Thanks for this, @M00NLIG7 — this is a clean, conservative win. The parallelism is gated on a genuine independence check (distinct destinations) rather than assumed, which is exactly the right instinct for a concurrency change in Kani. I did a deep review and it holds up:

Correctness (verified against the primitives):

• Path handling is behaviorally equivalent to the old Artifact::try_new (both canonicalize + require existence), so inputs/outputs are unchanged.
• Independence is sound: link_goto_binary only reads its inputs (plus the shared read-only c_lib/kani_lib_c) and writes exactly -o output, so distinct destinations ⇒ no write races. Shared/duplicate destinations correctly fall back to serial.
• NumThreads semantics preserved exactly (jobs() → NoMultithreading with no -j, so ordinary kani linking stays serial); link and verify pools are built identically and run sequentially, so no oversubscription.
• Indexed par_iter().collect() preserves order; errors propagate via collect::<Result<_>>.

I could run it end-to-end (I have goto-cc/CBMC locally): the cargo_autoharness_parallel equivalence test and cargo_autoharness_filter pass, cargo test -p kani-driver (85, incl. the 4 new concurrency tests), clippy, and fmt are all green.

Independent performance numbers using our own autoharness regression fixtures (16-core host; baseline = main, treatment = this PR, only the driver binary swapped so compiler/libs/CBMC are identical; median of 7–9 warm-cache reps):

Fixture	~harnesses	Phase	main	this PR	Change
filter	47	codegen+link (--only-codegen)	1.632s	0.380s	−77%
filter	47	full autoharness	2.329s	1.094s	−53%
generics	21	codegen+link (--only-codegen)	0.630s	0.219s	−65%
generics	21	full autoharness	1.104s	0.696s	−37%

(Spread was tight, e.g. filter --only-codegen main 1.62–1.64 / PR 0.35–0.41.) These fixtures are many tiny harnesses, so linking is a large share of total — the full-run percentages are an upper bound; heavy-verification crates will see closer to your realistic −5%/−16% numbers. Either way it reproduces the claim, and the win scales with harness count and cores.

Maintainability: good. It's well-contained (one execute_link_jobs helper + LinkJob), and centralizing pool construction in NumThreads::build_thread_pool actually removes duplication (the inline builder in harness_runner is gone). The concurrency logic is unit-tested, which lowers the risk of future regressions. project.rs's try_new is a touch denser than the old imperative loop, but still readable.

Approving. Two non-blocking nits inline, plus one note: parallel linking spawns up to --jobs concurrent goto-cc processes — bounded by the job count the user already chose, and your benchmarks show RSS staying flat, so no concern, just worth being aware of.

LGTM! 🚀