dejafu 0.5.0.2 → 0.5.1.0

raw patch · 6 files changed

+201/−11 lines, 6 filesdep +deepseqPVP ok

version bump matches the API change (PVP)

Dependencies added: deepseq

API changes (from Hackage documentation)

Files

• Test/DejaFu.hs +9/−1
• Test/DejaFu/Common.hs +104/−1
• Test/DejaFu/SCT.hs +36/−3
• Test/DejaFu/SCT/Internal.hs +42/−4
• Test/DejaFu/STM/Internal.hs +7/−0
• dejafu.cabal +3/−2

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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