barrucadu/dejafu
1
1
Fork 0
mirror of https://github.com/barrucadu/dejafu.git synced 2025-01-01 10:15:06 +03:00
Code Issues Projects Releases Wiki Activity

Split up Test.DejaFu.Common

Browse Source
This commit is contained in:
Michael Walker 2017-12-06 20:16:11 +00:00
parent 5ee2590f0e
commit 81bcb5a351
21 changed files with 1090 additions and 1196 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
dejafu-tests/Cases/Properties.hs
View File

@ -12,8 +12,9 @@ import qualified Data.Map as M
import Data.Maybe (fromJust, isJust) import Data.Maybe (fromJust, isJust)
import Data.Proxy (Proxy(..)) import Data.Proxy (Proxy(..))
import qualified Data.Sequence as S import qualified Data.Sequence as S
import Test.DejaFu.Common (ThreadAction, Lookahead) import Test.DejaFu.Types (ThreadAction, Lookahead)
import qualified Test.DejaFu.Common as D 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.Common as D
import qualified Test.DejaFu.Conc.Internal.Memory as Mem import qualified Test.DejaFu.Conc.Internal.Memory as Mem
import qualified Test.DejaFu.SCT.Internal as SCT import qualified Test.DejaFu.SCT.Internal as SCT

13
dejafu/CHANGELOG.markdown
View File

@ -47,9 +47,20 @@ This project is versioned according to the [Package Versioning Policy](https://p
### Test.DejaFu.Common ### 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 `ForkOS` and `IsCurrentThreadBound` thread actions. (#126)
- New `WillForkOS` and `WillIsCurrentThreadBound` lookaheads. (#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 ### Test.DejaFu.Conc
- The `ConcST` type alias is gone. - 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`. It is no longer possible to test things in `ST`.
- New functions `strengthenDiscard` and `weakenDiscard` to combine discard functions.
### Miscellaneous ### Miscellaneous
- The minimum supported version of concurrency is now 1.3.0.0. - The minimum supported version of concurrency is now 1.3.0.0.

28
dejafu/Test/DejaFu.hs
View File

@ -386,16 +386,16 @@ import Control.Monad.Conc.Class (MonadConc)
import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.Ref (MonadRef) import Control.Monad.Ref (MonadRef)
import Data.Function (on) import Data.Function (on)
import Data.List (intercalate, intersperse, minimumBy) import Data.List (intercalate, intersperse)
import Data.Maybe (catMaybes, isNothing, mapMaybe) import Data.Maybe (catMaybes, isNothing, mapMaybe)
import Data.Ord (comparing)
import Data.Profunctor (Profunctor(..)) import Data.Profunctor (Profunctor(..))
import Test.DejaFu.Common
import Test.DejaFu.Conc import Test.DejaFu.Conc
import Test.DejaFu.Defaults import Test.DejaFu.Defaults
import Test.DejaFu.Refinement import Test.DejaFu.Refinement
import Test.DejaFu.SCT 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 every line of a string.
indent :: String -> String indent :: String -> String
indent = intercalate "\n" . map ('\t':) . lines 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

1085
dejafu/Test/DejaFu/Common.hs
View File

File diff suppressed because it is too large Load Diff

4
dejafu/Test/DejaFu/Conc.hs
View File

@ -56,10 +56,12 @@ import Data.IORef (IORef)
import Test.DejaFu.Schedule import Test.DejaFu.Schedule
import qualified Control.Monad.Conc.Class as C import qualified Control.Monad.Conc.Class as C
import Test.DejaFu.Common
import Test.DejaFu.Conc.Internal import Test.DejaFu.Conc.Internal
import Test.DejaFu.Conc.Internal.Common import Test.DejaFu.Conc.Internal.Common
import Test.DejaFu.Internal
import Test.DejaFu.STM import Test.DejaFu.STM
import Test.DejaFu.Types
import Test.DejaFu.Utils
#if MIN_VERSION_base(4,9,0) #if MIN_VERSION_base(4,9,0)
import qualified Control.Monad.Fail as Fail import qualified Control.Monad.Fail as Fail

3
dejafu/Test/DejaFu/Conc/Internal.hs
View File

@ -29,13 +29,14 @@ import Data.Monoid ((<>))
import Data.Sequence (Seq, (<|)) import Data.Sequence (Seq, (<|))
import qualified Data.Sequence as Seq import qualified Data.Sequence as Seq
import Test.DejaFu.Common
import Test.DejaFu.Conc.Internal.Common import Test.DejaFu.Conc.Internal.Common
import Test.DejaFu.Conc.Internal.Memory import Test.DejaFu.Conc.Internal.Memory
import Test.DejaFu.Conc.Internal.Threading import Test.DejaFu.Conc.Internal.Threading
import Test.DejaFu.Internal
import Test.DejaFu.Schedule import Test.DejaFu.Schedule
import Test.DejaFu.STM (Result(..), import Test.DejaFu.STM (Result(..),
runTransaction) runTransaction)
import Test.DejaFu.Types
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
-- * Execution -- * Execution

2
dejafu/Test/DejaFu/Conc/Internal/Common.hs
View File

@ -16,8 +16,8 @@ module Test.DejaFu.Conc.Internal.Common where
import Control.Exception (Exception, MaskingState(..)) import Control.Exception (Exception, MaskingState(..))
import Data.Map.Strict (Map) import Data.Map.Strict (Map)
import Test.DejaFu.Common
import Test.DejaFu.STM (STMLike) import Test.DejaFu.STM (STMLike)
import Test.DejaFu.Types
#if MIN_VERSION_base(4,9,0) #if MIN_VERSION_base(4,9,0)
import qualified Control.Monad.Fail as Fail import qualified Control.Monad.Fail as Fail

6
dejafu/Test/DejaFu/Conc/Internal/Memory.hs
View File

@ -26,16 +26,16 @@ module Test.DejaFu.Conc.Internal.Memory where
import Control.Monad.Ref (MonadRef, readRef, import Control.Monad.Ref (MonadRef, readRef,
writeRef) writeRef)
import Data.Map.Strict (Map) import Data.Map.Strict (Map)
import qualified Data.Map.Strict as M
import Data.Maybe (maybeToList) import Data.Maybe (maybeToList)
import Data.Monoid ((<>)) import Data.Monoid ((<>))
import Data.Sequence (Seq, ViewL(..), singleton, import Data.Sequence (Seq, ViewL(..), singleton,
viewl, (><)) viewl, (><))
import Test.DejaFu.Common
import Test.DejaFu.Conc.Internal.Common import Test.DejaFu.Conc.Internal.Common
import Test.DejaFu.Conc.Internal.Threading import Test.DejaFu.Conc.Internal.Threading
import Test.DejaFu.Internal
import qualified Data.Map.Strict as M import Test.DejaFu.Types
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
-- * Manipulating @CRef@s -- * Manipulating @CRef@s

3
dejafu/Test/DejaFu/Conc/Internal/Threading.hs
View File

@ -20,8 +20,9 @@ import Data.List (intersect)
import Data.Map.Strict (Map) import Data.Map.Strict (Map)
import Data.Maybe (isJust) import Data.Maybe (isJust)
import Test.DejaFu.Common
import Test.DejaFu.Conc.Internal.Common import Test.DejaFu.Conc.Internal.Common
import Test.DejaFu.Internal
import Test.DejaFu.Types
import qualified Data.Map.Strict as M import qualified Data.Map.Strict as M

2
dejafu/Test/DejaFu/Defaults.hs
View File

@ -9,8 +9,8 @@
-- Default parameters for test execution. -- Default parameters for test execution.
module Test.DejaFu.Defaults where module Test.DejaFu.Defaults where
import Test.DejaFu.Common
import Test.DejaFu.SCT import Test.DejaFu.SCT
import Test.DejaFu.Types
-- | A default way to execute concurrent programs: systematically -- | A default way to execute concurrent programs: systematically
-- using 'defaultBounds'. -- using 'defaultBounds'.

354
dejafu/Test/DejaFu/Internal.hs Normal file
View File

@ -0,0 +1,354 @@
-- |
-- Module : Test.DejaFu.Internal
-- Copyright : (c) 2017 Michael Walker
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- 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)

57
dejafu/Test/DejaFu/SCT.hs
View File

@ -25,8 +25,6 @@ module Test.DejaFu.SCT
, Discard(..) , Discard(..)
, runSCTDiscard , runSCTDiscard
, resultsSetDiscard , resultsSetDiscard
, weakenDiscard
, strengthenDiscard
-- ** Strict variants -- ** Strict variants
, runSCT' , runSCT'
@ -119,9 +117,10 @@ import Data.Set (Set)
import qualified Data.Set as S import qualified Data.Set as S
import System.Random (RandomGen, randomR) import System.Random (RandomGen, randomR)
import Test.DejaFu.Common
import Test.DejaFu.Conc import Test.DejaFu.Conc
import Test.DejaFu.Internal
import Test.DejaFu.SCT.Internal import Test.DejaFu.SCT.Internal
import Test.DejaFu.Types
------------------------------------------------------------------------------- -------------------------------------------------------------------------------
-- Running Concurrent Programs -- Running Concurrent Programs
@ -237,58 +236,6 @@ resultsSet :: (MonadConc n, MonadRef r n, Ord a)
-> n (Set (Either Failure a)) -> n (Set (Either Failure a))
resultsSet = resultsSetDiscard (const Nothing) 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. -- | A variant of 'runSCT' which can selectively discard results.
-- --
-- The exact executions tried, and the order in which results are -- The exact executions tried, and the order in which results are

3
dejafu/Test/DejaFu/SCT/Internal.hs
View File

@ -30,8 +30,9 @@ import Data.Set (Set)
import qualified Data.Set as S import qualified Data.Set as S
import System.Random (RandomGen, randomR) import System.Random (RandomGen, randomR)
import Test.DejaFu.Common import Test.DejaFu.Internal
import Test.DejaFu.Schedule (Scheduler(..), decisionOf, tidOf) import Test.DejaFu.Schedule (Scheduler(..), decisionOf, tidOf)
import Test.DejaFu.Types
------------------------------------------------------------------------------- -------------------------------------------------------------------------------
-- * Dynamic partial-order reduction -- * Dynamic partial-order reduction

6
dejafu/Test/DejaFu/STM.hs
View File

@ -20,7 +20,6 @@ module Test.DejaFu.STM
-- * Executing Transactions -- * Executing Transactions
, Result(..) , Result(..)
, TTrace
, TAction(..) , TAction(..)
, TVarId , TVarId
, runTransaction , runTransaction
@ -35,8 +34,9 @@ import Data.IORef (IORef)
import Data.STRef (STRef) import Data.STRef (STRef)
import qualified Control.Monad.STM.Class as C import qualified Control.Monad.STM.Class as C
import Test.DejaFu.Common import Test.DejaFu.Internal
import Test.DejaFu.STM.Internal import Test.DejaFu.STM.Internal
import Test.DejaFu.Types
#if MIN_VERSION_base(4,9,0) #if MIN_VERSION_base(4,9,0)
import qualified Control.Monad.Fail as Fail import qualified Control.Monad.Fail as Fail
@ -112,7 +112,7 @@ instance C.MonadSTM (STMLike n r) where
-- --
-- @since 0.4.0.0 -- @since 0.4.0.0
runTransaction :: MonadRef r n 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 runTransaction ma tvid = do
(res, undo, tvid', trace) <- doTransaction (runSTM ma) tvid (res, undo, tvid', trace) <- doTransaction (runSTM ma) tvid

17
dejafu/Test/DejaFu/STM/Internal.hs
View File

@ -16,16 +16,17 @@
-- public interface of this library. -- public interface of this library.
module Test.DejaFu.STM.Internal where module Test.DejaFu.STM.Internal where
import Control.DeepSeq (NFData(..)) import Control.DeepSeq (NFData(..))
import Control.Exception (Exception, SomeException, fromException, import Control.Exception (Exception, SomeException, fromException,
toException) toException)
import Control.Monad.Ref (MonadRef, newRef, readRef, writeRef) import Control.Monad.Ref (MonadRef, newRef, readRef, writeRef)
import Data.List (nub) import Data.List (nub)
import Test.DejaFu.Common import Test.DejaFu.Internal
import Test.DejaFu.Types
#if MIN_VERSION_base(4,9,0) #if MIN_VERSION_base(4,9,0)
import qualified Control.Monad.Fail as Fail import qualified Control.Monad.Fail as Fail
#endif #endif
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
@ -133,7 +134,7 @@ instance Foldable Result where
-- * Execution -- * Execution
-- | Run a STM transaction, returning an action to undo its effects. -- | 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 doTransaction ma idsource = do
(c, ref) <- runRefCont SStop (Just . Right) (runCont ma) (c, ref) <- runRefCont SStop (Just . Right) (runCont ma)
(idsource', undo, readen, written, trace) <- go ref c (pure ()) idsource [] [] [] (idsource', undo, readen, written, trace) <- go ref c (pure ()) idsource [] [] []

7
dejafu/Test/DejaFu/Schedule.hs
View File

@ -29,10 +29,11 @@ module Test.DejaFu.Schedule
, makeNonPreemptive , makeNonPreemptive
) where ) where
import Data.List.NonEmpty (NonEmpty(..), toList) import Data.List.NonEmpty (NonEmpty(..), toList)
import System.Random (RandomGen, randomR) 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 -- | A @Scheduler@ drives the execution of a concurrent program. The
-- parameters it takes are: -- parameters it takes are:

602
dejafu/Test/DejaFu/Types.hs Normal file
View File

@ -0,0 +1,602 @@
-- |
-- Module : Test.DejaFu.Types
-- Copyright : (c) 2017 Michael Walker
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- 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

77
dejafu/Test/DejaFu/Utils.hs Normal file
View File

@ -0,0 +1,77 @@
-- |
-- Module : Test.DejaFu.utils
-- Copyright : (c) 2017 Michael Walker
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- 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 [] = "<trace discarded>"
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

6
dejafu/dejafu.cabal
View File

@ -38,17 +38,19 @@ source-repository this
library library
exposed-modules: Test.DejaFu exposed-modules: Test.DejaFu
, Test.DejaFu.Conc , Test.DejaFu.Conc
, Test.DejaFu.Common
, Test.DejaFu.Defaults , Test.DejaFu.Defaults
, Test.DejaFu.Refinement , Test.DejaFu.Refinement
, Test.DejaFu.Schedule
, Test.DejaFu.SCT , Test.DejaFu.SCT
, Test.DejaFu.STM , Test.DejaFu.STM
, Test.DejaFu.Schedule
, Test.DejaFu.Types
, Test.DejaFu.Utils
, Test.DejaFu.Conc.Internal , Test.DejaFu.Conc.Internal
, Test.DejaFu.Conc.Internal.Common , Test.DejaFu.Conc.Internal.Common
, Test.DejaFu.Conc.Internal.Memory , Test.DejaFu.Conc.Internal.Memory
, Test.DejaFu.Conc.Internal.Threading , Test.DejaFu.Conc.Internal.Threading
, Test.DejaFu.Internal
, Test.DejaFu.SCT.Internal , Test.DejaFu.SCT.Internal
, Test.DejaFu.STM.Internal , Test.DejaFu.STM.Internal

3
hunit-dejafu/Test/HUnit/DejaFu.hs
View File

@ -74,6 +74,7 @@ import Test.DejaFu hiding (Testable(..))
import qualified Test.DejaFu.Conc as Conc import qualified Test.DejaFu.Conc as Conc
import qualified Test.DejaFu.Refinement as R import qualified Test.DejaFu.Refinement as R
import qualified Test.DejaFu.SCT as SCT import qualified Test.DejaFu.SCT as SCT
import qualified Test.DejaFu.Types as D
import Test.HUnit (Assertable(..), Test(..), Testable(..), import Test.HUnit (Assertable(..), Test(..), Testable(..),
assertFailure, assertString) assertFailure, assertString)
import Test.HUnit.Lang (HUnitFailure(..)) import Test.HUnit.Lang (HUnitFailure(..))
@ -264,7 +265,7 @@ testconc discard way memtype tests concio = case map toTest tests of
where where
toTest (name, p) = TestLabel name . TestCase $ do 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 traces <- SCT.runSCTDiscard discarder way memtype concio
assertString . showErr $ peval p traces assertString . showErr $ peval p traces

3
tasty-dejafu/Test/Tasty/DejaFu.hs
View File

@ -78,6 +78,7 @@ import Test.DejaFu hiding (Testable(..))
import qualified Test.DejaFu.Conc as Conc import qualified Test.DejaFu.Conc as Conc
import qualified Test.DejaFu.Refinement as R import qualified Test.DejaFu.Refinement as R
import qualified Test.DejaFu.SCT as SCT import qualified Test.DejaFu.SCT as SCT
import qualified Test.DejaFu.Types as D
import Test.Tasty (TestName, TestTree, testGroup) import Test.Tasty (TestName, TestTree, testGroup)
import Test.Tasty.Options (IsOption(..), OptionDescription(..), import Test.Tasty.Options (IsOption(..), OptionDescription(..),
lookupOption) lookupOption)
@ -328,7 +329,7 @@ testconc discard way memtype tests concio = case map toTest tests of
where where
toTest (name, p) = toTest (name, p) =
let discarder = SCT.strengthenDiscard discard (pdiscard p) let discarder = D.strengthenDiscard discard (pdiscard p)
traces = SCT.runSCTDiscard discarder way memtype concio traces = SCT.runSCTDiscard discarder way memtype concio
in singleTest name $ ConcTest traces (peval p) in singleTest name $ ConcTest traces (peval p)