Re: memory ordering
Hi Edward, Thanks very much for this reply, it answers a lot of questions I'd had. I'd hoped that ordering would be preserved through C--, but c'est la vie. Optimizing compilers are ever the bane of concurrent algorithms! stg/SMP.h does define a loadLoadBarrier, which is exposed in Ryan Newton's atomic-primops package. From the docs, I think that's a general read barrier, and should do what I want. Assuming it works properly, of course. If I'm lucky it might even be optimized out. Thanks, John On Mon, Dec 30, 2013 at 6:04 AM, Edward Z. Yang wrote: > Hello John, > > Here are some prior discussions (which I will attempt to summarize > below): > > http://www.haskell.org/pipermail/haskell-cafe/2011-May/091878.html > http://www.haskell.org/pipermail/haskell-prime/2006-April/001237.html > http://www.haskell.org/pipermail/haskell-prime/2006-March/001079.html > > The guarantees that Haskell and GHC give in this area are hand-wavy at > best; at the moment, I don't think Haskell or GHC have a formal memory > model—this seems to be an open research problem. (Unfortunately, AFAICT > all the researchers working on relaxed memory models have their hands > full with things like C++ :-) > > If you want to go ahead and build something that /just/ works for a > /specific version/ of GHC, you will need to answer this question > separately for every phase of the compiler. For Core and STG, monads > will preserve ordering, so there is no trouble. However, for C--, we > will almost certainly apply optimizations which reorder reads (look at > CmmSink.hs). To properly support your algorithm, you will have to add > some new read barrier mach-ops, and teach the optimizer to respect them. > (This could be fiendishly subtle; it might be better to give C-- a > memory model first.) These mach-ops would then translate into > appropriate arch-specific assembly or LLVM instructions, preserving > the guarantees further. > > This is not related to your original question, but the situation is a > bit better with regards to reordering stores: we have a WriteBarrier > MachOp, which in principle, prevents store reordering. In practice, we > don't seem to actually have any C-- optimizations that reorder stores. > So, at least you can assume these will work OK! > > Hope this helps (and is not too inaccurate), > Edward > > Excerpts from John Lato's message of 2013-12-20 09:36:11 +0800: > > Hello, > > > > I'm working on a lock-free algorithm that's meant to be used in a > > concurrent setting, and I've run into a possible issue. > > > > The crux of the matter is that a particular function needs to perform the > > following: > > > > > x <- MVector.read vec ix > > > position <- readIORef posRef > > > > and the algorithm is only safe if these two reads are not reordered (both > > the vector and IORef are written to by other threads). > > > > My concern is, according to standard Haskell semantics this should be > safe, > > as IO sequencing should guarantee that the reads happen in-order. Of > > course this also relies upon the architecture's memory model, but x86 > also > > guarantees that reads happen in order. However doubts remain; I do not > > have confidence that the code generator will handle this properly. In > > particular, LLVM may freely re-order loads of NotAtomic and Unordered > > values. > > > > The one hope I have is that ghc will preserve IO semantics through the > > entire pipeline. This seems like it would be necessary for proper > handling > > of exceptions, for example. So, can anyone tell me if my worries are > > unfounded, or if there's any way to ensure the behavior I want? I could > > change the readIORef to an atomicModifyIORef, which should issue an > mfence, > > but that seems a bit heavy-handed as just a read fence would be > sufficient > > (although even that seems more than necessary). > > > > Thanks, > > John L. > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Decomposition of given equalities
On Mon, Dec 30, 2013 at 7:00 PM, Simon Peyton-Jones wrote: > | given `(f a ~ g b)` there's no possible way that `a` and `b`, resp. `f` > | and `g` might have different kinds (how could you ever have constructed > | `f a ~ g b` if they did?) > > Wait. It's quite possible for them to have different kinds. E.g. > > f :: (* -> *) -> * > a :: (* -> *) > g :: * -> * > b :: * > > Then (f a :: *) and (g b :: *), and it'd be quite reasonable to > form the equality (f a ~ g b). > Yes, it's quite possible, given f, a, g, and b of different kinds, to make `f a` and `g b` have the same *kind*. But how could they ever be the same type? Is it not the case that (f a ~ g b) iff (f ~ g) and (a ~ b) (obviously impossible if those are of different kinds)? You would have to worry about this possibility if type constructor variables weren't injective, but they are. > > Simon > > | -Original Message- > | From: Glasgow-haskell-users [mailto:glasgow-haskell-users- > | boun...@haskell.org] On Behalf Of Gábor Lehel > | Sent: 19 December 2013 16:12 > | To: Richard Eisenberg > | Cc: glasgow-haskell-users@haskell.org > | Subject: Re: Decomposition of given equalities > | > | Does this boil down to the fact that GHC doesn't have kind GADTs? I.e. > | given `(f a ~ g b)` there's no possible way that `a` and `b`, resp. `f` > | and `g` might have different kinds (how could you ever have constructed > | `f a ~ g b` if they did?), but GHC isn't equipped to reason about that > | (to store evidence for it and retrieve it later)? > | > | On Thu, Dec 19, 2013 at 4:01 PM, Richard Eisenberg > | wrote: > | > Let me revise slightly. GHC wouldn't guess that f3 would be f just > | because f is the only well-kinded thing in sight. > | > > | > Instead, it would use (f2 i ~ a) to reduce the target equality, (f3 i2 > | ~ a), to (f3 i2 ~ f2 i). It would then try to break this down into (f3 ~ > | f2) and (i2 ~ i). Here is where the kind problem comes in -- these > | equalities are ill-kinded. So, GHC (rightly, in my view) rejects this > | code, and reports an appropriate error message. Of course, more context > | in the error message might be an improvement, but I don't think the > | current message is wrong. > | > > | > As for Thijs's comment about lack of decomposition in GHC 7.6.3: > | You're right, that code fails in GHC 7.6.3 because of an attempt > | (present in GHC 7.6.x) to redesign the Core type system to allow for > | unsaturated type families (at least in Core, if not in Haskell). There > | were a few cases that came up that the redesign couldn't handle, like > | Thijs's. So, the redesign was abandoned. In GHC HEAD, Thijs's code works > | just fine. > | > > | > (The redesign was to get rid of the "left" and "right" coercions, > | > which allow decomposition of things like (f a ~ g b), in favor of an > | > "nth" coercion, which allows decomposition of things like (T a ~ T > | > b).) > | > > | > Good -- I feel much better about this answer, where there's no guess > | for the value of f3! > | > > | > Richard > | > > | > On Dec 18, 2013, at 11:30 PM, Richard Eisenberg wrote: > | > > | >> I'd say GHC has it right in this case. > | >> > | >> (f a ~ g b) exactly implies (f ~ g) and (a ~ b) if and only if the > | >> kinds match up. If, say, (f :: k1 -> *), (g :: k2 -> *), (a :: k1), > | >> and (b :: k2), then (f ~ g) and (a ~ b) are ill-kinded. In Gabor's > | >> initial problem, we have (with all type, kind, and coercion variables > | >> made explicit) > | >> > | >>> data InnerEq (j :: BOX) (k :: BOX) (i :: j) (a :: k) where InnerEq > | >>> :: forall (f :: j -> k). f i ~ a => InnerEq j k i a > | >>> > | >>> class TypeCompare (k :: BOX) (t :: k -> *) where maybeInnerEq :: > | >>> forall (j :: BOX) (f :: j -> k) (i :: j) (a :: k). > | >>> t (f i) -> t a -> Maybe (InnerEq j k i a) > | >>> > | >>> instance forall (j :: BOX) (k :: BOX) (i :: j). TypeCompare k > | >>> (InnerEq j k i) where maybeInnerEq :: forall (j2 :: BOX) (f :: j2 - > | > k) (i2 :: j2) (a :: k). > | >>> InnerEq j k i (f i2) -> InnerEq j k i a -> Maybe > | >>> (InnerEq j2 k i2 a) maybeInnerEq (InnerEq (f1 :: j -> k) (co1 :: f1 > | i ~ f i2)) > | >>> (InnerEq (f2 :: j -> k) (co2 :: f2 i ~ a)) > | >>>= Just (InnerEq (f3 :: j2 -> k) (co3 :: f3 i2 ~ a)) > | >> > | >> GHC must infer `f3` and `co3`. The only thing of kind `j2 -> k` lying > | >> around is f. So, we choose f3 := f. Now, we need to prove `f i2 ~ a`. > | Using the two equalities we have, we can rewrite this as a need to prove > | `f1 i ~ f2 i`. I can't see a way of doing this. Now, GHC complains that > | it cannot (renaming to my variables) deduce (i ~ i2) from (f1 i ~ f i2). > | But, this is exactly the case where the kinds *don't* match up. So, I > | agree that GHC can't deduce that equality, but I think that, even if it > | could, it wouldn't be able to type-check the whole term unless I've > | made a mistake somewhere. > | >> > | >> I don't see an immediate
RE: Decomposition of given equalities
| given `(f a ~ g b)` there's no possible way that `a` and `b`, resp. `f` | and `g` might have different kinds (how could you ever have constructed | `f a ~ g b` if they did?) Wait. It's quite possible for them to have different kinds. E.g. f :: (* -> *) -> * a :: (* -> *) g :: * -> * b :: * Then (f a :: *) and (g b :: *), and it'd be quite reasonable to form the equality (f a ~ g b). Simon | -Original Message- | From: Glasgow-haskell-users [mailto:glasgow-haskell-users- | boun...@haskell.org] On Behalf Of Gábor Lehel | Sent: 19 December 2013 16:12 | To: Richard Eisenberg | Cc: glasgow-haskell-users@haskell.org | Subject: Re: Decomposition of given equalities | | Does this boil down to the fact that GHC doesn't have kind GADTs? I.e. | given `(f a ~ g b)` there's no possible way that `a` and `b`, resp. `f` | and `g` might have different kinds (how could you ever have constructed | `f a ~ g b` if they did?), but GHC isn't equipped to reason about that | (to store evidence for it and retrieve it later)? | | On Thu, Dec 19, 2013 at 4:01 PM, Richard Eisenberg | wrote: | > Let me revise slightly. GHC wouldn't guess that f3 would be f just | because f is the only well-kinded thing in sight. | > | > Instead, it would use (f2 i ~ a) to reduce the target equality, (f3 i2 | ~ a), to (f3 i2 ~ f2 i). It would then try to break this down into (f3 ~ | f2) and (i2 ~ i). Here is where the kind problem comes in -- these | equalities are ill-kinded. So, GHC (rightly, in my view) rejects this | code, and reports an appropriate error message. Of course, more context | in the error message might be an improvement, but I don't think the | current message is wrong. | > | > As for Thijs's comment about lack of decomposition in GHC 7.6.3: | You're right, that code fails in GHC 7.6.3 because of an attempt | (present in GHC 7.6.x) to redesign the Core type system to allow for | unsaturated type families (at least in Core, if not in Haskell). There | were a few cases that came up that the redesign couldn't handle, like | Thijs's. So, the redesign was abandoned. In GHC HEAD, Thijs's code works | just fine. | > | > (The redesign was to get rid of the "left" and "right" coercions, | > which allow decomposition of things like (f a ~ g b), in favor of an | > "nth" coercion, which allows decomposition of things like (T a ~ T | > b).) | > | > Good -- I feel much better about this answer, where there's no guess | for the value of f3! | > | > Richard | > | > On Dec 18, 2013, at 11:30 PM, Richard Eisenberg wrote: | > | >> I'd say GHC has it right in this case. | >> | >> (f a ~ g b) exactly implies (f ~ g) and (a ~ b) if and only if the | >> kinds match up. If, say, (f :: k1 -> *), (g :: k2 -> *), (a :: k1), | >> and (b :: k2), then (f ~ g) and (a ~ b) are ill-kinded. In Gabor's | >> initial problem, we have (with all type, kind, and coercion variables | >> made explicit) | >> | >>> data InnerEq (j :: BOX) (k :: BOX) (i :: j) (a :: k) where InnerEq | >>> :: forall (f :: j -> k). f i ~ a => InnerEq j k i a | >>> | >>> class TypeCompare (k :: BOX) (t :: k -> *) where maybeInnerEq :: | >>> forall (j :: BOX) (f :: j -> k) (i :: j) (a :: k). | >>> t (f i) -> t a -> Maybe (InnerEq j k i a) | >>> | >>> instance forall (j :: BOX) (k :: BOX) (i :: j). TypeCompare k | >>> (InnerEq j k i) where maybeInnerEq :: forall (j2 :: BOX) (f :: j2 - | > k) (i2 :: j2) (a :: k). | >>> InnerEq j k i (f i2) -> InnerEq j k i a -> Maybe | >>> (InnerEq j2 k i2 a) maybeInnerEq (InnerEq (f1 :: j -> k) (co1 :: f1 | i ~ f i2)) | >>> (InnerEq (f2 :: j -> k) (co2 :: f2 i ~ a)) | >>>= Just (InnerEq (f3 :: j2 -> k) (co3 :: f3 i2 ~ a)) | >> | >> GHC must infer `f3` and `co3`. The only thing of kind `j2 -> k` lying | >> around is f. So, we choose f3 := f. Now, we need to prove `f i2 ~ a`. | Using the two equalities we have, we can rewrite this as a need to prove | `f1 i ~ f2 i`. I can't see a way of doing this. Now, GHC complains that | it cannot (renaming to my variables) deduce (i ~ i2) from (f1 i ~ f i2). | But, this is exactly the case where the kinds *don't* match up. So, I | agree that GHC can't deduce that equality, but I think that, even if it | could, it wouldn't be able to type-check the whole term unless I've | made a mistake somewhere. | >> | >> I don't see an immediate way to fix the problem, but I haven't | thought much about it. | >> | >> Does this help? Does anyone see a mistake in what I've done? | >> | >> Richard | >> | >> On Dec 18, 2013, at 6:38 PM, Gábor Lehel | wrote: | >> | >>> Hello, | >>> | >>> The upcoming GHC 7.8 recently gave me this error: | >>> | >>> Could not deduce (i ~ i1) | >>> from the context (f1 i ~ f i1) | >>> | >>> Which is strange to me: shouldn't (f1 i ~ f i1) exactly imply (f1 ~ | >>> f, i ~ i1)? (Or with nicer variable names: (f a ~ g b) => (f ~ g, a | >>> ~ | >>> b)?) | >>> | >>> When I inquired about this in #haskell on IRC, a person going by the | >>>
Re: memory ordering
Hello John, Here are some prior discussions (which I will attempt to summarize below): http://www.haskell.org/pipermail/haskell-cafe/2011-May/091878.html http://www.haskell.org/pipermail/haskell-prime/2006-April/001237.html http://www.haskell.org/pipermail/haskell-prime/2006-March/001079.html The guarantees that Haskell and GHC give in this area are hand-wavy at best; at the moment, I don't think Haskell or GHC have a formal memory model—this seems to be an open research problem. (Unfortunately, AFAICT all the researchers working on relaxed memory models have their hands full with things like C++ :-) If you want to go ahead and build something that /just/ works for a /specific version/ of GHC, you will need to answer this question separately for every phase of the compiler. For Core and STG, monads will preserve ordering, so there is no trouble. However, for C--, we will almost certainly apply optimizations which reorder reads (look at CmmSink.hs). To properly support your algorithm, you will have to add some new read barrier mach-ops, and teach the optimizer to respect them. (This could be fiendishly subtle; it might be better to give C-- a memory model first.) These mach-ops would then translate into appropriate arch-specific assembly or LLVM instructions, preserving the guarantees further. This is not related to your original question, but the situation is a bit better with regards to reordering stores: we have a WriteBarrier MachOp, which in principle, prevents store reordering. In practice, we don't seem to actually have any C-- optimizations that reorder stores. So, at least you can assume these will work OK! Hope this helps (and is not too inaccurate), Edward Excerpts from John Lato's message of 2013-12-20 09:36:11 +0800: > Hello, > > I'm working on a lock-free algorithm that's meant to be used in a > concurrent setting, and I've run into a possible issue. > > The crux of the matter is that a particular function needs to perform the > following: > > > x <- MVector.read vec ix > > position <- readIORef posRef > > and the algorithm is only safe if these two reads are not reordered (both > the vector and IORef are written to by other threads). > > My concern is, according to standard Haskell semantics this should be safe, > as IO sequencing should guarantee that the reads happen in-order. Of > course this also relies upon the architecture's memory model, but x86 also > guarantees that reads happen in order. However doubts remain; I do not > have confidence that the code generator will handle this properly. In > particular, LLVM may freely re-order loads of NotAtomic and Unordered > values. > > The one hope I have is that ghc will preserve IO semantics through the > entire pipeline. This seems like it would be necessary for proper handling > of exceptions, for example. So, can anyone tell me if my worries are > unfounded, or if there's any way to ensure the behavior I want? I could > change the readIORef to an atomicModifyIORef, which should issue an mfence, > but that seems a bit heavy-handed as just a read fence would be sufficient > (although even that seems more than necessary). > > Thanks, > John L. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
