[nils-loose]

Addresses #51: SV-COMP runs now stay inside the competition's limits (15 GB, 900 s CPU, 4 cores) and stop with UNKNOWN instead of being killed.

What changed and why

• One resource budget (symbolic-explorer/svcomp/ResourceBudget.py): the explorer and every executor JVM share it. A monitor thread polls the RSS and CPU time of the explorer and its descendants every 0.2 s. Where the memory limit comes from a cgroup (BenchExec, systemd scope), the CPU time is at least the cgroup's cpu.stat.
  • Defaults are the competition limits: --memory-limit 15000 (MB, i.e. BenchExec's 15e9 bytes) and --cpu-limit 900. A lower cgroup memory.max wins. --cpu-used adds CPU time spent before the explorer started.
  • Executor heap is derived from the limit: -Xmx5483m for 15 GB, replacing -Xmx32g. JavaSMT's Z3 context grows outside the heap at about the heap's rate: with -Xmx12g the executor RSS reached 14-15 GB.
  • 2 GB below the memory limit:
    • A running executor is killed with SIGKILL (a SIGTERM would let the shutdown hook send a cut-short trace), and exploration continues with other branches.
    • A running Z3 query is interrupted. If it is still over the limit 1 s later, or within 1 GB of the limit, the run ends with UNKNOWN. Z3 ignores interrupts while bit-blasting and grew by 2 GB/s on Conflict. Z3's own memory_max_size was tried and dropped because it made Z3 abort the process.
  • 20 s before the CPU limit: exploration stops with UNKNOWN. A violation that the stopped run printed is still reported.
  • Soundness: a run that was cut short (killed by the budget, or an OutOfMemoryError in the executor) leaves its path unexplored. It is recorded as resource_limit / out_of_memory and rules out SAFE, like the existing downgrades. Its (missing) trace is not checked for divergence. stats.json gets a resources section.
• Executor JVM uses C1 only (-XX:TieredStopAtLevel=1). Every round is a fresh JVM that runs 1-3 s. On 4 cores, C2 compiler threads took 41-44 % of the executor CPU and GC took 0.2 %. Same 120 s CPU: 22-53 % more rounds (MinePump 44→63, TCAS 59→90, Ramp-and-Hold 49→60). SerialGC and -Xint did not help.
• Competition package:
  • run_swat.py passes the CPU time used by copying and compiling the task.
  • run_swat.py no longer buffers and re-logs the explorer output. After 900 s that took over 20 s of CPU, so BenchExec still reported TIMEOUT, and it held hundreds of MB in memory. The output is now passed straight through, and the verdict for printing the witness is read from stats.json.
  • In sv-comp mode, the root logger stays at WARNING (the module DEBUG/INFO lines were 500 MB of stdout in 900 s).
  • The per-node [DFS] line now logs below DEBUG (270 MB of explorer.log).
  • BenchExec containers keep both in RAM.
• Local harness: svcomp test run passes --testcase-timeout-s as --cpu-limit.
• Removed: the unused svcomp/SVCompHandler.py (dead code with -Xmx32g and the 60 s timeout). The remaining 60 s defaults are in non-sv-comp drivers, or are overridden with None in sv-comp mode.

Measurements

Config: --sv-comp, nosa, cgroup MemoryMax=15000000000, explorer --cpu-limit = harness limit. Base is the integration branch.

set	runs	result
all baseline-correct runs, 300 s, 2 cores	1047	0 flips; total CPU to verdict -28 % (median -26 %, no run slower than 1.03x); max peak RSS 459 MB
re-check of 70 of them on the final commit	70	0 flips
affected (heap-over-15g, uncaught-oom KB records; all baseline oom/no-verdict runs) + 8 long timeouts, 900 s, 4 cores	55	0 point changes. Base: 27 OOM kills, 12 timeouts, 1 stall. New: all 55 end with a verdict (54 UNKNOWN, 1 VIOLATION same as base at 900 s)
runexec (BenchExec 3.35) of the package, 15e9 B / 900 s CPU / 960 s wall	4	SpdyStream VIOLATION + witness; Conflict UNKNOWN (peak 14.3 GB); BinaryTreeSearch-MemSat01 UNKNOWN (13.3 GB); MinePump spec1-5_product11 UNKNOWN at 881 s CPU. Before the cgroup-CPU and output fixes, the last one was TIMEOUT

New wrong verdicts: 0. Net points: 0. The gain is that 40 runs which used to be OOM/TIMEOUT/stall now give a clean UNKNOWN, and there is more exploration per CPU second. On the 900 s timeout sample, rounds went up 3-28 % (TCAS 363→464, HPack 265→322). Adjustable-Inner-Count-Halving finds its VIOLATION after 289 s instead of 379 s, which would be +1 under a 300 s limit.

The quick "oom" runs (4-6 s at 190 MB): these are not target OOMs. /usr/bin/time only counted the explorer, because the killed JVM was never waited for. The executor actually ran for about 150 s: the solver picked a nondet loop bound of 2^30 (BinaryTreeSearch-*, SortedListInsert, SatFibonacci, DistinguishedNameParser, InfiniteLoop), and the trace grew until the cgroup limit, about half of it Z3 native memory. They now end UNKNOWN. A target OutOfMemoryError (new int[2^31-1] in InsertionSort/MergeSort/Tsp) is not a property violation: it is neither a RuntimeException nor an assert. These runs already ended UNKNOWN, and now they are explicitly recorded as out_of_memory.

CPU vs wall (4 cores): base 1.17-1.6 CPU-s per wall-s on long runs, C1-only 1.02-1.16. So the 900 s CPU limit is reached after 760-860 s of wall time, before the 960 s hard wall limit.

Tests

tests/test_resource_budget.py (23 cases):

• cgroup v1/v2 limit and CPU parsing;
• the derived limits;
• the monitor killing the executor / interrupting a query / ending the run;
• driver verdicts after a stopped run;
• no query after the deadline.

The existing explorer unit tests pass.

Known limits

• Executor runs that never finish (2^30-iteration loops) still use CPU until the deadline. A per-round budget is not part of this PR.
• The memory stop relies on polling. The executor was seen growing by 2 GB/s, which the 2 GB headroom covers.
• The runexec check ran without cpuset delegation (cores pinned with taskset) and on a hand-assembled package directory, not a built archive. A full BenchExec campaign was not run.
• Pre-existing, not changed here: a ClassNotFoundException of Main gives "No symbolic vars" and therefore SAFE.

🤖 Generated with Claude Code

[nils-loose]

Included in dev through #92 (merge commit 534c182), together with the fixes for interactions between PRs. This PR stays as the record of the change and its measured flips.