MVar semantics: proposal

[Simon Marlow]

Jan-Willem - thanks for your thoughts on this, it's greatly appreciated.

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
> (untested):
> 
> 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
> consistency.

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
theory?

> 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
> consistent".

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.

> 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?

I imagine that, since the runtime still has to use barriers to prevent
partially-written objects from being visible to other threads, in effect
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.

> 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 would
be "complex" and "opaque".  Isn't it just a case of specifying certain
interactions as resulting in undefined behaviour?  Or do you think it's
too hard to specify exactly which interactions are undefined?

Cheers,
	Simon