DefaultProofControl spinlock free

+ spotless
KeYProject · Dec 7, 2023 · 6d17cc6 · 6d17cc6
1 parent efa8064
commit 6d17cc6
Show file tree

Hide file tree

Showing 3 changed files with 47 additions and 7 deletions.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/DefaultProofControl.java b/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));
             }

diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java
@@ -6,7 +6,6 @@
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.EventObject;
-import java.util.concurrent.locks.Condition;
 import java.util.List;
 import java.util.concurrent.CopyOnWriteArrayList;
 import java.util.function.Consumer;

diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java
@@ -28,9 +28,9 @@
 import de.uka.ilkd.key.rule.Taclet;
 import de.uka.ilkd.key.strategy.StrategyProperties;
 
-import org.jspecify.annotations.Nullable;
 import org.key_project.util.collection.ImmutableList;
 
+import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
@@ -49,7 +49,8 @@ public class MediatorProofControl extends AbstractProofControl {
     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.
+     * 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;
@@ -118,7 +119,7 @@ public void waitWhileAutoMode() {
                 "tried to block the UI thread whilst waiting for auto mode to finish"));
             return; // do not block the UI thread
         }
-        if(notInAutoMode != null) {
+        if (notInAutoMode != null) {
             try {
                 notInAutoMode.await();
             } catch (InterruptedException ignore) {