Skip to content

Commit

Permalink
io-sim-por: concurrent threads
Browse files Browse the repository at this point in the history
If 'happensBefore' is 'False', but 'theseStepsRace' is true in
'updateRaces', we used to remove the thread id from concurrent threads.
But this lead to discovering a schedule which is not runnable.  See note
in this patch for further details.
  • Loading branch information
coot committed Mar 7, 2022
1 parent bf6d8da commit 6b986f1
Showing 1 changed file with 14 additions and 7 deletions.
21 changes: 14 additions & 7 deletions io-sim/src/Control/Monad/IOSimPOR/Internal.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1463,16 +1463,23 @@ updateRaces newStep@Step{ stepThreadId = tid, stepEffect = newEffect }
-- then any threads that it wakes up become non-concurrent also.
let lessConcurrent = foldr Set.delete concurrent (effectWakeup newEffect) in
if tid `elem` concurrent then
let theseStepsRace = isRacyThreadId tid && racingSteps step newStep
let theseStepsRace = isRacyThreadId tid
&& step `racingSteps` newStep
happensBefore = step `happensBeforeStep` newStep
nondep' | happensBefore = nondep
| otherwise = newStep : nondep
-- We will only record the first race with each thread---reversing
-- the first race makes the next race detectable. Thus we remove a
-- thread from the concurrent set after the first race.
concurrent' | happensBefore = Set.delete tid lessConcurrent
| theseStepsRace = Set.delete tid concurrent
| otherwise = concurrent
-- We cannot remove the 'tid' thread from the set of concurrent
-- threads if 'theseStepsRace'. This was done previously in
-- order to record only the first race with each thread. But
-- it can happen that the frist race will block a thread that
-- is scheduled to run until another later step unblock it
-- (e.g. 'modifyTMVar`). If we remove the 'tid' from the set
-- of concurrent threads we can end up in a situation where
-- a schedule is not runnable, because the next thread to run
-- is still blocked (e.g. 'TMVar' is taken but not yet
-- released).
concurrent' | happensBefore = Set.delete tid lessConcurrent
| otherwise = concurrent
-- Here we record discovered races.
-- We only record a new race if we are following the default schedule,
-- to avoid finding the same race in different parts of the search space.
Expand Down

0 comments on commit 6b986f1

Please sign in to comment.