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

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.

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.

One step of the execution, including information for backtracking purposes. This backtracking information is used to generate new schedules.

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.

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.

Combine two bounds into a larger bound, where both must be satisfied.

The "true" bound, which allows everything.

A sensible default preemption bound: 2.

See Concurrency Testing Using Schedule Bounding: an Empirical Study, P. Thomson, A. F. Donaldson, A. Betts for justification.

Preemption bound function

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.

Count the number of preemptions in a schedule prefix.

A sensible default fair bound: 5.

This comes from playing around myself, but there is probably a better default.

Fair bound function

Add a backtrack point. If the thread isn't runnable, or performs a release operation, add all runnable threads.

Count the number of yields by a thread in a schedule prefix.

Get the maximum difference between the yield counts of all threads in this schedule prefix.

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.

Length bound function

Add a backtrack point. If the thread isn't runnable, add all runnable threads.

A Scheduler where the state is a SchedState.

The scheduler state

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.