You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Stopping on failure can be on two different levels:
If there are multiple harnesses, stop as soon as one of the harnesses fail
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).
@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:
Whether to use wildcards(*) in .expected files to handle thread ordering variations
Any suggestions for making the tests more robust while still verifying the fail-fast behavior
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:
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.
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.
Activity
zhassan-aws commentedon Aug 26, 2024
Thanks for the feature request @cospectrum. This makes sense.
There is a pretty ugly workaround to achieve that currently, which is to run with:
but we should add a Kani option instead.
If you're willing to add an option, we can provide some guidance.
zhassan-aws commentedon Oct 18, 2024
Stopping on failure can be on two different levels:
The second level is harder to implement because with CBMC's
--stop-on-failoption, it can stop because of a reachability check passing (i.e. an assertion is reachable).rajath-mk commentedon Feb 5, 2025
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 commentedon Feb 5, 2025
This should be part of the verification args.
This is the loop that runs all harnesses:
kani/kani-driver/src/harness_runner.rs
Line 40 in 380b1fb
rajath-mk commentedon Feb 6, 2025
@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:
Ref to commit: rajath-mk@6340423
zhassan-aws commentedon Feb 6, 2025
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:
so, we can have this line only in the expected file.
rajath-mk commentedon Feb 7, 2025
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 commentedon Feb 7, 2025
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
Fast fail feature - Stops verification process as soon as one failure…