MVar semantics: proposal
jmaessen at alum.mit.edu
Tue Apr 11 18:58:37 EDT 2006
Sorry for the long delay in responding to this message---this issue
takes all the brain cells I've got in one go.
Ordinarily I'd trim the forgoing discussion, but it was rusty enough
that I've retained it:
On Apr 4, 2006, at 7:12 AM, Simon Marlow wrote:
> Jan-Willem - thanks for your thoughts on this, it's greatly
> On 31 March 2006 18:49, Jan-Willem Maessen wrote:
>> John -
>> You are, in effect, proposing a memory model for MVars and IORefs.
>> The high-level model for programmers is "In order to communicate data
>> between threads, you *must* use an MVar, and never an IORef."
>> But the devil is in the details. I'd like to strongly urge *against*
>> adopting the extremely loose model you have proposed. The following
>> things seem particularly important:
>> * reads and writes to IORefs should be atomic, meaning either a
>> complete update is observed or no change is observed. In the absence
>> of this guarantee, misuse of IORefs can cause programs to crash in
>> unrepeatable ways. If the machine doesn't make this easy, the
>> implementor ought to sweat a little so that Haskell programmers don't
>> have to sweat at all.
>> * I assume forkIO constitutes a sequence point. I suspect throwTo et
>> al ought to as well.
>> * I would urge that atomicModifyIORef constitute a sequence point---I
>> suspect it loses a great deal of its utility otherwise.
>> Now, on to more difficult issues... Consider the following example
>> data RefList a = Nil | Cons a (IORef (RefList a))
>> cons :: a -> RefList a -> IO (RefList a)
>> cons x xs = do
>> a <- newIORef xs
>> return (Cons x a)
>> hd :: RefList a -> a
>> hd (Cons a _) = a
>> tl :: RefList a -> IO (RefList a)
>> tl (Cons a t) = readIORef a
>> setTl :: RefList a -> RefList a -> IO ()
>> setTl (Cons a t) t' = writeIORef t t'
>> main = do a <- cons 'a' Nil
>> forkIO $ do
>> c <- cons 'c' Nil
>> b <- cons 'b' Nil
>> setTl b c
>> setTl a b
>> at <- tl a
>> case at of
>> Nil -> return ()
>> Cons _ _ -> do
>> putChar (hd at)
>> att <- tl at
>> This program is, by your informal model, buggy. The question is
>> this: how badly wrong is it?
>> Let's say at happens to read b. Is (hd at) well defined? That's
>> assuming very strong consistency from the memory system already. How
>> about the IORef in at? Is that fully allocated, and properly
>> initialized? Again, if it is, that implies some pretty strong
>> consistency from the memory system.
>> Now, what about att? By your argument, it may or may not be c. We
>> can ask the same questions about its contents assuming it happens to
>> be c.
>> People have talked a lot about weakly-ordered NUMA machines for more
>> than a decade, and they're always just a couple of years away. In
>> practical terms, non-atomic NUMA memory models tend to be so hard to
>> program that these machines have never found any traction---you need
>> to throw away all of your software, including your OS, and start
>> afresh with programmers that are vastly more skilled than the ones
>> who wrote the stuff you've already got.
>> My feeling is that the purely-functional portion of the Haskell
>> language already makes pretty stringent demands of memory
> This is true - in GHC we are required to add a memory barrier to thunk
> update on architectures that don't have strong memory ordering,
> just to
> ensure that when you follow the pointer in an indirection you can
> actually see the value at the end of the pointer.
> Since x86 & x86_64 can implement strong memory ordering without
> (seemingly) too much overhead, surely adding the barrier
> instruction for
> other architectures shouldn't impose too much of a penalty, at
> least in
Interesting question. The currently-popular architectures can get by
without too many memory barriers, in large part by requiring stores
to commit to memory in order; my belief is that SPARC TSO can get by
with no memory barriers for thunk update/read, and that PowerPC
requires a write barrier (and perhaps read barriers).
It remains to be seen whether multi-core pipelines will change this
equation; there are reasons an architect might prefer to use a single
store pipeline for multiple threads, satisfying loads from one thread
from pending stores for another thread. The practical upshot would
be weaker memory models all around.
Sadly, x86 has a bad record of bungling synchronization operations,
and clear documentation on the x86 memory model is conspicuous by its
>> In light of those demands, and the fact that mutable
>> state is used in pretty tightly-controlled ways, it's worth
>> considering much stronger memory models than the one you propose.
>> I'd even go so far as to say "IORefs and IOArrays are sequentially
> Certainly possible; again on x86 & x86_64 it's a no-op, on other
> architectures it means adding a barrier to writeIORef. In GHC we're
> already doing a write barrier (of the generational GC kind, not the
> microprocessor kind) in writeIORef anyway.
It is certainly my hope that the memory barriers required by
writeIORef and company will be no worse than those required by thunk
update---ie, writeIORef should cost about as much as updating the
header word of a thunk.
>> The only argument against this behavior is their use in
>> the internals of arrays, file I/O, the FFI, etc., etc. (though really
>> it's all about IOUArrays in the latter cases) where we might
>> conceivably pay a bundle in performance.
>> Another possibility is an algebraic model based on commuting IO
>> actions. That approach is a particular bias of mine, having tangled
>> with these issues extensively in the past. It'd go something like
>> this: * Any data written to an IORef can safely be read by another
>> thread; we cannot observe
>> partially-written objects.
>> * readIORef commutes with readIORef.
>> * newIORef commutes with newIORef.
>> * writeIORef and newIORef commute with writeIORef or readIORef to
>> a different IORef.
>> * Nothing commutes with readMVar, writeMVar, or atomicModifyIORef.
>> * Nothing before a forkIO can be commuted to after forkIO.
> Does this model mean anything to the runtime, or would it just affect
> compile-time optimisations?
On weakly ordered machines, it tells us where we must insert memory
barriers, and what sort of memory barriers are required. In
practice, the easiest expedient is to bake those barriers in to
either the read or write operations. On some machines, these
operations are no-ops and get erased. On others, one can use
commutativity to hoist barriers, then take advantage of the fact that:
barrier >> barrier === barrier
> I imagine that, since the runtime still has to use barriers to prevent
> partially-written objects from being visible to other threads, in
> the runtime would end up providing full serialisation anyway. But my
> tiny brain hasn't quite the capacity to think this through completely
> right now, I'm hoping someone else has.
That is my belief as well. But the synchronization may not be as
"full" as you imagine---a good thing for the implementor, but a
potentially surprising thing for the programmer.
My particular concern here is actually array construction.
Conceptually, we'd like to avoid a barrier operation every time we
write a pointer into an IOArray or an STArray (the barrier ensures
that the data being stored in the array is properly formatted in
memory before the update occurs). I suspect this can be avoided, but
it's tricky to come up with a graceful way to guarantee it in
general. In the worst case, this would make constructing any kind of
array slow and clunky. That's an eventuality to think about, and
avoid. It might mean re-coding bulk updates to use something more
primitive (and unsafe) than writeIOArray / writeSTArray.
>> I think it's a Good Idea to choose a model that is conceptually
>> simple now, at the cost of imposing a few constraints on
>> implementors, rather than a complex specification which permits
>> maximum implementation flexibility but is utterly opaque.
> I don't have a strong opinion, since as I said earlier the constraints
> aren't that onerous in practice.
> However, I don't completely understand why the more flexible model
> be "complex" and "opaque". Isn't it just a case of specifying certain
> interactions as resulting in undefined behaviour? Or do you think
> too hard to specify exactly which interactions are undefined?
My assumption here is that bad synchronization should not cause
Haskell to crash with a seg fault (because we looked at something in
a partially-formed state). Getting a loose spec which still
guarantees this is tricky in practice. The other tricky part is
explaining to programmers why their code went wrong in some
unintuitive way. Here, saying "use MVars / STRefs to synchronize"
should go a long way.
More information about the Haskell-prime