From 81bcb5a35152952ca0448789d45d1fc1ccb9bd8f Mon Sep 17 00:00:00 2001 From: Michael Walker Date: Wed, 6 Dec 2017 20:16:11 +0000 Subject: [PATCH] Split up Test.DejaFu.Common --- dejafu-tests/Cases/Properties.hs | 5 +- dejafu/CHANGELOG.markdown | 13 +- dejafu/Test/DejaFu.hs | 28 +- dejafu/Test/DejaFu/Common.hs | 1085 ----------------- dejafu/Test/DejaFu/Conc.hs | 4 +- dejafu/Test/DejaFu/Conc/Internal.hs | 3 +- dejafu/Test/DejaFu/Conc/Internal/Common.hs | 2 +- dejafu/Test/DejaFu/Conc/Internal/Memory.hs | 6 +- dejafu/Test/DejaFu/Conc/Internal/Threading.hs | 3 +- dejafu/Test/DejaFu/Defaults.hs | 2 +- dejafu/Test/DejaFu/Internal.hs | 354 ++++++ dejafu/Test/DejaFu/SCT.hs | 57 +- dejafu/Test/DejaFu/SCT/Internal.hs | 3 +- dejafu/Test/DejaFu/STM.hs | 6 +- dejafu/Test/DejaFu/STM/Internal.hs | 17 +- dejafu/Test/DejaFu/Schedule.hs | 7 +- dejafu/Test/DejaFu/Types.hs | 602 +++++++++ dejafu/Test/DejaFu/Utils.hs | 77 ++ dejafu/dejafu.cabal | 6 +- hunit-dejafu/Test/HUnit/DejaFu.hs | 3 +- tasty-dejafu/Test/Tasty/DejaFu.hs | 3 +- 21 files changed, 1090 insertions(+), 1196 deletions(-) delete mode 100644 dejafu/Test/DejaFu/Common.hs create mode 100644 dejafu/Test/DejaFu/Internal.hs create mode 100644 dejafu/Test/DejaFu/Types.hs create mode 100644 dejafu/Test/DejaFu/Utils.hs diff --git a/dejafu-tests/Cases/Properties.hs b/dejafu-tests/Cases/Properties.hs index ee720cd..40990f4 100644 --- a/dejafu-tests/Cases/Properties.hs +++ b/dejafu-tests/Cases/Properties.hs @@ -12,8 +12,9 @@ import qualified Data.Map as M import Data.Maybe (fromJust, isJust) import Data.Proxy (Proxy(..)) import qualified Data.Sequence as S -import Test.DejaFu.Common (ThreadAction, Lookahead) -import qualified Test.DejaFu.Common as D +import Test.DejaFu.Types (ThreadAction, Lookahead) +import qualified Test.DejaFu.Types as D +import qualified Test.DejaFu.Internal as D import qualified Test.DejaFu.Conc.Internal.Common as D import qualified Test.DejaFu.Conc.Internal.Memory as Mem import qualified Test.DejaFu.SCT.Internal as SCT diff --git a/dejafu/CHANGELOG.markdown b/dejafu/CHANGELOG.markdown index 9470130..ee7dbb3 100644 --- a/dejafu/CHANGELOG.markdown +++ b/dejafu/CHANGELOG.markdown @@ -47,9 +47,20 @@ This project is versioned according to the [Package Versioning Policy](https://p ### Test.DejaFu.Common +- This module has been split up into new Test.DejaFu.Internal, Types, and Utils modules. (#155) + - New `ForkOS` and `IsCurrentThreadBound` thread actions. (#126) + - New `WillForkOS` and `WillIsCurrentThreadBound` lookaheads. (#126) +- The `TTrace` type synonym for `[TAction]` has been removed. + +- The `preEmpCount` function has been removed. + +- New functions `strengthenDiscard` and `weakenDiscard` to combine discard functions. + +- The `Discard` type is now defined here and re-exported from Test.DejaFu.SCT. + ### Test.DejaFu.Conc - The `ConcST` type alias is gone. @@ -73,8 +84,6 @@ This project is versioned according to the [Package Versioning Policy](https://p It is no longer possible to test things in `ST`. -- New functions `strengthenDiscard` and `weakenDiscard` to combine discard functions. - ### Miscellaneous - The minimum supported version of concurrency is now 1.3.0.0. diff --git a/dejafu/Test/DejaFu.hs b/dejafu/Test/DejaFu.hs index 8124607..d1b715d 100644 --- a/dejafu/Test/DejaFu.hs +++ b/dejafu/Test/DejaFu.hs @@ -386,16 +386,16 @@ import Control.Monad.Conc.Class (MonadConc) import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Ref (MonadRef) import Data.Function (on) -import Data.List (intercalate, intersperse, minimumBy) +import Data.List (intercalate, intersperse) import Data.Maybe (catMaybes, isNothing, mapMaybe) -import Data.Ord (comparing) import Data.Profunctor (Profunctor(..)) -import Test.DejaFu.Common import Test.DejaFu.Conc import Test.DejaFu.Defaults import Test.DejaFu.Refinement import Test.DejaFu.SCT +import Test.DejaFu.Types +import Test.DejaFu.Utils ------------------------------------------------------------------------------- @@ -941,25 +941,3 @@ moreThan n (_:rest) = moreThan (n-1) rest -- | Indent every line of a string. indent :: String -> String indent = intercalate "\n" . map ('\t':) . lines - --- | Find the \"simplest\" trace leading to each result. -simplestsBy - :: (Either Failure a -> Either Failure a -> Bool) - -> [(Either Failure a, Trace)] - -> [(Either Failure a, Trace)] -simplestsBy f = map choose . collect where - collect = groupBy' [] (\(a,_) (b,_) -> f a b) - choose = minimumBy . comparing $ \(_, trc) -> - let switchTos = length . filter (\(d,_,_) -> case d of SwitchTo _ -> True; _ -> False) - starts = length . filter (\(d,_,_) -> case d of Start _ -> True; _ -> False) - commits = length . filter (\(_,_,a) -> case a of CommitCRef _ _ -> True; _ -> False) - in (switchTos trc, commits trc, length trc, starts trc) - - groupBy' res _ [] = res - groupBy' res eq (y:ys) = groupBy' (insert' eq y res) eq ys - - insert' _ x [] = [[x]] - insert' eq x (ys@(y:_):yss) - | x `eq` y = (x:ys) : yss - | otherwise = ys : insert' eq x yss - insert' _ _ ([]:_) = undefined diff --git a/dejafu/Test/DejaFu/Common.hs b/dejafu/Test/DejaFu/Common.hs deleted file mode 100644 index 74c7d48..0000000 --- a/dejafu/Test/DejaFu/Common.hs +++ /dev/null @@ -1,1085 +0,0 @@ --- | --- Module : Test.DejaFu.Common --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- Stability : experimental --- Portability : portable --- --- Common types and functions used throughout DejaFu. -module Test.DejaFu.Common - ( -- * Identifiers - ThreadId(..) - , CRefId(..) - , MVarId(..) - , TVarId(..) - , initialThread - -- ** Identifier source - , IdSource(..) - , nextCRId - , nextMVId - , nextTVId - , nextTId - , initialIdSource - - -- * Actions - -- ** Thread actions - , ThreadAction(..) - , isBlock - , tvarsOf - , tvarsWritten - , tvarsRead - -- ** Lookahead - , Lookahead(..) - , rewind - , willRelease - -- ** Simplified actions - , ActionType(..) - , isBarrier - , isCommit - , synchronises - , crefOf - , mvarOf - , simplifyAction - , simplifyLookahead - -- ** STM actions - , TTrace - , TAction(..) - - -- * Traces - , Trace - , Decision(..) - , showTrace - , threadNames - , preEmpCount - - -- * Failures - , Failure(..) - , isInternalError - , isAbort - , isDeadlock - , isUncaughtException - , isIllegalSubconcurrency - , showFail - - -- * Memory models - , MemType(..) - - -- * Miscellaneous - , MonadFailException(..) - , runRefCont - , ehead - , etail - , eidx - , efromJust - , efromList - , fatal - ) where - -import Control.DeepSeq (NFData(..)) -import Control.Exception (Exception(..), MaskingState(..), - SomeException, displayException) -import Control.Monad.Ref (MonadRef(..)) -import Data.Function (on) -import Data.List (intercalate) -import Data.List.NonEmpty (NonEmpty(..)) -import Data.Maybe (fromMaybe, mapMaybe) -import Data.Set (Set) -import qualified Data.Set as S - -------------------------------------------------------------------------------- --- Identifiers - --- | Every live thread has a unique identitifer. --- --- The @Eq@ and @Ord@ instances only consider the int, not the name. --- --- @since 0.4.0.0 -data ThreadId = ThreadId (Maybe String) {-# UNPACK #-} !Int - --- | Previously this was a derived instance. --- --- @since 0.7.2.0 -instance Eq ThreadId where - (ThreadId _ i) == (ThreadId _ j) = i == j - -instance Ord ThreadId where - compare (ThreadId _ i) (ThreadId _ j) = compare i j - -instance Show ThreadId where - show (ThreadId (Just n) _) = n - show (ThreadId Nothing i) = show i - --- | @since 0.5.1.0 -instance NFData ThreadId where - rnf (ThreadId n i) = rnf (n, i) - --- | Every @CRef@ has a unique identifier. --- --- The @Eq@ and @Ord@ instances only consider the int, not the name. --- --- @since 0.4.0.0 -data CRefId = CRefId (Maybe String) {-# UNPACK #-} !Int - --- | Previously this was a derived instance. --- --- @since 0.7.2.0 -instance Eq CRefId where - (CRefId _ i) == (CRefId _ j) = i == j - -instance Ord CRefId where - compare (CRefId _ i) (CRefId _ j) = compare i j - -instance Show CRefId where - show (CRefId (Just n) _) = n - show (CRefId Nothing i) = show i - --- | @since 0.5.1.0 -instance NFData CRefId where - rnf (CRefId n i) = rnf (n, i) - --- | Every @MVar@ has a unique identifier. --- --- The @Eq@ and @Ord@ instances only consider the int, not the name. --- --- @since 0.4.0.0 -data MVarId = MVarId (Maybe String) {-# UNPACK #-} !Int - --- | Previously this was a derived instance. --- --- @since 0.7.2.0 -instance Eq MVarId where - (MVarId _ i) == (MVarId _ j) = i == j - -instance Ord MVarId where - compare (MVarId _ i) (MVarId _ j) = compare i j - -instance Show MVarId where - show (MVarId (Just n) _) = n - show (MVarId Nothing i) = show i - --- | @since 0.5.1.0 -instance NFData MVarId where - rnf (MVarId n i) = rnf (n, i) - --- | Every @TVar@ has a unique identifier. --- --- The @Eq@ and @Ord@ instances only consider the int, not the name. --- --- @since 0.4.0.0 -data TVarId = TVarId (Maybe String) {-# UNPACK #-} !Int - --- | Previously this was a derived instance. --- --- @since 0.7.2.0 -instance Eq TVarId where - (TVarId _ i) == (TVarId _ j) = i == j - -instance Ord TVarId where - compare (TVarId _ i) (TVarId _ j) = compare i j - -instance Show TVarId where - show (TVarId (Just n) _) = n - show (TVarId Nothing i) = show i - --- | @since 0.5.1.0 -instance NFData TVarId where - rnf (TVarId n i) = rnf (n, i) - --- | The ID of the initial thread. --- --- @since 0.4.0.0 -initialThread :: ThreadId -initialThread = ThreadId (Just "main") 0 - ---------------------------------------- --- Identifier source - --- | The number of ID parameters was getting a bit unwieldy, so this --- hides them all away. --- --- @since 0.4.0.0 -data IdSource = Id - { _nextCRId :: Int - , _nextMVId :: Int - , _nextTVId :: Int - , _nextTId :: Int - , _usedCRNames :: [String] - , _usedMVNames :: [String] - , _usedTVNames :: [String] - , _usedTNames :: [String] - } deriving (Eq, Ord, Show) - --- | @since 0.5.1.0 -instance NFData IdSource where - rnf idsource = rnf ( _nextCRId idsource - , _nextMVId idsource - , _nextTVId idsource - , _nextTId idsource - , _usedCRNames idsource - , _usedMVNames idsource - , _usedTVNames idsource - , _usedTNames idsource - ) - --- | Get the next free 'CRefId'. --- --- @since 0.4.0.0 -nextCRId :: String -> IdSource -> (IdSource, CRefId) -nextCRId name idsource = (newIdSource, newCRId) where - newIdSource = idsource { _nextCRId = newId, _usedCRNames = newUsed } - newCRId = CRefId newName newId - newId = _nextCRId idsource + 1 - (newName, newUsed) = nextId name (_usedCRNames idsource) - --- | Get the next free 'MVarId'. --- --- @since 0.4.0.0 -nextMVId :: String -> IdSource -> (IdSource, MVarId) -nextMVId name idsource = (newIdSource, newMVId) where - newIdSource = idsource { _nextMVId = newId, _usedMVNames = newUsed } - newMVId = MVarId newName newId - newId = _nextMVId idsource + 1 - (newName, newUsed) = nextId name (_usedMVNames idsource) - --- | Get the next free 'TVarId'. --- --- @since 0.4.0.0 -nextTVId :: String -> IdSource -> (IdSource, TVarId) -nextTVId name idsource = (newIdSource, newTVId) where - newIdSource = idsource { _nextTVId = newId, _usedTVNames = newUsed } - newTVId = TVarId newName newId - newId = _nextTVId idsource + 1 - (newName, newUsed) = nextId name (_usedTVNames idsource) - --- | Get the next free 'ThreadId'. --- --- @since 0.4.0.0 -nextTId :: String -> IdSource -> (IdSource, ThreadId) -nextTId name idsource = (newIdSource, newTId) where - newIdSource = idsource { _nextTId = newId, _usedTNames = newUsed } - newTId = ThreadId newName newId - newId = _nextTId idsource + 1 - (newName, newUsed) = nextId name (_usedTNames idsource) - --- | The initial ID source. --- --- @since 0.4.0.0 -initialIdSource :: IdSource -initialIdSource = Id 0 0 0 0 [] [] [] [] - -------------------------------------------------------------------------------- --- Actions - ---------------------------------------- --- Thread actions - --- | All the actions that a thread can perform. --- --- @since 1.0.0.0 -data ThreadAction = - Fork ThreadId - -- ^ Start a new thread. - | ForkOS ThreadId - -- ^ Start a new bound thread. - | IsCurrentThreadBound - -- ^ Check if the current thread is bound. - | MyThreadId - -- ^ Get the 'ThreadId' of the current thread. - | GetNumCapabilities Int - -- ^ Get the number of Haskell threads that can run simultaneously. - | SetNumCapabilities Int - -- ^ Set the number of Haskell threads that can run simultaneously. - | Yield - -- ^ Yield the current thread. - | ThreadDelay Int - -- ^ Yield/delay the current thread. - | NewMVar MVarId - -- ^ Create a new 'MVar'. - | PutMVar MVarId [ThreadId] - -- ^ Put into a 'MVar', possibly waking up some threads. - | BlockedPutMVar MVarId - -- ^ Get blocked on a put. - | TryPutMVar MVarId Bool [ThreadId] - -- ^ Try to put into a 'MVar', possibly waking up some threads. - | ReadMVar MVarId - -- ^ Read from a 'MVar'. - | TryReadMVar MVarId Bool - -- ^ Try to read from a 'MVar'. - | BlockedReadMVar MVarId - -- ^ Get blocked on a read. - | TakeMVar MVarId [ThreadId] - -- ^ Take from a 'MVar', possibly waking up some threads. - | BlockedTakeMVar MVarId - -- ^ Get blocked on a take. - | TryTakeMVar MVarId Bool [ThreadId] - -- ^ Try to take from a 'MVar', possibly waking up some threads. - | NewCRef CRefId - -- ^ Create a new 'CRef'. - | ReadCRef CRefId - -- ^ Read from a 'CRef'. - | ReadCRefCas CRefId - -- ^ Read from a 'CRef' for a future compare-and-swap. - | ModCRef CRefId - -- ^ Modify a 'CRef'. - | ModCRefCas CRefId - -- ^ Modify a 'CRef' using a compare-and-swap. - | WriteCRef CRefId - -- ^ Write to a 'CRef' without synchronising. - | CasCRef CRefId Bool - -- ^ Attempt to to a 'CRef' using a compare-and-swap, synchronising - -- it. - | CommitCRef ThreadId CRefId - -- ^ Commit the last write to the given 'CRef' by the given thread, - -- so that all threads can see the updated value. - | STM TTrace [ThreadId] - -- ^ An STM transaction was executed, possibly waking up some - -- threads. - | BlockedSTM TTrace - -- ^ Got blocked in an STM transaction. - | Catching - -- ^ Register a new exception handler - | PopCatching - -- ^ Pop the innermost exception handler from the stack. - | Throw - -- ^ Throw an exception. - | ThrowTo ThreadId - -- ^ Throw an exception to a thread. - | BlockedThrowTo ThreadId - -- ^ Get blocked on a 'throwTo'. - | Killed - -- ^ Killed by an uncaught exception. - | SetMasking Bool MaskingState - -- ^ Set the masking state. If 'True', this is being used to set the - -- masking state to the original state in the argument passed to a - -- 'mask'ed function. - | ResetMasking Bool MaskingState - -- ^ Return to an earlier masking state. If 'True', this is being - -- used to return to the state of the masked block in the argument - -- passed to a 'mask'ed function. - | LiftIO - -- ^ Lift an IO action. Note that this can only happen with - -- 'ConcIO'. - | Return - -- ^ A 'return' or 'pure' action was executed. - | Stop - -- ^ Cease execution and terminate. - | Subconcurrency - -- ^ Start executing an action with @subconcurrency@. - | StopSubconcurrency - -- ^ Stop executing an action with @subconcurrency@. - deriving (Eq, Show) - -instance NFData ThreadAction where - rnf (Fork t) = rnf t - rnf (ForkOS t) = rnf t - rnf (ThreadDelay n) = rnf n - rnf (GetNumCapabilities c) = rnf c - rnf (SetNumCapabilities c) = rnf c - rnf (NewMVar m) = rnf m - rnf (PutMVar m ts) = rnf (m, ts) - rnf (BlockedPutMVar m) = rnf m - rnf (TryPutMVar m b ts) = rnf (m, b, ts) - rnf (ReadMVar m) = rnf m - rnf (TryReadMVar m b) = rnf (m, b) - rnf (BlockedReadMVar m) = rnf m - rnf (TakeMVar m ts) = rnf (m, ts) - rnf (BlockedTakeMVar m) = rnf m - rnf (TryTakeMVar m b ts) = rnf (m, b, ts) - rnf (NewCRef c) = rnf c - rnf (ReadCRef c) = rnf c - rnf (ReadCRefCas c) = rnf c - rnf (ModCRef c) = rnf c - rnf (ModCRefCas c) = rnf c - rnf (WriteCRef c) = rnf c - rnf (CasCRef c b) = rnf (c, b) - rnf (CommitCRef t c) = rnf (t, c) - rnf (STM tr ts) = rnf (tr, ts) - rnf (BlockedSTM tr) = rnf tr - rnf (ThrowTo t) = rnf t - rnf (BlockedThrowTo t) = rnf t - rnf (SetMasking b m) = b `seq` m `seq` () - rnf (ResetMasking b m) = b `seq` m `seq` () - rnf a = a `seq` () - --- | Check if a @ThreadAction@ immediately blocks. --- --- @since 0.4.0.0 -isBlock :: ThreadAction -> Bool -isBlock (BlockedThrowTo _) = True -isBlock (BlockedTakeMVar _) = True -isBlock (BlockedReadMVar _) = True -isBlock (BlockedPutMVar _) = True -isBlock (BlockedSTM _) = True -isBlock _ = False - --- | Get the @TVar@s affected by a @ThreadAction@. --- --- @since 0.4.0.0 -tvarsOf :: ThreadAction -> Set TVarId -tvarsOf act = tvarsRead act `S.union` tvarsWritten act - --- | Get the @TVar@s a transaction wrote to (or would have, if it --- didn't @retry@). --- --- @since 0.9.0.2 -tvarsWritten :: ThreadAction -> Set TVarId -tvarsWritten act = S.fromList $ case act of - STM trc _ -> concatMap tvarsOf' trc - BlockedSTM trc -> concatMap tvarsOf' trc - _ -> [] - - where - tvarsOf' (TWrite tv) = [tv] - tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) - tvarsOf' (TCatch ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) - tvarsOf' _ = [] - --- | Get the @TVar@s a transaction read from. --- --- @since 0.9.0.2 -tvarsRead :: ThreadAction -> Set TVarId -tvarsRead act = S.fromList $ case act of - STM trc _ -> concatMap tvarsOf' trc - BlockedSTM trc -> concatMap tvarsOf' trc - _ -> [] - - where - tvarsOf' (TRead tv) = [tv] - tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) - tvarsOf' (TCatch ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) - tvarsOf' _ = [] - ---------------------------------------- --- Lookahead - --- | A one-step look-ahead at what a thread will do next. --- --- @since 1.0.0.0 -data Lookahead = - WillFork - -- ^ Will start a new thread. - | WillForkOS - -- ^ Will start a new bound thread. - | WillIsCurrentThreadBound - -- ^ Will check if the current thread is bound. - | WillMyThreadId - -- ^ Will get the 'ThreadId'. - | WillGetNumCapabilities - -- ^ Will get the number of Haskell threads that can run - -- simultaneously. - | WillSetNumCapabilities Int - -- ^ Will set the number of Haskell threads that can run - -- simultaneously. - | WillYield - -- ^ Will yield the current thread. - | WillThreadDelay Int - -- ^ Will yield/delay the current thread. - | WillNewMVar - -- ^ Will create a new 'MVar'. - | WillPutMVar MVarId - -- ^ Will put into a 'MVar', possibly waking up some threads. - | WillTryPutMVar MVarId - -- ^ Will try to put into a 'MVar', possibly waking up some threads. - | WillReadMVar MVarId - -- ^ Will read from a 'MVar'. - | WillTryReadMVar MVarId - -- ^ Will try to read from a 'MVar'. - | WillTakeMVar MVarId - -- ^ Will take from a 'MVar', possibly waking up some threads. - | WillTryTakeMVar MVarId - -- ^ Will try to take from a 'MVar', possibly waking up some threads. - | WillNewCRef - -- ^ Will create a new 'CRef'. - | WillReadCRef CRefId - -- ^ Will read from a 'CRef'. - | WillReadCRefCas CRefId - -- ^ Will read from a 'CRef' for a future compare-and-swap. - | WillModCRef CRefId - -- ^ Will modify a 'CRef'. - | WillModCRefCas CRefId - -- ^ Will modify a 'CRef' using a compare-and-swap. - | WillWriteCRef CRefId - -- ^ Will write to a 'CRef' without synchronising. - | WillCasCRef CRefId - -- ^ Will attempt to to a 'CRef' using a compare-and-swap, - -- synchronising it. - | WillCommitCRef ThreadId CRefId - -- ^ Will commit the last write by the given thread to the 'CRef'. - | WillSTM - -- ^ Will execute an STM transaction, possibly waking up some - -- threads. - | WillCatching - -- ^ Will register a new exception handler - | WillPopCatching - -- ^ Will pop the innermost exception handler from the stack. - | WillThrow - -- ^ Will throw an exception. - | WillThrowTo ThreadId - -- ^ Will throw an exception to a thread. - | WillSetMasking Bool MaskingState - -- ^ Will set the masking state. If 'True', this is being used to - -- set the masking state to the original state in the argument - -- passed to a 'mask'ed function. - | WillResetMasking Bool MaskingState - -- ^ Will return to an earlier masking state. If 'True', this is - -- being used to return to the state of the masked block in the - -- argument passed to a 'mask'ed function. - | WillLiftIO - -- ^ Will lift an IO action. Note that this can only happen with - -- 'ConcIO'. - | WillReturn - -- ^ Will execute a 'return' or 'pure' action. - | WillStop - -- ^ Will cease execution and terminate. - | WillSubconcurrency - -- ^ Will execute an action with @subconcurrency@. - | WillStopSubconcurrency - -- ^ Will stop executing an extion with @subconcurrency@. - deriving (Eq, Show) - -instance NFData Lookahead where - rnf (WillThreadDelay n) = rnf n - rnf (WillSetNumCapabilities c) = rnf c - rnf (WillPutMVar m) = rnf m - rnf (WillTryPutMVar m) = rnf m - rnf (WillReadMVar m) = rnf m - rnf (WillTryReadMVar m) = rnf m - rnf (WillTakeMVar m) = rnf m - rnf (WillTryTakeMVar m) = rnf m - rnf (WillReadCRef c) = rnf c - rnf (WillReadCRefCas c) = rnf c - rnf (WillModCRef c) = rnf c - rnf (WillModCRefCas c) = rnf c - rnf (WillWriteCRef c) = rnf c - rnf (WillCasCRef c) = rnf c - rnf (WillCommitCRef t c) = rnf (t, c) - rnf (WillThrowTo t) = rnf t - rnf (WillSetMasking b m) = b `seq` m `seq` () - rnf (WillResetMasking b m) = b `seq` m `seq` () - rnf l = l `seq` () - --- | Convert a 'ThreadAction' into a 'Lookahead': \"rewind\" what has --- happened. 'Killed' has no 'Lookahead' counterpart. --- --- @since 0.4.0.0 -rewind :: ThreadAction -> Maybe Lookahead -rewind (Fork _) = Just WillFork -rewind (ForkOS _) = Just WillForkOS -rewind IsCurrentThreadBound = Just WillIsCurrentThreadBound -rewind MyThreadId = Just WillMyThreadId -rewind (GetNumCapabilities _) = Just WillGetNumCapabilities -rewind (SetNumCapabilities i) = Just (WillSetNumCapabilities i) -rewind Yield = Just WillYield -rewind (ThreadDelay n) = Just (WillThreadDelay n) -rewind (NewMVar _) = Just WillNewMVar -rewind (PutMVar c _) = Just (WillPutMVar c) -rewind (BlockedPutMVar c) = Just (WillPutMVar c) -rewind (TryPutMVar c _ _) = Just (WillTryPutMVar c) -rewind (ReadMVar c) = Just (WillReadMVar c) -rewind (BlockedReadMVar c) = Just (WillReadMVar c) -rewind (TryReadMVar c _) = Just (WillTryReadMVar c) -rewind (TakeMVar c _) = Just (WillTakeMVar c) -rewind (BlockedTakeMVar c) = Just (WillTakeMVar c) -rewind (TryTakeMVar c _ _) = Just (WillTryTakeMVar c) -rewind (NewCRef _) = Just WillNewCRef -rewind (ReadCRef c) = Just (WillReadCRef c) -rewind (ReadCRefCas c) = Just (WillReadCRefCas c) -rewind (ModCRef c) = Just (WillModCRef c) -rewind (ModCRefCas c) = Just (WillModCRefCas c) -rewind (WriteCRef c) = Just (WillWriteCRef c) -rewind (CasCRef c _) = Just (WillCasCRef c) -rewind (CommitCRef t c) = Just (WillCommitCRef t c) -rewind (STM _ _) = Just WillSTM -rewind (BlockedSTM _) = Just WillSTM -rewind Catching = Just WillCatching -rewind PopCatching = Just WillPopCatching -rewind Throw = Just WillThrow -rewind (ThrowTo t) = Just (WillThrowTo t) -rewind (BlockedThrowTo t) = Just (WillThrowTo t) -rewind Killed = Nothing -rewind (SetMasking b m) = Just (WillSetMasking b m) -rewind (ResetMasking b m) = Just (WillResetMasking b m) -rewind LiftIO = Just WillLiftIO -rewind Return = Just WillReturn -rewind Stop = Just WillStop -rewind Subconcurrency = Just WillSubconcurrency -rewind StopSubconcurrency = Just WillStopSubconcurrency - --- | Check if an operation could enable another thread. --- --- @since 0.4.0.0 -willRelease :: Lookahead -> Bool -willRelease WillFork = True -willRelease WillForkOS = True -willRelease WillYield = True -willRelease (WillThreadDelay _) = True -willRelease (WillPutMVar _) = True -willRelease (WillTryPutMVar _) = True -willRelease (WillReadMVar _) = True -willRelease (WillTakeMVar _) = True -willRelease (WillTryTakeMVar _) = True -willRelease WillSTM = True -willRelease WillThrow = True -willRelease (WillSetMasking _ _) = True -willRelease (WillResetMasking _ _) = True -willRelease WillStop = True -willRelease _ = False - ---------------------------------------- --- Simplified actions - --- | A simplified view of the possible actions a thread can perform. --- --- @since 0.4.0.0 -data ActionType = - UnsynchronisedRead CRefId - -- ^ A 'readCRef' or a 'readForCAS'. - | UnsynchronisedWrite CRefId - -- ^ A 'writeCRef'. - | UnsynchronisedOther - -- ^ Some other action which doesn't require cross-thread - -- communication. - | PartiallySynchronisedCommit CRefId - -- ^ A commit. - | PartiallySynchronisedWrite CRefId - -- ^ A 'casCRef' - | PartiallySynchronisedModify CRefId - -- ^ A 'modifyCRefCAS' - | SynchronisedModify CRefId - -- ^ An 'atomicModifyCRef'. - | SynchronisedRead MVarId - -- ^ A 'readMVar' or 'takeMVar' (or @try@/@blocked@ variants). - | SynchronisedWrite MVarId - -- ^ A 'putMVar' (or @try@/@blocked@ variant). - | SynchronisedOther - -- ^ Some other action which does require cross-thread - -- communication. - deriving (Eq, Show) - --- | @since 0.5.1.0 -instance NFData ActionType where - rnf (UnsynchronisedRead c) = rnf c - rnf (UnsynchronisedWrite c) = rnf c - rnf (PartiallySynchronisedCommit c) = rnf c - rnf (PartiallySynchronisedWrite c) = rnf c - rnf (PartiallySynchronisedModify c) = rnf c - rnf (SynchronisedModify c) = rnf c - rnf (SynchronisedRead m) = rnf m - rnf (SynchronisedWrite m) = rnf m - rnf a = a `seq` () - --- | Check if an action imposes a write barrier. --- --- @since 0.4.0.0 -isBarrier :: ActionType -> Bool -isBarrier (SynchronisedModify _) = True -isBarrier (SynchronisedRead _) = True -isBarrier (SynchronisedWrite _) = True -isBarrier SynchronisedOther = True -isBarrier _ = False - --- | Check if an action commits a given 'CRef'. --- --- @since 0.4.0.0 -isCommit :: ActionType -> CRefId -> Bool -isCommit (PartiallySynchronisedCommit c) r = c == r -isCommit (PartiallySynchronisedWrite c) r = c == r -isCommit (PartiallySynchronisedModify c) r = c == r -isCommit _ _ = False - --- | Check if an action synchronises a given 'CRef'. --- --- @since 0.4.0.0 -synchronises :: ActionType -> CRefId -> Bool -synchronises a r = isCommit a r || isBarrier a - --- | Get the 'CRef' affected. --- --- @since 0.4.0.0 -crefOf :: ActionType -> Maybe CRefId -crefOf (UnsynchronisedRead r) = Just r -crefOf (UnsynchronisedWrite r) = Just r -crefOf (SynchronisedModify r) = Just r -crefOf (PartiallySynchronisedCommit r) = Just r -crefOf (PartiallySynchronisedWrite r) = Just r -crefOf (PartiallySynchronisedModify r) = Just r -crefOf _ = Nothing - --- | Get the 'MVar' affected. --- --- @since 0.4.0.0 -mvarOf :: ActionType -> Maybe MVarId -mvarOf (SynchronisedRead c) = Just c -mvarOf (SynchronisedWrite c) = Just c -mvarOf _ = Nothing - --- | Throw away information from a 'ThreadAction' and give a --- simplified view of what is happening. --- --- This is used in the SCT code to help determine interesting --- alternative scheduling decisions. --- --- @since 0.4.0.0 -simplifyAction :: ThreadAction -> ActionType -simplifyAction = maybe UnsynchronisedOther simplifyLookahead . rewind - --- | Variant of 'simplifyAction' that takes a 'Lookahead'. --- --- @since 0.4.0.0 -simplifyLookahead :: Lookahead -> ActionType -simplifyLookahead (WillPutMVar c) = SynchronisedWrite c -simplifyLookahead (WillTryPutMVar c) = SynchronisedWrite c -simplifyLookahead (WillReadMVar c) = SynchronisedRead c -simplifyLookahead (WillTryReadMVar c) = SynchronisedRead c -simplifyLookahead (WillTakeMVar c) = SynchronisedRead c -simplifyLookahead (WillTryTakeMVar c) = SynchronisedRead c -simplifyLookahead (WillReadCRef r) = UnsynchronisedRead r -simplifyLookahead (WillReadCRefCas r) = UnsynchronisedRead r -simplifyLookahead (WillModCRef r) = SynchronisedModify r -simplifyLookahead (WillModCRefCas r) = PartiallySynchronisedModify r -simplifyLookahead (WillWriteCRef r) = UnsynchronisedWrite r -simplifyLookahead (WillCasCRef r) = PartiallySynchronisedWrite r -simplifyLookahead (WillCommitCRef _ r) = PartiallySynchronisedCommit r -simplifyLookahead WillSTM = SynchronisedOther -simplifyLookahead (WillThrowTo _) = SynchronisedOther -simplifyLookahead _ = UnsynchronisedOther - ---------------------------------------- --- STM actions - --- | A trace of an STM transaction is just a list of actions that --- occurred, as there are no scheduling decisions to make. --- --- @since 0.4.0.0 -type TTrace = [TAction] - --- | All the actions that an STM transaction can perform. --- --- @since 0.8.0.0 -data TAction = - TNew TVarId - -- ^ Create a new @TVar@ - | TRead TVarId - -- ^ Read from a @TVar@. - | TWrite TVarId - -- ^ Write to a @TVar@. - | TRetry - -- ^ Abort and discard effects. - | TOrElse TTrace (Maybe TTrace) - -- ^ Execute a transaction until it succeeds (@STMStop@) or aborts - -- (@STMRetry@) and, if it aborts, execute the other transaction. - | TThrow - -- ^ Throw an exception, abort, and discard effects. - | TCatch TTrace (Maybe TTrace) - -- ^ Execute a transaction until it succeeds (@STMStop@) or aborts - -- (@STMThrow@). If the exception is of the appropriate type, it is - -- handled and execution continues; otherwise aborts, propagating - -- the exception upwards. - | TStop - -- ^ Terminate successfully and commit effects. - deriving (Eq, Show) - --- | @since 0.5.1.0 -instance NFData TAction where - rnf (TRead t) = rnf t - rnf (TWrite t) = rnf t - rnf (TOrElse tr mtr) = rnf (tr, mtr) - rnf (TCatch tr mtr) = rnf (tr, mtr) - rnf ta = ta `seq` () - -------------------------------------------------------------------------------- --- Traces - --- | One of the outputs of the runner is a @Trace@, which is a log of --- decisions made, all the unblocked threads and what they would do, --- and the action a thread took in its step. --- --- @since 0.8.0.0 -type Trace - = [(Decision, [(ThreadId, Lookahead)], ThreadAction)] - --- | Scheduling decisions are based on the state of the running --- program, and so we can capture some of that state in recording what --- specific decision we made. --- --- @since 0.5.0.0 -data Decision = - Start ThreadId - -- ^ Start a new thread, because the last was blocked (or it's the - -- start of computation). - | Continue - -- ^ Continue running the last thread for another step. - | SwitchTo ThreadId - -- ^ Pre-empt the running thread, and switch to another. - deriving (Eq, Show) - --- | @since 0.5.1.0 -instance NFData Decision where - rnf (Start t) = rnf t - rnf (SwitchTo t) = rnf t - rnf d = d `seq` () - --- | Pretty-print a trace, including a key of the thread IDs (not --- including thread 0). Each line of the key is indented by two --- spaces. --- --- @since 0.5.0.0 -showTrace :: Trace -> String -showTrace [] = "" -showTrace trc = intercalate "\n" $ go False trc : strkey where - go _ ((_,_,CommitCRef _ _):rest) = "C-" ++ go False rest - go _ ((Start (ThreadId _ i),_,a):rest) = "S" ++ show i ++ "-" ++ go (didYield a) rest - go y ((SwitchTo (ThreadId _ i),_,a):rest) = (if y then "p" else "P") ++ show i ++ "-" ++ go (didYield a) rest - go _ ((Continue,_,a):rest) = '-' : go (didYield a) rest - go _ _ = "" - - strkey = - [" " ++ show i ++ ": " ++ name | (i, name) <- threadNames trc] - - didYield Yield = True - didYield (ThreadDelay _) = True - didYield _ = False - --- | Get all named threads in the trace. --- --- @since 0.7.3.0 -threadNames :: Trace -> [(Int, String)] -threadNames = mapMaybe go where - go (_, _, Fork (ThreadId (Just name) i)) = Just (i, name) - go (_, _, ForkOS (ThreadId (Just name) i)) = Just (i, name) - go _ = Nothing - --- | Count the number of pre-emptions in a schedule prefix. --- --- Commit threads complicate this a bit. Conceptually, commits are --- happening truly in parallel, nondeterministically. The commit --- thread implementation is just there to unify the two sources of --- nondeterminism: commit timing and thread scheduling. --- --- SO, we don't count a switch TO a commit thread as a --- preemption. HOWEVER, the switch FROM a commit thread counts as a --- preemption if it is not to the thread that the commit interrupted. --- --- @since 0.5.0.0 -preEmpCount :: [(Decision, ThreadAction)] - -> (Decision, Lookahead) - -> Int -preEmpCount (x:xs) (d, _) = go initialThread x xs where - go _ (_, Yield) (r@(SwitchTo t, _):rest) = go t r rest - go _ (_, ThreadDelay _) (r@(SwitchTo t, _):rest) = go t r rest - go tid prior (r@(SwitchTo t, _):rest) - | isCommitThread t = go tid prior (skip rest) - | otherwise = 1 + go t r rest - go _ _ (r@(Start t, _):rest) = go t r rest - go tid _ (r@(Continue, _):rest) = go tid r rest - go _ prior [] = case (prior, d) of - ((_, Yield), SwitchTo _) -> 0 - ((_, ThreadDelay _), SwitchTo _) -> 0 - (_, SwitchTo _) -> 1 - _ -> 0 - - -- Commit threads have negative thread IDs for easy identification. - isCommitThread = (< initialThread) - - -- Skip until the next context switch. - skip = dropWhile (not . isContextSwitch . fst) - isContextSwitch Continue = False - isContextSwitch _ = True -preEmpCount [] _ = 0 - -------------------------------------------------------------------------------- --- Failures - - --- | An indication of how a concurrent computation failed. --- --- The @Eq@, @Ord@, and @NFData@ instances compare/evaluate the --- exception with @show@ in the @UncaughtException@ case. --- --- @since 0.9.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 - -- ^ 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 - -- has executed for too long, or there have been too many yields). - | Deadlock - -- ^ Every thread is blocked, and the main thread is /not/ blocked - -- in an STM transaction. - | STMDeadlock - -- ^ Every thread is blocked, and the main thread is blocked in an - -- 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. - deriving Show - -instance Eq Failure where - (==) = (==) `on` _other - -instance Ord Failure where - compare = compare `on` _other - -instance NFData Failure where - rnf = rnf . _other - --- | Convert failures into a different representation we can Eq / Ord --- / NFData. -_other :: Failure -> (Int, Maybe String) -_other InternalError = (0, Nothing) -_other Abort = (1, Nothing) -_other Deadlock = (2, Nothing) -_other STMDeadlock = (3, Nothing) -_other (UncaughtException e) = (4, Just (show e)) -_other IllegalSubconcurrency = (5, Nothing) - --- | Pretty-print a failure --- --- @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]" - --- | 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@. --- --- @since 0.9.0.0 -isAbort :: Failure -> Bool -isAbort Abort = True -isAbort _ = False - --- | Check if a failure is a @Deadlock@ or an @STMDeadlock@. --- --- @since 0.9.0.0 -isDeadlock :: Failure -> Bool -isDeadlock Deadlock = True -isDeadlock STMDeadlock = True -isDeadlock _ = False - --- | Check if a failure is an @UncaughtException@ --- --- @since 0.9.0.0 -isUncaughtException :: Failure -> Bool -isUncaughtException (UncaughtException _) = True -isUncaughtException _ = False - --- | Check if a failure is an @IllegalSubconcurrency@ --- --- @since 0.9.0.0 -isIllegalSubconcurrency :: Failure -> Bool -isIllegalSubconcurrency IllegalSubconcurrency = True -isIllegalSubconcurrency _ = False - -------------------------------------------------------------------------------- --- Memory Models - --- | The memory model to use for non-synchronised 'CRef' operations. --- --- @since 0.4.0.0 -data MemType = - SequentialConsistency - -- ^ The most intuitive model: a program behaves as a simple - -- interleaving of the actions in different threads. When a 'CRef' - -- is written to, that write is immediately visible to all threads. - | TotalStoreOrder - -- ^ Each thread has a write buffer. A thread sees its writes - -- immediately, but other threads will only see writes when they are - -- committed, which may happen later. Writes are committed in the - -- same order that they are created. - | PartialStoreOrder - -- ^ Each 'CRef' has a write buffer. A thread sees its writes - -- immediately, but other threads will only see writes when they are - -- committed, which may happen later. Writes to different 'CRef's - -- are not necessarily committed in the same order that they are - -- created. - deriving (Eq, Show, Read, Ord, Enum, Bounded) - --- | @since 0.5.1.0 -instance NFData MemType where - rnf m = m `seq` () - -------------------------------------------------------------------------------- --- Miscellaneous - --- | An exception for errors in testing caused by use of 'fail'. -newtype MonadFailException = MonadFailException String - deriving Show - -instance Exception MonadFailException - --- | Run with a continuation that writes its value into a reference, --- returning the computation and the reference. Using the reference --- is non-blocking, it is up to you to ensure you wait sufficiently. -runRefCont :: MonadRef r n => (n () -> x) -> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, r (Maybe b)) -runRefCont act f k = do - ref <- newRef Nothing - let c = k (act . writeRef ref . f) - pure (c, ref) - --- | 'head' but with a better error message if it fails. Use this --- only where it shouldn't fail! -ehead :: String -> [a] -> a -ehead _ (x:_) = x -ehead src _ = fatal src "head: empty list" - --- | 'tail' but with a better error message if it fails. Use this --- only where it shouldn't fail! -etail :: String -> [a] -> [a] -etail _ (_:xs) = xs -etail src _ = fatal src "tail: empty list" - --- | '(!!)' but with a better error message if it fails. Use this --- only where it shouldn't fail! -eidx :: String -> [a] -> Int -> a -eidx src xs i - | i < length xs = xs !! i - | otherwise = fatal src "(!!): index too large" - --- | 'fromJust' but with a better error message if it fails. Use this --- only where it shouldn't fail! -efromJust :: String -> Maybe a -> a -efromJust _ (Just x) = x -efromJust src _ = fatal src "fromJust: Nothing" - --- | 'fromList' but with a better error message if it fails. Use this --- only where it shouldn't fail! -efromList :: String -> [a] -> NonEmpty a -efromList _ (x:xs) = x:|xs -efromList src _ = fatal src "fromList: empty list" - --- | 'error' but saying where it came from -fatal :: String -> String -> a -fatal src msg = error ("(dejafu: " ++ src ++ ") " ++ msg) - - -------------------------------------------------------------------------------- --- Utilities - --- | Helper for @next*@ -nextId :: String -> [String] -> (Maybe String, [String]) -nextId name used = (newName, newUsed) where - newName - | null name = Nothing - | occurrences > 0 = Just (name ++ "-" ++ show occurrences) - | otherwise = Just name - newUsed - | null name = used - | otherwise = name : used - occurrences = length (filter (==name) used) diff --git a/dejafu/Test/DejaFu/Conc.hs b/dejafu/Test/DejaFu/Conc.hs index 6a9d2b8..14407b1 100755 --- a/dejafu/Test/DejaFu/Conc.hs +++ b/dejafu/Test/DejaFu/Conc.hs @@ -56,10 +56,12 @@ import Data.IORef (IORef) import Test.DejaFu.Schedule import qualified Control.Monad.Conc.Class as C -import Test.DejaFu.Common import Test.DejaFu.Conc.Internal import Test.DejaFu.Conc.Internal.Common +import Test.DejaFu.Internal import Test.DejaFu.STM +import Test.DejaFu.Types +import Test.DejaFu.Utils #if MIN_VERSION_base(4,9,0) import qualified Control.Monad.Fail as Fail diff --git a/dejafu/Test/DejaFu/Conc/Internal.hs b/dejafu/Test/DejaFu/Conc/Internal.hs index 9aa3ffc..df41d35 100755 --- a/dejafu/Test/DejaFu/Conc/Internal.hs +++ b/dejafu/Test/DejaFu/Conc/Internal.hs @@ -29,13 +29,14 @@ import Data.Monoid ((<>)) import Data.Sequence (Seq, (<|)) import qualified Data.Sequence as Seq -import Test.DejaFu.Common import Test.DejaFu.Conc.Internal.Common import Test.DejaFu.Conc.Internal.Memory import Test.DejaFu.Conc.Internal.Threading +import Test.DejaFu.Internal import Test.DejaFu.Schedule import Test.DejaFu.STM (Result(..), runTransaction) +import Test.DejaFu.Types -------------------------------------------------------------------------------- -- * Execution diff --git a/dejafu/Test/DejaFu/Conc/Internal/Common.hs b/dejafu/Test/DejaFu/Conc/Internal/Common.hs index 3b5fa65..4b1a2ae 100755 --- a/dejafu/Test/DejaFu/Conc/Internal/Common.hs +++ b/dejafu/Test/DejaFu/Conc/Internal/Common.hs @@ -16,8 +16,8 @@ module Test.DejaFu.Conc.Internal.Common where import Control.Exception (Exception, MaskingState(..)) import Data.Map.Strict (Map) -import Test.DejaFu.Common import Test.DejaFu.STM (STMLike) +import Test.DejaFu.Types #if MIN_VERSION_base(4,9,0) import qualified Control.Monad.Fail as Fail diff --git a/dejafu/Test/DejaFu/Conc/Internal/Memory.hs b/dejafu/Test/DejaFu/Conc/Internal/Memory.hs index d1328e4..28409f4 100755 --- a/dejafu/Test/DejaFu/Conc/Internal/Memory.hs +++ b/dejafu/Test/DejaFu/Conc/Internal/Memory.hs @@ -26,16 +26,16 @@ module Test.DejaFu.Conc.Internal.Memory where import Control.Monad.Ref (MonadRef, readRef, writeRef) import Data.Map.Strict (Map) +import qualified Data.Map.Strict as M import Data.Maybe (maybeToList) import Data.Monoid ((<>)) import Data.Sequence (Seq, ViewL(..), singleton, viewl, (><)) -import Test.DejaFu.Common import Test.DejaFu.Conc.Internal.Common import Test.DejaFu.Conc.Internal.Threading - -import qualified Data.Map.Strict as M +import Test.DejaFu.Internal +import Test.DejaFu.Types -------------------------------------------------------------------------------- -- * Manipulating @CRef@s diff --git a/dejafu/Test/DejaFu/Conc/Internal/Threading.hs b/dejafu/Test/DejaFu/Conc/Internal/Threading.hs index f71f223..0eb141e 100644 --- a/dejafu/Test/DejaFu/Conc/Internal/Threading.hs +++ b/dejafu/Test/DejaFu/Conc/Internal/Threading.hs @@ -20,8 +20,9 @@ import Data.List (intersect) import Data.Map.Strict (Map) import Data.Maybe (isJust) -import Test.DejaFu.Common import Test.DejaFu.Conc.Internal.Common +import Test.DejaFu.Internal +import Test.DejaFu.Types import qualified Data.Map.Strict as M diff --git a/dejafu/Test/DejaFu/Defaults.hs b/dejafu/Test/DejaFu/Defaults.hs index 21be1aa..6917186 100644 --- a/dejafu/Test/DejaFu/Defaults.hs +++ b/dejafu/Test/DejaFu/Defaults.hs @@ -9,8 +9,8 @@ -- Default parameters for test execution. module Test.DejaFu.Defaults where -import Test.DejaFu.Common import Test.DejaFu.SCT +import Test.DejaFu.Types -- | A default way to execute concurrent programs: systematically -- using 'defaultBounds'. diff --git a/dejafu/Test/DejaFu/Internal.hs b/dejafu/Test/DejaFu/Internal.hs new file mode 100644 index 0000000..e432cb3 --- /dev/null +++ b/dejafu/Test/DejaFu/Internal.hs @@ -0,0 +1,354 @@ +-- | +-- Module : Test.DejaFu.Internal +-- Copyright : (c) 2017 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : portable +-- +-- Internal types and functions used throughout DejaFu. This module +-- is NOT considered to form part of the public interface of this +-- library. +module Test.DejaFu.Internal where + +import Control.DeepSeq (NFData(..)) +import Control.Monad.Ref (MonadRef(..)) +import Data.List.NonEmpty (NonEmpty(..)) +import Data.Maybe (fromMaybe) +import Data.Set (Set) +import qualified Data.Set as S + +import Test.DejaFu.Types + +------------------------------------------------------------------------------- +-- * Identifiers + +-- | The number of ID parameters was getting a bit unwieldy, so this +-- hides them all away. +data IdSource = Id + { _nextCRId :: Int + , _nextMVId :: Int + , _nextTVId :: Int + , _nextTId :: Int + , _usedCRNames :: [String] + , _usedMVNames :: [String] + , _usedTVNames :: [String] + , _usedTNames :: [String] + } deriving (Eq, Ord, Show) + +instance NFData IdSource where + rnf idsource = rnf ( _nextCRId idsource + , _nextMVId idsource + , _nextTVId idsource + , _nextTId idsource + , _usedCRNames idsource + , _usedMVNames idsource + , _usedTVNames idsource + , _usedTNames idsource + ) + +-- | Get the next free 'CRefId'. +nextCRId :: String -> IdSource -> (IdSource, CRefId) +nextCRId name idsource = (newIdSource, newCRId) where + newIdSource = idsource { _nextCRId = newId, _usedCRNames = newUsed } + newCRId = CRefId newName newId + newId = _nextCRId idsource + 1 + (newName, newUsed) = nextId name (_usedCRNames idsource) + +-- | Get the next free 'MVarId'. +nextMVId :: String -> IdSource -> (IdSource, MVarId) +nextMVId name idsource = (newIdSource, newMVId) where + newIdSource = idsource { _nextMVId = newId, _usedMVNames = newUsed } + newMVId = MVarId newName newId + newId = _nextMVId idsource + 1 + (newName, newUsed) = nextId name (_usedMVNames idsource) + +-- | Get the next free 'TVarId'. +nextTVId :: String -> IdSource -> (IdSource, TVarId) +nextTVId name idsource = (newIdSource, newTVId) where + newIdSource = idsource { _nextTVId = newId, _usedTVNames = newUsed } + newTVId = TVarId newName newId + newId = _nextTVId idsource + 1 + (newName, newUsed) = nextId name (_usedTVNames idsource) + +-- | Get the next free 'ThreadId'. +nextTId :: String -> IdSource -> (IdSource, ThreadId) +nextTId name idsource = (newIdSource, newTId) where + newIdSource = idsource { _nextTId = newId, _usedTNames = newUsed } + newTId = ThreadId newName newId + newId = _nextTId idsource + 1 + (newName, newUsed) = nextId name (_usedTNames idsource) + +-- | Helper for @next*@ +nextId :: String -> [String] -> (Maybe String, [String]) +nextId name used = (newName, newUsed) where + newName + | null name = Nothing + | occurrences > 0 = Just (name ++ "-" ++ show occurrences) + | otherwise = Just name + newUsed + | null name = used + | otherwise = name : used + occurrences = length (filter (==name) used) + +-- | The initial ID source. +initialIdSource :: IdSource +initialIdSource = Id 0 0 0 0 [] [] [] [] + +------------------------------------------------------------------------------- +-- * Actions + +-- | Check if a @ThreadAction@ immediately blocks. +isBlock :: ThreadAction -> Bool +isBlock (BlockedThrowTo _) = True +isBlock (BlockedTakeMVar _) = True +isBlock (BlockedReadMVar _) = True +isBlock (BlockedPutMVar _) = True +isBlock (BlockedSTM _) = True +isBlock _ = False + +-- | Get the @TVar@s affected by a @ThreadAction@. +tvarsOf :: ThreadAction -> Set TVarId +tvarsOf act = tvarsRead act `S.union` tvarsWritten act + +-- | Get the @TVar@s a transaction wrote to (or would have, if it +-- didn't @retry@). +tvarsWritten :: ThreadAction -> Set TVarId +tvarsWritten act = S.fromList $ case act of + STM trc _ -> concatMap tvarsOf' trc + BlockedSTM trc -> concatMap tvarsOf' trc + _ -> [] + + where + tvarsOf' (TWrite tv) = [tv] + tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) + tvarsOf' (TCatch ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) + tvarsOf' _ = [] + +-- | Get the @TVar@s a transaction read from. +tvarsRead :: ThreadAction -> Set TVarId +tvarsRead act = S.fromList $ case act of + STM trc _ -> concatMap tvarsOf' trc + BlockedSTM trc -> concatMap tvarsOf' trc + _ -> [] + + where + tvarsOf' (TRead tv) = [tv] + tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) + tvarsOf' (TCatch ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) + tvarsOf' _ = [] + +-- | Convert a 'ThreadAction' into a 'Lookahead': \"rewind\" what has +-- happened. 'Killed' has no 'Lookahead' counterpart. +rewind :: ThreadAction -> Maybe Lookahead +rewind (Fork _) = Just WillFork +rewind (ForkOS _) = Just WillForkOS +rewind IsCurrentThreadBound = Just WillIsCurrentThreadBound +rewind MyThreadId = Just WillMyThreadId +rewind (GetNumCapabilities _) = Just WillGetNumCapabilities +rewind (SetNumCapabilities i) = Just (WillSetNumCapabilities i) +rewind Yield = Just WillYield +rewind (ThreadDelay n) = Just (WillThreadDelay n) +rewind (NewMVar _) = Just WillNewMVar +rewind (PutMVar c _) = Just (WillPutMVar c) +rewind (BlockedPutMVar c) = Just (WillPutMVar c) +rewind (TryPutMVar c _ _) = Just (WillTryPutMVar c) +rewind (ReadMVar c) = Just (WillReadMVar c) +rewind (BlockedReadMVar c) = Just (WillReadMVar c) +rewind (TryReadMVar c _) = Just (WillTryReadMVar c) +rewind (TakeMVar c _) = Just (WillTakeMVar c) +rewind (BlockedTakeMVar c) = Just (WillTakeMVar c) +rewind (TryTakeMVar c _ _) = Just (WillTryTakeMVar c) +rewind (NewCRef _) = Just WillNewCRef +rewind (ReadCRef c) = Just (WillReadCRef c) +rewind (ReadCRefCas c) = Just (WillReadCRefCas c) +rewind (ModCRef c) = Just (WillModCRef c) +rewind (ModCRefCas c) = Just (WillModCRefCas c) +rewind (WriteCRef c) = Just (WillWriteCRef c) +rewind (CasCRef c _) = Just (WillCasCRef c) +rewind (CommitCRef t c) = Just (WillCommitCRef t c) +rewind (STM _ _) = Just WillSTM +rewind (BlockedSTM _) = Just WillSTM +rewind Catching = Just WillCatching +rewind PopCatching = Just WillPopCatching +rewind Throw = Just WillThrow +rewind (ThrowTo t) = Just (WillThrowTo t) +rewind (BlockedThrowTo t) = Just (WillThrowTo t) +rewind Killed = Nothing +rewind (SetMasking b m) = Just (WillSetMasking b m) +rewind (ResetMasking b m) = Just (WillResetMasking b m) +rewind LiftIO = Just WillLiftIO +rewind Return = Just WillReturn +rewind Stop = Just WillStop +rewind Subconcurrency = Just WillSubconcurrency +rewind StopSubconcurrency = Just WillStopSubconcurrency + +-- | Check if an operation could enable another thread. +willRelease :: Lookahead -> Bool +willRelease WillFork = True +willRelease WillForkOS = True +willRelease WillYield = True +willRelease (WillThreadDelay _) = True +willRelease (WillPutMVar _) = True +willRelease (WillTryPutMVar _) = True +willRelease (WillReadMVar _) = True +willRelease (WillTakeMVar _) = True +willRelease (WillTryTakeMVar _) = True +willRelease WillSTM = True +willRelease WillThrow = True +willRelease (WillSetMasking _ _) = True +willRelease (WillResetMasking _ _) = True +willRelease WillStop = True +willRelease _ = False + +------------------------------------------------------------------------------- +-- * Simplified actions + +-- | A simplified view of the possible actions a thread can perform. +data ActionType = + UnsynchronisedRead CRefId + -- ^ A 'readCRef' or a 'readForCAS'. + | UnsynchronisedWrite CRefId + -- ^ A 'writeCRef'. + | UnsynchronisedOther + -- ^ Some other action which doesn't require cross-thread + -- communication. + | PartiallySynchronisedCommit CRefId + -- ^ A commit. + | PartiallySynchronisedWrite CRefId + -- ^ A 'casCRef' + | PartiallySynchronisedModify CRefId + -- ^ A 'modifyCRefCAS' + | SynchronisedModify CRefId + -- ^ An 'atomicModifyCRef'. + | SynchronisedRead MVarId + -- ^ A 'readMVar' or 'takeMVar' (or @try@/@blocked@ variants). + | SynchronisedWrite MVarId + -- ^ A 'putMVar' (or @try@/@blocked@ variant). + | SynchronisedOther + -- ^ Some other action which does require cross-thread + -- communication. + deriving (Eq, Show) + +instance NFData ActionType where + rnf (UnsynchronisedRead c) = rnf c + rnf (UnsynchronisedWrite c) = rnf c + rnf (PartiallySynchronisedCommit c) = rnf c + rnf (PartiallySynchronisedWrite c) = rnf c + rnf (PartiallySynchronisedModify c) = rnf c + rnf (SynchronisedModify c) = rnf c + rnf (SynchronisedRead m) = rnf m + rnf (SynchronisedWrite m) = rnf m + rnf a = a `seq` () + +-- | Check if an action imposes a write barrier. +isBarrier :: ActionType -> Bool +isBarrier (SynchronisedModify _) = True +isBarrier (SynchronisedRead _) = True +isBarrier (SynchronisedWrite _) = True +isBarrier SynchronisedOther = True +isBarrier _ = False + +-- | Check if an action commits a given 'CRef'. +isCommit :: ActionType -> CRefId -> Bool +isCommit (PartiallySynchronisedCommit c) r = c == r +isCommit (PartiallySynchronisedWrite c) r = c == r +isCommit (PartiallySynchronisedModify c) r = c == r +isCommit _ _ = False + +-- | Check if an action synchronises a given 'CRef'. +synchronises :: ActionType -> CRefId -> Bool +synchronises a r = isCommit a r || isBarrier a + +-- | Get the 'CRef' affected. +crefOf :: ActionType -> Maybe CRefId +crefOf (UnsynchronisedRead r) = Just r +crefOf (UnsynchronisedWrite r) = Just r +crefOf (SynchronisedModify r) = Just r +crefOf (PartiallySynchronisedCommit r) = Just r +crefOf (PartiallySynchronisedWrite r) = Just r +crefOf (PartiallySynchronisedModify r) = Just r +crefOf _ = Nothing + +-- | Get the 'MVar' affected. +mvarOf :: ActionType -> Maybe MVarId +mvarOf (SynchronisedRead c) = Just c +mvarOf (SynchronisedWrite c) = Just c +mvarOf _ = Nothing + +-- | Throw away information from a 'ThreadAction' and give a +-- simplified view of what is happening. +-- +-- This is used in the SCT code to help determine interesting +-- alternative scheduling decisions. +simplifyAction :: ThreadAction -> ActionType +simplifyAction = maybe UnsynchronisedOther simplifyLookahead . rewind + +-- | Variant of 'simplifyAction' that takes a 'Lookahead'. +simplifyLookahead :: Lookahead -> ActionType +simplifyLookahead (WillPutMVar c) = SynchronisedWrite c +simplifyLookahead (WillTryPutMVar c) = SynchronisedWrite c +simplifyLookahead (WillReadMVar c) = SynchronisedRead c +simplifyLookahead (WillTryReadMVar c) = SynchronisedRead c +simplifyLookahead (WillTakeMVar c) = SynchronisedRead c +simplifyLookahead (WillTryTakeMVar c) = SynchronisedRead c +simplifyLookahead (WillReadCRef r) = UnsynchronisedRead r +simplifyLookahead (WillReadCRefCas r) = UnsynchronisedRead r +simplifyLookahead (WillModCRef r) = SynchronisedModify r +simplifyLookahead (WillModCRefCas r) = PartiallySynchronisedModify r +simplifyLookahead (WillWriteCRef r) = UnsynchronisedWrite r +simplifyLookahead (WillCasCRef r) = PartiallySynchronisedWrite r +simplifyLookahead (WillCommitCRef _ r) = PartiallySynchronisedCommit r +simplifyLookahead WillSTM = SynchronisedOther +simplifyLookahead (WillThrowTo _) = SynchronisedOther +simplifyLookahead _ = UnsynchronisedOther + +------------------------------------------------------------------------------- +-- * Error reporting + +-- | 'head' but with a better error message if it fails. Use this +-- only where it shouldn't fail! +ehead :: String -> [a] -> a +ehead _ (x:_) = x +ehead src _ = fatal src "head: empty list" + +-- | 'tail' but with a better error message if it fails. Use this +-- only where it shouldn't fail! +etail :: String -> [a] -> [a] +etail _ (_:xs) = xs +etail src _ = fatal src "tail: empty list" + +-- | '(!!)' but with a better error message if it fails. Use this +-- only where it shouldn't fail! +eidx :: String -> [a] -> Int -> a +eidx src xs i + | i < length xs = xs !! i + | otherwise = fatal src "(!!): index too large" + +-- | 'fromJust' but with a better error message if it fails. Use this +-- only where it shouldn't fail! +efromJust :: String -> Maybe a -> a +efromJust _ (Just x) = x +efromJust src _ = fatal src "fromJust: Nothing" + +-- | 'fromList' but with a better error message if it fails. Use this +-- only where it shouldn't fail! +efromList :: String -> [a] -> NonEmpty a +efromList _ (x:xs) = x:|xs +efromList src _ = fatal src "fromList: empty list" + +-- | 'error' but saying where it came from +fatal :: String -> String -> a +fatal src msg = error ("(dejafu: " ++ src ++ ") " ++ msg) + +------------------------------------------------------------------------------- +-- * Miscellaneous + +-- | Run with a continuation that writes its value into a reference, +-- returning the computation and the reference. Using the reference +-- is non-blocking, it is up to you to ensure you wait sufficiently. +runRefCont :: MonadRef r n => (n () -> x) -> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, r (Maybe b)) +runRefCont act f k = do + ref <- newRef Nothing + let c = k (act . writeRef ref . f) + pure (c, ref) diff --git a/dejafu/Test/DejaFu/SCT.hs b/dejafu/Test/DejaFu/SCT.hs index f7e604a..44bcd61 100755 --- a/dejafu/Test/DejaFu/SCT.hs +++ b/dejafu/Test/DejaFu/SCT.hs @@ -25,8 +25,6 @@ module Test.DejaFu.SCT , Discard(..) , runSCTDiscard , resultsSetDiscard - , weakenDiscard - , strengthenDiscard -- ** Strict variants , runSCT' @@ -119,9 +117,10 @@ import Data.Set (Set) import qualified Data.Set as S import System.Random (RandomGen, randomR) -import Test.DejaFu.Common import Test.DejaFu.Conc +import Test.DejaFu.Internal import Test.DejaFu.SCT.Internal +import Test.DejaFu.Types ------------------------------------------------------------------------------- -- Running Concurrent Programs @@ -237,58 +236,6 @@ resultsSet :: (MonadConc n, MonadRef r n, Ord a) -> n (Set (Either Failure a)) resultsSet = resultsSetDiscard (const Nothing) --- | An @Either Failure a -> Maybe Discard@ value can be used to --- selectively discard results. --- --- @since 0.7.1.0 -data Discard - = DiscardTrace - -- ^ Discard the trace but keep the result. The result will appear - -- to have an empty trace. - | DiscardResultAndTrace - -- ^ Discard the result and the trace. It will simply not be - -- reported as a possible behaviour of the program. - deriving (Eq, Show, Read, Ord, Enum, Bounded) - -instance NFData Discard where - rnf d = d `seq` () - --- | Combine two discard values, keeping the weaker. --- --- @Nothing@ is weaker than @Just DiscardTrace@, which is weaker than --- @Just DiscardResultAndTrace@. This forms a commutative monoid --- where the unit is @const (Just DiscardResultAndTrace)@. --- --- @since 1.0.0.0 -weakenDiscard :: - (Either Failure a -> Maybe Discard) - -> (Either Failure a -> Maybe Discard) - -> Either Failure a -> Maybe Discard -weakenDiscard d1 d2 efa = case (d1 efa, d2 efa) of - (Nothing, _) -> Nothing - (_, Nothing) -> Nothing - (Just DiscardTrace, _) -> Just DiscardTrace - (_, Just DiscardTrace) -> Just DiscardTrace - _ -> Just DiscardResultAndTrace - --- | Combine two discard functions, keeping the stronger. --- --- @Just DiscardResultAndTrace@ is stronger than @Just DiscardTrace@, --- which is stronger than @Nothing@. This forms a commutative monoid --- where the unit is @const Nothing@. --- --- @since 1.0.0.0 -strengthenDiscard :: - (Either Failure a -> Maybe Discard) - -> (Either Failure a -> Maybe Discard) - -> Either Failure a -> Maybe Discard -strengthenDiscard d1 d2 efa = case (d1 efa, d2 efa) of - (Just DiscardResultAndTrace, _) -> Just DiscardResultAndTrace - (_, Just DiscardResultAndTrace) -> Just DiscardResultAndTrace - (Just DiscardTrace, _) -> Just DiscardTrace - (_, Just DiscardTrace) -> Just DiscardTrace - _ -> Nothing - -- | A variant of 'runSCT' which can selectively discard results. -- -- The exact executions tried, and the order in which results are diff --git a/dejafu/Test/DejaFu/SCT/Internal.hs b/dejafu/Test/DejaFu/SCT/Internal.hs index abda508..8f95512 100644 --- a/dejafu/Test/DejaFu/SCT/Internal.hs +++ b/dejafu/Test/DejaFu/SCT/Internal.hs @@ -30,8 +30,9 @@ import Data.Set (Set) import qualified Data.Set as S import System.Random (RandomGen, randomR) -import Test.DejaFu.Common +import Test.DejaFu.Internal import Test.DejaFu.Schedule (Scheduler(..), decisionOf, tidOf) +import Test.DejaFu.Types ------------------------------------------------------------------------------- -- * Dynamic partial-order reduction diff --git a/dejafu/Test/DejaFu/STM.hs b/dejafu/Test/DejaFu/STM.hs index 6c43117..a0ae983 100755 --- a/dejafu/Test/DejaFu/STM.hs +++ b/dejafu/Test/DejaFu/STM.hs @@ -20,7 +20,6 @@ module Test.DejaFu.STM -- * Executing Transactions , Result(..) - , TTrace , TAction(..) , TVarId , runTransaction @@ -35,8 +34,9 @@ import Data.IORef (IORef) import Data.STRef (STRef) import qualified Control.Monad.STM.Class as C -import Test.DejaFu.Common +import Test.DejaFu.Internal import Test.DejaFu.STM.Internal +import Test.DejaFu.Types #if MIN_VERSION_base(4,9,0) import qualified Control.Monad.Fail as Fail @@ -112,7 +112,7 @@ instance C.MonadSTM (STMLike n r) where -- -- @since 0.4.0.0 runTransaction :: MonadRef r n - => STMLike n r a -> IdSource -> n (Result a, IdSource, TTrace) + => STMLike n r a -> IdSource -> n (Result a, IdSource, [TAction]) runTransaction ma tvid = do (res, undo, tvid', trace) <- doTransaction (runSTM ma) tvid diff --git a/dejafu/Test/DejaFu/STM/Internal.hs b/dejafu/Test/DejaFu/STM/Internal.hs index ad520f5..fc2f7cd 100755 --- a/dejafu/Test/DejaFu/STM/Internal.hs +++ b/dejafu/Test/DejaFu/STM/Internal.hs @@ -16,16 +16,17 @@ -- public interface of this library. module Test.DejaFu.STM.Internal where -import Control.DeepSeq (NFData(..)) -import Control.Exception (Exception, SomeException, fromException, - toException) -import Control.Monad.Ref (MonadRef, newRef, readRef, writeRef) -import Data.List (nub) +import Control.DeepSeq (NFData(..)) +import Control.Exception (Exception, SomeException, fromException, + toException) +import Control.Monad.Ref (MonadRef, newRef, readRef, writeRef) +import Data.List (nub) -import Test.DejaFu.Common +import Test.DejaFu.Internal +import Test.DejaFu.Types #if MIN_VERSION_base(4,9,0) -import qualified Control.Monad.Fail as Fail +import qualified Control.Monad.Fail as Fail #endif -------------------------------------------------------------------------------- @@ -133,7 +134,7 @@ instance Foldable Result where -- * Execution -- | Run a STM transaction, returning an action to undo its effects. -doTransaction :: MonadRef r n => M n r a -> IdSource -> n (Result a, n (), IdSource, TTrace) +doTransaction :: MonadRef r n => M n r a -> IdSource -> n (Result a, n (), IdSource, [TAction]) doTransaction ma idsource = do (c, ref) <- runRefCont SStop (Just . Right) (runCont ma) (idsource', undo, readen, written, trace) <- go ref c (pure ()) idsource [] [] [] diff --git a/dejafu/Test/DejaFu/Schedule.hs b/dejafu/Test/DejaFu/Schedule.hs index 1bec215..6350131 100644 --- a/dejafu/Test/DejaFu/Schedule.hs +++ b/dejafu/Test/DejaFu/Schedule.hs @@ -29,10 +29,11 @@ module Test.DejaFu.Schedule , makeNonPreemptive ) where -import Data.List.NonEmpty (NonEmpty(..), toList) -import System.Random (RandomGen, randomR) +import Data.List.NonEmpty (NonEmpty(..), toList) +import System.Random (RandomGen, randomR) -import Test.DejaFu.Common +import Test.DejaFu.Internal +import Test.DejaFu.Types -- | A @Scheduler@ drives the execution of a concurrent program. The -- parameters it takes are: diff --git a/dejafu/Test/DejaFu/Types.hs b/dejafu/Test/DejaFu/Types.hs new file mode 100644 index 0000000..ce86844 --- /dev/null +++ b/dejafu/Test/DejaFu/Types.hs @@ -0,0 +1,602 @@ +-- | +-- Module : Test.DejaFu.Types +-- Copyright : (c) 2017 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : portable +-- +-- Common types and functions used throughout DejaFu. +module Test.DejaFu.Types where + +import Control.DeepSeq (NFData(..)) +import Control.Exception (Exception(..), MaskingState(..), + SomeException) +import Data.Function (on) + +------------------------------------------------------------------------------- +-- * Identifiers + +-- | Every live thread has a unique identitifer. +-- +-- The @Eq@ and @Ord@ instances only consider the int, not the name. +-- +-- @since 0.4.0.0 +data ThreadId = ThreadId (Maybe String) {-# UNPACK #-} !Int + +-- | Previously this was a derived instance. +-- +-- @since 0.7.2.0 +instance Eq ThreadId where + (ThreadId _ i) == (ThreadId _ j) = i == j + +instance Ord ThreadId where + compare (ThreadId _ i) (ThreadId _ j) = compare i j + +instance Show ThreadId where + show (ThreadId (Just n) _) = n + show (ThreadId Nothing i) = show i + +-- | @since 0.5.1.0 +instance NFData ThreadId where + rnf (ThreadId n i) = rnf (n, i) + +-- | Every @CRef@ has a unique identifier. +-- +-- The @Eq@ and @Ord@ instances only consider the int, not the name. +-- +-- @since 0.4.0.0 +data CRefId = CRefId (Maybe String) {-# UNPACK #-} !Int + +-- | Previously this was a derived instance. +-- +-- @since 0.7.2.0 +instance Eq CRefId where + (CRefId _ i) == (CRefId _ j) = i == j + +instance Ord CRefId where + compare (CRefId _ i) (CRefId _ j) = compare i j + +instance Show CRefId where + show (CRefId (Just n) _) = n + show (CRefId Nothing i) = show i + +-- | @since 0.5.1.0 +instance NFData CRefId where + rnf (CRefId n i) = rnf (n, i) + +-- | Every @MVar@ has a unique identifier. +-- +-- The @Eq@ and @Ord@ instances only consider the int, not the name. +-- +-- @since 0.4.0.0 +data MVarId = MVarId (Maybe String) {-# UNPACK #-} !Int + +-- | Previously this was a derived instance. +-- +-- @since 0.7.2.0 +instance Eq MVarId where + (MVarId _ i) == (MVarId _ j) = i == j + +instance Ord MVarId where + compare (MVarId _ i) (MVarId _ j) = compare i j + +instance Show MVarId where + show (MVarId (Just n) _) = n + show (MVarId Nothing i) = show i + +-- | @since 0.5.1.0 +instance NFData MVarId where + rnf (MVarId n i) = rnf (n, i) + +-- | Every @TVar@ has a unique identifier. +-- +-- The @Eq@ and @Ord@ instances only consider the int, not the name. +-- +-- @since 0.4.0.0 +data TVarId = TVarId (Maybe String) {-# UNPACK #-} !Int + +-- | Previously this was a derived instance. +-- +-- @since 0.7.2.0 +instance Eq TVarId where + (TVarId _ i) == (TVarId _ j) = i == j + +instance Ord TVarId where + compare (TVarId _ i) (TVarId _ j) = compare i j + +instance Show TVarId where + show (TVarId (Just n) _) = n + show (TVarId Nothing i) = show i + +-- | @since 0.5.1.0 +instance NFData TVarId where + rnf (TVarId n i) = rnf (n, i) + +-- | The ID of the initial thread. +-- +-- @since 0.4.0.0 +initialThread :: ThreadId +initialThread = ThreadId (Just "main") 0 + +------------------------------------------------------------------------------- +-- * Actions + +-- | All the actions that a thread can perform. +-- +-- @since 1.0.0.0 +data ThreadAction = + Fork ThreadId + -- ^ Start a new thread. + | ForkOS ThreadId + -- ^ Start a new bound thread. + | IsCurrentThreadBound + -- ^ Check if the current thread is bound. + | MyThreadId + -- ^ Get the 'ThreadId' of the current thread. + | GetNumCapabilities Int + -- ^ Get the number of Haskell threads that can run simultaneously. + | SetNumCapabilities Int + -- ^ Set the number of Haskell threads that can run simultaneously. + | Yield + -- ^ Yield the current thread. + | ThreadDelay Int + -- ^ Yield/delay the current thread. + | NewMVar MVarId + -- ^ Create a new 'MVar'. + | PutMVar MVarId [ThreadId] + -- ^ Put into a 'MVar', possibly waking up some threads. + | BlockedPutMVar MVarId + -- ^ Get blocked on a put. + | TryPutMVar MVarId Bool [ThreadId] + -- ^ Try to put into a 'MVar', possibly waking up some threads. + | ReadMVar MVarId + -- ^ Read from a 'MVar'. + | TryReadMVar MVarId Bool + -- ^ Try to read from a 'MVar'. + | BlockedReadMVar MVarId + -- ^ Get blocked on a read. + | TakeMVar MVarId [ThreadId] + -- ^ Take from a 'MVar', possibly waking up some threads. + | BlockedTakeMVar MVarId + -- ^ Get blocked on a take. + | TryTakeMVar MVarId Bool [ThreadId] + -- ^ Try to take from a 'MVar', possibly waking up some threads. + | NewCRef CRefId + -- ^ Create a new 'CRef'. + | ReadCRef CRefId + -- ^ Read from a 'CRef'. + | ReadCRefCas CRefId + -- ^ Read from a 'CRef' for a future compare-and-swap. + | ModCRef CRefId + -- ^ Modify a 'CRef'. + | ModCRefCas CRefId + -- ^ Modify a 'CRef' using a compare-and-swap. + | WriteCRef CRefId + -- ^ Write to a 'CRef' without synchronising. + | CasCRef CRefId Bool + -- ^ Attempt to to a 'CRef' using a compare-and-swap, synchronising + -- it. + | CommitCRef ThreadId CRefId + -- ^ Commit the last write to the given 'CRef' by the given thread, + -- so that all threads can see the updated value. + | STM [TAction] [ThreadId] + -- ^ An STM transaction was executed, possibly waking up some + -- threads. + | BlockedSTM [TAction] + -- ^ Got blocked in an STM transaction. + | Catching + -- ^ Register a new exception handler + | PopCatching + -- ^ Pop the innermost exception handler from the stack. + | Throw + -- ^ Throw an exception. + | ThrowTo ThreadId + -- ^ Throw an exception to a thread. + | BlockedThrowTo ThreadId + -- ^ Get blocked on a 'throwTo'. + | Killed + -- ^ Killed by an uncaught exception. + | SetMasking Bool MaskingState + -- ^ Set the masking state. If 'True', this is being used to set the + -- masking state to the original state in the argument passed to a + -- 'mask'ed function. + | ResetMasking Bool MaskingState + -- ^ Return to an earlier masking state. If 'True', this is being + -- used to return to the state of the masked block in the argument + -- passed to a 'mask'ed function. + | LiftIO + -- ^ Lift an IO action. Note that this can only happen with + -- 'ConcIO'. + | Return + -- ^ A 'return' or 'pure' action was executed. + | Stop + -- ^ Cease execution and terminate. + | Subconcurrency + -- ^ Start executing an action with @subconcurrency@. + | StopSubconcurrency + -- ^ Stop executing an action with @subconcurrency@. + deriving (Eq, Show) + +instance NFData ThreadAction where + rnf (Fork t) = rnf t + rnf (ForkOS t) = rnf t + rnf (ThreadDelay n) = rnf n + rnf (GetNumCapabilities c) = rnf c + rnf (SetNumCapabilities c) = rnf c + rnf (NewMVar m) = rnf m + rnf (PutMVar m ts) = rnf (m, ts) + rnf (BlockedPutMVar m) = rnf m + rnf (TryPutMVar m b ts) = rnf (m, b, ts) + rnf (ReadMVar m) = rnf m + rnf (TryReadMVar m b) = rnf (m, b) + rnf (BlockedReadMVar m) = rnf m + rnf (TakeMVar m ts) = rnf (m, ts) + rnf (BlockedTakeMVar m) = rnf m + rnf (TryTakeMVar m b ts) = rnf (m, b, ts) + rnf (NewCRef c) = rnf c + rnf (ReadCRef c) = rnf c + rnf (ReadCRefCas c) = rnf c + rnf (ModCRef c) = rnf c + rnf (ModCRefCas c) = rnf c + rnf (WriteCRef c) = rnf c + rnf (CasCRef c b) = rnf (c, b) + rnf (CommitCRef t c) = rnf (t, c) + rnf (STM tr ts) = rnf (tr, ts) + rnf (BlockedSTM tr) = rnf tr + rnf (ThrowTo t) = rnf t + rnf (BlockedThrowTo t) = rnf t + rnf (SetMasking b m) = b `seq` m `seq` () + rnf (ResetMasking b m) = b `seq` m `seq` () + rnf a = a `seq` () + +-- | A one-step look-ahead at what a thread will do next. +-- +-- @since 1.0.0.0 +data Lookahead = + WillFork + -- ^ Will start a new thread. + | WillForkOS + -- ^ Will start a new bound thread. + | WillIsCurrentThreadBound + -- ^ Will check if the current thread is bound. + | WillMyThreadId + -- ^ Will get the 'ThreadId'. + | WillGetNumCapabilities + -- ^ Will get the number of Haskell threads that can run + -- simultaneously. + | WillSetNumCapabilities Int + -- ^ Will set the number of Haskell threads that can run + -- simultaneously. + | WillYield + -- ^ Will yield the current thread. + | WillThreadDelay Int + -- ^ Will yield/delay the current thread. + | WillNewMVar + -- ^ Will create a new 'MVar'. + | WillPutMVar MVarId + -- ^ Will put into a 'MVar', possibly waking up some threads. + | WillTryPutMVar MVarId + -- ^ Will try to put into a 'MVar', possibly waking up some threads. + | WillReadMVar MVarId + -- ^ Will read from a 'MVar'. + | WillTryReadMVar MVarId + -- ^ Will try to read from a 'MVar'. + | WillTakeMVar MVarId + -- ^ Will take from a 'MVar', possibly waking up some threads. + | WillTryTakeMVar MVarId + -- ^ Will try to take from a 'MVar', possibly waking up some threads. + | WillNewCRef + -- ^ Will create a new 'CRef'. + | WillReadCRef CRefId + -- ^ Will read from a 'CRef'. + | WillReadCRefCas CRefId + -- ^ Will read from a 'CRef' for a future compare-and-swap. + | WillModCRef CRefId + -- ^ Will modify a 'CRef'. + | WillModCRefCas CRefId + -- ^ Will modify a 'CRef' using a compare-and-swap. + | WillWriteCRef CRefId + -- ^ Will write to a 'CRef' without synchronising. + | WillCasCRef CRefId + -- ^ Will attempt to to a 'CRef' using a compare-and-swap, + -- synchronising it. + | WillCommitCRef ThreadId CRefId + -- ^ Will commit the last write by the given thread to the 'CRef'. + | WillSTM + -- ^ Will execute an STM transaction, possibly waking up some + -- threads. + | WillCatching + -- ^ Will register a new exception handler + | WillPopCatching + -- ^ Will pop the innermost exception handler from the stack. + | WillThrow + -- ^ Will throw an exception. + | WillThrowTo ThreadId + -- ^ Will throw an exception to a thread. + | WillSetMasking Bool MaskingState + -- ^ Will set the masking state. If 'True', this is being used to + -- set the masking state to the original state in the argument + -- passed to a 'mask'ed function. + | WillResetMasking Bool MaskingState + -- ^ Will return to an earlier masking state. If 'True', this is + -- being used to return to the state of the masked block in the + -- argument passed to a 'mask'ed function. + | WillLiftIO + -- ^ Will lift an IO action. Note that this can only happen with + -- 'ConcIO'. + | WillReturn + -- ^ Will execute a 'return' or 'pure' action. + | WillStop + -- ^ Will cease execution and terminate. + | WillSubconcurrency + -- ^ Will execute an action with @subconcurrency@. + | WillStopSubconcurrency + -- ^ Will stop executing an extion with @subconcurrency@. + deriving (Eq, Show) + +instance NFData Lookahead where + rnf (WillThreadDelay n) = rnf n + rnf (WillSetNumCapabilities c) = rnf c + rnf (WillPutMVar m) = rnf m + rnf (WillTryPutMVar m) = rnf m + rnf (WillReadMVar m) = rnf m + rnf (WillTryReadMVar m) = rnf m + rnf (WillTakeMVar m) = rnf m + rnf (WillTryTakeMVar m) = rnf m + rnf (WillReadCRef c) = rnf c + rnf (WillReadCRefCas c) = rnf c + rnf (WillModCRef c) = rnf c + rnf (WillModCRefCas c) = rnf c + rnf (WillWriteCRef c) = rnf c + rnf (WillCasCRef c) = rnf c + rnf (WillCommitCRef t c) = rnf (t, c) + rnf (WillThrowTo t) = rnf t + rnf (WillSetMasking b m) = b `seq` m `seq` () + rnf (WillResetMasking b m) = b `seq` m `seq` () + rnf l = l `seq` () + +-- | All the actions that an STM transaction can perform. +-- +-- @since 0.8.0.0 +data TAction = + TNew TVarId + -- ^ Create a new @TVar@ + | TRead TVarId + -- ^ Read from a @TVar@. + | TWrite TVarId + -- ^ Write to a @TVar@. + | TRetry + -- ^ Abort and discard effects. + | TOrElse [TAction] (Maybe [TAction]) + -- ^ Execute a transaction until it succeeds (@STMStop@) or aborts + -- (@STMRetry@) and, if it aborts, execute the other transaction. + | TThrow + -- ^ Throw an exception, abort, and discard effects. + | TCatch [TAction] (Maybe [TAction]) + -- ^ Execute a transaction until it succeeds (@STMStop@) or aborts + -- (@STMThrow@). If the exception is of the appropriate type, it is + -- handled and execution continues; otherwise aborts, propagating + -- the exception upwards. + | TStop + -- ^ Terminate successfully and commit effects. + deriving (Eq, Show) + +-- | @since 0.5.1.0 +instance NFData TAction where + rnf (TRead t) = rnf t + rnf (TWrite t) = rnf t + rnf (TOrElse tr mtr) = rnf (tr, mtr) + rnf (TCatch tr mtr) = rnf (tr, mtr) + rnf ta = ta `seq` () + +------------------------------------------------------------------------------- +-- * Traces + +-- | One of the outputs of the runner is a @Trace@, which is a log of +-- decisions made, all the unblocked threads and what they would do, +-- and the action a thread took in its step. +-- +-- @since 0.8.0.0 +type Trace + = [(Decision, [(ThreadId, Lookahead)], ThreadAction)] + +-- | Scheduling decisions are based on the state of the running +-- program, and so we can capture some of that state in recording what +-- specific decision we made. +-- +-- @since 0.5.0.0 +data Decision = + Start ThreadId + -- ^ Start a new thread, because the last was blocked (or it's the + -- start of computation). + | Continue + -- ^ Continue running the last thread for another step. + | SwitchTo ThreadId + -- ^ Pre-empt the running thread, and switch to another. + deriving (Eq, Show) + +-- | @since 0.5.1.0 +instance NFData Decision where + rnf (Start t) = rnf t + rnf (SwitchTo t) = rnf t + rnf d = d `seq` () + +------------------------------------------------------------------------------- +-- * Failures + +-- | An indication of how a concurrent computation failed. +-- +-- The @Eq@, @Ord@, and @NFData@ instances compare/evaluate the +-- exception with @show@ in the @UncaughtException@ case. +-- +-- @since 0.9.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 + -- ^ 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 + -- has executed for too long, or there have been too many yields). + | Deadlock + -- ^ Every thread is blocked, and the main thread is /not/ blocked + -- in an STM transaction. + | STMDeadlock + -- ^ Every thread is blocked, and the main thread is blocked in an + -- 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. + deriving Show + +instance Eq Failure where + (==) = (==) `on` _other + +instance Ord Failure where + compare = compare `on` _other + +instance NFData Failure where + rnf = rnf . _other + +-- | Convert failures into a different representation we can Eq / Ord +-- / NFData. +_other :: Failure -> (Int, Maybe String) +_other InternalError = (0, Nothing) +_other Abort = (1, Nothing) +_other Deadlock = (2, Nothing) +_other STMDeadlock = (3, Nothing) +_other (UncaughtException e) = (4, Just (show e)) +_other IllegalSubconcurrency = (5, Nothing) + +-- | 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@. +-- +-- @since 0.9.0.0 +isAbort :: Failure -> Bool +isAbort Abort = True +isAbort _ = False + +-- | Check if a failure is a @Deadlock@ or an @STMDeadlock@. +-- +-- @since 0.9.0.0 +isDeadlock :: Failure -> Bool +isDeadlock Deadlock = True +isDeadlock STMDeadlock = True +isDeadlock _ = False + +-- | Check if a failure is an @UncaughtException@ +-- +-- @since 0.9.0.0 +isUncaughtException :: Failure -> Bool +isUncaughtException (UncaughtException _) = True +isUncaughtException _ = False + +-- | Check if a failure is an @IllegalSubconcurrency@ +-- +-- @since 0.9.0.0 +isIllegalSubconcurrency :: Failure -> Bool +isIllegalSubconcurrency IllegalSubconcurrency = True +isIllegalSubconcurrency _ = False + +------------------------------------------------------------------------------- +-- * Discarding results and traces + +-- | An @Either Failure a -> Maybe Discard@ value can be used to +-- selectively discard results. +-- +-- @since 0.7.1.0 +data Discard + = DiscardTrace + -- ^ Discard the trace but keep the result. The result will appear + -- to have an empty trace. + | DiscardResultAndTrace + -- ^ Discard the result and the trace. It will simply not be + -- reported as a possible behaviour of the program. + deriving (Eq, Show, Read, Ord, Enum, Bounded) + +instance NFData Discard where + rnf d = d `seq` () + +-- | Combine two discard values, keeping the weaker. +-- +-- @Nothing@ is weaker than @Just DiscardTrace@, which is weaker than +-- @Just DiscardResultAndTrace@. This forms a commutative monoid +-- where the unit is @const (Just DiscardResultAndTrace)@. +-- +-- @since 1.0.0.0 +weakenDiscard :: + (Either Failure a -> Maybe Discard) + -> (Either Failure a -> Maybe Discard) + -> Either Failure a -> Maybe Discard +weakenDiscard d1 d2 efa = case (d1 efa, d2 efa) of + (Nothing, _) -> Nothing + (_, Nothing) -> Nothing + (Just DiscardTrace, _) -> Just DiscardTrace + (_, Just DiscardTrace) -> Just DiscardTrace + _ -> Just DiscardResultAndTrace + +-- | Combine two discard functions, keeping the stronger. +-- +-- @Just DiscardResultAndTrace@ is stronger than @Just DiscardTrace@, +-- which is stronger than @Nothing@. This forms a commutative monoid +-- where the unit is @const Nothing@. +-- +-- @since 1.0.0.0 +strengthenDiscard :: + (Either Failure a -> Maybe Discard) + -> (Either Failure a -> Maybe Discard) + -> Either Failure a -> Maybe Discard +strengthenDiscard d1 d2 efa = case (d1 efa, d2 efa) of + (Just DiscardResultAndTrace, _) -> Just DiscardResultAndTrace + (_, Just DiscardResultAndTrace) -> Just DiscardResultAndTrace + (Just DiscardTrace, _) -> Just DiscardTrace + (_, Just DiscardTrace) -> Just DiscardTrace + _ -> Nothing + +------------------------------------------------------------------------------- +-- * Memory Models + +-- | The memory model to use for non-synchronised 'CRef' operations. +-- +-- @since 0.4.0.0 +data MemType = + SequentialConsistency + -- ^ The most intuitive model: a program behaves as a simple + -- interleaving of the actions in different threads. When a 'CRef' + -- is written to, that write is immediately visible to all threads. + | TotalStoreOrder + -- ^ Each thread has a write buffer. A thread sees its writes + -- immediately, but other threads will only see writes when they are + -- committed, which may happen later. Writes are committed in the + -- same order that they are created. + | PartialStoreOrder + -- ^ Each 'CRef' has a write buffer. A thread sees its writes + -- immediately, but other threads will only see writes when they are + -- committed, which may happen later. Writes to different 'CRef's + -- are not necessarily committed in the same order that they are + -- created. + deriving (Eq, Show, Read, Ord, Enum, Bounded) + +-- | @since 0.5.1.0 +instance NFData MemType where + rnf m = m `seq` () + +------------------------------------------------------------------------------- +-- * @MonadFail@ + +-- | An exception for errors in testing caused by use of 'fail'. +newtype MonadFailException = MonadFailException String + deriving Show + +instance Exception MonadFailException diff --git a/dejafu/Test/DejaFu/Utils.hs b/dejafu/Test/DejaFu/Utils.hs new file mode 100644 index 0000000..25c3b64 --- /dev/null +++ b/dejafu/Test/DejaFu/Utils.hs @@ -0,0 +1,77 @@ +-- | +-- Module : Test.DejaFu.utils +-- Copyright : (c) 2017 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : portable +-- +-- Utility functions for users of dejafu. +module Test.DejaFu.Utils where + +import Control.Exception (Exception(..), displayException) +import Data.List (intercalate, minimumBy) +import Data.Maybe (mapMaybe) +import Data.Ord (comparing) + +import Test.DejaFu.Types + +-- | Pretty-print a trace, including a key of the thread IDs (not +-- including thread 0). Each line of the key is indented by two +-- spaces. +-- +-- @since 0.5.0.0 +showTrace :: Trace -> String +showTrace [] = "" +showTrace trc = intercalate "\n" $ go False trc : strkey where + go _ ((_,_,CommitCRef _ _):rest) = "C-" ++ go False rest + go _ ((Start (ThreadId _ i),_,a):rest) = "S" ++ show i ++ "-" ++ go (didYield a) rest + go y ((SwitchTo (ThreadId _ i),_,a):rest) = (if y then "p" else "P") ++ show i ++ "-" ++ go (didYield a) rest + go _ ((Continue,_,a):rest) = '-' : go (didYield a) rest + go _ _ = "" + + strkey = + [" " ++ show i ++ ": " ++ name | (i, name) <- threadNames trc] + + didYield Yield = True + didYield (ThreadDelay _) = True + didYield _ = False + +-- | Get all named threads in the trace. +-- +-- @since 0.7.3.0 +threadNames :: Trace -> [(Int, String)] +threadNames = mapMaybe go where + go (_, _, Fork (ThreadId (Just name) i)) = Just (i, name) + go (_, _, ForkOS (ThreadId (Just name) i)) = Just (i, name) + go _ = Nothing + +-- | Pretty-print a failure +-- +-- @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]" + +-- | Find the \"simplest\" trace leading to each result. +simplestsBy :: (x -> x -> Bool) -> [(x, Trace)] -> [(x, Trace)] +simplestsBy f = map choose . collect where + collect = groupBy' [] (\(a,_) (b,_) -> f a b) + choose = minimumBy . comparing $ \(_, trc) -> + let switchTos = length . filter (\(d,_,_) -> case d of SwitchTo _ -> True; _ -> False) + starts = length . filter (\(d,_,_) -> case d of Start _ -> True; _ -> False) + commits = length . filter (\(_,_,a) -> case a of CommitCRef _ _ -> True; _ -> False) + in (switchTos trc, commits trc, length trc, starts trc) + + groupBy' res _ [] = res + groupBy' res eq (y:ys) = groupBy' (insert' eq y res) eq ys + + insert' _ x [] = [[x]] + insert' eq x (ys@(y:_):yss) + | x `eq` y = (x:ys) : yss + | otherwise = ys : insert' eq x yss + insert' _ _ ([]:_) = undefined diff --git a/dejafu/dejafu.cabal b/dejafu/dejafu.cabal index 1ebd62b..e478a75 100755 --- a/dejafu/dejafu.cabal +++ b/dejafu/dejafu.cabal @@ -38,17 +38,19 @@ source-repository this library exposed-modules: Test.DejaFu , Test.DejaFu.Conc - , Test.DejaFu.Common , Test.DejaFu.Defaults , Test.DejaFu.Refinement - , Test.DejaFu.Schedule , Test.DejaFu.SCT , Test.DejaFu.STM + , Test.DejaFu.Schedule + , Test.DejaFu.Types + , Test.DejaFu.Utils , Test.DejaFu.Conc.Internal , Test.DejaFu.Conc.Internal.Common , Test.DejaFu.Conc.Internal.Memory , Test.DejaFu.Conc.Internal.Threading + , Test.DejaFu.Internal , Test.DejaFu.SCT.Internal , Test.DejaFu.STM.Internal diff --git a/hunit-dejafu/Test/HUnit/DejaFu.hs b/hunit-dejafu/Test/HUnit/DejaFu.hs index 0da3003..01fb94a 100755 --- a/hunit-dejafu/Test/HUnit/DejaFu.hs +++ b/hunit-dejafu/Test/HUnit/DejaFu.hs @@ -74,6 +74,7 @@ import Test.DejaFu hiding (Testable(..)) import qualified Test.DejaFu.Conc as Conc import qualified Test.DejaFu.Refinement as R import qualified Test.DejaFu.SCT as SCT +import qualified Test.DejaFu.Types as D import Test.HUnit (Assertable(..), Test(..), Testable(..), assertFailure, assertString) import Test.HUnit.Lang (HUnitFailure(..)) @@ -264,7 +265,7 @@ testconc discard way memtype tests concio = case map toTest tests of where toTest (name, p) = TestLabel name . TestCase $ do - let discarder = SCT.strengthenDiscard discard (pdiscard p) + let discarder = D.strengthenDiscard discard (pdiscard p) traces <- SCT.runSCTDiscard discarder way memtype concio assertString . showErr $ peval p traces diff --git a/tasty-dejafu/Test/Tasty/DejaFu.hs b/tasty-dejafu/Test/Tasty/DejaFu.hs index 00ac77e..ce0e960 100755 --- a/tasty-dejafu/Test/Tasty/DejaFu.hs +++ b/tasty-dejafu/Test/Tasty/DejaFu.hs @@ -78,6 +78,7 @@ import Test.DejaFu hiding (Testable(..)) import qualified Test.DejaFu.Conc as Conc import qualified Test.DejaFu.Refinement as R import qualified Test.DejaFu.SCT as SCT +import qualified Test.DejaFu.Types as D import Test.Tasty (TestName, TestTree, testGroup) import Test.Tasty.Options (IsOption(..), OptionDescription(..), lookupOption) @@ -328,7 +329,7 @@ testconc discard way memtype tests concio = case map toTest tests of where toTest (name, p) = - let discarder = SCT.strengthenDiscard discard (pdiscard p) + let discarder = D.strengthenDiscard discard (pdiscard p) traces = SCT.runSCTDiscard discarder way memtype concio in singleTest name $ ConcTest traces (peval p)