io-sim: Add support for unique symbol generation

Author: LSLeary

io-sim/CHANGELOG.md

@@ -6,6 +6,8 @@
 
 ### Non-breaking changes
 
+* Added support for unique symbol generation à la `Data.Unique`.
+
 ### 1.8.0.1
 
 * Added support for `ghc-9.2`.

io-sim/src/Control/Monad/IOSim.hs

@@ -48,6 +48,7 @@ module Control.Monad.IOSim
   , ThreadLabel
   , IOSimThreadId (..)
   , Labelled (..)
+  , IOSimUnique
     -- ** Dynamic Tracing
   , traceM
   , traceSTM

io-sim/src/Control/Monad/IOSim/CommonTypes.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DeriveAnyClass     #-}
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE DerivingVia        #-}
+{-# LANGUAGE RoleAnnotations    #-}
 
 -- | Common types shared between `IOSim` and `IOSimPOR`.
 --
@@ -28,6 +29,7 @@ module Control.Monad.IOSim.CommonTypes
   , BlockedReason (..)
   , Labelled (..)
   , ppLabelled
+  , IOSimUnique(..)
     -- * Utils
   , ppList
   ) where
@@ -202,6 +204,12 @@ ppLabelled :: (a -> String) -> Labelled a -> String
 ppLabelled pp Labelled { l_labelled = a, l_label = Nothing  } = pp a
 ppLabelled pp Labelled { l_labelled = a, l_label = Just lbl } = concat ["Labelled ", pp a, " ", lbl]
 
+-- | Abstract unique symbols à la "Data.Unique".
+type role IOSimUnique nominal
+newtype IOSimUnique s = MkUnique{ unMkUnique :: Integer }
+  deriving stock   (Eq, Ord)
+  deriving newtype (Hashable, NFData)
+
 --
 -- Utils
 --

io-sim/src/Control/Monad/IOSim/Internal.hs

@@ -142,8 +142,9 @@ data SimState s a = SimState {
        timers   :: !(Timeouts s),
        -- | list of clocks
        clocks   :: !(Map ClockId UTCTime),
-       nextVid  :: !VarId,     -- ^ next unused 'VarId'
-       nextTmid :: !TimeoutId   -- ^ next unused 'TimeoutId'
+       nextVid  :: !VarId,          -- ^ next unused 'VarId'
+       nextTmid :: !TimeoutId,      -- ^ next unused 'TimeoutId'
+       nextUniq :: !(IOSimUnique s) -- ^ next unused @'IOSimUnique' s@
      }
 
 initialState :: SimState s a
@@ -155,7 +156,8 @@ initialState =
       timers   = PSQ.empty,
       clocks   = Map.singleton (ClockId []) epoch1970,
       nextVid  = 0,
-      nextTmid = TimeoutId 0
+      nextTmid = TimeoutId 0,
+      nextUniq = MkUnique 0
     }
   where
     epoch1970 = UTCTime (fromGregorian 1970 1 1) 0
@@ -197,7 +199,7 @@ schedule !thread@Thread{
            threads,
            timers,
            clocks,
-           nextVid, nextTmid,
+           nextVid, nextTmid, nextUniq,
            curTime  = time
          } =
   invariant (Just thread) simstate $
@@ -631,6 +633,11 @@ schedule !thread@Thread{
           thread' = thread { threadControl = ThreadControl k' ctl }
       schedule thread' simstate
 
+    NewUnique k -> do
+      let thread'   = thread{ threadControl = ThreadControl (k nextUniq) ctl }
+          simstate' = simstate{ nextUniq = MkUnique (unMkUnique nextUniq + 1) }
+      schedule thread' simstate'
+
 
 threadInterruptible :: Thread s a -> Bool
 threadInterruptible thread =

io-sim/src/Control/Monad/IOSim/Types.hs

@@ -93,6 +93,7 @@ import Control.Monad.Class.MonadTime.SI qualified as SI
 import Control.Monad.Class.MonadTimer
 import Control.Monad.Class.MonadTimer.SI (TimeoutState (..))
 import Control.Monad.Class.MonadTimer.SI qualified as SI
+import Control.Monad.Class.MonadUnique
 import Control.Monad.Primitive qualified as Prim
 import Control.Monad.ST.Lazy
 import Control.Monad.ST.Strict qualified as StrictST
@@ -104,6 +105,7 @@ import Control.Monad.Fail qualified as Fail
 import Data.Bifoldable
 import Data.Bifunctor (bimap)
 import Data.Dynamic (Dynamic, toDyn)
+import Data.Hashable (Hashable(hash))
 import Data.List.Trace qualified as Trace
 import Data.Map.Strict (Map)
 import Data.Maybe (fromMaybe)
@@ -193,6 +195,7 @@ data SimA s a where
   ExploreRaces :: SimA s b -> SimA s b
 
   Fix          :: (x -> IOSim s x) -> (x -> SimA s r) -> SimA s r
+  NewUnique    :: (IOSimUnique s -> SimA s r) -> SimA s r
 
 
 newtype STM s a = STM { unSTM :: forall r. (a -> StmA s r) -> StmA s r }
@@ -626,6 +629,11 @@ instance MonadTraceMVar (IOSim s) where
 instance MonadLabelledMVar (IOSim s) where
   labelMVar = labelMVarDefault
 
+instance MonadUnique (IOSim s) where
+  type Unique (IOSim s) = IOSimUnique s
+  newUnique  = IOSim (oneShot NewUnique)
+  hashUnique = hash
+
 data Async s a = Async !IOSimThreadId (STM s (Either SomeException a))
 
 instance Eq (Async s a) where

io-sim/src/Control/Monad/IOSimPOR/Internal.hs

@@ -200,6 +200,7 @@ data SimState s a = SimState {
        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.
+       nextUniq         :: !(IOSimUnique s), -- ^ next unused @'IOSimUnique' s@
        races            :: Races,
        -- | control the schedule followed, and initial value
        control          :: !ScheduleControl,
@@ -220,6 +221,7 @@ initialState =
       clocks   = Map.singleton (ClockId []) epoch1970,
       nextVid  = 0,
       nextTmid = TimeoutId 0,
+      nextUniq = MkUnique 0,
       races    = noRaces,
       control  = ControlDefault,
       control0 = ControlDefault,
@@ -273,7 +275,7 @@ schedule thread@Thread{
            threads,
            timers,
            clocks,
-           nextVid, nextTmid,
+           nextVid, nextTmid, nextUniq,
            curTime  = time,
            control,
            perStepTimeLimit
@@ -814,6 +816,11 @@ schedule thread@Thread{
       let thread' = thread { threadControl = ThreadControl k ctl }
       schedule thread' simstate
 
+    NewUnique k -> do
+      let thread'   = thread{ threadControl = ThreadControl (k nextUniq) ctl }
+          simstate' = simstate{ nextUniq = MkUnique (unMkUnique nextUniq + 1) }
+      schedule thread' simstate'
+
 
 threadInterruptible :: Thread s a -> Bool
 threadInterruptible thread =