| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Test.DPOR
Contents
Description
Systematic testing of concurrent computations through dynamic partial-order reduction and schedule bounding.
- dpor :: (Ord tid, NFData tid, NFData action, NFData lookahead, NFData s, Monad m) => (action -> Bool) -> (lookahead -> Bool) -> s -> (s -> action -> s) -> (s -> (tid, action) -> (tid, action) -> Bool) -> (s -> (tid, action) -> (tid, lookahead) -> 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)]
- 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 -> 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)]
- data DPOR tid action = DPOR {}
- type BacktrackFunc tid action lookahead s = [BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s]
- data BacktrackStep tid action lookahead state = BacktrackStep {
- bcktThreadid :: tid
- bcktDecision :: (Decision tid, action)
- bcktRunnable :: Map tid lookahead
- bcktBacktracks :: Map tid Bool
- bcktState :: state
- backtrackAt :: Ord tid => (BacktrackStep tid action lookahead s -> Bool) -> Bool -> BacktrackFunc tid action lookahead s
- type BoundFunc tid action lookahead = [(Decision tid, action)] -> (Decision tid, lookahead) -> Bool
- (&+&) :: BoundFunc tid action lookahead -> BoundFunc tid action lookahead -> BoundFunc tid action lookahead
- trueBound :: BoundFunc tid action lookahead
- newtype PreemptionBound = PreemptionBound Int
- defaultPreemptionBound :: PreemptionBound
- preempBound :: (action -> Bool) -> PreemptionBound -> BoundFunc tid action lookahead
- preempBacktrack :: Ord tid => (action -> Bool) -> BacktrackFunc tid action lookahead s
- preempCount :: (action -> Bool) -> [(Decision tid, action)] -> (Decision tid, lookahead) -> Int
- newtype FairBound = FairBound Int
- defaultFairBound :: FairBound
- fairBound :: Eq tid => (action -> Bool) -> (lookahead -> Bool) -> (action -> [tid]) -> FairBound -> BoundFunc tid action lookahead
- fairBacktrack :: Ord tid => (lookahead -> Bool) -> BacktrackFunc tid action lookahead s
- yieldCount :: Eq tid => (action -> Bool) -> (lookahead -> Bool) -> tid -> [(Decision tid, action)] -> (Decision tid, lookahead) -> Int
- maxYieldCountDiff :: Eq tid => (action -> Bool) -> (lookahead -> Bool) -> (action -> [tid]) -> [(Decision tid, action)] -> (Decision tid, lookahead) -> Int
- newtype LengthBound = LengthBound Int
- defaultLengthBound :: LengthBound
- lenBound :: LengthBound -> BoundFunc tid action lookahead
- lenBacktrack :: Ord tid => BacktrackFunc tid action lookahead s
- type DPORScheduler tid action lookahead s = Scheduler tid action lookahead (SchedState tid action lookahead s)
- data SchedState tid action lookahead s
- type Trace tid action lookahead = [(Decision tid, [(tid, NonEmpty lookahead)], action)]
- module Test.DPOR.Schedule
Bounded dynamic partial-order reduction
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, and so are not ordered.
Partial-order reduction is a technique for computing these partial orders, and only testing one total order for each partial order. This cuts down the amount of work to be done significantly. Bounded partial-order reduction is a further optimisation, which only considers schedules within some bound.
This module provides a generic function for DPOR, parameterised by the actual (domain-specific) dependency function to use.
See Bounded partial-order reduction, K. Coons, M. Musuvathi, K. McKinley for more details.
Arguments
| :: (Ord tid, NFData tid, NFData action, NFData lookahead, NFData s, Monad m) | |
| => (action -> Bool) | Determine if a thread yielded. |
| -> (lookahead -> Bool) | Determine if a thread will yield. |
| -> s | The initial state for backtracking. |
| -> (s -> action -> s) | The backtracking state step function. |
| -> (s -> (tid, action) -> (tid, action) -> Bool) | The dependency (1) function. |
| -> (s -> (tid, action) -> (tid, lookahead) -> Bool) | The dependency (2) function. |
| -> tid | The initial thread. |
| -> (tid -> Bool) | The thread partitioning function: when choosing what to execute, prefer threads which return true. |
| -> BoundFunc tid action lookahead | The bounding function. |
| -> BacktrackFunc tid action lookahead s | The backtracking function. Note that, for some bounding functions, this will need to add conservative backtracking points. |
| -> (DPOR tid action -> DPOR tid action) | Some post-processing to do after adding the new to-do points. |
| -> (DPORScheduler tid action lookahead s -> SchedState tid action lookahead s -> m (a, SchedState tid action lookahead s, Trace tid action lookahead)) | The runner: given the scheduler and state, execute the computation under that scheduler. |
| -> m [(a, Trace tid action lookahead)] |
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 action and lookahead, 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).
Arguments
| :: (Ord tid, NFData tid, NFData action, NFData lookahead, Monad m) | |
| => (action -> Bool) | Determine if a thread yielded. |
| -> (lookahead -> Bool) | Determine if a thread will yield. |
| -> ((tid, action) -> (tid, action) -> Bool) | The dependency (1) function. |
| -> ((tid, action) -> (tid, lookahead) -> Bool) | The dependency (2) function. |
| -> tid | The initial thread. |
| -> BoundFunc tid action lookahead | The bounding function. |
| -> BacktrackFunc tid action lookahead () | The backtracking function. Note that, for some bounding functions, this will need to add conservative backtracking points. |
| -> (DPORScheduler tid action lookahead () -> SchedState tid action lookahead () -> m (a, SchedState tid action lookahead (), Trace tid action lookahead)) | The runner: given the scheduler and state, execute the computation under that scheduler. |
| -> m [(a, Trace tid action lookahead)] |
A much simplified DPOR function: no state, no preference between threads, and no post-processing between iterations.
DPOR execution is represented as a tree of states, characterised by the decisions that lead to that state.
Constructors
| DPOR | |
Fields
| |
Backtracking
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.
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.
Constructors
| BacktrackStep | |
Fields
| |
Arguments
| :: Ord tid | |
| => (BacktrackStep tid action lookahead s -> Bool) | If this returns |
| -> 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.
Bounding
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.
(&+&) :: BoundFunc tid action lookahead -> BoundFunc tid action lookahead -> BoundFunc tid action lookahead Source #
Combine two bounds into a larger bound, where both must be satisfied.
Preemption
DPOR with preemption bounding. This adds conservative backtracking points at the prior context switch whenever a non-conervative backtracking point is added, as alternative decisions can influence the reachability of different states.
See the BPOR paper for more details.
newtype PreemptionBound Source #
Constructors
| PreemptionBound Int |
defaultPreemptionBound :: PreemptionBound Source #
A sensible default preemption bound: 2.
See Concurrency Testing Using Schedule Bounding: an Empirical Study, P. Thomson, A. F. Donaldson, A. Betts for justification.
Arguments
| :: (action -> Bool) | Determine if a thread yielded. |
| -> PreemptionBound | |
| -> BoundFunc tid action lookahead |
Preemption bound function
Arguments
| :: Ord tid | |
| => (action -> Bool) | If this is true of the action at a preemptive context switch, do NOT use that point for the conservative point, try earlier. |
| -> BacktrackFunc tid action lookahead s |
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.
Arguments
| :: (action -> Bool) | Determine if a thread yielded. |
| -> [(Decision tid, action)] | The schedule prefix. |
| -> (Decision tid, lookahead) | The to-do point. |
| -> Int |
Count the number of preemptions in a schedule prefix.
Fair
DPOR using fair bounding. This bounds the maximum difference between the number of yield operations different threads have performed.
See the DPOR paper for more details.
defaultFairBound :: FairBound Source #
A sensible default fair bound: 5.
This comes from playing around myself, but there is probably a better default.
Arguments
| :: Eq tid | |
| => (action -> Bool) | Determine if a thread yielded. |
| -> (lookahead -> Bool) | Determine if a thread will yield. |
| -> (action -> [tid]) | The new threads an action causes to come into existence. |
| -> FairBound | |
| -> BoundFunc tid action lookahead |
Fair bound function
Arguments
| :: Ord tid | |
| => (lookahead -> Bool) | Determine if an action is a release operation: if it could cause other threads to become runnable. |
| -> BacktrackFunc tid action lookahead s |
Add a backtrack point. If the thread isn't runnable, or performs a release operation, add all runnable threads.
Arguments
| :: Eq tid | |
| => (action -> Bool) | Determine if a thread yielded. |
| -> (lookahead -> Bool) | Determine if a thread will yield. |
| -> tid | The thread to count yields for. |
| -> [(Decision tid, action)] | |
| -> (Decision tid, lookahead) | |
| -> Int |
Count the number of yields by a thread in a schedule prefix.
Arguments
| :: Eq tid | |
| => (action -> Bool) | Determine if a thread yielded. |
| -> (lookahead -> Bool) | Determine if a thread will yield. |
| -> (action -> [tid]) | The new threads an action causes to come into existence. |
| -> [(Decision tid, action)] | |
| -> (Decision tid, lookahead) | |
| -> Int |
Get the maximum difference between the yield counts of all threads in this schedule prefix.
Length
BPOR using length bounding. This bounds the maximum length (in terms of primitive actions) of an execution.
newtype LengthBound Source #
Constructors
| LengthBound Int |
defaultLengthBound :: LengthBound Source #
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.
lenBound :: LengthBound -> BoundFunc tid action lookahead Source #
Length bound function
lenBacktrack :: Ord tid => BacktrackFunc tid action lookahead s Source #
Add a backtrack point. If the thread isn't runnable, add all runnable threads.
Scheduling & execution traces
The partial-order reduction is driven by incorporating information gained from trial executions of the concurrent program.
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
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.
module Test.DPOR.Schedule