From a4be7c57190ab0fa387488c33553db835bbcffc9 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Thu, 14 May 2020 23:01:21 +0200
Subject: [PATCH] Implement kernel interrupts properly
Jupyter's default interrupt behavior is to send a signal to the kernel
process, which terminates the process unless the process handles it
(which Java does not allow). By changing the kernel.json interrupt_mode
setting to message, Jupyter will instead send a regular message to the
kernel to request an interrupt, which is handled by the basekernel and
passed to the kernel implementation.
Our interrupt implementation now interrupts the Java thread of the
currently running command and sends an interrupt to the current state
space (which interrupts the underlying probcli). This should be
sufficient to interrupt all long-running code in probcli and ProB 2.
---
CHANGELOG.md | 1 +
src/main/java/de/prob2/jupyter/Main.java | 1 +
.../java/de/prob2/jupyter/ProBKernel.java | 30 ++++++++++++++++---
3 files changed, 28 insertions(+), 4 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9c5d7f2..26b076d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,7 @@
* Added support for Java 14.
* Added B parser version information to `:version` output.
+* Improved interrupt handling so that only the currently running command is interrupted, rather than terminating the entire kernel. This means that interrupts now no longer reset the kernel state (loaded machine, current animator state, local variables, etc.).
* Updated ProB 2 to version 3.11.0.
* Fixed a parse error when a line comment is used on the last line of an expression while any `:let` variables are defined.
* Fixed detection of B machines in cells without `::load`. Previously only single-line machines were recognized.
diff --git a/src/main/java/de/prob2/jupyter/Main.java b/src/main/java/de/prob2/jupyter/Main.java
index 574ab1f..4289a04 100644
--- a/src/main/java/de/prob2/jupyter/Main.java
+++ b/src/main/java/de/prob2/jupyter/Main.java
@@ -119,6 +119,7 @@ public final class Main {
kernelJsonData.add("argv", kernelJsonArgv);
kernelJsonData.addProperty("display_name", "ProB 2");
kernelJsonData.addProperty("language", "prob");
+ kernelJsonData.addProperty("interrupt_mode", "message");
final Gson gson = new GsonBuilder()
.setPrettyPrinting()
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index d32646d..f9eedb5 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -14,6 +14,7 @@ import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Properties;
+import java.util.concurrent.atomic.AtomicReference;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
import java.util.stream.Collectors;
@@ -192,6 +193,7 @@ public final class ProBKernel extends BaseKernel {
private final @NotNull AnimationSelector animationSelector;
private final @NotNull Map<@NotNull String, @NotNull Command> commands;
+ private final @NotNull AtomicReference<@Nullable Thread> currentEvalThread;
private final @NotNull Map<@NotNull String, @NotNull String> variables;
private @NotNull Path currentMachineDirectory;
@@ -208,6 +210,7 @@ public final class ProBKernel extends BaseKernel {
.map(injector::getInstance)
.collect(Collectors.toMap(Command::getName, cmd -> cmd));
+ this.currentEvalThread = new AtomicReference<>(null);
this.variables = new HashMap<>();
this.animationSelector.changeCurrentAnimation(new Trace(classicalBFactory.create("(initial Jupyter machine)", "MACHINE repl END").load()));
@@ -319,10 +322,7 @@ public final class ProBKernel extends BaseKernel {
return MACHINE_CODE_PATTERN.matcher(code).matches();
}
- @Override
- public @Nullable DisplayData eval(final String expr) {
- assert expr != null;
-
+ private @Nullable DisplayData evalInternal(final @NotNull String expr) {
final Matcher commandMatcher = COMMAND_PATTERN.matcher(expr);
if (commandMatcher.matches()) {
// The input is a command, execute it directly.
@@ -340,6 +340,19 @@ public final class ProBKernel extends BaseKernel {
}
}
+ @Override
+ public @Nullable DisplayData eval(final String expr) {
+ assert expr != null;
+
+ this.currentEvalThread.set(Thread.currentThread());
+
+ try {
+ return evalInternal(expr);
+ } finally {
+ this.currentEvalThread.set(null);
+ }
+ }
+
@Override
public @Nullable DisplayData inspect(final @NotNull String code, final int at, final boolean extraDetail) {
// Note: We ignore the extraDetail parameter, because in practice it is always false. This is because the inspect_request messages sent by Jupyter Notebook always have their detail_level set to 0.
@@ -442,6 +455,15 @@ public final class ProBKernel extends BaseKernel {
this.animationSelector.getCurrentTrace().getStateSpace().kill();
}
+ @Override
+ public void interrupt() {
+ final Thread evalThread = this.currentEvalThread.get();
+ if (evalThread != null) {
+ evalThread.interrupt();
+ }
+ this.animationSelector.getCurrentTrace().getStateSpace().sendInterrupt();
+ }
+
private @NotNull List<@NotNull String> formatErrorSource(final @NotNull List<@NotNull String> sourceLines, final @NotNull ErrorItem.Location location) {
if (sourceLines.isEmpty()) {
return Collections.singletonList(this.errorStyler.primary("// Source code not known"));
--
GitLab