diff --git a/io-sim/CHANGELOG.md b/io-sim/CHANGELOG.md index 01ead980..7260b8f7 100644 --- a/io-sim/CHANGELOG.md +++ b/io-sim/CHANGELOG.md @@ -8,6 +8,8 @@ - `Show` instance for `ScheduleMod` now prints `ThreadId`s in a slightly nicer way, matching the way those steps would be traced in the `SimTrace`. - Implement `MonadLabelledMVar` instance for `(IOSim s)` +- `TVarId` is now a sum type with one constructor per `TVar` role, e.g. `TVar`, + `TMVar`, `MVar` and a few others - except for `TChan`. ## 1.6.0.0 diff --git a/io-sim/src/Control/Monad/IOSim/CommonTypes.hs b/io-sim/src/Control/Monad/IOSim/CommonTypes.hs index 6b333dbd..df44f026 100644 --- a/io-sim/src/Control/Monad/IOSim/CommonTypes.hs +++ b/io-sim/src/Control/Monad/IOSim/CommonTypes.hs @@ -17,6 +17,7 @@ module Control.Monad.IOSim.CommonTypes , childThreadId , setRacyThread , TVarId (..) + , VarId , TimeoutId (..) , ClockId (..) , VectorClock (..) @@ -92,7 +93,24 @@ ppStepId (tid, step) | step < 0 ppStepId (tid, step) = concat [ppIOSimThreadId tid, ".", show step] -newtype TVarId = TVarId Int deriving (Eq, Ord, Enum, Show) +type VarId = Int +-- | 'TVar's are used to emulate other shared variables. Each one comes with +-- its own id constructor. +data TVarId = + TVarId !VarId + -- ^ a `TVar` + | TMVarId !VarId + -- ^ a `TMVar` simulated by a `TVar`. + | MVarId !VarId + -- ^ an `MVar` simulated by a `TVar`. + | TQueueId !VarId + -- ^ a 'TQueue` simulated by a `TVar`. + | TBQueueId !VarId + -- ^ a 'TBQueue` simulated by a `TVar`. + | TSemId !VarId + -- ^ a 'TSem` simulated by a `TVar`. + -- TODO: `TChan` + deriving (Eq, Ord, Show) newtype TimeoutId = TimeoutId Int deriving (Eq, Ord, Enum, Show) newtype ClockId = ClockId [Int] deriving (Eq, Ord, Show) newtype VectorClock = VectorClock { getVectorClock :: Map IOSimThreadId Int } @@ -139,7 +157,7 @@ data TVar s a = TVar { tvarVClock :: !(STRef s VectorClock), -- | Callback to construct a trace which will be attached to the dynamic - -- trace. + -- trace each time the `TVar` is committed. tvarTrace :: !(STRef s (Maybe (Maybe a -> a -> ST s TraceValue))) } diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index 0e72298e..8557136a 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -149,7 +149,7 @@ data SimState s a = SimState { timers :: !(Timeouts s), -- | list of clocks clocks :: !(Map ClockId UTCTime), - nextVid :: !TVarId, -- ^ next unused 'TVarId' + nextVid :: !VarId, -- ^ next unused 'VarId' nextTmid :: !TimeoutId -- ^ next unused 'TimeoutId' } @@ -161,7 +161,7 @@ initialState = curTime = Time 0, timers = PSQ.empty, clocks = Map.singleton (ClockId []) epoch1970, - nextVid = TVarId 0, + nextVid = 0, nextTmid = TimeoutId 0 } where @@ -358,7 +358,7 @@ schedule !thread@Thread{ error "schedule: StartTimeout: Impossible happened" StartTimeout d action' k -> do - !lock <- TMVar <$> execNewTVar nextVid (Just $! "lock-" ++ show nextTmid) Nothing + !lock <- TMVar <$> execNewTVar (TMVarId nextVid) (Just $! "lock-" ++ show nextTmid) Nothing let !expiry = d `addTime` time !timers' = PSQ.insert nextTmid expiry (TimerTimeout tid nextTmid lock) timers !thread' = thread { threadControl = @@ -376,18 +376,18 @@ schedule !thread@Thread{ schedule thread' simstate { timers = PSQ.delete tmid timers } RegisterDelay d k | d < 0 -> do - !tvar <- execNewTVar nextVid + !tvar <- execNewTVar (TVarId nextVid) (Just $! "<>") True let !expiry = d `addTime` time !thread' = thread { threadControl = ThreadControl (k tvar) ctl } trace <- schedule thread' simstate { nextVid = succ nextVid } - return (SimTrace time tid tlbl (EventRegisterDelayCreated nextTmid nextVid expiry) $ + return (SimTrace time tid tlbl (EventRegisterDelayCreated nextTmid (TVarId nextVid) expiry) $ SimTrace time tid tlbl (EventRegisterDelayFired nextTmid) $ trace) RegisterDelay d k -> do - !tvar <- execNewTVar nextVid + !tvar <- execNewTVar (TVarId nextVid) (Just $! "<>") False let !expiry = d `addTime` time @@ -397,7 +397,7 @@ schedule !thread@Thread{ , nextVid = succ nextVid , nextTmid = succ nextTmid } return (SimTrace time tid tlbl - (EventRegisterDelayCreated nextTmid nextVid expiry) trace) + (EventRegisterDelayCreated nextTmid (TVarId nextVid) expiry) trace) ThreadDelay d k | d < 0 -> do let !expiry = d `addTime` time @@ -424,12 +424,12 @@ schedule !thread@Thread{ !expiry = d `addTime` time !thread' = thread { threadControl = ThreadControl (k t) ctl } trace <- schedule thread' simstate { nextTmid = succ nextTmid } - return (SimTrace time tid tlbl (EventTimerCreated nextTmid nextVid expiry) $ + return (SimTrace time tid tlbl (EventTimerCreated nextTmid (TVarId nextVid) expiry) $ SimTrace time tid tlbl (EventTimerCancelled nextTmid) $ trace) NewTimeout d k -> do - !tvar <- execNewTVar nextVid + !tvar <- execNewTVar (TVarId nextVid) (Just $! "<>") TimeoutPending let !expiry = d `addTime` time @@ -439,7 +439,7 @@ schedule !thread@Thread{ trace <- schedule thread' simstate { timers = timers' , nextVid = succ nextVid , nextTmid = succ nextTmid } - return (SimTrace time tid tlbl (EventTimerCreated nextTmid nextVid expiry) trace) + return (SimTrace time tid tlbl (EventTimerCreated nextTmid (TVarId nextVid) expiry) trace) CancelTimeout (Timeout tvar tmid) k -> do let !timers' = PSQ.delete tmid timers @@ -1030,7 +1030,7 @@ execAtomically :: forall s a c. Time -> IOSimThreadId -> Maybe ThreadLabel - -> TVarId + -> VarId -> StmA s a -> (StmTxResult s a -> ST s (SimTrace c)) -> ST s (SimTrace c) @@ -1043,7 +1043,7 @@ execAtomically !time !tid !tlbl !nextVid0 !action0 !k0 = -> Map TVarId (SomeTVar s) -- set of vars written -> [SomeTVar s] -- vars written in order (no dups) -> [SomeTVar s] -- vars created in order - -> TVarId -- var fresh name supply + -> VarId -- var fresh name supply -> StmA s b -> ST s (SimTrace c) go !ctl !read !written !writtenSeq !createdSeq !nextVid !action = @@ -1145,8 +1145,8 @@ execAtomically !time !tid !tlbl !nextVid0 !action0 !k0 = let ctl' = BranchFrame (OrElseStmA b) k written writtenSeq createdSeq ctl go ctl' read Map.empty [] [] nextVid a - NewTVar !mbLabel x k -> do - !v <- execNewTVar nextVid mbLabel x + NewTVar mkId !mbLabel x k -> do + !v <- execNewTVar (mkId nextVid) mbLabel x go ctl read written writtenSeq (SomeTVar v : createdSeq) (succ nextVid) (k v) LabelTVar !label tvar k -> do @@ -1229,16 +1229,15 @@ execAtomically' = go Map.empty execNewTVar :: TVarId -> Maybe String -> a -> ST s (TVar s a) -execNewTVar nextVid !mbLabel x = do +execNewTVar !tvarId !mbLabel x = do !tvarLabel <- newSTRef mbLabel !tvarCurrent <- newSTRef x !tvarUndo <- newSTRef $! [] !tvarBlocked <- newSTRef ([], Set.empty) !tvarVClock <- newSTRef $! VectorClock Map.empty !tvarTrace <- newSTRef $! Nothing - return TVar {tvarId = nextVid, tvarLabel, - tvarCurrent, tvarUndo, tvarBlocked, tvarVClock, - tvarTrace} + return TVar {tvarId, tvarLabel, tvarCurrent, tvarUndo, tvarBlocked, + tvarVClock, tvarTrace} -- 'execReadTVar' is defined in `Control.Monad.IOSim.Type` and shared with /IOSimPOR/ diff --git a/io-sim/src/Control/Monad/IOSim/STM.hs b/io-sim/src/Control/Monad/IOSim/STM.hs index 31160e64..672926ed 100644 --- a/io-sim/src/Control/Monad/IOSim/STM.hs +++ b/io-sim/src/Control/Monad/IOSim/STM.hs @@ -264,7 +264,7 @@ newEmptyMVarDefault = MVar <$> newTVarIO (MVarEmpty mempty mempty) labelMVarDefault :: MonadLabelledSTM m => MVarDefault m a -> String -> m () -labelMVarDefault (MVar tvar) = atomically . labelTVar tvar . (<> "-MVar") +labelMVarDefault (MVar tvar) = atomically . labelTVar tvar newMVarDefault :: MonadSTM m => a -> m (MVarDefault m a) newMVarDefault a = MVar <$> newTVarIO (MVarFull a mempty) diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index b83363c1..403748a4 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -90,8 +90,8 @@ import Control.Monad.Class.MonadSay import Control.Monad.Class.MonadST import Control.Monad.Class.MonadSTM.Internal (MonadInspectSTM (..), MonadLabelledSTM (..), MonadSTM, MonadTraceSTM (..), TArrayDefault, - TChanDefault, TMVarDefault, TSemDefault, TraceValue, atomically, - retry) + TChanDefault (..), TMVarDefault (..), TSemDefault (..), TraceValue, + atomically, retry) import Control.Monad.Class.MonadSTM.Internal qualified as MonadSTM import Control.Monad.Class.MonadTest import Control.Monad.Class.MonadThrow as MonadThrow hiding (getMaskingState) @@ -219,7 +219,7 @@ data StmA s a where ThrowStm :: SomeException -> StmA s a CatchStm :: StmA s a -> (SomeException -> StmA s a) -> (a -> StmA s b) -> StmA s b - NewTVar :: Maybe String -> x -> (TVar s x -> StmA s b) -> StmA s b + NewTVar :: (VarId -> TVarId) -> Maybe String -> x -> (TVar s x -> StmA s b) -> StmA s b LabelTVar :: String -> TVar s a -> StmA s b -> StmA s b ReadTVar :: TVar s a -> (a -> StmA s b) -> StmA s b WriteTVar :: TVar s a -> a -> StmA s b -> StmA s b @@ -508,14 +508,14 @@ instance MonadSTM (IOSim s) where atomically action = IOSim $ oneShot $ \k -> Atomically action k - newTVar x = STM $ oneShot $ \k -> NewTVar Nothing x k + newTVar x = STM $ oneShot $ \k -> NewTVar TVarId Nothing x k readTVar tvar = STM $ oneShot $ \k -> ReadTVar tvar k writeTVar tvar x = STM $ oneShot $ \k -> WriteTVar tvar x (k ()) retry = STM $ oneShot $ \_ -> Retry orElse a b = STM $ oneShot $ \k -> OrElse (runSTM a) (runSTM b) k - newTMVar = MonadSTM.newTMVarDefault - newEmptyTMVar = MonadSTM.newEmptyTMVarDefault + newTMVar = \a -> STM $ oneShot $ \k -> NewTVar TMVarId Nothing (Just a) (k . TMVar) + newEmptyTMVar = STM $ oneShot $ \k -> NewTVar TMVarId Nothing Nothing (k . TMVar) takeTMVar = MonadSTM.takeTMVarDefault tryTakeTMVar = MonadSTM.tryTakeTMVarDefault putTMVar = MonadSTM.putTMVarDefault @@ -526,7 +526,7 @@ instance MonadSTM (IOSim s) where writeTMVar = MonadSTM.writeTMVarDefault isEmptyTMVar = MonadSTM.isEmptyTMVarDefault - newTQueue = newTQueueDefault + newTQueue = STM $ oneShot $ \k -> NewTVar TQueueId Nothing ([], []) (k . TQueue) readTQueue = readTQueueDefault tryReadTQueue = tryReadTQueueDefault peekTQueue = peekTQueueDefault @@ -536,7 +536,10 @@ instance MonadSTM (IOSim s) where isEmptyTQueue = isEmptyTQueueDefault unGetTQueue = unGetTQueueDefault - newTBQueue = newTBQueueDefault + newTBQueue size | size >= fromIntegral (maxBound :: Int) + = error "newTBQueue: size larger than Int" + | otherwise + = STM $ oneShot $ \k -> NewTVar TBQueueId Nothing ([], 0, [], size) (k . (`TBQueue` size )) readTBQueue = readTBQueueDefault tryReadTBQueue = tryReadTBQueueDefault peekTBQueue = peekTBQueueDefault @@ -548,7 +551,7 @@ instance MonadSTM (IOSim s) where isFullTBQueue = isFullTBQueueDefault unGetTBQueue = unGetTBQueueDefault - newTSem = MonadSTM.newTSemDefault + newTSem = \i -> STM $ oneShot $ \k -> NewTVar TSemId Nothing i (k . TSem) waitTSem = MonadSTM.waitTSemDefault signalTSem = MonadSTM.signalTSemDefault signalTSemN = MonadSTM.signalTSemNDefault @@ -588,8 +591,8 @@ instance MonadTraceSTM (IOSim s) where instance MonadMVar (IOSim s) where type MVar (IOSim s) = MVarDefault (IOSim s) - newEmptyMVar = newEmptyMVarDefault - newMVar = newMVarDefault + newEmptyMVar = atomically $ STM $ oneShot $ \k -> NewTVar MVarId Nothing (MVarEmpty mempty mempty) (k . MVar) + newMVar = \a -> atomically $ STM $ oneShot $ \k -> NewTVar MVarId Nothing (MVarFull a mempty) (k . MVar) takeMVar = takeMVarDefault putMVar = putMVarDefault tryTakeMVar = tryTakeMVarDefault @@ -1233,7 +1236,7 @@ data StmTxResult s a = ![SomeTVar s] -- ^ created tvars ![Dynamic] ![String] - !TVarId -- updated TVarId name supply + !VarId -- updated TVarId name supply -- | A blocked transaction reports the vars that were read so that the -- scheduler can block the thread on those vars. diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index 62da29ef..72409a6b 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -195,7 +195,7 @@ data SimState s a = SimState { -- | timeout locks in order to synchronize the timeout handler and the -- main thread clocks :: !(Map ClockId UTCTime), - nextVid :: !TVarId, -- ^ next unused 'TVarId' + nextVid :: !VarId, -- ^ next unused 'TVarId' nextTmid :: !TimeoutId, -- ^ next unused 'TimeoutId' -- | previous steps (which we may race with). -- Note this is *lazy*, so that we don't compute races we will not reverse. @@ -217,7 +217,7 @@ initialState = curTime = Time 0, timers = PSQ.empty, clocks = Map.singleton (ClockId []) epoch1970, - nextVid = TVarId 0, + nextVid = 0, nextTmid = TimeoutId 0, races = noRaces, control = ControlDefault, @@ -480,7 +480,7 @@ schedule thread@Thread{ error "schedule: StartTimeout: Impossible happened" StartTimeout d action' k -> do - lock <- TMVar <$> execNewTVar nextVid (Just $! "lock-" ++ show nextTmid) Nothing + lock <- TMVar <$> execNewTVar (TMVarId nextVid) (Just $! "lock-" ++ show nextTmid) Nothing let expiry = d `addTime` time timers' = PSQ.insert nextTmid expiry (TimerTimeout tid nextTmid lock) timers thread' = thread { threadControl = @@ -496,19 +496,19 @@ schedule thread@Thread{ schedule thread' simstate { timers = PSQ.delete tmid timers } RegisterDelay d k | d < 0 -> do - tvar <- execNewTVar nextVid + tvar <- execNewTVar (TVarId nextVid) (Just $! "<>") True modifySTRef (tvarVClock tvar) (leastUpperBoundVClock vClock) let !expiry = d `addTime` time !thread' = thread { threadControl = ThreadControl (k tvar) ctl } trace <- schedule thread' simstate { nextVid = succ nextVid } - return (SimPORTrace time tid tstep tlbl (EventRegisterDelayCreated nextTmid nextVid expiry) $ + return (SimPORTrace time tid tstep tlbl (EventRegisterDelayCreated nextTmid (TVarId nextVid) expiry) $ SimPORTrace time tid tstep tlbl (EventRegisterDelayFired nextTmid) $ trace) RegisterDelay d k -> do - tvar <- execNewTVar nextVid + tvar <- execNewTVar (TVarId nextVid) (Just $! "<>") False modifySTRef (tvarVClock tvar) (leastUpperBoundVClock vClock) @@ -519,7 +519,7 @@ schedule thread@Thread{ , nextVid = succ nextVid , nextTmid = succ nextTmid } return (SimPORTrace time tid tstep tlbl - (EventRegisterDelayCreated nextTmid nextVid expiry) trace) + (EventRegisterDelayCreated nextTmid (TVarId nextVid) expiry) trace) ThreadDelay d k | d < 0 -> do let expiry = d `addTime` time @@ -547,12 +547,12 @@ schedule thread@Thread{ expiry = d `addTime` time thread' = thread { threadControl = ThreadControl (k t) ctl } trace <- schedule thread' simstate { nextTmid = succ nextTmid } - return (SimPORTrace time tid tstep tlbl (EventTimerCreated nextTmid nextVid expiry) $ + return (SimPORTrace time tid tstep tlbl (EventTimerCreated nextTmid (TVarId nextVid) expiry) $ SimPORTrace time tid tstep tlbl (EventTimerCancelled nextTmid) $ trace) NewTimeout d k -> do - tvar <- execNewTVar nextVid + tvar <- execNewTVar (TVarId nextVid) (Just $! "<>") TimeoutPending modifySTRef (tvarVClock tvar) (leastUpperBoundVClock vClock) @@ -561,9 +561,9 @@ schedule thread@Thread{ timers' = PSQ.insert nextTmid expiry (Timer tvar) timers thread' = thread { threadControl = ThreadControl (k t) ctl } trace <- schedule thread' simstate { timers = timers' - , nextVid = succ (succ nextVid) - , nextTmid = succ nextTmid } - return (SimPORTrace time tid tstep tlbl (EventTimerCreated nextTmid nextVid expiry) trace) + , nextVid = succ (succ nextVid) + , nextTmid = succ nextTmid } + return (SimPORTrace time tid tstep tlbl (EventTimerCreated nextTmid (TVarId nextVid) expiry) trace) CancelTimeout (Timeout tvar tmid) k -> do let timers' = PSQ.delete tmid timers @@ -1358,7 +1358,7 @@ execAtomically :: forall s a c. Time -> IOSimThreadId -> Maybe ThreadLabel - -> TVarId + -> VarId -> StmA s a -> (StmTxResult s a -> ST s (SimTrace c)) -> ST s (SimTrace c) @@ -1371,7 +1371,7 @@ execAtomically !time !tid !tlbl !nextVid0 !action0 !k0 = -> Map TVarId (SomeTVar s) -- set of vars written -> [SomeTVar s] -- vars written in order (no dups) -> [SomeTVar s] -- vars created in order - -> TVarId -- var fresh name supply + -> VarId -- var fresh name supply -> StmA s b -> ST s (SimTrace c) go !ctl !read !written !writtenSeq !createdSeq !nextVid !action = @@ -1470,8 +1470,8 @@ execAtomically !time !tid !tlbl !nextVid0 !action0 !k0 = let ctl' = BranchFrame (OrElseStmA b) k written writtenSeq createdSeq ctl go ctl' read Map.empty [] [] nextVid a - NewTVar !mbLabel x k -> do - !v <- execNewTVar nextVid mbLabel x + NewTVar mkId !mbLabel x k -> do + !v <- execNewTVar (mkId nextVid) mbLabel x -- record a write to the TVar so we know to update its VClock let written' = Map.insert (tvarId v) (SomeTVar v) written -- save the value: it will be committed or reverted @@ -1560,14 +1560,14 @@ execAtomically' = go Map.empty execNewTVar :: TVarId -> Maybe String -> a -> ST s (TVar s a) -execNewTVar nextVid !mbLabel x = do +execNewTVar !tvarId !mbLabel x = do tvarLabel <- newSTRef mbLabel tvarCurrent <- newSTRef x tvarUndo <- newSTRef [] tvarBlocked <- newSTRef ([], Set.empty) tvarVClock <- newSTRef bottomVClock tvarTrace <- newSTRef Nothing - return TVar {tvarId = nextVid, tvarLabel, + return TVar {tvarId, tvarLabel, tvarCurrent, tvarUndo, tvarBlocked, tvarVClock, tvarTrace} @@ -1849,7 +1849,8 @@ normalizeRaces Races{ activeRaces, completeRaces } = $ activeRaces ) ++ completeRaces - in Races{ activeRaces = activeRaces', completeRaces = completeRaces' } + in Races{ activeRaces = activeRaces', + completeRaces = completeRaces' } -- When a thread terminates, we remove it from the concurrent thread diff --git a/io-sim/src/Control/Monad/IOSimPOR/Types.hs b/io-sim/src/Control/Monad/IOSimPOR/Types.hs index 228be12d..772acb51 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Types.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Types.hs @@ -69,15 +69,9 @@ instance Monoid Effect where -- Effect smart constructors -- --- readEffect :: SomeTVar s -> Effect --- readEffect r = mempty{effectReads = Set.singleton $ someTvarId r } - readEffects :: [Labelled (SomeTVar s)] -> Effect readEffects rs = mempty{effectReads = Set.fromList (map (someTvarId <$>) rs)} --- writeEffect :: SomeTVar s -> Effect --- writeEffect r = mempty{effectWrites = Set.singleton $ someTvarId r } - writeEffects :: [Labelled (SomeTVar s)] -> Effect writeEffects rs = mempty{effectWrites = Set.fromList (map (someTvarId <$>) rs)} @@ -224,11 +218,18 @@ data StepInfo = StepInfo { -- Races -- -data Races = Races { -- These steps may still race with future steps - activeRaces :: ![StepInfo], - -- These steps cannot be concurrent with future steps - completeRaces :: ![StepInfo] - } +-- | Information about all discovered races in a simulation categorised as +-- active and complete races. +-- +-- See 'normalizeRaces' how we split `StepInfo` into the two categories. +-- +data Races = Races { + -- | These steps may still race with future steps. + activeRaces :: ![StepInfo], + + -- | These steps cannot be concurrent with future steps. + completeRaces :: ![StepInfo] + } deriving Show noRaces :: Races