diff --git a/dejafu/Test/DejaFu/Deterministic.hs b/dejafu/Test/DejaFu/Deterministic.hs index a6db919..5db3c5f 100755 --- a/dejafu/Test/DejaFu/Deterministic.hs +++ b/dejafu/Test/DejaFu/Deterministic.hs @@ -114,7 +114,7 @@ instance Monad n => C.MonadConc (Conc n r (STMLike n r)) where -- ---------- - newCRef a = toConc (\c -> ANewRef a c) + newCRefN n a = toConc (\c -> ANewRef n a c) readCRef ref = toConc (AReadRef ref) readForCAS ref = toConc (AReadRefCas ref) @@ -129,7 +129,7 @@ instance Monad n => C.MonadConc (Conc n r (STMLike n r)) where -- ---------- - newEmptyCVar = toConc (\c -> ANewVar c) + newEmptyCVarN n = toConc (\c -> ANewVar n c) putCVar var a = toConc (\c -> APutVar var a (c ())) readCVar var = toConc (AReadVar var) diff --git a/dejafu/Test/DejaFu/Deterministic/Internal.hs b/dejafu/Test/DejaFu/Deterministic/Internal.hs index cdba907..6e273f6 100755 --- a/dejafu/Test/DejaFu/Deterministic/Internal.hs +++ b/dejafu/Test/DejaFu/Deterministic/Internal.hs @@ -202,13 +202,13 @@ stepThread fixed runstm memtype action idSource tid threads wb caps = case actio AGetNumCapabilities c -> stepGetNumCapabilities c ASetNumCapabilities i c -> stepSetNumCapabilities i c AYield c -> stepYield c - ANewVar c -> stepNewVar c + ANewVar n c -> stepNewVar n c APutVar var a c -> stepPutVar var a c ATryPutVar var a c -> stepTryPutVar var a c AReadVar var c -> stepReadVar var c ATakeVar var c -> stepTakeVar var c ATryTakeVar var c -> stepTryTakeVar var c - ANewRef a c -> stepNewRef a c + ANewRef n a c -> stepNewRef n a c AReadRef ref c -> stepReadRef ref c AReadRefCas ref c -> stepReadRefCas ref c APeekTicket tick c -> stepPeekTicket tick c @@ -235,8 +235,7 @@ stepThread fixed runstm memtype action idSource tid threads wb caps = case actio -- | Start a new thread, assigning it the next 'ThreadId' stepFork n a b = return $ Right (goto (b newtid) tid threads', idSource', Fork newtid, wb, caps) where threads' = launch tid newtid a threads - (idSource', tid'@(ThreadId _ i)) = nextTId idSource - newtid = if null n then tid' else ThreadId (Just n) i + (idSource', newtid) = nextTId n idSource -- | Get the 'ThreadId' of the current thread stepMyTId c = simple (goto (c tid) tid threads) MyThreadId @@ -417,15 +416,15 @@ stepThread fixed runstm memtype action idSource tid threads wb caps = case actio threads' = goto c tid (mask m tid threads) -- | Create a new @CVar@, using the next 'CVarId'. - stepNewVar c = do - let (idSource', newcvid) = nextCVId idSource + stepNewVar n c = do + let (idSource', newcvid) = nextCVId n idSource ref <- newRef fixed Nothing let cvar = CVar newcvid ref return $ Right (knows [Left newcvid] tid $ goto (c cvar) tid threads, idSource', NewVar newcvid, wb, caps) -- | Create a new @CRef@, using the next 'CRefId'. - stepNewRef a c = do - let (idSource', newcrid) = nextCRId idSource + stepNewRef n a c = do + let (idSource', newcrid) = nextCRId n idSource ref <- newRef fixed (M.empty, 0, a) let cref = CRef newcrid ref return $ Right (goto (c cref) tid threads, idSource', NewRef newcrid, wb, caps) diff --git a/dejafu/Test/DejaFu/Deterministic/Internal/Common.hs b/dejafu/Test/DejaFu/Deterministic/Internal/Common.hs index 73cbf47..3412ee5 100755 --- a/dejafu/Test/DejaFu/Deterministic/Internal/Common.hs +++ b/dejafu/Test/DejaFu/Deterministic/Internal/Common.hs @@ -97,14 +97,14 @@ data Action n r s = | AGetNumCapabilities (Int -> Action n r s) | ASetNumCapabilities Int (Action n r s) - | forall a. ANewVar (CVar r a -> Action n r s) + | forall a. ANewVar String (CVar r a -> Action n r s) | forall a. APutVar (CVar r a) a (Action n r s) | forall a. ATryPutVar (CVar r a) a (Bool -> Action n r s) | forall a. AReadVar (CVar r a) (a -> Action n r s) | forall a. ATakeVar (CVar r a) (a -> Action n r s) | forall a. ATryTakeVar (CVar r a) (Maybe a -> Action n r s) - | forall a. ANewRef a (CRef r 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) @@ -182,17 +182,40 @@ instance NFData CRefId where -- | The number of ID parameters was getting a bit unwieldy, so this -- hides them all away. -data IdSource = Id { _nextCRId :: Int, _nextCVId :: Int, _nextCTVId :: CTVarId, _nextTId :: Int } +data IdSource = Id + { _nextCRId :: Int + , _nextCVId :: Int + , _nextCTVId :: CTVarId + , _nextTId :: Int + , _usedCRNames :: [String] + , _usedCVNames :: [String] + , _usedTNames :: [String] } -- | Get the next free 'CRefId'. -nextCRId :: IdSource -> (IdSource, CRefId) -nextCRId idsource = (idsource { _nextCRId = newid }, CRefId Nothing newid) - where newid = _nextCRId idsource + 1 +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 -- | Get the next free 'CVarId'. -nextCVId :: IdSource -> (IdSource, CVarId) -nextCVId idsource = (idsource { _nextCVId = newid }, CVarId Nothing newid) where - newid = _nextCVId idsource + 1 +nextCVId :: String -> IdSource -> (IdSource, CVarId) +nextCVId name idsource = (idsource { _nextCVId = newid, _usedCVNames = newlst }, CVarId 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 -- | Get the next free 'CTVarId'. nextCTVId :: IdSource -> (IdSource, CTVarId) @@ -200,13 +223,21 @@ nextCTVId idsource = (idsource { _nextCTVId = newid }, newid) where newid = _nextCTVId idsource + 1 -- | Get the next free 'ThreadId'. -nextTId :: IdSource -> (IdSource, ThreadId) -nextTId idsource = (idsource { _nextTId = newid }, ThreadId Nothing newid) where - newid = _nextTId idsource + 1 +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 -- | The initial ID source. initialIdSource :: IdSource -initialIdSource = Id 0 0 0 0 +initialIdSource = Id 0 0 0 0 [] [] [] -------------------------------------------------------------------------------- -- * Scheduling & Traces @@ -519,13 +550,13 @@ lookahead = unsafeToNonEmpty . lookahead' where lookahead' (AMyTId _) = [WillMyThreadId] lookahead' (AGetNumCapabilities _) = [WillGetNumCapabilities] lookahead' (ASetNumCapabilities i k) = WillSetNumCapabilities i : lookahead' k - lookahead' (ANewVar _) = [WillNewVar] + lookahead' (ANewVar _ _) = [WillNewVar] lookahead' (APutVar (CVar c _) _ k) = WillPutVar c : lookahead' k lookahead' (ATryPutVar (CVar c _) _ _) = [WillTryPutVar c] lookahead' (AReadVar (CVar c _) _) = [WillReadVar c] lookahead' (ATakeVar (CVar c _) _) = [WillTakeVar c] lookahead' (ATryTakeVar (CVar c _) _) = [WillTryTakeVar c] - lookahead' (ANewRef _ _) = [WillNewRef] + lookahead' (ANewRef _ _ _) = [WillNewRef] lookahead' (AReadRef (CRef r _) _) = [WillReadRef r] lookahead' (AReadRefCas (CRef r _) _) = [WillReadRefCas r] lookahead' (APeekTicket (Ticket r _ _) _) = [WillPeekTicket r]