preemptive vs cooperative: attempt at formalization

[Simon Marlow]

On 13 April 2006 10:53, John Meacham wrote:

> On Thu, Apr 13, 2006 at 09:46:03AM +0100, Simon Marlow wrote:
>> You seem to be assuming more about cooperative scheduling than eg.
>> Hugs provides.  I can easily write a thread that starves the rest of
>> the system without using any _|_s.  eg.
>> 
>>   let loop = do x <- readIORef r; writeIORef r (x+1); loop in loop
> 
> this is a non-productive non-cooperative loop, as in _|_.

Ok, I'm confused because I'm thinking in terms of operational semantics
for IO.

Maybe a way to describe this is to give a meaning to an value of type IO
as a lazy sequence of yields and effects, with some way of "evaluating"
an IO action in the context of the world state, to get the next yield or
effect together with a continuation and the new world state.  Running an
IO action may give _|_ instead of the next yield or effect; ok.

Still, I think the operational semantics interpretation works fine too.

Cheers,
	Simon