Keep completed results when --fail-fast aborts a run - #4744
Conversation
feliperodri
added
the
[I] Refactoring / Clean Up
There was a problem hiding this comment.
Pull request overview
Retains completed harness results when --fail-fast aborts verification, keeping summaries and JSON exports accurate.
Changes:
- Accumulates parallel results safely and restores harness ordering.
- Replaces schedule-dependent UI expectations with script-based checks.
- Adds a deterministic sequential regression test.
Reviewed changes
Copilot reviewed 10 out of 10 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
kani-driver/src/harness_runner.rs |
Retains and sorts completed results. |
tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test_parallel.expected |
Removes obsolete fixed summary. |
tests/script-based-pre/fail_fast_parallel/fixture.rs |
Updates parallel fixture documentation. |
tests/script-based-pre/fail_fast_parallel/early_abort.sh |
Checks parallel fail-fast behavior. |
tests/script-based-pre/fail_fast_parallel/early_abort.expected |
Adds expected script result. |
tests/script-based-pre/fail_fast_parallel/config.yml |
Configures parallel regression test. |
tests/script-based-pre/fail_fast_keeps_completed/keeps_completed.sh |
Checks deterministic result retention. |
tests/script-based-pre/fail_fast_keeps_completed/keeps_completed.expected |
Adds expected script result. |
tests/script-based-pre/fail_fast_keeps_completed/fixture.rs |
Adds passing and failing harnesses. |
tests/script-based-pre/fail_fast_keeps_completed/config.yml |
Configures sequential regression test. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
7ef0626 to
3ed8af4
Compare
feliperodri
left a comment
feliperodri
left a comment
There was a problem hiding this comment.
Diagnosis and fix are right, and this is the direction I suggested in #4729 — the accumulator + re-sort is exactly it. Nice catch on the sort in particular: the old collect::<Result<Vec>> on an indexed rayon iterator was order-preserving, so without it you'd have silently changed export ordering for every parallel run, not just fail-fast ones. I also checked the determinism argument for the new sequential test and it holds (sort_harnesses_by_loc reverses on start line, jobs() defaults to 1 thread), and the existing sequential UI test really is unaffected.
Blocking on the first inline comment; the rest are cheap.
One more that I can't anchor inline because the file isn't in the diff: schema_utils.rs:362-365 says verification_results.results "is in completion order", which is why entries need harness_id. After this PR the order is deterministic. The conclusion still stands (sorted-by-loc != harness-metadata order) but the stated reason is now wrong — please reword.
Regression suites are still running, so I haven't seen an end-to-end green.
| Err(err) => return Err(err), | ||
| }; | ||
|
|
||
| // Completion order under parallelism is nondeterministic; restore harness order. |
There was a problem hiding this comment.
The order is fixed here, but the set is still schedule-dependent, and that's a user-visible contract change: --export-json is no longer reproducible for --fail-fast --jobs N, so CI consumers diffing exports will see churn run to run.
I think that's the right behavior (it's the honest one), but it needs to be written down somewhere. --fail-fast has zero mentions in docs/ and a one-line help string (args/mod.rs:261). Please add a sentence there: in-flight harnesses finish and get counted, so counts vary under --jobs.
| exit 1 | ||
| fi | ||
|
|
||
| python3 - "${EXPORT_FILE}" << 'EOF' |
There was a problem hiding this comment.
Wrong suite for this half. Every other --export-json test lives in tests/json-handler/, so nobody auditing export coverage will find this. Also, unlike its siblings there, it never runs scripts/validate_json_export.py — so nothing checks that the completed_with_fail_fast document still validates structurally.
Suggest splitting: keep the summary assertions here, move the export assertions to tests/json-handler/fail-fast/ and run the validator.
| fi | ||
|
|
||
| # The run must abort early: strictly fewer than all ten harnesses. | ||
| if [[ "${TOTAL}" -ge 10 ]]; then |
There was a problem hiding this comment.
Flagging, not blocking: this turns a pinned test into a timing test. Realistically safe — 4 threads means ~4 chunks and full() is checked before each item, so TOTAL lands near 4 — but the bound is doing no work if scheduling ever changes.
The VERDICTS == TOTAL check below is the load-bearing assertion and holds under any schedule. Fine to keep the < 10 guard, just don't count it as the regression check.
`check_all_harnesses` collected with `collect::<Result<Vec<_>>>()`,
which short-circuits on the first error. A `--fail-fast` abort was such
an error, so every harness that had already completed was dropped. The
summary then contradicted the per-harness output above it, and the
`--export-json` file under-reported the run the same way.
Accumulate completed results in a shared vector instead. The abort
signal carries no payload; the failing harness records its result like
any other. Results are re-sorted into harness order after the parallel
loop, since completion order is nondeterministic.
The parallel fail-fast UI test pinned the dropped-results behavior
("1 failures, 1 total" with ten failing harnesses under `--jobs 4`).
With completed results retained, its counts depend on thread
scheduling, so it becomes a script-based test asserting the stable
properties: the run aborts early, every counted harness is a failure,
and the summary total equals the number of verdicts printed above it.
The sequential UI test is unchanged: it aborts on its first harness,
so its pinned summary stays correct. A new sequential script-based
test covers result retention deterministically, in both the summary
and the --export-json file.
Resolves model-checking#4729
The abort was raised as an `Err(FailFastAbort)` through the same channel `try_for_each` uses for genuine errors, and `try_for_each` surfaces only one error. A harness failing for a real reason at the same time as another tripped the abort could therefore have its error discarded, leaving the run to report an ordinary fail-fast stop. Signal the abort with an `AtomicBool` instead, so the error channel carries genuine errors only and every one of them propagates. Harnesses that have not started check the latch and return without running; those already in flight finish and record their results, as before. The latch is read after the parallel region joins, which orders the stores before the read.
`verification_results.results` was described as being in completion order. It is not, and was not before this branch either: rayon's collect returns results in input order, and this branch now sorts them explicitly. What the comment is warning about still holds, since the two arrays are built from different orderings and need not agree, so say that instead.
The latch had no test of its own. `harness_runner.rs` carried no unit tests at all, and the script-based tests cover result retention rather than which signal takes the error channel, so reverting the latch left every test on the branch passing. Lift the parallel run into `run_until_abort`, generic over the unit of work, so the policy can be driven directly: the abort and error paths are what the reviewer asked about, and neither needed a harness or a solver to exercise. `check_all_harnesses` supplies the same closure it ran inline. The tests fix the permutations that matter: an abort reported through the flag and never through the error channel, a genuine error raised by one unit while another aborts concurrently, an error on its own, units after an abort not starting, and completed payloads kept in input order. Reverting the latch to an error-channel abort fails four of them, including the concurrent case.
The test asserting that a genuine error is not displaced by a concurrent abort claimed that if rayon ran both units on one thread "the assertion still holds". It does not: forcing the pool to one thread makes the test fail, because the aborting unit latches the abort before the erroring unit is ever visited, so there is no error left to propagate. Rayon is not obliged to split a two-element iterator, so that was a latent CI flake sitting inside the receipt for the fix. Latch the abort only once the aborting unit has seen its sibling start. Serialized, it declines to abort and the erroring unit runs afterwards, so the assertion holds instead of failing on a scheduling accident; in parallel the two still overlap and the test means what it says. Measured, not assumed: with the pool forced to one thread the test now passes, and reverting the latch to an error-channel abort still fails four of the six, the concurrent case among them, on five runs out of five. Also drop two comment claims that outran the code: the cancellation check is a `Relaxed` load and so is best effort rather than a guarantee that a unit will not start, and `verification_results.results` is sorted into `sort_harnesses_by_loc` order rather than left in scheduling order.
Help string: `--fail-fast` documented only that it stops the run. It also changes which harnesses get reported, because harnesses already running when one fails still finish and are counted, so the set varies under `--jobs N`. That is a user-visible contract for anyone diffing exports, and the flag's whole documentation was the one line. `docs/` has no fail-fast section to extend, so this stays in the help string. Test split: the export assertions lived in the script-based summary test, away from the rest of the export coverage in tests/json-handler/, and were the only ones there that never ran validate_json_export.py. Moved to tests/json-handler/fail-fast/, which follows the multiple-harnesses layout and validates the document before asserting on it, so an aborted run's export is now checked structurally as well. The summary test keeps the rendered-summary half. early_abort.sh: the comments presented the `< 10` bound as the regression check. It is a smoke check that the abort happened, and it is a statement about scheduling; VERDICTS == TOTAL is the assertion that reproduces model-checking#4729 and holds under any schedule. Relabelled both, changed neither. Also: the ordering step had no test that could fail. Every runner test uses a one-thread pool, where units complete in index order and the sort is a no-op, so deleting it broke nothing. Lifted it into `in_input_order` and drove it with a shuffled input, which is the case `--jobs N` produces.
The test dropped set -e because the kani run under test exits non-zero by design, but that also discarded the validator pipeline's status: pipefail alone only reports it, nothing consumed it, so a structurally invalid export could not fail the test. Exempt only the kani invocation from set -e, the way failed-verification/test.sh already does.
9acff28 to
bc25cdf
Compare
|
@feliperodri done, all items covered and retested. here's a summary per review item:
Also folded, from the earlier Copilot comments (never answered in-thread): the export case is One change beyond the threads: the ordering step was extracted into in_input_order and Local regression at the pushed commit: unit tests green (87 in kani-driver) and 15 compiletest |
check_all_harnessescollected results withcollect::<Result<Vec<_>>>(), which short-circuits on the first error. A--fail-fastabort was such an error, so every result that had already completed was dropped. The summary then contradicted the per-harness output above it, and--export-jsonunder-reported the run the same way.Completed results now accumulate in a shared vector as harnesses finish. The abort signal carries no payload; the failing harness records its result like any other. Results are re-sorted into harness order after the parallel loop, since completion order is nondeterministic.
The parallel fail-fast UI test pinned the old behavior: "1 failures, 1 total" for ten failing harnesses under
--jobs 4. With completed results retained, those counts depend on thread scheduling, so the test becomes a script-based test asserting the stable properties: the run aborts early (fewer than ten run) and every counted harness is a failure. The sequential UI test is unchanged: it aborts on its first harness, so its pinned summary stays correct. A new sequential script-based test proves retention deterministically ("1 successfully verified, 1 failures, 2 total"); it fails onmain.Testing:
cargo test -p kani-driver,rustfmt, andclippyare clean; the two new script-based tests and the existingstop_at_single_failUI test pass.Resolves #4729