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.

Types for Modelling Concurrency

type ModelConc = Program Basic

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.

data Program pty n a where

A representation of a concurrent program for testing.

To construct these, use the MonadConc instance, or see withSetup, withTeardown, and withSetupAndTeardown.

Since: 2.0.0.0

Constructors

ModelConc

Fields

• :: { runModelConc :: (a -> Action n) -> Action n
•    } -> Program Basic n a

WithSetup

Fields

• :: { wsSetup :: ModelConc n x
•    , wsProgram :: x -> ModelConc n a
•    } -> Program (WithSetup x) n a

WithSetupAndTeardown

Fields

• :: { wstSetup :: ModelConc n x
•    , wstProgram :: x -> ModelConc n y
•    , wstTeardown :: x -> Either Condition y -> ModelConc n a
•    } -> Program (WithSetupAndTeardown x y) n a

Instances

pty ~ Basic => MonadTrans (Program pty)

Defined in Test.DejaFu.Conc.Internal.Program

Methods

lift :: Monad m => m a -> Program pty m a

pty ~ Basic => Monad (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

(>>=) :: Program pty n a -> (a -> Program pty n b) -> Program pty n b

(>>) :: Program pty n a -> Program pty n b -> Program pty n b

return :: a -> Program pty n a

fail :: String -> Program pty n a

pty ~ Basic => Functor (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

fmap :: (a -> b) -> Program pty n a -> Program pty n b

(<$) :: a -> Program pty n b -> Program pty n a

pty ~ Basic => MonadFail (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

fail :: String -> Program pty n a

pty ~ Basic => Applicative (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

pure :: a -> Program pty n a

(<*>) :: Program pty n (a -> b) -> Program pty n a -> Program pty n b

liftA2 :: (a -> b -> c) -> Program pty n a -> Program pty n b -> Program pty n c

(*>) :: Program pty n a -> Program pty n b -> Program pty n b

(<*) :: Program pty n a -> Program pty n b -> Program pty n a

(pty ~ Basic, MonadIO n) => MonadIO (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

Methods

liftIO :: IO a -> Program pty n a

(pty ~ Basic, Monad n) => MonadConc (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

Associated Types

type STM (Program pty n) :: Type -> Type

type MVar (Program pty n) :: Type -> Type

type IORef (Program pty n) :: Type -> Type

type Ticket (Program pty n) :: Type -> Type

type ThreadId (Program pty n) :: Type

Methods

forkWithUnmask :: ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n))

forkWithUnmaskN :: String -> ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n))

forkOnWithUnmask :: Int -> ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n))

forkOnWithUnmaskN :: String -> Int -> ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n))

forkOSWithUnmask :: ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n))

forkOSWithUnmaskN :: String -> ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n))

supportsBoundThreads :: Program pty n Bool

isCurrentThreadBound :: Program pty n Bool

getNumCapabilities :: Program pty n Int

setNumCapabilities :: Int -> Program pty n ()

myThreadId :: Program pty n (ThreadId (Program pty n))

yield :: Program pty n ()

threadDelay :: Int -> Program pty n ()

newEmptyMVar :: Program pty n (MVar (Program pty n) a)

newEmptyMVarN :: String -> Program pty n (MVar (Program pty n) a)

putMVar :: MVar (Program pty n) a -> a -> Program pty n ()

tryPutMVar :: MVar (Program pty n) a -> a -> Program pty n Bool

readMVar :: MVar (Program pty n) a -> Program pty n a

tryReadMVar :: MVar (Program pty n) a -> Program pty n (Maybe a)

takeMVar :: MVar (Program pty n) a -> Program pty n a

tryTakeMVar :: MVar (Program pty n) a -> Program pty n (Maybe a)

newIORef :: a -> Program pty n (IORef (Program pty n) a)

newIORefN :: String -> a -> Program pty n (IORef (Program pty n) a)

readIORef :: IORef (Program pty n) a -> Program pty n a

atomicModifyIORef :: IORef (Program pty n) a -> (a -> (a, b)) -> Program pty n b

writeIORef :: IORef (Program pty n) a -> a -> Program pty n ()

atomicWriteIORef :: IORef (Program pty n) a -> a -> Program pty n ()

readForCAS :: IORef (Program pty n) a -> Program pty n (Ticket (Program pty n) a)

peekTicket' :: Proxy (Program pty n) -> Ticket (Program pty n) a -> a

casIORef :: IORef (Program pty n) a -> Ticket (Program pty n) a -> a -> Program pty n (Bool, Ticket (Program pty n) a)

modifyIORefCAS :: IORef (Program pty n) a -> (a -> (a, b)) -> Program pty n b

modifyIORefCAS_ :: IORef (Program pty n) a -> (a -> a) -> Program pty n ()

atomically :: STM (Program pty n) a -> Program pty n a

readTVarConc :: TVar (STM (Program pty n)) a -> Program pty n a

throwTo :: Exception e => ThreadId (Program pty n) -> e -> Program pty n ()

pty ~ Basic => MonadThrow (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

Methods

throwM :: Exception e => e -> Program pty n a

pty ~ Basic => MonadCatch (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

Methods

catch :: Exception e => Program pty n a -> (e -> Program pty n a) -> Program pty n a

pty ~ Basic => MonadMask (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

Methods

mask :: ((forall a. Program pty n a -> Program pty n a) -> Program pty n b) -> Program pty n b

uninterruptibleMask :: ((forall a. Program pty n a -> Program pty n a) -> Program pty n b) -> Program pty n b

generalBracket :: Program pty n a -> (a -> ExitCase b -> Program pty n c) -> (a -> Program pty n b) -> Program pty n (b, c)

type ThreadId (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

type ThreadId (Program pty n) = ThreadId

type Ticket (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

type Ticket (Program pty n) = ModelTicket

type IORef (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

type IORef (Program pty n) = ModelIORef n

type MVar (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

type MVar (Program pty n) = ModelMVar n

type STM (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

type STM (Program pty n) = ModelSTM n

data Basic

A type used to constrain Program: a Program Basic is a "basic" program with no set-up or teardown.

Construct with the MonadConc instance.

Since: 2.0.0.0

data WithSetup x

A type used to constrain Program: a Program (WithSetup x) is a program with some set-up action producing a value of type x.

Construct with withSetup.

Since: 2.0.0.0

data WithSetupAndTeardown x y

A type used to constrain Program: a Program (WithSetupAndTeardown x y) is a program producing a value of type y with some set-up action producing a value of type x and a teardown action producing the final result.

Construct with withTeardown or withSetupAndTeardown.

Since: 2.0.0.0

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 :: Ref n (Maybe a)

data ModelIORef n a

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

Constructors

ModelIORef

Fields

• iorefId :: IORefId
• iorefRef :: Ref n (Map ThreadId a, Integer, a)

data ModelTicket a

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

Constructors

ModelTicket

Fields

• ticketIORef :: IORefId
• 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)

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

ANewIORef String a (ModelIORef n a -> Action n)

AReadIORef (ModelIORef n a) (a -> Action n)

AReadIORefCas (ModelIORef n a) (ModelTicket a -> Action n)

AModIORef (ModelIORef n a) (a -> (a, b)) (b -> Action n)

AModIORefCas (ModelIORef n a) (a -> (a, b)) (b -> Action n)

AWriteIORef (ModelIORef n a) a (Action n)

ACasIORef (ModelIORef 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 IORefId

AStop (n ())

ANewInvariant (Invariant n ()) (Action n)

Scheduling & Traces

lookahead :: Action n -> Lookahead

Look as far ahead in the given continuation as possible.

Invariants

newtype Invariant n a

Invariants are atomic actions which can inspect the shared state of your computation, and terminate it on failure. Invariants have no visible effects, and are checked after each scheduling point.

To be checked, an invariant must be created during the setup phase of your Program, using registerInvariant. The invariant will then be checked in the main phase (but not in the setup or teardown phase). As a consequence of this, any shared state you want your invariant to check must also be created in the setup phase, and passed into the main phase as a parameter.

Since: 2.0.0.0

Constructors

Invariant

Fields

• runInvariant :: (a -> IAction n) -> IAction n

Instances

Monad (Invariant n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

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

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

return :: a -> Invariant n a

fail :: String -> Invariant n a

Functor (Invariant n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

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

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

MonadFail (Invariant n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

fail :: String -> Invariant n a

Applicative (Invariant n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

pure :: a -> Invariant n a

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

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

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

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

MonadThrow (Invariant n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

throwM :: Exception e => e -> Invariant n a

MonadCatch (Invariant n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

catch :: Exception e => Invariant n a -> (e -> Invariant n a) -> Invariant n a

data IAction n

Invariants are represented as a sequence of primitive actions.

Constructors

IInspectIORef (ModelIORef n a) (a -> IAction n)

IInspectMVar (ModelMVar n a) (Maybe a -> IAction n)

IInspectTVar (ModelTVar n a) (a -> IAction n)

Exception e => ICatch (e -> Invariant n a) (Invariant n a) (a -> IAction n)

Exception e => IThrow e

IStop (n ())