Test.DejaFu.SCT

Systematic testing for concurrent computations.

Bounded 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 both a generic function for BPOR, and also a pre-emption bounding BPOR runner, which is used by the Test.DejaFu module.

See Bounded partial-order reduction, K. Coons, M. Musuvathi, K. McKinley for more details.

data BacktrackStep

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

Constructors

BacktrackStep

Fields

_threadid :: ThreadId

The thread running at this step

_decision :: (Decision, ThreadAction)

What happened at this step.

_runnable :: Set ThreadId

The threads runnable at this step

_backtrack :: IntMap Bool

The list of alternative threads to run, and whether those alternatives were added conservatively due to the bound.

Instances

Eq BacktrackStep

Show BacktrackStep

NFData BacktrackStep

sctBounded

Arguments

:: ([Decision] -> Bool)

Check if a prefix trace is within the bound.

-> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])

Add a new backtrack point, this takes the history of the execution so far, the index to insert the backtracking point, and the thread to backtrack to. This may insert more than one backtracking point.

-> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> NonEmpty ThreadId)

Produce possible scheduling decisions, all will be tried.

-> (forall t. Conc t a)

-> [(Either Failure a, Trace)]

SCT via BPOR.

Schedules are generated by running the computation with a deterministic scheduler with some initial list of decisions, after which the supplied function is called. At each step of execution, possible-conflicting actions are looked for, if any are found, "backtracking points" are added, to cause the events to happen in a different order in a future execution.

Note that unlike with non-bounded partial-order reduction, this may do some redundant work as the introduction of a bound can make previously non-interfering events interfere with each other.

sctBoundedIO :: ([Decision] -> Bool) -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]) -> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> NonEmpty ThreadId) -> (forall t. ConcIO t a) -> IO [(Either Failure a, Trace)]

Variant of sctBounded for computations which do IO.

Pre-emption Bounding

BPOR using pre-emption 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.

sctPreBound

Arguments

:: Int

The maximum number of pre-emptions to allow in a single execution

-> (forall t. Conc t a)

The computation to run many times

-> [(Either Failure a, Trace)]

An SCT runner using a pre-emption bounding scheduler.

sctPreBoundIO :: Int -> (forall t. ConcIO t a) -> IO [(Either Failure a, Trace)]

Variant of sctPreBound for computations which do IO.

Utilities

tidOf :: ThreadId -> Decision -> ThreadId

Get the resultant ThreadId of a Decision, with a default case for Continue.

decisionOf :: Maybe ThreadId -> Set ThreadId -> ThreadId -> Decision

Get the Decision that would have resulted in this ThreadId, given a prior ThreadId (if any) and list of runnable threads.

activeTid :: [Decision] -> ThreadId

Get the tid of the currently active thread after executing a series of decisions. The list MUST begin with a Start.

preEmpCount :: [Decision] -> Int

Count the number of pre-emptions in a schedule

initialCVState :: IntMap Bool

Initial global CVar state

updateCVState :: IntMap Bool -> ThreadAction -> IntMap Bool

Update the CVar state with the action that has just happened.

willBlock :: IntMap Bool -> Lookahead -> Bool

Check if an action will block.

willBlockSafely :: IntMap Bool -> [Lookahead] -> Bool

Check if a list of actions will block safely (without modifying any global state). This allows further lookahead at, say, the spawn of a thread (which always starts with KnowsAbout).