Coupled timeouts: runner SIGKILL drops final JSON, requires duplicate inner deadline

Problem

etna experiment run --params timeout=N enforces the per-trial budget by wrapping the solve subprocess in run_command_with_timeout(N) (src/process.rs). When the budget elapses, the runner gets a hard SIGKILL.

That SIGKILL is unceremonious:

• the runner's final println!/JSON line is dropped,
• the driver's log_process_output sees a non-zero exit,
• the trial is recorded as status: aborted with no metrics,
• any progress (counterexample, trial count, timings) is lost.

The only way today to get a clean passed result on long-running random search is to have the runner enforce its own deadline that fires strictly before the outer SIGKILL. The cedar-lean workload does this:

-- in EtnaCedar.Main, the random-search loop:
if (← IO.monoMsNow) ≥ deadline then break    -- self-stop, fall through to clean JSON

-- defaults
defaultRuntimeMs := 55_000   -- 5 s under the assumed 60 s outer timeout

This is brittle: the runner has to guess how much time to leave for the JSON write + stdout flush + process exit + driver wait(). Get it wrong and the cooperative path doesn't fire. The two knobs (--params timeout=N and the workload's hardcoded inner deadline) are now coupled but advertised separately, so changing the outer requires recompiling/republishing the workload.

Repro

# Workload runner that loops forever and never emits.
echo '#!/bin/bash
while true; do sleep 1; done' > /tmp/loop.sh && chmod +x /tmp/loop.sh

# Wire it into a tiny steps.json with capabilities.solve = /tmp/loop.sh.
# Then: etna experiment run --params timeout=5
# Result: status=aborted, no metrics, no counterexample.

Suggested fixes (pick one)

A. Pass the timeout to the runner so it can self-stop cooperatively

Inject an env var (e.g. ETNA_TIMEOUT_MS) into the solve command's environment whenever run_command_with_timeout is invoked. Workloads that want graceful shutdown read it; workloads that don't are unchanged. ~10 LOC in src/driver.rs.

B. SIGTERM-then-SIGKILL with a grace window

run_command_with_timeout currently kills outright. Send SIGTERM at timeout, wait grace_period (e.g. 2 s), then SIGKILL if the child hasn't exited. Cooperative runners can install a SIGTERM handler that flushes the final JSON and exits. ~20 LOC in src/process.rs.

C. Both

A + B together: deadlines via env for runners that prefer that style, signals for runners that prefer that style. SIGTERM is the standard "graceful" semantic; ENV is friendlier for languages without robust signal handling (Lean, Python, Haskell stack runtime, …).

Why now

Lifting cedar-lean's per-trial cap from 200 to 1,000,000 trials made this pain visible — slow properties run for the full 60 s and would have been silently aborted without the inner deadline workaround. As more workloads adopt long random-search budgets, every workload will need the same coupled-deadline hack.

Related

• alpaylan/cedar-etna's runner: https://github.com/alpaylan/cedar-etna/blob/main/cedar-lean/EtnaCedar/Main.lean (see defaultRuntimeMs, getRuntimeBudgetMs)
• The run_command_with_timeout implementation: src/process.rs (alpaylan/etna-cli)

Start by reading run_command_with_timeout in src/process.rs and the solve-command handling in src/driver.rs, then reproduce the behavior with the /tmp/loop.sh workload described above. Compare the proposed environment-deadline and SIGTERM grace-window approaches against the existing process lifecycle. Done should preserve a cooperative runner's final JSON and progress instead of recording an otherwise gracefully stopped trial as aborted.