Copyright | (c) 2016 Michael Walker |
---|---|
License | MIT |
Maintainer | Michael Walker <mike@barrucadu.co.uk> |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell2010 |
Internal types and functions for dynamic partial-order reduction. This module is NOT considered to form part of the public interface of this library.
- data DPOR = DPOR {}
- data BacktrackStep = BacktrackStep {}
- initialState :: DPOR
- findSchedulePrefix :: DPOR -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
- incorporateTrace :: MemType -> Bool -> Trace -> DPOR -> DPOR
- findBacktrackSteps :: MemType -> BacktrackFunc -> Bool -> Seq (NonEmpty (ThreadId, Lookahead), [ThreadId]) -> Trace -> [BacktrackStep]
- incorporateBacktrackSteps :: ([(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool) -> [BacktrackStep] -> DPOR -> DPOR
- data DPORSchedState = DPORSchedState {
- schedSleep :: Map ThreadId ThreadAction
- schedPrefix :: [ThreadId]
- schedBPoints :: Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])
- schedIgnore :: Bool
- schedBoundKill :: Bool
- schedDepState :: DepState
- initialDPORSchedState :: Map ThreadId ThreadAction -> [ThreadId] -> DPORSchedState
- type BoundFunc = [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool
- type BacktrackFunc = [BacktrackStep] -> [(Int, Bool, ThreadId)] -> [BacktrackStep]
- backtrackAt :: (ThreadId -> BacktrackStep -> Bool) -> BacktrackFunc
- dporSched :: MemType -> BoundFunc -> Scheduler DPORSchedState
- data RandSchedState g = RandSchedState {
- schedWeights :: Map ThreadId Int
- schedGen :: g
- initialRandSchedState :: Maybe (Map ThreadId Int) -> g -> RandSchedState g
- randSched :: RandomGen g => (g -> (Int, g)) -> Scheduler (RandSchedState g)
- dependent :: MemType -> DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool
- dependent' :: MemType -> DepState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool
- dependentActions :: MemType -> DepState -> ActionType -> ActionType -> Bool
- data DepState = DepState {}
- initialDepState :: DepState
- updateDepState :: DepState -> ThreadId -> ThreadAction -> DepState
- updateCRState :: ThreadAction -> Map CRefId Bool -> Map CRefId Bool
- updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState
- isBuffered :: DepState -> CRefId -> Bool
- canInterrupt :: DepState -> ThreadId -> ThreadAction -> Bool
- canInterruptL :: DepState -> ThreadId -> Lookahead -> Bool
- isMaskedInterruptible :: DepState -> ThreadId -> Bool
- isMaskedUninterruptible :: DepState -> ThreadId -> Bool
- initialDPORThread :: DPOR -> ThreadId
- didYield :: ThreadAction -> Bool
- willYield :: Lookahead -> Bool
- killsDaemons :: ThreadId -> Lookahead -> Bool
- err :: String -> String -> a
- concatPartition :: (a -> Bool) -> [[a]] -> ([a], [a])
Dynamic partial-order reduction
DPOR execution is represented as a tree of states, characterised by the decisions that lead to that state.
DPOR | |
|
data BacktrackStep Source #
One step of the execution, including information for backtracking purposes. This backtracking information is used to generate new schedules.
BacktrackStep | |
|
initialState :: DPOR Source #
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) Source #
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.
:: MemType | Memory model |
-> 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.
:: MemType | Memory model. |
-> 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 (NonEmpty (ThreadId, Lookahead), [ThreadId]) | A sequence of threads at each step: the nonempty list of runnable 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 Source #
:: ([(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 |
-> 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
data DPORSchedState Source #
The scheduler state
DPORSchedState | |
|
initialDPORSchedState Source #
:: Map ThreadId ThreadAction | The initial sleep set. |
-> [ThreadId] | The schedule prefix. |
-> DPORSchedState |
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.
:: (ThreadId -> BacktrackStep -> Bool) | If this returns |
-> 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.
:: MemType | Memory model. |
-> 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.
data RandSchedState g Source #
The scheduler state
RandSchedState | |
|
Eq g => Eq (RandSchedState g) Source # | |
Show g => Show (RandSchedState g) Source # | |
NFData g => NFData (RandSchedState g) Source # | |
initialRandSchedState :: Maybe (Map ThreadId Int) -> g -> RandSchedState g Source #
Initial weighted random scheduler state.
randSched :: RandomGen g => (g -> (Int, g)) -> Scheduler (RandSchedState g) Source #
Weighted random scheduler: assigns to each new thread a weight, and makes a weighted random choice out of the runnable threads at every step.
dependent :: MemType -> DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool Source #
Check if an action is dependent on another.
dependent' :: MemType -> DepState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool Source #
dependentActions :: MemType -> DepState -> ActionType -> ActionType -> Bool Source #
Check if two ActionType
s are dependent. Note that this is not
sufficient to know if two ThreadAction
s are dependent, without
being so great an over-approximation as to be useless!
DepState | |
|
initialDepState :: DepState Source #
Initial dependency state.
updateDepState :: DepState -> ThreadId -> ThreadAction -> DepState Source #
Update the CRef
buffer state with the action that has just
happened.
updateCRState :: ThreadAction -> Map CRefId Bool -> Map CRefId Bool Source #
Update the CRef
buffer state with the action that has just
happened.
updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState Source #
Update the thread masking state with the action that has just happened.
canInterrupt :: DepState -> ThreadId -> ThreadAction -> Bool Source #
Check if an exception can interrupt a thread (action).
canInterruptL :: DepState -> ThreadId -> Lookahead -> Bool Source #
Check if an exception can interrupt a thread (lookahead).
isMaskedInterruptible :: DepState -> ThreadId -> Bool Source #
Check if a thread is masked interruptible.
isMaskedUninterruptible :: DepState -> ThreadId -> Bool Source #
Check if a thread is masked uninterruptible.
Utilities
initialDPORThread :: DPOR -> ThreadId Source #
didYield :: ThreadAction -> Bool Source #
Check if a thread yielded.