preemptive vs cooperative: attempt at formalization

[Simon Marlow]

On 11 April 2006 22:24, John Meacham wrote:

> I'd like to be a bit more formal when it comes to the distinction
> between cooperative and preemptive implementations of concurrency,
> here is a first attempt.
> 
> 1. termination,
> 
> In a concurrent implementation, a thread performing an infinite loop
> with no IO or interaction with the outside world can potentially stall
> switching to another thread forever, in FP, we usually denote an
> infinite loop by _|_. so I think the first difference would be:
> 
> [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 don't know what it means for a thread to "have value _|_".  A thread
is defined by its observable effects, threads don't have values.

> I am using _|_ in the stronger sense of non-termination, not including
> things like exceptions which should have a well defined behavior.
> 
> 2. fairness
> 
> Assuming no thread has value _|_ now, what can both models guarentee
> when it comes to fairness?
> 
> both can guarentee every runnable thread will eventually run with a
> round-robin type scheduler.

What if one of the threads never yields in a cooperative system?  Even
if it isn't calculating _|_, if it's just endlessly doing some pointless
IO?

Cheers,
	Simon