[Jabe03]

Stop safe mode containers on cancel and cap concurrent runs

Follow-up to #30. Needed by kind2-mc/kind2-language-server#22, which cancels out-of-date parses: without this, cancelling a safe mode run stops the docker client but can leave the container running.

Changes

• Shared docker run command: getDockerRunCommand() builds the resource limits and the Kind 2/solver mounts once, for checks, the interpreter and checkAvailable().
• --init: the container runs an init process as PID 1, so signals reach Kind 2 and orphaned solver processes are reaped.
• Killing containers: each safe mode run gets a unique --name (kind2-api-<uuid>). If the run is cancelled or the process is still alive when it ends, the API runs docker kill on that container before destroying the client process. Destroying the client alone doesn't reliably stop the container (for example on Windows).
• Concurrent run cap: a semaphore shared by every Kind2Api instance limits how many safe mode runs happen at once (default 2, set with the new static setSafeModeMaxRuns(int)). Waiting runs still respond to their monitor's cancellation.
• checkAvailable() in safe mode now runs Kind 2 inside the container, and waits for the process instead of reading exitValue() before it has exited.
• --no_include is only passed when safe mode is on (it used to be passed as --no_include false when safe mode was explicitly off).
• The two interpret overloads now share one runInterpreter method.
• After review: the docker kill timeout now applies; finished runs get a short grace period instead of being killed; setSafeModeMaxRuns resizes the limit in place, so it also applies to waiting runs; slots are held with try-with-resources; the interpreter stops waiting for a slot after 60 s; one helper builds the Kind 2 command prefix; the interpreter reads stderr and reports it when no trace comes back; programs are sent as UTF-8.

Outside safe mode the command line is unchanged.

Testing

• ./gradlew clean build passes.
• With real containers and a statically linked fake kind2 (sleeps, then prints a trace): finished checks and interpreter runs call no docker kill, a cancelled check is killed with no container left, raising and lowering the limit while runs wait takes effect right away, and the interpreter gives up after 60 s when no slot is free.
• Cancelling a safe mode run through Kind2Api (setSafeMode(true)) left no running containers and no leftover z3 processes in 4 of 4 tries.

🤖 Generated with Claude Code

[Jabe03]

Review of the safe mode run lifecycle. I'll address each comment with its own commit and reply here.

Not raised here: a cancel that arrives before Docker creates the container (pending issue 3 in the safe mode notes), since how to handle it hasn't been decided yet.

[daniel-larraz]

Review of the safe mode run management and interpreter error reporting. I checked each finding against the code; gson behavior was tested against 2.8.6.

The two worth fixing first are on the new interpreter error-reporting path: harmless stderr now replaces the empty result (L407), and parse failures escape as raw gson exceptions (L398). The rest are lower severity: cleanup/race edge cases, and a few smaller consistency and robustness points.

🤖 Generated with Claude Code

[daniel-larraz]

Harmless stderr output now replaces the empty result. On main the interpreter never read stderr, so a run without a trace returned "". Now any stderr text throws when there is no trace. For example, on hosts without swap accounting docker prints WARNING: Your kernel does not support swap limit capabilities ... on every run that sets --memory/--memory-swap. A Kind 2 error reported as JSON on stdout (no trace element) then turns into Error running the Kind 2 interpreter: WARNING: ..., which hides the real error.

Suggestion: report stderr only when stdout produced no output at all, or attach it to the message instead of changing the empty-trace behavior.

[daniel-larraz]

Only JsonIOException is caught here, and it is rethrown raw. I checked with gson 2.8.6 (JsonStreamParser is lenient):

• empty stdout → JsonIOException (End of input). When stderr is also empty, throw outputError lets it escape unwrapped, not as a Kind2Exception.
• non-JSON stdout such as Error: docker failed → JsonSyntaxException. That isn't caught, so it goes past catch (IOException) and the new stderr report is skipped.

Catching JsonParseException (the parent of both) and wrapping it in Kind2Exception would fix both cases.

[daniel-larraz]

In safe mode, checkAvailable now starts a full docker run outside the new run management. It uses the per-run CPU/memory limits but takes no run slot, gives the container no --name, and sets no timeout. If docker hangs (image pull, stuck daemon), readAll + waitFor() block forever, and there is no name to docker kill.

[daniel-larraz]

The kill can race with container creation. If the run is cancelled while docker run is still pulling or creating, docker kill <name> fails with "No such container" (only logged through debug). Then process.destroy() kills the client.

• If the client dies before it sends start, the container is left in the Created state. It doesn't run, but --rm never removes it.
• If the client sends start in the window between the failed kill and destroy(), the container runs with no owner after the slot is released. On Linux the SIGTERM from destroy() is normally forwarded to the container (sig-proxy), so this mostly matters on Windows, where the client is terminated without a signal.

Retrying the kill, or running docker rm -f <name> after the client exits, would close the gap.

[daniel-larraz]

execute(String) / execute(Program) can wait forever for a slot. Their monitors never cancel, and the timeout here is 0, so once all slots are held (e.g. by hung runs) these calls block in the tryAcquire loop with no error. That matches the Javadoc ("0 to wait as long as it takes"), but it's inconsistent with interpret, which gives up after 60 s.

[daniel-larraz]

An interrupted thread skips the kill wait. After an interrupt this re-sets the flag and returns !isAlive() (usually false), so killContainer runs with the flag set and kill.waitFor throws at once. The docker kill child still runs and kills the container, so this is low severity, but:

• the slot is released before the container is confirmed stopped, so a new run can briefly go over the cap;
• a docker kill that hangs is never destroyed.

Clearing the interrupt flag around the cleanup and restoring it afterwards would avoid this.

[daniel-larraz]

safeMode is read several times per run (newContainerName, getKind2Command, acquireSafeModeRun). A concurrent setSafeMode(true) can produce a docker run with no --name (which killContainer/exitsOnItsOwn then treat as native), or a native run that holds a slot. Changing settings during a run isn't really supported, since every setting is a plain field, so this is minor. Reading safeMode once into a local and passing it down is a cheap fix.

[daniel-larraz]

Nit: two styles for holding a slot. Here the slot is null-checked and then rebound as heldSlot, while runInterpreter acquires it in the try header. The nullable return (null only on cancel) means every caller has to remember the null check before try-with-resources. Throwing on cancel, or a RunSlot with a cancelled flag, would allow a single pattern.

[daniel-larraz]

Minor: ApiUtil.readAll turns each byte into a char ((char) i), so the stderr text in the new error message is decoded as Latin-1. A docker error that quotes a non-ASCII host path (e.g. /home/josé/...) comes out garbled, unlike the UTF-8 handling this PR adds for stdin and stdout. Reading through an InputStreamReader with UTF-8 would fix it.