[reactive] Bug fixes in progress

[Svein Ove Aas]

On Sat, May 30, 2009 at 5:37 PM, Bertram Felgenhauer
<bertram.felgenhauer at googlemail.com> wrote:
> Svein Ove Aas wrote:
>> - I've rewritten unamb, fixing all the issues I've managed to find
>>   (relating to nested unamb invocations, mostly) and having it throw a
>>   BothBottom exception if both values are a finite bottom.
>
> Can you name those issues? The old code only handled ThreadKilled
> properly (because this is the most important exception to get right;
> I didn't really give the others much thought.) What other problems
> were there?
>
Ah.. no. I did a bunch of tests, and basically permuted my code into
working - although, in retrospect, I can now reasonably claim it
*ought* to work too, so it's not pure magic.

Problem is, I forgot to write down most of those tests. I did add the
most critical one, namely recursive unamb invocations. The others were
potential race conditions with threads, that in retrospect I'm not
sure ever existed at all.

I'm going to have to take a long, hard look at how this function
really works now.

> I like moving the retry logic to unamb, because IO actions should never
> have to worry about being restarted. Only pure functions that use
> unsafePerformIO will have to worry.
>
I also get the impression that this restart logic should get factored
out into a separate library. Or perhaps we could rename Unamb to
WeirdRTSTricks.

> Isaac's answer is correct. I'll elaborate.
>
That's repeating my current mental model word for word, but it's nice
having it confirmed. :-)
>
> [...]
>> module Data.Unamb
> [...]
>> unamb :: a -> a -> a
>> unamb a b = unsafePerformIO $ do
>>               -- First, check whether one of the values already is evaluated
>>               -- #ifdef this for GHC
>>               a' <- return False --isEvaluated a
>>               b' <- return False --isEvaluated b
>>               case (a',b') of
>>                 (True,_)        -> return a
>>                 (_,True)        -> return b
>>                 otherwise       -> do retry (amb a b)
>>     where retry act = act `catch`
>>                         (\(SomeException e) -> do
>>                              -- The throwTo is apparently needed, to ensure the
>>                              -- exception is thrown to *this* thread.
>>                              -- unsafePerformIO would otherwise restart the
>>                              -- throwIO call when re-invoked.
>> --                              print "abort"
>>                              myid <- myThreadId
>>                              unblock $ throwTo myid e >> retry act)
>
> Would it make sense to do the isEvaluated checks again when retrying?
>
Yes, that's a good idea, once we call it at all. Really, I suppose the
entire unamb call should be inside retry.

> Obscure fact:  throwTo myid e  works even if exceptions are blocked in
> the current thread. (Rationale: throwTo is a blocking operation; if
> it blocks, exceptions can be delivered regardless of 'block' or
> 'unblock') So you could write
>
>  retry act = unblock act `catch` \(SomeException e) -> do
>                  myid <- myThreadId
>                  -- Kill this thread. We need to rethrow the exception
>                  -- as an /asynchronous/ exception to ensure that this
>                  -- computation can be restarted.
>                  throwTo myid e
>                  retry act
>
Hm. So the old code doesn't fail to work due to that particular
(nonexistent) deadlock, then.. I wonder what it was.

>> race a b = block $ do
>>   v <- newEmptyMVar
>>   let f x = forkIO $ putCatch x v
>>   ta <- f a
>>   tb <- f b
>>   let cleanup = killThread ta >> killThread tb
>>       loop 0 = throwIO BothBottom
>>       loop t = do x <- takeMVar v
>>                   case x of Nothing -> loop (t-1)
>>                             Just x' -> return x'
>>   unblock (loop (2 :: Int) `finally` cleanup)
>
> Okay, by signaling finite bottoms with Nothing you avoid having to wait
> for a garbage collection to detect the case of two finite bottoms,
> which would deliver a BlockedOnDeadMVar exception to the 'race' thread
> with the old code.
>
Yep. I'm contemplating embedding the two bottoms inside the exception, too.

-- 
Svein Ove Aas