Copyright	(c) 2016--2020 Michael Walker
License	MIT
Maintainer	Michael Walker <mike@barrucadu.co.uk>
Stability	experimental
Portability	CPP, ExistentialQuantification, GADTs, RankNTypes
Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.DejaFu.Conc.Internal.Common

Contents

Types for Modelling Concurrency
- Primitive Actions
- Scheduling & Traces
Invariants

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

type ModelConc = Program Basic
data Program pty n a where
- ModelConc :: {..} -> Program Basic n a
- WithSetup :: {..} -> Program (WithSetup x) n a
- WithSetupAndTeardown :: {..} -> Program (WithSetupAndTeardown x y) n a
data Basic
data WithSetup x
data WithSetupAndTeardown x y
data ModelMVar n a = ModelMVar {
- mvarId :: MVarId
- mvarRef :: Ref n (Maybe a)
}
data ModelIORef n a = ModelIORef {
- iorefId :: IORefId
- iorefRef :: Ref n (Map ThreadId a, Integer, a)
}
data ModelTicket a = ModelTicket {
- ticketIORef :: IORefId
- ticketWrites :: Integer
- ticketVal :: a
}
data Action n
- = 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)
lookahead :: Action n -> Lookahead
newtype Invariant n a = Invariant {
- runInvariant :: (a -> IAction n) -> IAction n
}
data IAction n
- = 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 ())

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 :: { 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

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 => MonadFail (Program pty n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Common Methods fail :: String -> 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 => 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 => 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 => 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, 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 => 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) #
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 #
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
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

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

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 iorefId :: IORefId iorefRef :: Ref n (Map ThreadId a, Integer, a)

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
Fields ticketIORef :: IORefId ticketWrites :: Integer ticketVal :: a

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 runInvariant :: (a -> IAction n) -> IAction n

Instances

Instances details

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 #
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 #
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 #
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 #
MonadThrow (Invariant n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Common Methods throwM :: Exception e => e -> 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 ())