module Test.DejaFu.Deterministic.Internal.Common where
import Control.DeepSeq (NFData(..))
import Control.Exception (Exception, MaskingState(..))
import Data.Dynamic (Dynamic)
import Data.Map.Strict (Map)
import Data.Maybe (mapMaybe)
import Data.List (sort, nub, intercalate)
import Data.List.NonEmpty (NonEmpty, fromList)
import Test.DejaFu.Internal
import Test.DPOR (Decision(..), Trace)
newtype M n r s a = M { runM :: (a -> Action n r s) -> Action n r s }
instance Functor (M n r s) where
fmap f m = M $ \ c -> runM m (c . f)
instance Applicative (M n r s) where
pure x = M $ \c -> AReturn $ c x
f <*> v = M $ \c -> runM f (\g -> runM v (c . g))
instance Monad (M n r s) where
return = pure
m >>= k = M $ \c -> runM m (\x -> runM (k x) c)
data MVar r a = MVar
{ _cvarId :: MVarId
, _cvarVal :: r (Maybe a)
}
data CRef r a = CRef
{ _crefId :: CRefId
, _crefVal :: r (Map ThreadId a, Integer, a)
}
data Ticket a = Ticket
{ _ticketCRef :: CRefId
, _ticketWrites :: Integer
, _ticketVal :: a
}
type Fixed n r s = Ref n r (M n r s)
cont :: ((a -> Action n r s) -> Action n r s) -> M n r s a
cont = M
runCont :: M n r s a -> (a -> Action n r s) -> Action n r s
runCont = runM
data Action n r s =
AFork String ((forall b. M n r s b -> M n r s b) -> Action n r s) (ThreadId -> Action n r s)
| AMyTId (ThreadId -> Action n r s)
| AGetNumCapabilities (Int -> Action n r s)
| ASetNumCapabilities Int (Action n r s)
| forall a. ANewVar String (MVar r a -> Action n r s)
| forall a. APutVar (MVar r a) a (Action n r s)
| forall a. ATryPutVar (MVar r a) a (Bool -> Action n r s)
| forall a. AReadVar (MVar r a) (a -> Action n r s)
| forall a. ATakeVar (MVar r a) (a -> Action n r s)
| forall a. ATryTakeVar (MVar r a) (Maybe a -> Action n r s)
| forall a. ANewRef String a (CRef r a -> Action n r s)
| forall a. AReadRef (CRef r a) (a -> Action n r s)
| forall a. AReadRefCas (CRef r a) (Ticket a -> Action n r s)
| forall a. APeekTicket (Ticket a) (a -> Action n r s)
| forall a b. AModRef (CRef r a) (a -> (a, b)) (b -> Action n r s)
| forall a b. AModRefCas (CRef r a) (a -> (a, b)) (b -> Action n r s)
| forall a. AWriteRef (CRef r a) a (Action n r s)
| forall a. ACasRef (CRef r a) (Ticket a) a ((Bool, Ticket a) -> Action n r s)
| forall e. Exception e => AThrow e
| forall e. Exception e => AThrowTo ThreadId e (Action n r s)
| forall a e. Exception e => ACatching (e -> M n r s a) (M n r s a) (a -> Action n r s)
| APopCatching (Action n r s)
| forall a. AMasking MaskingState ((forall b. M n r s b -> M n r s b) -> M n r s a) (a -> Action n r s)
| AResetMask Bool Bool MaskingState (Action n r s)
| AKnowsAbout (Either MVarId TVarId) (Action n r s)
| AForgets (Either MVarId TVarId) (Action n r s)
| AAllKnown (Action n r s)
| AMessage Dynamic (Action n r s)
| forall a. AAtom (s a) (a -> Action n r s)
| ALift (n (Action n r s))
| AYield (Action n r s)
| AReturn (Action n r s)
| ACommit ThreadId CRefId
| AStop
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)
initialThread :: ThreadId
initialThread = ThreadId (Just "main") 0
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 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 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)
data IdSource = Id
{ _nextCRId :: Int
, _nextCVId :: Int
, _nextTVId :: Int
, _nextTId :: Int
, _usedCRNames :: [String]
, _usedCVNames :: [String]
, _usedTVNames :: [String]
, _usedTNames :: [String] }
nextCRId :: String -> IdSource -> (IdSource, CRefId)
nextCRId name idsource = (idsource { _nextCRId = newid, _usedCRNames = newlst }, CRefId newname newid) where
newid = _nextCRId idsource + 1
newlst
| null name = _usedCRNames idsource
| otherwise = name : _usedCRNames idsource
newname
| null name = Nothing
| occurrences > 0 = Just (name ++ "-" ++ show occurrences)
| otherwise = Just name
occurrences = length . filter (==name) $ _usedCRNames idsource
nextCVId :: String -> IdSource -> (IdSource, MVarId)
nextCVId name idsource = (idsource { _nextCVId = newid, _usedCVNames = newlst }, MVarId newname newid) where
newid = _nextCVId idsource + 1
newlst
| null name = _usedCVNames idsource
| otherwise = name : _usedCVNames idsource
newname
| null name = Nothing
| occurrences > 0 = Just (name ++ "-" ++ show occurrences)
| otherwise = Just name
occurrences = length . filter (==name) $ _usedCVNames idsource
nextTVId :: String -> IdSource -> (IdSource, TVarId)
nextTVId name idsource = (idsource { _nextTVId = newid, _usedTVNames = newlst }, TVarId newname newid) where
newid = _nextTVId idsource + 1
newlst
| null name = _usedTVNames idsource
| otherwise = name : _usedTVNames idsource
newname
| null name = Nothing
| occurrences > 0 = Just (name ++ "-" ++ show occurrences)
| otherwise = Just name
occurrences = length . filter (==name) $ _usedTVNames idsource
nextTId :: String -> IdSource -> (IdSource, ThreadId)
nextTId name idsource = (idsource { _nextTId = newid, _usedTNames = newlst }, ThreadId newname newid) where
newid = _nextTId idsource + 1
newlst
| null name = _usedTNames idsource
| otherwise = name : _usedTNames idsource
newname
| null name = Nothing
| occurrences > 0 = Just (name ++ "-" ++ show occurrences)
| otherwise = Just name
occurrences = length . filter (==name) $ _usedTNames idsource
initialIdSource :: IdSource
initialIdSource = Id 0 0 0 0 [] [] [] []
showTrace :: Trace ThreadId ThreadAction Lookahead -> String
showTrace trc = intercalate "\n" $ trace "" 0 trc : (map (" "++) . sort . nub $ mapMaybe toKey trc) where
trace prefix num ((_,_,CommitRef _ _):ds) = thread prefix num ++ trace "C" 1 ds
trace prefix num ((Start (ThreadId _ i),_,_):ds) = thread prefix num ++ trace ("S" ++ show i) 1 ds
trace prefix num ((SwitchTo (ThreadId _ i),_,_):ds) = thread prefix num ++ trace ("P" ++ show i) 1 ds
trace prefix num ((Continue,_,_):ds) = trace prefix (num + 1) ds
trace prefix num [] = thread prefix num
thread prefix num = prefix ++ replicate num '-'
toKey (Start (ThreadId (Just name) i), _, _) = Just $ show i ++ ": " ++ name
toKey _ = Nothing
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
| PeekTicket 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
| Lift
| Return
| KnowsAbout
| Forgets
| AllKnown
| 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 (PeekTicket 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
type TTrace = [TAction]
data TAction =
TNew
| TRead TVarId
| TWrite TVarId
| TRetry
| TOrElse TTrace (Maybe TTrace)
| TThrow
| TCatch TTrace (Maybe TTrace)
| TStop
| TLift
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` ()
data Lookahead =
WillFork
| WillMyThreadId
| WillGetNumCapabilities
| WillSetNumCapabilities Int
| WillYield
| WillNewVar
| WillPutVar MVarId
| WillTryPutVar MVarId
| WillReadVar MVarId
| WillTakeVar MVarId
| WillTryTakeVar MVarId
| WillNewRef
| WillReadRef CRefId
| WillPeekTicket 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
| WillLift
| WillReturn
| WillKnowsAbout
| WillForgets
| WillAllKnown
| 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 (WillPeekTicket 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 (PeekTicket c) = Just (WillPeekTicket 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 Lift = Just WillLift
rewind Return = Just WillReturn
rewind KnowsAbout = Just WillKnowsAbout
rewind Forgets = Just WillForgets
rewind AllKnown = Just WillAllKnown
rewind (Message m) = Just (WillMessage m)
rewind Stop = Just WillStop
lookahead :: Action n r s -> NonEmpty Lookahead
lookahead = fromList . lookahead' where
lookahead' (AFork _ _ _) = [WillFork]
lookahead' (AMyTId _) = [WillMyThreadId]
lookahead' (AGetNumCapabilities _) = [WillGetNumCapabilities]
lookahead' (ASetNumCapabilities i k) = WillSetNumCapabilities i : lookahead' k
lookahead' (ANewVar _ _) = [WillNewVar]
lookahead' (APutVar (MVar c _) _ k) = WillPutVar c : lookahead' k
lookahead' (ATryPutVar (MVar c _) _ _) = [WillTryPutVar c]
lookahead' (AReadVar (MVar c _) _) = [WillReadVar c]
lookahead' (ATakeVar (MVar c _) _) = [WillTakeVar c]
lookahead' (ATryTakeVar (MVar c _) _) = [WillTryTakeVar c]
lookahead' (ANewRef _ _ _) = [WillNewRef]
lookahead' (AReadRef (CRef r _) _) = [WillReadRef r]
lookahead' (AReadRefCas (CRef r _) _) = [WillReadRefCas r]
lookahead' (APeekTicket (Ticket r _ _) _) = [WillPeekTicket r]
lookahead' (AModRef (CRef r _) _ _) = [WillModRef r]
lookahead' (AModRefCas (CRef r _) _ _) = [WillModRefCas r]
lookahead' (AWriteRef (CRef r _) _ k) = WillWriteRef r : lookahead' k
lookahead' (ACasRef (CRef r _) _ _ _) = [WillCasRef r]
lookahead' (ACommit t c) = [WillCommitRef t c]
lookahead' (AAtom _ _) = [WillSTM]
lookahead' (AThrow _) = [WillThrow]
lookahead' (AThrowTo tid _ k) = WillThrowTo tid : lookahead' k
lookahead' (ACatching _ _ _) = [WillCatching]
lookahead' (APopCatching k) = WillPopCatching : lookahead' k
lookahead' (AMasking ms _ _) = [WillSetMasking False ms]
lookahead' (AResetMask b1 b2 ms k) = (if b1 then WillSetMasking else WillResetMasking) b2 ms : lookahead' k
lookahead' (ALift _) = [WillLift]
lookahead' (AKnowsAbout _ k) = WillKnowsAbout : lookahead' k
lookahead' (AForgets _ k) = WillForgets : lookahead' k
lookahead' (AAllKnown k) = WillAllKnown : lookahead' k
lookahead' (AMessage m k) = WillMessage m : lookahead' k
lookahead' (AYield k) = WillYield : lookahead' k
lookahead' (AReturn k) = WillReturn : lookahead' k
lookahead' AStop = [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
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 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
cvarOf :: ActionType -> Maybe MVarId
cvarOf (SynchronisedRead c) = Just c
cvarOf (SynchronisedWrite c) = Just c
cvarOf _ = Nothing
simplify :: ThreadAction -> ActionType
simplify = maybe UnsynchronisedOther simplify' . rewind
simplify' :: Lookahead -> ActionType
simplify' (WillPutVar c) = SynchronisedWrite c
simplify' (WillTryPutVar c) = SynchronisedWrite c
simplify' (WillReadVar c) = SynchronisedRead c
simplify' (WillTakeVar c) = SynchronisedRead c
simplify' (WillTryTakeVar c) = SynchronisedRead c
simplify' (WillReadRef r) = UnsynchronisedRead r
simplify' (WillReadRefCas r) = UnsynchronisedRead r
simplify' (WillModRef r) = SynchronisedModify r
simplify' (WillModRefCas r) = PartiallySynchronisedModify r
simplify' (WillWriteRef r) = UnsynchronisedWrite r
simplify' (WillCasRef r) = PartiallySynchronisedWrite r
simplify' (WillCommitRef _ r) = PartiallySynchronisedCommit r
simplify' WillSTM = SynchronisedOther
simplify' (WillThrowTo _) = SynchronisedOther
simplify' _ = UnsynchronisedOther
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` ()