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 GeneralizedNewtypeDeriving None Haskell2010

Test.DPOR

Description

Systematic testing of concurrent computations through dynamic partial-order reduction and schedule bounding.

Synopsis

# 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

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).

The daemon-termination predicate returns True if the action being looked at will cause the entire computation to terminate, regardless of the other runnable threads (which are passed in the NonEmpty list). Such actions will then be put off for as long as possible. This allows supporting concurrency models with daemon threads without doing something as drastic as imposing a dependency between the program-terminating action and everything else.

Arguments

A much simplified DPOR function: no state, no preference between threads, and no post-processing between iterations.

data DPOR tid action Source #

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

Constructors

 DPOR FieldsdporRunnable :: Set tidWhat threads are runnable at this step.dporTodo :: Map tid BoolFollow-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 actionTransitions to ignore (in this node and children) until a dependent transition happens.dporTaken :: Map tid actionTransitions which have been taken, excluding conservatively-added ones. This is used in implementing sleep sets.dporAction :: Maybe actionWhat happened at this step. This will be Nothing at the root, Just everywhere else.

Instances

 (NFData tid, NFData action) => NFData (DPOR tid action) Source # Methodsrnf :: DPOR tid action -> () #

## 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 FieldsbcktThreadid :: tidThe thread running at this stepbcktDecision :: (Decision tid, action)What happened at this step.bcktRunnable :: Map tid lookaheadThe threads runnable at this stepbcktBacktracks :: Map tid BoolThe list of alternative threads to run, and whether those alternatives were added conservatively due to the bound.bcktState :: stateSome domain-specific state at this point.

Instances

 (Show tid, Show action, Show lookahead, Show state) => Show (BacktrackStep tid action lookahead state) Source # MethodsshowsPrec :: 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) Source # Methodsrnf :: BacktrackStep tid action lookahead state -> () #

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

## 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.

trueBound :: BoundFunc tid action lookahead Source #

The "true" bound, which allows everything.

### 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

Instances

 Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # MethodsshowList :: [PreemptionBound] -> ShowS # Source # Methodsrnf :: PreemptionBound -> () #

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.

newtype FairBound Source #

Constructors

 FairBound Int

Instances

 Source # MethodsenumFrom :: FairBound -> [FairBound] # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # MethodsshowList :: [FairBound] -> ShowS # Source # Methodsrnf :: FairBound -> () #

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

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

Instances

 Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # MethodsshowList :: [LengthBound] -> ShowS # Source # Methodsrnf :: LengthBound -> () #

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 #

# 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

Instances

 (Show tid, Show action, Show lookahead, Show s) => Show (SchedState tid action lookahead s) Source # MethodsshowsPrec :: 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) Source # Methodsrnf :: SchedState tid action lookahead s -> () #

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.