From 37e266926a650bc4d986aa59a99d265aa91c5d1a Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Mon, 17 Aug 2026 20:27:14 -0400
Subject: [PATCH] Run the CBMC-latest perf suite serially to stop runner OOMs

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.
---
 .github/workflows/cbmc-latest.yml | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/cbmc-latest.yml b/.github/workflows/cbmc-latest.yml
index 19bab7c420dc..223ec7f96ad8 100644
--- a/.github/workflows/cbmc-latest.yml
+++ b/.github/workflows/cbmc-latest.yml
@@ -65,6 +65,14 @@ jobs:
 
   perf:
     runs-on: ubuntu-24.04
+    # The perf suite is memory-hungry: the s2n-quic harnesses solve large
+    # formulas, and running them concurrently exhausts a standard runner, which
+    # shows up as an unattributable SIGTERM (exit 143) or "the hosted runner
+    # lost communication with the server" a few minutes into the step rather
+    # than as a test failure. Run serially instead, as kani.yml does. That takes
+    # ~45 min, so the 180-min step timeout leaves ample headroom, and the job
+    # timeout sits above (step timeout) x (max_attempts) so a retry can land.
+    timeout-minutes: 380
     steps:
       - name: Checkout Kani under "kani"
         uses: actions/checkout@v6
@@ -96,10 +104,20 @@ jobs:
           echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH
 
       - name: Execute Kani performance tests
-        working-directory: ./kani
-        run: ./scripts/kani-perf.sh
+        # Run the suite serially and allow one retry, matching the perf job in
+        # kani.yml. `working-directory` is not valid on a `uses` step, so the
+        # command changes directory itself.
+        uses: nick-fields/retry@v4
+        with:
+          timeout_minutes: 180
+          max_attempts: 2
+          command: cd kani && ./scripts/kani-perf.sh
+        env:
+          RUST_TEST_THREADS: 1
 
       - name: Execute Kani performance ignored tests
         working-directory: ./kani
         continue-on-error: true
         run: cargo run -p compiletest -- --suite perf --mode cargo-kani-test ignore --ignored --no-fail-fast
+        env:
+          RUST_TEST_THREADS: 1