mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-18 19:11:37 +03:00
Use a non-empty list type for scheduler threads
This commit is contained in:
parent
bf91775629
commit
ff015054f4
@ -37,6 +37,16 @@ data Fixed c n r t = F
|
||||
-- type.
|
||||
}
|
||||
|
||||
-- | The type of non-empty lists.
|
||||
data NonEmpty a = a :| [a] deriving (Eq, Ord, Read, Show)
|
||||
|
||||
instance Functor NonEmpty where
|
||||
fmap f (a :| as) = f a :| map f as
|
||||
|
||||
-- | Convert a 'NonEmpty' to a regular non-empty list.
|
||||
toList :: NonEmpty a -> [a]
|
||||
toList (a :| as) = a : as
|
||||
|
||||
-- * Running @Conc@ monads
|
||||
|
||||
-- | Scheduling is done in terms of a trace of 'Action's. Blocking can
|
||||
@ -61,14 +71,13 @@ type ThreadId = Int
|
||||
|
||||
-- | A @Scheduler@ maintains some internal state, @s@, takes the
|
||||
-- 'ThreadId' of the last thread scheduled, and the list of runnable
|
||||
-- threads (which will never be empty). It produces a 'ThreadId' to
|
||||
-- schedule, and a new state.
|
||||
-- threads. It produces a 'ThreadId' to schedule, and a new state.
|
||||
--
|
||||
-- Note: In order to prevent deadlock, the 'Conc' runtime will assume
|
||||
-- that a deadlock situation has arisen if the scheduler attempts to
|
||||
-- (a) schedule a blocked thread, or (b) schedule a nonexistant
|
||||
-- thread. In either of those cases, the computation will be halted.
|
||||
type Scheduler s = s -> ThreadId -> [ThreadId] -> (ThreadId, s)
|
||||
type Scheduler s = s -> ThreadId -> NonEmpty ThreadId -> (ThreadId, s)
|
||||
|
||||
-- | One of the outputs of the runner is a @Trace@, which is just a
|
||||
-- log of threads and actions they have taken.
|
||||
@ -154,7 +163,8 @@ runThreads fixed sofar prior sched s threads ref
|
||||
runThreads fixed sofar' chosen sched s' threads' ref
|
||||
|
||||
where
|
||||
(chosen, s') = if prior == -1 then (0, s) else sched s prior $ M.keys runnable
|
||||
(chosen, s') = if prior == -1 then (0, s) else sched s prior $ head runnable' :| tail runnable'
|
||||
runnable' = M.keys runnable
|
||||
runnable = M.filter (not . snd) threads
|
||||
thread = M.lookup chosen threads
|
||||
isBlocked = snd $ fromJust thread
|
||||
|
@ -3,6 +3,7 @@ module Control.Monad.Conc.Fixed.Schedulers
|
||||
( -- * Types
|
||||
Scheduler
|
||||
, ThreadId
|
||||
, NonEmpty(..)
|
||||
-- * Pre-emptive
|
||||
, randomSched
|
||||
, roundRobinSched
|
||||
@ -11,6 +12,7 @@ module Control.Monad.Conc.Fixed.Schedulers
|
||||
, roundRobinSchedNP
|
||||
-- * Utilities
|
||||
, makeNP
|
||||
, toList
|
||||
) where
|
||||
|
||||
import Control.Monad.Conc.Fixed.Internal
|
||||
@ -19,8 +21,9 @@ import System.Random (RandomGen, randomR)
|
||||
-- | A simple random scheduler which, at every step, picks a random
|
||||
-- thread to run.
|
||||
randomSched :: RandomGen g => Scheduler g
|
||||
randomSched g _ threads = (threads !! choice, g') where
|
||||
(choice, g') = randomR (0, length threads - 1) g
|
||||
randomSched g _ threads = (threads' !! choice, g') where
|
||||
(choice, g') = randomR (0, length threads' - 1) g
|
||||
threads' = toList threads
|
||||
|
||||
-- | A random scheduler which doesn't pre-empt the running
|
||||
-- thread. That is, if the last thread scheduled is still runnable,
|
||||
@ -32,8 +35,11 @@ randomSchedNP = makeNP randomSched
|
||||
-- thread with the next 'ThreadId'.
|
||||
roundRobinSched :: Scheduler ()
|
||||
roundRobinSched _ prior threads
|
||||
| prior >= maximum threads = (minimum threads, ())
|
||||
| otherwise = (minimum $ filter (>prior) threads, ())
|
||||
| prior >= maximum threads' = (minimum threads', ())
|
||||
| otherwise = (minimum $ filter (>prior) threads', ())
|
||||
|
||||
where
|
||||
threads' = toList threads
|
||||
|
||||
-- | A round-robin scheduler which doesn't pre-empt the running
|
||||
-- thread.
|
||||
@ -45,5 +51,5 @@ roundRobinSchedNP = makeNP roundRobinSched
|
||||
makeNP :: Scheduler s -> Scheduler s
|
||||
makeNP sched = newsched where
|
||||
newsched s prior threads
|
||||
| prior `elem` threads = (prior, s)
|
||||
| prior `elem` toList threads = (prior, s)
|
||||
| otherwise = sched s prior threads
|
||||
|
@ -81,13 +81,15 @@ makeSCT :: Scheduler s -> SCTScheduler s
|
||||
makeSCT sched (s, trace) prior threads = (tid, (s', (decision, alters) : trace)) where
|
||||
(tid, s') = sched s prior threads
|
||||
|
||||
decision | tid == prior = Continue
|
||||
| prior `elem` threads = SwitchTo tid
|
||||
| otherwise = Start tid
|
||||
decision | tid == prior = Continue
|
||||
| prior `elem` threads' = SwitchTo tid
|
||||
| otherwise = Start tid
|
||||
|
||||
alters | 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
|
||||
alters | 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'
|
||||
|
||||
threads' = toList threads
|
||||
|
||||
-- | Pretty-print a scheduler trace.
|
||||
showTrace :: SchedTrace -> String
|
||||
|
@ -85,21 +85,23 @@ pbInitialG = P { _pc = 0, _next = Empty, _halt = False }
|
||||
-- decisions to drive the initial trace, returning the generated
|
||||
-- suffix.
|
||||
pbSched :: SCTScheduler PBSched
|
||||
pbSched (s, trc) prior threads@(next:_) = case _decisions s of
|
||||
pbSched (s, trc) prior threads@(next:|_) = case _decisions s of
|
||||
-- If we have a decision queued, make it.
|
||||
(Start t:ds) -> let trc' = (Start t, alters t) in (t, (s { _decisions = ds, _prefix = trc' : _prefix s}, trc':trc))
|
||||
(Continue:ds) -> let trc' = (Continue, alters prior) in (prior, (s { _decisions = ds, _prefix = trc' : _prefix s}, trc':trc))
|
||||
(SwitchTo t:ds) -> let trc' = (SwitchTo t, alters t) in (t, (s { _decisions = ds, _prefix = trc' : _prefix s}, trc':trc))
|
||||
|
||||
-- Otherwise just use a non-pre-emptive scheduler.
|
||||
[] | prior `elem` threads -> let trc' = (Continue, alters prior) in (prior, (s { _suffix = trc' : _suffix s}, trc':trc))
|
||||
| otherwise -> let trc' = (Start next, alters next) in (next, (s { _suffix = trc' : _suffix s}, trc':trc))
|
||||
[] | prior `elem` threads' -> let trc' = (Continue, alters prior) in (prior, (s { _suffix = trc' : _suffix s}, trc':trc))
|
||||
| otherwise -> let trc' = (Start next, alters next) in (next, (s { _suffix = trc' : _suffix s}, 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
|
||||
| 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'
|
||||
|
||||
threads' = toList threads
|
||||
|
||||
-- | Pre-emption bounding termination function: terminates on attempt
|
||||
-- to start a PB above the limit.
|
||||
|
Loading…
Reference in New Issue
Block a user