diff --git a/Test/DejaFu.hs b/Test/DejaFu.hs --- a/Test/DejaFu.hs +++ b/Test/DejaFu.hs @@ -243,6 +243,7 @@ ) where import Control.Arrow (first) +import Control.DeepSeq (NFData(..)) import Control.Monad (when, unless) import Control.Monad.Ref (MonadRef) import Control.Monad.ST (runST) @@ -398,7 +399,14 @@ -- ^ The failing cases, if any. , _failureMsg :: String -- ^ A message to display on failure, if nonempty - } deriving Show + } deriving (Eq, Show) + +instance NFData a => NFData (Result a) where + rnf r = rnf ( _pass r + , _casesChecked r + , _failures r + , _failureMsg r + ) -- | A failed result, taking the given list of failures. defaultFail :: [(Either Failure a, Trace)] -> Result a diff --git a/Test/DejaFu/Common.hs b/Test/DejaFu/Common.hs --- a/Test/DejaFu/Common.hs +++ b/Test/DejaFu/Common.hs @@ -60,6 +60,7 @@ , MemType(..) ) where +import Control.DeepSeq (NFData(..)) import Control.Exception (MaskingState(..)) import Data.List (sort, nub, intercalate) import Data.List.NonEmpty (NonEmpty) @@ -81,6 +82,9 @@ show (ThreadId (Just n) _) = n show (ThreadId Nothing i) = show i +instance NFData ThreadId where + rnf (ThreadId n i) = rnf (n, i) + -- | Every @CRef@ has a unique identifier. data CRefId = CRefId (Maybe String) Int deriving Eq @@ -92,6 +96,9 @@ show (CRefId (Just n) _) = n show (CRefId Nothing i) = show i +instance NFData CRefId where + rnf (CRefId n i) = rnf (n, i) + -- | Every @MVar@ has a unique identifier. data MVarId = MVarId (Maybe String) Int deriving Eq @@ -103,6 +110,9 @@ show (MVarId (Just n) _) = n show (MVarId Nothing i) = show i +instance NFData MVarId where + rnf (MVarId n i) = rnf (n, i) + -- | Every @TVar@ has a unique identifier. data TVarId = TVarId (Maybe String) Int deriving Eq @@ -114,6 +124,9 @@ show (TVarId (Just n) _) = n show (TVarId Nothing i) = show i +instance NFData TVarId where + rnf (TVarId n i) = rnf (n, i) + -- | The ID of the initial thread. initialThread :: ThreadId initialThread = ThreadId (Just "main") 0 @@ -132,8 +145,19 @@ , _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 @@ -264,6 +288,36 @@ -- ^ Stop executing an action with @subconcurrency@. deriving (Eq, Show) +instance NFData ThreadAction where + rnf (Fork t) = rnf t + 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. isBlock :: ThreadAction -> Bool isBlock (BlockedThrowTo _) = True @@ -367,6 +421,26 @@ -- ^ Will stop executing an extion with @subconcurrency@. deriving (Eq, Show) +instance NFData Lookahead where + 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. rewind :: ThreadAction -> Maybe Lookahead @@ -454,6 +528,17 @@ -- 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 @@ -547,6 +632,13 @@ -- ^ Terminate successfully and commit effects. deriving (Eq, Show) +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 @@ -569,6 +661,11 @@ -- ^ Pre-empt the running thread, and switch to another. deriving (Eq, Show) +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. @@ -646,6 +743,9 @@ -- multiple threads existed. deriving (Eq, Show, Read, Ord, Enum, Bounded) +instance NFData Failure where + rnf f = f `seq` () + -- | Pretty-print a failure showFail :: Failure -> String showFail Abort = "[abort]" @@ -676,6 +776,9 @@ -- are not necessarily committed in the same order that they are -- created. deriving (Eq, Show, Read, Ord, Enum, Bounded) + +instance NFData MemType where + rnf m = m `seq` () ------------------------------------------------------------------------------- -- Utilities diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -13,7 +13,9 @@ ( -- * Running Concurrent Programs Way(..) , runSCT + , runSCT' , resultsSet + , resultsSet' -- * Bounded Partial-order Reduction @@ -88,6 +90,7 @@ , sctRandom ) where +import Control.DeepSeq (NFData(..)) import Control.Monad.Ref (MonadRef) import Data.List (foldl') import qualified Data.Map.Strict as M @@ -112,6 +115,10 @@ -- PRNG. deriving (Eq, Ord, Read, Show) +instance NFData g => NFData (Way g) where + rnf (Systematically bs) = rnf bs + rnf (Randomly g n) = rnf (g, n) + -- | Explore possible executions of a concurrent program. -- -- * If the 'Way' is @Systematically@, 'sctBound' is used. @@ -128,6 +135,16 @@ runSCT (Systematically cb) memtype = sctBound memtype cb runSCT (Randomly g lim) memtype = sctRandom memtype g lim +-- | A strict variant of 'runSCT'. +-- +-- Demanding the result of this will force it to normal form, which +-- may be more efficient in some situations. +runSCT' :: (MonadRef r n, RandomGen g, NFData a) + => Way g -> MemType -> Conc n r a -> n [(Either Failure a, Trace)] +runSCT' way memtype conc = do + res <- runSCT way memtype conc + rnf res `seq` pure res + -- | Return the set of results of a concurrent program. resultsSet :: (MonadRef r n, RandomGen g, Ord a) => Way g @@ -140,6 +157,16 @@ resultsSet way memtype conc = S.fromList . map fst <$> runSCT way memtype conc +-- | A strict variant of 'resultsSet'. +-- +-- Demanding the result of this will force it to normal form, which +-- may be more efficient in some situations. +resultsSet' :: (MonadRef r n, RandomGen g, Ord a, NFData a) + => Way g -> MemType -> Conc n r a -> n (Set (Either Failure a)) +resultsSet' way memtype conc = do + res <- resultsSet' way memtype conc + rnf res `seq` pure res + ------------------------------------------------------------------------------- -- Combined Bounds @@ -149,6 +176,12 @@ , boundLength :: Maybe LengthBound } deriving (Eq, Ord, Read, Show) +instance NFData Bounds where + rnf bs = rnf ( boundPreemp bs + , boundFair bs + , boundLength bs + ) + -- | No bounds enabled. This forces the scheduler to just use -- partial-order reduction and sleep sets to prune the search -- space. This will /ONLY/ work if your computation always terminates! @@ -180,7 +213,7 @@ -- Pre-emption bounding newtype PreemptionBound = PreemptionBound Int - deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show) + deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show, NFData) -- | An SCT runner using a pre-emption bounding scheduler. sctPreBound :: MonadRef r n @@ -223,7 +256,7 @@ -- Fair bounding newtype FairBound = FairBound Int - deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show) + deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show, NFData) -- | An SCT runner using a fair bounding scheduler. sctFairBound :: MonadRef r n @@ -252,7 +285,7 @@ -- Length bounding newtype LengthBound = LengthBound Int - deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show) + deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show, NFData) -- | An SCT runner using a length bounding scheduler. sctLengthBound :: MonadRef r n diff --git a/Test/DejaFu/SCT/Internal.hs b/Test/DejaFu/SCT/Internal.hs --- a/Test/DejaFu/SCT/Internal.hs +++ b/Test/DejaFu/SCT/Internal.hs @@ -11,6 +11,7 @@ -- interface of this library. module Test.DejaFu.SCT.Internal where +import Control.DeepSeq (NFData(..)) import Control.Exception (MaskingState(..)) import Data.Char (ord) import Data.Function (on) @@ -52,8 +53,17 @@ , dporAction :: Maybe ThreadAction -- ^ What happened at this step. This will be 'Nothing' at the root, -- 'Just' everywhere else. - } deriving Show + } deriving (Eq, Show) +instance NFData DPOR where + rnf dpor = rnf ( dporRunnable dpor + , dporTodo dpor + , dporDone dpor + , dporSleep dpor + , dporTaken dpor + , dporAction dpor + ) + -- | One step of the execution, including information for backtracking -- purposes. This backtracking information is used to generate new -- schedules. @@ -71,8 +81,17 @@ -- alternatives were added conservatively due to the bound. , bcktState :: DepState -- ^ Some domain-specific state at this point. - } deriving Show + } deriving (Eq, Show) +instance NFData BacktrackStep where + rnf bs = rnf ( bcktThreadid bs + , bcktDecision bs + , bcktAction bs + , bcktRunnable bs + , bcktBacktracks bs + , bcktState bs + ) + -- | Initial DPOR state, given an initial thread ID. This initial -- thread should exist and be runnable at the start of execution. initialState :: DPOR @@ -311,8 +330,17 @@ , schedDepState :: DepState -- ^ State used by the dependency function to determine when to -- remove decisions from the sleep set. - } deriving Show + } deriving (Eq, Show) +instance NFData DPORSchedState where + rnf s = rnf ( schedSleep s + , schedPrefix s + , schedBPoints s + , schedIgnore s + , schedBoundKill s + , schedDepState s + ) + -- | Initial DPOR scheduler state for a given prefix initialDPORSchedState :: Map ThreadId ThreadAction -- ^ The initial sleep set. @@ -499,8 +527,13 @@ -- ^ The thread weights: used in determining which to run. , schedGen :: g -- ^ The random number generator. - } + } deriving (Eq, Show) +instance NFData g => NFData (RandSchedState g) where + rnf s = rnf ( schedWeights s + , schedGen s + ) + -- | Initial weighted random scheduler state. initialRandSchedState :: g -> RandSchedState g initialRandSchedState = RandSchedState M.empty @@ -540,6 +573,11 @@ -- provides compatibility with dpor-0.1, where the thread IDs are -- not available. } deriving (Eq, Show) + +instance NFData DepState where + rnf depstate = rnf ( depCRState depstate + , [(t, m `seq` ()) | (t, m) <- M.toList (depMaskState depstate)] + ) -- | Initial dependency state. initialDepState :: DepState diff --git a/Test/DejaFu/STM/Internal.hs b/Test/DejaFu/STM/Internal.hs --- a/Test/DejaFu/STM/Internal.hs +++ b/Test/DejaFu/STM/Internal.hs @@ -15,6 +15,7 @@ -- 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.Cont (Cont, runCont) import Control.Monad.Ref (MonadRef, newRef, readRef, writeRef) @@ -70,6 +71,12 @@ | Exception SomeException -- ^ The transaction aborted by throwing an exception. deriving Show + +-- | This only reduces a 'SomeException' to WHNF. +instance NFData a => NFData (Result a) where + rnf (Success tr1 tr2 a) = rnf (tr1, tr2, a) + rnf (Retry tr) = rnf tr + rnf (Exception e) = e `seq` () -- | Check if a 'Result' is a @Success@. isSTMSuccess :: Result a -> Bool diff --git a/dejafu.cabal b/dejafu.cabal --- a/dejafu.cabal +++ b/dejafu.cabal @@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: dejafu -version: 0.5.0.2 +version: 0.5.1.0 synopsis: Systematic testing for Haskell concurrency. description: @@ -74,7 +74,7 @@ source-repository this type: git location: https://github.com/barrucadu/dejafu.git - tag: dejafu-0.5.0.2 + tag: dejafu-0.5.1.0 library exposed-modules: Test.DejaFu @@ -96,6 +96,7 @@ build-depends: base >=4.8 && <5 , concurrency ==1.1.0.* , containers >=0.5 && <0.6 + , deepseq >=1.1 && <2 , exceptions >=0.7 && <0.9 , monad-loops >=0.4 && <0.5 , mtl >=2.2 && <2.3