[Haskell-cafe] readMVar and the devils

[Conor T McBride]

Hi folks

I had a bit more of a play over the weekend. Got addicted.

Lumps of code further on down.

Jan-Willem Maessen wrote:
 >If you're really using MVars in write-once read-many style, the
 >semantics of readMVar shouldn't be a problem:
 >
 >* Before the initializing write, all calls to readMVar block.
 >* The initializing take fills the MVar and unblocks all the blocked
 >readers.
 >* Subsequent calls to readMVar should be able to complete gracefully,
 >though calls to readMVar will block temporarily if another call to
 >readMVar gets de-scheduled between the take and the put.
 >
 >If you're not doing this, what are you *actually* trying to do?  With
 >multiple writers, of course things get more complicated, but you should
 >be able to organize your code into take...put pairs or calls to 
 >withMVar as Andy Moran suggested.

OK, the idea is that there are registers or `holes'

type Hole x = -- a hole which should eventually contain an x

There are various producers trying to cook up a value for the hole.
If more than one makes an attempt to fill it, exactly one should
succeed.

There are various consumers who need the hole to be filled. These
should block until the value shows up, then read the value, leaving
it for other consumers.

The crux of the problem is this. Suppose I have producers X and Y
and consumers M and N. Say producer X wins the race; consumer M
temporarily empties the hole in order to read the value, intending to
put it back so that N can read it too; producer Y has only just woken
up and seizes the opportunity to sneak in his solution whilst M is
borrowing X's. The value changes; M blocks; it's a disaster!

If you just try to represent a Hole x as a single MVar x, then the
problem is exactly as I sent before

On 02 July 2004 10:16, I wrote:
> 
>>   do x <- takeMVar myMVar      -- (A)
>>      putMVar myMVar x          -- (B)
>>      return x

That's M. This is Y.

>>and another executing
>>
>>   putMVar myMVar y             -- (C)
>>
>>(1) Is it possible that an evil scheduler will execute (A) then (C)
>>       and block on (B)?

Simon Marlow wrote:
> Yes.  In fact, you don't need an evil scheduler, an ordinary scheduler
> will do this :-)

My operating hypothesis is that even ordinary schedulers are evil...

>>(2) Is it the case that if myMVar is nonempty and readMVar is chosen
>>       for execution, that readMVar myMVar takes the value
>>       from myMVar, guaranteed that the _same_ value will be put
>>       back immediately, and also returned?
> 
> Only if there are no other threads executing putMVar on myMVar
> concurrently.

So it's not what I need...

> readMVar is only atomic with respect to other well-behaved threads; that
> is, other threads doing strictly take-followed-by-put operations.

...because I have lots of bad behaviour about. Well, incompatible
behaviour anyway. The important thing is that information only
increases: what's true of an unknown should still be true of any
candidate value for that unknown; but there's no guarantee that
what's true of one candidate will be true of another.

>>I guess I could use some kind of extra semaphore MVar to ensure that
>>the reader has the lock on the program MVar, but that's more like
>>hard work. Is readMVar what I want?
> 
> It sounds like you want a different abstraction, but one that can almost
> certainly be built using MVars.  I'm not sure exactly what it is you
> need, but if you provide the signatures of the operations then I could
> probably sketch an implementation.

OK, here's what I want, what I do with it, and my attempt to deliver it.
But I'm not an expert, so please let me know if there's some disastrous
flaw...

The signature/spec:

type Hole x

hole :: IO (Hole x)
   -- returns a fresh empty hole for an x
askHole :: Hole x -> IO (Maybe x)
   -- inspects the current contents (or none) of the hole; mustn't
   -- block
tellHole :: Hole x -> x -> IO (Maybe x)
   -- tries to write the hole, returns what was previously there;
   -- if the hole was empty, the value supplied is installed
   -- if the hole was full, it's unchanged (too late, pal!);
   -- mustn't block
readHole :: Hole x -> IO x
   -- blocks until the hole has been filled, then returns its
   -- value
instance Eq (Hole x)
   -- a kind of higher-level `pointer equality'

Crucially, we have no way of telling the number of askers, tellers
or readers of the hole.

We can use this to model nondeterministic computation, like this:

newtype Fox x = Fox {unFox :: Hole x -> IO ()}

A Fox is a computation which can (perhaps) fill a given hole. Foxes
run in their own thread, like this:

infix 5 <==

(<==) :: Hole x -> Fox x -> IO ()
h <== Fox f = do
   forkIO (f h)
   return ()

You can fork off a fresh fox and grab its output hole like this:

foxhole :: Fox x -> IO (Hole x)
foxhole f = do
   h <- hole
   h <== f
   return h

Or you can run a fox in private, hiding its hole from everyone else
and waiting for its value like this:

fox :: Fox x -> IO x
fox f = do
   h <- foxhole f
   readHole h

And you saw this coming, right? A nondeterministic
programming monad.

instance Monad Fox where
   return x = Fox $ \ hx -> do
     tellHole hx x
     return ()
   fs >>= g = Fox $ \ ht -> do
     s <- fox fs
     ht <== g s
   fail _ = Fox $ \ _ -> return ()

instance MonadPlus Fox where
   mzero = Fox $ \ _ -> return ()
   mplus f g = Fox $ \ h -> do
     h <== f
     h <== g
     return ()

OK, that's where we're going. Here's my attempt.

data Hole x = Hole (MVar x) (MVar ()) (MVar ())
                 --  value   semaphore  trigger

The semaphore is used to read the value safely.
The trigger is used to announce the filling of the
hole. Nobody's allowed to grab the semaphore if
they're going to do anything which might block.

instance Eq (Hole x) where
   Hole v1 _ _ == Hole v2 _ _ = v1 == v2

hole :: IO (Hole x)
hole = return Hole `ap` newEmptyMVar
                    `ap` newMVar ())  -- sem is ready
                    `ap` newEmptyMVar

askHole :: Hole x -> IO (Maybe x)
askHole (Hole val sem _) = do
   takeMVar sem           -- lock out tellers
   mx <- tryTakeMVar val  -- sneak a peek
   case mx of             -- restore val
     Nothing -> return ()
     Just x -> putMVar val x
   putMVar sem ()         -- release the lock
   return mx

tellHole :: Hole x -> x -> IO (Maybe x)
tellHole (Hole val sem trig) x = do
   takeMVar sem           -- wait my turn
   mx <- tryTakeMVar val  -- sneak a peek
   case mx of
     Nothing -> do        -- I win!
       putMVar val x
       putMVar trig ()    -- tell the world!
       putMVar sem ()
       return Nothing
     Just x' -> do        -- rats!
       putMVar val x'     -- be a good citizen
       putMVar sem ()     -- and put it back
       return (Just x')   -- accept defeat

readHole :: Hole x -> IO x
readHole (Hole val sem trig) = do
   takeMVar trig  -- block on the trigger
   takeMVar sem   -- lock out the tellers
   x <- takeMVar val  -- photocopy it
   putMVar val x      -- put it back
   putMVar trig ()    -- resend the trigger
   putMVar sem ()     -- release the lock
   return x


Does this seem robust? I've had lots of fun with it in ghci.

However, my attempt to write a concurrent unification algorithm
has uncovered a subtle problem: the occur check isn't stable
under substitution. I have two threads unifying

   (1) x with y
   (2) y with x -> x

If each thread does an occur check, then a tell, there's the
possibility that the two checks will happen before the two
tells. And it's ok to do either tell. Just not both.

Hmmm...

Thanks again

Conor