Test.DejaFu.Conc.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.

Set-up

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

Trace but as a sequence.

data CResult n g a

The result of running a concurrent program.

Constructors

CResult

Fields

• finalContext :: Context n g
• finalRef :: IORef n (Maybe (Either Failure a))
• finalRestore :: Maybe (Threads n -> n ())

  Meaningless if this result doesn't come from a snapshotting execution.

• finalTrace :: SeqTrace
• finalDecision :: Maybe (ThreadId, ThreadAction)

data DCSnapshot n a

A snapshot of the concurrency state immediately after dontCheck finishes.

Since: dejafu-1.4.0.0

Constructors

DCSnapshot

Fields

• dcsContext :: Context n ()

  The execution context. The scheduler state is ignored when restoring.

• dcsRestore :: Threads n -> n ()

  Action to restore IORef, MVar, and TVar values.

• dcsRef :: IORef n (Maybe (Either Failure a))

  Reference where the result will be written.

runConcurrency :: (MonadConc n, HasCallStack) => Bool -> Scheduler g -> MemType -> g -> IdSource -> Int -> ModelConc n a -> n (CResult n g a)

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.

runConcurrency' :: (MonadConc n, HasCallStack) => Bool -> Scheduler g -> MemType -> Context n g -> ModelConc n a -> n (CResult n g a)

Run a concurrent program using the given context, and without killing threads which remain at the end. The context must have no main thread.

Only a separate function because ADontCheck needs it.

runConcurrencyWithSnapshot :: (MonadConc n, HasCallStack) => Scheduler g -> MemType -> Context n g -> (Threads n -> n ()) -> IORef n (Maybe (Either Failure a)) -> n (CResult n g a)

Like runConcurrency but starts from a snapshot.

killAllThreads :: (MonadConc n, HasCallStack) => Context n g -> n ()

Kill the remaining threads

Execution

data Context n g

The context a collection of threads are running in.

Constructors

Context

Fields

• cSchedState :: g
• cIdSource :: IdSource
• cThreads :: Threads n
• cWriteBuf :: WriteBuffer n
• cCaps :: Int

runThreads :: (MonadConc n, HasCallStack) => Bool -> Scheduler g -> MemType -> IORef n (Maybe (Either Failure a)) -> Context n g -> n (CResult n g a)

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

fixContext :: ThreadId -> What n g -> Context n g -> Context n g

Apply the context update from stepping an action.

unblockWaitingOn :: ThreadId -> Threads n -> Threads n

unblockWaitingOn tid unblocks every thread blocked in a throwTo tid.

Single-step execution

data Act

What a thread did, for trace purposes.

Constructors

Single ThreadAction

Just one action.

SubC SeqTrace (Maybe (ThreadId, ThreadAction))

subconcurrency, with the given trace and final action.

Instances

Eq Act

Defined in Test.DejaFu.Conc.Internal

Methods

(==) :: Act -> Act -> Bool

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

Show Act

Defined in Test.DejaFu.Conc.Internal

Methods

showsPrec :: Int -> Act -> ShowS

show :: Act -> String

showList :: [Act] -> ShowS

data What n g

What a thread did, for execution purposes.

Constructors

Succeeded (Context n g)

Action succeeded: continue execution.

Failed Failure

Action caused computation to fail: stop.

Snap (Context n g)

Action was a snapshot point and we're in snapshot mode: stop.

stepThread

Arguments

:: (MonadConc 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, Act, 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

Arguments

:: (MonadConc n, Exception e)

=> (Bool -> 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, Act, Threads n -> n ())

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

synchronised

Arguments

:: MonadConc n

=> (Context n g -> n (What n g, Act, Threads n -> n ()))

Action to run after the write barrier.

-> Context n g

The original execution context.

-> n (What n g, Act, Threads n -> n ())

Helper for actions impose a write barrier.

dcSched :: Scheduler (Maybe Int)

scheduler for ADontCheck