preemptive vs cooperative: attempt at formalization

[Malcolm Wallace]

"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.  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.

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").

> Maybe you could expand on in what sense you mean non-terminating, and
> what "productive" means?

I'm using "productive" to mean it generates a WHNF in finite time, even
if the full normal form takes infinite time.

> Is there something we need to worry about here?

No, I don't think so.  John was attempting to formalise an observable
difference between scheduling strategies, in much the manner that one
sees the strictness of functions being defined.  I am pointing out that
the situation with threads is not analogous.

    f _|_ == _|_		-- function is strict
    f _|_ /= _|_		-- function is non-strict

If you consider f to be the scheduler, and its arguments to be all
available threads, then

    schedule threads | any (==_|_) threads  ==>  _|_

means we have a cooperative scheduler.  The converse

    schedule threads | any (==_|_) threads  =/=>  _|_

means we have a preemptive scheduler.

The argument John was making is that this is a useful distinguishing
point to tell whether your concurrent implementation is cooperative or
preemptive.  My argument is that, even if you can distinguish them in
this way, it is not a useful distinction to make.  Your program is
simply wrong.  If you have a sequential program whose value is _|_, your
program is bad.  If you execute it in parallel with other programs, that
does not make it any less bad.  One scheduler reveals the wrongness by
hanging, another hides the wrongness by letting other things happen.  So
what?  It would be perverse to say that the preemptive scheduler is
semantically "better" in this situation.

Regards,
    Malcolm