@@ -105,6 +105,9 @@ data Thread s a = Thread {
105
105
}
106
106
deriving Show
107
107
108
+ threadStepId :: Thread s a -> (ThreadId , Int )
109
+ threadStepId Thread { threadId, threadStep } = (threadId, threadStep)
110
+
108
111
isRacyThreadId :: ThreadId -> Bool
109
112
isRacyThreadId (RacyThreadId _) = True
110
113
isRacyThreadId _ = True
@@ -1215,7 +1218,9 @@ ordNub = go Set.empty
1215
1218
| x `Set.member` s = go s xs
1216
1219
| otherwise = x : go (Set. insert x s) xs
1217
1220
1221
+ --
1218
1222
-- Effects
1223
+ --
1219
1224
1220
1225
data Effect = Effect {
1221
1226
effectReads :: ! (Set TVarId ),
@@ -1276,7 +1281,9 @@ racingEffects e e' =
1276
1281
effectLiftST eff
1277
1282
|| not (Set. null (effectReads eff) && Set. null (effectWrites eff))
1278
1283
1284
+ --
1279
1285
-- Steps
1286
+ --
1280
1287
1281
1288
data Step = Step {
1282
1289
stepThreadId :: ! ThreadId ,
@@ -1336,6 +1343,10 @@ data StepInfo = StepInfo {
1336
1343
}
1337
1344
deriving Show
1338
1345
1346
+ --
1347
+ -- Races
1348
+ --
1349
+
1339
1350
data Races = Races { -- These steps may still race with future steps
1340
1351
activeRaces :: ! [StepInfo ],
1341
1352
-- These steps cannot be concurrent with future steps
@@ -1467,55 +1478,24 @@ traceRaces r = r
1467
1478
-- traceRaces r@Races{activeRaces,completeRaces} =
1468
1479
-- Debug.trace ("Tracking "++show (length (concatMap stepInfoRaces activeRaces)) ++" races") r
1469
1480
1470
- -- Schedule modifications
1471
-
1472
- stepStepId :: Step -> (ThreadId , Int )
1473
- stepStepId Step { stepThreadId = tid, stepStep = n } = (tid,n)
1474
-
1475
- threadStepId :: Thread s a -> (ThreadId , Int )
1476
- threadStepId Thread { threadId, threadStep } = (threadId, threadStep)
1477
-
1478
- stepInfoToScheduleMods :: StepInfo -> [ScheduleMod ]
1479
- stepInfoToScheduleMods
1480
- StepInfo { stepInfoStep = step,
1481
- stepInfoControl = control,
1482
- stepInfoNonDep = nondep,
1483
- stepInfoRaces = races
1484
- } =
1485
- -- It is actually possible for a later step that races with an earlier one
1486
- -- not to *depend* on it in a happens-before sense. But we don't want to try
1487
- -- to follow any steps *after* the later one.
1488
- [ ScheduleMod
1489
- { scheduleModTarget = stepStepId step
1490
- , scheduleModControl = control
1491
- , scheduleModInsertion = takeWhile (/= stepStepId step')
1492
- (map stepStepId (reverse nondep))
1493
- ++ [stepStepId step']
1494
- -- It should be unnecessary to include the delayed
1495
- -- step in the insertion, since the default
1496
- -- scheduling should run it anyway. Removing it may
1497
- -- help avoid redundant schedules.
1498
- -- ++ [stepStepId step]
1499
- }
1500
- | step' <- races ]
1501
-
1502
- traceFinalRacesFound :: SimState s a -> SimTrace a -> SimTrace a
1503
- traceFinalRacesFound simstate@ SimState { control0 = control } =
1504
- TraceRacesFound [extendScheduleControl control m | m <- scheduleMods]
1505
- where SimState { races } =
1506
- quiescentRacesInSimState simstate
1507
- scheduleMods =
1508
- concatMap stepInfoToScheduleMods $ completeRaces races
1509
-
1510
1481
1482
+ --
1511
1483
-- Schedule control
1484
+ --
1512
1485
1513
1486
controlTargets :: StepId -> ScheduleControl -> Bool
1514
1487
controlTargets stepId
1515
1488
(ControlAwait (ScheduleMod { scheduleModTarget }: _)) =
1516
1489
stepId == scheduleModTarget
1517
1490
controlTargets _stepId _ = False
1518
1491
1492
+ followControl :: ScheduleControl -> ScheduleControl
1493
+ followControl (ControlAwait (ScheduleMod { scheduleModInsertion } : mods)) =
1494
+ ControlFollow scheduleModInsertion mods
1495
+ followControl (ControlAwait [] ) = error " Impossible: followControl (ControlAwait [])"
1496
+ followControl ControlDefault {} = error " Impossible: followControl ControlDefault{}"
1497
+ followControl ControlFollow {} = error " Impossible: followControl ControlFollow{}"
1498
+
1519
1499
controlFollows :: StepId -> ScheduleControl -> Bool
1520
1500
controlFollows _stepId ControlDefault = True
1521
1501
controlFollows _stepId (ControlFollow [] _) = True
@@ -1545,12 +1525,44 @@ advanceControl stepId control =
1545
1525
assert (not $ controlTargets stepId control) $
1546
1526
control
1547
1527
1548
- followControl :: ScheduleControl -> ScheduleControl
1549
- followControl (ControlAwait (ScheduleMod { scheduleModInsertion } : mods)) =
1550
- ControlFollow scheduleModInsertion mods
1551
- followControl (ControlAwait [] ) = error " Impossible: followControl (ControlAwait [])"
1552
- followControl ControlDefault {} = error " Impossible: followControl ControlDefault{}"
1553
- followControl ControlFollow {} = error " Impossible: followControl ControlFollow{}"
1528
+ --
1529
+ -- Schedule modifications
1530
+ --
1531
+
1532
+ stepStepId :: Step -> (ThreadId , Int )
1533
+ stepStepId Step { stepThreadId = tid, stepStep = n } = (tid,n)
1534
+
1535
+ stepInfoToScheduleMods :: StepInfo -> [ScheduleMod ]
1536
+ stepInfoToScheduleMods
1537
+ StepInfo { stepInfoStep = step,
1538
+ stepInfoControl = control,
1539
+ stepInfoNonDep = nondep,
1540
+ stepInfoRaces = races
1541
+ } =
1542
+ -- It is actually possible for a later step that races with an earlier one
1543
+ -- not to *depend* on it in a happens-before sense. But we don't want to try
1544
+ -- to follow any steps *after* the later one.
1545
+ [ ScheduleMod
1546
+ { scheduleModTarget = stepStepId step
1547
+ , scheduleModControl = control
1548
+ , scheduleModInsertion = takeWhile (/= stepStepId step')
1549
+ (map stepStepId (reverse nondep))
1550
+ ++ [stepStepId step']
1551
+ -- It should be unnecessary to include the delayed
1552
+ -- step in the insertion, since the default
1553
+ -- scheduling should run it anyway. Removing it may
1554
+ -- help avoid redundant schedules.
1555
+ -- ++ [stepStepId step]
1556
+ }
1557
+ | step' <- races ]
1558
+
1559
+ traceFinalRacesFound :: SimState s a -> SimTrace a -> SimTrace a
1560
+ traceFinalRacesFound simstate@ SimState { control0 = control } =
1561
+ TraceRacesFound [extendScheduleControl control m | m <- scheduleMods]
1562
+ where SimState { races } =
1563
+ quiescentRacesInSimState simstate
1564
+ scheduleMods =
1565
+ concatMap stepInfoToScheduleMods $ completeRaces races
1554
1566
1555
1567
-- Extend an existing schedule control with a newly discovered schedule mod
1556
1568
extendScheduleControl' :: ScheduleControl -> ScheduleMod -> ScheduleControl
0 commit comments