From dcbcc2938384bd08794e6776c17e8c33b69672a7 Mon Sep 17 00:00:00 2001
From: Philipp Haller <hallerp@gmail.com>
Date: Tue, 10 Oct 2006 15:01:56 +0000
Subject: Included proof of deadlock-freedom in Scheduler...

Included proof of deadlock-freedom in Scheduler.scala.
---
 src/actors/scala/actors/Actor.scala     |  4 ++--
 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
-- 
cgit v1.2.3