exploreRacesOfThreadsLabelled

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

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

@@ -54,6 +54,7 @@ module Control.Monad.IOSim
   , Unique
     -- ** Dynamic Tracing
   , traceM
+  , exploreRacesOfThreadsLabelled
   , traceSTM
     -- ** Pretty printers
   , ppTrace

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

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
 

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