
On Sat, May 30, 2009 at 5:37 PM, Bertram Felgenhauer
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