module Test.DejaFu.Internal where
import Control.DeepSeq (NFData(..))
import Control.Monad.Ref (MonadRef(..))
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.Map.Strict as M
import Data.Maybe (fromMaybe)
import Data.Set (Set)
import qualified Data.Set as S
import System.Random (RandomGen)
import Test.DejaFu.Types
data Settings n a = Settings
{ _way :: Way
, _memtype :: MemType
, _discard :: Maybe (Either Failure a -> Maybe Discard)
, _debugShow :: Maybe (a -> String)
, _debugPrint :: Maybe (String -> n ())
, _earlyExit :: Maybe (Either Failure a -> Bool)
}
data Way where
Systematic :: Bounds -> Way
Weighted :: RandomGen g => g -> Int -> Int -> Way
Uniform :: RandomGen g => g -> Int -> Way
instance Show Way where
show (Systematic bs) = "Systematic (" ++ show bs ++ ")"
show (Weighted _ n t) = "Weighted <gen> " ++ show (n, t)
show (Uniform _ n) = "Uniform <gen> " ++ show n
data IdSource = IdSource
{ _crids :: (Int, [String])
, _mvids :: (Int, [String])
, _tvids :: (Int, [String])
, _tids :: (Int, [String])
} deriving (Eq, Ord, Show)
instance NFData IdSource where
rnf idsource = rnf ( _crids idsource
, _mvids idsource
, _tvids idsource
, _tids idsource
)
nextCRId :: String -> IdSource -> (IdSource, CRefId)
nextCRId name idsource =
let (crid, crids') = nextId name (_crids idsource)
in (idsource { _crids = crids' }, CRefId crid)
nextMVId :: String -> IdSource -> (IdSource, MVarId)
nextMVId name idsource =
let (mvid, mvids') = nextId name (_mvids idsource)
in (idsource { _mvids = mvids' }, MVarId mvid)
nextTVId :: String -> IdSource -> (IdSource, TVarId)
nextTVId name idsource =
let (tvid, tvids') = nextId name (_tvids idsource)
in (idsource { _tvids = tvids' }, TVarId tvid)
nextTId :: String -> IdSource -> (IdSource, ThreadId)
nextTId name idsource =
let (tid, tids') = nextId name (_tids idsource)
in (idsource { _tids = tids' }, ThreadId tid)
nextId :: String -> (Int, [String]) -> (Id, (Int, [String]))
nextId name (num, used) = (Id newName (num+1), (num+1, 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)
initialIdSource :: IdSource
initialIdSource = IdSource (0, []) (0, []) (0, []) (0, [])
isBlock :: ThreadAction -> Bool
isBlock (BlockedThrowTo _) = True
isBlock (BlockedTakeMVar _) = True
isBlock (BlockedReadMVar _) = True
isBlock (BlockedPutMVar _) = True
isBlock (BlockedSTM _) = True
isBlock _ = False
tvarsOf :: ThreadAction -> Set TVarId
tvarsOf act = tvarsRead act `S.union` tvarsWritten act
tvarsWritten :: ThreadAction -> Set TVarId
tvarsWritten act = S.fromList $ case act of
STM trc _ -> concatMap tvarsOf' trc
BlockedSTM trc -> concatMap tvarsOf' trc
_ -> []
where
tvarsOf' (TNew tv) = [tv]
tvarsOf' (TWrite tv) = [tv]
tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)
tvarsOf' (TCatch ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)
tvarsOf' _ = []
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' _ = []
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
rewind (DontCheck _) = Just WillDontCheck
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 WillDontCheck = True
willRelease _ = False
data ActionType =
UnsynchronisedRead CRefId
| UnsynchronisedWrite CRefId
| UnsynchronisedOther
| PartiallySynchronisedCommit CRefId
| PartiallySynchronisedWrite CRefId
| PartiallySynchronisedModify CRefId
| SynchronisedModify CRefId
| SynchronisedRead MVarId
| SynchronisedWrite MVarId
| SynchronisedOther
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` ()
isBarrier :: ActionType -> Bool
isBarrier (SynchronisedModify _) = True
isBarrier (SynchronisedRead _) = True
isBarrier (SynchronisedWrite _) = True
isBarrier SynchronisedOther = True
isBarrier _ = False
isCommit :: ActionType -> CRefId -> Bool
isCommit (PartiallySynchronisedCommit c) r = c == r
isCommit (PartiallySynchronisedWrite c) r = c == r
isCommit (PartiallySynchronisedModify c) r = c == r
isCommit _ _ = False
synchronises :: ActionType -> CRefId -> Bool
synchronises a r = isCommit a r || isBarrier a
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
mvarOf :: ActionType -> Maybe MVarId
mvarOf (SynchronisedRead c) = Just c
mvarOf (SynchronisedWrite c) = Just c
mvarOf _ = Nothing
tidsOf :: ThreadAction -> Set ThreadId
tidsOf (Fork tid) = S.singleton tid
tidsOf (ForkOS tid) = S.singleton tid
tidsOf (PutMVar _ tids) = S.fromList tids
tidsOf (TryPutMVar _ _ tids) = S.fromList tids
tidsOf (TakeMVar _ tids) = S.fromList tids
tidsOf (TryTakeMVar _ _ tids) = S.fromList tids
tidsOf (CommitCRef tid _) = S.singleton tid
tidsOf (STM _ tids) = S.fromList tids
tidsOf (ThrowTo tid) = S.singleton tid
tidsOf (BlockedThrowTo tid) = S.singleton tid
tidsOf _ = S.empty
simplifyAction :: ThreadAction -> ActionType
simplifyAction = maybe UnsynchronisedOther simplifyLookahead . rewind
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
etail :: String -> [a] -> [a]
etail _ (_:xs) = xs
etail src _ = fatal src "tail: empty list"
eidx :: String -> [a] -> Int -> a
eidx src xs i
| i < length xs = xs !! i
| otherwise = fatal src "(!!): index too large"
efromJust :: String -> Maybe a -> a
efromJust _ (Just x) = x
efromJust src _ = fatal src "fromJust: Nothing"
efromList :: String -> [a] -> NonEmpty a
efromList _ (x:xs) = x:|xs
efromList src _ = fatal src "fromList: empty list"
eadjust :: (Ord k, Show k) => String -> (v -> v) -> k -> M.Map k v -> M.Map k v
eadjust src f k m = case M.lookup k m of
Just v -> M.insert k (f v) m
Nothing -> fatal src ("adjust: key '" ++ show k ++ "' not found")
einsert :: (Ord k, Show k) => String -> k -> v -> M.Map k v -> M.Map k v
einsert src k v m
| M.member k m = fatal src ("insert: key '" ++ show k ++ "' already present")
| otherwise = M.insert k v m
elookup :: (Ord k, Show k) => String -> k -> M.Map k v -> v
elookup src k =
fromMaybe (fatal src ("lookup: key '" ++ show k ++ "' not found")) .
M.lookup k
fatal :: String -> String -> a
fatal src msg = error ("(dejafu: " ++ src ++ ") " ++ msg)
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)