From c65479e37ff2e8dd67a37c811153fa47abec61d3 Mon Sep 17 00:00:00 2001
From: zuub-don <don@codetestcode.io>
Date: Wed, 19 Aug 2026 06:47:03 -0700
Subject: [PATCH] fix(verify): stop the resource guardrail from killing the JVM
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The nightly run's model checking job failed within a second of starting, on
main, with no explanation printed. Two bugs, and the second is why the first
was invisible.

`ulimit -v` is the wrong instrument for a JVM. It reserves far more address
space than it ever commits — compressed class space alone asks for a
gigabyte before any heap — so a virtual ceiling sized to the intended heap
stops it starting at all. It fails as "Could not allocate compressed class
space", which reads like a memory shortage and is actually the guardrail.
This never showed locally because the machine it was written on has enough
RAM that a quarter of it left plenty of headroom; the CI runner has 16GB, so
the quarter share was 4GB and the JVM could not start.

The heap is capped with -Xmx instead, which is the JVM's own instrument and
is precise about what it limits. `ulimit -v` still applies to native
processes, where it does what it was meant to.

The silence was separate. The failure path filtered TLC's output through
grep, and a grep that matches nothing exits non-zero — which under
`set -o pipefail` aborted the script before it printed anything. The one run
that failed was the one run that explained nothing. It now prints the output
unfiltered.

Verified by reproducing the CI budget locally: passes at 3997MB, and a
deliberately starved heap now reports "Too small maximum heap" rather than
exiting mute.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 verify/budget.sh | 22 ++++++++++++++++++++--
 verify/tla.sh    |  8 ++++++--
 2 files changed, 26 insertions(+), 4 deletions(-)

diff --git a/verify/budget.sh b/verify/budget.sh
index 549bc70..4a47c7f 100755
--- a/verify/budget.sh
+++ b/verify/budget.sh
@@ -50,10 +50,28 @@ guard_load() {
 }
 
 # Run a command inside the budget: capped memory, capped time, low priority.
+#
+# The virtual-memory ceiling turns a runaway into a clean allocation failure
+# rather than an OOM kill that takes something else with it. It suits native
+# processes; see `budgeted_jvm` for why it does not suit a JVM.
 budgeted() {
   guard_load
-  # A virtual-memory ceiling turns a runaway into a clean allocation failure
-  # rather than an OOM kill that takes something else with it.
   ( ulimit -v $(( VERIFY_MEM_MB * 1024 )) 2>/dev/null || true
     exec nice -n "$VERIFY_NICE" ionice -c3 timeout --signal=INT "$VERIFY_TIMEOUT" "$@" )
 }
+
+# As above, without the virtual-memory ceiling.
+#
+# A JVM reserves far more address space than it will ever commit -- compressed
+# class space alone asks for a gigabyte before any heap -- so `ulimit -v` sized
+# to the intended heap stops it starting at all. It fails as
+# "Could not allocate compressed class space", which reads like a memory
+# shortage and is really the guardrail. Found when this ran on a CI box with a
+# smaller budget than the machine it was written on.
+#
+# The heap is capped by -Xmx instead, which is the JVM's own instrument for the
+# job and is precise about what it limits.
+budgeted_jvm() {
+  guard_load
+  nice -n "$VERIFY_NICE" ionice -c3 timeout --signal=INT "$VERIFY_TIMEOUT" "$@"
+}
diff --git a/verify/tla.sh b/verify/tla.sh
index 6d15073..c84028f 100755
--- a/verify/tla.sh
+++ b/verify/tla.sh
@@ -33,7 +33,7 @@ echo "TLC: ${VERIFY_JOBS} workers, ${TLC_HEAP} heap"
 echo
 
 run_tlc() {
-  budgeted java -XX:+UseParallelGC -Xmx"$TLC_HEAP" -cp "$JAR" tlc2.TLC \
+  budgeted_jvm java -XX:+UseParallelGC -Xmx"$TLC_HEAP" -cp "$JAR" tlc2.TLC \
     -workers "$VERIFY_JOBS" -nowarning -config "$1" Gossip.tla 2>&1
 }
 
@@ -42,8 +42,12 @@ if out=$(run_tlc Gossip.cfg) && grep -q "Model checking completed. No error has
   grep -E "^[0-9]+ states|^The depth" <<<"$out" | sed 's/^/  /'
   echo "  PASS: converges on every schedule"
 else
-  grep -E "^Error|^State [0-9]+|/\\\\ known" <<<"$out" | head -20 | sed 's/^/  /'
   echo "  FAIL: the fix does not hold" >&2
+  # Print everything rather than a filtered view. A grep that matches nothing
+  # returns non-zero, and under `set -o pipefail` that used to abort the script
+  # before it said anything at all -- so the one run that failed was the one
+  # run with no explanation.
+  sed 's/^/  | /' <<<"$out" | tail -30 >&2
   exit 1
 fi