diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/actors/scala/actors/Actor.scala | 4 | ||||
-rw-r--r-- | src/actors/scala/actors/Scheduler.scala | 41 |
2 files changed, 41 insertions, 4 deletions
diff --git a/src/actors/scala/actors/Actor.scala b/src/actors/scala/actors/Actor.scala index cf60bd95e2..47793a88f3 100644 --- a/src/actors/scala/actors/Actor.scala +++ b/src/actors/scala/actors/Actor.scala @@ -13,8 +13,8 @@ package scala.actors import scala.collection.mutable.HashSet /** - * This object provides functions for the definition of actors and - * reactors, as well as all actor operations, such as + * This object provides functions for the definition of actors, + * as well as all actor operations, such as * <code>receive</code>, <code>react</code>, <code>reply</code>, * etc. * diff --git a/src/actors/scala/actors/Scheduler.scala b/src/actors/scala/actors/Scheduler.scala index bd98256aa9..8f27ce22a2 100644 --- a/src/actors/scala/actors/Scheduler.scala +++ b/src/actors/scala/actors/Scheduler.scala @@ -272,9 +272,46 @@ class QuitException extends Throwable { /** * The class <code>WorkerThread</code> is used by schedulers to execute - * reactor tasks on multiple threads. + * actor tasks on multiple threads. + * + * !!ACHTUNG: If you change this, make sure you understand the following + * proof of deadlock-freedom!! + * + * We proof that there is no deadlock between the scheduler and + * any worker thread possible. For this, note that the scheduler + * only acquires the lock of a worker thread by calling + * `execute'. This method is only called when the worker thread + * is in the idle queue of the scheduler. On the other hand, a + * worker thread only acquires the lock of the scheduler when it + * calls `getTask'. At the only callsite of `getTask', the + * worker thread holds its own lock. + * + * Thus, deadlock can only occur when a worker thread calls + * `getTask' while it is in the idle queue of the scheduler, + * because then the scheduler might call (at any time!) `execute' + * which tries to acquire the lock of the worker thread. In such + * a situation the worker thread would be waiting to acquire the + * lock of the scheduler and vice versa. + * + * Therefore, to prove deadlock-freedom, it suffices to ensure + * that a worker thread will never call `getTask' when it is in + * the idle queue of the scheduler. + * + * A worker thread enters the idle queue of the scheduler when + * `getTask' returns <code>null</code>. Then it will also stay + * in the while-loop W (<code>while (task == null)</code>) until + * `task' becomes non-null. The only way this can happen is + * through a call of `execute' by the scheduler. Before every + * call of `execute' the worker thread is removed from the idle + * queue of the scheduler. Only then--after executing its task-- + * the worker thread may call `getTask'. However, the scheduler + * is unable to call `execute' as the worker thread is not in + * the idle queue any more. In fact, the scheduler made sure + * that this is the case even _before_ calling `execute' and + * thus releasing the worker thread from the while-loop W. Thus, + * the property holds for every possible interleaving of thread + * execution. QED * - * TODO: put proof of deadlock-freedom here! * * @version Beta2 * @author Philipp Haller |