Skip to content

Commit 9b47268

Browse files
cootcoot
committed
io-sim-por: refactor updateRaces
1 parent 606ed50 commit 9b47268

File tree

1 file changed

+107
-127
lines changed

1 file changed

+107
-127
lines changed

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

Lines changed: 107 additions & 127 deletions
Original file line numberDiff line numberDiff line change
@@ -378,7 +378,7 @@ schedule thread@Thread{
378378
-- We record a step, in case there is no exception handler on replay.
379379
let (thread', eff) = stepThread thread0
380380
control' = advanceControl (threadStepId thread0) control
381-
races' = updateRacesInSimState thread0 simstate
381+
races' = updateRaces thread0 simstate
382382
trace <- schedule thread' simstate{ races = races',
383383
control = control',
384384
timers = timers'' }
@@ -826,12 +826,13 @@ deschedule Yield thread@Thread { threadId = tid,
826826
let (thread', eff) = stepThread thread
827827
runqueue' = insertThread thread' runqueue
828828
threads' = Map.insert tid thread' threads
829-
control' = advanceControl (threadStepId thread) control in
829+
control' = advanceControl (threadStepId thread) control
830+
races' = updateRaces thread simstate in
830831

831832
SimPORTrace time tid tstep tlbl (EventEffect vClock eff) <$>
832833
reschedule simstate { runqueue = runqueue',
833834
threads = threads',
834-
races = updateRacesInSimState thread simstate,
835+
races = races',
835836
control = control' }
836837

837838
deschedule Interruptable thread@Thread {
@@ -875,11 +876,12 @@ deschedule Interruptable thread@Thread{threadId = tid,
875876
-- Either masked or unmasked but no pending async exceptions.
876877
-- Either way, just carry on.
877878
-- Record a step, though, in case on replay there is an async exception.
878-
let (thread', eff) = stepThread thread in
879+
let (thread', eff) = stepThread thread
880+
races' = updateRaces thread simstate in
879881

880882
SimPORTrace time tid tstep tlbl (EventEffect vClock eff) <$>
881883
schedule thread'
882-
simstate{ races = updateRacesInSimState thread simstate,
884+
simstate{ races = races',
883885
control = advanceControl (threadStepId thread) control }
884886

885887
deschedule (Blocked _blockedReason) thread@Thread { threadId = tid
@@ -902,11 +904,12 @@ deschedule (Blocked blockedReason) thread@Thread{ threadId = tid,
902904
control } =
903905
let thread1 = thread { threadStatus = ThreadBlocked blockedReason }
904906
(thread', eff) = stepThread thread1
905-
threads' = Map.insert (threadId thread') thread' threads in
907+
threads' = Map.insert (threadId thread') thread' threads
908+
races' = updateRaces thread1 simstate in
906909

907910
SimPORTrace time tid tstep tlbl (EventEffect vClock eff) <$>
908911
reschedule simstate { threads = threads',
909-
races = updateRacesInSimState thread1 simstate,
912+
races = races',
910913
control = advanceControl (threadStepId thread1) control }
911914

912915
deschedule Terminated thread@Thread { threadId = tid, threadLabel = tlbl, threadVClock = vClock, threadEffect = effect }
@@ -920,10 +923,10 @@ deschedule Terminated thread@Thread { threadId = tid, threadLabel = tlbl, thread
920923
simstate'@SimState{threads}) =
921924
unblockThreads False vClock wakeup simstate
922925
threads' = Map.insert tid thread' threads
926+
races' = threadTerminatesRaces tid $ updateRaces thread1 simstate
923927
-- We must keep terminated threads in the state to preserve their vector clocks,
924928
-- which matters when other threads throwTo them.
925-
!trace <- reschedule simstate' { races = threadTerminatesRaces tid $
926-
updateRacesInSimState thread1 simstate,
929+
!trace <- reschedule simstate' { races = races',
927930
control = advanceControl (threadStepId thread) control,
928931
threads = threads' }
929932
return $ traceMany
@@ -1741,125 +1744,108 @@ data Races = Races { -- These steps may still race with future steps
17411744
noRaces :: Races
17421745
noRaces = Races [] []
17431746

1744-
updateRacesInSimState :: Thread s a -> SimState s a -> Races
1745-
updateRacesInSimState thread SimState{ control, threads, races } =
1746-
debugTraceRaces $
1747-
updateRaces step
1748-
(isThreadBlocked thread)
1749-
control
1750-
(Map.keysSet (Map.filter (\t -> not (isThreadDone t)
1751-
&& threadId t `Set.notMember`
1752-
effectForks (stepEffect step)
1753-
) threads))
1754-
races
1755-
where
1756-
step = currentStep thread
1757-
17581747
-- | 'updateRaces' turns a current 'Step' into 'StepInfo', and updates all
17591748
-- 'activeRaces'.
17601749
--
17611750
-- We take care that steps can only race against threads in their
17621751
-- concurrent set. When this becomes empty, a step can be retired into
17631752
-- the "complete" category, but only if there are some steps racing
17641753
-- with it.
1765-
updateRaces :: Step
1766-
-- ^ executed step
1767-
-> Bool
1768-
-- ^ is the thread blocking
1769-
-> ScheduleControl
1770-
-- ^ schedule control
1771-
-> Set ThreadId
1772-
-- ^ set of runnable threads which are not forked by the step, and
1773-
-- thus can race with it.
1774-
-> Races -> Races
1775-
updateRaces newStep@Step{ stepThreadId = tid, stepEffect = newEffect }
1776-
blocking
1777-
control
1778-
concurrent0
1779-
races@Races{ activeRaces } =
1780-
1781-
let -- A new step to add to the `activeRaces` list.
1782-
newStepInfo :: Maybe StepInfo
1783-
!newStepInfo | isNotRacyThreadId tid = Nothing
1784-
-- non-racy threads do not race
1785-
1786-
| Set.null concurrent = Nothing
1787-
-- cannot race with nothing
1788-
1789-
| isBlocking = Nothing
1790-
-- no need to defer a blocking transaction
1791-
1792-
| otherwise =
1793-
Just $! StepInfo { stepInfoStep = newStep,
1794-
stepInfoControl = control,
1795-
stepInfoConcurrent = concurrent,
1796-
stepInfoNonDep = [],
1797-
stepInfoRaces = []
1798-
}
1799-
where
1800-
concurrent :: Set ThreadId
1801-
concurrent = foldr Set.delete concurrent0 (effectWakeup newEffect)
1802-
1803-
isBlocking :: Bool
1804-
isBlocking = blocking && onlyReadEffect newEffect
1805-
1806-
-- Used to update each `StepInfo` in `activeRaces`.
1807-
updateStepInfo :: StepInfo -> StepInfo
1808-
updateStepInfo stepInfo@StepInfo { stepInfoStep = step,
1809-
stepInfoConcurrent = concurrent,
1810-
stepInfoNonDep,
1811-
stepInfoRaces } =
1812-
-- if this step depends on the previous step, or is not concurrent,
1813-
-- then any threads that it wakes up become non-concurrent also.
1814-
let !lessConcurrent = foldr Set.delete concurrent (effectWakeup newEffect) in
1815-
1816-
if tid `notElem` concurrent
1817-
then stepInfo { stepInfoConcurrent = lessConcurrent }
1818-
1819-
-- The core of IOSimPOR. Detect if `newStep` is racing with any
1820-
-- previous steps and update each `StepInfo`.
1821-
else let theseStepsRace = step `racingSteps` newStep
1822-
-- `step` happened before `newStep` (`newStep` happened after
1823-
-- `step`)
1824-
happensBefore = step `happensBeforeStep` newStep
1825-
1826-
-- We will only record the first race with each thread.
1827-
-- Reversing the first race makes the next race detectable.
1828-
-- Thus we remove a thread from the concurrent set after the
1829-
-- first race.
1830-
!concurrent'
1831-
| happensBefore = Set.delete tid lessConcurrent
1832-
| theseStepsRace = Set.delete tid concurrent
1833-
| otherwise = concurrent
1834-
1835-
!stepInfoNonDep'
1836-
-- `newStep` happened after `step`
1837-
| happensBefore = stepInfoNonDep
1838-
-- `newStep` did not happen after `step`
1839-
| otherwise = newStep : stepInfoNonDep
1840-
1841-
-- Here we record discovered races. We only record a new
1842-
-- race if we are following the default schedule, to avoid
1843-
-- finding the same race in different parts of the search
1844-
-- space.
1845-
!stepInfoRaces'
1846-
| theseStepsRace && isDefaultSchedule control
1847-
= newStep : stepInfoRaces
1848-
| otherwise = stepInfoRaces
1849-
1850-
in stepInfo { stepInfoConcurrent = effectForks newEffect
1851-
`Set.union` concurrent',
1852-
stepInfoNonDep = stepInfoNonDep',
1853-
stepInfoRaces = stepInfoRaces'
1854-
}
1855-
1856-
activeRaces' :: [StepInfo]
1857-
!activeRaces' =
1858-
case newStepInfo of
1859-
Nothing -> updateStepInfo <$> activeRaces
1860-
Just si -> si : (updateStepInfo <$> activeRaces)
1861-
1862-
in normalizeRaces races { activeRaces = activeRaces' }
1754+
updateRaces :: Thread s a -> SimState s a -> Races
1755+
updateRaces thread@Thread { threadId = tid }
1756+
SimState{ control, threads, races = races@Races { activeRaces } } =
1757+
let
1758+
newStep@Step{ stepEffect = newEffect } = currentStep thread
1759+
1760+
concurrent0 =
1761+
Map.keysSet (Map.filter (\t -> not (isThreadDone t)
1762+
&& threadId t `Set.notMember`
1763+
effectForks (stepEffect newStep)
1764+
) threads)
1765+
1766+
-- A new step to add to the `activeRaces` list.
1767+
newStepInfo :: Maybe StepInfo
1768+
!newStepInfo | isNotRacyThreadId tid = Nothing
1769+
-- non-racy threads do not race
1770+
1771+
| Set.null concurrent = Nothing
1772+
-- cannot race with nothing
1773+
1774+
| isBlocking = Nothing
1775+
-- no need to defer a blocking transaction
1776+
1777+
| otherwise =
1778+
Just $! StepInfo { stepInfoStep = newStep,
1779+
stepInfoControl = control,
1780+
stepInfoConcurrent = concurrent,
1781+
stepInfoNonDep = [],
1782+
stepInfoRaces = []
1783+
}
1784+
where
1785+
concurrent :: Set ThreadId
1786+
concurrent = foldr Set.delete concurrent0 (effectWakeup newEffect)
1787+
1788+
isBlocking :: Bool
1789+
isBlocking = isThreadBlocked thread && onlyReadEffect newEffect
1790+
1791+
-- Used to update each `StepInfo` in `activeRaces`.
1792+
updateStepInfo :: StepInfo -> StepInfo
1793+
updateStepInfo stepInfo@StepInfo { stepInfoStep = step,
1794+
stepInfoConcurrent = concurrent,
1795+
stepInfoNonDep,
1796+
stepInfoRaces } =
1797+
-- if this step depends on the previous step, or is not concurrent,
1798+
-- then any threads that it wakes up become non-concurrent also.
1799+
let !lessConcurrent = foldr Set.delete concurrent (effectWakeup newEffect) in
1800+
1801+
if tid `notElem` concurrent
1802+
then stepInfo { stepInfoConcurrent = lessConcurrent }
1803+
1804+
-- The core of IOSimPOR. Detect if `newStep` is racing with any
1805+
-- previous steps and update each `StepInfo`.
1806+
else let theseStepsRace = step `racingSteps` newStep
1807+
-- `step` happened before `newStep` (`newStep` happened after
1808+
-- `step`)
1809+
happensBefore = step `happensBeforeStep` newStep
1810+
1811+
-- We will only record the first race with each thread.
1812+
-- Reversing the first race makes the next race detectable.
1813+
-- Thus we remove a thread from the concurrent set after the
1814+
-- first race.
1815+
!concurrent'
1816+
| happensBefore = Set.delete tid lessConcurrent
1817+
| theseStepsRace = Set.delete tid concurrent
1818+
| otherwise = concurrent
1819+
1820+
!stepInfoNonDep'
1821+
-- `newStep` happened after `step`
1822+
| happensBefore = stepInfoNonDep
1823+
-- `newStep` did not happen after `step`
1824+
| otherwise = newStep : stepInfoNonDep
1825+
1826+
-- Here we record discovered races. We only record a new
1827+
-- race if we are following the default schedule, to avoid
1828+
-- finding the same race in different parts of the search
1829+
-- space.
1830+
!stepInfoRaces'
1831+
| theseStepsRace && isDefaultSchedule control
1832+
= newStep : stepInfoRaces
1833+
| otherwise = stepInfoRaces
1834+
1835+
in stepInfo { stepInfoConcurrent = effectForks newEffect
1836+
`Set.union` concurrent',
1837+
stepInfoNonDep = stepInfoNonDep',
1838+
stepInfoRaces = stepInfoRaces'
1839+
}
1840+
1841+
activeRaces' :: [StepInfo]
1842+
!activeRaces' =
1843+
case newStepInfo of
1844+
Nothing -> updateStepInfo <$> activeRaces
1845+
Just si -> si : (updateStepInfo <$> activeRaces)
1846+
1847+
in normalizeRaces races { activeRaces = activeRaces' }
1848+
18631849

18641850
normalizeRaces :: Races -> Races
18651851
normalizeRaces Races{ activeRaces, completeRaces } =
@@ -1893,12 +1879,6 @@ quiescentRaces Races{ activeRaces, completeRaces } =
18931879
, not (null (stepInfoRaces s))
18941880
] ++ completeRaces }
18951881

1896-
-- for debugging purposes
1897-
debugTraceRaces :: Races -> Races
1898-
debugTraceRaces r = r
1899-
-- debugTraceRaces r@Races{activeRaces,completeRaces} =
1900-
-- Debug.trace ("Tracking "++show (length (concatMap stepInfoRaces activeRaces)) ++" races") r
1901-
19021882

19031883
--
19041884
-- Schedule control

0 commit comments

Comments
 (0)