Distinct TVarIds for various TVar roles

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
 

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)))
      }
 

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 $! "<<timeout " ++ show (unTimeoutId nextTmid) ++ ">>")
                           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 $! "<<timeout " ++ show (unTimeoutId nextTmid) ++ ">>")
                           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 $! "<<timeout-state " ++ show (unTimeoutId nextTmid) ++ ">>")
                            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/

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)

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.