Skip to content
Snippets Groups Projects
Commit 5342489f authored by Markus Alexander Kuppe's avatar Markus Alexander Kuppe
Browse files

[Bugfix] Remove deadlock that happens when the main thread tries to

block all worker threads to do its periodic work (liveness checking and
checkpointing) while the worker threads finish concurrently. This makes
the main thread wait indefinitely.

The chance for this bug has been drastically increased by the fix in
commit ea6532a2 (check liveness
independent of checkpointing timer).
parent a51bb242
No related branches found
No related tags found
No related merge requests found
...@@ -179,7 +179,19 @@ public abstract class StateQueue implements IStateQueue { ...@@ -179,7 +179,19 @@ public abstract class StateQueue implements IStateQueue {
*/ */
public synchronized void finishAll() { public synchronized void finishAll() {
this.finish = true; this.finish = true;
// Notify all other worker threads.
this.notifyAll(); this.notifyAll();
// Need to wake main thread that waits (mu.wait()) to suspend access to
// the squeue (see suspendAll). The main thread might attempt to do its
// periodic work (tlc2.tool.ModelChecker.doPeriodicWork()) the moment
// all worker threads finish. Since suspendAll assumes the main thread
// is woken up (potentially) multiple times from sleeping indefinitely
// in the while loop before it finally returns after locking the
// StateQueue, we have to live up to this assumption.
synchronized (this.mu) {
// Technically notify() would do.
this.mu.notify();
}
} }
/* (non-Javadoc) /* (non-Javadoc)
...@@ -194,11 +206,13 @@ public abstract class StateQueue implements IStateQueue { ...@@ -194,11 +206,13 @@ public abstract class StateQueue implements IStateQueue {
this.stop = true; this.stop = true;
needWait = needsWaiting(); needWait = needsWaiting();
} }
// Wait for all worker threads to stop.
while (needWait) { while (needWait) {
synchronized (this.mu) { synchronized (this.mu) {
try { try {
// waiting here assumes that subsequently a worker // waiting here assumes that subsequently a worker
// is going to wake us up by calling isAvail() // is going to wake us up by calling isAvail() or
// this.mu.notify*()
this.mu.wait(); this.mu.wait();
} catch (Exception e) { } catch (Exception e) {
MP.printError(EC.GENERAL, "waiting for a worker to wake up", e); // LL changed call 7 April 2012 MP.printError(EC.GENERAL, "waiting for a worker to wake up", e); // LL changed call 7 April 2012
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment