preemptive vs cooperative: attempt at formalization

[Malcolm Wallace]

"Simon Marlow" <simonmar at microsoft.com> wrote:

> > 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 == _|_.

Ok, fair enough, if we accept that "ones" is terminating, because it
reaches a WHNF, then tell me what is the value of "print ones"?  For a
terminating computation, x, "print x" would have a real value of type
IO (), even though that value is abstract and you cannot name it.  But
surely the value of "print ones" is _|_, because it never terminates?

[ Hmm, maybe you would want to say that there _are_ WHNFs inside the
  value of "print ones", we just can't see them.  Abstractly, there is
  reduction going on like:
         print ones
    ==>  putChar '1' >> print ones
    ==>  putChar '1' >> putChar '1' >> print ones
    ==>  putChar '1' >> putChar '1' >> putChar '1' >> print ones
  and each of those sequenced putChar actions is like a WHNF that is
  being consumed by the RTS driver.
]

> > This infinite computation produces an infinite output.
> 
> 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).

Indeed, I was assuming that I/O implied a yield, but this assumption
should definitely be made explicit.  I propose that a cooperative
scheduler ought to yield at all primitive I/O actions, where primitive
means things like hPutChar, or takeMVar, which are implemented at a
lower level than Haskell.

> 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 wasn't originally aware that Hugs scheduler only yields on MVar
operations.  That seems too restrictive.  I believe the "all I/O
primitives" rule would guarantee progress in the absence of _|_.
Unless you can think of another counter-example?

Regards,
    Malcolm