Skip to content

Commit 2b35ab3

Browse files
committed
io-sim-por: don't follow threads which are after any of the races
Consider the following sequence of events x ⋮ y ⋮ z If x is racing with z, we will reverse x and z (e.g. postpone x after z). If y is also racing with x, then we should not include in the schedule any event which happens after it. Originally we used a policy to remove y's thread from the list of racing threads with the x's thread. But this turns out to be too week. While we are visiting new events we need to remove their threads as soon as the event happens after any of the so far discovered races. Otherwise we can end with a schedule which contains events that can only happen after the racing event was executed, and thus likely will block and violate internal invariant: all steps which we follow should be in the runqueue (e.g. should not be blocked).
1 parent 0fb902e commit 2b35ab3

File tree

1 file changed

+7
-4
lines changed

1 file changed

+7
-4
lines changed

io-sim/src/Control/Monad/IOSimPOR/Internal.hs

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1777,16 +1777,19 @@ updateRaces thread@Thread { threadId = tid }
17771777
else let theseStepsRace = step `racingSteps` newStep
17781778
-- `step` happened before `newStep` (`newStep` happened after
17791779
-- `step`)
1780-
happensBefore = step `happensBeforeStep` newStep
1780+
happensBefore = step `happensBeforeStep` newStep
1781+
-- `newStep` happens after any of the racing steps
1782+
afterRacingStep = any (`happensBeforeStep` newStep) stepInfoRaces
17811783

17821784
-- We will only record the first race with each thread.
17831785
-- Reversing the first race makes the next race detectable.
17841786
-- Thus we remove a thread from the concurrent set after the
17851787
-- first race.
17861788
!concurrent'
1787-
| happensBefore = Set.delete tid lessConcurrent
1788-
| theseStepsRace = Set.delete tid concurrent
1789-
| otherwise = concurrent
1789+
| happensBefore = Set.delete tid lessConcurrent
1790+
| theseStepsRace = Set.delete tid concurrent
1791+
| afterRacingStep = Set.delete tid concurrent
1792+
| otherwise = concurrent
17901793

17911794
!stepInfoNonDep'
17921795
-- `newStep` happened after `step`

0 commit comments

Comments
 (0)