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 13 April 2006 11:41, Malcolm Wallace wrote: > "Simon Marlow" <[EMAIL PROTECTED]> 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? "print ones" always has the value "print ones", i.e. it's already in WHNF(*). You could additionally give a semantics for running IO actions that includes a concept of _|_ (see my other message), but we shouldn't confuse this with the pure denotational semantics of Haskell. Cheers, Simon (*) if print is an IO primitive, that is. In practice it probably evaluates to "hPutStr stdout (show ones)". ___ 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
"Simon Marlow" <[EMAIL PROTECTED]> 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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: preemptive vs cooperative: attempt at formalization
On Thu, Apr 13, 2006 at 02:53:01AM -0700, John Meacham wrote: > this is a non-productive non-cooperative loop, as in _|_. since IORefs I mean this is a non-productive non-terminating loop, as in _|_. since IORefs 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
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 _|_. since IORefs can't be shared unless protected by an MVar there is no way to observe the side effect of this routine. MVar routines since they are potentially blocking (and moreso because we have the MVar fairness guarentee), must be yield points. > 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. it was not my intent to be any stronger, but rather just be a reformulation. 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
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 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
"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 12 April 2006 11:41, Malcolm Wallace wrote: > 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. That's slightly odd terminology. ones = 1:ones is definitely terminating. (length ones) is not, though. > 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, Wow. I wish I knew what that meant :) Maybe you could expand on in what sense you mean non-terminating, and what "productive" means? Is there something we need to worry about here? Cheers, Simon ___ 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
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
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 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
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
> [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. As an example of formalizing fairness, I'd like to point out L. de Alfaro, M. Faella, R. Majumdar, V. Raman. Code Aware Resource Management. In EMSOFT 05: Fifth ACM International Conference on Embedded Software, ACM Press, 2005. http://luca.soe.ucsc.edu/Publications?action=AttachFile&do=get&target=emsoft05.pdf ``To achieve compact, yet fair, managers, we consider win- ning strategies that may be randomized, that is, scheduling decisions may use lotteries over available moves; the strate- gies ensure progress and fairness with probability 1.'' Of a special interest is p5 of the paper: ''Inter-thread nondeterminism. We assume that the underlying operating system scheduler is fair: more precisely, we assume that, if a thread is infinitely often ready to execute, it will make progress infinitely often Intra-thread nondeterminism. Assuming that intrathread nondeterminism is resolved in an arbitrary way may easily lead to declaring the manager synthesis problem to be infeasible. In fact, whenever a thread can execute a loop while holding a resource, the arbitrary resolution of intra-thread nondeterminism introduces the possibility that the loop never terminates. In practice, a reasonable assumption is that intra-thread nondeterminism is resolved in a (strongly) fair fashion: if each choice is presented infinitely often, each choice outcome will follow infinitely often. Such fairness entails loop termination.'' The paper then formalizes these fairness assumptions and the goal of the fair resource manager in temporal logic. Thus the difference between cooperative and preemptive scheduling strategies becomes quite fuzzy: neither strategy guarantees much unless we make some assumptions about threads (e.g., no thread loops while holding a critical resource). But if we do make assumptions about threads, we might as well assume that threads are behaving nicely and yield (or the underlying monad or memory allocator yield on their behalf). ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
