[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.

[Jabe03]

A hung docker kill can block every later safe mode run. ApiUtil.readAll reads until the end of the output, so waitFor(DOCKER_KILL_TIMEOUT_SECONDS) is only reached after docker kill has already exited, and the timeout never applies. If the Docker daemon hangs, docker kill never exits, the caller's finally never gets to runs.release(), and with the default cap of 2, two such runs block all later safe mode runs. Wait with the timeout first (docker kill prints very little, so its output won't fill the pipe), then read the output.

[Jabe03]

Fixed in 3cfa0b1: killContainer now waits with the timeout first and only reads the output once docker kill has exited. On timeout it destroys the process and logs it.

[Jabe03]

Runs that finish normally still call docker kill. When Kind 2 closes stdout, jsp.hasNext() returns false right away, but the docker run client usually stays alive a little longer while it waits for the container's exit status. So process.isAlive() is usually true here, and each completed run starts an extra docker kill (logged as "No such container" or similar) while still holding its slot. Give the client a short grace period (process.waitFor(...)) before deciding the run didn't finish on its own.

[Jabe03]

Fixed in f554b5f: a new exitsOnItsOwn gives the docker client up to 2 s (DOCKER_EXIT_GRACE_MILLIS) to exit before the container is killed. Outside safe mode it returns at once without waiting. With a real container and a static fake kind2, checks that finished normally didn't call docker kill before or after this change (the race didn't show up for checks in my runs), and cancelling still kills the container (1 kill, 0 containers left).

[Jabe03]

Same isAlive() race as in callKind2: when the trace ends, the docker client is usually still alive, so a completed interpreter run also calls docker kill.

[Jabe03]

Fixed in the same commit, f554b5f. Here the race did show up: before, a normal interpreter run called docker kill (1 kill per run); now it calls none.

[Jabe03]

Interpret calls can't be cancelled while they wait for a slot. acquireSafeModeRun(null) waits for as long as it takes. In safe mode, if two long checks are already running, opening the simulator blocks the language server's request thread until one of them finishes, and there's no way to cancel it. The interpreter has no monitor, so it should at least stop waiting after a bounded time and fail with a Kind2Exception.

[Jabe03]

Fixed in c87e86d: acquireSafeModeRun takes a timeout, and the interpreter gives up after 60 s (SAFE_MODE_INTERPRET_WAIT_SECONDS) with a Kind2Exception. Checks still wait as long as needed and stop when their monitor is cancelled. Tested with the limit at 1 and a long check holding the slot: interpret threw after 60.1 s, and no containers were left after the check was cancelled.

[Jabe03]

Changing the limit doesn't affect callers that are already waiting. The semaphore is read once before the wait loop, so when setSafeModeMaxRuns replaces it, current waiters keep waiting on the old one. Lowering the limit lets more runs through than the new cap (old waiters plus new callers), and raising it doesn't wake anyone already waiting. Use one semaphore and change its number of permits instead of replacing it (a Semaphore subclass can call the protected reducePermits).

[Jabe03]

Fixed in 5e9e7e0: there's now one RunLimit (a fair Semaphore subclass), and setSafeModeMaxRuns changes its permits in place with release or reducePermits. I also updated the javadoc. Tested with real containers:

• 1 → 3 at 1.5 s with 3 waiting runs of 4 s: all 3 were running at 1.9 s, done in 5.9 s (before: one at a time, 13.1 s).
• 2 → 1 at 1.5 s, then 2 more runs: never more than 2 at once, then 1 at a time (before: 3 containers ran at once).

[Jabe03]

acquireSafeModeRun returns null both outside safe mode and when cancelled while waiting, so each caller has to check the monitor again and remember to release the slot (see the extra cancel check at the top of callKind2). Returning a slot object that can be closed (a no-op outside safe mode), used with try-with-resources, and a clear result for "cancelled" would make it impossible to forget the release.

[Jabe03]

Fixed in 11d861b: acquireSafeModeRun returns a RunSlot (AutoCloseable, and RunSlot.NONE outside safe mode) that both callers hold with try-with-resources. null now only means cancelled. It also checks the monitor once more after getting a slot, so a run cancelled just as a slot frees up doesn't start a container. Side effect: outside safe mode, a monitor that is already cancelled no longer makes callKind2 return early, which is the same as before this PR.

[Jabe03]

checkAvailable builds the safe mode / non-safe mode command prefix (docker run … + image + DOCKER_KIND2, or KIND2) a third time, after getKind2ProcessBuilder and getInterpreterCommand. A shared helper would keep checkAvailable running the same command that execute runs.

[Jabe03]

Fixed in fc062fc: the new getKind2Command(containerName, dockerArgs) builds the prefix for checks, the interpreter (which passes its extra mounts) and checkAvailable. I checked by reflection that the generated command lines match the previous commit exactly, in both safe mode and normal mode, with and without a Lustre file.

[Jabe03]

Existing before this PR (also in callKind2): program.getBytes() encodes with the platform's default charset, but the output is read as UTF-8. On Windows (cp1252), a program with non-ASCII characters is sent to Kind 2 in the wrong encoding. Use getBytes(StandardCharsets.UTF_8).

[Jabe03]

Fixed in 3fcce9f: both interpret and callKind2 now write the program with getBytes(StandardCharsets.UTF_8).