Copyright | (c) 2017--2020 Michael Walker |
---|---|
License | MIT |
Maintainer | Michael Walker <mike@barrucadu.co.uk> |
Stability | experimental |
Portability | DeriveAnyClass, DeriveGeneric, FlexibleContexts, GADTs, LambdaCase |
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.
Synopsis
- data Settings n a = Settings {
- _way :: Way
- _lengthBound :: Maybe LengthBound
- _memtype :: MemType
- _discard :: Maybe (Either Condition a -> Maybe Discard)
- _debugShow :: Maybe (a -> String)
- _debugPrint :: Maybe (String -> n ())
- _debugFatal :: Bool
- _earlyExit :: Maybe (Either Condition a -> Bool)
- _equality :: Maybe (a -> a -> Bool)
- _simplify :: Bool
- _safeIO :: Bool
- _showAborts :: Bool
- data Way where
- data IdSource = IdSource {}
- nextIORId :: String -> IdSource -> (IdSource, IORefId)
- 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 -> IORefId -> Bool
- synchronises :: ActionType -> IORefId -> Bool
- iorefOf :: ActionType -> Maybe IORefId
- mvarOf :: ActionType -> Maybe MVarId
- tidsOf :: ThreadAction -> Set ThreadId
- simplifyAction :: ThreadAction -> ActionType
- simplifyLookahead :: Lookahead -> ActionType
- initialCState :: ConcurrencyState
- updateCState :: MemType -> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
- updateIOState :: MemType -> ThreadAction -> Map IORefId Int -> Map IORefId Int
- updateMVState :: ThreadAction -> Set MVarId -> Set MVarId
- updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState
- etail :: HasCallStack => [a] -> [a]
- eidx :: HasCallStack => [a] -> Int -> a
- efromJust :: HasCallStack => Maybe a -> a
- efromList :: HasCallStack => [a] -> NonEmpty a
- efromRight :: HasCallStack => Either a b -> b
- efromLeft :: HasCallStack => Either a b -> 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 :: MonadDejaFu n => (n () -> x) -> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, Ref n (Maybe b))
SCT settings
SCT configuration record.
Since: 1.2.0.0
Settings | |
|
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.
Instances
Eq IdSource Source # | |
Ord IdSource Source # | |
Defined in Test.DejaFu.Internal | |
Show IdSource Source # | |
Generic IdSource Source # | |
NFData IdSource Source # | |
Defined in Test.DejaFu.Internal | |
type Rep IdSource Source # | |
Defined in Test.DejaFu.Internal type Rep IdSource = D1 ('MetaData "IdSource" "Test.DejaFu.Internal" "dejafu-2.4.0.3-3mGbtTqSt0UArHQ7j0hezX" 'False) (C1 ('MetaCons "IdSource" 'PrefixI 'True) ((S1 ('MetaSel ('Just "_iorids") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Int, [String])) :*: S1 ('MetaSel ('Just "_mvids") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Int, [String]))) :*: (S1 ('MetaSel ('Just "_tvids") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Int, [String])) :*: S1 ('MetaSel ('Just "_tids") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Int, [String]))))) |
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 IORefId | A |
UnsynchronisedWrite IORefId | A |
UnsynchronisedOther | Some other action which doesn't require cross-thread communication. |
PartiallySynchronisedCommit IORefId | A commit. |
PartiallySynchronisedWrite IORefId | A |
PartiallySynchronisedModify IORefId | A |
SynchronisedModify IORefId | An |
SynchronisedRead MVarId | A |
SynchronisedWrite MVarId | A |
SynchronisedOther | Some other action which does require cross-thread communication. |
Instances
isBarrier :: ActionType -> Bool Source #
Check if an action imposes a write barrier.
synchronises :: ActionType -> IORefId -> Bool Source #
Check if an action synchronises a given IORef
.
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
.
Concurrency state
initialCState :: ConcurrencyState Source #
Initial concurrency state.
updateCState :: MemType -> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState Source #
Update the concurrency state with the action that has just happened.
updateIOState :: MemType -> ThreadAction -> Map IORefId Int -> Map IORefId Int Source #
Update the IORef
buffer state with the action that has just
happened.
updateMVState :: ThreadAction -> Set MVarId -> Set MVarId Source #
Update the MVar
full/empty state with the action that has just
happened.
updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState Source #
Update the thread masking state with the action that has just happened.
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!
efromRight :: HasCallStack => Either a b -> b Source #
fromRight
but with a better error message if it fails. Use
this only where it shouldn't fail!
efromLeft :: HasCallStack => Either a b -> a Source #
fromLeft
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 :: MonadDejaFu n => (n () -> x) -> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, Ref 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.