Test.DejaFu.SCT.Internal.DPOR

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

Dynamic partial-order reduction

data DPOR

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

Constructors

DPOR

Fields

• dporRunnable :: Set ThreadId

  What threads are runnable at this step.

• dporTodo :: Map ThreadId Bool

  Follow-on decisions still to make, and whether that decision was added conservatively due to the bound.

• dporNext :: Maybe (ThreadId, DPOR)

  The next decision made. Executions are explored in a depth-first fashion, so this changes as old subtrees are exhausted and new ones explored.

• dporDone :: Set ThreadId

  All transitions which have been taken from this point, including conservatively-added ones.

• dporSleep :: Map ThreadId ThreadAction

  Transitions to ignore (in this node and children) until a dependent transition happens.

• dporTaken :: Map ThreadId ThreadAction

  Transitions which have been taken, excluding conservatively-added ones. This is used in implementing sleep sets.

Instances

Eq DPOR

Methods

(==) :: DPOR -> DPOR -> Bool

(/=) :: DPOR -> DPOR -> Bool

Show DPOR

Methods

showsPrec :: Int -> DPOR -> ShowS

show :: DPOR -> String

showList :: [DPOR] -> ShowS

NFData DPOR

Methods

rnf :: DPOR -> ()

data BacktrackStep

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

Constructors

BacktrackStep

Fields

• bcktThreadid :: ThreadId

  The thread running at this step

• bcktDecision :: Decision

  What was decided at this step.

• bcktAction :: ThreadAction

  What happened at this step.

• bcktRunnable :: Map ThreadId Lookahead

  The threads runnable at this step

• bcktBacktracks :: Map ThreadId Bool

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

• bcktState :: DepState

  Some domain-specific state at this point.

Instances

Eq BacktrackStep

Methods

(==) :: BacktrackStep -> BacktrackStep -> Bool

(/=) :: BacktrackStep -> BacktrackStep -> Bool

Show BacktrackStep

Methods

showsPrec :: Int -> BacktrackStep -> ShowS

show :: BacktrackStep -> String

showList :: [BacktrackStep] -> ShowS

NFData BacktrackStep

Methods

rnf :: BacktrackStep -> ()

initialState :: DPOR

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

findSchedulePrefix :: 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.

incorporateTrace

Arguments

:: 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 stack. This won't work if to-dos aren't explored depth-first.

findBacktrackSteps

Arguments

:: BacktrackFunc

Backtracking function. Given a list of backtracking points, and a thread to backtrack to at a specific point in that list, add the new backtracking points. There will be at least one: this chosen one, but the function may add others.

-> Bool

Whether the computation was aborted due to no decisions being in-bounds.

-> Seq ([(ThreadId, Lookahead)], [ThreadId])

A sequence of threads at each step: the list of runnable in-bound threads (with lookahead values), and the list of threads still to try. The reason for the two separate lists is because the threads chosen to try will be dependent on the specific domain.

-> Trace

The execution trace.

-> [BacktrackStep]

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.

incorporateBacktrackSteps :: [BacktrackStep] -> DPOR -> DPOR

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

DPOR scheduler

data DPORSchedState k

The scheduler state

Constructors

DPORSchedState

Fields

• schedSleep :: Map ThreadId ThreadAction

  The sleep set: decisions not to make until something dependent with them happens.

• schedPrefix :: [ThreadId]

  Decisions still to make

• schedBPoints :: Seq ([(ThreadId, Lookahead)], [ThreadId])

  Which threads are runnable and in-bound at each step, and the alternative decisions still to make.

• schedIgnore :: Bool

  Whether 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 :: Bool

  Whether the execution was terminated due to all decisions being out of bounds.

• schedDepState :: DepState

  State used by the dependency function to determine when to remove decisions from the sleep set.

• schedBState :: Maybe k

  State used by the incremental bounding function.

Instances

Eq k => Eq (DPORSchedState k)

Methods

(==) :: DPORSchedState k -> DPORSchedState k -> Bool

(/=) :: DPORSchedState k -> DPORSchedState k -> Bool

Show k => Show (DPORSchedState k)

Methods

showsPrec :: Int -> DPORSchedState k -> ShowS

show :: DPORSchedState k -> String

showList :: [DPORSchedState k] -> ShowS

NFData k => NFData (DPORSchedState k)

Methods

rnf :: DPORSchedState k -> ()

initialDPORSchedState

Arguments

:: Map ThreadId ThreadAction

The initial sleep set.

-> [ThreadId]

The schedule prefix.

-> DPORSchedState k

Initial DPOR scheduler state for a given prefix

type IncrementalBoundFunc k = Maybe k -> Maybe (ThreadId, ThreadAction) -> (Decision, Lookahead) -> Maybe k

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.

type BacktrackFunc = [BacktrackStep] -> [(Int, Bool, ThreadId)] -> [BacktrackStep]

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.

backtrackAt

Arguments

:: (ThreadId -> BacktrackStep -> Bool)

If this returns True, backtrack to all runnable threads, rather than just the given thread.

-> BacktrackFunc

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.

dporSched

Arguments

:: IncrementalBoundFunc k

Bound function: returns true if that schedule prefix terminated with the lookahead decision fits within the bound.

-> Scheduler (DPORSchedState k)

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.

Dependency function

dependent :: DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool

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.

dependent' :: DepState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool

Variant of dependent to handle Lookahead.

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

dependentActions :: DepState -> ActionType -> ActionType -> Bool

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!

Dependency function state

data DepState

Constructors

DepState

Fields

• depCRState :: Map CRefId Bool

  Keep track of which CRefs have buffered writes.

• depMVState :: Set MVarId

  Keep track of which MVars are full.

• depMaskState :: Map ThreadId MaskingState

  Keep 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

Eq DepState

Methods

(==) :: DepState -> DepState -> Bool

(/=) :: DepState -> DepState -> Bool

Show DepState

Methods

showsPrec :: Int -> DepState -> ShowS

show :: DepState -> String

showList :: [DepState] -> ShowS

NFData DepState

Methods

rnf :: DepState -> ()

initialDepState :: DepState

Initial dependency state.

updateDepState :: DepState -> ThreadId -> ThreadAction -> DepState

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

updateCRState :: ThreadAction -> Map CRefId Bool -> Map CRefId Bool

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

updateMVState :: ThreadAction -> Set MVarId -> Set MVarId

Update the MVar full/empty state with the action that has just happened.

updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState

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

isBuffered :: DepState -> CRefId -> Bool

Check if a CRef has a buffered write pending.

isFull :: DepState -> MVarId -> Bool

Check if an MVar is full.

canInterrupt :: DepState -> ThreadId -> ThreadAction -> Bool

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

canInterruptL :: DepState -> ThreadId -> Lookahead -> Bool

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

isMaskedInterruptible :: DepState -> ThreadId -> Bool

Check if a thread is masked interruptible.

isMaskedUninterruptible :: DepState -> ThreadId -> Bool

Check if a thread is masked uninterruptible.

Utilities

initialDPORThread :: DPOR -> ThreadId

didYield :: ThreadAction -> Bool

Check if a thread yielded.

willYield :: Lookahead -> Bool

Check if a thread will yield.

killsDaemons :: ThreadId -> Lookahead -> Bool

Check if an action will kill daemon threads.