Copyright | (c) 2016--2020 Michael Walker |
---|---|
License | MIT |
Maintainer | Michael Walker <mike@barrucadu.co.uk> |
Stability | experimental |
Portability | CPP, ExistentialQuantification, GADTs, RankNTypes |
Safe Haskell | None |
Language | Haskell2010 |
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
- 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 {}
- data ModelIORef n a = ModelIORef {}
- 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 Action
s.
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 | |
WithSetupAndTeardown | |
Fields
|
Instances
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 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
An MVar
is modelled as a unique ID and a reference holding a
Maybe
value.
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.
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
|
Primitive Actions
Scheduling is done in terms of a trace of Action
s. 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
Scheduling & Traces
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
Monad (Invariant n) Source # | |
Functor (Invariant n) Source # | |
MonadFail (Invariant n) Source # | |
Defined in Test.DejaFu.Conc.Internal.Common | |
Applicative (Invariant n) Source # | |
Defined in Test.DejaFu.Conc.Internal.Common | |
MonadThrow (Invariant n) Source # | |
Defined in Test.DejaFu.Conc.Internal.Common | |
MonadCatch (Invariant 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 ()) |