MVar semantics: proposal

[Jan-Willem Maessen]

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

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.   
Realistically, the machines which are likely to be built will make it  
easy to comply with a strong specification.

-Jan-Willem Maessen