Repository navigation
test(kani): distinguish the full batch timeout from one fewer member - #483
Merged
Merged
Conversation
kreneskyp
force-pushed
the
code/ir-614-batch-bound
branch
from
October 21, 2026 06:01
ce5149e to
163f26d
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
A batch timeout regression at the Linux
run_groupcall site could survive the existing coverage: four members with a three-second budget finished after eight seconds, inside both the correct twelve-second bound and an incorrect nine-second bound.Add a real bounded-process regression with two members, a twenty-second member budget, and a thirty-second backend stand-in that exports both successful reports. It verifies both members and one launcher, leaving ten seconds between completion and either candidate bound. Production timeout calculation and the existing timing test remain unchanged.
Validation: formatting and locked Clippy over all targets pass. The new test passes through the real Linux supervisor. Temporarily changing only the production call-site argument from
group.len()togroup.len() - 1makes that same test fail withBatchTimedOut { members: 2, timeout: 20s }before report classification; the healthy source is restored byte for byte and passes again. All checks run sequentially in a 16 GiB, zero-swap systemd scope. The lead owns the aggregate gate after independent review.Refs IR-614.