Run each harness as its own rayon job so -j N workers do not idle at the end of a run

[jadenfix]

With --jobs N, the end of a long run degrades to a single worker: one thread finishes the last few dozen harnesses alone while the others sit idle.

run_until_abort runs harnesses with items.par_iter().enumerate().try_for_each(..). Rayon's default splitter starts with splits = num_threads and halves it on every unstolen split, so with three workers the first job is divided only twice (501 harnesses → 250 → 125) before the remaining chunk is folded sequentially on one worker; once a worker has started folding a chunk, no other worker can take items from it. That is the fixed block of 125 harnesses Thread 0 ran in the measurement in #4961. Stolen jobs are re-split finely, so the other two workers balance between themselves, but whoever holds the sequential chunk is stuck with it, and with harness run times spanning milliseconds to the full --harness-timeout that chunk routinely ends up being the tail of the run.

This change adds .with_max_len(1) so that each harness is its own rayon job and an idle worker can always take the next one. Results, their order, and the --fail-fast abort latch are unchanged; only the order in which harnesses start changes, and each harness's output is already reported in its own block. The per-job overhead is one join per harness, which is negligible next to a cbmc invocation.

A unit test runs twelve units on a three-thread pool, where the default splitter would queue unit 1 behind unit 0 on the same worker, and checks that unit 1 starts while unit 0 is still running. The test fails on main and passes with this change.

Resolves #4961

Manual testing. I could not run CBMC on this machine, so I did not reproduce the kraken-core measurement end to end. To confirm the mechanism I ran a standalone simulation with the same rayon version (1.12.0): 501 sleep-based items on a three-thread pool, with durations correlated by position (blocks of 20–60 consecutive items sharing a scale between 1 ms and 128 ms, as harnesses sorted by source location would be), five seeds, measuring the wall time and the time during which only one worker was still busy:

seed	default chunking	with_max_len(1)
1	wall 5.77 s, per-thread [197, 176, 128], single-worker tail 0.03 s	wall 5.86 s, [205, 137, 159], tail 0.01 s
2	wall 5.51 s, [131, 198, 172], tail 0.07 s	wall 5.39 s, [155, 171, 175], tail 0.01 s
3	wall 8.99 s, [161, 125, 215], tail 3.30 s	wall 6.77 s, [229, 165, 107], tail 0.01 s
4	wall 7.17 s, [254, 153, 94], tail 0.44 s	wall 7.04 s, [145, 146, 210], tail 0.08 s
5	wall 3.71 s, [186, 197, 118], tail 0.13 s	wall 3.54 s, [195, 92, 214], tail 0.01 s

Seed 3 shows the reported shape: one worker holds a 125-item sequential chunk and spends 3.3 s of a 9.0 s run alone, and the change removes the tail. The other seeds show that when the chunk happens to be cheap there is no cost to the change.

cargo test -p kani-driver passes.

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

[Copilot]

🟢 Approval recommended

The focused scheduling change preserves result ordering and abort handling, with no blocking issues identified.

No open issues 🎉

What changed in this PR

Improves parallel harness scheduling so idle workers can take remaining harnesses instead of waiting on a worker’s sequential chunk, addressing #4961.

Changes:

• Adds .with_max_len(1) to schedule each harness separately.
• Adds a regression test checking that a slow harness does not block subsequent work.

File	Description
kani-driver/​src/​harness_runner.rs	Adjusts scheduling granularity and adds a concurrency regression test.

_{Review effort: Balanced}

[feliperodri]

LGTM, thank you for solving this!

[jadenfix]

Thanks for the review, @feliperodri. I checked the three remaining macOS 14 failures: each stops during dependency setup at brew install z3, while compiling Z3 5.3.1, before Kani or the new scheduler regression is tested. The regression job log shows the failure in Z3's symbol_table.h/AST build; the build and verify jobs fail at the same step.

The PR is already up to date with main. Is there a preferred runner or dependency setup fix for these macOS jobs? Happy to help with a focused follow-up.