diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index 2565eab3..8557136a 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -1236,9 +1236,8 @@ execNewTVar !tvarId !mbLabel x = do !tvarBlocked <- newSTRef ([], Set.empty) !tvarVClock <- newSTRef $! VectorClock Map.empty !tvarTrace <- newSTRef $! Nothing - return TVar {tvarId, 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/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index 56e3c963..72409a6b 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -561,8 +561,8 @@ 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 } + , 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 @@ -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