
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