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	Safe-Inferred
Language	Haskell2010

Test.DejaFu.Internal

Contents

SCT settings
Identifiers
Actions
Simplified actions
Concurrency state
Error reporting
Miscellaneous

Description

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
- Systematic :: Bounds -> Way
- Randomly :: RandomGen g => (g -> (Int, g)) -> g -> Int -> Way
data IdSource = IdSource {
- _iorids :: (Int, [String])
- _mvids :: (Int, [String])
- _tvids :: (Int, [String])
- _tids :: (Int, [String])
}
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
- = UnsynchronisedRead IORefId
- | UnsynchronisedWrite IORefId
- | UnsynchronisedOther
- | PartiallySynchronisedCommit IORefId
- | PartiallySynchronisedWrite IORefId
- | PartiallySynchronisedModify IORefId
- | SynchronisedModify IORefId
- | SynchronisedRead MVarId
- | SynchronisedWrite MVarId
- | SynchronisedOther
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

data Settings n a Source #

SCT configuration record.

Since: 1.2.0.0

Constructors

Settings
Fields _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 Source #

How to explore the possible executions of a concurrent program.

Since: 0.7.0.0

Constructors

Systematic :: Bounds -> Way
Randomly :: RandomGen g => (g -> (Int, g)) -> g -> Int -> Way

Instances

Instances details

Show Way Source #
Instance details Defined in Test.DejaFu.Internal Methods showsPrec :: Int -> Way -> ShowS # show :: Way -> String # showList :: [Way] -> ShowS #

Identifiers

data IdSource Source #

The number of ID parameters was getting a bit unwieldy, so this hides them all away.

Constructors

IdSource
Fields _iorids :: (Int, [String]) _mvids :: (Int, [String]) _tvids :: (Int, [String]) _tids :: (Int, [String])

Instances

Instances details

Generic IdSource Source #
Instance details Defined in Test.DejaFu.Internal Associated Types type Rep IdSource :: Type -> Type # Methods from :: IdSource -> Rep IdSource x # to :: Rep IdSource x -> IdSource #
Show IdSource Source #
Instance details Defined in Test.DejaFu.Internal Methods showsPrec :: Int -> IdSource -> ShowS # show :: IdSource -> String # showList :: [IdSource] -> ShowS #
NFData IdSource Source #
Instance details Defined in Test.DejaFu.Internal Methods rnf :: IdSource -> () #
Eq IdSource Source #
Instance details Defined in Test.DejaFu.Internal Methods (==) :: IdSource -> IdSource -> Bool # (/=) :: IdSource -> IdSource -> Bool #
Ord IdSource Source #
Instance details Defined in Test.DejaFu.Internal Methods compare :: IdSource -> IdSource -> Ordering # (<) :: IdSource -> IdSource -> Bool # (<=) :: IdSource -> IdSource -> Bool # (>) :: IdSource -> IdSource -> Bool # (>=) :: IdSource -> IdSource -> Bool # max :: IdSource -> IdSource -> IdSource # min :: IdSource -> IdSource -> IdSource #
type Rep IdSource Source #
Instance details Defined in Test.DejaFu.Internal type Rep IdSource = D1 ('MetaData "IdSource" "Test.DejaFu.Internal" "dejafu-2.4.0.6-2Exh5SnWzcKIwmIryqnn01" '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])))))

nextIORId :: String -> IdSource -> (IdSource, IORefId) Source #

Get the next free IORefId.

nextMVId :: String -> IdSource -> (IdSource, MVarId) Source #

Get the next free MVarId.

nextTVId :: String -> IdSource -> (IdSource, TVarId) Source #

Get the next free TVarId.

nextTId :: String -> IdSource -> (IdSource, ThreadId) Source #

Get the next free ThreadId.

nextId :: String -> (Int, [String]) -> (Id, (Int, [String])) Source #

Helper for next*

initialIdSource :: IdSource Source #

The initial ID source.

Actions

isBlock :: ThreadAction -> Bool Source #

Check if a ThreadAction immediately blocks.

tvarsOf :: ThreadAction -> Set TVarId Source #

Get the TVars affected by a ThreadAction.

tvarsWritten :: ThreadAction -> Set TVarId Source #

Get the TVars a transaction wrote to (or would have, if it didn't retry).

tvarsRead :: ThreadAction -> Set TVarId Source #

Get the TVars a transaction read from.

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.

Constructors

UnsynchronisedRead IORefId	A `readIORef` or a `readForCAS`.
UnsynchronisedWrite IORefId	A `writeIORef`.
UnsynchronisedOther	Some other action which doesn't require cross-thread communication.
PartiallySynchronisedCommit IORefId	A commit.
PartiallySynchronisedWrite IORefId	A `casIORef`
PartiallySynchronisedModify IORefId	A `modifyIORefCAS`
SynchronisedModify IORefId	An `atomicModifyIORef`.
SynchronisedRead MVarId	A `readMVar` or `takeMVar` (or `try`/`blocked` variants).
SynchronisedWrite MVarId	A `putMVar` (or `try`/`blocked` variant).
SynchronisedOther	Some other action which does require cross-thread communication.

Instances

Instances details

Generic ActionType Source #
Instance details Defined in Test.DejaFu.Internal Associated Types type Rep ActionType :: Type -> Type # Methods from :: ActionType -> Rep ActionType x # to :: Rep ActionType x -> ActionType #
Show ActionType Source #
Instance details Defined in Test.DejaFu.Internal Methods showsPrec :: Int -> ActionType -> ShowS # show :: ActionType -> String # showList :: [ActionType] -> ShowS #
NFData ActionType Source #
Instance details Defined in Test.DejaFu.Internal Methods rnf :: ActionType -> () #
Eq ActionType Source #
Instance details Defined in Test.DejaFu.Internal Methods (==) :: ActionType -> ActionType -> Bool # (/=) :: ActionType -> ActionType -> Bool #
type Rep ActionType Source #
Instance details Defined in Test.DejaFu.Internal type Rep ActionType = D1 ('MetaData "ActionType" "Test.DejaFu.Internal" "dejafu-2.4.0.6-2Exh5SnWzcKIwmIryqnn01" 'False) (((C1 ('MetaCons "UnsynchronisedRead" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IORefId)) :+: C1 ('MetaCons "UnsynchronisedWrite" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IORefId))) :+: (C1 ('MetaCons "UnsynchronisedOther" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PartiallySynchronisedCommit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IORefId)) :+: C1 ('MetaCons "PartiallySynchronisedWrite" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IORefId))))) :+: ((C1 ('MetaCons "PartiallySynchronisedModify" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IORefId)) :+: C1 ('MetaCons "SynchronisedModify" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IORefId))) :+: (C1 ('MetaCons "SynchronisedRead" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MVarId)) :+: (C1 ('MetaCons "SynchronisedWrite" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MVarId)) :+: C1 ('MetaCons "SynchronisedOther" 'PrefixI 'False) (U1 :: Type -> Type)))))

isBarrier :: ActionType -> Bool Source #

Check if an action imposes a write barrier.

isCommit :: ActionType -> IORefId -> Bool Source #

Check if an action commits a given IORef.

synchronises :: ActionType -> IORefId -> Bool Source #

Check if an action synchronises a given IORef.

iorefOf :: ActionType -> Maybe IORefId Source #

Get the IORef affected.

mvarOf :: ActionType -> Maybe MVarId Source #

Get the MVar affected.

tidsOf :: ThreadAction -> Set ThreadId Source #

Get the ThreadIds involved in a ThreadAction.

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!

fatal :: HasCallStack => String -> a Source #

error but saying where it came from

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.