Copyright | (c) 2016 Michael Walker |
---|---|
License | MIT |
Maintainer | Michael Walker <mike@barrucadu.co.uk> |
Stability | experimental |
Portability | FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, RankNTypes, TypeFamilies, TypeSynonymInstances |
Safe Haskell | None |
Language | Haskell2010 |
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 Conc n r s a
- type ConcST t = Conc (ST t) (STRef t) (STMST t)
- type ConcIO = Conc IO IORef STMIO
- data Failure
- data MemType
- runConcST :: Scheduler ThreadId ThreadAction Lookahead s -> MemType -> s -> (forall t. ConcST t a) -> (Either Failure a, s, Trace ThreadId ThreadAction Lookahead)
- runConcIO :: Scheduler ThreadId ThreadAction Lookahead s -> MemType -> s -> ConcIO a -> IO (Either Failure a, s, Trace ThreadId ThreadAction Lookahead)
- type Trace tid action lookahead = [(Decision tid, [(tid, NonEmpty lookahead)], action)]
- data Decision tid :: * -> *
- data ThreadId = ThreadId (Maybe String) Int
- data ThreadAction
- = Fork ThreadId
- | MyThreadId
- | GetNumCapabilities Int
- | SetNumCapabilities Int
- | Yield
- | NewVar MVarId
- | PutVar MVarId [ThreadId]
- | BlockedPutVar MVarId
- | TryPutVar MVarId Bool [ThreadId]
- | ReadVar MVarId
- | BlockedReadVar MVarId
- | TakeVar MVarId [ThreadId]
- | BlockedTakeVar MVarId
- | TryTakeVar MVarId Bool [ThreadId]
- | NewRef CRefId
- | ReadRef CRefId
- | ReadRefCas CRefId
- | PeekTicket CRefId
- | ModRef CRefId
- | ModRefCas CRefId
- | WriteRef CRefId
- | CasRef CRefId Bool
- | CommitRef ThreadId CRefId
- | STM TTrace [ThreadId]
- | BlockedSTM TTrace
- | Catching
- | PopCatching
- | Throw
- | ThrowTo ThreadId
- | BlockedThrowTo ThreadId
- | Killed
- | SetMasking Bool MaskingState
- | ResetMasking Bool MaskingState
- | Lift
- | Return
- | KnowsAbout
- | Forgets
- | AllKnown
- | Message Dynamic
- | Stop
- data Lookahead
- = WillFork
- | WillMyThreadId
- | WillGetNumCapabilities
- | WillSetNumCapabilities Int
- | WillYield
- | WillNewVar
- | WillPutVar MVarId
- | WillTryPutVar MVarId
- | WillReadVar MVarId
- | WillTakeVar MVarId
- | WillTryTakeVar MVarId
- | WillNewRef
- | WillReadRef CRefId
- | WillPeekTicket CRefId
- | WillReadRefCas CRefId
- | WillModRef CRefId
- | WillModRefCas CRefId
- | WillWriteRef CRefId
- | WillCasRef CRefId
- | WillCommitRef ThreadId CRefId
- | WillSTM
- | WillCatching
- | WillPopCatching
- | WillThrow
- | WillThrowTo ThreadId
- | WillSetMasking Bool MaskingState
- | WillResetMasking Bool MaskingState
- | WillLift
- | WillReturn
- | WillKnowsAbout
- | WillForgets
- | WillAllKnown
- | WillMessage Dynamic
- | WillStop
- data MVarId
- data CRefId
- data MaskingState :: *
- showTrace :: Trace ThreadId ThreadAction Lookahead -> String
- showFail :: Failure -> String
- module Test.DPOR.Schedule
The Conc
Monad
MonadIO ConcIO Source # | |
MonadBase IO ConcIO Source # | |
Monad (Conc n r s) Source # | |
Functor (Conc n r s) Source # | |
Applicative (Conc n r s) Source # | |
MonadThrow (Conc n r s) Source # | |
MonadCatch (Conc n r s) Source # | |
MonadMask (Conc n r s) Source # | |
Monad n => MonadConc (Conc n r (STMLike n r)) Source # | |
type STM (Conc n r (STMLike n r)) Source # | |
type MVar (Conc n r (STMLike n r)) Source # | |
type CRef (Conc n r (STMLike n r)) Source # | |
type Ticket (Conc n r (STMLike n r)) Source # | |
type ThreadId (Conc n r (STMLike n r)) Source # | |
type ConcST t = Conc (ST t) (STRef t) (STMST t) Source #
A MonadConc
implementation using ST
, this should be preferred
if you do not need liftIO
.
Executing computations
An indication of how a concurrent computation failed.
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 | The computation became blocked indefinitely on |
STMDeadlock | The computation became blocked indefinitely on |
UncaughtException | An uncaught exception bubbled to the top of the computation. |
The memory model to use for non-synchronised CRef
operations.
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 |
runConcST :: Scheduler ThreadId ThreadAction Lookahead s -> MemType -> s -> (forall t. ConcST t a) -> (Either Failure a, s, Trace ThreadId ThreadAction Lookahead) 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.
Note how the t
in Conc
is universally quantified, what this
means in practice is that you can't do something like this:
runConc roundRobinSched SequentialConsistency () newEmptyMVar
So mutable references cannot leak out of the Conc
computation. If
this is making your head hurt, check out the "How runST
works"
section of
https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html
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.
runConcIO :: Scheduler ThreadId ThreadAction Lookahead s -> MemType -> s -> ConcIO a -> IO (Either Failure a, s, Trace ThreadId ThreadAction Lookahead) Source #
Run a concurrent computation in the IO
monad 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.
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.
Execution traces
type Trace tid action lookahead = [(Decision tid, [(tid, NonEmpty lookahead)], action)] #
One of the outputs of the runner is a Trace
, which is a log of
decisions made, all the runnable threads and what they would do,
and the action a thread took in its step.
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.
Every live thread has a unique identitifer.
data ThreadAction Source #
All the actions that a thread can perform.
Fork ThreadId | Start a new thread. |
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. |
NewVar MVarId | Create a new |
PutVar MVarId [ThreadId] | Put into a |
BlockedPutVar MVarId | Get blocked on a put. |
TryPutVar MVarId Bool [ThreadId] | Try to put into a |
ReadVar MVarId | Read from a |
BlockedReadVar MVarId | Get blocked on a read. |
TakeVar MVarId [ThreadId] | Take from a |
BlockedTakeVar MVarId | Get blocked on a take. |
TryTakeVar MVarId Bool [ThreadId] | Try to take from a |
NewRef CRefId | Create a new |
ReadRef CRefId | Read from a |
ReadRefCas CRefId | Read from a |
PeekTicket CRefId | Extract the value from a |
ModRef CRefId | Modify a |
ModRefCas CRefId | Modify a |
WriteRef CRefId | Write to a |
CasRef CRefId Bool | Attempt to to a |
CommitRef ThreadId CRefId | Commit the last write to the given |
STM TTrace [ThreadId] | An STM transaction was executed, possibly waking up some threads. |
BlockedSTM TTrace | 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 |
Killed | Killed by an uncaught exception. |
SetMasking Bool MaskingState | Set the masking state. If |
ResetMasking Bool MaskingState | Return to an earlier masking state. If |
Lift | Lift an action from the underlying monad. Note that the
penultimate action in a trace will always be a |
Return | |
KnowsAbout | A |
Forgets | A |
AllKnown | A |
Message Dynamic | A |
Stop | Cease execution and terminate. |
A one-step look-ahead at what a thread will do next.
WillFork | Will start a new thread. |
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. |
WillNewVar | Will create a new |
WillPutVar MVarId | Will put into a |
WillTryPutVar MVarId | Will try to put into a |
WillReadVar MVarId | Will read from a |
WillTakeVar MVarId | Will take from a |
WillTryTakeVar MVarId | Will try to take from a |
WillNewRef | Will create a new |
WillReadRef CRefId | Will read from a |
WillPeekTicket CRefId | Will extract the value from a |
WillReadRefCas CRefId | Will read from a |
WillModRef CRefId | Will modify a |
WillModRefCas CRefId | Will nodify a |
WillWriteRef CRefId | Will write to a |
WillCasRef CRefId | Will attempt to to a |
WillCommitRef 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 |
WillLift | Will lift an action from the underlying monad. Note that the
penultimate action in a trace will always be a |
WillReturn | |
WillKnowsAbout | Will process a |
WillForgets | Will process a |
WillAllKnown | Will process a |
WillMessage Dynamic | Will process a _concMessage' annotation. |
WillStop | Will cease execution and terminate. |
Every MVar
has a unique identifier.
Every CRef
has a unique identifier.
data MaskingState :: * #
Describes the behaviour of a thread when an asynchronous exception is received.
Unmasked | asynchronous exceptions are unmasked (the normal state) |
MaskedInterruptible | the state during |
MaskedUninterruptible | the state during |
showTrace :: Trace ThreadId ThreadAction Lookahead -> String Source #
Pretty-print a trace, including a key of the thread IDs. Each line of the key is indented by two spaces.
Scheduling
module Test.DPOR.Schedule