From d62cdacd826ae9e8641131b571751afca37f43e4 Mon Sep 17 00:00:00 2001 From: Javier Sagredo Date: Thu, 12 Nov 2026 13:59:27 +0100 Subject: [PATCH 1/4] IOSimPOR: exploreRacesOfThreadsLabelled, to race only threads with chosen labels exploreRaces makes the calling thread's future children racy, by their thread ids. A test of a large system, which forks many threads before it gets to what it wants to explore, can either make all of them racy, and spend most of each schedule's race analysis on threads it does not care about, or none. exploreRacesOfThreadsLabelled p takes into account, when discovering races, each thread once it is given a label that satisfies p, until it is given one that does not. Such a thread's children do not inherit it. Thread ids do not change, so ScheduleControl replay is unaffected. runSimTrace ignores it. --- io-sim/src/Control/Monad/IOSim.hs | 1 + io-sim/src/Control/Monad/IOSim/Internal.hs | 3 ++ io-sim/src/Control/Monad/IOSim/Types.hs | 11 ++++++ io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 34 +++++++++++++++---- 4 files changed, 43 insertions(+), 6 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim.hs b/io-sim/src/Control/Monad/IOSim.hs index 53f9ad59..34534979 100644 --- a/io-sim/src/Control/Monad/IOSim.hs +++ b/io-sim/src/Control/Monad/IOSim.hs @@ -54,6 +54,7 @@ module Control.Monad.IOSim , Unique -- ** Dynamic Tracing , traceM + , exploreRacesOfThreadsLabelled , traceSTM -- ** Pretty printers , ppTrace diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index dfe70e29..c27d36f4 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -633,6 +633,9 @@ schedule !thread@Thread{ ExploreRaces k -> schedule thread{ threadControl = ThreadControl k ctl } simstate + ExploreRacesOfThreadsLabelled _ k -> + schedule thread{ threadControl = ThreadControl k ctl } simstate + Fix f k -> do r <- newSTRef (throw NonTermination) x <- unsafeInterleaveST $ readSTRef r diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index afef532b..7324801a 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -14,6 +14,7 @@ module Control.Monad.IOSim.Types ( IOSim (..) , runIOSim , traceM + , exploreRacesOfThreadsLabelled , traceSTM , liftST , SimA (..) @@ -148,6 +149,14 @@ runIOSim (IOSim k) = k Return traceM :: Typeable a => a -> IOSim s () traceM !x = IOSim $ oneShot $ \k -> Output (toDyn x) (k ()) +-- | /IOSimPOR/: from now on, take into account, when discovering races, each +-- thread once it is given a label that satisfies the predicate, until it is +-- given one that does not. Unlike 'exploreRaces', this does not make the +-- threads such a thread forks racy: each thread races by its own label. A later +-- call replaces the predicate. 'runSimTrace' ignores it. +exploreRacesOfThreadsLabelled :: (ThreadLabel -> Bool) -> IOSim s () +exploreRacesOfThreadsLabelled p = IOSim $ oneShot $ \k -> ExploreRacesOfThreadsLabelled p (k ()) + -- | Trace a value, in the same was as `traceM` does, but from the `STM` monad. -- This is primarily useful for debugging. -- @@ -197,6 +206,8 @@ data SimA s a where ExploreRaces :: SimA s b -> SimA s b + ExploreRacesOfThreadsLabelled :: (ThreadLabel -> Bool) -> 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 diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index 921188e0..b026321d 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -208,7 +208,12 @@ data SimState s a = SimState { control0 :: !ScheduleControl, -- | limit on the computation time allowed per scheduling step, for -- catching infinite loops etc - perStepTimeLimit :: Maybe Int + perStepTimeLimit :: Maybe Int, + -- | the predicate 'exploreRacesOfThreadsLabelled' gave, if any + racyLabel :: Maybe (ThreadLabel -> Bool), + -- | the threads whose label satisfies 'racyLabel': they race, whatever + -- their 'IOSimThreadId' + racyByLabel :: !(Set IOSimThreadId) } @@ -226,11 +231,23 @@ initialState = races = noRaces, control = ControlDefault, control0 = ControlDefault, - perStepTimeLimit = Nothing + perStepTimeLimit = Nothing, + racyLabel = Nothing, + racyByLabel = Set.empty } where epoch1970 = UTCTime (fromGregorian 1970 1 1) 0 +-- | Record whether the thread, given this label, races by its label: a label +-- that no longer satisfies the predicate stops it racing. +labelledRacy :: IOSimThreadId -> ThreadLabel -> SimState s a -> SimState s a +labelledRacy tid l simstate@SimState{ racyLabel, racyByLabel } = + case racyLabel of + Nothing -> simstate + Just p + | p l -> simstate { racyByLabel = Set.insert tid racyByLabel } + | otherwise -> simstate { racyByLabel = Set.delete tid racyByLabel } + invariant :: Maybe (Thread s a) -> SimState s a -> x -> x invariant (Just running) simstate@SimState{runqueue,threads,clocks} = @@ -714,7 +731,7 @@ schedule thread@Thread{ LabelThread tid' l k | tid' == tid -> do let thread' = thread { threadControl = ThreadControl k ctl , threadLabel = Just l } - schedule thread' simstate + schedule thread' (labelledRacy tid l simstate) GetThreadLabel tid' k -> do let tlbl' | tid' == tid = tlbl @@ -726,13 +743,17 @@ schedule thread@Thread{ LabelThread tid' l k -> do let thread' = thread { threadControl = ThreadControl k ctl } threads' = Map.adjust (\t -> t { threadLabel = Just l }) tid' threads - schedule thread' simstate { threads = threads' } + schedule thread' (labelledRacy tid' l simstate { threads = threads' }) ExploreRaces k -> do let thread' = thread { threadControl = ThreadControl k ctl , threadRacy = True } schedule thread' simstate + ExploreRacesOfThreadsLabelled p k -> do + let thread' = thread { threadControl = ThreadControl k ctl } + schedule thread' simstate { racyLabel = Just p } + Fix f k -> do r <- newSTRef (throw NonTermination) x <- unsafeInterleaveST $ readSTRef r @@ -1770,7 +1791,7 @@ stepThread thread@Thread { threadId = tid, -- with it. updateRaces :: Thread s a -> SimState s a -> Races updateRaces thread@Thread { threadId = tid } - SimState{ control, threads, races = races@Races { activeRaces } } = + SimState{ control, threads, racyByLabel, races = races@Races { activeRaces } } = let newStep@Step{ stepEffect = newEffect } = currentStep thread @@ -1782,7 +1803,8 @@ updateRaces thread@Thread { threadId = tid } -- A new step to add to the `activeRaces` list. newStepInfo :: Maybe StepInfo - !newStepInfo | isNotRacyThreadId tid = Nothing + !newStepInfo | isNotRacyThreadId tid + , tid `Set.notMember` racyByLabel = Nothing -- non-racy threads do not race | Set.null concurrent = Nothing From aae7a91ac63cca8dabf405688bbea96493004e36 Mon Sep 17 00:00:00 2001 From: Javier Sagredo Date: Thu, 12 Nov 2026 14:24:37 +0100 Subject: [PATCH 2/4] exploreRacesOfThreadsLabelled: also race threads already so labelled So a test can call it once it has set up what it wants to explore: the threads it started during the set-up race from then on, and the set-up's own races, which IOSimPOR would otherwise reverse first and spend its bounds on, are left out. A later call recomputes the set from the new predicate; calling it with const False stops all racing by label. --- io-sim/src/Control/Monad/IOSim/Types.hs | 10 ++++++---- io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 7 ++++++- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index 7324801a..d4a2c05d 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -150,10 +150,12 @@ traceM :: Typeable a => a -> IOSim s () traceM !x = IOSim $ oneShot $ \k -> Output (toDyn x) (k ()) -- | /IOSimPOR/: from now on, take into account, when discovering races, each --- thread once it is given a label that satisfies the predicate, until it is --- given one that does not. Unlike 'exploreRaces', this does not make the --- threads such a thread forks racy: each thread races by its own label. A later --- call replaces the predicate. 'runSimTrace' ignores it. +-- thread whose label satisfies the predicate: a thread already so labelled, +-- and a thread once it is given such a label, until it is given one that does +-- not. Unlike 'exploreRaces', this does not make the threads such a thread +-- forks racy: each thread races by its own label. A later call replaces the +-- predicate. Calling it once a test has set up what it wants to explore keeps +-- the races of the set-up out of the exploration. 'runSimTrace' ignores it. exploreRacesOfThreadsLabelled :: (ThreadLabel -> Bool) -> IOSim s () exploreRacesOfThreadsLabelled p = IOSim $ oneShot $ \k -> ExploreRacesOfThreadsLabelled p (k ()) diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index b026321d..4760a93b 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -752,7 +752,12 @@ schedule thread@Thread{ ExploreRacesOfThreadsLabelled p k -> do let thread' = thread { threadControl = ThreadControl k ctl } - schedule thread' simstate { racyLabel = Just p } + labelled = Set.fromList + [ threadId t + | t <- thread : Map.elems threads + , Just l <- [threadLabel t] + , p l ] + schedule thread' simstate { racyLabel = Just p, racyByLabel = labelled } Fix f k -> do r <- newSTRef (throw NonTermination) From df2ff87f128ba7b4069e5863091fd64141be360b Mon Sep 17 00:00:00 2001 From: Javier Sagredo Date: Thu, 12 Nov 2026 14:32:42 +0100 Subject: [PATCH 3/4] exploreRacesOfThreadsLabelled: unlabelled children race like their parent A thread racing by its label now lends that to the threads it forks, until they are labelled themselves; then their own label decides. A helper the code forks without a label, such as an async worker, races with the thread that started it, while a labelled child, such as a driver's sender, is still left out unless the predicate names it. --- io-sim/src/Control/Monad/IOSim/Types.hs | 6 +++--- io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 10 ++++++++-- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index d4a2c05d..d06a2ed5 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -152,9 +152,9 @@ traceM !x = IOSim $ oneShot $ \k -> Output (toDyn x) (k ()) -- | /IOSimPOR/: from now on, take into account, when discovering races, each -- thread whose label satisfies the predicate: a thread already so labelled, -- and a thread once it is given such a label, until it is given one that does --- not. Unlike 'exploreRaces', this does not make the threads such a thread --- forks racy: each thread races by its own label. A later call replaces the --- predicate. Calling it once a test has set up what it wants to explore keeps +-- not. A thread such a thread forks races too, until it is labelled: then its +-- own label decides. Unlike with 'exploreRaces', so, a labelled child does not +-- inherit it. A later call replaces the predicate. Calling it once a test has set up what it wants to explore keeps -- the races of the set-up out of the exploration. 'runSimTrace' ignores it. exploreRacesOfThreadsLabelled :: (ThreadLabel -> Bool) -> IOSim s () exploreRacesOfThreadsLabelled p = IOSim $ oneShot $ \k -> ExploreRacesOfThreadsLabelled p (k ()) diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index 4760a93b..2f7c4078 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -647,10 +647,16 @@ schedule thread@Thread{ , threadRacy = threadRacy thread } threads' = Map.insert tid' thread'' threads + -- A thread racing by its label lends that to the threads it forks, + -- until they are labelled themselves. + racyByLabel' + | tid `Set.member` racyByLabel simstate = Set.insert tid' (racyByLabel simstate) + | otherwise = racyByLabel simstate -- A newly forked thread may have a higher priority, so we deschedule this one. !trace <- deschedule Yield thread' - simstate { runqueue = insertThread thread'' runqueue - , threads = threads' } + simstate { runqueue = insertThread thread'' runqueue + , threads = threads' + , racyByLabel = racyByLabel' } return $ SimPORTrace time tid tstep tlbl (EventThreadForked tid') $ SimPORTrace time tid tstep tlbl (EventDeschedule Yield) $ trace From 424918910316bb3e50c3fff48dd0393ea694071e Mon Sep 17 00:00:00 2001 From: Javier Sagredo Date: Fri, 13 Nov 2026 14:25:37 +0100 Subject: [PATCH 4/4] Add changelog --- io-sim/CHANGELOG.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/io-sim/CHANGELOG.md b/io-sim/CHANGELOG.md index 9ad02b79..3245114d 100644 --- a/io-sim/CHANGELOG.md +++ b/io-sim/CHANGELOG.md @@ -1,5 +1,14 @@ # Revision history of io-sim +## Next version + +### Non-breaking changes + +* New primitive `IOSimPOR.exploreRacesOfThreadsLabelled` which accepts a list of + labels and races only threads whose labels match the list (even already + labelled). Unlabelled child threads also are considered racy. + + ## 1.11.0.0 ### Breaking changes