Remove spin lock in waitWhileAutoMode.

key.core/src/main/java/de/uka/ilkd/key/control/DefaultProofControl.java

@@ -3,6 +3,10 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.control;
 
+import java.util.concurrent.locks.Condition;
+import java.util.concurrent.locks.ReentrantLock;
+import javax.swing.*;
+
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.macros.ProofMacro;
 import de.uka.ilkd.key.macros.ProofMacroFinishedInfo;
@@ -19,12 +23,20 @@
 
 import org.key_project.util.collection.ImmutableList;
 
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
 /**
  * The default implementation of {@link ProofControl}.
  *
  * @author Martin Hentschel
  */
+@NullMarked
 public class DefaultProofControl extends AbstractProofControl {
+    private static final Logger LOGGER = LoggerFactory.getLogger(DefaultProofControl.class);
+
     /**
      * The {@link UserInterfaceControl} in which this {@link ProofControl} is used.
      */
@@ -33,8 +45,15 @@ public class DefaultProofControl extends AbstractProofControl {
     /**
      * The currently running {@link Thread}.
      */
+    @Nullable
     private Thread autoModeThread;
 
+    /**
+     * A condition for waiting during active auto-mode.
+     */
+    @Nullable
+    private Condition notInAutoMode;
+
     /**
      * Constructor.
      *
@@ -81,10 +100,16 @@ public synchronized void stopAutoMode() {
 
     @Override
     public void waitWhileAutoMode() {
-        while (isInAutoMode()) { // Wait until auto mode has stopped.
+        if (SwingUtilities.isEventDispatchThread()) {
+            LOGGER.error("", new IllegalStateException(
+                "tried to block the UI thread whilst waiting for auto mode to finish"));
+            return; // do not block the UI thread
+        }
+        if (notInAutoMode != null) {
             try {
-                Thread.sleep(100);
-            } catch (InterruptedException e) {
+                notInAutoMode.await();
+            } catch (InterruptedException ignore) {
+
             }
         }
     }
@@ -101,10 +126,13 @@ private class AutoModeThread extends Thread {
 
         private final ProverTaskListener ptl;
 
+        private final ReentrantLock lock = new ReentrantLock();
+
         public AutoModeThread(Proof proof, ImmutableList<Goal> goals, ProverTaskListener ptl) {
             this.proof = proof;
             this.goals = goals;
             this.ptl = ptl;
+            notInAutoMode = lock.newCondition();
         }
 
         @Override
@@ -122,6 +150,10 @@ public void run() {
                     starter.start();
                 }
             } finally {
+                lock.lock();
+                notInAutoMode.signalAll();
+                lock.unlock();
+
                 autoModeThread = null;
                 fireAutoModeStopped(new ProofEvent(proof));
             }
@@ -146,10 +178,13 @@ private class MacroThread extends Thread {
 
         private final PosInOccurrence posInOcc;
 
+        private final ReentrantLock lock = new ReentrantLock();
+
         public MacroThread(Node node, ProofMacro macro, PosInOccurrence posInOcc) {
             this.node = node;
             this.macro = macro;
             this.posInOcc = posInOcc;
+            notInAutoMode = lock.newCondition();
         }
 
         @Override
@@ -172,6 +207,11 @@ public void run() {
                 if (ptl != null) {
                     ptl.taskFinished(info);
                 }
+
+                lock.lock();
+                notInAutoMode.signalAll();
+                lock.unlock();
+
                 autoModeThread = null;
                 fireAutoModeStopped(new ProofEvent(proof));
             }

key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java

@@ -93,7 +93,7 @@ public class KeYMediator {
     /**
      * boolean flag indicating if the GUI is in auto mode
      */
-    private boolean inAutoMode = false;
+    private volatile boolean inAutoMode;
 
     /**
      * Currently activated listeners for user actions. Notified whenever a user action is applied.
@@ -512,13 +512,12 @@ public synchronized void stopInterface(boolean fullStop) {
 
     public synchronized void startInterface(boolean fullStop) {
         final boolean b = fullStop;
-        Runnable interfaceSignaller = () -> {
+        SwingUtilities.invokeLater(() -> {
             if (b) {
                 inAutoMode = false;
             }
             ui.notifyAutomodeStopped();
-        };
-        ThreadUtilities.invokeOnEventQueue(interfaceSignaller);
+        });
     }
 
     /**
@@ -667,7 +666,7 @@ public void proofPruned(final ProofTreeEvent e) {
         public void proofGoalsAdded(ProofTreeEvent e) {
             ImmutableList<Goal> newGoals = e.getGoals();
             // Check for a closed goal ...
-            if (newGoals.size() == 0) {
+            if (newGoals.isEmpty()) {
                 // No new goals have been generated ...
                 closedAGoal();
             }

key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java

@@ -5,6 +5,8 @@
 
 import java.util.ArrayList;
 import java.util.List;
+import java.util.concurrent.locks.Condition;
+import java.util.concurrent.locks.ReentrantLock;
 import javax.swing.*;
 
 import de.uka.ilkd.key.control.InteractionListener;
@@ -69,6 +71,9 @@
     private Exception exception;
     private final List<InteractionListener> interactionListeners = new ArrayList<>();
 
+    /** a condition for signaling the ready state */
+    private final Condition cond;
+
     /**
      * Instantiates a new proof macro worker.
      *
@@ -85,6 +90,8 @@
         this.macro = macro;
         this.mediator = mediator;
         this.posInOcc = posInOcc;
+
+        cond = new ReentrantLock().newCondition();
     }
 
     @Override
@@ -105,6 +112,7 @@
         } catch (final Exception exception) {
             // This should actually never happen.
             this.exception = exception;
+        } finally {
         }
 
         return info;
@@ -129,6 +137,9 @@
 
             mediator.setInteractive(true);
             mediator.startInterface(true);
+            // give the signal to waiting threads
+            cond.signalAll();
+
             mediator.getUI().getProofControl().fireAutoModeStopped(new ProofEvent(node.proof()));
             if (SELECT_GOAL_AFTER_MACRO) {
                 selectOpenGoalBelow();
@@ -167,4 +178,8 @@
             }
         }
     }
+
+    public Condition getReadyCondition() {
+        return cond;
+    }
 }

key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java

@@ -6,6 +6,8 @@
 import java.util.List;
 import java.util.concurrent.CancellationException;
 import java.util.concurrent.ExecutionException;
+import java.util.concurrent.locks.Condition;
+import java.util.concurrent.locks.ReentrantLock;
 import java.util.stream.Collectors;
 import javax.swing.*;
 
@@ -28,6 +30,7 @@
 
 import org.key_project.util.collection.ImmutableList;
 
+import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
@@ -45,6 +48,13 @@ public class MediatorProofControl extends AbstractProofControl {
     private final AbstractMediatorUserInterfaceControl ui;
     private AutoModeWorker worker;
 
+    /**
+     * This is condition is non-null during auto-mode execution. You can wait on it to block until
+     * auto-mode has finished.
+     */
+    @Nullable
+    private Condition notInAutoMode;
+
     public MediatorProofControl(AbstractMediatorUserInterfaceControl ui) {
         super(ui, ui);
         this.ui = ui;
@@ -82,6 +92,8 @@ public void startAutoMode(Proof proof, ImmutableList<Goal> goals, ProverTaskList
             return;
         }
         worker = new AutoModeWorker(proof, goals, ptl);
+        notInAutoMode = worker.getReadyCondition();
+
         ui.getMediator().initiateAutoMode(proof, true, false);
         worker.execute();
     }
@@ -107,10 +119,11 @@ public void waitWhileAutoMode() {
                 "tried to block the UI thread whilst waiting for auto mode to finish"));
             return; // do not block the UI thread
         }
-        while (ui.getMediator().isInAutoMode()) { // Wait until auto mode has stopped.
+        if (notInAutoMode != null) {
             try {
-                Thread.sleep(100);
-            } catch (InterruptedException e) {
+                notInAutoMode.await();
+            } catch (InterruptedException ignore) {
+
             }
         }
     }
@@ -138,6 +151,7 @@ public boolean isAutoModeSupported(Proof proof) {
     public void runMacro(Node node, ProofMacro macro, PosInOccurrence posInOcc) {
         KeYMediator mediator = ui.getMediator();
         final ProofMacroWorker worker = new ProofMacroWorker(node, macro, mediator, posInOcc);
+        notInAutoMode = worker.getReadyCondition();
         interactionListeners.forEach(worker::addInteractionListener);
         mediator.initiateAutoMode(node.proof(), true, false);
         mediator.addInterruptedListener(worker);
@@ -158,6 +172,8 @@ private class AutoModeWorker extends SwingWorker<ApplyStrategyInfo, Object> {
         private final ImmutableList<Goal> goals;
         private final ApplyStrategy applyStrategy;
         private ApplyStrategyInfo info;
+        private final ReentrantLock lock;
+        private final Condition ready;
 
         public AutoModeWorker(final Proof proof, final ImmutableList<Goal> goals,
                 ProverTaskListener ptl) {
@@ -174,6 +190,9 @@ public AutoModeWorker(final Proof proof, final ImmutableList<Goal> goals,
             if (ui.getMediator().getAutoSaver() != null) {
                 applyStrategy.addProverTaskObserver(ui.getMediator().getAutoSaver());
             }
+
+            lock = new ReentrantLock();
+            ready = lock.newCondition();
         }
 
         @Override
@@ -193,6 +212,11 @@ protected void done() {
                     applyStrategy.clear();
                 }
                 ui.getMediator().finishAutoMode(proof, true, true, null);
+
+                lock.lock();
+                ready.signalAll();
+                lock.unlock();
+
                 emitInteractiveAutoMode(initialGoals, proof, info);
 
                 if (info.getException() != null) {
@@ -212,7 +236,7 @@ private void notifyException(final Throwable exception) {
         }
 
         @Override
-        protected ApplyStrategyInfo doInBackground() throws Exception {
+        protected ApplyStrategyInfo doInBackground() {
             boolean stopMode =
                 proof.getSettings().getStrategySettings().getActiveStrategyProperties()
                         .getProperty(StrategyProperties.STOPMODE_OPTIONS_KEY)
@@ -222,5 +246,9 @@ protected ApplyStrategyInfo doInBackground() throws Exception {
                 ui.getMediator().getAutomaticApplicationTimeout(), stopMode);
             return info;
         }
+
+        public Condition getReadyCondition() {
+            return ready;
+        }
     }
 }