module Test.DejaFu.Common
(
ThreadId(..)
, CRefId(..)
, MVarId(..)
, TVarId(..)
, initialThread
, IdSource(..)
, nextCRId
, nextMVId
, nextTVId
, nextTId
, initialIdSource
, ThreadAction(..)
, isBlock
, tvarsOf
, Lookahead(..)
, rewind
, willRelease
, ActionType(..)
, isBarrier
, isCommit
, synchronises
, crefOf
, mvarOf
, simplifyAction
, simplifyLookahead
, TTrace
, TAction(..)
, Trace
, Decision(..)
, showTrace
, preEmpCount
, Failure(..)
, showFail
, MemType(..)
) where
import Control.DeepSeq (NFData(..))
import Control.Exception (MaskingState(..))
import Data.Dynamic (Dynamic)
import Data.List (sort, nub, intercalate)
import Data.Maybe (fromMaybe, mapMaybe)
import Data.Set (Set)
import qualified Data.Set as S
import Test.DPOR (Decision(..), Trace)
data ThreadId = ThreadId (Maybe String) Int
deriving Eq
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
instance NFData ThreadId where
rnf (ThreadId n i) = rnf (n, i)
data CRefId = CRefId (Maybe String) Int
deriving Eq
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
instance NFData CRefId where
rnf (CRefId n i) = rnf (n, i)
data MVarId = MVarId (Maybe String) Int
deriving Eq
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
instance NFData MVarId where
rnf (MVarId n i) = rnf (n, i)
data TVarId = TVarId (Maybe String) Int
deriving Eq
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
instance NFData TVarId where
rnf (TVarId n i) = rnf (n, i)
initialThread :: ThreadId
initialThread = ThreadId (Just "main") 0
data IdSource = Id
{ _nextCRId :: Int
, _nextMVId :: Int
, _nextTVId :: Int
, _nextTId :: Int
, _usedCRNames :: [String]
, _usedMVNames :: [String]
, _usedTVNames :: [String]
, _usedTNames :: [String]
}
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)
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)
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)
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)
initialIdSource :: IdSource
initialIdSource = Id 0 0 0 0 [] [] [] []
data ThreadAction =
Fork ThreadId
| MyThreadId
| GetNumCapabilities Int
| SetNumCapabilities Int
| Yield
| NewVar MVarId
| PutVar MVarId [ThreadId]
| BlockedPutVar MVarId
| TryPutVar MVarId Bool [ThreadId]
| ReadVar MVarId
| BlockedReadVar MVarId
| TakeVar MVarId [ThreadId]
| BlockedTakeVar MVarId
| TryTakeVar MVarId Bool [ThreadId]
| NewRef CRefId
| ReadRef CRefId
| ReadRefCas CRefId
| ModRef CRefId
| ModRefCas CRefId
| WriteRef CRefId
| CasRef CRefId Bool
| CommitRef ThreadId CRefId
| STM TTrace [ThreadId]
| BlockedSTM TTrace
| Catching
| PopCatching
| Throw
| ThrowTo ThreadId
| BlockedThrowTo ThreadId
| Killed
| SetMasking Bool MaskingState
| ResetMasking Bool MaskingState
| LiftIO
| Return
| Message Dynamic
| Stop
deriving Show
instance NFData ThreadAction where
rnf (Fork t) = rnf t
rnf (GetNumCapabilities i) = rnf i
rnf (SetNumCapabilities i) = rnf i
rnf (NewVar c) = rnf c
rnf (PutVar c ts) = rnf (c, ts)
rnf (BlockedPutVar c) = rnf c
rnf (TryPutVar c b ts) = rnf (c, b, ts)
rnf (ReadVar c) = rnf c
rnf (BlockedReadVar c) = rnf c
rnf (TakeVar c ts) = rnf (c, ts)
rnf (BlockedTakeVar c) = rnf c
rnf (TryTakeVar c b ts) = rnf (c, b, ts)
rnf (NewRef c) = rnf c
rnf (ReadRef c) = rnf c
rnf (ReadRefCas c) = rnf c
rnf (ModRef c) = rnf c
rnf (ModRefCas c) = rnf c
rnf (WriteRef c) = rnf c
rnf (CasRef c b) = rnf (c, b)
rnf (CommitRef t c) = rnf (t, c)
rnf (STM s ts) = rnf (s, ts)
rnf (BlockedSTM s) = rnf s
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 (Message m) = m `seq` ()
rnf a = a `seq` ()
isBlock :: ThreadAction -> Bool
isBlock (BlockedThrowTo _) = True
isBlock (BlockedTakeVar _) = True
isBlock (BlockedReadVar _) = True
isBlock (BlockedPutVar _) = True
isBlock (BlockedSTM _) = True
isBlock _ = False
tvarsOf :: ThreadAction -> Set TVarId
tvarsOf act = S.fromList $ case act of
STM trc _ -> concatMap tvarsOf' trc
BlockedSTM trc -> concatMap tvarsOf' trc
_ -> []
where
tvarsOf' (TRead 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' _ = []
data Lookahead =
WillFork
| WillMyThreadId
| WillGetNumCapabilities
| WillSetNumCapabilities Int
| WillYield
| WillNewVar
| WillPutVar MVarId
| WillTryPutVar MVarId
| WillReadVar MVarId
| WillTakeVar MVarId
| WillTryTakeVar MVarId
| WillNewRef
| WillReadRef CRefId
| WillReadRefCas CRefId
| WillModRef CRefId
| WillModRefCas CRefId
| WillWriteRef CRefId
| WillCasRef CRefId
| WillCommitRef ThreadId CRefId
| WillSTM
| WillCatching
| WillPopCatching
| WillThrow
| WillThrowTo ThreadId
| WillSetMasking Bool MaskingState
| WillResetMasking Bool MaskingState
| WillLiftIO
| WillReturn
| WillMessage Dynamic
| WillStop
deriving Show
instance NFData Lookahead where
rnf (WillSetNumCapabilities i) = rnf i
rnf (WillPutVar c) = rnf c
rnf (WillTryPutVar c) = rnf c
rnf (WillReadVar c) = rnf c
rnf (WillTakeVar c) = rnf c
rnf (WillTryTakeVar c) = rnf c
rnf (WillReadRef c) = rnf c
rnf (WillReadRefCas c) = rnf c
rnf (WillModRef c) = rnf c
rnf (WillModRefCas c) = rnf c
rnf (WillWriteRef c) = rnf c
rnf (WillCasRef c) = rnf c
rnf (WillCommitRef 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 (WillMessage m) = m `seq` ()
rnf l = l `seq` ()
rewind :: ThreadAction -> Maybe Lookahead
rewind (Fork _) = Just WillFork
rewind MyThreadId = Just WillMyThreadId
rewind (GetNumCapabilities _) = Just WillGetNumCapabilities
rewind (SetNumCapabilities i) = Just (WillSetNumCapabilities i)
rewind Yield = Just WillYield
rewind (NewVar _) = Just WillNewVar
rewind (PutVar c _) = Just (WillPutVar c)
rewind (BlockedPutVar c) = Just (WillPutVar c)
rewind (TryPutVar c _ _) = Just (WillTryPutVar c)
rewind (ReadVar c) = Just (WillReadVar c)
rewind (BlockedReadVar c) = Just (WillReadVar c)
rewind (TakeVar c _) = Just (WillTakeVar c)
rewind (BlockedTakeVar c) = Just (WillTakeVar c)
rewind (TryTakeVar c _ _) = Just (WillTryTakeVar c)
rewind (NewRef _) = Just WillNewRef
rewind (ReadRef c) = Just (WillReadRef c)
rewind (ReadRefCas c) = Just (WillReadRefCas c)
rewind (ModRef c) = Just (WillModRef c)
rewind (ModRefCas c) = Just (WillModRefCas c)
rewind (WriteRef c) = Just (WillWriteRef c)
rewind (CasRef c _) = Just (WillCasRef c)
rewind (CommitRef t c) = Just (WillCommitRef 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 (Message m) = Just (WillMessage m)
rewind Stop = Just WillStop
willRelease :: Lookahead -> Bool
willRelease WillFork = True
willRelease WillYield = True
willRelease (WillPutVar _) = True
willRelease (WillTryPutVar _) = True
willRelease (WillReadVar _) = True
willRelease (WillTakeVar _) = True
willRelease (WillTryTakeVar _) = True
willRelease WillSTM = True
willRelease WillThrow = True
willRelease (WillSetMasking _ _) = True
willRelease (WillResetMasking _ _) = True
willRelease WillStop = 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 r) = rnf r
rnf (UnsynchronisedWrite r) = rnf r
rnf (PartiallySynchronisedCommit r) = rnf r
rnf (PartiallySynchronisedWrite r) = rnf r
rnf (PartiallySynchronisedModify r) = rnf r
rnf (SynchronisedModify r) = rnf r
rnf (SynchronisedRead c) = rnf c
rnf (SynchronisedWrite c) = rnf c
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
simplifyAction :: ThreadAction -> ActionType
simplifyAction = maybe UnsynchronisedOther simplifyLookahead . rewind
simplifyLookahead :: Lookahead -> ActionType
simplifyLookahead (WillPutVar c) = SynchronisedWrite c
simplifyLookahead (WillTryPutVar c) = SynchronisedWrite c
simplifyLookahead (WillReadVar c) = SynchronisedRead c
simplifyLookahead (WillTakeVar c) = SynchronisedRead c
simplifyLookahead (WillTryTakeVar c) = SynchronisedRead c
simplifyLookahead (WillReadRef r) = UnsynchronisedRead r
simplifyLookahead (WillReadRefCas r) = UnsynchronisedRead r
simplifyLookahead (WillModRef r) = SynchronisedModify r
simplifyLookahead (WillModRefCas r) = PartiallySynchronisedModify r
simplifyLookahead (WillWriteRef r) = UnsynchronisedWrite r
simplifyLookahead (WillCasRef r) = PartiallySynchronisedWrite r
simplifyLookahead (WillCommitRef _ r) = PartiallySynchronisedCommit r
simplifyLookahead WillSTM = SynchronisedOther
simplifyLookahead (WillThrowTo _) = SynchronisedOther
simplifyLookahead _ = UnsynchronisedOther
type TTrace = [TAction]
data TAction =
TNew
| TRead TVarId
| TWrite TVarId
| TRetry
| TOrElse TTrace (Maybe TTrace)
| TThrow
| TCatch TTrace (Maybe TTrace)
| TStop
deriving (Eq, Show)
instance NFData TAction where
rnf (TRead v) = rnf v
rnf (TWrite v) = rnf v
rnf (TCatch s m) = rnf (s, m)
rnf (TOrElse s m) = rnf (s, m)
rnf a = a `seq` ()
showTrace :: Trace ThreadId ThreadAction Lookahead -> String
showTrace trc = intercalate "\n" $ concatMap go trc : strkey where
go (_,_,CommitRef _ _) = "C-"
go (Start (ThreadId _ i),_,_) = "S" ++ show i ++ "-"
go (SwitchTo (ThreadId _ i),_,_) = "P" ++ show i ++ "-"
go (Continue,_,_) = "-"
strkey = [" " ++ show i ++ ": " ++ name | (i, name) <- key]
key = sort . nub $ mapMaybe toKey trc where
toKey (Start (ThreadId (Just name) i), _, _)
| i > 0 = Just (i, name)
toKey _ = Nothing
preEmpCount :: [(Decision ThreadId, ThreadAction)]
-> (Decision ThreadId, Lookahead)
-> Int
preEmpCount ts (d, _) = go initialThread Nothing ts where
go _ (Just Yield) ((SwitchTo t, a):rest) = go t (Just a) rest
go tid prior ((SwitchTo t, a):rest)
| isCommitThread t = go tid prior (skip rest)
| otherwise = 1 + go t (Just a) rest
go _ _ ((Start t, a):rest) = go t (Just a) rest
go tid _ ((Continue, a):rest) = go tid (Just a) rest
go _ prior [] = case (prior, d) of
(Just Yield, SwitchTo _) -> 0
(_, SwitchTo _) -> 1
_ -> 0
isCommitThread = (< initialThread)
skip = dropWhile (not . isContextSwitch . fst)
isContextSwitch Continue = False
isContextSwitch _ = True
data Failure =
InternalError
| Abort
| Deadlock
| STMDeadlock
| UncaughtException
deriving (Eq, Show, Read, Ord, Enum, Bounded)
instance NFData Failure where
rnf f = f `seq` ()
showFail :: Failure -> String
showFail Abort = "[abort]"
showFail Deadlock = "[deadlock]"
showFail STMDeadlock = "[stm-deadlock]"
showFail InternalError = "[internal-error]"
showFail UncaughtException = "[exception]"
data MemType =
SequentialConsistency
| TotalStoreOrder
| PartialStoreOrder
deriving (Eq, Show, Read, Ord, Enum, Bounded)
instance NFData MemType where
rnf m = m `seq` ()
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)