From d05652f54b7575a3380810cd01b6394230032085 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Wed, 22 Jul 2026 20:06:21 +0200 Subject: [PATCH 1/2] Enable parallel try close macro and fix GUI progress bar regression introduce by MT --- .../uka/ilkd/key/macros/DefaultAutoMacro.java | 2 +- .../de/uka/ilkd/key/macros/ProofMacro.java | 8 +++---- .../ilkd/key/macros/StrategyProofMacro.java | 2 +- .../de/uka/ilkd/key/macros/TryCloseMacro.java | 21 +++++++------------ .../uka/ilkd/key/prover/impl/AutoProvers.java | 10 --------- .../ilkd/key/prover/impl/ParallelProver.java | 8 +++---- .../ilkd/key/prover/mt/MtMacroStressTest.java | 7 ++----- .../de/uka/ilkd/key/gui/MainStatusLine.java | 11 +++++++--- .../java/de/uka/ilkd/key/gui/MainWindow.java | 8 +++---- .../gui/prooftree/ProofTreePopupFactory.java | 5 ++--- 10 files changed, 33 insertions(+), 49 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/DefaultAutoMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/DefaultAutoMacro.java index 2a922260db1..89efe28dbc5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/DefaultAutoMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/DefaultAutoMacro.java @@ -74,7 +74,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, AutoProvers.create(goalChooser, proof.getInitConfig().getProfile()); final ProofMacroListener pml = - new ProgressBarListener(goals.size(), getMaxSteps(proof), listener); + new ProgressBarListener(1, getMaxSteps(proof), listener); applyStrategy.addProverTaskObserver(pml); try { diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacro.java index 6503b2d20ee..79a41aa3f9b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacro.java @@ -245,9 +245,9 @@ public void taskStarted(TaskStartedInfo info) { String suffix = getMessageSuffix(); // info.size() <= 0 means the inner prover reports an unknown workload: the // parallel prover commits concurrently and emits no per-step progress. Propagate - // it so the bar goes indeterminate ("busy") instead of a determinate one frozen - // at 0%. A positive inner size keeps the normal determinate bar (single-core). - int size = info.size() <= 0 ? 0 : numberGoals * numberSteps; + // -1 so the bar goes indeterminate ("busy"). A positive inner size keeps the + // normal determinate bar (single-core). + int size = info.size() <= 0 ? -1 : numberGoals * numberSteps; super.taskStarted(new DefaultTaskStartedInfo(TaskKind.Macro, info.message() + suffix, size)); if (size > 0) { @@ -256,7 +256,7 @@ public void taskStarted(TaskStartedInfo info) { } protected String getMessageSuffix() { - return " [" + (completedGoals + 1) + "/" + numberGoals + "]"; + return numberGoals <= 1 ? "" : "[" + (completedGoals + 1) + "/" + numberGoals + "]"; } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java index 8713f7e0ece..c3828c108b8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java @@ -110,7 +110,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, // // The observer to handle the progress bar final ProofMacroListener pml = - new ProgressBarListener(goals.size(), getMaxSteps(proof), listener); + new ProgressBarListener(1, getMaxSteps(proof), listener); applyStrategy.addProverTaskObserver(pml); // add a focus manager if there is a focus if (posInOcc != null) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java index 453e264b040..a376bde68e1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java @@ -147,23 +147,18 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, return null; } - // - // create the rule application engine. This macro closes one goal at a time under a tight - // per-goal step budget (the numberSteps field, e.g. FullAutoPilotProofMacro's - // NUMBER_OF_TRY_STEPS default), so it is pinned to the single-threaded prover: a single - // goal offers no parallelism, and several workers exploring its subtree apply rules in a - // less step-efficient order than the single-threaded prover, which can exhaust the budget - // before the goal closes (leaving a closable goal pruned). Wide, generously-budgeted runs - // keep using the multi-core prover. + // create the rule application engine final Profile profile = proof.getServices().getProfile(); final ProverCore applyStrategy = AutoProvers.create( - profile.getSelectedGoalChooserBuilder().create(), profile, false); + profile.getSelectedGoalChooserBuilder().create(), profile); // assert: all goals have the same proof - // + int maxSteps = numberSteps > 0 ? numberSteps + : proof.getSettings().getStrategySettings().getMaxSteps(); + // The observer to handle the progress bar final TryCloseProgressBarListener pml = - new TryCloseProgressBarListener(goals.size(), numberSteps, listener); + new TryCloseProgressBarListener(goals.size(), maxSteps, listener); final ImmutableList ignoredOpenGoals = setDifference(proof.openGoals(), goals); applyStrategy.addProverTaskObserver(pml); @@ -177,10 +172,8 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, try { for (final Goal goal : goals) { Node node = goal.node(); - int maxSteps = numberSteps > 0 ? numberSteps - : proof.getSettings().getStrategySettings().getMaxSteps(); final ProofSearchInformation result = applyStrategy.start(proof, - ImmutableList.nil().prepend(goal), maxSteps, -1, false); + ImmutableList.singleton(goal), maxSteps, -1, false); // final Goal closedGoal; // retreat if not closed diff --git a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/AutoProvers.java b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/AutoProvers.java index 53533c74995..87fb028be57 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/AutoProvers.java +++ b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/AutoProvers.java @@ -44,16 +44,6 @@ public static ProverCore create(GoalChooser goalChoose * Creates the auto-prover selected by the current configuration, optionally forcing the * single-threaded prover. * - *

- * {@code allowParallel == false} pins the run to {@link ApplyStrategy} even when the multi-core - * prover is enabled. This is for drivers that close one goal at a time under a tight per-goal - * step budget (notably {@link de.uka.ilkd.key.macros.TryCloseMacro}): there is no parallelism - * to - * gain from a single goal, and several workers exploring one goal's subtree apply rules in a - * different, less step-efficient order than the single-threaded prover -- which can exhaust the - * budget before the goal closes. The wide, generously-budgeted runs (interactive automode and - * most macros) keep using the parallel prover, where it pays off. - * * @param goalChooser the goal chooser to use * @param profile the profile of the proof to be processed * @param allowParallel whether the parallel prover may be used at all for this run diff --git a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/ParallelProver.java b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/ParallelProver.java index ad50cf3c2cd..0a837326137 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/ParallelProver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/ParallelProver.java @@ -305,11 +305,11 @@ public synchronized ApplyStrategyInfo start(Proof proof, ImmutableL this.nonCloseableGoal = null; this.firstError.set(null); - // size 0 -> the status line shows an indeterminate ("busy") bar: the parallel prover does - // not report a meaningful per-step progress value (workers commit concurrently), so a - // determinate bar would either sit at zero or need thread-unsafe cross-worker counting. + // the status line shows an indeterminate ("busy") bar (size == -1): + // the parallel prover does not report a meaningful per-step progress value (workers + // commit concurrently) fireTaskStarted(new DefaultTaskStartedInfo(TaskStartedInfo.TaskKind.Strategy, - PROCESSING_STRATEGY, 0)); + PROCESSING_STRATEGY, -1)); ApplyStrategyInfo result = runParallel(goals); diff --git a/key.core/src/test/java/de/uka/ilkd/key/prover/mt/MtMacroStressTest.java b/key.core/src/test/java/de/uka/ilkd/key/prover/mt/MtMacroStressTest.java index 8d4e9d41a29..134327b2432 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/prover/mt/MtMacroStressTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/prover/mt/MtMacroStressTest.java @@ -33,10 +33,7 @@ * The first scenario guards pruning a subtree that was produced by many workers: a * parallel run is stopped by a tiny step budget, the resulting partial subtree is pruned back to * the root, and a second parallel run must then close the proof — a corrupted tree from the - * prune would show up as an inconsistent goal set, a failure to close, or an exception. (This was - * formerly phrased via {@link de.uka.ilkd.key.macros.TryCloseMacro}, but that macro deliberately - * pins itself to the single-threaded prover — see {@code AutoProvers.create} — so the - * prune-after-parallel-exploration scenario is exercised directly here.) + * prune would show up as an inconsistent goal set, a failure to close, or an exception. * *

* The second scenario runs {@link FinishSymbolicExecutionMacro} on the parallel prover: its filter @@ -86,7 +83,7 @@ static void restoreSettings() { * Each repetition: run the parallel prover with a tiny step budget at a high worker count * (produces a partial, many-worker-built subtree), prune that subtree back to the root, assert * the goal set is consistent, then run the parallel prover to completion and assert the proof - * closes -- proving the prune left a consistent, completable tree. + * closes, which proves that the prune left a consistent, completable tree. */ @Test void pruneOfParallelSubtreeStaysSafeUnderManyWorkers() throws Exception { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainStatusLine.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainStatusLine.java index 3634f808f18..802a418829d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainStatusLine.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainStatusLine.java @@ -78,17 +78,22 @@ public void reset() { /** * Set the range of values the progress bar can display (see setMaximum of - * ProgressBar). A non-positive maximum means "unknown workload" -- the parallel - * prover reports no per-step progress -- and switches the bar to indeterminate ("busy") mode so + * ProgressBar). A negative value means + * "unknown workload", e.g. the parallel prover reports + * no per-step progress and switches the bar to indeterminate ("busy") mode so * it animates instead of sitting frozen at zero. + * The value 0 means no bar and positive number describes the maximum workload. */ public void setProgressBarMaximum(int value) { - if (value <= 0) { + if (value < 0) { progressBar.setIndeterminate(true); + } else if (value == 0) { + progressBar.setIndeterminate(false); } else { progressBar.setIndeterminate(false); progressBar.setMaximum(value); } + progressBar.setEnabled(value != 0); } /** diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 2487d19eb5b..3fc25d6b34e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -899,14 +899,14 @@ public void hideStatusProgress() { private void setStatusLineImmediately(String str, int max) { statusLine.setStatusText(str); - // A non-positive maximum means "unknown workload" -- the parallel prover (whose workers - // commit concurrently) and symbolic-execution stop conditions report no per-step progress. + // A negative maximum means "unknown workload", e.g. the parallel prover (whose workers + // commit concurrently). // Show the progress panel and let setProgressBarMaximum switch the bar to indeterminate // ("busy") mode so it animates, instead of hiding it and sitting frozen. A positive maximum // drives the normal determinate bar. (The panel is hidden again at task end via reset() / - // hideStatusProgress().) + // hideStatusProgress().) A maximum of 0 hides the bar getStatusLine().setProgressBarMaximum(max); - statusLine.setProgressPanelVisible(true); + statusLine.setProgressPanelVisible(max != 0); statusLine.validate(); statusLine.paintImmediately(0, 0, statusLine.getWidth(), statusLine.getHeight()); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java index ea17dc77998..9077e2d5259 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java @@ -488,9 +488,8 @@ public void eventCutting() { @Override public void eventException(Throwable throwable) { - // Clear the "Cutting..." status and its indeterminate ("busy") progress - // bar; the success path does this in eventEnd, and without it the bar - // keeps animating forever after a failed cut. + // Clear the "Cutting..." status text; the success path does + // this in eventEnd mediator.getUI().resetStatus(this); mediator.startInterface(true); From b9543d7f92f88fe76b978667a51fcd3f814716b3 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 23 Jul 2026 07:48:46 +0200 Subject: [PATCH 2/2] Changes from the StipuLa case study to improve GoalList performance - Stop pretty printing early when max length is reached. - Until know GoalList printed the whole sequent and afterwards shortened, this becomes a bottleneck for proofs with many goals and long sequents In StiupuLa that amounted to 7s to 10s freezing of the GUI after the prover finished --- .../java/de/uka/ilkd/key/pp/LogicPrinter.java | 38 ++++++++++++++++++- .../java/de/uka/ilkd/key/gui/GoalList.java | 5 ++- .../key/gui/WindowUserInterfaceControl.java | 2 - 3 files changed, 41 insertions(+), 4 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java index 6fb286cd17b..734e62a8d56 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java @@ -90,6 +90,9 @@ public class LogicPrinter { private QuantifiableVariablePrintMode quantifiableVariablePrintMode = QuantifiableVariablePrintMode.NORMAL; + // Stop printing after maxChar characters; -1 prints whole term independent of size + private int maxChar = -1; + private enum QuantifiableVariablePrintMode { NORMAL, WITH_OUT_DECLARATION } @@ -157,6 +160,37 @@ public static String quickPrintTerm(JTerm t, Services services) { NotationInfo.DEFAULT_UNICODE_ENABLED, NotationInfo.DEFAULT_HIDE_PACKAGE_PREFIX); } + + /** + * converts a term to a String + * + * @param t a term. + * @param maxChar number of characters to be printed (-1 = unlimited + * @param services the Services class with information about the logic + * @return the printed semisequent. + */ + public static String quickPrintTerm(JTerm t, int maxChar, Services services) { + LogicPrinter p = quickPrinter(services, NotationInfo.DEFAULT_PRETTY_SYNTAX, + NotationInfo.DEFAULT_UNICODE_ENABLED, + NotationInfo.DEFAULT_HIDE_PACKAGE_PREFIX); + p.setMaxChar(maxChar); + p.layouter().beginC(); + p.printTerm(t); + p.layouter().end(); + final String result = p.result(); + return result + (result.length() >= maxChar ? "..." : ""); + } + + /** + * sets the maximal number of characters to be printed + * + * @param maxChar number of characters to be printed (-1 = unlimited) + */ + public void setMaxChar(int maxChar) { + this.maxChar = maxChar; + } + + /** * Converts a term to a string. * @@ -821,7 +855,9 @@ public void printTerm(JTerm t) { if (parens) { layouter.print("("); } - notation.print(t, this); + if (maxChar == -1 || layouter.backend().count() < maxChar) { + notation.print(t, this); + } if (parens) { layouter.print(")"); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java index 23a0f486c40..3a87fc4acc7 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java @@ -229,12 +229,15 @@ public boolean contains(Name name) { } }); // do not print term labels try { + sp.setMaxChar(MAX_DISPLAYED_SEQUENT_LENGTH); sp.printSequent(seq); // Only read the result once printing has completed: result() returns the raw // backend buffer without flushing, so on a failed print it would yield a // truncated/empty sequent. Read it here on the success path instead. res = sp.result().replace('\n', ' '); - res = res.substring(0, Math.min(MAX_DISPLAYED_SEQUENT_LENGTH, res.length())); + if (res.length() > MAX_DISPLAYED_SEQUENT_LENGTH) { + res = res.substring(0, MAX_DISPLAYED_SEQUENT_LENGTH) + "..."; + } } catch (Exception ex) { LOGGER.warn("GoalList: Problem printing sequent.", ex); res = ""; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java index 76c5fed1476..0436f16f0bd 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java @@ -264,8 +264,6 @@ private void taskFinishedInternal(TaskFinishedInfo info) { mainWindow.displayResults(info.toString()); } } - // this seems to be a good place to free some memory - Runtime.getRuntime().gc(); } /**