dejafu- Systematic testing for Haskell concurrency.

Copyright(c) 2016 Michael Walker
MaintainerMichael Walker <>
PortabilityCPP, ExistentialQuantification, RankNTypes
Safe HaskellNone




Common types and utility functions for deterministic execution of MonadConc implementations. This module is NOT considered to form


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.





Monad (M n r) Source # 


(>>=) :: 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 # 


fmap :: (a -> b) -> M n r a -> M n r b #

(<$) :: a -> M n r b -> M n r a #

MonadFail (M n r) Source #



fail :: String -> M n r a #

Applicative (M n r) Source # 


pure :: 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.




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.





MonadRef (CRef r) (ConcT r n) # 


newRef :: a -> ConcT r n (CRef r a) #

readRef :: CRef r a -> ConcT r n a #

writeRef :: CRef r a -> a -> ConcT r n () #

modifyRef :: CRef r a -> (a -> a) -> ConcT r n () #

modifyRef' :: CRef r a -> (a -> a) -> ConcT r n () #

MonadAtomicRef (CRef r) (ConcT r n) # 


atomicModifyRef :: CRef r a -> (a -> (a, b)) -> ConcT r n b #

atomicModifyRef' :: CRef r a -> (a -> (a, b)) -> ConcT r n b #

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.



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.


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) 
ADelay Int (Action n r) 
AReturn (Action n r) 
ACommit ThreadId CRefId 
AStop (n ()) 
ASub (M n r a) (Either Failure a -> Action n r) 
AStopSub (Action n r) 

Scheduling & Traces

lookahead :: Action n r -> Lookahead Source #

Look as far ahead in the given continuation as possible.