RE: preemptive vs cooperative: attempt at formalization
On 12 April 2006 17:51, Malcolm Wallace wrote: Simon Marlow [EMAIL PROTECTED] 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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
RE: preemptive vs cooperative: attempt at formalization
On 13 April 2006 10:53, John Meacham wrote: On Thu, Apr 13, 2006 at 09:46:03AM +0100, Simon Marlow wrote: 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 this is a non-productive non-cooperative loop, as in _|_. Ok, I'm confused because I'm thinking in terms of operational semantics for IO. Maybe a way to describe this is to give a meaning to an value of type IO as a lazy sequence of yields and effects, with some way of evaluating an IO action in the context of the world state, to get the next yield or effect together with a continuation and the new world state. Running an IO action may give _|_ instead of the next yield or effect; ok. Still, I think the operational semantics interpretation works fine too. Cheers, Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: preemptive vs cooperative: attempt at formalization
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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
RE: preemptive vs cooperative: attempt at formalization
On 11 April 2006 22:24, John Meacham wrote: I'd like to be a bit more formal when it comes to the distinction between cooperative and preemptive implementations of concurrency, here is a first attempt. 1. termination, In a concurrent implementation, a thread performing an infinite loop with no IO or interaction with the outside world can potentially stall switching to another thread forever, in FP, we usually denote an infinite loop by _|_. so I think the first difference would be: [Rule 1] * in a cooperative implementation of threading, any thread with value _|_ may cause the whole program to have value _|_. In a preemtive one, this is not true. I don't know what it means for a thread to have value _|_. A thread is defined by its observable effects, threads don't have values. I am using _|_ in the stronger sense of non-termination, not including things like exceptions which should have a well defined behavior. 2. fairness Assuming no thread has value _|_ now, what can both models guarentee when it comes to fairness? both can guarentee every runnable thread will eventually run with a round-robin type scheduler. What if one of the threads never yields in a cooperative system? Even if it isn't calculating _|_, if it's just endlessly doing some pointless IO? Cheers, Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: preemptive vs cooperative: attempt at formalization
On Wed, Apr 12, 2006 at 10:58:32AM +0100, Simon Marlow wrote: I don't know what it means for a thread to have value _|_. A thread is defined by its observable effects, threads don't have values. sure they do, the value is just usually discarded. cooperative implementations are just the ones that don't have that luxury. :) What if one of the threads never yields in a cooperative system? Even if it isn't calculating _|_, if it's just endlessly doing some pointless IO? All real IO would have to effectively be a potential yield point. This is in practice assumed of any state threading implementation, but perhaps we should make it part of the standard to be sure. by real IO I mean reading/writing file descriptors and other interaction with the real world and not just anything in the IO monad. I don't think we need to do anything like enumerate the yield points or anything (except the 'yield' function of course), meeting the progress guarentee ensures a liberal sprinkling of them throughout the standard libs, in particular on any file descriptor read or write. Of course, if the user really wanted to, they could cheat using something like mmaping a file into memory and writing to that in a tight loop, but hopefully any user doing something like that would be aware of the ramifications. (heck, it would probably lock up the old version of ghc too if the tight loop thread never needed to GC) John -- John Meacham - ⑆repetae.net⑆john⑈ ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: preemptive vs cooperative: attempt at formalization
John Meacham [EMAIL PROTECTED] wrote: In a concurrent implementation, a thread performing an infinite loop with no IO or interaction with the outside world can potentially stall switching to another thread forever, in FP, we usually denote an infinite loop by _|_. so I think the first difference would be: 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. Why? Because ultimately the demand that forces production of the infinite data structure must come from somewhere, and that somewhere must essentially be I/O. (The only alternative consumers are terminating pure (no problem), non-terminating productive pure (so look upward to its demand), or an unproductive non-terminating computation, which brings us full circle.) It is a curious artifact that in certain multi-threaded implementations, a non-terminating non-productive thread does not make the entire system unproductive, but I don't think this is a behaviour anyone would want to rely on. I would say such a program has a bug, and the threaded RTS is just masking it. Regards, Malcolm ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: preemptive vs cooperative: attempt at formalization
Simon Marlow [EMAIL PROTECTED] 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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: preemptive vs cooperative: attempt at formalization
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. Oh, I didn't mean it was necessarily a useful quality to the end programmer, I was actually just trying to make the point you were making that such programs are incorrect and getting the non-termination case over with. So we can get to the fairness discussion without adding caveats like if no thread is in an infinite loop. But I didn't want to just say assuming your program is correct without giving some indication of what that actually means for a program to be correct. In any case, it is something we can point to and say this! this is a difference! whether it is a useful one or not. now for the contrived counter-example :) start two threads, one trying to prove goldbachs conjecture, the other trying to find a refutation. in a preemptive system this will terminate*, in a cooperative system it may not. John * insert goedel incompleteness caveat. -- John Meacham - ⑆repetae.net⑆john⑈ ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: preemptive vs cooperative: attempt at formalization
On 4/11/06, [EMAIL PROTECTED] [EMAIL PROTECTED] wrote: [Rule 1] * in a cooperative implementation of threading, any thread with value _|_ may cause the whole program to have value _|_. In a preemtive one, this is not true. I'm afraid that claim may need qualifications: I was thinking that it might be more useful to express it programatically: if preemptive then fork _|_ return () = () -- Taral [EMAIL PROTECTED] You can't prove anything. -- Gödel's Incompetence Theorem ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: preemptive vs cooperative: attempt at formalization
On Tue, Apr 11, 2006 at 09:05:12PM -0700, [EMAIL PROTECTED] wrote: [Rule 1] * in a cooperative implementation of threading, any thread with value _|_ may cause the whole program to have value _|_. In a preemtive one, this is not true. I'm afraid that claim may need qualifications: 1. if there is only one runnable thread, if it loops in pure code, the whole program loops -- regardless of preemptive/cooperative scheduling. 2. in a system with thread priorities, if the highest priority thread loops (in pure code or otherwise), the whole program loops -- again irrespective of the preemptive/cooperative scheduling. 3. [a variation of 1 or 2]. A thread that loops in a critical section (or holding a mutex on which the other threads wait) loops the whole program -- again, irrespective of preemptive/cooperative scheduling. would the simple qualifier 'if there exists another runnable thread' solve the issues? A thread is not runnable if it is waiting on a resource or can't run due to the priority policy of the scheduler. and it means there is at least one other thread to switch to. perhaps we should just make the ability to implement 'merge' and 'nmerge' the difference. though, defining the behavior of those routines very well could be a harder problem than defining the difference between preemptive and cooperative in the first place. -- John Meacham - ⑆repetae.net⑆john⑈ ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
