@@ -115,8 +115,9 @@ bottomVClock = VectorClock Map.empty
115
115
insertVClock :: ThreadId -> Int -> VectorClock -> VectorClock
116
116
insertVClock tid ! step (VectorClock m) = VectorClock (Map. insert tid step m)
117
117
118
- lubVClock :: VectorClock -> VectorClock -> VectorClock
119
- lubVClock (VectorClock m) (VectorClock m') = VectorClock (Map. unionWith max m m')
118
+ leastUpperBoundVClock :: VectorClock -> VectorClock -> VectorClock
119
+ leastUpperBoundVClock (VectorClock m) (VectorClock m') =
120
+ VectorClock (Map. unionWith max m m')
120
121
121
122
-- hbfVClock :: VectorClock -> VectorClock -> Bool
122
123
-- hbfVClock (VectorClock m) (VectorClock m') = Map.isSubmapOfBy (<=) m m'
@@ -480,8 +481,8 @@ schedule thread@Thread{
480
481
StmTxCommitted x read written nextVid' -> do
481
482
(wakeup, wokeby) <- threadsUnblockedByWrites written
482
483
mapM_ (\ (SomeTVar tvar) -> unblockAllThreadsFromTVar tvar) written
483
- vClockRead <- lubTVarVClocks read
484
- let vClock' = vClock `lubVClock ` vClockRead
484
+ vClockRead <- leastUpperBoundTVarVClocks read
485
+ let vClock' = vClock `leastUpperBoundVClock ` vClockRead
485
486
effect' = effect
486
487
<> readEffects read
487
488
<> writeEffects written
@@ -491,9 +492,9 @@ schedule thread@Thread{
491
492
threadEffect = effect' }
492
493
(unblocked,
493
494
simstate') = unblockThreads vClock' wakeup simstate
494
- sequence_ [ modifySTRef (tvarVClock r) (lubVClock vClock') | SomeTVar r <- written ]
495
+ sequence_ [ modifySTRef (tvarVClock r) (leastUpperBoundVClock vClock') | SomeTVar r <- written ]
495
496
vids <- traverse (\ (SomeTVar tvar) -> labelledTVarId tvar) written
496
- -- We deschedule a thread after a transaction... another may have woken up.
497
+ -- We deschedule a thread after a transaction... another may have woken up.
497
498
trace <- deschedule Yield thread' simstate' { nextVid = nextVid' }
498
499
return $
499
500
SimTrace time tid tlbl (EventTxCommitted vids [nextVid.. pred nextVid']) $
@@ -506,20 +507,20 @@ schedule thread@Thread{
506
507
507
508
StmTxAborted read e -> do
508
509
-- schedule this thread to immediately raise the exception
509
- vClockRead <- lubTVarVClocks read
510
+ vClockRead <- leastUpperBoundTVarVClocks read
510
511
let effect' = effect <> readEffects read
511
512
thread' = thread { threadControl = ThreadControl (Throw e) ctl,
512
- threadVClock = vClock `lubVClock ` vClockRead,
513
+ threadVClock = vClock `leastUpperBoundVClock ` vClockRead,
513
514
threadEffect = effect' }
514
515
trace <- schedule thread' simstate
515
516
return $ SimTrace time tid tlbl EventTxAborted trace
516
517
517
518
StmTxBlocked read -> do
518
519
mapM_ (\ (SomeTVar tvar) -> blockThreadOnTVar tid tvar) read
519
520
vids <- traverse (\ (SomeTVar tvar) -> labelledTVarId tvar) read
520
- vClockRead <- lubTVarVClocks read
521
+ vClockRead <- leastUpperBoundTVarVClocks read
521
522
let effect' = effect <> readEffects read
522
- thread' = thread { threadVClock = vClock `lubVClock ` vClockRead,
523
+ thread' = thread { threadVClock = vClock `leastUpperBoundVClock ` vClockRead,
523
524
threadEffect = effect' }
524
525
trace <- deschedule Blocked thread' simstate
525
526
return $ SimTrace time tid tlbl (EventTxBlocked vids) trace
@@ -568,7 +569,7 @@ schedule thread@Thread{
568
569
ThrowTo e tid' k -> do
569
570
let thread' = thread { threadControl = ThreadControl k ctl,
570
571
threadEffect = effect <> throwToEffect tid' <> wakeUpEffect,
571
- threadVClock = vClock `lubVClock ` vClockTgt }
572
+ threadVClock = vClock `leastUpperBoundVClock ` vClockTgt }
572
573
(vClockTgt,
573
574
wakeUpEffect,
574
575
willBlock) = (threadVClock t,
@@ -601,7 +602,7 @@ schedule thread@Thread{
601
602
t { threadControl = ThreadControl (Throw e) ctl'
602
603
, threadBlocked = False
603
604
, threadMasking = MaskedInterruptible
604
- , threadVClock = vClock' `lubVClock ` vClock }
605
+ , threadVClock = vClock' `leastUpperBoundVClock ` vClock }
605
606
simstate'@ SimState { threads = threads' }
606
607
= snd (unblockThreads vClock [tid'] simstate)
607
608
threads'' = Map. adjust adjustTarget tid' threads'
@@ -657,7 +658,7 @@ deschedule Interruptable thread@Thread {
657
658
let thread' = thread { threadControl = ThreadControl (Throw e) ctl
658
659
, threadMasking = MaskedInterruptible
659
660
, threadThrowTo = etids
660
- , threadVClock = vClock `lubVClock ` vClock' }
661
+ , threadVClock = vClock `leastUpperBoundVClock ` vClock' }
661
662
(unblocked,
662
663
simstate') = unblockThreads vClock [l_labelled tid'] simstate
663
664
-- the thread is stepped when we Yield
@@ -828,7 +829,7 @@ unblockThreads vClock wakeup simstate@SimState {runqueue, threads} =
828
829
threads' = List. foldl'
829
830
(flip (Map. adjust
830
831
(\ t -> t { threadBlocked = False ,
831
- threadVClock = vClock `lubVClock ` threadVClock t })))
832
+ threadVClock = vClock `leastUpperBoundVClock ` threadVClock t })))
832
833
threads unblocked
833
834
834
835
@@ -1138,9 +1139,9 @@ commitTVar TVar{tvarUndo} = do
1138
1139
readTVarUndos :: TVar s a -> ST s [a ]
1139
1140
readTVarUndos TVar {tvarUndo} = readSTRef tvarUndo
1140
1141
1141
- lubTVarVClocks :: [SomeTVar s ] -> ST s VectorClock
1142
- lubTVarVClocks tvars =
1143
- foldr lubVClock bottomVClock <$>
1142
+ leastUpperBoundTVarVClocks :: [SomeTVar s ] -> ST s VectorClock
1143
+ leastUpperBoundTVarVClocks tvars =
1144
+ foldr leastUpperBoundVClock bottomVClock <$>
1144
1145
sequence [readSTRef (tvarVClock r) | SomeTVar r <- tvars]
1145
1146
1146
1147
--
0 commit comments