Fast fail

[cospectrum]

Add a flag to exit after the first failed verification. Have not found a way to do this.
Use case: ci speed up.

[zhassan-aws]

Thanks for the feature request @cospectrum. This makes sense.

There is a pretty ugly workaround to achieve that currently, which is to run with:

--no-assertion-reach-checks --output-format old --enable-unstable --cbmc-args --stop-on-fail

but we should add a Kani option instead.

If you're willing to add an option, we can provide some guidance.

[zhassan-aws]

Stopping on failure can be on two different levels:

1. If there are multiple harnesses, stop as soon as one of the harnesses fail
2. Within one harness: if a check fails, do not continue with the remaining checks

The second level is harder to implement because with CBMC's --stop-on-fail option, it can stop because of a reachability check passing (i.e. an assertion is reachable).

[rajath-mk]

Hi @zhassan-aws , do we add the option to the common args (kani-driver/src/args/common.rs) or the verification args (kani-driver/src/args/mod.rs) ?

To implement the fast fail mechanism itself, I am looking at the try_fold iterator (library/core/src/iter/traits/iterator.rs).

As discussed, I am focusing on the implementation for the sequential part now, and in the later stages maybe ill look into the parallel step.

[zhassan-aws]

Hi @zhassan-aws , do we add the option to the common args (kani-driver/src/args/common.rs) or the verification args (kani-driver/src/args/mod.rs) ?

This should be part of the verification args.

To implement the fast fail mechanism itself, I am looking at the try_fold iterator (library/core/src/iter/traits/iterator.rs).

This is the loop that runs all harnesses:

kani/kani-driver/src/harness_runner.rs

Line 40 in 380b1fb

pub(crate) fn check_all_harnesses(

[rajath-mk]

@zhassan-aws As discussed, I implemented fail-fast for parallel execution using channels and an atomic boolean. The implementation uses a combination of std::sync::mpsc::channel() for communicating failed results and std::sync::atomic::AtomicBool for signaling other threads to stop starting new verifications.

The core mechanism works - when a test fails, it sets the atomic flag and other threads check this flag before starting new verifications. However, I'm facing challenges with the test framework. The parallel execution produces non-deterministic output ordering, making it difficult to write stable tests.

Would appreciate advice on:

1. Whether to use wildcards(*) in .expected files to handle thread ordering variations
2. Any suggestions for making the tests more robust while still verifying the fail-fast behavior

Ref to commit: rajath-mk@6340423

[zhassan-aws]

The parallel execution produces non-deterministic output ordering, making it difficult to write stable tests.

One idea is to have n harnesses that all fail, and run with a smaller number of jobs, e.g. 2. I would expect in this case that Kani would always print:

Complete - 0 successfully verified harnesses, 2 failures, 2 total.

so, we can have this line only in the expected file.

[rajath-mk]

Yes, that works well. Thanks. I have made another commit with the changes here: rajath-mk@ac18579

The current approach has minimal changes to the original code and has an additional channel and an error flag. But in order to utilize Rayon's par_iter's built in functionalities, I am looking into the try_for_each (which works since we use a mutex instead of an atomic error flag, but we lose some features such as inter thread comm), the try-fold method is suiting our purposes well based on the method definition. Will look into that.

[rajath-mk]

As discussed, added custom error handler with index based fetching --> in an event of a failure, the current index of the failed harness in the vector is captured, and later the element is obtained --> giving us essentially the first failed harness among all threads.

code working as expected: rajath-mk@88e6bed

@zhassan-aws