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 (..)
+  , Unique
     -- ** 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
+  , Unique (..)
     -- * Utils
   , ppList
   ) where
@@ -202,6 +204,16 @@ 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".
+newtype Unique s = MkUnique{ unMkUnique :: Integer }
+  deriving stock   (Eq, Ord)
+  deriving newtype NFData
+type role Unique nominal
+
+instance Hashable (Unique s) where
+  hash = fromInteger . unMkUnique
+  hashWithSalt = defaultHashWithSalt
+
 --
 -- Utils
 --

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

@@ -143,7 +143,8 @@ data SimState s a = SimState {
        -- | list of clocks
        clocks   :: !(Map ClockId UTCTime),
        nextVid  :: !VarId,     -- ^ next unused 'VarId'
-       nextTmid :: !TimeoutId   -- ^ next unused 'TimeoutId'
+       nextTmid :: !TimeoutId, -- ^ next unused 'TimeoutId'
+       nextUniq :: !(Unique s) -- ^ next unused @'Unique' 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,13 @@ schedule !thread@Thread{
           thread' = thread { threadControl = ThreadControl k' ctl }
       schedule thread' simstate
 
+    NewUnique k -> do
+      let thread'   = thread{ threadControl = ThreadControl (k nextUniq) ctl }
+          n         = unMkUnique nextUniq
+          simstate' = simstate{ nextUniq = MkUnique (n + 1) }
+      SimTrace time tid tlbl (EventUniqueCreated n)
+        <$> 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)
@@ -122,6 +124,7 @@ import GHC.Generics (Generic)
 import Quiet (Quiet (..))
 
 import Control.Monad.IOSim.CommonTypes
+import Control.Monad.IOSim.CommonTypes qualified as Sim
 import Control.Monad.IOSim.STM
 import Control.Monad.IOSimPOR.Types
 
@@ -193,6 +196,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    :: (Sim.Unique s -> SimA s r) -> SimA s r
 
 
 newtype STM s a = STM { unSTM :: forall r. (a -> StmA s r) -> StmA s r }
@@ -626,6 +630,11 @@ instance MonadTraceMVar (IOSim s) where
 instance MonadLabelledMVar (IOSim s) where
   labelMVar = labelMVarDefault
 
+instance MonadUnique (IOSim s) where
+  type Unique (IOSim s) = Sim.Unique s
+  newUnique  = IOSim (oneShot NewUnique)
+  hashUnique = hash
+
 data Async s a = Async !IOSimThreadId (STM s (Either SomeException a))
 
 instance Eq (Async s a) where
@@ -1056,6 +1065,9 @@ data SimEventType
   | EventThreadUnhandled SomeException
   -- ^ thread terminated by an unhandled exception
 
+  | EventUniqueCreated Integer
+  -- ^ created the n-th 'Unique'
+
   --
   -- STM events
   --
@@ -1163,6 +1175,7 @@ ppSimEventType = \case
   EventThreadFinished -> "ThreadFinished"
   EventThreadUnhandled a ->
     "ThreadUnhandled " ++ show a
+  EventUniqueCreated n -> "UniqueCreated " ++ show n
   EventTxCommitted written created mbEff ->
     concat [ "TxCommitted ",
              ppList (ppLabelled show) written, " ",

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         :: !(Unique s), -- ^ next unused @'Unique' 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,13 @@ schedule thread@Thread{
       let thread' = thread { threadControl = ThreadControl k ctl }
       schedule thread' simstate
 
+    NewUnique k -> do
+      let thread'   = thread{ threadControl = ThreadControl (k nextUniq) ctl }
+          n         = unMkUnique nextUniq
+          simstate' = simstate{ nextUniq = MkUnique (n + 1) }
+      SimPORTrace time tid tstep tlbl (EventUniqueCreated n)
+        <$> schedule thread' simstate'
+
 
 threadInterruptible :: Thread s a -> Bool
 threadInterruptible thread =