Copyright	(c) 2016--2021 Michael Walker
License	MIT
Maintainer	Michael Walker <mike@barrucadu.co.uk>
Stability	experimental
Portability	FlexibleContexts, LambdaCase, RankNTypes, RecordWildCards, ScopedTypeVariables
Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.DejaFu.Conc.Internal

Contents

Set-up
Execution
Single-step execution
Invariants

Description

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.

Synopsis

type SeqTrace = Seq (Decision, [(ThreadId, Lookahead)], ThreadAction)
data CResult n g a = CResult {
- finalContext :: Context n g
- finalRef :: Ref n (Maybe (Either Condition a))
- finalRestore :: Threads n -> n ()
- finalTrace :: SeqTrace
- finalDecision :: Maybe (ThreadId, ThreadAction)
}
runConcurrency :: (MonadDejaFu n, HasCallStack) => [Invariant n ()] -> Bool -> Scheduler g -> MemType -> g -> IdSource -> Int -> ModelConc n a -> n (CResult n g a)
runConcurrencyWithSnapshot :: (MonadDejaFu n, HasCallStack) => Scheduler g -> MemType -> Context n g -> (Threads n -> n ()) -> ModelConc n a -> n (CResult n g a)
killAllThreads :: (MonadDejaFu n, HasCallStack) => Context n g -> n ()
data Context n g = Context {
- cSchedState :: g
- cIdSource :: IdSource
- cThreads :: Threads n
- cWriteBuf :: WriteBuffer n
- cCaps :: Int
- cInvariants :: InvariantContext n
- cNewInvariants :: [Invariant n ()]
- cCState :: ConcurrencyState
}
runThreads :: (MonadDejaFu n, HasCallStack) => Bool -> Scheduler g -> MemType -> Ref n (Maybe (Either Condition a)) -> Context n g -> n (CResult n g a)
fixContext :: MemType -> ThreadId -> ThreadAction -> What n g -> Context n g -> Context n g
unblockWaitingOn :: ThreadId -> Threads n -> Threads n
data What n g
- = Succeeded (Context n g)
- | Failed Condition
stepThread :: forall n g. (MonadDejaFu n, HasCallStack) => Bool -> Bool -> Scheduler g -> MemType -> ThreadId -> Action n -> Context n g -> n (What n g, ThreadAction, Threads n -> n ())
stepThrow :: (MonadDejaFu n, Exception e) => (Maybe MaskingState -> ThreadAction) -> ThreadId -> e -> Context n g -> n (What n g, ThreadAction, Threads n -> n ())
synchronised :: MonadDejaFu n => (Context n g -> n x) -> Context n g -> n x
data InvariantContext n = InvariantContext {
- icActive :: [Invariant n ()]
- icBlocked :: [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
}
unblockInvariants :: ThreadAction -> InvariantContext n -> InvariantContext n
checkInvariants :: MonadDejaFu n => InvariantContext n -> n (Either SomeException (InvariantContext n))
checkInvariant :: MonadDejaFu n => Invariant n a -> n (Either SomeException ([IORefId], [MVarId], [TVarId]))
doInvariant :: MonadDejaFu n => Invariant n a -> n (Either SomeException a, [IORefId], [MVarId], [TVarId])
stepInvariant :: MonadDejaFu n => IAction n -> n (Either SomeException (Maybe (IAction n)), [IORefId], [MVarId], [TVarId])

Set-up

type SeqTrace = Seq (Decision, [(ThreadId, Lookahead)], ThreadAction) Source #

Trace but as a sequence.

data CResult n g a Source #

The result of running a concurrent program.

Constructors

CResult
Fields finalContext :: Context n g finalRef :: Ref n (Maybe (Either Condition a)) finalRestore :: Threads n -> n () Meaningless if this result doesn't come from a snapshotting execution. finalTrace :: SeqTrace finalDecision :: Maybe (ThreadId, ThreadAction)

runConcurrency :: (MonadDejaFu n, HasCallStack) => [Invariant n ()] -> Bool -> Scheduler g -> MemType -> g -> IdSource -> Int -> ModelConc n a -> n (CResult n g a) Source #

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

runConcurrencyWithSnapshot :: (MonadDejaFu n, HasCallStack) => Scheduler g -> MemType -> Context n g -> (Threads n -> n ()) -> ModelConc n a -> n (CResult n g a) Source #

Like runConcurrency but starts from a snapshot.

killAllThreads :: (MonadDejaFu n, HasCallStack) => Context n g -> n () Source #

Kill the remaining threads

Execution

data Context n g Source #

The context a collection of threads are running in.

Constructors

Context
Fields cSchedState :: g cIdSource :: IdSource cThreads :: Threads n cWriteBuf :: WriteBuffer n cCaps :: Int cInvariants :: InvariantContext n cNewInvariants :: [Invariant n ()] cCState :: ConcurrencyState

runThreads :: (MonadDejaFu n, HasCallStack) => Bool -> Scheduler g -> MemType -> Ref n (Maybe (Either Condition a)) -> Context n g -> n (CResult n g a) Source #

Run a collection of threads, until there are no threads left.

fixContext :: MemType -> ThreadId -> ThreadAction -> What n g -> Context n g -> Context n g Source #

Apply the context update from stepping an action.

unblockWaitingOn :: ThreadId -> Threads n -> Threads n Source #

unblockWaitingOn tid unblocks every thread blocked in a throwTo tid.

Single-step execution

data What n g Source #

What a thread did, for execution purposes.

Constructors

Succeeded (Context n g)	Action succeeded: continue execution.
Failed Condition	Action caused computation to fail: stop.

stepThread Source #

Arguments

:: forall n g. (MonadDejaFu n, HasCallStack)
=> Bool	Should we record a snapshot?
-> Bool	Is this the first action?
-> Scheduler g	The scheduler.
-> MemType	The memory model to use.
-> ThreadId	ID of the current thread
-> Action n	Action to step
-> Context n g	The execution context.
-> n (What n g, ThreadAction, Threads n -> n ())

Run a single thread one step, by dispatching on the type of Action.

Each case looks very similar. This is deliberate, so that the essential differences between actions are more apparent, and not hidden by accidental differences in how things are expressed.

Note: the returned snapshot action will definitely not do the right thing with relaxed memory.

stepThrow Source #

Arguments

:: (MonadDejaFu n, Exception e)
=> (Maybe MaskingState -> ThreadAction)	Action to include in the trace.
-> ThreadId	The thread receiving the exception.
-> e	Exception to raise.
-> Context n g	The execution context.
-> n (What n g, ThreadAction, Threads n -> n ())

Handle an exception being thrown from an AAtom, AThrow, or AThrowTo.

synchronised Source #

Arguments

:: MonadDejaFu n
=> (Context n g -> n x)	Action to run after the write barrier.
-> Context n g	The original execution context.
-> n x

Helper for actions impose a write barrier.

Invariants

data InvariantContext n Source #

The state of the invariants

Constructors

InvariantContext
Fields icActive :: [Invariant n ()] icBlocked :: [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]

unblockInvariants :: ThreadAction -> InvariantContext n -> InvariantContext n Source #

unblockInvariants act unblocks every invariant which could have its result changed by act.

checkInvariants :: MonadDejaFu n => InvariantContext n -> n (Either SomeException (InvariantContext n)) Source #

Check all active invariants, returning an arbitrary failure if multiple ones fail.

checkInvariant :: MonadDejaFu n => Invariant n a -> n (Either SomeException ([IORefId], [MVarId], [TVarId])) Source #

Check an invariant.

doInvariant :: MonadDejaFu n => Invariant n a -> n (Either SomeException a, [IORefId], [MVarId], [TVarId]) Source #

Run an invariant (more primitive)

stepInvariant :: MonadDejaFu n => IAction n -> n (Either SomeException (Maybe (IAction n)), [IORefId], [MVarId], [TVarId]) Source #

Run an invariant for one step