Run the CBMC-latest perf suite serially to stop runner OOMs - #4742
Open
feliperodri wants to merge 1 commit into
Open
Run the CBMC-latest perf suite serially to stop runner OOMs#4742feliperodri wants to merge 1 commit into
feliperodri wants to merge 1 commit into
Conversation
The `perf` job of the "Nightly: CBMC Latest" workflow has failed every day since 2026-07-25, and most days since February. The failure is not a CBMC incompatibility: the three `regression` jobs pass against the same CBMC HEAD, and the step annotations report `exit code 143` (SIGTERM) or "the hosted runner lost communication with the server", 5-9 minutes into a step that takes ~27 minutes when it succeeds. Runs 1300 (green) and 1301 (red) ran the same Kani commit, and CBMC had no commits in that window, so nothing in either code base changed - the job simply stopped getting lucky on memory. `kani.yml` runs the same `scripts/kani-perf.sh` with `RUST_TEST_THREADS: 1` and a retry, but this workflow was never updated to match, so compiletest defaults to `available_parallelism()` and solves several heavy s2n-quic harnesses at once. Serialize the suite here too, allow one retry for genuine infra failures, and raise the job timeout above (step timeout) x (max_attempts) so a retry can land. Note `working-directory` is not valid on a `uses` step, so the retried command changes directory itself.
feliperodri
added
the
[I] CI / Infrastructure
feliperodri
enabled auto-merge
August 18, 2026 14:50
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
1 participant
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.
The
perfjob of the "Nightly: CBMC Latest" workflow has failed every day since 2026-07-25, and most days since February. The failure is not a CBMC incompatibility: the threeregressionjobs pass against the same CBMC HEAD, and the step annotations reportexit code 143(SIGTERM) or "the hosted runner lost communication with the server", 5-9 minutes into a step that takes ~27 minutes when it succeeds. Runs 1300 (green) and 1301 (red) ran the same Kani commit, and CBMC had no commits in that window, so nothing in either code base changed - the job simply stopped getting lucky on memory.kani.ymlruns the samescripts/kani-perf.shwithRUST_TEST_THREADS: 1and a retry, but this workflow was never updated to match, so compiletest defaults toavailable_parallelism()and solves several heavy s2n-quic harnesses at once. Serialize the suite here too, allow one retry for genuine infra failures, and raise the job timeout above (step timeout) x (max_attempts) so a retry can land.Note
working-directoryis not valid on ausesstep, so the retried command changes directory itself.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.