Exclude managed Docker pauses from execution budgets

Makefile

@@ -1,6 +1,7 @@
 CHECKER_SOURCES := \
 	src/common/__init__.py \
 	src/common/check_proof.py \
+	src/common/active_clock.py \
 	src/common/verification_budget.py \
 	src/common/verification_toolchain.py \
 	src/common/cheating_detection.py \

docs/PAUSING.md

@@ -0,0 +1,78 @@
+# Pausing Docker experiments
+
+New Docker runs on Linux hosts provide a host-owned clock for managed pauses. Use:
+
+```sh
+tlaps-bench pause-container CONTAINER_NAME
+tlaps-bench resume-container CONTAINER_NAME
+```
+
+A quota guard can call these commands in place of `docker pause` and `docker
+unpause`, checking the exit status before recording a successful transition.
+Both commands are idempotent. The container name or ID is the same one accepted
+by Docker. Preflight containers are deliberately not pausable through this API.
+
+The runner's agent deadline and `agent_time_secs`, the grader envelope, and the
+official checker's SANY/TLAPM envelope subtract recorded pauses. Ordinary idle
+time, network/API waits, and solver execution still consume time. This is an
+elapsed-time budget, not a CPU-time budget.
+
+Claude Code benchmark launches set `CLAUDE_CODE_PRINT_BG_WAIT_CEILING_MS=0` in
+their child environment. This disables print mode's wall-clock ceiling for
+pending background tasks, which can otherwise terminate them immediately after
+a long freeze. The benchmark's configured `--timeout` remains the execution
+limit; `--timeout 0` intentionally has no overall limit. The caller's environment
+is unchanged. This setting does not suspend raw shell `timeout` commands or
+TLAPM/solver internal timers, and does not alter already-running Claude sessions.
+
+Docker agent results also record `agent_wall_time_secs` and
+`agent_paused_time_secs`; the difference is the measured active process runtime.
+On timeout, the existing `agent_time_secs` cap can additionally exclude shutdown
+or output-draining overhead. Verification
+reports retain `wall_secs` and add `active_secs` and `paused_secs`. Check-session
+recovery charges the persisted active budget; old sessions without these fields
+conservatively charge their entire recorded wall time. Self-check and formal
+grading keep independent budgets and cache namespaces.
+
+Each launch owns a durable ledger under `~/.tlaps-bench/runtime-clocks/`, outside
+the agent's writable mounts. The directory is mounted read-only at
+`/run/tlaps-bench-clock`. Its host path is recorded in the Docker label
+`org.specula.tlaps-bench.active-clock`; an `active-clock.json` snapshot is copied
+beside the launch's output after it exits. Retain the host ledger while retaining
+or inspecting its container. The clock uses the Linux boot ID and monotonic time
+and the host rejects a ledger from a previous host boot. The runner and Docker
+container must share the Linux monotonic clock domain. An incompatible clock
+epoch, or a host wall-clock adjustment over five seconds since clock creation,
+fails closed rather than producing an untrustworthy budget measurement.
+
+The controller freezes the container before writing the pause start, and durably
+closes the interval before thawing it. Host clock readers share the controller's
+lock so they cannot observe a half-published transition. Container readers check
+for concurrent publication without holding that lock across a freeze.
+Freeze-command transit before the recorded start and thaw-command transit after
+the close are conservatively charged. If the controller crashes between Docker and ledger
+updates, rerunning the command recovers the Docker state, but any unrecorded
+interval stays charged and the command reports that fact. A checker hard crash
+retains the existing write-ahead reservation of at most one heartbeat tick;
+restart downtime is not a new examination. As before, incomplete measurements
+after a hard crash should not be treated as complete wall/CPU telemetry.
+
+Boundaries:
+
+- This requires a new run and a checker image built from the updated source.
+  Existing containers lack the clock mount; the control commands reject them.
+  It does not retroactively repair previous experiment results.
+- Docker launches from non-Linux hosts keep their existing wall-clock budgets
+  and do not expose managed pause control.
+- Plain `docker pause/unpause`, process signals, machine suspension, and an
+  external guard that has not adopted these commands are not tracked. In
+  particular, never thaw a managed pause directly: the ledger would remain
+  paused. The controller detects that mismatch on its next invocation and
+  rejects it; that run's accounting needs investigation.
+- A backend that propagates an absolute deadline to its own child rejects
+  managed pauses until that backend supports the active clock.
+- Arbitrary shell `timeout`, CLI/tool timeouts, and TLAPM/solver internal tactic
+  timers retain their own semantics. They can expire during a freeze even though
+  the official checker envelope has time left. An experiment that requires those
+  internal timers to be unaffected must pause between checks instead of freezing
+  an active check. No proof-validation rule or timeout verdict is relaxed.

src/common/active_clock.py

@@ -0,0 +1,168 @@
+"""Elapsed wall time minus explicitly recorded, host-controlled container pauses."""
+
+from __future__ import annotations
+
+import fcntl
+import json
+import math
+import os
+import subprocess
+import tempfile
+import time
+from dataclasses import dataclass
+from pathlib import Path
+
+CLOCK_ENV = "TLAPS_ACTIVE_CLOCK"
+CLOCK_MOUNT = "/run/tlaps-bench-clock"
+CLOCK_LABEL = "org.specula.tlaps-bench.active-clock"
+POLL_SECS = 0.1
+
+
+def boot_id() -> str:
+    return Path("/proc/sys/kernel/random/boot_id").read_text().strip()
+
+
+def write_state(path: Path, state: dict) -> None:
+    """Publish before thawing; fsync both the file and its directory."""
+    with tempfile.NamedTemporaryFile(mode="w", dir=path.parent, delete=False) as stream:
+        temporary = Path(stream.name)
+        try:
+            json.dump(state, stream, allow_nan=False, sort_keys=True)
+            stream.flush()
+            os.fsync(stream.fileno())
+            os.chmod(temporary, 0o644)
+            os.replace(temporary, path)
+            fd = os.open(path.parent, os.O_RDONLY | os.O_DIRECTORY)
+            try:
+                os.fsync(fd)
+            finally:
+                os.close(fd)
+        finally:
+            temporary.unlink(missing_ok=True)
+
+
+@dataclass(frozen=True)
+class ClockReading:
+    wall: float
+    paused: float
+
+    @property
+    def active(self) -> float:
+        return self.wall - self.paused
+
+
+class ActiveClock:
+    def __init__(self, path: Path | None = None, *, verify_host_boot: bool = True):
+        self.path = path
+        self._host_reader = verify_host_boot
+        self._boot_id = boot_id() if path and verify_host_boot else None
+
+    @classmethod
+    def from_environment(cls):
+        value = os.environ.get(CLOCK_ENV)
+        # A container's proc namespace can expose a different boot ID even
+        # while sharing CLOCK_MONOTONIC with the host. The host controller
+        # validates the host boot; readers pin the ledger's initial identity.
+        return cls(Path(value) if value else None, verify_host_boot=False)
+
+    @classmethod
+    def create(cls, directory: Path, *, pause_supported: bool = True):
+        directory.mkdir(parents=True, exist_ok=False)
+        directory.chmod(0o755)
+        path = directory / "state.json"
+        (directory / "control.lock").touch(mode=0o644)
+        write_state(
+            path,
+            {
+                "version": 1,
+                "boot_id": boot_id(),
+                "pauses": [],
+                "pause_supported": pause_supported,
+                "monotonic_origin": time.monotonic(),
+                "wall_origin": time.time(),
+            },
+        )
+        return cls(path)
+
+    def read_state(self) -> dict:
+        try:
+            state = json.loads(self.path.read_text())
+            if state["version"] != 1 or not isinstance(state["boot_id"], str) or not state["boot_id"]:
+                raise ValueError("incompatible clock or host reboot")
+            if self._boot_id is None:
+                self._boot_id = state["boot_id"]
+            elif state["boot_id"] != self._boot_id:
+                raise ValueError("incompatible clock or host reboot")
+            if type(state["pause_supported"]) is not bool or type(state["pauses"]) is not list:
+                raise ValueError("invalid pause ledger")
+            for field in ("monotonic_origin", "wall_origin"):
+                if type(state[field]) not in (float, int) or not math.isfinite(state[field]):
+                    raise ValueError("invalid clock origin")
+            previous = 0.0
+            for index, interval in enumerate(state["pauses"]):
+                start, end = interval
+                if type(start) not in (float, int) or not math.isfinite(start) or start < previous:
+                    raise ValueError("invalid pause start")
+                if end is None:
+                    if index != len(state["pauses"]) - 1:
+                        raise ValueError("unfinished pause is not last")
+                elif type(end) not in (float, int) or not math.isfinite(end) or end < start:
+                    raise ValueError("invalid pause end")
+                previous = end if end is not None else start
+            return state
+        except (OSError, ValueError, TypeError, KeyError) as exc:
+            raise OSError(f"cannot read trusted active clock: {exc}") from exc
+
+    def read(self) -> ClockReading:
+        if self.path is None:
+            return ClockReading(time.monotonic(), 0.0)
+        if self._host_reader:
+            # Host observations must not race a controller's sampled timestamp
+            # and its durable publication. Container readers cannot take this
+            # lock: freezing a shared-lock holder would deadlock the controller.
+            with (self.path.parent / "control.lock").open("r") as lock:
+                fcntl.flock(lock, fcntl.LOCK_SH)
+                return self._read_snapshot()
+        return self._read_snapshot()
+
+    def _read_snapshot(self) -> ClockReading:
+        # A container may freeze between *any* two instructions, including
+        # between reading the ledger and sampling monotonic. Verify the same
+        # durable state on both sides of the timestamp before using it.
+        while True:
+            state = self.read_state()
+            now = time.monotonic()
+            wall = time.time()
+            if state == self.read_state():
+                break
+        if abs((now - state["monotonic_origin"]) - (wall - state["wall_origin"])) > 5:
+            raise OSError("active clock has a different monotonic epoch or the host wall clock changed by over 5s")
+        paused = 0.0
+        for start, end in state["pauses"]:
+            if start > now or (end is not None and end > now):
+                raise OSError("active-clock interval lies in the future")
+            paused += (now if end is None else end) - start
+        return ClockReading(now, paused)
+
+    def now(self) -> float:
+        return self.read().active
+
+
+def communicate(proc, timeout, *, clock: ActiveClock | None = None, input=None):
+    """Drain pipes while bounding active elapsed, including ordinary idle/API waits.
+
+    A short wall-clock poll may expire while the container is frozen. Recheck
+    the host ledger before deciding that the actual budget has expired.
+    """
+    clock = clock or ActiveClock.from_environment()
+    if clock.path is None or timeout is None:
+        return proc.communicate(input=input, timeout=timeout)
+    deadline = clock.now() + timeout
+    while True:
+        remaining = deadline - clock.now()
+        try:
+            return proc.communicate(input=input, timeout=max(0, min(POLL_SECS, remaining)))
+        except subprocess.TimeoutExpired as exc:
+            input = None  # Popen retains partially written input across calls.
+            if clock.now() >= deadline:
+                raise subprocess.TimeoutExpired(exc.cmd, timeout, output=exc.output, stderr=exc.stderr) from exc

src/common/check_proof.py

@@ -63,7 +63,6 @@
 import subprocess
 import sys
 import tempfile
-import time
 from concurrent.futures import ThreadPoolExecutor
 from dataclasses import asdict
 from pathlib import Path
@@ -204,7 +203,9 @@ def run_killgroup(cmd, timeout, cwd):
         start_new_session=True,
     )
     try:
-        out, err = proc.communicate(timeout=timeout)
+        from common.active_clock import communicate
+
+        out, err = communicate(proc, timeout)
         return out, err, proc.returncode
     except BaseException:
         # Interrupting a check must also stop its backends before recovery.
@@ -1217,7 +1218,9 @@ def _module_unit_result(
             "SANY did not provide a valid theorem location",
         )
 
-    remaining = None if deadline is None else deadline - time.monotonic()
+    from common.active_clock import ActiveClock
+
+    remaining = None if deadline is None else deadline - ActiveClock.from_environment().now()
     if remaining is not None and remaining <= 0:
         return (
             {
@@ -1463,7 +1466,7 @@ def _run_module_task_check(
             emit(f"ERROR: cannot stage module task inputs: {exc}")
             return 3
 
-        remaining = None if deadline is None else deadline - time.monotonic()
+        remaining = session.remaining()
         if remaining is not None and remaining <= 0 and session.load("submitted-sany") is None:
             emit("SANY-STATUS: unavailable")
             emit("CHECK-TIMEOUT: module checker budget exhausted before SANY validation")
@@ -1498,7 +1501,7 @@ def _run_module_task_check(
             return 1
 
         assert sany_run.raw is not None
-        remaining = None if deadline is None else deadline - time.monotonic()
+        remaining = session.remaining()
         if remaining is not None and remaining <= 0 and session.load("canonical-sany") is None:
             emit("CHECK-TIMEOUT: module checker budget exhausted before canonical SANY validation")
             emit("ERROR: module checker timeout exhausted before canonical SANY validation")