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 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..d06a2ed5 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,16 @@ 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 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. 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 ()) + -- | Trace a value, in the same was as `traceM` does, but from the `STM` monad. -- This is primarily useful for debugging. -- @@ -197,6 +208,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..2f7c4078 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} = @@ -630,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 @@ -714,7 +737,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 +749,22 @@ 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 } + 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) x <- unsafeInterleaveST $ readSTRef r @@ -1770,7 +1802,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 +1814,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