-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A generic implementation of dynamic partial-order reduction (DPOR) for testing arbitrary models of concurrency.
--   
--   We can characterise the state of a concurrent computation by
--   considering the ordering of dependent events. This is a partial order:
--   independent events can be performed in any order without affecting the
--   result. DPOR is a technique for computing these partial orders at
--   run-time, and only testing one total order for each partial order.
--   This cuts down the amount of work to be done significantly. In
--   particular, this package implemented bounded partial-order reduction,
--   which is a further optimisation. Only schedules within some *bound*
--   are considered.
--   
--   <ul>
--   <li>DPOR with no schedule bounding is <b>complete</b>, it <i>will</i>
--   find all distinct executions!</li>
--   <li>DPOR with schedule bounding is <b>incomplete</b>, it will only
--   find all distinct executions <i>within the bound</i>!</li>
--   </ul>
--   
--   <b>Caution:</b> The fundamental assumption behind DPOR is that the
--   *only* source of nondeterminism in your program is the scheduler. Or,
--   to put it another way, if you execute the same program with the same
--   schedule twice, you get the same result. If you are using this library
--   in combination with something which performs I/O, be *very* certain
--   that this is the case!
--   
--   See the <a>README</a> for more details.
--   
--   For details on the algorithm, albeit presented in a very imperative
--   way, see <i>Bounded partial-order reduction</i>, K. Coons, M.
--   Musuvathi, and K. McKinley (2013), available at
--   <a>http://research.microsoft.com/pubs/202164/bpor-oopsla-2013.pdf</a>
@package dpor
@version 0.2.0.0


-- | Scheduling for concurrent computations.
module Test.DPOR.Schedule

-- | A <tt>Scheduler</tt> drives the execution of a concurrent program. The
--   parameters it takes are:
--   
--   <ol>
--   <li>The trace so far.</li>
--   <li>The last thread executed (if this is the first invocation, this is
--   <tt>Nothing</tt>).</li>
--   <li>The runnable threads at this point.</li>
--   <li>The state.</li>
--   </ol>
--   
--   It returns a thread to execute, or <tt>Nothing</tt> if execution
--   should abort here, and also a new state.
type Scheduler tid action lookahead s = [(Decision tid, action)] -> Maybe (tid, action) -> NonEmpty (tid, lookahead) -> s -> (Maybe tid, s)

-- | 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 tid

-- | Start a new thread, because the last was blocked (or it's the start of
--   computation).
Start :: tid -> Decision tid

-- | Continue running the last thread for another step.
Continue :: Decision tid

-- | Pre-empt the running thread, and switch to another.
SwitchTo :: tid -> Decision tid

-- | Get the resultant thread identifier of a <a>Decision</a>, with a
--   default case for <a>Continue</a>.
tidOf :: tid -> Decision tid -> tid

-- | Get the <a>Decision</a> that would have resulted in this thread
--   identifier, given a prior thread (if any) and list of runnable
--   threads.
decisionOf :: (Eq tid, Foldable f) => Maybe tid -> f tid -> tid -> Decision tid

-- | Non-empty (and non-strict) list type.
data NonEmpty a :: * -> *
(:|) :: a -> [a] -> NonEmpty a

-- | A simple random scheduler which, at every step, picks a random thread
--   to run.
randomSched :: RandomGen g => Scheduler tid action lookahead g

-- | A round-robin scheduler which, at every step, schedules the thread
--   with the next <tt>ThreadId</tt>.
roundRobinSched :: Ord tid => Scheduler tid action lookahead ()

-- | 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.
randomSchedNP :: (RandomGen g, Eq tid) => Scheduler tid action lookahead g

-- | A round-robin scheduler which doesn't preempt the running thread.
roundRobinSchedNP :: Ord tid => Scheduler tid action lookahead ()

-- | Turn a potentially preemptive scheduler into a non-preemptive one.
makeNonPreemptive :: Eq tid => Scheduler tid action lookahead s -> Scheduler tid action lookahead s
instance GHC.Show.Show tid => GHC.Show.Show (Test.DPOR.Schedule.Decision tid)
instance GHC.Classes.Eq tid => GHC.Classes.Eq (Test.DPOR.Schedule.Decision tid)
instance Control.DeepSeq.NFData tid => Control.DeepSeq.NFData (Test.DPOR.Schedule.Decision tid)


-- | Internal types and functions for dynamic partial-order reduction. This
--   module is NOT considered to form part of the public interface of this
--   library.
module Test.DPOR.Internal

-- | DPOR execution is represented as a tree of states, characterised by
--   the decisions that lead to that state.
data DPOR tid action
DPOR :: Set tid -> Map tid Bool -> Map tid (DPOR tid action) -> Map tid action -> Map tid action -> Maybe action -> DPOR tid action

-- | What threads are runnable at this step.
[dporRunnable] :: DPOR tid action -> Set tid

-- | Follow-on decisions still to make, and whether that decision was added
--   conservatively due to the bound.
[dporTodo] :: DPOR tid action -> Map tid Bool

-- | Follow-on decisions that have been made.
[dporDone] :: DPOR tid action -> Map tid (DPOR tid action)

-- | Transitions to ignore (in this node and children) until a dependent
--   transition happens.
[dporSleep] :: DPOR tid action -> Map tid action

-- | Transitions which have been taken, excluding conservatively-added
--   ones. This is used in implementing sleep sets.
[dporTaken] :: DPOR tid action -> Map tid action

-- | What happened at this step. This will be <a>Nothing</a> at the root,
--   <a>Just</a> everywhere else.
[dporAction] :: DPOR tid action -> Maybe action

-- | One step of the execution, including information for backtracking
--   purposes. This backtracking information is used to generate new
--   schedules.
data BacktrackStep tid action lookahead state
BacktrackStep :: tid -> (Decision tid, action) -> Map tid lookahead -> Map tid Bool -> state -> BacktrackStep tid action lookahead state

-- | The thread running at this step
[bcktThreadid] :: BacktrackStep tid action lookahead state -> tid

-- | What happened at this step.
[bcktDecision] :: BacktrackStep tid action lookahead state -> (Decision tid, action)

-- | The threads runnable at this step
[bcktRunnable] :: BacktrackStep tid action lookahead state -> Map tid lookahead

-- | The list of alternative threads to run, and whether those alternatives
--   were added conservatively due to the bound.
[bcktBacktracks] :: BacktrackStep tid action lookahead state -> Map tid Bool

-- | Some domain-specific state at this point.
[bcktState] :: BacktrackStep tid action lookahead state -> state

-- | Initial DPOR state, given an initial thread ID. This initial thread
--   should exist and be runnable at the start of execution.
initialState :: Ord tid => tid -> DPOR tid action

-- | Produce a new schedule prefix from a <tt>DPOR</tt> tree. If there are
--   no new prefixes remaining, return <a>Nothing</a>. Also returns whether
--   the decision was added conservatively, and the sleep set at the point
--   where divergence happens.
--   
--   A schedule prefix is a possibly empty sequence of decisions that have
--   already been made, terminated by a single decision from the to-do set.
--   The intent is to put the system into a new state when executed with
--   this initial sequence of scheduling decisions.
findSchedulePrefix :: Ord tid => (tid -> Bool) -> (Int -> (Int, g)) -> DPOR tid action -> Maybe ([tid], Bool, Map tid action, g)

-- | One of the outputs of the runner is a <tt>Trace</tt>, which is a log
--   of decisions made, all the runnable threads and what they would do,
--   and the action a thread took in its step.
type Trace tid action lookahead = [(Decision tid, [(tid, NonEmpty lookahead)], action)]

-- | Add a new trace to the tree, creating a new subtree branching off at
--   the point where the "to-do" decision was made.
incorporateTrace :: Ord tid => state -> (state -> (tid, action) -> state) -> (state -> (tid, action) -> (tid, action) -> Bool) -> Bool -> Trace tid action lookahead -> DPOR tid action -> DPOR tid action

-- | Produce a list of new backtracking points from an execution trace.
--   These are then used to inform new "to-do" points in the <tt>DPOR</tt>
--   tree.
--   
--   Two traces are passed in to this function: the first is generated from
--   the special DPOR scheduler, the other from the execution of the
--   concurrent program.
--   
--   If the trace ends with any threads other than the initial one still
--   runnable, a dependency is imposed between this final action and
--   everything else.
findBacktrackSteps :: Ord tid => s -> (s -> (tid, action) -> s) -> (s -> (tid, action) -> (tid, lookahead) -> Bool) -> ([BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s]) -> Bool -> Seq (NonEmpty (tid, lookahead), [tid]) -> Trace tid action lookahead -> [BacktrackStep tid action lookahead s]

-- | Add new backtracking points, if they have not already been visited,
--   fit into the bound, and aren't in the sleep set.
incorporateBacktrackSteps :: Ord tid => ([(Decision tid, action)] -> (Decision tid, lookahead) -> Bool) -> [BacktrackStep tid action lookahead s] -> DPOR tid action -> DPOR tid action

-- | A <tt>Scheduler</tt> where the state is a <tt>SchedState</tt>.
type DPORScheduler tid action lookahead s = Scheduler tid action lookahead (SchedState tid action lookahead s)

-- | The scheduler state
data SchedState tid action lookahead s
SchedState :: Map tid action -> [tid] -> Seq (NonEmpty (tid, lookahead), [tid]) -> Bool -> Bool -> s -> SchedState tid action lookahead s

-- | The sleep set: decisions not to make until something dependent with
--   them happens.
[schedSleep] :: SchedState tid action lookahead s -> Map tid action

-- | Decisions still to make
[schedPrefix] :: SchedState tid action lookahead s -> [tid]

-- | Which threads are runnable at each step, and the alternative decisions
--   still to make.
[schedBPoints] :: SchedState tid action lookahead s -> Seq (NonEmpty (tid, lookahead), [tid])

-- | Whether to ignore this execution or not: <tt>True</tt> if the
--   execution is aborted due to all possible decisions being in the sleep
--   set, as then everything in this execution is covered by another.
[schedIgnore] :: SchedState tid action lookahead s -> Bool

-- | Whether the execution was terminated due to all decisions being out of
--   bounds.
[schedBoundKill] :: SchedState tid action lookahead s -> Bool

-- | State used by the dependency function to determine when to remove
--   decisions from the sleep set.
[schedDepState] :: SchedState tid action lookahead s -> s

-- | Initial scheduler state for a given prefix
initialSchedState :: s -> Map tid action -> [tid] -> SchedState tid action lookahead s

-- | A bounding function takes the scheduling decisions so far and a
--   decision chosen to come next, and returns if that decision is within
--   the bound.
type BoundFunc tid action lookahead = [(Decision tid, action)] -> (Decision tid, lookahead) -> Bool

-- | The "true" bound, which allows everything.
trueBound :: BoundFunc tid action lookahead

-- | A backtracking step is a point in the execution where another decision
--   needs to be made, in order to explore interesting new schedules. A
--   backtracking <i>function</i> takes the steps identified so far and a
--   point and a thread to backtrack to, and inserts at least that
--   backtracking point. More may be added to compensate for the effects of
--   the bounding function. For example, under pre-emption bounding a
--   conservative backtracking point is added at the prior context switch.
--   
--   In general, a backtracking function should identify one or more
--   backtracking points, and then use <tt>backtrackAt</tt> to do the
--   actual work.
type BacktrackFunc tid action lookahead s = [BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s]

-- | Add a backtracking point. If the thread isn't runnable, add all
--   runnable threads. If the backtracking point is already present, don't
--   re-add it UNLESS this would make it conservative.
backtrackAt :: Ord tid => (BacktrackStep tid action lookahead s -> Bool) -> Bool -> BacktrackFunc tid action lookahead s

-- | DPOR scheduler: takes a list of decisions, and maintains a trace
--   including the runnable threads, and the alternative choices allowed by
--   the bound-specific initialise function.
--   
--   After the initial decisions are exhausted, this prefers choosing the
--   prior thread if it's (1) still runnable and (2) hasn't just yielded.
--   Furthermore, threads which <i>will</i> yield are ignored in preference
--   of those which will not.
--   
--   This forces full evaluation of the result every step, to avoid any
--   possible space leaks.
dporSched :: (Ord tid, NFData tid, NFData action, NFData lookahead, NFData s) => (action -> Bool) -> (lookahead -> Bool) -> (s -> (tid, action) -> (tid, action) -> Bool) -> (s -> (tid, lookahead) -> NonEmpty tid -> Bool) -> (s -> (tid, action) -> s) -> BoundFunc tid action lookahead -> DPORScheduler tid action lookahead s
initialDPORThread :: DPOR tid action -> tid

-- | Render a <a>DPOR</a> value as a graph in GraphViz "dot" format.
toDot :: (tid -> String) -> (action -> String) -> DPOR tid action -> String

-- | Render a <a>DPOR</a> value as a graph in GraphViz "dot" format, with a
--   function to determine if a subtree should be included or not.
toDotFiltered :: (tid -> DPOR tid action -> Bool) -> (tid -> String) -> (action -> String) -> DPOR tid action -> String

-- | Internal errors.
err :: String -> String -> a
instance (GHC.Show.Show s, GHC.Show.Show lookahead, GHC.Show.Show action, GHC.Show.Show tid) => GHC.Show.Show (Test.DPOR.Internal.SchedState tid action lookahead s)
instance (GHC.Show.Show state, GHC.Show.Show lookahead, GHC.Show.Show action, GHC.Show.Show tid) => GHC.Show.Show (Test.DPOR.Internal.BacktrackStep tid action lookahead state)
instance (Control.DeepSeq.NFData tid, Control.DeepSeq.NFData action, Control.DeepSeq.NFData lookahead, Control.DeepSeq.NFData s) => Control.DeepSeq.NFData (Test.DPOR.Internal.SchedState tid action lookahead s)
instance (Control.DeepSeq.NFData tid, Control.DeepSeq.NFData action, Control.DeepSeq.NFData lookahead, Control.DeepSeq.NFData state) => Control.DeepSeq.NFData (Test.DPOR.Internal.BacktrackStep tid action lookahead state)
instance (Control.DeepSeq.NFData tid, Control.DeepSeq.NFData action) => Control.DeepSeq.NFData (Test.DPOR.Internal.DPOR tid action)


-- | Random and incomplete techniques for when complete testing is
--   infeasible.
module Test.DPOR.Random

-- | Random dynamic partial-order reduction.
--   
--   This is the <tt>dpor</tt> algorithm in <a>Test.DPOR</a>, however it
--   does not promise to test every distinct schedule: instead, an
--   execution limit is passed in, and a PRNG used to decide which actual
--   schedules to test. Testing terminates when either the execution limit
--   is reached, or when there are no distinct schedules remaining.
--   
--   Despite being "random", this still uses the normal partial-order
--   reduction and schedule bounding machinery, and so will prune the
--   search space to "interesting" cases, and will never try the same
--   schedule twice. Additionally, the thread partitioning function still
--   applies when selecting schedules.
randomDPOR :: (Ord tid, NFData tid, NFData action, NFData lookahead, NFData s, Monad m, RandomGen g) => (action -> Bool) -> (lookahead -> Bool) -> s -> (s -> (tid, action) -> s) -> (s -> (tid, action) -> (tid, action) -> Bool) -> (s -> (tid, action) -> (tid, lookahead) -> Bool) -> (s -> (tid, lookahead) -> NonEmpty tid -> Bool) -> tid -> (tid -> Bool) -> BoundFunc tid action lookahead -> BacktrackFunc tid action lookahead s -> (DPOR tid action -> DPOR tid action) -> (DPORScheduler tid action lookahead s -> SchedState tid action lookahead s -> m (a, SchedState tid action lookahead s, Trace tid action lookahead)) -> g -> Int -> m [(a, Trace tid action lookahead)]

-- | Pure random scheduling. Like <a>randomDPOR</a> but all actions are
--   dependent and the bounds are optional.
boundedRandom :: (Ord tid, NFData tid, NFData action, NFData lookahead, Monad m, RandomGen g) => (action -> Bool) -> (lookahead -> Bool) -> tid -> Maybe (BoundFunc tid action lookahead) -> (DPORScheduler tid action lookahead () -> SchedState tid action lookahead () -> m (a, SchedState tid action lookahead (), Trace tid action lookahead)) -> g -> Int -> m [(a, Trace tid action lookahead)]


-- | Systematic testing of concurrent computations through dynamic
--   partial-order reduction and schedule bounding.
module Test.DPOR

-- | Dynamic partial-order reduction.
--   
--   This takes a lot of functional parameters because it's so generic, but
--   most are fairly simple.
--   
--   Some state may be maintained when determining backtracking points,
--   which can then inform the dependency functions. This state is not
--   preserved between different schedules, and built up from scratch each
--   time.
--   
--   The dependency functions must be consistent: if we can convert between
--   <tt>action</tt> and <tt>lookahead</tt>, and supply some sensible
--   default state, then (1) == true implies that (2) is. In practice, (1)
--   is the most specific and (2) will be more pessimistic (due to,
--   typically, less information being available when merely looking
--   ahead).
--   
--   The daemon-termination predicate returns <tt>True</tt> if the action
--   being looked at will cause the entire computation to terminate,
--   regardless of the other runnable threads (which are passed in the
--   <a>NonEmpty</a> list). Such actions will then be put off for as long
--   as possible. This allows supporting concurrency models with daemon
--   threads without doing something as drastic as imposing a dependency
--   between the program-terminating action and <i>everything</i> else.
dpor :: (Ord tid, NFData tid, NFData action, NFData lookahead, NFData s, Monad m) => (action -> Bool) -> (lookahead -> Bool) -> s -> (s -> (tid, action) -> s) -> (s -> (tid, action) -> (tid, action) -> Bool) -> (s -> (tid, action) -> (tid, lookahead) -> Bool) -> (s -> (tid, lookahead) -> NonEmpty tid -> Bool) -> tid -> (tid -> Bool) -> BoundFunc tid action lookahead -> BacktrackFunc tid action lookahead s -> (DPOR tid action -> DPOR tid action) -> (DPORScheduler tid action lookahead s -> SchedState tid action lookahead s -> m (a, SchedState tid action lookahead s, Trace tid action lookahead)) -> m [(a, Trace tid action lookahead)]

-- | A much simplified DPOR function: no state, no preference between
--   threads, and no post-processing between iterations.
simpleDPOR :: (Ord tid, NFData tid, NFData action, NFData lookahead, Monad m) => (action -> Bool) -> (lookahead -> Bool) -> ((tid, action) -> (tid, action) -> Bool) -> ((tid, action) -> (tid, lookahead) -> Bool) -> ((tid, lookahead) -> NonEmpty tid -> Bool) -> tid -> BoundFunc tid action lookahead -> BacktrackFunc tid action lookahead () -> (DPORScheduler tid action lookahead () -> SchedState tid action lookahead () -> m (a, SchedState tid action lookahead (), Trace tid action lookahead)) -> m [(a, Trace tid action lookahead)]

-- | DPOR execution is represented as a tree of states, characterised by
--   the decisions that lead to that state.
data DPOR tid action
DPOR :: Set tid -> Map tid Bool -> Map tid (DPOR tid action) -> Map tid action -> Map tid action -> Maybe action -> DPOR tid action

-- | What threads are runnable at this step.
[dporRunnable] :: DPOR tid action -> Set tid

-- | Follow-on decisions still to make, and whether that decision was added
--   conservatively due to the bound.
[dporTodo] :: DPOR tid action -> Map tid Bool

-- | Follow-on decisions that have been made.
[dporDone] :: DPOR tid action -> Map tid (DPOR tid action)

-- | Transitions to ignore (in this node and children) until a dependent
--   transition happens.
[dporSleep] :: DPOR tid action -> Map tid action

-- | Transitions which have been taken, excluding conservatively-added
--   ones. This is used in implementing sleep sets.
[dporTaken] :: DPOR tid action -> Map tid action

-- | What happened at this step. This will be <a>Nothing</a> at the root,
--   <a>Just</a> everywhere else.
[dporAction] :: DPOR tid action -> Maybe action

-- | A backtracking step is a point in the execution where another decision
--   needs to be made, in order to explore interesting new schedules. A
--   backtracking <i>function</i> takes the steps identified so far and a
--   point and a thread to backtrack to, and inserts at least that
--   backtracking point. More may be added to compensate for the effects of
--   the bounding function. For example, under pre-emption bounding a
--   conservative backtracking point is added at the prior context switch.
--   
--   In general, a backtracking function should identify one or more
--   backtracking points, and then use <tt>backtrackAt</tt> to do the
--   actual work.
type BacktrackFunc tid action lookahead s = [BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s]

-- | One step of the execution, including information for backtracking
--   purposes. This backtracking information is used to generate new
--   schedules.
data BacktrackStep tid action lookahead state
BacktrackStep :: tid -> (Decision tid, action) -> Map tid lookahead -> Map tid Bool -> state -> BacktrackStep tid action lookahead state

-- | The thread running at this step
[bcktThreadid] :: BacktrackStep tid action lookahead state -> tid

-- | What happened at this step.
[bcktDecision] :: BacktrackStep tid action lookahead state -> (Decision tid, action)

-- | The threads runnable at this step
[bcktRunnable] :: BacktrackStep tid action lookahead state -> Map tid lookahead

-- | The list of alternative threads to run, and whether those alternatives
--   were added conservatively due to the bound.
[bcktBacktracks] :: BacktrackStep tid action lookahead state -> Map tid Bool

-- | Some domain-specific state at this point.
[bcktState] :: BacktrackStep tid action lookahead state -> state

-- | Add a backtracking point. If the thread isn't runnable, add all
--   runnable threads. If the backtracking point is already present, don't
--   re-add it UNLESS this would make it conservative.
backtrackAt :: Ord tid => (BacktrackStep tid action lookahead s -> Bool) -> Bool -> BacktrackFunc tid action lookahead s

-- | A bounding function takes the scheduling decisions so far and a
--   decision chosen to come next, and returns if that decision is within
--   the bound.
type BoundFunc tid action lookahead = [(Decision tid, action)] -> (Decision tid, lookahead) -> Bool

-- | Combine two bounds into a larger bound, where both must be satisfied.
(&+&) :: BoundFunc tid action lookahead -> BoundFunc tid action lookahead -> BoundFunc tid action lookahead

-- | The "true" bound, which allows everything.
trueBound :: BoundFunc tid action lookahead
newtype PreemptionBound
PreemptionBound :: Int -> PreemptionBound

-- | A sensible default preemption bound: 2.
--   
--   See <i>Concurrency Testing Using Schedule Bounding: an Empirical
--   Study</i>, P. Thomson, A. F. Donaldson, A. Betts for justification.
defaultPreemptionBound :: PreemptionBound

-- | Preemption bound function
preempBound :: (action -> Bool) -> PreemptionBound -> BoundFunc tid action lookahead

-- | Add a backtrack point, and also conservatively add one prior to the
--   most recent transition before that point. This may result in the same
--   state being reached multiple times, but is needed because of the
--   artificial dependency imposed by the bound.
preempBacktrack :: Ord tid => (action -> Bool) -> BacktrackFunc tid action lookahead s

-- | Count the number of preemptions in a schedule prefix.
preempCount :: (action -> Bool) -> [(Decision tid, action)] -> (Decision tid, lookahead) -> Int
newtype FairBound
FairBound :: Int -> FairBound

-- | A sensible default fair bound: 5.
--   
--   This comes from playing around myself, but there is probably a better
--   default.
defaultFairBound :: FairBound

-- | Fair bound function
fairBound :: Eq tid => (action -> Bool) -> (lookahead -> Bool) -> (action -> [tid]) -> FairBound -> BoundFunc tid action lookahead

-- | Add a backtrack point. If the thread isn't runnable, or performs a
--   release operation, add all runnable threads.
fairBacktrack :: Ord tid => (lookahead -> Bool) -> BacktrackFunc tid action lookahead s

-- | Count the number of yields by a thread in a schedule prefix.
yieldCount :: Eq tid => (action -> Bool) -> (lookahead -> Bool) -> tid -> [(Decision tid, action)] -> (Decision tid, lookahead) -> Int

-- | Get the maximum difference between the yield counts of all threads in
--   this schedule prefix.
maxYieldCountDiff :: Eq tid => (action -> Bool) -> (lookahead -> Bool) -> (action -> [tid]) -> [(Decision tid, action)] -> (Decision tid, lookahead) -> Int
newtype LengthBound
LengthBound :: Int -> LengthBound

-- | A sensible default length bound: 250.
--   
--   Based on the assumption that anything which executes for much longer
--   (or even this long) will take ages to test.
defaultLengthBound :: LengthBound

-- | Length bound function
lenBound :: LengthBound -> BoundFunc tid action lookahead

-- | Add a backtrack point. If the thread isn't runnable, add all runnable
--   threads.
lenBacktrack :: Ord tid => BacktrackFunc tid action lookahead s

-- | A <tt>Scheduler</tt> where the state is a <tt>SchedState</tt>.
type DPORScheduler tid action lookahead s = Scheduler tid action lookahead (SchedState tid action lookahead s)

-- | The scheduler state
data SchedState tid action lookahead s

-- | One of the outputs of the runner is a <tt>Trace</tt>, which is a log
--   of decisions made, all the runnable threads and what they would do,
--   and the action a thread took in its step.
type Trace tid action lookahead = [(Decision tid, [(tid, NonEmpty lookahead)], action)]
instance GHC.Show.Show Test.DPOR.LengthBound
instance GHC.Read.Read Test.DPOR.LengthBound
instance GHC.Real.Integral Test.DPOR.LengthBound
instance GHC.Real.Real Test.DPOR.LengthBound
instance GHC.Num.Num Test.DPOR.LengthBound
instance GHC.Classes.Ord Test.DPOR.LengthBound
instance GHC.Classes.Eq Test.DPOR.LengthBound
instance GHC.Enum.Enum Test.DPOR.LengthBound
instance Control.DeepSeq.NFData Test.DPOR.LengthBound
instance GHC.Show.Show Test.DPOR.FairBound
instance GHC.Read.Read Test.DPOR.FairBound
instance GHC.Real.Integral Test.DPOR.FairBound
instance GHC.Real.Real Test.DPOR.FairBound
instance GHC.Num.Num Test.DPOR.FairBound
instance GHC.Classes.Ord Test.DPOR.FairBound
instance GHC.Classes.Eq Test.DPOR.FairBound
instance GHC.Enum.Enum Test.DPOR.FairBound
instance Control.DeepSeq.NFData Test.DPOR.FairBound
instance GHC.Show.Show Test.DPOR.PreemptionBound
instance GHC.Read.Read Test.DPOR.PreemptionBound
instance GHC.Real.Integral Test.DPOR.PreemptionBound
instance GHC.Real.Real Test.DPOR.PreemptionBound
instance GHC.Num.Num Test.DPOR.PreemptionBound
instance GHC.Classes.Ord Test.DPOR.PreemptionBound
instance GHC.Classes.Eq Test.DPOR.PreemptionBound
instance GHC.Enum.Enum Test.DPOR.PreemptionBound
instance Control.DeepSeq.NFData Test.DPOR.PreemptionBound
