dejafu-0.5.0.0: Systematic testing for Haskell concurrency.

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

Test.DejaFu.SCT.Internal

Description

Internal types and functions for dynamic partial-order reduction. This module is NOT considered to form part of the public interface of this library.

Synopsis

# Dynamic partial-order reduction

data DPOR Source #

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

Constructors

 DPOR FieldsdporRunnable :: Set ThreadIdWhat threads are runnable at this step.dporTodo :: Map ThreadId BoolFollow-on decisions still to make, and whether that decision was added conservatively due to the bound.dporDone :: Map ThreadId DPORFollow-on decisions that have been made.dporSleep :: Map ThreadId ThreadActionTransitions to ignore (in this node and children) until a dependent transition happens.dporTaken :: Map ThreadId ThreadActionTransitions which have been taken, excluding conservatively-added ones. This is used in implementing sleep sets.dporAction :: Maybe ThreadActionWhat happened at this step. This will be Nothing at the root, Just everywhere else.

Instances

 Source # MethodsshowsPrec :: Int -> DPOR -> ShowS #show :: DPOR -> String #showList :: [DPOR] -> ShowS #

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

Constructors

 BacktrackStep FieldsbcktThreadid :: ThreadIdThe thread running at this stepbcktDecision :: DecisionWhat was decided at this step.bcktAction :: ThreadActionWhat happened at this step.bcktRunnable :: Map ThreadId LookaheadThe threads runnable at this stepbcktBacktracks :: Map ThreadId BoolThe list of alternative threads to run, and whether those alternatives were added conservatively due to the bound.bcktState :: DepStateSome domain-specific state at this point.

Instances

 Source # MethodsshowList :: [BacktrackStep] -> ShowS #

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

Arguments

 :: (ThreadId -> Bool) Some partitioning function, applied to the to-do decisions. If there is an identifier which passes the test, it will be used, rather than any which fail it. This allows a very basic way of domain-specific prioritisation between otherwise equal choices, which may be useful in some cases. -> DPOR -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)

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.

Arguments

 :: (DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool) Dependency function -> Bool Whether the "to-do" point which was used to create this new execution was conservative or not. -> Trace The execution trace: the decision made, the runnable threads, and the action performed. -> DPOR -> DPOR

Add a new trace to the tree, creating a new subtree branching off at the point where the "to-do" decision was made.

Arguments

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.

Arguments

 :: ([(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool) Bound function: returns true if that schedule prefix terminated with the lookahead decision fits within the bound. -> [BacktrackStep] Backtracking steps identified by findBacktrackSteps. -> DPOR -> DPOR

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

# DPOR scheduler

The scheduler state

Constructors

 DPORSchedState FieldsschedSleep :: Map ThreadId ThreadActionThe sleep set: decisions not to make until something dependent with them happens.schedPrefix :: [ThreadId]Decisions still to makeschedBPoints :: Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])Which threads are runnable at each step, and the alternative decisions still to make.schedIgnore :: BoolWhether to ignore this execution or not: True if the execution is aborted due to all possible decisions being in the sleep set, as then everything in this execution is covered by another.schedBoundKill :: BoolWhether the execution was terminated due to all decisions being out of bounds.schedDepState :: DepStateState used by the dependency function to determine when to remove decisions from the sleep set.

Instances

 Source # MethodsshowList :: [DPORSchedState] -> ShowS #

Arguments

Initial DPOR scheduler state for a given prefix

type BoundFunc = [(Decision, ThreadAction)] -> (Decision, 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.

type BacktrackFunc = [BacktrackStep] -> [(Int, Bool, ThreadId)] -> [BacktrackStep] 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 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.

Arguments

 :: (ThreadId -> BacktrackStep -> Bool) If this returns True, backtrack to all runnable threads, rather than just the given thread. -> BacktrackFunc

Arguments

 :: (DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool) Dependency function. -> BoundFunc Bound function: returns true if that schedule prefix terminated with the lookahead decision fits within the bound. -> Scheduler DPORSchedState

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.

The scheduler state

Constructors

 RandSchedState FieldsschedWeights :: Map ThreadId IntThe thread weights: used in determining which to run.schedGen :: gThe random number generator.

Initial weighted random scheduler state.

Weighted random scheduler: assigns to each new thread a weight, and makes a weighted random choice out of the runnable threads at every step.

data DepState Source #

Constructors

 DepState FieldsdepCRState :: Map CRefId BoolKeep track of which CRefs have buffered writes.depMaskState :: Map ThreadId MaskingStateKeep track of thread masking states. If a thread isn't present, the masking state is assumed to be Unmasked. This nicely provides compatibility with dpor-0.1, where the thread IDs are not available.

Instances

 Source # Methods Source # MethodsshowList :: [DepState] -> ShowS #

Initial dependency state.

Update the CRef buffer state with the action that has just happened.

Update the CRef buffer state with the action that has just happened.

Update the thread masking state with the action that has just happened.

Check if a CRef has a buffered write pending.

Check if an exception can interrupt a thread (action).

# Utilities

Check if a thread will yield.

Check if an action will kill daemon threads.

Arguments

 :: (ThreadId -> String) Show a tid - this should produce a string suitable for use as a node identifier. -> (ThreadAction -> String) Show a action. -> DPOR -> String

Render a DPOR value as a graph in GraphViz "dot" format.

Arguments

 :: (ThreadId -> DPOR -> Bool) Subtree predicate. -> (ThreadId -> String) -> (ThreadAction -> String) -> DPOR -> String

Render a DPOR value as a graph in GraphViz "dot" format, with a function to determine if a subtree should be included or not.

err :: String -> String -> a Source #

Internal errors.

concatPartition :: (a -> Bool) -> [[a]] -> ([a], [a]) Source #

A combination of partition and concat.