Remove Bool from Throw/ThrowTo/ThrownSTM actions

If the Maybe MaskingState is Just, then the thread survived; if it's
Nothing the thread was killed.

dejafu-tests/lib/Unit/Properties.hs

@@ -376,11 +376,11 @@ genThreadAction = HGen.choice
   , D.CommitIORef <$> genThreadId <*> genIORefId
   , D.STM <$> genSmallList genTAction <*> genSmallList genThreadId
   , D.BlockedSTM <$> genSmallList genTAction
-  , D.ThrownSTM <$> genSmallList genTAction <*> HGen.maybe genMaskingState <*> HGen.bool
+  , D.ThrownSTM <$> genSmallList genTAction <*> HGen.maybe genMaskingState
   , pure D.Catching
   , pure D.PopCatching
-  , D.Throw <$> HGen.maybe genMaskingState <*> HGen.bool
-  , D.ThrowTo <$> genThreadId <*> HGen.maybe genMaskingState <*> HGen.bool
+  , D.Throw <$> HGen.maybe genMaskingState
+  , D.ThrowTo <$> genThreadId <*> HGen.maybe genMaskingState
   , D.BlockedThrowTo <$> genThreadId
   , D.SetMasking <$> HGen.bool <*> genMaskingState
   , D.ResetMasking <$> HGen.bool <*> genMaskingState

dejafu/CHANGELOG.rst

@@ -19,7 +19,7 @@ Changed
 ~~~~~~~
 
 * ``Test.DejaFu.Types.ThreadAction``, ``Throw``, and ``ThrowTo`` now
-  include the resultant masking state.
+  include the resultant masking state, and no bool.
 
 Fixed
 ~~~~~

dejafu/Test/DejaFu/Conc/Internal.hs

@@ -556,7 +556,7 @@ stepThread _ _ _ _ tid (AThrowTo t e c) = synchronised $ \ctx@Context{..} ->
            )
        Nothing -> pure
          (Succeeded ctx { cThreads = threads' }
-         , ThrowTo t Nothing False
+         , ThrowTo t Nothing
          , const (pure ())
          )
 
@@ -632,7 +632,7 @@ stepThread _ _ _ _ tid (ANewInvariant inv c) = \ctx@Context{..} ->
 -- | Handle an exception being thrown from an @AAtom@, @AThrow@, or
 -- @AThrowTo@.
 stepThrow :: (MonadDejaFu n, Exception e)
-  => (Maybe MaskingState -> Bool -> ThreadAction)
+  => (Maybe MaskingState -> ThreadAction)
   -- ^ Action to include in the trace.
   -> ThreadId
   -- ^ The thread receiving the exception.
@@ -642,21 +642,21 @@ stepThrow :: (MonadDejaFu n, Exception e)
   -- ^ The execution context.
   -> n (What n g, ThreadAction, Threads n -> n ())
 stepThrow act tid e ctx@Context{..} = case propagate some tid cThreads of
-    Just (ms, ts') -> pure
+    Just ts' -> pure
       ( Succeeded ctx { cThreads = ts' }
-      , act (checkMask ms tid cThreads) False
+      , act (Just . _masking $ elookup tid ts')
       , const (pure ())
       )
     Nothing
       | tid == initialThread -> pure
         ( Failed (UncaughtException some)
-        , act Nothing True
+        , act Nothing
         , const (pure ())
         )
       | otherwise -> do
           ts' <- kill tid cThreads
           pure ( Succeeded ctx { cThreads = ts' }
-               , act Nothing True
+               , act Nothing
                , const (pure ())
                )
   where

dejafu/Test/DejaFu/Conc/Internal/Threading.hs

@@ -74,11 +74,11 @@ data Handler n = forall e. Exception e => Handler MaskingState (e -> Action n)
 
 -- | Propagate an exception upwards, finding the closest handler
 -- which can deal with it.
-propagate :: HasCallStack => SomeException -> ThreadId -> Threads n -> Maybe (MaskingState, Threads n)
+propagate :: HasCallStack => SomeException -> ThreadId -> Threads n -> Maybe (Threads n)
 propagate e tid threads = raise <$> propagate' handlers where
   handlers = _handlers (elookup tid threads)
 
-  raise (ms, act, hs) = (ms, except ms act hs tid threads)
+  raise (ms, act, hs) = except ms act hs tid threads
 
   propagate' [] = Nothing
   propagate' (Handler ms h:hs) = maybe (propagate' hs) (\act -> Just (ms, act, hs)) $ h <$> fromException e
@@ -114,13 +114,6 @@ except ms act hs = eadjust $ \thread -> thread
 mask :: HasCallStack => MaskingState -> ThreadId -> Threads n -> Threads n
 mask ms = eadjust $ \thread -> thread { _masking = ms }
 
--- | Check the masking state of a thread, returning @Nothing@ if it
--- matches the given one.
-checkMask :: HasCallStack => MaskingState -> ThreadId -> Threads n -> Maybe MaskingState
-checkMask ms tid threads =
-  let ms0 = M.findWithDefault Unmasked tid (_masking <$> threads)
-  in if ms0 == ms then Nothing else Just ms0
-
 --------------------------------------------------------------------------------
 -- * Manipulating threads
 

dejafu/Test/DejaFu/Internal.hs

@@ -136,7 +136,7 @@ tvarsOf act = tvarsRead act `S.union` tvarsWritten act
 tvarsWritten :: ThreadAction -> Set TVarId
 tvarsWritten act = S.fromList $ case act of
   STM trc _ -> concatMap tvarsOf' trc
-  ThrownSTM trc _ _ -> concatMap tvarsOf' trc
+  ThrownSTM trc _ -> concatMap tvarsOf' trc
   BlockedSTM trc -> concatMap tvarsOf' trc
   _ -> []
 
@@ -151,7 +151,7 @@ tvarsWritten act = S.fromList $ case act of
 tvarsRead :: ThreadAction -> Set TVarId
 tvarsRead act = S.fromList $ case act of
   STM trc _ -> concatMap tvarsOf' trc
-  ThrownSTM trc _ _ -> concatMap tvarsOf' trc
+  ThrownSTM trc _ -> concatMap tvarsOf' trc
   BlockedSTM trc -> concatMap tvarsOf' trc
   _ -> []
 
@@ -192,12 +192,12 @@ rewind (WriteIORef c) = WillWriteIORef c
 rewind (CasIORef c _) = WillCasIORef c
 rewind (CommitIORef t c) = WillCommitIORef t c
 rewind (STM _ _) = WillSTM
-rewind (ThrownSTM _ _ _) = WillSTM
+rewind (ThrownSTM _ _) = WillSTM
 rewind (BlockedSTM _) = WillSTM
 rewind Catching = WillCatching
 rewind PopCatching = WillPopCatching
-rewind (Throw _ _) = WillThrow
-rewind (ThrowTo t _ _) = WillThrowTo t
+rewind (Throw _) = WillThrow
+rewind (ThrowTo t _) = WillThrowTo t
 rewind (BlockedThrowTo t) = WillThrowTo t
 rewind (SetMasking b m) = WillSetMasking b m
 rewind (ResetMasking b m) = WillResetMasking b m
@@ -299,7 +299,7 @@ tidsOf (TakeMVar _ tids) = S.fromList tids
 tidsOf (TryTakeMVar _ _ tids) = S.fromList tids
 tidsOf (CommitIORef tid _) = S.singleton tid
 tidsOf (STM _ tids) = S.fromList tids
-tidsOf (ThrowTo tid _ _) = S.singleton tid
+tidsOf (ThrowTo tid _) = S.singleton tid
 tidsOf (BlockedThrowTo tid) = S.singleton tid
 tidsOf _ = S.empty
 
@@ -377,12 +377,12 @@ updateMaskState tid (Fork tid2) = \masks -> case M.lookup tid masks of
   Nothing -> masks
 updateMaskState tid (SetMasking   _ ms) = M.insert tid ms
 updateMaskState tid (ResetMasking _ ms) = M.insert tid ms
-updateMaskState tid (Throw _ True) = M.delete tid
-updateMaskState tid (Throw (Just ms) _) = M.insert tid ms
-updateMaskState tid (ThrownSTM _ _ True) = M.delete tid
-updateMaskState tid (ThrownSTM _ (Just ms) _) = M.insert tid ms
-updateMaskState _ (ThrowTo tid _ True) = M.delete tid
-updateMaskState _ (ThrowTo tid (Just ms) _) = M.insert tid ms
+updateMaskState tid (Throw Nothing) = M.delete tid
+updateMaskState tid (Throw (Just ms)) = M.insert tid ms
+updateMaskState tid (ThrownSTM _ Nothing) = M.delete tid
+updateMaskState tid (ThrownSTM _ (Just ms)) = M.insert tid ms
+updateMaskState _ (ThrowTo tid Nothing) = M.delete tid
+updateMaskState _ (ThrowTo tid (Just ms)) = M.insert tid ms
 updateMaskState tid Stop = M.delete tid
 updateMaskState _ _ = id
 

dejafu/Test/DejaFu/SCT/Internal.hs

@@ -399,8 +399,8 @@ renumber memtype tid0 crid0 = snd . mapAccumL go (I.empty, tid0, I.empty, crid0)
     (s, CasIORef (renumbered cridmap old) b)
   updateAction s@(tidmap, _, _, _) (STM tas olds) =
     (s, STM tas (map (renumbered tidmap) olds))
-  updateAction s@(tidmap, _, _, _) (ThrowTo old ms b) =
-    (s, ThrowTo (renumbered tidmap old) ms b)
+  updateAction s@(tidmap, _, _, _) (ThrowTo old ms) =
+    (s, ThrowTo (renumbered tidmap old) ms)
   updateAction s@(tidmap, _, _, _) (BlockedThrowTo old) =
     (s, BlockedThrowTo (renumbered tidmap old))
   updateAction s act = (s, act)

dejafu/Test/DejaFu/SCT/Internal/DPOR.hs

@@ -565,7 +565,7 @@ independent safeIO ds t1 a1 t2 a2
     -- :(
     --
     -- See #191 / #190
-    check _ (ThrowTo t _ _) tid _ | t == tid = True
+    check _ (ThrowTo t _) tid _ | t == tid = True
     check _ (BlockedThrowTo t) tid _ | t == tid = True
     -- can't re-order an unsynchronised write with something which synchronises that IORef.
     check _ (simplifyAction -> UnsynchronisedWrite r) _ (simplifyAction -> a) | synchronises a r = True
@@ -582,23 +582,23 @@ dependent safeIO ds t1 a1 t2 a2 = case (a1, a2) of
   -- actually blocked. 'dependent'' has to assume that all
   -- potentially-blocking operations can block, and so is more
   -- pessimistic in this case.
-  (ThrowTo t _ _, ThrowTo u _ _)
+  (ThrowTo t _, ThrowTo u _)
     | t == t2 && u == t1 -> canInterrupt ds t1 a1 || canInterrupt ds t2 a2
-  (ThrowTo t _ _, _) | t == t2 -> canInterrupt ds t2 a2 && a2 /= Stop
-  (_, ThrowTo t _ _) | t == t1 -> canInterrupt ds t1 a1 && a1 /= Stop
+  (ThrowTo t _, _) | t == t2 -> canInterrupt ds t2 a2 && a2 /= Stop
+  (_, ThrowTo t _) | t == t1 -> canInterrupt ds t1 a1 && a1 /= Stop
 
   -- Dependency of STM transactions can be /greatly/ improved here, as
   -- the 'Lookahead' does not know which @TVar@s will be touched, and
   -- so has to assume all transactions are dependent.
-  (STM _ _, STM _ _)         -> checkSTM
-  (STM _ _, BlockedSTM _)    -> checkSTM
-  (STM _ _, ThrownSTM _ _ _) -> checkSTM
-  (BlockedSTM _, STM _ _)         -> checkSTM
-  (BlockedSTM _, BlockedSTM _)    -> checkSTM
-  (BlockedSTM _, ThrownSTM _ _ _) -> checkSTM
-  (ThrownSTM _ _ _, STM _ _)         -> checkSTM
-  (ThrownSTM _ _ _, BlockedSTM _)    -> checkSTM
-  (ThrownSTM _ _ _, ThrownSTM _ _ _) -> checkSTM
+  (STM _ _, STM _ _)       -> checkSTM
+  (STM _ _, BlockedSTM _)  -> checkSTM
+  (STM _ _, ThrownSTM _ _) -> checkSTM
+  (BlockedSTM _, STM _ _)       -> checkSTM
+  (BlockedSTM _, BlockedSTM _)  -> checkSTM
+  (BlockedSTM _, ThrownSTM _ _) -> checkSTM
+  (ThrownSTM _ _, STM _ _)       -> checkSTM
+  (ThrownSTM _ _, BlockedSTM _)  -> checkSTM
+  (ThrownSTM _ _, ThrownSTM _ _) -> checkSTM
 
   _ -> dependent' safeIO ds t1 a1 t2 (rewind a2)
     && dependent' safeIO ds t2 a2 t1 (rewind a1)
@@ -622,15 +622,15 @@ dependent' safeIO ds t1 a1 t2 l2 = case (a1, l2) of
   -- thread and if the actions can be interrupted. We can also
   -- slightly improve on that by not considering interrupting the
   -- normal termination of a thread: it doesn't make a difference.
-  (ThrowTo t _ _, WillThrowTo u)
+  (ThrowTo t _, WillThrowTo u)
     | t == t2 && u == t1 -> canInterrupt ds t1 a1 || canInterruptL ds t2 l2
-  (ThrowTo t _ _, _)   | t == t2 -> canInterruptL ds t2 l2 && l2 /= WillStop
+  (ThrowTo t _, _)   | t == t2 -> canInterruptL ds t2 l2 && l2 /= WillStop
   (_, WillThrowTo t) | t == t1 -> canInterrupt  ds t1 a1 && a1 /= Stop
 
   -- Another worst-case: assume all STM is dependent.
   (STM _ _, WillSTM) -> True
   (BlockedSTM _, WillSTM) -> True
-  (ThrownSTM _ _ _, WillSTM) -> True
+  (ThrownSTM _ _, WillSTM) -> True
 
   -- the number of capabilities is essentially a global shared
   -- variable

dejafu/Test/DejaFu/Types.hs

@@ -289,24 +289,23 @@ data ThreadAction =
   | STM [TAction] [ThreadId]
   -- ^ An STM transaction was executed, possibly waking up some
   -- threads.
-  | ThrownSTM [TAction] (Maybe MaskingState) Bool
+  | ThrownSTM [TAction] (Maybe MaskingState)
   -- ^ An STM transaction threw an exception.  Give the resultant
-  -- masking state after jumping to the exception handler (if it
-  -- changed).  If the 'Bool' is @True@, then this killed the thread.
+  -- masking state after jumping to the exception handler (if the
+  -- thread is still alive).
   | BlockedSTM [TAction]
   -- ^ Got blocked in an STM transaction.
   | Catching
   -- ^ Register a new exception handler
   | PopCatching
   -- ^ Pop the innermost exception handler from the stack.
-  | Throw (Maybe MaskingState) Bool
+  | Throw (Maybe MaskingState)
   -- ^ Throw an exception, and give the resultant masking state after
-  -- jumping to the exception handler (if it changed).  If the 'Bool'
-  -- is @True@, then this killed the thread.
-  | ThrowTo ThreadId (Maybe MaskingState) Bool
+  -- jumping to the exception handler (if the thread is still alive).
+  | ThrowTo ThreadId (Maybe MaskingState)
   -- ^ Throw an exception to a thread, and give the resultant masking
-  -- state after jumping to the exception handler (if it changed).  If
-  -- the 'Bool' is @True@, then this killed the thread.
+  -- state after jumping to the exception handler (if the thread is
+  -- still alive).
   | BlockedThrowTo ThreadId
   -- ^ Get blocked on a 'throwTo'.
   | SetMasking Bool MaskingState
@@ -360,15 +359,15 @@ instance NFData ThreadAction where
   rnf (CasIORef c b) = rnf (c, b)
   rnf (CommitIORef t c) = rnf (t, c)
   rnf (STM as ts) = rnf (as, ts)
-  rnf (ThrownSTM as (Just m) b) = m `seq` rnf (as, b)
-  rnf (ThrownSTM as Nothing b) = rnf (as, b)
+  rnf (ThrownSTM as (Just m)) = m `seq` rnf as
+  rnf (ThrownSTM as Nothing) = rnf as
   rnf (BlockedSTM as) = rnf as
   rnf Catching = ()
   rnf PopCatching = ()
-  rnf (Throw (Just m) b) = m `seq` rnf b
-  rnf (Throw Nothing b) = rnf b
-  rnf (ThrowTo t (Just m) b) = m `seq` rnf (t, b)
-  rnf (ThrowTo t Nothing b) = rnf (t, b)
+  rnf (Throw (Just m)) = m `seq` ()
+  rnf (Throw Nothing) = ()
+  rnf (ThrowTo t (Just m)) = m `seq` rnf t
+  rnf (ThrowTo t Nothing) = rnf t
   rnf (BlockedThrowTo t) = rnf t
   rnf (SetMasking b m) = rnf (b, show m)
   rnf (ResetMasking b m) = rnf (b, show m)