dpor-0.2.0.0: A generic implementation of dynamic partial-order reduction (DPOR) for testing arbitrary models of concurrency.

Copyright (c) 2016 Michael Walker MIT Michael Walker experimental portable Safe Haskell2010

Test.DPOR.Random

Description

Random and incomplete techniques for when complete testing is infeasible.

Synopsis

# Randomness and partial-order reduction

Arguments

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, trueBound is used. -> (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.