[GuilhermeBn198]

Why

The Test-Comp 2027 pre-run (map2check.2026-10-29_21-07-49: 900 s, 3 GB, 1 core) ended 1,747 of 16,288 runs as OUT OF MEMORY, and 34 with no measurements (FAILED, killed by signal 1). BenchExec enforces the limit on the run's whole cgroup, tmpfs included, and none of the engines knew it. From the official logs:

• 821 runs died in KLEE's seeding loop. KLEE 3.1 never calls checkMemoryUsage() there, so --max-memory has no effect.
• About 200 runs had KLEE at its fixed 2,000 MB cap. That cap plus the files in tmpfs exceeds 3 GB.
• 239 runs died in the first AFL++ phase. afl-fuzz runs its target with no memory limit.

(The 14,507 ERROR runs all end with DONE. They are fixed by sosy-lab/benchexec#1352, merged on Nov 2.)

Changes

• utils/memory_budget.hpp (new): reads the run's limit from its cgroup v2 memory.max, walking up to the closest cgroup that has one. Inside BenchExec's container this is the namespace root. MAP2CHECK_MEMORY_LIMIT_MB overrides it. With no limit found, nothing changes.
• KLEE:
  • --max-memory is 40% of the limit, at most KLEE's default of 2,000 MB. A 15 GB run keeps the cap it had, and MAP2CHECK_KLEE_MAX_MEMORY still wins.
  • The watchdog in runKleeWatched reads memory.current every 0.5 s, during seeding too. At 80% of the limit it sends SIGINT, so KLEE halts and writes its tests. At 92% it sends SIGKILL. A phase stopped this way counts as incomplete (stoppedForMemory), never TRUE.
• Native programs: the afl-fuzz target (-m) and the replays of vectors (ulimit -v) get a third of the limit, at least 256 MB.
• AFL++: when afl-fuzz returns, any of its targets still alive is killed. afl-fuzz starts its forkservers with setsid() (afl-forkserver.c:1066, 4.40c), so when timeout -k SIGKILLs it, a running target survives. Measured on one run: 871 s of wall time, 909 s of CPU time, TIMEOUT. With the cleanup the same task ends done at 863 s of CPU for 860 s of wall.
• Wrapper: the margin between Map2Check's wall-clock budget and the CPU limit goes from 20 s to 30 s. Under BenchExec the CPU time came out up to 22 s above the wall time.

Tests

• MemoryBudgetTest (8 unit tests): fake cgroup trees (namespace root, nested, no limit, no cgroupfs), the env override, and the KLEE, native and halt/kill thresholds.
• test_fuzzer_leftovers.sh (new, added to CI): a fake afl-fuzz leaves a process named like the target in a new session. RED: it survives map2check. GREEN: it is gone.
• CI integration suites: all 13 pass on install_mg inside a 3 GB container, so with the governor active. test_benchexec_toolinfo.py: 24/24.
• A/B on BenchExec 3.34 (900 s / 3 GB / 1 core): the Zenodo 23672409 archive vs. this branch. The three Cover-Branches tasks that are OOM in the base finish, and TestCov coverage rises on all four. The TDX havoc_object task in Cover-Error is no longer OOM. A second run of this arm with the cleanup: all 6 tasks done. The final archive passes the smoke test on a clean ubuntu:24.04. Details and caveats are in docs/reports/tacas-experiment-log.md (2026-11-07).