@@ -130,7 +130,7 @@ happensBeforeStep step step' =
130
130
(getVectorClock $ stepVClock step')
131
131
132
132
labelledTVarId :: TVar s a -> ST s (Labelled TVarId )
133
- labelledTVarId TVar { tvarId, tvarLabel } = ( Labelled tvarId) <$> readSTRef tvarLabel
133
+ labelledTVarId TVar { tvarId, tvarLabel } = Labelled tvarId <$> readSTRef tvarLabel
134
134
135
135
labelledThreads :: Map ThreadId (Thread s a ) -> [Labelled ThreadId ]
136
136
labelledThreads threadMap =
@@ -892,7 +892,7 @@ removeMinimums = \psq ->
892
892
893
893
traceMany :: [(Time , ThreadId , Maybe ThreadLabel , SimEventType )]
894
894
-> SimTrace a -> SimTrace a
895
- traceMany [] trace = trace
895
+ traceMany [] trace = trace
896
896
traceMany ((time, tid, tlbl, event): ts) trace =
897
897
SimTrace time tid tlbl event (traceMany ts trace)
898
898
@@ -910,7 +910,10 @@ runSimTraceST mainAction = controlSimTraceST Nothing ControlDefault mainAction
910
910
911
911
controlSimTraceST :: Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a )
912
912
controlSimTraceST limit control mainAction =
913
- schedule mainThread initialState{ control = control, control0 = control, perStepTimeLimit = limit }
913
+ schedule mainThread initialState { control = control,
914
+ control0 = control,
915
+ perStepTimeLimit = limit
916
+ }
914
917
where
915
918
mainThread =
916
919
Thread {
@@ -1242,7 +1245,7 @@ someTvarId :: SomeTVar s -> TVarId
1242
1245
someTvarId (SomeTVar r) = tvarId r
1243
1246
1244
1247
onlyReadEffect :: Effect -> Bool
1245
- onlyReadEffect e@ Effect { effectReads } = e == mempty { effectReads }
1248
+ onlyReadEffect e = e { effectReads = effectReads mempty } == mempty
1246
1249
1247
1250
racingEffects :: Effect -> Effect -> Bool
1248
1251
racingEffects e e' =
@@ -1267,11 +1270,13 @@ data Step = Step {
1267
1270
deriving Show
1268
1271
1269
1272
-- steps race if they can be reordered with a possibly different outcome
1270
- racingSteps :: Step -> Step -> Bool
1273
+ racingSteps :: Step -- ^ an earlier step
1274
+ -> Step -- ^ a later step
1275
+ -> Bool
1271
1276
racingSteps s s' =
1272
1277
stepThreadId s /= stepThreadId s'
1273
1278
&& not (stepThreadId s' `elem` effectWakeup (stepEffect s))
1274
- && (racingEffects ( stepEffect s) ( stepEffect s')
1279
+ && (stepEffect s `racingEffects` stepEffect s'
1275
1280
|| throwsTo s s'
1276
1281
|| throwsTo s' s)
1277
1282
where throwsTo s1 s2 =
@@ -1333,6 +1338,9 @@ updateRacesInSimState thread SimState{ control, threads, races } =
1333
1338
(Map. keysSet (Map. filter (not . threadDone) threads))
1334
1339
races
1335
1340
1341
+ -- | 'updateRaces' turns a current 'Step' into 'StepInfo', and updates all
1342
+ -- 'activeRaces'.
1343
+ --
1336
1344
-- We take care that steps can only race against threads in their
1337
1345
-- concurrent set. When this becomes empty, a step can be retired into
1338
1346
-- the "complete" category, but only if there are some steps racing
@@ -1343,9 +1351,13 @@ updateRaces newStep@Step{ stepThreadId = tid, stepEffect = newEffect }
1343
1351
control
1344
1352
newConcurrent0
1345
1353
races@ Races { activeRaces } =
1346
- let -- a new step cannot race with any threads that it just woke up
1347
- newConcurrent = foldr Set. delete newConcurrent0 (effectWakeup newEffect)
1348
- new | isTestThreadId tid = [] -- test threads do not race
1354
+
1355
+ let justBlocking :: Bool
1356
+ justBlocking = blocking && onlyReadEffect newEffect
1357
+
1358
+ -- a new step cannot race with any threads that it just woke up
1359
+ new :: [StepInfo ]
1360
+ new | isTestThreadId tid = [] -- test threads do not race
1349
1361
| Set. null newConcurrent = [] -- cannot race with anything
1350
1362
| justBlocking = [] -- no need to defer a blocking transaction
1351
1363
| otherwise =
@@ -1355,14 +1367,18 @@ updateRaces newStep@Step{ stepThreadId = tid, stepEffect = newEffect }
1355
1367
stepInfoNonDep = [] ,
1356
1368
stepInfoRaces = []
1357
1369
}]
1358
- justBlocking = blocking && onlyReadEffect newEffect
1359
- updateActive =
1370
+ where
1371
+ newConcurrent :: Set ThreadId
1372
+ newConcurrent = foldr Set. delete newConcurrent0 (effectWakeup newEffect)
1373
+
1374
+ activeRaces' :: [StepInfo ]
1375
+ activeRaces' =
1360
1376
[ -- if this step depends on the previous step, or is not concurrent,
1361
1377
-- then any threads that it wakes up become non-concurrent also.
1362
1378
let lessConcurrent = foldr Set. delete concurrent (effectWakeup newEffect) in
1363
1379
if tid `elem` concurrent then
1364
1380
let theseStepsRace = not (isTestThreadId tid) && racingSteps step newStep
1365
- happensBefore = happensBeforeStep step newStep
1381
+ happensBefore = step `happensBeforeStep` newStep
1366
1382
nondep' | happensBefore = nondep
1367
1383
| otherwise = newStep : nondep
1368
1384
-- We will only record the first race with each thread---reversing
@@ -1378,18 +1394,22 @@ updateRaces newStep@Step{ stepThreadId = tid, stepEffect = newEffect }
1378
1394
control == ControlFollow [] [] ) &&
1379
1395
theseStepsRace = newStep : stepRaces
1380
1396
| otherwise = stepRaces
1381
- in stepInfo { stepInfoConcurrent = effectForks newEffect `Set.union` concurrent',
1397
+
1398
+ in stepInfo { stepInfoConcurrent = effectForks newEffect
1399
+ `Set.union` concurrent',
1382
1400
stepInfoNonDep = nondep',
1383
1401
stepInfoRaces = stepRaces'
1384
1402
}
1403
+
1385
1404
else stepInfo { stepInfoConcurrent = lessConcurrent }
1405
+
1386
1406
| stepInfo@ StepInfo { stepInfoStep = step,
1387
1407
stepInfoConcurrent = concurrent,
1388
1408
stepInfoNonDep = nondep,
1389
1409
stepInfoRaces = stepRaces
1390
1410
}
1391
1411
<- activeRaces ]
1392
- in normalizeRaces $ races { activeRaces = new ++ updateActive }
1412
+ in normalizeRaces $ races { activeRaces = new ++ activeRaces' }
1393
1413
1394
1414
-- When a thread terminates, we remove it from the concurrent thread
1395
1415
-- sets of active races.
@@ -1420,10 +1440,10 @@ quiescentRacesInSimState simstate@SimState{ races } =
1420
1440
quiescentRaces :: Races -> Races
1421
1441
quiescentRaces Races { activeRaces, completeRaces } =
1422
1442
Races { activeRaces = [] ,
1423
- completeRaces = [s{stepInfoConcurrent = Set. empty} |
1424
- s <- activeRaces,
1425
- not (null (stepInfoRaces s))] ++
1426
- completeRaces }
1443
+ completeRaces = [ s{stepInfoConcurrent = Set. empty}
1444
+ | s <- activeRaces
1445
+ , not (null (stepInfoRaces s))
1446
+ ] ++ completeRaces }
1427
1447
1428
1448
traceRaces :: Races -> Races
1429
1449
traceRaces r = r
@@ -1448,15 +1468,18 @@ stepInfoToScheduleMods
1448
1468
-- It is actually possible for a later step that races with an earlier one
1449
1469
-- not to *depend* on it in a happens-before sense. But we don't want to try
1450
1470
-- to follow any steps *after* the later one.
1451
- [ ScheduleMod (stepStepId step)
1452
- control
1453
- (takeWhile (/= stepStepId step')
1454
- (map stepStepId (reverse nondep))
1455
- ++ [stepStepId step'])
1456
- -- It should be unnecessary to include the delayed step in the insertion,
1457
- -- since the default scheduling should run it anyway. Removing it may
1458
- -- help avoid redundant schedules.
1459
- -- ++ [stepStepId step])
1471
+ [ ScheduleMod
1472
+ { scheduleModTarget = stepStepId step
1473
+ , scheduleModControl = control
1474
+ , scheduleModInsertion = takeWhile (/= stepStepId step')
1475
+ (map stepStepId (reverse nondep))
1476
+ ++ [stepStepId step']
1477
+ -- It should be unnecessary to include the delayed
1478
+ -- step in the insertion, since the default
1479
+ -- scheduling should run it anyway. Removing it may
1480
+ -- help avoid redundant schedules.
1481
+ -- ++ [stepStepId step]
1482
+ }
1460
1483
| step' <- races ]
1461
1484
1462
1485
traceFinalRacesFound :: SimState s a -> SimTrace a -> SimTrace a
@@ -1502,10 +1525,8 @@ advanceControl stepId c =
1502
1525
c
1503
1526
1504
1527
followControl :: ScheduleControl -> ScheduleControl
1505
- followControl (ControlAwait
1506
- (ScheduleMod {scheduleModTarget,
1507
- scheduleModInsertion} : mods)) =
1508
- ControlFollow scheduleModInsertion mods
1528
+ followControl (ControlAwait (ScheduleMod { scheduleModInsertion } : mods)) =
1529
+ ControlFollow scheduleModInsertion mods
1509
1530
followControl (ControlAwait [] ) = error " Impossible: followControl (ControlAwait [])"
1510
1531
followControl ControlDefault {} = error " Impossible: followControl ControlDefault{}"
1511
1532
followControl ControlFollow {} = error " Impossible: followControl ControlFollow{}"
0 commit comments