WorkerThread is used by schedulers to execute
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
getTask. At the only callsite of
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!)
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
it is in the idle queue of the scheduler.
A worker thread enters the idle queue of the scheduler when
null. Then it will also stay
in the while-loop W (
while (task eq null)) until
task becomes non-null. The only way this can happen is
through a call of
execute by the scheduler. Before every
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
thus releasing the worker thread from the while-loop W. Thus,
the property holds for every possible interleaving of thread