Skip to content

Commit

Permalink
DefaultProofControl spinlock free
Browse files Browse the repository at this point in the history
+ spotless
  • Loading branch information
wadoon committed Jan 4, 2024
1 parent f7ed29f commit 0373d7c
Show file tree
Hide file tree
Showing 3 changed files with 47 additions and 7 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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.
*/
Expand All @@ -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.
*
Expand Down Expand Up @@ -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) {

}
}
}
Expand All @@ -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
Expand All @@ -122,6 +150,10 @@ public void run() {
starter.start();
}
} finally {
lock.lock();
notInAutoMode.signalAll();
lock.unlock();

autoModeThread = null;
fireAutoModeStopped(new ProofEvent(proof));
}
Expand All @@ -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
Expand All @@ -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));
}
Expand Down
1 change: 0 additions & 1 deletion key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -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;
Expand Down Expand Up @@ -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) {
Expand Down

0 comments on commit 0373d7c

Please sign in to comment.