Copyright | (c) 2017--2018 Michael Walker |
---|---|
License | MIT |
Maintainer | Michael Walker <mike@barrucadu.co.uk> |
Stability | experimental |
Portability | DeriveAnyClass, DeriveGeneric, FlexibleContexts, GADTs |
Safe Haskell | None |
Language | Haskell2010 |
Internal types and functions used throughout DejaFu. This module is NOT considered to form part of the public interface of this library.
- data Settings n a = Settings {}
- data Way where
- data IdSource = IdSource {}
- nextCRId :: String -> IdSource -> (IdSource, CRefId)
- nextMVId :: String -> IdSource -> (IdSource, MVarId)
- nextTVId :: String -> IdSource -> (IdSource, TVarId)
- nextTId :: String -> IdSource -> (IdSource, ThreadId)
- nextId :: String -> (Int, [String]) -> (Id, (Int, [String]))
- initialIdSource :: IdSource
- isBlock :: ThreadAction -> Bool
- tvarsOf :: ThreadAction -> Set TVarId
- tvarsWritten :: ThreadAction -> Set TVarId
- tvarsRead :: ThreadAction -> Set TVarId
- rewind :: ThreadAction -> 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
- tidsOf :: ThreadAction -> Set ThreadId
- simplifyAction :: ThreadAction -> ActionType
- simplifyLookahead :: Lookahead -> ActionType
- etail :: HasCallStack => [a] -> [a]
- eidx :: HasCallStack => [a] -> Int -> a
- efromJust :: HasCallStack => Maybe a -> a
- efromList :: HasCallStack => [a] -> NonEmpty a
- eadjust :: (Ord k, Show k, HasCallStack) => (v -> v) -> k -> Map k v -> Map k v
- einsert :: (Ord k, Show k, HasCallStack) => k -> v -> Map k v -> Map k v
- elookup :: (Ord k, Show k, HasCallStack) => k -> Map k v -> v
- fatal :: HasCallStack => String -> a
- runRefCont :: MonadConc n => (n () -> x) -> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, CRef n (Maybe b))
SCT settings
SCT configuration record.
Since: 1.2.0.0
How to explore the possible executions of a concurrent program.
Since: 0.7.0.0
Identifiers
The number of ID parameters was getting a bit unwieldy, so this hides them all away.
initialIdSource :: IdSource Source #
The initial ID source.
Actions
isBlock :: ThreadAction -> Bool Source #
Check if a ThreadAction
immediately blocks.
tvarsWritten :: ThreadAction -> Set TVarId Source #
Get the TVar
s a transaction wrote to (or would have, if it
didn't retry
).
rewind :: ThreadAction -> Lookahead Source #
Convert a ThreadAction
into a Lookahead
: "rewind" what has
happened.
willRelease :: Lookahead -> Bool Source #
Check if an operation could enable another thread.
Simplified actions
data ActionType Source #
A simplified view of the possible actions a thread can perform.
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. |
isBarrier :: ActionType -> Bool Source #
Check if an action imposes a write barrier.
synchronises :: ActionType -> CRefId -> Bool Source #
Check if an action synchronises a given CRef
.
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.
simplifyLookahead :: Lookahead -> ActionType Source #
Variant of simplifyAction
that takes a Lookahead
.
Error reporting
etail :: HasCallStack => [a] -> [a] Source #
tail
but with a better error message if it fails. Use this
only where it shouldn't fail!
eidx :: HasCallStack => [a] -> Int -> a Source #
'(!!)' but with a better error message if it fails. Use this only where it shouldn't fail!
efromJust :: HasCallStack => Maybe a -> a Source #
fromJust
but with a better error message if it fails. Use this
only where it shouldn't fail!
efromList :: HasCallStack => [a] -> NonEmpty a Source #
fromList
but with a better error message if it fails. Use this
only where it shouldn't fail!
eadjust :: (Ord k, Show k, HasCallStack) => (v -> v) -> k -> Map k v -> Map k v Source #
adjust
but which errors if the key is not present. Use this
only where it shouldn't fail!
einsert :: (Ord k, Show k, HasCallStack) => k -> v -> Map k v -> Map k v Source #
insert
but which errors if the key is already present. Use
this only where it shouldn't fail!
elookup :: (Ord k, Show k, HasCallStack) => k -> Map k v -> v Source #
lookup
but which errors if the key is not present. Use this
only where it shouldn't fail!
Miscellaneous
runRefCont :: MonadConc n => (n () -> x) -> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, CRef n (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.