Skip to content

Run KeY operations on a dedicated executor instead of the common pool #14

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
wadoon merged 1 commit into from
Jun 29, 2026
Merged

Run KeY operations on a dedicated executor instead of the common pool #14

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
58 changes: 39 additions & 19 deletions keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,11 @@
import java.util.Objects;
import java.util.Stack;
import java.util.concurrent.CompletableFuture;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.Executors;
import java.util.concurrent.atomic.AtomicInteger;
import java.util.function.Function;
import java.util.function.Supplier;
import java.util.stream.Collectors;
import java.util.stream.Stream;
import java.util.stream.StreamSupport;
Expand Down Expand Up @@ -102,9 +105,25 @@ public void taskFinished(TaskFinishedInfo info) {
private final Map<String, ProofMacro> macrosByName = availableMacros.stream()
.collect(Collectors.toUnmodifiableMap(ProofMacro::getName, m -> m, (a, b) -> a));

/// Dedicated executor for KeY operations. Several of them (auto, macro,
/// script, ...) block their worker thread for the whole proof run, so running
/// them on the shared ForkJoinPool.commonPool() could starve unrelated work
/// across the JVM. Daemon threads, so the pool never keeps the JVM alive.
private final ExecutorService executor = Executors.newCachedThreadPool(runnable -> {
var thread = new Thread(runnable, "key-api-worker");
thread.setDaemon(true);
return thread;
});

public KeyApiImpl() {
}

/// Runs {@code task} on the dedicated {@link #executor} rather than the
/// common pool.
private <T> CompletableFuture<T> async(Supplier<T> task) {
return CompletableFuture.supplyAsync(task, executor);
}

private static <T> List<T> loadAll(Class<T> service) {
return StreamSupport.stream(
ClassLoaderUtil.loadServices(service).spliterator(), false).toList();
Expand All @@ -125,6 +144,7 @@ public CompletableFuture<Boolean> shutdown() {

@Override
public void exit() {
executor.shutdownNow();
this.exitHandler.apply(null);
}

Expand Down Expand Up @@ -157,7 +177,7 @@ public CompletableFuture<List<ProofScriptCommandDesc>> getAvailableScriptCommand
@Override
public CompletableFuture<MacroStatistic> script(ProofId proofId, String scriptLine,
StrategyOptions options) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var proof = data.find(proofId);
var env = data.find(proofId.env());
var script = ParsingFacade.parseScript(scriptLine);
Expand All @@ -175,7 +195,7 @@ public CompletableFuture<MacroStatistic> script(ProofId proofId, String scriptLi
@Override
public CompletableFuture<MacroStatistic> macro(ProofId proofId, String macroName,
StrategyOptions options) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var proof = data.find(proofId);
var env = data.find(proofId.env());
var macro = macrosByName.get(macroName);
Expand All @@ -196,7 +216,7 @@ public CompletableFuture<MacroStatistic> macro(ProofId proofId, String macroName

@Override
public CompletableFuture<ProofStatus> auto(ProofId proofId, StrategyOptions options) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var proof = data.find(proofId);
var env = data.find(proofId.env());
options.configure(proof);
Expand All @@ -223,7 +243,7 @@ public CompletableFuture<Boolean> dispose(ProofId id) {
@Override
public CompletableFuture<List<NodeDesc>> goals(ProofId proofId, boolean onlyOpened,
boolean onlyEnabled) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var proof = data.find(proofId);
if (onlyOpened && !onlyEnabled) {
return asNodeDesc(proofId, proof.openGoals());
Expand All @@ -250,7 +270,7 @@ private NodeDesc asNodeDesc(ProofId proofId, Node it) {

@Override
public CompletableFuture<NodeDesc> tree(ProofId proofId) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var proof = data.find(proofId);
return asNodeDescRecursive(proofId, proof.root());
});
Expand All @@ -268,15 +288,15 @@ private NodeDesc asNodeDescRecursive(ProofId proofId, Node root) {

@Override
public CompletableFuture<List<NodeDesc>> children(NodeId nodeId) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var node = data.find(nodeId);
return asNodeDesc(nodeId.proofId(), node.childrenStream());
});
}

@Override
public CompletableFuture<List<NodeDesc>> pruneTo(NodeId nodeId) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var proof = data.find(nodeId.proofId());
var node = data.find(nodeId);

Expand All @@ -292,7 +312,7 @@ public CompletableFuture<List<NodeDesc>> pruneTo(NodeId nodeId) {
/*
* @Override
* public CompletableFuture<Statistics> statistics(ProofId proofId) {
* return CompletableFuture.supplyAsync(() -> {
* return async(() -> {
* var proof = data.find(proofId);
* return proof.getStatistics();
* });
Expand All @@ -301,7 +321,7 @@ public CompletableFuture<List<NodeDesc>> pruneTo(NodeId nodeId) {

@Override
public CompletableFuture<Boolean> save(ProofId proofId, String path) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var proof = data.find(proofId);
var saver = new OutputStreamProofSaver(proof);

Expand All @@ -325,7 +345,7 @@ public CompletableFuture<TreeNodeDesc> treeRoot(ProofId proof) {

@Override
public CompletableFuture<NodeDesc> root(ProofId proofId) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var proof = data.find(proofId);
return asNodeDesc(proofId, proof.root());
});
Expand All @@ -339,7 +359,7 @@ public CompletableFuture<List<ProofId>> list() {

@Override
public CompletableFuture<List<TreeNodeDesc>> treeChildren(ProofId proof, TreeNodeId nodeId) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var serial = Integer.parseInt(nodeId.id());

Node root = data.find(proof).root();
Expand Down Expand Up @@ -373,7 +393,7 @@ public CompletableFuture<List<TreeNodeDesc>> treeChildren(ProofId proof, TreeNod

@Override
public CompletableFuture<List<TreeNodeDesc>> treeSubtree(ProofId proof, TreeNodeId nodeId) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var serial = Integer.parseInt(nodeId.id());
Node root = data.find(proof).root();

Expand Down Expand Up @@ -419,7 +439,7 @@ public CompletableFuture<List<TreeNodeDesc>> treeSubtree(ProofId proof, TreeNode

@Override
public CompletableFuture<List<SortDesc>> sorts(EnvironmentId envId) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var env = data.find(envId);
var sorts = env.getServices().getNamespaces().sorts().allElements();
return sorts.stream().map(SortDesc::from).toList();
Expand All @@ -428,7 +448,7 @@ public CompletableFuture<List<SortDesc>> sorts(EnvironmentId envId) {

@Override
public CompletableFuture<List<FunctionDesc>> functions(EnvironmentId envId) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var env = data.find(envId);
var functions = env.getServices().getNamespaces().functions().allElements();
return functions.stream().map(FunctionDesc::from).toList();
Expand All @@ -437,7 +457,7 @@ public CompletableFuture<List<FunctionDesc>> functions(EnvironmentId envId) {

@Override
public CompletableFuture<List<ContractDesc>> contracts(EnvironmentId envId) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var env = data.find(envId);
var contracts = env.getProofContracts();
return contracts.stream().map(it -> ContractDesc.from(envId, env.getServices(), it))
Expand All @@ -447,7 +467,7 @@ public CompletableFuture<List<ContractDesc>> contracts(EnvironmentId envId) {

@Override
public CompletableFuture<ProofId> openContract(ContractId contractId) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var env = data.find(contractId.envId());
var contracts = env.getProofContracts();
var contract =
Expand Down Expand Up @@ -476,7 +496,7 @@ public CompletableFuture<Boolean> envDispose(EnvironmentId environmentId) {

@Override
public CompletableFuture<NodeTextDesc> print(NodeId nodeId, PrintOptions options) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var node = data.find(nodeId);
var env = data.find(nodeId.proofId().env());
var notInfo = new NotationInfo();
Expand Down Expand Up @@ -527,7 +547,7 @@ private NodeTextSpan[] expandTermsForTable(PositionTable table) {

@Override
public CompletableFuture<List<TermActionDesc>> actions(NodeTextId printId, int caretPos) {
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var node = data.find(printId.nodeId());
var proof = data.find(printId.nodeId().proofId());
var goal = proof.getOpenGoal(node);
Expand All @@ -547,7 +567,7 @@ public CompletableFuture<List<TermActionDesc>> actions(NodeTextId printId, int c
@Override
public CompletableFuture<Boolean> applyAction(TermActionId id) {
// FIXME: We can probably cache this work in `actions`.
return CompletableFuture.supplyAsync(() -> {
return async(() -> {
var node = data.find(id.nodeTextId().nodeId());
var proof = data.find(id.nodeTextId().nodeId().proofId());
var goal = proof.getOpenGoal(node);
Expand Down
27 changes: 27 additions & 0 deletions keyext.api/src/test/java/org/keyproject/key/api/KeyApiExecutorTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
/* This file is part of KeY - https://key-project.org
* KeY is licensed under the GNU General Public License Version 2
* SPDX-License-Identifier: GPL-2.0-only */
package org.keyproject.key.api;

import org.junit.jupiter.api.Assertions;
import org.junit.jupiter.api.Test;

/**
* Smoke test that operations dispatched through the dedicated executor (instead
* of the common ForkJoinPool) still complete correctly.
*/
class KeyApiExecutorTest {
@Test
void executorBackedOperationsComplete() throws Exception {
var api = new KeyApiImpl();
var proofId = api.loadTerm("true").get();

// root()/goals() are dispatched on the dedicated executor; a completing
// future proves the executor accepts and runs the task.
var root = api.root(proofId).get();
Assertions.assertNotNull(root);
var goals = api.goals(proofId, false, false).get();
Assertions.assertNotNull(goals);
Assertions.assertFalse(goals.isEmpty());
}
}
Loading