[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 scheduling. 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. http://luca.soe.ucsc.edu/Publications?action=AttachFile&do=get&target=emsoft05.pdf ``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 infinitely often.... 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 termination.'' 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).