diff --git a/.gitignore b/.gitignore new file mode 100644 index 00000000..48a004cd --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +dist-newstyle diff --git a/io-classes/src/Control/Monad/Class/MonadFork.hs b/io-classes/src/Control/Monad/Class/MonadFork.hs index ced7e2d8..5c6f034a 100644 --- a/io-classes/src/Control/Monad/Class/MonadFork.hs +++ b/io-classes/src/Control/Monad/Class/MonadFork.hs @@ -16,7 +16,8 @@ import qualified Control.Concurrent as IO import Control.Exception (AsyncException (ThreadKilled), Exception) import Control.Monad.Reader (ReaderT (..), lift) import Data.Kind (Type) -import qualified GHC.Conc.Sync as IO (labelThread) +import GHC.Conc (ThreadStatus) +import qualified GHC.Conc.Sync as IO (labelThread, threadStatus) class (Monad m, Eq (ThreadId m), @@ -27,6 +28,7 @@ class (Monad m, Eq (ThreadId m), myThreadId :: m (ThreadId m) labelThread :: ThreadId m -> String -> m () + threadStatus :: ThreadId m -> m ThreadStatus class MonadThread m => MonadFork m where @@ -53,6 +55,7 @@ instance MonadThread IO where type ThreadId IO = IO.ThreadId myThreadId = IO.myThreadId labelThread = IO.labelThread + threadStatus = IO.threadStatus instance MonadFork IO where forkIO = IO.forkIO @@ -65,6 +68,7 @@ instance MonadThread m => MonadThread (ReaderT r m) where type ThreadId (ReaderT r m) = ThreadId m myThreadId = lift myThreadId labelThread t l = lift (labelThread t l) + threadStatus t = lift (threadStatus t) instance MonadFork m => MonadFork (ReaderT e m) where forkIO (ReaderT f) = ReaderT $ \e -> forkIO (f e) diff --git a/io-sim/src/Control/Monad/IOSim/CommonTypes.hs b/io-sim/src/Control/Monad/IOSim/CommonTypes.hs index 10e15e5e..c65f4aa3 100644 --- a/io-sim/src/Control/Monad/IOSim/CommonTypes.hs +++ b/io-sim/src/Control/Monad/IOSim/CommonTypes.hs @@ -80,5 +80,10 @@ instance Eq (TVar s a) where data SomeTVar s where SomeTVar :: !(TVar s a) -> SomeTVar s -data Deschedule = Yield | Interruptable | Blocked | Terminated | Sleep +-- | The reason a thread finished running +data FinishedReason = FinishedNormally + | FinishedDied + deriving (Ord, Eq, Show, Enum, Bounded) + +data Deschedule = Yield | Interruptable | Blocked | Terminated FinishedReason | Sleep deriving Show diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index f5c684be..74b5a611 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -69,6 +69,7 @@ import Deque.Strict (Deque) import qualified Deque.Strict as Deque import GHC.Exts (fromList) +import GHC.Conc (ThreadStatus(..), BlockReason(..)) import Control.Exception (NonTermination (..), assert, throw) import Control.Monad (join) @@ -122,7 +123,6 @@ labelledThreads threadMap = -- data TimerVars s = TimerVars !(TVar s TimeoutState) !(TVar s Bool) - -- | Internal state. -- data SimState s a = SimState { @@ -130,6 +130,8 @@ data SimState s a = SimState { -- | All threads other than the currently running thread: both running -- and blocked threads. threads :: !(Map ThreadId (Thread s a)), + -- | Keep track of the reason threads finished for 'threadStatus' + finished :: !(Map ThreadId FinishedReason), -- | current time curTime :: !Time, -- | ordered list of timers @@ -145,6 +147,7 @@ initialState = SimState { runqueue = mempty, threads = Map.empty, + finished = Map.empty, curTime = Time 0, timers = PSQ.empty, clocks = Map.singleton (ClockId []) epoch1970, @@ -189,6 +192,7 @@ schedule !thread@Thread{ !simstate@SimState { runqueue, threads, + finished, timers, clocks, nextVid, nextTmid, @@ -207,9 +211,9 @@ schedule !thread@Thread{ ForkFrame -> do -- this thread is done - !trace <- deschedule Terminated thread simstate + !trace <- deschedule (Terminated FinishedNormally) thread simstate return $ SimTrace time tid tlbl EventThreadFinished - $ SimTrace time tid tlbl (EventDeschedule Terminated) + $ SimTrace time tid tlbl (EventDeschedule $ Terminated FinishedNormally) $ trace MaskFrame k maskst' ctl' -> do @@ -227,7 +231,7 @@ schedule !thread@Thread{ let thread' = thread { threadControl = ThreadControl (k x) ctl' } schedule thread' simstate - Throw e -> {-# SCC "schedule.Throw" #-} + Throw thrower e -> {-# SCC "schedule.Throw" #-} case unwindControlStack e thread of Right thread'@Thread { threadMasking = maskst' } -> do -- We found a suitable exception handler, continue with that @@ -246,10 +250,12 @@ schedule !thread@Thread{ | otherwise -> do -- An unhandled exception in any other thread terminates the thread - !trace <- deschedule Terminated thread simstate + let reason | ThrowSelf <- thrower = FinishedNormally + | otherwise = FinishedDied + !trace <- deschedule (Terminated reason) thread simstate return $ SimTrace time tid tlbl (EventThrow e) $ SimTrace time tid tlbl (EventThreadUnhandled e) - $ SimTrace time tid tlbl (EventDeschedule Terminated) + $ SimTrace time tid tlbl (EventDeschedule $ Terminated reason) $ trace Catch action' handler k -> @@ -265,7 +271,7 @@ schedule !thread@Thread{ case mbWHNF of Left e -> do -- schedule this thread to immediately raise the exception - let thread' = thread { threadControl = ThreadControl (Throw e) ctl } + let thread' = thread { threadControl = ThreadControl (Throw ThrowSelf e) ctl } schedule thread' simstate Right whnf -> do -- continue with the resulting WHNF @@ -465,7 +471,7 @@ schedule !thread@Thread{ StmTxAborted _read e -> do -- schedule this thread to immediately raise the exception - let thread' = thread { threadControl = ThreadControl (Throw e) ctl } + let thread' = thread { threadControl = ThreadControl (Throw ThrowSelf e) ctl } !trace <- schedule thread' simstate return $ SimTrace time tid tlbl (EventTxAborted Nothing) trace @@ -494,6 +500,19 @@ schedule !thread@Thread{ threads' = Map.adjust (\t -> t { threadLabel = Just l }) tid' threads schedule thread' simstate { threads = threads' } + ThreadStatus tid' k -> + {-# SCC "schedule.ThreadStatus" #-} do + let result | Just r <- Map.lookup tid' finished = reasonToStatus r + | Just t <- Map.lookup tid' threads = threadStatus t + | otherwise = error "The impossible happened - tried to loookup thread in state." + reasonToStatus FinishedNormally = ThreadFinished + reasonToStatus FinishedDied = ThreadDied + threadStatus t | threadBlocked t = ThreadBlocked BlockedOnOther + | otherwise = ThreadRunning + + thread' = thread { threadControl = ThreadControl (k result) ctl } + schedule thread' simstate + GetMaskState k -> {-# SCC "schedule.GetMaskState" #-} do let thread' = thread { threadControl = ThreadControl (k maskst) ctl } @@ -518,7 +537,7 @@ schedule !thread@Thread{ {-# SCC "schedule.ThrowTo" #-} do -- Throw to ourself is equivalent to a synchronous throw, -- and works irrespective of masking state since it does not block. - let thread' = thread { threadControl = ThreadControl (Throw e) ctl } + let thread' = thread { threadControl = ThreadControl (Throw ThrowSelf e) ctl } trace <- schedule thread' simstate return (SimTrace time tid tlbl (EventThrowTo e tid) trace) @@ -548,8 +567,11 @@ schedule !thread@Thread{ -- be resolved if the thread terminates or if it leaves the exception -- handler (when restoring the masking state would trigger the any -- new pending async exception). - let adjustTarget t@Thread{ threadControl = ThreadControl _ ctl' } = - t { threadControl = ThreadControl (Throw e) ctl' + let thrower = case threadMasking <$> Map.lookup tid' threads of + Just Unmasked -> ThrowOther + _ -> ThrowSelf + adjustTarget t@Thread{ threadControl = ThreadControl _ ctl' } = + t { threadControl = ThreadControl (Throw thrower e) ctl' , threadBlocked = False } simstate'@SimState { threads = threads' } @@ -618,7 +640,7 @@ deschedule Interruptable !thread@Thread { -- So immediately raise the exception and unblock the blocked thread -- if possible. {-# SCC "deschedule.Interruptable.Unmasked" #-} - let thread' = thread { threadControl = ThreadControl (Throw e) ctl + let thread' = thread { threadControl = ThreadControl (Throw ThrowSelf e) ctl , threadMasking = MaskedInterruptible , threadThrowTo = etids } (unblocked, @@ -653,13 +675,16 @@ deschedule Blocked !thread !simstate@SimState{threads} = threads' = Map.insert (threadId thread') thread' threads in reschedule simstate { threads = threads' } -deschedule Terminated !thread !simstate@SimState{ curTime = time, threads } = +deschedule (Terminated reason) !thread !simstate@SimState{ curTime = time, threads } = -- This thread is done. If there are other threads blocked in a -- ThrowTo targeted at this thread then we can wake them up now. {-# SCC "deschedule.Terminated" #-} let !wakeup = map (l_labelled . snd) (reverse (threadThrowTo thread)) (unblocked, - !simstate') = unblockThreads wakeup simstate + !simstate') = unblockThreads wakeup + simstate { finished = Map.insert (threadId thread) + reason + (finished simstate) } in do !trace <- reschedule simstate' return $ traceMany diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index 951bb681..2dbd6cca 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -59,6 +59,7 @@ module Control.Monad.IOSim.Types , module Control.Monad.IOSim.CommonTypes , SimM , SimSTM + , Thrower (..) ) where import Control.Applicative @@ -112,6 +113,8 @@ import Control.Monad.IOSim.CommonTypes import Control.Monad.IOSim.STM import Control.Monad.IOSimPOR.Types +import GHC.Conc (ThreadStatus) + import qualified System.IO.Error as IO.Error (userError) @@ -130,6 +133,8 @@ traceM x = IOSim $ oneShot $ \k -> Output (toDyn x) (k ()) traceSTM :: Typeable a => a -> STMSim s () traceSTM x = STM $ oneShot $ \k -> OutputStm (toDyn x) (k ()) +data Thrower = ThrowSelf | ThrowOther deriving (Ord, Eq, Show) + data SimA s a where Return :: a -> SimA s a @@ -147,7 +152,7 @@ data SimA s a where UpdateTimeout:: Timeout (IOSim s) -> DiffTime -> SimA s b -> SimA s b CancelTimeout:: Timeout (IOSim s) -> SimA s b -> SimA s b - Throw :: SomeException -> SimA s a + Throw :: Thrower -> SomeException -> SimA s a Catch :: Exception e => SimA s a -> (e -> SimA s a) -> (a -> SimA s b) -> SimA s b Evaluate :: a -> (a -> SimA s b) -> SimA s b @@ -155,6 +160,7 @@ data SimA s a where Fork :: IOSim s () -> (ThreadId -> SimA s b) -> SimA s b GetThreadId :: (ThreadId -> SimA s b) -> SimA s b LabelThread :: ThreadId -> String -> SimA s b -> SimA s b + ThreadStatus :: ThreadId -> (ThreadStatus -> SimA s b) -> SimA s b Atomically :: STM s a -> (a -> SimA s b) -> SimA s b @@ -241,7 +247,7 @@ instance Monoid a => Monoid (IOSim s a) where #endif instance Fail.MonadFail (IOSim s) where - fail msg = IOSim $ oneShot $ \_ -> Throw (toException (IO.Error.userError msg)) + fail msg = IOSim $ oneShot $ \_ -> Throw ThrowSelf (toException (IO.Error.userError msg)) instance MonadFix (IOSim s) where mfix f = IOSim $ oneShot $ \k -> Fix f k @@ -288,7 +294,7 @@ instance MonadSay (IOSim s) where say msg = IOSim $ oneShot $ \k -> Say msg (k ()) instance MonadThrow (IOSim s) where - throwIO e = IOSim $ oneShot $ \_ -> Throw (toException e) + throwIO e = IOSim $ oneShot $ \_ -> Throw ThrowSelf (toException e) instance MonadEvaluate (IOSim s) where evaluate a = IOSim $ oneShot $ \k -> Evaluate a k @@ -366,6 +372,7 @@ instance MonadThread (IOSim s) where type ThreadId (IOSim s) = ThreadId myThreadId = IOSim $ oneShot $ \k -> GetThreadId k labelThread t l = IOSim $ oneShot $ \k -> LabelThread t l (k ()) + threadStatus t = IOSim $ oneShot $ \k -> ThreadStatus t k instance MonadFork (IOSim s) where forkIO task = IOSim $ oneShot $ \k -> Fork task k @@ -799,6 +806,7 @@ data SimEventType | EventPerformAction StepId | EventReschedule ScheduleControl | EventUnblocked [ThreadId] + | EventThreadStatus ThreadId ThreadId deriving Show type TraceEvent = SimEventType diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index 18894af2..ebda7281 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -89,6 +89,8 @@ import Control.Monad.IOSim.Types (SimEvent) import Control.Monad.IOSimPOR.Timeout (unsafeTimeout) import Control.Monad.IOSimPOR.Types +import GHC.Conc (ThreadStatus(..), BlockReason(..)) + -- -- Simulation interpreter -- @@ -122,7 +124,6 @@ isNotRacyThreadId :: ThreadId -> Bool isNotRacyThreadId (ThreadId _) = True isNotRacyThreadId _ = False - bottomVClock :: VectorClock bottomVClock = VectorClock Map.empty @@ -171,6 +172,8 @@ data SimState s a = SimState { -- | All threads other than the currently running thread: both running -- and blocked threads. threads :: !(Map ThreadId (Thread s a)), + -- | All finished threads (needed for threadStatus) + finished :: !(Map ThreadId (FinishedReason, VectorClock)), -- | current time curTime :: !Time, -- | ordered list of timers @@ -196,6 +199,7 @@ initialState = SimState { runqueue = PSQ.empty, threads = Map.empty, + finished = Map.empty, curTime = Time 0, timers = PSQ.empty, clocks = Map.singleton (ClockId []) epoch1970, @@ -211,14 +215,15 @@ initialState = invariant :: Maybe (Thread s a) -> SimState s a -> x -> x -invariant (Just running) simstate@SimState{runqueue,threads,clocks} = +invariant (Just running) simstate@SimState{runqueue,threads,finished,clocks} = assert (not (threadBlocked running)) + . assert (threadId running `Map.notMember` finished) . assert (threadId running `Map.notMember` threads) . assert (not (Down (threadId running) `PSQ.member` runqueue)) . assert (threadClockId running `Map.member` clocks) . invariant Nothing simstate -invariant Nothing SimState{runqueue,threads,clocks} = +invariant Nothing SimState{runqueue,threads,finished,clocks} = assert (PSQ.fold' (\(Down tid) _ _ a -> tid `Map.member` threads && a) True runqueue) . assert (and [ (threadBlocked t || threadDone t) == not (Down (threadId t) `PSQ.member` runqueue) | t <- Map.elems threads ]) @@ -227,6 +232,7 @@ invariant Nothing SimState{runqueue,threads,clocks} = (drop 1 (PSQ.toList runqueue)))) . assert (and [ threadClockId t `Map.member` clocks | t <- Map.elems threads ]) + . assert (Map.keysSet finished == Map.keysSet (Map.filter threadDone threads)) -- | Interpret the simulation monotonic time as a 'NominalDiffTime' since -- the start. @@ -255,6 +261,7 @@ schedule thread@Thread{ simstate@SimState { runqueue, threads, + finished, timers, clocks, nextVid, nextTmid, @@ -274,7 +281,9 @@ schedule thread@Thread{ -- follow. We should be at the beginning of a step; -- we put the present thread to sleep and reschedule -- the correct thread. - assert (effect == mempty) $ + -- The assertion says that the only effect that may have + -- happened in the start of a thread is us waking up. + assert (effect { effectStatusWrites = filter (/= tid) (effectStatusWrites effect) } == mempty) $ ( SimPORTrace time tid tstep tlbl (EventAwaitControl (tid,tstep) control) . SimPORTrace time tid tstep tlbl (EventDeschedule Sleep) ) <$> deschedule Sleep thread simstate @@ -305,15 +314,17 @@ schedule thread@Thread{ ForkFrame -> do -- this thread is done - !trace <- deschedule Terminated thread simstate + let thread' = thread + !trace <- deschedule (Terminated FinishedNormally) thread' simstate return $ SimPORTrace time tid tstep tlbl EventThreadFinished - $ SimPORTrace time tid tstep tlbl (EventDeschedule Terminated) + $ SimPORTrace time tid tstep tlbl (EventDeschedule $ Terminated FinishedNormally) $ trace MaskFrame k maskst' ctl' -> do -- pop the control stack, restore thread-local state let thread' = thread { threadControl = ThreadControl (k x) ctl' - , threadMasking = maskst' } + , threadMasking = maskst' + } -- but if we're now unmasked, check for any pending async exceptions !trace <- deschedule Interruptable thread' simstate return $ SimPORTrace time tid tstep tlbl (EventMask maskst') @@ -325,7 +336,7 @@ schedule thread@Thread{ let thread' = thread { threadControl = ThreadControl (k x) ctl' } schedule thread' simstate - Throw e -> case unwindControlStack e thread of + Throw thrower e -> case unwindControlStack e thread of Right thread0@Thread { threadMasking = maskst' } -> do -- We found a suitable exception handler, continue with that -- We record a step, in case there is no exception handler on replay. @@ -339,25 +350,31 @@ schedule thread@Thread{ Left isMain -- We unwound and did not find any suitable exception handler, so we -- have an unhandled exception at the top level of the thread. - | isMain -> + | isMain -> do + let thread' = thread { threadEffect = effect <> statusWriteEffect tid } -- An unhandled exception in the main thread terminates the program return (SimPORTrace time tid tstep tlbl (EventThrow e) $ SimPORTrace time tid tstep tlbl (EventThreadUnhandled e) $ - traceFinalRacesFound simstate $ + traceFinalRacesFound simstate { threads = Map.insert tid thread' threads } $ TraceMainException time e (labelledThreads threads)) | otherwise -> do -- An unhandled exception in any other thread terminates the thread - !trace <- deschedule Terminated thread simstate + let reason = if thrower == ThrowSelf then FinishedNormally else FinishedDied + thread' = thread { threadEffect = effect <> statusWriteEffect tid + } + terminated = Terminated reason + !trace <- deschedule terminated thread' simstate return $ SimPORTrace time tid tstep tlbl (EventThrow e) $ SimPORTrace time tid tstep tlbl (EventThreadUnhandled e) - $ SimPORTrace time tid tstep tlbl (EventDeschedule Terminated) + $ SimPORTrace time tid tstep tlbl (EventDeschedule terminated) $ trace Catch action' handler k -> do -- push the failure and success continuations onto the control stack let thread' = thread { threadControl = ThreadControl action' - (CatchFrame handler k ctl) } + (CatchFrame handler k ctl) + } schedule thread' simstate Evaluate expr k -> do @@ -365,7 +382,7 @@ schedule thread@Thread{ case mbWHNF of Left e -> do -- schedule this thread to immediately raise the exception - let thread' = thread { threadControl = ThreadControl (Throw e) ctl } + let thread' = thread { threadControl = ThreadControl (Throw ThrowSelf e) ctl } schedule thread' simstate Right whnf -> do -- continue with the resulting WHNF @@ -478,6 +495,7 @@ schedule thread@Thread{ let effect' = effect <> writeEffects written <> wakeupEffects wakeup + <> statusWriteEffects unblocked thread' = thread { threadControl = ThreadControl k ctl , threadEffect = effect' } @@ -508,7 +526,11 @@ schedule thread@Thread{ | otherwise = childThreadId tid nextTId thread' = thread { threadControl = ThreadControl (k tid') ctl, threadNextTId = nextTId + 1, - threadEffect = effect <> forkEffect tid' } + threadEffect = effect + <> forkEffect tid' + <> statusWriteEffect tid' + <> statusWriteEffect tid + } thread'' = Thread { threadId = tid' , threadControl = ThreadControl (runIOSim a) ForkFrame @@ -546,6 +568,7 @@ schedule thread@Thread{ <> readEffects read <> writeEffects written <> wakeupEffects unblocked + <> statusWriteEffects unblocked thread' = thread { threadControl = ThreadControl (k x) ctl, threadVClock = vClock', threadEffect = effect' } @@ -580,7 +603,7 @@ schedule thread@Thread{ -- schedule this thread to immediately raise the exception vClockRead <- leastUpperBoundTVarVClocks read let effect' = effect <> readEffects read - thread' = thread { threadControl = ThreadControl (Throw e) ctl, + thread' = thread { threadControl = ThreadControl (Throw ThrowSelf e) ctl, threadVClock = vClock `leastUpperBoundVClock` vClockRead, threadEffect = effect' } trace <- schedule thread' simstate @@ -613,6 +636,28 @@ schedule thread@Thread{ threads' = Map.adjust (\t -> t { threadLabel = Just l }) tid' threads schedule thread' simstate { threads = threads' } + ThreadStatus tid' k -> do + let result | Just (r, _) <- Map.lookup tid' finished = reasonToStatus r + | Just t <- Map.lookup tid' threads = threadStatus t + | tid' == tid = ThreadRunning + | otherwise = error "The impossible happened - tried to loookup thread in state." + otherVClock | Just t <- Map.lookup tid' threads = threadVClock t + | Just (_, c) <- Map.lookup tid' finished = c + | tid' == tid = vClock + | otherwise = error "The impossible happened" + reasonToStatus FinishedNormally = ThreadFinished + reasonToStatus FinishedDied = ThreadDied + threadStatus t | threadBlocked t = ThreadBlocked BlockedOnOther + | otherwise = ThreadRunning + + thread' = thread { threadControl = ThreadControl (k result) ctl + , threadVClock = vClock `leastUpperBoundVClock` otherVClock + , threadEffect = effect <> statusReadEffects [tid'] + } + trace <- schedule thread' simstate + return $ SimPORTrace time tid tstep tlbl (EventThreadStatus tid tid') + $ trace + ExploreRaces k -> do let thread' = thread { threadControl = ThreadControl k ctl , threadRacy = True } @@ -647,14 +692,21 @@ schedule thread@Thread{ ThrowTo e tid' _ | tid' == tid -> do -- Throw to ourself is equivalent to a synchronous throw, -- and works irrespective of masking state since it does not block. - let thread' = thread { threadControl = ThreadControl (Throw e) ctl } + let thread' = thread { threadControl = ThreadControl (Throw ThrowSelf e) ctl + , threadEffect = effect + } trace <- schedule thread' simstate return (SimPORTrace time tid tstep tlbl (EventThrowTo e tid) trace) ThrowTo e tid' k -> do let thread' = thread { threadControl = ThreadControl k ctl, - threadEffect = effect <> throwToEffect tid' <> wakeUpEffect, - threadVClock = vClock `leastUpperBoundVClock` vClockTgt } + threadEffect = effect <> throwToEffect tid' + <> wakeUpEffect + <> (if willBlock + then statusWriteEffect tid + else mempty), + threadVClock = vClock `leastUpperBoundVClock` vClockTgt + } (vClockTgt, wakeUpEffect, willBlock) = (threadVClock t, @@ -685,17 +737,16 @@ schedule thread@Thread{ -- new pending async exception). let adjustTarget t@Thread{ threadControl = ThreadControl _ ctl', threadVClock = vClock' } = - t { threadControl = ThreadControl (Throw e) ctl' + t { threadControl = ThreadControl (Throw ThrowOther e) ctl' , threadBlocked = False , threadVClock = vClock' `leastUpperBoundVClock` vClock } - simstate'@SimState { threads = threads' } - = snd (unblockThreads vClock [tid'] simstate) + (unblocked, simstate'@SimState { threads = threads' }) = unblockThreads vClock [tid'] simstate threads'' = Map.adjust adjustTarget tid' threads' simstate'' = simstate' { threads = threads'' } -- We yield at this point because the target thread may be higher -- priority, so this should be a step for race detection. - trace <- deschedule Yield thread' simstate'' + trace <- deschedule Yield thread' { threadEffect = threadEffect thread' <> statusWriteEffects unblocked } simstate'' return $ SimPORTrace time tid tstep tlbl (EventThrowTo e tid') $ trace @@ -716,7 +767,7 @@ threadInterruptible thread = deschedule :: Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a) -deschedule Yield thread@Thread { threadId = tid } +deschedule Yield thread@Thread { threadId = tid } simstate@SimState{runqueue, threads, control} = -- We don't interrupt runnable threads anywhere else. @@ -726,7 +777,8 @@ deschedule Yield thread@Thread { threadId = tid } runqueue' = insertThread thread' runqueue threads' = Map.insert tid thread' threads control' = advanceControl (threadStepId thread) control in - reschedule simstate { runqueue = runqueue', threads = threads', + reschedule simstate { runqueue = runqueue', + threads = threads', races = updateRacesInSimState thread simstate, control = control' } @@ -737,17 +789,20 @@ deschedule Interruptable thread@Thread { threadMasking = Unmasked, threadThrowTo = (e, tid', vClock') : etids, threadLabel = tlbl, - threadVClock = vClock + threadVClock = vClock, + threadEffect = effect } simstate@SimState{ curTime = time, threads } = do -- We're unmasking, but there are pending blocked async exceptions. -- So immediately raise the exception and unblock the blocked thread -- if possible. - let thread' = thread { threadControl = ThreadControl (Throw e) ctl + let thread' = thread { threadControl = ThreadControl (Throw ThrowOther e) ctl , threadMasking = MaskedInterruptible , threadThrowTo = etids - , threadVClock = vClock `leastUpperBoundVClock` vClock' } + , threadVClock = vClock `leastUpperBoundVClock` vClock' + , threadEffect = effect <> statusWriteEffects unblocked + } (unblocked, simstate') = unblockThreads vClock [l_labelled tid'] simstate -- the thread is stepped when we Yield @@ -760,7 +815,7 @@ deschedule Interruptable thread@Thread { , let tlbl'' = lookupThreadLabel tid'' threads ] trace -deschedule Interruptable thread simstate@SimState{ control } = +deschedule Interruptable thread@Thread{threadId = tid } simstate@SimState{ control } = -- Either masked or unmasked but no pending async exceptions. -- Either way, just carry on. -- Record a step, though, in case on replay there is an async exception. @@ -769,28 +824,31 @@ deschedule Interruptable thread simstate@SimState{ control } = simstate{ races = updateRacesInSimState thread simstate, control = advanceControl (threadStepId thread) control } -deschedule Blocked thread@Thread { threadThrowTo = _ : _ - , threadMasking = maskst } simstate +deschedule Blocked thread@Thread { threadId = tid + , threadThrowTo = _ : _ + , threadMasking = maskst + , threadEffect = effect } simstate | maskst /= MaskedUninterruptible = -- We're doing a blocking operation, which is an interrupt point even if -- we have async exceptions masked, and there are pending blocked async -- exceptions. So immediately raise the exception and unblock the blocked -- thread if possible. - deschedule Interruptable thread { threadMasking = Unmasked } simstate + deschedule Interruptable thread { threadMasking = Unmasked, threadEffect = effect <> statusWriteEffect tid } simstate -deschedule Blocked thread simstate@SimState{threads, control} = - let thread1 = thread { threadBlocked = True } - thread' = stepThread $ thread1 +deschedule Blocked thread@Thread{ threadId = tid, threadEffect = effect } simstate@SimState{threads, control} = + let thread1 = thread { threadBlocked = True , threadEffect = effect <> statusWriteEffect tid } + thread' = stepThread thread1 threads' = Map.insert (threadId thread') thread' threads in reschedule simstate { threads = threads', races = updateRacesInSimState thread1 simstate, control = advanceControl (threadStepId thread1) control } -deschedule Terminated thread@Thread { threadId = tid, threadVClock = vClock } - simstate@SimState{ curTime = time, control } = do +deschedule (Terminated reason) thread@Thread { threadId = tid, threadVClock = vClock, threadEffect = effect } + simstate@SimState{ curTime = time, control, finished = finished } = do -- This thread is done. If there are other threads blocked in a -- ThrowTo targeted at this thread then we can wake them up now. - let thread' = stepThread $ thread{ threadDone = True } + let thread1 = thread { threadEffect = effect <> statusWriteEffect tid } + thread' = stepThread $ thread { threadDone = True } wakeup = map (\(_,tid',_) -> l_labelled tid') (reverse (threadThrowTo thread)) (unblocked, simstate'@SimState{threads}) = @@ -799,9 +857,10 @@ deschedule Terminated thread@Thread { threadId = tid, threadVClock = vClock } -- We must keep terminated threads in the state to preserve their vector clocks, -- which matters when other threads throwTo them. !trace <- reschedule simstate' { races = threadTerminatesRaces tid $ - updateRacesInSimState thread simstate, + updateRacesInSimState thread1 simstate, control = advanceControl (threadStepId thread) control, - threads = threads' } + threads = threads', + finished = Map.insert tid (reason, vClock) finished } return $ traceMany -- TODO: step [ (time, tid', (-1), tlbl', EventThrowToWakeup) @@ -809,14 +868,15 @@ deschedule Terminated thread@Thread { threadId = tid, threadVClock = vClock } , let tlbl' = lookupThreadLabel tid' threads ] trace -deschedule Sleep thread@Thread { threadId = tid } +deschedule Sleep thread@Thread { threadId = tid , threadEffect = effect } simstate@SimState{runqueue, threads} = -- Schedule control says we should run a different thread. Put -- this one to sleep without recording a step. - let runqueue' = insertThread thread runqueue - threads' = Map.insert tid thread threads in + let thread' = thread { threadEffect = effect <> statusWriteEffect tid } + runqueue' = insertThread thread runqueue + threads' = Map.insert tid thread' threads in reschedule simstate { runqueue = runqueue', threads = threads' } @@ -1376,8 +1436,8 @@ racingSteps s s' = || throwsTo s s' || throwsTo s' s) where throwsTo s1 s2 = - stepThreadId s1 `elem` effectThrows (stepEffect s2) - && stepEffect s1 /= mempty + stepThreadId s2 `elem` effectThrows (stepEffect s1) + && stepEffect s2 /= mempty currentStep :: Thread s a -> Step currentStep Thread { threadId = tid, diff --git a/io-sim/src/Control/Monad/IOSimPOR/Types.hs b/io-sim/src/Control/Monad/IOSimPOR/Types.hs index 7af270f4..906c7d9c 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Types.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Types.hs @@ -14,20 +14,22 @@ import Control.Monad.IOSim.CommonTypes -- *IOSimPOR*. -- data Effect = Effect { - effectReads :: !(Set TVarId), - effectWrites :: !(Set TVarId), - effectForks :: !(Set ThreadId), - effectThrows :: ![ThreadId], - effectWakeup :: ![ThreadId] + effectReads :: !(Set TVarId), + effectWrites :: !(Set TVarId), + effectForks :: !(Set ThreadId), + effectThrows :: ![ThreadId], + effectWakeup :: ![ThreadId], + effectStatusReads :: ![ThreadId], + effectStatusWrites :: ![ThreadId] } deriving (Eq, Show) instance Semigroup Effect where - Effect r w s ts wu <> Effect r' w' s' ts' wu' = - Effect (r<>r') (w<>w') (s<>s') (ts++ts') (wu++wu') + Effect r w s ts wu sr sw <> Effect r' w' s' ts' wu' sr' sw' = + Effect (r <> r') (w <> w') (s <> s') (ts ++ ts') (wu++wu') (sr ++ sr') (sw ++ sw') instance Monoid Effect where - mempty = Effect Set.empty Set.empty Set.empty [] [] + mempty = Effect Set.empty Set.empty Set.empty [] [] [] [] -- readEffect :: SomeTVar s -> Effect -- readEffect r = mempty{effectReads = Set.singleton $ someTvarId r } @@ -50,6 +52,15 @@ throwToEffect tid = mempty{ effectThrows = [tid] } wakeupEffects :: [ThreadId] -> Effect wakeupEffects tids = mempty{effectWakeup = tids} +statusReadEffects :: [ThreadId] -> Effect +statusReadEffects tids = mempty{effectStatusReads = tids} + +statusWriteEffect :: ThreadId -> Effect +statusWriteEffect tid = mempty{effectStatusWrites = [tid]} + +statusWriteEffects :: [ThreadId] -> Effect +statusWriteEffects tids = mempty{effectStatusWrites = tids} + someTvarId :: SomeTVar s -> TVarId someTvarId (SomeTVar r) = tvarId r @@ -58,10 +69,13 @@ onlyReadEffect e = e { effectReads = effectReads mempty } == mempty racingEffects :: Effect -> Effect -> Bool racingEffects e e' = - effectThrows e `intersectsL` effectThrows e' - || effectReads e `intersects` effectWrites e' - || effectWrites e `intersects` effectReads e' - || effectWrites e `intersects` effectWrites e' + effectThrows e `intersectsL` effectThrows e' + || effectReads e `intersects` effectWrites e' + || effectWrites e `intersects` effectReads e' + || effectWrites e `intersects` effectWrites e' + || effectStatusReads e `intersectsL` effectStatusWrites e' + || effectStatusWrites e `intersectsL` effectStatusReads e' + || effectStatusWrites e `intersectsL` effectStatusWrites e' where intersects :: Ord a => Set a -> Set a -> Bool intersects a b = not $ a `Set.disjoint` b diff --git a/io-sim/test/Test/Control/Monad/IOSimPOR.hs b/io-sim/test/Test/Control/Monad/IOSimPOR.hs index dbb39427..b2184459 100644 --- a/io-sim/test/Test/Control/Monad/IOSimPOR.hs +++ b/io-sim/test/Test/Control/Monad/IOSimPOR.hs @@ -33,6 +33,7 @@ data Step = | ThrowTo Int | Delay Int | Timeout TimeoutStep + | CheckStatus Int deriving (Eq, Ord, Show) data TimeoutStep = @@ -50,11 +51,14 @@ instance Arbitrary Step where return $ ThrowTo i), (1,do Positive i <- arbitrary return $ Delay i), + (1,do NonNegative i <- arbitrary + return $ CheckStatus i), (1,Timeout <$> arbitrary)] shrink (WhenSet m n) = map (WhenSet m) (shrink n) ++ map (`WhenSet` n) (filter (>=n) (shrink m)) shrink (ThrowTo i) = map ThrowTo (shrink i) + shrink (CheckStatus i) = map CheckStatus (shrink i) shrink (Delay i) = map Delay (shrink i) shrink (Timeout t) = map Timeout (shrink t) @@ -98,16 +102,16 @@ newtype Tasks = Tasks [Task] deriving Show instance Arbitrary Tasks where - arbitrary = Tasks . fixThrowTos <$> scale (min 20) arbitrary - shrink (Tasks ts) = Tasks . fixThrowTos <$> + arbitrary = Tasks . fixSymbolicThreadIds <$> scale (min 20) arbitrary + shrink (Tasks ts) = Tasks . fixSymbolicThreadIds <$> removeTask ts ++ shrink ts ++ shrinkDelays ts ++ advanceThrowTo ts ++ sortTasks ts -fixThrowTos :: [Task] -> [Task] -fixThrowTos tasks = mapThrowTos (`mod` length tasks) tasks +fixSymbolicThreadIds :: [Task] -> [Task] +fixSymbolicThreadIds tasks = mapSymThreadIds (`mod` length tasks) tasks shrinkDelays :: [Task] -> [[Task]] shrinkDelays tasks @@ -142,6 +146,13 @@ advanceThrowTo (Task steps:ts) = advance (s:steppes) = (s:) <$> advance steppes advance [] = [] +mapSymThreadIds :: (Int -> Int) -> [Task] -> [Task] +mapSymThreadIds f tasks = map mapTask tasks + where mapTask (Task steps) = Task (map mapStep steps) + mapStep (ThrowTo i) = ThrowTo (f i) + mapStep (CheckStatus i) = CheckStatus (f i) + mapStep s = s + mapThrowTos :: (Int -> Int) -> [Task] -> [Task] mapThrowTos f tasks = map mapTask tasks where mapTask (Task steps) = Task (map mapStep steps) @@ -166,6 +177,7 @@ interpret r t (Task steps) = forkIO $ do when (a/=m) retry writeTVar r n interpretStep (ts,_) (ThrowTo i) = throwTo (ts !! i) (ExitFailure 0) + interpretStep (ts,_) (CheckStatus i) = void $ threadStatus (ts !! i) interpretStep _ (Delay i) = threadDelay (fromIntegral i) interpretStep (_,timer) (Timeout tstep) = do timerVal <- atomically $ readTVar timer @@ -202,6 +214,7 @@ propSimulates (Tasks tasks) = propExploration :: Tasks -> Property propExploration (Tasks tasks) = + -- Debug.trace ("\nTasks:\n"++ show tasks) $ any (not . null . (\(Task steps)->steps)) tasks ==> traceNoDuplicates $ \addTrace -> --traceCounter $ \addTrace -> diff --git a/io-sim/test/Test/IOSim.hs b/io-sim/test/Test/IOSim.hs index 53b817ac..ea1e90b0 100644 --- a/io-sim/test/Test/IOSim.hs +++ b/io-sim/test/Test/IOSim.hs @@ -39,6 +39,8 @@ import Test.QuickCheck import Test.Tasty import Test.Tasty.QuickCheck +import GHC.Conc (ThreadStatus(..)) + tests :: TestTree tests = @@ -144,8 +146,178 @@ tests = , testProperty "lazy" prop_mfix_lazy , testProperty "recdata" prop_mfix_recdata ] + -- NOTE: Most of the tests below only work because the io-sim + -- scheduler works the way it does. + , testGroup "ThreadStatus" + [ testProperty "thread status finished (IOSim)" + $ withMaxSuccess 1 $ runSimOrThrow prop_thread_status_finished + , testProperty "thread status finished (IO)" + $ withMaxSuccess 1 $ ioProperty prop_thread_status_finished + , testProperty "thread status running (IOSim)" + $ withMaxSuccess 1 $ runSimOrThrow prop_thread_status_running + , testProperty "thread status running (IO)" + $ withMaxSuccess 1 $ ioProperty prop_thread_status_running + , testProperty "thread status blocked (IOSim)" + $ withMaxSuccess 1 $ runSimOrThrow prop_thread_status_blocked + , testProperty "thread status blocked (IO)" + $ withMaxSuccess 1 $ ioProperty prop_thread_status_blocked + , testProperty "thread status blocked delay (IOSim)" + $ withMaxSuccess 1 $ runSimOrThrow prop_thread_status_blocked_delay + , testProperty "thread status blocked delay (IO)" + $ withMaxSuccess 1 $ ioProperty prop_thread_status_blocked_delay + , testProperty "thread status died (IOSim)" + $ withMaxSuccess 1 $ runSimOrThrow prop_thread_status_died + , testProperty "thread status died (IO)" + $ withMaxSuccess 1 $ ioProperty prop_thread_status_died + , testProperty "thread status died_own (IOSim)" + $ withMaxSuccess 1 $ runSimOrThrow prop_thread_status_died_own + , testProperty "thread status died_own (IO)" + $ withMaxSuccess 1 $ ioProperty prop_thread_status_died_own + , testProperty "thread status yield (IOSim)" + $ withMaxSuccess 1 $ runSimOrThrow prop_thread_status_yield + , testProperty "thread status yield (IO)" + $ withMaxSuccess 1 $ ioProperty prop_thread_status_yield + , testProperty "thread status mask (IOSim)" + $ withMaxSuccess 1 $ runSimOrThrow prop_thread_status_mask + , testProperty "thread status mask (IO)" + $ withMaxSuccess 1 $ ioProperty prop_thread_status_mask + , testProperty "thread status mask blocked (IOSim)" + $ withMaxSuccess 1 $ runSimOrThrow prop_thread_status_mask_blocked + , testProperty "thread status mask blocked (IO)" + $ withMaxSuccess 1 $ ioProperty prop_thread_status_mask_blocked + ] ] +-- +-- threadStatus +-- + +prop_two_threads_expect :: (MonadFork m, MonadThread m) + => m () + -> (ThreadId m -> m ()) + -> (ThreadStatus -> Property) + -> m Property +prop_two_threads_expect target main prop = do + tid <- forkIO target + main tid + status <- threadStatus tid + return $ prop status + +prop_two_threads_expect_ :: (MonadFork m, MonadThread m) + => m () + -> (ThreadStatus -> Property) + -> m Property +prop_two_threads_expect_ target prop = + prop_two_threads_expect target + (const $ yield) + prop + +prop_thread_status_finished :: (MonadFork m, MonadDelay m, MonadThread m) + => m Property +prop_thread_status_finished = + prop_two_threads_expect_ (pure ()) + (ThreadFinished ===) + +prop_thread_status_running :: (MonadFork m, MonadDelay m, MonadThread m) + => m Property +prop_thread_status_running = + prop_two_threads_expect_ (forever yield) + (ThreadRunning ===) + +prop_thread_status_blocked :: ( MonadFork m + , MonadDelay m + , MonadThread m + , MonadSTM m + ) + => m Property +prop_thread_status_blocked = do + var <- newEmptyTMVarIO + prop_two_threads_expect_ + (atomically $ takeTMVar var) + $ \ status -> case status of + ThreadBlocked _ -> property True + _ -> + counterexample (show status ++ " /= ThreadBlocked _") + False + +prop_thread_status_blocked_delay :: (MonadFork m, MonadDelay m, MonadThread m) + => m Property +prop_thread_status_blocked_delay = + prop_two_threads_expect_ + (threadDelay 1) + $ \ status -> case status of + ThreadBlocked _ -> property True + _ -> + counterexample (show status ++ " /= ThreadBlocked _") + False + +prop_thread_status_died :: ( MonadFork m + , MonadThrow m + , MonadDelay m + , MonadThread m + ) + => m Property +prop_thread_status_died = + prop_two_threads_expect (forever yield) + (\tid -> do throwTo tid DivideByZero; yield) + (ThreadDied ===) + +prop_thread_status_died_own :: ( MonadFork m + , MonadThrow m + , MonadDelay m + , MonadThread m + ) + => m Property +prop_thread_status_died_own = do + prop_two_threads_expect_ (throwIO DivideByZero) + (ThreadFinished ===) + +prop_thread_status_yield :: ( MonadFork m + , MonadThrow m + , MonadDelay m + , MonadThread m + , MonadSTM m + ) + => m Property +prop_thread_status_yield = do + var <- newEmptyTMVarIO + prop_two_threads_expect + (do atomically (putTMVar var ()); forever yield) + (const $ atomically (takeTMVar var)) + (ThreadRunning ===) + +prop_thread_status_mask :: ( MonadFork m + , MonadThrow m + , MonadDelay m + , MonadThread m + , MonadSTM m + , MonadMask m + ) + => m Property +prop_thread_status_mask = do + var <- newEmptyTMVarIO + prop_two_threads_expect + (mask_ (do atomically (putTMVar var ()); yield) >> forever yield) + (\tid -> do atomically (takeTMVar var) + throwTo tid DivideByZero + yield) + (ThreadFinished ===) + +prop_thread_status_mask_blocked :: ( MonadFork m + , MonadThrow m + , MonadThread m + , MonadMask m + ) + => m Property +prop_thread_status_mask_blocked = do + helper <- forkIO $ mask_ (forever yield) + prop_two_threads_expect_ + (throwTo helper DivideByZero) + $ \ status -> case status of + ThreadBlocked _ -> property True + _ -> + counterexample (show status ++ " /= ThreadBlocked _") + False -- -- Read/Write graph @@ -174,24 +346,17 @@ prop_stm_graph (TestThreadGraph g) = do -- read all the inputs and wait for them to become true -- then write to all the outputs let incomming = g' ! v - outgoing = g ! v atomically $ do sequence_ [ readTVar (vars ! var) >>= check | var <- incomming ] - sequence_ [ writeTVar (vars ! var) True | var <- outgoing ] + writeTVar (vars ! v) True - let -- the vertices with outgoing but no incoming edges - inputs = [ v - | v <- vertices g - , not (null (g ! v)) - , null (g' ! v) ] - -- the vertices with incoming but no outgoing edges + let -- the vertices with incoming but no outgoing edges outputs = [ v | v <- vertices g , not (null (g' ! v)) , null (g ! v) ] - -- write to the inputs and wait for the outputs - void $ forkIO $ atomically $ sequence_ [ writeTVar (vars ! var) True | var <- inputs ] + -- Wait for the outputs atomically $ sequence_ [ readTVar (vars ! var) >>= check | var <- outputs ] where g' = transposeG g -- for incoming edges @@ -273,12 +438,13 @@ test_timers xs = countUnique [] = 0 countUnique (a:as) = let as' = filter (== a) as - in 1 + countUnique as' + in 1 + countUnique as' lbl :: Eq a => [a] -> String lbl as = - let p = (if null as then 0 else (100 * countUnique as) `div` length as) `mod` 10 * 10 - in show p ++ "% unique" + let p = (if null as then 0 else (100 * countUnique as) `div` length as) + `mod` 10 * 10 + in show p ++ "% unique" experiment :: Probe m (DiffTime, Int) -> m () experiment p = do @@ -305,7 +471,7 @@ test_timers xs = sortFn :: DiffTime -> DiffTime -> Ordering sortFn a b | a >= 0 && b >= 0 = a `compare` b | a < 0 && b < 0 = EQ - | otherwise = a `compare` b + | otherwise = a `compare` b prop_timers_ST :: TestMicro -> Property prop_timers_ST (TestMicro xs) = @@ -356,12 +522,12 @@ prop_fork_order_IO = ioProperty . test_fork_order test_threadId_order :: forall m. - ( MonadFork m - , MonadSTM m - , MonadTimer m - ) - => Positive Int - -> m Property + ( MonadFork m + , MonadSTM m + , MonadTimer m + ) + => Positive Int + -> m Property test_threadId_order = \(Positive n) -> do isValid n <$> (forM [1..n] (const experiment)) where @@ -396,7 +562,7 @@ test_wakeup_order :: ( MonadFork m , MonadSTM m , MonadTimer m ) - => m Property + => m Property test_wakeup_order = do v <- newTVarIO False wakupOrder <- @@ -1060,7 +1226,12 @@ prop_stm_referenceM (SomeTerm _tyrep t) = do -- | Check that 'timeout' does not deadlock when executed with asynchronous -- exceptions uninterruptibly masked. -- -prop_timeout_no_deadlockM :: forall m. ( MonadFork m, MonadSTM m, MonadTimer m, MonadMask m ) +prop_timeout_no_deadlockM :: forall m. + ( MonadFork m + , MonadSTM m + , MonadTimer m + , MonadMask m + ) => m Bool prop_timeout_no_deadlockM = do v <- registerDelay' 0.01