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.