Test.DejaFu.Conc.Internal.Common

Common types and utility functions for deterministic execution of MonadConc implementations. This module is NOT considered to form part of the public interface of this library.

The ModelConc Monad

newtype ModelConc n 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 AStop actions having their parameter. 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

ModelConc

Fields

• runModelConc :: (a -> Action n) -> Action n

Instances

Monad (ModelConc n)

Methods

(>>=) :: ModelConc n a -> (a -> ModelConc n b) -> ModelConc n b

(>>) :: ModelConc n a -> ModelConc n b -> ModelConc n b

return :: a -> ModelConc n a

fail :: String -> ModelConc n a

Functor (ModelConc n)

Methods

fmap :: (a -> b) -> ModelConc n a -> ModelConc n b

(<$) :: a -> ModelConc n b -> ModelConc n a

MonadFail (ModelConc n)

Methods

fail :: String -> ModelConc n a

Applicative (ModelConc n)

Methods

pure :: a -> ModelConc n a

(<*>) :: ModelConc n (a -> b) -> ModelConc n a -> ModelConc n b

liftA2 :: (a -> b -> c) -> ModelConc n a -> ModelConc n b -> ModelConc n c

(*>) :: ModelConc n a -> ModelConc n b -> ModelConc n b

(<*) :: ModelConc n a -> ModelConc n b -> ModelConc n a

data ModelMVar n a

An MVar is modelled as a unique ID and a reference holding a Maybe value.

Constructors

ModelMVar

Fields

• mvarId :: MVarId
• mvarRef :: CRef n (Maybe a)

data ModelCRef n a

A CRef is modelled as a unique ID and a reference holding thread-local values, the number of commits, and the most recent committed value.

Constructors

ModelCRef

Fields

• crefId :: CRefId
• crefRef :: CRef n (Map ThreadId a, Integer, a)

data ModelTicket a

A Ticket is modelled as the ID of the ModelCRef it came from, the commits to the ModelCRef at the time it was produced, and the value observed.

Constructors

ModelTicket

Fields

• ticketCRef :: CRefId
• ticketWrites :: Integer
• ticketVal :: a

Primitive Actions

data Action n

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. ModelConc n b -> ModelConc n b) -> Action n) (ThreadId -> Action n)

AForkOS String ((forall b. ModelConc n b -> ModelConc n b) -> Action n) (ThreadId -> Action n)

AIsBound (Bool -> Action n)

AMyTId (ThreadId -> Action n)

AGetNumCapabilities (Int -> Action n)

ASetNumCapabilities Int (Action n)

ANewMVar String (ModelMVar n a -> Action n)

APutMVar (ModelMVar n a) a (Action n)

ATryPutMVar (ModelMVar n a) a (Bool -> Action n)

AReadMVar (ModelMVar n a) (a -> Action n)

ATryReadMVar (ModelMVar n a) (Maybe a -> Action n)

ATakeMVar (ModelMVar n a) (a -> Action n)

ATryTakeMVar (ModelMVar n a) (Maybe a -> Action n)

ANewCRef String a (ModelCRef n a -> Action n)

AReadCRef (ModelCRef n a) (a -> Action n)

AReadCRefCas (ModelCRef n a) (ModelTicket a -> Action n)

AModCRef (ModelCRef n a) (a -> (a, b)) (b -> Action n)

AModCRefCas (ModelCRef n a) (a -> (a, b)) (b -> Action n)

AWriteCRef (ModelCRef n a) a (Action n)

ACasCRef (ModelCRef n a) (ModelTicket a) a ((Bool, ModelTicket a) -> Action n)

Exception e => AThrow e

Exception e => AThrowTo ThreadId e (Action n)

Exception e => ACatching (e -> ModelConc n a) (ModelConc n a) (a -> Action n)

APopCatching (Action n)

AMasking MaskingState ((forall b. ModelConc n b -> ModelConc n b) -> ModelConc n a) (a -> Action n)

AResetMask Bool Bool MaskingState (Action n)

AAtom (ModelSTM n a) (a -> Action n)

ALift (n (Action n))

AYield (Action n)

ADelay Int (Action n)

AReturn (Action n)

ACommit ThreadId CRefId

AStop (n ())

ASub (ModelConc n a) (Either Failure a -> Action n)

AStopSub (Action n)

ADontCheck (Maybe Int) (ModelConc n a) (a -> Action n)

Scheduling & Traces

lookahead :: Action n -> Lookahead

Look as far ahead in the given continuation as possible.