| Copyright | (c) 2016--2018 Michael Walker |
|---|---|
| License | MIT |
| Maintainer | Michael Walker <mike@barrucadu.co.uk> |
| Stability | experimental |
| Portability | CPP, FlexibleInstances, GeneralizedNewtypeDeriving, TypeFamilies |
| Safe Haskell | None |
| Language | Haskell2010 |
Test.DejaFu.Conc
Description
Deterministic traced execution of concurrent computations.
This works by executing the computation on a single thread, calling out to the supplied scheduler after each step to determine which thread runs next.
- data ConcT n a
- type ConcIO = ConcT IO
- data Failure
- data MemType
- runConcurrent :: MonadConc n => Scheduler s -> MemType -> s -> ConcT n a -> n (Either Failure a, s, Trace)
- subconcurrency :: ConcT n a -> ConcT n (Either Failure a)
- dontCheck :: Maybe Int -> ConcT n a -> ConcT n a
- data DCSnapshot n a
- runForDCSnapshot :: MonadConc n => ConcT n a -> n (Maybe (Either Failure (DCSnapshot n a), Trace))
- runWithDCSnapshot :: MonadConc n => Scheduler s -> MemType -> s -> DCSnapshot n a -> n (Either Failure a, s, Trace)
- canDCSnapshot :: ConcT n a -> Bool
- threadsFromDCSnapshot :: DCSnapshot n a -> ([ThreadId], [ThreadId])
- type Trace = [(Decision, [(ThreadId, Lookahead)], ThreadAction)]
- data Decision
- newtype ThreadId = ThreadId Id
- 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 Bool
- | ThrowTo ThreadId Bool
- | 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 MVarId
- data CRefId
- data MaskingState :: *
- showTrace :: Trace -> String
- showFail :: Failure -> String
- module Test.DejaFu.Schedule
The ConcT monad transformer
Since: 1.4.0.0
Instances
| MonadTrans ConcT Source # | |
| Monad (ConcT n) Source # | |
| Functor (ConcT n) Source # | |
| MonadFail (ConcT n) Source # | |
| Applicative (ConcT n) Source # | |
| MonadIO n => MonadIO (ConcT n) Source # | Since: 1.0.0.0 |
| Monad n => MonadConc (ConcT n) Source # | |
| MonadThrow (ConcT n) Source # | |
| MonadCatch (ConcT n) Source # | |
| MonadMask (ConcT n) Source # | |
| type ThreadId (ConcT n) Source # | |
| type Ticket (ConcT n) Source # | |
| type CRef (ConcT n) Source # | |
| type MVar (ConcT n) Source # | |
| type STM (ConcT n) Source # | |
Executing computations
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 |
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 |
runConcurrent :: MonadConc n => Scheduler s -> MemType -> s -> ConcT n a -> n (Either Failure a, s, Trace) Source #
Run a concurrent computation with a given Scheduler and initial
state, returning a failure reason on error. Also returned is the
final state of the scheduler, and an execution trace.
If the RTS supports bound threads (ghc -threaded when linking) then
the main thread of the concurrent computation will be bound, and
forkOS / forkOSN will work during execution. If not, then the
main thread will not be found, and attempting to fork a bound
thread will raise an error.
Warning: Blocking on the action of another thread in liftIO
cannot be detected! So if you perform some potentially blocking
action in a liftIO the entire collection of threads may deadlock!
You should therefore keep IO blocks small, and only perform
blocking operations with the supplied primitives, insofar as
possible.
Note: In order to prevent computation from hanging, the runtime will assume that a deadlock situation has arisen if the scheduler attempts to (a) schedule a blocked thread, or (b) schedule a nonexistent thread. In either of those cases, the computation will be halted.
Since: 1.0.0.0
subconcurrency :: ConcT n a -> ConcT n (Either Failure a) Source #
Run a concurrent computation and return its result.
This can only be called in the main thread, when no other threads
exist. Calls to subconcurrency cannot be nested, or placed inside
a call to dontCheck. Violating either of these conditions will
result in the computation failing with IllegalSubconcurrency.
The overall test-case can still succeed if the predicate allows for
a failing computation.
Since: 0.6.0.0
Run an arbitrary action which gets some special treatment:
- For systematic testing,
dontCheckis not dependent with anything, even if the action has dependencies. - For pre-emption bounding,
dontCheckcounts for zero pre-emptions, even if the action performs pre-emptive context switches. - For fair bounding,
dontCheckcounts for zero yields/delays, even if the action performs yields or delays. - For length bounding,
dontCheckcounts for one step, even if the action has many. - All SCT functions use
runForDCSnapshot/runWithDCSnapshotto ensure that the action is only executed once, although you should be careful withIO(see note on snapshottingIO).
The action is executed atomically with a deterministic scheduler under sequential consistency. Any threads created inside the action continue to exist in the main computation.
This must be the first thing done in the main thread. Violating
this condition will result in the computation failing with
IllegalDontCheck. The overall test-case can still succeed if the
predicate allows for a failing computation.
If the action fails (deadlock, length bound exceeded, etc), the whole computation fails.
Since: 1.1.0.0
Snapshotting
Snapshotting IO: A snapshot captures entire state of your
concurrent program: the state of every thread, the number of
capabilities, the values of any CRefs, MVars, and TVars, and
records any IO that you performed.
When restoring a snapshot this IO is replayed, in order. But the
whole snapshotted computation is not. So the effects of the IO
take place again, but any return values are ignored. For example,
this program will not do what you want:
bad_snapshot = do
r <- dontCheck Nothing $ do
r <- liftIO (newIORef 0)
liftIO (modifyIORef r (+1))
pure r
liftIO (readIORef r)
When the snapshot is taken, the value in the IORef will be 1.
When the snapshot is restored for the first time, those IO
actions will be run again, but their return values will be discarded.
The value in the IORef will be 2. When the snapshot
is restored for the second time, the value in the IORef will be
3. And so on.
To safely use IO in a snapshotted computation, the combined effect must be idempotent.
You should either use actions which set the state to the final
value directly, rather than modifying it (eg, using a combination
of liftIO . readCRef and liftIO . writeIORef here), or reset
the state to a known value. Both of these approaches will work:
good_snapshot1 = do
r <- dontCheck Nothing $ do
let modify r f = liftIO (readIORef r) >>= liftIO . writeIORef r . f
r <- liftIO (newIORef 0)
modify r (+1)
pure r
liftIO (readIORef r)
good_snapshot2 = do
r <- dontCheck Nothing $ do
r <- liftIO (newIORef 0)
liftIO (writeIORef r 0)
liftIO (modifyIORef r (+1))
pure r
liftIO (readIORef r)
data DCSnapshot n a Source #
A snapshot of the concurrency state immediately after dontCheck
finishes.
Since: 1.4.0.0
runForDCSnapshot :: MonadConc n => ConcT n a -> n (Maybe (Either Failure (DCSnapshot n a), Trace)) Source #
Like runConcurrent, but terminates immediately after running
the dontCheck action with a DCSnapshot which can be used in
runWithDCSnapshot to avoid doing that work again.
If this program does not contain a legal use of dontCheck, then
the result will be Nothing.
If you are using the SCT functions on an action which contains a
dontCheck, snapshotting will be handled for you, without you
needing to call this function yourself.
Since: 1.1.0.0
runWithDCSnapshot :: MonadConc n => Scheduler s -> MemType -> s -> DCSnapshot n a -> n (Either Failure a, s, Trace) Source #
Like runConcurrent, but uses a DCSnapshot produced by
runForDCSnapshot to skip the dontCheck work.
If you are using the SCT functions on an action which contains a
dontCheck, snapshotting will be handled for you, without you
needing to call this function yourself.
Since: 1.1.0.0
canDCSnapshot :: ConcT n a -> Bool Source #
Check if a DCSnapshot can be taken from this computation.
Since: 1.1.0.0
threadsFromDCSnapshot :: DCSnapshot n a -> ([ThreadId], [ThreadId]) Source #
Get the threads which exist in a snapshot, partitioned into runnable and not runnable.
Since: 1.1.0.0
Execution 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
Every thread has a unique identitifer.
Since: 1.0.0.0
data ThreadAction Source #
All the actions that a thread can perform.
Since: 1.9.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 Bool | Throw an exception. If the |
| ThrowTo ThreadId Bool | Throw an exception to a thread. If the |
| 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 |
Every MVar has a unique identifier.
Since: 1.0.0.0
Every CRef has a unique identifier.
Since: 1.0.0.0
data MaskingState :: * #
Describes the behaviour of a thread when an asynchronous exception is received.
Constructors
| Unmasked | asynchronous exceptions are unmasked (the normal state) |
| MaskedInterruptible | the state during |
| MaskedUninterruptible | the state during |
Instances
showTrace :: Trace -> String Source #
Pretty-print a trace, including a key of the thread IDs (not including thread 0). Each line of the key is indented by two spaces.
Since: 0.5.0.0
Scheduling
module Test.DejaFu.Schedule