diff --git a/Test/DejaFu.hs b/Test/DejaFu.hs
--- a/Test/DejaFu.hs
+++ b/Test/DejaFu.hs
@@ -93,13 +93,16 @@
 
   -- * Testing with different settings
 
-  , autocheck'
-  , autocheckIO'
-  , dejafu'
-  , dejafus'
-  , dejafuIO'
-  , dejafusIO'
+  , Way(..)
+  , defaultWay
 
+  , autocheckWay
+  , autocheckWayIO
+  , dejafuWay
+  , dejafuWayIO
+  , dejafusWay
+  , dejafusWayIO
+
   -- ** Memory Models
 
   -- | Threads running under modern multicore processors do not behave
@@ -133,7 +136,7 @@
   --
   -- We can see this by testing with different memory models:
   --
-  -- > > autocheck' SequentialConsistency example2
+  -- > > autocheckWay defaultWay SequentialConsistency example2
   -- > [pass] Never Deadlocks (checked: 6)
   -- > [pass] No Exceptions (checked: 6)
   -- > [fail] Consistent Result (checked: 5)
@@ -145,7 +148,7 @@
   -- >         ...
   -- > False
   --
-  -- > > autocheck' TotalStoreOrder example2
+  -- > > autocheckWay defaultWay TotalStoreOrder example2
   -- > [pass] Never Deadlocks (checked: 303)
   -- > [pass] No Exceptions (checked: 303)
   -- > [fail] Consistent Result (checked: 302)
@@ -202,9 +205,9 @@
   , Result(..)
   , Failure(..)
   , runTest
-  , runTest'
+  , runTestWay
   , runTestM
-  , runTestM'
+  , runTestWayM
 
   -- * Predicates
 
@@ -240,22 +243,22 @@
   ) where
 
 import Control.Arrow (first)
-import Control.DeepSeq (NFData(..))
 import Control.Monad (when, unless)
 import Control.Monad.Ref (MonadRef)
 import Control.Monad.ST (runST)
 import Data.Function (on)
 import Data.List (intercalate, intersperse, minimumBy)
 import Data.Ord (comparing)
+import System.Random (RandomGen, StdGen)
 
 import Test.DejaFu.Common
 import Test.DejaFu.Conc
 import Test.DejaFu.SCT
 
--- | The default memory model: @TotalStoreOrder@
-defaultMemType :: MemType
-defaultMemType = TotalStoreOrder
 
+-------------------------------------------------------------------------------
+-- DejaFu
+
 -- | Automatically test a computation. In particular, look for
 -- deadlocks, uncaught exceptions, and multiple return values.
 --
@@ -266,10 +269,10 @@
   => (forall t. ConcST t a)
   -- ^ The computation to test
   -> IO Bool
-autocheck = autocheck' defaultMemType defaultBounds
+autocheck = autocheckWay defaultWay defaultMemType
 
--- | Variant of 'autocheck' which takes a memor model and schedule
--- bounds.
+-- | Variant of 'autocheck' which takes a way to run the program and a
+-- memory model.
 --
 -- Schedule bounding is used to filter the large number of possible
 -- schedules, and can be iteratively increased for further coverage
@@ -281,26 +284,28 @@
 --
 -- __Warning:__ Using largers bounds will almost certainly
 -- significantly increase the time taken to test!
-autocheck' :: (Eq a, Show a)
-  => MemType
+autocheckWay :: (Eq a, Show a, RandomGen g)
+  => Way g
+  -- ^ How to run the concurrent program.
+  -> MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> Bounds
-  -- ^ The schedule bounds
   -> (forall t. ConcST t a)
   -- ^ The computation to test
   -> IO Bool
-autocheck' memtype cb conc = dejafus' memtype cb conc autocheckCases
+autocheckWay way memtype conc =
+  dejafusWay way memtype conc autocheckCases
 
 -- | Variant of 'autocheck' for computations which do 'IO'.
 autocheckIO :: (Eq a, Show a) => ConcIO a -> IO Bool
-autocheckIO = autocheckIO' defaultMemType defaultBounds
+autocheckIO = autocheckWayIO defaultWay defaultMemType
 
--- | Variant of 'autocheck'' for computations which do 'IO'.
-autocheckIO' :: (Eq a, Show a) => MemType -> Bounds -> ConcIO a -> IO Bool
-autocheckIO' memtype cb concio = dejafusIO' memtype cb concio autocheckCases
+-- | Variant of 'autocheckWay' for computations which do 'IO'.
+autocheckWayIO :: (Eq a, Show a, RandomGen g) => Way g -> MemType -> ConcIO a -> IO Bool
+autocheckWayIO way memtype concio =
+  dejafusWayIO way memtype concio autocheckCases
 
 -- | Predicates for the various autocheck functions.
-autocheckCases :: (Eq a, Show a) => [(String, Predicate a)]
+autocheckCases :: Eq a => [(String, Predicate a)]
 autocheckCases =
   [ ("Never Deadlocks",   representative deadlocksNever)
   , ("No Exceptions",     representative exceptionsNever)
@@ -315,21 +320,21 @@
   -> (String, Predicate a)
   -- ^ The predicate (with a name) to check
   -> IO Bool
-dejafu = dejafu' defaultMemType defaultBounds
+dejafu = dejafuWay defaultWay defaultMemType
 
--- | Variant of 'dejafu'' which takes a memory model and schedule
--- bounds.
-dejafu' :: Show a
-  => MemType
+-- | Variant of 'dejafu' which takes a way to run the program and a
+-- memory model.
+dejafuWay :: (Show a, RandomGen g)
+  => Way g
+  -- ^ How to run the concurrent program.
+  -> MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> Bounds
-  -- ^ The schedule bounds
   -> (forall t. ConcST t a)
   -- ^ The computation to test
   -> (String, Predicate a)
   -- ^ The predicate (with a name) to check
   -> IO Bool
-dejafu' memtype cb conc test = dejafus' memtype cb conc [test]
+dejafuWay way memtype conc test = dejafusWay way memtype conc [test]
 
 -- | Variant of 'dejafu' which takes a collection of predicates to
 -- test, returning 'True' if all pass.
@@ -339,46 +344,49 @@
   -> [(String, Predicate a)]
   -- ^ The list of predicates (with names) to check
   -> IO Bool
-dejafus = dejafus' defaultMemType defaultBounds
+dejafus = dejafusWay defaultWay defaultMemType
 
--- | Variant of 'dejafus' which takes a memory model and schedule
--- bounds.
-dejafus' :: Show a
-  => MemType
+-- | Variant of 'dejafus' which takes a way to run the program and a
+-- memory model.
+dejafusWay :: (Show a, RandomGen g)
+  => Way g
+  -- ^ How to run the concurrent program.
+  -> MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> Bounds
-  -- ^ The schedule bounds.
   -> (forall t. ConcST t a)
   -- ^ The computation to test
   -> [(String, Predicate a)]
   -- ^ The list of predicates (with names) to check
   -> IO Bool
-dejafus' memtype cb conc tests = do
-  let traces = runST (sctBound memtype cb conc)
+dejafusWay way memtype conc tests = do
+  let traces = runST (runSCT way memtype conc)
   results <- mapM (\(name, test) -> doTest name $ test traces) tests
   return $ and results
 
 -- | Variant of 'dejafu' for computations which do 'IO'.
 dejafuIO :: Show a => ConcIO a -> (String, Predicate a) -> IO Bool
-dejafuIO = dejafuIO' defaultMemType defaultBounds
+dejafuIO = dejafuWayIO defaultWay defaultMemType
 
--- | Variant of 'dejafu'' for computations which do 'IO'.
-dejafuIO' :: Show a => MemType -> Bounds -> ConcIO a -> (String, Predicate a) -> IO Bool
-dejafuIO' memtype cb concio test = dejafusIO' memtype cb concio [test]
+-- | Variant of 'dejafuWay' for computations which do 'IO'.
+dejafuWayIO :: (Show a, RandomGen g) => Way g -> MemType -> ConcIO a -> (String, Predicate a) -> IO Bool
+dejafuWayIO way memtype concio test =
+  dejafusWayIO way memtype concio [test]
 
 -- | Variant of 'dejafus' for computations which do 'IO'.
 dejafusIO :: Show a => ConcIO a -> [(String, Predicate a)] -> IO Bool
-dejafusIO = dejafusIO' defaultMemType defaultBounds
+dejafusIO = dejafusWayIO defaultWay defaultMemType
 
--- | Variant of 'dejafus'' for computations which do 'IO'.
-dejafusIO' :: Show a => MemType -> Bounds -> ConcIO a -> [(String, Predicate a)] -> IO Bool
-dejafusIO' memtype cb concio tests = do
-  traces  <- sctBound memtype cb concio
+-- | Variant of 'dejafusWay' for computations which do 'IO'.
+dejafusWayIO :: (Show a, RandomGen g) => Way g -> MemType -> ConcIO a -> [(String, Predicate a)] -> IO Bool
+dejafusWayIO way memtype concio tests = do
+  traces  <- runSCT way memtype concio
   results <- mapM (\(name, test) -> doTest name $ test traces) tests
   return $ and results
 
--- * Test cases
 
+-------------------------------------------------------------------------------
+-- Test cases
+
 -- | The results of a test, including the number of cases checked to
 -- determine the final boolean outcome.
 data Result a = Result
@@ -386,23 +394,20 @@
   -- ^ Whether the test passed or not.
   , _casesChecked :: Int
   -- ^ The number of cases checked.
-  , _failures     :: [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
+  , _failures     :: [(Either Failure a, Trace)]
   -- ^ The failing cases, if any.
   , _failureMsg   :: String
   -- ^ A message to display on failure, if nonempty
   } deriving Show
 
 -- | A failed result, taking the given list of failures.
-defaultFail :: [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] -> Result a
+defaultFail :: [(Either Failure a, Trace)] -> Result a
 defaultFail failures = Result False 0 failures ""
 
 -- | A passed result.
 defaultPass :: Result a
 defaultPass = Result True 0 [] ""
 
-instance NFData a => NFData (Result a) where
-  rnf r = rnf (_pass r, _casesChecked r, _failures r, _failureMsg r)
-
 instance Functor Result where
   fmap f r = r { _failures = map (first $ fmap f) $ _failures r }
 
@@ -417,38 +422,42 @@
   -> (forall t. ConcST t a)
   -- ^ The computation to test
   -> Result a
-runTest test conc = runST (runTestM test conc)
+runTest test conc =
+  runST (runTestM test conc)
 
--- | Variant of 'runTest' which takes a memory model and schedule
--- bounds.
-runTest' ::
-    MemType
+-- | Variant of 'runTest' which takes a way to run the program and a
+-- memory model.
+runTestWay :: RandomGen g
+  => Way g
+  -- ^ How to run the concurrent program.
+  -> MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> Bounds
-  -- ^ The schedule bounds.
   -> Predicate a
   -- ^ The predicate to check
   -> (forall t. ConcST t a)
   -- ^ The computation to test
   -> Result a
-runTest' memtype cb predicate conc =
-  runST (runTestM' memtype cb predicate conc)
+runTestWay way memtype predicate conc =
+  runST (runTestWayM way memtype predicate conc)
 
 -- | Monad-polymorphic variant of 'runTest'.
 runTestM :: MonadRef r n
          => Predicate a -> Conc n r a -> n (Result a)
-runTestM = runTestM' defaultMemType defaultBounds
+runTestM = runTestWayM defaultWay defaultMemType
 
 -- | Monad-polymorphic variant of 'runTest''.
-runTestM' :: MonadRef r n
-          => MemType -> Bounds -> Predicate a -> Conc n r a -> n (Result a)
-runTestM' memtype cb predicate conc = predicate <$> sctBound memtype cb conc
+runTestWayM :: (MonadRef r n, RandomGen g)
+            => Way g -> MemType -> Predicate a -> Conc n r a -> n (Result a)
+runTestWayM way memtype predicate conc =
+  predicate <$> runSCT way memtype conc
 
--- * Predicates
 
+-------------------------------------------------------------------------------
+-- Predicates
+
 -- | A @Predicate@ is a function which collapses a list of results
 -- into a 'Result'.
-type Predicate a = [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] -> Result a
+type Predicate a = [(Either Failure a, Trace)] -> Result a
 
 -- | Reduce the list of failures in a @Predicate@ to one
 -- representative trace for each unique result.
@@ -601,7 +610,54 @@
 gives' :: (Eq a, Show a) => [a] -> Predicate a
 gives' = gives . map Right
 
--- * Internal
+
+-------------------------------------------------------------------------------
+-- Defaults
+
+-- | A default way to execute concurrent programs: systematically
+-- using 'defaultBounds'.
+--
+-- The type parameter is constrained to 'StdGen', even though it is
+-- unused, to avoid ambiguity errors.
+defaultWay :: Way StdGen
+defaultWay = Systematically defaultBounds
+
+-- | The default memory model: @TotalStoreOrder@
+defaultMemType :: MemType
+defaultMemType = TotalStoreOrder
+
+-- | All bounds enabled, using their default values.
+defaultBounds :: Bounds
+defaultBounds = Bounds
+  { boundPreemp = Just defaultPreemptionBound
+  , boundFair   = Just defaultFairBound
+  , boundLength = Just defaultLengthBound
+  }
+
+-- | A sensible default preemption bound: 2.
+--
+-- See /Concurrency Testing Using Schedule Bounding: an Empirical Study/,
+-- P. Thomson, A. F. Donaldson, A. Betts for justification.
+defaultPreemptionBound :: PreemptionBound
+defaultPreemptionBound = 2
+
+-- | A sensible default fair bound: 5.
+--
+-- This comes from playing around myself, but there is probably a
+-- better default.
+defaultFairBound :: FairBound
+defaultFairBound = 5
+
+-- | A sensible default length bound: 250.
+--
+-- Based on the assumption that anything which executes for much
+-- longer (or even this long) will take ages to test.
+defaultLengthBound :: LengthBound
+defaultLengthBound = 250
+
+
+-------------------------------------------------------------------------------
+-- Utils
 
 -- | Run a test and print to stdout
 doTest :: Show a => String -> Result a -> IO Bool
diff --git a/Test/DejaFu/Common.hs b/Test/DejaFu/Common.hs
--- a/Test/DejaFu/Common.hs
+++ b/Test/DejaFu/Common.hs
@@ -60,14 +60,12 @@
   , MemType(..)
   ) where
 
-import Control.DeepSeq (NFData(..))
 import Control.Exception (MaskingState(..))
-import Data.Dynamic (Dynamic)
 import Data.List (sort, nub, intercalate)
+import Data.List.NonEmpty (NonEmpty)
 import Data.Maybe (fromMaybe, mapMaybe)
 import Data.Set (Set)
 import qualified Data.Set as S
-import Test.DPOR (Decision(..), Trace)
 
 -------------------------------------------------------------------------------
 -- Identifiers
@@ -83,9 +81,6 @@
   show (ThreadId (Just n) _) = n
   show (ThreadId Nothing  i) = show i
 
-instance NFData ThreadId where
-  rnf (ThreadId n i) = rnf (n, i)
-
 -- | Every @CRef@ has a unique identifier.
 data CRefId = CRefId (Maybe String) Int
   deriving Eq
@@ -97,9 +92,6 @@
   show (CRefId (Just n) _) = n
   show (CRefId Nothing  i) = show i
 
-instance NFData CRefId where
-  rnf (CRefId n i) = rnf (n, i)
-
 -- | Every @MVar@ has a unique identifier.
 data MVarId = MVarId (Maybe String) Int
   deriving Eq
@@ -111,9 +103,6 @@
   show (MVarId (Just n) _) = n
   show (MVarId Nothing  i) = show i
 
-instance NFData MVarId where
-  rnf (MVarId n i) = rnf (n, i)
-
 -- | Every @TVar@ has a unique identifier.
 data TVarId = TVarId (Maybe String) Int
   deriving Eq
@@ -125,9 +114,6 @@
   show (TVarId (Just n) _) = n
   show (TVarId Nothing  i) = show i
 
-instance NFData TVarId where
-  rnf (TVarId n i) = rnf (n, i)
-
 -- | The ID of the initial thread.
 initialThread :: ThreadId
 initialThread = ThreadId (Just "main") 0
@@ -202,40 +188,42 @@
   -- ^ Set the number of Haskell threads that can run simultaneously.
   | Yield
   -- ^ Yield the current thread.
-  | NewVar MVarId
+  | NewMVar MVarId
   -- ^ Create a new 'MVar'.
-  | PutVar MVarId [ThreadId]
+  | PutMVar MVarId [ThreadId]
   -- ^ Put into a 'MVar', possibly waking up some threads.
-  | BlockedPutVar MVarId
+  | BlockedPutMVar MVarId
   -- ^ Get blocked on a put.
-  | TryPutVar MVarId Bool [ThreadId]
+  | TryPutMVar MVarId Bool [ThreadId]
   -- ^ Try to put into a 'MVar', possibly waking up some threads.
-  | ReadVar MVarId
+  | ReadMVar MVarId
   -- ^ Read from a 'MVar'.
-  | BlockedReadVar MVarId
+  | TryReadMVar MVarId Bool
+  -- ^ Try to read from a 'MVar'.
+  | BlockedReadMVar MVarId
   -- ^ Get blocked on a read.
-  | TakeVar MVarId [ThreadId]
+  | TakeMVar MVarId [ThreadId]
   -- ^ Take from a 'MVar', possibly waking up some threads.
-  | BlockedTakeVar MVarId
+  | BlockedTakeMVar MVarId
   -- ^ Get blocked on a take.
-  | TryTakeVar MVarId Bool [ThreadId]
+  | TryTakeMVar MVarId Bool [ThreadId]
   -- ^ Try to take from a 'MVar', possibly waking up some threads.
-  | NewRef CRefId
+  | NewCRef CRefId
   -- ^ Create a new 'CRef'.
-  | ReadRef CRefId
+  | ReadCRef CRefId
   -- ^ Read from a 'CRef'.
-  | ReadRefCas CRefId
+  | ReadCRefCas CRefId
   -- ^ Read from a 'CRef' for a future compare-and-swap.
-  | ModRef CRefId
+  | ModCRef CRefId
   -- ^ Modify a 'CRef'.
-  | ModRefCas CRefId
+  | ModCRefCas CRefId
   -- ^ Modify a 'CRef' using a compare-and-swap.
-  | WriteRef CRefId
+  | WriteCRef CRefId
   -- ^ Write to a 'CRef' without synchronising.
-  | CasRef CRefId Bool
+  | CasCRef CRefId Bool
   -- ^ Attempt to to a 'CRef' using a compare-and-swap, synchronising
   -- it.
-  | CommitRef ThreadId CRefId
+  | CommitCRef ThreadId CRefId
   -- ^ Commit the last write to the given 'CRef' by the given thread,
   -- so that all threads can see the updated value.
   | STM TTrace [ThreadId]
@@ -268,48 +256,18 @@
   -- 'ConcIO'.
   | Return
   -- ^ A 'return' or 'pure' action was executed.
-  | Message Dynamic
-  -- ^ A '_concMessage' annotation was processed.
   | Stop
   -- ^ Cease execution and terminate.
-  deriving Show
-
-instance NFData ThreadAction where
-  rnf (Fork t) = rnf t
-  rnf (GetNumCapabilities i) = rnf i
-  rnf (SetNumCapabilities i) = rnf i
-  rnf (NewVar c) = rnf c
-  rnf (PutVar c ts) = rnf (c, ts)
-  rnf (BlockedPutVar c) = rnf c
-  rnf (TryPutVar c b ts) = rnf (c, b, ts)
-  rnf (ReadVar c) = rnf c
-  rnf (BlockedReadVar c) = rnf c
-  rnf (TakeVar c ts) = rnf (c, ts)
-  rnf (BlockedTakeVar c) = rnf c
-  rnf (TryTakeVar c b ts) = rnf (c, b, ts)
-  rnf (NewRef c) = rnf c
-  rnf (ReadRef c) = rnf c
-  rnf (ReadRefCas c) = rnf c
-  rnf (ModRef c) = rnf c
-  rnf (ModRefCas c) = rnf c
-  rnf (WriteRef c) = rnf c
-  rnf (CasRef c b) = rnf (c, b)
-  rnf (CommitRef t c) = rnf (t, c)
-  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` ()
+  | Subconcurrency
+  -- ^ Start executing an action with @subconcurrency@.
+  deriving (Eq, Show)
 
 -- | Check if a @ThreadAction@ immediately blocks.
 isBlock :: ThreadAction -> Bool
 isBlock (BlockedThrowTo  _) = True
-isBlock (BlockedTakeVar _) = True
-isBlock (BlockedReadVar _) = True
-isBlock (BlockedPutVar  _) = True
+isBlock (BlockedTakeMVar _) = True
+isBlock (BlockedReadMVar _) = True
+isBlock (BlockedPutMVar  _) = True
 isBlock (BlockedSTM _) = True
 isBlock _ = False
 
@@ -344,34 +302,36 @@
   -- simultaneously.
   | WillYield
   -- ^ Will yield the current thread.
-  | WillNewVar
+  | WillNewMVar
   -- ^ Will create a new 'MVar'.
-  | WillPutVar MVarId
+  | WillPutMVar MVarId
   -- ^ Will put into a 'MVar', possibly waking up some threads.
-  | WillTryPutVar MVarId
+  | WillTryPutMVar MVarId
   -- ^ Will try to put into a 'MVar', possibly waking up some threads.
-  | WillReadVar MVarId
+  | WillReadMVar MVarId
   -- ^ Will read from a 'MVar'.
-  | WillTakeVar MVarId
+  | WillTryReadMVar MVarId
+  -- ^ Will try to read from a 'MVar'.
+  | WillTakeMVar MVarId
   -- ^ Will take from a 'MVar', possibly waking up some threads.
-  | WillTryTakeVar MVarId
+  | WillTryTakeMVar MVarId
   -- ^ Will try to take from a 'MVar', possibly waking up some threads.
-  | WillNewRef
+  | WillNewCRef
   -- ^ Will create a new 'CRef'.
-  | WillReadRef CRefId
+  | WillReadCRef CRefId
   -- ^ Will read from a 'CRef'.
-  | WillReadRefCas CRefId
+  | WillReadCRefCas CRefId
   -- ^ Will read from a 'CRef' for a future compare-and-swap.
-  | WillModRef CRefId
+  | WillModCRef CRefId
   -- ^ Will modify a 'CRef'.
-  | WillModRefCas CRefId
-  -- ^ Will nodify a 'CRef' using a compare-and-swap.
-  | WillWriteRef CRefId
+  | WillModCRefCas CRefId
+  -- ^ Will modify a 'CRef' using a compare-and-swap.
+  | WillWriteCRef CRefId
   -- ^ Will write to a 'CRef' without synchronising.
-  | WillCasRef CRefId
+  | WillCasCRef CRefId
   -- ^ Will attempt to to a 'CRef' using a compare-and-swap,
   -- synchronising it.
-  | WillCommitRef ThreadId CRefId
+  | WillCommitCRef ThreadId CRefId
   -- ^ Will commit the last write by the given thread to the 'CRef'.
   | WillSTM
   -- ^ Will execute an STM transaction, possibly waking up some
@@ -397,31 +357,11 @@
   -- 'ConcIO'.
   | WillReturn
   -- ^ Will execute a 'return' or 'pure' action.
-  | WillMessage Dynamic
-  -- ^ Will process a _concMessage' annotation.
   | WillStop
   -- ^ Will cease execution and terminate.
-  deriving Show
-
-instance NFData Lookahead where
-  rnf (WillSetNumCapabilities i) = rnf i
-  rnf (WillPutVar c) = rnf c
-  rnf (WillTryPutVar c) = rnf c
-  rnf (WillReadVar c) = rnf c
-  rnf (WillTakeVar c) = rnf c
-  rnf (WillTryTakeVar c) = rnf c
-  rnf (WillReadRef c) = rnf c
-  rnf (WillReadRefCas c) = rnf c
-  rnf (WillModRef c) = rnf c
-  rnf (WillModRefCas c) = rnf c
-  rnf (WillWriteRef c) = rnf c
-  rnf (WillCasRef c) = rnf c
-  rnf (WillCommitRef t c) = rnf (t, c)
-  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` ()
+  | WillSubconcurrency
+  -- ^ Will execute an action with @subconcurrency@.
+  deriving (Eq, Show)
 
 -- | Convert a 'ThreadAction' into a 'Lookahead': \"rewind\" what has
 -- happened. 'Killed' has no 'Lookahead' counterpart.
@@ -431,23 +371,24 @@
 rewind (GetNumCapabilities _) = Just WillGetNumCapabilities
 rewind (SetNumCapabilities i) = Just (WillSetNumCapabilities i)
 rewind Yield = Just WillYield
-rewind (NewVar _) = Just WillNewVar
-rewind (PutVar c _) = Just (WillPutVar c)
-rewind (BlockedPutVar c) = Just (WillPutVar c)
-rewind (TryPutVar c _ _) = Just (WillTryPutVar c)
-rewind (ReadVar c) = Just (WillReadVar c)
-rewind (BlockedReadVar c) = Just (WillReadVar c)
-rewind (TakeVar c _) = Just (WillTakeVar c)
-rewind (BlockedTakeVar c) = Just (WillTakeVar c)
-rewind (TryTakeVar c _ _) = Just (WillTryTakeVar c)
-rewind (NewRef _) = Just WillNewRef
-rewind (ReadRef c) = Just (WillReadRef c)
-rewind (ReadRefCas c) = Just (WillReadRefCas c)
-rewind (ModRef c) = Just (WillModRef c)
-rewind (ModRefCas c) = Just (WillModRefCas c)
-rewind (WriteRef c) = Just (WillWriteRef c)
-rewind (CasRef c _) = Just (WillCasRef c)
-rewind (CommitRef t c) = Just (WillCommitRef t c)
+rewind (NewMVar _) = Just WillNewMVar
+rewind (PutMVar c _) = Just (WillPutMVar c)
+rewind (BlockedPutMVar c) = Just (WillPutMVar c)
+rewind (TryPutMVar c _ _) = Just (WillTryPutMVar c)
+rewind (ReadMVar c) = Just (WillReadMVar c)
+rewind (BlockedReadMVar c) = Just (WillReadMVar c)
+rewind (TryReadMVar c _) = Just (WillTryReadMVar c)
+rewind (TakeMVar c _) = Just (WillTakeMVar c)
+rewind (BlockedTakeMVar c) = Just (WillTakeMVar c)
+rewind (TryTakeMVar c _ _) = Just (WillTryTakeMVar c)
+rewind (NewCRef _) = Just WillNewCRef
+rewind (ReadCRef c) = Just (WillReadCRef c)
+rewind (ReadCRefCas c) = Just (WillReadCRefCas c)
+rewind (ModCRef c) = Just (WillModCRef c)
+rewind (ModCRefCas c) = Just (WillModCRefCas c)
+rewind (WriteCRef c) = Just (WillWriteCRef c)
+rewind (CasCRef c _) = Just (WillCasCRef c)
+rewind (CommitCRef t c) = Just (WillCommitCRef t c)
 rewind (STM _ _) = Just WillSTM
 rewind (BlockedSTM _) = Just WillSTM
 rewind Catching = Just WillCatching
@@ -460,18 +401,17 @@
 rewind (ResetMasking b m) = Just (WillResetMasking b m)
 rewind LiftIO = Just WillLiftIO
 rewind Return = Just WillReturn
-rewind (Message m) = Just (WillMessage m)
 rewind Stop = Just WillStop
+rewind Subconcurrency = Just WillSubconcurrency
 
 -- | Check if an operation could enable another thread.
 willRelease :: Lookahead -> Bool
 willRelease WillFork = True
 willRelease WillYield = True
-willRelease (WillPutVar _) = True
-willRelease (WillTryPutVar _) = True
-willRelease (WillReadVar _) = True
-willRelease (WillTakeVar _) = True
-willRelease (WillTryTakeVar _) = True
+willRelease (WillPutMVar _) = True
+willRelease (WillTryPutMVar _) = True
+willRelease (WillTakeMVar _) = True
+willRelease (WillTryTakeMVar _) = True
 willRelease WillSTM = True
 willRelease WillThrow = True
 willRelease (WillSetMasking _ _) = True
@@ -508,17 +448,6 @@
   -- communication.
   deriving (Eq, Show)
 
-instance NFData ActionType where
-  rnf (UnsynchronisedRead  r) = rnf r
-  rnf (UnsynchronisedWrite r) = rnf r
-  rnf (PartiallySynchronisedCommit r) = rnf r
-  rnf (PartiallySynchronisedWrite  r) = rnf r
-  rnf (PartiallySynchronisedModify  r) = rnf r
-  rnf (SynchronisedModify  r) = rnf r
-  rnf (SynchronisedRead    c) = rnf c
-  rnf (SynchronisedWrite   c) = rnf c
-  rnf a = a `seq` ()
-
 -- | Check if an action imposes a write barrier.
 isBarrier :: ActionType -> Bool
 isBarrier (SynchronisedModify _) = True
@@ -564,18 +493,19 @@
 
 -- | Variant of 'simplifyAction' that takes a 'Lookahead'.
 simplifyLookahead :: Lookahead -> ActionType
-simplifyLookahead (WillPutVar c)     = SynchronisedWrite c
-simplifyLookahead (WillTryPutVar c)  = SynchronisedWrite c
-simplifyLookahead (WillReadVar c)    = SynchronisedRead c
-simplifyLookahead (WillTakeVar c)    = SynchronisedRead c
-simplifyLookahead (WillTryTakeVar c) = SynchronisedRead c
-simplifyLookahead (WillReadRef r)     = UnsynchronisedRead r
-simplifyLookahead (WillReadRefCas r)  = UnsynchronisedRead r
-simplifyLookahead (WillModRef r)      = SynchronisedModify r
-simplifyLookahead (WillModRefCas r)   = PartiallySynchronisedModify r
-simplifyLookahead (WillWriteRef r)    = UnsynchronisedWrite r
-simplifyLookahead (WillCasRef r)      = PartiallySynchronisedWrite r
-simplifyLookahead (WillCommitRef _ r) = PartiallySynchronisedCommit r
+simplifyLookahead (WillPutMVar c)     = SynchronisedWrite c
+simplifyLookahead (WillTryPutMVar c)  = SynchronisedWrite c
+simplifyLookahead (WillReadMVar c)    = SynchronisedRead c
+simplifyLookahead (WillTryReadMVar c) = SynchronisedRead c
+simplifyLookahead (WillTakeMVar c)    = SynchronisedRead c
+simplifyLookahead (WillTryTakeMVar c)  = SynchronisedRead c
+simplifyLookahead (WillReadCRef r)     = UnsynchronisedRead r
+simplifyLookahead (WillReadCRefCas r)  = UnsynchronisedRead r
+simplifyLookahead (WillModCRef r)      = SynchronisedModify r
+simplifyLookahead (WillModCRefCas r)   = PartiallySynchronisedModify r
+simplifyLookahead (WillWriteCRef r)    = UnsynchronisedWrite r
+simplifyLookahead (WillCasCRef r)      = PartiallySynchronisedWrite r
+simplifyLookahead (WillCommitCRef _ r) = PartiallySynchronisedCommit r
 simplifyLookahead WillSTM         = SynchronisedOther
 simplifyLookahead (WillThrowTo _) = SynchronisedOther
 simplifyLookahead _ = UnsynchronisedOther
@@ -611,22 +541,34 @@
   -- ^ Terminate successfully and commit effects.
   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` ()
-
 -------------------------------------------------------------------------------
 -- Traces
 
+-- | One of the outputs of the runner is a @Trace@, which is a log of
+-- decisions made, all the runnable threads and what they would do,
+-- and the action a thread took in its step.
+type Trace
+  = [(Decision, [(ThreadId, NonEmpty Lookahead)], ThreadAction)]
+
+-- | 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.
+  deriving (Eq, Show)
+
 -- | Pretty-print a trace, including a key of the thread IDs (not
 -- including thread 0). Each line of the key is indented by two
 -- spaces.
-showTrace :: Trace ThreadId ThreadAction Lookahead -> String
+showTrace :: Trace -> String
 showTrace trc = intercalate "\n" $ concatMap go trc : strkey where
-  go (_,_,CommitRef _ _) = "C-"
+  go (_,_,CommitCRef _ _) = "C-"
   go (Start    (ThreadId _ i),_,_) = "S" ++ show i ++ "-"
   go (SwitchTo (ThreadId _ i),_,_) = "P" ++ show i ++ "-"
   go (Continue,_,_) = "-"
@@ -648,18 +590,18 @@
 -- SO, we don't count a switch TO a commit thread as a
 -- preemption. HOWEVER, the switch FROM a commit thread counts as a
 -- preemption if it is not to the thread that the commit interrupted.
-preEmpCount :: [(Decision ThreadId, ThreadAction)]
-            -> (Decision ThreadId, Lookahead)
+preEmpCount :: [(Decision, ThreadAction)]
+            -> (Decision, Lookahead)
             -> Int
-preEmpCount ts (d, _) = go initialThread Nothing ts where
-  go _ (Just Yield) ((SwitchTo t, a):rest) = go t (Just a) rest
-  go tid prior ((SwitchTo t, a):rest)
+preEmpCount (x:xs) (d, _) = go initialThread x xs where
+  go _ (_, Yield) (r@(SwitchTo t, _):rest) = go t r rest
+  go tid prior (r@(SwitchTo t, _):rest)
     | isCommitThread t = go tid prior (skip rest)
-    | otherwise = 1 + go t (Just a) rest
-  go _   _ ((Start t,  a):rest) = go t   (Just a) rest
-  go tid _ ((Continue, a):rest) = go tid (Just a) rest
+    | otherwise = 1 + go t r rest
+  go _   _ (r@(Start t,  _):rest) = go t   r rest
+  go tid _ (r@(Continue, _):rest) = go tid r rest
   go _ prior [] = case (prior, d) of
-    (Just Yield, SwitchTo _) -> 0
+    ((_, Yield), SwitchTo _) -> 0
     (_, SwitchTo _) -> 1
     _ -> 0
 
@@ -670,6 +612,7 @@
   skip = dropWhile (not . isContextSwitch . fst)
   isContextSwitch Continue = False
   isContextSwitch _ = True
+preEmpCount [] _ = 0
 
 -------------------------------------------------------------------------------
 -- Failures
@@ -692,18 +635,19 @@
   -- ^ The computation became blocked indefinitely on @TVar@s.
   | UncaughtException
   -- ^ An uncaught exception bubbled to the top of the computation.
+  | IllegalSubconcurrency
+  -- ^ Calls to @subconcurrency@ were nested, or attempted when
+  -- multiple threads existed.
   deriving (Eq, Show, Read, Ord, Enum, Bounded)
 
-instance NFData Failure where
-  rnf f = f `seq` ()
-
 -- | Pretty-print a failure
 showFail :: Failure -> String
-showFail Abort             = "[abort]"
-showFail Deadlock          = "[deadlock]"
-showFail STMDeadlock       = "[stm-deadlock]"
-showFail InternalError     = "[internal-error]"
+showFail Abort = "[abort]"
+showFail Deadlock = "[deadlock]"
+showFail STMDeadlock = "[stm-deadlock]"
+showFail InternalError = "[internal-error]"
 showFail UncaughtException = "[exception]"
+showFail IllegalSubconcurrency = "[illegal-subconcurrency]"
 
 -------------------------------------------------------------------------------
 -- Memory Models
@@ -726,9 +670,6 @@
   -- are not necessarily committed in the same order that they are
   -- created.
   deriving (Eq, Show, Read, Ord, Enum, Bounded)
-
-instance NFData MemType where
-  rnf m = m `seq` ()
 
 -------------------------------------------------------------------------------
 -- Utilities
diff --git a/Test/DejaFu/Conc.hs b/Test/DejaFu/Conc.hs
--- a/Test/DejaFu/Conc.hs
+++ b/Test/DejaFu/Conc.hs
@@ -28,6 +28,7 @@
   , Failure(..)
   , MemType(..)
   , runConcurrent
+  , subconcurrency
 
   -- * Execution traces
   , Trace
@@ -42,33 +43,30 @@
   , showFail
 
   -- * Scheduling
-  , module Test.DPOR.Schedule
+  , module Test.DejaFu.Schedule
   ) where
 
 import Control.Exception (MaskingState(..))
 import qualified Control.Monad.Base as Ba
 import qualified Control.Monad.Catch as Ca
 import qualified Control.Monad.IO.Class as IO
-import Control.Monad.Ref (MonadRef, newRef, readRef, writeRef)
+import Control.Monad.Ref (MonadRef,)
 import Control.Monad.ST (ST)
-import Data.Dynamic (toDyn)
+import qualified Data.Foldable as F
 import Data.IORef (IORef)
-import qualified Data.Map.Strict as M
-import Data.Maybe (fromJust)
 import Data.STRef (STRef)
-import Test.DPOR.Schedule
+import Test.DejaFu.Schedule
 
 import qualified Control.Monad.Conc.Class as C
 import Test.DejaFu.Common
 import Test.DejaFu.Conc.Internal
 import Test.DejaFu.Conc.Internal.Common
-import Test.DejaFu.Conc.Internal.Threading
 import Test.DejaFu.STM
 
 {-# ANN module ("HLint: ignore Avoid lambda" :: String) #-}
 {-# ANN module ("HLint: ignore Use const"    :: String) #-}
 
-newtype Conc n r a = C { unC :: M n r (STMLike n r) a } deriving (Functor, Applicative, Monad)
+newtype Conc n r a = C { unC :: M n r a } deriving (Functor, Applicative, Monad)
 
 -- | A 'MonadConc' implementation using @ST@, this should be preferred
 -- if you do not need 'liftIO'.
@@ -77,10 +75,10 @@
 -- | A 'MonadConc' implementation using @IO@.
 type ConcIO = Conc IO IORef
 
-toConc :: ((a -> Action n r (STMLike n r)) -> Action n r (STMLike n r)) -> Conc n r a
+toConc :: ((a -> Action n r) -> Action n r) -> Conc n r a
 toConc = C . cont
 
-wrap :: (M n r (STMLike n r) a -> M n r (STMLike n r) a) -> Conc n r a -> Conc n r a
+wrap :: (M n r a -> M n r a) -> Conc n r a -> Conc n r a
 wrap f = C . f . unC
 
 instance IO.MonadIO ConcIO where
@@ -123,29 +121,30 @@
 
   -- ----------
 
-  newCRefN n a = toConc (\c -> ANewRef n a c)
+  newCRefN n a = toConc (\c -> ANewCRef n a c)
 
-  readCRef   ref = toConc (AReadRef    ref)
-  readForCAS ref = toConc (AReadRefCas ref)
+  readCRef   ref = toConc (AReadCRef    ref)
+  readForCAS ref = toConc (AReadCRefCas ref)
 
   peekTicket' _ = _ticketVal
 
-  writeCRef ref      a = toConc (\c -> AWriteRef ref a (c ()))
-  casCRef   ref tick a = toConc (ACasRef ref tick a)
+  writeCRef ref      a = toConc (\c -> AWriteCRef ref a (c ()))
+  casCRef   ref tick a = toConc (ACasCRef ref tick a)
 
-  atomicModifyCRef ref f = toConc (AModRef    ref f)
-  modifyCRefCAS    ref f = toConc (AModRefCas ref f)
+  atomicModifyCRef ref f = toConc (AModCRef    ref f)
+  modifyCRefCAS    ref f = toConc (AModCRefCas ref f)
 
   -- ----------
 
-  newEmptyMVarN n = toConc (\c -> ANewVar n c)
+  newEmptyMVarN n = toConc (\c -> ANewMVar n c)
 
-  putMVar  var a = toConc (\c -> APutVar var a (c ()))
-  readMVar var   = toConc (AReadVar var)
-  takeMVar var   = toConc (ATakeVar var)
+  putMVar  var a = toConc (\c -> APutMVar var a (c ()))
+  readMVar var   = toConc (AReadMVar var)
+  takeMVar var   = toConc (ATakeMVar var)
 
-  tryPutMVar  var a = toConc (ATryPutVar  var a)
-  tryTakeMVar var   = toConc (ATryTakeVar var)
+  tryPutMVar  var a = toConc (ATryPutMVar  var a)
+  tryReadMVar var   = toConc (ATryReadMVar var)
+  tryTakeMVar var   = toConc (ATryTakeMVar var)
 
   -- ----------
 
@@ -155,10 +154,6 @@
 
   atomically = toConc . AAtom
 
-  -- ----------
-
-  _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.
@@ -176,25 +171,20 @@
 -- nonexistent thread. In either of those cases, the computation will
 -- be halted.
 runConcurrent :: MonadRef r n
-              => Scheduler ThreadId ThreadAction Lookahead s
+              => Scheduler s
               -> MemType
               -> s
               -> Conc n r a
-              -> n (Either Failure a, s, Trace ThreadId ThreadAction Lookahead)
-runConcurrent sched memtype s (C conc) = do
-  ref <- newRef Nothing
-
-  let c = runCont conc (AStop . writeRef ref . Just . Right)
-  let threads = launch' Unmasked initialThread (const c) M.empty
-
-  (s', trace) <- runThreads runTransaction
-                           sched
-                           memtype
-                           s
-                           threads
-                           initialIdSource
-                           ref
-
-  out <- readRef ref
+              -> n (Either Failure a, s, Trace)
+runConcurrent sched memtype s ma = do
+  (res, s', trace) <- runConcurrency sched memtype s (unC ma)
+  pure (res, s', F.toList trace)
 
-  pure (fromJust out, s', reverse trace)
+-- | Run a concurrent computation and return its result.
+--
+-- This can only be called in the main thread, when no other threads
+-- exist. Calls to 'subconcurrency' cannot be nested. Violating either
+-- of these conditions will result in the computation failing with
+-- @IllegalSubconcurrency@.
+subconcurrency :: Conc n r a -> Conc n r (Either Failure a)
+subconcurrency ma = toConc (ASub (unC ma))
diff --git a/Test/DejaFu/Conc/Internal.hs b/Test/DejaFu/Conc/Internal.hs
--- a/Test/DejaFu/Conc/Internal.hs
+++ b/Test/DejaFu/Conc/Internal.hs
@@ -16,19 +16,23 @@
 module Test.DejaFu.Conc.Internal where
 
 import Control.Exception (MaskingState(..), toException)
-import Control.Monad.Ref (MonadRef, newRef, writeRef)
+import Control.Monad.Ref (MonadRef, newRef, readRef, writeRef)
+import qualified Data.Foldable as F
 import Data.Functor (void)
 import Data.List (sort)
 import Data.List.NonEmpty (NonEmpty(..), fromList)
 import qualified Data.Map.Strict as M
-import Data.Maybe (fromJust, isJust, isNothing, listToMaybe)
-import Test.DPOR (Scheduler)
+import Data.Maybe (fromJust, isJust, isNothing)
+import Data.Monoid ((<>))
+import Data.Sequence (Seq, (<|))
+import qualified Data.Sequence as Seq
 
 import Test.DejaFu.Common
 import Test.DejaFu.Conc.Internal.Common
 import Test.DejaFu.Conc.Internal.Memory
 import Test.DejaFu.Conc.Internal.Threading
-import Test.DejaFu.STM (Result(..))
+import Test.DejaFu.Schedule
+import Test.DejaFu.STM (Result(..), runTransaction)
 
 {-# ANN module ("HLint: ignore Use record patterns" :: String) #-}
 {-# ANN module ("HLint: ignore Use const"           :: String) #-}
@@ -36,40 +40,69 @@
 --------------------------------------------------------------------------------
 -- * Execution
 
+-- | 'Trace' but as a sequence.
+type SeqTrace
+  = Seq (Decision, [(ThreadId, NonEmpty Lookahead)], ThreadAction)
+
+-- | 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.
+runConcurrency :: MonadRef r n
+               => Scheduler g
+               -> MemType
+               -> g
+               -> M n r a
+               -> n (Either Failure a, g, SeqTrace)
+runConcurrency sched memtype g ma = do
+  ref <- newRef Nothing
+
+  let c = runCont ma (AStop . writeRef ref . Just . Right)
+  let threads = launch' Unmasked initialThread (const c) M.empty
+  let ctx = Context { cSchedState = g, cIdSource = initialIdSource, cThreads = threads, cWriteBuf = emptyBuffer, cCaps = 2 }
+
+  (finalCtx, trace) <- runThreads sched memtype ref ctx
+  out <- readRef ref
+  pure (fromJust out, cSchedState finalCtx, trace)
+
+-- | The context a collection of threads are running in.
+data Context n r g = Context
+  { cSchedState :: g
+  , cIdSource   :: IdSource
+  , cThreads    :: Threads n r
+  , cWriteBuf   :: WriteBuffer r
+  , cCaps       :: Int
+  }
+
 -- | Run a collection of threads, until there are no threads left.
---
--- Note: this returns the trace in reverse order, because it's more
--- 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 :: MonadRef r n => (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, Trace ThreadId ThreadAction Lookahead)
-runThreads 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
-    | isDeadlocked  = die g Deadlock
-    | isSTMLocked   = die g STMDeadlock
-    | isAborted     = die g' Abort
-    | isNonexistant = die g' InternalError
-    | isBlocked     = die g' InternalError
+runThreads :: MonadRef r n
+           => Scheduler g -> MemType -> r (Maybe (Either Failure a)) -> Context n r g -> n (Context n r g, SeqTrace)
+runThreads sched memtype ref = go Seq.empty [] Nothing where
+  -- sofar is the 'SeqTrace', sofarSched is the @[(Decision,
+  -- ThreadAction)]@ trace the scheduler needs.
+  go sofar sofarSched prior ctx
+    | isTerminated  = stop ctx
+    | isDeadlocked  = die Deadlock ctx
+    | isSTMLocked   = die STMDeadlock ctx
+    | isAborted     = die Abort $ ctx { cSchedState = g' }
+    | isNonexistant = die InternalError $ ctx { cSchedState = g' }
+    | isBlocked     = die InternalError $ ctx { cSchedState = g' }
     | otherwise = do
-      stepped <- stepThread runstm memtype (_continuation $ fromJust thread) idSource chosen threads wb caps
+      stepped <- stepThread sched memtype chosen (_continuation $ fromJust thread) $ ctx { cSchedState = g' }
       case stepped of
-        Right (threads', idSource', act, wb', caps') -> loop threads' idSource' act wb' caps'
-
+        Right (ctx', actOrTrc) -> loop actOrTrc ctx'
         Left UncaughtException
-          | chosen == initialThread -> die g' UncaughtException
-          | otherwise -> loop (kill chosen threads) idSource Killed wb caps
-
-        Left failure -> die g' failure
+          | chosen == initialThread -> die UncaughtException $ ctx { cSchedState = g' }
+          | otherwise -> loop (Right Killed) $ ctx { cThreads = kill chosen threadsc, cSchedState = g' }
+        Left failure -> die failure $ ctx { cSchedState = g' }
 
     where
-      (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
+      (choice, g')  = sched sofarSched prior (fromList $ map (\(t,l:|_) -> (t,l)) runnable') (cSchedState ctx)
       chosen        = fromJust choice
       runnable'     = [(t, nextActions t) | t <- sort $ M.keys runnable]
       runnable      = M.filter (isNothing . _blocking) threadsc
       thread        = M.lookup chosen threadsc
-      threadsc      = addCommitThreads wb threads
+      threadsc      = addCommitThreads (cWriteBuf ctx) threads
+      threads       = cThreads ctx
       isAborted     = isNothing choice
       isBlocked     = isJust . _blocking $ fromJust thread
       isNonexistant = isNothing thread
@@ -87,299 +120,265 @@
           _ -> thrd
 
       decision
-        | Just chosen == prior = Continue
-        | prior `notElem` map (Just . fst) runnable' = Start chosen
+        | Just chosen == (fst <$> prior) = Continue
+        | (fst <$> prior) `notElem` map (Just . fst) runnable' = Start chosen
         | otherwise = SwitchTo chosen
 
       nextActions t = lookahead . _continuation . fromJust $ M.lookup t threadsc
 
-      stop outg = pure (outg, sofar)
-      die  outg reason = writeRef ref (Just $ Left reason) >> stop outg
+      stop finalCtx = pure (finalCtx, sofar)
+      die reason finalCtx = writeRef ref (Just $ Left reason) >> stop finalCtx
 
-      loop threads' idSource' act wb' =
-        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'
+      loop trcOrAct ctx' =
+        let (act, trc) = case trcOrAct of
+              Left (a, as) -> (a, (decision, runnable', a) <| as)
+              Right a      -> (a, Seq.singleton (decision, runnable', a))
+            threads' = if (interruptible <$> M.lookup chosen (cThreads ctx')) /= Just False
+                       then unblockWaitingOn chosen (cThreads ctx')
+                       else cThreads ctx'
+            sofar' = sofar <> trc
+            sofarSched' = sofarSched <> map (\(d,_,a) -> (d,a)) (F.toList trc)
+            prior' = Just (chosen, act)
+        in go sofar' sofarSched' prior' $ ctx' { cThreads = delCommitThreads threads' }
 
 --------------------------------------------------------------------------------
 -- * Single-step execution
 
 -- | Run a single thread one step, by dispatching on the type of
 -- 'Action'.
-stepThread :: forall n r s. MonadRef r n
-  => (forall x. s x -> IdSource -> n (Result x, IdSource, TTrace))
-  -- ^ Run a 'MonadSTM' transaction atomically.
+stepThread :: forall n r g. MonadRef r n
+  => Scheduler g
+  -- ^ The scheduler.
   -> MemType
-  -- ^ The memory model
-  -> Action n r s
-  -- ^ Action to step
-  -> IdSource
-  -- ^ Source of fresh IDs
+  -- ^ The memory model to use.
   -> ThreadId
   -- ^ ID of the current thread
-  -> Threads n r s
-  -- ^ Current state of threads
-  -> WriteBuffer r
-  -- ^ @CRef@ write buffer
-  -> Int
-  -- ^ The number of capabilities
-  -> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int))
-stepThread runstm memtype action idSource tid threads wb caps = case action of
-  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  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  n a c   -> stepNewRef      n a c
-  AReadRef ref c   -> stepReadRef     ref c
-  AReadRefCas ref c -> stepReadRefCas ref c
-  AModRef  ref f c -> stepModRef      ref f c
-  AModRefCas ref f c -> stepModRefCas ref f c
-  AWriteRef ref a c -> stepWriteRef   ref a c
-  ACasRef ref tick a c -> stepCasRef ref tick a c
-  ACommit  t c     -> stepCommit      t c
-  AAtom    stm c   -> stepAtom        stm c
-  ALift    na      -> stepLift        na
-  AThrow   e       -> stepThrow       e
-  AThrowTo t e c   -> stepThrowTo     t e c
-  ACatching h ma c -> stepCatching    h ma c
-  APopCatching a   -> stepPopCatching a
-  AMasking m ma c  -> stepMasking     m ma c
-  AResetMask b1 b2 m c -> stepResetMask b1 b2 m c
-  AReturn     c    -> stepReturn c
-  AMessage    m c  -> stepMessage m c
-  AStop       na   -> stepStop na
+  -> Action n r
+  -- ^ Action to step
+  -> Context n r g
+  -- ^ The execution context.
+  -> n (Either Failure (Context n r g, Either (ThreadAction, SeqTrace) ThreadAction))
+stepThread sched memtype tid action ctx = case action of
+    -- start a new thread, assigning it the next 'ThreadId'
+    AFork n a b -> pure . Right $
+        let threads' = launch tid newtid a (cThreads ctx)
+            (idSource', newtid) = nextTId n (cIdSource ctx)
+        in (ctx { cThreads = goto (b newtid) tid threads', cIdSource = idSource' }, Right (Fork newtid))
 
-  where
-    -- | Start a new thread, assigning it the next 'ThreadId'
-    --
-    -- Explicit type signature needed for GHC 8. Looks like the
-    -- impredicative polymorphism checks got stronger.
-    stepFork :: String
-             -> ((forall b. M n r s b -> M n r s b) -> Action n r s)
-             -> (ThreadId -> Action n r s)
-             -> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int))
-    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 n idSource
+    -- get the 'ThreadId' of the current thread
+    AMyTId c -> simple (goto (c tid) tid (cThreads ctx)) MyThreadId
 
-    -- | Get the 'ThreadId' of the current thread
-    stepMyTId c = simple (goto (c tid) tid threads) MyThreadId
+    -- get the number of capabilities
+    AGetNumCapabilities c -> simple (goto (c (cCaps ctx)) tid (cThreads ctx)) $ GetNumCapabilities (cCaps ctx)
 
-    -- | Get the number of capabilities
-    stepGetNumCapabilities c = simple (goto (c caps) tid threads) $ GetNumCapabilities caps
+    -- set the number of capabilities
+    ASetNumCapabilities i c -> pure . Right $
+      (ctx { cThreads = goto c tid (cThreads ctx), cCaps = i }, Right (SetNumCapabilities i))
 
-    -- | Set the number of capabilities
-    stepSetNumCapabilities i c = return $ Right (goto c tid threads, idSource, SetNumCapabilities i, wb, i)
+    -- yield the current thread
+    AYield c -> simple (goto c tid (cThreads ctx)) Yield
 
-    -- | Yield the current thread
-    stepYield c = simple (goto c tid threads) Yield
+    -- create a new @MVar@, using the next 'MVarId'.
+    ANewMVar n c -> do
+      let (idSource', newmvid) = nextMVId n (cIdSource ctx)
+      ref <- newRef Nothing
+      let mvar = MVar newmvid ref
+      pure $ Right (ctx { cThreads = goto (c mvar) tid (cThreads ctx), cIdSource = idSource' }, Right (NewMVar newmvid))
 
-    -- | Put a value into a @MVar@, blocking the thread until it's
-    -- empty.
-    stepPutVar cvar@(MVar cvid _) a c = synchronised $ do
-      (success, threads', woken) <- putIntoMVar cvar a c tid threads
-      simple threads' $ if success then PutVar cvid woken else BlockedPutVar cvid
+    -- put a value into a @MVar@, blocking the thread until it's empty.
+    APutMVar cvar@(MVar cvid _) a c -> synchronised $ do
+      (success, threads', woken) <- putIntoMVar cvar a c tid (cThreads ctx)
+      simple threads' $ if success then PutMVar cvid woken else BlockedPutMVar cvid
 
-    -- | 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 tid threads
-      simple threads' $ TryPutVar cvid success woken
+    -- try to put a value into a @MVar@, without blocking.
+    ATryPutMVar cvar@(MVar cvid _) a c -> synchronised $ do
+      (success, threads', woken) <- tryPutIntoMVar cvar a c tid (cThreads ctx)
+      simple threads' $ TryPutMVar cvid success woken
 
-    -- | Get the value from a @MVar@, without emptying, blocking the
+    -- get the value from a @MVar@, without emptying, blocking the
     -- thread until it's full.
-    stepReadVar cvar@(MVar cvid _) c = synchronised $ do
-      (success, threads', _) <- readFromMVar cvar c tid threads
-      simple threads' $ if success then ReadVar cvid else BlockedReadVar cvid
+    AReadMVar cvar@(MVar cvid _) c -> synchronised $ do
+      (success, threads', _) <- readFromMVar cvar c tid (cThreads ctx)
+      simple threads' $ if success then ReadMVar cvid else BlockedReadMVar cvid
 
-    -- | Take the value from a @MVar@, blocking the thread until it's
+    -- try to get the value from a @MVar@, without emptying, without
+    -- blocking.
+    ATryReadMVar cvar@(MVar cvid _) c -> synchronised $ do
+      (success, threads', _) <- tryReadFromMVar cvar c tid (cThreads ctx)
+      simple threads' $ TryReadMVar cvid success
+
+    -- take the value from a @MVar@, blocking the thread until it's
     -- full.
-    stepTakeVar cvar@(MVar cvid _) c = synchronised $ do
-      (success, threads', woken) <- takeFromMVar cvar c tid threads
-      simple threads' $ if success then TakeVar cvid woken else BlockedTakeVar cvid
+    ATakeMVar cvar@(MVar cvid _) c -> synchronised $ do
+      (success, threads', woken) <- takeFromMVar cvar c tid (cThreads ctx)
+      simple threads' $ if success then TakeMVar cvid woken else BlockedTakeMVar cvid
 
-    -- | Try to take the value from a @MVar@, without blocking.
-    stepTryTakeVar cvar@(MVar cvid _) c = synchronised $ do
-      (success, threads', woken) <- tryTakeFromMVar cvar c tid threads
-      simple threads' $ TryTakeVar cvid success woken
+    -- try to take the value from a @MVar@, without blocking.
+    ATryTakeMVar cvar@(MVar cvid _) c -> synchronised $ do
+      (success, threads', woken) <- tryTakeFromMVar cvar c tid (cThreads ctx)
+      simple threads' $ TryTakeMVar cvid success woken
 
-    -- | Read from a @CRef@.
-    stepReadRef cref@(CRef crid _) c = do
+    -- create a new @CRef@, using the next 'CRefId'.
+    ANewCRef n a c -> do
+      let (idSource', newcrid) = nextCRId n (cIdSource ctx)
+      ref <- newRef (M.empty, 0, a)
+      let cref = CRef newcrid ref
+      pure $ Right (ctx { cThreads = goto (c cref) tid (cThreads ctx), cIdSource = idSource' }, Right (NewCRef newcrid))
+
+    -- read from a @CRef@.
+    AReadCRef cref@(CRef crid _) c -> do
       val <- readCRef cref tid
-      simple (goto (c val) tid threads) $ ReadRef crid
+      simple (goto (c val) tid (cThreads ctx)) $ ReadCRef crid
 
-    -- | Read from a @CRef@ for future compare-and-swap operations.
-    stepReadRefCas cref@(CRef crid _) c = do
+    -- read from a @CRef@ for future compare-and-swap operations.
+    AReadCRefCas cref@(CRef crid _) c -> do
       tick <- readForTicket cref tid
-      simple (goto (c tick) tid threads) $ ReadRefCas crid
+      simple (goto (c tick) tid (cThreads ctx)) $ ReadCRefCas crid
 
-    -- | Modify a @CRef@.
-    stepModRef cref@(CRef crid _) f c = synchronised $ do
+    -- modify a @CRef@.
+    AModCRef cref@(CRef crid _) f c -> synchronised $ do
       (new, val) <- f <$> readCRef cref tid
       writeImmediate cref new
-      simple (goto (c val) tid threads) $ ModRef crid
+      simple (goto (c val) tid (cThreads ctx)) $ ModCRef crid
 
-    -- | Modify a @CRef@ using a compare-and-swap.
-    stepModRefCas cref@(CRef crid _) f c = synchronised $ do
+    -- modify a @CRef@ using a compare-and-swap.
+    AModCRefCas cref@(CRef crid _) f c -> synchronised $ do
       tick@(Ticket _ _ old) <- readForTicket cref tid
       let (new, val) = f old
       void $ casCRef cref tid tick new
-      simple (goto (c val) tid threads) $ ModRefCas crid
+      simple (goto (c val) tid (cThreads ctx)) $ ModCRefCas crid
 
-    -- | Write to a @CRef@ without synchronising
-    stepWriteRef cref@(CRef crid _) a c = case memtype of
-      -- Write immediately.
+    -- write to a @CRef@ without synchronising.
+    AWriteCRef cref@(CRef crid _) a c -> case memtype of
+      -- write immediately.
       SequentialConsistency -> do
         writeImmediate cref a
-        simple (goto c tid threads) $ WriteRef crid
-
-      -- Add to buffer using thread id.
+        simple (goto c tid (cThreads ctx)) $ WriteCRef crid
+      -- add to buffer using thread id.
       TotalStoreOrder -> do
-        wb' <- bufferWrite wb (tid, Nothing) cref a
-        return $ Right (goto c tid threads, idSource, WriteRef crid, wb', caps)
-
-      -- Add to buffer using both thread id and cref id
+        wb' <- bufferWrite (cWriteBuf ctx) (tid, Nothing) cref a
+        pure $ Right (ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Right (WriteCRef crid))
+      -- add to buffer using both thread id and cref id
       PartialStoreOrder -> do
-        wb' <- bufferWrite wb (tid, Just crid) cref a
-        return $ Right (goto c tid threads, idSource, WriteRef crid, wb', caps)
+        wb' <- bufferWrite (cWriteBuf ctx) (tid, Just crid) cref a
+        pure $ Right (ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Right (WriteCRef crid))
 
-    -- | Perform a compare-and-swap on a @CRef@.
-    stepCasRef cref@(CRef crid _) tick a c = synchronised $ do
+    -- perform a compare-and-swap on a @CRef@.
+    ACasCRef cref@(CRef crid _) tick a c -> synchronised $ do
       (suc, tick') <- casCRef cref tid tick a
-      simple (goto (c (suc, tick')) tid threads) $ CasRef crid suc
+      simple (goto (c (suc, tick')) tid (cThreads ctx)) $ CasCRef crid suc
 
-    -- | Commit a @CRef@ write
-    stepCommit t c = do
+    -- commit a @CRef@ write
+    ACommit t c -> do
       wb' <- case memtype of
-        -- Shouldn't ever get here
+        -- shouldn't ever get here
         SequentialConsistency ->
           error "Attempting to commit under SequentialConsistency"
-
-        -- Commit using the thread id.
-        TotalStoreOrder -> commitWrite wb (t, Nothing)
-
-        -- Commit using the cref id.
-        PartialStoreOrder -> commitWrite wb (t, Just c)
-
-      return $ Right (threads, idSource, CommitRef t c, wb', caps)
+        -- commit using the thread id.
+        TotalStoreOrder -> commitWrite (cWriteBuf ctx) (t, Nothing)
+        -- commit using the cref id.
+        PartialStoreOrder -> commitWrite (cWriteBuf ctx) (t, Just c)
+      pure $ Right (ctx { cWriteBuf = wb' }, Right (CommitCRef t c))
 
-    -- | Run a STM transaction atomically.
-    stepAtom stm c = synchronised $ do
-      (res, idSource', trace) <- runstm stm idSource
+    -- run a STM transaction atomically.
+    AAtom stm c -> synchronised $ do
+      (res, idSource', trace) <- runTransaction stm (cIdSource ctx)
       case res of
         Success _ written val ->
-          let (threads', woken) = wake (OnTVar written) threads
-          in return $ Right (goto (c val) tid threads', idSource', STM trace woken, wb, caps)
+          let (threads', woken) = wake (OnTVar written) (cThreads ctx)
+          in pure $ Right (ctx { cThreads = goto (c val) tid threads', cIdSource = idSource' }, Right (STM trace woken))
         Retry touched ->
-          let threads' = block (OnTVar touched) tid threads
-          in return $ Right (threads', idSource', BlockedSTM trace, wb, caps)
+          let threads' = block (OnTVar touched) tid (cThreads ctx)
+          in pure $ Right (ctx { cThreads = threads', cIdSource = idSource'}, Right (BlockedSTM trace))
         Exception e -> do
           res' <- stepThrow e
-          return $ case res' of
-            Right (threads', _, _, _, _) -> Right (threads', idSource', Throw, wb, caps)
+          pure $ case res' of
+            Right (ctx', _) -> Right (ctx' { cIdSource = idSource' }, Right Throw)
             Left err -> Left err
 
-    -- | Run a subcomputation in an exception-catching context.
-    stepCatching h ma c = simple threads' Catching where
-      a     = runCont ma      (APopCatching . c)
-      e exc = runCont (h exc) (APopCatching . c)
-
-      threads' = goto a tid (catching e tid threads)
-
-    -- | Pop the top exception handler from the thread's stack.
-    stepPopCatching a = simple threads' PopCatching where
-      threads' = goto a tid (uncatching tid threads)
+    -- lift an action from the underlying monad into the @Conc@
+    -- computation.
+    ALift na -> do
+      a <- na
+      simple (goto a tid (cThreads ctx)) LiftIO
 
-    -- | Throw an exception, and propagate it to the appropriate
+    -- throw an exception, and propagate it to the appropriate
     -- handler.
-    stepThrow e =
-      case propagate (toException e) tid threads of
-        Just threads' -> simple threads' Throw
-        Nothing -> return $ Left UncaughtException
+    AThrow e -> stepThrow e
 
-    -- | Throw an exception to the target thread, and propagate it to
+    -- throw an exception to the target thread, and propagate it to
     -- the appropriate handler.
-    stepThrowTo t e c = synchronised $
-      let threads' = goto c tid threads
-          blocked  = block (OnMask t) tid threads
-      in case M.lookup t threads of
+    AThrowTo t e c -> synchronised $
+      let threads' = goto c tid (cThreads ctx)
+          blocked  = block (OnMask t) tid (cThreads ctx)
+      in case M.lookup t (cThreads ctx) of
            Just thread
              | interruptible thread -> case propagate (toException e) t threads' of
                Just threads'' -> simple threads'' $ ThrowTo t
                Nothing
-                 | t == initialThread -> return $ Left UncaughtException
+                 | t == initialThread -> pure $ Left UncaughtException
                  | otherwise -> simple (kill t threads') $ ThrowTo t
              | otherwise -> simple blocked $ BlockedThrowTo t
            Nothing -> simple threads' $ ThrowTo t
 
-    -- | Execute a subcomputation with a new masking state, and give
-    -- it a function to run a computation with the current masking
-    -- state.
-    --
-    -- Explicit type sig necessary for checking in the prescence of
-    -- 'umask', sadly.
-    stepMasking :: MaskingState
-                -> ((forall b. M n r s b -> M n r s b) -> M n r s a)
-                -> (a -> Action n r s)
-                -> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int))
-    stepMasking m ma c = simple threads' $ SetMasking False m where
-      a = runCont (ma umask) (AResetMask False False m' . c)
+    -- run a subcomputation in an exception-catching context.
+    ACatching h ma c ->
+      let a        = runCont ma      (APopCatching . c)
+          e exc    = runCont (h exc) (APopCatching . c)
+          threads' = goto a tid (catching e tid (cThreads ctx))
+      in simple threads' Catching
 
-      m' = _masking . fromJust $ M.lookup tid threads
-      umask mb = resetMask True m' >> mb >>= \b -> resetMask False m >> return b
-      resetMask typ ms = cont $ \k -> AResetMask typ True ms $ k ()
+    -- pop the top exception handler from the thread's stack.
+    APopCatching a ->
+      let threads' = goto a tid (uncatching tid (cThreads ctx))
+      in simple threads' PopCatching
 
-      threads' = goto a tid (mask m tid threads)
+    -- execute a subcomputation with a new masking state, and give it
+    -- a function to run a computation with the current masking state.
+    AMasking m ma c ->
+      let a = runCont (ma umask) (AResetMask False False m' . c)
+          m' = _masking . fromJust $ M.lookup tid (cThreads ctx)
+          umask mb = resetMask True m' >> mb >>= \b -> resetMask False m >> pure b
+          resetMask typ ms = cont $ \k -> AResetMask typ True ms $ k ()
+          threads' = goto a tid (mask m tid (cThreads ctx))
+      in simple threads' $ SetMasking False m
 
-    -- | Reset the masking thread of the state.
-    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 @MVar@, using the next 'MVarId'.
-    stepNewVar n c = do
-      let (idSource', newmvid) = nextMVId n idSource
-      ref <- newRef Nothing
-      let mvar = MVar newmvid ref
-      return $ Right (goto (c mvar) tid threads, idSource', NewVar newmvid, wb, caps)
-
-    -- | Create a new @CRef@, using the next 'CRefId'.
-    stepNewRef n a c = do
-      let (idSource', newcrid) = nextCRId n idSource
-      ref <- newRef (M.empty, 0, a)
-      let cref = CRef newcrid ref
-      return $ Right (goto (c cref) tid threads, idSource', NewRef newcrid, wb, caps)
+    -- reset the masking thread of the state.
+    AResetMask b1 b2 m c ->
+      let act      = (if b1 then SetMasking else ResetMasking) b2 m
+          threads' = goto c tid (mask m tid (cThreads ctx))
+      in simple threads' act
 
-    -- | Lift an action from the underlying monad into the @Conc@
-    -- computation.
-    stepLift na = do
-      a <- na
-      simple (goto a tid threads) LiftIO
+    -- execute a 'return' or 'pure'.
+    AReturn c -> simple (goto c tid (cThreads ctx)) Return
 
-    -- | Execute a 'return' or 'pure'.
-    stepReturn c = simple (goto c tid threads) Return
+    -- kill the current thread.
+    AStop na -> na >> simple (kill tid (cThreads ctx)) Stop
 
-    -- | Add a message to the trace.
-    stepMessage m c = simple (goto c tid threads) (Message m)
+    -- run a subconcurrent computation.
+    ASub ma c
+      | M.size (cThreads ctx) > 1 -> pure (Left IllegalSubconcurrency)
+      | otherwise -> do
+          (res, g', trace) <- runConcurrency sched memtype (cSchedState ctx) ma
+          pure $ Right (ctx { cThreads = goto (c res) tid (cThreads ctx), cSchedState = g' }, Left (Subconcurrency, trace))
+  where
 
-    -- | Kill the current thread.
-    stepStop na = na >> simple (kill tid threads) Stop
+    -- this is not inline in the long @case@ above as it's needed by
+    -- @AAtom@, @AThrow@, and @AThrowTo@.
+    stepThrow e =
+      case propagate (toException e) tid (cThreads ctx) of
+        Just threads' -> simple threads' Throw
+        Nothing -> pure $ Left UncaughtException
 
-    -- | Helper for actions which don't touch the 'IdSource' or
-    -- 'WriteBuffer'
-    simple threads' act = return $ Right (threads', idSource, act, wb, caps)
+    -- helper for actions which only change the threads.
+    simple threads' act = pure $ Right (ctx { cThreads = threads' }, Right act)
 
-    -- | Helper for actions impose a write barrier.
+    -- helper for actions impose a write barrier.
     synchronised ma = do
-      writeBarrier wb
+      writeBarrier (cWriteBuf ctx)
       res <- ma
 
       return $ case res of
-        Right (threads', idSource', act', _, caps') -> Right (threads', idSource', act', emptyBuffer, caps')
+        Right (ctx', act) -> Right (ctx' { cWriteBuf = emptyBuffer }, act)
         _ -> res
diff --git a/Test/DejaFu/Conc/Internal/Common.hs b/Test/DejaFu/Conc/Internal/Common.hs
--- a/Test/DejaFu/Conc/Internal/Common.hs
+++ b/Test/DejaFu/Conc/Internal/Common.hs
@@ -14,10 +14,10 @@
 module Test.DejaFu.Conc.Internal.Common where
 
 import Control.Exception (Exception, MaskingState(..))
-import Data.Dynamic (Dynamic)
 import Data.Map.Strict (Map)
 import Data.List.NonEmpty (NonEmpty, fromList)
 import Test.DejaFu.Common
+import Test.DejaFu.STM (STMLike)
 
 {-# ANN module ("HLint: ignore Use record patterns" :: String) #-}
 
@@ -32,16 +32,16 @@
 -- 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 }
+newtype M n r a = M { runM :: (a -> Action n r) -> Action n r }
 
-instance Functor (M n r s) where
+instance Functor (M n r) where
     fmap f m = M $ \ c -> runM m (c . f)
 
-instance Applicative (M n r s) where
+instance Applicative (M n r) where
     pure x  = M $ \c -> AReturn $ c x
     f <*> v = M $ \c -> runM f (\g -> runM v (c . g))
 
-instance Monad (M n r s) where
+instance Monad (M n r) where
     return  = pure
     m >>= k = M $ \c -> runM m (\x -> runM (k x) c)
 
@@ -82,11 +82,11 @@
   }
 
 -- | Construct a continuation-passing operation from a function.
-cont :: ((a -> Action n r s) -> Action n r s) -> M n r s a
+cont :: ((a -> Action n r) -> Action n r) -> M n r a
 cont = M
 
 -- | Run a CPS computation with the given final computation.
-runCont :: M n r s a -> (a -> Action n r s) -> Action n r s
+runCont :: M n r a -> (a -> Action n r) -> Action n r
 runCont = runM
 
 --------------------------------------------------------------------------------
@@ -96,68 +96,70 @@
 -- only occur as a result of an action, and they cover (most of) the
 -- primitives of the concurrency. 'spawn' is absent as it is
 -- implemented in terms of 'newEmptyMVar', 'fork', and 'putMVar'.
-data 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)
+data Action n r =
+    AFork  String ((forall b. M n r b -> M n r b) -> Action n r) (ThreadId -> Action n r)
+  | AMyTId (ThreadId -> Action n r)
 
-  | AGetNumCapabilities (Int -> Action n r s)
-  | ASetNumCapabilities Int (Action n r s)
+  | AGetNumCapabilities (Int -> Action n r)
+  | ASetNumCapabilities Int (Action n r)
 
-  | 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. ANewMVar String (MVar r a -> Action n r)
+  | forall a. APutMVar     (MVar r a) a (Action n r)
+  | forall a. ATryPutMVar  (MVar r a) a (Bool -> Action n r)
+  | forall a. AReadMVar    (MVar r a) (a -> Action n r)
+  | forall a. ATryReadMVar (MVar r a) (Maybe a -> Action n r)
+  | forall a. ATakeMVar    (MVar r a) (a -> Action n r)
+  | forall a. ATryTakeMVar (MVar r a) (Maybe a -> Action n r)
 
-  | 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 b. AModRef     (CRef r a) (a -> (a, b)) (b -> Action n r s)
-  | forall a b. AModRefCas  (CRef r a) (a -> (a, b)) (b -> Action n r s)
-  | forall a.   AWriteRef   (CRef r a) a (Action n r s)
-  | forall a.   ACasRef     (CRef r a) (Ticket a) a ((Bool, Ticket a) -> Action n r s)
+  | forall a.   ANewCRef String a (CRef r a -> Action n r)
+  | forall a.   AReadCRef    (CRef r a) (a -> Action n r)
+  | forall a.   AReadCRefCas (CRef r a) (Ticket a -> Action n r)
+  | forall a b. AModCRef     (CRef r a) (a -> (a, b)) (b -> Action n r)
+  | forall a b. AModCRefCas  (CRef r a) (a -> (a, b)) (b -> Action n r)
+  | forall a.   AWriteCRef   (CRef r a) a (Action n r)
+  | forall a.   ACasCRef     (CRef r a) (Ticket a) a ((Bool, Ticket a) -> Action n r)
 
   | forall e.   Exception e => AThrow e
-  | forall e.   Exception e => AThrowTo ThreadId e (Action n r s)
-  | forall a e. Exception e => ACatching (e -> M n r s a) (M n r s a) (a -> Action n r s)
-  | APopCatching (Action n r s)
-  | 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)
-
-  | AMessage    Dynamic (Action n r s)
+  | forall e.   Exception e => AThrowTo ThreadId e (Action n r)
+  | forall a e. Exception e => ACatching (e -> M n r a) (M n r a) (a -> Action n r)
+  | APopCatching (Action n r)
+  | forall a. AMasking MaskingState ((forall b. M n r b -> M n r b) -> M n r a) (a -> Action n r)
+  | AResetMask Bool Bool MaskingState (Action n r)
 
-  | forall a. AAtom (s a) (a -> Action n r s)
-  | ALift (n (Action n r s))
-  | AYield  (Action n r s)
-  | AReturn (Action n r s)
+  | forall a. AAtom (STMLike n r a) (a -> Action n r)
+  | ALift (n (Action n r))
+  | AYield  (Action n r)
+  | AReturn (Action n r)
   | ACommit ThreadId CRefId
   | AStop (n ())
 
+  | forall a. ASub (M n r a) (Either Failure a -> Action n r)
+
 --------------------------------------------------------------------------------
 -- * Scheduling & Traces
 
 -- | Look as far ahead in the given continuation as possible.
-lookahead :: Action n r s -> NonEmpty Lookahead
+lookahead :: Action n r -> NonEmpty Lookahead
 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 (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' (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' (ANewMVar _ _)           = [WillNewMVar]
+  lookahead' (APutMVar (MVar c _) _ k)    = WillPutMVar c : lookahead' k
+  lookahead' (ATryPutMVar (MVar c _) _ _) = [WillTryPutMVar c]
+  lookahead' (AReadMVar (MVar c _) _)     = [WillReadMVar c]
+  lookahead' (ATryReadMVar (MVar c _) _)  = [WillTryReadMVar c]
+  lookahead' (ATakeMVar (MVar c _) _)     = [WillTakeMVar c]
+  lookahead' (ATryTakeMVar (MVar c _) _)  = [WillTryTakeMVar c]
+  lookahead' (ANewCRef _ _ _)         = [WillNewCRef]
+  lookahead' (AReadCRef (CRef r _) _)     = [WillReadCRef r]
+  lookahead' (AReadCRefCas (CRef r _) _)  = [WillReadCRefCas r]
+  lookahead' (AModCRef (CRef r _) _ _)    = [WillModCRef r]
+  lookahead' (AModCRefCas (CRef r _) _ _) = [WillModCRefCas r]
+  lookahead' (AWriteCRef (CRef r _) _ k) = WillWriteCRef r : lookahead' k
+  lookahead' (ACasCRef (CRef r _) _ _ _) = [WillCasCRef r]
+  lookahead' (ACommit t c)           = [WillCommitCRef t c]
   lookahead' (AAtom _ _)             = [WillSTM]
   lookahead' (AThrow _)              = [WillThrow]
   lookahead' (AThrowTo tid _ k)      = WillThrowTo tid : lookahead' k
@@ -166,7 +168,7 @@
   lookahead' (AMasking ms _ _)       = [WillSetMasking False ms]
   lookahead' (AResetMask b1 b2 ms k) = (if b1 then WillSetMasking else WillResetMasking) b2 ms : lookahead' k
   lookahead' (ALift _)               = [WillLiftIO]
-  lookahead' (AMessage m k)          = WillMessage m : lookahead' k
   lookahead' (AYield k)              = WillYield : lookahead' k
   lookahead' (AReturn k)             = WillReturn : lookahead' k
   lookahead' (AStop _)               = [WillStop]
+  lookahead' (ASub _ _)              = [WillSubconcurrency]
diff --git a/Test/DejaFu/Conc/Internal/Memory.hs b/Test/DejaFu/Conc/Internal/Memory.hs
--- a/Test/DejaFu/Conc/Internal/Memory.hs
+++ b/Test/DejaFu/Conc/Internal/Memory.hs
@@ -126,7 +126,7 @@
   flush = mapM_ $ \(BufferedWrite _ cref a) -> writeImmediate 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 r -> Threads n r -> Threads n r
 addCommitThreads (WriteBuffer wb) ts = ts <> M.fromList phantoms where
   phantoms = [ (ThreadId Nothing $ negate tid, mkthread $ fromJust c)
              | ((k, b), tid) <- zip (M.toList wb) [1..]
@@ -136,41 +136,46 @@
   go EmptyL = Nothing
 
 -- | Remove phantom threads.
-delCommitThreads :: Threads n r s -> Threads n r s
+delCommitThreads :: Threads n r -> Threads n r
 delCommitThreads = M.filterWithKey $ \k _ -> k >= initialThread
 
 --------------------------------------------------------------------------------
 -- * Manipulating @MVar@s
 
 -- | Put into a @MVar@, blocking if full.
-putIntoMVar :: MonadRef r n => MVar r a -> a -> Action n r s
-            -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
+putIntoMVar :: MonadRef r n => MVar r a -> a -> Action n r
+            -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])
 putIntoMVar cvar a c = mutMVar True cvar a (const c)
 
 -- | Try to put into a @MVar@, not blocking if full.
-tryPutIntoMVar :: MonadRef r n => MVar r a -> a -> (Bool -> Action n r s)
-               -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
+tryPutIntoMVar :: MonadRef r n => MVar r a -> a -> (Bool -> Action n r)
+               -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])
 tryPutIntoMVar = mutMVar False
 
 -- | Read from a @MVar@, blocking if empty.
-readFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r s)
-            -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
+readFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r)
+            -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])
 readFromMVar cvar c = seeMVar False True cvar (c . fromJust)
 
+-- | Try to read from a @MVar@, not blocking if empty.
+tryReadFromMVar :: MonadRef r n => MVar r a -> (Maybe a -> Action n r)
+                -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])
+tryReadFromMVar = seeMVar False False
+
 -- | Take from a @MVar@, blocking if empty.
-takeFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r s)
-             -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
+takeFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r)
+             -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])
 takeFromMVar cvar c = seeMVar True True cvar (c . fromJust)
 
 -- | Try to take from a @MVar@, not blocking if empty.
-tryTakeFromMVar :: MonadRef r n => MVar r a -> (Maybe a -> Action n r s)
-                -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
+tryTakeFromMVar :: MonadRef r n => MVar r a -> (Maybe a -> Action n r)
+                -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])
 tryTakeFromMVar = seeMVar True False
 
 -- | Mutate a @MVar@, in either a blocking or nonblocking way.
 mutMVar :: MonadRef r n
-        => Bool -> MVar r a -> a -> (Bool -> Action n r s)
-        -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
+        => Bool -> MVar r a -> a -> (Bool -> Action n r)
+        -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])
 mutMVar blocking (MVar cvid ref) a c threadid threads = do
   val <- readRef ref
 
@@ -191,8 +196,8 @@
 -- | Read a @MVar@, in either a blocking or nonblocking
 -- way.
 seeMVar :: MonadRef r n
-        => Bool -> Bool -> MVar r a -> (Maybe a -> Action n r s)
-        -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
+        => Bool -> Bool -> MVar r a -> (Maybe a -> Action n r)
+        -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])
 seeMVar emptying blocking (MVar cvid ref) c threadid threads = do
   val <- readRef ref
 
diff --git a/Test/DejaFu/Conc/Internal/Threading.hs b/Test/DejaFu/Conc/Internal/Threading.hs
--- a/Test/DejaFu/Conc/Internal/Threading.hs
+++ b/Test/DejaFu/Conc/Internal/Threading.hs
@@ -27,22 +27,22 @@
 -- * Threads
 
 -- | Threads are stored in a map index by 'ThreadId'.
-type Threads n r s = Map ThreadId (Thread n r s)
+type Threads n r = Map ThreadId (Thread n r)
 
 -- | All the state of a thread.
-data Thread n r s = Thread
-  { _continuation :: Action n r s
+data Thread n r = Thread
+  { _continuation :: Action n r
   -- ^ The next action to execute.
   , _blocking     :: Maybe BlockedOn
   -- ^ The state of any blocks.
-  , _handlers     :: [Handler n r s]
+  , _handlers     :: [Handler n r]
   -- ^ Stack of exception handlers
   , _masking      :: MaskingState
   -- ^ The exception masking state.
   }
 
 -- | Construct a thread with just one action
-mkthread :: Action n r s -> Thread n r s
+mkthread :: Action n r -> Thread n r
 mkthread c = Thread c Nothing [] Unmasked
 
 --------------------------------------------------------------------------------
@@ -53,7 +53,7 @@
 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 n r -> BlockedOn -> Bool
 thread ~= theblock = case (_blocking thread, theblock) of
   (Just (OnMVarFull  _), OnMVarFull  _) -> True
   (Just (OnMVarEmpty _), OnMVarEmpty _) -> True
@@ -65,11 +65,11 @@
 -- * Exceptions
 
 -- | An exception handler.
-data Handler n r s = forall e. Exception e => Handler (e -> Action n r s)
+data Handler n r = forall e. Exception e => Handler (e -> Action n r)
 
 -- | Propagate an exception upwards, finding the closest handler
 -- which can deal with it.
-propagate :: SomeException -> ThreadId -> Threads n r s -> Maybe (Threads n r s)
+propagate :: SomeException -> ThreadId -> Threads n r -> Maybe (Threads n r)
 propagate e tid threads = case M.lookup tid threads >>= go . _handlers of
   Just (act, hs) -> Just $ except act hs tid threads
   Nothing -> Nothing
@@ -79,40 +79,40 @@
     go (Handler h:hs) = maybe (go hs) (\act -> Just (act, hs)) $ h <$> fromException e
 
 -- | Check if a thread can be interrupted by an exception.
-interruptible :: Thread n r s -> Bool
+interruptible :: Thread n r -> Bool
 interruptible thread = _masking thread == Unmasked || (_masking thread == MaskedInterruptible && isJust (_blocking thread))
 
 -- | Register a new exception handler.
-catching :: Exception e => (e -> Action n r s) -> ThreadId -> Threads n r s -> Threads n r s
+catching :: Exception e => (e -> Action n r) -> ThreadId -> Threads n r -> Threads n r
 catching h = M.alter $ \(Just thread) -> Just $ thread { _handlers = Handler h : _handlers thread }
 
 -- | Remove the most recent exception handler.
-uncatching :: ThreadId -> Threads n r s -> Threads n r s
+uncatching :: ThreadId -> Threads n r -> Threads n r
 uncatching = M.alter $ \(Just thread) -> Just $ thread { _handlers = tail $ _handlers thread }
 
 -- | Raise an exception in a thread.
-except :: Action n r s -> [Handler n r s] -> ThreadId -> Threads n r s -> Threads n r s
+except :: Action n r -> [Handler n r] -> ThreadId -> Threads n r -> Threads n r
 except act hs = M.alter $ \(Just thread) -> Just $ thread { _continuation = act, _handlers = hs, _blocking = Nothing }
 
 -- | Set the masking state of a thread.
-mask :: MaskingState -> ThreadId -> Threads n r s -> Threads n r s
+mask :: MaskingState -> ThreadId -> Threads n r -> Threads n r
 mask ms = M.alter $ \(Just thread) -> Just $ thread { _masking = ms }
 
 --------------------------------------------------------------------------------
 -- * Manipulating threads
 
 -- | Replace the @Action@ of a thread.
-goto :: Action n r s -> ThreadId -> Threads n r s -> Threads n r s
+goto :: Action n r -> ThreadId -> Threads n r -> Threads n r
 goto a = M.alter $ \(Just thread) -> Just (thread { _continuation = a })
 
 -- | 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 :: ThreadId -> ThreadId -> ((forall b. M n r b -> M n r b) -> Action n r) -> Threads n r -> Threads n r
 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' :: MaskingState -> ThreadId -> ((forall b. M n r b -> M n r b) -> Action n r) -> Threads n r -> Threads n r
 launch' ms tid a = M.insert tid thread where
   thread = Thread { _continuation = a umask, _blocking = Nothing, _handlers = [], _masking = ms }
 
@@ -120,11 +120,11 @@
   resetMask typ m = cont $ \k -> AResetMask typ True m $ k ()
 
 -- | Kill a thread.
-kill :: ThreadId -> Threads n r s -> Threads n r s
+kill :: ThreadId -> Threads n r -> Threads n r
 kill = M.delete
 
 -- | Block a thread.
-block :: BlockedOn -> ThreadId -> Threads n r s -> Threads n r s
+block :: BlockedOn -> ThreadId -> Threads n r -> Threads n r
 block blockedOn = M.alter doBlock where
   doBlock (Just thread) = Just $ thread { _blocking = Just blockedOn }
   doBlock _ = error "Invariant failure in 'block': thread does NOT exist!"
@@ -132,7 +132,7 @@
 -- | Unblock all threads waiting on the appropriate block. For 'TVar'
 -- blocks, this will wake all threads waiting on at least one of the
 -- given 'TVar's.
-wake :: BlockedOn -> Threads n r s -> (Threads n r s, [ThreadId])
+wake :: BlockedOn -> Threads n r -> (Threads n r, [ThreadId])
 wake blockedOn threads = (unblock <$> threads, M.keys $ M.filter isBlocked threads) where
   unblock thread
     | isBlocked thread = thread { _blocking = Nothing }
diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs
--- a/Test/DejaFu/SCT.hs
+++ b/Test/DejaFu/SCT.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 
 -- |
 -- Module      : Test.DejaFu.SCT
@@ -6,12 +6,17 @@
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
--- Portability : CPP
+-- Portability : GeneralizedNewtypeDeriving
 --
 -- Systematic testing for concurrent computations.
 module Test.DejaFu.SCT
-  ( -- * Bounded Partial-order Reduction
+  ( -- * Running Concurrent Programs
+    Way(..)
+  , runSCT
+  , resultsSet
 
+  -- * Bounded Partial-order Reduction
+
   -- | We can characterise the state of a concurrent computation by
   -- considering the ordering of dependent events. This is a partial
   -- order: independent events can be performed in any order without
@@ -23,35 +28,23 @@
   -- significantly. /Bounded/ partial-order reduction is a further
   -- optimisation, which only considers schedules within some bound.
   --
-  -- This module provides both a generic function for BPOR, and also a
-  -- pre-emption bounding BPOR runner, which is used by the
-  -- "Test.DejaFu" module.
-  --
-  -- See /Bounded partial-order reduction/, K. Coons, M. Musuvathi,
-  -- K. McKinley for more details.
-
-    sctBounded
-
-  -- * Combination Bounds
-
-  -- | Combination schedule bounding, where individual bounds are
-  -- enabled if they are set.
+  -- This module provides a combination pre-emption, fair, and length
+  -- bounding runner:
   --
   -- * Pre-emption + fair bounding is useful for programs which use
   --   loop/yield control flows but are otherwise terminating.
   --
   -- * Pre-emption, fair + length bounding is useful for
-  -- non-terminating programs, and used by the testing functionality
-  -- in @Test.DejaFu@.
+  --   non-terminating programs, and used by the testing functionality
+  --   in @Test.DejaFu@.
+  --
+  -- See /Bounded partial-order reduction/, K. Coons, M. Musuvathi,
+  -- K. McKinley for more details.
 
   , Bounds(..)
-  , defaultBounds
   , noBounds
-
   , sctBound
 
-  -- * Individual Bounds
-
   -- ** Pre-emption Bounding
 
   -- | BPOR using pre-emption bounding. This adds conservative
@@ -62,10 +55,7 @@
   -- See the BPOR paper for more details.
 
   , PreemptionBound(..)
-  , defaultPreemptionBound
   , sctPreBound
-  , pBacktrack
-  , pBound
 
   -- ** Fair Bounding
 
@@ -76,10 +66,7 @@
   -- See the BPOR paper for more details.
 
   , FairBound(..)
-  , defaultFairBound
   , sctFairBound
-  , fBacktrack
-  , fBound
 
   -- ** Length Bounding
 
@@ -87,52 +74,84 @@
   -- terms of primitive actions) of an execution.
 
   , LengthBound(..)
-  , defaultLengthBound
   , sctLengthBound
 
-  -- * Backtracking
+  -- * Random Scheduling
 
-  , BacktrackStep(..)
-  , BacktrackFunc
+  -- | By greatly sacrificing completeness, testing of a large
+  -- concurrent system can be greatly sped-up. Counter-intuitively,
+  -- random scheduling has better bug-finding behaviour than just
+  -- executing a program \"for real\" many times. This is perhaps
+  -- because a random scheduler is more chaotic than the real
+  -- scheduler.
+
+  , sctRandom
   ) where
 
-import Control.DeepSeq (NFData(..))
 import Control.Monad.Ref (MonadRef)
-import Data.Map.Strict (Map)
+import Data.List (foldl')
 import qualified Data.Map.Strict as M
 import Data.Maybe (isJust, fromJust)
+import Data.Set (Set)
 import qualified Data.Set as S
-import Test.DPOR ( DPOR(..), dpor
-                 , BacktrackFunc, BacktrackStep(..), backtrackAt
-                 , BoundFunc, (&+&), trueBound
-                 , PreemptionBound(..), defaultPreemptionBound, preempBacktrack
-                 , FairBound(..), defaultFairBound, fairBound, fairBacktrack
-                 , LengthBound(..), defaultLengthBound, lenBound, lenBacktrack
-                 )
+import System.Random (RandomGen)
 
 import Test.DejaFu.Common
 import Test.DejaFu.Conc
+import Test.DejaFu.SCT.Internal
 
 -------------------------------------------------------------------------------
+-- Running Concurrent Programs
+
+-- | How to explore the possible executions of a concurrent program.
+data Way g
+  = Systematically Bounds
+  -- ^ Systematically explore all executions within the bounds.
+  | Randomly g Int
+  -- ^ Explore a fixed number of random executions, with the given
+  -- PRNG.
+  deriving (Eq, Ord, Read, Show)
+
+-- | Explore possible executions of a concurrent program.
+--
+-- * If the 'Way' is @Systematically@, 'sctBound' is used.
+--
+-- * If the 'Way' is @Randomly@, 'sctRandom' is used.
+runSCT :: (MonadRef r n, RandomGen g)
+  => Way g
+  -- ^ How to run the concurrent program.
+  -> MemType
+  -- ^ The memory model to use for non-synchronised @CRef@ operations.
+  -> Conc n r a
+  -- ^ The computation to run many times.
+  -> n [(Either Failure a, Trace)]
+runSCT (Systematically cb) memtype = sctBound memtype cb
+runSCT (Randomly g lim)    memtype = sctRandom memtype g lim
+
+-- | Return the set of results of a concurrent program.
+resultsSet :: (MonadRef r n, RandomGen g, Ord a)
+  => Way g
+  -- ^ How to run the concurrent program.
+  -> MemType
+  -- ^ The memory model to use for non-synchronised @CRef@ operations.
+  -> Conc n r a
+  -- ^ The computation to run many times.
+  -> n (Set (Either Failure a))
+resultsSet way memtype conc =
+  S.fromList . map fst <$> runSCT way memtype conc
+
+-------------------------------------------------------------------------------
 -- Combined Bounds
 
 data Bounds = Bounds
   { boundPreemp :: Maybe PreemptionBound
   , boundFair   :: Maybe FairBound
   , boundLength :: Maybe LengthBound
-  }
-
--- | All bounds enabled, using their default values.
-defaultBounds :: Bounds
-defaultBounds = Bounds
-  { boundPreemp = Just defaultPreemptionBound
-  , boundFair   = Just defaultFairBound
-  , boundLength = Just defaultLengthBound
-  }
+  } deriving (Eq, Ord, Read, Show)
 
 -- | 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!
+-- space. This will /ONLY/ work if your computation always terminates!
 noBounds :: Bounds
 noBounds = Bounds
   { boundPreemp = Nothing
@@ -140,35 +159,29 @@
   , boundLength = Nothing
   }
 
--- | An SCT runner using a bounded scheduler
-sctBound :: MonadRef r n
-  => MemType
-  -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> Bounds
-  -- ^ The combined bounds.
-  -> Conc n r a
-  -- ^ The computation to run many times
-  -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
-sctBound memtype cb = sctBounded memtype (cBound cb) (cBacktrack cb)
-
 -- | Combination bound function
-cBound :: Bounds -> BoundFunc ThreadId ThreadAction Lookahead
-cBound (Bounds pb fb lb) = maybe trueBound pBound pb &+& maybe trueBound fBound fb &+& maybe trueBound lenBound lb
+cBound :: Bounds -> BoundFunc
+cBound (Bounds pb fb lb) =
+  maybe trueBound pBound pb &+&
+  maybe trueBound fBound fb &+&
+  maybe trueBound lBound lb
 
 -- | Combination backtracking function. Add all backtracking points
 -- corresponding to enabled bound functions.
 --
 -- If no bounds are enabled, just backtrack to the given point.
-cBacktrack :: Bounds -> BacktrackFunc 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 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
+cBacktrack :: Bounds -> BacktrackFunc
+cBacktrack (Bounds (Just _) _ _) = pBacktrack
+cBacktrack (Bounds _ (Just _) _) = fBacktrack
+cBacktrack (Bounds _ _ (Just _)) = lBacktrack
+cBacktrack _ = backtrackAt (\_ _ -> False)
 
 -------------------------------------------------------------------------------
 -- Pre-emption bounding
 
+newtype PreemptionBound = PreemptionBound Int
+  deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show)
+
 -- | An SCT runner using a pre-emption bounding scheduler.
 sctPreBound :: MonadRef r n
   => MemType
@@ -178,25 +191,40 @@
   -- execution
   -> Conc n r a
   -- ^ The computation to run many times
-  -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
-sctPreBound memtype pb = sctBounded memtype (pBound pb) pBacktrack
+  -> n [(Either Failure a, Trace)]
+sctPreBound memtype pb = sctBound memtype $ Bounds (Just pb) Nothing Nothing
 
+-- | Pre-emption bound function. This does not count pre-emptive
+-- context switches to a commit thread.
+pBound :: PreemptionBound -> BoundFunc
+pBound (PreemptionBound pb) ts dl = preEmpCount ts dl <= pb
+
 -- | 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.
-pBacktrack :: BacktrackFunc ThreadId ThreadAction Lookahead s
-pBacktrack = preempBacktrack isCommitRef
+pBacktrack :: BacktrackFunc
+pBacktrack bs = backtrackAt (\_ _ -> False) bs . concatMap addConservative where
+  addConservative o@(i, _, tid) = o : case conservative i of
+    Just j  -> [(j, True, tid)]
+    Nothing -> []
 
--- | 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
+  -- index of conservative point
+  conservative i = go (reverse (take (i-1) bs)) (i-1) where
+    go _ (-1) = Nothing
+    go (b1:rest@(b2:_)) j
+      | bcktThreadid b1 /= bcktThreadid b2
+        && not (isCommitRef $ bcktAction b1)
+        && not (isCommitRef $ bcktAction b2) = Just j
+      | otherwise = go rest (j-1)
+    go _ _ = Nothing
 
 -------------------------------------------------------------------------------
 -- Fair bounding
 
+newtype FairBound = FairBound Int
+  deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show)
+
 -- | An SCT runner using a fair bounding scheduler.
 sctFairBound :: MonadRef r n
   => MemType
@@ -206,21 +234,26 @@
   -- performed by different threads.
   -> Conc n r a
   -- ^ The computation to run many times
-  -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
-sctFairBound memtype fb = sctBounded memtype (fBound fb) fBacktrack
+  -> n [(Either Failure a, Trace)]
+sctFairBound memtype fb = sctBound memtype $ Bounds Nothing (Just fb) Nothing
 
 -- | Fair bound function
-fBound :: FairBound -> BoundFunc ThreadId ThreadAction Lookahead
-fBound = fairBound didYield willYield (\act -> case act of Fork t -> [t]; _ -> [])
+fBound :: FairBound -> BoundFunc
+fBound (FairBound fb) ts (_, l) = maxYieldCountDiff ts l <= fb
 
 -- | Add a backtrack point. If the thread isn't runnable, or performs
 -- a release operation, add all runnable threads.
-fBacktrack :: BacktrackFunc ThreadId ThreadAction Lookahead s
-fBacktrack = fairBacktrack willRelease
+fBacktrack :: BacktrackFunc
+fBacktrack = backtrackAt check where
+  -- True if a release operation is performed.
+  check t b = Just True == (willRelease <$> M.lookup t (bcktRunnable b))
 
 -------------------------------------------------------------------------------
 -- Length bounding
 
+newtype LengthBound = LengthBound Int
+  deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show)
+
 -- | An SCT runner using a length bounding scheduler.
 sctLengthBound :: MonadRef r n
   => MemType
@@ -230,80 +263,105 @@
   -- actions.
   -> Conc n r a
   -- ^ The computation to run many times
-  -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
-sctLengthBound memtype lb = sctBounded memtype (lenBound lb) lenBacktrack
+  -> n [(Either Failure a, Trace)]
+sctLengthBound memtype lb = sctBound memtype $ Bounds Nothing Nothing (Just lb)
 
+-- | 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 :: BacktrackFunc
+lBacktrack = backtrackAt (\_ _ -> False)
+
 -------------------------------------------------------------------------------
--- DPOR
+-- Systematic concurrency testing
 
 -- | SCT via BPOR.
 --
 -- Schedules are generated by running the computation with a
--- deterministic scheduler with some initial list of decisions, after
--- which the supplied function is called. At each step of execution,
--- possible-conflicting actions are looked for, if any are found,
--- \"backtracking points\" are added, to cause the events to happen in
--- a different order in a future execution.
+-- deterministic scheduler with some initial list of decisions. At
+-- each step of execution, possible-conflicting actions are looked
+-- for, if any are found, \"backtracking points\" are added, to cause
+-- the events to happen in a different order in a future execution.
 --
 -- Note that unlike with non-bounded partial-order reduction, this may
 -- do some redundant work as the introduction of a bound can make
 -- previously non-interfering events interfere with each other.
-sctBounded :: MonadRef r n
+sctBound :: MonadRef r n
   => MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> BoundFunc ThreadId ThreadAction Lookahead
-  -- ^ Check if a prefix trace is within the bound
-  -> BacktrackFunc ThreadId ThreadAction Lookahead DepState
-  -- ^ 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.
+  -> Bounds
+  -- ^ The combined bounds.
   -> Conc n r a
-  -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
-sctBounded memtype bf backtrack conc =
-  dpor didYield
-       willYield
-       initialDepState
-       updateDepState
-       (dependent  memtype)
-       (dependent' memtype)
-#if MIN_VERSION_dpor(0,2,0)
-       -- dpor-0.2 knows about daemon threads.
-       (\_ (t, l) _ -> t == initialThread && case l of WillStop -> True; _ -> False)
-#endif
-       initialThread
-       (>=initialThread)
-       bf
-       backtrack
-       pruneCommits
-       (\sched s -> runConcurrent sched memtype s conc)
+  -- ^ The computation to run many times
+  -> n [(Either Failure a, Trace)]
+sctBound memtype cb conc = go initialState where
+  -- Repeatedly run the computation gathering all the results and
+  -- traces into a list until there are no schedules remaining to try.
+  go dp = case nextPrefix dp of
+    Just (prefix, conservative, sleep) -> do
+      (res, s, trace) <- runConcurrent scheduler
+                                       memtype
+                                       (initialDPORSchedState sleep prefix)
+                                       conc
 
--------------------------------------------------------------------------------
--- Post-processing
+      let bpoints = findBacktracks (schedBoundKill s) (schedBPoints s) trace
+      let newDPOR = addTrace conservative trace dp
 
--- | 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 }
+      if schedIgnore s
+      then go newDPOR
+      else ((res, trace):) <$> go (addBacktracks bpoints newDPOR)
 
-  where
-    go b = b { dporDone = pruneCommits <$> dporDone bpor }
+    Nothing -> pure []
 
-    onlycommits = all (<initialThread) . M.keys $ dporTodo bpor
-    alldonesync = all barrier . M.elems $ dporDone bpor
+  -- Find the next schedule prefix.
+  nextPrefix = findSchedulePrefix (>=initialThread)
 
-    barrier = isBarrier . simplifyAction . fromJust . dporAction
+  -- The DPOR scheduler.
+  scheduler = dporSched (dependent memtype) (cBound cb)
 
+  -- Find the new backtracking steps.
+  findBacktracks = findBacktrackSteps (dependent' memtype) (cBacktrack cb)
+
+  -- Incorporate a trace into the DPOR tree.
+  addTrace = incorporateTrace (dependent memtype)
+
+  -- Incorporate the new backtracking steps into the DPOR tree.
+  addBacktracks = incorporateBacktrackSteps (cBound cb)
+
+-- | SCT via random scheduling.
+--
+-- Schedules are generated by assigning to each new thread a random
+-- weight. Threads are then scheduled by a weighted random selection.
+--
+-- This is not guaranteed to find all distinct results.
+sctRandom :: (MonadRef r n, RandomGen g)
+  => MemType
+  -- ^ The memory model to use for non-synchronised @CRef@ operations.
+  -> g
+  -- ^ The random number generator.
+  -> Int
+  -- ^ The number of executions to perform.
+  -> Conc n r a
+  -- ^ The computation to run many times.
+  -> n [(Either Failure a, Trace)]
+sctRandom memtype g0 lim0 conc = go g0 lim0 where
+  go _ 0 = pure []
+  go g n = do
+    (res, s, trace) <- runConcurrent randSched
+                                     memtype
+                                     (initialRandSchedState g)
+                                     conc
+
+    ((res, trace):) <$> go (schedGen s) (n-1)
+
 -------------------------------------------------------------------------------
 -- Dependency function
 
 -- | Check if an action is dependent on another.
-dependent :: MemType -> DepState -> (ThreadId, ThreadAction) -> (ThreadId, ThreadAction) -> Bool
+dependent :: MemType -> DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool
 -- This is basically the same as 'dependent'', but can make use of the
 -- additional information in a 'ThreadAction' to make different
 -- decisions in a few cases:
@@ -327,14 +385,14 @@
 --  - Dependency of STM transactions can be /greatly/ improved here,
 --    as the 'Lookahead' does not know which @TVar@s will be touched,
 --    and so has to assume all transactions are dependent.
-dependent _ _ (_, SetNumCapabilities a) (_, GetNumCapabilities b) = a /= b
-dependent _ ds (_, ThrowTo t) (t2, a) = t == t2 && canInterrupt ds t2 a
-dependent memtype ds (t1, a1) (t2, a2) = case rewind a2 of
+dependent _ _ _ (SetNumCapabilities a) _ (GetNumCapabilities b) = a /= b
+dependent _ ds _ (ThrowTo t) t2 a = t == t2 && canInterrupt ds t2 a
+dependent memtype ds t1 a1 t2 a2 = case rewind a2 of
   Just l2
     | isSTM a1 && isSTM a2
       -> not . S.null $ tvarsOf a1 `S.intersection` tvarsOf a2
     | not (isBlock a1 && isBarrier (simplifyLookahead l2)) ->
-      dependent' memtype ds (t1, a1) (t2, l2)
+      dependent' memtype ds t1 a1 t2 l2
   _ -> dependentActions memtype ds (simplifyAction a1) (simplifyAction a2)
 
   where
@@ -343,17 +401,11 @@
     isSTM _ = False
 
 -- | Variant of 'dependent' to handle 'Lookahead'.
-dependent' :: MemType -> DepState -> (ThreadId, ThreadAction) -> (ThreadId, Lookahead) -> Bool
-dependent' memtype ds (t1, a1) (t2, l2) = case (a1, l2) of
-#if MIN_VERSION_dpor(0,2,0)
-  -- dpor-0.2 handles this case, woo.
-#else
-  -- Because Haskell threads are daemonised, when the initial thread
-  -- stops all child threads do too, this imposes a dependency.
-  (Stop, _)     | t1 == initialThread -> True
-  (_, WillStop) | t2 == initialThread -> True
-#endif
-
+--
+-- Termination of the initial thread is handled specially in the DPOR
+-- implementation.
+dependent' :: MemType -> DepState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool
+dependent' memtype ds t1 a1 t2 l2 = case (a1, l2) of
   -- Worst-case assumption: all IO is dependent.
   (LiftIO, WillLiftIO) -> True
 
@@ -392,9 +444,11 @@
   -- 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
+  (UnsynchronisedRead          r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> a2 /= UnsynchronisedRead r1
+  (UnsynchronisedWrite         r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True
+  (PartiallySynchronisedWrite  r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True
+  (PartiallySynchronisedModify r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True
+  (SynchronisedModify          r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True
 
   -- Unsynchronised writes and synchronisation where the buffer is not
   -- empty.
@@ -420,121 +474,62 @@
     same f = isJust (f a1) && f a1 == f a2
 
 -------------------------------------------------------------------------------
--- Dependency function state
-
-data DepState = DepState
-  { depCRState :: Map CRefId Bool
-  -- ^ Keep track of which @CRef@s have buffered writes.
-  , depMaskState :: Map ThreadId MaskingState
-  -- ^ Keep track of thread masking states. If a thread isn't present,
-  -- the masking state is assumed to be @Unmasked@. This nicely
-  -- provides compatibility with dpor-0.1, where the thread IDs are
-  -- not available.
-  }
-
-instance NFData DepState where
-  -- Cheats: 'MaskingState' has no 'NFData' instance.
-  rnf ds = rnf (depCRState ds, M.keys (depMaskState ds))
-
--- | Initial dependency state.
-initialDepState :: DepState
-initialDepState = DepState M.empty M.empty
-
--- | Update the 'CRef' buffer state with the action that has just
--- happened.
-#if MIN_VERSION_dpor(0,2,0)
-updateDepState :: DepState -> (ThreadId, ThreadAction) -> DepState
-updateDepState depstate (tid, act) = DepState
-  { depCRState   = updateCRState       act $ depCRState   depstate
-  , depMaskState = updateMaskState tid act $ depMaskState depstate
-  }
-#else
-updateDepState :: DepState -> ThreadAction -> DepState
-updateDepState depstate act = depstate
-  { depCRState = updateCRState act $ depCRState depstate }
-#endif
-
--- | Update the 'CRef' buffer state with the action that has just
--- happened.
-updateCRState :: ThreadAction -> Map CRefId Bool -> Map CRefId Bool
-updateCRState (CommitRef _ r) = M.delete r
-updateCRState (WriteRef    r) = M.insert r True
-updateCRState ta
-  | isBarrier $ simplifyAction ta = const M.empty
-  | otherwise = id
-
--- | Update the thread masking state with the action that has just
--- happened.
-updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState
-updateMaskState tid (Fork tid2) = \masks -> case M.lookup tid masks of
-  -- A thread inherits the masking state of its parent.
-  Just ms -> M.insert tid2 ms masks
-  Nothing -> masks
-updateMaskState tid (SetMasking   _ ms) = M.insert tid ms
-updateMaskState tid (ResetMasking _ ms) = M.insert tid ms
-updateMaskState _ _ = id
+-- Utilities
 
--- | Check if a 'CRef' has a buffered write pending.
-isBuffered :: DepState -> CRefId -> Bool
-isBuffered depstate r = M.findWithDefault False r (depCRState depstate)
+-- | Determine if an action is a commit or not.
+isCommitRef :: ThreadAction -> Bool
+isCommitRef (CommitCRef _ _) = True
+isCommitRef _ = False
 
--- | Check if an exception can interrupt a thread (action).
-canInterrupt :: DepState -> ThreadId -> ThreadAction -> Bool
-canInterrupt depstate tid act
-  -- If masked interruptible, blocked actions can be interrupted.
-  | isMaskedInterruptible depstate tid = case act of
-    BlockedPutVar  _ -> True
-    BlockedReadVar _ -> True
-    BlockedTakeVar _ -> True
-    BlockedSTM     _ -> True
-    BlockedThrowTo _ -> True
-    _ -> False
-  -- If masked uninterruptible, nothing can be.
-  | isMaskedUninterruptible depstate tid = False
-  -- If no mask, anything can be.
-  | otherwise = True
+-- | Extra threads created in a fork.
+forkTids :: ThreadAction -> [ThreadId]
+forkTids (Fork t) = [t]
+forkTids _ = []
 
--- | Check if an exception can interrupt a thread (lookahead).
-canInterruptL :: DepState -> ThreadId -> Lookahead -> Bool
-canInterruptL depstate tid lh
-  -- If masked interruptible, actions which can block may be
-  -- interrupted.
-  | isMaskedInterruptible depstate tid = case lh of
-    WillPutVar  _ -> True
-    WillReadVar _ -> True
-    WillTakeVar _ -> True
-    WillSTM       -> True
-    WillThrowTo _ -> True
-    _ -> False
-  -- If masked uninterruptible, nothing can be.
-  | isMaskedUninterruptible depstate tid = False
-  -- If no mask, anything can be.
-  | otherwise = True
+-- | Count the number of yields by a thread in a schedule prefix.
+yieldCount :: ThreadId
+  -- ^ The thread to count yields for.
+  -> [(Decision, ThreadAction)]
+  -> Lookahead
+  -> Int
+yieldCount tid ts l = go initialThread ts where
+  go t ((Start    t', act):rest) = go' t t' act rest
+  go t ((SwitchTo t', act):rest) = go' t t' act rest
+  go t ((Continue,    act):rest) = go' t t  act rest
+  go t []
+    | t == tid && willYield l = 1
+    | otherwise = 0
 
--- | Check if a thread is masked interruptible.
-isMaskedInterruptible :: DepState -> ThreadId -> Bool
-isMaskedInterruptible depstate tid =
-  M.lookup tid (depMaskState depstate) == Just MaskedInterruptible
+  {-# INLINE go' #-}
+  go' t t' act rest
+    | t == tid && didYield act = 1 + go t' rest
+    | otherwise = go t' rest
 
--- | Check if a thread is masked uninterruptible.
-isMaskedUninterruptible :: DepState -> ThreadId -> Bool
-isMaskedUninterruptible depstate tid =
-  M.lookup tid (depMaskState depstate) == Just MaskedUninterruptible
+-- | Get the maximum difference between the yield counts of all
+-- threads in this schedule prefix.
+maxYieldCountDiff :: [(Decision, ThreadAction)]
+  -> Lookahead
+  -> Int
+maxYieldCountDiff ts l = go 0 yieldCounts where
+  go m (yc:ycs) =
+    let m' = m `max` foldl' (go' yc) 0 ycs
+    in go m' ycs
+  go m [] = m
+  go' yc0 m yc = m `max` abs (yc0 - yc)
 
--------------------------------------------------------------------------------
--- Utilities
+  yieldCounts = [yieldCount t ts l | t <- allTids ts]
 
--- | Determine if an action is a commit or not.
-isCommitRef :: ThreadAction -> Bool
-isCommitRef (CommitRef _ _) = True
-isCommitRef _ = False
+  -- All the threads created during the lifetime of the system.
+  allTids ((_, act):rest) =
+    let tids' = forkTids act
+    in if null tids' then allTids rest else tids' ++ allTids rest
+  allTids [] = [initialThread]
 
--- | Check if a thread yielded.
-didYield :: ThreadAction -> Bool
-didYield Yield = True
-didYield _ = False
+-- | The \"true\" bound, which allows everything.
+trueBound :: BoundFunc
+trueBound _ _ = True
 
--- | Check if a thread will yield.
-willYield :: Lookahead -> Bool
-willYield WillYield = True
-willYield _ = False
+-- | 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
diff --git a/Test/DejaFu/SCT/Internal.hs b/Test/DejaFu/SCT/Internal.hs
new file mode 100644
--- /dev/null
+++ b/Test/DejaFu/SCT/Internal.hs
@@ -0,0 +1,712 @@
+-- |
+-- Module      : Test.DejaFu.SCT.Internal
+-- Copyright   : (c) 2016 Michael Walker
+-- License     : MIT
+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
+-- Stability   : experimental
+-- Portability : portable
+--
+-- Internal types and functions for dynamic partial-order
+-- reduction. This module is NOT considered to form part of the public
+-- interface of this library.
+module Test.DejaFu.SCT.Internal where
+
+import Control.Exception (MaskingState(..))
+import Data.Char (ord)
+import Data.Function (on)
+import qualified Data.Foldable as F
+import Data.List (intercalate, nubBy, partition, sortOn)
+import Data.List.NonEmpty (NonEmpty(..), toList)
+import Data.Map.Strict (Map)
+import Data.Maybe (catMaybes, fromJust, isNothing, listToMaybe)
+import qualified Data.Map.Strict as M
+import Data.Set (Set)
+import qualified Data.Set as S
+import Data.Sequence (Seq, (|>))
+import qualified Data.Sequence as Sq
+import System.Random (RandomGen, randomR)
+
+import Test.DejaFu.Common
+import Test.DejaFu.Schedule (Decision(..), Scheduler, decisionOf, tidOf)
+
+-------------------------------------------------------------------------------
+-- * Dynamic partial-order reduction
+
+-- | DPOR execution is represented as a tree of states, characterised
+-- by the decisions that lead to that state.
+data DPOR = DPOR
+  { dporRunnable :: Set ThreadId
+  -- ^ What threads are runnable at this step.
+  , dporTodo     :: Map ThreadId Bool
+  -- ^ Follow-on decisions still to make, and whether that decision
+  -- was added conservatively due to the bound.
+  , dporDone     :: Map ThreadId DPOR
+  -- ^ Follow-on decisions that have been made.
+  , dporSleep    :: Map ThreadId ThreadAction
+  -- ^ Transitions to ignore (in this node and children) until a
+  -- dependent transition happens.
+  , dporTaken    :: Map ThreadId ThreadAction
+  -- ^ Transitions which have been taken, excluding
+  -- conservatively-added ones. This is used in implementing sleep
+  -- sets.
+  , dporAction   :: Maybe ThreadAction
+  -- ^ What happened at this step. This will be 'Nothing' at the root,
+  -- 'Just' everywhere else.
+  } deriving Show
+
+-- | One step of the execution, including information for backtracking
+-- purposes. This backtracking information is used to generate new
+-- schedules.
+data BacktrackStep = BacktrackStep
+  { bcktThreadid   :: ThreadId
+  -- ^ The thread running at this step
+  , bcktDecision   :: Decision
+  -- ^ What was decided at this step.
+  , bcktAction     :: ThreadAction
+  -- ^ What happened at this step.
+  , bcktRunnable   :: Map ThreadId Lookahead
+  -- ^ The threads runnable at this step
+  , bcktBacktracks :: Map ThreadId Bool
+  -- ^ The list of alternative threads to run, and whether those
+  -- alternatives were added conservatively due to the bound.
+  , bcktState      :: DepState
+  -- ^ Some domain-specific state at this point.
+  } deriving Show
+
+-- | Initial DPOR state, given an initial thread ID. This initial
+-- thread should exist and be runnable at the start of execution.
+initialState :: DPOR
+initialState = DPOR
+  { dporRunnable = S.singleton initialThread
+  , dporTodo     = M.singleton initialThread False
+  , dporDone     = M.empty
+  , dporSleep    = M.empty
+  , dporTaken    = M.empty
+  , dporAction   = Nothing
+  }
+
+-- | Produce a new schedule prefix from a @DPOR@ tree. If there are no new
+-- prefixes remaining, return 'Nothing'. Also returns whether the
+-- decision was added conservatively, and the sleep set at the point
+-- where divergence happens.
+--
+-- A schedule prefix is a possibly empty sequence of decisions that
+-- have already been made, terminated by a single decision from the
+-- to-do set. The intent is to put the system into a new state when
+-- executed with this initial sequence of scheduling decisions.
+findSchedulePrefix
+  :: (ThreadId -> Bool)
+  -- ^ Some partitioning function, applied to the to-do decisions. If
+  -- there is an identifier which passes the test, it will be used,
+  -- rather than any which fail it. This allows a very basic way of
+  -- domain-specific prioritisation between otherwise equal choices,
+  -- which may be useful in some cases.
+  -> DPOR
+  -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
+findSchedulePrefix predicate = listToMaybe . go where
+  go dpor =
+    let prefixes = here dpor : map go' (M.toList $ dporDone dpor)
+    in case concatPartition (\(t:_,_,_) -> predicate t) prefixes of
+         ([], choices) -> choices
+         (choices, _)  -> choices
+
+  go' (tid, dpor) = (\(ts,c,slp) -> (tid:ts,c,slp)) <$> go dpor
+
+  -- Prefix traces terminating with a to-do decision at this point.
+  here dpor = [([t], c, sleeps dpor) | (t, c) <- M.toList $ dporTodo dpor]
+
+  -- The new sleep set is the union of the sleep set of the node we're
+  -- branching from, plus all the decisions we've already explored.
+  sleeps dpor = dporSleep dpor `M.union` dporTaken dpor
+
+-- | Add a new trace to the tree, creating a new subtree branching off
+-- at the point where the \"to-do\" decision was made.
+incorporateTrace
+  :: (DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool)
+  -- ^ Dependency function
+  -> Bool
+  -- ^ Whether the \"to-do\" point which was used to create this new
+  -- execution was conservative or not.
+  -> Trace
+  -- ^ The execution trace: the decision made, the runnable threads,
+  -- and the action performed.
+  -> DPOR
+  -> DPOR
+incorporateTrace dependency conservative trace dpor0 = grow initialDepState (initialDPORThread dpor0) trace dpor0 where
+  grow state tid trc@((d, _, a):rest) dpor =
+    let tid'   = tidOf tid d
+        state' = updateDepState state tid' a
+    in case M.lookup tid' (dporDone dpor) of
+         Just dpor' ->
+           let done = M.insert tid' (grow state' tid' rest dpor') (dporDone dpor)
+           in dpor { dporDone = done }
+         Nothing ->
+           let taken = M.insert tid' a (dporTaken dpor)
+               sleep = dporSleep dpor `M.union` dporTaken dpor
+               done  = M.insert tid' (subtree state' tid' sleep trc) (dporDone dpor)
+           in dpor { dporTaken = if conservative then dporTaken dpor else taken
+                   , dporTodo  = M.delete tid' (dporTodo dpor)
+                   , dporDone  = done
+                   }
+  grow _ _ [] dpor = dpor
+
+  -- Construct a new subtree corresponding to a trace suffix.
+  subtree state tid sleep ((_, _, a):rest) =
+    let state' = updateDepState state tid a
+        sleep' = M.filterWithKey (\t a' -> not $ dependency state' tid a t a') sleep
+    in DPOR
+        { dporRunnable = S.fromList $ case rest of
+            ((_, runnable, _):_) -> map fst runnable
+            [] -> []
+        , dporTodo     = M.empty
+        , dporDone     = M.fromList $ case rest of
+          ((d', _, _):_) ->
+            let tid' = tidOf tid d'
+            in  [(tid', subtree state' tid' sleep' rest)]
+          [] -> []
+        , dporSleep = sleep'
+        , dporTaken = case rest of
+          ((d', _, a'):_) -> M.singleton (tidOf tid d') a'
+          [] -> M.empty
+        , dporAction = Just a
+        }
+  subtree _ _ _ [] = err "incorporateTrace" "subtree suffix empty!"
+
+-- | Produce a list of new backtracking points from an execution
+-- trace. These are then used to inform new \"to-do\" points in the
+-- @DPOR@ tree.
+--
+-- Two traces are passed in to this function: the first is generated
+-- from the special DPOR scheduler, the other from the execution of
+-- the concurrent program.
+--
+-- If the trace ends with any threads other than the initial one still
+-- runnable, a dependency is imposed between this final action and
+-- everything else.
+findBacktrackSteps
+  :: (DepState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool)
+  -- ^ Dependency function.
+  -> BacktrackFunc
+  -- ^ Backtracking function. Given a list of backtracking points, and
+  -- a thread to backtrack to at a specific point in that list, add
+  -- the new backtracking points. There will be at least one: this
+  -- chosen one, but the function may add others.
+  -> Bool
+  -- ^ Whether the computation was aborted due to no decisions being
+  -- in-bounds.
+  -> Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])
+  -- ^ A sequence of threads at each step: the nonempty list of
+  -- runnable threads (with lookahead values), and the list of threads
+  -- still to try. The reason for the two separate lists is because
+  -- the threads chosen to try will be dependent on the specific
+  -- domain.
+  -> Trace
+  -- ^ The execution trace.
+  -> [BacktrackStep]
+findBacktrackSteps dependency backtrack boundKill = go initialDepState S.empty initialThread [] . F.toList where
+  -- Walk through the traces one step at a time, building up a list of
+  -- new backtracking points.
+  go state allThreads tid bs ((e,i):is) ((d,_,a):ts) =
+    let tid' = tidOf tid d
+        state' = updateDepState state tid' a
+        this = BacktrackStep
+          { bcktThreadid   = tid'
+          , bcktDecision   = d
+          , bcktAction     = a
+          , bcktRunnable   = M.fromList . toList $ e
+          , bcktBacktracks = M.fromList $ map (\i' -> (i', False)) i
+          , bcktState      = state'
+          }
+        bs' = doBacktrack killsEarly allThreads' (toList e) (bs++[this])
+        runnable = S.fromList (M.keys $ bcktRunnable this)
+        allThreads' = allThreads `S.union` runnable
+        killsEarly = null ts && boundKill
+    in go state' allThreads' tid' bs' is ts
+  go _ _ _ bs _ _ = bs
+
+  -- Find the prior actions dependent with this one and add
+  -- backtracking points.
+  doBacktrack killsEarly allThreads enabledThreads bs =
+    let tagged = reverse $ zip [0..] bs
+        idxs   = [ (head is, False, u)
+                 | (u, n) <- enabledThreads
+                 , v <- S.toList allThreads
+                 , u /= v
+                 , let is = idxs' u n v tagged
+                 , not $ null is]
+
+        idxs' u n v = catMaybes . go' True where
+          {-# INLINE go' #-}
+          go' final ((i,b):rest)
+            -- Don't cross subconcurrency boundaries
+            | isSubC final b = []
+            -- If this is the final action in the trace and the
+            -- execution was killed due to nothing being within bounds
+            -- (@killsEarly == True@) assume worst-case dependency.
+            | bcktThreadid b == v && (killsEarly || isDependent b) = Just i : go' False rest
+            | otherwise = go' False rest
+          go' _ [] = []
+
+          {-# INLINE isSubC #-}
+          isSubC final b = case bcktAction b of
+            Stop -> not final && bcktThreadid b == initialThread
+            Subconcurrency -> bcktThreadid b == initialThread
+            _ -> False
+
+          {-# INLINE isDependent #-}
+          isDependent b = dependency (bcktState b) (bcktThreadid b) (bcktAction b) u n
+    in backtrack bs idxs
+
+-- | Add new backtracking points, if they have not already been
+-- visited, fit into the bound, and aren't in the sleep set.
+incorporateBacktrackSteps
+  :: ([(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool)
+  -- ^ Bound function: returns true if that schedule prefix terminated
+  -- with the lookahead decision fits within the bound.
+  -> [BacktrackStep]
+  -- ^ Backtracking steps identified by 'findBacktrackSteps'.
+  -> DPOR
+  -> DPOR
+incorporateBacktrackSteps bv = go Nothing [] where
+  go priorTid pref (b:bs) bpor =
+    let bpor' = doBacktrack priorTid pref b bpor
+        tid   = bcktThreadid b
+        pref' = pref ++ [(bcktDecision b, bcktAction b)]
+        child = go (Just tid) pref' bs . fromJust $ M.lookup tid (dporDone bpor)
+    in bpor' { dporDone = M.insert tid child $ dporDone bpor' }
+  go _ _ [] bpor = bpor
+
+  doBacktrack priorTid pref b bpor =
+    let todo' = [ x
+                | x@(t,c) <- M.toList $ bcktBacktracks b
+                , let decision  = decisionOf priorTid (dporRunnable bpor) t
+                , let lahead = fromJust . M.lookup t $ bcktRunnable b
+                , bv pref (decision, lahead)
+                , t `notElem` M.keys (dporDone bpor)
+                , c || M.notMember t (dporSleep bpor)
+                ]
+    in bpor { dporTodo = dporTodo bpor `M.union` M.fromList todo' }
+
+-------------------------------------------------------------------------------
+-- * DPOR scheduler
+
+-- | The scheduler state
+data DPORSchedState = DPORSchedState
+  { schedSleep     :: Map ThreadId ThreadAction
+  -- ^ The sleep set: decisions not to make until something dependent
+  -- with them happens.
+  , schedPrefix    :: [ThreadId]
+  -- ^ Decisions still to make
+  , schedBPoints   :: Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])
+  -- ^ Which threads are runnable at each step, and the alternative
+  -- decisions still to make.
+  , schedIgnore    :: 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.
+  , schedBoundKill :: Bool
+  -- ^ Whether the execution was terminated due to all decisions being
+  -- out of bounds.
+  , schedDepState  :: DepState
+  -- ^ State used by the dependency function to determine when to
+  -- remove decisions from the sleep set.
+  } deriving Show
+
+-- | Initial DPOR scheduler state for a given prefix
+initialDPORSchedState :: Map ThreadId ThreadAction
+  -- ^ The initial sleep set.
+  -> [ThreadId]
+  -- ^ The schedule prefix.
+  -> DPORSchedState
+initialDPORSchedState sleep prefix = DPORSchedState
+  { schedSleep     = sleep
+  , schedPrefix    = prefix
+  , schedBPoints   = Sq.empty
+  , schedIgnore    = False
+  , schedBoundKill = False
+  , schedDepState  = initialDepState
+  }
+
+-- | 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
+
+-- | A backtracking step is a point in the execution where another
+-- decision needs to be made, in order to explore interesting new
+-- schedules. A backtracking /function/ takes the steps identified so
+-- far and a list of points and thread at that point to backtrack
+-- to. More points be added to compensate for the effects of the
+-- bounding function. For example, under pre-emption bounding a
+-- conservative backtracking point is added at the prior context
+-- switch. The bool is whether the point is conservative. Conservative
+-- points are always explored, whereas non-conservative ones might be
+-- skipped based on future information.
+--
+-- In general, a backtracking function should identify one or more
+-- backtracking points, and then use @backtrackAt@ to do the actual
+-- work.
+type BacktrackFunc
+  = [BacktrackStep] -> [(Int, Bool, ThreadId)] -> [BacktrackStep]
+
+-- | Add a backtracking point. If the thread isn't runnable, add all
+-- runnable threads. If the backtracking point is already present,
+-- don't re-add it UNLESS this would make it conservative.
+backtrackAt
+  :: (ThreadId -> BacktrackStep -> Bool)
+  -- ^ If this returns @True@, backtrack to all runnable threads,
+  -- rather than just the given thread.
+  -> BacktrackFunc
+backtrackAt toAll bs0 = backtrackAt' . nubBy ((==) `on` fst') . sortOn fst' where
+  fst' (x,_,_) = x
+
+  backtrackAt' ((i,c,t):is) = go i bs0 i c t is
+  backtrackAt' [] = bs0
+
+  go i0 (b:bs) 0 c tid is
+    -- 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.
+    | not (toAll tid b) && tid `M.member` bcktRunnable b =
+      let val = M.lookup tid $ bcktBacktracks b
+          b' = if isNothing val || (val == Just False && c)
+            then b { bcktBacktracks = backtrackTo tid c b }
+            else b
+      in b' : case is of
+        ((i',c',t'):is') -> go i' bs (i'-i0-1) c' t' is'
+        [] -> bs
+    -- Otherwise just backtrack to everything runnable.
+    | otherwise =
+      let b' = b { bcktBacktracks = backtrackAll c b }
+      in b' : case is of
+        ((i',c',t'):is') -> go i' bs (i'-i0-1) c' t' is'
+        [] -> bs
+  go i0 (b:bs) i c tid is = b : go i0 bs (i-1) c tid is
+  go _ [] _ _ _ _ = err "backtrackAt" "ran out of schedule whilst backtracking!"
+
+  -- Backtrack to a single thread
+  backtrackTo tid c = M.insert tid c . bcktBacktracks
+
+  -- Backtrack to all runnable threads
+  backtrackAll c = M.map (const c) . bcktRunnable
+
+-- | DPOR 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.
+--
+-- After the initial decisions are exhausted, this prefers choosing
+-- the prior thread if it's (1) still runnable and (2) hasn't just
+-- yielded. Furthermore, threads which /will/ yield are ignored in
+-- preference of those which will not.
+dporSched
+  :: (DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool)
+  -- ^ Dependency function.
+  -> BoundFunc
+  -- ^ Bound function: returns true if that schedule prefix terminated
+  -- with the lookahead decision fits within the bound.
+  -> Scheduler DPORSchedState
+dporSched dependency inBound trc prior threads s = schedule where
+  -- Pick a thread to run.
+  schedule = case schedPrefix s of
+    -- If there is a decision available, make it
+    (d:ds) -> (Just d, (nextState []) { schedPrefix = ds })
+
+    -- 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 choices  = restrictToBound initialise
+          checkDep t a = case prior of
+            Just (tid, act) -> dependency (schedDepState s) tid act t a
+            Nothing -> False
+          ssleep'  = M.filterWithKey (\t a -> not $ checkDep t a) $ schedSleep s
+          choices' = filter (`notElem` M.keys ssleep') choices
+          signore' = not (null choices) && all (`elem` M.keys ssleep') choices
+          sbkill'  = not (null initialise) && null choices
+      in case choices' of
+            (nextTid:rest) -> (Just nextTid, (nextState rest) { schedSleep = ssleep' })
+            [] -> (Nothing, (nextState []) { schedIgnore = signore', schedBoundKill = sbkill' })
+
+  -- The next scheduler state
+  nextState rest = s
+    { schedBPoints  = schedBPoints s |> (threads, rest)
+    , schedDepState = nextDepState
+    }
+  nextDepState = let ds = schedDepState s in maybe ds (uncurry $ updateDepState ds) prior
+
+  -- Pick a new thread to run, not considering bounds. Choose the
+  -- current thread if available and it hasn't just yielded, otherwise
+  -- add all runnable threads.
+  initialise = tryDaemons . yieldsToEnd $ case prior of
+    Just (tid, act)
+      | not (didYield act) && tid `elem` tids -> [tid]
+    _ -> tids'
+
+  -- If one of the chosen actions will kill the computation, and there
+  -- are daemon threads, try them instead.
+  --
+  -- This is necessary if the killing action is NOT dependent with
+  -- every other action, according to the dependency function. This
+  -- is, strictly speaking, wrong; an action that kills another thread
+  -- is definitely dependent with everything in that thread. HOWEVER,
+  -- implementing it that way leads to an explosion of schedules
+  -- tried. Really, all that needs to happen is for the
+  -- thread-that-would-be-killed to be executed fully ONCE, and then
+  -- the normal dependency mechanism will identify any other
+  -- backtracking points that should be tried. This is achieved by
+  -- adding every thread that would be killed to the to-do list.
+  -- Furthermore, these threads MUST be ahead of the killing thread,
+  -- or the killing thread will end up in the sleep set and so the
+  -- killing action not performed. This is, again, because of the lack
+  -- of the dependency messing things up in the name of performance.
+  --
+  -- See commits a056f54 and 8554ce9, and my 4th June comment in issue
+  -- #52.
+  tryDaemons ts
+    | any doesKill ts = case partition doesKill tids' of
+        (kills, nokills) -> nokills ++ kills
+    | otherwise = ts
+  doesKill t = killsDaemons t (action t)
+
+  -- Restrict the possible decisions to those in the bound.
+  restrictToBound = filter (\t -> inBound trc (decision t, action t))
+
+  -- Move the threads which will immediately yield to the end of the list
+  yieldsToEnd ts = case partition (willYield . action) ts of
+    (yields, noyields) -> noyields ++ yields
+
+  -- Get the decision that will lead to a thread being scheduled.
+  decision = decisionOf (fst <$> prior) (S.fromList tids')
+
+  -- Get the action of a thread
+  action t = fromJust $ lookup t threads'
+
+  -- The runnable thread IDs
+  tids = fst <$> threads
+
+  -- The runnable threads as a normal list.
+  threads' = toList threads
+  tids'    = toList tids
+
+-------------------------------------------------------------------------------
+-- Weighted random scheduler
+
+-- | The scheduler state
+data RandSchedState g = RandSchedState
+  { schedWeights :: Map ThreadId Int
+  -- ^ The thread weights: used in determining which to run.
+  , schedGen     :: g
+  -- ^ The random number generator.
+  }
+
+-- | Initial weighted random scheduler state.
+initialRandSchedState :: g -> RandSchedState g
+initialRandSchedState = RandSchedState M.empty
+
+-- | Weighted random scheduler: assigns to each new thread a weight,
+-- and makes a weighted random choice out of the runnable threads at
+-- every step.
+randSched :: RandomGen g => Scheduler (RandSchedState g)
+randSched _ _ threads s = (pick choice enabled, RandSchedState weights' g'') where
+  -- Select a thread
+  pick idx ((x, f):xs)
+    | idx < f = Just x
+    | otherwise = pick (idx - f) xs
+  pick _ [] = Nothing
+  (choice, g'') = randomR (0, sum (map snd enabled) - 1) g'
+  enabled = M.toList $ M.filterWithKey (\tid _ -> tid `elem` tids) weights'
+
+  -- The weights, with any new threads added.
+  weights' = schedWeights s `M.union` M.fromList newWeights
+  (newWeights, g') = foldr assignWeight ([], schedGen s) $ filter (`M.notMember` schedWeights s) tids
+  assignWeight tid ~(ws, g0) =
+    let (w, g) = randomR (1, 50) g0
+    in ((tid, w):ws, g)
+
+  -- The runnable threads.
+  tids = map fst (toList threads)
+
+-------------------------------------------------------------------------------
+-- Dependency function state
+
+data DepState = DepState
+  { depCRState :: Map CRefId Bool
+  -- ^ Keep track of which @CRef@s have buffered writes.
+  , depMaskState :: Map ThreadId MaskingState
+  -- ^ Keep track of thread masking states. If a thread isn't present,
+  -- the masking state is assumed to be @Unmasked@. This nicely
+  -- provides compatibility with dpor-0.1, where the thread IDs are
+  -- not available.
+  } deriving (Eq, Show)
+
+-- | Initial dependency state.
+initialDepState :: DepState
+initialDepState = DepState M.empty M.empty
+
+-- | Update the 'CRef' buffer state with the action that has just
+-- happened.
+updateDepState :: DepState -> ThreadId -> ThreadAction -> DepState
+updateDepState depstate tid act = DepState
+  { depCRState   = updateCRState       act $ depCRState   depstate
+  , depMaskState = updateMaskState tid act $ depMaskState depstate
+  }
+
+-- | Update the 'CRef' buffer state with the action that has just
+-- happened.
+updateCRState :: ThreadAction -> Map CRefId Bool -> Map CRefId Bool
+updateCRState (CommitCRef _ r) = M.delete r
+updateCRState (WriteCRef    r) = M.insert r True
+updateCRState ta
+  | isBarrier $ simplifyAction ta = const M.empty
+  | otherwise = id
+
+-- | Update the thread masking state with the action that has just
+-- happened.
+updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState
+updateMaskState tid (Fork tid2) = \masks -> case M.lookup tid masks of
+  -- A thread inherits the masking state of its parent.
+  Just ms -> M.insert tid2 ms masks
+  Nothing -> masks
+updateMaskState tid (SetMasking   _ ms) = M.insert tid ms
+updateMaskState tid (ResetMasking _ ms) = M.insert tid ms
+updateMaskState _ _ = id
+
+-- | Check if a 'CRef' has a buffered write pending.
+isBuffered :: DepState -> CRefId -> Bool
+isBuffered depstate r = M.findWithDefault False r (depCRState depstate)
+
+-- | Check if an exception can interrupt a thread (action).
+canInterrupt :: DepState -> ThreadId -> ThreadAction -> Bool
+canInterrupt depstate tid act
+  -- If masked interruptible, blocked actions can be interrupted.
+  | isMaskedInterruptible depstate tid = case act of
+    BlockedPutMVar  _ -> True
+    BlockedReadMVar _ -> True
+    BlockedTakeMVar _ -> True
+    BlockedSTM      _ -> True
+    BlockedThrowTo  _ -> True
+    _ -> False
+  -- If masked uninterruptible, nothing can be.
+  | isMaskedUninterruptible depstate tid = False
+  -- If no mask, anything can be.
+  | otherwise = True
+
+-- | Check if an exception can interrupt a thread (lookahead).
+canInterruptL :: DepState -> ThreadId -> Lookahead -> Bool
+canInterruptL depstate tid lh
+  -- If masked interruptible, actions which can block may be
+  -- interrupted.
+  | isMaskedInterruptible depstate tid = case lh of
+    WillPutMVar  _ -> True
+    WillReadMVar _ -> True
+    WillTakeMVar _ -> True
+    WillSTM        -> True
+    WillThrowTo  _ -> True
+    _ -> False
+  -- If masked uninterruptible, nothing can be.
+  | isMaskedUninterruptible depstate tid = False
+  -- If no mask, anything can be.
+  | otherwise = True
+
+-- | Check if a thread is masked interruptible.
+isMaskedInterruptible :: DepState -> ThreadId -> Bool
+isMaskedInterruptible depstate tid =
+  M.lookup tid (depMaskState depstate) == Just MaskedInterruptible
+
+-- | Check if a thread is masked uninterruptible.
+isMaskedUninterruptible :: DepState -> ThreadId -> Bool
+isMaskedUninterruptible depstate tid =
+  M.lookup tid (depMaskState depstate) == Just MaskedUninterruptible
+
+-------------------------------------------------------------------------------
+-- * Utilities
+
+-- The initial thread of a DPOR tree.
+initialDPORThread :: DPOR -> ThreadId
+initialDPORThread = S.elemAt 0 . dporRunnable
+
+-- | 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
+
+-- | Check if an action will kill daemon threads.
+killsDaemons :: ThreadId -> Lookahead -> Bool
+killsDaemons t WillStop = t == initialThread
+killsDaemons _ _ = False
+
+-- | Render a 'DPOR' value as a graph in GraphViz \"dot\" format.
+toDot :: (ThreadId -> String)
+  -- ^ Show a @tid@ - this should produce a string suitable for
+  -- use as a node identifier.
+  -> (ThreadAction -> String)
+  -- ^ Show a @action@.
+  -> DPOR
+  -> String
+toDot = toDotFiltered (\_ _ -> True)
+
+-- | Render a 'DPOR' value as a graph in GraphViz \"dot\" format, with
+-- a function to determine if a subtree should be included or not.
+toDotFiltered :: (ThreadId -> DPOR -> Bool)
+  -- ^ Subtree predicate.
+  -> (ThreadId -> String)
+  -> (ThreadAction -> String)
+  -> DPOR
+  -> String
+toDotFiltered check showTid showAct = digraph . go "L" where
+  digraph str = "digraph {\n" ++ str ++ "\n}"
+
+  go l b = unlines $ node l b : edges l b
+
+  -- Display a labelled node.
+  node n b = n ++ " [label=\"" ++ label b ++ "\"]"
+
+  -- Display the edges.
+  edges l b = [ edge l l' i ++ go l' b'
+              | (i, b') <- M.toList (dporDone b)
+              , check i b'
+              , let l' = l ++ tidId i
+              ]
+
+  -- A node label, summary of the DPOR state at that node.
+  label b = showLst id
+    [ maybe "Nothing" (("Just " ++) . showAct) $ dporAction b
+    , "Run:" ++ showLst showTid (S.toList $ dporRunnable b)
+    , "Tod:" ++ showLst showTid (M.keys   $ dporTodo     b)
+    , "Slp:" ++ showLst (\(t,a) -> "(" ++ showTid t ++ ", " ++ showAct a ++ ")")
+        (M.toList $ dporSleep b)
+    ]
+
+  -- Display a labelled edge
+  edge n1 n2 l = n1 ++ " -> " ++ n2 ++ " [label=\"" ++ showTid l ++ "\"]\n"
+
+  -- Show a list of values
+  showLst showf xs = "[" ++ intercalate ", " (map showf xs) ++ "]"
+
+  -- Generate a graphviz-friendly identifier from a tid.
+  tidId = concatMap (show . ord) . showTid
+
+-- | Internal errors.
+err :: String -> String -> a
+err func msg = error (func ++ ": (internal error) " ++ msg)
+
+-- | A combination of 'partition' and 'concat'.
+concatPartition :: (a -> Bool) -> [[a]] -> ([a], [a])
+{-# INLINE concatPartition #-}
+-- note: `foldr (flip (foldr select))` is slow, as is `foldl (foldl
+-- select))`, and `foldl'` variants. The sweet spot seems to be `foldl
+-- (foldr select)` for some reason I don't really understand.
+concatPartition p = foldl (foldr select) ([], []) where
+  -- Lazy pattern matching, got this trick from the 'partition'
+  -- implementation. This reduces allocation fairly significantly; I
+  -- do not know why.
+  select a ~(ts, fs)
+    | p a       = (a:ts, fs)
+    | otherwise = (ts, a:fs)
diff --git a/Test/DejaFu/Schedule.hs b/Test/DejaFu/Schedule.hs
new file mode 100644
--- /dev/null
+++ b/Test/DejaFu/Schedule.hs
@@ -0,0 +1,129 @@
+-- |
+-- Module      : Test.DejaFu.Schedule
+-- Copyright   : (c) 2016 Michael Walker
+-- License     : MIT
+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
+-- Stability   : experimental
+-- Portability : portable
+--
+-- Scheduling for concurrent computations.
+module Test.DejaFu.Schedule
+  ( -- * Scheduling
+    Scheduler
+
+  , Decision(..)
+  , tidOf
+  , decisionOf
+
+  , NonEmpty(..)
+
+  -- ** Preemptive
+  , randomSched
+  , roundRobinSched
+
+  -- ** Non-preemptive
+  , randomSchedNP
+  , roundRobinSchedNP
+
+  -- * Utilities
+  , makeNonPreemptive
+  ) where
+
+import Data.List.NonEmpty (NonEmpty(..), toList)
+import System.Random (RandomGen, randomR)
+
+import Test.DejaFu.Common
+
+-- | A @Scheduler@ drives the execution of a concurrent program. The
+-- parameters it takes are:
+--
+-- 1. The trace so far.
+--
+-- 2. The last thread executed (if this is the first invocation, this
+--    is @Nothing@).
+--
+-- 3. The runnable threads at this point.
+--
+-- 4. The state.
+--
+-- It returns a thread to execute, or @Nothing@ if execution should
+-- abort here, and also a new state.
+type Scheduler state
+  = [(Decision, ThreadAction)]
+  -> Maybe (ThreadId, ThreadAction)
+  -> NonEmpty (ThreadId, Lookahead)
+  -> state
+  -> (Maybe ThreadId, state)
+
+-------------------------------------------------------------------------------
+-- Scheduling decisions
+
+-- | Get the resultant thread identifier 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 thread identifier,
+-- given a prior thread (if any) and list of runnable threads.
+decisionOf :: Foldable f
+  => Maybe ThreadId
+  -- ^ The prior thread.
+  -> f ThreadId
+  -- ^ The runnable threads.
+  -> ThreadId
+  -- ^ The current thread.
+  -> Decision
+decisionOf Nothing _ chosen = Start chosen
+decisionOf (Just prior) runnable chosen
+  | prior == chosen = Continue
+  | prior `elem` runnable = SwitchTo chosen
+  | otherwise = Start chosen
+
+-------------------------------------------------------------------------------
+-- Preemptive
+
+-- | A simple random scheduler which, at every step, picks a random
+-- thread to run.
+randomSched :: RandomGen g => Scheduler g
+randomSched _ _ threads g = (Just $ threads' !! choice, g') where
+  (choice, g') = randomR (0, length threads' - 1) g
+  threads' = map fst $ toList threads
+
+-- | A round-robin scheduler which, at every step, schedules the
+-- thread with the next 'ThreadId'.
+roundRobinSched :: Scheduler ()
+roundRobinSched _ Nothing ((tid,_):|_) _ = (Just tid, ())
+roundRobinSched _ (Just (prior, _)) threads _
+  | prior >= maximum threads' = (Just $ minimum threads', ())
+  | otherwise = (Just . minimum $ filter (>prior) threads', ())
+
+  where
+    threads' = map fst $ toList threads
+
+-------------------------------------------------------------------------------
+-- Non-preemptive
+
+-- | A random scheduler which doesn't preempt the running
+-- thread. That is, if the last thread scheduled is still runnable,
+-- run that, otherwise schedule randomly.
+randomSchedNP :: RandomGen g => Scheduler g
+randomSchedNP = makeNonPreemptive randomSched
+
+-- | A round-robin scheduler which doesn't preempt the running
+-- thread.
+roundRobinSchedNP :: Scheduler ()
+roundRobinSchedNP = makeNonPreemptive roundRobinSched
+
+-------------------------------------------------------------------------------
+-- Utilities
+
+-- | Turn a potentially preemptive scheduler into a non-preemptive
+-- one.
+makeNonPreemptive :: Scheduler s -> Scheduler s
+makeNonPreemptive sched = newsched where
+  newsched trc p@(Just (prior, _)) threads s
+    | prior `elem` map fst (toList threads) = (Just prior, s)
+    | otherwise = sched trc p threads s
+  newsched trc Nothing threads s = sched trc Nothing threads s
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.4.0.0
+version:             0.5.0.0
 synopsis:            Systematic testing for Haskell concurrency.
 
 description:
@@ -74,12 +74,13 @@
 source-repository this
   type:     git
   location: https://github.com/barrucadu/dejafu.git
-  tag:      dejafu-0.4.0.0
+  tag:      dejafu-0.5.0.0
 
 library
   exposed-modules:     Test.DejaFu
                      , Test.DejaFu.Conc
                      , Test.DejaFu.Common
+                     , Test.DejaFu.Schedule
                      , Test.DejaFu.SCT
                      , Test.DejaFu.STM
 
@@ -87,18 +88,18 @@
                      , Test.DejaFu.Conc.Internal.Common
                      , Test.DejaFu.Conc.Internal.Memory
                      , Test.DejaFu.Conc.Internal.Threading
+                     , Test.DejaFu.SCT.Internal
                      , Test.DejaFu.STM.Internal
 
   -- other-modules:       
   -- other-extensions:    
   build-depends:       base              >=4.8  && <5
-                     , concurrency       >=1.0  && <1.1
+                     , concurrency       ==1.1.0.*
                      , containers        >=0.5  && <0.6
-                     , deepseq           >=1.3  && <1.5
-                     , dpor              >=0.1  && <0.3
                      , exceptions        >=0.7  && <0.9
                      , monad-loops       >=0.4  && <0.5
                      , mtl               >=2.2  && <2.3
+                     , random            >=1.0  && <1.2
                      , ref-fd            >=0.4  && <0.5
                      , semigroups        >=0.16 && <0.19
                      , transformers      >=0.4  && <0.6