dejafu-2.4.0.3: A library for unit-testing concurrent programs.
Copyright(c) 2016--2020 Michael Walker
LicenseMIT
MaintainerMichael Walker <mike@barrucadu.co.uk>
Stabilityexperimental
PortabilityCPP, ExistentialQuantification, GADTs, RankNTypes
Safe HaskellNone
LanguageHaskell2010

Test.DejaFu.Conc.Internal.Common

Description

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.

Synopsis

Types for Modelling Concurrency

type ModelConc = Program Basic Source #

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 Source #

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

WithSetup 

Fields

WithSetupAndTeardown 

Fields

Instances

Instances details
pty ~ Basic => MonadTrans (Program pty) Source # 
Instance details

Defined in Test.DejaFu.Conc.Internal.Program

Methods

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

pty ~ Basic => Monad (Program pty n) Source # 
Instance details

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 #

pty ~ Basic => Functor (Program pty n) Source # 
Instance details

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) Source # 
Instance details

Defined in Test.DejaFu.Conc.Internal.Common

Methods

fail :: String -> Program pty n a #

pty ~ Basic => Applicative (Program pty n) Source # 
Instance details

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) Source # 
Instance details

Defined in Test.DejaFu.Conc.Internal.Program

Methods

liftIO :: IO a -> Program pty n a #

(pty ~ Basic, Monad n) => MonadConc (Program pty n) Source # 
Instance details

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

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 #

newTVarConc :: a -> Program pty n (TVar (STM (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 () #

getMaskingState :: Program pty n MaskingState #

unsafeUnmask :: Program pty n a -> Program pty n a #

pty ~ Basic => MonadThrow (Program pty n) Source # 
Instance details

Defined in Test.DejaFu.Conc.Internal.Program

Methods

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

pty ~ Basic => MonadCatch (Program pty n) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Defined in Test.DejaFu.Conc.Internal.Program

type ThreadId (Program pty n) = ThreadId
type Ticket (Program pty n) Source # 
Instance details

Defined in Test.DejaFu.Conc.Internal.Program

type Ticket (Program pty n) = ModelTicket
type IORef (Program pty n) Source # 
Instance details

Defined in Test.DejaFu.Conc.Internal.Program

type IORef (Program pty n) = ModelIORef n
type MVar (Program pty n) Source # 
Instance details

Defined in Test.DejaFu.Conc.Internal.Program

type MVar (Program pty n) = ModelMVar n
type STM (Program pty n) Source # 
Instance details

Defined in Test.DejaFu.Conc.Internal.Program

type STM (Program pty n) = ModelSTM n

data Basic Source #

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 Source #

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 Source #

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 Source #

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

Constructors

ModelMVar 

Fields

data ModelIORef n a Source #

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

data ModelTicket a Source #

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 

Primitive Actions

data Action n Source #

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) 
forall a. ANewMVar String (ModelMVar n a -> Action n) 
forall a. APutMVar (ModelMVar n a) a (Action n) 
forall a. ATryPutMVar (ModelMVar n a) a (Bool -> Action n) 
forall a. AReadMVar (ModelMVar n a) (a -> Action n) 
forall a. ATryReadMVar (ModelMVar n a) (Maybe a -> Action n) 
forall a. ATakeMVar (ModelMVar n a) (a -> Action n) 
forall a. ATryTakeMVar (ModelMVar n a) (Maybe a -> Action n) 
forall a. ANewIORef String a (ModelIORef n a -> Action n) 
forall a. AReadIORef (ModelIORef n a) (a -> Action n) 
forall a. AReadIORefCas (ModelIORef n a) (ModelTicket a -> Action n) 
forall a b. AModIORef (ModelIORef n a) (a -> (a, b)) (b -> Action n) 
forall a b. AModIORefCas (ModelIORef n a) (a -> (a, b)) (b -> Action n) 
forall a. AWriteIORef (ModelIORef n a) a (Action n) 
forall a. ACasIORef (ModelIORef n a) (ModelTicket a) a ((Bool, ModelTicket a) -> Action n) 
forall e.Exception e => AThrow e 
forall e.Exception e => AThrowTo ThreadId e (Action n) 
forall a e.Exception e => ACatching (e -> ModelConc n a) (ModelConc n a) (a -> Action n) 
APopCatching (Action n) 
forall a. AMasking MaskingState ((forall b. ModelConc n b -> ModelConc n b) -> ModelConc n a) (a -> Action n) 
AResetMask Bool Bool MaskingState (Action n) 
AGetMasking (MaskingState -> Action n) 
forall a. 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 Source #

Look as far ahead in the given continuation as possible.

Invariants

newtype Invariant n a Source #

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

Instances

Instances details
Monad (Invariant n) Source # 
Instance details

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 #

Functor (Invariant n) Source # 
Instance details

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) Source # 
Instance details

Defined in Test.DejaFu.Conc.Internal.Common

Methods

fail :: String -> Invariant n a #

Applicative (Invariant n) Source # 
Instance details

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) Source # 
Instance details

Defined in Test.DejaFu.Conc.Internal.Common

Methods

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

MonadCatch (Invariant n) Source # 
Instance details

Defined in Test.DejaFu.Conc.Internal.Common

Methods

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

data IAction n Source #

Invariants are represented as a sequence of primitive actions.

Constructors

forall a. IInspectIORef (ModelIORef n a) (a -> IAction n) 
forall a. IInspectMVar (ModelMVar n a) (Maybe a -> IAction n) 
forall a. IInspectTVar (ModelTVar n a) (a -> IAction n) 
forall a e.Exception e => ICatch (e -> Invariant n a) (Invariant n a) (a -> IAction n) 
forall e.Exception e => IThrow e 
IStop (n ())