Test.DPOR.Schedule

Scheduling for concurrent computations.

Scheduling

type Scheduler tid action lookahead s = [(Decision tid, action)] -> Maybe (tid, action) -> NonEmpty (tid, lookahead) -> s -> (Maybe tid, s)

A Scheduler drives the execution of a concurrent program. The parameters it takes are:

1. The trace so far.
2. The last thread executed (if this is the first invocation, this is Nothing).
3. The runnable threads at this point.
4. The state.

It returns a thread to execute, or Nothing if execution should abort here, and also a new state.

data Decision tid

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.

Constructors

Start tid

Start a new thread, because the last was blocked (or it's the start of computation).

Continue

Continue running the last thread for another step.

SwitchTo tid

Pre-empt the running thread, and switch to another.

Instances

Eq tid => Eq (Decision tid)

Show tid => Show (Decision tid)

NFData tid => NFData (Decision tid)

tidOf :: tid -> Decision tid -> tid

Get the resultant thread identifier of a Decision, with a default case for Continue.

decisionOf

Arguments

:: (Eq tid, Foldable f)

=> Maybe tid

The prior thread.

-> f tid

The runnable threads.

-> tid

The current thread.

-> Decision tid

Get the Decision that would have resulted in this thread identifier, given a prior thread (if any) and list of runnable threads.

data NonEmpty a :: * -> *

Constructors

a :| [a] infixr 5

Instances

Monad NonEmpty

Functor NonEmpty

MonadFix NonEmpty

Applicative NonEmpty

Foldable NonEmpty

Traversable NonEmpty

Generic1 NonEmpty

MonadZip NonEmpty

IsList (NonEmpty a)

Eq a => Eq (NonEmpty a)

Data a => Data (NonEmpty a)

Ord a => Ord (NonEmpty a)

Read a => Read (NonEmpty a)

Show a => Show (NonEmpty a)

Generic (NonEmpty a)

NFData a => NFData (NonEmpty a)

Hashable a => Hashable (NonEmpty a)

type Rep1 NonEmpty = D1 D1NonEmpty (C1 C1_0NonEmpty ((:*:) (S1 NoSelector Par1) (S1 NoSelector (Rec1 []))))

type Rep (NonEmpty a) = D1 D1NonEmpty (C1 C1_0NonEmpty ((:*:) (S1 NoSelector (Rec0 a)) (S1 NoSelector (Rec0 [a]))))

type Item (NonEmpty a) = a

Preemptive

randomSched :: RandomGen g => Scheduler tid action lookahead g

A simple random scheduler which, at every step, picks a random thread to run.

roundRobinSched :: Ord tid => Scheduler tid action lookahead ()

A round-robin scheduler which, at every step, schedules the thread with the next ThreadId.

Non-preemptive

randomSchedNP :: (RandomGen g, Eq tid) => Scheduler tid action lookahead g

A random scheduler which doesn't preempt the running thread. That is, if the last thread scheduled is still runnable, run that, otherwise schedule randomly.

roundRobinSchedNP :: Ord tid => Scheduler tid action lookahead ()

A round-robin scheduler which doesn't preempt the running thread.

Utilities

makeNonPreemptive :: Eq tid => Scheduler tid action lookahead s -> Scheduler tid action lookahead s

Turn a potentially preemptive scheduler into a non-preemptive one.