Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Internal types and functions for dynamic partial-order reduction.
- data DPOR tid action = DPOR {}
- data BacktrackStep tid action lookahead state = BacktrackStep {
- bcktThreadid :: tid
- bcktDecision :: (Decision tid, action)
- bcktRunnable :: Map tid lookahead
- bcktBacktracks :: Map tid Bool
- bcktState :: state
- initialState :: Ord tid => tid -> DPOR tid action
- findSchedulePrefix :: Ord tid => (tid -> Bool) -> DPOR tid action -> Maybe ([tid], Bool, Map tid action)
- type Trace tid action lookahead = [(Decision tid, [(tid, NonEmpty lookahead)], action)]
- incorporateTrace :: Ord tid => state -> (state -> action -> state) -> (state -> (tid, action) -> (tid, action) -> Bool) -> Bool -> Trace tid action lookahead -> DPOR tid action -> DPOR tid action
- findBacktrackSteps :: Ord tid => s -> (s -> action -> s) -> (s -> (tid, action) -> (tid, lookahead) -> Bool) -> ([BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s]) -> Seq (NonEmpty (tid, lookahead), [tid]) -> Trace tid action lookahead -> [BacktrackStep tid action lookahead s]
- incorporateBacktrackSteps :: Ord tid => ([(Decision tid, action)] -> (Decision tid, lookahead) -> Bool) -> [BacktrackStep tid action lookahead s] -> DPOR tid action -> DPOR tid action
- type DPORScheduler tid action lookahead s = Scheduler tid action lookahead (SchedState tid action lookahead s)
- data SchedState tid action lookahead s = SchedState {
- schedSleep :: Map tid action
- schedPrefix :: [tid]
- schedBPoints :: Seq (NonEmpty (tid, lookahead), [tid])
- schedIgnore :: Bool
- schedDepState :: s
- initialSchedState :: s -> Map tid action -> [tid] -> SchedState tid action lookahead s
- type BoundFunc tid action lookahead = [(Decision tid, action)] -> (Decision tid, lookahead) -> Bool
- type BacktrackFunc tid action lookahead s = [BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s]
- dporSched :: (Ord tid, NFData tid, NFData action, NFData lookahead, NFData s) => (action -> Bool) -> (lookahead -> Bool) -> (s -> (tid, action) -> (tid, action) -> Bool) -> (s -> action -> s) -> BoundFunc tid action lookahead -> DPORScheduler tid action lookahead s
- initialDPORThread :: DPOR tid action -> tid
- toDot :: (tid -> String) -> (action -> String) -> DPOR tid action -> String
- toDotFiltered :: (tid -> DPOR tid action -> Bool) -> (tid -> String) -> (action -> String) -> DPOR tid action -> String
Dynamic partial-order reduction
DPOR execution is represented as a tree of states, characterised by the decisions that lead to that state.
DPOR | |
|
data BacktrackStep tid action lookahead state Source
One step of the execution, including information for backtracking purposes. This backtracking information is used to generate new schedules.
BacktrackStep | |
|
initialState :: Ord tid => tid -> DPOR tid action Source
Initial DPOR state, given an initial thread ID. This initial thread should exist and be runnable at the start of execution.
:: 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. |
-> DPOR tid action | |
-> Maybe ([tid], Bool, Map tid action) |
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.
This returns the longest prefix, on the assumption that this will lead to lots of backtracking points being identified before higher-up decisions are reconsidered, so enlarging the sleep sets.
type Trace tid action lookahead = [(Decision tid, [(tid, NonEmpty lookahead)], action)] Source
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.
:: Ord tid | |
=> state | Initial state |
-> (state -> 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.
:: Ord tid | |
=> s | Initial state. |
-> (s -> 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. |
-> 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 Source
:: 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 |
-> 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) Source
A Scheduler
where the state is a SchedState
.
data SchedState tid action lookahead s Source
The scheduler state
SchedState | |
|
:: 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 Source
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 BacktrackFunc tid action lookahead s = [BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s] Source
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.
:: (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 -> 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 Source