diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml
index b6105b4c..720d3523 100644
--- a/.github/workflows/haskell-ci.yml
+++ b/.github/workflows/haskell-ci.yml
@@ -40,7 +40,7 @@ jobs:
 
     strategy:
       matrix:
-        ghc-version: [latest, 9.12, "9.10", 9.8, 9.6, 9.4, 9.2, 9.0, "8.10"]
+        ghc-version: [latest, 9.12, "9.10", 9.8, 9.6, 9.4, 9.2, 9.0]
         os: [ubuntu-latest]
       fail-fast: false
 
diff --git a/cabal.project b/cabal.project
index 3f841df8..3e656870 100644
--- a/cabal.project
+++ b/cabal.project
@@ -4,3 +4,16 @@ packages:
 tests: true
 
 test-show-details: direct
+
+source-repository-package
+  type: git
+  location: https://github.com/input-output-hk/io-sim
+  subdir: io-sim
+  tag: 5683864d3c7300f9ee4a3430b4a590bb130cb88a
+
+
+source-repository-package
+  type: git
+  location: https://github.com/input-output-hk/io-sim
+  subdir: io-classes
+  tag: 5683864d3c7300f9ee4a3430b4a590bb130cb88a
diff --git a/quickcheck-dynamic/CHANGELOG.md b/quickcheck-dynamic/CHANGELOG.md
index 17896ad1..3bc1f1b8 100644
--- a/quickcheck-dynamic/CHANGELOG.md
+++ b/quickcheck-dynamic/CHANGELOG.md
@@ -7,6 +7,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 As a minor extension, we also keep a semantic version for the `UNRELEASED`
 changes.
 
+## UNRELEASED
+
+* **BREAKING**: Removed `m` parameter from `PostConditionM` as this is not generally safe.
+* **BREAKING**: Additional `Show` constraint on the result of actions
+* A new module `Test.QuickCheck.ParallelActions` that implements testing linearizability of a model
+  when running in parallel.
+* Additional `Property` combinators `sometimes` and `always`
+
 ## 4.0.0 - 2025-03-12
 
 * **BREAKING**: Removed `Realized`
diff --git a/quickcheck-dynamic/quickcheck-dynamic.cabal b/quickcheck-dynamic/quickcheck-dynamic.cabal
index 925f27c6..bbac3dcc 100644
--- a/quickcheck-dynamic/quickcheck-dynamic.cabal
+++ b/quickcheck-dynamic/quickcheck-dynamic.cabal
@@ -6,6 +6,7 @@ license-files:
   LICENSE
   NOTICE
 
+Tested-with: GHC >= 9.0 && < 9.13
 maintainer:         sebastian.nagel@iohk.io
 author:             Ulf Norell
 category:           Testing
@@ -27,6 +28,9 @@ source-repository head
   type:     git
   location: https://github.com/input-output-hk/quickcheck-dynamic
 
+flag dev
+  default: False
+
 common lang
   default-language:   Haskell2010
   default-extensions:
@@ -62,6 +66,7 @@ common lang
     -Wall -Wnoncanonical-monad-instances -Wunused-packages
     -Wincomplete-uni-patterns -Wincomplete-record-updates
     -Wredundant-constraints -Widentities -Wno-unused-do-bind
+    -Wno-name-shadowing -Wno-x-partial
 
 library
   import:          lang
@@ -76,6 +81,23 @@ library
     Test.QuickCheck.Extras
     Test.QuickCheck.StateModel
     Test.QuickCheck.StateModel.Variables
+    Test.QuickCheck.ParallelActions
+
+  if flag(dev)
+    hs-source-dirs: test
+    exposed-modules:
+      Spec.DynamicLogic.Counters
+      Spec.DynamicLogic.Registry
+      Spec.DynamicLogic.RegistryModel
+      Test.QuickCheck.DynamicLogic.QuantifySpec
+      Test.QuickCheck.StateModelSpec
+    build-depends:
+      , io-classes
+      , io-sim
+      , stm
+      , tasty
+      , tasty-hunit
+      , tasty-quickcheck
 
   build-depends:
     , base        >=4.7 && <5
@@ -100,6 +122,8 @@ test-suite quickcheck-dynamic-test
   build-depends:
     , base
     , containers
+    , io-classes
+    , io-sim
     , mtl
     , QuickCheck
     , quickcheck-dynamic
diff --git a/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs b/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs
index 30713f27..4aaf7e26 100644
--- a/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs
+++ b/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs
@@ -60,10 +60,10 @@ instance Monad (DL s) where
 instance MonadFail (DL s) where
   fail = errorDL
 
-action :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s (Var a)
+action :: (Typeable a, Show a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s (Var a)
 action cmd = DL $ \_ k -> DL.after cmd k
 
-failingAction :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s ()
+failingAction :: (Typeable a, Show a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s ()
 failingAction cmd = DL $ \_ k -> DL.afterNegative cmd (k ())
 
 anyAction :: DL s ()
@@ -96,7 +96,7 @@ getModelStateDL = DL $ \s k -> k (underlyingState s) s
 getVarContextDL :: DL s VarContext
 getVarContextDL = DL $ \s k -> k (vars s) s
 
-forAllVar :: forall a s. Typeable a => DL s (Var a)
+forAllVar :: forall a s. (Typeable a, Show a) => DL s (Var a)
 forAllVar = do
   xs <- ctxAtType <$> getVarContextDL
   forAllQ $ elementsQ xs
diff --git a/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Internal.hs b/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Internal.hs
index ec01cbf7..8d0967f7 100644
--- a/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Internal.hs
+++ b/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Internal.hs
@@ -33,7 +33,7 @@ data DynLogic s
     Stopping (DynLogic s)
   | -- | After a specific action the predicate should hold
     forall a.
-    (Eq (Action s a), Show (Action s a), Typeable a) =>
+    (Eq (Action s a), Show (Action s a), Typeable a, Show a) =>
     After (ActionWithPolarity s a) (Var a -> DynPred s)
   | Error String (DynPred s)
   | -- | Adjust the probability of picking a branch
@@ -66,7 +66,7 @@ afterAny :: (Annotated s -> DynFormula s) -> DynFormula s
 afterAny f = DynFormula $ \n -> AfterAny $ \s -> unDynFormula (f s) n
 
 afterPolar
-  :: (Typeable a, Eq (Action s a), Show (Action s a))
+  :: (Typeable a, Show a, Eq (Action s a), Show (Action s a))
   => ActionWithPolarity s a
   -> (Var a -> Annotated s -> DynFormula s)
   -> DynFormula s
@@ -75,7 +75,7 @@ afterPolar act f = DynFormula $ \n -> After act $ \x s -> unDynFormula (f x s) n
 -- | Given `f` must be `True` after /some/ action.
 -- `f` is passed the state resulting from executing the `Action`.
 after
-  :: (Typeable a, Eq (Action s a), Show (Action s a))
+  :: (Typeable a, Show a, Eq (Action s a), Show (Action s a))
   => Action s a
   -> (Var a -> Annotated s -> DynFormula s)
   -> DynFormula s
@@ -85,7 +85,7 @@ after act f = afterPolar (ActionWithPolarity act PosPolarity) f
 -- `f` is passed the state resulting from executing the `Action`
 -- as a negative action.
 afterNegative
-  :: (Typeable a, Eq (Action s a), Show (Action s a))
+  :: (Typeable a, Show a, Eq (Action s a), Show (Action s a))
   => Action s a
   -> (Annotated s -> DynFormula s)
   -> DynFormula s
diff --git a/quickcheck-dynamic/src/Test/QuickCheck/Extras.hs b/quickcheck-dynamic/src/Test/QuickCheck/Extras.hs
index ea5b51c7..61d8f73b 100644
--- a/quickcheck-dynamic/src/Test/QuickCheck/Extras.hs
+++ b/quickcheck-dynamic/src/Test/QuickCheck/Extras.hs
@@ -2,6 +2,7 @@ module Test.QuickCheck.Extras where
 
 import Control.Monad.Reader
 import Control.Monad.State
+import Test.QuickCheck
 import Test.QuickCheck.Monadic
 
 runPropertyStateT :: Monad m => PropertyM (StateT s m) a -> s -> PropertyM m (a, s)
@@ -13,3 +14,9 @@ runPropertyReaderT :: Monad m => PropertyM (ReaderT e m) a -> e -> PropertyM m a
 runPropertyReaderT p e = MkPropertyM $ \k -> do
   m <- unPropertyM p $ fmap lift . k
   return $ runReaderT m e
+
+sometimes :: Testable p => Int -> p -> Property
+sometimes i = disjoin . replicate i
+
+always :: Testable p => Int -> p -> Property
+always i = conjoin . replicate i
diff --git a/quickcheck-dynamic/src/Test/QuickCheck/ParallelActions.hs b/quickcheck-dynamic/src/Test/QuickCheck/ParallelActions.hs
new file mode 100644
index 00000000..a6508dac
--- /dev/null
+++ b/quickcheck-dynamic/src/Test/QuickCheck/ParallelActions.hs
@@ -0,0 +1,258 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE RecordWildCards #-}
+
+-- | Experimental support for running parallel actions
+module Test.QuickCheck.ParallelActions (
+  RunModelPar (..),
+  Forking (..),
+  ParallelActions,
+  runParActions,
+) where
+
+import Control.Arrow (first, second)
+import Control.Concurrent
+import Control.Monad
+import Control.Monad.Reader
+import Control.Monad.Writer
+import Data.Data
+import Data.Set qualified as Set
+import Data.Tree
+import GHC.Generics
+import Test.QuickCheck hiding (Some)
+import Test.QuickCheck.Monadic
+import Test.QuickCheck.StateModel
+import Test.QuickCheck.StateModel.Variables
+
+-- | The callbacks necessary to run actions in parallel
+class RunModel state m => RunModelPar state m where
+  -- | Note that this version of `perform` doesn't get the current `state`.
+  -- This is because the system is not in a definite model state during
+  -- parallel execution.
+  performPar :: Typeable a => Action state a -> LookUp -> m (PerformResult state m a)
+  performPar = perform (error "Trying to evaluate state in default implementation of performPar")
+
+  -- | Like `monitoring` but without the `state`
+  monitoringPar :: Action state a -> LookUp -> Either (Error state m) a -> Property -> Property
+  monitoringPar _ _ _ = id
+
+data ParallelActions state
+  = ParallelActions
+  { linearActions :: Actions state
+  , threads :: [[Int]]
+  }
+  deriving (Eq, Generic)
+
+commonActions :: ParallelActions state -> [Step state]
+commonActions ParallelActions{linearActions = Actions steps, ..} =
+  [step | step@(v := _) <- steps, notElem (unsafeVarIndex v) $ concat threads]
+
+threadActions :: ParallelActions state -> [[Step state]]
+threadActions ParallelActions{linearActions = Actions steps, ..} =
+  [ [ v := s{polarity = PosPolarity}
+    | v := s <- steps
+    , elem (unsafeVarIndex v) thread
+    ]
+  | thread <- threads
+  ]
+
+firstParAction :: ParallelActions state -> Maybe Int
+firstParAction ParallelActions{..}
+  | null idxs = Nothing
+  | otherwise = Just $ minimum idxs
+  where
+    idxs = concat threads
+
+instance StateModel state => Show (ParallelActions state) where
+  show pas =
+    unlines $
+      [ "-- Common Prefix:"
+      , showWithUsed (foldMap allVariables threads) common
+      ]
+        ++ concat
+          [ [ "-- Thread " ++ [n]
+            , show thread
+            ]
+          | (n, thread) <- zip ['A' .. 'Z'] threads
+          ]
+    where
+      common = Actions $ commonActions pas
+      threads = Actions <$> threadActions pas
+
+instance StateModel state => Arbitrary (ParallelActions state) where
+  arbitrary = genParActions
+
+  shrink pas@(ParallelActions actions trs) =
+    [ParallelActions actions $ map (filter (/= i)) trs | Just i <- [firstParAction pas]]
+      ++ filter
+        checkParallelActions
+        [ ParallelActions actions $ filter (not . null) $ map (filter (`Set.member` vars)) trs
+        | actions <- shrink actions
+        , let vars = unsafeIndexSet $ allVariables actions
+        ]
+
+checkParallelActions :: StateModel state => ParallelActions state -> Bool
+checkParallelActions pas = all (checkWellTypedness commonCtx) (threadActions pas)
+  where
+    commonCtx = allVariables common
+    common = Actions $ commonActions pas
+
+checkWellTypedness :: StateModel state => VarContext -> [Step state] -> Bool
+checkWellTypedness _ [] = True
+checkWellTypedness ctx ((v := a) : ss) = a `wellTypedIn` ctx && checkWellTypedness (extendContext ctx v) ss
+
+genParActions :: forall state. StateModel state => Gen (ParallelActions state)
+genParActions = do
+  -- The ~ works around a bug in ghc (https://gitlab.haskell.org/ghc/ghc/-/issues/22004) (which is not in all ghc versions ?!)
+  as@(~(Actions steps)) <- arbitrary
+  let n = length steps
+  split <- choose (max 0 (n - 20), n - 1)
+  let (common, post) = splitAt split steps
+      commonCtx = allVariables common
+  tc <- choose (2, 5)
+  threads <- go post $ replicate tc (commonCtx, [])
+  return $ ParallelActions as $ filter (not . null) threads
+  where
+    go :: [Step state] -> [(VarContext, [Int])] -> Gen [[Int]]
+    go [] trs = return $ map (reverse . snd) trs
+    go ((v := a) : ss) trs = do
+      let candidates =
+            [ (ctx, tr, trs)
+            | ((ctx, tr), trs) <- holes trs
+            , a `wellTypedIn` ctx
+            ]
+      if null candidates
+        -- This means we made a mistake earlier and split two actions whose
+        -- result variables were used together later. At this point we just
+        -- give up and don't extend the traces.
+        then go [] trs
+        else do
+          (ctx, tr, trs) <- elements candidates
+          go ss $ (extendContext ctx v, unsafeVarIndex v : tr) : trs
+
+data TraceStep state m where
+  TraceStep
+    :: (Typeable a, Show a)
+    => Either (Error state m) a
+    -> Var a
+    -> ActionWithPolarity state a
+    -> TraceStep state m
+
+type Trace state m = [TraceStep state m]
+type TraceTree state m = Tree (TraceStep state m)
+
+runTracing
+  :: ( RunModelPar state m
+     , e ~ Error state m
+     , forall a. IsPerformResult e a
+     )
+  => Env -> [Step state] -> m (Trace state m, Env)
+runTracing env [] = return ([], env)
+runTracing env ((v := ap) : as) = do
+  r <- performResultToEither <$> performPar (polarAction ap) (lookUpVar env)
+  let step = TraceStep r v ap
+      env'
+        | Right val <- r = (v :== val) : env
+        | otherwise = env
+  (first (step :)) <$> runTracing env' as
+
+class Monad m => Forking m where
+  forkThread :: m a -> m (m a)
+
+instance Forking IO where
+  forkThread io = do
+    t <- newEmptyMVar
+    forkIO $ io >>= putMVar t
+    return $ takeMVar t
+
+instance Forking m => Forking (ReaderT r m) where
+  forkThread m = do
+    reg <- ask
+    lift $ fmap lift (forkThread $ runReaderT m reg)
+
+-- | Run parallel actions consisting of a common prefix and a number of
+-- parallel threads. After execution check that the preconditions were
+-- respected in all possible parallel executions and check that we find at
+-- least one parallel execution which is linearizible.
+runParActions
+  :: ( StateModel state
+     , RunModelPar state m
+     , e ~ Error state m
+     , forall a. IsPerformResult e a
+     , Forking m
+     )
+  => ParallelActions state -> PropertyM m ()
+runParActions pas = do
+  (trC, env) <- run $ runTracing mempty $ commonActions pas
+  joins <- mapM (run . forkThread . runTracing env) (threadActions pas)
+  trs <- mapM (fmap fst . run) joins
+  let used = varsUsedInActions $ linearActions pas
+  monitor $ counterexample "-- Main thread:"
+  monitorTrace used mempty trC
+  forM (zip ['A' .. 'Z'] trs) $ \(n, tr) -> do
+    monitor $ counterexample $ "\n-- Thread " ++ [n, ':']
+    monitorTrace used env tr
+  let ilvs = prepend trC $ interleavings trs
+  monitor $ tabulate "Trace tree size" (map (bucket . length) ilvs)
+  assert $ null ilvs || any (checkTrace initialAnnotatedState mempty) ilvs
+
+monitorTrace
+  :: forall state m
+   . (StateModel state, RunModelPar state m)
+  => VarContext -> Env -> Trace state m -> PropertyM m ()
+monitorTrace _used _env [] = pure ()
+monitorTrace used env (TraceStep r v act : tr) = do
+  let showR (Right x)
+        | v `wellTypedIn` used = show v ++ "@" ++ showsPrec 10 x ""
+        | otherwise = show x
+      showR (Left err) = "fail " ++ showsPrec 10 err ""
+  monitor $ counterexample (showR r ++ " <- " ++ show (polarAction act))
+  monitor $ monitoringPar @state @m (polarAction act) (lookUpVar env) r
+  monitorTrace used env' tr
+  where
+    env'
+      | Right val <- r = (v :== val) : env
+      | otherwise = env
+
+checkTrace
+  :: forall state m
+   . (StateModel state, RunModelPar state m)
+  => Annotated state -> Env -> TraceTree state m -> Bool
+checkTrace s env (Node (TraceStep r v (ActionWithPolarity a _)) trs) =
+  -- NOTE: we need to re-compute the polarity of `a` here because it may be that the failure can be explained,
+  -- but only by the action failing when it was previous successful
+  let act = actionWithPolarity s a
+      s' = computeNextState s act v
+      env'
+        | Right val <- r = (v :== val) : env
+        | otherwise = env
+      checkPost
+        | Right val <- r
+        , polarity act == PosPolarity =
+            fst . runWriter . runPost $
+              postcondition @state @m
+                (underlyingState s, underlyingState s')
+                (polarAction act)
+                (lookUpVar env')
+                val
+        | Left{} <- r, polarity act == PosPolarity = False
+        | otherwise =
+            fst . runWriter . runPost $
+              postconditionOnFailure @state @m
+                (underlyingState s, underlyingState s')
+                (polarAction act)
+                (lookUpVar env')
+                r
+   in (computePrecondition s act || discard) && checkPost && (null trs || any (checkTrace s' env') trs)
+
+prepend :: [a] -> [Tree a] -> [Tree a]
+prepend [] ts = ts
+prepend (p : ps) ts = [Node p $ prepend ps ts]
+
+interleavings :: [[a]] -> [Tree a]
+interleavings aas = do
+  (a : as, os) <- holes aas
+  pure $ Node a (interleavings (as : os))
+
+holes :: [a] -> [(a, [a])]
+holes [] = []
+holes (a : as) = (a, as) : map (second (a :)) (holes as)
diff --git a/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs b/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs
index 5c801da8..e2cdbfcf 100644
--- a/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs
+++ b/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs
@@ -16,6 +16,8 @@ module Test.QuickCheck.StateModel (
   PostconditionM (..),
   WithUsedVars (..),
   Annotated (..),
+  IsPerformResult,
+  PerformResult,
   Step (..),
   Polarity (..),
   ActionWithPolarity (..),
@@ -26,7 +28,6 @@ module Test.QuickCheck.StateModel (
   pattern (:=?),
   Env,
   Generic,
-  IsPerformResult,
   Options (..),
   monitorPost,
   counterexamplePost,
@@ -44,11 +45,15 @@ module Test.QuickCheck.StateModel (
   shrinkActionsWithOptions,
   defaultOptions,
   moreActions,
+  showWithUsed,
+  performResultToEither,
+  bucket,
+  actionWithPolarity,
+  varsUsedInActions,
 ) where
 
 import Control.Monad
-import Control.Monad.Reader
-import Control.Monad.Writer (WriterT, runWriterT, tell)
+import Control.Monad.Writer hiding (Any)
 import Data.Data
 import Data.Kind
 import Data.List
@@ -56,8 +61,7 @@ import Data.Monoid (Endo (..))
 import Data.Set qualified as Set
 import Data.Void
 import GHC.Generics
-import Test.QuickCheck (Arbitrary, Gen, Property, Smart (..), Testable, counterexample, forAllShrink, frequency, property, resize, shrinkList, sized, tabulate)
-import Test.QuickCheck qualified as QC
+import Test.QuickCheck hiding (Some)
 import Test.QuickCheck.DynamicLogic.SmartShrinking
 import Test.QuickCheck.Monadic
 import Test.QuickCheck.StateModel.Variables
@@ -160,15 +164,12 @@ class
 
 deriving instance (forall a. Show (Action state a)) => Show (Any (Action state))
 
-newtype PostconditionM m a = PostconditionM {runPost :: WriterT (Endo Property, Endo Property) m a}
+newtype PostconditionM a = PostconditionM {runPost :: Writer (Endo Property, Endo Property) a}
   deriving (Functor, Applicative, Monad)
 
-instance MonadTrans PostconditionM where
-  lift = PostconditionM . lift
-
-evaluatePostCondition :: Monad m => PostconditionM m Bool -> PropertyM m ()
+evaluatePostCondition :: Monad m => PostconditionM Bool -> PropertyM m ()
 evaluatePostCondition post = do
-  (b, (Endo mon, Endo onFail)) <- run . runWriterT . runPost $ post
+  let (b, (Endo mon, Endo onFail)) = runWriter . runPost $ post
   monitor mon
   unless b $ monitor onFail
   assert b
@@ -176,11 +177,11 @@ evaluatePostCondition post = do
 -- | Apply the property transformation to the property after evaluating
 -- the postcondition. Useful for collecting statistics while avoiding
 -- duplication between `monitoring` and `postcondition`.
-monitorPost :: Monad m => (Property -> Property) -> PostconditionM m ()
+monitorPost :: (Property -> Property) -> PostconditionM ()
 monitorPost m = PostconditionM $ tell (Endo m, mempty)
 
 -- | Acts as `Test.QuickCheck.counterexample` if the postcondition fails.
-counterexamplePost :: Monad m => String -> PostconditionM m ()
+counterexamplePost :: String -> PostconditionM ()
 counterexamplePost c = PostconditionM $ tell (mempty, Endo $ counterexample c)
 
 -- | The result required of `perform` depending on the `Error` type.
@@ -202,7 +203,7 @@ instance {-# OVERLAPPING #-} IsPerformResult Void a where
 instance {-# OVERLAPPABLE #-} (EitherIsh e a ~ Either e a) => IsPerformResult e a where
   performResultToEither = id
 
-class (forall a. Show (Action state a), Monad m) => RunModel state m where
+class (forall a. Show (Action state a), Show (Error state m), Monad m) => RunModel state m where
   -- | The type of errors that actions can throw. If this is defined as anything
   -- other than `Void` `perform` is required to return `Either (Error state) a`
   -- instead of `a`.
@@ -225,14 +226,14 @@ class (forall a. Show (Action state a), Monad m) => RunModel state m where
   -- | Postcondition on the `a` value produced at some step.
   -- The result is `assert`ed and will make the property fail should it be `False`. This is useful
   -- to check the implementation produces expected values.
-  postcondition :: (state, state) -> Action state a -> LookUp -> a -> PostconditionM m Bool
+  postcondition :: (state, state) -> Action state a -> LookUp -> a -> PostconditionM Bool
   postcondition _ _ _ _ = pure True
 
   -- | Postcondition on the result of running a _negative_ `Action`.
   -- The result is `assert`ed and will make the property fail should it be `False`. This is useful
   -- to check the implementation produces e.g. the expected errors or to check that the SUT hasn't
   -- been updated during the execution of the negative action.
-  postconditionOnFailure :: (state, state) -> Action state a -> LookUp -> Either (Error state m) a -> PostconditionM m Bool
+  postconditionOnFailure :: (state, state) -> Action state a -> LookUp -> Either (Error state m) a -> PostconditionM Bool
   postconditionOnFailure _ _ _ _ = pure True
 
   -- | Allows the user to attach additional information to the `Property` at each step of the process.
@@ -300,7 +301,7 @@ deriving instance Eq (Action state a) => Eq (ActionWithPolarity state a)
 
 data Step state where
   (:=)
-    :: (Typeable a, Eq (Action state a), Show (Action state a))
+    :: (Typeable a, Show a, Eq (Action state a), Show (Action state a))
     => Var a
     -> ActionWithPolarity state a
     -> Step state
@@ -352,12 +353,15 @@ instance Eq (Actions state) where
   Actions as == Actions as' = as == as'
 
 instance StateModel state => Show (Actions state) where
-  show (Actions as) =
-    let as' = WithUsedVars (usedVariables (Actions as)) <$> as
-     in intercalate "\n" $ zipWith (++) ("do " : repeat "   ") (map show as' ++ ["pure ()"])
+  show = showWithUsed mempty
+
+showWithUsed :: StateModel state => VarContext -> Actions state -> String
+showWithUsed ctx (Actions as) =
+  let as' = WithUsedVars (ctx <> varsUsedInActions (Actions as)) <$> as
+   in intercalate "\n" $ zipWith (++) ("do " : repeat "   ") (map show as' ++ ["pure ()" | null as'])
 
-usedVariables :: forall state. StateModel state => Actions state -> VarContext
-usedVariables (Actions as) = go initialAnnotatedState as
+varsUsedInActions :: forall state. StateModel state => Actions state -> VarContext
+varsUsedInActions (Actions as) = go initialAnnotatedState as
   where
     go :: Annotated state -> [Step state] -> VarContext
     go aState [] = allVariables (underlyingState aState)
@@ -439,10 +443,10 @@ generateActionsWithOptions Options{..} = do
           | otherwise = do
               a <- resize m $ computeArbitraryAction s
               case a of
-                Some act ->
+                Some act@ActionWithPolarity{..} ->
                   if computePrecondition s act
                     then return (Just (Some act), rej)
-                    else go (m + 1) n (actionName (polarAction act) : rej)
+                    else go (m + 1) n (actionName polarAction : rej)
 
 shrinkActionsWithOptions :: forall state. StateModel state => Options state -> Actions state -> [Actions state]
 shrinkActionsWithOptions _ (Actions_ rs as) =
@@ -492,7 +496,7 @@ computePrecondition s (ActionWithPolarity a p) =
         && polarPrecondition
 
 computeNextState
-  :: (StateModel state, Typeable a)
+  :: (StateModel state, Typeable a, Show a)
   => Annotated state
   -> ActionWithPolarity state a
   -> Var a
@@ -551,13 +555,6 @@ runActions
   => Actions state
   -> PropertyM m (Annotated state, Env)
 runActions (Actions_ rejected (Smart _ actions)) = do
-  let bucket = \n -> let (a, b) = go n in show a ++ " - " ++ show b
-        where
-          go n
-            | n < 100 = (d * 10, d * 10 + 9)
-            | otherwise = let (a, b) = go d in (a * 10, b * 10 + 9)
-            where
-              d = div n 10
   monitor $ tabulate "# of actions" [show $ bucket $ length actions]
   (finalState, env, names, polars) <- runSteps initialAnnotatedState [] actions
   monitor $ tabulate "Actions" names
@@ -567,6 +564,16 @@ runActions (Actions_ rejected (Smart _ actions)) = do
       tabulate "Actions rejected by precondition" rejected
   return (finalState, env)
 
+bucket :: Int -> String
+bucket n = show a ++ " - " ++ show b
+  where
+    (a, b) = go n
+    go n
+      | n < 100 = (d * 10, d * 10 + 9)
+      | otherwise = let (a, b) = go d in (a * 10, b * 10 + 9)
+      where
+        d = div n 10
+
 -- | Core function to execute a sequence of `Step` given some initial `Env`ironment and `Annotated`
 -- state. Return the list of action names and polarities to work around
 -- https://github.com/nick8325/quickcheck/issues/416 causing repeated calls to tabulate being slow.
@@ -614,7 +621,7 @@ runSteps s env ((v := act) : as) = do
     positiveActionSucceeded ret val = do
       (s', env', stateTransition) <- computeNewState ret
       evaluatePostCondition $
-        postcondition
+        postcondition @state @m
           stateTransition
           action
           (lookUpVar env)
@@ -624,7 +631,7 @@ runSteps s env ((v := act) : as) = do
     negativeActionResult ret = do
       (s', env', stateTransition) <- computeNewState ret
       evaluatePostCondition $
-        postconditionOnFailure
+        postconditionOnFailure @state @m
           stateTransition
           action
           (lookUpVar env)
diff --git a/quickcheck-dynamic/src/Test/QuickCheck/StateModel/Variables.hs b/quickcheck-dynamic/src/Test/QuickCheck/StateModel/Variables.hs
index a42a8b5c..b5c3091e 100644
--- a/quickcheck-dynamic/src/Test/QuickCheck/StateModel/Variables.hs
+++ b/quickcheck-dynamic/src/Test/QuickCheck/StateModel/Variables.hs
@@ -16,8 +16,11 @@ module Test.QuickCheck.StateModel.Variables (
   isWellTyped,
   allVariables,
   isEmptyCtx,
+  wellTypedIn,
+  unsafeVarIndex,
   unsafeCoerceVar,
   unsafeNextVarIndex,
+  unsafeIndexSet,
 ) where
 
 import Data.Data
@@ -35,7 +38,7 @@ import Test.QuickCheck (Gen, Smart (..), elements)
 
 -- | A symbolic variable for a value of type `a`
 newtype Var a = Var Int
-  deriving (Eq, Ord, Typeable, Data)
+  deriving (Eq, Ord, Data)
 
 -- | Create a fresh symbolic variable with given identifier. While 'Var's are
 -- usually created by action generators, this function can be used for example
@@ -55,7 +58,7 @@ class HasVariables a where
 instance HasVariables a => HasVariables (Smart a) where
   getAllVariables (Smart _ a) = getAllVariables a
 
-instance Typeable a => HasVariables (Var a) where
+instance (Typeable a, Show a) => HasVariables (Var a) where
   getAllVariables = Set.singleton . Some
 
 instance (HasVariables k, HasVariables v) => HasVariables (Map k v) where
@@ -84,7 +87,7 @@ deriving via HasNoVariables Word32 instance HasVariables Word32
 deriving via HasNoVariables Word64 instance HasVariables Word64
 
 data Any f where
-  Some :: (Typeable a, Eq (f a)) => f a -> Any f
+  Some :: (Typeable a, Show a, Eq (f a)) => f a -> Any f
 
 instance Eq (Any f) where
   Some (a :: f a) == Some (b :: f b) =
@@ -110,19 +113,25 @@ instance Show VarContext where
       -- The use of typeRep here is on purpose to avoid printing `Var` unnecessarily.
       showBinding (Some v) = show v ++ " :: " ++ show (typeRep v)
 
+unsafeIndexSet :: VarContext -> Set Int
+unsafeIndexSet (VarCtx ctx) = Set.map (\(Some v) -> unsafeVarIndex v) ctx
+
 isEmptyCtx :: VarContext -> Bool
 isEmptyCtx (VarCtx ctx) = null ctx
 
-isWellTyped :: Typeable a => Var a -> VarContext -> Bool
+isWellTyped :: (Typeable a, Show a) => Var a -> VarContext -> Bool
 isWellTyped v (VarCtx ctx) = not (null ctx) && Some v `Set.member` ctx
 
+wellTypedIn :: HasVariables a => a -> VarContext -> Bool
+wellTypedIn a ctx = all (\(Some v) -> v `isWellTyped` ctx) (getAllVariables a)
+
 -- TODO: check the invariant that no variable index is used
 -- twice at different types. This is generally not an issue
 -- because lookups take types into account (so it *shouldn't*
 -- cause an issue, but it might be good practise to crash
 -- if the invariant is violated anyway as it is evidence that
 -- something is horribly broken at the use site).
-extendContext :: Typeable a => VarContext -> Var a -> VarContext
+extendContext :: (Typeable a, Show a) => VarContext -> Var a -> VarContext
 extendContext (VarCtx ctx) v = VarCtx $ Set.insert (Some v) ctx
 
 allVariables :: HasVariables a => a -> VarContext
@@ -140,6 +149,9 @@ shrinkVar ctx v = filter (< v) $ ctxAtType ctx
 unsafeCoerceVar :: Var a -> Var b
 unsafeCoerceVar (Var i) = Var i
 
+unsafeVarIndex :: Var a -> Int
+unsafeVarIndex (Var i) = i
+
 unsafeNextVarIndex :: VarContext -> Int
 unsafeNextVarIndex (VarCtx vs) = 1 + maximum (0 : [i | Some (Var i) <- Set.toList vs])
 
diff --git a/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs b/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs
index e842be62..20afdfd5 100644
--- a/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs
+++ b/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE ImpredicativeTypes #-}
 {-# LANGUAGE NamedFieldPuns #-}
 
 -- | Define several variant models of /counters/ which are useful to
@@ -5,10 +6,20 @@
 module Spec.DynamicLogic.Counters where
 
 import Control.Monad.Reader
-import Data.IORef
-import Test.QuickCheck (frequency)
+import Test.QuickCheck hiding (Some)
+import Test.QuickCheck.Extras
+import Test.QuickCheck.Gen.Unsafe
+import Test.QuickCheck.Monadic
+import Test.QuickCheck.ParallelActions
 import Test.QuickCheck.StateModel
 
+import Control.Concurrent.Class.MonadSTM
+import Control.Monad.Class.MonadFork
+import Control.Monad.Class.MonadTest
+import Control.Monad.Class.MonadThrow
+import Control.Monad.Class.MonadTimer
+import Control.Monad.IOSim
+
 -- A very simple model with a single action that always succeed in
 -- predictable way. This model is useful for testing the runtime.
 newtype SimpleCounter = SimpleCounter {count :: Int}
@@ -29,10 +40,13 @@ instance StateModel SimpleCounter where
 
   nextState SimpleCounter{count} IncSimple _ = SimpleCounter (count + 1)
 
-instance RunModel SimpleCounter (ReaderT (IORef Int) IO) where
+instance RunModel SimpleCounter (ReaderT (CounterState IO) IO) where
   perform _ IncSimple _ = do
-    ref <- ask
-    lift $ atomicModifyIORef' ref (\count -> (succ count, count))
+    ref <- asks counterState
+    lift $ atomically $ do
+      c <- readTVar ref
+      writeTVar ref (c + 1)
+      return c
 
 -- A very simple model with a single action whose postcondition fails in a
 -- predictable way. This model is useful for testing the runtime.
@@ -54,10 +68,13 @@ instance StateModel FailingCounter where
 
   nextState FailingCounter{failingCount} Inc' _ = FailingCounter (failingCount + 1)
 
-instance RunModel FailingCounter (ReaderT (IORef Int) IO) where
+instance RunModel FailingCounter (ReaderT (CounterState IO) IO) where
   perform _ Inc' _ = do
-    ref <- ask
-    lift $ atomicModifyIORef' ref (\count -> (succ count, count))
+    ref <- asks counterState
+    lift $ atomically $ do
+      c <- readTVar ref
+      writeTVar ref (c + 1)
+      return c
 
   postcondition (_, FailingCounter{failingCount}) _ _ _ = pure $ failingCount < 4
 
@@ -82,16 +99,77 @@ instance StateModel Counter where
   nextState (Counter n) Inc _ = Counter (n + 1)
   nextState _ Reset _ = Counter 0
 
-instance RunModel Counter (ReaderT (IORef Int) IO) where
+newtype CounterState m = CounterState {counterState :: TVar m Int}
+
+setupCounterState :: MonadSTM m => m (CounterState m)
+setupCounterState = CounterState <$> atomically (newTVar 0)
+
+instance (MonadSTM m) => RunModel Counter (ReaderT (CounterState m) m) where
   perform _ Inc _ = do
-    ref <- ask
-    lift $ modifyIORef ref succ
+    ref <- asks counterState
+    lift $ do
+      n <- atomically $ readTVar ref
+      atomically $ writeTVar ref (n + 1)
   perform _ Reset _ = do
-    ref <- ask
+    ref <- asks counterState
     lift $ do
-      n <- readIORef ref
-      writeIORef ref 0
+      n <- atomically $ readTVar ref
+      atomically $ writeTVar ref 0
       pure n
 
   postcondition (Counter n, _) Reset _ res = pure $ n == res
   postcondition _ _ _ _ = pure True
+
+instance MonadSTM m => RunModelPar Counter (ReaderT (CounterState m) m) where
+  performPar Inc _ = do
+    ref <- asks counterState
+    -- lift $ atomically $ modifyTVar ref (\ c -> (c+1, ()))
+    lift $ do
+      n <- atomically $ readTVar ref
+      atomically $ writeTVar ref (n + 1)
+  performPar Reset _ = do
+    ref <- asks counterState
+    lift $ atomically $ do
+      c <- readTVar ref
+      writeTVar ref 0
+      return c
+
+prop_counter :: Actions Counter -> Property
+prop_counter as = monadicIO $ do
+  ref <- lift $ atomically $ newTVar (0 :: Int)
+  runPropertyReaderT (runActions as) (CounterState ref :: CounterState IO)
+  assert True
+
+prop_counter_par :: ParallelActions Counter -> Property
+prop_counter_par as = always 10 $ monadicIO $ do
+  ref <- lift setupCounterState
+  runPropertyReaderT (runParActions as) ref
+
+prop_counter_parIOSimPor :: ParallelActions Counter -> Property
+prop_counter_parIOSimPor as =
+  monadicIOSimPOR_ prop
+  where
+    prop :: forall s. PropertyM (IOSim s) ()
+    prop = do
+      ref <- lift $ atomically $ newTVar (0 :: Int)
+      lift $ exploreRaces
+      runPropertyReaderT (runParActions as) (CounterState ref :: CounterState (IOSim s))
+
+-- NOTE: This is a hack to get around issues with old ghc versions
+data Exists where
+  Ex :: (forall s. IOSim s Property) -> Exists
+
+monadicIOSimPOR_ :: Testable a => (forall s. PropertyM (IOSim s) a) -> Property
+monadicIOSimPOR_ prop = forAllBlind prop' $ \(Ex p) -> exploreSimTrace id p $ \_ tr ->
+  either (flip counterexample False . show) id $ traceResult False tr
+  where
+    prop' :: Gen Exists
+    prop' = do
+      Capture eval <- capture
+      pure $ Ex $ eval $ monadic' prop
+
+instance Forking (IOSim s) where
+  forkThread io = do
+    t <- atomically newEmptyTMVar
+    forkIO $ io >>= atomically . putTMVar t
+    return $ atomically $ takeTMVar t
diff --git a/quickcheck-dynamic/test/Spec/DynamicLogic/Registry.hs b/quickcheck-dynamic/test/Spec/DynamicLogic/Registry.hs
index b4677cc6..fcefa1e3 100644
--- a/quickcheck-dynamic/test/Spec/DynamicLogic/Registry.hs
+++ b/quickcheck-dynamic/test/Spec/DynamicLogic/Registry.hs
@@ -2,49 +2,93 @@
 -- process registry.
 module Spec.DynamicLogic.Registry where
 
-import Control.Concurrent.STM
+import Control.Concurrent.Class.MonadSTM
+import Control.Exception.Base (pattern ErrorCall)
 import Control.Monad
-import GHC.Conc
+import Control.Monad.Class.MonadFork
+import Control.Monad.Class.MonadThrow
+import Data.List qualified as List
 
-type Registry = TVar [(String, ThreadId)]
+data Reg m = Reg
+  { registered :: [(String, ThreadId m)]
+  -- This is because IOSim doesn't have a way to tell if a thread is alive or
+  -- not
+  , aliveThreads :: [ThreadId m]
+  }
 
-isAlive :: ThreadId -> IO Bool
-isAlive tid = do
-  s <- threadStatus tid
-  return $ s /= ThreadFinished && s /= ThreadDied
+emptyReg :: Reg m
+emptyReg = Reg [] []
 
-setupRegistry :: IO Registry
-setupRegistry = atomically $ newTVar []
+modifyRegistered :: ([(String, ThreadId m)] -> [(String, ThreadId m)]) -> Reg m -> Reg m
+modifyRegistered f reg = reg{registered = f (registered reg)}
 
-whereis :: Registry -> String -> IO (Maybe ThreadId)
+modifyAlive :: ([ThreadId m] -> [ThreadId m]) -> Reg m -> Reg m
+modifyAlive f reg = reg{aliveThreads = f (aliveThreads reg)}
+
+newtype Registry m = Registry (TVar m (Reg m))
+
+readReg :: MonadSTM m => Registry m -> STM m (Reg m)
+readReg (Registry r) = readTVar r
+
+writeReg :: MonadSTM m => Registry m -> Reg m -> STM m ()
+writeReg (Registry r) = writeTVar r
+
+modifyReg :: MonadSTM m => Registry m -> (Reg m -> Reg m) -> STM m ()
+modifyReg (Registry r) = modifyTVar r
+
+type MonadRegistry m = (MonadSTM m, MonadFork m, MonadThrow m, MonadThrow (STM m))
+
+isAlive :: MonadRegistry m => Registry m -> ThreadId m -> m Bool
+isAlive registry tid =
+  elem tid . aliveThreads <$> atomically (readReg registry)
+
+setupRegistry :: forall m. MonadRegistry m => m (Registry m)
+setupRegistry = atomically $ Registry <$> newTVar @m emptyReg
+
+spawn :: MonadRegistry m => Registry m -> m () -> m (ThreadId m)
+spawn registry run = do
+  sync <- atomically newEmptyTMVar
+  let body = do
+        self <- myThreadId
+        atomically $ do
+          modifyReg registry $ modifyAlive (self :)
+          writeTMVar sync self
+        run
+      after _ = do
+        self <- myThreadId
+        atomically $ modifyReg registry $ modifyAlive $ List.delete self
+  forkFinally body after
+  atomically $ readTMVar sync
+
+whereis :: MonadRegistry m => Registry m -> String -> m (Maybe (ThreadId m))
 whereis registry name = do
   reg <- readRegistry registry
   return $ lookup name reg
 
-register :: Registry -> String -> ThreadId -> IO ()
+register :: MonadRegistry m => Registry m -> String -> ThreadId m -> m ()
 register registry name tid = do
-  ok <- isAlive tid
+  ok <- isAlive registry tid
   reg <- readRegistry registry
   if ok && name `notElem` map fst reg && tid `notElem` map snd reg
     then atomically $ do
-      reg' <- readTVar registry
+      reg' <- registered <$> readReg registry
       if name `notElem` map fst reg' && tid `notElem` map snd reg'
-        then writeTVar registry ((name, tid) : reg')
-        else error "badarg"
-    else error "badarg"
+        then modifyReg registry $ \reg -> reg{registered = (name, tid) : reg'}
+        else throwIO (ErrorCall "badarg")
+    else throwIO (ErrorCall "badarg")
 
-unregister :: Registry -> String -> IO ()
+unregister :: MonadRegistry m => Registry m -> String -> m ()
 unregister registry name = do
   reg <- readRegistry registry
   when (name `elem` map fst reg) $ do
-    atomically $ modifyTVar registry $ filter ((/= name) . fst)
+    atomically $ modifyReg registry $ modifyRegistered $ filter ((/= name) . fst)
 
-readRegistry :: Registry -> IO [(String, ThreadId)]
-readRegistry registry = garbageCollect registry *> atomically (readTVar registry)
+readRegistry :: MonadRegistry m => Registry m -> m [(String, ThreadId m)]
+readRegistry registry = garbageCollect registry *> atomically (registered <$> readReg registry)
 
-garbageCollect :: Registry -> IO ()
+garbageCollect :: forall m. MonadRegistry m => Registry m -> m ()
 garbageCollect registry = do
-  reg <- atomically $ readTVar registry
-  garbage <- filterM (fmap not . isAlive) (map snd reg)
-  atomically $ modifyTVar registry $ filter ((`notElem` garbage) . snd)
+  reg <- registered <$> atomically (readReg @m registry)
+  garbage <- filterM (fmap not . isAlive registry) (map snd reg)
+  atomically $ modifyReg registry $ modifyRegistered $ filter ((`notElem` garbage) . snd)
   return ()
diff --git a/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs b/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs
index 2ede548c..5c29b1e4 100644
--- a/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs
+++ b/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs
@@ -1,19 +1,28 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
 module Spec.DynamicLogic.RegistryModel where
 
-import Control.Concurrent
-import Control.Exception
+import Control.Concurrent.Class.MonadSTM
+import Control.Monad.Class.MonadFork
+import Control.Monad.Class.MonadTest
+import Control.Monad.Class.MonadThrow
+import Control.Monad.Class.MonadTimer
+import Control.Monad.IOSim
 
 import GHC.Generics
+import Unsafe.Coerce
 
 import Control.Monad.Reader
 import Data.Either
 import Data.List
 import Data.Map (Map)
 import Data.Map qualified as Map
-import Test.QuickCheck (Gen, Property)
-import Test.QuickCheck qualified as QC
+import Data.Typeable
+import Test.QuickCheck as QC hiding (Some)
+import Test.QuickCheck.Gen.Unsafe (Capture (..), capture)
 import Test.QuickCheck.Monadic hiding (assert)
-import Test.QuickCheck.Monadic qualified as QC
 import Test.Tasty hiding (after)
 
 import Test.Tasty.QuickCheck (testProperty)
@@ -21,29 +30,40 @@ import Test.Tasty.QuickCheck (testProperty)
 import Spec.DynamicLogic.Registry
 import Test.QuickCheck.DynamicLogic
 import Test.QuickCheck.Extras
+import Test.QuickCheck.ParallelActions
 import Test.QuickCheck.StateModel
 
-data RegState = RegState
-  { regs :: Map String (Var ThreadId)
-  , dead :: [Var ThreadId]
+type GoodMonad m =
+  ( Typeable (ThreadId m)
+  , Show (ThreadId m)
+  , MonadSTM m
+  , MonadFork m
+  , MonadDelay m
+  , MonadCatch m
+  , MonadThrow (STM m)
+  )
+
+data RegState m = RegState
+  { regs :: Map String (Var (ThreadId m))
+  , dead :: [Var (ThreadId m)]
   }
   deriving (Show, Generic)
 
-deriving instance Show (Action RegState a)
-deriving instance Eq (Action RegState a)
+deriving instance Show (Action (RegState m) a)
+deriving instance Eq (Action (RegState m) a)
 
-instance HasVariables (Action RegState a) where
+instance GoodMonad m => HasVariables (Action (RegState m) a) where
   getAllVariables (Register _ v) = getAllVariables v
   getAllVariables (KillThread v) = getAllVariables v
   getAllVariables _ = mempty
 
-instance StateModel RegState where
-  data Action RegState a where
-    Spawn :: Action RegState ThreadId
-    WhereIs :: String -> Action RegState (Maybe ThreadId)
-    Register :: String -> Var ThreadId -> Action RegState ()
-    Unregister :: String -> Action RegState ()
-    KillThread :: Var ThreadId -> Action RegState ()
+instance GoodMonad m => StateModel (RegState m) where
+  data Action (RegState m) a where
+    Spawn :: Action (RegState m) (ThreadId m)
+    WhereIs :: String -> Action (RegState m) (Maybe (ThreadId m))
+    Register :: String -> Var (ThreadId m) -> Action (RegState m) ()
+    Unregister :: String -> Action (RegState m) ()
+    KillThread :: Var (ThreadId m) -> Action (RegState m) ()
 
   precondition s (Register name tid) =
     name `Map.notMember` regs s
@@ -56,8 +76,8 @@ instance StateModel RegState where
   validFailingAction _ _ = True
 
   arbitraryAction ctx s =
-    let threadIdCtx = ctxAtType @ThreadId ctx
-     in QC.frequency $
+    let threadIdCtx = ctxAtType @(ThreadId m) ctx
+     in frequency $
           [
             ( max 1 $ 10 - length threadIdCtx
             , return $ Some Spawn
@@ -107,20 +127,21 @@ instance StateModel RegState where
       }
   nextState s WhereIs{} _ = s
 
-type RegM = ReaderT Registry IO
+type RegM m = ReaderT (Registry m) m
 
-instance RunModel RegState RegM where
-  type Error RegState RegM = SomeException
+instance GoodMonad m => RunModel (RegState m) (RegM m) where
+  type Error (RegState m) (RegM m) = String
 
   perform _ Spawn _ = do
-    tid <- lift $ forkIO (threadDelay 10000000)
+    reg <- ask
+    tid <- lift $ spawn reg (threadDelay 10000000)
     pure $ Right tid
   perform _ (Register name tid) env = do
     reg <- ask
-    lift $ try $ register reg name (env tid)
+    lift $ fmap (either (Left . displayException . toException @SomeException) Right) $ try $ register reg name (env tid)
   perform _ (Unregister name) _ = do
     reg <- ask
-    lift $ try $ unregister reg name
+    lift $ fmap (either (Left . displayException . toException @SomeException) Right) $ try $ unregister reg name
   perform _ (WhereIs name) _ = do
     reg <- ask
     res <- lift $ whereis reg name
@@ -136,30 +157,40 @@ instance RunModel RegState RegM where
 
   postconditionOnFailure (s, _) act@Register{} _ res = do
     monitorPost $
-      QC.tabulate
+      tabulate
         "Reason for -Register"
         [why s act]
     pure $ isLeft res
   postconditionOnFailure _s _ _ _ = pure True
 
   monitoring (_s, s') act@(showDictAction -> ShowDict) _ res =
-    QC.counterexample (show res ++ " <- " ++ show act ++ "\n  -- State: " ++ show s')
-      . QC.tabulate "Registry size" [show $ Map.size (regs s')]
+    counterexample (show res ++ " <- " ++ show act ++ "\n  -- State: " ++ show s')
+      . tabulate "Registry size" [show $ Map.size (regs s')]
+
+-- NOTE: We rely on the default implementation of `performPar` here because
+-- `perform` doesn't actually look at the state.
+instance GoodMonad m => RunModelPar (RegState m) (RegM m)
 
 data ShowDict a where
   ShowDict :: Show a => ShowDict a
 
-showDictAction :: forall a. Action RegState a -> ShowDict a
+showDictAction :: forall m a. GoodMonad m => Action (RegState m) a -> ShowDict a
 showDictAction Spawn{} = ShowDict
 showDictAction WhereIs{} = ShowDict
 showDictAction Register{} = ShowDict
 showDictAction Unregister{} = ShowDict
 showDictAction KillThread{} = ShowDict
 
-instance DynLogicModel RegState where
+instance GoodMonad m => DynLogicModel (RegState m) where
   restricted _ = False
 
-why :: RegState -> Action RegState a -> String
+instance Forking (IOSim s) where
+  forkThread io = do
+    t <- atomically newEmptyTMVar
+    forkIO $ io >>= atomically . putTMVar t
+    return $ atomically $ takeTMVar t
+
+why :: (RegState m) -> Action (RegState m) a -> String
 why s (Register name tid) =
   unwords $
     ["name already registered" | name `Map.member` regs s]
@@ -168,13 +199,13 @@ why s (Register name tid) =
 why _ _ = "(impossible)"
 
 arbitraryName :: Gen String
-arbitraryName = QC.elements allNames
+arbitraryName = elements allNames
 
-probablyRegistered :: RegState -> Gen String
-probablyRegistered s = QC.oneof $ map pure (Map.keys $ regs s) ++ [arbitraryName]
+probablyRegistered :: (RegState m) -> Gen String
+probablyRegistered s = oneof $ map pure (Map.keys $ regs s) ++ [arbitraryName]
 
-probablyUnregistered :: RegState -> Gen String
-probablyUnregistered s = QC.elements $ allNames ++ (allNames \\ Map.keys (regs s))
+probablyUnregistered :: (RegState m) -> Gen String
+probablyUnregistered s = elements $ allNames ++ (allNames \\ Map.keys (regs s))
 
 shrinkName :: String -> [String]
 shrinkName name = [n | n <- allNames, n < name]
@@ -182,20 +213,71 @@ shrinkName name = [n | n <- allNames, n < name]
 allNames :: [String]
 allNames = ["a", "b", "c", "d", "e"]
 
-prop_Registry :: Actions RegState -> Property
+prop_Registry :: Actions (RegState IO) -> Property
 prop_Registry s =
   monadicIO $ do
-    monitor $ QC.counterexample "\nExecution\n"
+    monitor $ counterexample "\nExecution\n"
     reg <- lift setupRegistry
     runPropertyReaderT (runActions s) reg
-    QC.assert True
+    return True
 
-propDL :: DL RegState () -> Property
+prop_parRegistry :: ParallelActions (RegState IO) -> Property
+prop_parRegistry as =
+  monadicIO $ do
+    reg <- lift setupRegistry
+    runPropertyReaderT (runParActions as) reg
+
+newtype IOSimActions = IOSimActions (forall s. ParallelActions (RegState (IOSim s)))
+
+instance Arbitrary IOSimActions where
+  arbitrary = do
+    Capture eval <- capture
+    pure $ IOSimActions (eval arbitrary)
+
+  shrink (IOSimActions acts) = [IOSimActions (unsafeCoerce acts) | acts <- shrink acts]
+
+instance Show IOSimActions where
+  show (IOSimActions acts) = show acts
+
+prop_parRegistryIOSim :: IOSimActions -> Property
+prop_parRegistryIOSim (IOSimActions as) = monadicIOSim_ prop
+  where
+    prop :: forall s. PropertyM (IOSim s) ()
+    prop = do
+      reg <- lift setupRegistry
+      runPropertyReaderT (runParActions $ as @s) reg
+      pure ()
+
+prop_parRegistryIOSimPor :: IOSimActions -> Property
+prop_parRegistryIOSimPor (IOSimActions as) =
+  monadicIOSimPOR_ prop
+  where
+    prop :: forall s. PropertyM (IOSim s) ()
+    prop = do
+      reg <- lift setupRegistry
+      lift exploreRaces
+      runPropertyReaderT (runParActions $ as @s) reg
+      pure ()
+
+-- NOTE: This is a hack to get around issues with old ghc versions
+data Exists where
+  Ex :: (forall s. IOSim s Property) -> Exists
+
+monadicIOSimPOR_ :: Testable a => (forall s. PropertyM (IOSim s) a) -> Property
+monadicIOSimPOR_ prop = forAllBlind prop' $ \(Ex p) -> exploreSimTrace id p $ \_ tr ->
+  either discard id $ traceResult False tr
+  where
+    prop' :: Gen Exists
+    prop' = do
+      Capture eval <- capture
+      pure $ Ex $ eval $ monadic' prop
+
+propDL :: DL (RegState IO) () -> Property
 propDL d = forAllDL d prop_Registry
 
 -- DL helpers
 
-unregisterNameAndTid :: String -> Var ThreadId -> DL RegState ()
+unregisterNameAndTid :: String -> Var (ThreadId m) -> DL (RegState m) ()
 unregisterNameAndTid name tid = do
   s <- getModelStateDL
   sequence_
@@ -204,7 +286,7 @@ unregisterNameAndTid name tid = do
     , name' == name || tid' == tid
     ]
 
-unregisterTid :: Var ThreadId -> DL RegState ()
+unregisterTid :: Var (ThreadId m) -> DL (RegState m) ()
 unregisterTid tid = do
   s <- getModelStateDL
   sequence_
@@ -213,50 +295,50 @@ unregisterTid tid = do
     , tid' == tid
     ]
 
-getAlive :: DL RegState [Var ThreadId]
+getAlive :: forall m. GoodMonad m => DL (RegState m) [Var (ThreadId m)]
 getAlive = do
   s <- getModelStateDL
   ctx <- getVarContextDL
-  pure $ ctxAtType @ThreadId ctx \\ dead s
+  pure $ ctxAtType @(ThreadId m) ctx \\ dead s
 
-pickThread :: DL RegState (Var ThreadId)
+pickThread :: forall m. GoodMonad m => DL (RegState m) (Var (ThreadId m))
 pickThread = do
-  tids <- ctxAtType @ThreadId <$> getVarContextDL
+  tids <- ctxAtType @(ThreadId m) <$> getVarContextDL
   forAllQ $ elementsQ tids
 
-pickAlive :: DL RegState (Var ThreadId)
+pickAlive :: GoodMonad m => DL (RegState m) (Var (ThreadId m))
 pickAlive = do
   alive <- getAlive
   forAllQ $ elementsQ alive
 
-pickFreshName :: DL RegState String
+pickFreshName :: DL (RegState m) String
 pickFreshName = do
   used <- Map.keys . regs <$> getModelStateDL
   forAllQ $ elementsQ (allNames \\ used)
 
 -- test that the registry never contains more than k processes
 
-regLimit :: Int -> DL RegState ()
+regLimit :: Int -> DL (RegState m) ()
 regLimit k = do
   anyActions_
   assertModel "Too many processes" $ \s -> Map.size (regs s) <= k
 
 -- test that we can register a pid that is not dead, if we unregister the name first.
 
-canRegisterAlive :: String -> DL RegState ()
+canRegisterAlive :: GoodMonad m => String -> DL (RegState m) ()
 canRegisterAlive name = do
   tid <- pickAlive
   unregisterNameAndTid name tid
   action $ Register name tid
   pure ()
 
-canRegister :: DL RegState ()
+canRegister :: GoodMonad m => DL (RegState m) ()
 canRegister = do
   anyActions_
   name <- pickFreshName
   canRegisterAlive name
 
-canRegisterNoUnregister :: DL RegState ()
+canRegisterNoUnregister :: GoodMonad m => DL (RegState m) ()
 canRegisterNoUnregister = do
   anyActions_
   name <- pickFreshName
@@ -269,7 +351,8 @@ tests =
   testGroup
     "registry model example"
     [ testProperty "prop_Registry" $ prop_Registry
-    , testProperty "moreActions 10 $ prop_Registry" $ moreActions 10 prop_Registry
+    , testProperty "moreActions 10 $ prop_Registry" $ moreActions 10 $ prop_Registry
     , testProperty "canRegister" $ propDL canRegister
-    , testProperty "canRegisterNoUnregister" $ QC.expectFailure $ propDL canRegisterNoUnregister
+    , testProperty "canRegisterNoUnregister" $ expectFailure $ propDL canRegisterNoUnregister
+    , testProperty "prop_parRegistryIOSimPor" $ expectFailure $ withMaxSuccess 1000 $ discardAfter 1000 $ prop_parRegistryIOSimPor
     ]
diff --git a/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs b/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs
index b3bd1097..aefd5d85 100644
--- a/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs
+++ b/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs
@@ -4,10 +4,9 @@
 module Test.QuickCheck.StateModelSpec where
 
 import Control.Monad.Reader (lift)
-import Data.IORef (newIORef)
 import Data.List (isInfixOf)
-import Spec.DynamicLogic.Counters (Counter (..), FailingCounter, SimpleCounter (..))
-import Test.QuickCheck (Property, Result (..), Testable, chatty, checkCoverage, choose, counterexample, cover, noShrinking, property, stdArgs)
+import Spec.DynamicLogic.Counters (FailingCounter, SimpleCounter (..), prop_counter, prop_counter_parIOSimPor, setupCounterState)
+import Test.QuickCheck
 import Test.QuickCheck.Extras (runPropertyReaderT)
 import Test.QuickCheck.Monadic (assert, monadicIO, monitor, pick)
 import Test.QuickCheck.StateModel (
@@ -43,6 +42,9 @@ tests =
     , testProperty
         "moreActions introduces long sequences of actions"
         prop_longSequences
+    , testProperty
+        "IOSimPor finds counterexample in parallel counters"
+        $ expectFailure prop_counter_parIOSimPor
     ]
 
 captureTerminal :: Testable p => p -> IO Result
@@ -50,23 +52,17 @@ captureTerminal p =
   withState stdArgs{chatty = False} $ \st ->
     test st (property p)
 
-prop_counter :: Actions Counter -> Property
-prop_counter as = monadicIO $ do
-  ref <- lift $ newIORef (0 :: Int)
-  runPropertyReaderT (runActions as) ref
-  assert True
-
 prop_returnsFinalState :: Actions SimpleCounter -> Property
 prop_returnsFinalState actions@(Actions as) =
   monadicIO $ do
-    ref <- lift $ newIORef (0 :: Int)
+    ref <- lift $ setupCounterState
     (s, _) <- runPropertyReaderT (runActions actions) ref
     assert $ count (underlyingState s) == length as
 
 prop_variablesIndicesAre1Based :: Actions SimpleCounter -> Property
 prop_variablesIndicesAre1Based actions@(Actions as) =
   noShrinking $ monadicIO $ do
-    ref <- lift $ newIORef (0 :: Int)
+    ref <- lift setupCounterState
     (_, env) <- runPropertyReaderT (runActions actions) ref
     act <- pick $ choose (0, length as - 1)
     monitor $
@@ -81,7 +77,7 @@ prop_variablesIndicesAre1Based actions@(Actions as) =
 prop_failsOnPostcondition :: Actions FailingCounter -> Property
 prop_failsOnPostcondition actions =
   monadicIO $ do
-    ref <- lift $ newIORef (0 :: Int)
+    ref <- lift setupCounterState
     runPropertyReaderT (runActions actions) ref
     assert True