From e1128ee0b4a6ace1d07fac6d55712adced408779 Mon Sep 17 00:00:00 2001 From: Maximilian Algehed Date: Fri, 26 Aug 2022 15:48:00 +0200 Subject: [PATCH 1/9] Added gitignore --- .gitignore | 1 + 1 file changed, 1 insertion(+) create mode 100644 .gitignore diff --git a/.gitignore b/.gitignore new file mode 100644 index 00000000..48a004cd --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +dist-newstyle From 4d71c221d16d60d2f0eea5201e22a1def5de2c9b Mon Sep 17 00:00:00 2001 From: Maximilian Algehed Date: Thu, 25 Aug 2022 12:03:27 +0200 Subject: [PATCH 2/9] Added threadStatus to io-classes interface --- io-classes/src/Control/Monad/Class/MonadFork.hs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/io-classes/src/Control/Monad/Class/MonadFork.hs b/io-classes/src/Control/Monad/Class/MonadFork.hs index b152c0ff..193bb6bd 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 @@ -54,6 +56,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 @@ -67,6 +70,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) From 5b9935ee45df4e48af7c6cf56bb5706d2a040823 Mon Sep 17 00:00:00 2001 From: Maximilian Algehed Date: Thu, 25 Aug 2022 12:27:53 +0200 Subject: [PATCH 3/9] ThreadStatus in IOSim and IOSimPOR --- io-sim/src/Control/Monad/IOSim/CommonTypes.hs | 7 +- io-sim/src/Control/Monad/IOSim/Internal.hs | 54 +++++-- io-sim/src/Control/Monad/IOSim/Types.hs | 14 +- io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 146 ++++++++++++------ io-sim/src/Control/Monad/IOSimPOR/Types.hs | 37 +++-- io-sim/test/Main.hs | 2 +- io-sim/test/Test/Control/Monad/IOSimPOR.hs | 22 ++- io-sim/test/Test/IOSim.hs | 114 ++++++++++++-- 8 files changed, 308 insertions(+), 88 deletions(-) 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 218567de..71b57e1f 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -14,6 +14,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-orphans #-} -- incomplete uni patterns in 'schedule' (when interpreting 'StmTxCommitted') @@ -69,6 +70,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) @@ -123,7 +125,6 @@ labelledThreads threadMap = -- data TimerVars s = TimerVars !(TVar s TimeoutState) !(TVar s Bool) - -- | Internal state. -- data SimState s a = SimState { @@ -131,6 +132,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 @@ -146,6 +149,7 @@ initialState = SimState { runqueue = mempty, threads = Map.empty, + finished = Map.empty, curTime = Time 0, timers = PSQ.empty, clocks = Map.singleton (ClockId []) epoch1970, @@ -190,6 +194,7 @@ schedule !thread@Thread{ !simstate@SimState { runqueue, threads, + finished, timers, clocks, nextVid, nextTmid, @@ -208,9 +213,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 @@ -228,7 +233,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 @@ -247,10 +252,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 -> @@ -266,7 +273,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 @@ -466,7 +473,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 @@ -495,6 +502,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 Thread{..} | threadBlocked = 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 } @@ -519,7 +539,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) @@ -549,8 +569,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' } @@ -619,7 +642,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, @@ -654,13 +677,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 da201531..f56539db 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 @@ -113,6 +114,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) @@ -131,6 +134,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 @@ -148,7 +153,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 @@ -156,6 +161,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 @@ -242,7 +248,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 @@ -289,7 +295,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 @@ -373,6 +379,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 @@ -802,6 +809,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 f6507022..a86bf3fa 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -16,6 +16,7 @@ {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-orphans #-} -- incomplete uni patterns in 'schedule' (when interpreting 'StmTxCommitted') @@ -90,6 +91,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 -- @@ -98,7 +101,7 @@ data Thread s a = Thread { threadId :: !ThreadId, threadControl :: !(ThreadControl s a), threadBlocked :: !Bool, - threadDone :: !Bool, + threadDone :: !Bool, -- TODO: do we need this when we keep track of finished threads separately? threadMasking :: !MaskingState, -- other threads blocked in a ThrowTo to us because we are or were masked threadThrowTo :: ![(SomeException, Labelled ThreadId, VectorClock)], @@ -123,7 +126,6 @@ isNotRacyThreadId :: ThreadId -> Bool isNotRacyThreadId (ThreadId _) = True isNotRacyThreadId _ = False - bottomVClock :: VectorClock bottomVClock = VectorClock Map.empty @@ -172,6 +174,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 @@ -197,6 +201,7 @@ initialState = SimState { runqueue = PSQ.empty, threads = Map.empty, + finished = Map.empty, curTime = Time 0, timers = PSQ.empty, clocks = Map.singleton (ClockId []) epoch1970, @@ -212,14 +217,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 ]) @@ -228,6 +234,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. @@ -256,6 +263,7 @@ schedule thread@Thread{ simstate@SimState { runqueue, threads, + finished, timers, clocks, nextVid, nextTmid, @@ -275,7 +283,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 @@ -306,15 +316,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') @@ -326,7 +338,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. @@ -340,25 +352,30 @@ 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 + } + !trace <- deschedule (Terminated reason) 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 reason) $ 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 @@ -366,7 +383,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 @@ -479,6 +496,7 @@ schedule thread@Thread{ let effect' = effect <> writeEffects written <> wakeupEffects wakeup + <> statusWriteEffects unblocked thread' = thread { threadControl = ThreadControl k ctl , threadEffect = effect' } @@ -509,7 +527,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 @@ -547,6 +569,7 @@ schedule thread@Thread{ <> readEffects read <> writeEffects written <> wakeupEffects unblocked + <> statusWriteEffects unblocked thread' = thread { threadControl = ThreadControl (k x) ctl, threadVClock = vClock', threadEffect = effect' } @@ -581,7 +604,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 @@ -614,6 +637,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 Thread{..} | threadBlocked = 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 } @@ -648,14 +693,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, @@ -686,17 +738,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 @@ -717,7 +768,8 @@ 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 + , threadEffect = effect } simstate@SimState{runqueue, threads, control} = -- We don't interrupt runnable threads anywhere else. @@ -738,17 +790,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 @@ -761,7 +816,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. @@ -770,28 +825,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}) = @@ -800,9 +858,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) @@ -810,14 +869,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' } diff --git a/io-sim/src/Control/Monad/IOSimPOR/Types.hs b/io-sim/src/Control/Monad/IOSimPOR/Types.hs index 7af270f4..3cf486ac 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,12 @@ 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` 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/Main.hs b/io-sim/test/Main.hs index 1a54c244..ec70dc24 100644 --- a/io-sim/test/Main.hs +++ b/io-sim/test/Main.hs @@ -12,5 +12,5 @@ tests :: TestTree tests = testGroup "IO Sim" [ Test.IOSim.tests - , Test.Control.Monad.Class.MonadMVar.tests + -- , Test.Control.Monad.Class.MonadMVar.tests ] diff --git a/io-sim/test/Test/Control/Monad/IOSimPOR.hs b/io-sim/test/Test/Control/Monad/IOSimPOR.hs index dace394c..37836db5 100644 --- a/io-sim/test/Test/Control/Monad/IOSimPOR.hs +++ b/io-sim/test/Test/Control/Monad/IOSimPOR.hs @@ -28,12 +28,14 @@ import Data.List import Data.Map (Map) import qualified Data.Map as Map import Test.QuickCheck +import qualified Debug.Trace as Debug data Step = WhenSet Int Int | ThrowTo Int | Delay Int | Timeout TimeoutStep + | CheckStatus Int deriving (Eq, Ord, Show) data TimeoutStep = @@ -51,11 +53,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) @@ -99,16 +104,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 @@ -143,6 +148,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) @@ -167,6 +179,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 @@ -203,6 +216,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 923a5520..15e8012a 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,107 @@ 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 +275,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 From 48e087cc2ef0ed8f4bc9da788d06e2325cf2b9fd Mon Sep 17 00:00:00 2001 From: Maximilian Algehed Date: Wed, 31 Aug 2022 11:12:18 +0200 Subject: [PATCH 4/9] Fix unintuitive name --- io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index a86bf3fa..98635e10 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -1437,8 +1437,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, From 5f02bca990542bf3145a72eb34e89f5122d2d1dc Mon Sep 17 00:00:00 2001 From: Maximilian Algehed Date: Fri, 2 Sep 2022 09:51:39 +0200 Subject: [PATCH 5/9] Some style-guide refactoring --- io-sim/src/Control/Monad/IOSim/Internal.hs | 9 +- io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 20 +- io-sim/test/Test/Control/Monad/IOSimPOR.hs | 1 - io-sim/test/Test/IOSim.hs | 203 ++++++++++++------ 4 files changed, 154 insertions(+), 79 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index 71b57e1f..71f8f87d 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -14,7 +14,6 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-orphans #-} -- incomplete uni patterns in 'schedule' (when interpreting 'StmTxCommitted') @@ -507,10 +506,10 @@ schedule !thread@Thread{ 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 Thread{..} | threadBlocked = ThreadBlocked BlockedOnOther - | otherwise = ThreadRunning + reasonToStatus FinishedNormally = ThreadFinished + reasonToStatus FinishedDied = ThreadDied + threadStatus t | threadBlocked t = ThreadBlocked BlockedOnOther + | otherwise = ThreadRunning thread' = thread { threadControl = ThreadControl (k result) ctl } schedule thread' simstate diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index 98635e10..62456088 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -16,7 +16,6 @@ {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-orphans #-} -- incomplete uni patterns in 'schedule' (when interpreting 'StmTxCommitted') @@ -365,10 +364,11 @@ schedule thread@Thread{ let reason = if thrower == ThrowSelf then FinishedNormally else FinishedDied thread' = thread { threadEffect = effect <> statusWriteEffect tid } - !trace <- deschedule (Terminated reason) thread' simstate + 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 reason) + $ SimPORTrace time tid tstep tlbl (EventDeschedule terminated) $ trace Catch action' handler k -> do @@ -528,9 +528,9 @@ schedule thread@Thread{ thread' = thread { threadControl = ThreadControl (k tid') ctl, threadNextTId = nextTId + 1, threadEffect = effect - <> forkEffect tid' - <> statusWriteEffect tid' - <> statusWriteEffect tid + <> forkEffect tid' + <> statusWriteEffect tid' + <> statusWriteEffect tid } thread'' = Thread { threadId = tid' , threadControl = ThreadControl (runIOSim a) @@ -646,10 +646,10 @@ schedule thread@Thread{ | Just (_, c) <- Map.lookup tid' finished = c | tid' == tid = vClock | otherwise = error "The impossible happened" - reasonToStatus FinishedNormally = ThreadFinished - reasonToStatus FinishedDied = ThreadDied - threadStatus Thread{..} | threadBlocked = ThreadBlocked BlockedOnOther - | otherwise = ThreadRunning + 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 diff --git a/io-sim/test/Test/Control/Monad/IOSimPOR.hs b/io-sim/test/Test/Control/Monad/IOSimPOR.hs index 37836db5..fb1272d2 100644 --- a/io-sim/test/Test/Control/Monad/IOSimPOR.hs +++ b/io-sim/test/Test/Control/Monad/IOSimPOR.hs @@ -28,7 +28,6 @@ import Data.List import Data.Map (Map) import qualified Data.Map as Map import Test.QuickCheck -import qualified Debug.Trace as Debug data Step = WhenSet Int Int diff --git a/io-sim/test/Test/IOSim.hs b/io-sim/test/Test/IOSim.hs index 15e8012a..6a4cf515 100644 --- a/io-sim/test/Test/IOSim.hs +++ b/io-sim/test/Test/IOSim.hs @@ -146,26 +146,45 @@ 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. + -- 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 + [ 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 ] ] @@ -188,65 +207,117 @@ 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_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 :: (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 :: (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 :: ( 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_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_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 :: ( 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 :: ( 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_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_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 + prop_two_threads_expect_ + (throwTo helper DivideByZero) + $ \ status -> case status of + ThreadBlocked _ -> property True + _ -> + counterexample (show status ++ " /= ThreadBlocked _") + False -- -- Read/Write graph @@ -367,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 @@ -399,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) = @@ -450,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 @@ -490,7 +562,7 @@ test_wakeup_order :: ( MonadFork m , MonadSTM m , MonadTimer m ) - => m Property + => m Property test_wakeup_order = do v <- newTVarIO False wakupOrder <- @@ -1154,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 From 788f5e748e97a1cc1d69165f35ec317fef17f883 Mon Sep 17 00:00:00 2001 From: Maximilian Algehed Date: Fri, 2 Sep 2022 09:57:20 +0200 Subject: [PATCH 6/9] Review comments --- io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 6 +++--- io-sim/src/Control/Monad/IOSimPOR/Types.hs | 1 + 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index 62456088..5b128a52 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -768,8 +768,7 @@ threadInterruptible thread = deschedule :: Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a) -deschedule Yield thread@Thread { threadId = tid - , threadEffect = effect } +deschedule Yield thread@Thread { threadId = tid } simstate@SimState{runqueue, threads, control} = -- We don't interrupt runnable threads anywhere else. @@ -779,7 +778,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' } diff --git a/io-sim/src/Control/Monad/IOSimPOR/Types.hs b/io-sim/src/Control/Monad/IOSimPOR/Types.hs index 3cf486ac..906c7d9c 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Types.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Types.hs @@ -74,6 +74,7 @@ racingEffects e 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 From db2112d68e3ae3d65431bdc4573cbf2c00af6476 Mon Sep 17 00:00:00 2001 From: Maximilian Algehed Date: Fri, 2 Sep 2022 10:00:02 +0200 Subject: [PATCH 7/9] Remove todo --- io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index 5b128a52..7f244371 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -100,7 +100,7 @@ data Thread s a = Thread { threadId :: !ThreadId, threadControl :: !(ThreadControl s a), threadBlocked :: !Bool, - threadDone :: !Bool, -- TODO: do we need this when we keep track of finished threads separately? + threadDone :: !Bool, threadMasking :: !MaskingState, -- other threads blocked in a ThrowTo to us because we are or were masked threadThrowTo :: ![(SomeException, Labelled ThreadId, VectorClock)], From 99759e143ad058fe55fd764aff1279f7e73fbadd Mon Sep 17 00:00:00 2001 From: Maximilian Algehed Date: Tue, 20 Sep 2022 11:21:41 +0200 Subject: [PATCH 8/9] turn on test that was accidentally turned off --- io-sim/test/Main.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/io-sim/test/Main.hs b/io-sim/test/Main.hs index ec70dc24..1a54c244 100644 --- a/io-sim/test/Main.hs +++ b/io-sim/test/Main.hs @@ -12,5 +12,5 @@ tests :: TestTree tests = testGroup "IO Sim" [ Test.IOSim.tests - -- , Test.Control.Monad.Class.MonadMVar.tests + , Test.Control.Monad.Class.MonadMVar.tests ] From d1872357c68c374489980a4dd89addb8ea2bf795 Mon Sep 17 00:00:00 2001 From: Marcin Szamotulski Date: Thu, 29 Sep 2022 12:24:32 +0200 Subject: [PATCH 9/9] Disabled threadStatus tests on Windows See issue input-output-hk/io-sim#28 --- io-sim/test/Test/IOSim.hs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/io-sim/test/Test/IOSim.hs b/io-sim/test/Test/IOSim.hs index 6a4cf515..4ae7658a 100644 --- a/io-sim/test/Test/IOSim.hs +++ b/io-sim/test/Test/IOSim.hs @@ -171,16 +171,22 @@ tests = $ withMaxSuccess 1 $ ioProperty prop_thread_status_died , testProperty "thread status died_own (IOSim)" $ withMaxSuccess 1 $ runSimOrThrow prop_thread_status_died_own +-- TODO: issue input-output-hk/io-sim#28 +#if !defined(mingw32_HOST_OS) , testProperty "thread status died_own (IO)" $ withMaxSuccess 1 $ ioProperty prop_thread_status_died_own +#endif , 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 +-- TODO: issue input-output-hk/io-sim#28 +#if !defined(mingw32_HOST_OS) , testProperty "thread status mask (IO)" $ withMaxSuccess 1 $ ioProperty prop_thread_status_mask +#endif , testProperty "thread status mask blocked (IOSim)" $ withMaxSuccess 1 $ runSimOrThrow prop_thread_status_mask_blocked , testProperty "thread status mask blocked (IO)"