| Copyright | (c) 2017--2018 Michael Walker |
|---|---|
| License | MIT |
| Maintainer | Michael Walker <mike@barrucadu.co.uk> |
| Stability | experimental |
| Portability | DeriveGeneric, GeneralizedNewtypeDeriving, StandaloneDeriving |
| Safe Haskell | None |
| Language | Haskell2010 |
Test.DejaFu.Types
Contents
Description
Common types and functions used throughout DejaFu.
- newtype ThreadId = ThreadId Id
- newtype CRefId = CRefId Id
- newtype MVarId = MVarId Id
- newtype TVarId = TVarId Id
- data Id = Id (Maybe String) !Int
- initialThread :: ThreadId
- data ThreadAction
- = Fork ThreadId
- | ForkOS ThreadId
- | IsCurrentThreadBound Bool
- | MyThreadId
- | GetNumCapabilities Int
- | SetNumCapabilities Int
- | Yield
- | ThreadDelay Int
- | NewMVar MVarId
- | PutMVar MVarId [ThreadId]
- | BlockedPutMVar MVarId
- | TryPutMVar MVarId Bool [ThreadId]
- | ReadMVar MVarId
- | TryReadMVar MVarId Bool
- | BlockedReadMVar MVarId
- | TakeMVar MVarId [ThreadId]
- | BlockedTakeMVar MVarId
- | TryTakeMVar MVarId Bool [ThreadId]
- | NewCRef CRefId
- | ReadCRef CRefId
- | ReadCRefCas CRefId
- | ModCRef CRefId
- | ModCRefCas CRefId
- | WriteCRef CRefId
- | CasCRef CRefId Bool
- | CommitCRef ThreadId CRefId
- | STM [TAction] [ThreadId]
- | BlockedSTM [TAction]
- | Catching
- | PopCatching
- | Throw
- | ThrowTo ThreadId
- | BlockedThrowTo ThreadId
- | SetMasking Bool MaskingState
- | ResetMasking Bool MaskingState
- | LiftIO
- | Return
- | Stop
- | Subconcurrency
- | StopSubconcurrency
- | DontCheck Trace
- data Lookahead
- = WillFork
- | WillForkOS
- | WillIsCurrentThreadBound
- | WillMyThreadId
- | WillGetNumCapabilities
- | WillSetNumCapabilities Int
- | WillYield
- | WillThreadDelay Int
- | WillNewMVar
- | WillPutMVar MVarId
- | WillTryPutMVar MVarId
- | WillReadMVar MVarId
- | WillTryReadMVar MVarId
- | WillTakeMVar MVarId
- | WillTryTakeMVar MVarId
- | WillNewCRef
- | WillReadCRef CRefId
- | WillReadCRefCas CRefId
- | WillModCRef CRefId
- | WillModCRefCas CRefId
- | WillWriteCRef CRefId
- | WillCasCRef CRefId
- | WillCommitCRef ThreadId CRefId
- | WillSTM
- | WillCatching
- | WillPopCatching
- | WillThrow
- | WillThrowTo ThreadId
- | WillSetMasking Bool MaskingState
- | WillResetMasking Bool MaskingState
- | WillLiftIO
- | WillReturn
- | WillStop
- | WillSubconcurrency
- | WillStopSubconcurrency
- | WillDontCheck
- data TAction
- type Trace = [(Decision, [(ThreadId, Lookahead)], ThreadAction)]
- data Decision
- data Failure
- isInternalError :: Failure -> Bool
- isAbort :: Failure -> Bool
- isDeadlock :: Failure -> Bool
- isUncaughtException :: Failure -> Bool
- isIllegalSubconcurrency :: Failure -> Bool
- isIllegalDontCheck :: Failure -> Bool
- data Bounds = Bounds {}
- newtype PreemptionBound = PreemptionBound Int
- newtype FairBound = FairBound Int
- newtype LengthBound = LengthBound Int
- data Discard
- weakenDiscard :: (Either Failure a -> Maybe Discard) -> (Either Failure a -> Maybe Discard) -> Either Failure a -> Maybe Discard
- strengthenDiscard :: (Either Failure a -> Maybe Discard) -> (Either Failure a -> Maybe Discard) -> Either Failure a -> Maybe Discard
- data MemType
- newtype MonadFailException = MonadFailException String
Identifiers
Every thread has a unique identitifer.
Since: 1.0.0.0
Every CRef has a unique identifier.
Since: 1.0.0.0
Every MVar has a unique identifier.
Since: 1.0.0.0
Every TVar has a unique identifier.
Since: 1.0.0.0
An identifier for a thread, MVar, CRef, or TVar.
The number is the important bit. The string is to make execution traces easier to read, but is meaningless.
Since: 1.0.0.0
initialThread :: ThreadId Source #
The ID of the initial thread.
Since: 0.4.0.0
Actions
data ThreadAction Source #
All the actions that a thread can perform.
Since: 1.4.0.0
Constructors
| Fork ThreadId | Start a new thread. |
| ForkOS ThreadId | Start a new bound thread. |
| IsCurrentThreadBound Bool | Check if the current thread is bound. |
| MyThreadId | Get the |
| GetNumCapabilities Int | Get the number of Haskell threads that can run simultaneously. |
| SetNumCapabilities Int | Set the number of Haskell threads that can run simultaneously. |
| Yield | Yield the current thread. |
| ThreadDelay Int | Yield/delay the current thread. |
| NewMVar MVarId | Create a new |
| PutMVar MVarId [ThreadId] | Put into a |
| BlockedPutMVar MVarId | Get blocked on a put. |
| TryPutMVar MVarId Bool [ThreadId] | Try to put into a |
| ReadMVar MVarId | Read from a |
| TryReadMVar MVarId Bool | Try to read from a |
| BlockedReadMVar MVarId | Get blocked on a read. |
| TakeMVar MVarId [ThreadId] | Take from a |
| BlockedTakeMVar MVarId | Get blocked on a take. |
| TryTakeMVar MVarId Bool [ThreadId] | Try to take from a |
| NewCRef CRefId | Create a new |
| ReadCRef CRefId | Read from a |
| ReadCRefCas CRefId | Read from a |
| ModCRef CRefId | Modify a |
| ModCRefCas CRefId | Modify a |
| WriteCRef CRefId | Write to a |
| CasCRef CRefId Bool | Attempt to to a |
| CommitCRef ThreadId CRefId | Commit the last write to the given |
| STM [TAction] [ThreadId] | An STM transaction was executed, possibly waking up some threads. |
| BlockedSTM [TAction] | Got blocked in an STM transaction. |
| Catching | Register a new exception handler |
| PopCatching | Pop the innermost exception handler from the stack. |
| Throw | Throw an exception. |
| ThrowTo ThreadId | Throw an exception to a thread. |
| BlockedThrowTo ThreadId | Get blocked on a |
| SetMasking Bool MaskingState | Set the masking state. If |
| ResetMasking Bool MaskingState | Return to an earlier masking state. If |
| LiftIO | Lift an IO action. Note that this can only happen with
|
| Return | |
| Stop | Cease execution and terminate. |
| Subconcurrency | Start executing an action with |
| StopSubconcurrency | Stop executing an action with |
| DontCheck Trace | Execute an action with |
Instances
| Eq ThreadAction Source # | |
| Show ThreadAction Source # | |
| Generic ThreadAction Source # | Since: 1.3.1.0 |
| NFData ThreadAction Source # | |
| type Rep ThreadAction Source # | |
A one-step look-ahead at what a thread will do next.
Since: 1.1.0.0
Constructors
| WillFork | Will start a new thread. |
| WillForkOS | Will start a new bound thread. |
| WillIsCurrentThreadBound | Will check if the current thread is bound. |
| WillMyThreadId | Will get the |
| WillGetNumCapabilities | Will get the number of Haskell threads that can run simultaneously. |
| WillSetNumCapabilities Int | Will set the number of Haskell threads that can run simultaneously. |
| WillYield | Will yield the current thread. |
| WillThreadDelay Int | Will yield/delay the current thread. |
| WillNewMVar | Will create a new |
| WillPutMVar MVarId | Will put into a |
| WillTryPutMVar MVarId | Will try to put into a |
| WillReadMVar MVarId | Will read from a |
| WillTryReadMVar MVarId | Will try to read from a |
| WillTakeMVar MVarId | Will take from a |
| WillTryTakeMVar MVarId | Will try to take from a |
| WillNewCRef | Will create a new |
| WillReadCRef CRefId | Will read from a |
| WillReadCRefCas CRefId | Will read from a |
| WillModCRef CRefId | Will modify a |
| WillModCRefCas CRefId | Will modify a |
| WillWriteCRef CRefId | Will write to a |
| WillCasCRef CRefId | Will attempt to to a |
| WillCommitCRef ThreadId CRefId | Will commit the last write by the given thread to the |
| WillSTM | Will execute an STM transaction, possibly waking up some threads. |
| WillCatching | Will register a new exception handler |
| WillPopCatching | Will pop the innermost exception handler from the stack. |
| WillThrow | Will throw an exception. |
| WillThrowTo ThreadId | Will throw an exception to a thread. |
| WillSetMasking Bool MaskingState | Will set the masking state. If |
| WillResetMasking Bool MaskingState | Will return to an earlier masking state. If |
| WillLiftIO | Will lift an IO action. Note that this can only happen with
|
| WillReturn | |
| WillStop | Will cease execution and terminate. |
| WillSubconcurrency | Will execute an action with |
| WillStopSubconcurrency | Will stop executing an extion with |
| WillDontCheck | Will execute an action with |
All the actions that an STM transaction can perform.
Since: 0.8.0.0
Constructors
| TNew TVarId | Create a new |
| TRead TVarId | Read from a |
| TWrite TVarId | Write to a |
| TRetry | Abort and discard effects. |
| TOrElse [TAction] (Maybe [TAction]) | Execute a transaction. If the transaction aborts by calling
|
| TThrow | Throw an exception, abort, and discard effects. |
| TCatch [TAction] (Maybe [TAction]) | Execute a transaction. If the transaction aborts by throwing an exception of the appropriate type, it is handled and execution continues; otherwise aborts, propagating the exception upwards. |
| TStop | Terminate successfully and commit effects. |
Traces
type Trace = [(Decision, [(ThreadId, Lookahead)], ThreadAction)] Source #
One of the outputs of the runner is a Trace, which is a log of
decisions made, all the alternative unblocked threads and what they
would do, and the action a thread took in its step.
Since: 0.8.0.0
Scheduling decisions are based on the state of the running program, and so we can capture some of that state in recording what specific decision we made.
Since: 0.5.0.0
Failures
An indication of how a concurrent computation failed.
The Eq, Ord, and NFData instances compare/evaluate the
exception with show in the UncaughtException case.
Since: 1.1.0.0
Constructors
| InternalError | Will be raised if the scheduler does something bad. This should never arise unless you write your own, faulty, scheduler! If it does, please file a bug report. |
| Abort | The scheduler chose to abort execution. This will be produced if, for example, all possible decisions exceed the specified bounds (there have been too many pre-emptions, the computation has executed for too long, or there have been too many yields). |
| Deadlock | Every thread is blocked, and the main thread is not blocked in an STM transaction. |
| STMDeadlock | Every thread is blocked, and the main thread is blocked in an STM transaction. |
| UncaughtException SomeException | An uncaught exception bubbled to the top of the computation. |
| IllegalSubconcurrency | Calls to |
| IllegalDontCheck | A call to |
isInternalError :: Failure -> Bool Source #
Check if a failure is an InternalError.
Since: 0.9.0.0
isDeadlock :: Failure -> Bool Source #
Check if a failure is a Deadlock or an STMDeadlock.
Since: 0.9.0.0
isUncaughtException :: Failure -> Bool Source #
Check if a failure is an UncaughtException
Since: 0.9.0.0
isIllegalSubconcurrency :: Failure -> Bool Source #
Check if a failure is an IllegalSubconcurrency
Since: 0.9.0.0
isIllegalDontCheck :: Failure -> Bool Source #
Check if a failure is an IllegalDontCheck
Since: 1.1.0.0
Schedule bounding
Since: 0.2.0.0
Constructors
| Bounds | |
Fields | |
newtype PreemptionBound Source #
Restrict the number of pre-emptive context switches allowed in an execution.
A pre-emption bound of zero disables pre-emptions entirely.
Since: 0.2.0.0
Constructors
| PreemptionBound Int |
Instances
| Enum PreemptionBound Source # | |
| Eq PreemptionBound Source # | |
| Integral PreemptionBound Source # | |
| Num PreemptionBound Source # | |
| Ord PreemptionBound Source # | |
| Read PreemptionBound Source # | |
| Real PreemptionBound Source # | |
| Show PreemptionBound Source # | |
| Generic PreemptionBound Source # | Since: 1.3.1.0 |
| NFData PreemptionBound Source # | Since: 0.5.1.0 |
| type Rep PreemptionBound Source # | |
Restrict the maximum difference between the number of yield or delay operations different threads have performed.
A fair bound of zero disables yields and delays entirely.
Since: 0.2.0.0
Instances
| Enum FairBound Source # | |
| Eq FairBound Source # | |
| Integral FairBound Source # | |
| Num FairBound Source # | |
| Ord FairBound Source # | |
| Read FairBound Source # | |
| Real FairBound Source # | |
| Show FairBound Source # | |
| Generic FairBound Source # | Since: 1.3.1.0 |
| NFData FairBound Source # | Since: 0.5.1.0 |
| type Rep FairBound Source # | |
newtype LengthBound Source #
Restrict the maximum length (in terms of primitive actions) of an execution.
A length bound of zero immediately aborts the execution.
Since: 0.2.0.0
Constructors
| LengthBound Int |
Instances
| Enum LengthBound Source # | |
| Eq LengthBound Source # | |
| Integral LengthBound Source # | |
| Num LengthBound Source # | |
| Ord LengthBound Source # | |
| Read LengthBound Source # | |
| Real LengthBound Source # | |
| Show LengthBound Source # | |
| Generic LengthBound Source # | Since: 1.3.1.0 |
| NFData LengthBound Source # | Since: 0.5.1.0 |
| type Rep LengthBound Source # | |
Discarding results and traces
An Either Failure a -> Maybe Discard value can be used to
selectively discard results.
Since: 0.7.1.0
Constructors
| DiscardTrace | Discard the trace but keep the result. The result will appear to have an empty trace. |
| DiscardResultAndTrace | Discard the result and the trace. It will simply not be reported as a possible behaviour of the program. |
weakenDiscard :: (Either Failure a -> Maybe Discard) -> (Either Failure a -> Maybe Discard) -> Either Failure a -> Maybe Discard Source #
Combine two discard values, keeping the weaker.
Nothing is weaker than Just DiscardTrace, which is weaker than
Just DiscardResultAndTrace. This forms a commutative monoid
where the unit is const (Just DiscardResultAndTrace).
Since: 1.0.0.0
strengthenDiscard :: (Either Failure a -> Maybe Discard) -> (Either Failure a -> Maybe Discard) -> Either Failure a -> Maybe Discard Source #
Combine two discard functions, keeping the stronger.
Just DiscardResultAndTrace is stronger than Just DiscardTrace,
which is stronger than Nothing. This forms a commutative monoid
where the unit is const Nothing.
Since: 1.0.0.0
Memory Models
The memory model to use for non-synchronised CRef operations.
Since: 0.4.0.0
Constructors
| SequentialConsistency | The most intuitive model: a program behaves as a simple
interleaving of the actions in different threads. When a |
| TotalStoreOrder | Each thread has a write buffer. A thread sees its writes immediately, but other threads will only see writes when they are committed, which may happen later. Writes are committed in the same order that they are created. |
| PartialStoreOrder | Each |
MonadFail
newtype MonadFailException Source #
An exception for errors in testing caused by use of fail.
Constructors
| MonadFailException String |
Instances
| Show MonadFailException Source # | |
| Generic MonadFailException Source # | Since: 1.3.1.0 |
| Exception MonadFailException Source # | |
| NFData MonadFailException Source # | Since: 1.3.1.0 |
| type Rep MonadFailException Source # | |