diff --git a/CHANGELOG.rst b/CHANGELOG.rst
--- a/CHANGELOG.rst
+++ b/CHANGELOG.rst
@@ -7,6 +7,145 @@
 .. _PVP: https://pvp.haskell.org/
 
 
+2.0.0.0 (2019-02-12)
+--------------------
+
+* Git: :tag:`dejafu-2.0.0.0`
+* Hackage: :hackage:`dejafu-2.0.0.0`
+
+Added
+~~~~~
+
+* The ``Program`` types and their constructors (re-exported from
+  ``Test.DejaFu``):
+    * ``Test.DejaFu.Conc.Program``
+    * ``Test.DejaFu.Conc.Basic``
+    * ``Test.DejaFu.Conc.WithSetup``
+    * ``Test.DejaFu.Conc.WithSetupAndTeardown``
+    * ``Test.DejaFu.Conc.withSetup``
+    * ``Test.DejaFu.Conc.withTeardown``
+    * ``Test.DejaFu.Conc.withSetupAndTeardown``
+
+* The ``Invariant`` type and associated functions (re-exported from
+  ``Test.DejaFu``):
+    * ``Test.DejaFu.Conc.Invariant``
+    * ``Test.DejaFu.Conc.registerInvariant``
+    * ``Test.DejaFu.Conc.inspectIORef``
+    * ``Test.DejaFu.Conc.inspectMVar``
+    * ``Test.DejaFu.Conc.inspectTVar``
+
+* New snapshotting functions:
+    * ``Test.DejaFu.Conc.Snapshot``
+    * ``Test.DejaFu.Conc.recordSnapshot``
+    * ``Test.DejaFu.Conc.runSnapshot``
+
+* ``Test.DejaFu.Settings.llengthBound``, which now applies to all ways
+  of testing.
+
+* ``Test.DejaFu.Types.isInvariantFailure`` (re-exported from
+  ``Test.DejaFu``).
+
+* ``Test.DejaFu.runTestWithSettings`` function.
+
+* A simplified form of the concurrency state:
+    * ``Test.DejaFu.Types.ConcurrencyState``
+    * ``Test.DejaFu.Types.isBuffered``
+    * ``Test.DejaFu.Types.numBuffered``
+    * ``Test.DejaFu.Types.isFull``
+    * ``Test.DejaFu.Types.canInterrupt``
+    * ``Test.DejaFu.Types.canInterruptL``
+    * ``Test.DejaFu.Types.isMaskedInterruptible``
+    * ``Test.DejaFu.Types.isMaskedUninterruptible``
+
+Changed
+~~~~~~~
+
+* ``Test.DejaFu.Schedule.Scheduler`` has a ``ConcurrencyState``
+  parameter.
+
+* ``Test.DejaFu.alwaysSameBy`` and ``Test.DejaFu.notAlwaysSameBy``
+  return a representative trace for each unique condition.
+
+* Functions which took a ``ConcT`` now take a ``Program pty``:
+    * ``Test.DejaFu.autocheck``
+    * ``Test.DejaFu.autocheckWay``
+    * ``Test.DejaFu.autocheckWithSettings``
+    * ``Test.DejaFu.dejafu``
+    * ``Test.DejaFu.dejafuWay``
+    * ``Test.DejaFu.dejafuWithSettings``
+    * ``Test.DejaFu.dejafus``
+    * ``Test.DejaFu.dejafusWay``
+    * ``Test.DejaFu.dejafusWithSettings``
+    * ``Test.DejaFu.runTest``
+    * ``Test.DejaFu.runTestWay``
+    * ``Test.DejaFu.runTestWithSettings``
+    * ``Test.DejaFu.Conc.runConcurrent``
+    * ``Test.DejaFu.SCT.runSCT``
+    * ``Test.DejaFu.SCT.resultsSet``
+    * ``Test.DejaFu.SCT.runSCT'``
+    * ``Test.DejaFu.SCT.resultsSet'``
+    * ``Test.DejaFu.SCT.runSCTWithSettings``
+    * ``Test.DejaFu.SCT.resultsSetWithSettings``
+    * ``Test.DejaFu.SCT.runSCTWithSettings'``
+    * ``Test.DejaFu.SCT.resultsSetWithSettings'``
+
+* ``Test.DejaFu.Conc.ConcT`` is an alias for ``Program Basic``.
+
+* ``Test.DejaFu.Types.Bounds``:
+    * Removed ``boundLength`` field.
+
+* ``Test.DejaFu.Types.Condition``:
+    * Added ``InvariantFailure`` constructor
+    * Removed ``STMDeadlock`` constructor
+
+* ``Test.DejaFu.Types.Error``:
+    * Removed ``NestedSubconcurrency``, ``MultithreadedSubconcurrency``,
+      and ``LateDontCheck`` constructors.
+
+* ``Test.DejaFu.Types.Lookahead``:
+    * Added ``WillRegisterInvariant`` constructor
+    * Removed ``WillSubconcurrency``, ``WillStopSubconcurrency``, and
+      ``WillDontCheck`` constructors
+
+* ``Test.DejaFu.Types.ThreadAction``:
+    * Added ``RegisterInvariant`` constructor
+    * Removed ``Subconcurrency``, ``StopSubconcurrency``, and
+      ``DontCheck`` constructors
+
+Removed
+~~~~~~~
+
+* The deprecated functions:
+    * ``Test.DejaFu.dejafuDiscard``
+    * ``Test.DejaFu.SCT.runSCTDiscard``
+    * ``Test.DejaFu.SCT.runSCTDiscard'``
+    * ``Test.DejaFu.SCT.resultsSetDiscard``
+    * ``Test.DejaFu.SCT.resultsSetDiscard'``
+    * ``Test.DejaFu.SCT.sctBound``
+    * ``Test.DejaFu.SCT.sctBoundDiscard``
+    * ``Test.DejaFu.SCT.sctUniformRandom``
+    * ``Test.DejaFu.SCT.sctUniformRandomDiscard``
+    * ``Test.DejaFu.SCT.sctWeightedRandom``
+    * ``Test.DejaFu.SCT.sctWeightedRandomDiscard``
+
+* The deprecated type ``Test.DejaFu.Types.Failure``
+
+* Old snapshotting functions:
+    * ``Test.DejaFu.Conc.DCSnapshot``
+    * ``Test.DejaFu.Conc.runForDCSnapshot``
+    * ``Test.DejaFu.Conc.runWithDCSnapshot``
+    * ``Test.DejaFu.Conc.canDCSnapshot``
+    * ``Test.DejaFu.Conc.threadsFromDCSnapshot``
+
+* ``Test.DejaFu.Conc.dontCheck``
+
+* ``Test.DejaFu.Conc.subconcurrency``
+
+* ``Test.DejaFu.Settings.defaultLengthBound``
+
+* ``Test.DejaFu.Types.isIncorrectUsage``
+
+
 1.12.0.0 (2019-01-20)
 ---------------------
 
diff --git a/Test/DejaFu.hs b/Test/DejaFu.hs
--- a/Test/DejaFu.hs
+++ b/Test/DejaFu.hs
@@ -2,16 +2,20 @@
 
 {- |
 Module      : Test.DejaFu
-Copyright   : (c) 2015--2018 Michael Walker
+Copyright   : (c) 2015--2019 Michael Walker
 License     : MIT
 Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 Stability   : experimental
 Portability : TupleSections
 
-dejafu is a library for unit-testing concurrent Haskell programs,
-written using the [concurrency](https://hackage.haskell.org/package/concurrency)
-package's 'MonadConc' typeclass.
+dejafu is a library for unit-testing concurrent Haskell programs which
+are written using the <https://hackage.haskell.org/package/concurrency
+concurrency> package's 'MonadConc' typeclass.
 
+For more in-depth documentation, including migration guides from
+earlier versions of dejafu, see the <https://dejafu.readthedocs.io
+website>.
+
 __A first test:__ This is a simple concurrent program which forks two
 threads and each races to write to the same @MVar@:
 
@@ -46,16 +50,66 @@
 
  * Each \"-\" represents one \"step\" of the computation.
 
-__Conditions:__ A program may fail to terminate in a way which
-produces a value. dejafu can detect a few such cases:
+__Memory models:__ dejafu supports three different memory models,
+which affect how one thread's 'IORef' updates become visible to other
+threads.
 
- * 'Deadlock', if every thread is blocked.
+ * Sequential consistency: a program behaves as a simple interleaving
+   of the actions in different threads. When an 'IORef' is written to,
+   that write is immediately visible to all threads.
 
- * 'STMDeadlock', if every thread is blocked /and/ the main thread is
-   blocked in an STM transaction.
+  * Total store order (TSO): each thread has a write buffer.  A thread
+    sees its writes immediately, but other threads will only see
+    writes when they are committed, which may happen later.  Writes
+    are committed in the same order that they are created.
 
- * 'UncaughtException', if the main thread is killed by an exception.
+  * Partial store order (PSO): each 'IORef' has a write buffer.  A
+    thread sees its writes immediately, but other threads will only
+    see writes when they are committed, which may happen later.
+    Writes to different 'IORef's are not necessarily committed in the
+    same order that they are created.
 
+This small example shows the difference between sequential consistency
+and TSO:
+
+>>> :{
+let relaxed = do
+      r1 <- newIORef False
+      r2 <- newIORef False
+      x <- spawn $ writeIORef r1 True >> readIORef r2
+      y <- spawn $ writeIORef r2 True >> readIORef r1
+      (,) <$> readMVar x <*> readMVar y
+:}
+
+The 'autocheckWay' function will let us specify the memory model:
+
+>>> autocheckWay defaultWay SequentialConsistency relaxed
+[pass] Successful
+[fail] Deterministic
+    (False,True) S0---------S1----S0--S2----S0--
+<BLANKLINE>
+    (True,True) S0---------S1-P2----S1---S0---
+<BLANKLINE>
+    (True,False) S0---------S2----S1----S0---
+False
+
+>>> autocheckWay defaultWay TotalStoreOrder relaxed
+[pass] Successful
+[fail] Deterministic
+    (False,True) S0---------S1----S0--S2----S0--
+<BLANKLINE>
+    (False,False) S0---------S1--P2----S1--S0---
+<BLANKLINE>
+    (True,False) S0---------S2----S1----S0---
+<BLANKLINE>
+    (True,True) S0---------S1-C-S2----S1---S0---
+False
+
+The result @(False,False)@ is possible using TSO and PSO, but not
+sequential consistency.  The \"C\" in the trace shows where a /commit/
+action occurred, which makes a write to an 'IORef' visible to all
+threads.
+
 __Beware of 'liftIO':__ dejafu works by running your test case lots of
 times with different schedules.  If you use 'liftIO' at all, make sure
 that any @IO@ you perform is deterministic when executed in the same
@@ -107,9 +161,9 @@
 -}
 
   , Result(..)
-  , Condition(..)
   , runTest
   , runTestWay
+  , runTestWithSettings
 
   -- ** Predicates
 
@@ -169,23 +223,24 @@
 
 -}
 
+  , Condition(..)
   , isAbort
   , isDeadlock
   , isUncaughtException
+  , isInvariantFailure
 
-  -- * Property testing
+  -- * Property-based testing
 
   {- |
 
-dejafu can also use a property-testing style to test stateful
+dejafu can also use a property-based testing style to test stateful
 operations for a variety of inputs.  Inputs are generated using the
-[leancheck](https://hackage.haskell.org/package/leancheck) library for
+<https://hackage.haskell.org/package/leancheck leancheck> library for
 enumerative testing.
 
-__Testing @MVar@ operations with multiple producers__:
-
-These are a little different to the property tests you may be familiar
-with from libraries like QuickCheck (and leancheck).  As we're testing
+__Testing @MVar@ operations with multiple producers__: These are a
+little different to the property tests you may be familiar with from
+libraries like QuickCheck (and leancheck).  As we're testing
 properties of /stateful/ and /concurrent/ things, we need to provide
 some extra information.
 
@@ -237,11 +292,27 @@
 
   , module Test.DejaFu.Refinement
 
-  -- * Deprecated
-  , Failure
-  , dejafuDiscard
-  ) where
+  -- * Expressing concurrent programs
+  , Program
+  , Basic
+  , ConcT
+  , ConcIO
 
+  -- ** Setup and teardown
+  , WithSetup
+  , WithSetupAndTeardown
+  , withSetup
+  , withTeardown
+  , withSetupAndTeardown
+
+  -- ** Invariants
+  , Invariant
+  , registerInvariant
+  , inspectIORef
+  , inspectMVar
+  , inspectTVar
+) where
+
 import           Control.Arrow            (first)
 import           Control.DeepSeq          (NFData(..))
 import           Control.Monad            (unless, when)
@@ -302,9 +373,9 @@
 --     "world" S0----S2--S0--
 -- False
 --
--- @since 1.0.0.0
+-- @since 2.0.0.0
 autocheck :: (MonadConc n, MonadIO n, Eq a, Show a)
-  => ConcT n a
+  => Program pty n a
   -- ^ The computation to test.
   -> n Bool
 autocheck = autocheckWithSettings defaultSettings
@@ -334,13 +405,13 @@
 --     (True,False) S0---------S2----S1----S0---
 -- False
 --
--- @since 1.0.0.0
+-- @since 2.0.0.0
 autocheckWay :: (MonadConc n, MonadIO n, Eq a, Show a)
   => Way
   -- ^ How to run the concurrent program.
   -> MemType
   -- ^ The memory model to use for non-synchronised @IORef@ operations.
-  -> ConcT n a
+  -> Program pty n a
   -- ^ The computation to test.
   -> n Bool
 autocheckWay way = autocheckWithSettings . fromWayAndMemType way
@@ -369,16 +440,16 @@
 --     (True,False) S0---------S2----S1----S0---
 -- False
 --
--- @since 1.2.0.0
+-- @since 2.0.0.0
 autocheckWithSettings :: (MonadConc n, MonadIO n, Eq a, Show a)
   => Settings n a
   -- ^ The SCT settings.
-  -> ConcT n a
+  -> Program pty n a
   -- ^ The computation to test.
   -> n Bool
 autocheckWithSettings settings = dejafusWithSettings settings
   [ ("Successful", representative successful)
-  , ("Deterministic", alwaysSame) -- already representative
+  , ("Deterministic", representative alwaysSame)
   ]
 
 -- | Check a predicate and print the result to stdout, return 'True'
@@ -395,13 +466,13 @@
 --     "world" S0----S2--S0--
 -- False
 --
--- @since 1.0.0.0
+-- @since 2.0.0.0
 dejafu :: (MonadConc n, MonadIO n, Show b)
   => String
   -- ^ The name of the test.
   -> ProPredicate a b
   -- ^ The predicate to check.
-  -> ConcT n a
+  -> Program pty n a
   -- ^ The computation to test.
   -> n Bool
 dejafu = dejafuWithSettings defaultSettings
@@ -425,7 +496,7 @@
 --     "world" S0----S2--S1-S0--
 -- False
 --
--- @since 1.0.0.0
+-- @since 2.0.0.0
 dejafuWay :: (MonadConc n, MonadIO n, Show b)
   => Way
   -- ^ How to run the concurrent program.
@@ -435,7 +506,7 @@
   -- ^ The name of the test.
   -> ProPredicate a b
   -- ^ The predicate to check.
-  -> ConcT n a
+  -> Program pty n a
   -- ^ The computation to test.
   -> n Bool
 dejafuWay way = dejafuWithSettings . fromWayAndMemType way
@@ -451,7 +522,7 @@
 --     "world" S0----S2--S1-S0--
 -- False
 --
--- @since 1.2.0.0
+-- @since 2.0.0.0
 dejafuWithSettings :: (MonadConc n, MonadIO n, Show b)
   => Settings n a
   -- ^ The SCT settings.
@@ -459,40 +530,12 @@
   -- ^ The name of the test.
   -> ProPredicate a b
   -- ^ The predicate to check.
-  -> ConcT n a
+  -> Program pty n a
   -- ^ The computation to test.
   -> n Bool
 dejafuWithSettings settings name test =
   dejafusWithSettings settings [(name, test)]
 
--- | Variant of 'dejafuWay' which can selectively discard results.
---
--- >>> dejafuDiscard (\_ -> Just DiscardTrace) defaultWay defaultMemType "Discarding" alwaysSame example
--- [fail] Discarding
---     "hello" <trace discarded>
--- <BLANKLINE>
---     "world" <trace discarded>
--- False
---
--- @since 1.0.0.0
-dejafuDiscard :: (MonadConc n, MonadIO n, Show b)
-  => (Either Condition a -> Maybe Discard)
-  -- ^ Selectively discard results.
-  -> Way
-  -- ^ How to run the concurrent program.
-  -> MemType
-  -- ^ The memory model to use for non-synchronised @IORef@ operations.
-  -> String
-  -- ^ The name of the test.
-  -> ProPredicate a b
-  -- ^ The predicate to check.
-  -> ConcT n a
-  -- ^ The computation to test.
-  -> n Bool
-dejafuDiscard discard way =
-  dejafuWithSettings . set ldiscard (Just discard) . fromWayAndMemType way
-{-# DEPRECATED dejafuDiscard "Use dejafuWithSettings instead" #-}
-
 -- | Variant of 'dejafu' which takes a collection of predicates to
 -- test, returning 'True' if all pass.
 --
@@ -504,11 +547,11 @@
 -- [pass] B
 -- False
 --
--- @since 1.0.0.0
+-- @since 2.0.0.0
 dejafus :: (MonadConc n, MonadIO n, Show b)
   => [(String, ProPredicate a b)]
   -- ^ The list of predicates (with names) to check.
-  -> ConcT n a
+  -> Program pty n a
   -- ^ The computation to test.
   -> n Bool
 dejafus = dejafusWithSettings defaultSettings
@@ -526,7 +569,7 @@
 -- [pass] B
 -- False
 --
--- @since 1.0.0.0
+-- @since 2.0.0.0
 dejafusWay :: (MonadConc n, MonadIO n, Show b)
   => Way
   -- ^ How to run the concurrent program.
@@ -534,7 +577,7 @@
   -- ^ The memory model to use for non-synchronised @IORef@ operations.
   -> [(String, ProPredicate a b)]
   -- ^ The list of predicates (with names) to check.
-  -> ConcT n a
+  -> Program pty n a
   -- ^ The computation to test.
   -> n Bool
 dejafusWay way = dejafusWithSettings . fromWayAndMemType way
@@ -551,13 +594,13 @@
 -- [pass] B
 -- False
 --
--- @since 1.2.0.0
+-- @since 2.0.0.0
 dejafusWithSettings :: (MonadConc n, MonadIO n, Show b)
   => Settings n a
   -- ^ The SCT settings.
   -> [(String, ProPredicate a b)]
   -- ^ The list of predicates (with names) to check.
-  -> ConcT n a
+  -> Program pty n a
   -- ^ The computation to test.
   -> n Bool
 dejafusWithSettings settings tests conc = do
@@ -627,11 +670,11 @@
 -- found, is unspecified and may change between releases.  This may
 -- affect which failing traces are reported, when there is a failure.
 --
--- @since 1.0.0.0
+-- @since 2.0.0.0
 runTest :: MonadConc n
   => ProPredicate a b
   -- ^ The predicate to check
-  -> ConcT n a
+  -> Program pty n a
   -- ^ The computation to test
   -> n (Result b)
 runTest = runTestWithSettings defaultSettings
@@ -643,7 +686,7 @@
 -- found, is unspecified and may change between releases.  This may
 -- affect which failing traces are reported, when there is a failure.
 --
--- @since 1.0.0.0
+-- @since 2.0.0.0
 runTestWay :: MonadConc n
   => Way
   -- ^ How to run the concurrent program.
@@ -651,7 +694,7 @@
   -- ^ The memory model to use for non-synchronised @IORef@ operations.
   -> ProPredicate a b
   -- ^ The predicate to check
-  -> ConcT n a
+  -> Program pty n a
   -- ^ The computation to test
   -> n (Result b)
 runTestWay way = runTestWithSettings . fromWayAndMemType way
@@ -662,13 +705,13 @@
 -- found, is unspecified and may change between releases.  This may
 -- affect which failing traces are reported, when there is a failure.
 --
--- @since 1.2.0.0
+-- @since 2.0.0.0
 runTestWithSettings :: MonadConc n
   => Settings n a
   -- ^ The SCT settings.
   -> ProPredicate a b
   -- ^ The predicate to check
-  -> ConcT n a
+  -> Program pty n a
   -- ^ The computation to test
   -> n (Result b)
 runTestWithSettings settings p conc =
@@ -723,7 +766,7 @@
       in result { _failures = simplestsBy (==) (_failures result) }
   }
 
--- | Check that a computation never fails.
+-- | Check that a computation never produces a @Left@ value.
 --
 -- @since 1.9.1.0
 successful :: Predicate a
@@ -801,8 +844,7 @@
 exceptionsSometimes :: Predicate a
 exceptionsSometimes = somewhereTrue $ either isUncaughtException (const False)
 
--- | Check that a computation always gives the same, successful,
--- result.
+-- | Check that a computation always gives the same, @Right@, result.
 --
 -- > alwaysSame = alwaysSameBy (==)
 --
@@ -811,7 +853,7 @@
 alwaysSame = alwaysSameBy (==)
 
 -- | Check that a computation always gives the same (according to the
--- provided function), successful, result.
+-- provided function), @Right@, result.
 --
 -- > alwaysSameOn = alwaysSameBy ((==) `on` f)
 --
@@ -829,14 +871,15 @@
   , peval = \xs ->
       let (failures, successes) = partition (isLeft . fst) xs
           simpleSuccesses = simplestsBy (f `on` efromRight) successes
-      in case (failures, simpleSuccesses) of
+          simpleFailures  = simplestsBy ((==) `on` efromLeft) failures
+      in case (simpleFailures, simpleSuccesses) of
         ([], []) -> defaultPass
         ([], [_]) -> defaultPass
-        (_, _) -> defaultFail (failures ++ simpleSuccesses)
+        (_, _) -> defaultFail (simpleFailures ++ simpleSuccesses)
   }
 
 -- | Check that a computation never fails, and gives multiple distinct
--- successful results.
+-- @Right@ results.
 --
 -- > notAlwaysSame = notAlwaysSameBy (==)
 --
@@ -845,7 +888,7 @@
 notAlwaysSame = notAlwaysSameBy (==)
 
 -- | Check that a computation never fails, and gives multiple distinct
--- (according to the provided function) successful results.
+-- (according to the provided function) @Right@ results.
 --
 -- > notAlwaysSameOn = notAlwaysSameBy ((==) `on` f)
 --
@@ -854,7 +897,7 @@
 notAlwaysSameOn f = notAlwaysSameBy ((==) `on` f)
 
 -- | Check that a computation never fails, and gives multiple distinct
--- successful results, by applying a transformation on results.
+-- @Right@ results, by applying a transformation on results.
 --
 -- This inverts the condition, so (eg) @notAlwaysSameBy (==)@ will
 -- pass if there are unequal results.
@@ -865,13 +908,14 @@
     { pdiscard = const Nothing
     , peval = \xs ->
         let (failures, successes) = partition (isLeft . fst) xs
+            simpleFailures = simplestsBy ((==) `on` efromLeft) failures
         in case successes of
-          [x] -> defaultFail (x : failures)
+          [x] -> defaultFail (x : simpleFailures)
           _  ->
             let res = go successes (defaultFail [])
             in case failures of
               [] -> res
-              _ -> res { _failures = failures ++ _failures res, _pass = False }
+              _ -> res { _failures = simpleFailures ++ _failures res, _pass = False }
     }
   where
     y1 .*. y2 = not (on f (efromRight . fst) y1 y2)
@@ -945,7 +989,9 @@
 
     failures = filter (\(r, _) -> r `notElem` expected)
 
--- | Variant of 'gives' that doesn't allow for non-success conditions.
+-- | Variant of 'gives' that doesn't allow for @Left@ results.
+--
+-- > gives' = gives . map Right
 --
 -- @since 1.0.0.0
 gives' :: (Eq a, Show a) => [a] -> Predicate a
diff --git a/Test/DejaFu/Conc.hs b/Test/DejaFu/Conc.hs
--- a/Test/DejaFu/Conc.hs
+++ b/Test/DejaFu/Conc.hs
@@ -1,16 +1,10 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE TypeFamilies #-}
-
 -- |
 -- Module      : Test.DejaFu.Conc
--- Copyright   : (c) 2016--2018 Michael Walker
+-- Copyright   : (c) 2016--2019 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
--- Portability : CPP, FlexibleInstances, GeneralizedNewtypeDeriving, TypeFamilies
+-- Portability : portable
 --
 -- Deterministic traced execution of concurrent computations.
 --
@@ -18,28 +12,38 @@
 -- out to the supplied scheduler after each step to determine which
 -- thread runs next.
 module Test.DejaFu.Conc
-  ( -- * The @ConcT@ monad transformer
-    ConcT
+  ( -- * Expressing concurrent programs
+    Program
+  , Basic
+  , ConcT
   , ConcIO
 
-  -- * Executing computations
-  , Condition(..)
-  , MemType(..)
-  , runConcurrent
-  , subconcurrency
-  , dontCheck
+  -- ** Setup and teardown
+  , WithSetup
+  , WithSetupAndTeardown
+  , withSetup
+  , withTeardown
+  , withSetupAndTeardown
 
-  -- ** Snapshotting
+  -- ** Invariants
+  , Invariant
+  , registerInvariant
+  , inspectIORef
+  , inspectMVar
+  , inspectTVar
 
-  -- $snapshotting_io
+  -- * Executing concurrent programs
+  , Snapshot
+  , MemType(..)
+  , runConcurrent
+  , recordSnapshot
+  , runSnapshot
 
-  , DCSnapshot
-  , runForDCSnapshot
-  , runWithDCSnapshot
-  , canDCSnapshot
-  , threadsFromDCSnapshot
+  -- ** Scheduling
+  , module Test.DejaFu.Schedule
 
-  -- * Execution traces
+  -- * Results
+  , Condition(..)
   , Trace
   , Decision(..)
   , ThreadId(..)
@@ -50,349 +54,140 @@
   , MaskingState(..)
   , showTrace
   , showCondition
-
-  -- * Scheduling
-  , module Test.DejaFu.Schedule
-
-  -- * Deprecated
-  , Failure
   ) where
 
-import           Control.Exception                   (MaskingState(..))
-import qualified Control.Monad.Catch                 as Ca
-import           Control.Monad.Fail                  (MonadFail)
-import qualified Control.Monad.IO.Class              as IO
-import           Control.Monad.Trans.Class           (MonadTrans(..))
-import qualified Data.Foldable                       as F
-import           Data.List                           (partition)
-import qualified Data.Map.Strict                     as M
-import           Data.Maybe                          (isNothing)
-import           Test.DejaFu.Schedule
+import           Control.Exception                 (MaskingState(..))
 
-import qualified Control.Monad.Conc.Class            as C
-import           Test.DejaFu.Conc.Internal
 import           Test.DejaFu.Conc.Internal.Common
-import           Test.DejaFu.Conc.Internal.STM       (ModelSTM)
-import           Test.DejaFu.Conc.Internal.Threading (_blocking)
-import           Test.DejaFu.Internal
+import           Test.DejaFu.Conc.Internal.Program
+import           Test.DejaFu.Conc.Internal.STM     (ModelTVar)
+import           Test.DejaFu.Schedule
 import           Test.DejaFu.Types
 import           Test.DejaFu.Utils
 
+-------------------------------------------------------------------------------
+-- Expressing concurrent programs
+
 -- | @since 1.4.0.0
-newtype ConcT n a = C { unC :: ModelConc n a }
-  deriving (Functor, Applicative, Monad, MonadFail)
+type ConcT = Program Basic
 
 -- | A 'MonadConc' implementation using @IO@.
 --
 -- @since 0.4.0.0
 type ConcIO = ConcT IO
 
-toConc :: ((a -> Action n) -> Action n) -> ConcT n a
-toConc = C . ModelConc
-
-wrap :: (ModelConc n a -> ModelConc n a) -> ConcT n a -> ConcT n a
-wrap f = C . f . unC
-
--- | @since 1.0.0.0
-instance IO.MonadIO n => IO.MonadIO (ConcT n) where
-  liftIO ma = toConc (\c -> ALift (fmap c (IO.liftIO ma)))
-
-instance MonadTrans ConcT where
-  lift ma = toConc (\c -> ALift (fmap c ma))
-
-instance Ca.MonadCatch (ConcT n) where
-  catch ma h = toConc (ACatching (unC . h) (unC ma))
-
-instance Ca.MonadThrow (ConcT n) where
-  throwM e = toConc (\_ -> AThrow e)
-
-instance Ca.MonadMask (ConcT n) where
-  mask                mb = toConc (AMasking MaskedInterruptible   (\f -> unC $ mb $ wrap f))
-  uninterruptibleMask mb = toConc (AMasking MaskedUninterruptible (\f -> unC $ mb $ wrap f))
-
-#if MIN_VERSION_exceptions(0,10,0)
-  generalBracket acquire release use = Ca.mask $ \unmasked -> do
-    resource <- acquire
-    b <- unmasked (use resource) `Ca.catch` (\e -> release resource (Ca.ExitCaseException e) >> Ca.throwM e)
-    c <- release resource (Ca.ExitCaseSuccess b)
-    pure (b, c)
-#elif MIN_VERSION_exceptions(0,9,0)
-  -- from https://github.com/fpco/stackage/issues/3315#issuecomment-368583481
-  generalBracket acquire release cleanup use = Ca.mask $ \unmasked -> do
-    resource <- acquire
-    result <- unmasked (use resource) `Ca.catch` (\e -> cleanup resource e >> Ca.throwM e)
-    _ <- release resource
-    pure result
-#endif
-
-instance Monad n => C.MonadConc (ConcT n) where
-  type MVar     (ConcT n) = ModelMVar n
-  type IORef    (ConcT n) = ModelIORef n
-  type Ticket   (ConcT n) = ModelTicket
-  type STM      (ConcT n) = ModelSTM n
-  type ThreadId (ConcT n) = ThreadId
-
-  -- ----------
-
-  forkWithUnmaskN   n ma = toConc (AFork n (\umask -> runModelConc (unC $ ma $ wrap umask) (\_ -> AStop (pure ()))))
-  forkOnWithUnmaskN n _  = C.forkWithUnmaskN n
-  forkOSWithUnmaskN n ma
-    | C.rtsSupportsBoundThreads =
-      toConc (AForkOS n (\umask -> runModelConc (unC $ ma $ wrap umask) (\_ -> AStop (pure ()))))
-    | otherwise = fail "RTS doesn't support multiple OS threads (use ghc -threaded when linking)"
-
-  isCurrentThreadBound = toConc AIsBound
-
-  -- This implementation lies and returns 2 until a value is set. This
-  -- will potentially avoid special-case behaviour for 1 capability,
-  -- so it seems a sane choice.
-  getNumCapabilities      = toConc AGetNumCapabilities
-  setNumCapabilities caps = toConc (\c -> ASetNumCapabilities caps (c ()))
-
-  myThreadId = toConc AMyTId
-
-  yield = toConc (\c -> AYield (c ()))
-  threadDelay n = toConc (\c -> ADelay n (c ()))
-
-  -- ----------
-
-  newIORefN n a = toConc (ANewIORef n a)
-
-  readIORef   ref = toConc (AReadIORef    ref)
-  readForCAS ref = toConc (AReadIORefCas ref)
-
-  peekTicket' _ = ticketVal
-
-  writeIORef ref      a = toConc (\c -> AWriteIORef ref a (c ()))
-  casIORef   ref tick a = toConc (ACasIORef ref tick a)
-
-  atomicModifyIORef ref f = toConc (AModIORef    ref f)
-  modifyIORefCAS    ref f = toConc (AModIORefCas ref f)
-
-  -- ----------
-
-  newEmptyMVarN n = toConc (ANewMVar n)
-
-  putMVar  var a = toConc (\c -> APutMVar var a (c ()))
-  readMVar var   = toConc (AReadMVar var)
-  takeMVar var   = toConc (ATakeMVar var)
-
-  tryPutMVar  var a = toConc (ATryPutMVar  var a)
-  tryReadMVar var   = toConc (ATryReadMVar var)
-  tryTakeMVar var   = toConc (ATryTakeMVar var)
-
-  -- ----------
-
-  throwTo tid e = toConc (\c -> AThrowTo tid e (c ()))
-
-  -- ----------
-
-  atomically = toConc . AAtom
-
--- | Run a concurrent computation with a given 'Scheduler' and initial
--- state, returning either the final result or the condition which
--- prevented that. Also returned is the final state of the scheduler,
--- and an execution trace.
---
--- If the RTS supports bound threads (ghc -threaded when linking) then
--- the main thread of the concurrent computation will be bound, and
--- @forkOS@ / @forkOSN@ will work during execution.  If not, then the
--- main thread will not be found, and attempting to fork a bound
--- thread will raise an error.
---
--- __Warning:__ Blocking on the action of another thread in 'liftIO'
--- cannot be detected! So if you perform some potentially blocking
--- action in a 'liftIO' the entire collection of threads may deadlock!
--- You should therefore keep @IO@ blocks small, and only perform
--- blocking operations with the supplied primitives, insofar as
--- possible.
---
--- __Note:__ In order to prevent computation from hanging, the runtime
--- will assume that a deadlock situation has arisen if the scheduler
--- attempts to (a) schedule a blocked thread, or (b) schedule a
--- nonexistent thread. In either of those cases, the computation will
--- be halted.
---
--- @since 1.0.0.0
-runConcurrent :: C.MonadConc n
-  => Scheduler s
-  -> MemType
-  -> s
-  -> ConcT n a
-  -> n (Either Condition a, s, Trace)
-runConcurrent sched memtype s ma = do
-  res <- runConcurrency False sched memtype s initialIdSource 2 (unC ma)
-  out <- efromJust <$> C.readIORef (finalRef res)
-  pure ( out
-       , cSchedState (finalContext res)
-       , F.toList (finalTrace res)
-       )
+-------------------------------------------------------------------------------
+-- Setup & teardown
 
--- | Run a concurrent computation and return its result.
+-- | A concurrent program with some set-up action.
 --
--- This can only be called in the main thread, when no other threads
--- exist. Calls to 'subconcurrency' cannot be nested, or placed inside
--- a call to 'dontCheck'. Violating either of these conditions will
--- result in the computation throwing a @NestedSubconcurrency@ or
--- @MultithreadedSubconcurrency@ error.
+-- In terms of results, this is the same as @setup >>= program@.
+-- However, the setup action will be __snapshotted__ (see
+-- 'recordSnapshot' and 'runSnapshot') by the testing functions.  This
+-- means that even if dejafu runs this program many many times, the
+-- setup action will only be run the first time, and its effects
+-- remembered for subsequent executions.
 --
--- @since 0.6.0.0
-subconcurrency :: ConcT n a -> ConcT n (Either Condition a)
-subconcurrency ma = toConc (ASub (unC ma))
+-- @since 2.0.0.0
+withSetup
+  :: Program Basic n x
+  -- ^ Setup action
+  -> (x -> Program Basic n a)
+  -- ^ Main program
+  -> Program (WithSetup x) n a
+withSetup setup p = WithSetup
+  { wsSetup   = setup
+  , wsProgram = p
+  }
 
--- | Run an arbitrary action which gets some special treatment:
---
---  * For systematic testing, 'dontCheck' is not dependent with
---    anything, even if the action has dependencies.
---
---  * For pre-emption bounding, 'dontCheck' counts for zero
---    pre-emptions, even if the action performs pre-emptive context
---    switches.
---
---  * For fair bounding, 'dontCheck' counts for zero yields/delays,
---    even if the action performs yields or delays.
+-- | A concurrent program with some set-up and teardown actions.
 --
---  * For length bounding, 'dontCheck' counts for one step, even if
---    the action has many.
+-- This is similar to
 --
---   * All SCT functions use 'runForDCSnapshot' / 'runWithDCSnapshot'
---     to ensure that the action is only executed once, although you
---     should be careful with @IO@ (see note on snapshotting @IO@).
+-- @
+-- do
+--   x <- setup
+--   y <- program x
+--   teardown x y
+-- @
 --
--- The action is executed atomically with a deterministic scheduler
--- under sequential consistency.  Any threads created inside the
--- action continue to exist in the main computation.
+-- But with two differences:
 --
--- This must be the first thing done in the main thread.  Violating
--- this condition will result in the computation throwing a
--- @LateDontCheck@ exception.
+--   * The setup action can be __snapshotted__, as described for
+--     'withSetup'
 --
--- If the action does not successfully produce a value (deadlock,
--- length bound exceeded, etc), the whole computation is terminated.
+--   * The teardown action will be executed even if the main action
+--     fails to produce a value.
 --
--- @since 1.1.0.0
-dontCheck
-  :: Maybe Int
-  -- ^ An optional length bound.
-  -> ConcT n a
-  -- ^ The action to execute.
-  -> ConcT n a
-dontCheck lb ma = toConc (ADontCheck lb (unC ma))
-
--------------------------------------------------------------------------------
--- Snapshotting
+-- @since 2.0.0.0
+withTeardown
+  :: (x -> Either Condition y -> Program Basic n a)
+  -- ^ Teardown action
+  -> Program (WithSetup x) n y
+  -- ^ Main program
+  -> Program (WithSetupAndTeardown x y) n a
+withTeardown teardown ws = WithSetupAndTeardown
+  { wstSetup    = wsSetup ws
+  , wstProgram  = wsProgram ws
+  , wstTeardown = teardown
+  }
 
--- $snapshotting_io
---
--- __Snapshotting @IO@:__ A snapshot captures entire state of your
--- concurrent program: the state of every thread, the number of
--- capabilities, the values of any @IORef@s, @MVar@s, and @TVar@s, and
--- records any @IO@ that you performed.
---
--- When restoring a snapshot this @IO@ is replayed, in order.  But the
--- whole snapshotted computation is not.  So the effects of the @IO@
--- take place again, but any return values are ignored.  For example,
--- this program will not do what you want:
+-- | A combination of 'withSetup' and 'withTeardown' for convenience.
 --
 -- @
--- bad_snapshot = do
---   r <- dontCheck Nothing $ do
---     r <- liftIO (newIORef 0)
---     liftIO (modifyIORef r (+1))
---     pure r
---   liftIO (readIORef r)
+-- withSetupAndTeardown setup teardown =
+--   withTeardown teardown . withSetup setup
 -- @
 --
--- When the snapshot is taken, the value in the @IORef@ will be 1.
--- When the snapshot is restored for the first time, those @IO@
--- actions will be run again, /but their return values will be discarded/.
--- The value in the @IORef@ will be 2.  When the snapshot
--- is restored for the second time, the value in the @IORef@ will be
--- 3.  And so on.
---
--- To safely use @IO@ in a snapshotted computation, __the combined effect must be idempotent__.
--- You should either use actions which set the state to the final
--- value directly, rather than modifying it (eg, using a combination
--- of @liftIO . readIORef@ and @liftIO . writeIORef@ here), or reset
--- the state to a known value.  Both of these approaches will work:
+-- @since 2.0.0.0
+withSetupAndTeardown
+  :: Program Basic n x
+  -- ^ Setup action
+  -> (x -> Either Condition y -> Program Basic n a)
+  -- ^ Teardown action
+  -> (x -> Program Basic n y)
+  -- ^ Main program
+  -> Program (WithSetupAndTeardown x y) n a
+withSetupAndTeardown setup teardown =
+  withTeardown teardown . withSetup setup
+
+-------------------------------------------------------------------------------
+-- Invariants
+
+-- | Call this in the setup phase to register new invariant which will
+-- be checked after every scheduling point in the main phase.
+-- Invariants are atomic actions which can inspect the shared state of
+-- your computation.
 --
--- @
--- good_snapshot1 = do
---   r <- dontCheck Nothing $ do
---     let modify r f = liftIO (readIORef r) >>= liftIO . writeIORef r . f
---     r <- liftIO (newIORef 0)
---     modify r (+1)
---     pure r
---   liftIO (readIORef r)
+-- If the invariant throws an exception, the execution will be aborted
+-- with n @InvariantFailure@.  Any teardown action will still be run.
 --
--- good_snapshot2 = do
---   r <- dontCheck Nothing $ do
---     r <- liftIO (newIORef 0)
---     liftIO (writeIORef r 0)
---     liftIO (modifyIORef r (+1))
---     pure r
---   liftIO (readIORef r)
--- @
+-- @since 2.0.0.0
+registerInvariant :: Invariant n a -> Program Basic n ()
+registerInvariant inv = ModelConc (\c -> ANewInvariant (() <$ inv) (c ()))
 
--- | Like 'runConcurrent', but terminates immediately after running
--- the 'dontCheck' action with a 'DCSnapshot' which can be used in
--- 'runWithDCSnapshot' to avoid doing that work again.
---
--- If this program does not contain a legal use of 'dontCheck', then
--- the result will be @Nothing@.
+-- | Read the content of an @IORef@.
 --
--- If you are using the SCT functions on an action which contains a
--- 'dontCheck', snapshotting will be handled for you, without you
--- needing to call this function yourself.
+-- This returns the globally visible value, which may not be the same
+-- as the value visible to any particular thread when using a memory
+-- model other than 'SequentialConsistency'.
 --
--- @since 1.1.0.0
-runForDCSnapshot :: C.MonadConc n
-  => ConcT n a
-  -> n (Maybe (Either Condition (DCSnapshot n a), Trace))
-runForDCSnapshot ma = do
-  res <- runConcurrency True roundRobinSchedNP SequentialConsistency () initialIdSource 2 (unC ma)
-  out <- C.readIORef (finalRef res)
-  pure $ case (finalRestore res, out) of
-    (Just _, Just (Left f)) -> Just (Left f, F.toList (finalTrace res))
-    (Just restore, _) -> Just (Right (DCSnapshot (finalContext res) restore (finalRef res)), F.toList (finalTrace res))
-    (_, _) -> Nothing
+-- @since 2.0.0.0
+inspectIORef :: ModelIORef n a -> Invariant n a
+inspectIORef = Invariant . IInspectIORef
 
--- | Like 'runConcurrent', but uses a 'DCSnapshot' produced by
--- 'runForDCSnapshot' to skip the 'dontCheck' work.
+-- | Read the content of an @MVar@.
 --
--- If you are using the SCT functions on an action which contains a
--- 'dontCheck', snapshotting will be handled for you, without you
--- needing to call this function yourself.
+-- This is essentially @tryReadMVar@.
 --
--- @since 1.1.0.0
-runWithDCSnapshot :: C.MonadConc n
-  => Scheduler s
-  -> MemType
-  -> s
-  -> DCSnapshot n a
-  -> n (Either Condition a, s, Trace)
-runWithDCSnapshot sched memtype s snapshot = do
-  let context = (dcsContext snapshot) { cSchedState = s }
-  let restore = dcsRestore snapshot
-  let ref = dcsRef snapshot
-  res <- runConcurrencyWithSnapshot sched memtype context restore ref
-  out <- efromJust <$> C.readIORef (finalRef res)
-  pure ( out
-       , cSchedState (finalContext res)
-       , F.toList (finalTrace res)
-       )
+-- @since 2.0.0.0
+inspectMVar :: ModelMVar n a -> Invariant n (Maybe a)
+inspectMVar = Invariant . IInspectMVar
 
--- | Check if a 'DCSnapshot' can be taken from this computation.
+-- | Read the content of a @TVar@.
 --
--- @since 1.1.0.0
-canDCSnapshot :: ConcT n a -> Bool
-canDCSnapshot (C (ModelConc k)) = lookahead (k undefined) == WillDontCheck
-
--- | Get the threads which exist in a snapshot, partitioned into
--- runnable and not runnable.
+-- This is essentially @readTVar@.
 --
--- @since 1.1.0.0
-threadsFromDCSnapshot :: DCSnapshot n a -> ([ThreadId], [ThreadId])
-threadsFromDCSnapshot snapshot = partition isRunnable (M.keys threads) where
-  threads = cThreads (dcsContext snapshot)
-  isRunnable tid = isNothing (_blocking =<< M.lookup tid threads)
+-- @since 2.0.0.0
+inspectTVar :: ModelTVar n a -> Invariant n a
+inspectTVar = Invariant . IInspectTVar
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
@@ -1,4 +1,5 @@
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE RecordWildCards #-}
@@ -9,7 +10,7 @@
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
--- Portability : FlexibleContexts, MultiWayIf, RankNTypes, RecordWildCards
+-- Portability : FlexibleContexts, LambdaCase, MultiWayIf, RankNTypes, RecordWildCards
 --
 -- Concurrent monads with a fixed scheduler: internal types and
 -- functions. This module is NOT considered to form part of the public
@@ -21,14 +22,13 @@
                                                       toException)
 import qualified Control.Monad.Catch                 as E
 import qualified Control.Monad.Conc.Class            as C
-import           Data.Foldable                       (foldrM, toList)
+import           Data.Foldable                       (foldrM)
 import           Data.Functor                        (void)
-import           Data.List                           (sortOn)
+import           Data.List                           (nub, partition, sortOn)
 import qualified Data.Map.Strict                     as M
-import           Data.Maybe                          (fromMaybe, isJust,
-                                                      isNothing)
+import           Data.Maybe                          (isJust, isNothing)
 import           Data.Monoid                         ((<>))
-import           Data.Sequence                       (Seq, (<|))
+import           Data.Sequence                       (Seq)
 import qualified Data.Sequence                       as Seq
 import           GHC.Stack                           (HasCallStack)
 
@@ -51,32 +51,19 @@
 data CResult n g a = CResult
   { finalContext :: Context n g
   , finalRef :: C.IORef n (Maybe (Either Condition a))
-  , finalRestore :: Maybe (Threads n -> n ())
+  , finalRestore :: Threads n -> n ()
   -- ^ Meaningless if this result doesn't come from a snapshotting
   -- execution.
   , finalTrace :: SeqTrace
   , finalDecision :: Maybe (ThreadId, ThreadAction)
   }
 
--- | A snapshot of the concurrency state immediately after 'dontCheck'
--- finishes.
---
--- @since 1.4.0.0
-data DCSnapshot n a = DCSnapshot
-  { dcsContext :: Context n ()
-  -- ^ The execution context.  The scheduler state is ignored when
-  -- restoring.
-  , dcsRestore :: Threads n -> n ()
-  -- ^ Action to restore IORef, MVar, and TVar values.
-  , dcsRef :: C.IORef n (Maybe (Either Condition a))
-  -- ^ Reference where the result will be written.
-  }
-
 -- | Run a concurrent computation with a given 'Scheduler' and initial
 -- state, returning a Condition reason on error. Also returned is the
 -- final state of the scheduler, and an execution trace.
 runConcurrency :: (C.MonadConc n, HasCallStack)
-  => Bool
+  => [Invariant n ()]
+  -> Bool
   -> Scheduler g
   -> MemType
   -> g
@@ -84,34 +71,22 @@
   -> Int
   -> ModelConc n a
   -> n (CResult n g a)
-runConcurrency forSnapshot sched memtype g idsrc caps ma = do
-  let ctx = Context { cSchedState = g
-                    , cIdSource   = idsrc
-                    , cThreads    = M.empty
-                    , cWriteBuf   = emptyBuffer
-                    , cCaps       = caps
+runConcurrency invariants forSnapshot sched memtype g idsrc caps ma = do
+  let ctx = Context { cSchedState    = g
+                    , cIdSource      = idsrc
+                    , cThreads       = M.empty
+                    , cWriteBuf      = emptyBuffer
+                    , cCaps          = caps
+                    , cInvariants    = InvariantContext { icActive = invariants, icBlocked = [] }
+                    , cNewInvariants = []
+                    , cCState        = initialCState
                     }
-  res <- runConcurrency' forSnapshot sched memtype ctx ma
-  killAllThreads (finalContext res)
-  pure res
-
--- | Run a concurrent program using the given context, and without
--- killing threads which remain at the end.  The context must have no
--- main thread.
---
--- Only a separate function because @ADontCheck@ needs it.
-runConcurrency' :: (C.MonadConc n, HasCallStack)
-  => Bool
-  -> Scheduler g
-  -> MemType
-  -> Context n g
-  -> ModelConc n a
-  -> n (CResult n g a)
-runConcurrency' forSnapshot sched memtype ctx ma = do
   (c, ref) <- runRefCont AStop (Just . Right) (runModelConc ma)
   let threads0 = launch' Unmasked initialThread (const c) (cThreads ctx)
   threads <- (if C.rtsSupportsBoundThreads then makeBound initialThread else pure) threads0
-  runThreads forSnapshot sched memtype ref ctx { cThreads = threads }
+  res <- runThreads forSnapshot sched memtype ref ctx { cThreads = threads }
+  killAllThreads (finalContext res)
+  pure res
 
 -- | Like 'runConcurrency' but starts from a snapshot.
 runConcurrencyWithSnapshot :: (C.MonadConc n, HasCallStack)
@@ -119,13 +94,17 @@
   -> MemType
   -> Context n g
   -> (Threads n -> n ())
-  -> C.IORef n (Maybe (Either Condition a))
+  -> ModelConc n a
   -> n (CResult n g a)
-runConcurrencyWithSnapshot sched memtype ctx restore ref = do
-  let boundThreads = M.filter (isJust . _bound) (cThreads ctx)
-  threads <- foldrM makeBound (cThreads ctx) (M.keys boundThreads)
-  restore threads
-  res <- runThreads False sched memtype ref ctx { cThreads = threads }
+runConcurrencyWithSnapshot sched memtype ctx restore ma = do
+  (c, ref) <- runRefCont AStop (Just . Right) (runModelConc ma)
+  let threads0 = M.delete initialThread (cThreads ctx)
+  let threads1 = launch' Unmasked initialThread (const c) threads0
+  let boundThreads = M.filter (isJust . _bound) threads1
+  threads2 <- (if C.rtsSupportsBoundThreads then makeBound initialThread else pure) threads1
+  threads3 <- foldrM makeBound threads2 (M.keys boundThreads)
+  restore threads3
+  res <- runThreads False sched memtype ref ctx { cThreads = threads3 }
   killAllThreads (finalContext res)
   pure res
 
@@ -140,11 +119,14 @@
 
 -- | The context a collection of threads are running in.
 data Context n g = Context
-  { cSchedState :: g
-  , cIdSource   :: IdSource
-  , cThreads    :: Threads n
-  , cWriteBuf   :: WriteBuffer n
-  , cCaps       :: Int
+  { cSchedState    :: g
+  , cIdSource      :: IdSource
+  , cThreads       :: Threads n
+  , cWriteBuf      :: WriteBuffer n
+  , cCaps          :: Int
+  , cInvariants    :: InvariantContext n
+  , cNewInvariants :: [Invariant n ()]
+  , cCState        :: ConcurrencyState
   }
 
 -- | Run a collection of threads, until there are no threads left.
@@ -166,7 +148,7 @@
   stop finalR finalT finalD finalC = pure CResult
     { finalContext  = finalC
     , finalRef      = ref
-    , finalRestore  = if forSnapshot then Just finalR else Nothing
+    , finalRestore  = finalR
     , finalTrace    = finalT
     , finalDecision = finalD
     }
@@ -175,7 +157,6 @@
   schedule restore sofar prior ctx
     | isTerminated  = stop restore sofar prior ctx
     | isDeadlocked  = die Deadlock restore sofar prior ctx
-    | isSTMLocked   = die STMDeadlock restore sofar prior ctx
     | otherwise =
       let ctx' = ctx { cSchedState = g' }
       in case choice of
@@ -192,19 +173,14 @@
              Nothing -> E.throwM ScheduledMissingThread
            Nothing -> die Abort restore sofar prior ctx'
     where
-      (choice, g')  = scheduleThread sched prior (efromList runnable') (cSchedState ctx)
+      (choice, g')  = scheduleThread sched prior (efromList runnable') (cCState ctx) (cSchedState ctx)
       runnable'     = [(t, lookahead (_continuation a)) | (t, a) <- sortOn fst $ M.assocs runnable]
       runnable      = M.filter (not . isBlocked) threadsc
       threadsc      = addCommitThreads (cWriteBuf ctx) threads
       threads       = cThreads ctx
       isBlocked     = isJust . _blocking
       isTerminated  = initialThread `notElem` M.keys threads
-      isDeadlocked  = M.null (M.filter (not . isBlocked) threads) &&
-        (((~=  OnMVarFull  undefined) <$> M.lookup initialThread threads) == Just True ||
-         ((~=  OnMVarEmpty undefined) <$> M.lookup initialThread threads) == Just True ||
-         ((~=  OnMask      undefined) <$> M.lookup initialThread threads) == Just True)
-      isSTMLocked = M.null (M.filter (not . isBlocked) threads) &&
-        ((~=  OnTVar []) <$> M.lookup initialThread threads) == Just True
+      isDeadlocked  = M.null (M.filter (not . isBlocked) threads)
 
   -- run the chosen thread for one step and then pass control back to
   -- 'schedule'
@@ -223,33 +199,36 @@
             if forSnapshot
             then restore threads' >> actionSnap threads'
             else restore threads'
-      let ctx' = fixContext chosen res ctx
+      let ctx' = fixContext memtype chosen actOrTrc res ctx
       case res of
-        Succeeded _ ->
-          schedule restore' sofar' prior' ctx'
+        Succeeded _ -> checkInvariants (cInvariants ctx') >>= \case
+          Right ic ->
+            schedule restore' sofar' prior' ctx' { cInvariants = ic }
+          Left exc ->
+            die (InvariantFailure exc) restore' sofar' prior' ctx'
         Failed failure ->
           die failure restore' sofar' prior' ctx'
-        Snap _ ->
-          stop actionSnap sofar' prior' ctx'
     where
-      getTrc (Single a) = Seq.singleton (decision, alternatives, a)
-      getTrc (SubC as _) = (decision, alternatives, Subconcurrency) <| as
+      getTrc a = Seq.singleton (decision, alternatives, a)
 
-      getPrior (Single a) = Just (chosen, a)
-      getPrior (SubC _ finalD) = finalD
+      getPrior a = Just (chosen, a)
 
 -- | Apply the context update from stepping an action.
-fixContext :: ThreadId -> What n g -> Context n g -> Context n g
-fixContext chosen (Succeeded ctx@Context{..}) _ =
-  ctx { cThreads = delCommitThreads $
-        if (interruptible <$> M.lookup chosen cThreads) /= Just False
-        then unblockWaitingOn chosen cThreads
-        else cThreads
+fixContext :: MemType -> ThreadId -> ThreadAction -> What n g -> Context n g -> Context n g
+fixContext memtype tid act what ctx0 = fixContextCommon $ case what of
+    Succeeded ctx@Context{..} -> ctx
+      { cThreads =
+          if (interruptible <$> M.lookup tid cThreads) /= Just False
+          then unblockWaitingOn tid cThreads
+          else cThreads
       }
-fixContext _ (Failed _) ctx@Context{..} =
-  ctx { cThreads = delCommitThreads cThreads }
-fixContext _ (Snap ctx@Context{..}) _ =
-  ctx { cThreads = delCommitThreads cThreads }
+    _ -> ctx0
+  where
+  fixContextCommon ctx@Context{..} = ctx
+    { cThreads    = delCommitThreads cThreads
+    , cInvariants = unblockInvariants act cInvariants
+    , cCState     = updateCState memtype cCState tid act
+    }
 
 -- | @unblockWaitingOn tid@ unblocks every thread blocked in a
 -- @throwTo tid@.
@@ -261,22 +240,12 @@
 --------------------------------------------------------------------------------
 -- * Single-step execution
 
--- | What a thread did, for trace purposes.
-data Act
-  = Single ThreadAction
-  -- ^ Just one action.
-  | SubC SeqTrace (Maybe (ThreadId, ThreadAction))
-  -- ^ @subconcurrency@, with the given trace and final action.
-  deriving (Eq, Show)
-
 -- | What a thread did, for execution purposes.
 data What n g
   = Succeeded (Context n g)
   -- ^ Action succeeded: continue execution.
   | Failed Condition
   -- ^ Action caused computation to fail: stop.
-  | Snap (Context n g)
-  -- ^ Action was a snapshot point and we're in snapshot mode: stop.
 
 -- | Run a single thread one step, by dispatching on the type of
 -- 'Action'.
@@ -302,13 +271,13 @@
   -- ^ Action to step
   -> Context n g
   -- ^ The execution context.
-  -> n (What n g, Act, Threads n -> n ())
+  -> n (What n g, ThreadAction, Threads n -> n ())
 -- start a new thread, assigning it the next 'ThreadId'
 stepThread _ _ _ _ tid (AFork n a b) = \ctx@Context{..} -> pure $
   let (idSource', newtid) = nextTId n cIdSource
       threads' = launch tid newtid a cThreads
   in ( Succeeded ctx { cThreads = goto (b newtid) tid threads', cIdSource = idSource' }
-     , Single (Fork newtid)
+     , Fork newtid
      , const (pure ())
      )
 
@@ -318,7 +287,7 @@
   let threads' = launch tid newtid a cThreads
   threads'' <- makeBound newtid threads'
   pure ( Succeeded ctx { cThreads = goto (b newtid) tid threads'', cIdSource = idSource' }
-       , Single (ForkOS newtid)
+       , ForkOS newtid
        , const (pure ())
        )
 
@@ -326,42 +295,42 @@
 stepThread _ _ _ _ tid (AIsBound c) = \ctx@Context{..} -> do
   let isBound = isJust . _bound $ elookup tid cThreads
   pure ( Succeeded ctx { cThreads = goto (c isBound) tid cThreads }
-       , Single (IsCurrentThreadBound isBound)
+       , IsCurrentThreadBound isBound
        , const (pure ())
        )
 
 -- get the 'ThreadId' of the current thread
 stepThread _ _ _ _ tid (AMyTId c) = \ctx@Context{..} ->
   pure ( Succeeded ctx { cThreads = goto (c tid) tid cThreads }
-       , Single MyThreadId
+       , MyThreadId
        , const (pure ())
        )
 
 -- get the number of capabilities
 stepThread _ _ _ _ tid (AGetNumCapabilities c) = \ctx@Context{..} ->
   pure ( Succeeded ctx { cThreads = goto (c cCaps) tid cThreads }
-       , Single (GetNumCapabilities cCaps)
+       , GetNumCapabilities cCaps
        , const (pure ())
        )
 
 -- set the number of capabilities
 stepThread _ _ _ _ tid (ASetNumCapabilities i c) = \ctx@Context{..} ->
   pure ( Succeeded ctx { cThreads = goto c tid cThreads, cCaps = i }
-       , Single (SetNumCapabilities i)
+       , SetNumCapabilities i
        , const (pure ())
        )
 
 -- yield the current thread
 stepThread _ _ _ _ tid (AYield c) = \ctx@Context{..} ->
   pure ( Succeeded ctx { cThreads = goto c tid cThreads }
-       , Single Yield
+       , Yield
        , const (pure ())
        )
 
 -- yield the current thread (delay is ignored)
 stepThread _ _ _ _ tid (ADelay n c) = \ctx@Context{..} ->
   pure ( Succeeded ctx { cThreads = goto c tid cThreads }
-       , Single (ThreadDelay n)
+       , ThreadDelay n
        , const (pure ())
        )
 
@@ -371,7 +340,7 @@
   ref <- C.newIORef Nothing
   let mvar = ModelMVar newmvid ref
   pure ( Succeeded ctx { cThreads = goto (c mvar) tid cThreads, cIdSource = idSource' }
-       , Single (NewMVar newmvid)
+       , NewMVar newmvid
        , const (C.writeIORef ref Nothing)
        )
 
@@ -379,7 +348,7 @@
 stepThread _ _ _ _ tid (APutMVar mvar@ModelMVar{..} a c) = synchronised $ \ctx@Context{..} -> do
   (success, threads', woken, effect) <- putIntoMVar mvar a c tid cThreads
   pure ( Succeeded ctx { cThreads = threads' }
-       , Single (if success then PutMVar mvarId woken else BlockedPutMVar mvarId)
+       , if success then PutMVar mvarId woken else BlockedPutMVar mvarId
        , const effect
        )
 
@@ -387,7 +356,7 @@
 stepThread _ _ _ _ tid (ATryPutMVar mvar@ModelMVar{..} a c) = synchronised $ \ctx@Context{..} -> do
   (success, threads', woken, effect) <- tryPutIntoMVar mvar a c tid cThreads
   pure ( Succeeded ctx { cThreads = threads' }
-       , Single (TryPutMVar mvarId success woken)
+       , TryPutMVar mvarId success woken
        , const effect
        )
 
@@ -396,7 +365,7 @@
 stepThread _ _ _ _ tid (AReadMVar mvar@ModelMVar{..} c) = synchronised $ \ctx@Context{..} -> do
   (success, threads', _, _) <- readFromMVar mvar c tid cThreads
   pure ( Succeeded ctx { cThreads = threads' }
-       , Single (if success then ReadMVar mvarId else BlockedReadMVar mvarId)
+       , if success then ReadMVar mvarId else BlockedReadMVar mvarId
        , const (pure ())
        )
 
@@ -405,7 +374,7 @@
 stepThread _ _ _ _ tid (ATryReadMVar mvar@ModelMVar{..} c) = synchronised $ \ctx@Context{..} -> do
   (success, threads', _, _) <- tryReadFromMVar mvar c tid cThreads
   pure ( Succeeded ctx { cThreads = threads' }
-       , Single (TryReadMVar mvarId success)
+       , TryReadMVar mvarId success
        , const (pure ())
        )
 
@@ -413,7 +382,7 @@
 stepThread _ _ _ _ tid (ATakeMVar mvar@ModelMVar{..} c) = synchronised $ \ctx@Context{..} -> do
   (success, threads', woken, effect) <- takeFromMVar mvar c tid cThreads
   pure ( Succeeded ctx { cThreads = threads' }
-       , Single (if success then TakeMVar mvarId woken else BlockedTakeMVar mvarId)
+       , if success then TakeMVar mvarId woken else BlockedTakeMVar mvarId
        , const effect
        )
 
@@ -421,7 +390,7 @@
 stepThread _ _ _ _ tid (ATryTakeMVar mvar@ModelMVar{..} c) = synchronised $ \ctx@Context{..} -> do
   (success, threads', woken, effect) <- tryTakeFromMVar mvar c tid cThreads
   pure ( Succeeded ctx { cThreads = threads' }
-       , Single (TryTakeMVar mvarId success woken)
+       , TryTakeMVar mvarId success woken
        , const effect
        )
 
@@ -432,7 +401,7 @@
   ioref <- C.newIORef val
   let ref = ModelIORef newiorid ioref
   pure ( Succeeded ctx { cThreads = goto (c ref) tid cThreads, cIdSource = idSource' }
-       , Single (NewIORef newiorid)
+       , NewIORef newiorid
        , const (C.writeIORef ioref val)
        )
 
@@ -440,7 +409,7 @@
 stepThread _ _ _ _  tid (AReadIORef ref@ModelIORef{..} c) = \ctx@Context{..} -> do
   val <- readIORef ref tid
   pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads }
-       , Single (ReadIORef iorefId)
+       , ReadIORef iorefId
        , const (pure ())
        )
 
@@ -448,7 +417,7 @@
 stepThread _ _ _ _ tid (AReadIORefCas ref@ModelIORef{..} c) = \ctx@Context{..} -> do
   tick <- readForTicket ref tid
   pure ( Succeeded ctx { cThreads = goto (c tick) tid cThreads }
-       , Single (ReadIORefCas iorefId)
+       , ReadIORefCas iorefId
        , const (pure ())
        )
 
@@ -457,7 +426,7 @@
   (new, val) <- f <$> readIORef ref tid
   effect <- writeImmediate ref new
   pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads }
-       , Single (ModIORef iorefId)
+       , ModIORef iorefId
        , const effect
        )
 
@@ -467,7 +436,7 @@
   let (new, val) = f old
   (_, _, effect) <- casIORef ref tid tick new
   pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads }
-       , Single (ModIORefCas iorefId)
+       , ModIORefCas iorefId
        , const effect
        )
 
@@ -477,21 +446,21 @@
   SequentialConsistency -> do
     effect <- writeImmediate ref a
     pure ( Succeeded ctx { cThreads = goto c tid cThreads }
-         , Single (WriteIORef iorefId)
+         , WriteIORef iorefId
          , const effect
          )
   -- add to buffer using thread id.
   TotalStoreOrder -> do
     wb' <- bufferWrite cWriteBuf (tid, Nothing) ref a
     pure ( Succeeded ctx { cThreads = goto c tid cThreads, cWriteBuf = wb' }
-         , Single (WriteIORef iorefId)
+         , WriteIORef iorefId
          , const (pure ())
          )
   -- add to buffer using both thread id and IORef id
   PartialStoreOrder -> do
     wb' <- bufferWrite cWriteBuf (tid, Just iorefId) ref a
     pure ( Succeeded ctx { cThreads = goto c tid cThreads, cWriteBuf = wb' }
-         , Single (WriteIORef iorefId)
+         , WriteIORef iorefId
          , const (pure ())
          )
 
@@ -499,7 +468,7 @@
 stepThread _ _ _ _ tid (ACasIORef ref@ModelIORef{..} tick a c) = synchronised $ \ctx@Context{..} -> do
   (suc, tick', effect) <- casIORef ref tid tick a
   pure ( Succeeded ctx { cThreads = goto (c (suc, tick')) tid cThreads }
-       , Single (CasIORef iorefId suc)
+       , CasIORef iorefId suc
        , const effect
        )
 
@@ -516,7 +485,7 @@
     PartialStoreOrder ->
       commitWrite cWriteBuf (t, Just c)
   pure ( Succeeded ctx { cWriteBuf = wb' }
-       , Single (CommitIORef t c)
+       , CommitIORef t c
        , const (pure ())
        )
 
@@ -529,22 +498,21 @@
     Success _ written val -> do
       let (threads', woken) = wake (OnTVar written) cThreads
       pure ( Succeeded ctx { cThreads = goto (c val) tid threads', cIdSource = idSource' }
-           , Single (STM trace woken)
+           , STM trace woken
            , effect
            )
     Retry touched -> do
       let threads' = block (OnTVar touched) tid cThreads
       pure ( Succeeded ctx { cThreads = threads', cIdSource = idSource'}
-           , Single (BlockedSTM trace)
+           , BlockedSTM trace
            , effect
            )
     Exception e -> do
       let act = STM trace []
       res' <- stepThrow (const act) tid e ctx
       pure $ case res' of
-        (Succeeded ctx', _, effect') -> (Succeeded ctx' { cIdSource = idSource' }, Single act, effect')
-        (Failed err, _, effect') -> (Failed err, Single act, effect')
-        (Snap _, _, _) -> fatal "stepThread.AAtom" "Unexpected snapshot while propagating STM exception"
+        (Succeeded ctx', _, effect') -> (Succeeded ctx' { cIdSource = idSource' }, act, effect')
+        (Failed err, _, effect') -> (Failed err, act, effect')
 
 -- lift an action from the underlying monad into the @Conc@
 -- computation.
@@ -552,7 +520,7 @@
   let effect threads = runLiftedAct tid threads na
   a <- effect cThreads
   pure (Succeeded ctx { cThreads = goto a tid cThreads }
-       , Single LiftIO
+       , LiftIO
        , void <$> effect
        )
 
@@ -569,12 +537,12 @@
          | interruptible thread -> stepThrow (ThrowTo t) t e ctx { cThreads = threads' }
          | otherwise -> pure
            ( Succeeded ctx { cThreads = blocked }
-           , Single (BlockedThrowTo t)
+           , BlockedThrowTo t
            , const (pure ())
            )
        Nothing -> pure
          (Succeeded ctx { cThreads = threads' }
-         , Single (ThrowTo t False)
+         , ThrowTo t False
          , const (pure ())
          )
 
@@ -583,14 +551,14 @@
   let a     = runModelConc ma (APopCatching . c)
       e exc = runModelConc (h exc) c
   in ( Succeeded ctx { cThreads = goto a tid (catching e tid cThreads) }
-     , Single Catching
+     , Catching
      , const (pure ())
      )
 
 -- pop the top exception handler from the thread's stack.
 stepThread _ _ _ _ tid (APopCatching a) = \ctx@Context{..} ->
   pure ( Succeeded ctx { cThreads = goto a tid (uncatching tid cThreads) }
-       , Single PopCatching
+       , PopCatching
        , const (pure ())
        )
 
@@ -602,21 +570,21 @@
       m' = _masking $ elookup tid cThreads
       a  = runModelConc (ma umask) (AResetMask False False m' . c)
   in ( Succeeded ctx { cThreads = goto a tid (mask m tid cThreads) }
-     , Single (SetMasking False m)
+     , SetMasking False m
      , const (pure ())
      )
 
 -- reset the masking thread of the state.
 stepThread _ _ _ _ tid (AResetMask b1 b2 m c) = \ctx@Context{..} ->
   pure ( Succeeded ctx { cThreads = goto c tid (mask m tid cThreads) }
-       , Single ((if b1 then SetMasking else ResetMasking) b2 m)
+       , (if b1 then SetMasking else ResetMasking) b2 m
        , const (pure ())
        )
 
 -- execute a 'return' or 'pure'.
 stepThread _ _ _ _ tid (AReturn c) = \ctx@Context{..} ->
   pure ( Succeeded ctx { cThreads = goto c tid cThreads }
-       , Single Return
+       , Return
        , const (pure ())
        )
 
@@ -625,61 +593,20 @@
   na
   threads' <- kill tid cThreads
   pure ( Succeeded ctx { cThreads = threads' }
-       , Single Stop
+       , Stop
        , const (pure ())
        )
 
--- run a subconcurrent computation.
-stepThread forSnapshot _ sched memtype tid (ASub ma c) = \ctx ->
-  if | forSnapshot -> E.throwM NestedSubconcurrency
-     | M.size (cThreads ctx) > 1 -> E.throwM MultithreadedSubconcurrency
-     | otherwise -> do
-         res <- runConcurrency False sched memtype (cSchedState ctx) (cIdSource ctx) (cCaps ctx) ma
-         out <- efromJust <$> C.readIORef (finalRef res)
-         pure ( Succeeded ctx
-                { cThreads    = goto (AStopSub (c out)) tid (cThreads ctx)
-                , cIdSource   = cIdSource (finalContext res)
-                , cSchedState = cSchedState (finalContext res)
-                }
-              , SubC (finalTrace res) (finalDecision res)
-              , const (pure ())
-              )
-
--- after the end of a subconcurrent computation. does nothing, only
--- exists so that: there is an entry in the trace for returning to
--- normal computation; and every item in the trace corresponds to a
--- scheduling point.
-stepThread _ _ _ _ tid (AStopSub c) = \ctx@Context{..} ->
-  pure ( Succeeded ctx { cThreads = goto c tid cThreads }
-       , Single StopSubconcurrency
+-- register an invariant to be checked in the next execution
+stepThread _ _ _ _ tid (ANewInvariant inv c) = \ctx@Context{..} ->
+  pure ( Succeeded ctx
+         { cThreads = goto c tid cThreads
+         , cNewInvariants = inv : cNewInvariants
+         }
+       , RegisterInvariant
        , const (pure ())
        )
 
--- run an action atomically, with a non-preemptive length bounded
--- round robin scheduler, under sequential consistency.
-stepThread forSnapshot isFirst _ _ tid (ADontCheck lb ma c) = \ctx ->
-  if | isFirst -> do
-         -- create a restricted context
-         threads' <- kill tid (cThreads ctx)
-         let dcCtx = ctx { cThreads = threads', cSchedState = lb }
-         res <- runConcurrency' forSnapshot dcSched SequentialConsistency dcCtx ma
-         out <- efromJust <$> C.readIORef (finalRef res)
-         case out of
-           Right a -> do
-             let threads'' = launch' Unmasked tid (const (c a)) (cThreads (finalContext res))
-             threads''' <- (if C.rtsSupportsBoundThreads then makeBound tid else pure) threads''
-             pure ( (if forSnapshot then Snap else Succeeded) (finalContext res)
-                    { cThreads = threads''', cSchedState = cSchedState ctx }
-                  , Single (DontCheck (toList (finalTrace res)))
-                  , fromMaybe (const (pure ())) (finalRestore res)
-                  )
-           Left f -> pure
-             ( Failed f
-             , Single (DontCheck (toList (finalTrace res)))
-             , const (pure ())
-             )
-     | otherwise -> E.throwM LateDontCheck
-
 -- | Handle an exception being thrown from an @AAtom@, @AThrow@, or
 -- @AThrowTo@.
 stepThrow :: (C.MonadConc n, Exception e)
@@ -691,23 +618,23 @@
   -- ^ Exception to raise.
   -> Context n g
   -- ^ The execution context.
-  -> n (What n g, Act, Threads n -> n ())
+  -> n (What n g, ThreadAction, Threads n -> n ())
 stepThrow act tid e ctx@Context{..} = case propagate some tid cThreads of
     Just ts' -> pure
       ( Succeeded ctx { cThreads = ts' }
-      , Single (act False)
+      , act False
       , const (pure ())
       )
     Nothing
       | tid == initialThread -> pure
         ( Failed (UncaughtException some)
-        , Single (act True)
+        , act True
         , const (pure ())
         )
       | otherwise -> do
           ts' <- kill tid cThreads
           pure ( Succeeded ctx { cThreads = ts' }
-               , Single (act True)
+               , act True
                , const (pure ())
                )
   where
@@ -715,19 +642,107 @@
 
 -- | Helper for actions impose a write barrier.
 synchronised :: C.MonadConc n
-  => (Context n g -> n (What n g, Act, Threads n -> n ()))
+  => (Context n g -> n x)
   -- ^ Action to run after the write barrier.
   -> Context n g
   -- ^ The original execution context.
-  -> n (What n g, Act, Threads n -> n ())
+  -> n x
 synchronised ma ctx@Context{..} = do
   writeBarrier cWriteBuf
   ma ctx { cWriteBuf = emptyBuffer }
 
--- | scheduler for @ADontCheck@
-dcSched :: Scheduler (Maybe Int)
-dcSched = Scheduler go where
-  go _ _ (Just 0) = (Nothing, Just 0)
-  go prior threads s =
-    let (t, _) = scheduleThread roundRobinSchedNP prior threads ()
-    in (t, fmap (\lb -> lb - 1) s)
+--------------------------------------------------------------------------------
+-- * Invariants
+
+-- | The state of the invariants
+data InvariantContext n = InvariantContext
+  { icActive  :: [Invariant n ()]
+  , icBlocked :: [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
+  }
+
+-- | @unblockInvariants act@ unblocks every invariant which could have
+-- its result changed by @act@.
+unblockInvariants ::  ThreadAction -> InvariantContext n -> InvariantContext n
+unblockInvariants act ic = InvariantContext active blocked where
+  active = map fst unblocked ++ icActive ic
+
+  (unblocked, blocked) = (`partition` icBlocked ic) $
+    \(_, (ioridsB, mvidsB, tvidsB)) ->
+      maybe False (`elem` ioridsB) (iorefOf (simplifyAction act)) ||
+      maybe False (`elem` mvidsB)  (mvarOf (simplifyAction act))  ||
+      any (`elem` tvidsB) (tvarsOf act)
+
+-- | Check all active invariants, returning an arbitrary failure if
+-- multiple ones fail.
+checkInvariants :: C.MonadConc n
+  => InvariantContext n
+  -> n (Either E.SomeException (InvariantContext n))
+checkInvariants ic = go (icActive ic) >>= \case
+    Right blocked -> pure (Right (InvariantContext [] (blocked ++ icBlocked ic)))
+    Left exc -> pure (Left exc)
+  where
+    go (inv:is) = checkInvariant inv >>= \case
+      Right o -> fmap ((inv,o):) <$> go is
+      Left exc -> pure (Left exc)
+    go [] = pure (Right [])
+
+-- | Check an invariant.
+checkInvariant :: C.MonadConc n
+  => Invariant n a
+  -> n (Either E.SomeException ([IORefId], [MVarId], [TVarId]))
+checkInvariant inv = doInvariant inv >>= \case
+  (Right _, iorefs, mvars, tvars) -> pure (Right (iorefs, mvars, tvars))
+  (Left exc, _, _, _) -> pure (Left exc)
+
+-- | Run an invariant (more primitive)
+doInvariant :: C.MonadConc n
+  => Invariant n a
+  -> n (Either E.SomeException a, [IORefId], [MVarId], [TVarId])
+doInvariant inv = do
+    (c, ref) <- runRefCont IStop (Just . Right) (runInvariant inv)
+    (iorefs, mvars, tvars) <- go ref c [] [] []
+    val <- C.readIORef ref
+    pure (efromJust val, nub iorefs, nub mvars, nub tvars)
+  where
+    go ref act iorefs mvars tvars = do
+      (res, iorefs', mvars', tvars') <- stepInvariant act
+      let newIORefs = iorefs' ++ iorefs
+      let newMVars  = mvars'  ++ mvars
+      let newTVars  = tvars'  ++ tvars
+      case res of
+        Right (Just act') ->
+          go ref act' newIORefs newMVars newTVars
+        Right Nothing ->
+          pure (newIORefs, newMVars, newTVars)
+        Left exc -> do
+          C.writeIORef ref (Just (Left exc))
+          pure (newIORefs, newMVars, newTVars)
+
+-- | Run an invariant for one step
+stepInvariant :: C.MonadConc n
+  => IAction n
+  -> n (Either E.SomeException (Maybe (IAction n)), [IORefId], [MVarId], [TVarId])
+stepInvariant (IInspectIORef ioref@ModelIORef{..} k) = do
+  a <- readIORefGlobal ioref
+  pure (Right (Just (k a)), [iorefId], [], [])
+stepInvariant (IInspectMVar ModelMVar{..} k) = do
+  a <- C.readIORef mvarRef
+  pure (Right (Just (k a)), [], [mvarId], [])
+stepInvariant (IInspectTVar ModelTVar{..} k) = do
+  a <- C.readIORef tvarRef
+  pure (Right (Just (k a)), [], [], [tvarId])
+stepInvariant (ICatch h nx k) = doInvariant nx >>= \case
+  (Right a, iorefs, mvars, tvars) ->
+    pure (Right (Just (k a)), iorefs, mvars, tvars)
+  (Left exc, iorefs, mvars, tvars) -> case E.fromException exc of
+    Just exc' -> doInvariant (h exc') >>= \case
+      (Right a, iorefs', mvars', tvars') ->
+        pure (Right (Just (k a)), iorefs' ++ iorefs, mvars' ++ mvars, tvars' ++ tvars)
+      (Left exc'', iorefs', mvars', tvars') ->
+        pure (Left exc'', iorefs' ++ iorefs, mvars' ++ mvars, tvars' ++ tvars)
+    Nothing -> pure (Left exc, iorefs, mvars, tvars)
+stepInvariant (IThrow exc) =
+  pure (Left (toException exc), [], [], [])
+stepInvariant (IStop finalise) = do
+  finalise
+  pure (Right Nothing, [], [], [])
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
@@ -1,13 +1,14 @@
 {-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 
 -- |
 -- Module      : Test.DejaFu.Conc.Internal.Common
--- Copyright   : (c) 2016--2018 Michael Walker
+-- Copyright   : (c) 2016--2019 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
--- Portability : ExistentialQuantification, RankNTypes
+-- Portability : ExistentialQuantification, GADTs, RankNTypes
 --
 -- Common types and utility functions for deterministic execution of
 -- 'MonadConc' implementations. This module is NOT considered to form
@@ -15,14 +16,16 @@
 module Test.DejaFu.Conc.Internal.Common where
 
 import           Control.Exception             (Exception, MaskingState(..))
+import           Control.Monad.Catch           (MonadCatch(..), MonadThrow(..))
 import qualified Control.Monad.Conc.Class      as C
 import qualified Control.Monad.Fail            as Fail
 import           Data.Map.Strict               (Map)
-import           Test.DejaFu.Conc.Internal.STM (ModelSTM)
+
+import           Test.DejaFu.Conc.Internal.STM (ModelSTM, ModelTVar)
 import           Test.DejaFu.Types
 
 --------------------------------------------------------------------------------
--- * The @ModelConc@ Monad
+-- * Types for Modelling Concurrency
 
 -- | The underlying monad is based on continuations over 'Action's.
 --
@@ -32,26 +35,73 @@
 -- current expression of threads and exception handlers very difficult
 -- (perhaps even not possible without significant reworking), so I
 -- abandoned the attempt.
-newtype ModelConc n a = ModelConc { runModelConc :: (a -> Action n) -> Action n }
+type ModelConc = Program Basic
 
-instance Functor (ModelConc n) where
-    fmap f m = ModelConc $ \c -> runModelConc m (c . f)
+-- | A representation of a concurrent program for testing.
+--
+-- To construct these, use the 'C.MonadConc' instance, or see
+-- 'Test.DejaFu.Conc.withSetup', 'Test.DejaFu.Conc.withTeardown', and
+-- 'Test.DejaFu.Conc.withSetupAndTeardown'.
+--
+-- @since 2.0.0.0
+data Program pty n a where
+  ModelConc ::
+    { runModelConc :: (a -> Action n) -> Action n
+    } -> Program Basic n a
+  WithSetup ::
+    { wsSetup   :: ModelConc n x
+    , wsProgram :: x -> ModelConc n a
+    } -> Program (WithSetup x) n a
+  WithSetupAndTeardown ::
+    { wstSetup    :: ModelConc n x
+    , wstProgram  :: x -> ModelConc n y
+    , wstTeardown :: x -> Either Condition y -> ModelConc n a
+    } -> Program (WithSetupAndTeardown x y) n a
 
-instance Applicative (ModelConc n) where
-    -- without the @AReturn@, a thread could lock up testing by
-    -- entering an infinite loop (eg: @forever (return ())@)
-    pure x  = ModelConc $ \c -> AReturn $ c x
-    f <*> v = ModelConc $ \c -> runModelConc f (\g -> runModelConc v (c . g))
+-- | A type used to constrain 'Program': a @Program Basic@ is a
+-- \"basic\" program with no set-up or teardown.
+--
+-- Construct with the 'MonadConc' instance.
+--
+-- @since 2.0.0.0
+data Basic
 
-instance Monad (ModelConc n) where
-    return  = pure
-    m >>= k = ModelConc $ \c -> runModelConc m (\x -> runModelConc (k x) c)
+-- | A type used to constrain 'Program': a @Program (WithSetup x)@ is
+-- a program with some set-up action producing a value of type @x@.
+--
+-- Construct with 'Test.DejaFu.Conc.withSetup'.
+--
+-- @since 2.0.0.0
+data WithSetup x
 
-    fail = Fail.fail
+-- | A type used to constrain 'Program': a @Program
+-- (WithSetupAndTeardown x y)@ is a program producing a value of type
+-- @y@ with some set-up action producing a value of type @x@ and a
+-- teardown action producing the final result.
+--
+-- Construct with 'Test.DejaFu.Conc.withTeardown' or
+-- 'Test.DejaFu.Conc.withSetupAndTeardown'.
+--
+-- @since 2.0.0.0
+data WithSetupAndTeardown x y
 
-instance Fail.MonadFail (ModelConc n) where
-    fail e = ModelConc $ \_ -> AThrow (MonadFailException e)
+instance (pty ~ Basic) => Functor (Program pty n) where
+  fmap f m = ModelConc $ \c -> runModelConc m (c . f)
 
+instance (pty ~ Basic) => Applicative (Program pty n) where
+  -- without the @AReturn@, a thread could lock up testing by entering
+  -- an infinite loop (eg: @forever (return ())@)
+  pure x  = ModelConc $ \c -> AReturn $ c x
+  f <*> v = ModelConc $ \c -> runModelConc f (\g -> runModelConc v (c . g))
+
+instance (pty ~ Basic) => Monad (Program pty n) where
+  return  = pure
+  fail    = Fail.fail
+  m >>= k = ModelConc $ \c -> runModelConc m (\x -> runModelConc (k x) c)
+
+instance (pty ~ Basic) => Fail.MonadFail (Program pty n) where
+  fail e = ModelConc $ \_ -> AThrow (MonadFailException e)
+
 -- | An @MVar@ is modelled as a unique ID and a reference holding a
 -- @Maybe@ value.
 data ModelMVar n a = ModelMVar
@@ -77,7 +127,7 @@
   }
 
 --------------------------------------------------------------------------------
--- * Primitive Actions
+-- ** Primitive Actions
 
 -- | Scheduling is done in terms of a trace of 'Action's. Blocking can
 -- only occur as a result of an action, and they cover (most of) the
@@ -123,12 +173,10 @@
   | ACommit ThreadId IORefId
   | AStop (n ())
 
-  | forall a. ASub (ModelConc n a) (Either Condition a -> Action n)
-  | AStopSub (Action n)
-  | forall a. ADontCheck (Maybe Int) (ModelConc n a) (a -> Action n)
+  | ANewInvariant (Invariant n ()) (Action n)
 
 --------------------------------------------------------------------------------
--- * Scheduling & Traces
+-- ** Scheduling & Traces
 
 -- | Look as far ahead in the given continuation as possible.
 lookahead :: Action n -> Lookahead
@@ -165,6 +213,51 @@
 lookahead (ADelay n _) = WillThreadDelay n
 lookahead (AReturn _) = WillReturn
 lookahead (AStop _) = WillStop
-lookahead (ASub _ _) = WillSubconcurrency
-lookahead (AStopSub _) = WillStopSubconcurrency
-lookahead (ADontCheck _ _ _) = WillDontCheck
+lookahead (ANewInvariant _ _) = WillRegisterInvariant
+
+-------------------------------------------------------------------------------
+-- * Invariants
+
+-- | Invariants are atomic actions which can inspect the shared state
+-- of your computation, and terminate it on failure.  Invariants have
+-- no visible effects, and are checked after each scheduling point.
+--
+-- To be checked, an invariant must be created during the setup phase
+-- of your 'Program', using 'Test.DejaFu.Conc.registerInvariant'.  The
+-- invariant will then be checked in the main phase (but not in the
+-- setup or teardown phase).  As a consequence of this, any shared
+-- state you want your invariant to check must also be created in the
+-- setup phase, and passed into the main phase as a parameter.
+--
+-- @since 2.0.0.0
+newtype Invariant n a = Invariant { runInvariant :: (a -> IAction n) -> IAction n }
+
+instance Functor (Invariant n) where
+  fmap f m = Invariant $ \c -> runInvariant m (c . f)
+
+instance Applicative (Invariant n) where
+  pure x  = Invariant $ \c -> c x
+  f <*> v = Invariant $ \c -> runInvariant f (\g -> runInvariant v (c . g))
+
+instance Monad (Invariant n) where
+  return  = pure
+  fail    = Fail.fail
+  m >>= k = Invariant $ \c -> runInvariant m (\x -> runInvariant (k x) c)
+
+instance Fail.MonadFail (Invariant n) where
+  fail e = Invariant $ \_ -> IThrow (MonadFailException e)
+
+instance MonadThrow (Invariant n) where
+  throwM e = Invariant $ \_ -> IThrow e
+
+instance MonadCatch (Invariant n) where
+  catch stm handler = Invariant $ ICatch handler stm
+
+-- | Invariants are represented as a sequence of primitive actions.
+data IAction n
+  = forall a. IInspectIORef (ModelIORef n a) (a -> IAction n)
+  | forall a. IInspectMVar  (ModelMVar  n a) (Maybe a -> IAction n)
+  | forall a. IInspectTVar  (ModelTVar  n a) (a -> IAction n)
+  | forall a e. Exception e => ICatch (e -> Invariant n a) (Invariant n a) (a -> IAction n)
+  | forall e. Exception e => IThrow e
+  | IStop (n ())
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
@@ -114,6 +114,12 @@
   (vals, count, def) <- C.readIORef iorefRef
   pure (M.findWithDefault def tid vals, count)
 
+-- | Read the global state of a @IORef@.
+readIORefGlobal :: C.MonadConc n => ModelIORef n a -> n a
+readIORefGlobal ModelIORef{..} = do
+  (_, _, def) <- C.readIORef iorefRef
+  pure def
+
 -- | Write and commit to a @IORef@ immediately, clearing the update map
 -- and incrementing the write count.
 writeImmediate :: C.MonadConc n => ModelIORef n a -> a -> n (n ())
diff --git a/Test/DejaFu/Conc/Internal/Program.hs b/Test/DejaFu/Conc/Internal/Program.hs
new file mode 100644
--- /dev/null
+++ b/Test/DejaFu/Conc/Internal/Program.hs
@@ -0,0 +1,374 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE TypeFamilies #-}
+
+-- GHC doesn't need this to compile the module, but stylish-haskell
+-- does to format it.
+{-# LANGUAGE FlexibleContexts #-}
+
+-- |
+-- Module      : Test.DejaFu.Conc.Internal.Program
+-- Copyright   : (c) 2019 Michael Walker
+-- License     : MIT
+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
+-- Stability   : experimental
+-- Portability : CPP, FlexibleContexts, FlexibleInstances, GADTs, LambdaCase, RecordWildCards, TypeFamilies
+--
+-- Representations of concurrent programs with setup, teardown, and
+-- snapshotting.  This module is NOT considered to form part of the
+-- public interface of this library.
+--
+-- This module defines orphan instances for the 'Program' type which
+-- lives in "Test.DejaFu.Conc.Internal.Common", to avoid needing to
+-- pull a bunch more stuff into that module.
+module Test.DejaFu.Conc.Internal.Program where
+
+import           Control.Applicative                 (Applicative(..))
+import           Control.Exception                   (MaskingState(..))
+import qualified Control.Monad.Catch                 as Ca
+import qualified Control.Monad.IO.Class              as IO
+import           Control.Monad.Trans.Class           (MonadTrans(..))
+import qualified Data.Foldable                       as F
+import           Data.List                           (partition)
+import qualified Data.Map.Strict                     as M
+import           Data.Maybe                          (isNothing)
+import           GHC.Stack                           (HasCallStack)
+
+import qualified Control.Monad.Conc.Class            as C
+import           Test.DejaFu.Conc.Internal
+import           Test.DejaFu.Conc.Internal.Common
+import           Test.DejaFu.Conc.Internal.STM       (ModelSTM)
+import           Test.DejaFu.Conc.Internal.Threading (Threads, _blocking)
+import           Test.DejaFu.Internal
+import           Test.DejaFu.Schedule
+import           Test.DejaFu.Types
+
+-------------------------------------------------------------------------------
+-- Expressing concurrent programs
+
+instance (pty ~ Basic, IO.MonadIO n) => IO.MonadIO (Program pty n) where
+  liftIO ma = ModelConc (\c -> ALift (fmap c (IO.liftIO ma)))
+
+instance (pty ~ Basic) => MonadTrans (Program pty) where
+  lift ma = ModelConc (\c -> ALift (fmap c ma))
+
+instance (pty ~ Basic) =>  Ca.MonadCatch (Program pty n) where
+  catch ma h = ModelConc (ACatching h ma)
+
+instance (pty ~ Basic) => Ca.MonadThrow (Program pty n) where
+  throwM e = ModelConc (\_ -> AThrow e)
+
+instance (pty ~ Basic) => Ca.MonadMask (Program pty n) where
+  mask                mb = ModelConc (AMasking MaskedInterruptible   (\f -> mb f))
+  uninterruptibleMask mb = ModelConc (AMasking MaskedUninterruptible (\f -> mb f))
+
+#if MIN_VERSION_exceptions(0,10,0)
+  generalBracket acquire release use = Ca.mask $ \unmasked -> do
+    resource <- acquire
+    b <- unmasked (use resource) `Ca.catch` (\e -> release resource (Ca.ExitCaseException e) >> Ca.throwM e)
+    c <- release resource (Ca.ExitCaseSuccess b)
+    pure (b, c)
+#elif MIN_VERSION_exceptions(0,9,0)
+  -- from https://github.com/fpco/stackage/issues/3315#issuecomment-368583481
+  generalBracket acquire release cleanup use = Ca.mask $ \unmasked -> do
+    resource <- acquire
+    result <- unmasked (use resource) `Ca.catch` (\e -> cleanup resource e >> Ca.throwM e)
+    _ <- release resource
+    pure result
+#endif
+
+instance (pty ~ Basic, Monad n) => C.MonadConc (Program pty n) where
+  type MVar     (Program pty n) = ModelMVar n
+  type IORef    (Program pty n) = ModelIORef n
+  type Ticket   (Program pty n) = ModelTicket
+  type STM      (Program pty n) = ModelSTM n
+  type ThreadId (Program pty n) = ThreadId
+
+  -- ----------
+
+  forkWithUnmaskN   n ma = ModelConc (AFork n (\umask -> runModelConc (ma umask) (\_ -> AStop (pure ()))))
+  forkOnWithUnmaskN n _  = C.forkWithUnmaskN n
+  forkOSWithUnmaskN n ma
+    | C.rtsSupportsBoundThreads =
+      ModelConc (AForkOS n (\umask -> runModelConc (ma umask) (\_ -> AStop (pure ()))))
+    | otherwise = fail "RTS doesn't support multiple OS threads (use ghc -threaded when linking)"
+
+  isCurrentThreadBound = ModelConc AIsBound
+
+  -- This implementation lies and returns 2 until a value is set. This
+  -- will potentially avoid special-case behaviour for 1 capability,
+  -- so it seems a sane choice.
+  getNumCapabilities      = ModelConc AGetNumCapabilities
+  setNumCapabilities caps = ModelConc (\c -> ASetNumCapabilities caps (c ()))
+
+  myThreadId = ModelConc AMyTId
+
+  yield = ModelConc (\c -> AYield (c ()))
+  threadDelay n = ModelConc (\c -> ADelay n (c ()))
+
+  -- ----------
+
+  newIORefN n a = ModelConc (ANewIORef n a)
+
+  readIORef   ref = ModelConc (AReadIORef    ref)
+  readForCAS ref = ModelConc (AReadIORefCas ref)
+
+  peekTicket' _ = ticketVal
+
+  writeIORef ref      a = ModelConc (\c -> AWriteIORef ref a (c ()))
+  casIORef   ref tick a = ModelConc (ACasIORef ref tick a)
+
+  atomicModifyIORef ref f = ModelConc (AModIORef    ref f)
+  modifyIORefCAS    ref f = ModelConc (AModIORefCas ref f)
+
+  -- ----------
+
+  newEmptyMVarN n = ModelConc (ANewMVar n)
+
+  putMVar  var a = ModelConc (\c -> APutMVar var a (c ()))
+  readMVar var   = ModelConc (AReadMVar var)
+  takeMVar var   = ModelConc (ATakeMVar var)
+
+  tryPutMVar  var a = ModelConc (ATryPutMVar  var a)
+  tryReadMVar var   = ModelConc (ATryReadMVar var)
+  tryTakeMVar var   = ModelConc (ATryTakeMVar var)
+
+  -- ----------
+
+  throwTo tid e = ModelConc (\c -> AThrowTo tid e (c ()))
+
+  -- ----------
+
+  atomically = ModelConc . AAtom
+
+-------------------------------------------------------------------------------
+-- Executing concurrent programs
+
+-- | Run a concurrent computation with a given 'Scheduler' and initial
+-- state, returning either the final result or the condition which
+-- prevented that. Also returned is the final state of the scheduler,
+-- and an execution trace.
+--
+-- If the RTS supports bound threads (ghc -threaded when linking) then
+-- the main thread of the concurrent computation will be bound, and
+-- @forkOS@ / @forkOSN@ will work during execution.  If not, then the
+-- main thread will not be found, and attempting to fork a bound
+-- thread will raise an error.
+--
+-- __Warning:__ Blocking on the action of another thread in 'liftIO'
+-- cannot be detected! So if you perform some potentially blocking
+-- action in a 'liftIO' the entire collection of threads may deadlock!
+-- You should therefore keep @IO@ blocks small, and only perform
+-- blocking operations with the supplied primitives, insofar as
+-- possible.
+--
+-- __Note:__ In order to prevent computation from hanging, the runtime
+-- will assume that a deadlock situation has arisen if the scheduler
+-- attempts to (a) schedule a blocked thread, or (b) schedule a
+-- nonexistent thread. In either of those cases, the computation will
+-- be halted.
+--
+-- @since 2.0.0.0
+runConcurrent :: C.MonadConc n
+  => Scheduler s
+  -> MemType
+  -> s
+  -> Program pty n a
+  -> n (Either Condition a, s, Trace)
+runConcurrent sched memtype s ma@(ModelConc _) = do
+  res <- runConcurrency [] False sched memtype s initialIdSource 2 ma
+  out <- efromJust <$> C.readIORef (finalRef res)
+  pure ( out
+       , cSchedState (finalContext res)
+       , F.toList (finalTrace res)
+       )
+runConcurrent sched memtype s ma = recordSnapshot ma >>= \case
+  Just (Left cond, trc) -> pure (Left cond, s, trc)
+  Just (Right snap, _)  -> runSnapshot sched memtype s snap
+  Nothing -> fatal "failed to record snapshot!"
+
+-- | Runs any setup action and returns a 'Snapshot' which can be
+-- passed to 'runSnapshot'.  If there is no setup action (this is a
+-- @Program Basic@, then @Nothing@ is returned.  The snapshot captures
+-- the state at the end of the setup, so the full program can be run
+-- multiple times without repeating the setup.
+--
+-- The setup action is executed atomically with a deterministic
+-- scheduler under sequential consistency.  Any forked threads
+-- continue to exist in the main program.
+--
+-- If the setup action does not successfully produce a value
+-- (deadlock, uncaught exception, etc), no snapshot is produced.
+--
+-- __Snapshotting @IO@:__ A snapshot captures entire state of your
+-- concurrent program: the state of every thread, the number of
+-- capabilities, the values of any @IORef@s, @MVar@s, and @TVar@s, and
+-- records any @IO@ that you performed.
+--
+-- When restoring a snapshot this @IO@ is replayed, in order.  But the
+-- whole snapshotted computation is not.  So the effects of the @IO@
+-- take place again, but any return values are ignored.  For example,
+-- this program will not do what you want:
+--
+-- @
+-- bad_snapshot = withSetup
+--   (do r <- liftIO (newIORef 0)
+--       liftIO (modifyIORef r (+1))
+--       pure r)
+--   (liftIO . readIORef)
+-- @
+--
+-- When the snapshot is taken, the value in the @IORef@ will be 1.
+-- When the snapshot is restored for the first time, those @IO@
+-- actions will be run again, /but their return values will be
+-- discarded/.  The value in the @IORef@ will be 2.  When the snapshot
+-- is restored for the second time, the value in the @IORef@ will be
+-- 3.  And so on.
+--
+-- To safely use @IO@ in a snapshotted computation, __the combined
+-- effect must be idempotent__.  You should either use actions which
+-- set the state to the final value directly, rather than modifying it
+-- (eg, using a combination of @liftIO . readIORef@ and @liftIO
+-- . writeIORef@ here), or reset the state to a known value.  Both of
+-- these approaches will work:
+--
+-- @
+-- good_snapshot1 = withSetup
+--   (do let modify r f = liftIO (readIORef r) >>= liftIO . writeIORef r . f
+--        r <- liftIO (newIORef 0)
+--        modify r (+1)
+--        pure r)
+--   (liftIO . readIORef)
+--
+-- good_snapshot2 = withSetup
+--   (do r <- liftIO (newIORef 0)
+--       liftIO (writeIORef r 0)
+--       liftIO (modifyIORef r (+1))
+--       pure r)
+--   (liftIO . readIORef)
+-- @
+--
+-- @since 2.0.0.0
+recordSnapshot
+  :: C.MonadConc n
+  => Program pty n a
+  -> n (Maybe (Either Condition (Snapshot pty n a), Trace))
+recordSnapshot ModelConc{..} = pure Nothing
+recordSnapshot WithSetup{..} =
+  let mkSnapshot snap _ = WS snap
+  in defaultRecordSnapshot mkSnapshot wsSetup wsProgram
+recordSnapshot WithSetupAndTeardown{..} =
+  let mkSnapshot snap = WSAT snap . wstTeardown
+  in defaultRecordSnapshot mkSnapshot wstSetup wstProgram
+
+-- | Runs a program with snapshotted setup to completion.
+--
+-- @since 2.0.0.0
+runSnapshot
+  :: C.MonadConc n
+  => Scheduler s
+  -> MemType
+  -> s
+  -> Snapshot pty n a
+  -> n (Either Condition a, s, Trace)
+runSnapshot sched memtype s (WS SimpleSnapshot{..}) = do
+  let context = fromSnapContext s snapContext
+  CResult{..} <- runConcurrencyWithSnapshot sched memtype context snapRestore snapNext
+  out <- efromJust <$> C.readIORef finalRef
+  pure ( out
+       , cSchedState finalContext
+       , F.toList finalTrace
+       )
+runSnapshot sched memtype s (WSAT SimpleSnapshot{..} teardown) = do
+  let context = fromSnapContext s snapContext
+  intermediateResult <- runConcurrencyWithSnapshot sched memtype context snapRestore snapNext
+  let idsrc = cIdSource (finalContext intermediateResult)
+  out1 <- efromJust <$> C.readIORef (finalRef intermediateResult)
+  teardownResult <- simpleRunConcurrency False idsrc (teardown out1)
+  out2 <- efromJust <$> C.readIORef (finalRef teardownResult)
+  pure ( out2
+       , cSchedState (finalContext intermediateResult)
+       , F.toList (finalTrace intermediateResult)
+       )
+
+-------------------------------------------------------------------------------
+-- Snapshotting
+
+-- | A record of the state of a concurrent program immediately after
+-- completing the setup action.
+--
+-- @since 2.0.0.0
+data Snapshot pty n a where
+  WS   :: SimpleSnapshot n a -> Snapshot (WithSetup x) n a
+  WSAT :: SimpleSnapshot n a -> (Either Condition a -> ModelConc n y) -> Snapshot (WithSetupAndTeardown x a) n y
+
+data SimpleSnapshot n a = SimpleSnapshot
+  { snapContext :: Context n ()
+  , snapRestore :: Threads n -> n ()
+  , snapNext    :: ModelConc n a
+  }
+
+-- | Get the 'Context' from a 'Snapshot'.
+contextFromSnapshot :: Snapshot p n a -> Context n ()
+contextFromSnapshot (WS SimpleSnapshot{..})     = snapContext
+contextFromSnapshot (WSAT SimpleSnapshot{..} _) = snapContext
+
+-- | Get the threads which exist in a snapshot, partitioned into
+-- runnable and not runnable.
+threadsFromSnapshot :: Snapshot p n a -> ([ThreadId], [ThreadId])
+threadsFromSnapshot snap = (initialThread : runnable, blocked) where
+  (runnable, blocked) = partition isRunnable (M.keys threads)
+  threads = cThreads (contextFromSnapshot snap)
+  isRunnable tid = isNothing (_blocking =<< M.lookup tid threads)
+
+-- | 'recordSnapshot' implemented generically.
+--
+-- Throws an error if the snapshot could not be produced.
+defaultRecordSnapshot :: C.MonadConc n
+  => (SimpleSnapshot n a -> x -> snap)
+  -> ModelConc n x
+  -> (x -> ModelConc n a)
+  -> n (Maybe (Either Condition snap, Trace))
+defaultRecordSnapshot mkSnapshot setup program = do
+  CResult{..} <- simpleRunConcurrency True initialIdSource setup
+  let trc = F.toList finalTrace
+  out <- C.readIORef finalRef
+  pure . Just $ case out of
+    Just (Right a) ->
+      let snap = mkSnapshot (SimpleSnapshot finalContext finalRestore (program a)) a
+      in (Right snap, trc)
+    Just (Left f) -> (Left f, trc)
+    -- alternative behaviour: return @Nothing@ here.  but this should
+    -- never fail, so it should be an error if it does.
+    Nothing -> fatal "failed to produce snapshot"
+
+-------------------------------------------------------------------------------
+-- Utilities
+
+-- | Run a concurrent program with a deterministic scheduler in
+-- snapshotting or non-snapshotting mode.
+simpleRunConcurrency ::(C.MonadConc n, HasCallStack)
+  => Bool
+  -> IdSource
+  -> ModelConc n a
+  -> n (CResult n () a)
+simpleRunConcurrency forSnapshot idsrc =
+  runConcurrency [] forSnapshot roundRobinSchedNP SequentialConsistency () idsrc 2
+
+-- | Make a new context from a snapshot context.
+fromSnapContext :: g -> Context n s -> Context n g
+fromSnapContext g ctx@Context{..} = ctx
+  { cSchedState = g
+  , cInvariants = InvariantContext
+    { icActive  = cNewInvariants
+    , icBlocked = []
+    }
+  , cNewInvariants = []
+  }
+
+wrap :: (((a -> Action n) -> Action n) -> ((a -> Action n) -> Action n)) -> ModelConc n a -> ModelConc n a
+wrap f = ModelConc . f . runModelConc
diff --git a/Test/DejaFu/Internal.hs b/Test/DejaFu/Internal.hs
--- a/Test/DejaFu/Internal.hs
+++ b/Test/DejaFu/Internal.hs
@@ -2,23 +2,26 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
 
 -- |
 -- Module      : Test.DejaFu.Internal
--- Copyright   : (c) 2017--2018 Michael Walker
+-- Copyright   : (c) 2017--2019 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
--- Portability : DeriveAnyClass, DeriveGeneric, FlexibleContexts, GADTs
+-- Portability : DeriveAnyClass, DeriveGeneric, FlexibleContexts, GADTs, LambdaCase
 --
 -- Internal types and functions used throughout DejaFu.  This module
 -- is NOT considered to form part of the public interface of this
 -- library.
 module Test.DejaFu.Internal where
 
-import           Control.DeepSeq          (NFData)
+import           Control.DeepSeq          (NFData(..))
+import           Control.Exception        (MaskingState(..))
 import qualified Control.Monad.Conc.Class as C
 import           Data.List.NonEmpty       (NonEmpty(..))
+import           Data.Map.Strict          (Map)
 import qualified Data.Map.Strict          as M
 import           Data.Maybe               (fromMaybe)
 import           Data.Set                 (Set)
@@ -37,6 +40,7 @@
 -- @since 1.2.0.0
 data Settings n a = Settings
   { _way :: Way
+  , _lengthBound :: Maybe LengthBound
   , _memtype :: MemType
   , _discard :: Maybe (Either Condition a -> Maybe Discard)
   , _debugShow :: Maybe (a -> String)
@@ -197,9 +201,7 @@
 rewind LiftIO = WillLiftIO
 rewind Return = WillReturn
 rewind Stop = WillStop
-rewind Subconcurrency = WillSubconcurrency
-rewind StopSubconcurrency = WillStopSubconcurrency
-rewind (DontCheck _) = WillDontCheck
+rewind RegisterInvariant = WillRegisterInvariant
 
 -- | Check if an operation could enable another thread.
 willRelease :: Lookahead -> Bool
@@ -217,7 +219,6 @@
 willRelease (WillSetMasking _ _) = True
 willRelease (WillResetMasking _ _) = True
 willRelease WillStop = True
-willRelease WillDontCheck = True
 willRelease _ = False
 
 -------------------------------------------------------------------------------
@@ -326,6 +327,58 @@
 simplifyLookahead _ = UnsynchronisedOther
 
 -------------------------------------------------------------------------------
+-- * Concurrency state
+
+-- | Initial concurrency state.
+initialCState :: ConcurrencyState
+initialCState = ConcurrencyState M.empty S.empty M.empty
+
+-- | Update the concurrency state with the action that has just
+-- happened.
+updateCState :: MemType -> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
+updateCState memtype cstate tid act = ConcurrencyState
+  { concIOState   = updateIOState memtype act $ concIOState   cstate
+  , concMVState   = updateMVState         act $ concMVState   cstate
+  , concMaskState = updateMaskState tid   act $ concMaskState cstate
+  }
+
+-- | Update the @IORef@ buffer state with the action that has just
+-- happened.
+updateIOState :: MemType -> ThreadAction -> Map IORefId Int -> Map IORefId Int
+updateIOState SequentialConsistency _ = const M.empty
+updateIOState _ (CommitIORef _ r) = (`M.alter` r) $ \case
+  Just 1  -> Nothing
+  Just n  -> Just (n-1)
+  Nothing -> Nothing
+updateIOState _ (WriteIORef    r) = M.insertWith (+) r 1
+updateIOState _ ta
+  | isBarrier $ simplifyAction ta = const M.empty
+  | otherwise = id
+
+-- | Update the @MVar@ full/empty state with the action that has just
+-- happened.
+updateMVState :: ThreadAction -> Set MVarId -> Set MVarId
+updateMVState (PutMVar mvid _) = S.insert mvid
+updateMVState (TryPutMVar mvid True _) = S.insert mvid
+updateMVState (TakeMVar mvid _) = S.delete mvid
+updateMVState (TryTakeMVar mvid True _) = S.delete mvid
+updateMVState _ = 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 tid (Throw True) = M.delete tid
+updateMaskState _ (ThrowTo tid True) = M.delete tid
+updateMaskState tid Stop = M.delete tid
+updateMaskState _ _ = id
+
+-------------------------------------------------------------------------------
 -- * Error reporting
 
 -- | 'tail' but with a better error message if it fails.  Use this
@@ -358,6 +411,12 @@
 efromRight :: HasCallStack => Either a b -> b
 efromRight (Right b) = b
 efromRight _ = withFrozenCallStack $ fatal "fromRight: Left"
+
+-- | 'fromLeft' but with a better error message if it fails.  Use
+-- this only where it shouldn't fail!
+efromLeft :: HasCallStack => Either a b -> a
+efromLeft (Left a) = a
+efromLeft _ = withFrozenCallStack $ fatal "fromLeft: Right"
 
 -- | 'M.adjust' but which errors if the key is not present.  Use this
 -- only where it shouldn't fail!
diff --git a/Test/DejaFu/Refinement.hs b/Test/DejaFu/Refinement.hs
--- a/Test/DejaFu/Refinement.hs
+++ b/Test/DejaFu/Refinement.hs
@@ -114,7 +114,8 @@
 import qualified Data.Set                 as S
 import           Test.LeanCheck           (Listable(..), concatMapT, mapT)
 
-import           Test.DejaFu.Conc         (ConcIO, Condition, subconcurrency)
+import           Test.DejaFu.Conc         (ConcIO, Condition,
+                                           withSetupAndTeardown)
 import           Test.DejaFu.SCT          (runSCT)
 import           Test.DejaFu.Settings     (defaultMemType, defaultWay)
 
@@ -411,12 +412,14 @@
   -> x
   -> IO (Set (Maybe Condition, o))
 evalSigWithSeed sig x = do
-  results <- runSCT defaultWay defaultMemType $ do
-    s <- initialise sig x
-    r <- subconcurrency $ do
-      _ <- fork (interfere sig s x)
-      _ <- expression sig s
-      pure ()
-    o <- observe sig s x
-    pure (either Just (const Nothing) r, o)
+  results <- runSCT defaultWay defaultMemType $
+    withSetupAndTeardown
+      (initialise sig x)
+      (\s r -> do
+          o <- observe sig s x
+          pure (either Just (const Nothing) r, o))
+      (\s -> do
+          _ <- fork (interfere sig s x)
+          _ <- expression sig s
+          pure ())
   pure . S.fromList $ map (\(Right a, _) -> a) results
diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs
--- a/Test/DejaFu/SCT.hs
+++ b/Test/DejaFu/SCT.hs
@@ -2,7 +2,7 @@
 
 -- |
 -- Module      : Test.DejaFu.SCT
--- Copyright   : (c) 2015--2018 Michael Walker
+-- Copyright   : (c) 2015--2019 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
@@ -22,18 +22,6 @@
   , resultsSetWithSettings
   , resultsSetWithSettings'
   , module Test.DejaFu.Settings
-
-  -- * Deprecated
-  , runSCTDiscard
-  , runSCTDiscard'
-  , resultsSetDiscard
-  , resultsSetDiscard'
-  , sctBound
-  , sctBoundDiscard
-  , sctUniformRandom
-  , sctUniformRandomDiscard
-  , sctWeightedRandom
-  , sctWeightedRandomDiscard
   ) where
 
 import           Control.Applicative               ((<|>))
@@ -44,7 +32,6 @@
 import           Data.Maybe                        (fromMaybe)
 import           Data.Set                          (Set)
 import qualified Data.Set                          as S
-import           System.Random                     (RandomGen)
 
 import           Test.DejaFu.Conc
 import           Test.DejaFu.Internal
@@ -64,67 +51,30 @@
 -- The exact executions tried, and the order in which results are
 -- found, is unspecified and may change between releases.
 --
--- @since 1.0.0.0
+-- @since 2.0.0.0
 runSCT :: MonadConc n
   => Way
   -- ^ How to run the concurrent program.
   -> MemType
   -- ^ The memory model to use for non-synchronised @IORef@ operations.
-  -> ConcT n a
+  -> Program pty n a
   -- ^ The computation to run many times.
   -> n [(Either Condition a, Trace)]
 runSCT way = runSCTWithSettings . fromWayAndMemType way
 
 -- | Return the set of results of a concurrent program.
 --
--- @since 1.0.0.0
+-- @since 2.0.0.0
 resultsSet :: (MonadConc n, Ord a)
   => Way
   -- ^ How to run the concurrent program.
   -> MemType
   -- ^ The memory model to use for non-synchronised @IORef@ operations.
-  -> ConcT n a
+  -> Program pty n a
   -- ^ The computation to run many times.
   -> n (Set (Either Condition a))
 resultsSet way = resultsSetWithSettings . fromWayAndMemType way
 
--- | A variant of 'runSCT' which can selectively discard results.
---
--- The exact executions tried, and the order in which results are
--- found, is unspecified and may change between releases.
---
--- @since 1.0.0.0
-runSCTDiscard :: MonadConc n
-  => (Either Condition a -> Maybe Discard)
-  -- ^ Selectively discard results.
-  -> Way
-  -- ^ How to run the concurrent program.
-  -> MemType
-  -- ^ The memory model to use for non-synchronised @IORef@ operations.
-  -> ConcT n a
-  -- ^ The computation to run many times.
-  -> n [(Either Condition a, Trace)]
-runSCTDiscard discard way = runSCTWithSettings . set ldiscard (Just discard) . fromWayAndMemType way
-{-# DEPRECATED runSCTDiscard "Use runSCTWithSettings instead" #-}
-
--- | A variant of 'resultsSet' which can selectively discard results.
---
--- @since 1.0.0.0
-resultsSetDiscard :: (MonadConc n, Ord a)
-  => (Either Condition a -> Maybe Discard)
-  -- ^ Selectively discard results.  Traces are always discarded.
-  -> Way
-  -- ^ How to run the concurrent program.
-  -> MemType
-  -- ^ The memory model to use for non-synchronised @IORef@ operations.
-  -> ConcT n a
-  -- ^ The computation to run many times.
-  -> n (Set (Either Condition a))
-resultsSetDiscard discard way memtype conc =
-  let discard' efa = discard efa <|> Just DiscardTrace
-  in S.fromList . map fst <$> runSCTDiscard discard' way memtype conc
-{-# DEPRECATED resultsSetDiscard "Use resultsSetWithSettings instead" #-}
-
 -- | A strict variant of 'runSCT'.
 --
 -- Demanding the result of this will force it to normal form, which
@@ -133,9 +83,15 @@
 -- The exact executions tried, and the order in which results are
 -- found, is unspecified and may change between releases.
 --
--- @since 1.0.0.0
+-- @since 2.0.0.0
 runSCT' :: (MonadConc n, NFData a)
-  => Way -> MemType -> ConcT n a -> n [(Either Condition a, Trace)]
+  => Way
+  -- ^ How to run the concurrent program.
+  -> MemType
+  -- ^ The memory model to use for non-synchronised @IORef@ operations.
+  -> Program pty n a
+  -- ^ The computation to run many times.
+  -> n [(Either Condition a, Trace)]
 runSCT' way = runSCTWithSettings' . fromWayAndMemType way
 
 -- | A strict variant of 'resultsSet'.
@@ -143,40 +99,17 @@
 -- Demanding the result of this will force it to normal form, which
 -- may be more efficient in some situations.
 --
--- @since 1.0.0.0
+-- @since 2.0.0.0
 resultsSet' :: (MonadConc n, Ord a, NFData a)
-  => Way -> MemType -> ConcT n a -> n (Set (Either Condition a))
+  => Way
+  -- ^ How to run the concurrent program.
+  -> MemType
+  -- ^ The memory model to use for non-synchronised @IORef@ operations.
+  -> Program pty n a
+  -- ^ The computation to run many times.
+  -> n (Set (Either Condition a))
 resultsSet' way = resultsSetWithSettings' . fromWayAndMemType way
 
--- | A strict variant of 'runSCTDiscard'.
---
--- Demanding the result of this will force it to normal form, which
--- may be more efficient in some situations.
---
--- The exact executions tried, and the order in which results are
--- found, is unspecified and may change between releases.
---
--- @since 1.0.0.0
-runSCTDiscard' :: (MonadConc n, NFData a)
-  => (Either Condition a -> Maybe Discard) -> Way -> MemType -> ConcT n a -> n [(Either Condition a, Trace)]
-runSCTDiscard' discard way memtype conc = do
-  res <- runSCTDiscard discard way memtype conc
-  rnf res `seq` pure res
-{-# DEPRECATED runSCTDiscard' "Use runSCTWithSettings' instead" #-}
-
--- | A strict variant of 'resultsSetDiscard'.
---
--- Demanding the result of this will force it to normal form, which
--- may be more efficient in some situations.
---
--- @since 1.0.0.0
-resultsSetDiscard' :: (MonadConc n, Ord a, NFData a)
-  => (Either Condition a -> Maybe Discard) -> Way -> MemType -> ConcT n a -> n (Set (Either Condition a))
-resultsSetDiscard' discard way memtype conc = do
-  res <- resultsSetDiscard discard way memtype conc
-  rnf res `seq` pure res
-{-# DEPRECATED resultsSetDiscard' "Use resultsSetWithSettings' instead" #-}
-
 -------------------------------------------------------------------------------
 -- Configuration
 
@@ -185,11 +118,11 @@
 -- The exact executions tried, and the order in which results are
 -- found, is unspecified and may change between releases.
 --
--- @since 1.2.0.0
+-- @since 2.0.0.0
 runSCTWithSettings :: MonadConc n
   => Settings n a
   -- ^ The SCT settings.
-  -> ConcT n a
+  -> Program pty n a
   -- ^ The computation to run many times.
   -> n [(Either Condition a, Trace)]
 runSCTWithSettings settings conc = case _way settings of
@@ -198,13 +131,13 @@
 
         check = findSchedulePrefix
 
-        step run dp (prefix, conservative, sleep) = do
+        step cstate0 run dp (prefix, conservative, sleep) = do
           (res, s, trace) <- run
-            (dporSched (_safeIO settings) (_memtype settings) (cBound cb0))
-            (initialDPORSchedState sleep prefix)
+            (dporSched (_safeIO settings) (cBound (_lengthBound settings) cb0))
+            (initialDPORSchedState sleep prefix cstate0)
 
-          let bpoints = findBacktrackSteps (_safeIO settings) (_memtype settings) (cBacktrack cb0) (schedBoundKill s) (schedBPoints s) trace
-          let newDPOR = incorporateTrace (_safeIO settings) (_memtype settings) conservative trace dp
+          let bpoints = findBacktrackSteps (_safeIO settings) (_memtype settings) (cBacktrack cb0) (schedBoundKill s) cstate0 (schedBPoints s) trace
+          let newDPOR = incorporateTrace (_safeIO settings) (_memtype settings) conservative trace cstate0 dp
 
           pure $ if schedIgnore s
                  then (force newDPOR, Nothing)
@@ -217,20 +150,20 @@
         check (_, 0) = Nothing
         check s = Just s
 
-        step run _ (g, n) = do
+        step _ run _ (g, n) = do
           (res, s, trace) <- run
             (randSched gen)
-            (initialRandSchedState g)
+            (initialRandSchedState (_lengthBound settings) g)
           pure ((schedGen s, n-1), Just (res, trace))
     in sct settings initial check step conc
 
 -- | A variant of 'resultsSet' which takes a 'Settings' record.
 --
--- @since 1.2.0.0
+-- @since 2.0.0.0
 resultsSetWithSettings :: (MonadConc n, Ord a)
   => Settings n a
   -- ^ The SCT settings.
-  -> ConcT n a
+  -> Program pty n a
   -- ^ The computation to run many times.
   -> n (Set (Either Condition a))
 resultsSetWithSettings settings conc =
@@ -245,10 +178,12 @@
 -- The exact executions tried, and the order in which results are
 -- found, is unspecified and may change between releases.
 --
--- @since 1.2.0.0
+-- @since 2.0.0.0
 runSCTWithSettings' :: (MonadConc n, NFData a)
   => Settings n a
-  -> ConcT n a
+  -- ^ The SCT settings.
+  -> Program pty n a
+  -- ^ The computation to run many times.
   -> n [(Either Condition a, Trace)]
 runSCTWithSettings' settings conc = do
   res <- runSCTWithSettings settings conc
@@ -259,10 +194,12 @@
 -- Demanding the result of this will force it to normal form, which
 -- may be more efficient in some situations.
 --
--- @since 1.2.0.0
+-- @since 2.0.0.0
 resultsSetWithSettings' :: (MonadConc n, Ord a, NFData a)
   => Settings n a
-  -> ConcT n a
+  -- ^ The SCT settings.
+  -> Program pty n a
+  -- ^ The computation to run many times.
   -> n (Set (Either Condition a))
 resultsSetWithSettings' settings conc = do
   res <- resultsSetWithSettings settings conc
@@ -272,24 +209,40 @@
 -- Combined Bounds
 
 -- | Combination bound function
-cBound :: Bounds -> IncrementalBoundFunc ((Int, Maybe ThreadId), M.Map ThreadId Int, Int)
-cBound (Bounds pb fb lb) (Just (k1, k2, k3)) prior lh =
+cBound :: Maybe LengthBound -> Bounds -> IncrementalBoundFunc ((Int, Maybe ThreadId), M.Map ThreadId Int, Int)
+cBound lb (Bounds pb fb) (Just (k1, k2, k3)) prior lh =
   let k1' = maybe (\k _ _ -> k) pBound pb (Just k1) prior lh
       k2' = maybe (\k _ _ -> k) fBound fb (Just k2) prior lh
       k3' = maybe (\k _ _ -> k) lBound lb (Just k3) prior lh
   in (,,) <$> k1' <*> k2' <*> k3'
-cBound _ Nothing _ _ = Just ((0, Nothing), M.empty, 1)
+cBound _ _ Nothing _ _ = Just ((0, Nothing), M.empty, 1)
 
--- | Combination backtracking function. Add all backtracking points
--- corresponding to enabled bound functions.
+-- | Backtracks to the given point.
 --
--- If no bounds are enabled, just backtrack to the given point.
+-- If pre-emption bounding is enabled, also conservatively adds a
+-- backtracking point 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.
 cBacktrack :: Bounds -> BacktrackFunc
-cBacktrack (Bounds (Just _) _ _) = pBacktrack
-cBacktrack (Bounds _ (Just _) _) = fBacktrack
-cBacktrack (Bounds _ _ (Just _)) = lBacktrack
-cBacktrack _ = backtrackAt (\_ _ -> False)
+cBacktrack (Bounds (Just _) _) bs =
+    backtrackAt (\_ _ -> False) bs . concatMap addConservative
+  where
+    addConservative o@(i, _, tid) = o : case conservative i of
+      Just j  -> [(j, True, tid)]
+      Nothing -> []
 
+    -- 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
+cBacktrack _ bs = backtrackAt (\_ _ -> False) bs
+
 -------------------------------------------------------------------------------
 -- Pre-emption bounding
 
@@ -300,26 +253,6 @@
   let k'@(pcount, _) = preEmpCountInc (fromMaybe (0, Nothing) k) prior lhead
   in if pcount <= pb then Just k' else Nothing
 
--- | 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
-pBacktrack bs = backtrackAt (\_ _ -> False) bs . concatMap addConservative where
-  addConservative o@(i, _, tid) = o : case conservative i of
-    Just j  -> [(j, True, tid)]
-    Nothing -> []
-
-  -- 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
 
@@ -331,13 +264,6 @@
      then Just k'
      else Nothing
 
--- | Add a backtrack point. If the thread doesn't exist or is blocked,
--- or performs a release operation, add all unblocked threads.
-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
 
@@ -346,147 +272,6 @@
 lBound (LengthBound lb) len _ _ =
   let len' = maybe 1 (+1) len
   in if len' < lb then Just len' else Nothing
-
--- | Add a backtrack point. If the thread doesn't exist or is blocked,
--- add all unblocked threads.
-lBacktrack :: BacktrackFunc
-lBacktrack = backtrackAt (\_ _ -> False)
-
--------------------------------------------------------------------------------
--- Systematic concurrency testing
-
--- | SCT via BPOR.
---
--- Schedules are generated by running the computation with a
--- 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.
---
--- The exact executions tried, and the order in which results are
--- found, is unspecified and may change between releases.
---
--- @since 1.0.0.0
-sctBound :: MonadConc n
-  => MemType
-  -- ^ The memory model to use for non-synchronised @IORef@ operations.
-  -> Bounds
-  -- ^ The combined bounds.
-  -> ConcT n a
-  -- ^ The computation to run many times
-  -> n [(Either Condition a, Trace)]
-sctBound = sctBoundDiscard (const Nothing)
-{-# DEPRECATED sctBound "Use runSCT instead" #-}
-
--- | A variant of 'sctBound' which can selectively discard results.
---
--- The exact executions tried, and the order in which results are
--- found, is unspecified and may change between releases.
---
--- @since 1.0.0.0
-sctBoundDiscard :: MonadConc n
-  => (Either Condition a -> Maybe Discard)
-  -- ^ Selectively discard results.
-  -> MemType
-  -- ^ The memory model to use for non-synchronised @IORef@ operations.
-  -> Bounds
-  -- ^ The combined bounds.
-  -> ConcT n a
-  -- ^ The computation to run many times
-  -> n [(Either Condition a, Trace)]
-sctBoundDiscard discard memtype cb = runSCTWithSettings $
-  set ldiscard (Just discard) (fromWayAndMemType (systematically cb) memtype)
-{-# DEPRECATED sctBoundDiscard "Use runSCTWithSettings instead" #-}
-
--- | SCT via uniform 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.
---
--- @since 1.0.0.0
-sctUniformRandom :: (MonadConc n, RandomGen g)
-  => MemType
-  -- ^ The memory model to use for non-synchronised @IORef@ operations.
-  -> g
-  -- ^ The random number generator.
-  -> Int
-  -- ^ The number of executions to perform.
-  -> ConcT n a
-  -- ^ The computation to run many times.
-  -> n [(Either Condition a, Trace)]
-sctUniformRandom = sctUniformRandomDiscard (const Nothing)
-{-# DEPRECATED sctUniformRandom "Use runSCT instead" #-}
-
--- | A variant of 'sctUniformRandom' which can selectively discard
--- results.
---
--- This is not guaranteed to find all distinct results.
---
--- @since 1.0.0.0
-sctUniformRandomDiscard :: (MonadConc n, RandomGen g)
-  => (Either Condition a -> Maybe Discard)
-  -- ^ Selectively discard results.
-  -> MemType
-  -- ^ The memory model to use for non-synchronised @IORef@ operations.
-  -> g
-  -- ^ The random number generator.
-  -> Int
-  -- ^ The number of executions to perform.
-  -> ConcT n a
-  -- ^ The computation to run many times.
-  -> n [(Either Condition a, Trace)]
-sctUniformRandomDiscard discard memtype g lim = runSCTWithSettings $
-  set ldiscard (Just discard) (fromWayAndMemType (uniformly g lim) memtype)
-{-# DEPRECATED sctUniformRandomDiscard "Use runSCTWithSettings instead" #-}
-
--- | SCT via weighted 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.
---
--- @since 1.7.0.0
-sctWeightedRandom :: (MonadConc n, RandomGen g)
-  => MemType
-  -- ^ The memory model to use for non-synchronised @IORef@ operations.
-  -> g
-  -- ^ The random number generator.
-  -> Int
-  -- ^ The number of executions to perform.
-  -> ConcT n a
-  -- ^ The computation to run many times.
-  -> n [(Either Condition a, Trace)]
-sctWeightedRandom = sctWeightedRandomDiscard (const Nothing)
-{-# DEPRECATED sctWeightedRandom "Use runSCT instead" #-}
-
--- | A variant of 'sctWeightedRandom' which can selectively discard
--- results.
---
--- This is not guaranteed to find all distinct results.
---
--- @since 1.7.0.0
-sctWeightedRandomDiscard :: (MonadConc n, RandomGen g)
-  => (Either Condition a -> Maybe Discard)
-  -- ^ Selectively discard results.
-  -> MemType
-  -- ^ The memory model to use for non-synchronised @IORef@ operations.
-  -> g
-  -- ^ The random number generator.
-  -> Int
-  -- ^ The number of executions to perform.
-  -> ConcT n a
-  -- ^ The computation to run many times.
-  -> n [(Either Condition a, Trace)]
-sctWeightedRandomDiscard discard memtype g lim = runSCTWithSettings $
-  set ldiscard (Just discard) (fromWayAndMemType (randomly g lim) memtype)
-{-# DEPRECATED sctWeightedRandomDiscard "Use runSCTWithSettings instead" #-}
 
 -------------------------------------------------------------------------------
 -- Utilities
diff --git a/Test/DejaFu/SCT/Internal.hs b/Test/DejaFu/SCT/Internal.hs
--- a/Test/DejaFu/SCT/Internal.hs
+++ b/Test/DejaFu/SCT/Internal.hs
@@ -15,18 +15,19 @@
 -- considered to form part of the public interface of this library.
 module Test.DejaFu.SCT.Internal where
 
-import           Control.Monad.Conc.Class         (MonadConc)
-import           Data.Coerce                      (Coercible, coerce)
-import qualified Data.IntMap.Strict               as I
-import           Data.List                        (find, mapAccumL)
-import           Data.Maybe                       (fromMaybe)
-import           GHC.Stack                        (HasCallStack)
+import           Control.Monad.Conc.Class          (MonadConc)
+import           Data.Coerce                       (Coercible, coerce)
+import qualified Data.IntMap.Strict                as I
+import           Data.List                         (find, mapAccumL)
+import           Data.Maybe                        (fromMaybe)
+import           GHC.Stack                         (HasCallStack)
 
 import           Test.DejaFu.Conc
-import           Test.DejaFu.Conc.Internal        (Context(..), DCSnapshot(..))
-import           Test.DejaFu.Conc.Internal.Memory (commitThreadId)
+import           Test.DejaFu.Conc.Internal         (Context(..))
+import           Test.DejaFu.Conc.Internal.Memory  (commitThreadId)
+import           Test.DejaFu.Conc.Internal.Program
 import           Test.DejaFu.Internal
-import           Test.DejaFu.Schedule             (Scheduler(..))
+import           Test.DejaFu.Schedule              (Scheduler(..))
 import           Test.DejaFu.SCT.Internal.DPOR
 import           Test.DejaFu.Types
 import           Test.DejaFu.Utils
@@ -42,47 +43,47 @@
   -- ^ Initial state
   -> (s -> Maybe t)
   -- ^ State predicate
-  -> ((Scheduler g -> g -> n (Either Condition a, g, Trace)) -> s -> t -> n (s, Maybe (Either Condition a, Trace)))
+  -> (ConcurrencyState -> (Scheduler g -> g -> n (Either Condition a, g, Trace)) -> s -> t -> n (s, Maybe (Either Condition a, Trace)))
   -- ^ Run the computation and update the state
-  -> ConcT n a
+  -> Program pty n a
   -> n [(Either Condition a, Trace)]
-sct settings s0 sfun srun conc
-    | canDCSnapshot conc = runForDCSnapshot conc >>= \case
-        Just (Right snap, _) -> sct'Snap snap
-        Just (Left f, trace) -> pure [(Left f, trace)]
-        _ -> do
-          debugFatal "Failed to construct snapshot, continuing without."
-          sct'Full
-    | otherwise = sct'Full
+sct settings s0 sfun srun conc = recordSnapshot conc >>= \case
+    Just (Right snap, _) -> sct'Snap snap
+    Just (Left f, trace) -> pure [(Left f, trace)]
+    Nothing -> sct'Full
   where
     sct'Full = sct'
       settings
+      initialCState
       (s0 [initialThread])
       sfun
-      (srun runFull)
+      (srun initialCState runFull)
       runFull
       (toId 1)
       (toId 1)
 
-    sct'Snap snap = let idsrc = cIdSource (dcsContext snap) in sct'
-      settings
-      (s0 (fst (threadsFromDCSnapshot snap)))
-      sfun
-      (srun (runSnap snap))
-      (runSnap snap)
-      (toId $ 1 + fst (_tids idsrc))
-      (toId $ 1 + fst (_iorids idsrc))
+    sct'Snap snap =
+      let idsrc = cIdSource (contextFromSnapshot snap)
+          cstate = cCState (contextFromSnapshot snap)
+      in sct'
+         settings
+         cstate
+         (s0 (fst (threadsFromSnapshot snap)))
+         sfun
+         (srun cstate (runSnap snap))
+         (runSnap snap)
+         (toId $ 1 + fst (_tids idsrc))
+         (toId $ 1 + fst (_iorids idsrc))
 
     runFull sched s = runConcurrent sched (_memtype settings) s conc
-    runSnap snap sched s = runWithDCSnapshot sched (_memtype settings) s snap
-
-    debugFatal = if _debugFatal settings then fatal else debugPrint
-    debugPrint = fromMaybe (const (pure ())) (_debugPrint settings)
+    runSnap snap sched s = runSnapshot sched (_memtype settings) s snap
 
 -- | Like 'sct' but given a function to run the computation.
 sct' :: (MonadConc n, HasCallStack)
   => Settings n a
   -- ^ The SCT settings ('Way' is ignored)
+  -> ConcurrencyState
+  -- ^ The initial concurrency state
   -> s
   -- ^ Initial state
   -> (s -> Maybe t)
@@ -96,7 +97,7 @@
   -> IORefId
   -- ^ The first available @IORefId@
   -> n [(Either Condition a, Trace)]
-sct' settings s0 sfun srun run nTId nCRId = go Nothing [] s0 where
+sct' settings cstate0 s0 sfun srun run nTId nCRId = go Nothing [] s0 where
   go (Just res) _ _ | earlyExit res = pure []
   go res0 seen !s = case sfun s of
     Just t -> srun s t >>= \case
@@ -128,7 +129,7 @@
   dosimplify res trace seen s
     | not (_simplify settings) = ((res, trace) :) <$> go (Just res) seen s
     | otherwise = do
-        shrunk <- simplifyExecution settings run nTId nCRId res trace
+        shrunk <- simplifyExecution settings cstate0 run nTId nCRId res trace
         (shrunk :) <$> go (Just res) seen s
 
   earlyExit = fromMaybe (const False) (_earlyExit settings)
@@ -152,6 +153,8 @@
 simplifyExecution :: (MonadConc n, HasCallStack)
   => Settings n a
   -- ^ The SCT settings ('Way' is ignored)
+  -> ConcurrencyState
+  -- ^ The initial concurrency state
   -> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
   -- ^ Just run the computation
   -> ThreadId
@@ -162,7 +165,7 @@
   -- ^ The expected result
   -> Trace
   -> n (Either Condition a, Trace)
-simplifyExecution settings run nTId nCRId res trace
+simplifyExecution settings cstate0 run nTId nCRId res trace
     | tidTrace == simplifiedTrace = do
         debugPrint ("Simplifying new result '" ++ p res ++ "': no simplification possible!")
         pure (res, trace)
@@ -178,7 +181,7 @@
             pure (res, trace)
   where
     tidTrace = toTIdTrace trace
-    simplifiedTrace = simplify (_safeIO settings) (_memtype settings) tidTrace
+    simplifiedTrace = simplify (_safeIO settings) (_memtype settings) cstate0 tidTrace
     fixup = renumber (_memtype settings) (fromId nTId) (fromId nCRId)
 
     debugFatal = if _debugFatal settings then fatal else debugPrint
@@ -194,11 +197,11 @@
   -- ^ The reduced sequence of scheduling decisions
   -> n (Either Condition a, [(ThreadId, ThreadAction)], Trace)
 replay run = run (Scheduler (const sched)) where
-    sched runnable ((t, Stop):ts) = case findThread t runnable of
+    sched runnable cs ((t, Stop):ts) = case findThread t runnable of
       Just t' -> (Just t', ts)
-      Nothing -> sched runnable ts
-    sched runnable ((t, _):ts) = (findThread t runnable, ts)
-    sched _ _ = (Nothing, [])
+      Nothing -> sched runnable cs ts
+    sched runnable _ ((t, _):ts) = (findThread t runnable, ts)
+    sched _ _ _ = (Nothing, [])
 
     -- find a thread ignoring names
     findThread tid0 =
@@ -209,10 +212,15 @@
 
 -- | Simplify a trace by permuting adjacent independent actions to
 -- reduce context switching.
-simplify :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
-simplify safeIO memtype trc0 = loop (length trc0) (prepare trc0) where
-  prepare = dropCommits safeIO memtype . lexicoNormalForm safeIO memtype
-  step = pushForward safeIO memtype . pullBack safeIO memtype
+simplify
+  :: Bool
+  -> MemType
+  -> ConcurrencyState
+  -> [(ThreadId, ThreadAction)]
+  -> [(ThreadId, ThreadAction)]
+simplify safeIO memtype cstate0 trc0 = loop (length trc0) (prepare trc0) where
+  prepare = dropCommits safeIO memtype cstate0 . lexicoNormalForm safeIO memtype cstate0
+  step = pushForward safeIO memtype cstate0 . pullBack safeIO memtype cstate0
 
   loop 0 trc = trc
   loop n trc =
@@ -220,10 +228,15 @@
     in if trc' /= trc then loop (n-1) trc' else trc
 
 -- | Put a trace into lexicographic (by thread ID) normal form.
-lexicoNormalForm :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
-lexicoNormalForm safeIO memtype = go where
+lexicoNormalForm
+  :: Bool
+  -> MemType
+  -> ConcurrencyState
+  -> [(ThreadId, ThreadAction)]
+  -> [(ThreadId, ThreadAction)]
+lexicoNormalForm safeIO memtype cstate0 = go where
   go trc =
-    let trc' = permuteBy safeIO memtype (repeat (>)) trc
+    let trc' = permuteBy safeIO memtype cstate0 (repeat (>)) trc
     in if trc == trc' then trc else go trc'
 
 -- | Swap adjacent independent actions in the trace if a predicate
@@ -231,25 +244,31 @@
 permuteBy
   :: Bool
   -> MemType
+  -> ConcurrencyState
   -> [ThreadId -> ThreadId -> Bool]
   -> [(ThreadId, ThreadAction)]
   -> [(ThreadId, ThreadAction)]
-permuteBy safeIO memtype = go initialDepState where
+permuteBy safeIO memtype = go where
   go ds (p:ps) (t1@(tid1, ta1):t2@(tid2, ta2):trc)
     | independent safeIO ds tid1 ta1 tid2 ta2 && p tid1 tid2 = go' ds ps t2 (t1 : trc)
     | otherwise = go' ds ps t1 (t2 : trc)
   go _ _ trc = trc
 
-  go' ds ps t@(tid, ta) trc = t : go (updateDepState memtype ds tid ta) ps trc
+  go' ds ps t@(tid, ta) trc = t : go (updateCState memtype ds tid ta) ps trc
 
 -- | Throw away commit actions which are followed by a memory barrier.
-dropCommits :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
-dropCommits _ SequentialConsistency = id
-dropCommits safeIO memtype = go initialDepState where
+dropCommits
+  :: Bool
+  -> MemType
+  -> ConcurrencyState
+  -> [(ThreadId, ThreadAction)]
+  -> [(ThreadId, ThreadAction)]
+dropCommits _ SequentialConsistency = const id
+dropCommits safeIO memtype = go where
   go ds (t1@(tid1, ta1@(CommitIORef _ iorefid)):t2@(tid2, ta2):trc)
     | isBarrier (simplifyAction ta2) && numBuffered ds iorefid == 1 = go ds (t2:trc)
-    | independent safeIO ds tid1 ta1 tid2 ta2 = t2 : go (updateDepState memtype ds tid2 ta2) (t1:trc)
-  go ds (t@(tid,ta):trc) = t : go (updateDepState memtype ds tid ta) trc
+    | independent safeIO ds tid1 ta1 tid2 ta2 = t2 : go (updateCState memtype ds tid2 ta2) (t1:trc)
+  go ds (t@(tid,ta):trc) = t : go (updateCState memtype ds tid ta) trc
   go _ [] = []
 
 -- | Attempt to reduce context switches by \"pulling\" thread actions
@@ -259,10 +278,15 @@
 -- act3)]@, where @act2@ and @act3@ are independent.  In this case
 -- 'pullBack' will swap them, giving the sequence @[(tidA, act1),
 -- (tidA, act3), (tidB, act2)]@.  It works for arbitrary separations.
-pullBack :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
-pullBack safeIO memtype = go initialDepState where
+pullBack
+  :: Bool
+  -> MemType
+  -> ConcurrencyState
+  -> [(ThreadId, ThreadAction)]
+  -> [(ThreadId, ThreadAction)]
+pullBack safeIO memtype = go where
   go ds (t1@(tid1, ta1):trc@((tid2, _):_)) =
-    let ds' = updateDepState memtype ds tid1 ta1
+    let ds' = updateCState memtype ds tid1 ta1
         trc' = if tid1 /= tid2
                then maybe trc (uncurry (:)) (findAction tid1 ds' trc)
                else trc
@@ -272,7 +296,7 @@
   findAction tid0 = fgo where
     fgo ds (t@(tid, ta):trc)
       | tid == tid0 = Just (t, trc)
-      | otherwise = case fgo (updateDepState memtype ds tid ta) trc of
+      | otherwise = case fgo (updateCState memtype ds tid ta) trc of
           Just (ft@(ftid, fa), trc')
             | independent safeIO ds tid ta ftid fa -> Just (ft, t:trc')
           _ -> Nothing
@@ -288,10 +312,15 @@
 -- act3)]@, where @act1@ and @act2@ are independent.  In this case
 -- 'pushForward' will swap them, giving the sequence @[(tidB, act2),
 -- (tidA, act1), (tidA, act3)]@.  It works for arbitrary separations.
-pushForward :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
-pushForward safeIO memtype = go initialDepState where
+pushForward
+  :: Bool
+  -> MemType
+  -> ConcurrencyState
+  -> [(ThreadId, ThreadAction)]
+  -> [(ThreadId, ThreadAction)]
+pushForward safeIO memtype = go where
   go ds (t1@(tid1, ta1):trc@((tid2, _):_)) =
-    let ds' = updateDepState memtype ds tid1 ta1
+    let ds' = updateCState memtype ds tid1 ta1
     in if tid1 /= tid2
        then maybe (t1 : go ds' trc) (go ds) (findAction tid1 ta1 ds trc)
        else t1 : go ds' trc
@@ -300,7 +329,7 @@
   findAction tid0 ta0 = fgo where
     fgo ds (t@(tid, ta):trc)
       | tid == tid0 = Just ((tid0, ta0) : t : trc)
-      | independent safeIO ds tid0 ta0 tid ta = (t:) <$> fgo (updateDepState memtype ds tid ta) trc
+      | independent safeIO ds tid0 ta0 tid ta = (t:) <$> fgo (updateCState memtype ds tid ta) trc
       | otherwise = Nothing
     fgo _ _ = Nothing
 
diff --git a/Test/DejaFu/SCT/Internal/DPOR.hs b/Test/DejaFu/SCT/Internal/DPOR.hs
--- a/Test/DejaFu/SCT/Internal/DPOR.hs
+++ b/Test/DejaFu/SCT/Internal/DPOR.hs
@@ -1,7 +1,6 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE ViewPatterns #-}
 
 -- |
@@ -10,7 +9,7 @@
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
--- Portability : DeriveAnyClass, DeriveGeneric, FlexibleContexts, LambdaCase, ViewPatterns
+-- Portability : DeriveAnyClass, DeriveGeneric, FlexibleContexts, ViewPatterns
 --
 -- Internal types and functions for SCT via dynamic partial-order
 -- reduction.  This module is NOT considered to form part of the
@@ -18,8 +17,7 @@
 module Test.DejaFu.SCT.Internal.DPOR where
 
 import           Control.Applicative  ((<|>))
-import           Control.DeepSeq      (NFData(..))
-import           Control.Exception    (MaskingState(..))
+import           Control.DeepSeq      (NFData)
 import qualified Data.Foldable        as F
 import           Data.Function        (on)
 import           Data.List            (nubBy, partition, sortOn)
@@ -104,7 +102,7 @@
   , bcktBacktracks :: Map ThreadId Bool
   -- ^ The list of alternative threads to run, and whether those
   -- alternatives were added conservatively due to the bound.
-  , bcktState      :: DepState
+  , bcktState      :: ConcurrencyState
   -- ^ Some domain-specific state at this point.
   } deriving (Eq, Show, Generic, NFData)
 
@@ -164,12 +162,14 @@
   -> Trace
   -- ^ The execution trace: the decision made, the runnable threads,
   -- and the action performed.
+  -> ConcurrencyState
+  -- ^ The initial concurrency state
   -> DPOR
   -> DPOR
-incorporateTrace safeIO memtype conservative trace dpor0 = grow initialDepState (initialDPORThread dpor0) trace dpor0 where
+incorporateTrace safeIO memtype conservative trace state0 dpor0 = grow state0 (initialDPORThread dpor0) trace dpor0 where
   grow state tid trc@((d, _, a):rest) dpor =
     let tid'   = tidOf tid d
-        state' = updateDepState memtype state tid' a
+        state' = updateCState memtype state tid' a
     in case dporNext dpor of
          Just (t, child)
            | t == tid' ->
@@ -190,7 +190,7 @@
 
   -- Construct a new subtree corresponding to a trace suffix.
   subtree state tid sleep ((_, _, a):rest) = validateDPOR $
-    let state' = updateDepState memtype state tid a
+    let state' = updateCState memtype state tid a
         sleep' = M.filterWithKey (\t a' -> not $ dependent safeIO state' tid a t a') sleep
     in DPOR
         { dporRunnable = S.fromList $ case rest of
@@ -235,6 +235,8 @@
   -> Bool
   -- ^ Whether the computation was aborted due to no decisions being
   -- in-bounds.
+  -> ConcurrencyState
+  -- ^ The initial concurrency state.
   -> Seq ([(ThreadId, Lookahead)], [ThreadId])
   -- ^ A sequence of threads at each step: the list of runnable
   -- in-bound threads (with lookahead values), and the list of threads
@@ -244,12 +246,12 @@
   -> Trace
   -- ^ The execution trace.
   -> [BacktrackStep]
-findBacktrackSteps safeIO memtype backtrack boundKill = go initialDepState S.empty initialThread [] . F.toList where
+findBacktrackSteps safeIO memtype backtrack boundKill state0 = go state0 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 memtype state tid' a
+        state' = updateCState memtype state tid' a
         this = BacktrackStep
           { bcktThreadid   = tid'
           , bcktDecision   = d
@@ -275,23 +277,15 @@
                  , u /= v
                  , i <- maybeToList (findIndex u n v tagged)]
 
-        findIndex u n v = go' True where
+        findIndex u n v = go' where
           {-# INLINE go' #-}
-          go' final ((i,b):rest)
-            -- Don't cross subconcurrency boundaries
-            | isSubC final b = Nothing
+          go' ((i,b):rest)
             -- 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
-            | otherwise = go' False rest
-          go' _ [] = Nothing
-
-          {-# INLINE isSubC #-}
-          isSubC final b = case bcktAction b of
-            Stop -> not final && bcktThreadid b == initialThread
-            Subconcurrency -> bcktThreadid b == initialThread
-            _ -> False
+            | otherwise = go' rest
+          go' [] = Nothing
 
           {-# INLINE isDependent #-}
           isDependent b
@@ -352,7 +346,7 @@
   , schedBoundKill :: Bool
   -- ^ Whether the execution was terminated due to all decisions being
   -- out of bounds.
-  , schedDepState  :: DepState
+  , schedCState    :: ConcurrencyState
   -- ^ State used by the dependency function to determine when to
   -- remove decisions from the sleep set.
   , schedBState    :: Maybe k
@@ -364,14 +358,16 @@
   -- ^ The initial sleep set.
   -> [ThreadId]
   -- ^ The schedule prefix.
+  -> ConcurrencyState
+  -- ^ The initial concurrency state.
   -> DPORSchedState k
-initialDPORSchedState sleep prefix = DPORSchedState
+initialDPORSchedState sleep prefix state0 = DPORSchedState
   { schedSleep     = sleep
   , schedPrefix    = prefix
   , schedBPoints   = Sq.empty
   , schedIgnore    = False
   , schedBoundKill = False
-  , schedDepState  = initialDepState
+  , schedCState    = state0
   , schedBState    = Nothing
   }
 
@@ -450,19 +446,22 @@
 dporSched :: HasCallStack
   => Bool
   -- ^ True if all IO is thread safe.
-  -> MemType
   -> IncrementalBoundFunc k
   -- ^ Bound function: returns true if that schedule prefix terminated
   -- with the lookahead decision fits within the bound.
   -> Scheduler (DPORSchedState k)
-dporSched safeIO memtype boundf = Scheduler $ \prior threads s ->
+dporSched safeIO boundf = Scheduler $ \prior threads cstate s ->
   let
     -- The next scheduler state
     nextState rest = s
       { schedBPoints  = schedBPoints s |> (restrictToBound fst threads', rest)
-      , schedDepState = nextDepState
+      -- we only update this after using the current value; so in
+      -- effect this field is the depstate *before* the action which
+      -- just happened, we need this because we need to know if the
+      -- prior action (in the state we did it from) is dependent with
+      -- anything in the sleep set.
+      , schedCState = cstate
       }
-    nextDepState = let ds = schedDepState s in maybe ds (uncurry $ updateDepState memtype ds) prior
 
     -- Pick a new thread to run, not considering bounds. Choose the
     -- current thread if available and it hasn't just yielded,
@@ -530,7 +529,7 @@
     [] ->
       let choices  = restrictToBound id initialise
           checkDep t a = case prior of
-            Just (tid, act) -> dependent safeIO (schedDepState s) tid act t a
+            Just (tid, act) -> dependent safeIO (schedCState 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
@@ -550,18 +549,13 @@
 --
 -- This implements a stronger check that @not (dependent ...)@, as it
 -- handles some cases which 'dependent' doesn't need to care about.
---
--- This should not be used to re-order traces which contain
--- subconcurrency.
-independent :: Bool -> DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool
+independent :: Bool -> ConcurrencyState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool
 independent safeIO ds t1 a1 t2 a2
     | t1 == t2 = False
     | check t1 a1 t2 a2 = False
     | check t2 a2 t1 a1 = False
     | otherwise = not (dependent safeIO ds t1 a1 t2 a2)
   where
-    -- @dontCheck@ must be the first thing in the computation.
-    check _ (DontCheck _) _ _ = True
     -- can't re-order any action of a thread with the fork which
     -- created it.
     check _ (Fork t) tid _ | t == tid = True
@@ -582,7 +576,7 @@
 -- This is basically the same as 'dependent'', but can make use of the
 -- additional information in a 'ThreadAction' to make better decisions
 -- in a few cases.
-dependent :: Bool -> DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool
+dependent :: Bool -> ConcurrencyState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool
 dependent safeIO ds t1 a1 t2 a2 = case (a1, a2) of
   -- When masked interruptible, a thread can only be interrupted when
   -- actually blocked. 'dependent'' has to assume that all
@@ -614,7 +608,7 @@
 --
 -- Termination of the initial thread is handled specially in the DPOR
 -- implementation.
-dependent' :: Bool -> DepState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool
+dependent' :: Bool -> ConcurrencyState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool
 dependent' safeIO ds t1 a1 t2 l2 = case (a1, l2) of
   -- Worst-case assumption: all IO is dependent.
   (LiftIO, WillLiftIO) -> not safeIO
@@ -643,7 +637,7 @@
 -- | Check if two 'ActionType's are dependent. Note that this is not
 -- sufficient to know if two 'ThreadAction's are dependent, without
 -- being so great an over-approximation as to be useless!
-dependentActions :: DepState -> ActionType -> ActionType -> Bool
+dependentActions :: ConcurrencyState -> ActionType -> ActionType -> Bool
 dependentActions ds a1 a2 = case (a1, a2) of
   (UnsynchronisedRead _, UnsynchronisedRead _) -> False
 
@@ -676,131 +670,6 @@
   (SynchronisedRead  v1, SynchronisedWrite v2) | v1 == v2 -> True
 
   (_, _) -> maybe False (\r -> Just r == iorefOf a2) (iorefOf a1)
-
--------------------------------------------------------------------------------
--- ** Dependency function state
-
-data DepState = DepState
-  { depIOState :: Map IORefId Int
-  -- ^ Keep track of which @IORef@s have buffered writes.
-  , depMVState :: Set MVarId
-  -- ^ Keep track of which @MVar@s are full.
-  , 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)
-
-instance NFData DepState where
-  rnf depstate = rnf ( depIOState depstate
-                     , depMVState depstate
-                     , [(t, m `seq` ()) | (t, m) <- M.toList (depMaskState depstate)]
-                     )
-
--- | Initial dependency state.
-initialDepState :: DepState
-initialDepState = DepState M.empty S.empty M.empty
-
--- | Update the dependency state with the action that has just
--- happened.
-updateDepState :: MemType -> DepState -> ThreadId -> ThreadAction -> DepState
-updateDepState memtype depstate tid act = DepState
-  { depIOState   = updateIOState memtype act $ depIOState   depstate
-  , depMVState   = updateMVState         act $ depMVState   depstate
-  , depMaskState = updateMaskState tid   act $ depMaskState depstate
-  }
-
--- | Update the @IORef@ buffer state with the action that has just
--- happened.
-updateIOState :: MemType -> ThreadAction -> Map IORefId Int -> Map IORefId Int
-updateIOState SequentialConsistency _ = const M.empty
-updateIOState _ (CommitIORef _ r) = (`M.alter` r) $ \case
-  Just 1  -> Nothing
-  Just n  -> Just (n-1)
-  Nothing -> Nothing
-updateIOState _ (WriteIORef    r) = M.insertWith (+) r 1
-updateIOState _ ta
-  | isBarrier $ simplifyAction ta = const M.empty
-  | otherwise = id
-
--- | Update the @MVar@ full/empty state with the action that has just
--- happened.
-updateMVState :: ThreadAction -> Set MVarId -> Set MVarId
-updateMVState (PutMVar mvid _) = S.insert mvid
-updateMVState (TryPutMVar mvid True _) = S.insert mvid
-updateMVState (TakeMVar mvid _) = S.delete mvid
-updateMVState (TryTakeMVar mvid True _) = S.delete mvid
-updateMVState _ = 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 tid (Throw True) = M.delete tid
-updateMaskState _ (ThrowTo tid True) = M.delete tid
-updateMaskState tid Stop = M.delete tid
-updateMaskState _ _ = id
-
--- | Check if a @IORef@ has a buffered write pending.
-isBuffered :: DepState -> IORefId -> Bool
-isBuffered depstate r = numBuffered depstate r /= 0
-
--- | Check how many buffered writes an @IORef@ has.
-numBuffered :: DepState -> IORefId -> Int
-numBuffered depstate r = M.findWithDefault 0 r (depIOState depstate)
-
--- | Check if an @MVar@ is full.
-isFull :: DepState -> MVarId -> Bool
-isFull depstate v = S.member v (depMVState 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
diff --git a/Test/DejaFu/SCT/Internal/Weighted.hs b/Test/DejaFu/SCT/Internal/Weighted.hs
--- a/Test/DejaFu/SCT/Internal/Weighted.hs
+++ b/Test/DejaFu/SCT/Internal/Weighted.hs
@@ -3,11 +3,11 @@
 
 -- |
 -- Module      : Test.DejaFu.SCT.Internal.Weighted
--- Copyright   : (c) 2015--2018 Michael Walker
+-- Copyright   : (c) 2015--2019 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
--- Portability : portable
+-- Portability : DeriveAnyClass, DeriveGeneric
 --
 -- Internal types and functions for SCT via weighted random
 -- scheduling.  This module is NOT considered to form part of the
@@ -31,19 +31,21 @@
 data RandSchedState g = RandSchedState
   { schedWeights :: Map ThreadId Int
   -- ^ The thread weights: used in determining which to run.
-  , schedGen     :: g
+  , schedLengthBound :: Maybe LengthBound
+  -- ^ The optional length bound.
+  , schedGen :: g
   -- ^ The random number generator.
   } deriving (Eq, Show, Generic, NFData)
 
 -- | Initial weighted random scheduler state.
-initialRandSchedState :: g -> RandSchedState g
+initialRandSchedState :: Maybe LengthBound -> 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 => (g -> (Int, g)) -> Scheduler (RandSchedState g)
-randSched weightf = Scheduler $ \_ threads s ->
+randSched weightf = Scheduler $ \_ threads _ s ->
   let
     -- Select a thread
     pick idx ((x, f):xs)
@@ -61,4 +63,7 @@
 
     -- The runnable threads.
     tids = map fst (toList threads)
-  in (pick choice enabled, RandSchedState weights' g'')
+  in case schedLengthBound s of
+    Just 0 -> (Nothing, s)
+    Just n -> (pick choice enabled, RandSchedState weights' (Just (n - 1)) g'')
+    Nothing -> (pick choice enabled, RandSchedState weights' Nothing g'')
diff --git a/Test/DejaFu/Schedule.hs b/Test/DejaFu/Schedule.hs
--- a/Test/DejaFu/Schedule.hs
+++ b/Test/DejaFu/Schedule.hs
@@ -37,16 +37,19 @@
 --
 -- 2. The unblocked threads.
 --
--- 3. The state.
+-- 3. The concurrency state.
 --
+-- 4. The scheduler state.
+--
 -- It returns a thread to execute, or @Nothing@ if execution should
 -- abort here, and also a new state.
 --
--- @since 0.8.0.0
+-- @since 2.0.0.0
 newtype Scheduler state = Scheduler
   { scheduleThread
     :: Maybe (ThreadId, ThreadAction)
     -> NonEmpty (ThreadId, Lookahead)
+    -> ConcurrencyState
     -> state
     -> (Maybe ThreadId, state)
   }
@@ -60,7 +63,7 @@
 -- @since 0.8.0.0
 randomSched :: RandomGen g => Scheduler g
 randomSched = Scheduler go where
-  go _ threads g =
+  go _ threads _ g =
     let threads' = map fst (toList threads)
         (choice, g') = randomR (0, length threads' - 1) g
     in (Just $ eidx threads' choice, g')
@@ -71,8 +74,8 @@
 -- @since 0.8.0.0
 roundRobinSched :: Scheduler ()
 roundRobinSched = Scheduler go where
-  go Nothing ((tid,_):|_) _ = (Just tid, ())
-  go (Just (prior, _)) threads _ =
+  go Nothing ((tid,_):|_) _ _ = (Just tid, ())
+  go (Just (prior, _)) threads _ _ =
     let threads' = map fst (toList threads)
         candidates =
           if prior >= maximum threads'
@@ -109,7 +112,7 @@
 -- @since 0.8.0.0
 makeNonPreemptive :: Scheduler s -> Scheduler s
 makeNonPreemptive sched = Scheduler newsched where
-  newsched p@(Just (prior, _)) threads s
+  newsched p@(Just (prior, _)) threads cs s
     | prior `elem` map fst (toList threads) = (Just prior, s)
-    | otherwise = scheduleThread sched p threads s
-  newsched Nothing threads s = scheduleThread sched Nothing threads s
+    | otherwise = scheduleThread sched p threads cs s
+  newsched Nothing threads cs s = scheduleThread sched Nothing threads cs s
diff --git a/Test/DejaFu/Settings.hs b/Test/DejaFu/Settings.hs
--- a/Test/DejaFu/Settings.hs
+++ b/Test/DejaFu/Settings.hs
@@ -23,7 +23,7 @@
   , randomly
   , uniformly
 
-  -- *** Schedule bounds
+  -- *** Schedule bounding
 
   -- | Schedule bounding is used by the 'systematically' approach to
   -- limit the search-space, which in general will be huge.
@@ -50,13 +50,23 @@
   , Bounds(..)
   , PreemptionBound(..)
   , FairBound(..)
-  , LengthBound(..)
   , defaultBounds
   , defaultPreemptionBound
   , defaultFairBound
-  , defaultLengthBound
   , noBounds
 
+  -- *** Length bounding
+
+  -- | Length bounding can be used to test potentially nonterminating
+  -- computations.  Any execution exceeding the length bound gets
+  -- discarded.
+  --
+  -- While 'PreemptionBound' and 'FairBound' are only used by
+  -- 'systematically', all 'Way's use the length bound.
+
+  , LengthBound(..)
+  , llengthBound
+
   -- ** The @MemType@
 
   -- | When executed on a multi-core processor some @IORef@ / @IORef@
@@ -258,6 +268,7 @@
 fromWayAndMemType :: Applicative n => Way -> MemType -> Settings n a
 fromWayAndMemType way memtype = Settings
   { _way = way
+  , _lengthBound = Nothing
   , _memtype = memtype
   , _discard = Nothing
   , _debugShow = Nothing
@@ -332,7 +343,7 @@
 uniformly = Randomly $ \g -> (1, g)
 
 -------------------------------------------------------------------------------
--- Schedule bounds
+-- Schedule bounding
 
 -- | All bounds enabled, using their default values.
 --
@@ -344,7 +355,6 @@
 defaultBounds = Bounds
   { boundPreemp = Just defaultPreemptionBound
   , boundFair   = Just defaultFairBound
-  , boundLength = Nothing
   }
 
 -- | A sensible default preemption bound: 2.
@@ -365,14 +375,6 @@
 defaultFairBound :: FairBound
 defaultFairBound = 5
 
--- | There is no default length bound.
---
--- This is only suitable if your computation will always terminate!
---
--- @since 1.8.0.0
-defaultLengthBound :: LengthBound
-defaultLengthBound = 250
-
 -- | 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 terminates!
@@ -382,8 +384,16 @@
 noBounds = Bounds
   { boundPreemp = Nothing
   , boundFair   = Nothing
-  , boundLength = Nothing
   }
+
+-------------------------------------------------------------------------------
+-- Length bounding
+
+-- | A lens into the length bound.
+--
+-- @since 2.0.0.0
+llengthBound :: Lens' (Settings n a) (Maybe LengthBound)
+llengthBound afb s = (\b -> s {_lengthBound = b}) <$> afb (_lengthBound s)
 
 -------------------------------------------------------------------------------
 -- The @MemType@
diff --git a/Test/DejaFu/Types.hs b/Test/DejaFu/Types.hs
--- a/Test/DejaFu/Types.hs
+++ b/Test/DejaFu/Types.hs
@@ -5,7 +5,7 @@
 
 -- |
 -- Module      : Test.DejaFu.Types
--- Copyright   : (c) 2017--2018 Michael Walker
+-- Copyright   : (c) 2017--2019 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
@@ -21,7 +21,11 @@
 import           Data.Function                        (on)
 import           Data.Functor.Contravariant           (Contravariant(..))
 import           Data.Functor.Contravariant.Divisible (Divisible(..))
+import           Data.Map.Strict                      (Map)
+import qualified Data.Map.Strict                      as M
 import           Data.Semigroup                       (Semigroup(..))
+import           Data.Set                             (Set)
+import qualified Data.Set                             as S
 import           GHC.Generics                         (Generic)
 
 -------------------------------------------------------------------------------
@@ -106,7 +110,7 @@
 
 -- | All the actions that a thread can perform.
 --
--- @since 1.11.0.0
+-- @since 2.0.0.0
 data ThreadAction =
     Fork ThreadId
   -- ^ Start a new thread.
@@ -194,12 +198,8 @@
   -- ^ A 'return' or 'pure' action was executed.
   | Stop
   -- ^ Cease execution and terminate.
-  | Subconcurrency
-  -- ^ Start executing an action with @subconcurrency@.
-  | StopSubconcurrency
-  -- ^ Stop executing an action with @subconcurrency@.
-  | DontCheck Trace
-  -- ^ Execute an action with @dontCheck@.
+  | RegisterInvariant
+  -- ^ Register an invariant.
   deriving (Eq, Generic, Show)
 
 -- this makes me sad
@@ -242,13 +242,11 @@
   rnf LiftIO = ()
   rnf Return = ()
   rnf Stop = ()
-  rnf Subconcurrency = ()
-  rnf StopSubconcurrency = ()
-  rnf (DontCheck as) = rnf as
+  rnf RegisterInvariant = ()
 
 -- | A one-step look-ahead at what a thread will do next.
 --
--- @since 1.11.0.0
+-- @since 2.0.0.0
 data Lookahead =
     WillFork
   -- ^ Will start a new thread.
@@ -325,12 +323,8 @@
   -- ^ Will execute a 'return' or 'pure' action.
   | WillStop
   -- ^ Will cease execution and terminate.
-  | WillSubconcurrency
-  -- ^ Will execute an action with @subconcurrency@.
-  | WillStopSubconcurrency
-  -- ^ Will stop executing an extion with @subconcurrency@.
-  | WillDontCheck
-  -- ^ Will execute an action with @dontCheck@.
+  | WillRegisterInvariant
+  -- ^ Will register an invariant
   deriving (Eq, Generic, Show)
 
 -- this also makes me sad
@@ -368,9 +362,7 @@
   rnf WillLiftIO = ()
   rnf WillReturn = ()
   rnf WillStop = ()
-  rnf WillSubconcurrency = ()
-  rnf WillStopSubconcurrency = ()
-  rnf WillDontCheck = ()
+  rnf WillRegisterInvariant = ()
 
 -- | All the actions that an STM transaction can perform.
 --
@@ -438,19 +430,14 @@
 -------------------------------------------------------------------------------
 -- * Conditions
 
--- | A type synonym for 'Condition', use that instead.
---
--- @since 1.12.0.0
-{-# DEPRECATED Failure "The 'Failure' type has been split up into 'Condition' and 'Error', with different semantics." #-}
-type Failure = Condition
-
 -- | An indication of how a concurrent computation terminated, if it
 -- didn't produce a value.
 --
 -- The @Eq@, @Ord@, and @NFData@ instances compare/evaluate the
--- exception with @show@ in the @UncaughtException@ case.
+-- exception with @show@ in the @UncaughtException@ and
+-- @InvariantFailure@ cases.
 --
--- @since 1.12.0.0
+-- @since 2.0.0.0
 data Condition
   = Abort
   -- ^ The scheduler chose to abort execution. This will be produced
@@ -458,20 +445,18 @@
   -- bounds (there have been too many pre-emptions, the computation
   -- has executed for too long, or there have been too many yields).
   | Deadlock
-  -- ^ Every thread is blocked, and the main thread is /not/ blocked
-  -- in an STM transaction.
-  | STMDeadlock
-  -- ^ Every thread is blocked, and the main thread is blocked in an
-  -- STM transaction.
+  -- ^ Every thread is blocked
   | UncaughtException SomeException
   -- ^ An uncaught exception bubbled to the top of the computation.
+  | InvariantFailure SomeException
+  -- ^ An uncaught exception caused an invariant to fail.
   deriving (Show, Generic)
 
 instance Eq Condition where
   Abort                  == Abort                  = True
   Deadlock               == Deadlock               = True
-  STMDeadlock            == STMDeadlock            = True
   (UncaughtException e1) == (UncaughtException e2) = show e1 == show e2
+  (InvariantFailure  e1) == (InvariantFailure  e2) = show e1 == show e2
   _ == _ = False
 
 instance Ord Condition where
@@ -479,11 +464,12 @@
     transform :: Condition -> (Int, Maybe String)
     transform Abort = (1, Nothing)
     transform Deadlock = (2, Nothing)
-    transform STMDeadlock = (3, Nothing)
-    transform (UncaughtException e) = (4, Just (show e))
+    transform (UncaughtException e) = (3, Just (show e))
+    transform (InvariantFailure  e) = (4, Just (show e))
 
 instance NFData Condition where
   rnf (UncaughtException e) = rnf (show e)
+  rnf (InvariantFailure  e) = rnf (show e)
   rnf f = f `seq` ()
 
 -- | Check if a condition is an @Abort@.
@@ -493,12 +479,11 @@
 isAbort Abort = True
 isAbort _ = False
 
--- | Check if a condition is a @Deadlock@ or an @STMDeadlock@.
+-- | Check if a condition is a @Deadlock@.
 --
 -- @since 0.9.0.0
 isDeadlock :: Condition -> Bool
 isDeadlock Deadlock = True
-isDeadlock STMDeadlock = True
 isDeadlock _ = False
 
 -- | Check if a condition is an @UncaughtException@
@@ -508,13 +493,20 @@
 isUncaughtException (UncaughtException _) = True
 isUncaughtException _ = False
 
+-- | Check if a condition is an @InvariantFailure@
+--
+-- @since 2.0.0.0
+isInvariantFailure :: Condition -> Bool
+isInvariantFailure (InvariantFailure _) = True
+isInvariantFailure _ = False
+
 -------------------------------------------------------------------------------
 -- * Errors
 
 -- | An indication that there is a bug in dejafu or you are using it
 -- incorrectly.
 --
--- @since 1.12.0.0
+-- @since 2.0.0.0
 data Error
   = ScheduledBlockedThread
   -- ^ Raised as an exception if the scheduler attempts to schedule a
@@ -522,14 +514,6 @@
   | ScheduledMissingThread
   -- ^ Raised as an exception if the scheduler attempts to schedule a
   -- nonexistent thread.
-  | NestedSubconcurrency
-  -- ^ Raised as an exception if a @subconcurrency@ is nested inside
-  -- another @subconcurrency@ or a @dontCheck@.
-  | MultithreadedSubconcurrency
-  -- ^ Raised as an exception if @subconcurrency@ is called after
-  -- forking threads.
-  | LateDontCheck
-  -- ^ Raised as an exception if @dontCheck@ is called after the first action.
   deriving (Show, Eq, Ord, Bounded, Enum, Generic)
 
 instance Exception Error
@@ -538,33 +522,17 @@
 --
 -- @since 1.12.0.0
 isSchedulerError :: Error -> Bool
-isSchedulerError ScheduledBlockedThread = True
-isSchedulerError ScheduledMissingThread = True
-isSchedulerError _ = False
-
--- | Check if an error is an incorrect usage of dejafu.
---
--- @since 1.12.0.0
-isIncorrectUsage :: Error -> Bool
-isIncorrectUsage NestedSubconcurrency = True
-isIncorrectUsage MultithreadedSubconcurrency = True
-isIncorrectUsage LateDontCheck = True
-isIncorrectUsage _ = False
+isSchedulerError _ = True
 
 -------------------------------------------------------------------------------
 -- * Schedule bounding
 
--- | @since 0.2.0.0
+-- | @since 2.0.0.0
 data Bounds = Bounds
   { boundPreemp :: Maybe PreemptionBound
   , boundFair   :: Maybe FairBound
-  , boundLength :: Maybe LengthBound
-  } deriving (Eq, Ord, Read, Show)
-
--- | @since 1.3.1.0
-deriving instance Generic Bounds
+  } deriving (Eq, Ord, Read, Show, Generic)
 
--- | @since 0.5.1.0
 instance NFData Bounds
 
 -- | Restrict the number of pre-emptive context switches allowed in an
@@ -757,3 +725,97 @@
 
 -- | @since 1.3.1.0
 instance NFData MonadFailException
+
+-------------------------------------------------------------------------------
+-- ** Concurrency state
+
+-- | A summary of the concurrency state of the program.
+--
+-- @since 2.0.0.0
+data ConcurrencyState = ConcurrencyState
+  { concIOState :: Map IORefId Int
+  -- ^ Keep track of which @IORef@s have buffered writes.
+  , concMVState :: Set MVarId
+  -- ^ Keep track of which @MVar@s are full.
+  , concMaskState :: 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)
+
+instance NFData ConcurrencyState where
+  rnf cstate = rnf
+    ( concIOState cstate
+    , concMVState cstate
+    , [(t, show m) | (t, m) <- M.toList (concMaskState cstate)]
+    )
+
+-- | Check if a @IORef@ has a buffered write pending.
+--
+-- @since 2.0.0.0
+isBuffered :: ConcurrencyState -> IORefId -> Bool
+isBuffered cstate r = numBuffered cstate r /= 0
+
+-- | Check how many buffered writes an @IORef@ has.
+--
+-- @since 2.0.0.0
+numBuffered :: ConcurrencyState -> IORefId -> Int
+numBuffered cstate r = M.findWithDefault 0 r (concIOState cstate)
+
+-- | Check if an @MVar@ is full.
+--
+-- @since 2.0.0.0
+isFull :: ConcurrencyState -> MVarId -> Bool
+isFull cstate v = S.member v (concMVState cstate)
+
+-- | Check if an exception can interrupt a thread (action).
+--
+-- @since 2.0.0.0
+canInterrupt :: ConcurrencyState -> ThreadId -> ThreadAction -> Bool
+canInterrupt cstate tid act
+  -- If masked interruptible, blocked actions can be interrupted.
+  | isMaskedInterruptible cstate tid = case act of
+    BlockedPutMVar  _ -> True
+    BlockedReadMVar _ -> True
+    BlockedTakeMVar _ -> True
+    BlockedSTM      _ -> True
+    BlockedThrowTo  _ -> True
+    _ -> False
+  -- If masked uninterruptible, nothing can be.
+  | isMaskedUninterruptible cstate tid = False
+  -- If no mask, anything can be.
+  | otherwise = True
+
+-- | Check if an exception can interrupt a thread (lookahead).
+--
+-- @since 2.0.0.0
+canInterruptL :: ConcurrencyState -> ThreadId -> Lookahead -> Bool
+canInterruptL cstate tid lh
+  -- If masked interruptible, actions which can block may be
+  -- interrupted.
+  | isMaskedInterruptible cstate tid = case lh of
+    WillPutMVar  _ -> True
+    WillReadMVar _ -> True
+    WillTakeMVar _ -> True
+    WillSTM        -> True
+    WillThrowTo  _ -> True
+    _ -> False
+  -- If masked uninterruptible, nothing can be.
+  | isMaskedUninterruptible cstate tid = False
+  -- If no mask, anything can be.
+  | otherwise = True
+
+-- | Check if a thread is masked interruptible.
+--
+-- @since 2.0.0.0
+isMaskedInterruptible :: ConcurrencyState -> ThreadId -> Bool
+isMaskedInterruptible cstate tid =
+  M.lookup tid (concMaskState cstate) == Just MaskedInterruptible
+
+-- | Check if a thread is masked uninterruptible.
+--
+-- @since 2.0.0.0
+isMaskedUninterruptible :: ConcurrencyState -> ThreadId -> Bool
+isMaskedUninterruptible cstate tid =
+  M.lookup tid (concMaskState cstate) == Just MaskedUninterruptible
diff --git a/Test/DejaFu/Utils.hs b/Test/DejaFu/Utils.hs
--- a/Test/DejaFu/Utils.hs
+++ b/Test/DejaFu/Utils.hs
@@ -84,8 +84,8 @@
 showCondition :: Condition -> String
 showCondition Abort = "[abort]"
 showCondition Deadlock = "[deadlock]"
-showCondition STMDeadlock = "[stm-deadlock]"
 showCondition (UncaughtException exc) = "[" ++ displayException exc ++ "]"
+showCondition (InvariantFailure _) = "[invariant failure]"
 
 -------------------------------------------------------------------------------
 -- * Scheduling
diff --git a/dejafu.cabal b/dejafu.cabal
--- a/dejafu.cabal
+++ b/dejafu.cabal
@@ -2,18 +2,18 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                dejafu
-version:             1.12.0.0
+version:             2.0.0.0
 synopsis:            A library for unit-testing concurrent programs.
 
 description:
   /[Déjà Fu is] A martial art in which the user's limbs move in time as well as space, […] It is best described as "the feeling that you have been kicked in the head this way before"/ -- Terry Pratchett, Thief of Time
   .
   This package builds on the
-  [concurrency](https://hackage.haskell.org/package/concurrency)
+  <https://hackage.haskell.org/package/concurrency concurrency>
   package by enabling you to deterministically test your concurrent
   programs.
   .
-  See the [website](https://dejafu.readthedocs.io) or README for more.
+  See the <https://dejafu.readthedocs.io website> or README for more.
 
 homepage:            https://github.com/barrucadu/dejafu
 license:             MIT
@@ -33,7 +33,7 @@
 source-repository this
   type:     git
   location: https://github.com/barrucadu/dejafu.git
-  tag:      dejafu-1.12.0.0
+  tag:      dejafu-2.0.0.0
 
 library
   exposed-modules:     Test.DejaFu
@@ -48,6 +48,7 @@
                      , Test.DejaFu.Conc.Internal
                      , Test.DejaFu.Conc.Internal.Common
                      , Test.DejaFu.Conc.Internal.Memory
+                     , Test.DejaFu.Conc.Internal.Program
                      , Test.DejaFu.Conc.Internal.STM
                      , Test.DejaFu.Conc.Internal.Threading
                      , Test.DejaFu.Internal