preemptive vs cooperative: attempt at formalization
oleg at pobox.com
oleg at pobox.com
Wed Apr 12 00:05:12 EDT 2006
> [Rule 1]
> * in a cooperative implementation of threading, any thread with value
> _|_ may cause the whole program to have value _|_. In a preemtive one,
> this is not true.
I'm afraid that claim may need qualifications:
1. if there is only one runnable thread, if it loops in pure code,
the whole program loops -- regardless of preemptive/cooperative
2. in a system with thread priorities, if the highest priority thread
loops (in pure code or otherwise), the whole program loops -- again
irrespective of the preemptive/cooperative scheduling.
3. [a variation of 1 or 2]. A thread that loops in a critical section
(or holding a mutex on which the other threads wait) loops the whole
program -- again, irrespective of preemptive/cooperative scheduling.
As an example of formalizing fairness, I'd like to point out
L. de Alfaro, M. Faella, R. Majumdar, V. Raman. Code Aware Resource
Management. In EMSOFT 05: Fifth ACM International Conference on Embedded
Software, ACM Press, 2005.
``To achieve compact, yet fair, managers, we consider win-
ning strategies that may be randomized, that is, scheduling
decisions may use lotteries over available moves; the strate-
gies ensure progress and fairness with probability 1.''
Of a special interest is p5 of the paper:
''Inter-thread nondeterminism. We assume that the underlying operating
system scheduler is fair: more precisely, we assume that, if a thread
is infinitely often ready to execute, it will make progress
Intra-thread nondeterminism. Assuming that intrathread nondeterminism
is resolved in an arbitrary way may easily lead to declaring the
manager synthesis problem to be infeasible. In fact, whenever a thread
can execute a loop while holding a resource, the arbitrary resolution
of intra-thread nondeterminism introduces the possibility that the
loop never terminates. In practice, a reasonable assumption is that
intra-thread nondeterminism is resolved in a (strongly) fair fashion:
if each choice is presented infinitely often, each choice outcome
will follow infinitely often. Such fairness entails loop
The paper then formalizes these fairness assumptions and the goal of
the fair resource manager in temporal logic.
Thus the difference between cooperative and preemptive scheduling
strategies becomes quite fuzzy: neither strategy guarantees much
unless we make some assumptions about threads (e.g., no thread loops
while holding a critical resource). But if we do make assumptions
about threads, we might as well assume that threads are behaving
nicely and yield (or the underlying monad or memory allocator yield
on their behalf).
More information about the Haskell-prime