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

Check the DPOR data invariants and raise an error if any are broken.

This is a reasonable thing to do, because if the state is corrupted then nothing sensible can happen anyway.

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

Initial DPOR state, given an initial thread ID. This initial thread should exist and be runnable at the start of execution.

The main thread must be in the list of initially runnable threads.

Produce a new schedule prefix from a DPOR tree. If there are no new prefixes remaining, return Nothing. Also returns whether the decision was added conservatively, and the sleep set at the point where divergence happens.

A schedule prefix is a possibly empty sequence of decisions that have already been made, terminated by a single decision from the to-do set. The intent is to put the system into a new state when executed with this initial sequence of scheduling decisions.

Add a new trace to the stack. This won't work if to-dos aren't explored depth-first.

Produce a list of new backtracking points from an execution trace. These are then used to inform new "to-do" points in the DPOR tree.

Two traces are passed in to this function: the first is generated from the special DPOR scheduler, the other from the execution of the concurrent program.

If the trace ends with any threads other than the initial one still runnable, a dependency is imposed between this final action and everything else.

Add new backtracking points, if they have not already been visited and aren't in the sleep set.

The scheduler state

Initial DPOR scheduler state for a given prefix

An incremental bounding function is a stateful function that takes the last and next decisions, and returns a new state only if the next decision is within the bound.

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 list of points and thread at that point to backtrack to. More points 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. The bool is whether the point is conservative. Conservative points are always explored, whereas non-conservative ones might be skipped based on future information.

In general, a backtracking function should identify one or more backtracking points, and then use backtrackAt to do the actual work.

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.

DPOR scheduler: takes a list of decisions, and maintains a trace including the runnable threads, and the alternative choices allowed by the bound-specific initialise function.

After the initial decisions are exhausted, this prefers choosing the prior thread if it's (1) still runnable and (2) hasn't just yielded. Furthermore, threads which will yield are ignored in preference of those which will not.

Check if two actions commute.

This implements a stronger check that not (dependent ...), as it handles some cases which dependent doesn't need to care about.

Check if an action is dependent on another.

This is basically the same as dependent', but can make use of the additional information in a ThreadAction to make better decisions in a few cases.

Variant of dependent to handle Lookahead.

Termination of the initial thread is handled specially in the DPOR implementation.

Check if two ActionTypes are dependent. Note that this is not sufficient to know if two ThreadActions are dependent, without being so great an over-approximation as to be useless!

Check if a thread yielded.

Check if a thread will yield.

Check if an action will kill daemon threads.