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
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?
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
absence.
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.
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
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.
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
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?
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.
-Jan
Cheers,
Simon
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
