smt_solver: validate deep models on a large stack

edgebench/tasks/smt_solver/NOTES.md

@@ -53,6 +53,25 @@ shared host, two runs each. Raw score; 0..100 in brackets.
 Deterministic rows match exactly, including per-logic counts. The timed rows differ by a few cases
 near the 60 s limit; the old-new difference of means is smaller than either side's own spread.
 
+## Changes
+
+### 1.1.0
+
+`validate_sat_witness` recursed with a limit of 20000, more than the default 8 MiB stack holds. On deep
+files a correct `sat` model segfaulted the pool worker and ended the evaluation with no score file,
+which the judge reported as a valid 0 (`correct=0/0`). Validation now runs in a thread with a 2 GiB
+stack (address space; pages are committed as the recursion reaches them) and a recursion limit of
+1,000,000. A correct model deeper than that scores as an invalid model, but the evaluation continues.
+If the thread cannot start or the validator runs out of memory, the evaluation ends as it did on a
+crash, rather than rejecting the model.
+
+The formula and scale are unchanged. Regrade crashed evaluations (a valid 0 with `correct=0/0` from a
+submission that built and ran), and models rejected at the old recursion limit or because the validator
+ran out of memory. Other verdicts stay, on a host that can reserve 2 GiB of address space per validation. At 8 CPUs and 7 GiB a real solver goes from 0.00 to 46.15; of its 354
+models, 350 get the same verdict from both validators and the other 4 are the crashes. Failure-path
+controls are unchanged. Source, Deviations and Regression summary describe 1.0.0. Issue:
+https://github.com/ByteDance-Seed/EdgeBench/issues/42
+
 ## Known issues
 
 Kept as in v1, so scores stay comparable. Fixing any of them changes scores and bumps `version`.

edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py

@@ -26,11 +26,14 @@
 import subprocess
 import sys
 import tempfile
+import threading
 import time
 from concurrent.futures import ProcessPoolExecutor, as_completed
 from pathlib import Path
 
 sys.setrecursionlimit(max(sys.getrecursionlimit(), 20000))
+VALIDATOR_RECURSION_LIMIT = 1_000_000
+VALIDATOR_STACK_BYTES = 2 * 1024**3  # address space; pages are committed as the recursion reaches them
 
 LOGICS = ["QF_UF", "QF_LRA", "QF_LIA", "QF_UFLRA"]
 DIFFICULTIES = ["easy", "medium", "hard"]
@@ -536,6 +539,8 @@ def eval(self, term, env=None):
             try:
                 if self.logic != "QF_UF":
                     return ("num", parse_numeric_literal(term))
+            except MemoryError:
+                raise
             except Exception:
                 pass
             if term in self.decls:
@@ -643,8 +648,37 @@ def validate(self):
             seen[key] = result
 
 
+class ValidatorFailure(BaseException):
+    """The validator could not run, which says nothing about the model. Not an Exception, so that
+    run_solver_case does not record it as an invalid model: it ends the evaluation without a score."""
+
+
 def validate_sat_witness(benchmark_path, witness):
-    WitnessChecker(benchmark_path, witness).validate()
+    # Hard files nest deeply enough to overflow the default stack, which kills the pool worker and ends the
+    # whole evaluation, and to pass 20000 recursions. Too deep even for this is a rejected model, not a crash.
+    box = {}
+
+    def run():
+        limit = sys.getrecursionlimit()
+        sys.setrecursionlimit(VALIDATOR_RECURSION_LIMIT)
+        try:
+            WitnessChecker(benchmark_path, witness).validate()
+        except BaseException as exc:
+            box["exc"] = exc
+        finally:
+            sys.setrecursionlimit(limit)
+
+    try:
+        threading.stack_size(VALIDATOR_STACK_BYTES)
+        thread = threading.Thread(target=run)
+        thread.start()
+    except (RuntimeError, ValueError, MemoryError) as exc:
+        raise ValidatorFailure(f"cannot start the validator thread: {exc}") from exc
+    thread.join()
+    if isinstance(box.get("exc"), MemoryError):
+        raise ValidatorFailure("the validator ran out of memory")
+    if "exc" in box:
+        raise box["exc"]
 
 
 def parse_solver_output(stdout):

edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py

@@ -26,11 +26,14 @@
 import subprocess
 import sys
 import tempfile
+import threading
 import time
 from concurrent.futures import ProcessPoolExecutor, as_completed
 from pathlib import Path
 
 sys.setrecursionlimit(max(sys.getrecursionlimit(), 20000))
+VALIDATOR_RECURSION_LIMIT = 1_000_000
+VALIDATOR_STACK_BYTES = 2 * 1024**3  # address space; pages are committed as the recursion reaches them
 
 LOGICS = ["QF_UF", "QF_LRA", "QF_LIA", "QF_UFLRA"]
 DIFFICULTIES = ["easy", "medium", "hard"]
@@ -536,6 +539,8 @@ def eval(self, term, env=None):
             try:
                 if self.logic != "QF_UF":
                     return ("num", parse_numeric_literal(term))
+            except MemoryError:
+                raise
             except Exception:
                 pass
             if term in self.decls:
@@ -643,8 +648,37 @@ def validate(self):
             seen[key] = result
 
 
+class ValidatorFailure(BaseException):
+    """The validator could not run, which says nothing about the model. Not an Exception, so that
+    run_solver_case does not record it as an invalid model: it ends the evaluation without a score."""
+
+
 def validate_sat_witness(benchmark_path, witness):
-    WitnessChecker(benchmark_path, witness).validate()
+    # Hard files nest deeply enough to overflow the default stack, which kills the pool worker and ends the
+    # whole evaluation, and to pass 20000 recursions. Too deep even for this is a rejected model, not a crash.
+    box = {}
+
+    def run():
+        limit = sys.getrecursionlimit()
+        sys.setrecursionlimit(VALIDATOR_RECURSION_LIMIT)
+        try:
+            WitnessChecker(benchmark_path, witness).validate()
+        except BaseException as exc:
+            box["exc"] = exc
+        finally:
+            sys.setrecursionlimit(limit)
+
+    try:
+        threading.stack_size(VALIDATOR_STACK_BYTES)
+        thread = threading.Thread(target=run)
+        thread.start()
+    except (RuntimeError, ValueError, MemoryError) as exc:
+        raise ValidatorFailure(f"cannot start the validator thread: {exc}") from exc
+    thread.join()
+    if isinstance(box.get("exc"), MemoryError):
+        raise ValidatorFailure("the validator ran out of memory")
+    if "exc" in box:
+        raise box["exc"]
 
 
 def parse_solver_output(stdout):

edgebench/tasks/smt_solver/task.toml

@@ -4,7 +4,7 @@ name = "Smt Solver"
 category = "Combinatorial Optimization"
 language = "Python"
 description = "Build an SMT solver from scratch for four quantifier-free theories (uninterpreted functions, linear real and integer arithmetic, and their combination). External SMT solvers are forbidden; model witnesses are independently validated."
-version = "1.0.0"
+version = "1.1.0"
 status = "migrated"
 
 [environment]