preemptive vs cooperative: attempt at formalization

[Simon Marlow]

On 12 April 2006 17:51, Malcolm Wallace wrote:

> "Simon Marlow" <simonmar at microsoft.com> wrote:
> 
>>> By infinite loop, you mean both non-terminating, and non-productive.
>>> A non-terminating but productive pure computation (e.g. ones =
>>> 1:ones) is not necessarily a problem.
>> 
>> That's slightly odd terminology.  ones = 1:ones  is definitely
>> terminating.  (length ones) is not, though.
> 
> Well, the expression "ones" on its own is non-terminating.

under what definition of non-termination?  Non-termination has meant the
same as _|_ in a call-by-name semantics as far as I'm concerned, and
"ones" is most definitely not == _|_.

> So if you
> say "putStrLn (show ones)", it doesn't just sit there doing nothing.
> This infinite computation produces an infinite output.  So the fact
> that it is non-terminating is irrelevant.  I may very well want a
> thread to do exactly that, and even with a cooperative scheduler this
> is perfectly OK.  Other threads will still run just fine.

Depends entirely on whether putStrLn yields at regular intervals while
it is evaluating its argument.  If we are to allow cooperative
scheduling, then the spec needs to say whether it does or not (and
similarly for any IO operation you want to implicitly yield).

> The only time when other threads will *not* run under cooperative
> scheduling is when the non-terminating pure computation is *also*
> unproductive (like your "length ones").

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

I must be missing something.  The progress guarantee we have on the wiki
makes complete sense, but the fairness guarantee that John proposed
seems much stronger.

I had in mind defining something based on an operational semantics such
as in [1].  The cooperative guarantee would be something like "if any
transition can be made, then the system will choose one to make", with
an extra condition about pure terms that evaluate to _|_, and a
guarantee that certain operations like yield choose the next transition
from another thread.  Preemtpive would remove the _|_ condition, the
yield condition, and add a fairness property.

Cheers,
	Simon

[1] Asynchronous Exceptions in Haskell,
http://www.haskell.org/~simonmar/papers/async.pdf