From c47c0cca37f4d8f7eed5d39a25a6ea5ea35f2987 Mon Sep 17 00:00:00 2001 From: Josh Date: Fri, 9 Oct 2026 09:41:36 -0500 Subject: [PATCH 01/10] Refactor safe mode execution to use a dedicated method for Docker run command --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 90 ++++++++++--------- 1 file changed, 48 insertions(+), 42 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 09c5742..84b340b 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -552,32 +552,45 @@ private void mountSolversToDocker(List options){ mountIfPresent(options, "yices2Bin", yices2Bin, DOCKER_YICES2_BIN); mountIfPresent(options, "z3Bin", z3Bin, DOCKER_Z3_BIN); } - private ProcessBuilder getKind2ProcessBuilder() { + /** + * Returns the docker run command, up to but not including the image name, with the resource + * limits and the Kind 2 and solver mounts that every safe mode execution uses. + */ + private List getDockerRunCommand() { List options = new ArrayList<>(); + options.add("docker"); + options.add("run"); + options.add("--rm"); + options.add("-i"); - if (safeMode != null && safeMode) { - options.add("docker"); - options.add("run"); - options.add("--rm"); - options.add("-i"); + // Run an init process as PID 1 so that signals reach Kind 2 even if it installs no handler, + // and so that orphaned solver processes are reaped. + options.add("--init"); - options.add("--cpus"); - options.add(safeModeCpuUsage.toString()); + options.add("--cpus"); + options.add(safeModeCpuUsage.toString()); - options.add("--memory"); - options.add(safeModeMemoryUsage); + options.add("--memory"); + options.add(safeModeMemoryUsage); - options.add("--memory-swap"); - options.add(safeModeSwapUsage); + options.add("--memory-swap"); + options.add(safeModeSwapUsage); - options.add("--network"); - options.add("none"); - mountIfPresent(options, "KIND2", KIND2, DOCKER_KIND2); - - mountSolversToDocker(options); - + options.add("--network"); + options.add("none"); + + mountIfPresent(options, "KIND2", KIND2, DOCKER_KIND2); + mountSolversToDocker(options); + return options; + } + + private ProcessBuilder getKind2ProcessBuilder() { + List options = new ArrayList<>(); + + if (safeMode != null && safeMode) { + options.addAll(getDockerRunCommand()); options.add(dockerImage); - options.add("/usr/local/bin/kind2"); + options.add(DOCKER_KIND2); } else { options.add(KIND2); } @@ -594,25 +607,7 @@ private List getInterpreterCommand(File interpreterFile, Path lustreFile List options = new ArrayList<>(); if (safeMode != null && safeMode) { - options.add("docker"); - options.add("run"); - options.add("--rm"); - options.add("-i"); - - options.add("--cpus"); - options.add(safeModeCpuUsage.toString()); - - options.add("--memory"); - options.add(safeModeMemoryUsage); - - options.add("--memory-swap"); - options.add(safeModeSwapUsage); - - options.add("--network"); - options.add("none"); - - mountIfPresent(options, "KIND2", KIND2, DOCKER_KIND2); - mountSolversToDocker(options); + options.addAll(getDockerRunCommand()); options.add("--mount"); options.add(bindMountSpec(interpreterFile.toPath(), DOCKER_INTERPRETER_INPUT)); @@ -980,9 +975,9 @@ public List getOptions() { options.add("--fake_filepath"); options.add(fakeFilepath); } - if (safeMode != null){ + if (safeMode != null && safeMode) { options.add("--no_include"); - options.add(safeMode.toString()); + options.add("true"); } options.addAll(this.otherOptions); return options; @@ -1862,12 +1857,23 @@ void sleep(long interval) { * @throws java.lang.Exception When Kind is not available */ public String checkAvailable() throws Exception { - ProcessBuilder builder = new ProcessBuilder(KIND2, "--version"); + List command = new ArrayList<>(); + if (safeMode != null && safeMode) { + command.addAll(getDockerRunCommand()); + command.add(dockerImage); + command.add(DOCKER_KIND2); + } else { + command.add(KIND2); + } + command.add("--version"); + + ProcessBuilder builder = new ProcessBuilder(command); builder.redirectErrorStream(true); Process process = builder.start(); + process.getOutputStream().close(); String output = ApiUtil.readAll(process.getInputStream()); - if (process.exitValue() != 0) { + if (process.waitFor() != 0) { throw new Kind2Exception("Error running kind2: " + output); } return output; From 77546a25acf62802480a8d3a03f7abf8f293de2a Mon Sep 17 00:00:00 2001 From: Josh Date: Fri, 9 Oct 2026 10:12:39 -0500 Subject: [PATCH 02/10] Implement safe mode execution with maximum runs and proper termination --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 181 +++++++++++++----- 1 file changed, 137 insertions(+), 44 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 84b340b..25c6a1f 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -19,6 +19,9 @@ import java.util.HashSet; import java.util.List; import java.util.Set; +import java.util.UUID; +import java.util.concurrent.Semaphore; +import java.util.concurrent.TimeUnit; import com.google.gson.JsonElement; import com.google.gson.JsonIOException; @@ -40,6 +43,10 @@ public class Kind2Api { private static final Double DEFAULT_SAFE_MODE_CPU_USAGE = 1.0; private static final String DEFAULT_SAFE_MODE_MEMORY_USAGE = "2g"; private static final String DEFAULT_SAFE_MODE_SWAP_USAGE = DEFAULT_SAFE_MODE_MEMORY_USAGE; + private static final int DEFAULT_SAFE_MODE_MAX_RUNS = 2; + private static final long DOCKER_KILL_TIMEOUT_SECONDS = 10; + // Shared by every instance, so the cap holds however many Kind2Api objects a JVM creates. + private static volatile Semaphore safeModeRuns = new Semaphore(DEFAULT_SAFE_MODE_MAX_RUNS, true); private Double safeModeCpuUsage; private String safeModeMemoryUsage; private String safeModeSwapUsage; @@ -299,35 +306,7 @@ public void done() {} public String interpret(URI uri, String main, String json) { File interpreterFile = ApiUtil.writeInterpreterFile(json); Path lustreFile = toLocalPath(uri).toAbsolutePath().normalize(); - - List options = getInterpreterCommand( - interpreterFile, - lustreFile - ); - - options.add("--lus_main"); - options.add(main); - options.add("--enable"); - options.add("interpreter"); - - ProcessBuilder builder = new ProcessBuilder(options); - - debug.println("Kind 2 command(URI Interpret):\n" + ApiUtil.getQuotedCommand(builder.command())); - try { - Process process = builder.start(); - final InputStreamReader reader = new InputStreamReader(process.getInputStream(), java.nio.charset.StandardCharsets.UTF_8); - JsonStreamParser jsp = new JsonStreamParser(reader); - String trace = ""; - while (jsp.hasNext()) { - JsonElement jele = jsp.next(); - if (jele.isJsonObject() && jele.getAsJsonObject().has("trace")) { - trace = jele.getAsJsonObject().get("trace").toString(); - } - } - return trace; - } catch (IOException e) { - throw new Kind2Exception(e.getMessage()); - } + return runInterpreter(interpreterFile, lustreFile, null, main); } /** @@ -360,24 +339,33 @@ private static Path toLocalPath(URI uri) { * @throws Kind2Exception if Kind 2 fails to run */ public String interpret(String program, String main, String json) { - File interpreterFile = ApiUtil.writeInterpreterFile(json); + return runInterpreter(interpreterFile, null, program, main); + } - List options = - getInterpreterCommand(interpreterFile, null); + /** + * Runs the interpreter on either {@code lustreFile} or {@code program}, whichever is non-null, + * and returns the trace. + */ + private String runInterpreter(File interpreterFile, Path lustreFile, String program, String main) { + String containerName = newContainerName(); + List options = getInterpreterCommand(interpreterFile, lustreFile, containerName); options.add("--lus_main"); options.add(main); options.add("--enable"); options.add("interpreter"); - + ProcessBuilder builder = new ProcessBuilder(options); - debug.println("Kind 2 command(String Interpret):\n " + ApiUtil.getQuotedCommand(builder.command())); + debug.println("Kind 2 command(Interpret):\n" + ApiUtil.getQuotedCommand(builder.command())); + Semaphore runs = acquireSafeModeRun(null); + Process process = null; try { - Process process = builder.start(); - process.getOutputStream().write(program.getBytes()); - process.getOutputStream().flush(); + process = builder.start(); + if (program != null) { + process.getOutputStream().write(program.getBytes()); + } process.getOutputStream().close(); final InputStreamReader reader = new InputStreamReader(process.getInputStream(), java.nio.charset.StandardCharsets.UTF_8); JsonStreamParser jsp = new JsonStreamParser(reader); @@ -391,6 +379,14 @@ public String interpret(String program, String main, String json) { return trace; } catch (IOException e) { throw new Kind2Exception(e.getMessage()); + } finally { + if (process != null && process.isAlive()) { + killContainer(containerName); + process.destroy(); + } + if (runs != null) { + runs.release(); + } } } @@ -425,8 +421,18 @@ public void execute(String program, Result result, IProgressMonitor monitor, Res private void callKind2(String program, Result result, IProgressMonitor monitor, ResultListener listener) throws IOException, InterruptedException { - ProcessBuilder builder = getKind2ProcessBuilder(); + String containerName = newContainerName(); + ProcessBuilder builder = getKind2ProcessBuilder(containerName); debug.println("Kind 2 command: " + ApiUtil.getQuotedCommand(builder.command())); + Semaphore runs = acquireSafeModeRun(monitor); + if (monitor.isCanceled()) { + // Cancelled while waiting for a free run. + if (runs != null) { + runs.release(); + } + monitor.done(); + return; + } Process process = null; boolean exceptionThrown = false; JsonStreamParser jsp; @@ -477,8 +483,16 @@ private void callKind2(String program, Result result, IProgressMonitor monitor, } } finally { if (process != null) { + // Destroying the docker client does not reliably stop the container (for example on + // Windows), so kill the container itself if the run did not finish on its own. + if (process.isAlive() || monitor.isCanceled()) { + killContainer(containerName); + } process.destroy(); } + if (runs != null) { + runs.release(); + } monitor.done(); } } @@ -552,17 +566,79 @@ private void mountSolversToDocker(List options){ mountIfPresent(options, "yices2Bin", yices2Bin, DOCKER_YICES2_BIN); mountIfPresent(options, "z3Bin", z3Bin, DOCKER_Z3_BIN); } + /** + * Returns a unique container name in safe mode, or null otherwise. + */ + private String newContainerName() { + if (safeMode != null && safeMode) { + return "kind2-api-" + UUID.randomUUID(); + } + return null; + } + + /** + * In safe mode, waits for one of the {@link #setSafeModeMaxRuns(int)} run slots and returns the + * semaphore to release it to. Returns null outside safe mode, or if {@code monitor} is + * cancelled while waiting. + */ + private Semaphore acquireSafeModeRun(IProgressMonitor monitor) { + if (safeMode == null || !safeMode) { + return null; + } + Semaphore runs = safeModeRuns; + try { + while (!runs.tryAcquire(POLL_INTERVAL, TimeUnit.MILLISECONDS)) { + if (monitor != null && monitor.isCanceled()) { + return null; + } + } + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + throw new Kind2Exception("Interrupted while waiting to run Kind 2", e); + } + return runs; + } + + /** + * Kills a safe mode container, ignoring failures such as the container having already exited. + */ + private void killContainer(String containerName) { + if (containerName == null) { + return; + } + try { + ProcessBuilder builder = new ProcessBuilder("docker", "kill", containerName); + builder.redirectErrorStream(true); + Process kill = builder.start(); + kill.getOutputStream().close(); + String output = ApiUtil.readAll(kill.getInputStream()); + if (!kill.waitFor(DOCKER_KILL_TIMEOUT_SECONDS, TimeUnit.SECONDS)) { + kill.destroy(); + } + debug.println("docker kill " + containerName + ": " + output.trim()); + } catch (IOException e) { + debug.println("docker kill " + containerName + " failed: " + e.getMessage()); + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + } + } + /** * Returns the docker run command, up to but not including the image name, with the resource * limits and the Kind 2 and solver mounts that every safe mode execution uses. */ - private List getDockerRunCommand() { + private List getDockerRunCommand(String containerName) { List options = new ArrayList<>(); options.add("docker"); options.add("run"); options.add("--rm"); options.add("-i"); + if (containerName != null) { + options.add("--name"); + options.add(containerName); + } + // Run an init process as PID 1 so that signals reach Kind 2 even if it installs no handler, // and so that orphaned solver processes are reaped. options.add("--init"); @@ -584,11 +660,11 @@ private List getDockerRunCommand() { return options; } - private ProcessBuilder getKind2ProcessBuilder() { + private ProcessBuilder getKind2ProcessBuilder(String containerName) { List options = new ArrayList<>(); if (safeMode != null && safeMode) { - options.addAll(getDockerRunCommand()); + options.addAll(getDockerRunCommand(containerName)); options.add(dockerImage); options.add(DOCKER_KIND2); } else { @@ -603,11 +679,11 @@ private ProcessBuilder getKind2ProcessBuilder() { } - private List getInterpreterCommand(File interpreterFile, Path lustreFile) { + private List getInterpreterCommand(File interpreterFile, Path lustreFile, String containerName) { List options = new ArrayList<>(); if (safeMode != null && safeMode) { - options.addAll(getDockerRunCommand()); + options.addAll(getDockerRunCommand(containerName)); options.add("--mount"); options.add(bindMountSpec(interpreterFile.toPath(), DOCKER_INTERPRETER_INPUT)); @@ -1066,6 +1142,23 @@ public void setSafeModeSwapUsage(String amount){ safeModeSwapUsage = amount; } + /** + * Sets how many safe mode executions of Kind 2 may run at once in this JVM. The limit is shared + * by every {@code Kind2Api} instance, so the worst-case resource usage is this value times the + * per-run CPU and memory limits. Further executions wait until a run finishes. Runs already in + * progress when the limit changes are not affected. + *

+ * Default: 2 + * @param maxRuns the maximum number of concurrent safe mode executions, at least 1. + */ + public static void setSafeModeMaxRuns(int maxRuns) { + if (maxRuns < 1) { + throw new IllegalArgumentException("Max runs was set to " + maxRuns + + ", but a value of at least 1 is expected"); + } + safeModeRuns = new Semaphore(maxRuns, true); + } + /** * If called with true, enables safe mode for this API instance. * Safe mode enables the following features: disabling the use of include statements, @@ -1859,7 +1952,7 @@ void sleep(long interval) { public String checkAvailable() throws Exception { List command = new ArrayList<>(); if (safeMode != null && safeMode) { - command.addAll(getDockerRunCommand()); + command.addAll(getDockerRunCommand(null)); command.add(dockerImage); command.add(DOCKER_KIND2); } else { From 3cfa0b1a009adfe5067996915d0d65a128c70ca1 Mon Sep 17 00:00:00 2001 From: Josh Date: Fri, 16 Oct 2026 12:18:09 -0500 Subject: [PATCH 03/10] Apply the docker kill timeout before reading its output Co-Authored-By: Claude Opus 5.5 --- src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 25c6a1f..acfacfd 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -611,10 +611,14 @@ private void killContainer(String containerName) { builder.redirectErrorStream(true); Process kill = builder.start(); kill.getOutputStream().close(); - String output = ApiUtil.readAll(kill.getInputStream()); + // Wait before reading, since reading blocks until docker kill exits. Its output is a line at + // most, so it cannot fill the pipe while we wait. if (!kill.waitFor(DOCKER_KILL_TIMEOUT_SECONDS, TimeUnit.SECONDS)) { kill.destroy(); + debug.println("docker kill " + containerName + " timed out"); + return; } + String output = ApiUtil.readAll(kill.getInputStream()); debug.println("docker kill " + containerName + ": " + output.trim()); } catch (IOException e) { debug.println("docker kill " + containerName + " failed: " + e.getMessage()); From f554b5fbbb2037e12b966db9f97832bab678dd55 Mon Sep 17 00:00:00 2001 From: Josh Date: Fri, 16 Oct 2026 12:18:24 -0500 Subject: [PATCH 04/10] Give the docker client time to exit before killing its container When Kind 2's output ends, the docker client is usually still waiting for the container's exit status, so checking isAlive() right away made almost every finished run call docker kill. Co-Authored-By: Claude Opus 5.5 --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 27 ++++++++++++++++--- 1 file changed, 24 insertions(+), 3 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index acfacfd..5f83774 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -45,6 +45,7 @@ public class Kind2Api { private static final String DEFAULT_SAFE_MODE_SWAP_USAGE = DEFAULT_SAFE_MODE_MEMORY_USAGE; private static final int DEFAULT_SAFE_MODE_MAX_RUNS = 2; private static final long DOCKER_KILL_TIMEOUT_SECONDS = 10; + private static final long DOCKER_EXIT_GRACE_MILLIS = 2000; // Shared by every instance, so the cap holds however many Kind2Api objects a JVM creates. private static volatile Semaphore safeModeRuns = new Semaphore(DEFAULT_SAFE_MODE_MAX_RUNS, true); private Double safeModeCpuUsage; @@ -380,8 +381,10 @@ private String runInterpreter(File interpreterFile, Path lustreFile, String prog } catch (IOException e) { throw new Kind2Exception(e.getMessage()); } finally { - if (process != null && process.isAlive()) { - killContainer(containerName); + if (process != null) { + if (!exitsOnItsOwn(process, containerName)) { + killContainer(containerName); + } process.destroy(); } if (runs != null) { @@ -485,7 +488,7 @@ private void callKind2(String program, Result result, IProgressMonitor monitor, if (process != null) { // Destroying the docker client does not reliably stop the container (for example on // Windows), so kill the container itself if the run did not finish on its own. - if (process.isAlive() || monitor.isCanceled()) { + if (monitor.isCanceled() || !exitsOnItsOwn(process, containerName)) { killContainer(containerName); } process.destroy(); @@ -599,6 +602,24 @@ private Semaphore acquireSafeModeRun(IProgressMonitor monitor) { return runs; } + /** + * Returns whether a run's process exits on its own once its output has ended. In safe mode the + * docker client outlives the output while it waits for the container's exit status, so it gets + * a short grace period. Outside safe mode ({@code containerName} is null) there is no container + * to kill, so this returns true without waiting. + */ + private static boolean exitsOnItsOwn(Process process, String containerName) { + if (containerName == null) { + return true; + } + try { + return process.waitFor(DOCKER_EXIT_GRACE_MILLIS, TimeUnit.MILLISECONDS); + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + return !process.isAlive(); + } + } + /** * Kills a safe mode container, ignoring failures such as the container having already exited. */ From 5e9e7e08f79e5396ce910dc055f08b124e2aeb50 Mon Sep 17 00:00:00 2001 From: Josh Date: Fri, 16 Oct 2026 12:18:41 -0500 Subject: [PATCH 05/10] Resize the safe mode run limit in place Replacing the semaphore left callers that were already waiting on the old one, so a lower limit was not enforced and a higher one did not wake them. Co-Authored-By: Claude Opus 5.5 --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 36 ++++++++++++++++--- 1 file changed, 31 insertions(+), 5 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 5f83774..943b938 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -47,7 +47,7 @@ public class Kind2Api { private static final long DOCKER_KILL_TIMEOUT_SECONDS = 10; private static final long DOCKER_EXIT_GRACE_MILLIS = 2000; // Shared by every instance, so the cap holds however many Kind2Api objects a JVM creates. - private static volatile Semaphore safeModeRuns = new Semaphore(DEFAULT_SAFE_MODE_MAX_RUNS, true); + private static final RunLimit safeModeRuns = new RunLimit(DEFAULT_SAFE_MODE_MAX_RUNS); private Double safeModeCpuUsage; private String safeModeMemoryUsage; private String safeModeSwapUsage; @@ -588,7 +588,7 @@ private Semaphore acquireSafeModeRun(IProgressMonitor monitor) { if (safeMode == null || !safeMode) { return null; } - Semaphore runs = safeModeRuns; + RunLimit runs = safeModeRuns; try { while (!runs.tryAcquire(POLL_INTERVAL, TimeUnit.MILLISECONDS)) { if (monitor != null && monitor.isCanceled()) { @@ -1170,8 +1170,9 @@ public void setSafeModeSwapUsage(String amount){ /** * Sets how many safe mode executions of Kind 2 may run at once in this JVM. The limit is shared * by every {@code Kind2Api} instance, so the worst-case resource usage is this value times the - * per-run CPU and memory limits. Further executions wait until a run finishes. Runs already in - * progress when the limit changes are not affected. + * per-run CPU and memory limits. Further executions wait until a run finishes. The new limit also + * applies to executions that are already waiting; runs already in progress are not stopped, but + * no new run starts while more than {@code maxRuns} are in progress. *

* Default: 2 * @param maxRuns the maximum number of concurrent safe mode executions, at least 1. @@ -1181,7 +1182,32 @@ public static void setSafeModeMaxRuns(int maxRuns) { throw new IllegalArgumentException("Max runs was set to " + maxRuns + ", but a value of at least 1 is expected"); } - safeModeRuns = new Semaphore(maxRuns, true); + safeModeRuns.setLimit(maxRuns); + } + + /** + * A fair semaphore whose number of permits can be changed while runs hold or wait for them. + */ + private static final class RunLimit extends Semaphore { + private static final long serialVersionUID = 1L; + /** The current limit; guarded by {@code this}. */ + private int limit; + + RunLimit(int limit) { + super(limit, true); + this.limit = limit; + } + + synchronized void setLimit(int newLimit) { + int delta = newLimit - limit; + limit = newLimit; + if (delta > 0) { + release(delta); + } else if (delta < 0) { + // May leave the available permits negative until enough running runs finish. + reducePermits(-delta); + } + } } /** From 11d861be00929866e4cc21c6eae82cdf615656d8 Mon Sep 17 00:00:00 2001 From: Josh Date: Fri, 16 Oct 2026 12:19:44 -0500 Subject: [PATCH 06/10] Hold safe mode run slots with try-with-resources acquireSafeModeRun now returns a closeable slot (a no-op one outside safe mode) and null only when cancelled, so callers can't forget the release. It also checks the monitor once more after acquiring, so a run cancelled just as a slot frees up does not start a container. Co-Authored-By: Claude Opus 5.5 --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 207 ++++++++++-------- 1 file changed, 112 insertions(+), 95 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 943b938..5528518 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -360,35 +360,33 @@ private String runInterpreter(File interpreterFile, Path lustreFile, String prog ProcessBuilder builder = new ProcessBuilder(options); debug.println("Kind 2 command(Interpret):\n" + ApiUtil.getQuotedCommand(builder.command())); - Semaphore runs = acquireSafeModeRun(null); - Process process = null; - try { - process = builder.start(); - if (program != null) { - process.getOutputStream().write(program.getBytes()); - } - process.getOutputStream().close(); - final InputStreamReader reader = new InputStreamReader(process.getInputStream(), java.nio.charset.StandardCharsets.UTF_8); - JsonStreamParser jsp = new JsonStreamParser(reader); - String trace = ""; - while (jsp.hasNext()) { - JsonElement jele = jsp.next(); - if (jele.isJsonObject() && jele.getAsJsonObject().has("trace")) { - trace = jele.getAsJsonObject().get("trace").toString(); + try (RunSlot slot = acquireSafeModeRun(null)) { + Process process = null; + try { + process = builder.start(); + if (program != null) { + process.getOutputStream().write(program.getBytes()); + } + process.getOutputStream().close(); + final InputStreamReader reader = new InputStreamReader(process.getInputStream(), java.nio.charset.StandardCharsets.UTF_8); + JsonStreamParser jsp = new JsonStreamParser(reader); + String trace = ""; + while (jsp.hasNext()) { + JsonElement jele = jsp.next(); + if (jele.isJsonObject() && jele.getAsJsonObject().has("trace")) { + trace = jele.getAsJsonObject().get("trace").toString(); + } + } + return trace; + } catch (IOException e) { + throw new Kind2Exception(e.getMessage()); + } finally { + if (process != null) { + if (!exitsOnItsOwn(process, containerName)) { + killContainer(containerName); } - } - return trace; - } catch (IOException e) { - throw new Kind2Exception(e.getMessage()); - } finally { - if (process != null) { - if (!exitsOnItsOwn(process, containerName)) { - killContainer(containerName); + process.destroy(); } - process.destroy(); - } - if (runs != null) { - runs.release(); } } } @@ -427,76 +425,72 @@ private void callKind2(String program, Result result, IProgressMonitor monitor, String containerName = newContainerName(); ProcessBuilder builder = getKind2ProcessBuilder(containerName); debug.println("Kind 2 command: " + ApiUtil.getQuotedCommand(builder.command())); - Semaphore runs = acquireSafeModeRun(monitor); - if (monitor.isCanceled()) { + RunSlot slot = acquireSafeModeRun(monitor); + if (slot == null) { // Cancelled while waiting for a free run. - if (runs != null) { - runs.release(); - } monitor.done(); return; } - Process process = null; - boolean exceptionThrown = false; - JsonStreamParser jsp; - try { - process = builder.start(); - process.getOutputStream().write(program.getBytes()); - process.getOutputStream().flush(); - process.getOutputStream().close(); - final InputStreamReader reader = new InputStreamReader(process.getInputStream(), java.nio.charset.StandardCharsets.UTF_8); - jsp = new JsonStreamParser(reader); - // The following assignment is required because variables used in lambdas must be final or effectively final. - final Process processForMonitor = process; - Thread monitorThread = new Thread(() -> { - while (!monitor.isCanceled() && processForMonitor.isAlive()) { - sleep(POLL_INTERVAL); - } - if (monitor.isCanceled() && processForMonitor.isAlive()) { - debug.println("Monitor canceled, destroying Kind2 process"); - processForMonitor.destroy(); - try { reader.close(); } catch (IOException e) { /* ignore */ } - } - }); - monitorThread.start(); - while (jsp.hasNext()) { - JsonElement jele = jsp.next(); - debug.println("Parsing JSON element: " + jele.toString()); - result.addJsonElement(jele); - if(listener != null){ - listener.onUpdate(result); - } - debug.println(result.getResultMap().toString()); - } - } catch (JsonIOException e) { - // ignore JsonIOException, which may occur if the process is destroyed while reading JSON - } catch (Throwable t) { - exceptionThrown = true; - throw t; - } finally { + try (RunSlot heldSlot = slot) { + Process process = null; + boolean exceptionThrown = false; + JsonStreamParser jsp; try { - if (!monitor.isCanceled()) { - try { - result.finish(); - } catch (Throwable t) { - if (!exceptionThrown) { - throw t; - } + process = builder.start(); + process.getOutputStream().write(program.getBytes()); + process.getOutputStream().flush(); + process.getOutputStream().close(); + final InputStreamReader reader = new InputStreamReader(process.getInputStream(), java.nio.charset.StandardCharsets.UTF_8); + jsp = new JsonStreamParser(reader); + // The following assignment is required because variables used in lambdas must be final or effectively final. + final Process processForMonitor = process; + Thread monitorThread = new Thread(() -> { + while (!monitor.isCanceled() && processForMonitor.isAlive()) { + sleep(POLL_INTERVAL); + } + if (monitor.isCanceled() && processForMonitor.isAlive()) { + debug.println("Monitor canceled, destroying Kind2 process"); + processForMonitor.destroy(); + try { reader.close(); } catch (IOException e) { /* ignore */ } } + }); + monitorThread.start(); + while (jsp.hasNext()) { + JsonElement jele = jsp.next(); + debug.println("Parsing JSON element: " + jele.toString()); + result.addJsonElement(jele); + if(listener != null){ + listener.onUpdate(result); + } + debug.println(result.getResultMap().toString()); } + } catch (JsonIOException e) { + // ignore JsonIOException, which may occur if the process is destroyed while reading JSON + } catch (Throwable t) { + exceptionThrown = true; + throw t; } finally { - if (process != null) { - // Destroying the docker client does not reliably stop the container (for example on - // Windows), so kill the container itself if the run did not finish on its own. - if (monitor.isCanceled() || !exitsOnItsOwn(process, containerName)) { - killContainer(containerName); + try { + if (!monitor.isCanceled()) { + try { + result.finish(); + } catch (Throwable t) { + if (!exceptionThrown) { + throw t; + } + } } - process.destroy(); - } - if (runs != null) { - runs.release(); + } finally { + if (process != null) { + // Destroying the docker client does not reliably stop the container (for example on + // Windows), so kill the container itself if the run did not finish on its own. + if (monitor.isCanceled() || !exitsOnItsOwn(process, containerName)) { + killContainer(containerName); + } + process.destroy(); + } + monitor.done(); } - monitor.done(); } } } @@ -580,17 +574,17 @@ private String newContainerName() { } /** - * In safe mode, waits for one of the {@link #setSafeModeMaxRuns(int)} run slots and returns the - * semaphore to release it to. Returns null outside safe mode, or if {@code monitor} is - * cancelled while waiting. + * In safe mode, waits for one of the {@link #setSafeModeMaxRuns(int)} run slots. Outside safe + * mode, returns a slot that holds nothing. Close the slot when the run ends. + * + * @return the slot, or null only if {@code monitor} is cancelled before a slot is free */ - private Semaphore acquireSafeModeRun(IProgressMonitor monitor) { + private RunSlot acquireSafeModeRun(IProgressMonitor monitor) { if (safeMode == null || !safeMode) { - return null; + return RunSlot.NONE; } - RunLimit runs = safeModeRuns; try { - while (!runs.tryAcquire(POLL_INTERVAL, TimeUnit.MILLISECONDS)) { + while (!safeModeRuns.tryAcquire(POLL_INTERVAL, TimeUnit.MILLISECONDS)) { if (monitor != null && monitor.isCanceled()) { return null; } @@ -599,7 +593,30 @@ private Semaphore acquireSafeModeRun(IProgressMonitor monitor) { Thread.currentThread().interrupt(); throw new Kind2Exception("Interrupted while waiting to run Kind 2", e); } - return runs; + if (monitor != null && monitor.isCanceled()) { + safeModeRuns.release(); + return null; + } + return new RunSlot(safeModeRuns); + } + + /** + * A held safe mode run slot, released by {@link #close()}. Outside safe mode it holds nothing. + */ + private static final class RunSlot implements AutoCloseable { + static final RunSlot NONE = new RunSlot(null); + private final Semaphore runs; + + RunSlot(Semaphore runs) { + this.runs = runs; + } + + @Override + public void close() { + if (runs != null) { + runs.release(); + } + } } /** From c87e86d977bf08e611b48fac7cda781cc31fa6cc Mon Sep 17 00:00:00 2001 From: Josh Date: Fri, 16 Oct 2026 12:20:01 -0500 Subject: [PATCH 07/10] Stop waiting for a safe mode run slot after 60 s in the interpreter The interpreter has no monitor, so a call made while the run limit was reached blocked the caller's thread until a long check finished. It now throws a Kind2Exception instead. Co-Authored-By: Claude Opus 5.5 --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 5528518..99bd7d5 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -46,6 +46,8 @@ public class Kind2Api { private static final int DEFAULT_SAFE_MODE_MAX_RUNS = 2; private static final long DOCKER_KILL_TIMEOUT_SECONDS = 10; private static final long DOCKER_EXIT_GRACE_MILLIS = 2000; + // The interpreter has no monitor to cancel it, so it gives up waiting for a run slot after this. + private static final long SAFE_MODE_INTERPRET_WAIT_SECONDS = 60; // Shared by every instance, so the cap holds however many Kind2Api objects a JVM creates. private static final RunLimit safeModeRuns = new RunLimit(DEFAULT_SAFE_MODE_MAX_RUNS); private Double safeModeCpuUsage; @@ -360,7 +362,7 @@ private String runInterpreter(File interpreterFile, Path lustreFile, String prog ProcessBuilder builder = new ProcessBuilder(options); debug.println("Kind 2 command(Interpret):\n" + ApiUtil.getQuotedCommand(builder.command())); - try (RunSlot slot = acquireSafeModeRun(null)) { + try (RunSlot slot = acquireSafeModeRun(null, SAFE_MODE_INTERPRET_WAIT_SECONDS)) { Process process = null; try { process = builder.start(); @@ -425,7 +427,7 @@ private void callKind2(String program, Result result, IProgressMonitor monitor, String containerName = newContainerName(); ProcessBuilder builder = getKind2ProcessBuilder(containerName); debug.println("Kind 2 command: " + ApiUtil.getQuotedCommand(builder.command())); - RunSlot slot = acquireSafeModeRun(monitor); + RunSlot slot = acquireSafeModeRun(monitor, 0); if (slot == null) { // Cancelled while waiting for a free run. monitor.done(); @@ -577,17 +579,25 @@ private String newContainerName() { * In safe mode, waits for one of the {@link #setSafeModeMaxRuns(int)} run slots. Outside safe * mode, returns a slot that holds nothing. Close the slot when the run ends. * + * @param monitor checked for cancellation while waiting, or null + * @param timeoutSeconds how long to wait before throwing, or 0 to wait as long as it takes * @return the slot, or null only if {@code monitor} is cancelled before a slot is free + * @throws Kind2Exception if no slot is free within {@code timeoutSeconds} */ - private RunSlot acquireSafeModeRun(IProgressMonitor monitor) { + private RunSlot acquireSafeModeRun(IProgressMonitor monitor, long timeoutSeconds) { if (safeMode == null || !safeMode) { return RunSlot.NONE; } + long deadline = System.nanoTime() + TimeUnit.SECONDS.toNanos(timeoutSeconds); try { while (!safeModeRuns.tryAcquire(POLL_INTERVAL, TimeUnit.MILLISECONDS)) { if (monitor != null && monitor.isCanceled()) { return null; } + if (timeoutSeconds > 0 && System.nanoTime() - deadline >= 0) { + throw new Kind2Exception("No safe mode run was free after " + timeoutSeconds + + " seconds, since the limit of concurrent runs was reached"); + } } } catch (InterruptedException e) { Thread.currentThread().interrupt(); From fc062fc412b6a70087c4c9fa52e1d24ace7da258 Mon Sep 17 00:00:00 2001 From: Josh Date: Fri, 16 Oct 2026 12:21:00 -0500 Subject: [PATCH 08/10] Build the Kind 2 command prefix in one place checkAvailable, checks and the interpreter now share getKind2Command, so checkAvailable runs the same command that execute does. The generated command lines are unchanged. Co-Authored-By: Claude Opus 5.5 --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 79 ++++++++----------- 1 file changed, 32 insertions(+), 47 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 99bd7d5..919b4de 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -712,17 +712,26 @@ private List getDockerRunCommand(String containerName) { return options; } - private ProcessBuilder getKind2ProcessBuilder(String containerName) { - List options = new ArrayList<>(); - + /** + * Returns the command that starts Kind 2, without its options: {@code docker run ...} with the + * given extra docker arguments, the image and the Kind 2 path in the container in safe mode, or + * just {@link #KIND2} otherwise. + */ + private List getKind2Command(String containerName, List dockerArgs) { + List command = new ArrayList<>(); if (safeMode != null && safeMode) { - options.addAll(getDockerRunCommand(containerName)); - options.add(dockerImage); - options.add(DOCKER_KIND2); + command.addAll(getDockerRunCommand(containerName)); + command.addAll(dockerArgs); + command.add(dockerImage); + command.add(DOCKER_KIND2); } else { - options.add(KIND2); + command.add(KIND2); } + return command; + } + private ProcessBuilder getKind2ProcessBuilder(String containerName) { + List options = getKind2Command(containerName, new ArrayList<>()); options.addAll(getOptions()); ProcessBuilder builder = new ProcessBuilder(options); @@ -732,45 +741,28 @@ private ProcessBuilder getKind2ProcessBuilder(String containerName) { private List getInterpreterCommand(File interpreterFile, Path lustreFile, String containerName) { - List options = new ArrayList<>(); - - if (safeMode != null && safeMode) { - options.addAll(getDockerRunCommand(containerName)); - - options.add("--mount"); - options.add(bindMountSpec(interpreterFile.toPath(), DOCKER_INTERPRETER_INPUT)); - - if (lustreFile != null) { - options.add("--mount"); - options.add(bindMountSpec(lustreFile.toAbsolutePath(), DOCKER_LUSTRE_FILE)); - } - - options.add(dockerImage); - options.add(DOCKER_KIND2); - - options.addAll(getOptions()); - - options.add("--interpreter_input_file"); - options.add(DOCKER_INTERPRETER_INPUT); - + boolean inDocker = safeMode != null && safeMode; + List mounts = new ArrayList<>(); + if (inDocker) { + mounts.add("--mount"); + mounts.add(bindMountSpec(interpreterFile.toPath(), DOCKER_INTERPRETER_INPUT)); if (lustreFile != null) { - options.add(DOCKER_LUSTRE_FILE); + mounts.add("--mount"); + mounts.add(bindMountSpec(lustreFile.toAbsolutePath(), DOCKER_LUSTRE_FILE)); } - - return options; } - options.add(KIND2); - options.addAll(getOptions()); + List options = getKind2Command(containerName, mounts); + options.addAll(getOptions()); - options.add("--interpreter_input_file"); - options.add(interpreterFile.getAbsolutePath()); + options.add("--interpreter_input_file"); + options.add(inDocker ? DOCKER_INTERPRETER_INPUT : interpreterFile.getAbsolutePath()); - if (lustreFile != null) { - options.add(lustreFile.toString()); - } + if (lustreFile != null) { + options.add(inDocker ? DOCKER_LUSTRE_FILE : lustreFile.toString()); + } - return options; + return options; } /** @@ -2028,14 +2020,7 @@ void sleep(long interval) { * @throws java.lang.Exception When Kind is not available */ public String checkAvailable() throws Exception { - List command = new ArrayList<>(); - if (safeMode != null && safeMode) { - command.addAll(getDockerRunCommand(null)); - command.add(dockerImage); - command.add(DOCKER_KIND2); - } else { - command.add(KIND2); - } + List command = getKind2Command(null, new ArrayList<>()); command.add("--version"); ProcessBuilder builder = new ProcessBuilder(command); From 7d230a498b2d711b54098f53db9fbafddc5a3a77 Mon Sep 17 00:00:00 2001 From: Josh Date: Fri, 16 Oct 2026 12:23:09 -0500 Subject: [PATCH 09/10] Read the interpreter's stderr and report it when there is no trace stderr was never read, so docker errors in safe mode were lost, and enough stderr output blocked Kind 2 and hung the run. It is now read on its own thread, and if no trace comes back, interpret throws a Kind2Exception with it. Co-Authored-By: Claude Opus 5.5 --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 44 ++++++++++++++++--- 1 file changed, 39 insertions(+), 5 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 919b4de..d915071 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -9,6 +9,7 @@ import java.io.File; import java.io.IOException; +import java.io.InputStream; import java.io.InputStreamReader; import java.net.URI; import java.net.URISyntaxException; @@ -366,6 +367,19 @@ private String runInterpreter(File interpreterFile, Path lustreFile, String prog Process process = null; try { process = builder.start(); + // Read stderr on its own thread so that it cannot fill its pipe and block Kind 2. It is + // kept apart from stdout, which must hold only JSON. + final InputStream errorStream = process.getErrorStream(); + final StringBuffer errors = new StringBuffer(); + Thread errorReader = new Thread(() -> { + try { + errors.append(ApiUtil.readAll(errorStream)); + } catch (IOException e) { + // The stream is closed when the process is destroyed. + } + }); + errorReader.setDaemon(true); + errorReader.start(); if (program != null) { process.getOutputStream().write(program.getBytes()); } @@ -373,15 +387,35 @@ private String runInterpreter(File interpreterFile, Path lustreFile, String prog final InputStreamReader reader = new InputStreamReader(process.getInputStream(), java.nio.charset.StandardCharsets.UTF_8); JsonStreamParser jsp = new JsonStreamParser(reader); String trace = ""; - while (jsp.hasNext()) { - JsonElement jele = jsp.next(); - if (jele.isJsonObject() && jele.getAsJsonObject().has("trace")) { - trace = jele.getAsJsonObject().get("trace").toString(); - } + JsonIOException outputError = null; + try { + while (jsp.hasNext()) { + JsonElement jele = jsp.next(); + if (jele.isJsonObject() && jele.getAsJsonObject().has("trace")) { + trace = jele.getAsJsonObject().get("trace").toString(); + } + } + } catch (JsonIOException e) { + // Thrown when stdout is empty, for example when docker fails to start the container. + outputError = e; + } + if (trace.isEmpty()) { + // Without a trace, stderr may say why, for example a docker error in safe mode. + errorReader.join(DOCKER_EXIT_GRACE_MILLIS); + String errorOutput = errors.toString().trim(); + if (!errorOutput.isEmpty()) { + throw new Kind2Exception("Error running the Kind 2 interpreter: " + errorOutput); + } + } + if (outputError != null) { + throw outputError; } return trace; } catch (IOException e) { throw new Kind2Exception(e.getMessage()); + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + throw new Kind2Exception("Interrupted while running the Kind 2 interpreter", e); } finally { if (process != null) { if (!exitsOnItsOwn(process, containerName)) { From 3fcce9fc99b52a6369c668f2c54f91c802e95796 Mon Sep 17 00:00:00 2001 From: Josh Date: Fri, 16 Oct 2026 12:23:29 -0500 Subject: [PATCH 10/10] Send the Lustre program to Kind 2 as UTF-8 It was encoded with the platform's default charset while the output is read as UTF-8, so non-ASCII programs broke on Windows. Co-Authored-By: Claude Opus 5.5 --- src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index d915071..af942aa 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -381,7 +381,7 @@ private String runInterpreter(File interpreterFile, Path lustreFile, String prog errorReader.setDaemon(true); errorReader.start(); if (program != null) { - process.getOutputStream().write(program.getBytes()); + process.getOutputStream().write(program.getBytes(java.nio.charset.StandardCharsets.UTF_8)); } process.getOutputStream().close(); final InputStreamReader reader = new InputStreamReader(process.getInputStream(), java.nio.charset.StandardCharsets.UTF_8); @@ -473,7 +473,7 @@ private void callKind2(String program, Result result, IProgressMonitor monitor, JsonStreamParser jsp; try { process = builder.start(); - process.getOutputStream().write(program.getBytes()); + process.getOutputStream().write(program.getBytes(java.nio.charset.StandardCharsets.UTF_8)); process.getOutputStream().flush(); process.getOutputStream().close(); final InputStreamReader reader = new InputStreamReader(process.getInputStream(), java.nio.charset.StandardCharsets.UTF_8);