From a15a109b60b577ca4ef0053323b89d6ae7ab4af7 Mon Sep 17 00:00:00 2001 From: Michael Walker Date: Tue, 3 Feb 2015 14:14:36 +0000 Subject: [PATCH] Give CVars IDs --- Test/DejaFu/Deterministic.hs | 5 +- Test/DejaFu/Deterministic/IO.hs | 5 +- Test/DejaFu/Deterministic/Internal.hs | 167 ++++++++++++++------------ Test/DejaFu/SCT/Bounding.hs | 16 +-- 4 files changed, 103 insertions(+), 90 deletions(-) mode change 100644 => 100755 Test/DejaFu/Deterministic/Internal.hs diff --git a/Test/DejaFu/Deterministic.hs b/Test/DejaFu/Deterministic.hs index 7bdb655..2b9da9c 100755 --- a/Test/DejaFu/Deterministic.hs +++ b/Test/DejaFu/Deterministic.hs @@ -28,6 +28,7 @@ module Test.DejaFu.Deterministic , Trace , Decision , ThreadAction + , CVarId , showTrace -- * Scheduling @@ -93,8 +94,8 @@ fork (C ma) = C $ cont $ \c -> AFork (runCont ma $ const AStop) $ c () -- | Create a new empty 'CVar'. newEmptyCVar :: Conc t (CVar t a) newEmptyCVar = C $ cont lifted where - lifted c = ANew $ c <$> newEmptyCVar' - newEmptyCVar' = V <$> newSTRef (Nothing, []) + lifted c = ANew $ \cvid -> c <$> newEmptyCVar' cvid + newEmptyCVar' cvid = V <$> newSTRef (cvid, Nothing, []) -- | Block on a 'CVar' until it is empty, then write to it. putCVar :: CVar t a -> a -> Conc t () diff --git a/Test/DejaFu/Deterministic/IO.hs b/Test/DejaFu/Deterministic/IO.hs index 12519b8..9572267 100644 --- a/Test/DejaFu/Deterministic/IO.hs +++ b/Test/DejaFu/Deterministic/IO.hs @@ -32,6 +32,7 @@ module Test.DejaFu.Deterministic.IO , Trace , Decision , ThreadAction + , CVarId , showTrace -- * Scheduling @@ -98,8 +99,8 @@ fork (C ma) = C $ cont $ \c -> AFork (runCont ma $ const AStop) $ c () -- | Create a new empty 'CVar'. newEmptyCVar :: ConcIO t (CVar t a) newEmptyCVar = C $ cont lifted where - lifted c = ANew $ c <$> newEmptyCVar' - newEmptyCVar' = V <$> newIORef (Nothing, []) + lifted c = ANew $ \cvid -> c <$> newEmptyCVar' cvid + newEmptyCVar' cvid = V <$> newIORef (cvid, Nothing, []) -- | Block on a 'CVar' until it is empty, then write to it. putCVar :: CVar t a -> a -> ConcIO t () diff --git a/Test/DejaFu/Deterministic/Internal.hs b/Test/DejaFu/Deterministic/Internal.hs old mode 100644 new mode 100755 index f686a31..0163ad4 --- a/Test/DejaFu/Deterministic/Internal.hs +++ b/Test/DejaFu/Deterministic/Internal.hs @@ -6,7 +6,7 @@ module Test.DejaFu.Deterministic.Internal where import Control.DeepSeq (NFData(..)) -import Control.Monad (mapAndUnzipM) +import Control.Monad (liftM, mapAndUnzipM) import Control.Monad.Cont (Cont, runCont) import Data.List.Extra import Data.Map (Map) @@ -19,9 +19,9 @@ import qualified Data.Map as M -- | The underlying monad is based on continuations over Actions. type M n r a = Cont (Action n r) a --- | CVars are represented as a reference containing a maybe value, --- and a list of things blocked on it. -type R r a = r (Maybe a, [Block]) +-- | CVars are represented as a reference containing a Maybe value, a +-- list of things blocked on it, and a unique numeric identifier. +type R r a = r (CVarId, Maybe a, [Block]) -- | Dict of methods for concrete implementations to override. data Fixed c n r t = F @@ -51,16 +51,16 @@ data Action n r = | forall a. AGet (R r a) (a -> Action n r) | forall a. ATake (R r a) (a -> Action n r) | forall a. ATryTake (R r a) (Maybe a -> Action n r) - | ANew (n (Action n r)) + | ANew (CVarId -> n (Action n r)) | ALift (n (Action n r)) | AStop --- | Every live thread has a unique identitifer. These are implemented --- as integers, but you shouldn't assume they are necessarily --- contiguous, or globally unique (although it is the case that no two --- threads alive at the same time will have the same identifier). +-- | Every live thread has a unique identitifer. type ThreadId = Int +-- | Every 'CVar' also has a unique identifier. +type CVarId = Int + -- | A @Scheduler@ maintains some internal state, @s@, takes the -- 'ThreadId' of the last thread scheduled, and the list of runnable -- threads. It produces a 'ThreadId' to schedule, and a new state. @@ -109,23 +109,23 @@ instance NFData Decision where data ThreadAction = Fork ThreadId -- ^ Start a new thread. - | New + | New CVarId -- ^ Create a new 'CVar'. - | Put [ThreadId] + | Put CVarId [ThreadId] -- ^ Put into a 'CVar', possibly waking up some threads. - | BlockedPut + | BlockedPut CVarId -- ^ Get blocked on a put. - | TryPut Bool [ThreadId] + | TryPut CVarId Bool [ThreadId] -- ^ Try to put into a 'CVar', possibly waking up some threads. - | Read + | Read CVarId -- ^ Read from a 'CVar'. - | BlockedRead + | BlockedRead CVarId -- ^ Get blocked on a read. - | Take [ThreadId] + | Take CVarId [ThreadId] -- ^ Take from a 'CVar', possibly waking up some threads. - | BlockedTake + | BlockedTake CVarId -- ^ Get blocked on a take. - | TryTake Bool [ThreadId] + | TryTake CVarId Bool [ThreadId] -- ^ Try to take from a 'CVar', possibly waking up some threads. | Lift -- ^ Lift an action from the underlying monad. Note that the @@ -136,16 +136,16 @@ data ThreadAction = deriving (Eq, Show) instance NFData ThreadAction where - rnf (TryTake b tids) = rnf (b, tids) - rnf (TryPut b tids) = rnf (b, tids) - rnf (Fork tid) = rnf tid - rnf (Take tids) = rnf tids - rnf (Put tids) = rnf tids - rnf BlockedRead = () - rnf BlockedTake = () - rnf BlockedPut = () - rnf New = () - rnf Read = () + rnf (TryTake c b tids) = rnf (c, b, tids) + rnf (TryPut c b tids) = rnf (c, b, tids) + rnf (BlockedRead c) = rnf c + rnf (BlockedTake c) = rnf c + rnf (BlockedPut c) = rnf c + rnf (Take c tids) = rnf (c, tids) + rnf (Put c tids) = rnf (c, tids) + rnf (Fork tid) = rnf tid + rnf (New c) = rnf c + rnf (Read c) = rnf c rnf Lift = () rnf Stop = () @@ -161,7 +161,7 @@ runFixed fixed sched s ma = do let c = getCont fixed $ ma >>= liftN fixed . writeRef fixed ref . Just let threads = M.fromList [(0, (runCont c $ const AStop, False))] - (s', trace) <- runThreads fixed [] (negate 1) sched s threads ref + (s', trace) <- runThreads fixed (-1, 0) [] (negate 1) sched s threads ref out <- readRef fixed ref return (out, s', reverse trace) @@ -184,16 +184,20 @@ type Threads n r = Map ThreadId (Action n r, Bool) -- exposed to users of the library, this is just an internal gotcha to -- watch out for. runThreads :: (Monad (c t), Monad n) => Fixed c n r t - -> Trace -> ThreadId -> Scheduler s -> s -> Threads n r -> r (Maybe a) -> n (s, Trace) -runThreads fixed sofar prior sched s threads ref + -> (CVarId, ThreadId) -> Trace -> ThreadId -> Scheduler s -> s -> Threads n r -> r (Maybe a) -> n (s, Trace) +runThreads fixed (lastcvid, lasttid) sofar prior sched s threads ref | isTerminated = return (s, sofar) | isDeadlocked = writeRef fixed ref Nothing >> return (s, sofar) | isNonexistant = writeRef fixed ref Nothing >> return (s, sofar) | isBlocked = writeRef fixed ref Nothing >> return (s, sofar) | otherwise = do - (threads', act) <- stepThread (fst $ fromJust thread) fixed chosen threads + (threads', act) <- stepThread (fst $ fromJust thread) fixed (lastcvid, lasttid) chosen threads let sofar' = (decision, alternatives, act) : sofar - runThreads fixed sofar' chosen sched s' threads' ref + + let lastcvid' = case act of { New c -> c; _ -> lastcvid } + let lasttid' = case act of { Fork t -> t; _ -> lasttid } + + runThreads fixed (lastcvid', lasttid') sofar' chosen sched s' threads' ref where (chosen, s') = if prior == -1 then (0, s) else sched s prior $ head runnable' :| tail runnable' @@ -219,7 +223,7 @@ runThreads fixed sofar prior sched s threads ref -- 'Action'. stepThread :: (Monad (c t), Monad n) => Action n r - -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) + -> Fixed c n r t -> (CVarId, ThreadId) -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) stepThread (AFork a b) = stepFork a b stepThread (APut ref a c) = stepPut ref a c stepThread (ATryPut ref a c) = stepTryPut ref a c @@ -233,89 +237,97 @@ stepThread AStop = stepStop -- | Start a new thread, assigning it a unique 'ThreadId' stepFork :: (Monad (c t), Monad n) => Action n r -> Action n r - -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) -stepFork a b _ i threads = return (goto b i threads', Fork newid) where - (threads', newid) = launch a threads + -> Fixed c n r t -> (CVarId, ThreadId) -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) +stepFork a b _ (_, lasttid) i threads = return (goto b i threads', Fork newtid ) where + threads' = launch newtid a threads + newtid = lasttid + 1 -- | Put a value into a @CVar@, blocking the thread until it's empty. stepPut :: (Monad (c t), Monad n) => R r a -> a -> Action n r - -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) -stepPut ref a c fixed i threads = do + -> Fixed c n r t -> (CVarId, ThreadId) -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) +stepPut ref a c fixed _ i threads = do (success, threads', woken) <- putIntoCVar True ref a (const c) fixed i threads - return (threads', if success then Put woken else BlockedPut) + cvid <- getCVarId fixed ref + return (threads', if success then Put cvid woken else BlockedPut cvid) -- | Try to put a value into a @CVar@, without blocking. stepTryPut :: (Monad (c t), Monad n) => R r a -> a -> (Bool -> Action n r) - -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) -stepTryPut ref a c fixed i threads = do + -> Fixed c n r t -> (CVarId, ThreadId) -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) +stepTryPut ref a c fixed _ i threads = do (success, threads', woken) <- putIntoCVar False ref a c fixed i threads - return (threads', TryPut success woken) + cvid <- getCVarId fixed ref + return (threads', TryPut cvid success woken) -- | Get the value from a @CVar@, without emptying, blocking the -- thread until it's full. stepGet :: (Monad (c t), Monad n) => R r a -> (a -> Action n r) - -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) -stepGet ref c fixed i threads = do - (val, _) <- readRef fixed ref + -> Fixed c n r t -> (CVarId, ThreadId) -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) +stepGet ref c fixed _ i threads = do + (cvid, val, _) <- readRef fixed ref case val of - Just val' -> return (goto (c val') i threads, Read) + Just val' -> return (goto (c val') i threads, Read cvid) Nothing -> do threads' <- block fixed ref WaitFull i threads - return (threads', BlockedRead) + return (threads', BlockedRead cvid) -- | Take the value from a @CVar@, blocking the thread until it's -- full. stepTake :: (Monad (c t), Monad n) => R r a -> (a -> Action n r) - -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) -stepTake ref c fixed i threads = do + -> Fixed c n r t -> (CVarId, ThreadId) -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) +stepTake ref c fixed _ i threads = do (success, threads', woken) <- takeFromCVar True ref (c . fromJust) fixed i threads - return (threads', if success then Take woken else BlockedTake) + cvid <- getCVarId fixed ref + return (threads', if success then Take cvid woken else BlockedTake cvid) -- | Try to take the value from a @CVar@, without blocking. stepTryTake :: (Monad (c t), Monad n) => R r a -> (Maybe a -> Action n r) - -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) -stepTryTake ref c fixed i threads = do + -> Fixed c n r t -> (CVarId, ThreadId) -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) +stepTryTake ref c fixed _ i threads = do (success, threads', woken) <- takeFromCVar True ref c fixed i threads - return (threads', TryTake success woken) + cvid <- getCVarId fixed ref + return (threads', TryTake cvid success woken) --- | Create a new @CVar@. This is exactly the same as lifting a value, --- except by separating the two we can (a) produce a more useful --- trace, and (b) make smarter pre-emption decisions. +-- | Create a new @CVar@. stepNew :: (Monad (c t), Monad n) - => n (Action n r) - -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) -stepNew na _ i threads = do - a <- na - return (goto a i threads, New) + => (CVarId -> n (Action n r)) + -> Fixed c n r t -> (CVarId, ThreadId) -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) +stepNew na _ (lastcvid, _) i threads = do + let newcvid = lastcvid + 1 + a <- na newcvid + return (goto a i threads, New newcvid) -- | Lift an action from the underlying monad into the @Conc@ -- computation. stepLift :: (Monad (c t), Monad n) => n (Action n r) - -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) -stepLift na _ i threads = do + -> Fixed c n r t -> (CVarId, ThreadId) -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) +stepLift na _ _ i threads = do a <- na return (goto a i threads, Lift) -- | Kill the current thread. stepStop :: (Monad (c t), Monad n) - => Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) -stepStop _ i threads = return (kill i threads, Stop) + => Fixed c n r t -> (CVarId, ThreadId) -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction) +stepStop _ _ i threads = return (kill i threads, Stop) -- * Manipulating @CVar@s +-- | Get the ID of a CVar +getCVarId :: (Monad (c t), Monad n) => Fixed c n r t -> R r a -> n CVarId +getCVarId fixed ref = (\(cvid,_,_) -> cvid) `liftM` readRef fixed ref + -- | Put a value into a @CVar@, in either a blocking or nonblocking -- way. putIntoCVar :: (Monad (c t), Monad n) => Bool -> R r a -> a -> (Bool -> Action n r) -> Fixed c n r t -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId]) putIntoCVar blocking ref a c fixed i threads = do - (val, blocks) <- readRef fixed ref + (cvid, val, blocks) <- readRef fixed ref case val of Just _ @@ -327,7 +339,7 @@ putIntoCVar blocking ref a c fixed i threads = do return (False, goto (c False) i threads, []) Nothing -> do - writeRef fixed ref (Just a, blocks) + writeRef fixed ref (cvid, Just a, blocks) (threads', woken) <- wake fixed ref WaitFull threads return (True, goto (c True) i threads', woken) @@ -337,11 +349,11 @@ takeFromCVar :: (Monad (c t), Monad n) => Bool -> R r a -> (Maybe a -> Action n r) -> Fixed c n r t -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId]) takeFromCVar blocking ref c fixed i threads = do - (val, blocks) <- readRef fixed ref + (cvid, val, blocks) <- readRef fixed ref case val of Just _ -> do - writeRef fixed ref (Nothing, blocks) + writeRef fixed ref (cvid, Nothing, blocks) (threads', woken) <- wake fixed ref WaitEmpty threads return (True, goto (c val) i threads', woken) @@ -363,14 +375,13 @@ goto a = M.alter $ \(Just (_, b)) -> Just (a, b) block :: (Monad (c t), Monad n) => Fixed c n r t -> R r a -> (ThreadId -> Block) -> ThreadId -> Threads n r -> n (Threads n r) block fixed ref typ tid threads = do - (val, blocks) <- readRef fixed ref - writeRef fixed ref (val, typ tid : blocks) + (cvid, val, blocks) <- readRef fixed ref + writeRef fixed ref (cvid, val, typ tid : blocks) return $ M.alter (\(Just (a, _)) -> Just (a, True)) tid threads --- | Start a thread with the next free ID. -launch :: Action n r -> Threads n r -> (Threads n r, ThreadId) -launch a m = (M.insert k (a, False) m, k) where - k = succ . maximum $ M.keys m +-- | Start a thread with the given ID. This must not already be in use! +launch :: ThreadId -> Action n r -> Threads n r -> Threads n r +launch tid a = M.insert tid (a, False) -- | Kill a thread. kill :: ThreadId -> Threads n r -> Threads n r @@ -387,10 +398,10 @@ wake fixed ref typ m = do where wake' a@(tid, (act, True)) = do let blck = typ tid - (val, blocks) <- readRef fixed ref + (cvid, val, blocks) <- readRef fixed ref if blck `elem` blocks - then writeRef fixed ref (val, filter (/= blck) blocks) >> return ((tid, (act, False)), Just tid) + then writeRef fixed ref (cvid, val, filter (/= blck) blocks) >> return ((tid, (act, False)), Just tid) else return (a, Nothing) wake' a = return (a, Nothing) diff --git a/Test/DejaFu/SCT/Bounding.hs b/Test/DejaFu/SCT/Bounding.hs index b873ba1..b4075f3 100755 --- a/Test/DejaFu/SCT/Bounding.hs +++ b/Test/DejaFu/SCT/Bounding.hs @@ -218,13 +218,13 @@ bStep siblings offspring blim (s, g) t = case _next g of -- | Check if a 'ThreadAction' might be an interesting candidate for -- pre-empting or delaying. interesting :: Bool -> ThreadAction -> Bool -interesting _ (Put _) = True -interesting _ (TryPut _ _) = True -interesting _ (Take _) = True -interesting _ (TryTake _ _) = True -interesting _ BlockedPut = True -interesting _ Read = True -interesting _ BlockedRead = True -interesting _ BlockedTake = True +interesting _ (Put _ _) = True +interesting _ (TryPut _ _ _) = True +interesting _ (Take _ _) = True +interesting _ (TryTake _ _ _) = True +interesting _ (BlockedPut _) = True +interesting _ (Read _) = True +interesting _ (BlockedRead _) = True +interesting _ (BlockedTake _) = True interesting l Lift = l interesting _ _ = False