Copyright	(c) 2016 Michael Walker
License	MIT
Maintainer	Michael Walker <mike@barrucadu.co.uk>
Stability	experimental
Portability	portable
Safe Haskell	Safe
Language	Haskell2010

Test.DPOR.Internal

Contents

Dynamic partial-order reduction
DPOR scheduler
Utilities

Description

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

Synopsis

Dynamic partial-order reduction

data DPOR tid action #

DPOR execution is represented as a tree of states, characterised by the decisions that lead to that state.

Constructors

DPOR

Fields

dporRunnable :: Set tid
What threads are runnable at this step.
dporTodo :: Map tid Bool
Follow-on decisions still to make, and whether that decision was added conservatively due to the bound.
dporDone :: Map tid (DPOR tid action)
Follow-on decisions that have been made.
dporSleep :: Map tid action
Transitions to ignore (in this node and children) until a dependent transition happens.
dporTaken :: Map tid action
Transitions which have been taken, excluding conservatively-added ones. This is used in implementing sleep sets.
dporAction :: Maybe action
What happened at this step. This will be Nothing at the root, Just everywhere else.

Instances

(NFData tid, NFData action) => NFData (DPOR tid action) #
Methods rnf :: DPOR tid action -> () #

data BacktrackStep tid action lookahead state #

One step of the execution, including information for backtracking purposes. This backtracking information is used to generate new schedules.

Constructors

BacktrackStep

Fields

bcktThreadid :: tid
The thread running at this step
bcktDecision :: (Decision tid, action)
What happened at this step.
bcktRunnable :: Map tid lookahead
The threads runnable at this step
bcktBacktracks :: Map tid Bool
The list of alternative threads to run, and whether those alternatives were added conservatively due to the bound.
bcktState :: state
Some domain-specific state at this point.

Instances

(Show state, Show lookahead, Show action, Show tid) => Show (BacktrackStep tid action lookahead state) #
Methods showsPrec :: Int -> BacktrackStep tid action lookahead state -> ShowS # show :: BacktrackStep tid action lookahead state -> String # showList :: [BacktrackStep tid action lookahead state] -> ShowS #
(NFData tid, NFData action, NFData lookahead, NFData state) => NFData (BacktrackStep tid action lookahead state) #
Methods rnf :: BacktrackStep tid action lookahead state -> () #

initialState :: Ord tid => tid -> DPOR tid action #

Initial DPOR state, given an initial thread ID. This initial thread should exist and be runnable at the start of execution.

findSchedulePrefix #

Arguments

:: Ord tid
=> (tid -> Bool)	Some partitioning function, applied to the to-do decisions. If there is an identifier which passes the test, it will be used, rather than any which fail it. This allows a very basic way of domain-specific prioritisation between otherwise equal choices, which may be useful in some cases.
-> (Int -> (Int, g))	List indexing function, used to select which schedule to return. Takes the length of the list, and returns an index and some generator state. The index returned MUST be in range!
-> DPOR tid action
-> Maybe ([tid], Bool, Map tid action, g)

Produce a new schedule prefix from a DPOR tree. If there are no new prefixes remaining, return Nothing. 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.

type Trace tid action lookahead = [(Decision tid, [(tid, NonEmpty lookahead)], action)] #

One of the outputs of the runner is a Trace, 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.

incorporateTrace #

Arguments

:: Ord tid
=> state	Initial state
-> (state -> (tid, action) -> state)	State step function
-> (state -> (tid, action) -> (tid, action) -> Bool)	Dependency function
-> Bool	Whether the "to-do" point which was used to create this new execution was conservative or not.
-> Trace tid action lookahead	The execution trace: the decision made, the runnable threads, and the action performed.
-> DPOR tid action
-> DPOR tid action

Add a new trace to the tree, creating a new subtree branching off at the point where the "to-do" decision was made.

findBacktrackSteps #

Arguments

:: Ord tid
=> s	Initial state.
-> (s -> (tid, action) -> s)	State step function.
-> (s -> (tid, action) -> (tid, lookahead) -> Bool)	Dependency function.
-> ([BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s])	Backtracking function. Given a list of backtracking points, and a thread to backtrack to at a specific point in that list, add the new backtracking points. There will be at least one: this chosen one, but the function may add others.
-> Bool	Whether the computation was aborted due to no decisions being in-bounds.
-> Seq (NonEmpty (tid, lookahead), [tid])	A sequence of threads at each step: the nonempty list of runnable threads (with lookahead values), and the list of threads still to try. The reason for the two separate lists is because the threads chosen to try will be dependent on the specific domain.
-> Trace tid action lookahead	The execution trace.
-> [BacktrackStep tid action lookahead s]

Produce a list of new backtracking points from an execution trace. These are then used to inform new "to-do" points in the DPOR 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.

incorporateBacktrackSteps #

Arguments

:: Ord tid
=> ([(Decision tid, action)] -> (Decision tid, lookahead) -> Bool)	Bound function: returns true if that schedule prefix terminated with the lookahead decision fits within the bound.
-> [BacktrackStep tid action lookahead s]	Backtracking steps identified by `findBacktrackSteps`.
-> DPOR tid action
-> DPOR tid action

Add new backtracking points, if they have not already been visited, fit into the bound, and aren't in the sleep set.

DPOR scheduler

type DPORScheduler tid action lookahead s = Scheduler tid action lookahead (SchedState tid action lookahead s) #

A Scheduler where the state is a SchedState.

data SchedState tid action lookahead s #

The scheduler state

Constructors

SchedState

Fields

schedSleep :: Map tid action
The sleep set: decisions not to make until something dependent with them happens.
schedPrefix :: [tid]
Decisions still to make
schedBPoints :: Seq (NonEmpty (tid, lookahead), [tid])
Which threads are runnable at each step, and the alternative decisions still to make.
schedIgnore :: Bool
Whether to ignore this execution or not: True 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.
schedBoundKill :: Bool
Whether the execution was terminated due to all decisions being out of bounds.
schedDepState :: s
State used by the dependency function to determine when to remove decisions from the sleep set.

Instances

(Show s, Show lookahead, Show action, Show tid) => Show (SchedState tid action lookahead s) #
Methods showsPrec :: Int -> SchedState tid action lookahead s -> ShowS # show :: SchedState tid action lookahead s -> String # showList :: [SchedState tid action lookahead s] -> ShowS #
(NFData tid, NFData action, NFData lookahead, NFData s) => NFData (SchedState tid action lookahead s) #
Methods rnf :: SchedState tid action lookahead s -> () #

initialSchedState #

Arguments

:: s	The initial dependency function state.
-> Map tid action	The initial sleep set.
-> [tid]	The schedule prefix.
-> SchedState tid action lookahead s

Initial scheduler state for a given prefix

type BoundFunc tid action lookahead = [(Decision tid, action)] -> (Decision tid, lookahead) -> Bool #

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.

trueBound :: BoundFunc tid action lookahead #

The "true" bound, which allows everything.

type BacktrackFunc tid action lookahead s = [BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s] #

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 function 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 backtrackAt to do the actual work.

backtrackAt #

Arguments

:: Ord tid
=> (BacktrackStep tid action lookahead s -> Bool)	If this returns `True`, backtrack to all runnable threads, rather than just the given thread.
-> Bool	Is this backtracking point conservative? Conservative points are always explored, whereas non-conservative ones might be skipped based on future information.
-> BacktrackFunc 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.

dporSched #

Arguments

:: (Ord tid, NFData tid, NFData action, NFData lookahead, NFData s)
=> (action -> Bool)	Determine if a thread yielded.
-> (lookahead -> Bool)	Determine if a thread will yield.
-> (s -> (tid, action) -> (tid, action) -> Bool)	Dependency function.
-> (s -> (tid, lookahead) -> NonEmpty tid -> Bool)	Daemon-termination predicate.
-> (s -> (tid, action) -> s)	Dependency function's state step function.
-> BoundFunc tid action lookahead	Bound function: returns true if that schedule prefix terminated with the lookahead decision fits within the bound.
-> DPORScheduler 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 will 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.

Utilities

initialDPORThread :: DPOR tid action -> tid #

toDot #

Arguments

:: (tid -> String)	Show a `tid` - this should produce a string suitable for use as a node identifier.
-> (action -> String)	Show a `action`.
-> DPOR tid action
-> String

Render a DPOR value as a graph in GraphViz "dot" format.

toDotFiltered #

Arguments

:: (tid -> DPOR tid action -> Bool)	Subtree predicate.
-> (tid -> String)
-> (action -> String)
-> DPOR tid action
-> String

Render a DPOR value as a graph in GraphViz "dot" format, with a function to determine if a subtree should be included or not.

err :: String -> String -> a #

Internal errors.