dejafu-0.5.0.0: Systematic testing for Haskell concurrency.

Copyright (c) 2016 Michael Walker MIT Michael Walker experimental ExistentialQuantification, RankNTypes None 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

Synopsis

# The Conc Monad

newtype M n r a 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.

Constructors

 M FieldsrunM :: (a -> Action n r) -> Action n r

Instances

 Monad (M n r) Source # Methods(>>=) :: M n r a -> (a -> M n r b) -> M n r b #(>>) :: M n r a -> M n r b -> M n r b #return :: a -> M n r a #fail :: String -> M n r a # Functor (M n r) Source # Methodsfmap :: (a -> b) -> M n r a -> M n r b #(<\$) :: a -> M n r b -> M n r a # Applicative (M n r) Source # Methodspure :: a -> M n r a #(<*>) :: M n r (a -> b) -> M n r a -> M n r b #(*>) :: M n r a -> M n r b -> M n r b #(<*) :: M n r a -> M n r b -> M n r a #

data MVar r a Source #

The concurrent variable type used with the Conc monad. One notable difference between these and MVars is that MVars are single-wakeup, and wake up in a FIFO order. Writing to a MVar wakes up all threads blocked on reading it, and it is up to the scheduler which one runs next. Taking from a MVar behaves analogously.

Constructors

 MVar Fields_cvarId :: MVarId _cvarVal :: r (Maybe a)

data CRef r a Source #

The mutable non-blocking reference type. These are like IORefs.

CRefs are represented as a unique numeric identifier and a reference containing (a) any thread-local non-synchronised writes (so each thread sees its latest write), (b) a commit count (used in compare-and-swaps), and (c) the current value visible to all threads.

Constructors

 CRef Fields_crefId :: CRefId _crefVal :: r (Map ThreadId a, Integer, a)

data Ticket a Source #

The compare-and-swap proof type.

Tickets are represented as just a wrapper around the identifier of the CRef it came from, the commit count at the time it was produced, and an a value. This doesn't work in the source package (atomic-primops) because of the need to use pointer equality. Here we can just pack extra information into CRef to avoid that need.

Constructors

 Ticket Fields_ticketCRef :: CRefId _ticketWrites :: Integer _ticketVal :: a

cont :: ((a -> Action n r) -> Action n r) -> M n r a Source #

Construct a continuation-passing operation from a function.

runCont :: M n r a -> (a -> Action n r) -> Action n r Source #

Run a CPS computation with the given final computation.

# Primitive Actions

data Action n r 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. M n r b -> M n r b) -> Action n r) (ThreadId -> Action n r) AMyTId (ThreadId -> Action n r) AGetNumCapabilities (Int -> Action n r) ASetNumCapabilities Int (Action n r) ANewMVar String (MVar r a -> Action n r) APutMVar (MVar r a) a (Action n r) ATryPutMVar (MVar r a) a (Bool -> Action n r) AReadMVar (MVar r a) (a -> Action n r) ATryReadMVar (MVar r a) (Maybe a -> Action n r) ATakeMVar (MVar r a) (a -> Action n r) ATryTakeMVar (MVar r a) (Maybe a -> Action n r) ANewCRef String a (CRef r a -> Action n r) AReadCRef (CRef r a) (a -> Action n r) AReadCRefCas (CRef r a) (Ticket a -> Action n r) AModCRef (CRef r a) (a -> (a, b)) (b -> Action n r) AModCRefCas (CRef r a) (a -> (a, b)) (b -> Action n r) AWriteCRef (CRef r a) a (Action n r) ACasCRef (CRef r a) (Ticket a) a ((Bool, Ticket a) -> Action n r) Exception e => AThrow e Exception e => AThrowTo ThreadId e (Action n r) Exception e => ACatching (e -> M n r a) (M n r a) (a -> Action n r) APopCatching (Action n r) AMasking MaskingState ((forall b. M n r b -> M n r b) -> M n r a) (a -> Action n r) AResetMask Bool Bool MaskingState (Action n r) AAtom (STMLike n r a) (a -> Action n r) ALift (n (Action n r)) AYield (Action n r) AReturn (Action n r) ACommit ThreadId CRefId AStop (n ()) ASub (M n r a) (Either Failure a -> Action n r)

# Scheduling & Traces

Look as far ahead in the given continuation as possible.