Skip to content

Commit

Permalink
Fix automode freezing the UI (#3203)
Browse files Browse the repository at this point in the history
See #3200 for details. This PR fixes all of #3200.
  • Loading branch information
mattulbrich authored Jul 21, 2023
2 parents f56c6fc + 7434c26 commit 0ac6d7f
Show file tree
Hide file tree
Showing 8 changed files with 156 additions and 6 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -706,9 +706,8 @@ public Pair<String, Location> getProofScript() throws ProblemLoaderException {
}
}

private ReplayResult replayProof(Proof proof)
throws ProofInputException, ProblemLoaderException {
LOGGER.info("Replaying proof " + proof.name());
private ReplayResult replayProof(Proof proof) {
LOGGER.info("Replaying proof {}", proof.name());
String status = "";
List<Throwable> errors = new LinkedList<>();
Node lastTouchedNode = proof.root();
Expand Down
2 changes: 2 additions & 0 deletions key.ui/src/main/java/de/uka/ilkd/key/core/Main.java
Original file line number Diff line number Diff line change
Expand Up @@ -178,6 +178,8 @@ public static void main(final String[] args) {
// does no harm on non macs
System.setProperty("apple.laf.useScreenMenuBar", "true");

Watchdog.start();

try {
cl = createCommandLine();
cl.parse(args);
Expand Down
118 changes: 118 additions & 0 deletions key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,118 @@
package de.uka.ilkd.key.core;

import java.awt.*;
import java.util.Set;

import de.uka.ilkd.key.util.ThreadUtilities;

import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

/**
* Watchdog to monitor the state of the KeY system. If all worker and UI threads
* are waiting / blocked, a deadlock is reported to the log.
*
* @author Arne Keller
*/
public final class Watchdog {
private static final Logger LOGGER = LoggerFactory.getLogger(Watchdog.class);
/**
* Threads that are ignored by the watchdog when checking for a deadlock.
* These are not relevant for that use case since they are always runnable.
*/
private static final Set<String> IGNORED_THREADS = Set.of("Watchdog", "Reference Handler",
"Signal Dispatcher", "Notification Thread", "AWT-XAWT", "DestroyJavaVM");
/**
* These modules are ignored when printing stacktraces.
*/
private static final Set<String> IGNORED_MODULES = Set.of("java.desktop", "java.base");

private Watchdog() {

}

/**
* Start the watchdog in a background thread.
*/
public static void start() {
new Thread(Watchdog::run, "Watchdog").start();
}

private static void run() {
while (true) {
try {
Thread.sleep(20000);
} catch (InterruptedException e) {
return;
}
var threads = ThreadUtilities.getThreads();
var anyProgress = false;

/*
* example of UI deadlock:
*
* Reference Handler RUNNABLE
* Finalizer WAITING
* Signal Dispatcher RUNNABLE
* Notification Thread RUNNABLE
* Java2D Disposer WAITING
* AWT-XAWT RUNNABLE
* AWT-Shutdown WAITING
* process reaper TIMED_WAITING
* TimerQueue WAITING
* Thread-0 RUNNABLE
* Timer-0 TIMED_WAITING
* AWT-EventQueue-0 TIMED_WAITING
* DestroyJavaVM RUNNABLE
* SwingWorker-pool-1-thread-1 WAITING
* ForkJoinPool.commonPool-worker-1 TIMED_WAITING
* Common-Cleaner TIMED_WAITING
*/

for (Thread thread : threads) {
if (thread == null || IGNORED_THREADS.contains(thread.getName())) {
continue;
}
switch (thread.getState()) {
case NEW:
case RUNNABLE:
anyProgress = true;
break;
case WAITING:
if (thread.getName().equals("AWT-EventQueue-0")
&& EventQueue.getCurrentEvent() == null) {
anyProgress = true; // nothing to do
}
break;
case BLOCKED:
case TIMED_WAITING:
case TERMINATED:
break;
}
}

if (!anyProgress) {
// print error to console
// unfortunately, we cannot display a dialog since the UI thread is blocked...
LOGGER.error("Watchdog detected deadlock!");
LOGGER.info("Current thread state:");
for (Thread thread : threads) {
if (thread == null || IGNORED_THREADS.contains(thread.getName())) {
continue;
}
LOGGER.info("{} {}", thread.getName(), thread.getState());
var trace = thread.getStackTrace();
for (int j = 0; j < trace.length; j++) {
var el = trace[j];
if (j > 0 && el.getModuleName() != null
&& IGNORED_MODULES.contains(el.getModuleName())) {
continue;
}
LOGGER.info(" {}", el);
}
}
return;
}
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,7 @@ public void progressStarted(Object sender) {

@Override
public void progressStopped(Object sender) {
mainWindow.getMediator().startInterface(true);
// no need to call startInterface(), will be done by ProblemLoader once loading is done
}

@Override
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -166,7 +166,7 @@ public void actionPerformed(ActionEvent e) {
// This method delegates the request only to the UserInterfaceControl which implements
// the functionality.
// No functionality is allowed in this method body!
getMediator().getUI().getProofControl().stopAndWaitAutoMode();
getMediator().getUI().getProofControl().stopAutoMode();
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ public void runAsynchronously() {
private long runTime;

@Override
protected Throwable doInBackground() throws Exception {
protected Throwable doInBackground() {
long currentTime = System.currentTimeMillis();
final Throwable message = doWork();
runTime = System.currentTimeMillis() - currentTime;
Expand Down
10 changes: 10 additions & 0 deletions key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,9 @@

import org.key_project.util.collection.ImmutableList;

import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

/**
* A {@link ProofControl} which performs the automode in a {@link SwingWorker}.
*
Expand All @@ -32,6 +35,8 @@
// KeYMediator.
// Refactor the implementation and use events to update the user interface.
public class MediatorProofControl extends AbstractProofControl {
private static final Logger LOGGER = LoggerFactory.getLogger(MediatorProofControl.class);

private final AbstractMediatorUserInterfaceControl ui;
private AutoModeWorker worker;

Expand Down Expand Up @@ -95,6 +100,11 @@ public void stopAutoMode() {
*/
@Override
public void waitWhileAutoMode() {
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
}
while (ui.getMediator().isInAutoMode()) { // Wait until auto mode has stopped.
try {
Thread.sleep(100);
Expand Down
21 changes: 21 additions & 0 deletions key.ui/src/main/java/de/uka/ilkd/key/util/ThreadUtilities.java
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,9 @@
public final class ThreadUtilities {
private static final Logger LOGGER = LoggerFactory.getLogger(ThreadUtilities.class);

private ThreadUtilities() {
}


/**
* Invoke a runnable object on the AWT event thread and wait for the execution to finish.
Expand Down Expand Up @@ -49,4 +52,22 @@ public static void invokeOnEventQueue(Runnable runnable) {
}
}

/**
* Get all running threads.
*
* @return array of threads, some entries may be null
*/
public static Thread[] getThreads() {
ThreadGroup rootGroup = Thread.currentThread().getThreadGroup();
ThreadGroup parentGroup;
while ((parentGroup = rootGroup.getParent()) != null) {
rootGroup = parentGroup;
}

Thread[] threads = new Thread[rootGroup.activeCount() + 1];
while (rootGroup.enumerate(threads, true) == threads.length) {
threads = new Thread[threads.length * 2];
}
return threads;
}
}

0 comments on commit 0ac6d7f

Please sign in to comment.