Test.DejaFu.Internal

Internal types and functions used throughout DejaFu. This module is NOT considered to form part of the public interface of this library.

SCT settings

data Settings n a

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

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

Show Way

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

Defined in Test.DejaFu.Internal

Methods

(==) :: IdSource -> IdSource -> Bool

(/=) :: IdSource -> IdSource -> Bool

Ord IdSource

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

Defined in Test.DejaFu.Internal

Methods

showsPrec :: Int -> IdSource -> ShowS

show :: IdSource -> String

showList :: [IdSource] -> ShowS

Generic IdSource

Defined in Test.DejaFu.Internal

Associated Types

type Rep IdSource :: Type -> Type

Methods

from :: IdSource -> Rep IdSource x

to :: Rep IdSource x -> IdSource

NFData IdSource

Defined in Test.DejaFu.Internal

Methods

rnf :: IdSource -> ()

type Rep IdSource

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])))))

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

Defined in Test.DejaFu.Internal

Methods

(==) :: ActionType -> ActionType -> Bool

(/=) :: ActionType -> ActionType -> Bool

Show ActionType

Defined in Test.DejaFu.Internal

Methods

showsPrec :: Int -> ActionType -> ShowS

show :: ActionType -> String

showList :: [ActionType] -> ShowS

Generic ActionType

Defined in Test.DejaFu.Internal

Associated Types

type Rep ActionType :: Type -> Type

Methods

from :: ActionType -> Rep ActionType x

to :: Rep ActionType x -> ActionType

NFData ActionType

Defined in Test.DejaFu.Internal

Methods

rnf :: ActionType -> ()

type Rep ActionType

Defined in Test.DejaFu.Internal

type Rep ActionType = D1 ('MetaData "ActionType" "Test.DejaFu.Internal" "dejafu-2.4.0.3-3mGbtTqSt0UArHQ7j0hezX" '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

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.

Concurrency state

initialCState :: ConcurrencyState

Initial concurrency state.

updateCState :: MemType -> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState

Update the concurrency state with the action that has just happened.

updateIOState :: MemType -> ThreadAction -> Map IORefId Int -> Map IORefId Int

Update the IORef buffer state with the action that has just happened.

updateMVState :: ThreadAction -> Set MVarId -> Set MVarId

Update the MVar full/empty state with the action that has just happened.

updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState

Update the thread masking state with the action that has just happened.

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!

efromLeft :: HasCallStack => Either a b -> a

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

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 :: MonadDejaFu n => (n () -> x) -> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, Ref 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.