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

Test.DejaFu.Internal

Contents

SCT settings
Identifiers
Actions
Simplified actions
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
- _memtype :: MemType
- _discard :: Maybe (Either Failure a -> Maybe Discard)
- _debugShow :: Maybe (a -> String)
- _debugPrint :: Maybe (String -> n ())
- _debugFatal :: Bool
- _earlyExit :: Maybe (Either Failure a -> Bool)
- _equality :: Maybe (a -> a -> Bool)
- _simplify :: Bool
- _safeIO :: 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
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
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, IORef n (Maybe b))

SCT settings

data Settings n a #

SCT configuration record.

Since: dejafu-1.2.0.0

Constructors

Settings
Fields _way :: Way _memtype :: MemType _discard :: Maybe (Either Failure a -> Maybe Discard) _debugShow :: Maybe (a -> String) _debugPrint :: Maybe (String -> n ()) _debugFatal :: Bool _earlyExit :: Maybe (Either Failure a -> Bool) _equality :: Maybe (a -> a -> Bool) _simplify :: Bool _safeIO :: Bool

data Way where #

How to explore the possible executions of a concurrent program.

Since: dejafu-0.7.0.0

Constructors

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

Instances

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

Identifiers

data IdSource #

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

Eq IdSource #
Instance details Defined in Test.DejaFu.Internal Methods (==) :: IdSource -> IdSource -> Bool # (/=) :: IdSource -> IdSource -> Bool #
Ord IdSource #
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 #
Show IdSource #
Instance details Defined in Test.DejaFu.Internal Methods showsPrec :: Int -> IdSource -> ShowS # show :: IdSource -> String # showList :: [IdSource] -> ShowS #
Generic IdSource #
Instance details Defined in Test.DejaFu.Internal Associated Types type Rep IdSource :: * -> * # Methods from :: IdSource -> Rep IdSource x # to :: Rep IdSource x -> IdSource #
NFData IdSource #
Instance details Defined in Test.DejaFu.Internal Methods rnf :: IdSource -> () #
type Rep IdSource #
Instance details Defined in Test.DejaFu.Internal type Rep IdSource = D1 (MetaData "IdSource" "Test.DejaFu.Internal" "dejafu-1.11.0.2-AnBNhcajOaIEu4diDt4daf" 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) #

Get the next free IORefId.

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

Get the next free MVarId.

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

Get the next free TVarId.

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

Get the next free ThreadId.

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

Helper for next*

initialIdSource :: IdSource #

The initial ID source.

Actions

isBlock :: ThreadAction -> Bool #

Check if a ThreadAction immediately blocks.

tvarsOf :: ThreadAction -> Set TVarId #

Get the TVars affected by a ThreadAction.

tvarsWritten :: ThreadAction -> Set TVarId #

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

tvarsRead :: ThreadAction -> Set TVarId #

Get the TVars a transaction read from.

rewind :: ThreadAction -> Lookahead #

Convert a ThreadAction into a Lookahead: "rewind" what has happened.

willRelease :: Lookahead -> Bool #

Check if an operation could enable another thread.

Simplified actions

data ActionType #

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

Eq ActionType #
Instance details Defined in Test.DejaFu.Internal Methods (==) :: ActionType -> ActionType -> Bool # (/=) :: ActionType -> ActionType -> Bool #
Show ActionType #
Instance details Defined in Test.DejaFu.Internal Methods showsPrec :: Int -> ActionType -> ShowS # show :: ActionType -> String # showList :: [ActionType] -> ShowS #
Generic ActionType #
Instance details Defined in Test.DejaFu.Internal Associated Types type Rep ActionType :: * -> * # Methods from :: ActionType -> Rep ActionType x # to :: Rep ActionType x -> ActionType #
NFData ActionType #
Instance details Defined in Test.DejaFu.Internal Methods rnf :: ActionType -> () #
type Rep ActionType #
Instance details Defined in Test.DejaFu.Internal type Rep ActionType = D1 (MetaData "ActionType" "Test.DejaFu.Internal" "dejafu-1.11.0.2-AnBNhcajOaIEu4diDt4daf" 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 :: * -> ) :+: (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 :: -> *)))))

isBarrier :: ActionType -> Bool #

Check if an action imposes a write barrier.

isCommit :: ActionType -> IORefId -> Bool #

Check if an action commits a given IORef.

synchronises :: ActionType -> IORefId -> Bool #

Check if an action synchronises a given IORef.

iorefOf :: ActionType -> Maybe IORefId #

Get the IORef affected.

mvarOf :: ActionType -> Maybe MVarId #

Get the MVar affected.

tidsOf :: ThreadAction -> Set ThreadId #

Get the ThreadIds involved in a ThreadAction.

simplifyAction :: ThreadAction -> ActionType #

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 #

Variant of simplifyAction that takes a Lookahead.

Error reporting

etail :: HasCallStack => [a] -> [a] #

tail but with a better error message if it fails. Use this only where it shouldn't fail!

eidx :: HasCallStack => [a] -> Int -> a #

'(!!)' but with a better error message if it fails. Use this only where it shouldn't fail!

efromJust :: HasCallStack => Maybe a -> a #

fromJust but with a better error message if it fails. Use this only where it shouldn't fail!

efromList :: HasCallStack => [a] -> NonEmpty a #

fromList but with a better error message if it fails. Use this only where it shouldn't fail!

efromRight :: HasCallStack => Either a b -> b #

fromRight 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 #

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 #

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 #

lookup but which errors if the key is not present. Use this only where it shouldn't fail!

fatal :: HasCallStack => String -> a #

error but saying where it came from

Miscellaneous

runRefCont :: MonadConc n => (n () -> x) -> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, IORef n (Maybe b)) #

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.