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..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 @@ -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; @@ -19,6 +20,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 +44,13 @@ 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; + 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; private String safeModeMemoryUsage; private String safeModeSwapUsage; @@ -299,35 +310,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,37 +343,87 @@ 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())); - try { - Process 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); - 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(); + debug.println("Kind 2 command(Interpret):\n" + ApiUtil.getQuotedCommand(builder.command())); + try (RunSlot slot = acquireSafeModeRun(null, SAFE_MODE_INTERPRET_WAIT_SECONDS)) { + 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(java.nio.charset.StandardCharsets.UTF_8)); + } + process.getOutputStream().close(); + final InputStreamReader reader = new InputStreamReader(process.getInputStream(), java.nio.charset.StandardCharsets.UTF_8); + JsonStreamParser jsp = new JsonStreamParser(reader); + String trace = ""; + 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)) { + killContainer(containerName); } + process.destroy(); + } } - return trace; - } catch (IOException e) { - throw new Kind2Exception(e.getMessage()); } } @@ -425,61 +458,75 @@ 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())); - 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 { + RunSlot slot = acquireSafeModeRun(monitor, 0); + if (slot == null) { + // Cancelled while waiting for a free run. + monitor.done(); + return; + } + 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(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); + 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) { - process.destroy(); + try { + if (!monitor.isCanceled()) { + try { + result.finish(); + } catch (Throwable t) { + if (!exceptionThrown) { + 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); + } + process.destroy(); + } + monitor.done(); } - monitor.done(); } } } @@ -552,102 +599,204 @@ private void mountSolversToDocker(List options){ mountIfPresent(options, "yices2Bin", yices2Bin, DOCKER_YICES2_BIN); mountIfPresent(options, "z3Bin", z3Bin, DOCKER_Z3_BIN); } - private ProcessBuilder getKind2ProcessBuilder() { - List options = new ArrayList<>(); - + /** + * Returns a unique container name in safe mode, or null otherwise. + */ + private String newContainerName() { if (safeMode != null && safeMode) { - options.add("docker"); - options.add("run"); - options.add("--rm"); - options.add("-i"); - - options.add("--cpus"); - options.add(safeModeCpuUsage.toString()); + return "kind2-api-" + UUID.randomUUID(); + } + return null; + } - options.add("--memory"); - options.add(safeModeMemoryUsage); + /** + * 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, 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(); + throw new Kind2Exception("Interrupted while waiting to run Kind 2", e); + } + if (monitor != null && monitor.isCanceled()) { + safeModeRuns.release(); + return null; + } + return new RunSlot(safeModeRuns); + } - options.add("--memory-swap"); - options.add(safeModeSwapUsage); + /** + * 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; - options.add("--network"); - options.add("none"); - mountIfPresent(options, "KIND2", KIND2, DOCKER_KIND2); - - mountSolversToDocker(options); - - options.add(dockerImage); - options.add("/usr/local/bin/kind2"); - } else { - options.add(KIND2); + RunSlot(Semaphore runs) { + this.runs = runs; } - options.addAll(getOptions()); + @Override + public void close() { + if (runs != null) { + runs.release(); + } + } + } - ProcessBuilder builder = new ProcessBuilder(options); - builder.redirectErrorStream(true); - return builder; + /** + * 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. + */ + 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(); + // 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()); + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + } + } - private List getInterpreterCommand(File interpreterFile, Path lustreFile) { + /** + * 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(String containerName) { 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"); + if (containerName != null) { + options.add("--name"); + options.add(containerName); + } - options.add("--cpus"); - options.add(safeModeCpuUsage.toString()); + // 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("--memory"); - options.add(safeModeMemoryUsage); + options.add("--cpus"); + options.add(safeModeCpuUsage.toString()); - options.add("--memory-swap"); - options.add(safeModeSwapUsage); + options.add("--memory"); + options.add(safeModeMemoryUsage); - options.add("--network"); - options.add("none"); + options.add("--memory-swap"); + options.add(safeModeSwapUsage); - mountIfPresent(options, "KIND2", KIND2, DOCKER_KIND2); - mountSolversToDocker(options); + options.add("--network"); + options.add("none"); - options.add("--mount"); - options.add(bindMountSpec(interpreterFile.toPath(), DOCKER_INTERPRETER_INPUT)); + mountIfPresent(options, "KIND2", KIND2, DOCKER_KIND2); + mountSolversToDocker(options); + return options; + } - if (lustreFile != null) { - options.add("--mount"); - options.add(bindMountSpec(lustreFile.toAbsolutePath(), DOCKER_LUSTRE_FILE)); - } + /** + * 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) { + command.addAll(getDockerRunCommand(containerName)); + command.addAll(dockerArgs); + command.add(dockerImage); + command.add(DOCKER_KIND2); + } else { + command.add(KIND2); + } + return command; + } - options.add(dockerImage); - options.add(DOCKER_KIND2); + private ProcessBuilder getKind2ProcessBuilder(String containerName) { + List options = getKind2Command(containerName, new ArrayList<>()); + options.addAll(getOptions()); - options.addAll(getOptions()); + ProcessBuilder builder = new ProcessBuilder(options); + builder.redirectErrorStream(true); + return builder; + } - options.add("--interpreter_input_file"); - options.add(DOCKER_INTERPRETER_INPUT); + private List getInterpreterCommand(File interpreterFile, Path lustreFile, String containerName) { + 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; } /** @@ -980,9 +1129,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; @@ -1071,6 +1220,49 @@ 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. 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. + */ + 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.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); + } + } + } + /** * If called with true, enables safe mode for this API instance. * Safe mode enables the following features: disabling the use of include statements, @@ -1862,12 +2054,16 @@ 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 = getKind2Command(null, new ArrayList<>()); + 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;