mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-30 09:07:16 +03:00
Consider pre-emptions around liftIOs in PB runner
This commit is contained in:
parent
9aee30ac57
commit
4efd3b5a25
@ -22,12 +22,12 @@ sctPreBound :: Int
|
|||||||
-- ^ The pre-emption bound. Anything < 0 will be
|
-- ^ The pre-emption bound. Anything < 0 will be
|
||||||
-- interpreted as 0.
|
-- interpreted as 0.
|
||||||
-> (forall t. Conc t a) -> [(Maybe a, SCTTrace)]
|
-> (forall t. Conc t a) -> [(Maybe a, SCTTrace)]
|
||||||
sctPreBound pb = runSCT' pbSched pbInitialS pbInitialG (pbTerm pb') (pbStep pb') where
|
sctPreBound pb = runSCT' pbSched pbInitialS pbInitialG (pbTerm pb') (pbStep pb' False) where
|
||||||
pb' = if pb < 0 then 0 else pb
|
pb' = if pb < 0 then 0 else pb
|
||||||
|
|
||||||
-- | Variant of 'sctPreBound' using 'IO'. See usual caveats about IO.
|
-- | Variant of 'sctPreBound' using 'IO'. See usual caveats about IO.
|
||||||
sctPreBoundIO :: Int -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
|
sctPreBoundIO :: Int -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
|
||||||
sctPreBoundIO pb = runSCTIO' pbSched pbInitialS pbInitialG (pbTerm pb') (pbStep pb') where
|
sctPreBoundIO pb = runSCTIO' pbSched pbInitialS pbInitialG (pbTerm pb') (pbStep pb' True) where
|
||||||
pb' = if pb < 0 then 0 else pb
|
pb' = if pb < 0 then 0 else pb
|
||||||
|
|
||||||
-- * Utils
|
-- * Utils
|
||||||
@ -104,8 +104,12 @@ pbTerm pb _ g = (_pc g == pb + 1) || _halt g
|
|||||||
-- count. Testing with a very concurrent problem (finding a deadlock
|
-- count. Testing with a very concurrent problem (finding a deadlock
|
||||||
-- in 100 dining philosophers) has revealed this may work better in
|
-- in 100 dining philosophers) has revealed this may work better in
|
||||||
-- practice.
|
-- practice.
|
||||||
pbStep :: Int -> (a, SchedTrace, SchedTrace) -> PreBoundState -> SCTTrace -> (([Decision], SchedTrace, SchedTrace), PreBoundState)
|
pbStep :: Int
|
||||||
pbStep pb (_, rPref, rSuff) g t = case _next g of
|
-- ^ Pre-emption bound.
|
||||||
|
-> Bool
|
||||||
|
-- ^ Whether to consider pre-emptions around lifts.
|
||||||
|
-> (a, SchedTrace, SchedTrace) -> PreBoundState -> SCTTrace -> (([Decision], SchedTrace, SchedTrace), PreBoundState)
|
||||||
|
pbStep pb lifts (_, rPref, rSuff) g t = case _next g of
|
||||||
-- We have schedules remaining, so run the next
|
-- We have schedules remaining, so run the next
|
||||||
Lazy (x:xs) rest -> (s' x, g { _next = nextPB +| thisPB +| xs +| rest })
|
Lazy (x:xs) rest -> (s' x, g { _next = nextPB +| thisPB +| xs +| rest })
|
||||||
|
|
||||||
@ -138,7 +142,7 @@ pbStep pb (_, rPref, rSuff) g t = case _next g of
|
|||||||
|
|
||||||
-- | All schedules we get from the current one with ONE extra
|
-- | All schedules we get from the current one with ONE extra
|
||||||
-- pre-emption.
|
-- pre-emption.
|
||||||
nextPB = [ pref' y | y <- offspring suff']
|
nextPB = [ pref' y | y <- offspring lifts suff']
|
||||||
|
|
||||||
-- * Utils (Internal)
|
-- * Utils (Internal)
|
||||||
|
|
||||||
@ -152,21 +156,22 @@ siblings [] = []
|
|||||||
|
|
||||||
-- | Return all modifications to this schedule which do introduce an
|
-- | Return all modifications to this schedule which do introduce an
|
||||||
-- extra pre-emption. Only introduce pre-emptions around CVar actions.
|
-- extra pre-emption. Only introduce pre-emptions around CVar actions.
|
||||||
offspring :: SCTTrace -> [[Decision]]
|
offspring :: Bool -> SCTTrace -> [[Decision]]
|
||||||
offspring ((Continue, alts, ta):ds)
|
offspring lifts ((Continue, alts, ta):ds)
|
||||||
| preCand ta = [Continue : n | n <- offspring ds, not $ null n] ++ [[n] | n <- alts]
|
| preCand lifts ta = [Continue : n | n <- offspring lifts ds, not $ null n] ++ [[n] | n <- alts]
|
||||||
| preCand ta = [Continue : n | n <- offspring ds, not $ null n]
|
| otherwise = [Continue : n | n <- offspring lifts ds, not $ null n]
|
||||||
offspring ((d, _, _):ds) = [d : n | n <- offspring ds]
|
offspring lifts ((d, _, _):ds) = [d : n | n <- offspring lifts ds]
|
||||||
offspring [] = []
|
offspring _ [] = []
|
||||||
|
|
||||||
-- | Check if a 'ThreadAction' is a candidate for pre-emption.
|
-- | Check if a 'ThreadAction' is a candidate for pre-emption.
|
||||||
preCand :: ThreadAction -> Bool
|
preCand :: Bool -> ThreadAction -> Bool
|
||||||
preCand (Put _) = True
|
preCand _ (Put _) = True
|
||||||
preCand (TryPut _ _) = True
|
preCand _ (TryPut _ _) = True
|
||||||
preCand (Take _) = True
|
preCand _ (Take _) = True
|
||||||
preCand (TryTake _ _) = True
|
preCand _ (TryTake _ _) = True
|
||||||
preCand BlockedPut = True
|
preCand _ BlockedPut = True
|
||||||
preCand Read = True
|
preCand _ Read = True
|
||||||
preCand BlockedRead = True
|
preCand _ BlockedRead = True
|
||||||
preCand BlockedTake = True
|
preCand _ BlockedTake = True
|
||||||
preCand _ = False
|
preCand b Lift = b
|
||||||
|
preCand _ _ = False
|
||||||
|
Loading…
Reference in New Issue
Block a user