Cap harness parallelism on ubuntu partition runners

Both ubuntu-latest 'Verify std library (partition 1)' jobs died with
'The runner has received a shutdown signal' while verifying the
ffi::c_str harnesses; the macos jobs passed. run-kani.sh passes -j
(one thread per core) to kani, so the 4-core/16 GB ubuntu runners
verify four harnesses concurrently. With the new Kani/CBMC pin the
c_str harnesses have grown memory-hungry - measured individually with
CI-equivalent flags (--no-assert-contracts, --object-bits 12):

  check_from_bytes_with_nul  9.6 GB
  check_to_str               5.4 GB
  check_as_ptr               3.1 GB
  check_bytes                3.1 GB
  check_count_bytes          1.7 GB

Four such harnesses in flight exceed 16 GB, OOM-killing the runner.

Introduce KANI_JOBS to let CI cap the number of parallel harnesses and
set it to 2 for the ubuntu partition jobs. The heaviest known cluster
(the four c_str harnesses above) then peaks at ~13.4 GB of concurrent
solver memory (measured by sampling the process tree), which fits the
runner with headroom to spare. macos jobs keep the full -j behavior.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

.github/workflows/kani.yml

@@ -35,6 +35,10 @@ jobs:
       WORKER_INDEX: ${{ matrix.partition }}
       # Total number of workers running this step
       WORKER_TOTAL: 4
+      # Cap parallel harness verification on ubuntu-latest: its 4-core/16 GB
+      # runners get OOM-killed when 4 memory-hungry harnesses (up to ~10 GB
+      # each, e.g. the ffi::c_str ones) run concurrently.
+      KANI_JOBS: ${{ matrix.os == 'ubuntu-latest' && 2 || '' }}
 
     steps:
       - name: Remove unnecessary software to free up disk space

scripts/run-kani.sh

@@ -213,11 +213,18 @@ run_verification_subset() {
 
     echo "Running verification for harnesses:"
     printf '%s\n' "${harnesses[@]}"
+    # Use KANI_JOBS to cap the number of parallel harnesses; some harnesses peak
+    # at close to 10 GB of memory, so running one per core can exhaust the
+    # memory of smaller CI runners (e.g., 4-core/16 GB ubuntu-latest).
+    local jobs_arg="-j"
+    if [[ -n "${KANI_JOBS:-}" ]]; then
+        jobs_arg="--jobs=${KANI_JOBS}"
+    fi
     "$kani_path" verify-std -Z unstable-options ./library \
         $unstable_args \
         --no-assert-contracts \
         $harness_args --exact \
-        -j \
+        $jobs_arg \
         --output-format=terse \
         "${command_args[@]}" \
         --cbmc-args --object-bits 12