diff --git a/Control/Concurrent/CVar.hs b/Control/Concurrent/CVar.hs
deleted file mode 100644
--- a/Control/Concurrent/CVar.hs
+++ /dev/null
@@ -1,123 +0,0 @@
--- | Combinators using @CVar@s. These provide many of the helpful
--- functions found in Control.Concurrent.MVar, but for @CVar@s.
-module Control.Concurrent.CVar
- ( -- *@CVar@s
-  CVar
- , newEmptyCVar
- , newCVar
- , takeCVar
- , putCVar
- , readCVar
- , swapCVar
- , tryTakeCVar
- , tryPutCVar
- , isEmptyCVar
- , withCVar
- , withCVarMasked
- , modifyCVar_
- , modifyCVar
- , modifyCVarMasked_
- , modifyCVarMasked
-
- -- * Binary semaphores
- -- | A common use of @CVar@s is in making binary semaphores to
- -- control mutual exclusion over a resource, so a couple of helper
- -- functions are provided.
- , lock
- , unlock
- ) where
-
-import Control.Monad (liftM)
-import Control.Monad.Catch (mask_, onException)
-import Control.Monad.Conc.Class
-
--- | Create a new @CVar@ containing a value.
-newCVar :: MonadConc m => a -> m (CVar m a)
-newCVar a = do
-  cvar <- newEmptyCVar
-  putCVar cvar a
-  return cvar
-
--- | Swap the contents of a @CVar@, and return the value taken. This
--- function is atomic only if there are no other producers fro this
--- @CVar@.
-swapCVar :: MonadConc m => CVar m a -> a -> m a
-swapCVar cvar a = mask_ $ do
-  old <- takeCVar cvar
-  putCVar cvar a
-  return old
-
--- | Check if a @CVar@ is empty.
-isEmptyCVar :: MonadConc m => CVar m a -> m Bool
-isEmptyCVar cvar = do
-  val <- tryTakeCVar cvar
-  case val of
-    Just val' -> putCVar cvar val' >> return True
-    Nothing   -> return False
-
--- | Operate on the contents of a @CVar@, replacing the contents after
--- finishing. This operation is exception-safe: it will replace the
--- original contents of the @CVar@ if an exception is raised. However,
--- it is only atomic if there are no other producers for this @CVar@.
-{-# INLINE withCVar #-}
-withCVar :: MonadConc m => CVar m a -> (a -> m b) -> m b
-withCVar cvar f = mask $ \restore -> do
-  val <- takeCVar cvar
-  out <- restore (f val) `onException` putCVar cvar val
-  putCVar cvar val
-
-  return out
-
--- | Like 'withCVar', but the @IO@ action in the second argument is
--- executed with asynchronous exceptions masked.
-{-# INLINE withCVarMasked #-}
-withCVarMasked :: MonadConc m => CVar m a -> (a -> m b) -> m b
-withCVarMasked cvar f = mask_ $ do
-  val <- takeCVar cvar
-  out <- f val `onException` putCVar cvar val
-  putCVar cvar val
-
-  return out
-
--- | An exception-safe wrapper for modifying the contents of a @CVar@.
--- Like 'withCVar', 'modifyCVar' will replace the original contents of
--- the @CVar@ if an exception is raised during the operation. This
--- function is only atomic if there are no other producers for this
--- @CVar@.
-{-# INLINE modifyCVar_ #-}
-modifyCVar_ :: MonadConc m => CVar m a -> (a -> m a) -> m ()
-modifyCVar_ cvar f = modifyCVar cvar $ liftM (\a -> (a,())) . f
-
--- | A slight variation on 'modifyCVar_' that allows a value to be
--- returned (@b@) in addition to the modified value of the @CVar@.
-{-# INLINE modifyCVar #-}
-modifyCVar :: MonadConc m => CVar m a -> (a -> m (a, b)) -> m b
-modifyCVar cvar f = mask $ \restore -> do
-  val <- takeCVar cvar
-  (val', out) <- restore (f val) `onException` putCVar cvar val
-  putCVar cvar val'
-  return out
-
--- | Like 'modifyCVar_', but the @IO@ action in the second argument is
--- executed with asynchronous exceptions masked.
-{-# INLINE modifyCVarMasked_ #-}
-modifyCVarMasked_ :: MonadConc m => CVar m a -> (a -> m a) -> m ()
-modifyCVarMasked_ cvar f = modifyCVarMasked cvar $ liftM (\a -> (a,())) . f
-
--- | Like 'modifyCVar', but the @IO@ action in the second argument is
--- executed with asynchronous exceptions masked.
-{-# INLINE modifyCVarMasked #-}
-modifyCVarMasked :: MonadConc m => CVar m a -> (a -> m (a, b)) -> m b
-modifyCVarMasked cvar f = mask_ $ do
-  val <- takeCVar cvar
-  (val', out) <- f val `onException` putCVar cvar val
-  putCVar cvar val'
-  return out
-
--- | Put a @()@ into a @CVar@, claiming the lock. This is atomic.
-lock :: MonadConc m => CVar m () -> m ()
-lock = flip putCVar ()
-
--- | Empty a @CVar@, releasing the lock. This is atomic.
-unlock :: MonadConc m => CVar m () -> m ()
-unlock = takeCVar
diff --git a/Control/Concurrent/CVar/Strict.hs b/Control/Concurrent/CVar/Strict.hs
deleted file mode 100644
--- a/Control/Concurrent/CVar/Strict.hs
+++ /dev/null
@@ -1,97 +0,0 @@
--- | Strict alternatives to the functions in
--- Control.Monad.Conc.CVar. Specifically, values are evaluated to
--- normal form before being put into a @CVar@.
-module Control.Concurrent.CVar.Strict
- ( -- *@CVar@s
-  CVar
- , newEmptyCVar
- , newCVar
- , takeCVar
- , putCVar
- , readCVar
- , swapCVar
- , tryTakeCVar
- , tryPutCVar
- , isEmptyCVar
- , withCVar
- , withCVarMasked
- , modifyCVar_
- , modifyCVar
- , modifyCVarMasked_
- , modifyCVarMasked
-
- -- * Binary semaphores
- -- | A common use of @CVar@s is in making binary semaphores to
- -- control mutual exclusion over a resource, so a couple of helper
- -- functions are provided.
- , lock
- , unlock
- ) where
-
-import Control.Concurrent.CVar (isEmptyCVar, withCVar, withCVarMasked, lock, unlock)
-import Control.DeepSeq (NFData, force)
-import Control.Monad (liftM)
-import Control.Monad.Catch (mask_, onException)
-import Control.Monad.Conc.Class hiding (newEmptyCVar, putCVar, tryPutCVar)
-
-import qualified Control.Concurrent.CVar  as V
-import qualified Control.Monad.Conc.Class as C
-
--- | Create a new empty @CVar@.
-newEmptyCVar :: (MonadConc m, NFData a) => m (CVar m a)
-newEmptyCVar = C.newEmptyCVar
-
--- | Create a new @CVar@ containing a value.
-newCVar :: (MonadConc m, NFData a) => a -> m (CVar m a)
-newCVar = V.newCVar . force
-
--- | Swap the contents of a @CVar@, and return the value taken.
-swapCVar :: (MonadConc m, NFData a) => CVar m a -> a -> m a
-swapCVar cvar = V.swapCVar cvar . force
-
--- | Put a value into a @CVar@. If there is already a value there,
--- this will block until that value has been taken, at which point the
--- value will be stored.
-putCVar :: (MonadConc m, NFData a) => CVar m a -> a -> m ()
-putCVar cvar = C.putCVar cvar . force
-
--- | Attempt to put a value in a @CVar@, returning 'True' (and filling
--- the @CVar@) if there was nothing there, otherwise returning
--- 'False'.
-tryPutCVar :: (MonadConc m, NFData a) => CVar m a -> a -> m Bool
-tryPutCVar cvar = C.tryPutCVar cvar . force
-
--- | An exception-safe wrapper for modifying the contents of a @CVar@.
--- Like 'withCVar', 'modifyCVar' will replace the original contents of
--- the @CVar@ if an exception is raised during the operation. This
--- function is only atomic if there are no other producers for this
--- @CVar@.
-{-# INLINE modifyCVar_ #-}
-modifyCVar_ :: (MonadConc m, NFData a) => CVar m a -> (a -> m a) -> m ()
-modifyCVar_ cvar f = modifyCVar cvar $ liftM (\a -> (a,())) . f
-
--- | A slight variation on 'modifyCVar_' that allows a value to be
--- returned (@b@) in addition to the modified value of the @CVar@.
-{-# INLINE modifyCVar #-}
-modifyCVar :: (MonadConc m, NFData a) => CVar m a -> (a -> m (a, b)) -> m b
-modifyCVar cvar f = mask $ \restore -> do
-  val <- takeCVar cvar
-  (val', out) <- restore (f val) `onException` putCVar cvar val
-  putCVar cvar val'
-  return out
-
--- | Like 'modifyCVar_', but the @IO@ action in the second argument is
--- executed with asynchronous exceptions masked.
-{-# INLINE modifyCVarMasked_ #-}
-modifyCVarMasked_ :: (MonadConc m, NFData a) => CVar m a -> (a -> m a) -> m ()
-modifyCVarMasked_ cvar f = modifyCVarMasked cvar $ liftM (\a -> (a,())) . f
-
--- | Like 'modifyCVar', but the @IO@ action in the second argument is
--- executed with asynchronous exceptions masked.
-{-# INLINE modifyCVarMasked #-}
-modifyCVarMasked :: (MonadConc m, NFData a) => CVar m a -> (a -> m (a, b)) -> m b
-modifyCVarMasked cvar f = mask_ $ do
-  val <- takeCVar cvar
-  (val', out) <- f val `onException` putCVar cvar val
-  putCVar cvar val'
-  return out
diff --git a/Control/Concurrent/Classy.hs b/Control/Concurrent/Classy.hs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/Classy.hs
@@ -0,0 +1,32 @@
+-- | Classy concurrency.
+--
+-- Concurrency is \"lightweight\", which means that both thread
+-- creation and context switching overheads are extremely
+-- low. Scheduling of Haskell threads is done internally in the
+-- Haskell runtime system, and doesn't make use of any operating
+-- system-supplied thread packages.
+--
+-- Haskell threads can communicate via @MVar@s, a kind of synchronised
+-- mutable variable (see "Control.Concurrent.Classy.MVar"). Several
+-- common concurrency abstractions can be built from @MVar@s, and
+-- these are provided by the "Control.Concurrent.Classy"
+-- library. Threads may also communicate via exceptions.
+module Control.Concurrent.Classy
+  ( module Control.Monad.Conc.Class
+  , module Control.Concurrent.Classy.Chan
+  , module Control.Concurrent.Classy.CRef
+  , module Control.Concurrent.Classy.MVar
+  , module Control.Concurrent.Classy.STM
+  , module Control.Concurrent.Classy.QSem
+  , module Control.Concurrent.Classy.QSemN
+  ) where
+
+import Control.Monad.Conc.Class
+import Control.Concurrent.Classy.Chan
+import Control.Concurrent.Classy.CRef
+import Control.Concurrent.Classy.MVar
+import Control.Concurrent.Classy.STM
+import Control.Concurrent.Classy.QSem
+import Control.Concurrent.Classy.QSemN
+
+{-# ANN module ("HLint: ignore Use import/export shortcut" :: String) #-}
diff --git a/Control/Concurrent/Classy/CRef.hs b/Control/Concurrent/Classy/CRef.hs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/Classy/CRef.hs
@@ -0,0 +1,106 @@
+-- | Mutable references in a concurrency monad.
+--
+-- __Deviations:__ There is no @Eq@ instance for @MonadConc@ the
+-- @CRef@ type. Furthermore, the @mkWeakIORef@ function is not
+-- provided.
+module Control.Concurrent.Classy.CRef
+  ( -- * CRefs
+    newCRef
+  , readCRef
+  , writeCRef
+  , modifyCRef
+  , modifyCRef'
+  , atomicModifyCRef
+  , atomicModifyCRef'
+  , atomicWriteCRef
+
+  -- * Memory Model
+
+  -- | In a concurrent program, @CRef@ operations may appear
+  -- out-of-order to another thread, depending on the memory model of
+  -- the underlying processor architecture. For example, on x86 (which
+  -- uses total store order), loads can move ahead of stores. Consider
+  -- this example:
+  --
+  -- > crefs :: MonadConc m => m (Bool, Bool)
+  -- > crefs = do
+  -- >   r1 <- newCRef False
+  -- >   r2 <- newCRef False
+  -- >
+  -- >   x <- spawn $ writeCRef r1 True >> readCRef r2
+  -- >   y <- spawn $ writeCRef r2 True >> readCRef r1
+  -- >
+  -- >   (,) <$> readCVar x <*> readCVar y
+  --
+  -- Under a sequentially consistent memory model the possible results
+  -- are @(True, True)@, @(True, False)@, and @(False, True)@. Under
+  -- total or partial store order, @(False, False)@ is also a possible
+  -- result, even though there is no interleaving of the threads which
+  -- can lead to this.
+  --
+  -- We can see this by testing with different memory models:
+  --
+  -- > > autocheck' SequentialConsistency crefs
+  -- > [pass] Never Deadlocks (checked: 6)
+  -- > [pass] No Exceptions (checked: 6)
+  -- > [fail] Consistent Result (checked: 5)
+  -- >         (False,True) S0-------S1-----S0--S2-----S0---
+  -- >         (True,False) S0-------S1-P2-----S1----S0----
+  -- >         (True,True) S0-------S1--P2-----S1---S0----
+  -- >         (False,True) S0-------S1---P2-----S1--S0----
+  -- >         (True,False) S0-------S2-----S1-----S0----
+  -- >         ...
+  -- > False
+  --
+  -- > > autocheck' TotalStoreOrder crefs
+  -- > [pass] Never Deadlocks (checked: 303)
+  -- > [pass] No Exceptions (checked: 303)
+  -- > [fail] Consistent Result (checked: 302)
+  -- >         (False,True) S0-------S1-----C-S0--S2-----C-S0---
+  -- >         (True,False) S0-------S1-P2-----C-S1----S0----
+  -- >         (True,True) S0-------S1-P2--C-S1----C-S0--S2---S0---
+  -- >         (False,True) S0-------S1-P2--P1--C-C-S1--S0--S2---S0---
+  -- >         (False,False) S0-------S1-P2--P1----S2---C-C-S0----
+  -- >         ...
+  -- > False
+  --
+  -- Traces for non-sequentially-consistent memory models show where
+  -- writes to @CRef@s are /committed/, which makes a write visible to
+  -- all threads rather than just the one which performed the
+  -- write. Only 'writeCRef' is broken up into separate write and
+  -- commit steps, 'atomicModifyCRef' is still atomic and imposes a
+  -- memory barrier.
+  ) where
+
+import Control.Monad.Conc.Class
+
+-- | Mutate the contents of a @CRef@.
+--
+-- Be warned that 'modifyCRef' does not apply the function strictly.
+-- This means if the program calls 'modifyCRef' many times, but
+-- seldomly uses the value, thunks will pile up in memory resulting in
+-- a space leak. This is a common mistake made when using a @CRef@ as
+-- a counter. For example, the following will likely produce a stack
+-- overflow:
+--
+-- >ref <- newCRef 0
+-- >replicateM_ 1000000 $ modifyCRef ref (+1)
+-- >readCRef ref >>= print
+--
+-- To avoid this problem, use 'modifyCRef'' instead.
+modifyCRef :: MonadConc m => CRef m a -> (a -> a) -> m ()
+modifyCRef ref f = readCRef ref >>= writeCRef ref . f
+
+-- | Strict version of 'modifyCRef'
+modifyCRef' :: MonadConc m => CRef m a -> (a -> a) -> m ()
+modifyCRef' ref f = do
+  x <- readCRef ref
+  writeCRef ref $! f x
+
+-- | Strict version of 'atomicModifyCRef'. This forces both the value
+-- stored in the @CRef@ as well as the value returned.
+atomicModifyCRef' :: MonadConc m => CRef m a -> (a -> (a,b)) -> m b
+atomicModifyCRef' ref f = do
+  b <- atomicModifyCRef ref $ \a -> case f a of
+    v@(a',_) -> a' `seq` v
+  pure $! b
diff --git a/Control/Concurrent/Classy/Chan.hs b/Control/Concurrent/Classy/Chan.hs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/Classy/Chan.hs
@@ -0,0 +1,71 @@
+-- | Unbounded channels.
+--
+-- __Deviations:__ @Chan@ as defined here does not have an @Eq@
+-- instance, this is because the @MonadConc@ @MVar@ type does not have
+-- an @Eq@ constraint. The deprecated @unGetChan@ and @isEmptyCHan@
+-- functions are not provided. Furthermore, the @getChanContents@
+-- function is not provided as it needs unsafe I/O.
+module Control.Concurrent.Classy.Chan
+  ( -- * The 'Chan' type
+    Chan
+
+  -- * Operations
+  , newChan
+  , writeChan
+  , readChan
+  , dupChan
+
+  -- * Stream interface
+  , writeList2Chan
+  ) where
+
+import Control.Concurrent.Classy.MVar
+import Control.Monad.Catch (mask_)
+import Control.Monad.Conc.Class (MonadConc)
+
+-- | 'Chan' is an abstract type representing an unbounded FIFO
+-- channel.
+data Chan m a
+  = Chan (MVar m (Stream m a))
+         (MVar m (Stream m a)) -- Invariant: the Stream a is always an empty MVar
+
+type Stream m a = MVar m (ChItem m a)
+
+data ChItem m a = ChItem a (Stream m a)
+
+-- | Build and returns a new instance of 'Chan'.
+newChan :: MonadConc m => m (Chan m a)
+newChan = do
+  hole  <- newEmptyMVar
+  readVar  <- newMVar hole
+  writeVar <- newMVar hole
+  pure (Chan readVar writeVar)
+
+-- | Write a value to a 'Chan'.
+writeChan :: MonadConc m => Chan m a -> a -> m ()
+writeChan (Chan _ writeVar) val = do
+  new_hole <- newEmptyMVar
+  mask_ $ do
+    old_hole <- takeMVar writeVar
+    putMVar old_hole (ChItem val new_hole)
+    putMVar writeVar new_hole
+
+-- | Read the next value from the 'Chan'.
+readChan :: MonadConc m => Chan m a -> m a
+readChan (Chan readVar _) =  modifyMVarMasked readVar $ \read_end -> do
+  (ChItem val new_read_end) <- readMVar read_end
+  pure (new_read_end, val)
+
+-- | Duplicate a 'Chan': the duplicate channel begins empty, but data
+-- written to either channel from then on will be available from both.
+-- Hence this creates a kind of broadcast channel, where data written
+-- by anyone is seen by everyone else.
+dupChan :: MonadConc m => Chan m a -> m (Chan m a)
+dupChan (Chan _ writeVar) = do
+  hole       <- readMVar writeVar
+  newReadVar <- newMVar hole
+  pure (Chan newReadVar writeVar)
+
+-- | Write an entire list of items to a 'Chan'.
+writeList2Chan :: MonadConc m => Chan m a -> [a] -> m ()
+writeList2Chan = mapM_ . writeChan
diff --git a/Control/Concurrent/Classy/MVar.hs b/Control/Concurrent/Classy/MVar.hs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/Classy/MVar.hs
@@ -0,0 +1,120 @@
+-- | An @'MVar' t@ is mutable location that is either empty or contains a
+-- value of type @t@.  It has two fundamental operations: 'putMVar'
+-- which fills an 'MVar' if it is empty and blocks otherwise, and
+-- 'takeMVar' which empties an 'MVar' if it is full and blocks
+-- otherwise.  They can be used in multiple different ways:
+--
+--   1. As synchronized mutable variables,
+--
+--   2. As channels, with 'takeMVar' and 'putMVar' as receive and
+--      send, and
+--
+--   3. As a binary semaphore @'MVar' ()@, with 'takeMVar' and
+--      'putMVar' as wait and signal.
+--
+-- __Deviations:__ There is no @Eq@ instance for @MonadConc@ the
+-- @MVar@ type. Furthermore, the @mkWeakMVar@ and @addMVarFinalizer@
+-- functions are not provided. Finally, normal @MVar@s have a fairness
+-- guarantee, which dejafu does not currently make use of when
+-- generating schedules to test, so your program may be tested with
+-- /unfair/ schedules.
+module Control.Concurrent.Classy.MVar
+ ( -- *@MVar@s
+  MVar
+ , newEmptyMVar
+ , newEmptyMVarN
+ , newMVar
+ , newMVarN
+ , takeMVar
+ , putMVar
+ , readMVar
+ , swapMVar
+ , tryTakeMVar
+ , tryPutMVar
+ , isEmptyMVar
+ , withMVar
+ , withMVarMasked
+ , modifyMVar_
+ , modifyMVar
+ , modifyMVarMasked_
+ , modifyMVarMasked
+ ) where
+
+import Control.Monad.Catch (mask_, onException)
+import Control.Monad.Conc.Class
+
+-- | Swap the contents of a @MVar@, and return the value taken. This
+-- function is atomic only if there are no other producers fro this
+-- @MVar@.
+swapMVar :: MonadConc m => MVar m a -> a -> m a
+swapMVar cvar a = mask_ $ do
+  old <- takeMVar cvar
+  putMVar cvar a
+  return old
+
+-- | Check if a @MVar@ is empty.
+isEmptyMVar :: MonadConc m => MVar m a -> m Bool
+isEmptyMVar cvar = do
+  val <- tryTakeMVar cvar
+  case val of
+    Just val' -> putMVar cvar val' >> return True
+    Nothing   -> return False
+
+-- | Operate on the contents of a @MVar@, replacing the contents after
+-- finishing. This operation is exception-safe: it will replace the
+-- original contents of the @MVar@ if an exception is raised. However,
+-- it is only atomic if there are no other producers for this @MVar@.
+{-# INLINE withMVar #-}
+withMVar :: MonadConc m => MVar m a -> (a -> m b) -> m b
+withMVar cvar f = mask $ \restore -> do
+  val <- takeMVar cvar
+  out <- restore (f val) `onException` putMVar cvar val
+  putMVar cvar val
+
+  return out
+
+-- | Like 'withMVar', but the @IO@ action in the second argument is
+-- executed with asynchronous exceptions masked.
+{-# INLINE withMVarMasked #-}
+withMVarMasked :: MonadConc m => MVar m a -> (a -> m b) -> m b
+withMVarMasked cvar f = mask_ $ do
+  val <- takeMVar cvar
+  out <- f val `onException` putMVar cvar val
+  putMVar cvar val
+
+  return out
+
+-- | An exception-safe wrapper for modifying the contents of a @MVar@.
+-- Like 'withMVar', 'modifyMVar' will replace the original contents of
+-- the @MVar@ if an exception is raised during the operation. This
+-- function is only atomic if there are no other producers for this
+-- @MVar@.
+{-# INLINE modifyMVar_ #-}
+modifyMVar_ :: MonadConc m => MVar m a -> (a -> m a) -> m ()
+modifyMVar_ cvar f = modifyMVar cvar $ fmap (\a -> (a,())) . f
+
+-- | A slight variation on 'modifyMVar_' that allows a value to be
+-- returned (@b@) in addition to the modified value of the @MVar@.
+{-# INLINE modifyMVar #-}
+modifyMVar :: MonadConc m => MVar m a -> (a -> m (a, b)) -> m b
+modifyMVar cvar f = mask $ \restore -> do
+  val <- takeMVar cvar
+  (val', out) <- restore (f val) `onException` putMVar cvar val
+  putMVar cvar val'
+  return out
+
+-- | Like 'modifyMVar_', but the @IO@ action in the second argument is
+-- executed with asynchronous exceptions masked.
+{-# INLINE modifyMVarMasked_ #-}
+modifyMVarMasked_ :: MonadConc m => MVar m a -> (a -> m a) -> m ()
+modifyMVarMasked_ cvar f = modifyMVarMasked cvar $ fmap (\a -> (a,())) . f
+
+-- | Like 'modifyMVar', but the @IO@ action in the second argument is
+-- executed with asynchronous exceptions masked.
+{-# INLINE modifyMVarMasked #-}
+modifyMVarMasked :: MonadConc m => MVar m a -> (a -> m (a, b)) -> m b
+modifyMVarMasked cvar f = mask_ $ do
+  val <- takeMVar cvar
+  (val', out) <- f val `onException` putMVar cvar val
+  putMVar cvar val'
+  return out
diff --git a/Control/Concurrent/Classy/QSem.hs b/Control/Concurrent/Classy/QSem.hs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/Classy/QSem.hs
@@ -0,0 +1,37 @@
+-- | Simple quantity semaphores.
+module Control.Concurrent.Classy.QSem
+  ( -- * Simple Quantity Semaphores
+    QSem
+  , newQSem
+  , waitQSem
+  , signalQSem
+  ) where
+
+import Control.Concurrent.Classy.QSemN
+import Control.Monad.Conc.Class (MonadConc)
+
+-- | @QSem@ is a quantity semaphore in which the resource is acquired
+-- and released in units of one. It provides guaranteed FIFO ordering
+-- for satisfying blocked 'waitQSem' calls.
+--
+-- The pattern
+--
+-- > bracket_ qaitQSem signalSSem (...)
+--
+-- is safe; it never loses a unit of the resource.
+newtype QSem m = QSem (QSemN m)
+
+-- | Build a new 'QSem' with a supplied initial quantity. The initial
+-- quantity must be at least 0.
+newQSem :: MonadConc m => Int -> m (QSem m)
+newQSem initial
+  | initial < 0 = fail "newQSem: Initial quantity mus tbe non-negative."
+  | otherwise   = QSem <$> newQSemN initial
+
+-- | Wait for a unit to become available.
+waitQSem :: MonadConc m => QSem m -> m ()
+waitQSem (QSem qSemN) = waitQSemN qSemN 1
+
+-- | Signal that a unit of the 'QSem' is available.
+signalQSem :: MonadConc m => QSem m -> m ()
+signalQSem (QSem qSemN) = signalQSemN qSemN 1
diff --git a/Control/Concurrent/Classy/QSemN.hs b/Control/Concurrent/Classy/QSemN.hs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/Classy/QSemN.hs
@@ -0,0 +1,89 @@
+-- | Quantity semaphores in which each thread may wait for an arbitrary
+-- \"amount\".
+module Control.Concurrent.Classy.QSemN
+  ( -- * General Quantity Semaphores
+    QSemN
+  , newQSemN
+  , waitQSemN
+  , signalQSemN
+  ) where
+
+import Control.Monad.Conc.Class (MonadConc)
+import Control.Concurrent.Classy.MVar
+import Control.Monad.Catch (mask_, onException, uninterruptibleMask_)
+import Data.Maybe
+
+-- | 'QSemN' is a quantity semaphore in which the resource is aqcuired
+-- and released in units of one. It provides guaranteed FIFO ordering
+-- for satisfying blocked `waitQSemN` calls.
+--
+-- The pattern
+--
+-- > bracket_ (waitQSemN n) (signalQSemN n) (...)
+--
+-- is safe; it never loses any of the resource.
+newtype QSemN m = QSemN (MVar m (Int, [(Int, MVar m ())], [(Int, MVar m ())]))
+
+-- | Build a new 'QSemN' with a supplied initial quantity.
+--  The initial quantity must be at least 0.
+newQSemN :: MonadConc m => Int -> m (QSemN m)
+newQSemN initial
+  | initial < 0 = fail "newQSemN: Initial quantity must be non-negative"
+  | otherwise   = QSemN <$> newMVar (initial, [], [])
+
+-- | Wait for the specified quantity to become available
+waitQSemN :: MonadConc m => QSemN m -> Int -> m ()
+waitQSemN (QSemN m) sz = mask_ $ do
+  (quantity, b1, b2) <- takeMVar m
+  let remaining = quantity - sz
+  if remaining < 0
+  -- Enqueue and block the thread
+  then do
+    b <- newEmptyMVar
+    putMVar m (quantity, b1, (sz,b):b2)
+    wait b
+  -- Claim the resource
+  else
+    putMVar m (remaining, b1, b2)
+
+  where
+    wait b = takeMVar b `onException` uninterruptibleMask_ (do
+      (quantity, b1, b2) <- takeMVar m
+      r  <- tryTakeMVar b
+      r' <- if isJust r
+           then signal sz (quantity, b1, b2)
+           else putMVar b () >> pure (quantity, b1, b2)
+      putMVar m r')
+
+-- | Signal that a given quantity is now available from the 'QSemN'.
+signalQSemN :: MonadConc m => QSemN m -> Int -> m ()
+signalQSemN (QSemN m) sz = uninterruptibleMask_ $ do
+  r  <- takeMVar m
+  r' <- signal sz r
+  putMVar m r'
+
+-- | Fix the queue and signal as many threads as we can.
+signal :: MonadConc m
+  => Int
+  -> (Int, [(Int,MVar m ())], [(Int,MVar m ())])
+  -> m (Int, [(Int,MVar m ())], [(Int,MVar m ())])
+signal sz0 (i,a1,a2) = loop (sz0 + i) a1 a2 where
+  -- No more resource left, done.
+  loop 0 bs b2 = pure (0,  bs, b2)
+
+  -- Fix the queue
+  loop sz [] [] = pure (sz, [], [])
+  loop sz [] b2 = loop sz (reverse b2) []
+
+  -- Signal as many threads as there is enough resource to satisfy,
+  -- stopping as soon as one thread requires more resource than there
+  -- is.
+  loop sz ((j,b):bs) b2
+    | j > sz = do
+      r <- isEmptyMVar b
+      if r then pure (sz, (j,b):bs, b2)
+           else loop sz bs b2
+    | otherwise = do
+      r <- tryPutMVar b ()
+      if r then loop (sz-j) bs b2
+           else loop sz bs b2
diff --git a/Control/Concurrent/Classy/STM.hs b/Control/Concurrent/Classy/STM.hs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/Classy/STM.hs
@@ -0,0 +1,20 @@
+-- | Classy software transactional memory.
+module Control.Concurrent.Classy.STM
+  ( module Control.Monad.STM.Class
+  , module Control.Concurrent.Classy.STM.TVar
+  , module Control.Concurrent.Classy.STM.TMVar
+  , module Control.Concurrent.Classy.STM.TChan
+  , module Control.Concurrent.Classy.STM.TQueue
+  , module Control.Concurrent.Classy.STM.TBQueue
+  , module Control.Concurrent.Classy.STM.TArray
+  ) where
+
+import Control.Monad.STM.Class
+import Control.Concurrent.Classy.STM.TVar
+import Control.Concurrent.Classy.STM.TMVar
+import Control.Concurrent.Classy.STM.TChan
+import Control.Concurrent.Classy.STM.TQueue
+import Control.Concurrent.Classy.STM.TBQueue
+import Control.Concurrent.Classy.STM.TArray
+
+{-# ANN module ("HLint: ignore Use import/export shortcut" :: String) #-}
diff --git a/Control/Concurrent/Classy/STM/TArray.hs b/Control/Concurrent/Classy/STM/TArray.hs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/Classy/STM/TArray.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}
+
+-- | TArrays: transactional arrays, for use in STM-like monads.
+--
+-- __Deviations:__ @TArray@ as defined here does not have an @Eq@
+-- instance, this is because the @MonadSTM@ @TVar@ type does not have
+-- an @Eq@ constraint.
+module Control.Concurrent.Classy.STM.TArray (TArray) where
+
+import Data.Array (Array, bounds)
+import Data.Array.Base (listArray, arrEleBottom, unsafeAt, MArray(..),
+                        IArray(numElements))
+import Data.Ix (rangeSize)
+
+import Control.Monad.STM.Class
+
+-- | @TArray@ is a transactional array, supporting the usual 'MArray'
+-- interface for mutable arrays.
+--
+-- It is currently implemented as @Array ix (TVar stm e)@, but it may
+-- be replaced by a more efficient implementation in the future (the
+-- interface will remain the same, however).
+newtype TArray stm i e = TArray (Array i (TVar stm e))
+
+instance MonadSTM stm => MArray (TArray stm) e stm where
+  getBounds (TArray a) = pure (bounds a)
+
+  newArray b e = do
+    a <- rep (rangeSize b) (newTVar e)
+    pure $ TArray (listArray b a)
+
+  newArray_ b = newArray b arrEleBottom
+
+  unsafeRead  (TArray a) = readTVar  . unsafeAt a
+  unsafeWrite (TArray a) = writeTVar . unsafeAt a
+
+  getNumElements (TArray a) = pure (numElements a)
+
+-- | Like 'replicateM' but uses an accumulator to prevent stack overflows.
+-- Unlike 'replicateM' the returned list is in reversed order.  This
+-- doesn't matter though since this function is only used to create
+-- arrays with identical elements.
+rep :: Monad m => Int -> m a -> m [a]
+rep n m = go n [] where
+  go 0 xs = pure xs
+  go i xs = do
+    x <- m
+    go (i-1) (x:xs)
diff --git a/Control/Concurrent/Classy/STM/TBQueue.hs b/Control/Concurrent/Classy/STM/TBQueue.hs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/Classy/STM/TBQueue.hs
@@ -0,0 +1,138 @@
+-- | 'TBQueue' is a bounded version of 'TQueue'. The queue has a maximum
+-- capacity set when it is created.  If the queue already contains the
+-- maximum number of elements, then 'writeTBQueue' blocks until an
+-- element is removed from the queue.
+--
+-- The implementation is based on the traditional purely-functional
+-- queue representation that uses two lists to obtain amortised /O(1)/
+-- enqueue and dequeue operations.
+--
+-- __Deviations:__ @TBQueue@ as defined here does not have an @Eq@
+-- instance, this is because the @MonadSTM@ @TVar@ type does not have
+-- an @Eq@ constraint. Furthermore, the @newTBQueueIO@ function is not
+-- provided.
+module Control.Concurrent.Classy.STM.TBQueue
+  ( -- * TBQueue
+    TBQueue
+  , newTBQueue
+  , readTBQueue
+  , tryReadTBQueue
+  , peekTBQueue
+  , tryPeekTBQueue
+  , writeTBQueue
+  , unGetTBQueue
+  , isEmptyTBQueue
+  , isFullTBQueue
+  ) where
+
+import Control.Monad.STM.Class
+
+-- | 'TBQueue' is an abstract type representing a bounded FIFO
+-- channel.
+data TBQueue stm a
+   = TBQueue (TVar stm Int)
+             (TVar stm [a])
+             (TVar stm Int)
+             (TVar stm [a])
+
+-- | Build and returns a new instance of 'TBQueue'
+newTBQueue :: MonadSTM stm
+  => Int   -- ^ maximum number of elements the queue can hold
+  -> stm (TBQueue stm a)
+newTBQueue size = do
+  readT  <- newTVar []
+  writeT <- newTVar []
+  rsize <- newTVar 0
+  wsize <- newTVar size
+  pure (TBQueue rsize readT wsize writeT)
+
+-- | Write a value to a 'TBQueue'; retries if the queue is full.
+writeTBQueue :: MonadSTM stm => TBQueue stm a -> a -> stm ()
+writeTBQueue (TBQueue rsize _ wsize writeT) a = do
+  w <- readTVar wsize
+  if w /= 0
+  then writeTVar wsize (w - 1)
+  else do
+    r <- readTVar rsize
+    if r /= 0
+    then do
+      writeTVar rsize 0
+      writeTVar wsize (r - 1)
+    else retry
+  listend <- readTVar writeT
+  writeTVar writeT (a:listend)
+
+-- | Read the next value from the 'TBQueue'.
+readTBQueue :: MonadSTM stm => TBQueue stm a -> stm a
+readTBQueue (TBQueue rsize readT _ writeT) = do
+  xs <- readTVar readT
+  r  <- readTVar rsize
+  writeTVar rsize (r + 1)
+  case xs of
+    (x:xs') -> do
+      writeTVar readT xs'
+      pure x
+    [] -> do
+      ys <- readTVar writeT
+      case ys of
+        [] -> retry
+        _  -> do
+          let (z:zs) = reverse ys
+          writeTVar writeT []
+          writeTVar readT zs
+          pure z
+
+-- | A version of 'readTBQueue' which does not retry. Instead it
+-- returns @Nothing@ if no value is available.
+tryReadTBQueue :: MonadSTM stm => TBQueue stm a -> stm (Maybe a)
+tryReadTBQueue c = (Just <$> readTBQueue c) `orElse` pure Nothing
+
+-- | Get the next value from the @TBQueue@ without removing it,
+-- retrying if the channel is empty.
+peekTBQueue :: MonadSTM stm => TBQueue stm a -> stm a
+peekTBQueue c = do
+  x <- readTBQueue c
+  unGetTBQueue c x
+  return x
+
+-- | A version of 'peekTBQueue' which does not retry. Instead it
+-- returns @Nothing@ if no value is available.
+tryPeekTBQueue :: MonadSTM stm => TBQueue stm a -> stm (Maybe a)
+tryPeekTBQueue c = do
+  m <- tryReadTBQueue c
+  case m of
+    Nothing -> pure Nothing
+    Just x  -> do
+      unGetTBQueue c x
+      pure m
+
+-- | Put a data item back onto a channel, where it will be the next item read.
+-- Retries if the queue is full.
+unGetTBQueue :: MonadSTM stm => TBQueue stm a -> a -> stm ()
+unGetTBQueue (TBQueue rsize readT wsize _) a = do
+  r <- readTVar rsize
+  if r > 0
+  then writeTVar rsize (r - 1)
+  else do
+    w <- readTVar wsize
+    if w > 0
+    then writeTVar wsize (w - 1)
+    else retry
+  xs <- readTVar readT
+  writeTVar readT (a:xs)
+
+-- | Returns 'True' if the supplied 'TBQueue' is empty.
+isEmptyTBQueue :: MonadSTM stm => TBQueue stm a -> stm Bool
+isEmptyTBQueue (TBQueue _ readT _ writeT) = do
+  xs <- readTVar readT
+  case xs of
+    (_:_) -> pure False
+    [] -> null <$> readTVar writeT
+
+-- | Returns 'True' if the supplied 'TBQueue' is full.
+isFullTBQueue :: MonadSTM stm => TBQueue stm a -> stm Bool
+isFullTBQueue (TBQueue rsize _ wsize _) = do
+  w <- readTVar wsize
+  if w > 0
+  then pure False
+  else (>0) <$> readTVar rsize
diff --git a/Control/Concurrent/Classy/STM/TChan.hs b/Control/Concurrent/Classy/STM/TChan.hs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/Classy/STM/TChan.hs
@@ -0,0 +1,127 @@
+-- | Transactional channels
+--
+-- __Deviations:__ @TChan@ as defined here does not have an @Eq@
+-- instance, this is because the @MonadSTM@ @TVar@ type does not have
+-- an @Eq@ constraint. Furthermore, the @newTChanIO@ and
+-- @newBroadcastTChanIO@ functions are not provided.
+module Control.Concurrent.Classy.STM.TChan
+  ( -- * TChans
+    TChan
+
+  -- * Construction
+  , newTChan
+  , newBroadcastTChan
+  , dupTChan
+  , cloneTChan
+
+  -- * Reading and writing
+  , readTChan
+  , tryReadTChan
+  , peekTChan
+  , tryPeekTChan
+  , writeTChan
+  , unGetTChan
+  , isEmptyTChan
+  ) where
+
+import Control.Monad.STM.Class
+
+-- | 'TChan' is an abstract type representing an unbounded FIFO
+-- channel.
+data TChan stm a = TChan (TVar stm (TVarList stm a))
+                         (TVar stm (TVarList stm a))
+
+type TVarList stm a = TVar stm (TList stm a)
+data TList stm a = TNil | TCons a (TVarList stm a)
+
+-- |Build and return a new instance of 'TChan'
+newTChan :: MonadSTM stm => stm (TChan stm a)
+newTChan = do
+  hole   <- newTVar TNil
+  readH  <- newTVar hole
+  writeH <- newTVar hole
+  pure (TChan readH writeH)
+
+-- | Create a write-only 'TChan'.  More precisely, 'readTChan' will 'retry'
+-- even after items have been written to the channel.  The only way to
+-- read a broadcast channel is to duplicate it with 'dupTChan'.
+newBroadcastTChan :: MonadSTM stm => stm (TChan stm a)
+newBroadcastTChan = do
+    hole   <- newTVar TNil
+    readT  <- newTVar (error "reading from a TChan created by newBroadcastTChan; use dupTChan first")
+    writeT <- newTVar hole
+    pure (TChan readT writeT)
+
+-- | Write a value to a 'TChan'.
+writeTChan :: MonadSTM stm => TChan stm a -> a -> stm ()
+writeTChan (TChan _ writeT) a = do
+  listend  <- readTVar writeT
+  listend' <- newTVar TNil
+  writeTVar listend (TCons a listend')
+  writeTVar writeT listend'
+
+-- | Read the next value from the 'TChan'.
+readTChan :: MonadSTM stm => TChan stm a -> stm a
+readTChan tchan = tryReadTChan tchan >>= maybe retry pure
+
+-- | A version of 'readTChan' which does not retry. Instead it
+-- returns @Nothing@ if no value is available.
+tryReadTChan :: MonadSTM stm => TChan stm a -> stm (Maybe a)
+tryReadTChan (TChan readT _) = do
+  listhead <- readTVar readT
+  hd <- readTVar listhead
+  case hd of
+    TNil       -> pure Nothing
+    TCons a tl -> do
+      writeTVar readT tl
+      pure (Just a)
+
+-- | Get the next value from the 'TChan' without removing it,
+-- retrying if the channel is empty.
+peekTChan :: MonadSTM stm => TChan stm a -> stm a
+peekTChan tchan = tryPeekTChan tchan >>= maybe retry pure
+
+-- | A version of 'peekTChan' which does not retry. Instead it
+-- returns @Nothing@ if no value is available.
+tryPeekTChan :: MonadSTM stm => TChan stm a -> stm (Maybe a)
+tryPeekTChan (TChan readT _) = do
+  listhead <- readTVar readT
+  hd <- readTVar listhead
+  pure $ case hd of
+    TNil      -> Nothing
+    TCons a _ -> Just a
+
+-- | Duplicate a 'TChan': the duplicate channel begins empty, but data written to
+-- either channel from then on will be available from both.  Hence
+-- this creates a kind of broadcast channel, where data written by
+-- anyone is seen by everyone else.
+dupTChan :: MonadSTM stm => TChan stm a -> stm (TChan stm a)
+dupTChan (TChan _ writeT) = do
+  hole   <- readTVar writeT
+  readT' <- newTVar hole
+  return (TChan readT' writeT)
+
+-- | Put a data item back onto a channel, where it will be the next
+-- item read.
+unGetTChan :: MonadSTM stm => TChan stm a -> a -> stm ()
+unGetTChan (TChan readT _) a = do
+   listhead <- readTVar readT
+   head' <- newTVar (TCons a listhead)
+   writeTVar readT head'
+
+-- | Returns 'True' if the supplied 'TChan' is empty.
+isEmptyTChan :: MonadSTM stm => TChan stm a -> stm Bool
+isEmptyTChan (TChan readT _) = do
+  listhead <- readTVar readT
+  hd <- readTVar listhead
+  pure $ case hd of
+    TNil -> True
+    TCons _ _ -> False
+
+-- | Clone a 'TChan': similar to 'dupTChan', but the cloned channel starts with the
+-- same content available as the original channel.
+cloneTChan :: MonadSTM stm => TChan stm a -> stm (TChan stm a)
+cloneTChan (TChan readT writeT) = do
+  readpos <- readTVar readT
+  readT' <- newTVar readpos
+  pure (TChan readT' writeT)
diff --git a/Control/Concurrent/Classy/STM/TMVar.hs b/Control/Concurrent/Classy/STM/TMVar.hs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/Classy/STM/TMVar.hs
@@ -0,0 +1,110 @@
+-- | Transactional @MVar@s, for use with 'MonadSTM'.
+--
+-- __Deviations:__ @TMVar@ as defined here does not have an @Eq@
+-- instance, this is because the @MonadSTM@ @TVar@ type does not have
+-- an @Eq@ constraint. Furthermore, the @newTMVarIO@,
+-- @newEmptyTMVarIO@, and @mkWeakTMVar@ functions are not provided.
+module Control.Concurrent.Classy.STM.TMVar
+  ( -- * @TMVar@s
+    TMVar
+  , newTMVar
+  , newTMVarN
+  , newEmptyTMVar
+  , newEmptyTMVarN
+  , takeTMVar
+  , putTMVar
+  , readTMVar
+  , tryTakeTMVar
+  , tryPutTMVar
+  , tryReadTMVar
+  , isEmptyTMVar
+  , swapTMVar
+  ) where
+
+import Control.Monad (liftM, when, unless)
+import Control.Monad.STM.Class
+import Data.Maybe (isJust, isNothing)
+
+-- | A @TMVar@ is like an @MVar@ or a @mVar@, but using transactional
+-- memory. As transactions are atomic, this makes dealing with
+-- multiple @TMVar@s easier than wrangling multiple @mVar@s.
+newtype TMVar stm a = TMVar (TVar stm (Maybe a))
+
+-- | Create a 'TMVar' containing the given value.
+newTMVar :: MonadSTM stm => a -> stm (TMVar stm a)
+newTMVar = newTMVarN ""
+
+-- | Create a 'TMVar' containing the given value, with the given
+-- name.
+--
+-- Name conflicts are handled as usual for 'TVar's. The name is
+-- prefixed with \"ctmvar-\".
+newTMVarN :: MonadSTM stm => String -> a -> stm (TMVar stm a)
+newTMVarN n a = do
+  let n' = if null n then "ctmvar" else "ctmvar-" ++ n
+  ctvar <- newTVarN n' $ Just a
+  return $ TMVar ctvar
+
+-- | Create a new empty 'TMVar'.
+newEmptyTMVar :: MonadSTM stm => stm (TMVar stm a)
+newEmptyTMVar = newEmptyTMVarN ""
+
+-- | Create a new empty 'TMVar' with the given name.
+--
+-- Name conflicts are handled as usual for 'TVar's. The name is
+-- prefixed with \"ctmvar-\".
+newEmptyTMVarN :: MonadSTM stm => String -> stm (TMVar stm a)
+newEmptyTMVarN n = do
+  let n' = if null n then "ctmvar" else "ctmvar-" ++ n
+  ctvar <- newTVarN n' Nothing
+  return $ TMVar ctvar
+
+-- | Take the contents of a 'TMVar', or 'retry' if it is empty.
+takeTMVar :: MonadSTM stm => TMVar stm a -> stm a
+takeTMVar ctmvar = do
+  taken <- tryTakeTMVar ctmvar
+  maybe retry return taken
+
+-- | Write to a 'TMVar', or 'retry' if it is full.
+putTMVar :: MonadSTM stm => TMVar stm a -> a -> stm ()
+putTMVar ctmvar a = do
+  putted <- tryPutTMVar ctmvar a
+  unless putted retry
+
+-- | Read from a 'TMVar' without emptying, or 'retry' if it is empty.
+readTMVar :: MonadSTM stm => TMVar stm a -> stm a
+readTMVar ctmvar = do
+  readed <- tryReadTMVar ctmvar
+  maybe retry return readed
+
+-- | Try to take the contents of a 'TMVar', returning 'Nothing' if it
+-- is empty.
+tryTakeTMVar :: MonadSTM stm => TMVar stm a -> stm (Maybe a)
+tryTakeTMVar (TMVar ctvar) = do
+  val <- readTVar ctvar
+  when (isJust val) $ writeTVar ctvar Nothing
+  return val
+
+-- | Try to write to a 'TMVar', returning 'False' if it is full.
+tryPutTMVar :: MonadSTM stm => TMVar stm a -> a -> stm Bool
+tryPutTMVar (TMVar ctvar) a = do
+  val <- readTVar ctvar
+  when (isNothing val) $ writeTVar ctvar (Just a)
+  return $ isNothing val
+
+-- | Try to read from a 'TMVar' without emptying, returning 'Nothing'
+-- if it is empty.
+tryReadTMVar :: MonadSTM stm => TMVar stm a -> stm (Maybe a)
+tryReadTMVar (TMVar ctvar) = readTVar ctvar
+
+-- | Check if a 'TMVar' is empty or not.
+isEmptyTMVar :: MonadSTM stm => TMVar stm a -> stm Bool
+isEmptyTMVar ctmvar = isNothing `liftM` tryReadTMVar ctmvar
+
+-- | Swap the contents of a 'TMVar' returning the old contents, or
+-- 'retry' if it is empty.
+swapTMVar :: MonadSTM stm => TMVar stm a -> a -> stm a
+swapTMVar ctmvar a = do
+  val <- takeTMVar ctmvar
+  putTMVar ctmvar a
+  return val
diff --git a/Control/Concurrent/Classy/STM/TQueue.hs b/Control/Concurrent/Classy/STM/TQueue.hs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/Classy/STM/TQueue.hs
@@ -0,0 +1,105 @@
+-- | A 'TQueue' is like a 'TChan', with two important differences:
+--
+--  * it has faster throughput than both 'TChan' and 'Chan' (although
+--    the costs are amortised, so the cost of individual operations
+--    can vary a lot).
+--
+--  * it does /not/ provide equivalents of the 'dupTChan' and
+--    'cloneTChan' operations.
+--
+-- The implementation is based on the traditional purely-functional
+-- queue representation that uses two lists to obtain amortised /O(1)/
+-- enqueue and dequeue operations.
+--
+-- __Deviations:__ @TQueue@ as defined here does not have an @Eq@
+-- instance, this is because the @MonadSTM@ @TVar@ type does not have
+-- an @Eq@ constraint. Furthermore, the @newTQueueIO@ function is not
+-- provided.
+module Control.Concurrent.Classy.STM.TQueue
+  ( -- * TQueue
+    TQueue
+  , newTQueue
+  , readTQueue
+  , tryReadTQueue
+  , peekTQueue
+  , tryPeekTQueue
+  , writeTQueue
+  , unGetTQueue
+  , isEmptyTQueue
+  ) where
+
+import Control.Monad.STM.Class
+
+-- | 'TQueue' is an abstract type representing an unbounded FIFO channel.
+data TQueue stm a = TQueue (TVar stm [a])
+                           (TVar stm [a])
+
+-- | Build and returns a new instance of 'TQueue'
+newTQueue :: MonadSTM stm => stm (TQueue stm a)
+newTQueue = do
+  readT  <- newTVar []
+  writeT <- newTVar []
+  pure (TQueue readT writeT)
+
+-- | Write a value to a 'TQueue'.
+writeTQueue :: MonadSTM stm => TQueue stm a -> a -> stm ()
+writeTQueue (TQueue _ writeT) a = do
+  listend <- readTVar writeT
+  writeTVar writeT (a:listend)
+
+-- | Read the next value from the 'TQueue'.
+readTQueue :: MonadSTM stm => TQueue stm a -> stm a
+readTQueue (TQueue readT writeT) = do
+  xs <- readTVar readT
+  case xs of
+    (x:xs') -> do
+      writeTVar readT xs'
+      pure x
+    [] -> do
+      ys <- readTVar writeT
+      case ys of
+        [] -> retry
+        _  -> case reverse ys of
+               [] -> error "readTQueue"
+               (z:zs) -> do
+                 writeTVar writeT []
+                 writeTVar readT zs
+                 pure z
+
+-- | A version of 'readTQueue' which does not retry. Instead it
+-- returns @Nothing@ if no value is available.
+tryReadTQueue :: MonadSTM stm => TQueue stm a -> stm (Maybe a)
+tryReadTQueue c = (Just <$> readTQueue c) `orElse` pure Nothing
+
+-- | Get the next value from the @TQueue@ without removing it,
+-- retrying if the channel is empty.
+peekTQueue :: MonadSTM stm => TQueue stm a -> stm a
+peekTQueue c = do
+  x <- readTQueue c
+  unGetTQueue c x
+  pure x
+
+-- | A version of 'peekTQueue' which does not retry. Instead it
+-- returns @Nothing@ if no value is available.
+tryPeekTQueue :: MonadSTM stm => TQueue stm a -> stm (Maybe a)
+tryPeekTQueue c = do
+  m <- tryReadTQueue c
+  case m of
+    Nothing -> pure Nothing
+    Just x  -> do
+      unGetTQueue c x
+      pure m
+
+-- |Put a data item back onto a channel, where it will be the next item read.
+unGetTQueue :: MonadSTM stm => TQueue stm a -> a -> stm ()
+unGetTQueue (TQueue readT _) a = do
+  xs <- readTVar readT
+  writeTVar readT (a:xs)
+
+-- |Returns 'True' if the supplied 'TQueue' is empty.
+isEmptyTQueue :: MonadSTM stm => TQueue stm a -> stm Bool
+isEmptyTQueue (TQueue readT writeT) = do
+  xs <- readTVar readT
+  case xs of
+    (_:_) -> pure False
+    [] -> null <$> readTVar writeT
diff --git a/Control/Concurrent/Classy/STM/TVar.hs b/Control/Concurrent/Classy/STM/TVar.hs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/Classy/STM/TVar.hs
@@ -0,0 +1,54 @@
+-- | Transactional variables, for use with 'MonadSTM'.
+--
+-- __Deviations:__ There is no @Eq@ instance for @MonadSTM@ the @TVar@
+-- type. Furthermore, the @newTVarIO@ and @mkWeakTVar@ functions are
+-- not provided.
+module Control.Concurrent.Classy.STM.TVar
+  ( -- * @TVar@s
+    TVar
+  , newTVar
+  , newTVarN
+  , readTVar
+  , readTVarConc
+  , writeTVar
+  , modifyTVar
+  , modifyTVar'
+  , swapTVar
+  , registerDelay
+  ) where
+
+import Control.Monad.STM.Class
+import Control.Monad.Conc.Class
+import Data.Functor (void)
+
+-- * @TVar@s
+
+-- | Mutate the contents of a 'TVar'. This is non-strict.
+modifyTVar :: MonadSTM stm => TVar stm a -> (a -> a) -> stm ()
+modifyTVar ctvar f = do
+  a <- readTVar ctvar
+  writeTVar ctvar $ f a
+
+-- | Mutate the contents of a 'TVar' strictly.
+modifyTVar' :: MonadSTM stm => TVar stm a -> (a -> a) -> stm ()
+modifyTVar' ctvar f = do
+  a <- readTVar ctvar
+  writeTVar ctvar $! f a
+
+-- | Swap the contents of a 'TVar', returning the old value.
+swapTVar :: MonadSTM stm => TVar stm a -> a -> stm a
+swapTVar ctvar a = do
+  old <- readTVar ctvar
+  writeTVar ctvar a
+  return old
+
+-- | Set the value of returned 'TVar' to @True@ after a given number
+-- of microseconds. The caveats associated with 'threadDelay' also
+-- apply.
+registerDelay :: MonadConc m => Int -> m (TVar (STM m) Bool)
+registerDelay delay = do
+  var <- atomically (newTVar False)
+  void . fork $ do
+    threadDelay delay
+    atomically (writeTVar var True)
+  pure var
diff --git a/Control/Concurrent/STM/CTMVar.hs b/Control/Concurrent/STM/CTMVar.hs
deleted file mode 100644
--- a/Control/Concurrent/STM/CTMVar.hs
+++ /dev/null
@@ -1,86 +0,0 @@
--- | Transactional @CVar@s, for use with 'MonadSTM'.
-module Control.Concurrent.STM.CTMVar
-  ( -- * @CTMVar@s
-    CTMVar
-  , newCTMVar
-  , newEmptyCTMVar
-  , takeCTMVar
-  , putCTMVar
-  , readCTMVar
-  , tryTakeCTMVar
-  , tryPutCTMVar
-  , tryReadCTMVar
-  , isEmptyCTMVar
-  , swapCTMVar
-  ) where
-
-import Control.Monad (liftM, when, unless)
-import Control.Monad.STM.Class
-import Data.Maybe (isJust, isNothing)
-
--- | A @CTMVar@ is like an @MVar@ or a @CVar@, but using transactional
--- memory. As transactions are atomic, this makes dealing with
--- multiple @CTMVar@s easier than wrangling multiple @CVar@s.
-newtype CTMVar m a = CTMVar (CTVar m (Maybe a))
-
--- | Create a 'CTMVar' containing the given value.
-newCTMVar :: MonadSTM m => a -> m (CTMVar m a)
-newCTMVar a = do
-  ctvar <- newCTVar $ Just a
-  return $ CTMVar ctvar
-
--- | Create a new empty 'CTMVar'.
-newEmptyCTMVar :: MonadSTM m => m (CTMVar m a)
-newEmptyCTMVar = do
-  ctvar <- newCTVar Nothing
-  return $ CTMVar ctvar
-
--- | Take the contents of a 'CTMVar', or 'retry' if it is empty.
-takeCTMVar :: MonadSTM m => CTMVar m a -> m a
-takeCTMVar ctmvar = do
-  taken <- tryTakeCTMVar ctmvar
-  maybe retry return taken
-
--- | Write to a 'CTMVar', or 'retry' if it is full.
-putCTMVar :: MonadSTM m => CTMVar m a -> a -> m ()
-putCTMVar ctmvar a = do
-  putted <- tryPutCTMVar ctmvar a
-  unless putted retry
-
--- | Read from a 'CTMVar' without emptying, or 'retry' if it is empty.
-readCTMVar :: MonadSTM m => CTMVar m a -> m a
-readCTMVar ctmvar = do
-  readed <- tryReadCTMVar ctmvar
-  maybe retry return readed
-
--- | Try to take the contents of a 'CTMVar', returning 'Nothing' if it
--- is empty.
-tryTakeCTMVar :: MonadSTM m => CTMVar m a -> m (Maybe a)
-tryTakeCTMVar (CTMVar ctvar) = do
-  val <- readCTVar ctvar
-  when (isJust val) $ writeCTVar ctvar Nothing
-  return val
-
--- | Try to write to a 'CTMVar', returning 'False' if it is full.
-tryPutCTMVar :: MonadSTM m => CTMVar m a -> a -> m Bool
-tryPutCTMVar (CTMVar ctvar) a = do
-  val <- readCTVar ctvar
-  when (isNothing val) $ writeCTVar ctvar (Just a)
-  return $ isNothing val
-
--- | Try to read from a 'CTMVar' without emptying, returning 'Nothing'
--- if it is empty.
-tryReadCTMVar :: MonadSTM m => CTMVar m a -> m (Maybe a)
-tryReadCTMVar (CTMVar ctvar) = readCTVar ctvar
-
--- | Check if a 'CTMVar' is empty or not.
-isEmptyCTMVar :: MonadSTM m => CTMVar m a -> m Bool
-isEmptyCTMVar ctmvar = isNothing `liftM` tryReadCTMVar ctmvar
-
--- | Swap the contents of a 'CTMVar' returning the old contents, or
--- 'retry' if it is empty.
-swapCTMVar :: MonadSTM m => CTMVar m a -> a -> m a
-swapCTMVar ctmvar a = do
-  val <- takeCTMVar ctmvar
-  putCTMVar ctmvar a
-  return val
diff --git a/Control/Concurrent/STM/CTVar.hs b/Control/Concurrent/STM/CTVar.hs
deleted file mode 100644
--- a/Control/Concurrent/STM/CTVar.hs
+++ /dev/null
@@ -1,34 +0,0 @@
--- | Transactional variables, for use with 'MonadSTM'.
-module Control.Concurrent.STM.CTVar
-  ( -- * @CTVar@s
-    CTVar
-  , newCTVar
-  , readCTVar
-  , writeCTVar
-  , modifyCTVar
-  , modifyCTVar'
-  , swapCTVar
-  ) where
-
-import Control.Monad.STM.Class
-
--- * @CTVar@s
-
--- | Mutate the contents of a 'CTVar'. This is non-strict.
-modifyCTVar :: MonadSTM m => CTVar m a -> (a -> a) -> m ()
-modifyCTVar ctvar f = do
-  a <- readCTVar ctvar
-  writeCTVar ctvar $ f a
-
--- | Mutate the contents of a 'CTVar' strictly.
-modifyCTVar' :: MonadSTM m => CTVar m a -> (a -> a) -> m ()
-modifyCTVar' ctvar f = do
-  a <- readCTVar ctvar
-  writeCTVar ctvar $! f a
-
--- | Swap the contents of a 'CTVar', returning the old value.
-swapCTVar :: MonadSTM m => CTVar m a -> a -> m a
-swapCTVar ctvar a = do
-  old <- readCTVar ctvar
-  writeCTVar ctvar a
-  return old
diff --git a/Control/Monad/Conc/Class.hs b/Control/Monad/Conc/Class.hs
--- a/Control/Monad/Conc/Class.hs
+++ b/Control/Monad/Conc/Class.hs
@@ -1,54 +1,88 @@
 {-# LANGUAGE CPP              #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE RankNTypes       #-}
+{-# LANGUAGE TemplateHaskell  #-}
 {-# LANGUAGE TypeFamilies     #-}
 
 -- | This module captures in a typeclass the interface of concurrency
 -- monads.
+--
+-- __Deviations:__ An instance of @MonadCoonc@ is not required to be
+-- an instance of @MonadFix@, unlike @IO@. The @CRef@, @MVar@, and
+-- @Ticket@ types are not required to be instances of @Show@ or @Eq@,
+-- unlike their normal counterparts. The @threadCapability@,
+-- @threadWaitRead@, @threadWaitWrite@, @threadWaitReadSTM@,
+-- @threadWaitWriteSTM@, and @mkWeakThreadId@ functions are not
+-- provided. The @threadDelay@ function is not required to delay the
+-- thread, merely to yield it. Bound threads are not supported. The
+-- @BlockedIndefinitelyOnMVar@ (and similar) exceptions are /not/
+-- thrown during testing, so do not rely on them at all.
 module Control.Monad.Conc.Class
   ( MonadConc(..)
 
-  -- * Utilities
+  -- * Threads
   , spawn
   , forkFinally
   , killThread
-  , cas
 
-  -- * Bound Threads
+  -- ** Named Threads
+  , forkN
+  , forkOnN
+  , lineNum
 
+  -- ** Bound Threads
+
   -- | @MonadConc@ does not support bound threads, if you need that
   -- sort of thing you will have to use regular @IO@.
 
   , rtsSupportsBoundThreads
   , isCurrentThreadBound
+
+  -- * Exceptions
+  , throw
+  , catch
+  , mask
+  , uninterruptibleMask
+
+  -- * Mutable State
+  , newMVar
+  , newMVarN
+  , cas
+
+  -- * Utilities for instance writers
+  , makeTransConc
+  , liftedF
+  , liftedFork
   ) where
 
-import Control.Concurrent (forkIO)
-import Control.Concurrent.MVar (MVar, readMVar, newEmptyMVar, putMVar, tryPutMVar, takeMVar, tryTakeMVar)
+-- for the class and utilities
 import Control.Exception (Exception, AsyncException(ThreadKilled), SomeException)
-import Control.Monad (liftM)
 import Control.Monad.Catch (MonadCatch, MonadThrow, MonadMask)
-import Control.Monad.Reader (ReaderT(..), runReaderT)
-import Control.Monad.STM (STM)
-import Control.Monad.STM.Class (MonadSTM, CTVar)
-import Control.Monad.Trans (lift)
-import Data.IORef (IORef, atomicModifyIORef, newIORef, readIORef, writeIORef, atomicWriteIORef)
-
-import qualified Control.Concurrent as C
 import qualified Control.Monad.Catch as Ca
+import Control.Monad.STM.Class (MonadSTM, TVar, readTVar)
+import Control.Monad.Trans.Control (MonadTransControl, StT, liftWith)
+import Data.Typeable (Typeable)
+import Language.Haskell.TH (Q, DecsQ, Exp, Loc(..), Info(VarI), Name, Type(..), reify, location, varE)
+
+-- for the 'IO' instance
+import qualified Control.Concurrent as IO
+import qualified Control.Concurrent.STM.TVar as IO
+import qualified Control.Monad.STM as IO
+import qualified Data.Atomics as IO
+import qualified Data.IORef as IO
+
+-- for the transformer instances
+import Control.Monad.Reader (ReaderT)
+import Control.Monad.Trans (lift)
+import Control.Monad.Trans.Identity (IdentityT)
 import qualified Control.Monad.RWS.Lazy as RL
 import qualified Control.Monad.RWS.Strict as RS
-import qualified Control.Monad.STM as S
 import qualified Control.Monad.State.Lazy as SL
 import qualified Control.Monad.State.Strict as SS
 import qualified Control.Monad.Writer.Lazy as WL
 import qualified Control.Monad.Writer.Strict as WS
-import qualified Data.Atomics as A
 
-#if __GLASGOW_HASKELL__ < 710
-import Control.Applicative (Applicative)
-import Data.Monoid (Monoid, mempty)
-#endif
+{-# ANN module ("HLint: ignore Use const" :: String) #-}
 
 -- | @MonadConc@ is an abstraction over GHC's typical concurrency
 -- abstraction. It captures the interface of concurrency monads in
@@ -59,20 +93,45 @@
 -- which can be run atomically.
 class ( Applicative m, Monad m
       , MonadCatch m, MonadThrow m, MonadMask m
-      , MonadSTM (STMLike m)
-      , Eq (ThreadId m), Show (ThreadId m)) => MonadConc m  where
+      , MonadSTM (STM m)
+      , Ord (ThreadId m), Show (ThreadId m)) => MonadConc m  where
+
+  {-# MINIMAL
+        (forkWithUnmask | forkWithUnmaskN)
+      , (forkOnWithUnmask | forkOnWithUnmaskN)
+      , getNumCapabilities
+      , setNumCapabilities
+      , myThreadId
+      , yield
+      , (newEmptyMVar | newEmptyMVarN)
+      , putMVar
+      , tryPutMVar
+      , readMVar
+      , takeMVar
+      , tryTakeMVar
+      , (newCRef | newCRefN)
+      , atomicModifyCRef
+      , writeCRef
+      , readForCAS
+      , peekTicket
+      , casCRef
+      , modifyCRefCAS
+      , atomically
+      , throwTo
+    #-}
+
   -- | The associated 'MonadSTM' for this class.
-  type STMLike m :: * -> *
+  type STM m :: * -> *
 
   -- | The mutable reference type, like 'MVar's. This may contain one
   -- value at a time, attempting to read or take from an \"empty\"
-  -- @CVar@ will block until it is full, and attempting to put to a
-  -- \"full\" @CVar@ will block until it is empty.
-  type CVar m :: * -> *
+  -- @MVar@ will block until it is full, and attempting to put to a
+  -- \"full\" @MVar@ will block until it is empty.
+  type MVar m :: * -> *
 
   -- | The mutable non-blocking reference type. These may suffer from
   -- relaxed memory effects if functions outside the set @newCRef@,
-  -- @readCRef@, @modifyCRef@, and @atomicWriteCRef@ are used.
+  -- @readCRef@, @atomicModifyCRef@, and @atomicWriteCRef@ are used.
   type CRef m :: * -> *
 
   -- | When performing compare-and-swap operations on @CRef@s, a
@@ -84,7 +143,7 @@
   type ThreadId m :: *
 
   -- | Fork a computation to happen concurrently. Communication may
-  -- happen over @CVar@s.
+  -- happen over @MVar@s.
   --
   -- > fork ma = forkWithUnmask (\_ -> ma)
   fork :: m () -> m (ThreadId m)
@@ -93,8 +152,22 @@
   -- | Like 'fork', but the child thread is passed a function that can
   -- be used to unmask asynchronous exceptions. This function should
   -- not be used within a 'mask' or 'uninterruptibleMask'.
+  --
+  -- > forkWithUnmask = forkWithUnmaskN ""
   forkWithUnmask :: ((forall a. m a -> m a) -> m ()) -> m (ThreadId m)
+  forkWithUnmask = forkWithUnmaskN ""
 
+  -- | Like 'forkWithUnmask', but the thread is given a name which may
+  -- be used to present more useful debugging information.
+  --
+  -- If an empty name is given, the @ThreadId@ is used. If names
+  -- conflict, successive threads with the same name are given a
+  -- numeric suffix, counting up from 1.
+  --
+  -- > forkWithUnmaskN _ = forkWithUnmask
+  forkWithUnmaskN :: String -> ((forall a. m a -> m a) -> m ()) -> m (ThreadId m)
+  forkWithUnmaskN _ = forkWithUnmask
+
   -- | Fork a computation to happen on a specific processor. The
   -- specified int is the /capability number/, typically capabilities
   -- correspond to physical processors or cores but this is
@@ -105,10 +178,20 @@
   forkOn :: Int -> m () -> m (ThreadId m)
   forkOn c ma = forkOnWithUnmask c (\_ -> ma)
 
-  -- | Like 'forkWithUnmask' but the child thread is pinned to the
+  -- | Like 'forkWithUnmask', but the child thread is pinned to the
   -- given CPU, as with 'forkOn'.
+  --
+  -- > forkOnWithUnmask = forkOnWithUnmaskN ""
   forkOnWithUnmask :: Int -> ((forall a. m a -> m a) -> m ()) -> m (ThreadId m)
+  forkOnWithUnmask = forkOnWithUnmaskN ""
 
+  -- | Like 'forkWithUnmaskN', but the child thread is pinned to the
+  -- given CPU, as with 'forkOn'.
+  --
+  -- > forkOnWithUnmaskN _ = forkOnWithUnmask
+  forkOnWithUnmaskN :: String -> Int -> ((forall a. m a -> m a) -> m ()) -> m (ThreadId m)
+  forkOnWithUnmaskN _ = forkOnWithUnmask
+
   -- | Get the number of Haskell threads that can run simultaneously.
   getNumCapabilities :: m Int
 
@@ -122,37 +205,76 @@
   -- (if any).
   yield :: m ()
 
-  -- | Create a new empty @CVar@.
-  newEmptyCVar :: m (CVar m a)
+  -- | Yields the current thread, and optionally suspends the current
+  -- thread for a given number of microseconds.
+  --
+  -- If suspended, there is no guarantee that the thread will be
+  -- rescheduled promptly when the delay has expired, but the thread
+  -- will never continue to run earlier than specified.
+  --
+  -- > threadDelay _ = yield
+  threadDelay :: Int -> m ()
+  threadDelay _ = yield
 
-  -- | Put a value into a @CVar@. If there is already a value there,
+  -- | Create a new empty @MVar@.
+  --
+  -- > newEmptyMVar = newEmptyMVarN ""
+  newEmptyMVar :: m (MVar m a)
+  newEmptyMVar = newEmptyMVarN ""
+
+  -- | Create a new empty @MVar@, but it is given a name which may be
+  -- used to present more useful debugging information.
+  --
+  -- If an empty name is given, a counter starting from 0 is used. If
+  -- names conflict, successive @MVar@s with the same name are given a
+  -- numeric suffix, counting up from 1.
+  --
+  -- > newEmptyMVarN _ = newEmptyMVar
+  newEmptyMVarN :: String -> m (MVar m a)
+  newEmptyMVarN _ = newEmptyMVar
+
+  -- | Put a value into a @MVar@. If there is already a value there,
   -- this will block until that value has been taken, at which point
   -- the value will be stored.
-  putCVar :: CVar m a -> a -> m ()
+  putMVar :: MVar m a -> a -> m ()
 
-  -- | Attempt to put a value in a @CVar@ non-blockingly, returning
-  -- 'True' (and filling the @CVar@) if there was nothing there,
+  -- | Attempt to put a value in a @MVar@ non-blockingly, returning
+  -- 'True' (and filling the @MVar@) if there was nothing there,
   -- otherwise returning 'False'.
-  tryPutCVar :: CVar m a -> a -> m Bool
+  tryPutMVar :: MVar m a -> a -> m Bool
 
-  -- | Block until a value is present in the @CVar@, and then return
+  -- | Block until a value is present in the @MVar@, and then return
   -- it. As with 'readMVar', this does not \"remove\" the value,
   -- multiple reads are possible.
-  readCVar :: CVar m a -> m a
+  readMVar :: MVar m a -> m a
 
-  -- | Take a value from a @CVar@. This \"empties\" the @CVar@,
+  -- | Take a value from a @MVar@. This \"empties\" the @MVar@,
   -- allowing a new value to be put in. This will block if there is no
-  -- value in the @CVar@ already, until one has been put.
-  takeCVar :: CVar m a -> m a
+  -- value in the @MVar@ already, until one has been put.
+  takeMVar :: MVar m a -> m a
 
-  -- | Attempt to take a value from a @CVar@ non-blockingly, returning
-  -- a 'Just' (and emptying the @CVar@) if there was something there,
+  -- | Attempt to take a value from a @MVar@ non-blockingly, returning
+  -- a 'Just' (and emptying the @MVar@) if there was something there,
   -- otherwise returning 'Nothing'.
-  tryTakeCVar :: CVar m a -> m (Maybe a)
+  tryTakeMVar :: MVar m a -> m (Maybe a)
 
   -- | Create a new reference.
+  --
+  -- > newCRef = newCRefN ""
   newCRef :: a -> m (CRef m a)
+  newCRef = newCRefN ""
 
+  -- | Create a new reference, but it is given a name which may be
+  -- used to present more useful debugging information.
+  --
+  -- If an empty name is given, a counter starting from 0 is used. If
+  -- names conflict, successive @CRef@s with the same name are given a
+  -- numeric suffix, counting up from 1.
+  --
+  -- > newCRefN _ = newCRef
+  newCRefN :: String -> a -> m (CRef m a)
+  newCRefN _ = newCRef
+
   -- | Read the current value stored in a reference.
   --
   -- > readCRef cref = readForCAS cref >>= peekTicket
@@ -161,18 +283,18 @@
 
   -- | Atomically modify the value stored in a reference. This imposes
   -- a full memory barrier.
-  modifyCRef :: CRef m a -> (a -> (a, b)) -> m b
+  atomicModifyCRef :: CRef m a -> (a -> (a, b)) -> m b
 
   -- | Write a new value into an @CRef@, without imposing a memory
   -- barrier. This means that relaxed memory effects can be observed.
   writeCRef :: CRef m a -> a -> m ()
 
   -- | Replace the value stored in a reference, with the
-  -- barrier-to-reordering property that 'modifyCRef' has.
+  -- barrier-to-reordering property that 'atomicModifyCRef' has.
   --
-  -- > atomicWriteCRef r a = modifyCRef r $ const (a, ())
+  -- > atomicWriteCRef r a = atomicModifyCRef r $ const (a, ())
   atomicWriteCRef :: CRef m a -> a -> m ()
-  atomicWriteCRef r a = modifyCRef r $ const (a, ())
+  atomicWriteCRef r a = atomicModifyCRef r $ const (a, ())
 
   -- | Read the current value stored in a reference, returning a
   -- @Ticket@, for use in future compare-and-swap operations.
@@ -192,7 +314,7 @@
   -- This is strict in the \"new\" value argument.
   casCRef :: CRef m a -> Ticket m a -> a -> m (Bool, Ticket m a)
 
-  -- | A replacement for 'modifyCRef' using a compare-and-swap.
+  -- | A replacement for 'atomicModifyCRef' using a compare-and-swap.
   --
   -- This is strict in the \"new\" value argument.
   modifyCRefCAS :: CRef m a -> (a -> (a, b)) -> m b
@@ -204,76 +326,35 @@
   modifyCRefCAS_ cref f = modifyCRefCAS cref (\a -> (f a, ()))
 
   -- | Perform an STM transaction atomically.
-  atomically :: STMLike m a -> m a
-
-  -- | Throw an exception. This will \"bubble up\" looking for an
-  -- exception handler capable of dealing with it and, if one is not
-  -- found, the thread is killed.
-  --
-  -- > throw = Control.Monad.Catch.throwM
-  throw :: Exception e => e -> m a
-  throw = Ca.throwM
+  atomically :: STM m a -> m a
 
-  -- | Catch an exception. This is only required to be able to catch
-  -- exceptions raised by 'throw', unlike the more general
-  -- Control.Exception.catch function. If you need to be able to catch
-  -- /all/ errors, you will have to use 'IO'.
+  -- | Read the current value stored in a @TVar@. This may be
+  -- implemented differently for speed.
   --
-  -- > catch = Control.Monad.Catch.catch
-  catch :: Exception e => m a -> (e -> m a) -> m a
-  catch = Ca.catch
+  -- > readTVarConc = atomically . readTVar
+  readTVarConc :: TVar (STM m) a -> m a
+  readTVarConc = atomically . readTVar
 
   -- | Throw an exception to the target thread. This blocks until the
   -- exception is delivered, and it is just as if the target thread
   -- had raised it with 'throw'. This can interrupt a blocked action.
   throwTo :: Exception e => ThreadId m -> e -> m ()
 
-  -- | Executes a computation with asynchronous exceptions
-  -- /masked/. That is, any thread which attempts to raise an
-  -- exception in the current thread with 'throwTo' will be blocked
-  -- until asynchronous exceptions are unmasked again.
-  --
-  -- The argument passed to mask is a function that takes as its
-  -- argument another function, which can be used to restore the
-  -- prevailing masking state within the context of the masked
-  -- computation. This function should not be used within an
-  -- 'uninterruptibleMask'.
-  --
-  -- > mask = Control.Monad.Catch.mask
-  mask :: ((forall a. m a -> m a) -> m b) -> m b
-  mask = Ca.mask
-
-  -- | Like 'mask', but the masked computation is not
-  -- interruptible. THIS SHOULD BE USED WITH GREAT CARE, because if a
-  -- thread executing in 'uninterruptibleMask' blocks for any reason,
-  -- then the thread (and possibly the program, if this is the main
-  -- thread) will be unresponsive and unkillable. This function should
-  -- only be necessary if you need to mask exceptions around an
-  -- interruptible operation, and you can guarantee that the
-  -- interruptible operation will only block for a short period of
-  -- time. The supplied unmasking function should not be used within a
-  -- 'mask'.
-  --
-  -- > uninterruptibleMask = Control.Monad.Catch.uninterruptibleMask
-  uninterruptibleMask :: ((forall a. m a -> m a) -> m b) -> m b
-  uninterruptibleMask = Ca.uninterruptibleMask
-
   -- | Does nothing.
   --
   -- This function is purely for testing purposes, and indicates that
-  -- the thread has a reference to the provided @CVar@ or
-  -- @CTVar@. This function may be called multiple times, to add new
-  -- knowledge to the system. It does not need to be called when
-  -- @CVar@s or @CTVar@s are created, these get recorded
-  -- automatically.
+  -- the thread has a reference to the provided @MVar@ or @TVar@. This
+  -- function may be called multiple times, to add new knowledge to
+  -- the system. It does not need to be called when @MVar@s or @TVar@s
+  -- are created, these get recorded automatically.
   --
   -- Gathering this information allows detection of cases where the
   -- main thread is blocked on a variable no runnable thread has a
   -- reference to, which is a deadlock situation.
   --
-  -- > _concKnowsAbout _ = return ()
-  _concKnowsAbout :: Either (CVar m a) (CTVar (STMLike m) a) -> m ()
-  _concKnowsAbout _ = return ()
+  -- > _concKnowsAbout _ = pure ()
+  _concKnowsAbout :: Either (MVar m a) (TVar (STM m) a) -> m ()
+  _concKnowsAbout _ = pure ()
 
   -- | Does nothing.
   --
@@ -285,9 +366,9 @@
   -- positives! Be very sure that the current thread will /never/
   -- refer to the variable again, for instance when leaving its scope.
   --
-  -- > _concForgets _ = return ()
-  _concForgets :: Either (CVar m a) (CTVar (STMLike m) a) -> m ()
-  _concForgets _ = return ()
+  -- > _concForgets _ = pure ()
+  _concForgets :: Either (MVar m a) (TVar (STM m) a) -> m ()
+  _concForgets _ = pure ()
 
   -- | Does nothing.
   --
@@ -296,55 +377,50 @@
   -- '_concKnowsAbout'. If every thread has called '_concAllKnown',
   -- then detection of nonglobal deadlock is turned on.
   --
-  -- If a thread receives references to @CVar@s or @CTVar@s in the
+  -- If a thread receives references to @MVar@s or @TVar@s in the
   -- future (for instance, if one was sent over a channel), then
   -- '_concKnowsAbout' should be called immediately, otherwise there
   -- is a risk of identifying false positives.
   --
-  -- > _concAllKnown = return ()
+  -- > _concAllKnown = pure ()
   _concAllKnown :: m ()
-  _concAllKnown = return ()
+  _concAllKnown = pure ()
 
-instance MonadConc IO where
-  type STMLike  IO = STM
-  type CVar     IO = MVar
-  type CRef     IO = IORef
-  type Ticket   IO = A.Ticket
-  type ThreadId IO = C.ThreadId
+  -- | Does nothing.
+  --
+  -- During testing, records a message which shows up in the trace.
+  --
+  -- > _concMessage _ = pure ()
+  _concMessage :: Typeable a => a -> m ()
+  _concMessage _ = pure ()
 
-  readCVar       = readMVar
-  fork           = forkIO
-  forkWithUnmask = C.forkIOWithUnmask
-  forkOn         = C.forkOn
-  forkOnWithUnmask = C.forkOnWithUnmask
-  getNumCapabilities = C.getNumCapabilities
-  setNumCapabilities = C.setNumCapabilities
-  myThreadId     = C.myThreadId
-  yield          = C.yield
-  throwTo        = C.throwTo
-  newEmptyCVar   = newEmptyMVar
-  putCVar        = putMVar
-  tryPutCVar     = tryPutMVar
-  takeCVar       = takeMVar
-  tryTakeCVar    = tryTakeMVar
-  newCRef        = newIORef
-  readCRef       = readIORef
-  modifyCRef     = atomicModifyIORef
-  writeCRef      = writeIORef
-  atomicWriteCRef = atomicWriteIORef
-  readForCAS     = A.readForCAS
-  peekTicket     = return . A.peekTicket
-  casCRef        = A.casIORef
-  modifyCRefCAS  = A.atomicModifyIORefCAS
-  atomically     = S.atomically
+-------------------------------------------------------------------------------
+-- Utilities
 
+-- | Get the current line number as a String. Useful for automatically
+-- naming threads, @MVar@s, and @CRef@s.
+--
+-- Example usage:
+--
+-- > forkN $lineNum ...
+--
+-- Unfortunately this can't be packaged up into a
+-- @forkL@/@forkOnL@/etc set of functions, because this imposes a
+-- 'Lift' constraint on the monad, which 'IO' does not have.
+lineNum :: Q Exp
+lineNum = do
+  line <- show . fst . loc_start <$> location
+  [| line |]
+
+-- Threads
+
 -- | Create a concurrent computation for the provided action, and
--- return a @CVar@ which can be used to query the result.
-spawn :: MonadConc m => m a -> m (CVar m a)
+-- return a @MVar@ which can be used to query the result.
+spawn :: MonadConc m => m a -> m (MVar m a)
 spawn ma = do
-  cvar <- newEmptyCVar
-  _ <- fork $ _concKnowsAbout (Left cvar) >> ma >>= putCVar cvar
-  return cvar
+  cvar <- newEmptyMVar
+  _ <- fork $ _concKnowsAbout (Left cvar) >> ma >>= putMVar cvar
+  pure cvar
 
 -- | Fork a thread and call the supplied function when the thread is
 -- about to terminate, with an exception or a returned value. The
@@ -363,303 +439,285 @@
 killThread :: MonadConc m => ThreadId m -> m ()
 killThread tid = throwTo tid ThreadKilled
 
+-- | Like 'fork', but the thread is given a name which may be used to
+-- present more useful debugging information.
+--
+-- If no name is given, the @ThreadId@ is used. If names conflict,
+-- successive threads with the same name are given a numeric suffix,
+-- counting up from 1.
+forkN :: MonadConc m => String -> m () -> m (ThreadId m)
+forkN name ma = forkWithUnmaskN name (\_ -> ma)
+
+-- | Like 'forkOn', but the thread is given a name which may be used
+-- to present more useful debugging information.
+--
+-- If no name is given, the @ThreadId@ is used. If names conflict,
+-- successive threads with the same name are given a numeric suffix,
+-- counting up from 1.
+forkOnN :: MonadConc m => String -> Int -> m () -> m (ThreadId m)
+forkOnN name i ma = forkOnWithUnmaskN name i (\_ -> ma)
+
+-- Bound Threads
+
 -- | Provided for compatibility, always returns 'False'.
 rtsSupportsBoundThreads :: Bool
 rtsSupportsBoundThreads = False
 
 -- | Provided for compatibility, always returns 'False'.
 isCurrentThreadBound :: MonadConc m => m Bool
-isCurrentThreadBound = return False
+isCurrentThreadBound = pure False
 
--- | Compare-and-swap a value in a @CRef@, returning an indication of
--- success and the new value.
-cas :: MonadConc m => CRef m a -> a -> m (Bool, a)
-cas cref a = do
-  tick         <- readForCAS cref
-  (suc, tick') <- casCRef cref tick a
-  a'           <- peekTicket tick'
+-- Exceptions
 
-  return (suc, a')
+-- | Throw an exception. This will \"bubble up\" looking for an
+-- exception handler capable of dealing with it and, if one is not
+-- found, the thread is killed.
+throw :: (MonadConc m, Exception e) => e -> m a
+throw = Ca.throwM
 
--------------------------------------------------------------------------------
--- Transformer instances
+-- | Catch an exception. This is only required to be able to catch
+-- exceptions raised by 'throw', unlike the more general
+-- Control.Exception.catch function. If you need to be able to catch
+-- /all/ errors, you will have to use 'IO'.
+catch :: (MonadConc m, Exception e) => m a -> (e -> m a) -> m a
+catch = Ca.catch
 
-instance MonadConc m => MonadConc (ReaderT r m) where
-  type STMLike  (ReaderT r m) = STMLike m
-  type CVar     (ReaderT r m) = CVar m
-  type CRef     (ReaderT r m) = CRef m
-  type Ticket   (ReaderT r m) = Ticket m
-  type ThreadId (ReaderT r m) = ThreadId m
+-- | Executes a computation with asynchronous exceptions
+-- /masked/. That is, any thread which attempts to raise an exception
+-- in the current thread with 'throwTo' will be blocked until
+-- asynchronous exceptions are unmasked again.
+--
+-- The argument passed to mask is a function that takes as its
+-- argument another function, which can be used to restore the
+-- prevailing masking state within the context of the masked
+-- computation. This function should not be used within an
+-- 'uninterruptibleMask'.
+mask :: MonadConc m => ((forall a. m a -> m a) -> m b) -> m b
+mask = Ca.mask
 
-  fork              = reader fork
-  forkOn i          = reader (forkOn i)
-  forkWithUnmask ma = ReaderT $ \r -> forkWithUnmask (\f -> runReaderT (ma $ reader f) r)
-  forkOnWithUnmask i ma = ReaderT $ \r -> forkOnWithUnmask i (\f -> runReaderT (ma $ reader f) r)
+-- | Like 'mask', but the masked computation is not
+-- interruptible. THIS SHOULD BE USED WITH GREAT CARE, because if a
+-- thread executing in 'uninterruptibleMask' blocks for any reason,
+-- then the thread (and possibly the program, if this is the main
+-- thread) will be unresponsive and unkillable. This function should
+-- only be necessary if you need to mask exceptions around an
+-- interruptible operation, and you can guarantee that the
+-- interruptible operation will only block for a short period of
+-- time. The supplied unmasking function should not be used within a
+-- 'mask'.
+uninterruptibleMask :: MonadConc m => ((forall a. m a -> m a) -> m b) -> m b
+uninterruptibleMask = Ca.uninterruptibleMask
 
-  getNumCapabilities = lift getNumCapabilities
-  setNumCapabilities = lift . setNumCapabilities
-  myThreadId         = lift myThreadId
-  yield              = lift yield
-  throwTo t          = lift . throwTo t
-  newEmptyCVar       = lift newEmptyCVar
-  readCVar           = lift . readCVar
-  putCVar v          = lift . putCVar v
-  tryPutCVar v       = lift . tryPutCVar v
-  takeCVar           = lift . takeCVar
-  tryTakeCVar        = lift . tryTakeCVar
-  newCRef            = lift . newCRef
-  readCRef           = lift . readCRef
-  modifyCRef r       = lift . modifyCRef r
-  writeCRef r        = lift . writeCRef r
-  atomicWriteCRef r  = lift . atomicWriteCRef r
-  readForCAS         = lift . readForCAS
-  peekTicket         = lift . peekTicket
-  casCRef r t        = lift . casCRef r t
-  modifyCRefCAS r    = lift . modifyCRefCAS r
-  atomically         = lift . atomically
-  _concKnowsAbout    = lift . _concKnowsAbout
-  _concForgets       = lift . _concForgets
-  _concAllKnown      = lift _concAllKnown
+-- Mutable Variables
 
-reader :: Monad m => (m a -> m b) -> ReaderT r m a -> ReaderT r m b
-reader f ma = ReaderT $ \r -> f (runReaderT ma r)
+-- | Create a new @MVar@ containing a value.
+newMVar :: MonadConc m => a -> m (MVar m a)
+newMVar a = do
+  cvar <- newEmptyMVar
+  putMVar cvar a
+  pure cvar
 
-instance (MonadConc m, Monoid w) => MonadConc (WL.WriterT w m) where
-  type STMLike  (WL.WriterT w m) = STMLike m
-  type CVar     (WL.WriterT w m) = CVar m
-  type CRef     (WL.WriterT w m) = CRef m
-  type Ticket   (WL.WriterT w m) = Ticket m
-  type ThreadId (WL.WriterT w m) = ThreadId m
+-- | Create a new @MVar@ containing a value, but it is given a name
+-- which may be used to present more useful debugging information.
+--
+-- If no name is given, a counter starting from 0 is used. If names
+-- conflict, successive @MVar@s with the same name are given a numeric
+-- suffix, counting up from 1.
+newMVarN :: MonadConc m => String -> a -> m (MVar m a)
+newMVarN n a = do
+  cvar <- newEmptyMVarN n
+  putMVar cvar a
+  pure cvar
 
-  fork              = writerlazy fork
-  forkOn i          = writerlazy (forkOn i)
-  forkWithUnmask ma = lift $ forkWithUnmask (\f -> fst `liftM` WL.runWriterT (ma $ writerlazy f))
-  forkOnWithUnmask i ma = lift $ forkOnWithUnmask i (\f -> fst `liftM` WL.runWriterT (ma $ writerlazy f))
+-- | Compare-and-swap a value in a @CRef@, returning an indication of
+-- success and the new value.
+cas :: MonadConc m => CRef m a -> a -> m (Bool, a)
+cas cref a = do
+  tick         <- readForCAS cref
+  (suc, tick') <- casCRef cref tick a
+  a'           <- peekTicket tick'
 
-  getNumCapabilities = lift getNumCapabilities
-  setNumCapabilities = lift . setNumCapabilities
-  myThreadId         = lift myThreadId
-  yield              = lift yield
-  throwTo t          = lift . throwTo t
-  newEmptyCVar       = lift newEmptyCVar
-  readCVar           = lift . readCVar
-  putCVar v          = lift . putCVar v
-  tryPutCVar v       = lift . tryPutCVar v
-  takeCVar           = lift . takeCVar
-  tryTakeCVar        = lift . tryTakeCVar
-  newCRef            = lift . newCRef
-  readCRef           = lift . readCRef
-  modifyCRef r       = lift . modifyCRef r
-  writeCRef r        = lift . writeCRef r
-  atomicWriteCRef r  = lift . atomicWriteCRef r
-  readForCAS         = lift . readForCAS
-  peekTicket         = lift . peekTicket
-  casCRef r t        = lift . casCRef r t
-  modifyCRefCAS r    = lift . modifyCRefCAS r
-  atomically         = lift . atomically
-  _concKnowsAbout    = lift . _concKnowsAbout
-  _concForgets       = lift . _concForgets
-  _concAllKnown      = lift _concAllKnown
+  pure (suc, a')
 
-writerlazy :: (Monad m, Monoid w) => (m a -> m b) -> WL.WriterT w m a -> WL.WriterT w m b
-writerlazy f ma = lift . f $ fst `liftM` WL.runWriterT ma
+-------------------------------------------------------------------------------
+-- Concrete instances
 
-instance (MonadConc m, Monoid w) => MonadConc (WS.WriterT w m) where
-  type STMLike  (WS.WriterT w m) = STMLike m
-  type CVar     (WS.WriterT w m) = CVar m
-  type CRef     (WS.WriterT w m) = CRef m
-  type Ticket   (WS.WriterT w m) = Ticket m
-  type ThreadId (WS.WriterT w m) = ThreadId m
+instance MonadConc IO where
+  type STM      IO = IO.STM
+  type MVar     IO = IO.MVar
+  type CRef     IO = IO.IORef
+  type Ticket   IO = IO.Ticket
+  type ThreadId IO = IO.ThreadId
 
-  fork              = writerstrict fork
-  forkOn i          = writerstrict (forkOn i)
-  forkWithUnmask ma = lift $ forkWithUnmask (\f -> fst `liftM` WS.runWriterT (ma $ writerstrict f))
-  forkOnWithUnmask i ma = lift $ forkOnWithUnmask i (\f -> fst `liftM` WS.runWriterT (ma $ writerstrict f))
+  fork   = IO.forkIO
+  forkOn = IO.forkOn
 
-  getNumCapabilities = lift getNumCapabilities
-  setNumCapabilities = lift . setNumCapabilities
-  myThreadId         = lift myThreadId
-  yield              = lift yield
-  throwTo t          = lift . throwTo t
-  newEmptyCVar       = lift newEmptyCVar
-  readCVar           = lift . readCVar
-  putCVar v          = lift . putCVar v
-  tryPutCVar v       = lift . tryPutCVar v
-  takeCVar           = lift . takeCVar
-  tryTakeCVar        = lift . tryTakeCVar
-  newCRef            = lift . newCRef
-  readCRef           = lift . readCRef
-  modifyCRef r       = lift . modifyCRef r
-  writeCRef r        = lift . writeCRef r
-  atomicWriteCRef r  = lift . atomicWriteCRef r
-  readForCAS         = lift . readForCAS
-  peekTicket         = lift . peekTicket
-  casCRef r t        = lift . casCRef r t
-  modifyCRefCAS r    = lift . modifyCRefCAS r
-  atomically         = lift . atomically
-  _concKnowsAbout    = lift . _concKnowsAbout
-  _concForgets       = lift . _concForgets
-  _concAllKnown      = lift _concAllKnown
+  forkWithUnmask   = IO.forkIOWithUnmask
+  forkOnWithUnmask = IO.forkOnWithUnmask
 
-writerstrict :: (Monad m, Monoid w) => (m a -> m b) -> WS.WriterT w m a -> WS.WriterT w m b
-writerstrict f ma = lift . f $ fst `liftM` WS.runWriterT ma
+  getNumCapabilities = IO.getNumCapabilities
+  setNumCapabilities = IO.setNumCapabilities
+  readMVar           = IO.readMVar
+  myThreadId         = IO.myThreadId
+  yield              = IO.yield
+  threadDelay        = IO.threadDelay
+  throwTo            = IO.throwTo
+  newEmptyMVar       = IO.newEmptyMVar
+  putMVar            = IO.putMVar
+  tryPutMVar         = IO.tryPutMVar
+  takeMVar           = IO.takeMVar
+  tryTakeMVar        = IO.tryTakeMVar
+  newCRef            = IO.newIORef
+  readCRef           = IO.readIORef
+  atomicModifyCRef   = IO.atomicModifyIORef
+  writeCRef          = IO.writeIORef
+  atomicWriteCRef    = IO.atomicWriteIORef
+  readForCAS         = IO.readForCAS
+  peekTicket         = pure . IO.peekTicket
+  casCRef            = IO.casIORef
+  modifyCRefCAS      = IO.atomicModifyIORefCAS
+  atomically         = IO.atomically
+  readTVarConc       = IO.readTVarIO
 
-instance MonadConc m => MonadConc (SL.StateT s m) where
-  type STMLike  (SL.StateT s m) = STMLike m
-  type CVar     (SL.StateT s m) = CVar m
-  type CRef     (SL.StateT s m) = CRef m
-  type Ticket   (SL.StateT s m) = Ticket m
-  type ThreadId (SL.StateT s m) = ThreadId m
+-------------------------------------------------------------------------------
+-- Transformer instances
 
-  fork              = statelazy fork
-  forkOn i          = statelazy (forkOn i)
-  forkWithUnmask ma = SL.StateT $ \s -> (\a -> (a,s)) `liftM` forkWithUnmask (\f -> SL.evalStateT (ma $ statelazy f) s)
-  forkOnWithUnmask i ma = SL.StateT $ \s -> (\a -> (a,s)) `liftM` forkOnWithUnmask i (\f -> SL.evalStateT (ma $ statelazy f) s)
+#define INSTANCE(T,C,F)                                          \
+instance C => MonadConc (T m) where                             { \
+  type STM      (T m) = STM m                                  ; \
+  type MVar     (T m) = MVar m                                 ; \
+  type CRef     (T m) = CRef m                                 ; \
+  type Ticket   (T m) = Ticket m                               ; \
+  type ThreadId (T m) = ThreadId m                             ; \
+                                                                 \
+  fork   = liftedF F fork                                      ; \
+  forkOn = liftedF F . forkOn                                  ; \
+                                                                 \
+  forkWithUnmask        = liftedFork F forkWithUnmask          ; \
+  forkWithUnmaskN   n   = liftedFork F (forkWithUnmaskN   n  ) ; \
+  forkOnWithUnmask    i = liftedFork F (forkOnWithUnmask    i) ; \
+  forkOnWithUnmaskN n i = liftedFork F (forkOnWithUnmaskN n i) ; \
+                                                                 \
+  getNumCapabilities = lift getNumCapabilities                 ; \
+  setNumCapabilities = lift . setNumCapabilities               ; \
+  myThreadId         = lift myThreadId                         ; \
+  yield              = lift yield                              ; \
+  threadDelay        = lift . threadDelay                      ; \
+  throwTo t          = lift . throwTo t                        ; \
+  newEmptyMVar       = lift newEmptyMVar                       ; \
+  newEmptyMVarN      = lift . newEmptyMVarN                    ; \
+  readMVar           = lift . readMVar                         ; \
+  putMVar v          = lift . putMVar v                        ; \
+  tryPutMVar v       = lift . tryPutMVar v                     ; \
+  takeMVar           = lift . takeMVar                         ; \
+  tryTakeMVar        = lift . tryTakeMVar                      ; \
+  newCRef            = lift . newCRef                          ; \
+  newCRefN n         = lift . newCRefN n                       ; \
+  readCRef           = lift . readCRef                         ; \
+  atomicModifyCRef r = lift . atomicModifyCRef r               ; \
+  writeCRef r        = lift . writeCRef r                      ; \
+  atomicWriteCRef r  = lift . atomicWriteCRef r                ; \
+  readForCAS         = lift . readForCAS                       ; \
+  peekTicket         = lift . peekTicket                       ; \
+  casCRef r t        = lift . casCRef r t                      ; \
+  modifyCRefCAS r    = lift . modifyCRefCAS r                  ; \
+  atomically         = lift . atomically                       ; \
+  readTVarConc       = lift . readTVarConc                     ; \
+                                                                 \
+  _concKnowsAbout = lift . _concKnowsAbout                     ; \
+  _concForgets    = lift . _concForgets                        ; \
+  _concAllKnown   = lift _concAllKnown                         ; \
+  _concMessage    = lift . _concMessage                        }
 
-  getNumCapabilities = lift getNumCapabilities
-  setNumCapabilities = lift . setNumCapabilities
-  myThreadId         = lift myThreadId
-  yield              = lift yield
-  throwTo t          = lift . throwTo t
-  newEmptyCVar       = lift newEmptyCVar
-  readCVar           = lift . readCVar
-  putCVar v          = lift . putCVar v
-  tryPutCVar v       = lift . tryPutCVar v
-  takeCVar           = lift . takeCVar
-  tryTakeCVar        = lift . tryTakeCVar
-  newCRef            = lift . newCRef
-  readCRef           = lift . readCRef
-  modifyCRef r       = lift . modifyCRef r
-  writeCRef r        = lift . writeCRef r
-  atomicWriteCRef r  = lift . atomicWriteCRef r
-  readForCAS         = lift . readForCAS
-  peekTicket         = lift . peekTicket
-  casCRef r t        = lift . casCRef r t
-  modifyCRefCAS r    = lift . modifyCRefCAS r
-  atomically         = lift . atomically
-  _concKnowsAbout    = lift . _concKnowsAbout
-  _concForgets       = lift . _concForgets
-  _concAllKnown      = lift _concAllKnown
+INSTANCE(ReaderT r, MonadConc m, id)
 
-statelazy :: Monad m => (m a -> m b) -> SL.StateT s m a -> SL.StateT s m b
-statelazy f ma = SL.StateT $ \s -> (\b -> (b,s)) `liftM` f (SL.evalStateT ma s)
+INSTANCE(IdentityT, MonadConc m, id)
 
-instance MonadConc m => MonadConc (SS.StateT s m) where
-  type STMLike  (SS.StateT s m) = STMLike m
-  type CVar     (SS.StateT s m) = CVar m
-  type CRef     (SS.StateT s m) = CRef m
-  type Ticket   (SS.StateT s m) = Ticket m
-  type ThreadId (SS.StateT s m) = ThreadId m
+INSTANCE(WL.WriterT w, (MonadConc m, Monoid w), fst)
+INSTANCE(WS.WriterT w, (MonadConc m, Monoid w), fst)
 
-  fork              = statestrict fork
-  forkOn i          = statestrict (forkOn i)
-  forkWithUnmask ma = SS.StateT $ \s -> (\a -> (a,s)) `liftM` forkWithUnmask (\f -> SS.evalStateT (ma $ statestrict f) s)
-  forkOnWithUnmask i ma = SS.StateT $ \s -> (\a -> (a,s)) `liftM` forkOnWithUnmask i (\f -> SS.evalStateT (ma $ statestrict f) s)
+INSTANCE(SL.StateT s, MonadConc m, fst)
+INSTANCE(SS.StateT s, MonadConc m, fst)
 
-  getNumCapabilities = lift getNumCapabilities
-  setNumCapabilities = lift . setNumCapabilities
-  myThreadId         = lift myThreadId
-  yield              = lift yield
-  throwTo t          = lift . throwTo t
-  newEmptyCVar       = lift newEmptyCVar
-  readCVar           = lift . readCVar
-  putCVar v          = lift . putCVar v
-  tryPutCVar v       = lift . tryPutCVar v
-  takeCVar           = lift . takeCVar
-  tryTakeCVar        = lift . tryTakeCVar
-  newCRef            = lift . newCRef
-  readCRef           = lift . readCRef
-  modifyCRef r       = lift . modifyCRef r
-  writeCRef r        = lift . writeCRef r
-  atomicWriteCRef r  = lift . atomicWriteCRef r
-  readForCAS         = lift . readForCAS
-  peekTicket         = lift . peekTicket
-  casCRef r t        = lift . casCRef r t
-  modifyCRefCAS r    = lift . modifyCRefCAS r
-  atomically         = lift . atomically
-  _concKnowsAbout    = lift . _concKnowsAbout
-  _concForgets       = lift . _concForgets
-  _concAllKnown      = lift _concAllKnown
+INSTANCE(RL.RWST r w s, (MonadConc m, Monoid w), (\(a,_,_) -> a))
+INSTANCE(RS.RWST r w s, (MonadConc m, Monoid w), (\(a,_,_) -> a))
 
-statestrict :: Monad m => (m a -> m b) -> SS.StateT s m a -> SS.StateT s m b
-statestrict f ma = SS.StateT $ \s -> (\b -> (b,s)) `liftM` f (SS.evalStateT ma s)
+#undef INSTANC
 
-instance (MonadConc m, Monoid w) => MonadConc (RL.RWST r w s m) where
-  type STMLike  (RL.RWST r w s m) = STMLike m
-  type CVar     (RL.RWST r w s m) = CVar m
-  type CRef     (RL.RWST r w s m) = CRef m
-  type Ticket   (RL.RWST r w s m) = Ticket m
-  type ThreadId (RL.RWST r w s m) = ThreadId m
+-------------------------------------------------------------------------------
 
-  fork              = rwslazy fork
-  forkOn i          = rwslazy (forkOn i)
-  forkWithUnmask ma = RL.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkWithUnmask (\f -> fst `liftM` RL.evalRWST (ma $ rwslazy f) r s)
-  forkOnWithUnmask i ma = RL.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkOnWithUnmask i (\f -> fst `liftM` RL.evalRWST (ma $ rwslazy f) r s)
+-- | Make an instance @MonadConc m => MonadConc (t m)@ for a given
+-- transformer, @t@. The parameter should be the name of a function
+-- @:: forall a. StT t a -> a@.
+makeTransConc :: Name -> DecsQ
+makeTransConc unstN = do
+  unstI <- reify unstN
+  case unstI of
+    VarI _ (ForallT _ _ (AppT (AppT ArrowT (AppT (AppT (ConT _) t) _)) _)) _ _ ->
+      [d|
+        instance (MonadConc m) => MonadConc ($(pure t) m) where
+          type STM      ($(pure t) m) = STM m
+          type MVar     ($(pure t) m) = MVar m
+          type CRef     ($(pure t) m) = CRef m
+          type Ticket   ($(pure t) m) = Ticket m
+          type ThreadId ($(pure t) m) = ThreadId m
 
-  getNumCapabilities = lift getNumCapabilities
-  setNumCapabilities = lift . setNumCapabilities
-  myThreadId         = lift myThreadId
-  yield              = lift yield
-  throwTo t          = lift . throwTo t
-  newEmptyCVar       = lift newEmptyCVar
-  readCVar           = lift . readCVar
-  putCVar v          = lift . putCVar v
-  tryPutCVar v       = lift . tryPutCVar v
-  takeCVar           = lift . takeCVar
-  tryTakeCVar        = lift . tryTakeCVar
-  newCRef            = lift . newCRef
-  readCRef           = lift . readCRef
-  modifyCRef r       = lift . modifyCRef r
-  writeCRef r        = lift . writeCRef r
-  atomicWriteCRef r  = lift . atomicWriteCRef r
-  readForCAS         = lift . readForCAS
-  peekTicket         = lift . peekTicket
-  casCRef r t        = lift . casCRef r t
-  modifyCRefCAS r    = lift . modifyCRefCAS r
-  atomically         = lift . atomically
-  _concKnowsAbout    = lift . _concKnowsAbout
-  _concForgets       = lift . _concForgets
-  _concAllKnown      = lift _concAllKnown
+          fork   = liftedF $(varE unstN) fork
+          forkOn = liftedF $(varE unstN) . forkOn
 
-rwslazy :: (Monad m, Monoid w) => (m a -> m b) -> RL.RWST r w s m a -> RL.RWST r w s m b
-rwslazy f ma = RL.RWST $ \r s -> (\b -> (b,s,mempty)) `liftM` f (fst `liftM` RL.evalRWST ma r s)
+          forkWithUnmask        = liftedFork $(varE unstN) forkWithUnmask
+          forkWithUnmaskN   n   = liftedFork $(varE unstN) (forkWithUnmaskN   n  )
+          forkOnWithUnmask    i = liftedFork $(varE unstN) (forkOnWithUnmask    i)
+          forkOnWithUnmaskN n i = liftedFork $(varE unstN) (forkOnWithUnmaskN n i)
 
-instance (MonadConc m, Monoid w) => MonadConc (RS.RWST r w s m) where
-  type STMLike  (RS.RWST r w s m) = STMLike m
-  type CVar     (RS.RWST r w s m) = CVar m
-  type CRef     (RS.RWST r w s m) = CRef m
-  type Ticket   (RS.RWST r w s m) = Ticket m
-  type ThreadId (RS.RWST r w s m) = ThreadId m
+          getNumCapabilities = lift getNumCapabilities
+          setNumCapabilities = lift . setNumCapabilities
+          myThreadId         = lift myThreadId
+          yield              = lift yield
+          threadDelay        = lift . threadDelay
+          throwTo tid        = lift . throwTo tid
+          newEmptyMVar       = lift newEmptyMVar
+          newEmptyMVarN      = lift . newEmptyMVarN
+          readMVar           = lift . readMVar
+          putMVar v          = lift . putMVar v
+          tryPutMVar v       = lift . tryPutMVar v
+          takeMVar           = lift . takeMVar
+          tryTakeMVar        = lift . tryTakeMVar
+          newCRef            = lift . newCRef
+          newCRefN n         = lift . newCRefN n
+          readCRef           = lift . readCRef
+          atomicModifyCRef r = lift . atomicModifyCRef r
+          writeCRef r        = lift . writeCRef r
+          atomicWriteCRef r  = lift . atomicWriteCRef r
+          readForCAS         = lift . readForCAS
+          peekTicket         = lift . peekTicket
+          casCRef r tick     = lift . casCRef r tick
+          modifyCRefCAS r    = lift . modifyCRefCAS r
+          atomically         = lift . atomically
+          readTVarConc       = lift . readTVarConc
 
-  fork              = rwsstrict fork
-  forkOn i          = rwsstrict (forkOn i)
-  forkWithUnmask ma = RS.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkWithUnmask (\f -> fst `liftM` RS.evalRWST (ma $ rwsstrict f) r s)
-  forkOnWithUnmask i ma = RS.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkOnWithUnmask i (\f -> fst `liftM` RS.evalRWST (ma $ rwsstrict f) r s)
+          _concKnowsAbout = lift . _concKnowsAbout
+          _concForgets    = lift . _concForgets
+          _concAllKnown   = lift _concAllKnown
+          _concMessage    = lift . _concMessage
+      |]
+    _ -> fail "Expected a value of type (forall a -> StT t a -> a)"
 
-  getNumCapabilities = lift getNumCapabilities
-  setNumCapabilities = lift . setNumCapabilities
-  myThreadId         = lift myThreadId
-  yield              = lift yield
-  throwTo t          = lift . throwTo t
-  newEmptyCVar       = lift newEmptyCVar
-  readCVar           = lift . readCVar
-  putCVar v          = lift . putCVar v
-  tryPutCVar v       = lift . tryPutCVar v
-  takeCVar           = lift . takeCVar
-  tryTakeCVar        = lift . tryTakeCVar
-  newCRef            = lift . newCRef
-  readCRef           = lift . readCRef
-  modifyCRef r       = lift . modifyCRef r
-  writeCRef r        = lift . writeCRef r
-  atomicWriteCRef r  = lift . atomicWriteCRef r
-  readForCAS         = lift . readForCAS
-  peekTicket         = lift . peekTicket
-  casCRef r t        = lift . casCRef r t
-  modifyCRefCAS r    = lift . modifyCRefCAS r
-  atomically         = lift . atomically
-  _concKnowsAbout    = lift . _concKnowsAbout
-  _concForgets       = lift . _concForgets
-  _concAllKnown      = lift _concAllKnown
+-- | Given a function to remove the transformer-specific state, lift
+-- a function invocation.
+liftedF :: (MonadTransControl t, MonadConc m)
+  => (forall x. StT t x -> x)
+  -> (m a -> m b)
+  -> t m a
+  -> t m b
+liftedF unst f ma = liftWith $ \run -> f (unst <$> run ma)
 
-rwsstrict :: (Monad m, Monoid w) => (m a -> m b) -> RS.RWST r w s m a -> RS.RWST r w s m b
-rwsstrict f ma = RS.RWST $ \r s -> (\b -> (b,s,mempty)) `liftM` f (fst `liftM` RS.evalRWST ma r s)
+-- | Given a function to remove the transformer-specific state, lift
+-- a @fork(on)WithUnmask@ invocation.
+liftedFork :: (MonadTransControl t, MonadConc m)
+  => (forall x. StT t x -> x)
+  -> (((forall x. m x -> m x) -> m a) -> m b)
+  -> ((forall x. t m x -> t m x) -> t m a)
+  -> t m b
+liftedFork unst f ma = liftWith $ \run ->
+  f (\unmask -> unst <$> run (ma $ liftedF unst unmask))
diff --git a/Control/Monad/STM/Class.hs b/Control/Monad/STM/Class.hs
--- a/Control/Monad/STM/Class.hs
+++ b/Control/Monad/STM/Class.hs
@@ -1,163 +1,182 @@
-{-# LANGUAGE CPP          #-}
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE CPP             #-}
+{-# LANGUAGE RankNTypes      #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies    #-}
 
 -- | This module provides an abstraction over 'STM', which can be used
 -- with 'MonadConc'.
-module Control.Monad.STM.Class where
+--
+-- This module only defines the 'STM' class; you probably want to
+-- import "Control.Concurrent.Classy.STM" (which exports
+-- "Control.Monad.STM.Class").
+--
+-- __Deviations:__ An instance of @MonadSTM@ is not required to be an
+-- @Alternative@, @MonadPlus@, and @MonadFix@, unlike @STM@. The
+-- @always@ and @alwaysSucceeds@ functions are not provided; if you
+-- need these file an issue and I'll look into it.
+module Control.Monad.STM.Class
+  ( MonadSTM(..)
+  , check
+  , throwSTM
+  , catchSTM
 
-import Control.Concurrent.STM (STM)
-import Control.Concurrent.STM.TVar (TVar, newTVar, readTVar, writeTVar)
+  -- * Utilities for instance writers
+  , makeTransSTM
+  , liftedOrElse
+  ) where
+
 import Control.Exception (Exception)
 import Control.Monad (unless)
-import Control.Monad.Catch (MonadCatch, MonadThrow, throwM, catch)
-import Control.Monad.Reader (ReaderT(..), runReaderT)
+import Control.Monad.Reader (ReaderT)
 import Control.Monad.Trans (lift)
+import Control.Monad.Trans.Control (MonadTransControl, StT, liftWith)
+import Control.Monad.Trans.Identity (IdentityT)
+import Language.Haskell.TH (DecsQ, Info(VarI), Name, Type(..), reify, varE)
 
+import qualified Control.Concurrent.STM as STM
+import qualified Control.Monad.Catch as Ca
 import qualified Control.Monad.RWS.Lazy as RL
 import qualified Control.Monad.RWS.Strict as RS
-import qualified Control.Monad.STM as S
 import qualified Control.Monad.State.Lazy as SL
 import qualified Control.Monad.State.Strict as SS
 import qualified Control.Monad.Writer.Lazy as WL
 import qualified Control.Monad.Writer.Strict as WS
 
-#if __GLASGOW_HASKELL__ < 710
-import Control.Applicative (Applicative)
-import Data.Monoid (Monoid)
-#endif
-
 -- | @MonadSTM@ is an abstraction over 'STM'.
 --
 -- This class does not provide any way to run transactions, rather
 -- each 'MonadConc' has an associated @MonadSTM@ from which it can
 -- atomically run a transaction.
---
--- A minimal implementation consists of 'retry', 'orElse', 'newCTVar',
--- 'readCTVar', and 'writeCTVar'.
-class (Applicative m, Monad m, MonadCatch m, MonadThrow m) => MonadSTM m where
+class Ca.MonadCatch stm => MonadSTM stm where
+  {-# MINIMAL
+        retry
+      , orElse
+      , (newTVar | newTVarN)
+      , readTVar
+      , writeTVar
+    #-}
+
   -- | The mutable reference type. These behave like 'TVar's, in that
   -- they always contain a value and updates are non-blocking and
   -- synchronised.
-  type CTVar m :: * -> *
+  type TVar stm :: * -> *
 
   -- | Retry execution of this transaction because it has seen values
-  -- in @CTVar@s that it shouldn't have. This will result in the
-  -- thread running the transaction being blocked until any @CTVar@s
+  -- in @TVar@s that it shouldn't have. This will result in the
+  -- thread running the transaction being blocked until any @TVar@s
   -- referenced in it have been mutated.
-  retry :: m a
+  retry :: stm a
 
   -- | Run the first transaction and, if it @retry@s, run the second
   -- instead. If the monad is an instance of
   -- 'Alternative'/'MonadPlus', 'orElse' should be the '(<|>)'/'mplus'
   -- function.
-  orElse :: m a -> m a -> m a
+  orElse :: stm a -> stm a -> stm a
 
-  -- | Check whether a condition is true and, if not, call @retry@.
+  -- | Create a new @TVar@ containing the given value.
   --
-  -- > check b = unless b retry
-  check :: Bool -> m ()
-  check b = unless b retry
+  -- > newTVar = newTVarN ""
+  newTVar :: a -> stm (TVar stm a)
+  newTVar = newTVarN ""
 
-  -- | Create a new @CTVar@ containing the given value.
-  newCTVar :: a -> m (CTVar m a)
+  -- | Create a new @TVar@ containing the given value, but it is
+  -- given a name which may be used to present more useful debugging
+  -- information.
+  --
+  -- If an empty name is given, a counter starting from 0 is used. If
+  -- names conflict, successive @TVar@s with the same name are given
+  -- a numeric suffix, counting up from 1.
+  --
+  -- > newTVarN _ = newTVar
+  newTVarN :: String -> a -> stm (TVar stm a)
+  newTVarN _ = newTVar
 
-  -- | Return the current value stored in a @CTVar@.
-  readCTVar :: CTVar m a -> m a
+  -- | Return the current value stored in a @TVar@.
+  readTVar :: TVar stm a -> stm a
 
-  -- | Write the supplied value into the @CTVar@.
-  writeCTVar :: CTVar m a -> a -> m ()
+  -- | Write the supplied value into the @TVar@.
+  writeTVar :: TVar stm a -> a -> stm ()
 
-  -- | Throw an exception. This aborts the transaction and propagates
-  -- the exception.
-  --
-  -- > throwSTM = Control.Monad.Catch.throwM
-  throwSTM :: Exception e => e -> m a
-  throwSTM = throwM
+-- | Check whether a condition is true and, if not, call @retry@.
+check :: MonadSTM stm => Bool -> stm ()
+check b = unless b retry
 
-  -- | Handling exceptions from 'throwSTM'.
-  --
-  -- > catchSTM = Control.Monad.Catch.catch
-  catchSTM :: Exception e => m a -> (e -> m a) -> m a
-  catchSTM = Control.Monad.Catch.catch
+-- | Throw an exception. This aborts the transaction and propagates
+-- the exception.
+throwSTM :: (MonadSTM stm, Exception e) => e -> stm a
+throwSTM = Ca.throwM
 
-instance MonadSTM STM where
-  type CTVar STM = TVar
+-- | Handling exceptions from 'throwSTM'.
+catchSTM :: (MonadSTM stm, Exception e) => stm a -> (e -> stm a) -> stm a
+catchSTM = Ca.catch
 
-  retry      = S.retry
-  orElse     = S.orElse
-  newCTVar   = newTVar
-  readCTVar  = readTVar
-  writeCTVar = writeTVar
+instance MonadSTM STM.STM where
+  type TVar STM.STM = STM.TVar
 
+  retry     = STM.retry
+  orElse    = STM.orElse
+  newTVar   = STM.newTVar
+  readTVar  = STM.readTVar
+  writeTVar = STM.writeTVar
+
 -------------------------------------------------------------------------------
 -- Transformer instances
 
-instance MonadSTM m => MonadSTM (ReaderT r m) where
-  type CTVar (ReaderT r m) = CTVar m
-
-  retry        = lift retry
-  orElse ma mb = ReaderT $ \r -> orElse (runReaderT ma r) (runReaderT mb r)
-  check        = lift . check
-  newCTVar     = lift . newCTVar
-  readCTVar    = lift . readCTVar
-  writeCTVar v = lift . writeCTVar v
-
-instance (MonadSTM m, Monoid w) => MonadSTM (WL.WriterT w m) where
-  type CTVar (WL.WriterT w m) = CTVar m
-
-  retry        = lift retry
-  orElse ma mb = WL.WriterT $ orElse (WL.runWriterT ma) (WL.runWriterT mb)
-  check        = lift . check
-  newCTVar     = lift . newCTVar
-  readCTVar    = lift . readCTVar
-  writeCTVar v = lift . writeCTVar v
+#define INSTANCE(T,C,F)                                  \
+instance C => MonadSTM (T stm) where { \
+  type TVar (T stm) = TVar stm      ; \
+                                      \
+  retry       = lift retry          ; \
+  orElse      = liftedOrElse F      ; \
+  newTVar     = lift . newTVar      ; \
+  newTVarN n  = lift . newTVarN n   ; \
+  readTVar    = lift . readTVar     ; \
+  writeTVar v = lift . writeTVar v  }
 
-instance (MonadSTM m, Monoid w) => MonadSTM (WS.WriterT w m) where
-  type CTVar (WS.WriterT w m) = CTVar m
+INSTANCE(ReaderT r, MonadSTM stm, id)
 
-  retry        = lift retry
-  orElse ma mb = WS.WriterT $ orElse (WS.runWriterT ma) (WS.runWriterT mb)
-  check        = lift . check
-  newCTVar     = lift . newCTVar
-  readCTVar    = lift . readCTVar
-  writeCTVar v = lift . writeCTVar v
+INSTANCE(IdentityT, MonadSTM stm, id)
 
-instance MonadSTM m => MonadSTM (SL.StateT s m) where
-  type CTVar (SL.StateT s m) = CTVar m
+INSTANCE(WL.WriterT w, (MonadSTM stm, Monoid w), fst)
+INSTANCE(WS.WriterT w, (MonadSTM stm, Monoid w), fst)
 
-  retry        = lift retry
-  orElse ma mb = SL.StateT $ \s -> orElse (SL.runStateT ma s) (SL.runStateT mb s)
-  check        = lift . check
-  newCTVar     = lift . newCTVar
-  readCTVar    = lift . readCTVar
-  writeCTVar v = lift . writeCTVar v
+INSTANCE(SL.StateT s, MonadSTM stm, fst)
+INSTANCE(SS.StateT s, MonadSTM stm, fst)
 
-instance MonadSTM m => MonadSTM (SS.StateT s m) where
-  type CTVar (SS.StateT s m) = CTVar m
+INSTANCE(RL.RWST r w s, (MonadSTM stm, Monoid w), (\(a,_,_) -> a))
+INSTANCE(RS.RWST r w s, (MonadSTM stm, Monoid w), (\(a,_,_) -> a))
 
-  retry        = lift retry
-  orElse ma mb = SS.StateT $ \s -> orElse (SS.runStateT ma s) (SS.runStateT mb s)
-  check        = lift . check
-  newCTVar     = lift . newCTVar
-  readCTVar    = lift . readCTVar
-  writeCTVar v = lift . writeCTVar v
+#undef INSTANC
 
-instance (MonadSTM m, Monoid w) => MonadSTM (RL.RWST r w s m) where
-  type CTVar (RL.RWST r w s m) = CTVar m
+-------------------------------------------------------------------------------
 
-  retry        = lift retry
-  orElse ma mb = RL.RWST $ \r s -> orElse (RL.runRWST ma r s) (RL.runRWST mb r s)
-  check        = lift . check
-  newCTVar     = lift . newCTVar
-  readCTVar    = lift . readCTVar
-  writeCTVar v = lift . writeCTVar v
+-- | Make an instance @MonadSTM m => MonadSTM (t m)@ for a given
+-- transformer, @t@. The parameter should be the name of a function
+-- @:: forall a. StT t a -> a@.
+makeTransSTM :: Name -> DecsQ
+makeTransSTM unstN = do
+  unstI <- reify unstN
+  case unstI of
+    VarI _ (ForallT _ _ (AppT (AppT ArrowT (AppT (AppT (ConT _) t) _)) _)) _ _ ->
+      [d|
+        instance (MonadSTM stm, MonadTransControl $(pure t)) => MonadSTM ($(pure t) stm) where
+          type TVar ($(pure t) stm) = TVar stm
 
-instance (MonadSTM m, Monoid w) => MonadSTM (RS.RWST r w s m) where
-  type CTVar (RS.RWST r w s m) = CTVar m
+          retry       = lift retry
+          orElse      = liftedOrElse $(varE unstN)
+          newTVar     = lift . newTVar
+          newTVarN n  = lift . newTVarN n
+          readTVar    = lift . readTVar
+          writeTVar v = lift . writeTVar v
+      |]
+    _ -> fail "Expected a value of type (forall a -> StT t a -> a)"
 
-  retry        = lift retry
-  orElse ma mb = RS.RWST $ \r s -> orElse (RS.runRWST ma r s) (RS.runRWST mb r s)
-  check        = lift . check
-  newCTVar     = lift . newCTVar
-  readCTVar    = lift . readCTVar
-  writeCTVar v = lift . writeCTVar v
+-- | Given a function to remove the transformer-specific state, lift
+-- an @orElse@ invocation.
+liftedOrElse :: (MonadTransControl t, MonadSTM stm)
+  => (forall x. StT t x -> x)
+  -> t stm a -> t stm a -> t stm a
+liftedOrElse unst ma mb = liftWith $ \run ->
+  let ma' = unst <$> run ma
+      mb' = unst <$> run mb
+  in ma' `orElse` mb'
diff --git a/Data/List/Extra.hs b/Data/List/Extra.hs
deleted file mode 100644
--- a/Data/List/Extra.hs
+++ /dev/null
@@ -1,60 +0,0 @@
-{-# LANGUAGE CPP #-}
--- | Extra list functions and list-like types.
-module Data.List.Extra where
-
-import Control.DeepSeq (NFData(..))
-import Data.Traversable (fmapDefault, foldMapDefault)
-
-#if __GLASGOW_HASKELL__ < 710
-import Control.Applicative ((<$>), (<*>))
-import Data.Foldable (Foldable(..))
-import Data.Traversable (Traversable(..))
-#else
--- Why does this give a redundancy warning? It's necessary in order to
--- define the toList function in the Foldable instance for NonEmpty!
-import Data.Foldable (toList)
-#endif
-
--- * Regular lists
-
--- | Check if a list has more than some number of elements.
-moreThan :: [a] -> Int -> Bool
-moreThan [] n = n < 0
-moreThan _ 0  = True
-moreThan (_:xs) n = moreThan xs (n-1)
-
--- * Non-empty lists
-
--- This gets exposed to users of the library, so it has a bunch of
--- classes which aren't actually used in the rest of the code to make
--- it more friendly to further use.
-
--- | The type of non-empty lists.
-data NonEmpty a = a :| [a] deriving (Eq, Ord, Read, Show)
-
-instance Functor NonEmpty where
-  fmap = fmapDefault
-
-instance Foldable NonEmpty where
-  foldMap = foldMapDefault
-
-#if __GLASGOW_HASKELL__ >= 710
-  -- toList isn't in Foldable until GHC 7.10
-  toList (a :| as) = a : as
-#endif
-
-instance Traversable NonEmpty where
-  traverse f (a:|as) = (:|) <$> f a <*> traverse f as
-
-instance NFData a => NFData (NonEmpty a) where
-  rnf (x:|xs) = rnf (x, xs)
-
--- | Convert a 'NonEmpty' to a regular non-empty list.
-toList :: NonEmpty a -> [a]
-toList (a :| as) = a : as
-
--- | Convert a regular non-empty list to a 'NonEmpty'. This is
--- necessarily partial.
-unsafeToNonEmpty :: [a] -> NonEmpty a
-unsafeToNonEmpty (a:as) = a :| as
-unsafeToNonEmpty [] = error "Cannot convert [] to NonEmpty!"
diff --git a/Test/DejaFu.hs b/Test/DejaFu.hs
--- a/Test/DejaFu.hs
+++ b/Test/DejaFu.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE CPP        #-}
 {-# LANGUAGE RankNTypes #-}
 
 -- | Deterministic testing for concurrent computations.
@@ -10,18 +9,21 @@
 --
 -- > example1 :: MonadConc m => m Int
 -- > example1 = do
--- >   a <- newEmptyCVar
--- >   b <- newEmptyCVar
+-- >   a <- newEmptyMVar
+-- >   b <- newEmptyMVar
 -- >
--- >   c <- newCVar 0
+-- >   c <- newMVar 0
 -- >
--- >   j1 <- spawn $ lock a >> lock b >> modifyCVar_ c (return . succ) >> unlock b >> unlock a
--- >   j2 <- spawn $ lock b >> lock a >> modifyCVar_ c (return . pred) >> unlock a >> unlock b
+-- >   let lock m = putMVar m ()
+-- >   let unlock = takeMVar
 -- >
--- >   takeCVar j1
--- >   takeCVar j2
+-- >   j1 <- spawn $ lock a >> lock b >> modifyMVar_ c (return . succ) >> unlock b >> unlock a
+-- >   j2 <- spawn $ lock b >> lock a >> modifyMVar_ c (return . pred) >> unlock a >> unlock b
 -- >
--- >   takeCVar c
+-- >   takeMVar j1
+-- >   takeMVar j2
+-- >
+-- >   takeMVar c
 --
 -- The correct result is 0, as it starts out as 0 and is incremented
 -- and decremented by threads 1 and 2, respectively. However, note the
@@ -109,7 +111,7 @@
   -- >   x <- spawn $ writeCRef r1 True >> readCRef r2
   -- >   y <- spawn $ writeCRef r2 True >> readCRef r1
   -- >
-  -- >   (,) <$> readCVar x <*> readCVar y
+  -- >   (,) <$> readMVar x <*> readMVar y
   --
   -- Under a sequentially consistent memory model the possible results
   -- are @(True, True)@, @(True, False)@, and @(False, True)@. Under
@@ -147,8 +149,8 @@
   -- writes to @CRef@s are /committed/, which makes a write visible to
   -- all threads rather than just the one which performed the
   -- write. Only 'writeCRef' is broken up into separate write and
-  -- commit steps, 'modifyCRef' is still atomic and imposes a memory
-  -- barrier.
+  -- commit steps, 'atomicModifyCRef' is still atomic and imposes a
+  -- memory barrier.
 
   , MemType(..)
   , defaultMemType
@@ -169,6 +171,7 @@
 
   , Bounds(..)
   , defaultBounds
+  , noBounds
   , PreemptionBound(..)
   , defaultPreemptionBound
   , FairBound(..)
@@ -228,18 +231,13 @@
 import Control.DeepSeq (NFData(..))
 import Control.Monad (when, unless)
 import Data.Function (on)
-import Data.List (minimumBy)
-import Data.List.Extra
-import Data.Monoid ((<>))
+import Data.List (intercalate, intersperse, minimumBy)
+--import Data.List.NonEmpty
 import Data.Ord (comparing)
 import Test.DejaFu.Deterministic
+import Test.DejaFu.Deterministic.Internal (preEmpCount)
 import Test.DejaFu.SCT
 
-#if __GLASGOW_HASKELL__ < 710
-import Control.Applicative ((<$>))
-import Data.Foldable (Foldable(..))
-#endif
-
 -- | The default memory model: @TotalStoreOrder@
 defaultMemType :: MemType
 defaultMemType = TotalStoreOrder
@@ -372,14 +370,14 @@
   -- ^ Whether the test passed or not.
   , _casesChecked :: Int
   -- ^ The number of cases checked.
-  , _failures     :: [(Either Failure a, Trace)]
+  , _failures     :: [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
   -- ^ The failing cases, if any.
   , _failureMsg   :: String
   -- ^ A message to display on failure, if nonempty
-  } deriving (Show, Eq)
+  } deriving Show
 
 -- | A failed result, taking the given list of failures.
-defaultFail :: [(Either Failure a, Trace)] -> Result a
+defaultFail :: [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] -> Result a
 defaultFail failures = Result False 0 failures ""
 
 -- | A passed result.
@@ -431,7 +429,7 @@
 
 -- | A @Predicate@ is a function which collapses a list of results
 -- into a 'Result'.
-type Predicate a = [(Either Failure a, Trace)] -> Result a
+type Predicate a = [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] -> Result a
 
 -- | Reduce the list of failures in a @Predicate@ to one
 -- representative trace for each unique result.
@@ -443,15 +441,18 @@
 representative p xs = result { _failures = choose . collect $ _failures result } where
   result  = p xs
   collect = groupBy' [] ((==) `on` fst)
-  choose  = map $ minimumBy (comparing $ \(_, trc) -> (preEmpCount' trc, length trc))
+  choose  = map $ minimumBy (comparing $ \(_, trc) -> (preEmps trc, length trc))
 
+  preEmps trc = preEmpCount (map (\(d,_,a) -> (d, a)) trc) (Continue, WillStop)
+
   groupBy' res _ [] = res
-  groupBy' res eq (x:xs) = groupBy' (insert' eq x res) eq xs
+  groupBy' res eq (y:ys) = groupBy' (insert' eq y res) eq ys
 
-  insert' eq x [] = [[x]]
+  insert' _ x [] = [[x]]
   insert' eq x (ys@(y:_):yss)
     | x `eq` y  = (x:ys) : yss
     | otherwise = ys : insert' eq x yss
+  insert' _ _ ([]:_) = undefined
 
 -- | Check that a computation never aborts.
 abortsNever :: Predicate a
@@ -598,12 +599,24 @@
       putStrLn $ _failureMsg result
 
     let failures = _failures result
-    mapM_ (\(r, t) -> putStrLn $ "\t" ++ either showFail show r ++ " " ++ showTrace t) $ take 5 failures
-    when (moreThan failures 5) $
-      putStrLn "\t..."
+    let output = map (\(r, t) -> putStrLn . indent $ either showFail show r ++ " " ++ showTrace t) $ take 5 failures
+    sequence_ $ intersperse (putStrLn "") output
+    when (moreThan 5 failures) $
+      putStrLn (indent "...")
 
   return $ _pass result
 
+-- | Check if a list is longer than some value, without needing to
+-- compute the entire length.
+moreThan :: Int -> [a] -> Bool
+moreThan n [] = n < 0
+moreThan 0 _ = True
+moreThan n (_:rest) = moreThan (n-1) rest
+
 -- | Increment the cases
 incCC :: Result a -> Result a
 incCC r = r { _casesChecked = _casesChecked r + 1 }
+
+-- | Indent every line of a string.
+indent :: String -> String
+indent = intercalate "\n" . map ('\t':) . lines
diff --git a/Test/DejaFu/Deterministic.hs b/Test/DejaFu/Deterministic.hs
--- a/Test/DejaFu/Deterministic.hs
+++ b/Test/DejaFu/Deterministic.hs
@@ -1,6 +1,6 @@
-{-# LANGUAGE CPP                        #-}
 {-# LANGUAGE FlexibleInstances          #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses      #-}
 {-# LANGUAGE RankNTypes                 #-}
 {-# LANGUAGE TypeFamilies               #-}
 {-# LANGUAGE TypeSynonymInstances       #-}
@@ -21,44 +21,39 @@
   , MemType(..)
   , runConcST
   , runConcIO
-  , runConcST'
-  , runConcIO'
 
   -- * Execution traces
   , Trace
-  , Trace'
   , Decision(..)
+  , ThreadId(..)
   , ThreadAction(..)
   , Lookahead(..)
-  , CVarId
+  , MVarId
   , CRefId
   , MaskingState(..)
-  , toTrace
   , showTrace
   , showFail
 
   -- * Scheduling
-  , module Test.DejaFu.Deterministic.Schedule
+  , module Test.DPOR.Schedule
   ) where
 
 import Control.Exception (MaskingState(..))
 import Control.Monad.ST (ST, runST)
+import Data.Dynamic (toDyn)
 import Data.IORef (IORef)
 import Data.STRef (STRef)
 import Test.DejaFu.Deterministic.Internal
-import Test.DejaFu.Deterministic.Schedule
 import Test.DejaFu.Internal (refST, refIO)
 import Test.DejaFu.STM (STMLike, STMIO, STMST, runTransactionIO, runTransactionST)
-import Test.DejaFu.STM.Internal (CTVar(..))
+import Test.DejaFu.STM.Internal (TVar(..))
+import Test.DPOR.Schedule
 
+import qualified Control.Monad.Base as Ba
 import qualified Control.Monad.Catch as Ca
 import qualified Control.Monad.Conc.Class as C
 import qualified Control.Monad.IO.Class as IO
 
-#if __GLASGOW_HASKELL__ < 710
-import Control.Applicative (Applicative(..), (<$>))
-#endif
-
 {-# ANN module ("HLint: ignore Avoid lambda" :: String) #-}
 {-# ANN module ("HLint: ignore Use const"    :: String) #-}
 
@@ -80,6 +75,9 @@
 instance IO.MonadIO ConcIO where
   liftIO ma = toConc (\c -> ALift (fmap c ma))
 
+instance Ba.MonadBase IO ConcIO where
+  liftBase = IO.liftIO
+
 instance Ca.MonadCatch (Conc n r s) where
   catch ma h = toConc (ACatching (unC . h) (unC ma))
 
@@ -91,16 +89,16 @@
   uninterruptibleMask mb = toConc (AMasking MaskedUninterruptible (\f -> unC $ mb $ wrap f))
 
 instance Monad n => C.MonadConc (Conc n r (STMLike n r)) where
-  type CVar     (Conc n r (STMLike n r)) = CVar r
+  type MVar     (Conc n r (STMLike n r)) = MVar r
   type CRef     (Conc n r (STMLike n r)) = CRef r
   type Ticket   (Conc n r (STMLike n r)) = Ticket
-  type STMLike  (Conc n r (STMLike n r)) = STMLike n r
+  type STM      (Conc n r (STMLike n r)) = STMLike n r
   type ThreadId (Conc n r (STMLike n r)) = ThreadId
 
   -- ----------
 
-  forkWithUnmask  ma = toConc (AFork (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop)))
-  forkOnWithUnmask _ = C.forkWithUnmask
+  forkWithUnmaskN   n ma = toConc (AFork n (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop)))
+  forkOnWithUnmaskN n _  = C.forkWithUnmaskN n
 
   -- This implementation lies and returns 2 until a value is set. This
   -- will potentially avoid special-case behaviour for 1 capability,
@@ -114,7 +112,7 @@
 
   -- ----------
 
-  newCRef a = toConc (\c -> ANewRef a c)
+  newCRefN n a = toConc (\c -> ANewRef n a c)
 
   readCRef   ref = toConc (AReadRef    ref)
   readForCAS ref = toConc (AReadRefCas ref)
@@ -124,19 +122,19 @@
   writeCRef ref      a = toConc (\c -> AWriteRef ref a (c ()))
   casCRef   ref tick a = toConc (ACasRef ref tick a)
 
-  modifyCRef    ref f = toConc (AModRef    ref f)
-  modifyCRefCAS ref f = toConc (AModRefCas ref f)
+  atomicModifyCRef ref f = toConc (AModRef    ref f)
+  modifyCRefCAS    ref f = toConc (AModRefCas ref f)
 
   -- ----------
 
-  newEmptyCVar = toConc (\c -> ANewVar c)
+  newEmptyMVarN n = toConc (\c -> ANewVar n c)
 
-  putCVar  var a = toConc (\c -> APutVar var a (c ()))
-  readCVar var   = toConc (AReadVar var)
-  takeCVar var   = toConc (ATakeVar var)
+  putMVar  var a = toConc (\c -> APutVar var a (c ()))
+  readMVar var   = toConc (AReadVar var)
+  takeMVar var   = toConc (ATakeVar var)
 
-  tryPutCVar  var a = toConc (ATryPutVar  var a)
-  tryTakeCVar var   = toConc (ATryTakeVar var)
+  tryPutMVar  var a = toConc (ATryPutVar  var a)
+  tryTakeMVar var   = toConc (ATryTakeVar var)
 
   -- ----------
 
@@ -148,14 +146,16 @@
 
   -- ----------
 
-  _concKnowsAbout (Left  (CVar  (cvarid,  _))) = toConc (\c -> AKnowsAbout (Left  cvarid)  (c ()))
-  _concKnowsAbout (Right (CTVar (ctvarid, _))) = toConc (\c -> AKnowsAbout (Right ctvarid) (c ()))
+  _concKnowsAbout (Left  (MVar cvarid  _)) = toConc (\c -> AKnowsAbout (Left  cvarid)  (c ()))
+  _concKnowsAbout (Right (TVar (ctvarid, _))) = toConc (\c -> AKnowsAbout (Right ctvarid) (c ()))
 
-  _concForgets (Left  (CVar  (cvarid,  _))) = toConc (\c -> AForgets (Left  cvarid)  (c ()))
-  _concForgets (Right (CTVar (ctvarid, _))) = toConc (\c -> AForgets (Right ctvarid) (c ()))
+  _concForgets (Left  (MVar cvarid  _)) = toConc (\c -> AForgets (Left  cvarid)  (c ()))
+  _concForgets (Right (TVar (ctvarid, _))) = toConc (\c -> AForgets (Right ctvarid) (c ()))
 
   _concAllKnown = toConc (\c -> AAllKnown (c ()))
 
+  _concMessage msg = toConc (\c -> AMessage (toDyn msg) (c ()))
+
 -- | Run a concurrent computation with a given 'Scheduler' and initial
 -- state, returning a failure reason on error. Also returned is the
 -- final state of the scheduler, and an execution trace.
@@ -163,20 +163,20 @@
 -- Note how the @t@ in 'Conc' is universally quantified, what this
 -- means in practice is that you can't do something like this:
 --
--- > runConc roundRobinSched SequentialConsistency () newEmptyCVar
+-- > runConc roundRobinSched SequentialConsistency () newEmptyMVar
 --
 -- So mutable references cannot leak out of the 'Conc' computation. If
 -- this is making your head hurt, check out the \"How @runST@ works\"
 -- section of
 -- <https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html>
-runConcST :: Scheduler s -> MemType -> s -> (forall t. ConcST t a) -> (Either Failure a, s, Trace)
-runConcST sched memtype s ma =
-  let (r, s', t') = runConcST' sched memtype s ma
-  in  (r, s', toTrace t')
-
--- | Variant of 'runConcST' which produces a 'Trace''.
-runConcST' :: Scheduler s -> MemType -> s -> (forall t. ConcST t a) -> (Either Failure a, s, Trace')
-runConcST' sched memtype s ma = runST $ runFixed fixed runTransactionST sched memtype s $ unC ma where
+--
+-- __Note:__ In order to prevent computation from hanging, the runtime
+-- will assume that a deadlock situation has arisen if the scheduler
+-- attempts to (a) schedule a blocked thread, or (b) schedule a
+-- nonexistent thread. In either of those cases, the computation will
+-- be halted.
+runConcST :: Scheduler ThreadId ThreadAction Lookahead s -> MemType -> s -> (forall t. ConcST t a) -> (Either Failure a, s, Trace ThreadId ThreadAction Lookahead)
+runConcST sched memtype s ma = runST $ runFixed fixed runTransactionST sched memtype s $ unC ma where
   fixed = refST $ \mb -> cont (\c -> ALift $ c <$> mb)
 
 -- | Run a concurrent computation in the @IO@ monad with a given
@@ -190,12 +190,12 @@
 -- You should therefore keep @IO@ blocks small, and only perform
 -- blocking operations with the supplied primitives, insofar as
 -- possible.
-runConcIO :: Scheduler s -> MemType -> s -> ConcIO a -> IO (Either Failure a, s, Trace)
-runConcIO sched memtype s ma = do
-  (r, s', t') <- runConcIO' sched memtype s ma
-  return (r, s', toTrace t')
-
--- | Variant of 'runConcIO' which produces a 'Trace''.
-runConcIO' :: Scheduler s -> MemType -> s -> ConcIO a -> IO (Either Failure a, s, Trace')
-runConcIO' sched memtype s ma = runFixed fixed runTransactionIO sched memtype s $ unC ma where
+--
+-- __Note:__ In order to prevent computation from hanging, the runtime
+-- will assume that a deadlock situation has arisen if the scheduler
+-- attempts to (a) schedule a blocked thread, or (b) schedule a
+-- nonexistent thread. In either of those cases, the computation will
+-- be halted.
+runConcIO :: Scheduler ThreadId ThreadAction Lookahead s -> MemType -> s -> ConcIO a -> IO (Either Failure a, s, Trace ThreadId ThreadAction Lookahead)
+runConcIO sched memtype s ma = runFixed fixed runTransactionIO sched memtype s $ unC ma where
   fixed = refIO $ \mb -> cont (\c -> ALift $ c <$> mb)
diff --git a/Test/DejaFu/Deterministic/Internal.hs b/Test/DejaFu/Deterministic/Internal.hs
--- a/Test/DejaFu/Deterministic/Internal.hs
+++ b/Test/DejaFu/Deterministic/Internal.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE CPP                 #-}
 {-# LANGUAGE RankNTypes          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
@@ -11,7 +10,7 @@
 
  -- * The @Conc@ Monad
  , M(..)
- , CVar(..)
+ , MVar(..)
  , CRef(..)
  , Ticket(..)
  , Fixed
@@ -23,8 +22,9 @@
 
  -- * Identifiers
  , ThreadId(..)
- , CVarId(..)
+ , MVarId(..)
  , CRefId(..)
+ , initialThread
 
  -- * Memory Models
  , MemType(..)
@@ -35,16 +35,17 @@
  , Decision(..)
  , ThreadAction(..)
  , Lookahead(..)
- , Trace'
+ , isBlock
  , lookahead
  , willRelease
- , toTrace
+ , preEmpCount
  , showTrace
  , showFail
 
  -- * Synchronised and Unsynchronised Actions
  , ActionType(..)
  , isBarrier
+ , isCommit
  , synchronises
  , crefOf
  , cvarOf
@@ -55,23 +56,20 @@
  , Failure(..)
  ) where
 
-import Control.Exception (MaskingState(..), SomeException(..))
+import Control.Exception (MaskingState(..), toException)
+import Data.Functor (void)
 import Data.List (sort)
-import Data.List.Extra
-import Data.Maybe (fromJust, isJust, fromMaybe, isNothing, listToMaybe)
-import Data.Typeable (cast)
-import Test.DejaFu.STM (CTVarId, Result(..))
+import Data.List.NonEmpty (NonEmpty(..), fromList)
+import Data.Maybe (fromJust, isJust, isNothing, listToMaybe)
+import Test.DejaFu.STM (Result(..))
 import Test.DejaFu.Internal
 import Test.DejaFu.Deterministic.Internal.Common
 import Test.DejaFu.Deterministic.Internal.Memory
 import Test.DejaFu.Deterministic.Internal.Threading
+import Test.DPOR (Decision(..), Scheduler, Trace)
 
 import qualified Data.Map.Strict as M
 
-#if __GLASGOW_HASKELL__ < 710
-import Control.Applicative ((<$>), (<*>))
-#endif
-
 {-# ANN module ("HLint: ignore Use record patterns" :: String) #-}
 {-# ANN module ("HLint: ignore Use const"           :: String) #-}
 
@@ -82,19 +80,19 @@
 -- state, returning a 'Just' if it terminates, and 'Nothing' if a
 -- deadlock is detected. Also returned is the final state of the
 -- scheduler, and an execution trace.
-runFixed :: (Functor n, Monad n) => Fixed n r s -> (forall x. s x -> CTVarId -> n (Result x, CTVarId))
-         -> Scheduler g -> MemType -> g -> M n r s a -> n (Either Failure a, g, Trace')
+runFixed :: (Functor n, Monad n) => Fixed n r s -> (forall x. s x -> IdSource -> n (Result x, IdSource, TTrace))
+         -> Scheduler ThreadId ThreadAction Lookahead g -> MemType -> g -> M n r s a -> n (Either Failure a, g, Trace ThreadId ThreadAction Lookahead)
 runFixed fixed runstm sched memtype s ma = (\(e,g,_,t) -> (e,g,t)) <$> runFixed' fixed runstm sched memtype s initialIdSource ma
 
 -- | Same as 'runFixed', be parametrised by an 'IdSource'.
 runFixed' :: forall n r s g a. (Functor n, Monad n)
-  => Fixed n r s -> (forall x. s x -> CTVarId -> n (Result x, CTVarId))
-  -> Scheduler g -> MemType -> g -> IdSource -> M n r s a -> n (Either Failure a, g, IdSource, Trace')
+  => Fixed n r s -> (forall x. s x -> IdSource -> n (Result x, IdSource, TTrace))
+  -> Scheduler ThreadId ThreadAction Lookahead g -> MemType -> g -> IdSource -> M n r s a -> n (Either Failure a, g, IdSource, Trace ThreadId ThreadAction Lookahead)
 runFixed' fixed runstm sched memtype s idSource ma = do
   ref <- newRef fixed Nothing
 
   let c       = ma >>= liftN fixed . writeRef fixed ref . Just . Right
-  let threads = launch' Unmasked 0 ((\a _ -> a) $ runCont c $ const AStop) M.empty
+  let threads = launch' Unmasked initialThread ((\a _ -> a) $ runCont c $ const AStop) M.empty
 
   (s', idSource', trace) <- runThreads fixed runstm sched memtype s threads idSource ref
   out <- readRef fixed ref
@@ -107,8 +105,8 @@
 -- efficient to prepend to a list than append. As this function isn't
 -- exposed to users of the library, this is just an internal gotcha to
 -- watch out for.
-runThreads :: (Functor n, Monad n) => Fixed n r s -> (forall x. s x -> CTVarId -> n (Result x, CTVarId))
-           -> Scheduler g -> MemType -> g -> Threads n r s -> IdSource -> r (Maybe (Either Failure a)) -> n (g, IdSource, Trace')
+runThreads :: (Functor n, Monad n) => Fixed n r s -> (forall x. s x -> IdSource -> n (Result x, IdSource, TTrace))
+           -> Scheduler ThreadId ThreadAction Lookahead g -> MemType -> g -> Threads n r s -> IdSource -> r (Maybe (Either Failure a)) -> n (g, IdSource, Trace ThreadId ThreadAction Lookahead)
 runThreads fixed runstm sched memtype origg origthreads idsrc ref = go idsrc [] Nothing origg origthreads emptyBuffer 2 where
   go idSource sofar prior g threads wb caps
     | isTerminated  = stop g
@@ -123,13 +121,13 @@
         Right (threads', idSource', act, wb', caps') -> loop threads' idSource' act wb' caps'
 
         Left UncaughtException
-          | chosen == 0 -> die g' UncaughtException
+          | chosen == initialThread -> die g' UncaughtException
           | otherwise -> loop (kill chosen threads) idSource Killed wb caps
 
         Left failure -> die g' failure
 
     where
-      (choice, g')  = sched g (map (\(d,_,a) -> (d,a)) $ reverse sofar) ((\p (_,_,a) -> (p,a)) <$> prior <*> listToMaybe sofar) $ unsafeToNonEmpty runnable'
+      (choice, g')  = sched (map (\(d,_,a) -> (d,a)) $ reverse sofar) ((\p (_,_,a) -> (p,a)) <$> prior <*> listToMaybe sofar) (fromList $ map (\(t,l:|_) -> (t,l)) runnable') g
       chosen        = fromJust choice
       runnable'     = [(t, nextActions t) | t <- sort $ M.keys runnable]
       runnable      = M.filter (isNothing . _blocking) threadsc
@@ -138,11 +136,13 @@
       isAborted     = isNothing choice
       isBlocked     = isJust . _blocking $ fromJust thread
       isNonexistant = isNothing thread
-      isTerminated  = 0 `notElem` M.keys threads
-      isDeadlocked  = isLocked 0 threads && (((~= OnCVarFull  undefined) <$> M.lookup 0 threads) == Just True ||
-                                           ((~=  OnCVarEmpty undefined) <$> M.lookup 0 threads) == Just True ||
-                                           ((~=  OnMask      undefined) <$> M.lookup 0 threads) == Just True)
-      isSTMLocked   = isLocked 0 threads && ((~=  OnCTVar    []) <$> M.lookup 0 threads) == Just True
+      isTerminated  = initialThread `notElem` M.keys threads
+      isDeadlocked  = isLocked initialThread threads &&
+        (((~=  OnMVarFull  undefined) <$> M.lookup initialThread threads) == Just True ||
+         ((~=  OnMVarEmpty undefined) <$> M.lookup initialThread threads) == Just True ||
+         ((~=  OnMask      undefined) <$> M.lookup initialThread threads) == Just True)
+      isSTMLocked = isLocked initialThread threads &&
+        ((~=  OnTVar []) <$> M.lookup initialThread threads) == Just True
 
       unblockWaitingOn tid = fmap unblock where
         unblock thrd = case _blocking thrd of
@@ -154,18 +154,13 @@
         | prior `notElem` map (Just . fst) runnable' = Start chosen
         | otherwise = SwitchTo chosen
 
-      alternatives
-        | Just chosen == prior = [(SwitchTo t, na) | (t, na) <- runnable', Just t /= prior]
-        | prior `notElem` map (Just . fst) runnable' = [(Start t, na) | (t, na) <- runnable', t /= chosen]
-        | otherwise = [(if Just t == prior then Continue else SwitchTo t, na) | (t, na) <- runnable', t /= chosen]
-
       nextActions t = lookahead . _continuation . fromJust $ M.lookup t threadsc
 
       stop outg = return (outg, idSource, sofar)
       die  outg reason = writeRef fixed ref (Just $ Left reason) >> stop outg
 
       loop threads' idSource' act wb' =
-        let sofar' = ((decision, alternatives, act) : sofar)
+        let sofar' = ((decision, runnable', act) : sofar)
             threads'' = if (interruptible <$> M.lookup chosen threads') /= Just False then unblockWaitingOn chosen threads' else threads'
         in go idSource' sofar' (Just chosen) g' (delCommitThreads threads'') wb'
 
@@ -175,7 +170,7 @@
 -- | Run a single thread one step, by dispatching on the type of
 -- 'Action'.
 stepThread :: forall n r s. (Functor n, Monad n) => Fixed n r s
-  -> (forall x. s x -> CTVarId -> n (Result x, CTVarId))
+  -> (forall x. s x -> IdSource -> n (Result x, IdSource, TTrace))
   -- ^ Run a 'MonadSTM' transaction atomically.
   -> MemType
   -- ^ The memory model
@@ -193,18 +188,18 @@
   -- ^ The number of capabilities
   -> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int))
 stepThread fixed runstm memtype action idSource tid threads wb caps = case action of
-  AFork    a b     -> stepFork        a b
+  AFork    n a b   -> stepFork        n a b
   AMyTId   c       -> stepMyTId       c
   AGetNumCapabilities   c -> stepGetNumCapabilities c
   ASetNumCapabilities i c -> stepSetNumCapabilities i c
   AYield   c       -> stepYield       c
-  ANewVar  c       -> stepNewVar      c
+  ANewVar  n c     -> stepNewVar      n c
   APutVar  var a c -> stepPutVar      var a c
   ATryPutVar var a c -> stepTryPutVar var a c
   AReadVar var c   -> stepReadVar     var c
   ATakeVar var c   -> stepTakeVar     var c
   ATryTakeVar var c -> stepTryTakeVar var c
-  ANewRef  a c     -> stepNewRef      a c
+  ANewRef  n a c   -> stepNewRef      n a c
   AReadRef ref c   -> stepReadRef     ref c
   AReadRefCas ref c -> stepReadRefCas ref c
   APeekTicket tick c -> stepPeekTicket tick c
@@ -225,13 +220,14 @@
   AKnowsAbout v c  -> stepKnowsAbout  v c
   AForgets    v c  -> stepForgets v c
   AAllKnown   c    -> stepAllKnown c
+  AMessage    m c  -> stepMessage m c
   AStop            -> stepStop
 
   where
     -- | Start a new thread, assigning it the next 'ThreadId'
-    stepFork a b = return $ Right (goto (b newtid) tid threads', idSource', Fork newtid, wb, caps) where
+    stepFork n a b = return $ Right (goto (b newtid) tid threads', idSource', Fork newtid, wb, caps) where
       threads' = launch tid newtid a threads
-      (idSource', newtid) = nextTId idSource
+      (idSource', newtid) = nextTId n idSource
 
     -- | Get the 'ThreadId' of the current thread
     stepMyTId c = simple (goto (c tid) tid threads) MyThreadId
@@ -245,62 +241,62 @@
     -- | Yield the current thread
     stepYield c = simple (goto c tid threads) Yield
 
-    -- | Put a value into a @CVar@, blocking the thread until it's
+    -- | Put a value into a @MVar@, blocking the thread until it's
     -- empty.
-    stepPutVar cvar@(CVar (cvid, _)) a c = synchronised $ do
-      (success, threads', woken) <- putIntoCVar cvar a c fixed tid threads
+    stepPutVar cvar@(MVar cvid _) a c = synchronised $ do
+      (success, threads', woken) <- putIntoMVar cvar a c fixed tid threads
       simple threads' $ if success then PutVar cvid woken else BlockedPutVar cvid
 
-    -- | Try to put a value into a @CVar@, without blocking.
-    stepTryPutVar cvar@(CVar (cvid, _)) a c = synchronised $ do
-      (success, threads', woken) <- tryPutIntoCVar cvar a c fixed tid threads
+    -- | Try to put a value into a @MVar@, without blocking.
+    stepTryPutVar cvar@(MVar cvid _) a c = synchronised $ do
+      (success, threads', woken) <- tryPutIntoMVar cvar a c fixed tid threads
       simple threads' $ TryPutVar cvid success woken
 
-    -- | Get the value from a @CVar@, without emptying, blocking the
+    -- | Get the value from a @MVar@, without emptying, blocking the
     -- thread until it's full.
-    stepReadVar cvar@(CVar (cvid, _)) c = synchronised $ do
-      (success, threads', _) <- readFromCVar cvar c fixed tid threads
+    stepReadVar cvar@(MVar cvid _) c = synchronised $ do
+      (success, threads', _) <- readFromMVar cvar c fixed tid threads
       simple threads' $ if success then ReadVar cvid else BlockedReadVar cvid
 
-    -- | Take the value from a @CVar@, blocking the thread until it's
+    -- | Take the value from a @MVar@, blocking the thread until it's
     -- full.
-    stepTakeVar cvar@(CVar (cvid, _)) c = synchronised $ do
-      (success, threads', woken) <- takeFromCVar cvar c fixed tid threads
+    stepTakeVar cvar@(MVar cvid _) c = synchronised $ do
+      (success, threads', woken) <- takeFromMVar cvar c fixed tid threads
       simple threads' $ if success then TakeVar cvid woken else BlockedTakeVar cvid
 
-    -- | Try to take the value from a @CVar@, without blocking.
-    stepTryTakeVar cvar@(CVar (cvid, _)) c = synchronised $ do
-      (success, threads', woken) <- tryTakeFromCVar cvar c fixed tid threads
+    -- | Try to take the value from a @MVar@, without blocking.
+    stepTryTakeVar cvar@(MVar cvid _) c = synchronised $ do
+      (success, threads', woken) <- tryTakeFromMVar cvar c fixed tid threads
       simple threads' $ TryTakeVar cvid success woken
 
     -- | Read from a @CRef@.
-    stepReadRef cref@(CRef (crid, _)) c = do
+    stepReadRef cref@(CRef crid _) c = do
       val <- readCRef fixed cref tid
       simple (goto (c val) tid threads) $ ReadRef crid
 
     -- | Read from a @CRef@ for future compare-and-swap operations.
-    stepReadRefCas cref@(CRef (crid, _)) c = do
+    stepReadRefCas cref@(CRef crid _) c = do
       tick <- readForTicket fixed cref tid
       simple (goto (c tick) tid threads) $ ReadRefCas crid
 
     -- | Extract the value from a @Ticket@.
-    stepPeekTicket (Ticket (crid, _, a)) c = simple (goto (c a) tid threads) $ PeekTicket crid
+    stepPeekTicket (Ticket crid _ a) c = simple (goto (c a) tid threads) $ PeekTicket crid
 
     -- | Modify a @CRef@.
-    stepModRef cref@(CRef (crid, _)) f c = synchronised $ do
+    stepModRef cref@(CRef crid _) f c = synchronised $ do
       (new, val) <- f <$> readCRef fixed cref tid
       writeImmediate fixed cref new
       simple (goto (c val) tid threads) $ ModRef crid
 
     -- | Modify a @CRef@ using a compare-and-swap.
-    stepModRefCas cref@(CRef (crid, _)) f c = synchronised $ do
-      tick@(Ticket (_, _, old)) <- readForTicket fixed cref tid
+    stepModRefCas cref@(CRef crid _) f c = synchronised $ do
+      tick@(Ticket _ _ old) <- readForTicket fixed cref tid
       let (new, val) = f old
-      casCRef fixed cref tid tick new
+      void $ casCRef fixed cref tid tick new
       simple (goto (c val) tid threads) $ ModRefCas crid
 
     -- | Write to a @CRef@ without synchronising
-    stepWriteRef cref@(CRef (crid, _)) a c = case memtype of
+    stepWriteRef cref@(CRef crid _) a c = case memtype of
       -- Write immediately.
       SequentialConsistency -> do
         writeImmediate fixed cref a
@@ -308,51 +304,49 @@
 
       -- Add to buffer using thread id.
       TotalStoreOrder -> do
-        let (ThreadId tid') = tid
-        wb' <- bufferWrite fixed wb tid' cref a tid
+        wb' <- bufferWrite fixed wb (tid, Nothing) cref a
         return $ Right (goto c tid threads, idSource, WriteRef crid, wb', caps)
 
-      -- Add to buffer using cref id
+      -- Add to buffer using both thread id and cref id
       PartialStoreOrder -> do
-        let (CRefId crid') = crid
-        wb' <- bufferWrite fixed wb crid' cref a tid
+        wb' <- bufferWrite fixed wb (tid, Just crid) cref a
         return $ Right (goto c tid threads, idSource, WriteRef crid, wb', caps)
 
     -- | Perform a compare-and-swap on a @CRef@.
-    stepCasRef cref@(CRef (crid, _)) tick a c = synchronised $ do
+    stepCasRef cref@(CRef crid _) tick a c = synchronised $ do
       (suc, tick') <- casCRef fixed cref tid tick a
       simple (goto (c (suc, tick')) tid threads) $ CasRef crid suc
 
     -- | Commit a @CRef@ write
-    stepCommit t@(ThreadId t') c@(CRefId c') = do
+    stepCommit t c = do
       wb' <- case memtype of
         -- Shouldn't ever get here
         SequentialConsistency ->
           error "Attempting to commit under SequentialConsistency"
 
         -- Commit using the thread id.
-        TotalStoreOrder -> commitWrite fixed wb t'
+        TotalStoreOrder -> commitWrite fixed wb (t, Nothing)
 
         -- Commit using the cref id.
-        PartialStoreOrder -> commitWrite fixed wb c'
+        PartialStoreOrder -> commitWrite fixed wb (t, Just c)
 
       return $ Right (threads, idSource, CommitRef t c, wb', caps)
 
     -- | Run a STM transaction atomically.
     stepAtom stm c = synchronised $ do
-      let oldctvid = _nextCTVId idSource
-      (res, newctvid) <- runstm stm oldctvid
+      (res, idSource', trace) <- runstm stm idSource
       case res of
-        Success readen written val
-          | any (<oldctvid) readen || any (<oldctvid) written ->
-            let (threads', woken) = wake (OnCTVar written) threads
-            in return $ Right (knows (map Right written) tid $ goto (c val) tid threads', idSource { _nextCTVId = newctvid }, STM woken, wb, caps)
-          | otherwise ->
-           return $ Right (knows (map Right written) tid $ goto (c val) tid threads, idSource { _nextCTVId = newctvid }, FreshSTM, wb, caps)
+        Success _ written val ->
+          let (threads', woken) = wake (OnTVar written) threads
+          in return $ Right (knows (map Right written) tid $ goto (c val) tid threads', idSource', STM trace woken, wb, caps)
         Retry touched ->
-          let threads' = block (OnCTVar touched) tid threads
-          in return $ Right (threads', idSource { _nextCTVId = newctvid }, BlockedSTM, wb, caps)
-        Exception e -> stepThrow e
+          let threads' = block (OnTVar touched) tid threads
+          in return $ Right (threads', idSource', BlockedSTM trace, wb, caps)
+        Exception e -> do
+          res' <- stepThrow e
+          return $ case res' of
+            Right (threads', _, _, _, _) -> Right (threads', idSource', Throw, wb, caps)
+            Left err -> Left err
 
     -- | Run a subcomputation in an exception-catching context.
     stepCatching h ma c = simple threads' Catching where
@@ -368,7 +362,7 @@
     -- | Throw an exception, and propagate it to the appropriate
     -- handler.
     stepThrow e =
-      case propagate (wrap e) tid threads of
+      case propagate (toException e) tid threads of
         Just threads' -> simple threads' Throw
         Nothing -> return $ Left UncaughtException
 
@@ -379,10 +373,10 @@
           blocked  = block (OnMask t) tid threads
       in case M.lookup t threads of
            Just thread
-             | interruptible thread -> case propagate (wrap e) t threads' of
+             | interruptible thread -> case propagate (toException e) t threads' of
                Just threads'' -> simple threads'' $ ThrowTo t
                Nothing
-                 | t == 0     -> return $ Left UncaughtException
+                 | t == initialThread -> return $ Left UncaughtException
                  | otherwise -> simple (kill t threads') $ ThrowTo t
              | otherwise -> simple blocked $ BlockedThrowTo t
            Nothing -> simple threads' $ ThrowTo t
@@ -407,22 +401,22 @@
       threads' = goto a tid (mask m tid threads)
 
     -- | Reset the masking thread of the state.
-    stepResetMask b1 b2 m c = simple threads' action where
-      action   = (if b1 then SetMasking else ResetMasking) b2 m
+    stepResetMask b1 b2 m c = simple threads' act where
+      act      = (if b1 then SetMasking else ResetMasking) b2 m
       threads' = goto c tid (mask m tid threads)
 
-    -- | Create a new @CVar@, using the next 'CVarId'.
-    stepNewVar c = do
-      let (idSource', newcvid) = nextCVId idSource
+    -- | Create a new @MVar@, using the next 'MVarId'.
+    stepNewVar n c = do
+      let (idSource', newcvid) = nextCVId n idSource
       ref <- newRef fixed Nothing
-      let cvar = CVar (newcvid, ref)
+      let cvar = MVar newcvid ref
       return $ Right (knows [Left newcvid] tid $ goto (c cvar) tid threads, idSource', NewVar newcvid, wb, caps)
 
     -- | Create a new @CRef@, using the next 'CRefId'.
-    stepNewRef a c = do
-      let (idSource', newcrid) = nextCRId idSource
+    stepNewRef n a c = do
+      let (idSource', newcrid) = nextCRId n idSource
       ref <- newRef fixed (M.empty, 0, a)
-      let cref = CRef (newcrid, ref)
+      let cref = CRef newcrid ref
       return $ Right (goto (c cref) tid threads, idSource', NewRef newcrid, wb, caps)
 
     -- | Lift an action from the underlying monad into the @Conc@
@@ -443,6 +437,9 @@
     -- | Record that all shared variables are known.
     stepAllKnown c = simple (fullknown tid $ goto c tid threads) AllKnown
 
+    -- | Add a message to the trace.
+    stepMessage m c = simple (goto c tid threads) (Message m)
+
     -- | Kill the current thread.
     stepStop = simple (kill tid threads) Stop
 
@@ -458,6 +455,3 @@
       return $ case res of
         Right (threads', idSource', act', _, caps') -> Right (threads', idSource', act', emptyBuffer, caps')
         _ -> res
-
-    -- | Helper function for wrapping up exceptions.
-    wrap e = fromMaybe (SomeException e) $ cast e
diff --git a/Test/DejaFu/Deterministic/Internal/Common.hs b/Test/DejaFu/Deterministic/Internal/Common.hs
--- a/Test/DejaFu/Deterministic/Internal/Common.hs
+++ b/Test/DejaFu/Deterministic/Internal/Common.hs
@@ -1,7 +1,5 @@
-{-# LANGUAGE CPP                        #-}
-{-# LANGUAGE ExistentialQuantification  #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE RankNTypes                 #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE RankNTypes                #-}
 
 -- | Common types and utility functions for deterministic execution of
 -- 'MonadConc' implementations.
@@ -9,19 +7,28 @@
 
 import Control.DeepSeq (NFData(..))
 import Control.Exception (Exception, MaskingState(..))
+import Data.Dynamic (Dynamic)
 import Data.Map.Strict (Map)
-import Data.List.Extra
+import Data.Maybe (mapMaybe)
+import Data.List (sort, nub, intercalate)
+import Data.List.NonEmpty (NonEmpty, fromList)
 import Test.DejaFu.Internal
-import Test.DejaFu.STM (CTVarId)
+import Test.DPOR (Decision(..), Trace)
 
-#if __GLASGOW_HASKELL__ < 710
-import Control.Applicative (Applicative(..))
-#endif
+{-# ANN module ("HLint: ignore Use record patterns" :: String) #-}
 
 --------------------------------------------------------------------------------
 -- * The @Conc@ Monad
 
--- | The underlying monad is based on continuations over Actions.
+-- | 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
+-- @Lift@ action as the penultimate action of thread 0 used to
+-- communicate back the result, and be more pleasing in a
+-- sense. 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.
 newtype M n r s a = M { runM :: (a -> Action n r s) -> Action n r s }
 
 instance Functor (M n r s) where
@@ -37,14 +44,14 @@
 
 -- | The concurrent variable type used with the 'Conc' monad. One
 -- notable difference between these and 'MVar's is that 'MVar's are
--- single-wakeup, and wake up in a FIFO order. Writing to a @CVar@
+-- 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 @CVar@ behaves
+-- scheduler which one runs next. Taking from a @MVar@ behaves
 -- analogously.
---
--- @CVar@s are represented as a unique numeric identifier, and a
--- reference containing a Maybe value.
-newtype CVar r a = CVar (CVarId, r (Maybe a))
+data MVar r a = MVar
+  { _cvarId   :: MVarId
+  , _cvarVal  :: r (Maybe a)
+  }
 
 -- | The mutable non-blocking reference type. These are like 'IORef's.
 --
@@ -53,7 +60,10 @@
 -- (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.
-newtype CRef r a = CRef (CRefId, r (Map ThreadId a, Integer, a))
+data CRef r a = CRef
+  { _crefId   :: CRefId
+  , _crefVal  :: r (Map ThreadId a, Integer, a)
+  }
 
 -- | The compare-and-swap proof type.
 --
@@ -62,7 +72,11 @@
 -- 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.
-newtype Ticket a = Ticket (CRefId, Integer, a)
+data Ticket a = Ticket
+  { _ticketCRef   :: CRefId
+  , _ticketWrites :: Integer
+  , _ticketVal    :: a
+  }
 
 -- | Dict of methods for implementations to override.
 type Fixed n r s = Ref n r (M n r s)
@@ -81,22 +95,22 @@
 -- | 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 'newEmptyCVar', 'fork', and 'putCVar'.
+-- implemented in terms of 'newEmptyMVar', 'fork', and 'putMVar'.
 data Action n r s =
-    AFork  ((forall b. M n r s b -> M n r s b) -> Action n r s) (ThreadId -> Action n r s)
+    AFork  String ((forall b. M n r s b -> M n r s b) -> Action n r s) (ThreadId -> Action n r s)
   | AMyTId (ThreadId -> Action n r s)
 
   | AGetNumCapabilities (Int -> Action n r s)
   | ASetNumCapabilities Int (Action n r s)
 
-  | forall a. ANewVar     (CVar r a -> Action n r s)
-  | forall a. APutVar     (CVar r a) a (Action n r s)
-  | forall a. ATryPutVar  (CVar r a) a (Bool -> Action n r s)
-  | forall a. AReadVar    (CVar r a) (a -> Action n r s)
-  | forall a. ATakeVar    (CVar r a) (a -> Action n r s)
-  | forall a. ATryTakeVar (CVar r a) (Maybe a -> Action n r s)
+  | forall a. ANewVar String (MVar r a -> Action n r s)
+  | forall a. APutVar     (MVar r a) a (Action n r s)
+  | forall a. ATryPutVar  (MVar r a) a (Bool -> Action n r s)
+  | forall a. AReadVar    (MVar r a) (a -> Action n r s)
+  | forall a. ATakeVar    (MVar r a) (a -> Action n r s)
+  | forall a. ATryTakeVar (MVar r a) (Maybe a -> Action n r s)
 
-  | forall a.   ANewRef a   (CRef r a -> Action n r s)
+  | forall a.   ANewRef String a (CRef r a -> Action n r s)
   | forall a.   AReadRef    (CRef r a) (a -> Action n r s)
   | forall a.   AReadRefCas (CRef r a) (Ticket a -> Action n r s)
   | forall a.   APeekTicket (Ticket a) (a -> Action n r s)
@@ -112,9 +126,10 @@
   | forall a. AMasking MaskingState ((forall b. M n r s b -> M n r s b) -> M n r s a) (a -> Action n r s)
   | AResetMask Bool Bool MaskingState (Action n r s)
 
-  | AKnowsAbout (Either CVarId CTVarId) (Action n r s)
-  | AForgets    (Either CVarId CTVarId) (Action n r s)
+  | AKnowsAbout (Either MVarId TVarId) (Action n r s)
+  | AForgets    (Either MVarId TVarId) (Action n r s)
   | AAllKnown   (Action n r s)
+  | AMessage    Dynamic (Action n r s)
 
   | forall a. AAtom (s a) (a -> Action n r s)
   | ALift (n (Action n r s))
@@ -127,117 +142,150 @@
 -- * Identifiers
 
 -- | Every live thread has a unique identitifer.
-newtype ThreadId = ThreadId Int
-  deriving (NFData, Enum, Eq, Ord, Num, Real, Integral)
+data ThreadId = ThreadId (Maybe String) Int
+  deriving Eq
 
+instance Ord ThreadId where
+  compare (ThreadId _ i) (ThreadId _ j) = compare i j
+
 instance Show ThreadId where
-  show (ThreadId i) = show i
+  show (ThreadId (Just n) _) = n
+  show (ThreadId Nothing  i) = show i
 
--- | Every 'CVar' has a unique identifier.
-newtype CVarId = CVarId Int
-  deriving (NFData, Enum, Eq, Ord, Num, Real, Integral)
+instance NFData ThreadId where
+  rnf (ThreadId n i) = rnf (n, i)
 
-instance Show CVarId where
-  show (CVarId i) = show i
+-- | The ID of the initial thread.
+initialThread :: ThreadId
+initialThread = ThreadId (Just "main") 0
 
--- | Every 'CRef' has a unique identifier.
-newtype CRefId = CRefId Int
-  deriving (NFData, Enum, Eq, Ord, Num, Real, Integral)
+-- | Every @MVar@ has a unique identifier.
+data MVarId = MVarId (Maybe String) Int
+  deriving Eq
 
+instance Ord MVarId where
+  compare (MVarId _ i) (MVarId _ j) = compare i j
+
+instance Show MVarId where
+  show (MVarId (Just n) _) = n
+  show (MVarId Nothing  i) = show i
+
+instance NFData MVarId where
+  rnf (MVarId n i) = rnf (n, i)
+
+-- | Every @CRef@ has a unique identifier.
+data CRefId = CRefId (Maybe String) Int
+  deriving Eq
+
+instance Ord CRefId where
+  compare (CRefId _ i) (CRefId _ j) = compare i j
+
 instance Show CRefId where
-  show (CRefId i) = show i
+  show (CRefId (Just n) _) = n
+  show (CRefId Nothing  i) = show i
 
+instance NFData CRefId where
+  rnf (CRefId n i) = rnf (n, i)
+
+-- | Every @TVar@ has a unique identifier.
+data TVarId = TVarId (Maybe String) Int
+  deriving Eq
+
+instance Ord TVarId where
+  compare (TVarId _ i) (TVarId _ j) = compare i j
+
+instance Show TVarId where
+  show (TVarId (Just n) _) = n
+  show (TVarId Nothing  i) = show i
+
+instance NFData TVarId where
+  rnf (TVarId n i) = rnf (n, i)
+
 -- | The number of ID parameters was getting a bit unwieldy, so this
 -- hides them all away.
-data IdSource = Id { _nextCRId :: CRefId, _nextCVId :: CVarId, _nextCTVId :: CTVarId, _nextTId :: ThreadId }
+data IdSource = Id
+  { _nextCRId  :: Int
+  , _nextCVId  :: Int
+  , _nextTVId  :: Int
+  , _nextTId   :: Int
+  , _usedCRNames :: [String]
+  , _usedCVNames :: [String]
+  , _usedTVNames :: [String]
+  , _usedTNames  :: [String] }
 
 -- | Get the next free 'CRefId'.
-nextCRId :: IdSource -> (IdSource, CRefId)
-nextCRId idsource = let newid = _nextCRId idsource + 1 in (idsource { _nextCRId = newid }, newid)
+nextCRId :: String -> IdSource -> (IdSource, CRefId)
+nextCRId name idsource = (idsource { _nextCRId = newid, _usedCRNames = newlst }, CRefId newname newid) where
+  newid  = _nextCRId idsource + 1
+  newlst
+    | null name = _usedCRNames idsource
+    | otherwise = name : _usedCRNames idsource
+  newname
+    | null name       = Nothing
+    | occurrences > 0 = Just (name ++ "-" ++ show occurrences)
+    | otherwise       = Just name
+  occurrences = length . filter (==name) $ _usedCRNames idsource
 
--- | Get the next free 'CVarId'.
-nextCVId :: IdSource -> (IdSource, CVarId)
-nextCVId idsource = let newid = _nextCVId idsource + 1 in (idsource { _nextCVId = newid }, newid)
+-- | Get the next free 'MVarId'.
+nextCVId :: String -> IdSource -> (IdSource, MVarId)
+nextCVId name idsource = (idsource { _nextCVId = newid, _usedCVNames = newlst }, MVarId newname newid) where
+  newid  = _nextCVId idsource + 1
+  newlst
+    | null name = _usedCVNames idsource
+    | otherwise = name : _usedCVNames idsource
+  newname
+    | null name       = Nothing
+    | occurrences > 0 = Just (name ++ "-" ++ show occurrences)
+    | otherwise       = Just name
+  occurrences = length . filter (==name) $ _usedCVNames idsource
 
--- | Get the next free 'CTVarId'.
-nextCTVId :: IdSource -> (IdSource, CTVarId)
-nextCTVId idsource = let newid = _nextCTVId idsource + 1 in (idsource { _nextCTVId = newid }, newid)
+-- | Get the next free 'TVarId'.
+nextTVId :: String -> IdSource -> (IdSource, TVarId)
+nextTVId name idsource = (idsource { _nextTVId = newid, _usedTVNames = newlst }, TVarId newname newid) where
+  newid  = _nextTVId idsource + 1
+  newlst
+    | null name = _usedTVNames idsource
+    | otherwise = name : _usedTVNames idsource
+  newname
+    | null name       = Nothing
+    | occurrences > 0 = Just (name ++ "-" ++ show occurrences)
+    | otherwise       = Just name
+  occurrences = length . filter (==name) $ _usedTVNames idsource
 
 -- | Get the next free 'ThreadId'.
-nextTId :: IdSource -> (IdSource, ThreadId)
-nextTId idsource = let newid = _nextTId idsource + 1 in (idsource { _nextTId = newid }, newid)
+nextTId :: String -> IdSource -> (IdSource, ThreadId)
+nextTId name idsource = (idsource { _nextTId = newid, _usedTNames = newlst }, ThreadId newname newid) where
+  newid  = _nextTId idsource + 1
+  newlst
+    | null name = _usedTNames idsource
+    | otherwise = name : _usedTNames idsource
+  newname
+    | null name       = Nothing
+    | occurrences > 0 = Just (name ++ "-" ++ show occurrences)
+    | otherwise       = Just name
+  occurrences = length . filter (==name) $ _usedTNames idsource
 
 -- | The initial ID source.
 initialIdSource :: IdSource
-initialIdSource = Id 0 0 0 0
+initialIdSource = Id 0 0 0 0 [] [] [] []
 
 --------------------------------------------------------------------------------
 -- * Scheduling & Traces
 
--- | A @Scheduler@ maintains some internal state; @s@, takes the trace
--- so far; the 'ThreadId' and 'ThreadAction' of the last thread
--- scheduled (or 'Nothing' if this is the first decision); and the
--- list of runnable threads including a lookahead (as far as can be
--- determined). It produces a 'ThreadId' to schedule, and a new state.
---
--- __Note:__ In order to prevent computation from hanging, the runtime
--- will assume that a deadlock situation has arisen if the scheduler
--- attempts to (a) schedule a blocked thread, or (b) schedule a
--- nonexistent thread. In either of those cases, the computation will
--- be halted.
-type Scheduler s = s -> [(Decision, ThreadAction)] -> Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, NonEmpty Lookahead) -> (Maybe ThreadId, s)
-
--- | One of the outputs of the runner is a @Trace@, which is a log of
--- decisions made, alternative decisions (including what action would
--- have been performed had that decision been taken), and the action a
--- thread took in its step.
-type Trace = [(Decision, [(Decision, Lookahead)], ThreadAction)]
-
--- | Like a 'Trace', but gives more lookahead (where possible) for
--- alternative decisions.
-type Trace' = [(Decision, [(Decision, NonEmpty Lookahead)], ThreadAction)]
-
--- | Throw away information from a 'Trace'' to get just a 'Trace'.
-toTrace :: Trace' -> Trace
-toTrace = map go where
-  go (_, alters, CommitRef t c) = (Commit, goA alters, CommitRef t c)
-  go (dec, alters, act) = (dec, goA alters, act)
-
-  goA = map $ \x -> case x of
-    (_, WillCommitRef t c:|_) -> (Commit, WillCommitRef t c)
-    (d, a:|_) -> (d, a)
-
--- | Pretty-print a trace.
-showTrace :: Trace -> String
-showTrace = trace "" 0 where
-  trace prefix num ((Start tid,_,_):ds)    = thread prefix num ++ trace ("S" ++ show tid) 1 ds
-  trace prefix num ((SwitchTo tid,_,_):ds) = thread prefix num ++ trace ("P" ++ show tid) 1 ds
-  trace prefix num ((Continue,_,_):ds)     = trace prefix (num + 1) ds
-  trace prefix num ((Commit,_,_):ds)       = thread prefix num ++ trace "C" 1 ds
-  trace prefix num []                      = thread prefix num
+-- | Pretty-print a trace, including a key of the thread IDs. Each
+-- line of the key is indented by two spaces.
+showTrace :: Trace ThreadId ThreadAction Lookahead -> String
+showTrace trc = intercalate "\n" $ trace "" 0 trc : (map ("  "++) . sort . nub $ mapMaybe toKey trc) where
+  trace prefix num ((_,_,CommitRef _ _):ds) = thread prefix num ++ trace "C" 1 ds
+  trace prefix num ((Start    (ThreadId _ i),_,_):ds) = thread prefix num ++ trace ("S" ++ show i) 1 ds
+  trace prefix num ((SwitchTo (ThreadId _ i),_,_):ds) = thread prefix num ++ trace ("P" ++ show i) 1 ds
+  trace prefix num ((Continue,_,_):ds) = trace prefix (num + 1) ds
+  trace prefix num [] = thread prefix num
 
   thread prefix num = prefix ++ replicate num '-'
 
--- | Scheduling decisions are based on the state of the running
--- program, and so we can capture some of that state in recording what
--- specific decision we made.
-data Decision =
-    Start ThreadId
-  -- ^ Start a new thread, because the last was blocked (or it's the
-  -- start of computation).
-  | Continue
-  -- ^ Continue running the last thread for another step.
-  | SwitchTo ThreadId
-  -- ^ Pre-empt the running thread, and switch to another.
-  | Commit
-  -- ^ Commit a 'CRef' write action so that every thread can see the
-  -- result.
-  deriving (Eq, Show)
-
-instance NFData Decision where
-  rnf (Start    tid) = rnf tid
-  rnf (SwitchTo tid) = rnf tid
-  rnf d = d `seq` ()
+  toKey (Start (ThreadId (Just name) i), _, _) = Just $ show i ++ ": " ++ name
+  toKey _ = Nothing
 
 -- | All the actions that a thread can perform.
 data ThreadAction =
@@ -251,24 +299,24 @@
   -- ^ Set the number of Haskell threads that can run simultaneously.
   | Yield
   -- ^ Yield the current thread.
-  | NewVar CVarId
-  -- ^ Create a new 'CVar'.
-  | PutVar CVarId [ThreadId]
-  -- ^ Put into a 'CVar', possibly waking up some threads.
-  | BlockedPutVar CVarId
+  | NewVar MVarId
+  -- ^ Create a new 'MVar'.
+  | PutVar MVarId [ThreadId]
+  -- ^ Put into a 'MVar', possibly waking up some threads.
+  | BlockedPutVar MVarId
   -- ^ Get blocked on a put.
-  | TryPutVar CVarId Bool [ThreadId]
-  -- ^ Try to put into a 'CVar', possibly waking up some threads.
-  | ReadVar CVarId
-  -- ^ Read from a 'CVar'.
-  | BlockedReadVar CVarId
+  | TryPutVar MVarId Bool [ThreadId]
+  -- ^ Try to put into a 'MVar', possibly waking up some threads.
+  | ReadVar MVarId
+  -- ^ Read from a 'MVar'.
+  | BlockedReadVar MVarId
   -- ^ Get blocked on a read.
-  | TakeVar CVarId [ThreadId]
-  -- ^ Take from a 'CVar', possibly waking up some threads.
-  | BlockedTakeVar CVarId
+  | TakeVar MVarId [ThreadId]
+  -- ^ Take from a 'MVar', possibly waking up some threads.
+  | BlockedTakeVar MVarId
   -- ^ Get blocked on a take.
-  | TryTakeVar CVarId Bool [ThreadId]
-  -- ^ Try to take from a 'CVar', possibly waking up some threads.
+  | TryTakeVar MVarId Bool [ThreadId]
+  -- ^ Try to take from a 'MVar', possibly waking up some threads.
   | NewRef CRefId
   -- ^ Create a new 'CRef'.
   | ReadRef CRefId
@@ -289,13 +337,10 @@
   | CommitRef ThreadId CRefId
   -- ^ Commit the last write to the given 'CRef' by the given thread,
   -- so that all threads can see the updated value.
-  | STM [ThreadId]
+  | STM TTrace [ThreadId]
   -- ^ An STM transaction was executed, possibly waking up some
   -- threads.
-  | FreshSTM
-  -- ^ An STM transaction was executed, and all it did was create and
-  -- write to new 'CTVar's, no existing 'CTVar's were touched.
-  | BlockedSTM
+  | BlockedSTM TTrace
   -- ^ Got blocked in an STM transaction.
   | Catching
   -- ^ Register a new exception handler
@@ -329,9 +374,11 @@
   -- ^ A '_concForgets' annotation was processed.
   | AllKnown
   -- ^ A '_concALlKnown' annotation was processed.
+  | Message Dynamic
+  -- ^ A '_concMessage' annotation was processed.
   | Stop
   -- ^ Cease execution and terminate.
-  deriving (Eq, Show)
+  deriving Show
 
 instance NFData ThreadAction where
   rnf (Fork t) = rnf t
@@ -355,13 +402,63 @@
   rnf (WriteRef c) = rnf c
   rnf (CasRef c b) = rnf (c, b)
   rnf (CommitRef t c) = rnf (t, c)
-  rnf (STM ts) = rnf ts
+  rnf (STM s ts) = rnf (s, ts)
+  rnf (BlockedSTM s) = rnf s
   rnf (ThrowTo t) = rnf t
   rnf (BlockedThrowTo t) = rnf t
   rnf (SetMasking b m) = b `seq` m `seq` ()
   rnf (ResetMasking b m) = b `seq` m `seq` ()
+  rnf (Message m) = m `seq` ()
   rnf a = a `seq` ()
 
+-- | Check if a @ThreadAction@ immediately blocks.
+isBlock :: ThreadAction -> Bool
+isBlock (BlockedThrowTo  _) = True
+isBlock (BlockedTakeVar _) = True
+isBlock (BlockedReadVar _) = True
+isBlock (BlockedPutVar  _) = True
+isBlock (BlockedSTM _) = True
+isBlock _ = False
+
+-- | A trace of an STM transaction is just a list of actions that
+-- occurred, as there are no scheduling decisions to make.
+type TTrace = [TAction]
+
+-- | All the actions that an STM transaction can perform.
+data TAction =
+    TNew
+  -- ^ Create a new @TVar@
+  | TRead  TVarId
+  -- ^ Read from a @TVar@.
+  | TWrite TVarId
+  -- ^ Write to a @TVar@.
+  | TRetry
+  -- ^ Abort and discard effects.
+  | TOrElse TTrace (Maybe TTrace)
+  -- ^ Execute a transaction until it succeeds (@STMStop@) or aborts
+  -- (@STMRetry@) and, if it aborts, execute the other transaction.
+  | TThrow
+  -- ^ Throw an exception, abort, and discard effects.
+  | TCatch TTrace (Maybe TTrace)
+  -- ^ Execute a transaction until it succeeds (@STMStop@) or aborts
+  -- (@STMThrow@). If the exception is of the appropriate type, it is
+  -- handled and execution continues; otherwise aborts, propagating
+  -- the exception upwards.
+  | TStop
+  -- ^ Terminate successfully and commit effects.
+  | TLift
+  -- ^ Lifts an action from the underlying monad. Note that the
+  -- penultimate action in a trace will always be a @Lift@, this is an
+  -- artefact of how the runner works.
+  deriving (Eq, Show)
+
+instance NFData TAction where
+  rnf (TRead  v) = rnf v
+  rnf (TWrite v) = rnf v
+  rnf (TCatch  s m) = rnf (s, m)
+  rnf (TOrElse s m) = rnf (s, m)
+  rnf a = a `seq` ()
+
 -- | A one-step look-ahead at what a thread will do next.
 data Lookahead =
     WillFork
@@ -377,17 +474,17 @@
   | WillYield
   -- ^ Will yield the current thread.
   | WillNewVar
-  -- ^ Will create a new 'CVar'.
-  | WillPutVar CVarId
-  -- ^ Will put into a 'CVar', possibly waking up some threads.
-  | WillTryPutVar CVarId
-  -- ^ Will try to put into a 'CVar', possibly waking up some threads.
-  | WillReadVar CVarId
-  -- ^ Will read from a 'CVar'.
-  | WillTakeVar CVarId
-  -- ^ Will take from a 'CVar', possibly waking up some threads.
-  | WillTryTakeVar CVarId
-  -- ^ Will try to take from a 'CVar', possibly waking up some threads.
+  -- ^ Will create a new 'MVar'.
+  | WillPutVar MVarId
+  -- ^ Will put into a 'MVar', possibly waking up some threads.
+  | WillTryPutVar MVarId
+  -- ^ Will try to put into a 'MVar', possibly waking up some threads.
+  | WillReadVar MVarId
+  -- ^ Will read from a 'MVar'.
+  | WillTakeVar MVarId
+  -- ^ Will take from a 'MVar', possibly waking up some threads.
+  | WillTryTakeVar MVarId
+  -- ^ Will try to take from a 'MVar', possibly waking up some threads.
   | WillNewRef
   -- ^ Will create a new 'CRef'.
   | WillReadRef CRefId
@@ -438,9 +535,11 @@
   -- ^ Will process a '_concForgets' annotation.
   | WillAllKnown
   -- ^ Will process a '_concALlKnown' annotation.
+  | WillMessage Dynamic
+  -- ^ Will process a _concMessage' annotation.
   | WillStop
   -- ^ Will cease execution and terminate.
-  deriving (Eq, Show)
+  deriving Show
 
 instance NFData Lookahead where
   rnf (WillSetNumCapabilities i) = rnf i
@@ -460,29 +559,30 @@
   rnf (WillThrowTo t) = rnf t
   rnf (WillSetMasking b m) = b `seq` m `seq` ()
   rnf (WillResetMasking b m) = b `seq` m `seq` ()
+  rnf (WillMessage m) = m `seq` ()
   rnf l = l `seq` ()
 
 -- | Look as far ahead in the given continuation as possible.
 lookahead :: Action n r s -> NonEmpty Lookahead
-lookahead = unsafeToNonEmpty . lookahead' where
-  lookahead' (AFork _ _)             = [WillFork]
+lookahead = fromList . lookahead' where
+  lookahead' (AFork _ _ _)           = [WillFork]
   lookahead' (AMyTId _)              = [WillMyThreadId]
   lookahead' (AGetNumCapabilities _) = [WillGetNumCapabilities]
   lookahead' (ASetNumCapabilities i k) = WillSetNumCapabilities i : lookahead' k
-  lookahead' (ANewVar _)             = [WillNewVar]
-  lookahead' (APutVar (CVar (c, _)) _ k)    = WillPutVar c : lookahead' k
-  lookahead' (ATryPutVar (CVar (c, _)) _ _) = [WillTryPutVar c]
-  lookahead' (AReadVar (CVar (c, _)) _)     = [WillReadVar c]
-  lookahead' (ATakeVar (CVar (c, _)) _)     = [WillTakeVar c]
-  lookahead' (ATryTakeVar (CVar (c, _)) _)  = [WillTryTakeVar c]
-  lookahead' (ANewRef _ _)           = [WillNewRef]
-  lookahead' (AReadRef (CRef (r, _)) _)     = [WillReadRef r]
-  lookahead' (AReadRefCas (CRef (r, _)) _)  = [WillReadRefCas r]
-  lookahead' (APeekTicket (Ticket (r, _, _)) _) = [WillPeekTicket r]
-  lookahead' (AModRef (CRef (r, _)) _ _)    = [WillModRef r]
-  lookahead' (AModRefCas (CRef (r, _)) _ _) = [WillModRefCas r]
-  lookahead' (AWriteRef (CRef (r, _)) _ k) = WillWriteRef r : lookahead' k
-  lookahead' (ACasRef (CRef (r, _)) _ _ _) = [WillCasRef r]
+  lookahead' (ANewVar _ _)           = [WillNewVar]
+  lookahead' (APutVar (MVar c _) _ k)    = WillPutVar c : lookahead' k
+  lookahead' (ATryPutVar (MVar c _) _ _) = [WillTryPutVar c]
+  lookahead' (AReadVar (MVar c _) _)     = [WillReadVar c]
+  lookahead' (ATakeVar (MVar c _) _)     = [WillTakeVar c]
+  lookahead' (ATryTakeVar (MVar c _) _)  = [WillTryTakeVar c]
+  lookahead' (ANewRef _ _ _)         = [WillNewRef]
+  lookahead' (AReadRef (CRef r _) _)     = [WillReadRef r]
+  lookahead' (AReadRefCas (CRef r _) _)  = [WillReadRefCas r]
+  lookahead' (APeekTicket (Ticket r _ _) _) = [WillPeekTicket r]
+  lookahead' (AModRef (CRef r _) _ _)    = [WillModRef r]
+  lookahead' (AModRefCas (CRef r _) _ _) = [WillModRefCas r]
+  lookahead' (AWriteRef (CRef r _) _ k) = WillWriteRef r : lookahead' k
+  lookahead' (ACasRef (CRef r _) _ _ _) = [WillCasRef r]
   lookahead' (ACommit t c)           = [WillCommitRef t c]
   lookahead' (AAtom _ _)             = [WillSTM]
   lookahead' (AThrow _)              = [WillThrow]
@@ -495,6 +595,7 @@
   lookahead' (AKnowsAbout _ k)       = WillKnowsAbout : lookahead' k
   lookahead' (AForgets _ k)          = WillForgets : lookahead' k
   lookahead' (AAllKnown k)           = WillAllKnown : lookahead' k
+  lookahead' (AMessage m k)          = WillMessage m : lookahead' k
   lookahead' (AYield k)              = WillYield : lookahead' k
   lookahead' (AReturn k)             = WillReturn : lookahead' k
   lookahead' AStop                   = [WillStop]
@@ -515,6 +616,16 @@
 willRelease WillStop = True
 willRelease _ = False
 
+-- Count the number of pre-emptions in a schedule prefix.
+preEmpCount :: [(Decision ThreadId, ThreadAction)] -> (Decision ThreadId, Lookahead) -> Int
+preEmpCount ts (d, _) = go Nothing ts where
+  go p ((d', a):rest) = preEmpC p d' + go (Just a) rest
+  go p [] = preEmpC p d
+
+  preEmpC (Just Yield) (SwitchTo _) = 0
+  preEmpC _ (SwitchTo t) = if t >= initialThread then 1 else 0
+  preEmpC _ _ = 0
+
 -- | A simplified view of the possible actions a thread can perform.
 data ActionType =
     UnsynchronisedRead  CRefId
@@ -532,10 +643,10 @@
   -- ^ A 'modifyCRefCAS'
   | SynchronisedModify  CRefId
   -- ^ An 'atomicModifyCRef'.
-  | SynchronisedRead    CVarId
-  -- ^ A 'readCVar' or 'takeCVar' (or @try@/@blocked@ variants).
-  | SynchronisedWrite   CVarId
-  -- ^ A 'putCVar' (or @try@/@blocked@ variant).
+  | SynchronisedRead    MVarId
+  -- ^ A 'readMVar' or 'takeMVar' (or @try@/@blocked@ variants).
+  | SynchronisedWrite   MVarId
+  -- ^ A 'putMVar' (or @try@/@blocked@ variant).
   | SynchronisedOther
   -- ^ Some other action which does require cross-thread
   -- communication.
@@ -560,12 +671,16 @@
 isBarrier SynchronisedOther = True
 isBarrier _ = False
 
--- | Check if an action is synchronises a given 'CRef'.
+-- | Check if an action commits a given 'CRef'.
+isCommit :: ActionType -> CRefId -> Bool
+isCommit (PartiallySynchronisedCommit c) r = c == r
+isCommit (PartiallySynchronisedWrite  c) r = c == r
+isCommit (PartiallySynchronisedModify c) r = c == r
+isCommit _ _ = False
+
+-- | Check if an action synchronises a given 'CRef'.
 synchronises :: ActionType -> CRefId -> Bool
-synchronises (PartiallySynchronisedCommit c) r = c == r
-synchronises (PartiallySynchronisedWrite  c) r = c == r
-synchronises (PartiallySynchronisedModify c) r = c == r
-synchronises a _ = isBarrier a
+synchronises a r = isCommit a r || isBarrier a
 
 -- | Get the 'CRef' affected.
 crefOf :: ActionType -> Maybe CRefId
@@ -577,8 +692,8 @@
 crefOf (PartiallySynchronisedModify r) = Just r
 crefOf _ = Nothing
 
--- | Get the 'CVar' affected.
-cvarOf :: ActionType -> Maybe CVarId
+-- | Get the 'MVar' affected.
+cvarOf :: ActionType -> Maybe MVarId
 cvarOf (SynchronisedRead  c) = Just c
 cvarOf (SynchronisedWrite c) = Just c
 cvarOf _ = Nothing
@@ -604,8 +719,8 @@
 simplify (WriteRef r)    = UnsynchronisedWrite r
 simplify (CasRef r _)    = PartiallySynchronisedWrite r
 simplify (CommitRef _ r) = PartiallySynchronisedCommit r
-simplify (STM _)            = SynchronisedOther
-simplify BlockedSTM         = SynchronisedOther
+simplify (STM _ _)          = SynchronisedOther
+simplify (BlockedSTM _)     = SynchronisedOther
 simplify (ThrowTo _)        = SynchronisedOther
 simplify (BlockedThrowTo _) = SynchronisedOther
 simplify _ = UnsynchronisedOther
@@ -643,9 +758,9 @@
   -- bounds (there have been too many pre-emptions, the computation
   -- has executed for too long, or there have been too many yields).
   | Deadlock
-  -- ^ The computation became blocked indefinitely on @CVar@s.
+  -- ^ The computation became blocked indefinitely on @MVar@s.
   | STMDeadlock
-  -- ^ The computation became blocked indefinitely on @CTVar@s.
+  -- ^ The computation became blocked indefinitely on @TVar@s.
   | UncaughtException
   -- ^ An uncaught exception bubbled to the top of the computation.
   deriving (Eq, Show, Read, Ord, Enum, Bounded)
diff --git a/Test/DejaFu/Deterministic/Internal/Memory.hs b/Test/DejaFu/Deterministic/Internal/Memory.hs
--- a/Test/DejaFu/Deterministic/Internal/Memory.hs
+++ b/Test/DejaFu/Deterministic/Internal/Memory.hs
@@ -1,12 +1,20 @@
 {-# LANGUAGE BangPatterns #-}
-{-# LANGUAGE CPP          #-}
 {-# LANGUAGE GADTs        #-}
 
--- | Operations over @CRef@s and @CVar@s
+-- | Operations over @CRef@s and @MVar@s
+--
+-- Relaxed memory operations over @CRef@s are implemented with an
+-- explicit write buffer: one per thread for TSO, and one per
+-- thread/variable combination for PSO. Unsynchronised writes append
+-- to this buffer, and periodically separate threads commit from these
+-- buffers to the \"actual\" @CRef@.
+--
+-- This model comes from /Dynamic Partial Order Reduction for Relaxed
+-- Memory Models/, N. Zhang, M. Kusano, and C. Wang (2015).
 module Test.DejaFu.Deterministic.Internal.Memory where
 
 import Control.Monad (when)
-import Data.IntMap.Strict (IntMap)
+import Data.Map.Strict (Map)
 import Data.Maybe (isJust, fromJust)
 import Data.Monoid ((<>))
 import Data.Sequence (Seq, ViewL(..), (><), singleton, viewl)
@@ -14,22 +22,18 @@
 import Test.DejaFu.Deterministic.Internal.Threading
 import Test.DejaFu.Internal
 
-import qualified Data.IntMap.Strict as I
 import qualified Data.Map.Strict as M
 
-#if __GLASGOW_HASKELL__ < 710
-import Data.Foldable (mapM_)
-import Prelude hiding (mapM_)
-#endif
-
 --------------------------------------------------------------------------------
 -- * Manipulating @CRef@s
 
 -- | In non-sequentially-consistent memory models, non-synchronised
 -- writes get buffered.
 --
--- In TSO, the keys are @ThreadId@s. In PSO, the keys are @CRefId@s.
-newtype WriteBuffer r = WriteBuffer { buffer :: IntMap (Seq (BufferedWrite r)) }
+-- The @CRefId@ parameter is only used under PSO. Under TSO each
+-- thread has a single buffer.
+newtype WriteBuffer r = WriteBuffer
+  { buffer :: Map (ThreadId, Maybe CRefId) (Seq (BufferedWrite r)) }
 
 -- | A buffered write is a reference to the variable, and the value to
 -- write. Universally quantified over the value type so that the only
@@ -39,28 +43,28 @@
 
 -- | An empty write buffer.
 emptyBuffer :: WriteBuffer r
-emptyBuffer = WriteBuffer I.empty
+emptyBuffer = WriteBuffer M.empty
 
 -- | Add a new write to the end of a buffer.
-bufferWrite :: Monad n => Fixed n r s -> WriteBuffer r -> Int -> CRef r a -> a -> ThreadId -> n (WriteBuffer r)
-bufferWrite fixed (WriteBuffer wb) i cref@(CRef (_, ref)) new tid = do
+bufferWrite :: Monad n => Fixed n r s -> WriteBuffer r -> (ThreadId, Maybe CRefId) -> CRef r a -> a -> n (WriteBuffer r)
+bufferWrite fixed (WriteBuffer wb) k@(tid, _) cref@(CRef _ ref) new = do
   -- Construct the new write buffer
   let write = singleton $ BufferedWrite tid cref new
-  let buffer' = I.insertWith (><) i write wb
+  let buffer' = M.insertWith (flip (><)) k write wb
 
   -- Write the thread-local value to the @CRef@'s update map.
-  (map, count, def) <- readRef fixed ref
-  writeRef fixed ref (M.insert tid new map, count, def)
+  (locals, count, def) <- readRef fixed ref
+  writeRef fixed ref (M.insert tid new locals, count, def)
 
   return $ WriteBuffer buffer'
 
 -- | Commit the write at the head of a buffer.
-commitWrite :: Monad n => Fixed n r s -> WriteBuffer r -> Int -> n (WriteBuffer r)
-commitWrite fixed w@(WriteBuffer wb) i = case maybe EmptyL viewl $ I.lookup i wb of
+commitWrite :: Monad n => Fixed n r s -> WriteBuffer r -> (ThreadId, Maybe CRefId) -> n (WriteBuffer r)
+commitWrite fixed w@(WriteBuffer wb) k = case maybe EmptyL viewl $ M.lookup k wb of
   BufferedWrite _ cref a :< rest -> do
     writeImmediate fixed cref a
-    return . WriteBuffer $ I.insert i rest wb
-    
+    return . WriteBuffer $ M.insert k rest wb
+
   EmptyL -> return w
 
 -- | Read from a @CRef@, returning a newer thread-local non-committed
@@ -73,15 +77,15 @@
 -- | Read from a @CRef@, returning a @Ticket@ representing the current
 -- view of the thread.
 readForTicket :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n (Ticket a)
-readForTicket fixed cref@(CRef (crid, _)) tid = do
+readForTicket fixed cref@(CRef crid _) tid = do
   (val, count) <- readCRefPrim fixed cref tid
-  return $ Ticket (crid, count, val)
+  return $ Ticket crid count val
 
 -- | Perform a compare-and-swap on a @CRef@ if the ticket is still
 -- valid. This is strict in the \"new\" value argument.
 casCRef :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> Ticket a -> a -> n (Bool, Ticket a)
-casCRef fixed cref tid (Ticket (_, cc, _)) !new = do
-  tick'@(Ticket (_, cc', _)) <- readForTicket fixed cref tid
+casCRef fixed cref tid (Ticket _ cc _) !new = do
+  tick'@(Ticket _ cc' _) <- readForTicket fixed cref tid
 
   if cc == cc'
   then do
@@ -92,7 +96,7 @@
 
 -- | Read the local state of a @CRef@.
 readCRefPrim :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n (a, Integer)
-readCRefPrim fixed (CRef (_, ref)) tid = do
+readCRefPrim fixed (CRef _ ref) tid = do
   (vals, count, def) <- readRef fixed ref
 
   return (M.findWithDefault def tid vals, count)
@@ -100,65 +104,68 @@
 -- | Write and commit to a @CRef@ immediately, clearing the update map
 -- and incrementing the write count.
 writeImmediate :: Monad n => Fixed n r s -> CRef r a -> a -> n ()
-writeImmediate fixed (CRef (_, ref)) a = do
+writeImmediate fixed (CRef _ ref) a = do
   (_, count, _) <- readRef fixed ref
   writeRef fixed ref (M.empty, count + 1, a)
 
 -- | Flush all writes in the buffer.
 writeBarrier :: Monad n => Fixed n r s -> WriteBuffer r -> n ()
-writeBarrier fixed (WriteBuffer wb) = mapM_ flush $ I.elems wb where
+writeBarrier fixed (WriteBuffer wb) = mapM_ flush $ M.elems wb where
   flush = mapM_ $ \(BufferedWrite _ cref a) -> writeImmediate fixed cref a
 
 -- | Add phantom threads to the thread list to commit pending writes.
 addCommitThreads :: WriteBuffer r -> Threads n r s -> Threads n r s
 addCommitThreads (WriteBuffer wb) ts = ts <> M.fromList phantoms where
-  phantoms = [(ThreadId $ negate k - 1, mkthread $ fromJust c) | (k, b) <- I.toList wb, let c = go $ viewl b, isJust c]
-  go (BufferedWrite tid (CRef (crid, _)) _ :< _) = Just $ ACommit tid crid
+  phantoms = [ (ThreadId Nothing $ negate tid, mkthread $ fromJust c)
+             | ((k, b), tid) <- zip (M.toList wb) [1..]
+             , let c = go $ viewl b
+             , isJust c]
+  go (BufferedWrite tid (CRef crid _) _ :< _) = Just $ ACommit tid crid
   go EmptyL = Nothing
 
 -- | Remove phantom threads.
 delCommitThreads :: Threads n r s -> Threads n r s
-delCommitThreads = M.filterWithKey $ \k _ -> k >= 0
+delCommitThreads = M.filterWithKey $ \k _ -> k >= initialThread
 
 --------------------------------------------------------------------------------
--- * Manipulating @CVar@s
+-- * Manipulating @MVar@s
 
--- | Put into a @CVar@, blocking if full.
-putIntoCVar :: Monad n => CVar r a -> a -> Action n r s
+-- | Put into a @MVar@, blocking if full.
+putIntoMVar :: Monad n => MVar r a -> a -> Action n r s
              -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
-putIntoCVar cvar a c = mutCVar True cvar a (const c)
+putIntoMVar cvar a c = mutMVar True cvar a (const c)
 
--- | Try to put into a @CVar@, not blocking if full.
-tryPutIntoCVar :: Monad n => CVar r a -> a -> (Bool -> Action n r s)
+-- | Try to put into a @MVar@, not blocking if full.
+tryPutIntoMVar :: Monad n => MVar r a -> a -> (Bool -> Action n r s)
                  -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
-tryPutIntoCVar = mutCVar False
+tryPutIntoMVar = mutMVar False
 
--- | Read from a @CVar@, blocking if empty.
-readFromCVar :: Monad n => CVar r a -> (a -> Action n r s)
+-- | Read from a @MVar@, blocking if empty.
+readFromMVar :: Monad n => MVar r a -> (a -> Action n r s)
               -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
-readFromCVar cvar c = seeCVar False True cvar (c . fromJust)
+readFromMVar cvar c = seeMVar False True cvar (c . fromJust)
 
--- | Take from a @CVar@, blocking if empty.
-takeFromCVar :: Monad n => CVar r a -> (a -> Action n r s)
+-- | Take from a @MVar@, blocking if empty.
+takeFromMVar :: Monad n => MVar r a -> (a -> Action n r s)
               -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
-takeFromCVar cvar c = seeCVar True True cvar (c . fromJust)
+takeFromMVar cvar c = seeMVar True True cvar (c . fromJust)
 
--- | Try to take from a @CVar@, not blocking if empty.
-tryTakeFromCVar :: Monad n => CVar r a -> (Maybe a -> Action n r s)
+-- | Try to take from a @MVar@, not blocking if empty.
+tryTakeFromMVar :: Monad n => MVar r a -> (Maybe a -> Action n r s)
                   -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
-tryTakeFromCVar = seeCVar True False
+tryTakeFromMVar = seeMVar True False
 
--- | Mutate a @CVar@, in either a blocking or nonblocking way.
-mutCVar :: Monad n
-         => Bool -> CVar r a -> a -> (Bool -> Action n r s)
+-- | Mutate a @MVar@, in either a blocking or nonblocking way.
+mutMVar :: Monad n
+         => Bool -> MVar r a -> a -> (Bool -> Action n r s)
          -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
-mutCVar blocking (CVar (cvid, ref)) a c fixed threadid threads = do
+mutMVar blocking (MVar cvid ref) a c fixed threadid threads = do
   val <- readRef fixed ref
 
   case val of
     Just _
       | blocking ->
-        let threads' = block (OnCVarEmpty cvid) threadid threads
+        let threads' = block (OnMVarEmpty cvid) threadid threads
         in return (False, threads', [])
 
       | otherwise ->
@@ -166,26 +173,26 @@
 
     Nothing -> do
       writeRef fixed ref $ Just a
-      let (threads', woken) = wake (OnCVarFull cvid) threads
+      let (threads', woken) = wake (OnMVarFull cvid) threads
       return (True, goto (c True) threadid threads', woken)
 
--- | Read a @CVar@, in either a blocking or nonblocking
+-- | Read a @MVar@, in either a blocking or nonblocking
 -- way.
-seeCVar :: Monad n
-         => Bool -> Bool -> CVar r a -> (Maybe a -> Action n r s)
+seeMVar :: Monad n
+         => Bool -> Bool -> MVar r a -> (Maybe a -> Action n r s)
          -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
-seeCVar emptying blocking (CVar (cvid, ref)) c fixed threadid threads = do
+seeMVar emptying blocking (MVar cvid ref) c fixed threadid threads = do
   val <- readRef fixed ref
 
   case val of
     Just _ -> do
       when emptying $ writeRef fixed ref Nothing
-      let (threads', woken) = wake (OnCVarEmpty cvid) threads
+      let (threads', woken) = wake (OnMVarEmpty cvid) threads
       return (True, goto (c val) threadid threads', woken)
 
     Nothing
       | blocking ->
-        let threads' = block (OnCVarFull cvid) threadid threads
+        let threads' = block (OnMVarFull cvid) threadid threads
         in return (False, threads', [])
 
       | otherwise ->
diff --git a/Test/DejaFu/Deterministic/Internal/Threading.hs b/Test/DejaFu/Deterministic/Internal/Threading.hs
--- a/Test/DejaFu/Deterministic/Internal/Threading.hs
+++ b/Test/DejaFu/Deterministic/Internal/Threading.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE CPP                       #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE RankNTypes                #-}
 
@@ -9,15 +8,10 @@
 import Data.List (intersect, nub)
 import Data.Map.Strict (Map)
 import Data.Maybe (fromMaybe, isJust, isNothing)
-import Test.DejaFu.STM (CTVarId)
 import Test.DejaFu.Deterministic.Internal.Common
 
 import qualified Data.Map.Strict as M
 
-#if __GLASGOW_HASKELL__ < 710
-import Control.Applicative ((<$>))
-#endif
-
 --------------------------------------------------------------------------------
 -- * Threads
 
@@ -34,7 +28,7 @@
   -- ^ Stack of exception handlers
   , _masking      :: MaskingState
   -- ^ The exception masking state.
-  , _known        :: [Either CVarId CTVarId]
+  , _known        :: [Either MVarId TVarId]
   -- ^ Shared variables the thread knows about.
   , _fullknown    :: Bool
   -- ^ Whether the referenced variables of the thread are completely
@@ -51,14 +45,14 @@
 
 -- | A @BlockedOn@ is used to determine what sort of variable a thread
 -- is blocked on.
-data BlockedOn = OnCVarFull CVarId | OnCVarEmpty CVarId | OnCTVar [CTVarId] | OnMask ThreadId deriving Eq
+data BlockedOn = OnMVarFull MVarId | OnMVarEmpty MVarId | OnTVar [TVarId] | OnMask ThreadId deriving Eq
 
 -- | Determine if a thread is blocked in a certain way.
 (~=) :: Thread n r s -> BlockedOn -> Bool
 thread ~= theblock = case (_blocking thread, theblock) of
-  (Just (OnCVarFull  _), OnCVarFull  _) -> True
-  (Just (OnCVarEmpty _), OnCVarEmpty _) -> True
-  (Just (OnCTVar     _), OnCTVar     _) -> True
+  (Just (OnMVarFull  _), OnMVarFull  _) -> True
+  (Just (OnMVarEmpty _), OnMVarEmpty _) -> True
+  (Just (OnTVar      _), OnTVar      _) -> True
   (Just (OnMask      _), OnMask      _) -> True
   _ -> False
 
@@ -78,18 +72,18 @@
 
     -- | Check if no other runnable thread has a reference to anything
     -- the block references.
-    noRefs (Just (OnCVarFull  cvarid)) = null $ findCVar   cvarid
-    noRefs (Just (OnCVarEmpty cvarid)) = null $ findCVar   cvarid
-    noRefs (Just (OnCTVar     ctvids)) = null $ findCTVars ctvids
+    noRefs (Just (OnMVarFull  cvarid)) = null $ findMVar  cvarid
+    noRefs (Just (OnMVarEmpty cvarid)) = null $ findMVar  cvarid
+    noRefs (Just (OnTVar      tvids))  = null $ findTVars tvids
     noRefs _ = True
 
     -- | Get IDs of all threads (other than the one under
-    -- consideration) which reference a 'CVar'.
-    findCVar cvarid = M.keys $ M.filterWithKey (check [Left cvarid]) ts
+    -- consideration) which reference a 'MVar'.
+    findMVar cvarid = M.keys $ M.filterWithKey (check [Left cvarid]) ts
 
     -- | Get IDs of all runnable threads (other than the one under
-    -- consideration) which reference some 'CTVar's.
-    findCTVars ctvids = M.keys $ M.filterWithKey (check (map Right ctvids)) ts
+    -- consideration) which reference some 'TVar's.
+    findTVars tvids = M.keys $ M.filterWithKey (check (map Right tvids)) ts
 
     -- | Check if a thread references a variable, and if it's not the
     -- thread under consideration.
@@ -144,15 +138,15 @@
 -- | Start a thread with the given ID, inheriting the masking state
 -- from the parent thread. This ID must not already be in use!
 launch :: ThreadId -> ThreadId -> ((forall b. M n r s b -> M n r s b) -> Action n r s) -> Threads n r s -> Threads n r s
-launch parent tid a threads = launch' mask tid a threads where
-  mask = fromMaybe Unmasked $ _masking <$> M.lookup parent threads
+launch parent tid a threads = launch' ms tid a threads where
+  ms = fromMaybe Unmasked $ _masking <$> M.lookup parent threads
 
 -- | Start a thread with the given ID and masking state. This must not already be in use!
 launch' :: MaskingState -> ThreadId -> ((forall b. M n r s b -> M n r s b) -> Action n r s) -> Threads n r s -> Threads n r s
-launch' mask tid a = M.insert tid thread where
-  thread = Thread { _continuation = a umask, _blocking = Nothing, _handlers = [], _masking = mask, _known = [], _fullknown = False }
+launch' ms tid a = M.insert tid thread where
+  thread = Thread { _continuation = a umask, _blocking = Nothing, _handlers = [], _masking = ms, _known = [], _fullknown = False }
 
-  umask mb = resetMask True Unmasked >> mb >>= \b -> resetMask False mask >> return b
+  umask mb = resetMask True Unmasked >> mb >>= \b -> resetMask False ms >> return b
   resetMask typ m = cont $ \k -> AResetMask typ True m $ k ()
 
 -- | Kill a thread.
@@ -165,9 +159,9 @@
   doBlock (Just thread) = Just $ thread { _blocking = Just blockedOn }
   doBlock _ = error "Invariant failure in 'block': thread does NOT exist!"
 
--- | Unblock all threads waiting on the appropriate block. For 'CTVar'
+-- | Unblock all threads waiting on the appropriate block. For 'TVar'
 -- blocks, this will wake all threads waiting on at least one of the
--- given 'CTVar's.
+-- given 'TVar's.
 wake :: BlockedOn -> Threads n r s -> (Threads n r s, [ThreadId])
 wake blockedOn threads = (unblock <$> threads, M.keys $ M.filter isBlocked threads) where
   unblock thread
@@ -175,17 +169,17 @@
     | otherwise = thread
 
   isBlocked thread = case (_blocking thread, blockedOn) of
-    (Just (OnCTVar ctvids), OnCTVar blockedOn') -> ctvids `intersect` blockedOn' /= []
+    (Just (OnTVar tvids), OnTVar blockedOn') -> tvids `intersect` blockedOn' /= []
     (theblock, _) -> theblock == Just blockedOn
 
 -- | Record that a thread knows about a shared variable.
-knows :: [Either CVarId CTVarId] -> ThreadId -> Threads n r s -> Threads n r s
+knows :: [Either MVarId TVarId] -> ThreadId -> Threads n r s -> Threads n r s
 knows theids = M.alter go where
   go (Just thread) = Just $ thread { _known = nub $ theids ++ _known thread }
   go _ = error "Invariant failure in 'knows': thread does NOT exist!"
 
 -- | Forget about a shared variable.
-forgets :: [Either CVarId CTVarId] -> ThreadId -> Threads n r s -> Threads n r s
+forgets :: [Either MVarId TVarId] -> ThreadId -> Threads n r s -> Threads n r s
 forgets theids = M.alter go where
   go (Just thread) = Just $ thread { _known = filter (`notElem` theids) $ _known thread }
   go _ = error "Invariant failure in 'forgets': thread does NOT exist!"
diff --git a/Test/DejaFu/Deterministic/Schedule.hs b/Test/DejaFu/Deterministic/Schedule.hs
deleted file mode 100644
--- a/Test/DejaFu/Deterministic/Schedule.hs
+++ /dev/null
@@ -1,57 +0,0 @@
--- | Deterministic scheduling for concurrent computations.
-module Test.DejaFu.Deterministic.Schedule
-  ( Scheduler
-  , ThreadId
-  , NonEmpty(..)
-  -- * Pre-emptive
-  , randomSched
-  , roundRobinSched
-  -- * Non pre-emptive
-  , randomSchedNP
-  , roundRobinSchedNP
-  -- * Utilities
-  , makeNP
-  , toList
-  ) where
-
-import Data.List.Extra
-import System.Random (RandomGen, randomR)
-import Test.DejaFu.Deterministic.Internal
-
--- | A simple random scheduler which, at every step, picks a random
--- thread to run.
-randomSched :: RandomGen g => Scheduler g
-randomSched g _ _ threads = (Just $ threads' !! choice, g') where
-  (choice, g') = randomR (0, length threads' - 1) g
-  threads' = map fst $ toList threads
-
--- | A random scheduler which doesn't pre-empt the running
--- thread. That is, if the last thread scheduled is still runnable,
--- run that, otherwise schedule randomly.
-randomSchedNP :: RandomGen g => Scheduler g
-randomSchedNP = makeNP randomSched
-
--- | A round-robin scheduler which, at every step, schedules the
--- thread with the next 'ThreadId'.
-roundRobinSched :: Scheduler ()
-roundRobinSched _ _ Nothing _ = (Just 0, ())
-roundRobinSched _ _ (Just (prior, _)) threads
-  | prior >= maximum threads' = (Just $ minimum threads', ())
-  | otherwise = (Just . minimum $ filter (>prior) threads', ())
-
-  where
-    threads' = map fst $ toList threads
-
--- | A round-robin scheduler which doesn't pre-empt the running
--- thread.
-roundRobinSchedNP :: Scheduler ()
-roundRobinSchedNP = makeNP roundRobinSched
-
--- | Turn a potentially pre-emptive scheduler into a non-preemptive
--- one.
-makeNP :: Scheduler s -> Scheduler s
-makeNP sched = newsched where
-  newsched s trc p@(Just (prior, _)) threads
-    | prior `elem` map fst (toList threads) = (Just prior, s)
-    | otherwise = sched s trc p threads
-  newsched s trc Nothing threads = sched s trc Nothing threads
diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs
--- a/Test/DejaFu/SCT.hs
+++ b/Test/DejaFu/SCT.hs
@@ -1,6 +1,4 @@
-{-# LANGUAGE CPP                        #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE RankNTypes                 #-}
+{-# LANGUAGE RankNTypes #-}
 
 -- | Systematic testing for concurrent computations.
 module Test.DejaFu.SCT
@@ -25,7 +23,6 @@
   -- K. McKinley for more details.
 
     BacktrackStep(..)
-  , BoundFunc
 
   , sctBounded
   , sctBoundedIO
@@ -44,6 +41,7 @@
 
   , Bounds(..)
   , defaultBounds
+  , noBounds
 
   , sctBound
   , sctBoundIO
@@ -63,6 +61,8 @@
   , defaultPreemptionBound
   , sctPreBound
   , sctPreBoundIO
+  , pBacktrack
+  , pBound
 
   -- ** Fair Bounding
 
@@ -76,6 +76,8 @@
   , defaultFairBound
   , sctFairBound
   , sctFairBoundIO
+  , fBacktrack
+  , fBound
 
   -- ** Length Bounding
 
@@ -86,73 +88,50 @@
   , defaultLengthBound
   , sctLengthBound
   , sctLengthBoundIO
-
-  -- * Utilities
-
-  , (&+&)
-  , trueBound
-  , tidOf
-  , decisionOf
-  , activeTid
-  , preEmpCount
-  , preEmpCount'
-  , yieldCount
-  , maxYieldCountDiff
-  , initialise
-  , initialCVState
-  , updateCVState
-  , willBlock
-  , willBlockSafely
   ) where
 
-import Control.DeepSeq (NFData, force)
 import Data.Functor.Identity (Identity(..), runIdentity)
-import Data.List (nub, partition)
-import Data.Sequence (Seq, (|>))
-import Data.Map (Map)
-import Data.Maybe (isNothing, isJust, fromJust)
-import Test.DejaFu.Deterministic
-import Test.DejaFu.Deterministic.Internal (willRelease)
-import Test.DejaFu.SCT.Internal
-
+import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as M
-import qualified Data.Sequence as Sq
-import qualified Data.Set as S
-
-#if __GLASGOW_HASKELL__ < 710
-import Control.Applicative ((<$>), (<*>))
-#endif
-
--- | A bounding function takes the scheduling decisions so far and a
--- decision chosen to come next, and returns if that decision is
--- within the bound.
-type BoundFunc = [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool
-
--- | Combine two bounds into a larger bound, where both must be
--- satisfied.
-(&+&) :: BoundFunc -> BoundFunc -> BoundFunc
-(&+&) b1 b2 ts dl = b1 ts dl && b2 ts dl
+import Data.Maybe (isJust, fromJust)
+import Test.DPOR ( DPOR(..), dpor
+                 , BacktrackStep(..), backtrackAt
+                 , BoundFunc, (&+&), trueBound
+                 , PreemptionBound(..), defaultPreemptionBound, preempBacktrack
+                 , FairBound(..), defaultFairBound, fairBound, fairBacktrack
+                 , LengthBound(..), defaultLengthBound, lenBound, lenBacktrack
+                 )
 
--- | The \"true\" bound, which allows everything.
-trueBound :: BoundFunc
-trueBound _ _ = True
+import Test.DejaFu.Deterministic (ConcIO, ConcST, runConcIO, runConcST)
+import Test.DejaFu.Deterministic.Internal
 
--- * Combined Bounds
+-------------------------------------------------------------------------------
+-- Combined Bounds
 
 data Bounds = Bounds
-  { preemptionBound :: Maybe PreemptionBound
-  , fairBound       :: Maybe FairBound
-  , lengthBound     :: Maybe LengthBound
+  { boundPreemp :: Maybe PreemptionBound
+  , boundFair   :: Maybe FairBound
+  , boundLength :: Maybe LengthBound
   }
 
 -- | All bounds enabled, using their default values.
 defaultBounds :: Bounds
 defaultBounds = Bounds
-  { preemptionBound = Just defaultPreemptionBound
-  , fairBound       = Just defaultFairBound
-  , lengthBound     = Just defaultLengthBound
+  { boundPreemp = Just defaultPreemptionBound
+  , boundFair   = Just defaultFairBound
+  , boundLength = Just defaultLengthBound
   }
 
+-- | No bounds enabled. This forces the scheduler to just use
+-- partial-order reduction and sleep sets to prune the search
+-- space. This will /ONLY/ work if your computation always terminated!
+noBounds :: Bounds
+noBounds = Bounds
+  { boundPreemp = Nothing
+  , boundFair   = Nothing
+  , boundLength = Nothing
+  }
+
 -- | An SCT runner using a bounded scheduler
 sctBound :: MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
@@ -160,33 +139,37 @@
   -- ^ The combined bounds.
   -> (forall t. ConcST t a)
   -- ^ The computation to run many times
-  -> [(Either Failure a, Trace)]
+  -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
 sctBound memtype cb = sctBounded memtype (cBound cb) (cBacktrack cb)
 
 -- | Variant of 'sctBound' for computations which do 'IO'.
-sctBoundIO :: MemType -> Bounds -> ConcIO a -> IO [(Either Failure a, Trace)]
+sctBoundIO :: MemType
+  -> Bounds
+  -> ConcIO a
+  -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
 sctBoundIO memtype cb = sctBoundedIO memtype (cBound cb) (cBacktrack cb)
 
 -- | Combination bound function
-cBound :: Bounds -> BoundFunc
-cBound (Bounds pb fb lb) = maybe trueBound pbBound pb &+& maybe trueBound fBound fb &+& maybe trueBound lBound lb
+cBound :: Bounds -> BoundFunc ThreadId ThreadAction Lookahead
+cBound (Bounds pb fb lb) = maybe trueBound pBound pb &+& maybe trueBound fBound fb &+& maybe trueBound lenBound lb
 
 -- | Combination backtracking function. Add all backtracking points
 -- corresponding to enabled bound functions.
-cBacktrack :: Bounds -> [BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]
+--
+-- If no bounds are enabled, just backtrack to the given point.
+cBacktrack :: Bounds
+  -> [BacktrackStep ThreadId ThreadAction Lookahead s]
+  -> Int
+  -> ThreadId
+  -> [BacktrackStep ThreadId ThreadAction Lookahead s]
+cBacktrack (Bounds Nothing Nothing Nothing) bs i t = backtrackAt (const False) False bs i t
 cBacktrack (Bounds pb fb lb) bs i t = lBack . fBack $ pBack bs where
-  pBack backs = if isJust pb then pbBacktrack backs i t else backs
-  fBack backs = if isJust fb then fBacktrack  backs i t else backs
-  lBack backs = if isJust lb then lBacktrack  backs i t else backs
-
--- * Pre-emption bounding
-
-newtype PreemptionBound = PreemptionBound Int
-  deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show)
+  pBack backs = if isJust pb then pBacktrack   backs i t else backs
+  fBack backs = if isJust fb then fBacktrack   backs i t else backs
+  lBack backs = if isJust lb then lenBacktrack backs i t else backs
 
--- | A sensible default pre-emption bound: 2
-defaultPreemptionBound :: PreemptionBound
-defaultPreemptionBound = 2
+-------------------------------------------------------------------------------
+-- Pre-emption bounding
 
 -- | An SCT runner using a pre-emption bounding scheduler.
 sctPreBound :: MemType
@@ -196,77 +179,37 @@
   -- execution
   -> (forall t. ConcST t a)
   -- ^ The computation to run many times
-  -> [(Either Failure a, Trace)]
-sctPreBound memtype pb = sctBounded memtype (pbBound pb) pbBacktrack
+  -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
+sctPreBound memtype pb = sctBounded memtype (pBound pb) pBacktrack
 
 -- | Variant of 'sctPreBound' for computations which do 'IO'.
-sctPreBoundIO :: MemType -> PreemptionBound -> ConcIO a -> IO [(Either Failure a, Trace)]
-sctPreBoundIO memtype pb = sctBoundedIO memtype (pbBound pb) pbBacktrack
-
--- | Pre-emption bound function
-pbBound :: PreemptionBound -> BoundFunc
-pbBound (PreemptionBound pb) ts dl = preEmpCount ts dl <= pb
-
--- | Count the number of pre-emptions in a schedule prefix.
-preEmpCount :: [(Decision, ThreadAction)] -> (Decision, a) -> Int
-preEmpCount ts (d, _) = go Nothing ts where
-  go p ((d, a):rest) = preEmpC p d + go (Just a) rest
-  go p [] = preEmpC p d
-
-  preEmpC (Just Yield) (SwitchTo _) = 0
-  preEmpC _ (SwitchTo t) = if t >= 0 then 1 else 0
-  preEmpC _ _ = 0
-
--- | Count the number of pre-emptions in an entire trace
-preEmpCount' :: Trace -> Int
-preEmpCount' trc = preEmpCount (map (\(d,_,a) -> (d, a)) trc) (Continue, WillStop)
+sctPreBoundIO :: MemType
+  -> PreemptionBound
+  -> ConcIO a
+  -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
+sctPreBoundIO memtype pb = sctBoundedIO memtype (pBound pb) pBacktrack
 
 -- | Add a backtrack point, and also conservatively add one prior to
 -- the most recent transition before that point. This may result in
 -- the same state being reached multiple times, but is needed because
 -- of the artificial dependency imposed by the bound.
-pbBacktrack :: [BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]
-pbBacktrack bs i tid = maybe id (\j' b -> backtrack True b j' tid) j $ backtrack False bs i tid where
-  -- Index of the conservative point
-  j = goJ . reverse . pairs $ zip [0..i-1] bs where
-    goJ (((_,b1), (j',b2)):rest)
-      | _threadid b1 /= _threadid b2 && not (commit b1) && not (commit b2) = Just j'
-      | otherwise = goJ rest
-    goJ [] = Nothing
-
-  {-# INLINE pairs #-}
-  pairs = zip <*> tail
-
-  commit b = case _decision b of
-    (_, CommitRef _ _) -> True
-    _ -> False
-
-  -- Add a backtracking point. If the thread isn't runnable, add all
-  -- runnable threads.
-  backtrack c bx@(b:rest) 0 t
-    -- If the backtracking point is already present, don't re-add it,
-    -- UNLESS this would force it to backtrack (it's conservative)
-    -- where before it might not.
-    | t `M.member` _runnable b =
-      let val = M.lookup t $ _backtrack b
-      in  if isNothing val || (val == Just False && c)
-          then b { _backtrack = M.insert t c $ _backtrack b } : rest
-          else bx
-
-    -- Otherwise just backtrack to everything runnable.
-    | otherwise = b { _backtrack = M.fromList [ (t',c) | t' <- M.keys $ _runnable b ] } : rest
-
-  backtrack c (b:rest) n t = b : backtrack c rest (n-1) t
-  backtrack _ [] _ _ = error "Ran out of schedule whilst backtracking!"
-
--- * Fair bounding
+pBacktrack :: [BacktrackStep ThreadId ThreadAction Lookahead s]
+  -- ^ The current backtracking points.
+  -> Int
+  -- ^ The point to backtrack to.
+  -> ThreadId
+  -- ^ The thread to backtrack to.
+  -> [BacktrackStep ThreadId ThreadAction Lookahead s]
+pBacktrack = preempBacktrack isCommitRef
 
-newtype FairBound = FairBound Int
-  deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show)
+-- | Pre-emption bound function. This is different to @preempBound@ in
+-- that it does not count pre-emptive context switches to a commit
+-- thread.
+pBound :: PreemptionBound -> BoundFunc ThreadId ThreadAction Lookahead
+pBound (PreemptionBound pb) ts dl = preEmpCount ts dl <= pb
 
--- | A sensible default fair bound: 5
-defaultFairBound :: FairBound
-defaultFairBound = 5
+-------------------------------------------------------------------------------
+-- Fair bounding
 
 -- | An SCT runner using a fair bounding scheduler.
 sctFairBound :: MemType
@@ -276,67 +219,33 @@
   -- performed by different threads.
   -> (forall t. ConcST t a)
   -- ^ The computation to run many times
-  -> [(Either Failure a, Trace)]
+  -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
 sctFairBound memtype fb = sctBounded memtype (fBound fb) fBacktrack
 
 -- | Variant of 'sctFairBound' for computations which do 'IO'.
-sctFairBoundIO :: MemType -> FairBound -> ConcIO a -> IO [(Either Failure a, Trace)]
+sctFairBoundIO :: MemType
+  -> FairBound
+  -> ConcIO a
+  -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
 sctFairBoundIO memtype fb = sctBoundedIO memtype (fBound fb) fBacktrack
 
 -- | Fair bound function
-fBound :: FairBound -> BoundFunc
-fBound (FairBound fb) ts dl = maxYieldCountDiff ts dl <= fb
-
--- | Count the number of yields by a thread in a schedule prefix.
-yieldCount :: ThreadId -> [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Int
-yieldCount tid ts (_, l) = go 0 ts where
-  go t ((Start    t', Yield):rest) = (if t == tid then 1 else 0) + go t' rest
-  go t ((SwitchTo t', Yield):rest) = (if t == tid then 1 else 0) + go t' rest
-  go t ((Continue,    Yield):rest) = (if t == tid then 1 else 0) + go t  rest
-  go _ ((Start    t', _):rest) = go t' rest
-  go _ ((SwitchTo t', _):rest) = go t' rest
-  go t ((Continue,    _):rest) = go t  rest
-  go t (_:rest) = go t rest
-  go t [] = if l == WillYield && t == tid then 1 else 0
-
--- | Get the maximum difference between the yield counts of all
--- threads in this schedule prefix.
-maxYieldCountDiff :: [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Int
-maxYieldCountDiff ts dl = maximum yieldCountDiffs where
-  yieldCounts = [yieldCount tid ts dl | tid <- nub $ allTids ts]
-  yieldCountDiffs = [y1 - y2 | y1 <- yieldCounts, y2 <- yieldCounts]
-
-  allTids ((_, Fork tid):rest) = tid : allTids rest
-  allTids (_:rest) = allTids rest
-  allTids [] = [0]
+fBound :: FairBound -> BoundFunc ThreadId ThreadAction Lookahead
+fBound = fairBound didYield willYield (\act -> case act of Fork t -> [t]; _ -> [])
 
 -- | Add a backtrack point. If the thread isn't runnable, or performs
 -- a release operation, add all runnable threads.
-fBacktrack :: [BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]
-fBacktrack bx@(b:rest) 0 t
-  -- If the backtracking point is already present, don't re-add it,
-  -- UNLESS this would force it to backtrack (it's conservative) where
-  -- before it might not.
-  | Just False == (willRelease <$> M.lookup t (_runnable b)) =
-    let val = M.lookup t $ _backtrack b
-    in  if isNothing val
-        then b { _backtrack = M.insert t False $ _backtrack b } : rest
-        else bx
-
-  -- Otherwise just backtrack to everything runnable.
-  | otherwise = b { _backtrack = M.fromList [ (t',False) | t' <- M.keys $ _runnable b ] } : rest
-
-fBacktrack (b:rest) n t = b : fBacktrack rest (n-1) t
-fBacktrack [] _ _ = error "Ran out of schedule whilst backtracking!"
-
--- * Length Bounding
-
-newtype LengthBound = LengthBound Int
-  deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show)
+fBacktrack :: [BacktrackStep ThreadId ThreadAction Lookahead s]
+  -- ^ The current backtracking points.
+  -> Int
+  -- ^ The point to backtrack to.
+  -> ThreadId
+  -- ^ The thread to backtrack to.
+  -> [BacktrackStep ThreadId ThreadAction Lookahead s]
+fBacktrack = fairBacktrack willRelease
 
--- | A sensible default length bound: 250
-defaultLengthBound :: LengthBound
-defaultLengthBound = 250
+-------------------------------------------------------------------------------
+-- Length bounding
 
 -- | An SCT runner using a length bounding scheduler.
 sctLengthBound :: MemType
@@ -346,31 +255,18 @@
   -- actions.
   -> (forall t. ConcST t a)
   -- ^ The computation to run many times
-  -> [(Either Failure a, Trace)]
-sctLengthBound memtype lb = sctBounded memtype (lBound lb) lBacktrack
+  -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
+sctLengthBound memtype lb = sctBounded memtype (lenBound lb) lenBacktrack
 
 -- | Variant of 'sctFairBound' for computations which do 'IO'.
-sctLengthBoundIO :: MemType -> LengthBound -> ConcIO a -> IO [(Either Failure a, Trace)]
-sctLengthBoundIO memtype lb = sctBoundedIO memtype (lBound lb) lBacktrack
-
--- | Length bound function
-lBound :: LengthBound -> BoundFunc
-lBound (LengthBound lb) ts _ = length ts < lb
-
--- | Add a backtrack point. If the thread isn't runnable, add all
--- runnable threads.
-lBacktrack :: [BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]
-lBacktrack bx@(b:rest) 0 t
-  | t `M.member` _runnable b =
-    let val = M.lookup t $ _backtrack b
-    in  if isNothing val
-        then b { _backtrack = M.insert t False $ _backtrack b } : rest
-        else bx
-  | otherwise = b { _backtrack = M.fromList [ (t',False) | t' <- M.keys $ _runnable b ] } : rest
-lBacktrack (b:rest) n t = b : lBacktrack rest (n-1) t
-lBacktrack [] _ _ = error "Ran out of schedule whilst backtracking!"
+sctLengthBoundIO :: MemType
+  -> LengthBound
+  -> ConcIO a
+  -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
+sctLengthBoundIO memtype lb = sctBoundedIO memtype (lenBound lb) lenBacktrack
 
--- * BPOR
+-------------------------------------------------------------------------------
+-- DPOR
 
 -- | SCT via BPOR.
 --
@@ -386,129 +282,176 @@
 -- previously non-interfering events interfere with each other.
 sctBounded :: MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> BoundFunc
+  -> BoundFunc ThreadId ThreadAction Lookahead
   -- ^ Check if a prefix trace is within the bound
-  -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])
+  -> ([BacktrackStep ThreadId ThreadAction Lookahead CRState] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead CRState])
   -- ^ Add a new backtrack point, this takes the history of the
   -- execution so far, the index to insert the backtracking point, and
   -- the thread to backtrack to. This may insert more than one
   -- backtracking point.
-  -> (forall t. ConcST t a) -> [(Either Failure a, Trace)]
+  -> (forall t. ConcST t a) -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
 sctBounded memtype bf backtrack c = runIdentity $ sctBoundedM memtype bf backtrack run where
-  run memty sched s = Identity $ runConcST' sched memty s c
+  run memty sched s = Identity $ runConcST sched memty s c
 
 -- | Variant of 'sctBounded' for computations which do 'IO'.
-sctBoundedIO :: MemType -> BoundFunc
-  -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])
-  -> ConcIO a -> IO [(Either Failure a, Trace)]
+sctBoundedIO :: MemType
+  -> BoundFunc ThreadId ThreadAction Lookahead
+  -> ([BacktrackStep ThreadId ThreadAction Lookahead CRState] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead CRState])
+  -> ConcIO a -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
 sctBoundedIO memtype bf backtrack c = sctBoundedM memtype bf backtrack run where
-  run memty sched s = runConcIO' sched memty s c
+  run memty sched s = runConcIO sched memty s c
 
 -- | Generic SCT runner.
-sctBoundedM :: (Functor m, Monad m)
+sctBoundedM :: Monad m
   => MemType
-  -> ([(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool)
-  -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])
-  -> (MemType -> Scheduler SchedState -> SchedState -> m (Either Failure a, SchedState, Trace'))
+  -> ([(Decision ThreadId, ThreadAction)] -> (Decision ThreadId, Lookahead) -> Bool)
+  -> ([BacktrackStep ThreadId ThreadAction Lookahead CRState] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead CRState])
+  -> (forall s. MemType -> Scheduler ThreadId ThreadAction Lookahead s -> s -> m (Either Failure a, s, Trace ThreadId ThreadAction Lookahead))
   -- ^ Monadic runner, with computation fixed.
-  -> m [(Either Failure a, Trace)]
-sctBoundedM memtype bf backtrack run = go initialState where
-  go bpor = case next bpor of
-    Just (sched, conservative, sleep) -> do
-      (res, s, trace) <- run memtype (bporSched memtype $ initialise bf) (initialSchedState sleep sched)
+  -> m [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
+sctBoundedM memtype bf backtrack run =
+  dpor didYield
+       willYield
+       initialCRState
+       updateCRState
+       (dependent  memtype)
+       (dependent' memtype)
+       initialThread
+       (>=initialThread)
+       bf
+       backtrack
+       pruneCommits
+       (run memtype)
 
-      let bpoints = findBacktrack memtype backtrack (_sbpoints s) trace
-      let newBPOR = grow memtype conservative trace bpor
+-------------------------------------------------------------------------------
+-- Post-processing
 
-      if _signore s
-      then go newBPOR
-      else ((res, toTrace trace):) <$> go (pruneCommits $ todo bf bpoints newBPOR)
+-- | Remove commits from the todo sets where every other action will
+-- result in a write barrier (and so a commit) occurring.
+--
+-- To get the benefit from this, do not execute commit actions from
+-- the todo set until there are no other choises.
+pruneCommits :: DPOR ThreadId ThreadAction -> DPOR ThreadId ThreadAction
+pruneCommits bpor
+  | not onlycommits || not alldonesync = go bpor
+  | otherwise = go bpor { dporTodo = M.empty }
 
-    Nothing -> return []
+  where
+    go b = b { dporDone = pruneCommits <$> dporDone bpor }
 
--- * BPOR Scheduler
+    onlycommits = all (<initialThread) . M.keys $ dporTodo bpor
+    alldonesync = all barrier . M.elems $ dporDone bpor
 
--- | The scheduler state
-data SchedState = SchedState
-  { _ssleep   :: Map ThreadId ThreadAction
-  -- ^ The sleep set: decisions not to make until something dependent
-  -- with them happens.
-  , _sprefix  :: [ThreadId]
-  -- ^ Decisions still to make
-  , _sbpoints :: Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])
-  -- ^ Which threads are runnable at each step, and the alternative
-  -- decisions still to make.
-  , _signore  :: Bool
-  -- ^ Whether to ignore this execution or not: @True@ if the
-  -- execution is aborted due to all possible decisions being in the
-  -- sleep set, as then everything in this execution is covered by
-  -- another.
-  } deriving Show
+    barrier = isBarrier . simplify . fromJust . dporAction
 
--- | Initial scheduler state for a given prefix
-initialSchedState :: Map ThreadId ThreadAction -> [ThreadId] -> SchedState
-initialSchedState sleep prefix = SchedState
-  { _ssleep   = sleep
-  , _sprefix  = prefix
-  , _sbpoints = Sq.empty
-  , _signore  = False
-  }
+-------------------------------------------------------------------------------
+-- Dependency function
 
--- | BPOR scheduler: takes a list of decisions, and maintains a trace
--- including the runnable threads, and the alternative choices allowed
--- by the bound-specific initialise function.
-bporSched :: MemType
-  -> ([(Decision, ThreadAction)] -> Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> [ThreadId])
-  -> Scheduler SchedState
-bporSched memtype init = force $ \s trc prior threads -> case _sprefix s of
-  -- If there is a decision available, make it
-  (d:ds) ->
-    let threads' = fmap (\(t,a:|_) -> (t,a)) threads
-    in  (Just d, s { _sprefix = ds, _sbpoints = _sbpoints s |> (threads', []) })
+-- | Check if an action is dependent on another.
+dependent :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, ThreadAction) -> Bool
+dependent _ _ (_, Lift) (_, Lift) = True
+dependent _ _ (_, ThrowTo t) (t2, Stop) | t == t2 = False
+dependent _ _ (t2, Stop) (_, ThrowTo t) | t == t2 = False
+dependent _ _ (_, ThrowTo t) (t2, _) = t == t2
+dependent _ _ (t2, _) (_, ThrowTo t) = t == t2
+dependent _ _ (_, STM _ _) (_, STM _ _) = True
+dependent _ _ (_, GetNumCapabilities a) (_, SetNumCapabilities b) = a /= b
+dependent _ _ (_, SetNumCapabilities a) (_, GetNumCapabilities b) = a /= b
+dependent _ _ (_, SetNumCapabilities a) (_, SetNumCapabilities b) = a /= b
+dependent memtype buf (_, d1) (_, d2) = dependentActions memtype buf (simplify d1) (simplify d2)
 
-  -- Otherwise query the initialise function for a list of possible
-  -- choices, filter out anything in the sleep set, and make one of
-  -- them arbitrarily (recording the others).
-  [] ->
-    let threads' = fmap (\(t,a:|_) -> (t,a)) threads
-        choices  = init trc prior threads'
-        checkDep t a = case prior of
-          Just (tid, act) -> dependent memtype unknownCRState (tid, act) (t, a)
-          Nothing -> False
-        ssleep'  = M.filterWithKey (\t a -> not $ checkDep t a) $ _ssleep s
-        choices' = filter (`notElem` M.keys ssleep') choices
-        signore' = not (null choices) && all (`elem` M.keys ssleep') choices
-    in  case choices' of
-          (nextTid:rest) -> (Just nextTid, s { _sbpoints = _sbpoints s |> (threads', rest), _ssleep = ssleep' })
-          [] -> (Nothing, s { _sbpoints = _sbpoints s |> (threads', []), _signore = signore' })
+-- | Variant of 'dependent' to handle 'ThreadAction''s
+dependent' :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, Lookahead) -> Bool
+dependent' _ _ (_, Lift) (_, WillLift) = True
+dependent' _ _ (_, ThrowTo t) (t2, WillStop) | t == t2 = False
+dependent' _ _ (t2, Stop) (_, WillThrowTo t) | t == t2 = False
+dependent' _ _ (_, ThrowTo t) (t2, _)     = t == t2
+dependent' _ _ (t2, _) (_, WillThrowTo t) = t == t2
+dependent' _ _ (_, STM _ _) (_, WillSTM) = True
+dependent' _ _ (_, GetNumCapabilities a) (_, WillSetNumCapabilities b) = a /= b
+dependent' _ _ (_, SetNumCapabilities _) (_, WillGetNumCapabilities)   = True
+dependent' _ _ (_, SetNumCapabilities a) (_, WillSetNumCapabilities b) = a /= b
+-- This is safe because, if the thread blocks anyway, a context switch
+-- will occur anyway so there's no point pre-empting the action.
+--
+-- UNLESS the pre-emption would possibly allow for a different relaxed
+-- memory stage.
+dependent' _ _ (_, a1) (_, a2) | isBlock a1 && isBarrier (simplify' a2) = False
+dependent' memtype buf (_, d1) (_, d2) = dependentActions memtype buf (simplify d1) (simplify' d2)
 
--- | Pick a new thread to run, which does not exceed the bound. Choose
--- the current thread if available and it hasn't just yielded,
--- otherwise add all runnable threads.
-initialise :: BoundFunc
-  -> [(Decision, ThreadAction)]
-  -> Maybe (ThreadId, ThreadAction)
-  -> NonEmpty (ThreadId, Lookahead)
-  -> [ThreadId]
-initialise bf trc prior threads = restrictToBound . yieldsToEnd $ case prior of
-  Just (_, Yield) -> map fst threads'
-  Just (tid, _)
-    | any (\(t, _) -> t == tid) threads' -> [tid]
-  _ -> map fst threads'
+-- | Check if two 'ActionType's are dependent. Note that this is not
+-- sufficient to know if two 'ThreadAction's are dependent, without
+-- being so great an over-approximation as to be useless!
+dependentActions :: MemType -> CRState -> ActionType -> ActionType -> Bool
+dependentActions memtype buf a1 a2 = case (a1, a2) of
+  -- Unsynchronised reads and writes are always dependent, even under
+  -- a relaxed memory model, as an unsynchronised write gives rise to
+  -- a commit, which synchronises.
+  (UnsynchronisedRead  r1, UnsynchronisedWrite r2) -> r1 == r2
+  (UnsynchronisedWrite r1, UnsynchronisedRead  r2) -> r1 == r2
+  (UnsynchronisedWrite r1, UnsynchronisedWrite r2) -> r1 == r2
 
+  -- Unsynchronised writes and synchronisation where the buffer is not
+  -- empty.
+  --
+  -- See [RMMVerification], lemma 5.25.
+  (UnsynchronisedWrite r1, _) | same crefOf && isCommit a2 r1 && isBuffered buf r1 -> False
+  (_, UnsynchronisedWrite r2) | same crefOf && isCommit a1 r2 && isBuffered buf r2 -> False
+
+  -- Unsynchronised reads where a memory barrier would flush a
+  -- buffered write
+  (UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered buf r1 && memtype /= SequentialConsistency
+  (_, UnsynchronisedRead r2) | isBarrier a1 -> isBuffered buf r2 && memtype /= SequentialConsistency
+
+  (_, _)
+    -- Two actions on the same CRef where at least one is synchronised
+    | same crefOf && (synchronises a1 (fromJust $ crefOf a1) || synchronises a2 (fromJust $ crefOf a2)) -> True
+    -- Two actions on the same MVar
+    | same cvarOf -> True
+
+  _ -> False
+
   where
-    -- Restrict the possible decisions to those in the bound.
-    restrictToBound = fst . partition (\t -> bf trc (decision t, action t))
+    same f = isJust (f a1) && f a1 == f a2
 
-    -- Move the threads which will immediately yield to the end of the list
-    yieldsToEnd ts = case partition ((== WillYield) . action) ts of
-      (willYield, noYield) -> noYield ++ willYield
+-------------------------------------------------------------------------------
+-- Dependency function state
 
-    -- Get the decision that will lead to a thread being scheduled.
-    decision = decisionOf (fst <$> prior) (S.fromList $ map fst threads')
+type CRState = Map CRefId Bool
 
-    -- Get the action of a thread
-    action t = fromJust $ lookup t threads'
+-- | Initial global 'CRef buffer state.
+initialCRState :: CRState
+initialCRState = M.empty
 
-    -- The list of threads
-    threads' = toList threads
+-- | Update the 'CRef' buffer state with the action that has just
+-- happened.
+updateCRState :: CRState -> ThreadAction -> CRState
+updateCRState crstate (CommitRef _ r) = M.delete r crstate
+updateCRState crstate (WriteRef r) = M.insert r True crstate
+updateCRState crstate ta
+  | isBarrier $ simplify ta = initialCRState
+  | otherwise = crstate
+
+-- | Check if a 'CRef' has a buffered write pending.
+--
+-- If the state is @Unknown@, this assumes @True@.
+isBuffered :: CRState -> CRefId -> Bool
+isBuffered crstate r = M.findWithDefault False r crstate
+
+-------------------------------------------------------------------------------
+-- Utilities
+
+-- | Determine if an action is a commit or not.
+isCommitRef :: ThreadAction -> Bool
+isCommitRef (CommitRef _ _) = True
+isCommitRef _ = False
+
+-- | Check if a thread yielded.
+didYield :: ThreadAction -> Bool
+didYield Yield = True
+didYield _ = False
+
+-- | Check if a thread will yield.
+willYield :: Lookahead -> Bool
+willYield WillYield = True
+willYield _ = False
diff --git a/Test/DejaFu/SCT/Internal.hs b/Test/DejaFu/SCT/Internal.hs
deleted file mode 100644
--- a/Test/DejaFu/SCT/Internal.hs
+++ /dev/null
@@ -1,437 +0,0 @@
-{-# LANGUAGE CPP #-}
-
--- | Internal utilities and types for BPOR.
-module Test.DejaFu.SCT.Internal where
-
-import Control.DeepSeq (NFData(..))
-import Data.List (foldl', partition, sortBy, intercalate)
-import Data.Map.Strict (Map)
-import Data.Maybe (mapMaybe, isJust, fromJust, listToMaybe)
-import Data.Ord (Down(..), comparing)
-import Data.Sequence (Seq, ViewL(..))
-import Data.Set (Set)
-import Test.DejaFu.Deterministic.Internal
-import Test.DejaFu.Deterministic.Schedule
-
-import qualified Data.Map.Strict as M
-import qualified Data.Sequence as Sq
-import qualified Data.Set as S
-
-#if __GLASGOW_HASKELL__ < 710
-import Control.Applicative ((<$>), (<*>))
-#endif
-
--- * BPOR state
-
--- | One step of the execution, including information for backtracking
--- purposes. This backtracking information is used to generate new
--- schedules.
-data BacktrackStep = BacktrackStep
-  { _threadid  :: ThreadId
-  -- ^ The thread running at this step
-  , _decision  :: (Decision, ThreadAction)
-  -- ^ What happened at this step.
-  , _runnable  :: Map ThreadId Lookahead
-  -- ^ The threads runnable at this step
-  , _backtrack :: Map ThreadId Bool
-  -- ^ The list of alternative threads to run, and whether those
-  -- alternatives were added conservatively due to the bound.
-  } deriving (Eq, Show)
-
-instance NFData BacktrackStep where
-  rnf b = rnf (_threadid b, _decision b, _runnable b, _backtrack b)
-
--- | BPOR execution is represented as a tree of states, characterised
--- by the decisions that lead to that state.
-data BPOR = BPOR
-  { _brunnable :: Set ThreadId
-  -- ^ What threads are runnable at this step.
-  , _btodo     :: Map ThreadId Bool
-  -- ^ Follow-on decisions still to make, and whether that decision
-  -- was added conservatively due to the bound.
-  , _bignore   :: Set ThreadId
-  -- ^ Follow-on decisions never to make, because they will result in
-  -- the chosen thread immediately blocking without achieving
-  -- anything, which can't have any effect on the result of the
-  -- program.
-  , _bdone     :: Map ThreadId BPOR
-  -- ^ Follow-on decisions that have been made.
-  , _bsleep    :: Map ThreadId ThreadAction
-  -- ^ Transitions to ignore (in this node and children) until a
-  -- dependent transition happens.
-  , _btaken    :: Map ThreadId ThreadAction
-  -- ^ Transitions which have been taken, excluding
-  -- conservatively-added ones. This is used in implementing sleep
-  -- sets.
-  , _baction    :: Maybe ThreadAction
-  -- ^ What happened at this step. This will be 'Nothing' at the root,
-  -- 'Just' everywhere else.
-  }
-
--- | Render a 'BPOR' value as a graph in GraphViz \"dot\" format.
-toDot :: BPOR -> String
-toDot bpor = "digraph {\n" ++ go "L" bpor ++ "\n}" where
-  go l b = unlines $ node l b : [edge l l' i ++ go l' b' | (i, b') <- M.toList (_bdone b), let l' = l ++ show' i]
-
-  -- Display a labelled node.
-  node n b = n ++ " [label=\"" ++ label b ++ "\"]"
-
-  -- A node label, summary of the BPOR state at that node.
-  label b = intercalate ","
-    [ show $ _baction b
-    , "Run:" ++ show (S.toList $ _brunnable b)
-    , "Tod:" ++ show (M.keys   $ _btodo     b)
-    , "Ign:" ++ show (S.toList $ _bignore   b)
-    , "Slp:" ++ show (M.toList $ _bsleep    b)
-    ]
-
-  -- Display a labelled edge
-  edge n1 n2 l = n1 ++ "-> " ++ n2 ++ " [label=\"" ++ show l ++ "\"]\n"
-
-  -- Show a number, replacing a minus sign for \"N\".
-  show' i = if i < 0 then "N" ++ show (negate i) else show i
-
--- | Variant of 'toDot' which doesn't include aborted subtrees.
-toDotSmall :: BPOR -> String
-toDotSmall bpor = "digraph {\n" ++ go "L" bpor ++ "\n}" where
-  go l b = unlines $ node l b : [edge l l' i ++ go l' b' | (i, b') <- M.toList (_bdone b), check b', let l' = l ++ show' i]
-
-  -- Check that a subtree has at least one non-aborted branch.
-  check b = S.null (_brunnable b) || any check (M.elems $ _bdone b)
-
-  -- Display a labelled node.
-  node n b = n ++ " [label=\"" ++ label b ++ "\"]"
-
-  -- A node label, summary of the BPOR state at that node.
-  label b = intercalate ","
-    [ show $ _baction b
-    , "Run:" ++ show (S.toList $ _brunnable b)
-    , "Tod:" ++ show (M.keys   $ _btodo     b)
-    , "Ign:" ++ show (S.toList $ _bignore   b)
-    , "Slp:" ++ show (M.toList $ _bsleep    b)
-    ]
-
-  -- Display a labelled edge
-  edge n1 n2 l = n1 ++ "-> " ++ n2 ++ " [label=\"" ++ show l ++ "\"]\n"
-
-  -- Show a number, replacing a minus sign for \"N\".
-  show' i = if i < 0 then "N" ++ show (negate i) else show i
-
--- | Initial BPOR state.
-initialState :: BPOR
-initialState = BPOR
-  { _brunnable = S.singleton (ThreadId 0)
-  , _btodo     = M.singleton (ThreadId 0) False
-  , _bignore   = S.empty
-  , _bdone     = M.empty
-  , _bsleep    = M.empty
-  , _btaken    = M.empty
-  , _baction   = Nothing
-  }
-
--- | Produce a new schedule from a BPOR tree. If there are no new
--- schedules remaining, return 'Nothing'. Also returns whether the
--- decision was added conservatively, and the sleep set at the point
--- where divergence happens.
---
--- This returns the longest prefix, on the assumption that this will
--- lead to lots of backtracking points being identified before
--- higher-up decisions are reconsidered, so enlarging the sleep sets.
-next :: BPOR -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
-next = go 0 where
-  go tid bpor =
-        -- All the possible prefix traces from this point, with
-        -- updated BPOR subtrees if taken from the done list.
-    let prefixes = mapMaybe go' (M.toList $ _bdone bpor) ++ [([t], c, sleeps bpor) | (t, c) <- M.toList $ _btodo bpor]
-        -- Sort by number of preemptions, in descending order.
-        cmp = preEmps tid bpor . (\(a,_,_) -> a)
-
-    in if null prefixes
-       then Nothing
-       else case partition (\(t:_,_,_) -> t < 0) $ sortBy (comparing $ Down . cmp) prefixes of
-              (commits, others)
-                | not $ null others  -> listToMaybe others
-                | not $ null commits -> listToMaybe commits
-                | otherwise -> error "Invariant failure in 'next': empty prefix list!"
-
-  go' (tid, bpor) = (\(ts,c,slp) -> (tid:ts,c,slp)) <$> go tid bpor
-
-  sleeps bpor = _bsleep bpor `M.union` _btaken bpor
-
-  preEmps tid bpor (t:ts) =
-    let rest = preEmps t (fromJust . M.lookup t $ _bdone bpor) ts
-    in  if t > 0 && tid /= t && tid `S.member` _brunnable bpor then 1 + rest else rest
-  preEmps _ _ [] = 0::Int
-
--- | Produce a list of new backtracking points from an execution
--- trace.
-findBacktrack :: MemType
-  -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])
-  -> Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])
-  -> Trace'
-  -> [BacktrackStep]
-findBacktrack memtype backtrack = go initialCRState S.empty 0 [] . Sq.viewl where
-  go crstate allThreads tid bs ((e,i):<is) ((d,_,a):ts) =
-    let tid' = tidOf tid d
-        crstate' = updateCRState crstate a
-        this = BacktrackStep
-          { _threadid  = tid'
-          , _decision  = (d, a)
-          , _runnable  = M.fromList . toList $ e
-          , _backtrack = M.fromList $ map (\i' -> (i', False)) i
-          }
-        allThreads' = allThreads `S.union` S.fromList (M.keys $ _runnable this)
-        killsEarly = null ts && any (/=0) (M.keys $ _runnable this)
-        bs' = doBacktrack killsEarly crstate' allThreads' (toList e) (bs++[this])
-    in go crstate' allThreads' tid' bs' (Sq.viewl is) ts
-  go _ _ _ bs _ _ = bs
-
-  doBacktrack killsEarly crstate allThreads enabledThreads bs =
-    let tagged = reverse $ zip [0..] bs
-        idxs   = [ (head is, u)
-                 | (u, n) <- enabledThreads
-                 , v <- S.toList allThreads
-                 , u /= v
-                 , let is = [ i
-                            | (i, b) <- tagged
-                            , _threadid b == v
-                            , killsEarly || dependent' memtype crstate (_threadid b, snd $ _decision b) (u, n)
-                            ]
-                 , not $ null is] :: [(Int, ThreadId)]
-    in foldl' (\b (i, u) -> backtrack b i u) bs idxs
-
--- | Add a new trace to the tree, creating a new subtree.
-grow :: MemType -> Bool -> Trace' -> BPOR -> BPOR
-grow memtype conservative = grow' initialCVState initialCRState 0 where
-  grow' cvstate crstate tid trc@((d, _, a):rest) bpor =
-    let tid'     = tidOf tid d
-        cvstate' = updateCVState cvstate a
-        crstate' = updateCRState crstate a
-    in  case M.lookup tid' $ _bdone bpor of
-          Just bpor' -> bpor { _bdone  = M.insert tid' (grow' cvstate' crstate' tid' rest bpor') $ _bdone bpor }
-          Nothing    -> bpor { _btaken = if conservative then _btaken bpor else M.insert tid' a $ _btaken bpor
-                            , _btodo  = M.delete tid' $ _btodo bpor
-                            , _bdone  = M.insert tid' (subtree cvstate' crstate' tid' (_bsleep bpor `M.union` _btaken bpor) trc) $ _bdone bpor }
-  grow' _ _ _ [] bpor = bpor
-
-  subtree cvstate crstate tid sleep ((d, ts, a):rest) =
-    let cvstate' = updateCVState cvstate a
-        crstate' = updateCRState crstate a
-        sleep'   = M.filterWithKey (\t a' -> not $ dependent memtype crstate' (tid, a) (t,a')) sleep
-    in BPOR
-        { _brunnable = S.fromList $ tids tid d a ts
-        , _btodo     = M.empty
-        , _bignore   = S.fromList [tidOf tid d' | (d',as) <- ts, willBlockSafely cvstate' $ toList as]
-        , _bdone     = M.fromList $ case rest of
-          ((d', _, _):_) ->
-            let tid' = tidOf tid d'
-            in  [(tid', subtree cvstate' crstate' tid' sleep' rest)]
-          [] -> []
-        , _bsleep = sleep'
-        , _btaken = case rest of
-          ((d', _, a'):_) -> M.singleton (tidOf tid d') a'
-          [] -> M.empty
-        , _baction = Just a
-        }
-  subtree _ _ _ _ [] = error "Invariant failure in 'subtree': suffix empty!"
-
-  tids tid d (Fork t)           ts = tidOf tid d : t : map (tidOf tid . fst) ts
-  tids tid _ (BlockedPutVar _)  ts = map (tidOf tid . fst) ts
-  tids tid _ (BlockedReadVar _) ts = map (tidOf tid . fst) ts
-  tids tid _ (BlockedTakeVar _) ts = map (tidOf tid . fst) ts
-  tids tid _ BlockedSTM         ts = map (tidOf tid . fst) ts
-  tids tid _ (BlockedThrowTo _) ts = map (tidOf tid . fst) ts
-  tids tid _ Stop               ts = map (tidOf tid . fst) ts
-  tids tid d _ ts = tidOf tid d : map (tidOf tid . fst) ts
-
--- | Add new backtracking points, if they have not already been
--- visited, fit into the bound, and aren't in the sleep set.
-todo :: ([(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool) -> [BacktrackStep] -> BPOR -> BPOR
-todo bv = step where
-  step bs bpor =
-    let (bpor', bs') = go 0 [] Nothing bs bpor
-    in  if all (M.null . _backtrack) bs'
-        then bpor'
-        else step bs' bpor'
-
-  go tid pref lastb (b:bs) bpor =
-    let (bpor', blocked) = backtrack pref b bpor
-        tid'   = tidOf tid . fst $ _decision b
-        pref'  = pref ++ [_decision b]
-        (child, blocked')  = go tid' pref' (Just b) bs . fromJust $ M.lookup tid' (_bdone bpor)
-        bpor'' = bpor' { _bdone = M.insert tid' child $ _bdone bpor' }
-    in  case lastb of
-         Just b' -> (bpor'', b' { _backtrack = blocked } : blocked')
-         Nothing -> (bpor'', blocked')
-
-  go _ _ (Just b') _ bpor = (bpor, [b' { _backtrack = M.empty }])
-  go _ _ Nothing   _ bpor = (bpor, [])
-
-  backtrack pref b bpor =
-    let todo' = [ x
-                | x@(t,c) <- M.toList $ _backtrack b
-                , let decision  = decisionOf (Just . activeTid $ map fst pref) (_brunnable bpor) t
-                , let lookahead = fromJust . M.lookup t $ _runnable b
-                , bv pref (decision, lookahead)
-                , t `notElem` M.keys (_bdone bpor)
-                , c || M.notMember t (_bsleep bpor)
-                ]
-        (blocked, nxt) = partition (\(t,_) -> t `S.member` _bignore bpor) todo'
-    in  (bpor { _btodo = _btodo bpor `M.union` M.fromList nxt }, M.fromList blocked)
-
--- | Remove commits from the todo sets where every other action will
--- result in a write barrier (and so a commit) occurring.
---
--- To get the benefit from this, do not execute commit actions from
--- the todo set until there are no other choises.
-pruneCommits :: BPOR -> BPOR
-pruneCommits bpor
-  | not onlycommits || not alldonesync = go bpor
-  | otherwise = go bpor { _btodo = M.empty, _bdone = pruneCommits <$> _bdone bpor }
-
-  where
-    go b = b { _bdone = pruneCommits <$> _bdone bpor }
-
-    onlycommits = all (<0) . M.keys $ _btodo bpor
-    alldonesync = all barrier . M.elems $ _bdone bpor
-
-    barrier = isBarrier . simplify . fromJust . _baction
-
--- * Utilities
-
--- | Get the resultant 'ThreadId' of a 'Decision', with a default case
--- for 'Continue'.
-tidOf :: ThreadId -> Decision -> ThreadId
-tidOf _ (Start t)    = t
-tidOf _ (SwitchTo t) = t
-tidOf tid _          = tid
-
--- | Get the 'Decision' that would have resulted in this 'ThreadId',
--- given a prior 'ThreadId' (if any) and list of runnable threads.
-decisionOf :: Maybe ThreadId -> Set ThreadId -> ThreadId -> Decision
-decisionOf prior runnable chosen
-  | prior == Just chosen = Continue
-  | prior `S.member` S.map Just runnable = SwitchTo chosen
-  | otherwise = Start chosen
-
--- | Get the tid of the currently active thread after executing a
--- series of decisions. The list MUST begin with a 'Start'.
-activeTid :: [Decision] -> ThreadId
-activeTid = foldl' tidOf 0
-
--- | Check if an action is dependent on another.
-dependent :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, ThreadAction) -> Bool
-dependent _ _ (_, Lift) (_, Lift) = True
-dependent _ _ (_, ThrowTo t) (t2, a) = t == t2 && a /= Stop
-dependent _ _ (t2, a) (_, ThrowTo t) = t == t2 && a /= Stop
-dependent _ _ (_, STM _) (_, STM _) = True
-dependent _ _ (_, GetNumCapabilities a) (_, SetNumCapabilities b) = a /= b
-dependent _ _ (_, SetNumCapabilities a) (_, GetNumCapabilities b) = a /= b
-dependent _ _ (_, SetNumCapabilities a) (_, SetNumCapabilities b) = a /= b
-dependent memtype buf (_, d1) (_, d2) = dependentActions memtype buf (simplify d1) (simplify d2)
-
--- | Variant of 'dependent' to handle 'ThreadAction''s
-dependent' :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, Lookahead) -> Bool
-dependent' _ _ (_, Lift) (_, WillLift) = True
-dependent' _ _ (_, ThrowTo t) (t2, a)     = t == t2 && a /= WillStop
-dependent' _ _ (t2, a) (_, WillThrowTo t) = t == t2 && a /= Stop
-dependent' _ _ (_, STM _) (_, WillSTM) = True
-dependent' _ _ (_, GetNumCapabilities a) (_, WillSetNumCapabilities b) = a /= b
-dependent' _ _ (_, SetNumCapabilities a) (_, WillGetNumCapabilities)   = True
-dependent' _ _ (_, SetNumCapabilities a) (_, WillSetNumCapabilities b) = a /= b
-dependent' memtype buf (_, d1) (_, d2) = dependentActions memtype buf (simplify d1) (simplify' d2)
-
--- | Check if two 'ActionType's are dependent. Note that this is not
--- sufficient to know if two 'ThreadAction's are dependent, without
--- being so great an over-approximation as to be useless!
-dependentActions :: MemType -> CRState -> ActionType -> ActionType -> Bool
-dependentActions memtype buf a1 a2 = case (a1, a2) of
-  -- Unsynchronised reads and writes are always dependent, even under
-  -- a relaxed memory model, as an unsynchronised write gives rise to
-  -- a commit, which synchronises.
-  (UnsynchronisedRead  r1, UnsynchronisedWrite r2) -> r1 == r2
-  (UnsynchronisedWrite r1, UnsynchronisedRead  r2) -> r1 == r2
-  (UnsynchronisedWrite r1, UnsynchronisedWrite r2) -> r1 == r2
-
-  -- Unsynchronised reads where a memory barrier would flush a
-  -- buffered write
-  (UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered buf r1 && memtype /= SequentialConsistency
-  (_, UnsynchronisedRead r2) | isBarrier a1 -> isBuffered buf r2 && memtype /= SequentialConsistency
-
-  (_, _)
-    -- Two actions on the same CRef where at least one is synchronised
-    | same crefOf && (synchronises a1 (fromJust $ crefOf a1) || synchronises a2 (fromJust $ crefOf a2)) -> True
-    -- Two actions on the same CVar
-    | same cvarOf -> True
-
-  _ -> False
-
-  where
-    same f = isJust (f a1) && f a1 == f a2
-
--- * Keeping track of 'CVar' full/empty states
-
-type CVState = Map CVarId Bool
-
--- | Initial global 'CVar' state
-initialCVState :: CVState
-initialCVState = M.empty
-
--- | Update the 'CVar' state with the action that has just happened.
-updateCVState :: CVState -> ThreadAction -> CVState
-updateCVState cvstate (PutVar  c _) = M.insert c True  cvstate
-updateCVState cvstate (TakeVar c _) = M.insert c False cvstate
-updateCVState cvstate (TryPutVar  c True _) = M.insert c True  cvstate
-updateCVState cvstate (TryTakeVar c True _) = M.insert c False cvstate
-updateCVState cvstate _ = cvstate
-
--- | Check if an action will block.
-willBlock :: CVState -> Lookahead -> Bool
-willBlock cvstate (WillPutVar  c) = M.lookup c cvstate == Just True
-willBlock cvstate (WillTakeVar c) = M.lookup c cvstate == Just False
-willBlock cvstate (WillReadVar c) = M.lookup c cvstate == Just False
-willBlock _ _ = False
-
--- | Check if a list of actions will block safely (without modifying
--- any global state). This allows further lookahead at, say, the
--- 'spawn' of a thread (which always starts with 'KnowsAbout').
-willBlockSafely :: CVState -> [Lookahead] -> Bool
-willBlockSafely cvstate (WillMyThreadId:as) = willBlockSafely cvstate as
-willBlockSafely cvstate (WillNewVar:as)     = willBlockSafely cvstate as
-willBlockSafely cvstate (WillNewRef:as)     = willBlockSafely cvstate as
-willBlockSafely cvstate (WillReturn:as)     = willBlockSafely cvstate as
-willBlockSafely cvstate (WillKnowsAbout:as) = willBlockSafely cvstate as
-willBlockSafely cvstate (WillForgets:as)    = willBlockSafely cvstate as
-willBlockSafely cvstate (WillAllKnown:as)   = willBlockSafely cvstate as
-willBlockSafely cvstate (WillPutVar  c:_) = willBlock cvstate (WillPutVar  c)
-willBlockSafely cvstate (WillTakeVar c:_) = willBlock cvstate (WillTakeVar c)
-willBlockSafely _ _ = False
-
--- * Keeping track of 'CRef' buffer state
-
-data CRState = Known (Map CRefId Bool) | Unknown
-
--- | Initial global 'CRef buffer state.
-initialCRState :: CRState
-initialCRState = Known M.empty
-
--- | 'CRef' buffer state with nothing known.
-unknownCRState :: CRState
-unknownCRState = Unknown
-
--- | Update the 'CRef' buffer state with the action that has just
--- happened.
-updateCRState :: CRState -> ThreadAction -> CRState
-updateCRState Unknown _ = Unknown
-updateCRState (Known crstate) (CommitRef _ r) = Known $ M.delete r crstate
-updateCRState (Known crstate) (WriteRef r) = Known $ M.insert r True crstate
-updateCRState crstate ta
-  | isBarrier $ simplify ta = initialCRState
-  | otherwise = crstate
-
--- | Check if a 'CRef' has a buffered write pending.
---
--- If the state is @Unknown@, this assumes @True@.
-isBuffered :: CRState -> CRefId -> Bool
-isBuffered Unknown _ = True
-isBuffered (Known crstate) r = M.findWithDefault False r crstate
diff --git a/Test/DejaFu/STM.hs b/Test/DejaFu/STM.hs
--- a/Test/DejaFu/STM.hs
+++ b/Test/DejaFu/STM.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE CPP                        #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE RankNTypes                 #-}
 {-# LANGUAGE TypeFamilies               #-}
@@ -13,7 +12,9 @@
 
   -- * Executing Transactions
   , Result(..)
-  , CTVarId
+  , TTrace
+  , TAction(..)
+  , TVarId
   , runTransactionST
   , runTransactionIO
   ) where
@@ -24,15 +25,12 @@
 import Control.Monad.ST (ST)
 import Data.IORef (IORef)
 import Data.STRef (STRef)
+import Test.DejaFu.Deterministic.Internal.Common (TVarId, IdSource, TAction(..), TTrace)
 import Test.DejaFu.Internal
 import Test.DejaFu.STM.Internal
 
 import qualified Control.Monad.STM.Class as C
 
-#if __GLASGOW_HASKELL__ < 710
-import Control.Applicative (Applicative)
-#endif
-
 {-# ANN module ("HLint: ignore Use record patterns" :: String) #-}
 
 newtype STMLike n r a = S { runSTM :: M n r a } deriving (Functor, Applicative, Monad)
@@ -43,7 +41,7 @@
 
 -- | A 'MonadSTM' implementation using @ST@, it encapsulates a single
 -- atomic transaction. The environment, that is, the collection of
--- defined 'CTVar's is implicit, there is no list of them, they exist
+-- defined 'TVar's is implicit, there is no list of them, they exist
 -- purely as references. This makes the types simpler, but means you
 -- can't really get an aggregate of them (if you ever wanted to for
 -- some reason).
@@ -51,51 +49,51 @@
 
 -- | A 'MonadSTM' implementation using @ST@, it encapsulates a single
 -- atomic transaction. The environment, that is, the collection of
--- defined 'CTVar's is implicit, there is no list of them, they exist
+-- defined 'TVar's is implicit, there is no list of them, they exist
 -- purely as references. This makes the types simpler, but means you
 -- can't really get an aggregate of them (if you ever wanted to for
 -- some reason).
 type STMIO = STMLike IO IORef
 
 instance MonadThrow (STMLike n r) where
-  throwM e = toSTM (\_ -> SThrow e)
+  throwM = toSTM . const . SThrow
 
 instance MonadCatch (STMLike n r) where
-  catch stm handler = toSTM (SCatch (runSTM . handler) (runSTM stm))
+  catch (S stm) handler = toSTM (SCatch (runSTM . handler) stm)
 
 instance Monad n => C.MonadSTM (STMLike n r) where
-  type CTVar (STMLike n r) = CTVar r
+  type TVar (STMLike n r) = TVar r
 
-  retry = toSTM (\_ -> SRetry)
+  retry = toSTM (const SRetry)
 
-  orElse a b = toSTM (SOrElse (runSTM a) (runSTM b))
+  orElse (S a) (S b) = toSTM (SOrElse a b)
 
-  newCTVar a = toSTM (SNew a)
+  newTVarN n = toSTM . SNew n
 
-  readCTVar ctvar = toSTM (SRead ctvar)
+  readTVar = toSTM . SRead
 
-  writeCTVar ctvar a = toSTM (\c -> SWrite ctvar a (c ()))
+  writeTVar tvar a = toSTM (\c -> SWrite tvar a (c ()))
 
 -- | Run a transaction in the 'ST' monad, returning the result and new
--- initial 'CTVarId'. If the transaction ended by calling 'retry', any
--- 'CTVar' modifications are undone.
-runTransactionST :: STMST t a -> CTVarId -> ST t (Result a, CTVarId)
+-- initial 'TVarId'. If the transaction ended by calling 'retry', any
+-- 'TVar' modifications are undone.
+runTransactionST :: STMST t a -> IdSource -> ST t (Result a, IdSource, TTrace)
 runTransactionST = runTransactionM fixedST where
   fixedST = refST $ \mb -> cont (\c -> SLift $ c `liftM` mb)
 
 -- | Run a transaction in the 'IO' monad, returning the result and new
--- initial 'CTVarId'. If the transaction ended by calling 'retry', any
--- 'CTVar' modifications are undone.
-runTransactionIO :: STMIO a -> CTVarId -> IO (Result a, CTVarId)
+-- initial 'TVarId'. If the transaction ended by calling 'retry', any
+-- 'TVar' modifications are undone.
+runTransactionIO :: STMIO a -> IdSource -> IO (Result a, IdSource, TTrace)
 runTransactionIO = runTransactionM fixedIO where
   fixedIO = refIO $ \mb -> cont (\c -> SLift $ c `liftM` mb)
 
 -- | Run a transaction in an arbitrary monad.
 runTransactionM :: Monad n
-  => Fixed n r -> STMLike n r a -> CTVarId -> n (Result a, CTVarId)
-runTransactionM ref ma ctvid = do
-  (res, undo, ctvid') <- doTransaction ref (runSTM ma) ctvid
+  => Fixed n r -> STMLike n r a -> IdSource -> n (Result a, IdSource, TTrace)
+runTransactionM ref ma tvid = do
+  (res, undo, tvid', trace) <- doTransaction ref (runSTM ma) tvid
 
   case res of
-    Success _ _ _ -> return (res, ctvid')
-    _ -> undo >> return (res, ctvid)
+    Success _ _ _ -> return (res, tvid', trace)
+    _ -> undo >> return (res, tvid, trace)
diff --git a/Test/DejaFu/STM/Internal.hs b/Test/DejaFu/STM/Internal.hs
--- a/Test/DejaFu/STM/Internal.hs
+++ b/Test/DejaFu/STM/Internal.hs
@@ -1,24 +1,16 @@
-{-# LANGUAGE CPP                       #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE RankNTypes                #-}
-{-# LANGUAGE ScopedTypeVariables       #-}
 
 -- | 'MonadSTM' testing implementation, internal types and
 -- definitions.
 module Test.DejaFu.STM.Internal where
 
-import Control.Exception (Exception, SomeException(..), fromException)
+import Control.Exception (Exception, SomeException, fromException, toException)
 import Control.Monad.Cont (Cont, runCont)
 import Data.List (nub)
-import Data.Maybe (fromMaybe)
-import Data.Typeable (cast)
+import Test.DejaFu.Deterministic.Internal.Common (TVarId, IdSource, TAction(..), TTrace, nextTVId)
 import Test.DejaFu.Internal
 
-#if __GLASGOW_HASKELL__ < 710
-import Data.Foldable (Foldable(..))
-import Data.Monoid (mempty)
-#endif
-
 --------------------------------------------------------------------------------
 -- The @STMLike@ monad
 
@@ -36,40 +28,36 @@
 -- actions.
 data STMAction n r
   = forall a e. Exception e => SCatch (e -> M n r a) (M n r a) (a -> STMAction n r)
-  | forall a. SRead  (CTVar r a) (a -> STMAction n r)
-  | forall a. SWrite (CTVar r a) a (STMAction n r)
+  | forall a. SRead  (TVar r a) (a -> STMAction n r)
+  | forall a. SWrite (TVar r a) a (STMAction n r)
   | forall a. SOrElse (M n r a) (M n r a) (a -> STMAction n r)
-  | forall a. SNew a (CTVar r a -> STMAction n r)
+  | forall a. SNew String a (TVar r a -> STMAction n r)
   | SLift (n (STMAction n r))
   | forall e. Exception e => SThrow e
   | SRetry
   | SStop
 
 --------------------------------------------------------------------------------
--- * @CTVar@s
-
--- | A 'CTVar' is a tuple of a unique ID and the value contained. The
--- ID is so that blocked transactions can be re-run when a 'CTVar'
--- they depend on has changed.
-newtype CTVar r a = CTVar (CTVarId, r a)
+-- * @TVar@s
 
--- | The unique ID of a 'CTVar'. Only meaningful within a single
--- concurrent computation.
-type CTVarId = Int
+-- | A 'TVar' is a tuple of a unique ID and the value contained. The
+-- ID is so that blocked transactions can be re-run when a 'TVar' they
+-- depend on has changed.
+newtype TVar r a = TVar (TVarId, r a)
 
 --------------------------------------------------------------------------------
 -- * Output
 
--- | The result of an STM transaction, along with which 'CTVar's it
+-- | The result of an STM transaction, along with which 'TVar's it
 -- touched whilst executing.
 data Result a =
-    Success [CTVarId] [CTVarId] a
+    Success [TVarId] [TVarId] a
   -- ^ The transaction completed successfully, reading the first list
-  -- 'CTVar's and writing to the second.
-  | Retry   [CTVarId]
+  -- 'TVar's and writing to the second.
+  | Retry [TVarId]
   -- ^ The transaction aborted by calling 'retry', and read the
-  -- returned 'CTVar's. It should be retried when at least one of the
-  -- 'CTVar's has been mutated.
+  -- returned 'TVar's. It should be retried when at least one of the
+  -- 'TVar's has been mutated.
   | Exception SomeException
   -- ^ The transaction aborted by throwing an exception.
   deriving Show
@@ -87,90 +75,94 @@
 -- * Execution
 
 -- | Run a STM transaction, returning an action to undo its effects.
-doTransaction :: Monad n => Fixed n r -> M n r a -> CTVarId -> n (Result a, n (), CTVarId)
-doTransaction fixed ma newctvid = do
+doTransaction :: Monad n => Fixed n r -> M n r a -> IdSource -> n (Result a, n (), IdSource, TTrace)
+doTransaction fixed ma idsource = do
   ref <- newRef fixed Nothing
 
   let c = runCont (ma >>= liftN fixed . writeRef fixed ref . Just . Right) $ const SStop
 
-  (newctvid', undo, readen, written) <- go ref c (return ()) newctvid [] []
+  (idsource', undo, readen, written, trace) <- go ref c (return ()) idsource [] [] []
 
   res <- readRef fixed ref
 
   case res of
-    Just (Right val) -> return (Success (nub readen) (nub written) val, undo, newctvid')
+    Just (Right val) -> return (Success (nub readen) (nub written) val, undo, idsource', reverse trace)
 
-    Just (Left  exc) -> undo >> return (Exception exc,      return (), newctvid)
-    Nothing          -> undo >> return (Retry $ nub readen, return (), newctvid)
+    Just (Left  exc) -> undo >> return (Exception exc,      return (), idsource, reverse trace)
+    Nothing          -> undo >> return (Retry $ nub readen, return (), idsource, reverse trace)
 
   where
-    go ref act undo nctvid readen written = do
-      (act', undo', nctvid', readen', written') <- stepTrans fixed act nctvid
-      let ret = (nctvid', undo >> undo', readen' ++ readen, written' ++ written)
-      case act' of
-        SStop  -> return ret
-        SRetry -> writeRef fixed ref Nothing >> return ret
-        SThrow exc -> writeRef fixed ref (Just . Left $ wrap exc) >> return ret
+    go ref act undo nidsrc readen written sofar = do
+      (act', undo', nidsrc', readen', written', tact) <- stepTrans fixed act nidsrc
 
-        _ -> go ref act' (undo >> undo') nctvid' (readen' ++ readen) (written' ++ written)
+      let newIDSource = nidsrc'
+          newAct = act'
+          newUndo = undo >> undo'
+          newReaden = readen' ++ readen
+          newWritten = written' ++ written
+          newSofar = tact : sofar
 
-    -- | This wraps up an uncaught exception inside a @SomeException@,
-    -- unless it already is a @SomeException@. This is because
-    -- multiple levels of @SomeException@ do not play nicely with
-    -- @fromException@.
-    wrap e = fromMaybe (SomeException e) $ cast e
+      case tact of
+        TStop  -> return (newIDSource, newUndo, newReaden, newWritten, TStop:newSofar)
+        TRetry -> writeRef fixed ref Nothing
+          >> return (newIDSource, newUndo, newReaden, newWritten, TRetry:newSofar)
+        TThrow -> writeRef fixed ref (Just . Left $ case act of SThrow e -> toException e; _ -> undefined)
+          >> return (newIDSource, newUndo, newReaden, newWritten, TThrow:newSofar)
+        _ -> go ref newAct newUndo newIDSource newReaden newWritten newSofar
 
 -- | Run a transaction for one step.
-stepTrans :: Monad n => Fixed n r -> STMAction n r -> CTVarId -> n (STMAction n r, n (), CTVarId, [CTVarId], [CTVarId])
-stepTrans fixed act newctvid = case act of
+stepTrans :: Monad n => Fixed n r -> STMAction n r -> IdSource -> n (STMAction n r, n (), IdSource, [TVarId], [TVarId], TAction)
+stepTrans fixed act idsource = case act of
   SCatch  h stm c -> stepCatch h stm c
   SRead   ref c   -> stepRead ref c
   SWrite  ref a c -> stepWrite ref a c
-  SNew    a c     -> stepNew a c
+  SNew    n a c   -> stepNew n a c
   SOrElse a b c   -> stepOrElse a b c
   SLift   na      -> stepLift na
 
-  halt -> return (halt, nothing, newctvid, [], [])
+  SThrow e -> return (SThrow e, nothing, idsource, [], [], TThrow)
+  SRetry   -> return (SRetry,   nothing, idsource, [], [], TRetry)
+  SStop    -> return (SStop,    nothing, idsource, [], [], TStop)
 
   where
     nothing = return ()
 
-    stepCatch h stm c = onFailure stm c
-      (\readen -> return (SRetry, nothing, newctvid, readen, []))
-      (\exc    -> case fromException exc of
-        Just exc' -> transaction (h exc') c
-        Nothing   -> return (SThrow exc, nothing, newctvid, [], []))
+    stepCatch h stm c = cases TCatch stm c
+      (\trace readen -> return (SRetry, nothing, idsource, readen, [], TCatch trace Nothing))
+      (\trace exc    -> case fromException exc of
+        Just exc' -> transaction (TCatch trace . Just) (h exc') c
+        Nothing   -> return (SThrow exc, nothing, idsource, [], [], TCatch trace Nothing))
 
-    stepRead (CTVar (ctvid, ref)) c = do
+    stepRead (TVar (tvid, ref)) c = do
       val <- readRef fixed ref
-      return (c val, nothing, newctvid, [ctvid], [])
+      return (c val, nothing, idsource, [tvid], [], TRead tvid)
 
-    stepWrite (CTVar (ctvid, ref)) a c = do
+    stepWrite (TVar (tvid, ref)) a c = do
       old <- readRef fixed ref
       writeRef fixed ref a
-      return (c, writeRef fixed ref old, newctvid, [], [ctvid])
+      return (c, writeRef fixed ref old, idsource, [], [tvid], TWrite tvid)
 
-    stepNew a c = do
-      let newctvid' = newctvid + 1
+    stepNew n a c = do
+      let (idsource', tvid) = nextTVId n idsource
       ref <- newRef fixed a
-      let ctvar = CTVar (newctvid, ref)
-      return (c ctvar, nothing, newctvid', [], [newctvid])
+      let tvar = TVar (tvid, ref)
+      return (c tvar, nothing, idsource', [], [tvid], TNew)
 
-    stepOrElse a b c = onFailure a c
-      (\_   -> transaction b c)
-      (\exc -> return (SThrow exc, nothing, newctvid, [], []))
+    stepOrElse a b c = cases TOrElse a c
+      (\trace _   -> transaction (TOrElse trace . Just) b c)
+      (\trace exc -> return (SThrow exc, nothing, idsource, [], [], TOrElse trace Nothing))
 
     stepLift na = do
       a <- na
-      return (a, nothing, newctvid, [], [])
+      return (a, nothing, idsource, [], [], TLift)
 
-    onFailure stm onSuccess onRetry onException = do
-      (res, undo, newctvid') <- doTransaction fixed stm newctvid
+    cases tact stm onSuccess onRetry onException = do
+      (res, undo, idsource', trace) <- doTransaction fixed stm idsource
       case res of
-        Success readen written val -> return (onSuccess val, undo, newctvid', readen, written)
-        Retry readen  -> onRetry readen
-        Exception exc -> onException exc
+        Success readen written val -> return (onSuccess val, undo, idsource', readen, written, tact trace Nothing)
+        Retry readen  -> onRetry     trace readen
+        Exception exc -> onException trace exc
 
-    transaction stm onSuccess = onFailure stm onSuccess
-      (\readen -> return (SRetry, nothing, newctvid, readen, []))
-      (\exc    -> return (SThrow exc, nothing, newctvid, [], []))
+    transaction tact stm onSuccess = cases (\t _ -> tact t) stm onSuccess
+      (\trace readen -> return (SRetry, nothing, idsource, readen, [], tact trace))
+      (\trace exc    -> return (SThrow exc, nothing, idsource, [], [], tact trace))
diff --git a/dejafu.cabal b/dejafu.cabal
--- a/dejafu.cabal
+++ b/dejafu.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                dejafu
-version:             0.2.0.0
+version:             0.3.0.0
 synopsis:            Overloadable primitives for testable, potentially non-deterministic, concurrency.
 
 description:
@@ -75,20 +75,28 @@
 source-repository this
   type:     git
   location: https://github.com/barrucadu/dejafu.git
-  tag:      0.1.0.0
+  tag:      dejafu-0.3.0.0
 
 library
   exposed-modules:     Control.Monad.Conc.Class
                      , Control.Monad.STM.Class
 
-                     , Control.Concurrent.CVar
-                     , Control.Concurrent.CVar.Strict
-                     , Control.Concurrent.STM.CTVar
-                     , Control.Concurrent.STM.CTMVar
+                     , Control.Concurrent.Classy
+                     , Control.Concurrent.Classy.Chan
+                     , Control.Concurrent.Classy.CRef
+                     , Control.Concurrent.Classy.MVar
+                     , Control.Concurrent.Classy.QSem
+                     , Control.Concurrent.Classy.QSemN
+                     , Control.Concurrent.Classy.STM
+                     , Control.Concurrent.Classy.STM.TVar
+                     , Control.Concurrent.Classy.STM.TMVar
+                     , Control.Concurrent.Classy.STM.TChan
+                     , Control.Concurrent.Classy.STM.TQueue
+                     , Control.Concurrent.Classy.STM.TBQueue
+                     , Control.Concurrent.Classy.STM.TArray
 
                      , Test.DejaFu
                      , Test.DejaFu.Deterministic
-                     , Test.DejaFu.Deterministic.Schedule
                      , Test.DejaFu.SCT
                      , Test.DejaFu.STM
 
@@ -97,22 +105,25 @@
                      , Test.DejaFu.Deterministic.Internal.Memory
                      , Test.DejaFu.Deterministic.Internal.Threading
                      , Test.DejaFu.Internal
-                     , Test.DejaFu.SCT.Internal
                      , Test.DejaFu.STM.Internal
-                     , Data.List.Extra
 
   -- other-modules:       
   -- other-extensions:    
   build-depends:       base >=4.5 && <5
+                     , array
                      , atomic-primops
                      , containers
+                     , dpor
                      , deepseq
                      , exceptions >=0.7
+                     , monad-control
                      , monad-loops
                      , mtl
-                     , random
+                     , semigroups
                      , stm
+                     , template-haskell
                      , transformers
+                     , transformers-base
   -- hs-source-dirs:      
   default-language:    Haskell2010
   ghc-options:         -Wall