Test.DejaFu.Deterministic.Internal

Concurrent monads with a fixed scheduler: internal types and functions. This module is NOT considered to form part of the public interface of this library.

Execution

runFixed :: (Functor n, Monad n) => Fixed n r s -> (forall x. s x -> IdSource -> n (Result x, IdSource, TTrace)) -> Scheduler ThreadId ThreadAction Lookahead g -> MemType -> g -> M n r s a -> n (Either Failure a, g, Trace ThreadId ThreadAction Lookahead)

Run a concurrent computation with a given Scheduler and initial state, returning a Just if it terminates, and Nothing if a deadlock is detected. Also returned is the final state of the scheduler, and an execution trace.

runFixed' :: forall n r s g a. (Functor n, Monad n) => Fixed n r s -> (forall x. s x -> IdSource -> n (Result x, IdSource, TTrace)) -> Scheduler ThreadId ThreadAction Lookahead g -> MemType -> g -> IdSource -> M n r s a -> n (Either Failure a, g, IdSource, Trace ThreadId ThreadAction Lookahead)

Same as runFixed, be parametrised by an IdSource.

The Conc Monad

newtype M n r s a

The underlying monad is based on continuations over Actions.

One might wonder why the return type isn't reflected in Action, and a free monad formulation used. This would remove the need for a Lift action as the penultimate action of thread 0 used to communicate back the result, and be more pleasing in a sense. However, this makes the current expression of threads and exception handlers very difficult (perhaps even not possible without significant reworking), so I abandoned the attempt.

Constructors

M

Fields

• runM :: (a -> Action n r s) -> Action n r s

Instances

Monad (M n r s)

Methods

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

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

return :: a -> M n r s a

fail :: String -> M n r s a

Functor (M n r s)

Methods

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

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

Applicative (M n r s)

Methods

pure :: a -> M n r s a

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

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

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

data MVar r a

The concurrent variable type used with the Conc monad. One notable difference between these and MVars is that MVars are single-wakeup, and wake up in a FIFO order. Writing to a MVar wakes up all threads blocked on reading it, and it is up to the scheduler which one runs next. Taking from a MVar behaves analogously.

Constructors

MVar

Fields

• _cvarId :: MVarId
• _cvarVal :: r (Maybe a)

data CRef r a

The mutable non-blocking reference type. These are like IORefs.

CRefs are represented as a unique numeric identifier and a reference containing (a) any thread-local non-synchronised writes (so each thread sees its latest write), (b) a commit count (used in compare-and-swaps), and (c) the current value visible to all threads.

Constructors

CRef

Fields

• _crefId :: CRefId
• _crefVal :: r (Map ThreadId a, Integer, a)

data Ticket a

The compare-and-swap proof type.

Tickets are represented as just a wrapper around the identifier of the CRef it came from, the commit count at the time it was produced, and an a value. This doesn't work in the source package (atomic-primops) because of the need to use pointer equality. Here we can just pack extra information into CRef to avoid that need.

Constructors

Ticket

Fields

• _ticketCRef :: CRefId
• _ticketWrites :: Integer
• _ticketVal :: a

type Fixed n r s = Ref n r (M n r s)

Dict of methods for implementations to override.

cont :: ((a -> Action n r s) -> Action n r s) -> M n r s a

Construct a continuation-passing operation from a function.

runCont :: M n r s a -> (a -> Action n r s) -> Action n r s

Run a CPS computation with the given final computation.

Primitive Actions

data Action n r s

Scheduling is done in terms of a trace of Actions. Blocking can only occur as a result of an action, and they cover (most of) the primitives of the concurrency. spawn is absent as it is implemented in terms of newEmptyMVar, fork, and putMVar.

Constructors

AFork String ((forall b. M n r s b -> M n r s b) -> Action n r s) (ThreadId -> Action n r s)

AMyTId (ThreadId -> Action n r s)

AGetNumCapabilities (Int -> Action n r s)

ASetNumCapabilities Int (Action n r s)

ANewVar String (MVar r a -> Action n r s)

APutVar (MVar r a) a (Action n r s)

ATryPutVar (MVar r a) a (Bool -> Action n r s)

AReadVar (MVar r a) (a -> Action n r s)

ATakeVar (MVar r a) (a -> Action n r s)

ATryTakeVar (MVar r a) (Maybe a -> Action n r s)

ANewRef String a (CRef r a -> Action n r s)

AReadRef (CRef r a) (a -> Action n r s)

AReadRefCas (CRef r a) (Ticket a -> Action n r s)

APeekTicket (Ticket a) (a -> Action n r s)

AModRef (CRef r a) (a -> (a, b)) (b -> Action n r s)

AModRefCas (CRef r a) (a -> (a, b)) (b -> Action n r s)

AWriteRef (CRef r a) a (Action n r s)

ACasRef (CRef r a) (Ticket a) a ((Bool, Ticket a) -> Action n r s)

Exception e => AThrow e

Exception e => AThrowTo ThreadId e (Action n r s)

Exception e => ACatching (e -> M n r s a) (M n r s a) (a -> Action n r s)

APopCatching (Action n r s)

AMasking MaskingState ((forall b. M n r s b -> M n r s b) -> M n r s a) (a -> Action n r s)

AResetMask Bool Bool MaskingState (Action n r s)

AKnowsAbout (Either MVarId TVarId) (Action n r s)

AForgets (Either MVarId TVarId) (Action n r s)

AAllKnown (Action n r s)

AMessage Dynamic (Action n r s)

AAtom (s a) (a -> Action n r s)

ALift (n (Action n r s))

AYield (Action n r s)

AReturn (Action n r s)

ACommit ThreadId CRefId

AStop

Identifiers

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 MVarId

Every MVar has a unique identifier.

Constructors

MVarId (Maybe String) Int

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.

Constructors

CRefId (Maybe String) Int

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

initialThread :: ThreadId

The ID of the initial thread.

Memory Models

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

Scheduling & Traces

type Scheduler tid action lookahead s = [(Decision tid, action)] -> Maybe (tid, action) -> NonEmpty (tid, lookahead) -> s -> (Maybe tid, s)

A Scheduler drives the execution of a concurrent program. The parameters it takes are:

1. The trace so far.
2. The last thread executed (if this is the first invocation, this is Nothing).
3. The runnable threads at this point.
4. The state.

It returns a thread to execute, or Nothing if execution should abort here, and also a new state.

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

isBlock :: ThreadAction -> Bool

Check if a ThreadAction immediately blocks.

lookahead :: Action n r s -> NonEmpty Lookahead

Look as far ahead in the given continuation as possible.

rewind :: ThreadAction -> Maybe Lookahead

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

willRelease :: Lookahead -> Bool

Check if an operation could enable another thread.

preEmpCount :: [(Decision ThreadId, ThreadAction)] -> (Decision ThreadId, Lookahead) -> Int

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

tvarsOf :: ThreadAction -> Set TVarId

Get the TVars affected.

Synchronised and Unsynchronised Actions

data ActionType

A simplified view of the possible actions a thread can perform.

Constructors

UnsynchronisedRead CRefId

A readCRef or a readForCAS.

UnsynchronisedWrite CRefId

A writeCRef.

UnsynchronisedOther

Some other action which doesn't require cross-thread communication.

PartiallySynchronisedCommit CRefId

A commit.

PartiallySynchronisedWrite CRefId

A casCRef

PartiallySynchronisedModify CRefId

A modifyCRefCAS

SynchronisedModify CRefId

An atomicModifyCRef.

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

Methods

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

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

Show ActionType

Methods

showsPrec :: Int -> ActionType -> ShowS

show :: ActionType -> String

showList :: [ActionType] -> ShowS

NFData ActionType

Methods

rnf :: ActionType -> ()

isBarrier :: ActionType -> Bool

Check if an action imposes a write barrier.

isCommit :: ActionType -> CRefId -> Bool

Check if an action commits a given CRef.

synchronises :: ActionType -> CRefId -> Bool

Check if an action synchronises a given CRef.

crefOf :: ActionType -> Maybe CRefId

Get the CRef affected.

cvarOf :: ActionType -> Maybe MVarId

Get the MVar affected.

simplify :: 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.

simplify' :: Lookahead -> ActionType

Variant of simplify that takes a Lookahead.

Failures

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