Test.DejaFu.Deterministic

Deterministic traced execution of concurrent computations.

This works by executing the computation on a single thread, calling out to the supplied scheduler after each step to determine which thread runs next.

The Conc Monad

data Conc n r s a

Instances

MonadIO ConcIO

Methods

liftIO :: IO a -> ConcIO a

MonadBase IO ConcIO

Methods

liftBase :: IO α -> ConcIO α

Monad (Conc n r s)

Methods

(>>=) :: Conc n r s a -> (a -> Conc n r s b) -> Conc n r s b

(>>) :: Conc n r s a -> Conc n r s b -> Conc n r s b

return :: a -> Conc n r s a

fail :: String -> Conc n r s a

Functor (Conc n r s)

Methods

fmap :: (a -> b) -> Conc n r s a -> Conc n r s b

(<$) :: a -> Conc n r s b -> Conc n r s a

Applicative (Conc n r s)

Methods

pure :: a -> Conc n r s a

(<*>) :: Conc n r s (a -> b) -> Conc n r s a -> Conc n r s b

(*>) :: Conc n r s a -> Conc n r s b -> Conc n r s b

(<*) :: Conc n r s a -> Conc n r s b -> Conc n r s a

MonadThrow (Conc n r s)

Methods

throwM :: Exception e => e -> Conc n r s a

MonadCatch (Conc n r s)

Methods

catch :: Exception e => Conc n r s a -> (e -> Conc n r s a) -> Conc n r s a

MonadMask (Conc n r s)

Methods

mask :: ((forall a. Conc n r s a -> Conc n r s a) -> Conc n r s b) -> Conc n r s b

uninterruptibleMask :: ((forall a. Conc n r s a -> Conc n r s a) -> Conc n r s b) -> Conc n r s b

Monad n => MonadConc (Conc n r (STMLike n r))

Associated Types

type STM (Conc n r (STMLike n r) :: * -> *) :: * -> *

type MVar (Conc n r (STMLike n r) :: * -> *) :: * -> *

type CRef (Conc n r (STMLike n r) :: * -> *) :: * -> *

type Ticket (Conc n r (STMLike n r) :: * -> *) :: * -> *

type ThreadId (Conc n r (STMLike n r) :: * -> *) :: *

Methods

fork :: Conc n r (STMLike n r) () -> Conc n r (STMLike n r) (ThreadId (Conc n r (STMLike n r)))

forkWithUnmask :: ((forall a. Conc n r (STMLike n r) a -> Conc n r (STMLike n r) a) -> Conc n r (STMLike n r) ()) -> Conc n r (STMLike n r) (ThreadId (Conc n r (STMLike n r)))

forkWithUnmaskN :: String -> ((forall a. Conc n r (STMLike n r) a -> Conc n r (STMLike n r) a) -> Conc n r (STMLike n r) ()) -> Conc n r (STMLike n r) (ThreadId (Conc n r (STMLike n r)))

forkOn :: Int -> Conc n r (STMLike n r) () -> Conc n r (STMLike n r) (ThreadId (Conc n r (STMLike n r)))

forkOnWithUnmask :: Int -> ((forall a. Conc n r (STMLike n r) a -> Conc n r (STMLike n r) a) -> Conc n r (STMLike n r) ()) -> Conc n r (STMLike n r) (ThreadId (Conc n r (STMLike n r)))

forkOnWithUnmaskN :: String -> Int -> ((forall a. Conc n r (STMLike n r) a -> Conc n r (STMLike n r) a) -> Conc n r (STMLike n r) ()) -> Conc n r (STMLike n r) (ThreadId (Conc n r (STMLike n r)))

getNumCapabilities :: Conc n r (STMLike n r) Int

setNumCapabilities :: Int -> Conc n r (STMLike n r) ()

myThreadId :: Conc n r (STMLike n r) (ThreadId (Conc n r (STMLike n r)))

yield :: Conc n r (STMLike n r) ()

threadDelay :: Int -> Conc n r (STMLike n r) ()

newEmptyMVar :: Conc n r (STMLike n r) (MVar (Conc n r (STMLike n r)) a)

newEmptyMVarN :: String -> Conc n r (STMLike n r) (MVar (Conc n r (STMLike n r)) a)

putMVar :: MVar (Conc n r (STMLike n r)) a -> a -> Conc n r (STMLike n r) ()

tryPutMVar :: MVar (Conc n r (STMLike n r)) a -> a -> Conc n r (STMLike n r) Bool

readMVar :: MVar (Conc n r (STMLike n r)) a -> Conc n r (STMLike n r) a

takeMVar :: MVar (Conc n r (STMLike n r)) a -> Conc n r (STMLike n r) a

tryTakeMVar :: MVar (Conc n r (STMLike n r)) a -> Conc n r (STMLike n r) (Maybe a)

newCRef :: a -> Conc n r (STMLike n r) (CRef (Conc n r (STMLike n r)) a)

newCRefN :: String -> a -> Conc n r (STMLike n r) (CRef (Conc n r (STMLike n r)) a)

readCRef :: CRef (Conc n r (STMLike n r)) a -> Conc n r (STMLike n r) a

atomicModifyCRef :: CRef (Conc n r (STMLike n r)) a -> (a -> (a, b)) -> Conc n r (STMLike n r) b

writeCRef :: CRef (Conc n r (STMLike n r)) a -> a -> Conc n r (STMLike n r) ()

atomicWriteCRef :: CRef (Conc n r (STMLike n r)) a -> a -> Conc n r (STMLike n r) ()

readForCAS :: CRef (Conc n r (STMLike n r)) a -> Conc n r (STMLike n r) (Ticket (Conc n r (STMLike n r)) a)

peekTicket :: Ticket (Conc n r (STMLike n r)) a -> Conc n r (STMLike n r) a

casCRef :: CRef (Conc n r (STMLike n r)) a -> Ticket (Conc n r (STMLike n r)) a -> a -> Conc n r (STMLike n r) (Bool, Ticket (Conc n r (STMLike n r)) a)

modifyCRefCAS :: CRef (Conc n r (STMLike n r)) a -> (a -> (a, b)) -> Conc n r (STMLike n r) b

modifyCRefCAS_ :: CRef (Conc n r (STMLike n r)) a -> (a -> a) -> Conc n r (STMLike n r) ()

atomically :: STM (Conc n r (STMLike n r)) a -> Conc n r (STMLike n r) a

readTVarConc :: TVar (STM (Conc n r (STMLike n r))) a -> Conc n r (STMLike n r) a

throwTo :: Exception e => ThreadId (Conc n r (STMLike n r)) -> e -> Conc n r (STMLike n r) ()

_concKnowsAbout :: Either (MVar (Conc n r (STMLike n r)) a) (TVar (STM (Conc n r (STMLike n r))) a) -> Conc n r (STMLike n r) ()

_concForgets :: Either (MVar (Conc n r (STMLike n r)) a) (TVar (STM (Conc n r (STMLike n r))) a) -> Conc n r (STMLike n r) ()

_concAllKnown :: Conc n r (STMLike n r) ()

_concMessage :: Typeable * a => a -> Conc n r (STMLike n r) ()

type STM (Conc n r (STMLike n r))

type STM (Conc n r (STMLike n r)) = STMLike n r

type MVar (Conc n r (STMLike n r))

type MVar (Conc n r (STMLike n r)) = MVar r

type CRef (Conc n r (STMLike n r))

type CRef (Conc n r (STMLike n r)) = CRef r

type Ticket (Conc n r (STMLike n r))

type Ticket (Conc n r (STMLike n r)) = Ticket

type ThreadId (Conc n r (STMLike n r))

type ThreadId (Conc n r (STMLike n r)) = ThreadId

type ConcST t = Conc (ST t) (STRef t) (STMST t)

A MonadConc implementation using ST, this should be preferred if you do not need liftIO.

type ConcIO = Conc IO IORef STMIO

A MonadConc implementation using IO.

Executing computations

data Failure

An indication of how a concurrent computation failed.

Constructors

InternalError

Will be raised if the scheduler does something bad. This should never arise unless you write your own, faulty, scheduler! If it does, please file a bug report.

Abort

The scheduler chose to abort execution. This will be produced if, for example, all possible decisions exceed the specified bounds (there have been too many pre-emptions, the computation has executed for too long, or there have been too many yields).

Deadlock

The computation became blocked indefinitely on MVars.

STMDeadlock

The computation became blocked indefinitely on TVars.

UncaughtException

An uncaught exception bubbled to the top of the computation.

Instances

Bounded Failure

Methods

minBound :: Failure

maxBound :: Failure

Enum Failure

Methods

succ :: Failure -> Failure

pred :: Failure -> Failure

toEnum :: Int -> Failure

fromEnum :: Failure -> Int

enumFrom :: Failure -> [Failure]

enumFromThen :: Failure -> Failure -> [Failure]

enumFromTo :: Failure -> Failure -> [Failure]

enumFromThenTo :: Failure -> Failure -> Failure -> [Failure]

Eq Failure

Methods

(==) :: Failure -> Failure -> Bool

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

Ord Failure

Methods

compare :: Failure -> Failure -> Ordering

(<) :: Failure -> Failure -> Bool

(<=) :: Failure -> Failure -> Bool

(>) :: Failure -> Failure -> Bool

(>=) :: Failure -> Failure -> Bool

max :: Failure -> Failure -> Failure

min :: Failure -> Failure -> Failure

Read Failure

Methods

readsPrec :: Int -> ReadS Failure

readList :: ReadS [Failure]

readPrec :: ReadPrec Failure

readListPrec :: ReadPrec [Failure]

Show Failure

Methods

showsPrec :: Int -> Failure -> ShowS

show :: Failure -> String

showList :: [Failure] -> ShowS

NFData Failure

Methods

rnf :: Failure -> ()

data MemType

The memory model to use for non-synchronised CRef operations.

Constructors

SequentialConsistency

The most intuitive model: a program behaves as a simple interleaving of the actions in different threads. When a CRef is written to, that write is immediately visible to all threads.

TotalStoreOrder

Each thread has a write buffer. A thread sees its writes immediately, but other threads will only see writes when they are committed, which may happen later. Writes are committed in the same order that they are created.

PartialStoreOrder

Each CRef has a write buffer. A thread sees its writes immediately, but other threads will only see writes when they are committed, which may happen later. Writes to different CRefs are not necessarily committed in the same order that they are created.

Instances

Bounded MemType

Methods

minBound :: MemType

maxBound :: MemType

Enum MemType

Methods

succ :: MemType -> MemType

pred :: MemType -> MemType

toEnum :: Int -> MemType

fromEnum :: MemType -> Int

enumFrom :: MemType -> [MemType]

enumFromThen :: MemType -> MemType -> [MemType]

enumFromTo :: MemType -> MemType -> [MemType]

enumFromThenTo :: MemType -> MemType -> MemType -> [MemType]

Eq MemType

Methods

(==) :: MemType -> MemType -> Bool

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

Ord MemType

Methods

compare :: MemType -> MemType -> Ordering

(<) :: MemType -> MemType -> Bool

(<=) :: MemType -> MemType -> Bool

(>) :: MemType -> MemType -> Bool

(>=) :: MemType -> MemType -> Bool

max :: MemType -> MemType -> MemType

min :: MemType -> MemType -> MemType

Read MemType

Methods

readsPrec :: Int -> ReadS MemType

readList :: ReadS [MemType]

readPrec :: ReadPrec MemType

readListPrec :: ReadPrec [MemType]

Show MemType

Methods

showsPrec :: Int -> MemType -> ShowS

show :: MemType -> String

showList :: [MemType] -> ShowS

NFData MemType

Methods

rnf :: MemType -> ()

runConcST :: Scheduler ThreadId ThreadAction Lookahead s -> MemType -> s -> (forall t. ConcST t a) -> (Either Failure a, s, Trace ThreadId ThreadAction Lookahead)

Run a concurrent computation with a given Scheduler and initial state, returning a failure reason on error. Also returned is the final state of the scheduler, and an execution trace.

Note how the t in Conc is universally quantified, what this means in practice is that you can't do something like this:

runConc roundRobinSched SequentialConsistency () newEmptyMVar

So mutable references cannot leak out of the Conc computation. If this is making your head hurt, check out the "How runST works" section of https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html

Note: In order to prevent computation from hanging, the runtime will assume that a deadlock situation has arisen if the scheduler attempts to (a) schedule a blocked thread, or (b) schedule a nonexistent thread. In either of those cases, the computation will be halted.

runConcIO :: Scheduler ThreadId ThreadAction Lookahead s -> MemType -> s -> ConcIO a -> IO (Either Failure a, s, Trace ThreadId ThreadAction Lookahead)

Run a concurrent computation in the IO monad with a given Scheduler and initial state, returning a failure reason on error. Also returned is the final state of the scheduler, and an execution trace.

Warning: Blocking on the action of another thread in liftIO cannot be detected! So if you perform some potentially blocking action in a liftIO the entire collection of threads may deadlock! You should therefore keep IO blocks small, and only perform blocking operations with the supplied primitives, insofar as possible.

Note: In order to prevent computation from hanging, the runtime will assume that a deadlock situation has arisen if the scheduler attempts to (a) schedule a blocked thread, or (b) schedule a nonexistent thread. In either of those cases, the computation will be halted.

Execution traces

type Trace tid action lookahead = [(Decision tid, [(tid, NonEmpty lookahead)], action)]

One of the outputs of the runner is a Trace, which is a log of decisions made, all the runnable threads and what they would do, and the action a thread took in its step.

data Decision tid :: * -> *

Scheduling decisions are based on the state of the running program, and so we can capture some of that state in recording what specific decision we made.

Constructors

Start tid

Start a new thread, because the last was blocked (or it's the start of computation).

Continue

Continue running the last thread for another step.

SwitchTo tid

Pre-empt the running thread, and switch to another.

Instances

Eq tid => Eq (Decision tid)

Methods

(==) :: Decision tid -> Decision tid -> Bool

(/=) :: Decision tid -> Decision tid -> Bool

Show tid => Show (Decision tid)

Methods

showsPrec :: Int -> Decision tid -> ShowS

show :: Decision tid -> String

showList :: [Decision tid] -> ShowS

NFData tid => NFData (Decision tid)

Methods

rnf :: Decision tid -> ()

data ThreadId

Every live thread has a unique identitifer.

Constructors

ThreadId (Maybe String) Int

Instances

Eq ThreadId

Methods

(==) :: ThreadId -> ThreadId -> Bool

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

Ord ThreadId

Methods

compare :: ThreadId -> ThreadId -> Ordering

(<) :: ThreadId -> ThreadId -> Bool

(<=) :: ThreadId -> ThreadId -> Bool

(>) :: ThreadId -> ThreadId -> Bool

(>=) :: ThreadId -> ThreadId -> Bool

max :: ThreadId -> ThreadId -> ThreadId

min :: ThreadId -> ThreadId -> ThreadId

Show ThreadId

Methods

showsPrec :: Int -> ThreadId -> ShowS

show :: ThreadId -> String

showList :: [ThreadId] -> ShowS

NFData ThreadId

Methods

rnf :: ThreadId -> ()

data ThreadAction

All the actions that a thread can perform.

Constructors

Fork ThreadId

Start a new thread.

MyThreadId

Get the ThreadId of the current thread.

GetNumCapabilities Int

Get the number of Haskell threads that can run simultaneously.

SetNumCapabilities Int

Set the number of Haskell threads that can run simultaneously.

Yield

Yield the current thread.

NewVar MVarId

Create a new MVar.

PutVar MVarId [ThreadId]

Put into a MVar, possibly waking up some threads.

BlockedPutVar MVarId

Get blocked on a put.

TryPutVar MVarId Bool [ThreadId]

Try to put into a MVar, possibly waking up some threads.

ReadVar MVarId

Read from a MVar.

BlockedReadVar MVarId

Get blocked on a read.

TakeVar MVarId [ThreadId]

Take from a MVar, possibly waking up some threads.

BlockedTakeVar MVarId

Get blocked on a take.

TryTakeVar MVarId Bool [ThreadId]

Try to take from a MVar, possibly waking up some threads.

NewRef CRefId

Create a new CRef.

ReadRef CRefId

Read from a CRef.

ReadRefCas CRefId

Read from a CRef for a future compare-and-swap.

PeekTicket CRefId

Extract the value from a Ticket.

ModRef CRefId

Modify a CRef.

ModRefCas CRefId

Modify a CRef using a compare-and-swap.

WriteRef CRefId

Write to a CRef without synchronising.

CasRef CRefId Bool

Attempt to to a CRef using a compare-and-swap, synchronising it.

CommitRef ThreadId CRefId

Commit the last write to the given CRef by the given thread, so that all threads can see the updated value.

STM TTrace [ThreadId]

An STM transaction was executed, possibly waking up some threads.

BlockedSTM TTrace

Got blocked in an STM transaction.

Catching

Register a new exception handler

PopCatching

Pop the innermost exception handler from the stack.

Throw

Throw an exception.

ThrowTo ThreadId

Throw an exception to a thread.

BlockedThrowTo ThreadId

Get blocked on a throwTo.

Killed

Killed by an uncaught exception.

SetMasking Bool MaskingState

Set the masking state. If True, this is being used to set the masking state to the original state in the argument passed to a masked function.

ResetMasking Bool MaskingState

Return to an earlier masking state. If True, this is being used to return to the state of the masked block in the argument passed to a masked function.

Lift

Lift an action from the underlying monad. Note that the penultimate action in a trace will always be a Lift, this is an artefact of how the runner works.

Return

A return or pure action was executed.

KnowsAbout

A _concKnowsAbout annotation was processed.

Forgets

A _concForgets annotation was processed.

AllKnown

A _concALlKnown annotation was processed.

Message Dynamic

A _concMessage annotation was processed.

Stop

Cease execution and terminate.

Instances

Show ThreadAction

Methods

showsPrec :: Int -> ThreadAction -> ShowS

show :: ThreadAction -> String

showList :: [ThreadAction] -> ShowS

NFData ThreadAction

Methods

rnf :: ThreadAction -> ()

data Lookahead

A one-step look-ahead at what a thread will do next.

Constructors

WillFork

Will start a new thread.

WillMyThreadId

Will get the ThreadId.

WillGetNumCapabilities

Will get the number of Haskell threads that can run simultaneously.

WillSetNumCapabilities Int

Will set the number of Haskell threads that can run simultaneously.

WillYield

Will yield the current thread.

WillNewVar

Will create a new MVar.

WillPutVar MVarId

Will put into a MVar, possibly waking up some threads.

WillTryPutVar MVarId

Will try to put into a MVar, possibly waking up some threads.

WillReadVar MVarId

Will read from a MVar.

WillTakeVar MVarId

Will take from a MVar, possibly waking up some threads.

WillTryTakeVar MVarId

Will try to take from a MVar, possibly waking up some threads.

WillNewRef

Will create a new CRef.

WillReadRef CRefId

Will read from a CRef.

WillPeekTicket CRefId

Will extract the value from a Ticket.

WillReadRefCas CRefId

Will read from a CRef for a future compare-and-swap.

WillModRef CRefId

Will modify a CRef.

WillModRefCas CRefId

Will nodify a CRef using a compare-and-swap.

WillWriteRef CRefId

Will write to a CRef without synchronising.

WillCasRef CRefId

Will attempt to to a CRef using a compare-and-swap, synchronising it.

WillCommitRef ThreadId CRefId

Will commit the last write by the given thread to the CRef.

WillSTM

Will execute an STM transaction, possibly waking up some threads.

WillCatching

Will register a new exception handler

WillPopCatching

Will pop the innermost exception handler from the stack.

WillThrow

Will throw an exception.

WillThrowTo ThreadId

Will throw an exception to a thread.

WillSetMasking Bool MaskingState

Will set the masking state. If True, this is being used to set the masking state to the original state in the argument passed to a masked function.

WillResetMasking Bool MaskingState

Will return to an earlier masking state. If True, this is being used to return to the state of the masked block in the argument passed to a masked function.

WillLift

Will lift an action from the underlying monad. Note that the penultimate action in a trace will always be a Lift, this is an artefact of how the runner works.

WillReturn

Will execute a return or pure action.

WillKnowsAbout

Will process a _concKnowsAbout annotation.

WillForgets

Will process a _concForgets annotation.

WillAllKnown

Will process a _concALlKnown annotation.

WillMessage Dynamic

Will process a _concMessage' annotation.

WillStop

Will cease execution and terminate.

Instances

Show Lookahead

Methods

showsPrec :: Int -> Lookahead -> ShowS

show :: Lookahead -> String

showList :: [Lookahead] -> ShowS

NFData Lookahead

Methods

rnf :: Lookahead -> ()

data MVarId

Every MVar has a unique identifier.

Instances

Eq MVarId

Methods

(==) :: MVarId -> MVarId -> Bool

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

Ord MVarId

Methods

compare :: MVarId -> MVarId -> Ordering

(<) :: MVarId -> MVarId -> Bool

(<=) :: MVarId -> MVarId -> Bool

(>) :: MVarId -> MVarId -> Bool

(>=) :: MVarId -> MVarId -> Bool

max :: MVarId -> MVarId -> MVarId

min :: MVarId -> MVarId -> MVarId

Show MVarId

Methods

showsPrec :: Int -> MVarId -> ShowS

show :: MVarId -> String

showList :: [MVarId] -> ShowS

NFData MVarId

Methods

rnf :: MVarId -> ()

data CRefId

Every CRef has a unique identifier.

Instances

Eq CRefId

Methods

(==) :: CRefId -> CRefId -> Bool

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

Ord CRefId

Methods

compare :: CRefId -> CRefId -> Ordering

(<) :: CRefId -> CRefId -> Bool

(<=) :: CRefId -> CRefId -> Bool

(>) :: CRefId -> CRefId -> Bool

(>=) :: CRefId -> CRefId -> Bool

max :: CRefId -> CRefId -> CRefId

min :: CRefId -> CRefId -> CRefId

Show CRefId

Methods

showsPrec :: Int -> CRefId -> ShowS

show :: CRefId -> String

showList :: [CRefId] -> ShowS

NFData CRefId

Methods

rnf :: CRefId -> ()

data MaskingState :: *

Describes the behaviour of a thread when an asynchronous exception is received.

Constructors

Unmasked

asynchronous exceptions are unmasked (the normal state)

MaskedInterruptible

the state during mask: asynchronous exceptions are masked, but blocking operations may still be interrupted

MaskedUninterruptible

the state during uninterruptibleMask: asynchronous exceptions are masked, and blocking operations may not be interrupted

Instances

Eq MaskingState

Methods

(==) :: MaskingState -> MaskingState -> Bool

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

Show MaskingState

Methods

showsPrec :: Int -> MaskingState -> ShowS

show :: MaskingState -> String

showList :: [MaskingState] -> ShowS

showTrace :: Trace ThreadId ThreadAction Lookahead -> String

Pretty-print a trace, including a key of the thread IDs. Each line of the key is indented by two spaces.

showFail :: Failure -> String

Pretty-print a failure

Scheduling

module Test.DPOR.Schedule