mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-18 19:11:37 +03:00
Vastly improve PB runner
This commit is contained in:
Michael Walker
parent
c0ac24773e
commit
981169c25f
@ -56,115 +56,13 @@ module Control.Monad.Conc.SCT
|
||||
-- * Utilities
|
||||
, toSCT
|
||||
, showTrace
|
||||
, ordNub
|
||||
) where
|
||||
|
||||
import Control.Monad.Conc.Fixed
|
||||
import Control.Monad.Conc.SCT.Internal
|
||||
import Control.Monad.Conc.SCT.PreBound
|
||||
import System.Random (RandomGen)
|
||||
|
||||
import qualified Control.Monad.Conc.Fixed.IO as CIO
|
||||
import qualified Data.Set as Set
|
||||
|
||||
-- * Types
|
||||
|
||||
-- | An @SCTScheduler@ is like a regular 'Scheduler', except it builds
|
||||
-- a trace of scheduling decisions made.
|
||||
--
|
||||
-- Note that the 'SchedTrace' is built in *reverse*, this is more
|
||||
-- efficient than appending to the list every time.
|
||||
type SCTScheduler s = Scheduler (s, SchedTrace)
|
||||
|
||||
-- | A @SchedTrace@ is just a list of all the decisions that were made,
|
||||
-- with the alternative decisions that could have been made at each
|
||||
-- step.
|
||||
type SchedTrace = [(Decision, [Decision])]
|
||||
|
||||
-- | A @SCTTrace@ is a combined 'SchedTrace' and 'Trace'.
|
||||
type SCTTrace = [(Decision, [Decision], ThreadAction)]
|
||||
|
||||
-- | Scheduling decisions are based on the state of the running
|
||||
-- program, and so we can capture some of that state in recording what
|
||||
-- specific decision we made.
|
||||
data Decision =
|
||||
Start ThreadId
|
||||
-- ^ Start a new thread, because the last was blocked (or it's the
|
||||
-- initial thread).
|
||||
| Continue
|
||||
-- ^ Continue running the last thread for another step.
|
||||
| SwitchTo ThreadId
|
||||
-- ^ Pre-empt the running thread, and switch to another.
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
-- * SCT Runners
|
||||
|
||||
-- | Run a concurrent program under a given scheduler a number of
|
||||
-- times, collecting the results and the scheduling that gave rise to
|
||||
-- them.
|
||||
--
|
||||
-- The initial state for each run is the final state of the last run,
|
||||
-- so it is important that the scheduler actually maintain some
|
||||
-- internal state, or all the results will be identical.
|
||||
runSCT :: SCTScheduler s -> s -> Int -> (forall t. Conc t a) -> [(Maybe a, SCTTrace)]
|
||||
runSCT sched s n = runSCT' sched s n term step where
|
||||
term _ g = g == 0
|
||||
step s' g _ = (s', g - 1)
|
||||
|
||||
-- | A varant of 'runSCT' for concurrent programs that do 'IO'.
|
||||
--
|
||||
-- Warning! The IO will be executed lots of times, in lots of
|
||||
-- interleavings! Be very confident that nothing in a 'liftIO' can
|
||||
-- block on the action of another thread, or you risk deadlocking this
|
||||
-- function!
|
||||
runSCTIO :: SCTScheduler s -> s -> Int -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
|
||||
runSCTIO sched s n = runSCTIO' sched s n term step where
|
||||
term _ g = g == 0
|
||||
step s' g _ = (s', g - 1)
|
||||
|
||||
-- | Run a concurrent program under a given scheduler, where the SCT
|
||||
-- runner itself maintains some internal state, and has a function to
|
||||
-- produce a new scheduler state for each run, and decide termination
|
||||
-- based on the internal state.
|
||||
--
|
||||
-- Note: the state step function takes the state returned by the
|
||||
-- scheduler, not the initial state!
|
||||
runSCT' :: SCTScheduler s -- ^ The scheduler
|
||||
-> s -- ^ The scheduler's initial satte
|
||||
-> g -- ^ The runner's initial state
|
||||
-> (s -> g -> Bool) -- ^ Termination decider
|
||||
-> (s -> g -> SCTTrace -> (s, g)) -- ^ State step function
|
||||
-> (forall t. Conc t a) -- ^ Conc program
|
||||
-> [(Maybe a, SCTTrace)]
|
||||
runSCT' sched s g term step c
|
||||
| term s g = []
|
||||
| otherwise = (res, trace) : rest where
|
||||
|
||||
(res, (s', strace), ttrace) = runConc' sched (s, [(Start 0, [])]) c
|
||||
|
||||
trace = reverse $ scttrace strace ttrace
|
||||
|
||||
(s'', g') = step s' g trace
|
||||
|
||||
rest = runSCT' sched s'' g' term step c
|
||||
|
||||
-- | A variant of runSCT' for concurrent programs that do IO.
|
||||
--
|
||||
-- Warning! The IO will be executed lots of times, in lots of
|
||||
-- interleavings! Be very confident that nothing in a 'liftIO' can
|
||||
-- block on the action of another thread, or you risk deadlocking this
|
||||
-- function!
|
||||
runSCTIO' :: SCTScheduler s -> s -> g -> (s -> g -> Bool) -> (s -> g -> SCTTrace -> (s, g)) -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
|
||||
runSCTIO' sched s g term step c
|
||||
| term s g = return []
|
||||
| otherwise = do
|
||||
(res, (s', strace), ttrace) <- CIO.runConc' sched (s, [(Start 0, [])]) c
|
||||
|
||||
let trace = reverse $ scttrace strace ttrace
|
||||
let (s'', g') = step s' g trace
|
||||
|
||||
rest <- runSCTIO' sched s'' g' term step c
|
||||
|
||||
return $ (res, trace) : rest
|
||||
|
||||
-- * Random Schedulers
|
||||
|
||||
-- | A simple pre-emptive random scheduler.
|
||||
@ -175,139 +73,6 @@ sctRandom = toSCT randomSched
|
||||
sctRandomNP :: RandomGen g => SCTScheduler g
|
||||
sctRandomNP = toSCT randomSchedNP
|
||||
|
||||
-- * Pre-emption bounding
|
||||
|
||||
data PreBoundState = P
|
||||
{ _pc :: Int
|
||||
-- ^ Current pre-emption count.
|
||||
, _next :: [[Decision]]
|
||||
-- ^ Schedules to try in this pc.
|
||||
, _done :: [SCTTrace]
|
||||
-- ^ Schedules completed in this pc.
|
||||
, _halt :: Bool
|
||||
-- ^ Indicates more schedules couldn't be found, and to halt
|
||||
-- immediately.
|
||||
}
|
||||
|
||||
-- | An SCT runner using a pre-emption bounding scheduler. Schedules
|
||||
-- will be explored systematically, starting with all
|
||||
-- pre-emption-count zero schedules, and gradually adding more
|
||||
-- pre-emptions.
|
||||
sctPreBound :: Int
|
||||
-- ^ The pre-emption bound. Anything < 0 will be
|
||||
-- interpreted as 0.
|
||||
-> (forall t. Conc t a) -> [(Maybe a, SCTTrace)]
|
||||
sctPreBound pb = runSCT' pbSched s g (pbTerm pb') (pbStep pb') where
|
||||
s = ([], [], [])
|
||||
g = P { _pc = 0, _next = [], _done = [], _halt = False }
|
||||
pb' = if pb < 0 then 0 else pb
|
||||
|
||||
-- | Variant of 'sctPreBound' using 'IO'. See usual caveats about IO.
|
||||
sctPreBoundIO :: Int -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
|
||||
sctPreBoundIO pb = runSCTIO' pbSched s g (pbTerm pb') (pbStep pb') where
|
||||
s = ([], [], [])
|
||||
g = P { _pc = 0, _next = [], _done = [], _halt = False }
|
||||
pb' = if pb < 0 then 0 else pb
|
||||
|
||||
-- | Pre-emption bounding scheduler, which uses a queue of scheduling
|
||||
-- decisions to drive the initial trace, returning the generated
|
||||
-- suffix.
|
||||
pbSched :: SCTScheduler ([Decision], SchedTrace, SchedTrace)
|
||||
pbSched ((d, pref, suff), trc) prior threads@(next:_) = case d of
|
||||
-- If we have a decision queued, make it.
|
||||
(Start t:ds) -> let trc' = (Start t, alters t) in (t, ((ds, trc':pref, suff), trc':trc))
|
||||
(Continue:ds) -> let trc' = (Continue, alters prior) in (prior, ((ds, trc':pref, suff), trc':trc))
|
||||
(SwitchTo t:ds) -> let trc' = (SwitchTo t, alters t) in (t, ((ds, trc':pref, suff), trc':trc))
|
||||
|
||||
-- Otherwise just use a non-pre-emptive scheduler.
|
||||
[] | prior `elem` threads -> let trc' = (Continue, alters prior) in (prior, (([], pref, trc':suff), trc':trc))
|
||||
| otherwise -> let trc' = (Start next, alters next) in (next, (([], pref, trc':suff), trc':trc))
|
||||
|
||||
where
|
||||
alters tid
|
||||
| tid == prior = map SwitchTo $ filter (/=prior) threads
|
||||
| prior `elem` threads = Continue : map SwitchTo (filter (\t -> t /= prior && t /= tid) threads)
|
||||
| otherwise = map Start $ filter (/=tid) threads
|
||||
|
||||
-- | Pre-emption bounding termination function: terminates on attempt
|
||||
-- to start a PB above the limit.
|
||||
pbTerm :: Int -> a -> PreBoundState -> Bool
|
||||
pbTerm pb _ g = (_pc g == pb + 1) || _halt g
|
||||
|
||||
-- | Pre-emption bounding state step function: computes remaining
|
||||
-- schedules to try and chooses one.
|
||||
pbStep :: Int -> (a, SchedTrace, SchedTrace) -> PreBoundState -> SCTTrace -> (([Decision], SchedTrace, SchedTrace), PreBoundState)
|
||||
pbStep pb (_, rPref, rSuff) g t = case _next g of
|
||||
-- We have schedules remaining in this PB, so run the next
|
||||
(x:xs) -> (s' x, g { _next = xs ++ thisPB, _done = done' })
|
||||
|
||||
-- We have no schedules remaining, try to generate some more.
|
||||
--
|
||||
-- If there are no more schedules in this PB, and this isn't the
|
||||
-- last PB, advance to the next.
|
||||
--
|
||||
-- If there are no schedules in the next PB, halt.
|
||||
[] ->
|
||||
case thisPB of
|
||||
(x:xs) -> (s' x, g { _next = xs, _done = done' })
|
||||
[] -> if _pc g == pb
|
||||
then halt
|
||||
else case nextPB of
|
||||
(x:xs) -> (s' x, g { _pc = pc', _next = xs, _done = [] })
|
||||
[] -> halt
|
||||
|
||||
where
|
||||
pref = reverse rPref
|
||||
suff = reverse rSuff
|
||||
|
||||
halt = (([], [], []), g { _halt = True })
|
||||
done' = if couldPre t then t : _done g else _done g
|
||||
pc' = _pc g + 1
|
||||
|
||||
s' ds = (tail ds, [], [])
|
||||
|
||||
pref' rest = if null pref then (\((d,_,_):_) -> d:rest) t else map fst pref ++ rest
|
||||
thisPB = [ pref' y | y <- others suff ]
|
||||
nextPB = [ y | y <- ordNub $ concatMap next done', preEmpCount y == pc' ]
|
||||
|
||||
-- | Return all modifications to this schedule which do not
|
||||
-- introduce extra pre-emptions.
|
||||
others ((Start i, alts):ds) = [Start i : o | o <- others ds, not $ null o] ++ [[a] | a <- alts]
|
||||
others ((SwitchTo i, alts):ds) = [SwitchTo i : o | o <- others ds, not $ null o] ++ [[a] | a <- alts]
|
||||
others ((d, _):ds) = [d : o | o <- others ds, not $ null o]
|
||||
others [] = []
|
||||
|
||||
-- | Return all modifications to this schedule which do introduce
|
||||
-- an extra pre-emption. Only introduce pre-emptions around CVar
|
||||
-- actions.
|
||||
next ((Continue, alts, ta):ds) = [Continue : n | n <- next ds] ++ if preCand ta then [[n] | n <- alts] else []
|
||||
next ((Start t, _, _):ds) = [Start t : n | n <- next ds]
|
||||
next ((SwitchTo t, _, _):ds) = [SwitchTo t : n | n <- next ds]
|
||||
next [] = []
|
||||
|
||||
-- | Check if a 'ThreadAction' is a candidate for pre-emption.
|
||||
preCand (Put _) = True
|
||||
preCand (TryPut _ _) = True
|
||||
preCand (Take _) = True
|
||||
preCand (TryTake _ _) = True
|
||||
preCand BlockedPut = True
|
||||
preCand Read = True
|
||||
preCand BlockedRead = True
|
||||
preCand BlockedTake = True
|
||||
preCand _ = False
|
||||
|
||||
-- | Check if a trace could be modified to have additional pre-emptions
|
||||
couldPre ((Continue, [], _):ds) = couldPre ds
|
||||
couldPre ((Continue, _, ta):ds) = preCand ta || couldPre ds
|
||||
couldPre (_:ds) = couldPre ds
|
||||
couldPre [] = False
|
||||
|
||||
-- | Check the pre-emption count of some scheduling decisions.
|
||||
preEmpCount :: [Decision] -> Int
|
||||
preEmpCount (SwitchTo _:ss) = 1 + preEmpCount ss
|
||||
preEmpCount (_:ss) = preEmpCount ss
|
||||
preEmpCount [] = 0
|
||||
|
||||
-- * Utils
|
||||
|
||||
-- | Convert a 'Scheduler' to an 'SCTScheduler' by recording the
|
||||
@ -333,16 +98,3 @@ showTrace = trace "" 0 . map fst where
|
||||
trace prefix num [] = thread prefix num
|
||||
|
||||
thread prefix num = prefix ++ replicate num '-'
|
||||
|
||||
-- | Zip a list of 'SchedTrace's and a 'Trace' together into an
|
||||
-- 'SCTTrace'.
|
||||
scttrace :: SchedTrace -> Trace -> SCTTrace
|
||||
scttrace = zipWith $ \(d, alts) (_, act) -> (d, alts, act)
|
||||
|
||||
-- | O(nlogn) nub, <https://github.com/nh2/haskell-ordnub>
|
||||
ordNub :: Ord a => [a] -> [a]
|
||||
ordNub = go Set.empty where
|
||||
go _ [] = []
|
||||
go s (x:xs)
|
||||
| x `Set.member` s = go s xs
|
||||
| otherwise = x : go (Set.insert x s) xs
|
||||
|
||||
116
Control/Monad/Conc/SCT/Internal.hs
Executable file
116
Control/Monad/Conc/SCT/Internal.hs
Executable file
@ -0,0 +1,116 @@
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
|
||||
-- | A runner for concurrent monads to systematically detect
|
||||
-- concurrency errors such as data races and deadlocks: internal definitions.
|
||||
module Control.Monad.Conc.SCT.Internal where
|
||||
|
||||
import Control.Monad.Conc.Fixed
|
||||
|
||||
import qualified Control.Monad.Conc.Fixed.IO as CIO
|
||||
|
||||
-- * Types
|
||||
|
||||
-- | An @SCTScheduler@ is like a regular 'Scheduler', except it builds
|
||||
-- a trace of scheduling decisions made.
|
||||
--
|
||||
-- Note that the 'SchedTrace' is built in *reverse*, this is more
|
||||
-- efficient than appending to the list every time.
|
||||
type SCTScheduler s = Scheduler (s, SchedTrace)
|
||||
|
||||
-- | A @SchedTrace@ is just a list of all the decisions that were made,
|
||||
-- with the alternative decisions that could have been made at each
|
||||
-- step.
|
||||
type SchedTrace = [(Decision, [Decision])]
|
||||
|
||||
-- | A @SCTTrace@ is a combined 'SchedTrace' and 'Trace'.
|
||||
type SCTTrace = [(Decision, [Decision], ThreadAction)]
|
||||
|
||||
-- | Scheduling decisions are based on the state of the running
|
||||
-- program, and so we can capture some of that state in recording what
|
||||
-- specific decision we made.
|
||||
data Decision =
|
||||
Start ThreadId
|
||||
-- ^ Start a new thread, because the last was blocked (or it's the
|
||||
-- initial thread).
|
||||
| Continue
|
||||
-- ^ Continue running the last thread for another step.
|
||||
| SwitchTo ThreadId
|
||||
-- ^ Pre-empt the running thread, and switch to another.
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
-- * SCT Runners
|
||||
|
||||
-- | Run a concurrent program under a given scheduler a number of
|
||||
-- times, collecting the results and the scheduling that gave rise to
|
||||
-- them.
|
||||
--
|
||||
-- The initial state for each run is the final state of the last run,
|
||||
-- so it is important that the scheduler actually maintain some
|
||||
-- internal state, or all the results will be identical.
|
||||
runSCT :: SCTScheduler s -> s -> Int -> (forall t. Conc t a) -> [(Maybe a, SCTTrace)]
|
||||
runSCT sched s n = runSCT' sched s n term step where
|
||||
term _ g = g == 0
|
||||
step s' g _ = (s', g - 1)
|
||||
|
||||
-- | A varant of 'runSCT' for concurrent programs that do 'IO'.
|
||||
--
|
||||
-- Warning! The IO will be executed lots of times, in lots of
|
||||
-- interleavings! Be very confident that nothing in a 'liftIO' can
|
||||
-- block on the action of another thread, or you risk deadlocking this
|
||||
-- function!
|
||||
runSCTIO :: SCTScheduler s -> s -> Int -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
|
||||
runSCTIO sched s n = runSCTIO' sched s n term step where
|
||||
term _ g = g == 0
|
||||
step s' g _ = (s', g - 1)
|
||||
|
||||
-- | Run a concurrent program under a given scheduler, where the SCT
|
||||
-- runner itself maintains some internal state, and has a function to
|
||||
-- produce a new scheduler state for each run, and decide termination
|
||||
-- based on the internal state.
|
||||
--
|
||||
-- Note: the state step function takes the state returned by the
|
||||
-- scheduler, not the initial state!
|
||||
runSCT' :: SCTScheduler s -- ^ The scheduler
|
||||
-> s -- ^ The scheduler's initial satte
|
||||
-> g -- ^ The runner's initial state
|
||||
-> (s -> g -> Bool) -- ^ Termination decider
|
||||
-> (s -> g -> SCTTrace -> (s, g)) -- ^ State step function
|
||||
-> (forall t. Conc t a) -- ^ Conc program
|
||||
-> [(Maybe a, SCTTrace)]
|
||||
runSCT' sched s g term step c
|
||||
| term s g = []
|
||||
| otherwise = (res, trace) : rest where
|
||||
|
||||
(res, (s', strace), ttrace) = runConc' sched (s, [(Start 0, [])]) c
|
||||
|
||||
trace = reverse $ scttrace strace ttrace
|
||||
|
||||
(s'', g') = step s' g trace
|
||||
|
||||
rest = runSCT' sched s'' g' term step c
|
||||
|
||||
-- | A variant of runSCT' for concurrent programs that do IO.
|
||||
--
|
||||
-- Warning! The IO will be executed lots of times, in lots of
|
||||
-- interleavings! Be very confident that nothing in a 'liftIO' can
|
||||
-- block on the action of another thread, or you risk deadlocking this
|
||||
-- function!
|
||||
runSCTIO' :: SCTScheduler s -> s -> g -> (s -> g -> Bool) -> (s -> g -> SCTTrace -> (s, g)) -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
|
||||
runSCTIO' sched s g term step c
|
||||
| term s g = return []
|
||||
| otherwise = do
|
||||
(res, (s', strace), ttrace) <- CIO.runConc' sched (s, [(Start 0, [])]) c
|
||||
|
||||
let trace = reverse $ scttrace strace ttrace
|
||||
let (s'', g') = step s' g trace
|
||||
|
||||
rest <- runSCTIO' sched s'' g' term step c
|
||||
|
||||
return $ (res, trace) : rest
|
||||
|
||||
-- * Utils (Internal)
|
||||
|
||||
-- | Zip a list of 'SchedTrace's and a 'Trace' together into an
|
||||
-- 'SCTTrace'.
|
||||
scttrace :: SchedTrace -> Trace -> SCTTrace
|
||||
scttrace = zipWith $ \(d, alts) (_, act) -> (d, alts, act)
|
||||
174
Control/Monad/Conc/SCT/PreBound.hs
Executable file
174
Control/Monad/Conc/SCT/PreBound.hs
Executable file
@ -0,0 +1,174 @@
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
|
||||
-- Pre-emption bounding SCT runner for Conc monads.
|
||||
module Control.Monad.Conc.SCT.PreBound
|
||||
( -- * SCT Runners
|
||||
sctPreBound
|
||||
, sctPreBoundIO
|
||||
-- * Utils
|
||||
, preEmpCount
|
||||
) where
|
||||
|
||||
import Control.Monad.Conc.Fixed
|
||||
import Control.Monad.Conc.SCT.Internal
|
||||
|
||||
import qualified Control.Monad.Conc.Fixed.IO as CIO
|
||||
|
||||
-- * SCT Runners
|
||||
|
||||
-- | An SCT runner using a pre-emption bounding scheduler. Schedules
|
||||
-- will be explored systematically, starting with all
|
||||
-- pre-emption-count zero schedules, and gradually adding more
|
||||
-- pre-emptions.
|
||||
sctPreBound :: Int
|
||||
-- ^ The pre-emption bound. Anything < 0 will be
|
||||
-- interpreted as 0.
|
||||
-> (forall t. Conc t a) -> [(Maybe a, SCTTrace)]
|
||||
sctPreBound pb = runSCT' pbSched pbInitialS pbInitialG (pbTerm pb') (pbStep pb') where
|
||||
pb' = if pb < 0 then 0 else pb
|
||||
|
||||
-- | Variant of 'sctPreBound' using 'IO'. See usual caveats about IO.
|
||||
sctPreBoundIO :: Int -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
|
||||
sctPreBoundIO pb = runSCTIO' pbSched pbInitialS pbInitialG (pbTerm pb') (pbStep pb') where
|
||||
pb' = if pb < 0 then 0 else pb
|
||||
|
||||
-- * Utils
|
||||
|
||||
-- | Check the pre-emption count of some scheduling decisions.
|
||||
preEmpCount :: [Decision] -> Int
|
||||
preEmpCount (SwitchTo _:ss) = 1 + preEmpCount ss
|
||||
preEmpCount (_:ss) = preEmpCount ss
|
||||
preEmpCount [] = 0
|
||||
|
||||
-- * State
|
||||
|
||||
-- | Data type representing a lazy, chunky, stream of data.
|
||||
data Lazy a = Lazy [a] (Lazy a) | Empty
|
||||
|
||||
-- | Prepend a value onto a lazy stream.
|
||||
(+|) :: [a] -> Lazy a -> Lazy a
|
||||
[] +| l = l
|
||||
xs +| l = Lazy xs l
|
||||
|
||||
infixr +|
|
||||
|
||||
data PreBoundState = P
|
||||
{ _pc :: Int
|
||||
-- ^ Current pre-emption count.
|
||||
, _next :: Lazy [Decision]
|
||||
-- ^ Schedules to try.
|
||||
, _halt :: Bool
|
||||
-- ^ Indicates more schedules couldn't be found, and to halt
|
||||
-- immediately.
|
||||
}
|
||||
|
||||
-- | Initial scheduler state for the PB scheduler.
|
||||
pbInitialS :: ([Decision], SchedTrace, SchedTrace)
|
||||
pbInitialS = ([], [], [])
|
||||
|
||||
-- | Initial runner state for the PB scheduler.
|
||||
pbInitialG :: PreBoundState
|
||||
pbInitialG = P { _pc = 0, _next = Empty, _halt = False }
|
||||
|
||||
-- * PB Scheduler
|
||||
|
||||
-- | Pre-emption bounding scheduler, which uses a queue of scheduling
|
||||
-- decisions to drive the initial trace, returning the generated
|
||||
-- suffix.
|
||||
pbSched :: SCTScheduler ([Decision], SchedTrace, SchedTrace)
|
||||
pbSched ((d, pref, suff), trc) prior threads@(next:_) = case d of
|
||||
-- If we have a decision queued, make it.
|
||||
(Start t:ds) -> let trc' = (Start t, alters t) in (t, ((ds, trc':pref, suff), trc':trc))
|
||||
(Continue:ds) -> let trc' = (Continue, alters prior) in (prior, ((ds, trc':pref, suff), trc':trc))
|
||||
(SwitchTo t:ds) -> let trc' = (SwitchTo t, alters t) in (t, ((ds, trc':pref, suff), trc':trc))
|
||||
|
||||
-- Otherwise just use a non-pre-emptive scheduler.
|
||||
[] | prior `elem` threads -> let trc' = (Continue, alters prior) in (prior, (([], pref, trc':suff), trc':trc))
|
||||
| otherwise -> let trc' = (Start next, alters next) in (next, (([], pref, trc':suff), trc':trc))
|
||||
|
||||
where
|
||||
alters tid
|
||||
| tid == prior = map SwitchTo $ filter (/=prior) threads
|
||||
| prior `elem` threads = Continue : map SwitchTo (filter (\t -> t /= prior && t /= tid) threads)
|
||||
| otherwise = map Start $ filter (/=tid) threads
|
||||
|
||||
-- | Pre-emption bounding termination function: terminates on attempt
|
||||
-- to start a PB above the limit.
|
||||
pbTerm :: Int -> a -> PreBoundState -> Bool
|
||||
pbTerm pb _ g = (_pc g == pb + 1) || _halt g
|
||||
|
||||
-- | Pre-emption bounding state step function: computes remaining
|
||||
-- schedules to try and chooses one.
|
||||
--
|
||||
-- This effectively produces schedules in a depth-first order, rather
|
||||
-- than breadth-first. This means it will explore some schedules with
|
||||
-- a higher pre-emption count before all the ones with a lower
|
||||
-- count. Testing with a very concurrent problem (finding a deadlock
|
||||
-- in 100 dining philosophers) has revealed this may work better in
|
||||
-- practice.
|
||||
pbStep :: Int -> (a, SchedTrace, SchedTrace) -> PreBoundState -> SCTTrace -> (([Decision], SchedTrace, SchedTrace), PreBoundState)
|
||||
pbStep pb (_, rPref, rSuff) g t = case _next g of
|
||||
-- We have schedules remaining, so run the next
|
||||
Lazy (x:xs) rest -> (s' x, g { _next = nextPB +| thisPB +| xs +| rest })
|
||||
|
||||
-- We have no schedules remaining, try to generate some more.
|
||||
--
|
||||
-- If there are no more schedules, halt.
|
||||
Empty ->
|
||||
case thisPB of
|
||||
(x:xs)
|
||||
| pb /= _pc g -> (s' x, g { _next = nextPB +| xs +| Empty })
|
||||
| pb == _pc g -> (s' x, g { _next = xs +| Empty })
|
||||
[] -> (s' [], g { _halt = True })
|
||||
|
||||
where
|
||||
-- The prefix and suffix are in reverse order, fix those.
|
||||
pref = reverse rPref
|
||||
suff = reverse rSuff
|
||||
|
||||
-- A prefix we can append decisions to, and a suffix with
|
||||
-- 'ThreadAction' information.
|
||||
pref' rest = if null pref then (\((d,_,_):_) -> d:rest) t else map fst pref ++ rest
|
||||
suff' = drop (length pref) t
|
||||
|
||||
-- | New scheduler state, with a given list of initial decisions.
|
||||
s' ds = (tail ds, [], [])
|
||||
|
||||
-- | All schedules we get from the current one WITHOUT introducing
|
||||
-- any pre-emptions.
|
||||
thisPB = [ pref' y | y <- siblings suff]
|
||||
|
||||
-- | All schedules we get from the current one with ONE extra
|
||||
-- pre-emption.
|
||||
nextPB = [ pref' y | y <- offspring suff']
|
||||
|
||||
-- * Utils (Internal)
|
||||
|
||||
-- | Return all modifications to this schedule which do not introduce
|
||||
-- extra pre-emptions.
|
||||
siblings :: SchedTrace -> [[Decision]]
|
||||
siblings ((Start i, alts):ds) = [Start i : o | o <- siblings ds, not $ null o] ++ [[a] | a <- alts]
|
||||
siblings ((SwitchTo i, alts):ds) = [SwitchTo i : o | o <- siblings ds, not $ null o] ++ [[a] | a <- alts]
|
||||
siblings ((d, _):ds) = [d : o | o <- siblings ds, not $ null o]
|
||||
siblings [] = []
|
||||
|
||||
-- | Return all modifications to this schedule which do introduce an
|
||||
-- extra pre-emption. Only introduce pre-emptions around CVar actions.
|
||||
offspring :: SCTTrace -> [[Decision]]
|
||||
offspring ((Continue, alts, ta):ds)
|
||||
| preCand ta = [Continue : n | n <- offspring ds, not $ null n] ++ [[n] | n <- alts]
|
||||
| preCand ta = [Continue : n | n <- offspring ds, not $ null n]
|
||||
offspring ((d, _, _):ds) = [d : n | n <- offspring ds]
|
||||
offspring [] = []
|
||||
|
||||
-- | Check if a 'ThreadAction' is a candidate for pre-emption.
|
||||
preCand :: ThreadAction -> Bool
|
||||
preCand (Put _) = True
|
||||
preCand (TryPut _ _) = True
|
||||
preCand (Take _) = True
|
||||
preCand (TryTake _ _) = True
|
||||
preCand BlockedPut = True
|
||||
preCand Read = True
|
||||
preCand BlockedRead = True
|
||||
preCand BlockedTake = True
|
||||
preCand _ = False
|
||||
@ -13,8 +13,8 @@ testCases =
|
||||
, Test "2 Philosophers" $ testNot "No deadlocks found!" $ testDeadlockFree 1 $ philosophers 2
|
||||
, Test "3 Philosophers" $ testNot "No deadlocks found!" $ testDeadlockFree 1 $ philosophers 3
|
||||
, Test "4 Philosophers" $ testNot "No deadlocks found!" $ testDeadlockFree 1 $ philosophers 4
|
||||
, Test "5 Philosophers" $ testNot "No deadlocks found!" $ testDeadlockFree 1 $ philosophers 5
|
||||
--, Test "100 Philosophers" $ testNot "No deadlocks found!" $ testDeadlockFree 2 $ philosophers 100
|
||||
, Test "25 Philosophers" $ testNot "No deadlocks found!" $ testDeadlockFree 1 $ philosophers 25
|
||||
, Test "100 Philosophers" $ testNot "No deadlocks found!" $ testDeadlockFree 2 $ philosophers 100
|
||||
, Test "Threshold Value" $ testNot "All values equal!" $ testAlwaysSame 1 thresholdValue
|
||||
, Test "Forgotten Unlock" $ testDeadlocks 1 forgottenUnlock
|
||||
, Test "Simple 2-Race" $ testNot "All values equal!" $ testAlwaysSame 1 simple2Race
|
||||
@ -122,4 +122,4 @@ raceyStack = do
|
||||
val <- pop s
|
||||
case val of
|
||||
Just x -> t2 s (n-1) (total+x)
|
||||
Nothing -> return Nothing
|
||||
Nothing -> return Nothing
|
||||
|
||||
@ -25,6 +25,8 @@ library
|
||||
, Control.Monad.Conc.Fixed.Schedulers
|
||||
, Control.Monad.Conc.SCT
|
||||
other-modules: Control.Monad.Conc.Fixed.Internal
|
||||
, Control.Monad.Conc.SCT.Internal
|
||||
, Control.Monad.Conc.SCT.PreBound
|
||||
-- other-extensions:
|
||||
build-depends: base >=4.6 && <5
|
||||
, containers
|
||||
|
||||
Loading…
Reference in New Issue
Block a user