MVar semantics: proposal
jmaessen at alum.mit.edu
Fri Mar 31 12:49:27 EST 2006
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
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
* 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.
More information about the Haskell-prime