| 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.Random
Description
Random and incomplete techniques for when complete testing is infeasible.
- 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)]
- 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)]
Randomness and partial-order reduction
Arguments
| :: (Ord tid, NFData tid, NFData action, NFData lookahead, NFData s, Monad m, RandomGen g) | |
| => (action -> Bool) | Determine if a thread yielded. |
| -> (lookahead -> Bool) | Determine if a thread will yield. |
| -> s | The initial state for backtracking. |
| -> (s -> (tid, 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. |
| -> (s -> (tid, lookahead) -> NonEmpty tid -> Bool) | The daemon-termination predicate. |
| -> 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. |
| -> g | Random number generator, used to determine which schedules to try. |
| -> Int | Execution limit, used to abort the execution whilst schedules still remain. |
| -> m [(a, Trace tid action lookahead)] |
Random dynamic partial-order reduction.
This is the dpor algorithm in Test.DPOR, 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.
Non-POR techniques
These algorithms do not make use of partial-order reduction to systematically prune the search space and search for interesting interleavings. Instead, the exploration is driven entirely by random choice, with optional bounds. However, the same schedule will never be explored twice.
Arguments
| :: (Ord tid, NFData tid, NFData action, NFData lookahead, Monad m, RandomGen g) | |
| => (action -> Bool) | Determine if a thread yielded. |
| -> (lookahead -> Bool) | Determine if a thread will yield. |
| -> tid | The initial thread. |
| -> Maybe (BoundFunc tid action lookahead) | The bounding function. If no function is provided, |
| -> (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. |
| -> g | Random number generator, used to determine which schedules to try. |
| -> Int | Execution limit, used to abort the execution whilst schedules still remain. |
| -> m [(a, Trace tid action lookahead)] |
Pure random scheduling. Like randomDPOR but all actions are
dependent and the bounds are optional.