Copyright | (c) 2016 Michael Walker |
---|---|
License | MIT |
Maintainer | Michael Walker <mike@barrucadu.co.uk> |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell2010 |
Common types and functions used throughout DejaFu.
- data ThreadId = ThreadId (Maybe String) !Int
- data CRefId = CRefId (Maybe String) !Int
- data MVarId = MVarId (Maybe String) !Int
- data TVarId = TVarId (Maybe String) !Int
- initialThread :: ThreadId
- data IdSource = Id {
- _nextCRId :: Int
- _nextMVId :: Int
- _nextTVId :: Int
- _nextTId :: Int
- _usedCRNames :: [String]
- _usedMVNames :: [String]
- _usedTVNames :: [String]
- _usedTNames :: [String]
- nextCRId :: String -> IdSource -> (IdSource, CRefId)
- nextMVId :: String -> IdSource -> (IdSource, MVarId)
- nextTVId :: String -> IdSource -> (IdSource, TVarId)
- nextTId :: String -> IdSource -> (IdSource, ThreadId)
- initialIdSource :: IdSource
- data ThreadAction
- = Fork ThreadId
- | MyThreadId
- | GetNumCapabilities Int
- | SetNumCapabilities Int
- | Yield
- | 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 TTrace [ThreadId]
- | BlockedSTM TTrace
- | Catching
- | PopCatching
- | Throw
- | ThrowTo ThreadId
- | BlockedThrowTo ThreadId
- | Killed
- | SetMasking Bool MaskingState
- | ResetMasking Bool MaskingState
- | LiftIO
- | Return
- | Stop
- | Subconcurrency
- | StopSubconcurrency
- isBlock :: ThreadAction -> Bool
- tvarsOf :: ThreadAction -> Set TVarId
- data Lookahead
- = WillFork
- | WillMyThreadId
- | WillGetNumCapabilities
- | WillSetNumCapabilities Int
- | WillYield
- | 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
- rewind :: ThreadAction -> Maybe Lookahead
- willRelease :: Lookahead -> Bool
- data ActionType
- isBarrier :: ActionType -> Bool
- isCommit :: ActionType -> CRefId -> Bool
- synchronises :: ActionType -> CRefId -> Bool
- crefOf :: ActionType -> Maybe CRefId
- mvarOf :: ActionType -> Maybe MVarId
- simplifyAction :: ThreadAction -> ActionType
- simplifyLookahead :: Lookahead -> ActionType
- type TTrace = [TAction]
- data TAction
- type Trace = [(Decision, [(ThreadId, Lookahead)], ThreadAction)]
- data Decision
- showTrace :: Trace -> String
- threadNames :: Trace -> [(Int, String)]
- preEmpCount :: [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Int
- data Failure
- showFail :: Failure -> String
- data MemType
- newtype MonadFailException = MonadFailException String
- runRefCont :: MonadRef r n => (n () -> x) -> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, r (Maybe b))
Identifiers
Every live thread has a unique identitifer.
The Eq
and Ord
instances only consider the int, not the name.
Since: 0.4.0.0
Every CRef
has a unique identifier.
The Eq
and Ord
instances only consider the int, not the name.
Since: 0.4.0.0
Every MVar
has a unique identifier.
The Eq
and Ord
instances only consider the int, not the name.
Since: 0.4.0.0
Every TVar
has a unique identifier.
The Eq
and Ord
instances only consider the int, not the name.
Since: 0.4.0.0
initialThread :: ThreadId Source #
The ID of the initial thread.
Since: 0.4.0.0
Identifier source
The number of ID parameters was getting a bit unwieldy, so this hides them all away.
Since: 0.4.0.0
Id | |
|
nextCRId :: String -> IdSource -> (IdSource, CRefId) Source #
Get the next free CRefId
.
Since: 0.4.0.0
nextMVId :: String -> IdSource -> (IdSource, MVarId) Source #
Get the next free MVarId
.
Since: 0.4.0.0
nextTVId :: String -> IdSource -> (IdSource, TVarId) Source #
Get the next free TVarId
.
Since: 0.4.0.0
nextTId :: String -> IdSource -> (IdSource, ThreadId) Source #
Get the next free ThreadId
.
Since: 0.4.0.0
initialIdSource :: IdSource Source #
The initial ID source.
Since: 0.4.0.0
Actions
Thread actions
data ThreadAction Source #
All the actions that a thread can perform.
Since: 0.5.0.2
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. |
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 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 |
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 |
Eq ThreadAction Source # | |
Show ThreadAction Source # | |
NFData ThreadAction Source # | Since: 0.5.1.0 |
isBlock :: ThreadAction -> Bool Source #
Check if a ThreadAction
immediately blocks.
Since: 0.4.0.0
tvarsOf :: ThreadAction -> Set TVarId Source #
Get the TVar
s affected by a ThreadAction
.
Since: 0.4.0.0
Lookahead
A one-step look-ahead at what a thread will do next.
Since: 0.5.0.2
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. |
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 |
rewind :: ThreadAction -> Maybe Lookahead Source #
Convert a ThreadAction
into a Lookahead
: "rewind" what has
happened. Killed
has no Lookahead
counterpart.
Since: 0.4.0.0
willRelease :: Lookahead -> Bool Source #
Check if an operation could enable another thread.
Since: 0.4.0.0
Simplified actions
data ActionType Source #
A simplified view of the possible actions a thread can perform.
Since: 0.4.0.0
UnsynchronisedRead CRefId | A |
UnsynchronisedWrite CRefId | A |
UnsynchronisedOther | Some other action which doesn't require cross-thread communication. |
PartiallySynchronisedCommit CRefId | A commit. |
PartiallySynchronisedWrite CRefId | A |
PartiallySynchronisedModify CRefId | A |
SynchronisedModify CRefId | An |
SynchronisedRead MVarId | A |
SynchronisedWrite MVarId | A |
SynchronisedOther | Some other action which does require cross-thread communication. |
Eq ActionType Source # | |
Show ActionType Source # | |
NFData ActionType Source # | Since: 0.5.1.0 |
isBarrier :: ActionType -> Bool Source #
Check if an action imposes a write barrier.
Since: 0.4.0.0
isCommit :: ActionType -> CRefId -> Bool Source #
Check if an action commits a given CRef
.
Since: 0.4.0.0
synchronises :: ActionType -> CRefId -> Bool Source #
Check if an action synchronises a given CRef
.
Since: 0.4.0.0
simplifyAction :: ThreadAction -> ActionType Source #
Throw away information from a ThreadAction
and give a
simplified view of what is happening.
This is used in the SCT code to help determine interesting alternative scheduling decisions.
Since: 0.4.0.0
simplifyLookahead :: Lookahead -> ActionType Source #
Variant of simplifyAction
that takes a Lookahead
.
Since: 0.4.0.0
STM actions
type TTrace = [TAction] Source #
A trace of an STM transaction is just a list of actions that occurred, as there are no scheduling decisions to make.
Since: 0.4.0.0
All the actions that an STM transaction can perform.
Since: 0.8.0.0
TNew TVarId | Create a new |
TRead TVarId | Read from a |
TWrite TVarId | Write to a |
TRetry | Abort and discard effects. |
TOrElse TTrace (Maybe TTrace) | Execute a transaction until it succeeds ( |
TThrow | Throw an exception, abort, and discard effects. |
TCatch TTrace (Maybe TTrace) | Execute a transaction until it succeeds ( |
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 runnable 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
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
preEmpCount :: [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Int Source #
Count the number of pre-emptions in a schedule prefix.
Commit threads complicate this a bit. Conceptually, commits are happening truly in parallel, nondeterministically. The commit thread implementation is just there to unify the two sources of nondeterminism: commit timing and thread scheduling.
SO, we don't count a switch TO a commit thread as a preemption. HOWEVER, the switch FROM a commit thread counts as a preemption if it is not to the thread that the commit interrupted.
Since: 0.5.0.0
Failures
An indication of how a concurrent computation failed.
Since: 0.5.0.0
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. |
IllegalSubconcurrency | Calls to |
Memory models
The memory model to use for non-synchronised CRef
operations.
Since: 0.4.0.0
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 |
Miscellaneous
newtype MonadFailException Source #
An exception for errors in testing caused by use of fail
.
runRefCont :: MonadRef r n => (n () -> x) -> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, r (Maybe b)) Source #
Run with a continuation that writes its value into a reference, returning the computation and the reference. Using the reference is non-blocking, it is up to you to ensure you wait sufficiently.