preemptive vs cooperative: attempt at formalization

[David Roundy]

On Wed, Apr 12, 2006 at 05:50:40PM +0100, Malcolm Wallace wrote:
> 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.

I understood John's criterion in terms of a limiting case that can be
exactly specified regarding latency.  As I see it, the point of preemptive
systems is to have a lower latency than cooperative systems, and this is
also what distinguishes the two.  But the trouble is that preemptive
systems can't have a fixed latency guarantee, and shouldn't be expected to.
So he's pointing out that at a minimum, a preemptive system should always
have a latency less than infinity, while a cooperative system always *can*
have an infinite latency.  While you're right that the limiting case is bad
code, the point isn't to handle that case well, the point is to emphasize
the close-to-limiting case, when a pure function might run for longer than
your desired latency.  His spec does this in a rigorous, but achievable
manner (i.e. a useful spec).
-- 
David Roundy
http://www.darcs.net