@@ -1463,23 +1463,16 @@ updateRaces newStep@Step{ stepThreadId = tid, stepEffect = newEffect }
1463
1463
-- then any threads that it wakes up become non-concurrent also.
1464
1464
let lessConcurrent = foldr Set. delete concurrent (effectWakeup newEffect) in
1465
1465
if tid `elem` concurrent then
1466
- let theseStepsRace = isRacyThreadId tid
1467
- && step `racingSteps` newStep
1466
+ let theseStepsRace = isRacyThreadId tid && racingSteps step newStep
1468
1467
happensBefore = step `happensBeforeStep` newStep
1469
1468
nondep' | happensBefore = nondep
1470
1469
| otherwise = newStep : nondep
1471
- -- We cannot remove the 'tid' thread from the set of concurrent
1472
- -- threads if 'theseStepsRace'. This was done previously in
1473
- -- order to record only the first race with each thread. But
1474
- -- it can happen that the frist race will block a thread that
1475
- -- is scheduled to run until another later step unblock it
1476
- -- (e.g. 'modifyTMVar`). If we remove the 'tid' from the set
1477
- -- of concurrent threads we can end up in a situation where
1478
- -- a schedule is not runnable, because the next thread to run
1479
- -- is still blocked (e.g. 'TMVar' is taken but not yet
1480
- -- released).
1481
- concurrent' | happensBefore = Set. delete tid lessConcurrent
1482
- | otherwise = concurrent
1470
+ -- We will only record the first race with each thread---reversing
1471
+ -- the first race makes the next race detectable. Thus we remove a
1472
+ -- thread from the concurrent set after the first race.
1473
+ concurrent' | happensBefore = Set. delete tid lessConcurrent
1474
+ | theseStepsRace = Set. delete tid concurrent
1475
+ | otherwise = concurrent
1483
1476
-- Here we record discovered races.
1484
1477
-- We only record a new race if we are following the default schedule,
1485
1478
-- to avoid finding the same race in different parts of the search space.
0 commit comments