dejafu 1.11.0.5 → 1.12.0.0

raw patch · 13 files changed

+245/−199 lines, 13 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.rst +40/−0
• Test/DejaFu.hs +24/−48
• Test/DejaFu/Conc.hs +18/−16
• Test/DejaFu/Conc/Internal.hs +12/−15
• Test/DejaFu/Conc/Internal/Common.hs +1/−1
• Test/DejaFu/Internal.hs +3/−2
• Test/DejaFu/Refinement.hs +4/−4
• Test/DejaFu/SCT.hs +23/−23
• Test/DejaFu/SCT/Internal.hs +13/−11
• Test/DejaFu/Settings.hs +26/−5
• Test/DejaFu/Types.hs +71/−61
• Test/DejaFu/Utils.hs +8/−11
• dejafu.cabal +2/−2

@@ -7,6 +7,46 @@ .. _PVP: https://pvp.haskell.org/  +1.12.0.0 (2019-01-20)+---------------------++* Git: :tag:`dejafu-1.12.0.0`+* Hackage: :hackage:`dejafu-1.12.0.0`++Added+~~~~~++* ``Test.DejaFu.Types.Error`` for internal errors and misuses, with+  predicates:+    * ``Test.DejaFu.Types.isSchedulerError``+    * ``Test.DejaFu.Types.isIncorrectUsage``++* Deprecated ``Test.DejaFu.Types.Failure`` type synonym for+  ``Condition``.++* The ``Test.DejaFu.Settings.lshowAborts`` option, to make SCT+  functions show ``Abort`` conditions.++* ``Test.DejaFu.Utils.showCondition``++Changed+~~~~~~~++* Renamed ``Test.DejaFu.Types.Failure`` to+  ``Test.DejaFu.Types.Condition``.++* The SCT functions drop ``Left Abort`` results by default, restore+  the old behaviour with ``Test.DejaFu.Settings.lshowAborts``.++Removed+~~~~~~~++* ``Test.DejaFu.Types.isInternalError``+* ``Test.DejaFu.Types.isIllegalDontCheck``+* ``Test.DejaFu.Types.isIllegalSubconcurrency``+* ``Test.DejaFu.Utils.showFail``++ 1.11.0.5 (2019-01-17) --------------------- 

@@ -46,8 +46,8 @@   * Each \"-\" represents one \"step\" of the computation. -__Failures:__ If a program doesn't terminate successfully, we say it-has /failed/.  dejafu can detect a few different types of failure:+__Conditions:__ A program may fail to terminate in a way which+produces a value. dejafu can detect a few such cases:   * 'Deadlock', if every thread is blocked. @@ -56,28 +56,6 @@   * 'UncaughtException', if the main thread is killed by an exception. -There are two types of failure which dejafu itself may raise:-- * 'Abort', used in systematic testing (the default) if there are no-   allowed decisions remaining.  For example, by default any test case-   which takes more than 250 scheduling points to finish will be-   aborted.  You can use the 'systematically' function to supply (or-   disable) your own bounds.-- * 'InternalError', used if something goes wrong.  If you get this and-   aren't using a scheduler you wrote yourself, please [file a-   bug](https://github.com/barrucadu/dejafu/issues).--Finally, there are two failures which can arise through improper use of-dejafu:-- * 'IllegalDontCheck', the "Test.DejaFu.Conc.dontCheck" function is-   used as anything other than the fist action in the main thread.-- * 'IllegalSubconcurrency', the "Test.DejaFu.Conc.subconcurrency"-   function is used when multiple threads exist, or is used inside-   another @subconcurrency@ call.- __Beware of 'liftIO':__ dejafu works by running your test case lots of times with different schedules.  If you use 'liftIO' at all, make sure that any @IO@ you perform is deterministic when executed in the same@@ -129,7 +107,7 @@ -}    , Result(..)-  , Failure(..)+  , Condition(..)   , runTest   , runTestWay @@ -183,20 +161,17 @@   , gives   , gives' -  -- *** Failures+  -- *** Conditions    {- | -Helper functions to identify failures.+Helper functions to identify conditions.  -} -  , isInternalError   , isAbort   , isDeadlock   , isUncaughtException-  , isIllegalSubconcurrency-  , isIllegalDontCheck    -- * Property testing @@ -263,6 +238,7 @@   , module Test.DejaFu.Refinement    -- * Deprecated+  , Failure   , dejafuDiscard   ) where @@ -500,7 +476,7 @@ -- -- @since 1.0.0.0 dejafuDiscard :: (MonadConc n, MonadIO n, Show b)-  => (Either Failure a -> Maybe Discard)+  => (Either Condition a -> Maybe Discard)   -- ^ Selectively discard results.   -> Way   -- ^ How to run the concurrent program.@@ -618,7 +594,7 @@ data Result a = Result   { _pass :: Bool   -- ^ Whether the test passed or not.-  , _failures :: [(Either Failure a, Trace)]+  , _failures :: [(Either Condition a, Trace)]   -- ^ The failing cases, if any.   , _failureMsg :: String   -- ^ A message to display on failure, if nonempty@@ -631,7 +607,7 @@               )  -- | A failed result, taking the given list of failures.-defaultFail :: [(Either Failure a, Trace)] -> Result a+defaultFail :: [(Either Condition a, Trace)] -> Result a defaultFail failures = Result False failures ""  -- | A passed result.@@ -717,9 +693,9 @@ -- -- @since 1.0.0.0 data ProPredicate a b = ProPredicate-  { pdiscard :: Either Failure a -> Maybe Discard+  { pdiscard :: Either Condition a -> Maybe Discard   -- ^ Selectively discard results before computing the result.-  , peval :: [(Either Failure a, Trace)] -> Result b+  , peval :: [(Either Condition a, Trace)] -> Result b   -- ^ Compute the result with the un-discarded results.   } @@ -755,7 +731,7 @@  -- | Check that a computation never aborts. ----- Any result other than an abort, including other 'Failure's, is+-- Any result other than an abort, including other 'Condition's, is -- allowed. -- -- @since 1.0.0.0@@ -770,7 +746,7 @@  -- | Check that a computation aborts at least once. ----- Any result other than an abort, including other 'Failure's, is+-- Any result other than an abort, including other 'Condition's, is -- allowed. -- -- @since 1.0.0.0@@ -779,7 +755,7 @@  -- | Check that a computation never deadlocks. ----- Any result other than a deadlock, including other 'Failure's, is+-- Any result other than a deadlock, including other 'Condition's, is -- allowed. -- -- @since 1.0.0.0@@ -794,7 +770,7 @@  -- | Check that a computation deadlocks at least once. ----- Any result other than a deadlock, including other 'Failure's, is+-- Any result other than a deadlock, including other 'Condition's, is -- allowed. -- -- @since 1.0.0.0@@ -804,7 +780,7 @@ -- | Check that a computation never fails with an uncaught exception. -- -- Any result other than an uncaught exception, including other--- 'Failure's, is allowed.+-- 'Condition's, is allowed. -- -- @since 1.0.0.0 exceptionsNever :: Predicate a@@ -819,7 +795,7 @@ -- | Check that a computation fails with an uncaught exception at least once. -- -- Any result other than an uncaught exception, including other--- 'Failure's, is allowed.+-- 'Condition's, is allowed. -- -- @since 1.0.0.0 exceptionsSometimes :: Predicate a@@ -911,7 +887,7 @@ -- | Check that a @Maybe@-producing function always returns 'Nothing'. -- -- @since 1.0.0.0-alwaysNothing :: (Either Failure a -> Maybe (Either Failure b)) -> ProPredicate a b+alwaysNothing :: (Either Condition a -> Maybe (Either Condition b)) -> ProPredicate a b alwaysNothing f = ProPredicate   { pdiscard = maybe (Just DiscardResultAndTrace) (const Nothing) . f   , peval = \xs ->@@ -923,14 +899,14 @@ -- true. -- -- @since 1.0.0.0-alwaysTrue :: (Either Failure a -> Bool) -> Predicate a+alwaysTrue :: (Either Condition a -> Bool) -> Predicate a alwaysTrue p = alwaysNothing (\efa -> if p efa then Nothing else Just efa)  -- | Check that a @Maybe@-producing function returns 'Nothing' at -- least once. -- -- @since 1.0.0.0-somewhereNothing :: (Either Failure a -> Maybe (Either Failure b)) -> ProPredicate a b+somewhereNothing :: (Either Condition a -> Maybe (Either Condition b)) -> ProPredicate a b somewhereNothing f = ProPredicate   { pdiscard = maybe (Just DiscardTrace) (const Nothing) . f   , peval = \xs ->@@ -942,14 +918,14 @@ -- least once. -- -- @since 1.0.0.0-somewhereTrue :: (Either Failure a -> Bool) -> Predicate a+somewhereTrue :: (Either Condition a -> Bool) -> Predicate a somewhereTrue p = somewhereNothing (\efa -> if p efa then Nothing else Just efa)  -- | Predicate for when there is a known set of results where every -- result must be exhibited at least once. -- -- @since 1.0.0.0-gives :: (Eq a, Show a) => [Either Failure a] -> Predicate a+gives :: (Eq a, Show a) => [Either Condition a] -> Predicate a gives expected = ProPredicate     { pdiscard = \efa -> if efa `elem` expected then Just DiscardTrace else Nothing     , peval = \xs -> go expected [] xs $ defaultFail (failures xs)@@ -969,7 +945,7 @@      failures = filter (\(r, _) -> r `notElem` expected) --- | Variant of 'gives' that doesn't allow for expected failures.+-- | Variant of 'gives' that doesn't allow for non-success conditions. -- -- @since 1.0.0.0 gives' :: (Eq a, Show a) => [a] -> Predicate a@@ -993,7 +969,7 @@         putStrLn $ _failureMsg result        let failures = _failures result-      let output = map (\(r, t) -> putStrLn . indent $ either showFail show r ++ " " ++ showTrace t) $ take 5 failures+      let output = map (\(r, t) -> putStrLn . indent $ either showCondition show r ++ " " ++ showTrace t) $ take 5 failures       sequence_ $ intersperse (putStrLn "") output       when (moreThan 5 failures) $         putStrLn (indent "...")

@@ -23,7 +23,7 @@   , ConcIO    -- * Executing computations-  , Failure(..)+  , Condition(..)   , MemType(..)   , runConcurrent   , subconcurrency@@ -49,10 +49,13 @@   , IORefId   , MaskingState(..)   , showTrace-  , showFail+  , showCondition    -- * Scheduling   , module Test.DejaFu.Schedule++  -- * Deprecated+  , Failure   ) where  import           Control.Exception                   (MaskingState(..))@@ -187,8 +190,9 @@   atomically = toConc . AAtom  -- | Run a concurrent computation with a given 'Scheduler' and initial--- state, returning a failure reason on error. Also returned is the--- final state of the scheduler, and an execution trace.+-- state, returning either the final result or the condition which+-- prevented that. Also returned is the final state of the scheduler,+-- and an execution trace. -- -- If the RTS supports bound threads (ghc -threaded when linking) then -- the main thread of the concurrent computation will be bound, and@@ -215,7 +219,7 @@   -> MemType   -> s   -> ConcT n a-  -> n (Either Failure a, s, Trace)+  -> n (Either Condition a, s, Trace) runConcurrent sched memtype s ma = do   res <- runConcurrency False sched memtype s initialIdSource 2 (unC ma)   out <- efromJust <$> C.readIORef (finalRef res)@@ -229,12 +233,11 @@ -- This can only be called in the main thread, when no other threads -- exist. Calls to 'subconcurrency' cannot be nested, or placed inside -- a call to 'dontCheck'. Violating either of these conditions will--- result in the computation failing with @IllegalSubconcurrency@.--- The overall test-case can still succeed if the predicate allows for--- a failing computation.+-- result in the computation throwing a @NestedSubconcurrency@ or+-- @MultithreadedSubconcurrency@ error. -- -- @since 0.6.0.0-subconcurrency :: ConcT n a -> ConcT n (Either Failure a)+subconcurrency :: ConcT n a -> ConcT n (Either Condition a) subconcurrency ma = toConc (ASub (unC ma))  -- | Run an arbitrary action which gets some special treatment:@@ -261,12 +264,11 @@ -- action continue to exist in the main computation. -- -- This must be the first thing done in the main thread.  Violating--- this condition will result in the computation failing with--- @IllegalDontCheck@.  The overall test-case can still succeed if the--- predicate allows for a failing computation.+-- this condition will result in the computation throwing a+-- @LateDontCheck@ exception. ----- If the action fails (deadlock, length bound exceeded, etc), the--- whole computation fails.+-- If the action does not successfully produce a value (deadlock,+-- length bound exceeded, etc), the whole computation is terminated. -- -- @since 1.1.0.0 dontCheck@@ -346,7 +348,7 @@ -- @since 1.1.0.0 runForDCSnapshot :: C.MonadConc n   => ConcT n a-  -> n (Maybe (Either Failure (DCSnapshot n a), Trace))+  -> n (Maybe (Either Condition (DCSnapshot n a), Trace)) runForDCSnapshot ma = do   res <- runConcurrency True roundRobinSchedNP SequentialConsistency () initialIdSource 2 (unC ma)   out <- C.readIORef (finalRef res)@@ -368,7 +370,7 @@   -> MemType   -> s   -> DCSnapshot n a-  -> n (Either Failure a, s, Trace)+  -> n (Either Condition a, s, Trace) runWithDCSnapshot sched memtype s snapshot = do   let context = (dcsContext snapshot) { cSchedState = s }   let restore = dcsRestore snapshot

@@ -19,6 +19,7 @@ import           Control.Exception                   (Exception,                                                       MaskingState(..),                                                       toException)+import qualified Control.Monad.Catch                 as E import qualified Control.Monad.Conc.Class            as C import           Data.Foldable                       (foldrM, toList) import           Data.Functor                        (void)@@ -49,7 +50,7 @@ -- | The result of running a concurrent program. data CResult n g a = CResult   { finalContext :: Context n g-  , finalRef :: C.IORef n (Maybe (Either Failure a))+  , finalRef :: C.IORef n (Maybe (Either Condition a))   , finalRestore :: Maybe (Threads n -> n ())   -- ^ Meaningless if this result doesn't come from a snapshotting   -- execution.@@ -67,12 +68,12 @@   -- restoring.   , dcsRestore :: Threads n -> n ()   -- ^ Action to restore IORef, MVar, and TVar values.-  , dcsRef :: C.IORef n (Maybe (Either Failure a))+  , dcsRef :: C.IORef n (Maybe (Either Condition a))   -- ^ Reference where the result will be written.   }  -- | Run a concurrent computation with a given 'Scheduler' and initial--- state, returning a failure reason on error. Also returned is the+-- state, returning a Condition reason on error. Also returned is the -- final state of the scheduler, and an execution trace. runConcurrency :: (C.MonadConc n, HasCallStack)   => Bool@@ -118,7 +119,7 @@   -> MemType   -> Context n g   -> (Threads n -> n ())-  -> C.IORef n (Maybe (Either Failure a))+  -> C.IORef n (Maybe (Either Condition a))   -> n (CResult n g a) runConcurrencyWithSnapshot sched memtype ctx restore ref = do   let boundThreads = M.filter (isJust . _bound) (cThreads ctx)@@ -151,7 +152,7 @@   => Bool   -> Scheduler g   -> MemType-  -> C.IORef n (Maybe (Either Failure a))+  -> C.IORef n (Maybe (Either Condition a))   -> Context n g   -> n (CResult n g a) runThreads forSnapshot sched memtype ref = schedule (const $ pure ()) Seq.empty Nothing where@@ -180,7 +181,7 @@       in case choice of            Just chosen -> case M.lookup chosen threadsc of              Just thread-               | isBlocked thread -> die InternalError restore sofar prior ctx'+               | isBlocked thread -> E.throwM ScheduledBlockedThread                | otherwise ->                  let decision                        | Just chosen == (fst <$> prior) = Continue@@ -188,7 +189,7 @@                        | otherwise = SwitchTo chosen                      alternatives = filter (\(t, _) -> t /= chosen) runnable'                  in step decision alternatives chosen thread restore sofar prior ctx'-             Nothing -> die InternalError restore sofar prior ctx'+             Nothing -> E.throwM ScheduledMissingThread            Nothing -> die Abort restore sofar prior ctx'     where       (choice, g')  = scheduleThread sched prior (efromList runnable') (cSchedState ctx)@@ -272,7 +273,7 @@ data What n g   = Succeeded (Context n g)   -- ^ Action succeeded: continue execution.-  | Failed Failure+  | Failed Condition   -- ^ Action caused computation to fail: stop.   | Snap (Context n g)   -- ^ Action was a snapshot point and we're in snapshot mode: stop.@@ -630,8 +631,8 @@  -- run a subconcurrent computation. stepThread forSnapshot _ sched memtype tid (ASub ma c) = \ctx ->-  if | forSnapshot -> pure (Failed IllegalSubconcurrency, Single Subconcurrency, const (pure ()))-     | M.size (cThreads ctx) > 1 -> pure (Failed IllegalSubconcurrency, Single Subconcurrency, const (pure ()))+  if | forSnapshot -> E.throwM NestedSubconcurrency+     | M.size (cThreads ctx) > 1 -> E.throwM MultithreadedSubconcurrency      | otherwise -> do          res <- runConcurrency False sched memtype (cSchedState ctx) (cIdSource ctx) (cCaps ctx) ma          out <- efromJust <$> C.readIORef (finalRef res)@@ -677,11 +678,7 @@              , Single (DontCheck (toList (finalTrace res)))              , const (pure ())              )-     | otherwise -> pure-       ( Failed IllegalDontCheck-       , Single (DontCheck [])-       , const (pure ())-       )+     | otherwise -> E.throwM LateDontCheck  -- | Handle an exception being thrown from an @AAtom@, @AThrow@, or -- @AThrowTo@.

@@ -123,7 +123,7 @@   | ACommit ThreadId IORefId   | AStop (n ()) -  | forall a. ASub (ModelConc n a) (Either Failure a -> Action n)+  | forall a. ASub (ModelConc n a) (Either Condition a -> Action n)   | AStopSub (Action n)   | forall a. ADontCheck (Maybe Int) (ModelConc n a) (a -> Action n) 

@@ -38,14 +38,15 @@ data Settings n a = Settings   { _way :: Way   , _memtype :: MemType-  , _discard :: Maybe (Either Failure a -> Maybe Discard)+  , _discard :: Maybe (Either Condition a -> Maybe Discard)   , _debugShow :: Maybe (a -> String)   , _debugPrint :: Maybe (String -> n ())   , _debugFatal :: Bool-  , _earlyExit :: Maybe (Either Failure a -> Bool)+  , _earlyExit :: Maybe (Either Condition a -> Bool)   , _equality :: Maybe (a -> a -> Bool)   , _simplify  :: Bool   , _safeIO :: Bool+  , _showAborts :: Bool   }  -- | How to explore the possible executions of a concurrent program.

@@ -114,7 +114,7 @@ import qualified Data.Set                 as S import           Test.LeanCheck           (Listable(..), concatMapT, mapT) -import           Test.DejaFu.Conc         (ConcIO, Failure, subconcurrency)+import           Test.DejaFu.Conc         (ConcIO, Condition, subconcurrency) import           Test.DejaFu.SCT          (runSCT) import           Test.DejaFu.Settings     (defaultMemType, defaultWay) @@ -266,9 +266,9 @@     -- ^ The seed for this set of executions.     , failingArgs  :: [String]     -- ^ The values of free variables, as strings.-    , leftResults  :: Set (Maybe Failure, o)+    , leftResults  :: Set (Maybe Condition, o)     -- ^ The set of results of the left signature.-    , rightResults :: Set (Maybe Failure, o)+    , rightResults :: Set (Maybe Condition, o)     -- ^ The set of results of the right signature.     }   | NoExpectedFailure@@ -409,7 +409,7 @@ evalSigWithSeed :: Ord o   => Sig s o x   -> x-  -> IO (Set (Maybe Failure, o))+  -> IO (Set (Maybe Condition, o)) evalSigWithSeed sig x = do   results <- runSCT defaultWay defaultMemType $ do     s <- initialise sig x

@@ -72,7 +72,7 @@   -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> ConcT n a   -- ^ The computation to run many times.-  -> n [(Either Failure a, Trace)]+  -> n [(Either Condition a, Trace)] runSCT way = runSCTWithSettings . fromWayAndMemType way  -- | Return the set of results of a concurrent program.@@ -85,7 +85,7 @@   -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> ConcT n a   -- ^ The computation to run many times.-  -> n (Set (Either Failure a))+  -> n (Set (Either Condition a)) resultsSet way = resultsSetWithSettings . fromWayAndMemType way  -- | A variant of 'runSCT' which can selectively discard results.@@ -95,7 +95,7 @@ -- -- @since 1.0.0.0 runSCTDiscard :: MonadConc n-  => (Either Failure a -> Maybe Discard)+  => (Either Condition a -> Maybe Discard)   -- ^ Selectively discard results.   -> Way   -- ^ How to run the concurrent program.@@ -103,7 +103,7 @@   -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> ConcT n a   -- ^ The computation to run many times.-  -> n [(Either Failure a, Trace)]+  -> n [(Either Condition a, Trace)] runSCTDiscard discard way = runSCTWithSettings . set ldiscard (Just discard) . fromWayAndMemType way {-# DEPRECATED runSCTDiscard "Use runSCTWithSettings instead" #-} @@ -111,7 +111,7 @@ -- -- @since 1.0.0.0 resultsSetDiscard :: (MonadConc n, Ord a)-  => (Either Failure a -> Maybe Discard)+  => (Either Condition a -> Maybe Discard)   -- ^ Selectively discard results.  Traces are always discarded.   -> Way   -- ^ How to run the concurrent program.@@ -119,7 +119,7 @@   -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> ConcT n a   -- ^ The computation to run many times.-  -> n (Set (Either Failure a))+  -> n (Set (Either Condition a)) resultsSetDiscard discard way memtype conc =   let discard' efa = discard efa <|> Just DiscardTrace   in S.fromList . map fst <$> runSCTDiscard discard' way memtype conc@@ -135,7 +135,7 @@ -- -- @since 1.0.0.0 runSCT' :: (MonadConc n, NFData a)-  => Way -> MemType -> ConcT n a -> n [(Either Failure a, Trace)]+  => Way -> MemType -> ConcT n a -> n [(Either Condition a, Trace)] runSCT' way = runSCTWithSettings' . fromWayAndMemType way  -- | A strict variant of 'resultsSet'.@@ -145,7 +145,7 @@ -- -- @since 1.0.0.0 resultsSet' :: (MonadConc n, Ord a, NFData a)-  => Way -> MemType -> ConcT n a -> n (Set (Either Failure a))+  => Way -> MemType -> ConcT n a -> n (Set (Either Condition a)) resultsSet' way = resultsSetWithSettings' . fromWayAndMemType way  -- | A strict variant of 'runSCTDiscard'.@@ -158,7 +158,7 @@ -- -- @since 1.0.0.0 runSCTDiscard' :: (MonadConc n, NFData a)-  => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT n a -> n [(Either Failure a, Trace)]+  => (Either Condition a -> Maybe Discard) -> Way -> MemType -> ConcT n a -> n [(Either Condition a, Trace)] runSCTDiscard' discard way memtype conc = do   res <- runSCTDiscard discard way memtype conc   rnf res `seq` pure res@@ -171,7 +171,7 @@ -- -- @since 1.0.0.0 resultsSetDiscard' :: (MonadConc n, Ord a, NFData a)-  => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT n a -> n (Set (Either Failure a))+  => (Either Condition a -> Maybe Discard) -> Way -> MemType -> ConcT n a -> n (Set (Either Condition a)) resultsSetDiscard' discard way memtype conc = do   res <- resultsSetDiscard discard way memtype conc   rnf res `seq` pure res@@ -191,7 +191,7 @@   -- ^ The SCT settings.   -> ConcT n a   -- ^ The computation to run many times.-  -> n [(Either Failure a, Trace)]+  -> n [(Either Condition a, Trace)] runSCTWithSettings settings conc = case _way settings of   Systematic cb0 ->     let initial = initialState@@ -232,7 +232,7 @@   -- ^ The SCT settings.   -> ConcT n a   -- ^ The computation to run many times.-  -> n (Set (Either Failure a))+  -> n (Set (Either Condition a)) resultsSetWithSettings settings conc =   let settings' = settings { _discard = Just $ \efa -> fromMaybe (const Nothing) (_discard settings) efa <|> Just DiscardTrace }   in S.fromList . map fst <$> runSCTWithSettings settings' conc@@ -249,7 +249,7 @@ runSCTWithSettings' :: (MonadConc n, NFData a)   => Settings n a   -> ConcT n a-  -> n [(Either Failure a, Trace)]+  -> n [(Either Condition a, Trace)] runSCTWithSettings' settings conc = do   res <- runSCTWithSettings settings conc   rnf res `seq` pure res@@ -263,7 +263,7 @@ resultsSetWithSettings' :: (MonadConc n, Ord a, NFData a)   => Settings n a   -> ConcT n a-  -> n (Set (Either Failure a))+  -> n (Set (Either Condition a)) resultsSetWithSettings' settings conc = do   res <- resultsSetWithSettings settings conc   rnf res `seq` pure res@@ -378,7 +378,7 @@   -- ^ The combined bounds.   -> ConcT n a   -- ^ The computation to run many times-  -> n [(Either Failure a, Trace)]+  -> n [(Either Condition a, Trace)] sctBound = sctBoundDiscard (const Nothing) {-# DEPRECATED sctBound "Use runSCT instead" #-} @@ -389,7 +389,7 @@ -- -- @since 1.0.0.0 sctBoundDiscard :: MonadConc n-  => (Either Failure a -> Maybe Discard)+  => (Either Condition a -> Maybe Discard)   -- ^ Selectively discard results.   -> MemType   -- ^ The memory model to use for non-synchronised @IORef@ operations.@@ -397,7 +397,7 @@   -- ^ The combined bounds.   -> ConcT n a   -- ^ The computation to run many times-  -> n [(Either Failure a, Trace)]+  -> n [(Either Condition a, Trace)] sctBoundDiscard discard memtype cb = runSCTWithSettings $   set ldiscard (Just discard) (fromWayAndMemType (systematically cb) memtype) {-# DEPRECATED sctBoundDiscard "Use runSCTWithSettings instead" #-}@@ -419,7 +419,7 @@   -- ^ The number of executions to perform.   -> ConcT n a   -- ^ The computation to run many times.-  -> n [(Either Failure a, Trace)]+  -> n [(Either Condition a, Trace)] sctUniformRandom = sctUniformRandomDiscard (const Nothing) {-# DEPRECATED sctUniformRandom "Use runSCT instead" #-} @@ -430,7 +430,7 @@ -- -- @since 1.0.0.0 sctUniformRandomDiscard :: (MonadConc n, RandomGen g)-  => (Either Failure a -> Maybe Discard)+  => (Either Condition a -> Maybe Discard)   -- ^ Selectively discard results.   -> MemType   -- ^ The memory model to use for non-synchronised @IORef@ operations.@@ -440,7 +440,7 @@   -- ^ The number of executions to perform.   -> ConcT n a   -- ^ The computation to run many times.-  -> n [(Either Failure a, Trace)]+  -> n [(Either Condition a, Trace)] sctUniformRandomDiscard discard memtype g lim = runSCTWithSettings $   set ldiscard (Just discard) (fromWayAndMemType (uniformly g lim) memtype) {-# DEPRECATED sctUniformRandomDiscard "Use runSCTWithSettings instead" #-}@@ -462,7 +462,7 @@   -- ^ The number of executions to perform.   -> ConcT n a   -- ^ The computation to run many times.-  -> n [(Either Failure a, Trace)]+  -> n [(Either Condition a, Trace)] sctWeightedRandom = sctWeightedRandomDiscard (const Nothing) {-# DEPRECATED sctWeightedRandom "Use runSCT instead" #-} @@ -473,7 +473,7 @@ -- -- @since 1.7.0.0 sctWeightedRandomDiscard :: (MonadConc n, RandomGen g)-  => (Either Failure a -> Maybe Discard)+  => (Either Condition a -> Maybe Discard)   -- ^ Selectively discard results.   -> MemType   -- ^ The memory model to use for non-synchronised @IORef@ operations.@@ -483,7 +483,7 @@   -- ^ The number of executions to perform.   -> ConcT n a   -- ^ The computation to run many times.-  -> n [(Either Failure a, Trace)]+  -> n [(Either Condition a, Trace)] sctWeightedRandomDiscard discard memtype g lim = runSCTWithSettings $   set ldiscard (Just discard) (fromWayAndMemType (randomly g lim) memtype) {-# DEPRECATED sctWeightedRandomDiscard "Use runSCTWithSettings instead" #-}

@@ -42,10 +42,10 @@   -- ^ Initial state   -> (s -> Maybe t)   -- ^ State predicate-  -> ((Scheduler g -> g -> n (Either Failure a, g, Trace)) -> s -> t -> n (s, Maybe (Either Failure a, Trace)))+  -> ((Scheduler g -> g -> n (Either Condition a, g, Trace)) -> s -> t -> n (s, Maybe (Either Condition a, Trace)))   -- ^ Run the computation and update the state   -> ConcT n a-  -> n [(Either Failure a, Trace)]+  -> n [(Either Condition a, Trace)] sct settings s0 sfun srun conc     | canDCSnapshot conc = runForDCSnapshot conc >>= \case         Just (Right snap, _) -> sct'Snap snap@@ -87,19 +87,20 @@   -- ^ Initial state   -> (s -> Maybe t)   -- ^ State predicate-  -> (s -> t -> n (s, Maybe (Either Failure a, Trace)))+  -> (s -> t -> n (s, Maybe (Either Condition a, Trace)))   -- ^ Run the computation and update the state-  -> (forall x. Scheduler x -> x -> n (Either Failure a, x, Trace))+  -> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))   -- ^ Just run the computation   -> ThreadId   -- ^ The first available @ThreadId@   -> IORefId   -- ^ The first available @IORefId@-  -> n [(Either Failure a, Trace)]+  -> n [(Either Condition a, Trace)] sct' settings s0 sfun srun run nTId nCRId = go Nothing [] s0 where   go (Just res) _ _ | earlyExit res = pure []-  go _ seen !s = case sfun s of+  go res0 seen !s = case sfun s of     Just t -> srun s t >>= \case+      (s', Just (Left Abort, _)) | hideAborts -> go res0 seen s'       (s', Just (res, trace)) -> case discard res of         Just DiscardResultAndTrace -> go (Just res) seen s'         Just DiscardTrace -> result res [] seen s'@@ -132,6 +133,7 @@    earlyExit = fromMaybe (const False) (_earlyExit settings)   discard = fromMaybe (const Nothing) (_discard settings)+  hideAborts = not (_showAborts settings)  -- | Given a result and a trace, produce a more minimal trace. --@@ -150,16 +152,16 @@ simplifyExecution :: (MonadConc n, HasCallStack)   => Settings n a   -- ^ The SCT settings ('Way' is ignored)-  -> (forall x. Scheduler x -> x -> n (Either Failure a, x, Trace))+  -> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))   -- ^ Just run the computation   -> ThreadId   -- ^ The first available @ThreadId@   -> IORefId   -- ^ The first available @IORefId@-  -> Either Failure a+  -> Either Condition a   -- ^ The expected result   -> Trace-  -> n (Either Failure a, Trace)+  -> n (Either Condition a, Trace) simplifyExecution settings run nTId nCRId res trace     | tidTrace == simplifiedTrace = do         debugPrint ("Simplifying new result '" ++ p res ++ "': no simplification possible!")@@ -186,11 +188,11 @@  -- | Replay an execution. replay :: MonadConc n-  => (forall x. Scheduler x -> x -> n (Either Failure a, x, Trace))+  => (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))   -- ^ Run the computation   -> [(ThreadId, ThreadAction)]   -- ^ The reduced sequence of scheduling decisions-  -> n (Either Failure a, [(ThreadId, ThreadAction)], Trace)+  -> n (Either Condition a, [(ThreadId, ThreadAction)], Trace) replay run = run (Scheduler (const sched)) where     sched runnable ((t, Stop):ts) = case findThread t runnable of       Just t' -> (Just t', ts)

@@ -118,7 +118,7 @@   -- opportunity to get rid of them early is possibly a great saving   -- of memory.   ---  -- A discard function, which has type @Either Failure a -> Maybe+  -- A discard function, which has type @Either Condition a -> Maybe   -- Discard@, can selectively discard results or execution traces   -- before the schedule exploration finishes, allowing them to be   -- garbage collected sooner.@@ -134,8 +134,9 @@    -- | Sometimes we don't want to wait for all executions to be   -- explored, we just want to stop as soon as a particular result is-  -- found.  An early-exit predicate, which has type @Either Failure a-  -- -> Bool@, can opt to halt execution when such a result is found.+  -- found.  An early-exit predicate, which has type @Either Condition+  -- a -> Bool@, can opt to halt execution when such a result is+  -- found.   --   -- All results found up to, and including, the one which terminates   -- the exploration are reported.@@ -202,6 +203,16 @@    , lsafeIO +  -- ** Abort conditions++  -- | Occasionally in an execution dejafu will discover that no+  -- available scheduling decisions are within the specified bounds,+  -- and aborts the execution to move onto the next.  This is+  -- signalled by an 'Abort' condition.  By default, abort conditions+  -- are /not/ returned from the SCT functions.++  , lshowAborts+   -- ** Debug output    -- | You can opt to receive debugging messages by setting debugging@@ -256,6 +267,7 @@   , _equality = Nothing   , _simplify = False   , _safeIO = False+  , _showAborts = False   }  -------------------------------------------------------------------------------@@ -394,7 +406,7 @@ -- | A lens into the discard function. -- -- @since 1.2.0.0-ldiscard :: Lens' (Settings n a) (Maybe (Either Failure a -> Maybe Discard))+ldiscard :: Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard)) ldiscard afb s = (\b -> s {_discard = b}) <$> afb (_discard s)  -------------------------------------------------------------------------------@@ -403,7 +415,7 @@ -- | A lens into the early-exit predicate. -- -- @since 1.2.0.0-learlyExit :: Lens' (Settings n a) (Maybe (Either Failure a -> Bool))+learlyExit :: Lens' (Settings n a) (Maybe (Either Condition a -> Bool)) learlyExit afb s = (\b -> s {_earlyExit = b}) <$> afb (_earlyExit s)  -------------------------------------------------------------------------------@@ -432,6 +444,15 @@ -- @since 1.10.1.0 lsafeIO :: Lens' (Settings n a) Bool lsafeIO afb s = (\b -> s {_safeIO = b}) <$> afb (_safeIO s)++-------------------------------------------------------------------------------+-- Abort conditions++-- | A lens into the show-aborts flag.+--+-- @since 1.12.0.0+lshowAborts :: Lens' (Settings n a) Bool+lshowAborts afb s = (\b -> s {_showAborts = b}) <$> afb (_showAborts s)  ------------------------------------------------------------------------------- -- Debug output

@@ -436,20 +436,23 @@ instance NFData Decision  ---------------------------------------------------------------------------------- * Failures+-- * Conditions --- | An indication of how a concurrent computation failed.+-- | A type synonym for 'Condition', use that instead. --+-- @since 1.12.0.0+{-# DEPRECATED Failure "The 'Failure' type has been split up into 'Condition' and 'Error', with different semantics." #-}+type Failure = Condition++-- | An indication of how a concurrent computation terminated, if it+-- didn't produce a value.+-- -- The @Eq@, @Ord@, and @NFData@ instances compare/evaluate the -- exception with @show@ in the @UncaughtException@ case. ----- @since 1.1.0.0-data Failure-  = InternalError-  -- ^ Will be raised if the scheduler does something bad. This should-  -- never arise unless you write your own, faulty, scheduler! If it-  -- does, please file a bug report.-  | Abort+-- @since 1.12.0.0+data Condition+  = Abort   -- ^ The scheduler chose to abort execution. This will be produced   -- if, for example, all possible decisions exceed the specified   -- bounds (there have been too many pre-emptions, the computation@@ -462,85 +465,92 @@   -- STM transaction.   | UncaughtException SomeException   -- ^ An uncaught exception bubbled to the top of the computation.-  | IllegalSubconcurrency-  -- ^ Calls to @subconcurrency@ were nested, or attempted when-  -- multiple threads existed.-  | IllegalDontCheck-  -- ^ A call to @dontCheck@ was attempted after the first action of-  -- the initial thread.-  deriving Show+  deriving (Show, Generic) -instance Eq Failure where-  InternalError          == InternalError          = True+instance Eq Condition where   Abort                  == Abort                  = True   Deadlock               == Deadlock               = True   STMDeadlock            == STMDeadlock            = True   (UncaughtException e1) == (UncaughtException e2) = show e1 == show e2-  IllegalSubconcurrency  == IllegalSubconcurrency  = True-  IllegalDontCheck       == IllegalDontCheck       = True   _ == _ = False -instance Ord Failure where+instance Ord Condition where   compare = compare `on` transform where-    transform :: Failure -> (Int, Maybe String)-    transform InternalError = (0, Nothing)+    transform :: Condition -> (Int, Maybe String)     transform Abort = (1, Nothing)     transform Deadlock = (2, Nothing)     transform STMDeadlock = (3, Nothing)     transform (UncaughtException e) = (4, Just (show e))-    transform IllegalSubconcurrency = (5, Nothing)-    transform IllegalDontCheck = (6, Nothing) -instance NFData Failure where+instance NFData Condition where   rnf (UncaughtException e) = rnf (show e)   rnf f = f `seq` () --- | @since 1.3.1.0-deriving instance Generic Failure---- | Check if a failure is an @InternalError@.------ @since 0.9.0.0-isInternalError :: Failure -> Bool-isInternalError InternalError = True-isInternalError _ = False---- | Check if a failure is an @Abort@.+-- | Check if a condition is an @Abort@. -- -- @since 0.9.0.0-isAbort :: Failure -> Bool+isAbort :: Condition -> Bool isAbort Abort = True isAbort _ = False --- | Check if a failure is a @Deadlock@ or an @STMDeadlock@.+-- | Check if a condition is a @Deadlock@ or an @STMDeadlock@. -- -- @since 0.9.0.0-isDeadlock :: Failure -> Bool+isDeadlock :: Condition -> Bool isDeadlock Deadlock = True isDeadlock STMDeadlock = True isDeadlock _ = False --- | Check if a failure is an @UncaughtException@+-- | Check if a condition is an @UncaughtException@ -- -- @since 0.9.0.0-isUncaughtException :: Failure -> Bool+isUncaughtException :: Condition -> Bool isUncaughtException (UncaughtException _) = True isUncaughtException _ = False --- | Check if a failure is an @IllegalSubconcurrency@+-------------------------------------------------------------------------------+-- * Errors++-- | An indication that there is a bug in dejafu or you are using it+-- incorrectly. ----- @since 0.9.0.0-isIllegalSubconcurrency :: Failure -> Bool-isIllegalSubconcurrency IllegalSubconcurrency = True-isIllegalSubconcurrency _ = False+-- @since 1.12.0.0+data Error+  = ScheduledBlockedThread+  -- ^ Raised as an exception if the scheduler attempts to schedule a+  -- blocked thread.+  | ScheduledMissingThread+  -- ^ Raised as an exception if the scheduler attempts to schedule a+  -- nonexistent thread.+  | NestedSubconcurrency+  -- ^ Raised as an exception if a @subconcurrency@ is nested inside+  -- another @subconcurrency@ or a @dontCheck@.+  | MultithreadedSubconcurrency+  -- ^ Raised as an exception if @subconcurrency@ is called after+  -- forking threads.+  | LateDontCheck+  -- ^ Raised as an exception if @dontCheck@ is called after the first action.+  deriving (Show, Eq, Ord, Bounded, Enum, Generic) --- | Check if a failure is an @IllegalDontCheck@+instance Exception Error++-- | Check if an error is a scheduler error. ----- @since 1.1.0.0-isIllegalDontCheck :: Failure -> Bool-isIllegalDontCheck IllegalDontCheck = True-isIllegalDontCheck _ = False+-- @since 1.12.0.0+isSchedulerError :: Error -> Bool+isSchedulerError ScheduledBlockedThread = True+isSchedulerError ScheduledMissingThread = True+isSchedulerError _ = False +-- | Check if an error is an incorrect usage of dejafu.+--+-- @since 1.12.0.0+isIncorrectUsage :: Error -> Bool+isIncorrectUsage NestedSubconcurrency = True+isIncorrectUsage MultithreadedSubconcurrency = True+isIncorrectUsage LateDontCheck = True+isIncorrectUsage _ = False+ ------------------------------------------------------------------------------- -- * Schedule bounding @@ -605,7 +615,7 @@ ------------------------------------------------------------------------------- -- * Discarding results and traces --- | An @Either Failure a -> Maybe Discard@ value can be used to+-- | An @Either Condition a -> Maybe Discard@ value can be used to -- selectively discard results. -- -- @since 0.7.1.0@@ -632,7 +642,7 @@ -- -- @since 1.5.1.0 newtype Weaken a = Weaken-  { getWeakDiscarder :: Either Failure a -> Maybe Discard }+  { getWeakDiscarder :: Either Condition a -> Maybe Discard }  instance Semigroup (Weaken a) where   (<>) = divide (\efa -> (efa, efa))@@ -657,9 +667,9 @@ -- -- @since 1.0.0.0 weakenDiscard ::-     (Either Failure a -> Maybe Discard)-  -> (Either Failure a -> Maybe Discard)-  -> Either Failure a -> Maybe Discard+     (Either Condition a -> Maybe Discard)+  -> (Either Condition a -> Maybe Discard)+  -> Either Condition a -> Maybe Discard weakenDiscard d1 d2 =   getWeakDiscarder (Weaken d1 <> Weaken d2) @@ -672,7 +682,7 @@ -- -- @since 1.5.1.0 newtype Strengthen a = Strengthen-  { getStrongDiscarder :: Either Failure a -> Maybe Discard }+  { getStrongDiscarder :: Either Condition a -> Maybe Discard }  instance Semigroup (Strengthen a) where   (<>) = divide (\efa -> (efa, efa))@@ -697,9 +707,9 @@ -- -- @since 1.0.0.0 strengthenDiscard ::-     (Either Failure a -> Maybe Discard)-  -> (Either Failure a -> Maybe Discard)-  -> Either Failure a -> Maybe Discard+     (Either Condition a -> Maybe Discard)+  -> (Either Condition a -> Maybe Discard)+  -> Either Condition a -> Maybe Discard strengthenDiscard d1 d2 =   getStrongDiscarder (Strengthen d1 <> Strengthen d2) 

@@ -76,19 +76,16 @@   insert' _ _ ([]:_) = undefined  ---------------------------------------------------------------------------------- * Failures+-- * Conditions --- | Pretty-print a failure+-- | Pretty-print a condition ----- @since 0.4.0.0-showFail :: Failure -> String-showFail Abort = "[abort]"-showFail Deadlock = "[deadlock]"-showFail STMDeadlock = "[stm-deadlock]"-showFail InternalError = "[internal-error]"-showFail (UncaughtException exc) = "[" ++ displayException exc ++ "]"-showFail IllegalSubconcurrency = "[illegal-subconcurrency]"-showFail IllegalDontCheck = "[illegal-dontcheck]"+-- @since 1.12.0.0+showCondition :: Condition -> String+showCondition Abort = "[abort]"+showCondition Deadlock = "[deadlock]"+showCondition STMDeadlock = "[stm-deadlock]"+showCondition (UncaughtException exc) = "[" ++ displayException exc ++ "]"  ------------------------------------------------------------------------------- -- * Scheduling

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                dejafu-version:             1.11.0.5+version:             1.12.0.0 synopsis:            A library for unit-testing concurrent programs.  description:@@ -33,7 +33,7 @@ source-repository this   type:     git   location: https://github.com/barrucadu/dejafu.git-  tag:      dejafu-1.11.0.5+  tag:      dejafu-1.12.0.0  library   exposed-modules:     Test.DejaFu