dejafu 1.3.2.0 → 1.4.0.0

raw patch · 14 files changed

+1032/−869 lines, 14 filesdep −ref-fdPVP ok

version bump matches the API change (PVP)

Dependencies removed: ref-fd

API changes (from Hackage documentation)

Files

• CHANGELOG.rst +29/−0
• Test/DejaFu.hs +26/−28
• Test/DejaFu/Conc.hs +47/−60
• Test/DejaFu/Conc/Internal.hs +533/−394
• Test/DejaFu/Conc/Internal/Common.hs +78/−98
• Test/DejaFu/Conc/Internal/Memory.hs +112/−86
• Test/DejaFu/Conc/Internal/STM.hs +67/−65
• Test/DejaFu/Conc/Internal/Threading.hs +30/−28
• Test/DejaFu/Internal.hs +60/−57
• Test/DejaFu/SCT.hs +36/−37
• Test/DejaFu/SCT/Internal.hs +5/−6
• Test/DejaFu/SCT/Internal/DPOR.hs +6/−3
• Test/DejaFu/Types.hs +1/−4
• dejafu.cabal +2/−3

@@ -7,6 +7,35 @@ .. _PVP: https://pvp.haskell.org/  +1.4.0.0 (2018-03-17)+--------------------++* Git: :tag:`dejafu-1.4.0.0`+* Hackage: :hackage:`dejafu-1.4.0.0`++Changed+~~~~~~~++- (:issue:`201`) ``Test.DejaFu.Conc.ConcT r n a`` drops its ``r``+  parameter, becoming ``ConcT n a``.++- (:issue:`201`) All functions drop the ``MonadConc`` constraint.++Removed+~~~~~~~++- (:issue:`201`) The ``MonadRef`` and ``MonadAtomicRef`` instances for+  ``Test.DejaFu.Conc.ConcT``.++- (:issue:`198`) The ``Test.DejaFu.Types.Killed`` thread action, which+  was unused.++Fixed+~~~~~++- (:issue:`250`) Add missing dependency for ``throwTo`` actions.++ 1.3.2.0 (2018-03-12) -------------------- 

@@ -1,5 +1,4 @@ {-# LANGUAGE LambdaCase #-}-{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TupleSections #-}  {- |@@ -273,7 +272,6 @@ import           Control.Monad            (unless, when) import           Control.Monad.Conc.Class (MonadConc) import           Control.Monad.IO.Class   (MonadIO(..))-import           Control.Monad.Ref        (MonadRef) import           Data.Function            (on) import           Data.List                (intercalate, intersperse) import           Data.Maybe               (catMaybes, isJust, isNothing,@@ -329,8 +327,8 @@ -- False -- -- @since 1.0.0.0-autocheck :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a)-  => ConcT r n a+autocheck :: (MonadConc n, MonadIO n, Eq a, Show a)+  => ConcT n a   -- ^ The computation to test.   -> n Bool autocheck = autocheckWithSettings defaultSettings@@ -363,12 +361,12 @@ -- False -- -- @since 1.0.0.0-autocheckWay :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a)+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 @CRef@ operations.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to test.   -> n Bool autocheckWay way = autocheckWithSettings . fromWayAndMemType way@@ -400,10 +398,10 @@ -- False -- -- @since 1.2.0.0-autocheckWithSettings :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a)+autocheckWithSettings :: (MonadConc n, MonadIO n, Eq a, Show a)   => Settings n a   -- ^ The SCT settings.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to test.   -> n Bool autocheckWithSettings settings = dejafusWithSettings settings@@ -427,12 +425,12 @@ -- False -- -- @since 1.0.0.0-dejafu :: (MonadConc n, MonadIO n, MonadRef r n, Show b)+dejafu :: (MonadConc n, MonadIO n, Show b)   => String   -- ^ The name of the test.   -> ProPredicate a b   -- ^ The predicate to check.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to test.   -> n Bool dejafu = dejafuWithSettings defaultSettings@@ -457,7 +455,7 @@ -- False -- -- @since 1.0.0.0-dejafuWay :: (MonadConc n, MonadIO n, MonadRef r n, Show b)+dejafuWay :: (MonadConc n, MonadIO n, Show b)   => Way   -- ^ How to run the concurrent program.   -> MemType@@ -466,7 +464,7 @@   -- ^ The name of the test.   -> ProPredicate a b   -- ^ The predicate to check.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to test.   -> n Bool dejafuWay way = dejafuWithSettings . fromWayAndMemType way@@ -483,14 +481,14 @@ -- False -- -- @since 1.2.0.0-dejafuWithSettings :: (MonadConc n, MonadIO n, MonadRef r n, Show b)+dejafuWithSettings :: (MonadConc n, MonadIO n, Show b)   => Settings n a   -- ^ The SCT settings.   -> String   -- ^ The name of the test.   -> ProPredicate a b   -- ^ The predicate to check.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to test.   -> n Bool dejafuWithSettings settings name test =@@ -506,7 +504,7 @@ -- False -- -- @since 1.0.0.0-dejafuDiscard :: (MonadConc n, MonadIO n, MonadRef r n, Show b)+dejafuDiscard :: (MonadConc n, MonadIO n, Show b)   => (Either Failure a -> Maybe Discard)   -- ^ Selectively discard results.   -> Way@@ -517,7 +515,7 @@   -- ^ The name of the test.   -> ProPredicate a b   -- ^ The predicate to check.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to test.   -> n Bool dejafuDiscard discard way =@@ -536,10 +534,10 @@ -- False -- -- @since 1.0.0.0-dejafus :: (MonadConc n, MonadIO n, MonadRef r n, Show b)+dejafus :: (MonadConc n, MonadIO n, Show b)   => [(String, ProPredicate a b)]   -- ^ The list of predicates (with names) to check.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to test.   -> n Bool dejafus = dejafusWithSettings defaultSettings@@ -558,14 +556,14 @@ -- False -- -- @since 1.0.0.0-dejafusWay :: (MonadConc n, MonadIO n, MonadRef r n, Show b)+dejafusWay :: (MonadConc n, MonadIO n, Show b)   => Way   -- ^ How to run the concurrent program.   -> MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.   -> [(String, ProPredicate a b)]   -- ^ The list of predicates (with names) to check.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to test.   -> n Bool dejafusWay way = dejafusWithSettings . fromWayAndMemType way@@ -583,12 +581,12 @@ -- False -- -- @since 1.2.0.0-dejafusWithSettings :: (MonadConc n, MonadIO n, MonadRef r n, Show b)+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 r n a+  -> ConcT n a   -- ^ The computation to test.   -> n Bool dejafusWithSettings settings tests conc = do@@ -659,10 +657,10 @@ -- affect which failing traces are reported, when there is a failure. -- -- @since 1.0.0.0-runTest :: (MonadConc n, MonadRef r n)+runTest :: MonadConc n   => ProPredicate a b   -- ^ The predicate to check-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to test   -> n (Result b) runTest = runTestWithSettings defaultSettings@@ -675,14 +673,14 @@ -- affect which failing traces are reported, when there is a failure. -- -- @since 1.0.0.0-runTestWay :: (MonadConc n, MonadRef r n)+runTestWay :: MonadConc n   => Way   -- ^ How to run the concurrent program.   -> MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.   -> ProPredicate a b   -- ^ The predicate to check-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to test   -> n (Result b) runTestWay way = runTestWithSettings . fromWayAndMemType way@@ -694,12 +692,12 @@ -- affect which failing traces are reported, when there is a failure. -- -- @since 1.2.0.0-runTestWithSettings :: (MonadConc n, MonadRef r n)+runTestWithSettings :: MonadConc n   => Settings n a   -- ^ The SCT settings.   -> ProPredicate a b   -- ^ The predicate to check-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to test   -> n (Result b) runTestWithSettings settings p conc =

@@ -1,7 +1,6 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} @@ -11,7 +10,7 @@ -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : CPP, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, TypeFamilies+-- Portability : CPP, FlexibleInstances, GeneralizedNewtypeDeriving, TypeFamilies -- -- Deterministic traced execution of concurrent computations. --@@ -59,11 +58,8 @@ import           Control.Exception                   (MaskingState(..)) import qualified Control.Monad.Catch                 as Ca import qualified Control.Monad.IO.Class              as IO-import           Control.Monad.Ref                   (MonadRef)-import qualified Control.Monad.Ref                   as Re import           Control.Monad.Trans.Class           (MonadTrans(..)) import qualified Data.Foldable                       as F-import           Data.IORef                          (IORef) import           Data.List                           (partition) import qualified Data.Map.Strict                     as M import           Data.Maybe                          (isNothing)@@ -72,9 +68,8 @@ 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-import           Test.DejaFu.Conc.Internal.Threading (Thread(_blocking),-                                                      Threads)+import           Test.DejaFu.Conc.Internal.STM       (ModelSTM)+import           Test.DejaFu.Conc.Internal.Threading (_blocking) import           Test.DejaFu.Internal import           Test.DejaFu.Types import           Test.DejaFu.Utils@@ -83,52 +78,40 @@ import qualified Control.Monad.Fail                  as Fail #endif --- | @since 0.6.0.0-newtype ConcT r n a = C { unC :: M n r a } deriving (Functor, Applicative, Monad)+-- | @since 1.4.0.0+newtype ConcT n a = C { unC :: ModelConc n a }+  deriving (Functor, Applicative, Monad)  #if MIN_VERSION_base(4,9,0)--- | @since 0.9.1.0-instance Fail.MonadFail (ConcT r n) where+instance Fail.MonadFail (ConcT n) where   fail = C . fail #endif  -- | A 'MonadConc' implementation using @IO@. -- -- @since 0.4.0.0-type ConcIO = ConcT IORef IO+type ConcIO = ConcT IO -toConc :: ((a -> Action n r) -> Action n r) -> ConcT r n a-toConc = C . cont+toConc :: ((a -> Action n) -> Action n) -> ConcT n a+toConc = C . ModelConc -wrap :: (M n r a -> M n r a) -> ConcT r n a -> ConcT r n a+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 r n) where+instance IO.MonadIO n => IO.MonadIO (ConcT n) where   liftIO ma = toConc (\c -> ALift (fmap c (IO.liftIO ma))) -instance Re.MonadRef (CRef r) (ConcT r n) where-  newRef a = toConc (ANewCRef "" a)--  readRef ref = toConc (AReadCRef ref)--  writeRef ref a = toConc (\c -> AWriteCRef ref a (c ()))--  modifyRef ref f = toConc (AModCRef ref (\a -> (f a, ())))--instance Re.MonadAtomicRef (CRef r) (ConcT r n) where-  atomicModifyRef ref f = toConc (AModCRef ref f)--instance MonadTrans (ConcT r) where+instance MonadTrans ConcT where   lift ma = toConc (\c -> ALift (fmap c ma)) -instance Ca.MonadCatch (ConcT r n) where+instance Ca.MonadCatch (ConcT n) where   catch ma h = toConc (ACatching (unC . h) (unC ma)) -instance Ca.MonadThrow (ConcT r n) where+instance Ca.MonadThrow (ConcT n) where   throwM e = toConc (\_ -> AThrow e) -instance Ca.MonadMask (ConcT r n) where+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)) @@ -147,16 +130,16 @@     pure result #endif -instance Monad n => C.MonadConc (ConcT r n) where-  type MVar     (ConcT r n) = MVar r-  type CRef     (ConcT r n) = CRef r-  type Ticket   (ConcT r n) = Ticket-  type STM      (ConcT r n) = S n r-  type ThreadId (ConcT r n) = ThreadId+instance Monad n => C.MonadConc (ConcT n) where+  type MVar     (ConcT n) = ModelMVar n+  type CRef     (ConcT n) = ModelCRef n+  type Ticket   (ConcT n) = ModelTicket+  type STM      (ConcT n) = ModelSTM n+  type ThreadId (ConcT n) = ThreadId    -- ---------- -  forkWithUnmaskN   n ma = toConc (AFork   n (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop (pure ()))))+  forkWithUnmaskN   n ma = toConc (AFork n (\umask -> runModelConc (unC $ ma $ wrap umask) (\_ -> AStop (pure ()))))   forkOnWithUnmaskN n _  = C.forkWithUnmaskN n   forkOSN n ma = forkOSWithUnmaskN n (const ma) @@ -180,7 +163,7 @@   readCRef   ref = toConc (AReadCRef    ref)   readForCAS ref = toConc (AReadCRefCas ref) -  peekTicket' _ = _ticketVal+  peekTicket' _ = ticketVal    writeCRef ref      a = toConc (\c -> AWriteCRef ref a (c ()))   casCRef   ref tick a = toConc (ACasCRef ref tick a)@@ -209,9 +192,13 @@   atomically = toConc . AAtom  -- move this into the instance defn when forkOSWithUnmaskN is added to MonadConc in 2018-forkOSWithUnmaskN :: Applicative n => String -> ((forall a. ConcT r n a -> ConcT r n a) -> ConcT r n ()) -> ConcT r n ThreadId+forkOSWithUnmaskN :: Applicative n+  => String+  -> ((forall a. ConcT n a -> ConcT n a) -> ConcT n ())+  -> ConcT n ThreadId forkOSWithUnmaskN n ma-  | C.rtsSupportsBoundThreads = toConc (AForkOS n (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop (pure ()))))+  | 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)"  -- | Run a concurrent computation with a given 'Scheduler' and initial@@ -238,15 +225,15 @@ -- be halted. -- -- @since 1.0.0.0-runConcurrent :: (C.MonadConc n, MonadRef r n)+runConcurrent :: C.MonadConc n   => Scheduler s   -> MemType   -> s-  -> ConcT r n a+  -> ConcT n a   -> n (Either Failure a, s, Trace) runConcurrent sched memtype s ma = do   res <- runConcurrency False sched memtype s initialIdSource 2 (unC ma)-  out <- efromJust "runConcurrent" <$> Re.readRef (finalRef res)+  out <- efromJust "runConcurrent" <$> C.readCRef (finalRef res)   pure ( out        , cSchedState (finalContext res)        , F.toList (finalTrace res)@@ -262,7 +249,7 @@ -- a failing computation. -- -- @since 0.6.0.0-subconcurrency :: ConcT r n a -> ConcT r n (Either Failure a)+subconcurrency :: ConcT n a -> ConcT n (Either Failure a) subconcurrency ma = toConc (ASub (unC ma))  -- | Run an arbitrary action which gets some special treatment:@@ -300,9 +287,9 @@ dontCheck   :: Maybe Int   -- ^ An optional length bound.-  -> ConcT r n a+  -> ConcT n a   -- ^ The action to execute.-  -> ConcT r n a+  -> ConcT n a dontCheck lb ma = toConc (ADontCheck lb (unC ma))  -------------------------------------------------------------------------------@@ -339,7 +326,7 @@ -- 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+-- of @liftIO . readCRef@ and @liftIO . writeIORef@ here), or reset -- the state to a known value.  Both of these approaches will work: -- -- @@@ -372,12 +359,12 @@ -- needing to call this function yourself. -- -- @since 1.1.0.0-runForDCSnapshot :: (C.MonadConc n, MonadRef r n)-  => ConcT r n a-  -> n (Maybe (Either Failure (DCSnapshot r n a), Trace))+runForDCSnapshot :: C.MonadConc n+  => ConcT n a+  -> n (Maybe (Either Failure (DCSnapshot n a), Trace)) runForDCSnapshot ma = do   res <- runConcurrency True roundRobinSchedNP SequentialConsistency () initialIdSource 2 (unC ma)-  out <- Re.readRef (finalRef res)+  out <- C.readCRef (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))@@ -391,18 +378,18 @@ -- needing to call this function yourself. -- -- @since 1.1.0.0-runWithDCSnapshot :: (C.MonadConc n, MonadRef r n)+runWithDCSnapshot :: C.MonadConc n   => Scheduler s   -> MemType   -> s-  -> DCSnapshot r n a+  -> DCSnapshot n a   -> n (Either Failure 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 "runWithDCSnapshot" <$> Re.readRef (finalRef res)+  out <- efromJust "runWithDCSnapshot" <$> C.readCRef (finalRef res)   pure ( out        , cSchedState (finalContext res)        , F.toList (finalTrace res)@@ -411,14 +398,14 @@ -- | Check if a 'DCSnapshot' can be taken from this computation. -- -- @since 1.1.0.0-canDCSnapshot :: ConcT r n a -> Bool-canDCSnapshot (C (M k)) = lookahead (k undefined) == WillDontCheck+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. -- -- @since 1.1.0.0-threadsFromDCSnapshot :: DCSnapshot r n a -> ([ThreadId], [ThreadId])+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)

@@ -1,6 +1,6 @@-{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE MultiWayIf #-} {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE RecordWildCards #-}  -- | -- Module      : Test.DejaFu.Conc.Internal@@ -8,19 +8,17 @@ -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : MultiParamTypeClasses, RankNTypes, ScopedTypeVariables+-- Portability : MultiWayIf, RankNTypes, RecordWildCards -- -- Concurrent monads with a fixed scheduler: internal types and -- functions. This module is NOT considered to form part of the public -- interface of this library. module Test.DejaFu.Conc.Internal where -import           Control.Exception                   (MaskingState(..),+import           Control.Exception                   (Exception,+                                                      MaskingState(..),                                                       toException)-import           Control.Monad.Conc.Class            (MonadConc,-                                                      rtsSupportsBoundThreads)-import           Control.Monad.Ref                   (MonadRef, newRef, readRef,-                                                      writeRef)+import qualified Control.Monad.Conc.Class            as C import           Data.Foldable                       (foldrM, toList) import           Data.Functor                        (void) import           Data.List                           (sortOn)@@ -40,17 +38,17 @@ import           Test.DejaFu.Types  ----------------------------------------------------------------------------------- * Execution+-- * Set-up  -- | 'Trace' but as a sequence. type SeqTrace   = Seq (Decision, [(ThreadId, Lookahead)], ThreadAction)  -- | The result of running a concurrent program.-data CResult n r g a = CResult-  { finalContext :: Context n r g-  , finalRef :: r (Maybe (Either Failure a))-  , finalRestore :: Maybe (Threads n r -> n ())+data CResult n g a = CResult+  { finalContext :: Context n g+  , finalRef :: C.CRef n (Maybe (Either Failure a))+  , finalRestore :: Maybe (Threads n -> n ())   -- ^ Meaningless if this result doesn't come from a snapshotting   -- execution.   , finalTrace :: SeqTrace@@ -60,29 +58,29 @@ -- | A snapshot of the concurrency state immediately after 'dontCheck' -- finishes. ----- @since 1.1.0.0-data DCSnapshot r n a = DCSnapshot-  { dcsContext :: Context n r ()+-- @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 r -> n ()+  , dcsRestore :: Threads n -> n ()   -- ^ Action to restore CRef, MVar, and TVar values.-  , dcsRef :: r (Maybe (Either Failure a))+  , dcsRef :: C.CRef n (Maybe (Either Failure a))   -- ^ Reference where the result will be written.   }  -- | Run a concurrent computation with a given 'Scheduler' and initial -- state, returning a failure reason on error. Also returned is the -- final state of the scheduler, and an execution trace.-runConcurrency :: (MonadConc n, MonadRef r n)+runConcurrency :: C.MonadConc n   => Bool   -> Scheduler g   -> MemType   -> g   -> IdSource   -> Int-  -> M n r a-  -> n (CResult n r g a)+  -> ModelConc n a+  -> n (CResult n g a) runConcurrency forSnapshot sched memtype g idsrc caps ma = do   let ctx = Context { cSchedState = g                     , cIdSource   = idsrc@@ -94,94 +92,102 @@   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+  => 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 }+ -- | Like 'runConcurrency' but starts from a snapshot.-runConcurrencyWithSnapshot :: (MonadConc n, MonadRef r n)+runConcurrencyWithSnapshot :: C.MonadConc n   => Scheduler g   -> MemType-  -> Context n r g-  -> (Threads n r -> n ())-  -> r (Maybe (Either Failure a))-  -> n (CResult n r g a)+  -> Context n g+  -> (Threads n -> n ())+  -> C.CRef n (Maybe (Either Failure 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)-  let ctx' = ctx { cThreads = threads }-  restore (cThreads ctx')-  res <- runConcurrency'' False sched memtype ref ctx { cThreads = threads}+  restore threads+  res <- runThreads False sched memtype ref ctx { cThreads = threads }   killAllThreads (finalContext res)   pure res  -- | Kill the remaining threads-killAllThreads :: MonadConc n => Context n r g -> n ()+killAllThreads :: C.MonadConc n => Context n g -> n () killAllThreads ctx =   let finalThreads = cThreads ctx   in mapM_ (`kill` finalThreads) (M.keys finalThreads) --- | Run a concurrent program using the given context, and without--- killing threads which remain at the end.  The context must have no--- main thread.-runConcurrency' :: (MonadConc n, MonadRef r n)-  => Bool-  -> Scheduler g-  -> MemType-  -> Context n r g-  -> M n r a-  -> n (CResult n r g a)-runConcurrency' forSnapshot sched memtype ctx ma = do-  (c, ref) <- runRefCont AStop (Just . Right) (runM ma)-  let threads0 = launch' Unmasked initialThread (const c) (cThreads ctx)-  threads <- (if rtsSupportsBoundThreads then makeBound initialThread else pure) threads0-  runConcurrency'' forSnapshot sched memtype ref ctx { cThreads = threads}---- | Like 'runConcurrency'' but doesn't do *ANY* set up at all.-runConcurrency'' :: (MonadConc n, MonadRef r n)-  => Bool-  -> Scheduler g-  -> MemType-  -> r (Maybe (Either Failure a))-  -> Context n r g-  -> n (CResult n r g a)-runConcurrency'' forSnapshot sched memtype ref ctx = do-  (finalCtx, trace, finalD, restore) <- runThreads forSnapshot sched memtype ref ctx-  pure CResult-    { finalContext = finalCtx-    , finalRef = ref-    , finalRestore = restore-    , finalTrace = trace-    , finalDecision = finalD-    }+-------------------------------------------------------------------------------+-- * Execution  -- | The context a collection of threads are running in.-data Context n r g = Context+data Context n g = Context   { cSchedState :: g   , cIdSource   :: IdSource-  , cThreads    :: Threads n r-  , cWriteBuf   :: WriteBuffer r+  , cThreads    :: Threads n+  , cWriteBuf   :: WriteBuffer n   , cCaps       :: Int   }  -- | Run a collection of threads, until there are no threads left.-runThreads :: (MonadConc n, MonadRef r n)+runThreads :: C.MonadConc n   => Bool   -> Scheduler g   -> MemType-  -> r (Maybe (Either Failure a))-  -> Context n r g-  -> n (Context n r g, SeqTrace, Maybe (ThreadId, ThreadAction), Maybe (Threads n r -> n ()))-runThreads forSnapshot sched memtype ref = go (const $ pure ()) Seq.empty Nothing where-  go restore sofar prior ctx+  -> C.CRef n (Maybe (Either Failure a))+  -> Context n g+  -> n (CResult n g a)+runThreads forSnapshot sched memtype ref = schedule (const $ pure ()) Seq.empty Nothing where+  -- signal failure & terminate+  die reason finalR finalT finalD finalC = do+    C.writeCRef ref (Just $ Left reason)+    stop finalR finalT finalD finalC++  -- just terminate; 'ref' must have been written to before calling+  -- this+  stop finalR finalT finalD finalC = pure CResult+    { finalContext  = finalC+    , finalRef      = ref+    , finalRestore  = if forSnapshot then Just finalR else Nothing+    , finalTrace    = finalT+    , finalDecision = finalD+    }++  -- check for termination, pick a thread, and call 'step'+  schedule restore sofar prior ctx     | isTerminated  = stop restore sofar prior ctx-    | isDeadlocked  = die restore sofar prior Deadlock ctx-    | isSTMLocked   = die restore sofar prior STMDeadlock 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            Just chosen -> case M.lookup chosen threadsc of              Just thread-               | isBlocked thread -> die restore sofar prior InternalError ctx'-               | otherwise -> step chosen thread ctx'-             Nothing -> die restore sofar prior InternalError ctx'-           Nothing -> die restore sofar prior Abort ctx'+               | isBlocked thread -> die InternalError restore sofar prior ctx'+               | otherwise ->+                 let decision+                       | Just chosen == (fst <$> prior) = Continue+                       | (fst <$> prior) `notElem` map (Just . fst) runnable' = Start chosen+                       | otherwise = SwitchTo chosen+                     alternatives = filter (\(t, _) -> t /= chosen) runnable'+                 in step decision alternatives chosen thread restore sofar prior ctx'+             Nothing -> die InternalError restore sofar prior ctx'+           Nothing -> die Abort restore sofar prior ctx'     where       (choice, g')  = scheduleThread sched prior (efromList "runThreads" runnable') (cSchedState ctx)       runnable'     = [(t, lookahead (_continuation a)) | (t, a) <- sortOn fst $ M.assocs runnable]@@ -197,59 +203,57 @@       isSTMLocked = M.null (M.filter (not . isBlocked) threads) &&         ((~=  OnTVar []) <$> M.lookup initialThread threads) == Just True -      unblockWaitingOn tid = fmap unblock where-        unblock thrd = case _blocking thrd of-          Just (OnMask t) | t == tid -> thrd { _blocking = Nothing }-          _ -> thrd--      die restore' sofar' finalD reason finalCtx = do-        writeRef ref (Just $ Left reason)-        stop restore' sofar' finalD finalCtx--      stop restore' sofar' finalD finalCtx =-        pure (finalCtx, sofar', finalD, if forSnapshot then Just restore' else Nothing)--      step chosen thread ctx' = do-          (res, actOrTrc, actionSnap) <- stepThread-              forSnapshot-              (isNothing prior)-              sched-              memtype-              chosen-              (_continuation thread)-              ctx { cSchedState = g' }-          let trc    = getTrc actOrTrc-          let sofar' = sofar <> trc-          let prior' = getPrior actOrTrc-          let restore' threads' =-                if forSnapshot-                then restore threads' >> actionSnap threads'-                else restore threads'-          case res of-            Succeeded ctx'' ->-              let threads' = if (interruptible <$> M.lookup chosen (cThreads ctx'')) /= Just False-                             then unblockWaitingOn chosen (cThreads ctx'')-                             else cThreads ctx''-                  ctx''' = ctx'' { cThreads = delCommitThreads threads' }-              in go restore' sofar' prior' ctx'''-            Failed failure ->-              let ctx'' = ctx' { cThreads = delCommitThreads threads }-              in die restore' sofar' prior' failure ctx''-            Snap ctx'' ->-              stop actionSnap sofar' prior' ctx''-        where-          decision-            | Just chosen == (fst <$> prior) = Continue-            | (fst <$> prior) `notElem` map (Just . fst) runnable' = Start chosen-            | otherwise = SwitchTo chosen+  -- run the chosen thread for one step and then pass control back to+  -- 'schedule'+  step decision alternatives chosen thread restore sofar prior ctx = do+      (res, actOrTrc, actionSnap) <- stepThread+          forSnapshot+          (isNothing prior)+          sched+          memtype+          chosen+          (_continuation thread)+          ctx+      let sofar' = sofar <> getTrc actOrTrc+      let prior' = getPrior actOrTrc+      let restore' threads' =+            if forSnapshot+            then restore threads' >> actionSnap threads'+            else restore threads'+      let ctx' = fixContext chosen res ctx+      case res of+        Succeeded _ ->+          schedule 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 (Single a) = Seq.singleton (decision, alternatives, a)-          getTrc (SubC as _) = (decision, alternatives, Subconcurrency) <| as+      getPrior (Single a) = Just (chosen, a)+      getPrior (SubC _ finalD) = finalD -          alternatives = filter (\(t, _) -> t /= chosen) runnable'+-- | 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 _ (Failed _) ctx@Context{..} =+  ctx { cThreads = delCommitThreads cThreads }+fixContext _ (Snap ctx@Context{..}) _ =+  ctx { cThreads = delCommitThreads cThreads } -          getPrior (Single a) = Just (chosen, a)-          getPrior (SubC _ finalD) = finalD+-- | @unblockWaitingOn tid@ unblocks every thread blocked in a+-- @throwTo tid@.+unblockWaitingOn :: ThreadId -> Threads n -> Threads n+unblockWaitingOn tid = fmap $ \thread -> case _blocking thread of+  Just (OnMask t) | t == tid -> thread { _blocking = Nothing }+  _ -> thread  -------------------------------------------------------------------------------- -- * Single-step execution@@ -263,20 +267,24 @@   deriving (Eq, Show)  -- | What a thread did, for execution purposes.-data What n r g-  = Succeeded (Context n r g)+data What n g+  = Succeeded (Context n g)   -- ^ Action succeeded: continue execution.   | Failed Failure   -- ^ Action caused computation to fail: stop.-  | Snap (Context n r g)+  | 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'. --+-- Each case looks very similar.  This is deliberate, so that the+-- essential differences between actions are more apparent, and not+-- hidden by accidental differences in how things are expressed.+-- -- Note: the returned snapshot action will definitely not do the right -- thing with relaxed memory.-stepThread :: forall n r g. (MonadConc n, MonadRef r n)+stepThread :: C.MonadConc n   => Bool   -- ^ Should we record a snapshot?   -> Bool@@ -287,309 +295,440 @@   -- ^ The memory model to use.   -> ThreadId   -- ^ ID of the current thread-  -> Action n r+  -> Action n   -- ^ Action to step-  -> Context n r g+  -> Context n g   -- ^ The execution context.-  -> n (What n r g, Act, Threads n r -> n ())-stepThread forSnapshot isFirst sched memtype tid action ctx = case action of-    -- start a new thread, assigning it the next 'ThreadId'-    AFork n a b -> pure $-      let threads' = launch tid newtid a (cThreads ctx)-          (idSource', newtid) = nextTId n (cIdSource ctx)-      in (Succeeded ctx { cThreads = goto (b newtid) tid threads', cIdSource = idSource' }, Single (Fork newtid), noSnap)--    -- start a new bound thread, assigning it the next 'ThreadId'-    AForkOS n a b -> do-      let (idSource', newtid) = nextTId n (cIdSource ctx)-      let threads' = launch tid newtid a (cThreads ctx)-      threads'' <- makeBound newtid threads'-      pure (Succeeded ctx { cThreads = goto (b newtid) tid threads'', cIdSource = idSource' }, Single (ForkOS newtid), noSnap)+  -> n (What n g, Act, 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)+     , const (pure ())+     ) -    -- check if the current thread is bound-    AIsBound c ->-      let isBound = isJust . _bound $ elookup "stepThread.AIsBound" tid (cThreads ctx)-      in simple (goto (c isBound) tid (cThreads ctx)) (IsCurrentThreadBound isBound) noSnap+-- start a new bound thread, assigning it the next 'ThreadId'+stepThread _ _ _ _ tid (AForkOS n a b) = \ctx@Context{..} -> do+  let (idSource', newtid) = nextTId n cIdSource+  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)+       , const (pure ())+       ) -    -- get the 'ThreadId' of the current thread-    AMyTId c -> simple (goto (c tid) tid (cThreads ctx)) MyThreadId noSnap+-- check if the current thread is bound+stepThread _ _ _ _ tid (AIsBound c) = \ctx@Context{..} -> do+  let isBound = isJust . _bound $ elookup "stepThread.AIsBound" tid cThreads+  pure ( Succeeded ctx { cThreads = goto (c isBound) tid cThreads }+       , Single (IsCurrentThreadBound isBound)+       , const (pure ())+       ) -    -- get the number of capabilities-    AGetNumCapabilities c -> simple (goto (c (cCaps ctx)) tid (cThreads ctx)) (GetNumCapabilities $ cCaps ctx) noSnap+-- get the 'ThreadId' of the current thread+stepThread _ _ _ _ tid (AMyTId c) = \ctx@Context{..} ->+  pure ( Succeeded ctx { cThreads = goto (c tid) tid cThreads }+       , Single MyThreadId+       , const (pure ())+       ) -    -- set the number of capabilities-    ASetNumCapabilities i c -> pure-      (Succeeded ctx { cThreads = goto c tid (cThreads ctx), cCaps = i }, Single (SetNumCapabilities i), noSnap)+-- get the number of capabilities+stepThread _ _ _ _ tid (AGetNumCapabilities c) = \ctx@Context{..} ->+  pure ( Succeeded ctx { cThreads = goto (c cCaps) tid cThreads }+       , Single (GetNumCapabilities cCaps)+       , const (pure ())+       ) -    -- yield the current thread-    AYield c -> simple (goto c tid (cThreads ctx)) Yield noSnap+-- 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)+       , const (pure ())+       ) -    -- yield the current thread (delay is ignored)-    ADelay n c -> simple (goto c tid (cThreads ctx)) (ThreadDelay n) noSnap+-- yield the current thread+stepThread _ _ _ _ tid (AYield c) = \ctx@Context{..} ->+  pure ( Succeeded ctx { cThreads = goto c tid cThreads }+       , Single Yield+       , const (pure ())+       ) -    -- create a new @MVar@, using the next 'MVarId'.-    ANewMVar n c -> do-      let (idSource', newmvid) = nextMVId n (cIdSource ctx)-      ref <- newRef Nothing-      let mvar = MVar newmvid ref-      pure ( Succeeded ctx { cThreads = goto (c mvar) tid (cThreads ctx), cIdSource = idSource' }-           , Single (NewMVar newmvid)-           , const (writeRef ref Nothing)-           )+-- 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)+       , const (pure ())+       ) -    -- put a value into a @MVar@, blocking the thread until it's empty.-    APutMVar cvar@(MVar cvid _) a c -> synchronised $ do-      (success, threads', woken, effect) <- putIntoMVar cvar a c tid (cThreads ctx)-      simple threads' (if success then PutMVar cvid woken else BlockedPutMVar cvid) (const effect)+-- create a new @MVar@, using the next 'MVarId'.+stepThread _ _ _ _ tid (ANewMVar n c) = \ctx@Context{..} -> do+  let (idSource', newmvid) = nextMVId n cIdSource+  ref <- C.newCRef Nothing+  let mvar = ModelMVar newmvid ref+  pure ( Succeeded ctx { cThreads = goto (c mvar) tid cThreads, cIdSource = idSource' }+       , Single (NewMVar newmvid)+       , const (C.writeCRef ref Nothing)+       ) -    -- try to put a value into a @MVar@, without blocking.-    ATryPutMVar cvar@(MVar cvid _) a c -> synchronised $ do-      (success, threads', woken, effect) <- tryPutIntoMVar cvar a c tid (cThreads ctx)-      simple threads' (TryPutMVar cvid success woken) (const effect)+-- put a value into a @MVar@, blocking the thread until it's empty.+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)+       , const effect+       ) -    -- get the value from a @MVar@, without emptying, blocking the-    -- thread until it's full.-    AReadMVar cvar@(MVar cvid _) c -> synchronised $ do-      (success, threads', _, _) <- readFromMVar cvar c tid (cThreads ctx)-      simple threads' (if success then ReadMVar cvid else BlockedReadMVar cvid) noSnap+-- try to put a value into a @MVar@, without blocking.+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)+       , const effect+       ) -    -- try to get the value from a @MVar@, without emptying, without-    -- blocking.-    ATryReadMVar cvar@(MVar cvid _) c -> synchronised $ do-      (success, threads', _, _) <- tryReadFromMVar cvar c tid (cThreads ctx)-      simple threads' (TryReadMVar cvid success) noSnap+-- get the value from a @MVar@, without emptying, blocking the thread+-- until it's full.+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)+       , const (pure ())+       ) -    -- take the value from a @MVar@, blocking the thread until it's-    -- full.-    ATakeMVar cvar@(MVar cvid _) c -> synchronised $ do-      (success, threads', woken, effect) <- takeFromMVar cvar c tid (cThreads ctx)-      simple threads' (if success then TakeMVar cvid woken else BlockedTakeMVar cvid) (const effect)+-- try to get the value from a @MVar@, without emptying, without+-- blocking.+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)+       , const (pure ())+       ) -    -- try to take the value from a @MVar@, without blocking.-    ATryTakeMVar cvar@(MVar cvid _) c -> synchronised $ do-      (success, threads', woken, effect) <- tryTakeFromMVar cvar c tid (cThreads ctx)-      simple threads' (TryTakeMVar cvid success woken) (const effect)+-- take the value from a @MVar@, blocking the thread until it's full.+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)+       , const effect+       ) -    -- create a new @CRef@, using the next 'CRefId'.-    ANewCRef n a c -> do-      let (idSource', newcrid) = nextCRId n (cIdSource ctx)-      let val = (M.empty, 0, a)-      ref <- newRef val-      let cref = CRef newcrid ref-      pure ( Succeeded ctx { cThreads = goto (c cref) tid (cThreads ctx), cIdSource = idSource' }-           , Single (NewCRef newcrid)-           , const (writeRef ref val)-           )+-- try to take the value from a @MVar@, without blocking.+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)+       , const effect+       ) -    -- read from a @CRef@.-    AReadCRef cref@(CRef crid _) c -> do-      val <- readCRef cref tid-      simple (goto (c val) tid (cThreads ctx)) (ReadCRef crid) noSnap+-- create a new @CRef@, using the next 'CRefId'.+stepThread _ _ _ _  tid (ANewCRef n a c) = \ctx@Context{..} -> do+  let (idSource', newcrid) = nextCRId n cIdSource+  let val = (M.empty, 0, a)+  ref <- C.newCRef val+  let cref = ModelCRef newcrid ref+  pure ( Succeeded ctx { cThreads = goto (c cref) tid cThreads, cIdSource = idSource' }+       , Single (NewCRef newcrid)+       , const (C.writeCRef ref val)+       ) -    -- read from a @CRef@ for future compare-and-swap operations.-    AReadCRefCas cref@(CRef crid _) c -> do-      tick <- readForTicket cref tid-      simple (goto (c tick) tid (cThreads ctx)) (ReadCRefCas crid) noSnap+-- read from a @CRef@.+stepThread _ _ _ _  tid (AReadCRef cref@ModelCRef{..} c) = \ctx@Context{..} -> do+  val <- readCRef cref tid+  pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads }+       , Single (ReadCRef crefId)+       , const (pure ())+       ) -    -- modify a @CRef@.-    AModCRef cref@(CRef crid _) f c -> synchronised $ do-      (new, val) <- f <$> readCRef cref tid-      effect <- writeImmediate cref new-      simple (goto (c val) tid (cThreads ctx)) (ModCRef crid) (const effect)+-- read from a @CRef@ for future compare-and-swap operations.+stepThread _ _ _ _ tid (AReadCRefCas cref@ModelCRef{..} c) = \ctx@Context{..} -> do+  tick <- readForTicket cref tid+  pure ( Succeeded ctx { cThreads = goto (c tick) tid cThreads }+       , Single (ReadCRefCas crefId)+       , const (pure ())+       ) -    -- modify a @CRef@ using a compare-and-swap.-    AModCRefCas cref@(CRef crid _) f c -> synchronised $ do-      tick@(Ticket _ _ old) <- readForTicket cref tid-      let (new, val) = f old-      (_, _, effect) <- casCRef cref tid tick new-      simple (goto (c val) tid (cThreads ctx)) (ModCRefCas crid) (const effect)+-- modify a @CRef@.+stepThread _ _ _ _ tid (AModCRef cref@ModelCRef{..} f c) = synchronised $ \ctx@Context{..} -> do+  (new, val) <- f <$> readCRef cref tid+  effect <- writeImmediate cref new+  pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads }+       , Single (ModCRef crefId)+       , const effect+       ) -    -- write to a @CRef@ without synchronising.-    AWriteCRef cref@(CRef crid _) a c -> case memtype of-      -- write immediately.-      SequentialConsistency -> do-        effect <- writeImmediate cref a-        simple (goto c tid (cThreads ctx)) (WriteCRef crid) (const effect)-      -- add to buffer using thread id.-      TotalStoreOrder -> do-        wb' <- bufferWrite (cWriteBuf ctx) (tid, Nothing) cref a-        pure (Succeeded ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Single (WriteCRef crid), noSnap)-      -- add to buffer using both thread id and cref id-      PartialStoreOrder -> do-        wb' <- bufferWrite (cWriteBuf ctx) (tid, Just crid) cref a-        pure (Succeeded ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Single (WriteCRef crid), noSnap)+-- modify a @CRef@ using a compare-and-swap.+stepThread _ _ _ _ tid (AModCRefCas cref@ModelCRef{..} f c) = synchronised $ \ctx@Context{..} -> do+  tick@(ModelTicket _ _ old) <- readForTicket cref tid+  let (new, val) = f old+  (_, _, effect) <- casCRef cref tid tick new+  pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads }+       , Single (ModCRefCas crefId)+       , const effect+       ) -    -- perform a compare-and-swap on a @CRef@.-    ACasCRef cref@(CRef crid _) tick a c -> synchronised $ do-      (suc, tick', effect) <- casCRef cref tid tick a-      simple (goto (c (suc, tick')) tid (cThreads ctx)) (CasCRef crid suc) (const effect)+-- write to a @CRef@ without synchronising.+stepThread _ _ _ memtype tid (AWriteCRef cref@ModelCRef{..} a c) = \ctx@Context{..} -> case memtype of+  -- write immediately.+  SequentialConsistency -> do+    effect <- writeImmediate cref a+    pure ( Succeeded ctx { cThreads = goto c tid cThreads }+         , Single (WriteCRef crefId)+         , const effect+         )+  -- add to buffer using thread id.+  TotalStoreOrder -> do+    wb' <- bufferWrite cWriteBuf (tid, Nothing) cref a+    pure ( Succeeded ctx { cThreads = goto c tid cThreads, cWriteBuf = wb' }+         , Single (WriteCRef crefId)+         , const (pure ())+         )+  -- add to buffer using both thread id and cref id+  PartialStoreOrder -> do+    wb' <- bufferWrite cWriteBuf (tid, Just crefId) cref a+    pure ( Succeeded ctx { cThreads = goto c tid cThreads, cWriteBuf = wb' }+         , Single (WriteCRef crefId)+         , const (pure ())+         ) -    -- commit a @CRef@ write-    ACommit t c -> do-      wb' <- case memtype of-        -- shouldn't ever get here-        SequentialConsistency ->-          fatal "stepThread.ACommit" "Attempting to commit under SequentialConsistency"-        -- commit using the thread id.-        TotalStoreOrder -> commitWrite (cWriteBuf ctx) (t, Nothing)-        -- commit using the cref id.-        PartialStoreOrder -> commitWrite (cWriteBuf ctx) (t, Just c)-      pure (Succeeded ctx { cWriteBuf = wb' }, Single (CommitCRef t c), noSnap)+-- perform a compare-and-swap on a @CRef@.+stepThread _ _ _ _ tid (ACasCRef cref@ModelCRef{..} tick a c) = synchronised $ \ctx@Context{..} -> do+  (suc, tick', effect) <- casCRef cref tid tick a+  pure ( Succeeded ctx { cThreads = goto (c (suc, tick')) tid cThreads }+       , Single (CasCRef crefId suc)+       , const effect+       ) -    -- run a STM transaction atomically.-    AAtom stm c -> synchronised $ do-      let transaction = runTransaction stm (cIdSource ctx)-      let effect = const (void transaction)-      (res, idSource', trace) <- transaction-      case res of-        Success _ written val ->-          let (threads', woken) = wake (OnTVar written) (cThreads ctx)-          in pure (Succeeded ctx { cThreads = goto (c val) tid threads', cIdSource = idSource' }, Single (STM trace woken), effect)-        Retry touched ->-          let threads' = block (OnTVar touched) tid (cThreads ctx)-          in pure (Succeeded ctx { cThreads = threads', cIdSource = idSource'}, Single (BlockedSTM trace), effect)-        Exception e -> do-          let act = STM trace []-          res' <- stepThrow tid (cThreads ctx) act e-          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"+-- commit a @CRef@ write+stepThread _ _ _ memtype _ (ACommit t c) = \ctx@Context{..} -> do+  wb' <- case memtype of+    -- shouldn't ever get here+    SequentialConsistency ->+      fatal "stepThread.ACommit" "Attempting to commit under SequentialConsistency"+    -- commit using the thread id.+    TotalStoreOrder ->+      commitWrite cWriteBuf (t, Nothing)+    -- commit using the cref id.+    PartialStoreOrder ->+      commitWrite cWriteBuf (t, Just c)+  pure ( Succeeded ctx { cWriteBuf = wb' }+       , Single (CommitCRef t c)+       , const (pure ())+       ) -    -- lift an action from the underlying monad into the @Conc@-    -- computation.-    ALift na -> do-      let effect threads = runLiftedAct tid threads na-      a <- effect (cThreads ctx)-      simple (goto a tid (cThreads ctx)) LiftIO (void <$> effect)+-- run a STM transaction atomically.+stepThread _ _ _ _ tid (AAtom stm c) = synchronised $ \ctx@Context{..} -> do+  let transaction = runTransaction stm cIdSource+  let effect = const (void transaction)+  (res, idSource', trace) <- transaction+  case res of+    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)+           , effect+           )+    Retry touched -> do+      let threads' = block (OnTVar touched) tid cThreads+      pure ( Succeeded ctx { cThreads = threads', cIdSource = idSource'}+           , Single (BlockedSTM trace)+           , effect+           )+    Exception e -> do+      let act = STM trace []+      res' <- stepThrow 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" -    -- throw an exception, and propagate it to the appropriate-    -- handler.-    AThrow e -> stepThrow tid (cThreads ctx) Throw e+-- lift an action from the underlying monad into the @Conc@+-- computation.+stepThread _ _ _ _ tid (ALift na) = \ctx@Context{..} -> do+  let effect threads = runLiftedAct tid threads na+  a <- effect cThreads+  pure (Succeeded ctx { cThreads = goto a tid cThreads }+       , Single LiftIO+       , void <$> effect+       ) -    -- throw an exception to the target thread, and propagate it to-    -- the appropriate handler.-    AThrowTo t e c -> synchronised $-      let threads' = goto c tid (cThreads ctx)-          blocked  = block (OnMask t) tid (cThreads ctx)-      in case M.lookup t (cThreads ctx) of-           Just thread-             | interruptible thread -> stepThrow t threads' (ThrowTo t) e-             | otherwise -> simple blocked (BlockedThrowTo t) noSnap-           Nothing -> simple threads' (ThrowTo t) noSnap+-- throw an exception, and propagate it to the appropriate handler.+stepThread _ _ _ _ tid (AThrow e) = stepThrow Throw tid e -    -- run a subcomputation in an exception-catching context.-    ACatching h ma c ->-      let a        = runCont ma (APopCatching . c)-          e exc    = runCont (h exc) c-          threads' = goto a tid (catching e tid (cThreads ctx))-      in simple threads' Catching noSnap+-- throw an exception to the target thread, and propagate it to the+-- appropriate handler.+stepThread _ _ _ _ tid (AThrowTo t e c) = synchronised $ \ctx@Context{..} ->+  let threads' = goto c tid cThreads+      blocked  = block (OnMask t) tid cThreads+  in case M.lookup t cThreads of+       Just thread+         | interruptible thread -> stepThrow (ThrowTo t) t e ctx { cThreads = threads' }+         | otherwise -> pure+           ( Succeeded ctx { cThreads = blocked }+           , Single (BlockedThrowTo t)+           , const (pure ())+           )+       Nothing -> pure+         (Succeeded ctx { cThreads = threads' }+         , Single (ThrowTo t)+         , const (pure ())+         ) -    -- pop the top exception handler from the thread's stack.-    APopCatching a ->-      let threads' = goto a tid (uncatching tid (cThreads ctx))-      in simple threads' PopCatching noSnap+-- run a subcomputation in an exception-catching context.+stepThread _ _ _ _ tid (ACatching h ma c) = \ctx@Context{..} -> pure $+  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+     , const (pure ())+     ) -    -- execute a subcomputation with a new masking state, and give it-    -- a function to run a computation with the current masking state.-    AMasking m ma c ->-      let a = runCont (ma umask) (AResetMask False False m' . c)-          m' = _masking $ elookup "stepThread.AMasking" tid (cThreads ctx)-          umask mb = resetMask True m' >> mb >>= \b -> resetMask False m >> pure b-          resetMask typ ms = cont $ \k -> AResetMask typ True ms $ k ()-          threads' = goto a tid (mask m tid (cThreads ctx))-      in simple threads' (SetMasking False m) noSnap+-- 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+       , const (pure ())+       ) +-- execute a subcomputation with a new masking state, and give it a+-- function to run a computation with the current masking state.+stepThread _ _ _ _ tid (AMasking m ma c) = \ctx@Context{..} -> pure $+  let resetMask typ ms = ModelConc $ \k -> AResetMask typ True ms $ k ()+      umask mb = resetMask True m' >> mb >>= \b -> resetMask False m >> pure b+      m' = _masking $ elookup "stepThread.AMasking" 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)+     , const (pure ())+     ) -    -- reset the masking thread of the state.-    AResetMask b1 b2 m c ->-      let act      = (if b1 then SetMasking else ResetMasking) b2 m-          threads' = goto c tid (mask m tid (cThreads ctx))-      in simple threads' act noSnap+-- 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)+       , const (pure ())+       ) -    -- execute a 'return' or 'pure'.-    AReturn c -> simple (goto c tid (cThreads ctx)) Return noSnap+-- execute a 'return' or 'pure'.+stepThread _ _ _ _ tid (AReturn c) = \ctx@Context{..} ->+  pure ( Succeeded ctx { cThreads = goto c tid cThreads }+       , Single Return+       , const (pure ())+       ) -    -- kill the current thread.-    AStop na -> do-      na-      threads' <- kill tid (cThreads ctx)-      simple threads' Stop noSnap+-- kill the current thread.+stepThread _ _ _ _ tid (AStop na) = \ctx@Context{..} -> do+  na+  threads' <- kill tid cThreads+  pure ( Succeeded ctx { cThreads = threads' }+       , Single Stop+       , const (pure ())+       ) -    -- run a subconcurrent computation.-    ASub ma c-      | forSnapshot -> pure (Failed IllegalSubconcurrency, Single Subconcurrency, noSnap)-      | M.size (cThreads ctx) > 1 -> pure (Failed IllegalSubconcurrency, Single Subconcurrency, noSnap)-      | otherwise -> do-          res <- runConcurrency False sched memtype (cSchedState ctx) (cIdSource ctx) (cCaps ctx) ma-          out <- efromJust "stepThread.ASub" <$> readRef (finalRef res)-          pure (Succeeded ctx+-- run a subconcurrent computation.+stepThread forSnapshot _ sched memtype tid (ASub ma c) = \ctx ->+  if | forSnapshot -> pure (Failed IllegalSubconcurrency, Single Subconcurrency, const (pure ()))+     | M.size (cThreads ctx) > 1 -> pure (Failed IllegalSubconcurrency, Single Subconcurrency, const (pure ()))+     | otherwise -> do+         res <- runConcurrency False sched memtype (cSchedState ctx) (cIdSource ctx) (cCaps ctx) ma+         out <- efromJust "stepThread.ASub" <$> C.readCRef (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)-               , noSnap-               )--    -- 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.-    AStopSub c -> simple (goto c tid (cThreads ctx)) StopSubconcurrency noSnap--    -- run an action atomically, with a non-preemptive length bounded-    -- round robin scheduler, under sequential consistency.-    ADontCheck lb ma c-      | 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 "stepThread.ADontCheck" <$> readRef (finalRef res)-          case out of-            Right a -> do-              let threads'' = launch' Unmasked tid (const (c a)) (cThreads (finalContext res))-              threads''' <- (if 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 noSnap (finalRestore res)-                   )-            Left f ->-              pure (Failed f, Single (DontCheck (toList (finalTrace res))), noSnap)-      | otherwise -> pure (Failed IllegalDontCheck, Single (DontCheck []), noSnap)-  where--    -- this is not inline in the long @case@ above as it's needed by-    -- @AAtom@, @AThrow@, and @AThrowTo@.-    stepThrow t ts act e =-      let some = toException e-      in case propagate some t ts of-           Just ts' -> simple ts' act noSnap-           Nothing-             | t == initialThread -> pure (Failed (UncaughtException some), Single act, noSnap)-             | otherwise -> do-                 ts' <- kill t ts-                 simple ts' act noSnap+              , SubC (finalTrace res) (finalDecision res)+              , const (pure ())+              ) -    -- helper for actions which only change the threads.-    simple threads' act effect = pure (Succeeded ctx { cThreads = threads' }, Single act, effect)+-- 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+       , const (pure ())+       ) -    -- helper for actions impose a write barrier.-    synchronised ma = do-      writeBarrier (cWriteBuf ctx)-      res <- ma+-- 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 "stepThread.ADontCheck" <$> C.readCRef (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 -> pure+       ( Failed IllegalDontCheck+       , Single (DontCheck [])+       , const (pure ())+       ) -      pure $ case res of-        (Succeeded ctx', act, effect) -> (Succeeded ctx' { cWriteBuf = emptyBuffer }, act, effect)-        _ -> res+-- | Handle an exception being thrown from an @AAtom@, @AThrow@, or+-- @AThrowTo@.+stepThrow :: (C.MonadConc n, Exception e)+  => ThreadAction+  -- ^ Action to include in the trace.+  -> ThreadId+  -- ^ The thread receiving the exception.+  -> e+  -- ^ Exception to raise.+  -> Context n g+  -- ^ The execution context.+  -> n (What n g, Act, Threads n -> n ())+stepThrow act tid e ctx@Context{..} = case propagate some tid cThreads of+    Just ts' -> pure+      ( Succeeded ctx { cThreads = ts' }+      , Single act+      , const (pure ())+      )+    Nothing+      | tid == initialThread -> pure+        ( Failed (UncaughtException some)+        , Single act+        , const (pure ())+        )+      | otherwise -> do+          ts' <- kill tid cThreads+          pure ( Succeeded ctx { cThreads = ts' }+               , Single act+               , const (pure ())+               )+  where+    some = toException e -    -- scheduler for @ADontCheck@-    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)+-- | Helper for actions impose a write barrier.+synchronised :: C.MonadConc n+  => (Context n g -> n (What n g, Act, Threads n -> n ()))+  -- ^ Action to run after the write barrier.+  -> Context n g+  -- ^ The original execution context.+  -> n (What n g, Act, Threads n -> n ())+synchronised ma ctx@Context{..} = do+  writeBarrier cWriteBuf+  ma ctx { cWriteBuf = emptyBuffer } -    -- no snapshot-    noSnap _ = pure ()+-- | 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)

@@ -16,8 +16,9 @@ module Test.DejaFu.Conc.Internal.Common where  import           Control.Exception             (Exception, MaskingState(..))+import qualified Control.Monad.Conc.Class      as C import           Data.Map.Strict               (Map)-import           Test.DejaFu.Conc.Internal.STM (S)+import           Test.DejaFu.Conc.Internal.STM (ModelSTM) import           Test.DejaFu.Types  #if MIN_VERSION_base(4,9,0)@@ -25,7 +26,7 @@ #endif  ----------------------------------------------------------------------------------- * The @Conc@ Monad+-- * The @ModelConc@ Monad  -- | The underlying monad is based on continuations over 'Action's. --@@ -35,73 +36,52 @@ -- current expression of threads and exception handlers very difficult -- (perhaps even not possible without significant reworking), so I -- abandoned the attempt.-newtype M n r a = M { runM :: (a -> Action n r) -> Action n r }+newtype ModelConc n a = ModelConc { runModelConc :: (a -> Action n) -> Action n } -instance Functor (M n r) where-    fmap f m = M $ \ c -> runM m (c . f)+instance Functor (ModelConc n) where+    fmap f m = ModelConc $ \c -> runModelConc m (c . f) -instance Applicative (M n r) where+instance Applicative (ModelConc n) where     -- without the @AReturn@, a thread could lock up testing by     -- entering an infinite loop (eg: @forever (return ())@)-    pure x  = M $ \c -> AReturn $ c x-    f <*> v = M $ \c -> runM f (\g -> runM v (c . g))+    pure x  = ModelConc $ \c -> AReturn $ c x+    f <*> v = ModelConc $ \c -> runModelConc f (\g -> runModelConc v (c . g)) -instance Monad (M n r) where+instance Monad (ModelConc n) where     return  = pure-    m >>= k = M $ \c -> runM m (\x -> runM (k x) c)+    m >>= k = ModelConc $ \c -> runModelConc m (\x -> runModelConc (k x) c)  #if MIN_VERSION_base(4,9,0)     fail = Fail.fail --- | @since 0.7.1.2-instance Fail.MonadFail (M n r) where+instance Fail.MonadFail (ModelConc n) where #endif-    fail e = cont (\_ -> AThrow (MonadFailException e))+    fail e = ModelConc $ \_ -> AThrow (MonadFailException e) --- | The concurrent variable type used with the 'Conc' monad. One--- notable difference between these and 'MVar's is that 'MVar's are--- single-wakeup, and wake up in a FIFO order. Writing to a @MVar@--- wakes up all threads blocked on reading it, and it is up to the--- scheduler which one runs next. Taking from a @MVar@ behaves--- analogously.-data MVar r a = MVar-  { _cvarId   :: MVarId-  , _cvarVal  :: r (Maybe a)+-- | An @MVar@ is modelled as a unique ID and a reference holding a+-- @Maybe@ value.+data ModelMVar n a = ModelMVar+  { mvarId  :: MVarId+  , mvarRef :: C.CRef n (Maybe a)   } --- | The mutable non-blocking reference type. These are like 'IORef's.------ @CRef@s are represented as a unique numeric identifier and a--- reference containing (a) any thread-local non-synchronised writes--- (so each thread sees its latest write), (b) a commit count (used in--- compare-and-swaps), and (c) the current value visible to all--- threads.-data CRef r a = CRef-  { _crefId   :: CRefId-  , _crefVal  :: r (Map ThreadId a, Integer, a)+-- | A @CRef@ is modelled as a unique ID and a reference holding+-- thread-local values, the number of commits, and the most recent+-- committed value.+data ModelCRef n a = ModelCRef+  { crefId  :: CRefId+  , crefRef :: C.CRef n (Map ThreadId a, Integer, a)   } --- | The compare-and-swap proof type.------ @Ticket@s are represented as just a wrapper around the identifier--- of the 'CRef' it came from, the commit count at the time it was--- produced, and an @a@ value. This doesn't work in the source package--- (atomic-primops) because of the need to use pointer equality. Here--- we can just pack extra information into 'CRef' to avoid that need.-data Ticket a = Ticket-  { _ticketCRef   :: CRefId-  , _ticketWrites :: Integer-  , _ticketVal    :: a+-- | A @Ticket@ is modelled as the ID of the @ModelCRef@ it came from,+-- the commits to the @ModelCRef@ at the time it was produced, and the+-- value observed.+data ModelTicket a = ModelTicket+  { ticketCRef   :: CRefId+  , ticketWrites :: Integer+  , ticketVal    :: a   } --- | Construct a continuation-passing operation from a function.-cont :: ((a -> Action n r) -> Action n r) -> M n r a-cont = M---- | Run a CPS computation with the given final computation.-runCont :: M n r a -> (a -> Action n r) -> Action n r-runCont = runM- -------------------------------------------------------------------------------- -- * Primitive Actions @@ -109,55 +89,55 @@ -- only occur as a result of an action, and they cover (most of) the -- primitives of the concurrency. 'spawn' is absent as it is -- implemented in terms of 'newEmptyMVar', 'fork', and 'putMVar'.-data Action n r =-    AFork   String ((forall b. M n r b -> M n r b) -> Action n r) (ThreadId -> Action n r)-  | AForkOS String ((forall b. M n r b -> M n r b) -> Action n r) (ThreadId -> Action n r)-  | AIsBound (Bool -> Action n r)-  | AMyTId (ThreadId -> Action n r)+data Action n =+    AFork   String ((forall b. ModelConc n b -> ModelConc n b) -> Action n) (ThreadId -> Action n)+  | AForkOS String ((forall b. ModelConc n b -> ModelConc n b) -> Action n) (ThreadId -> Action n)+  | AIsBound (Bool -> Action n)+  | AMyTId (ThreadId -> Action n) -  | AGetNumCapabilities (Int -> Action n r)-  | ASetNumCapabilities Int (Action n r)+  | AGetNumCapabilities (Int -> Action n)+  | ASetNumCapabilities Int (Action n) -  | forall a. ANewMVar String (MVar r a -> Action n r)-  | forall a. APutMVar     (MVar r a) a (Action n r)-  | forall a. ATryPutMVar  (MVar r a) a (Bool -> Action n r)-  | forall a. AReadMVar    (MVar r a) (a -> Action n r)-  | forall a. ATryReadMVar (MVar r a) (Maybe a -> Action n r)-  | forall a. ATakeMVar    (MVar r a) (a -> Action n r)-  | forall a. ATryTakeMVar (MVar r a) (Maybe a -> Action n r)+  | forall a. ANewMVar String (ModelMVar n a -> Action n)+  | forall a. APutMVar     (ModelMVar n a) a (Action n)+  | forall a. ATryPutMVar  (ModelMVar n a) a (Bool -> Action n)+  | forall a. AReadMVar    (ModelMVar n a) (a -> Action n)+  | forall a. ATryReadMVar (ModelMVar n a) (Maybe a -> Action n)+  | forall a. ATakeMVar    (ModelMVar n a) (a -> Action n)+  | forall a. ATryTakeMVar (ModelMVar n a) (Maybe a -> Action n) -  | forall a.   ANewCRef String a (CRef r a -> Action n r)-  | forall a.   AReadCRef    (CRef r a) (a -> Action n r)-  | forall a.   AReadCRefCas (CRef r a) (Ticket a -> Action n r)-  | forall a b. AModCRef     (CRef r a) (a -> (a, b)) (b -> Action n r)-  | forall a b. AModCRefCas  (CRef r a) (a -> (a, b)) (b -> Action n r)-  | forall a.   AWriteCRef   (CRef r a) a (Action n r)-  | forall a.   ACasCRef     (CRef r a) (Ticket a) a ((Bool, Ticket a) -> Action n r)+  | forall a.   ANewCRef String a (ModelCRef n a -> Action n)+  | forall a.   AReadCRef    (ModelCRef n a) (a -> Action n)+  | forall a.   AReadCRefCas (ModelCRef n a) (ModelTicket a -> Action n)+  | forall a b. AModCRef     (ModelCRef n a) (a -> (a, b)) (b -> Action n)+  | forall a b. AModCRefCas  (ModelCRef n a) (a -> (a, b)) (b -> Action n)+  | forall a.   AWriteCRef   (ModelCRef n a) a (Action n)+  | forall a.   ACasCRef     (ModelCRef n a) (ModelTicket a) a ((Bool, ModelTicket a) -> Action n)    | forall e.   Exception e => AThrow e-  | forall e.   Exception e => AThrowTo ThreadId e (Action n r)-  | forall a e. Exception e => ACatching (e -> M n r a) (M n r a) (a -> Action n r)-  | APopCatching (Action n r)-  | forall a. AMasking MaskingState ((forall b. M n r b -> M n r b) -> M n r a) (a -> Action n r)-  | AResetMask Bool Bool MaskingState (Action n r)+  | forall e.   Exception e => AThrowTo ThreadId e (Action n)+  | forall a e. Exception e => ACatching (e -> ModelConc n a) (ModelConc n a) (a -> Action n)+  | APopCatching (Action n)+  | forall a. AMasking MaskingState ((forall b. ModelConc n b -> ModelConc n b) -> ModelConc n a) (a -> Action n)+  | AResetMask Bool Bool MaskingState (Action n) -  | forall a. AAtom (S n r a) (a -> Action n r)-  | ALift (n (Action n r))-  | AYield  (Action n r)-  | ADelay Int (Action n r)-  | AReturn (Action n r)+  | forall a. AAtom (ModelSTM n a) (a -> Action n)+  | ALift (n (Action n))+  | AYield  (Action n)+  | ADelay Int (Action n)+  | AReturn (Action n)   | ACommit ThreadId CRefId   | AStop (n ()) -  | forall a. ASub (M n r a) (Either Failure a -> Action n r)-  | AStopSub (Action n r)-  | forall a. ADontCheck (Maybe Int) (M n r a) (a -> Action n r)+  | forall a. ASub (ModelConc n a) (Either Failure a -> Action n)+  | AStopSub (Action n)+  | forall a. ADontCheck (Maybe Int) (ModelConc n a) (a -> Action n)  -------------------------------------------------------------------------------- -- * Scheduling & Traces  -- | Look as far ahead in the given continuation as possible.-lookahead :: Action n r -> Lookahead+lookahead :: Action n -> Lookahead lookahead (AFork _ _ _) = WillFork lookahead (AForkOS _ _ _) = WillForkOS lookahead (AIsBound _) = WillIsCurrentThreadBound@@ -165,19 +145,19 @@ lookahead (AGetNumCapabilities _) = WillGetNumCapabilities lookahead (ASetNumCapabilities i _) = WillSetNumCapabilities i lookahead (ANewMVar _ _) = WillNewMVar-lookahead (APutMVar (MVar c _) _ _) = WillPutMVar c-lookahead (ATryPutMVar (MVar c _) _ _) = WillTryPutMVar c-lookahead (AReadMVar (MVar c _) _) = WillReadMVar c-lookahead (ATryReadMVar (MVar c _) _) = WillTryReadMVar c-lookahead (ATakeMVar (MVar c _) _) = WillTakeMVar c-lookahead (ATryTakeMVar (MVar c _) _) = WillTryTakeMVar c+lookahead (APutMVar (ModelMVar m _) _ _) = WillPutMVar m+lookahead (ATryPutMVar (ModelMVar m _) _ _) = WillTryPutMVar m+lookahead (AReadMVar (ModelMVar m _) _) = WillReadMVar m+lookahead (ATryReadMVar (ModelMVar m _) _) = WillTryReadMVar m+lookahead (ATakeMVar (ModelMVar m _) _) = WillTakeMVar m+lookahead (ATryTakeMVar (ModelMVar m _) _) = WillTryTakeMVar m lookahead (ANewCRef _ _ _) = WillNewCRef-lookahead (AReadCRef (CRef r _) _) = WillReadCRef r-lookahead (AReadCRefCas (CRef r _) _) = WillReadCRefCas r-lookahead (AModCRef (CRef r _) _ _) = WillModCRef r-lookahead (AModCRefCas (CRef r _) _ _) = WillModCRefCas r-lookahead (AWriteCRef (CRef r _) _ _) = WillWriteCRef r-lookahead (ACasCRef (CRef r _) _ _ _) = WillCasCRef r+lookahead (AReadCRef (ModelCRef r _) _) = WillReadCRef r+lookahead (AReadCRefCas (ModelCRef r _) _) = WillReadCRefCas r+lookahead (AModCRef (ModelCRef r _) _ _) = WillModCRef r+lookahead (AModCRefCas (ModelCRef r _) _ _) = WillModCRefCas r+lookahead (AWriteCRef (ModelCRef r _) _ _) = WillWriteCRef r+lookahead (ACasCRef (ModelCRef r _) _ _ _) = WillCasCRef r lookahead (ACommit t c) = WillCommitCRef t c lookahead (AAtom _ _) = WillSTM lookahead (AThrow _) = WillThrow

@@ -1,6 +1,7 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RecordWildCards #-}  -- | -- Module      : Test.DejaFu.Conc.Internal.Memory@@ -8,7 +9,7 @@ -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : BangPatterns, GADTs, MultiParamTypeClasses+-- Portability : BangPatterns, GADTs, LambdaCase, RecordWildCards -- -- Operations over @CRef@s and @MVar@s. This module is NOT considered -- to form part of the public interface of this library.@@ -23,8 +24,7 @@ -- Memory Models/, N. Zhang, M. Kusano, and C. Wang (2015). module Test.DejaFu.Conc.Internal.Memory where -import           Control.Monad.Ref                   (MonadRef, readRef,-                                                      writeRef)+import qualified Control.Monad.Conc.Class            as C import           Data.Map.Strict                     (Map) import qualified Data.Map.Strict                     as M import           Data.Maybe                          (maybeToList)@@ -45,60 +45,59 @@ -- -- The @CRefId@ parameter is only used under PSO. Under TSO each -- thread has a single buffer.-newtype WriteBuffer r = WriteBuffer-  { buffer :: Map (ThreadId, Maybe CRefId) (Seq (BufferedWrite r)) }+newtype WriteBuffer n = WriteBuffer+  { buffer :: Map (ThreadId, Maybe CRefId) (Seq (BufferedWrite n)) }  -- | A buffered write is a reference to the variable, and the value to -- write. Universally quantified over the value type so that the only -- thing which can be done with it is to write it to the reference.-data BufferedWrite r where-  BufferedWrite :: ThreadId -> CRef r a -> a -> BufferedWrite r+data BufferedWrite n where+  BufferedWrite :: ThreadId -> ModelCRef n a -> a -> BufferedWrite n  -- | An empty write buffer.-emptyBuffer :: WriteBuffer r+emptyBuffer :: WriteBuffer n emptyBuffer = WriteBuffer M.empty  -- | Add a new write to the end of a buffer.-bufferWrite :: MonadRef r n => WriteBuffer r -> (ThreadId, Maybe CRefId) -> CRef r a -> a -> n (WriteBuffer r)-bufferWrite (WriteBuffer wb) k@(tid, _) cref@(CRef _ ref) new = do+bufferWrite :: C.MonadConc n => WriteBuffer n -> (ThreadId, Maybe CRefId) -> ModelCRef n a -> a -> n (WriteBuffer n)+bufferWrite (WriteBuffer wb) k@(tid, _) cref@ModelCRef{..} new = do   -- Construct the new write buffer   let write = singleton $ BufferedWrite tid cref new   let buffer' = M.insertWith (flip (><)) k write wb    -- Write the thread-local value to the @CRef@'s update map.-  (locals, count, def) <- readRef ref-  writeRef ref (M.insert tid new locals, count, def)+  (locals, count, def) <- C.readCRef crefRef+  C.writeCRef crefRef (M.insert tid new locals, count, def)    pure (WriteBuffer buffer')  -- | Commit the write at the head of a buffer.-commitWrite :: MonadRef r n => WriteBuffer r -> (ThreadId, Maybe CRefId) -> n (WriteBuffer r)+commitWrite :: C.MonadConc n => WriteBuffer n -> (ThreadId, Maybe CRefId) -> n (WriteBuffer n) commitWrite w@(WriteBuffer wb) k = case maybe EmptyL viewl $ M.lookup k wb of   BufferedWrite _ cref a :< rest -> do     _ <- writeImmediate cref a     pure . WriteBuffer $ M.insert k rest wb-   EmptyL -> pure w  -- | Read from a @CRef@, returning a newer thread-local non-committed -- write if there is one.-readCRef :: MonadRef r n => CRef r a -> ThreadId -> n a+readCRef :: C.MonadConc n => ModelCRef n a -> ThreadId -> n a readCRef cref tid = do   (val, _) <- readCRefPrim cref tid   pure val  -- | Read from a @CRef@, returning a @Ticket@ representing the current -- view of the thread.-readForTicket :: MonadRef r n => CRef r a -> ThreadId -> n (Ticket a)-readForTicket cref@(CRef crid _) tid = do+readForTicket :: C.MonadConc n => ModelCRef n a -> ThreadId -> n (ModelTicket a)+readForTicket cref@ModelCRef{..} tid = do   (val, count) <- readCRefPrim cref tid-  pure (Ticket crid count val)+  pure (ModelTicket crefId count val)  -- | Perform a compare-and-swap on a @CRef@ if the ticket is still -- valid. This is strict in the \"new\" value argument.-casCRef :: MonadRef r n => CRef r a -> ThreadId -> Ticket a -> a -> n (Bool, Ticket a, n ())-casCRef cref tid (Ticket _ cc _) !new = do-  tick'@(Ticket _ cc' _) <- readForTicket cref tid+casCRef :: C.MonadConc n => ModelCRef n a -> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ())+casCRef cref tid (ModelTicket _ cc _) !new = do+  tick'@(ModelTicket _ cc' _) <- readForTicket cref tid    if cc == cc'   then do@@ -108,34 +107,33 @@   else pure (False, tick', pure ())  -- | Read the local state of a @CRef@.-readCRefPrim :: MonadRef r n => CRef r a -> ThreadId -> n (a, Integer)-readCRefPrim (CRef _ ref) tid = do-  (vals, count, def) <- readRef ref-+readCRefPrim :: C.MonadConc n => ModelCRef n a -> ThreadId -> n (a, Integer)+readCRefPrim ModelCRef{..} tid = do+  (vals, count, def) <- C.readCRef crefRef   pure (M.findWithDefault def tid vals, count)  -- | Write and commit to a @CRef@ immediately, clearing the update map -- and incrementing the write count.-writeImmediate :: MonadRef r n => CRef r a -> a -> n (n ())-writeImmediate (CRef _ ref) a = do-  (_, count, _) <- readRef ref-  let effect = writeRef ref (M.empty, count + 1, a)+writeImmediate :: C.MonadConc n => ModelCRef n a -> a -> n (n ())+writeImmediate ModelCRef{..} a = do+  (_, count, _) <- C.readCRef crefRef+  let effect = C.writeCRef crefRef (M.empty, count + 1, a)   effect   pure effect  -- | Flush all writes in the buffer.-writeBarrier :: MonadRef r n => WriteBuffer r -> n ()+writeBarrier :: C.MonadConc n => WriteBuffer n -> n () writeBarrier (WriteBuffer wb) = mapM_ flush $ M.elems wb where   flush = mapM_ $ \(BufferedWrite _ cref a) -> writeImmediate cref a  -- | Add phantom threads to the thread list to commit pending writes.-addCommitThreads :: WriteBuffer r -> Threads n r -> Threads n r+addCommitThreads :: WriteBuffer n -> Threads n -> Threads n addCommitThreads (WriteBuffer wb) ts = ts <> M.fromList phantoms where   phantoms = [ (uncurry commitThreadId k, mkthread c)              | (k, b) <- M.toList wb              , c <- maybeToList (go $ viewl b)              ]-  go (BufferedWrite tid (CRef crid _) _ :< _) = Just $ ACommit tid crid+  go (BufferedWrite tid ModelCRef{..} _ :< _) = Just $ ACommit tid crefId   go EmptyL = Nothing  -- | The ID of a commit thread.@@ -145,7 +143,7 @@   go Nothing = t + 1  -- | Remove phantom threads.-delCommitThreads :: Threads n r -> Threads n r+delCommitThreads :: Threads n -> Threads n delCommitThreads = M.filterWithKey $ \k _ -> k >= initialThread  --------------------------------------------------------------------------------@@ -156,76 +154,104 @@ data Emptying = Emptying | NonEmptying  -- | Put into a @MVar@, blocking if full.-putIntoMVar :: MonadRef r n => MVar r a -> a -> Action n r-            -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ())+putIntoMVar :: C.MonadConc n+  => ModelMVar n a+  -> a+  -> Action n+  -> ThreadId+  -> Threads n+  -> n (Bool, Threads n, [ThreadId], n ()) putIntoMVar cvar a c = mutMVar Blocking cvar a (const c)  -- | Try to put into a @MVar@, not blocking if full.-tryPutIntoMVar :: MonadRef r n => MVar r a -> a -> (Bool -> Action n r)-               -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ())+tryPutIntoMVar :: C.MonadConc n+  => ModelMVar n a+  -> a+  -> (Bool -> Action n)+  -> ThreadId+  -> Threads n+  -> n (Bool, Threads n, [ThreadId], n ()) tryPutIntoMVar = mutMVar NonBlocking  -- | Read from a @MVar@, blocking if empty.-readFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r)-            -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ())+readFromMVar :: C.MonadConc n+  => ModelMVar n a+  -> (a -> Action n)+  -> ThreadId+  -> Threads n+  -> n (Bool, Threads n, [ThreadId], n ()) readFromMVar cvar c = seeMVar NonEmptying Blocking cvar (c . efromJust "readFromMVar")  -- | Try to read from a @MVar@, not blocking if empty.-tryReadFromMVar :: MonadRef r n => MVar r a -> (Maybe a -> Action n r)-                -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ())+tryReadFromMVar :: C.MonadConc n+  => ModelMVar n a+  -> (Maybe a -> Action n)+  -> ThreadId+  -> Threads n+  -> n (Bool, Threads n, [ThreadId], n ()) tryReadFromMVar = seeMVar NonEmptying NonBlocking  -- | Take from a @MVar@, blocking if empty.-takeFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r)-             -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ())+takeFromMVar :: C.MonadConc n+  => ModelMVar n a+  -> (a -> Action n)+  -> ThreadId+  -> Threads n+  -> n (Bool, Threads n, [ThreadId], n ()) takeFromMVar cvar c = seeMVar Emptying Blocking cvar (c . efromJust "takeFromMVar")  -- | Try to take from a @MVar@, not blocking if empty.-tryTakeFromMVar :: MonadRef r n => MVar r a -> (Maybe a -> Action n r)-                -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ())+tryTakeFromMVar :: C.MonadConc n+  => ModelMVar n a+  -> (Maybe a -> Action n)+  -> ThreadId+  -> Threads n+  -> n (Bool, Threads n, [ThreadId], n ()) tryTakeFromMVar = seeMVar Emptying NonBlocking  -- | Mutate a @MVar@, in either a blocking or nonblocking way.-mutMVar :: MonadRef r n-        => Blocking -> MVar r a -> a -> (Bool -> Action n r)-        -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ())-mutMVar blocking (MVar cvid ref) a c threadid threads = do-  val <- readRef ref--  case val of-    Just _ -> case blocking of-      Blocking ->-        let threads' = block (OnMVarEmpty cvid) threadid threads-        in pure (False, threads', [], pure ())-      NonBlocking ->-        pure (False, goto (c False) threadid threads, [], pure ())--    Nothing -> do-      let effect = writeRef ref $ Just a-      let (threads', woken) = wake (OnMVarFull cvid) threads-      effect-      pure (True, goto (c True) threadid threads', woken, effect)+mutMVar :: C.MonadConc n+  => Blocking+  -> ModelMVar n a+  -> a+  -> (Bool -> Action n)+  -> ThreadId+  -> Threads n+  -> n (Bool, Threads n, [ThreadId], n ())+mutMVar blocking ModelMVar{..} a c threadid threads = C.readCRef mvarRef >>= \case+  Just _ -> case blocking of+    Blocking ->+      let threads' = block (OnMVarEmpty mvarId) threadid threads+      in pure (False, threads', [], pure ())+    NonBlocking ->+      pure (False, goto (c False) threadid threads, [], pure ())+  Nothing -> do+    let effect = C.writeCRef mvarRef $ Just a+    let (threads', woken) = wake (OnMVarFull mvarId) threads+    effect+    pure (True, goto (c True) threadid threads', woken, effect)  -- | Read a @MVar@, in either a blocking or nonblocking -- way.-seeMVar :: MonadRef r n-        => Emptying -> Blocking -> MVar r a -> (Maybe a -> Action n r)-        -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ())-seeMVar emptying blocking (MVar cvid ref) c threadid threads = do-  val <- readRef ref--  case val of-    Just _ -> do-      let effect = case emptying of-            Emptying -> writeRef ref Nothing-            NonEmptying -> pure ()-      let (threads', woken) = wake (OnMVarEmpty cvid) threads-      effect-      pure (True, goto (c val) threadid threads', woken, effect)--    Nothing -> case blocking of-      Blocking ->-        let threads' = block (OnMVarFull cvid) threadid threads-        in pure (False, threads', [], pure ())-      NonBlocking ->-        pure (False, goto (c Nothing) threadid threads, [], pure ())+seeMVar :: C.MonadConc n+  => Emptying+  -> Blocking+  -> ModelMVar n a+  -> (Maybe a -> Action n)+  -> ThreadId+  -> Threads n+  -> n (Bool, Threads n, [ThreadId], n ())+seeMVar emptying blocking ModelMVar{..} c threadid threads = C.readCRef mvarRef >>= \case+  val@(Just _) -> do+    let effect = case emptying of+          Emptying -> C.writeCRef mvarRef Nothing+          NonEmptying -> pure ()+    let (threads', woken) = wake (OnMVarEmpty mvarId) threads+    effect+    pure (True, goto (c val) threadid threads', woken, effect)+  Nothing -> case blocking of+    Blocking ->+      let threads' = block (OnMVarFull mvarId) threadid threads+      in pure (False, threads', [], pure ())+    NonBlocking ->+      pure (False, goto (c Nothing) threadid threads, [], pure ())

@@ -1,6 +1,6 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TypeFamilies #-}  -- Must come after TypeFamilies@@ -12,89 +12,89 @@ -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : CPP, ExistentialQuantification, MultiParamTypeClasses, NoMonoLocalBinds, TypeFamilies+-- Portability : CPP, ExistentialQuantification, NoMonoLocalBinds, RecordWildCards, TypeFamilies -- -- 'MonadSTM' testing implementation, internal types and definitions. -- This module is NOT considered to form part of the public interface -- of this library. module Test.DejaFu.Conc.Internal.STM where -import           Control.Applicative     (Alternative(..))-import           Control.Exception       (Exception, SomeException,-                                          fromException, toException)-import           Control.Monad           (MonadPlus(..))-import           Control.Monad.Catch     (MonadCatch(..), MonadThrow(..))-import           Control.Monad.Ref       (MonadRef, newRef, readRef, writeRef)-import           Data.List               (nub)+import           Control.Applicative      (Alternative(..))+import           Control.Exception        (Exception, SomeException,+                                           fromException, toException)+import           Control.Monad            (MonadPlus(..))+import           Control.Monad.Catch      (MonadCatch(..), MonadThrow(..))+import qualified Control.Monad.Conc.Class as C+import qualified Control.Monad.STM.Class  as S+import           Data.List                (nub) -import qualified Control.Monad.STM.Class as C import           Test.DejaFu.Internal import           Test.DejaFu.Types  #if MIN_VERSION_base(4,9,0)-import qualified Control.Monad.Fail      as Fail+import qualified Control.Monad.Fail       as Fail #endif  ----------------------------------------------------------------------------------- * The @S@ monad+-- * The @ModelSTM@ monad  -- | The underlying monad is based on continuations over primitive -- actions. -- -- This is not @Cont@ because we want to give it a custom @MonadFail@ -- instance.-newtype S n r a = S { runSTM :: (a -> STMAction n r) -> STMAction n r }+newtype ModelSTM n a = ModelSTM { runModelSTM :: (a -> STMAction n) -> STMAction n } -instance Functor (S n r) where-    fmap f m = S $ \c -> runSTM m (c . f)+instance Functor (ModelSTM n) where+    fmap f m = ModelSTM $ \c -> runModelSTM m (c . f) -instance Applicative (S n r) where-    pure x  = S $ \c -> c x-    f <*> v = S $ \c -> runSTM f (\g -> runSTM v (c . g))+instance Applicative (ModelSTM n) where+    pure x  = ModelSTM $ \c -> c x+    f <*> v = ModelSTM $ \c -> runModelSTM f (\g -> runModelSTM v (c . g)) -instance Monad (S n r) where+instance Monad (ModelSTM n) where     return  = pure-    m >>= k = S $ \c -> runSTM m (\x -> runSTM (k x) c)+    m >>= k = ModelSTM $ \c -> runModelSTM m (\x -> runModelSTM (k x) c)  #if MIN_VERSION_base(4,9,0)     fail = Fail.fail -instance Fail.MonadFail (S n r) where+instance Fail.MonadFail (ModelSTM n) where #endif-    fail e = S $ \_ -> SThrow (MonadFailException e)+    fail e = ModelSTM $ \_ -> SThrow (MonadFailException e) -instance MonadThrow (S n r) where-  throwM e = S $ \_ -> SThrow e+instance MonadThrow (ModelSTM n) where+  throwM e = ModelSTM $ \_ -> SThrow e -instance MonadCatch (S n r) where-  catch stm handler = S $ SCatch handler stm+instance MonadCatch (ModelSTM n) where+  catch stm handler = ModelSTM $ SCatch handler stm -instance Alternative (S n r) where-  a <|> b = S $ SOrElse a b-  empty = S $ const SRetry+instance Alternative (ModelSTM n) where+  a <|> b = ModelSTM $ SOrElse a b+  empty = ModelSTM $ const SRetry -instance MonadPlus (S n r)+instance MonadPlus (ModelSTM n) -instance C.MonadSTM (S n r) where-  type TVar (S n r) = TVar r+instance S.MonadSTM (ModelSTM n) where+  type TVar (ModelSTM n) = ModelTVar n -  newTVarN n = S . SNew n+  newTVarN n = ModelSTM . SNew n -  readTVar = S . SRead+  readTVar = ModelSTM . SRead -  writeTVar tvar a = S $ \c -> SWrite tvar a (c ())+  writeTVar tvar a = ModelSTM $ \c -> SWrite tvar a (c ())  -------------------------------------------------------------------------------- -- * Primitive actions  -- | STM transactions are represented as a sequence of primitive -- actions.-data STMAction n r-  = forall a e. Exception e => SCatch (e -> S n r a) (S n r a) (a -> STMAction n r)-  | forall a. SRead  (TVar r a) (a -> STMAction n r)-  | forall a. SWrite (TVar r a) a (STMAction n r)-  | forall a. SOrElse (S n r a) (S n r a) (a -> STMAction n r)-  | forall a. SNew String a (TVar r a -> STMAction n r)+data STMAction n+  = forall a e. Exception e => SCatch (e -> ModelSTM n a) (ModelSTM n a) (a -> STMAction n)+  | forall a. SRead  (ModelTVar n a) (a -> STMAction n)+  | forall a. SWrite (ModelTVar n a) a (STMAction n)+  | forall a. SOrElse (ModelSTM n a) (ModelSTM n a) (a -> STMAction n)+  | forall a. SNew String a (ModelTVar n a -> STMAction n)   | forall e. Exception e => SThrow e   | SRetry   | SStop (n ())@@ -102,10 +102,12 @@ -------------------------------------------------------------------------------- -- * @TVar@s --- | A 'TVar' is a tuple of a unique ID and the value contained. The--- ID is so that blocked transactions can be re-run when a 'TVar' they--- depend on has changed.-newtype TVar r a = TVar (TVarId, r a)+-- | A @TVar@ is modelled as a unique ID and a reference holding a+-- value.+data ModelTVar n a = ModelTVar+  { tvarId  :: TVarId+  , tvarRef :: C.CRef n a+  }  -------------------------------------------------------------------------------- -- * Output@@ -130,8 +132,8 @@  -- | Run a transaction, returning the result and new initial 'TVarId'. -- If the transaction failed, any effects are undone.-runTransaction :: MonadRef r n-  => S n r a+runTransaction :: C.MonadConc n+  => ModelSTM n a   -> IdSource   -> n (Result a, IdSource, [TAction]) runTransaction ma tvid = do@@ -142,14 +144,14 @@ -- -- If the transaction fails, its effects will automatically be undone, -- so the undo action returned will be @pure ()@.-doTransaction :: MonadRef r n-  => S n r a+doTransaction :: C.MonadConc n+  => ModelSTM n a   -> IdSource   -> n (Result a, n (), IdSource, [TAction]) doTransaction ma idsource = do-  (c, ref) <- runRefCont SStop (Just . Right) (runSTM ma)+  (c, ref) <- runRefCont SStop (Just . Right) (runModelSTM ma)   (idsource', undo, readen, written, trace) <- go ref c (pure ()) idsource [] [] []-  res <- readRef ref+  res <- C.readCRef ref    case res of     Just (Right val) -> pure (Success (nub readen) (nub written) val, undo, idsource', reverse trace)@@ -170,18 +172,18 @@       case tact of         TStop  -> pure (newIDSource, newUndo, newReaden, newWritten, TStop:newSofar)         TRetry -> do-          writeRef ref Nothing+          C.writeCRef ref Nothing           pure (newIDSource, newUndo, newReaden, newWritten, TRetry:newSofar)         TThrow -> do-          writeRef ref (Just . Left $ case act of SThrow e -> toException e; _ -> undefined)+          C.writeCRef ref (Just . Left $ case act of SThrow e -> toException e; _ -> undefined)           pure (newIDSource, newUndo, newReaden, newWritten, TThrow:newSofar)         _ -> go ref newAct newUndo newIDSource newReaden newWritten newSofar  -- | Run a transaction for one step.-stepTrans :: MonadRef r n-  => STMAction n r+stepTrans :: C.MonadConc n+  => STMAction n   -> IdSource-  -> n (STMAction n r, n (), IdSource, [TVarId], [TVarId], TAction)+  -> n (STMAction n, n (), IdSource, [TVarId], [TVarId], TAction) stepTrans act idsource = case act of   SCatch  h stm c -> stepCatch h stm c   SRead   ref c   -> stepRead ref c@@ -202,19 +204,19 @@         Just exc' -> transaction (TCatch trace . Just) (h exc') c         Nothing   -> pure (SThrow exc, nothing, idsource, [], [], TCatch trace Nothing)) -    stepRead (TVar (tvid, ref)) c = do-      val <- readRef ref-      pure (c val, nothing, idsource, [tvid], [], TRead tvid)+    stepRead ModelTVar{..} c = do+      val <- C.readCRef tvarRef+      pure (c val, nothing, idsource, [tvarId], [], TRead tvarId) -    stepWrite (TVar (tvid, ref)) a c = do-      old <- readRef ref-      writeRef ref a-      pure (c, writeRef ref old, idsource, [], [tvid], TWrite tvid)+    stepWrite ModelTVar{..} a c = do+      old <- C.readCRef tvarRef+      C.writeCRef tvarRef a+      pure (c, C.writeCRef tvarRef old, idsource, [], [tvarId], TWrite tvarId)      stepNew n a c = do       let (idsource', tvid) = nextTVId n idsource-      ref <- newRef a-      let tvar = TVar (tvid, ref)+      ref <- C.newCRef a+      let tvar = ModelTVar tvid ref       pure (c tvar, nothing, idsource', [], [tvid], TNew tvid)      stepOrElse a b c = cases TOrElse a c

@@ -13,10 +13,10 @@ -- form part of the public interface of this library. module Test.DejaFu.Conc.Internal.Threading where -import qualified Control.Concurrent.Classy        as C import           Control.Exception                (Exception, MaskingState(..),                                                    SomeException, fromException) import           Control.Monad                    (forever)+import qualified Control.Monad.Conc.Class         as C import           Data.List                        (intersect) import           Data.Map.Strict                  (Map) import qualified Data.Map.Strict                  as M@@ -30,34 +30,34 @@ -- * Threads  -- | Threads are stored in a map index by 'ThreadId'.-type Threads n r = Map ThreadId (Thread n r)+type Threads n = Map ThreadId (Thread n)  -- | All the state of a thread.-data Thread n r = Thread-  { _continuation :: Action n r+data Thread n = Thread+  { _continuation :: Action n   -- ^ The next action to execute.   , _blocking     :: Maybe BlockedOn   -- ^ The state of any blocks.-  , _handlers     :: [Handler n r]+  , _handlers     :: [Handler n]   -- ^ Stack of exception handlers   , _masking      :: MaskingState   -- ^ The exception masking state.-  , _bound        :: Maybe (BoundThread n r)+  , _bound        :: Maybe (BoundThread n)   -- ^ State for the associated bound thread, if it exists.   }  -- | The state of a bound thread.-data BoundThread n r = BoundThread-  { _runboundIO :: C.MVar n (n (Action n r))+data BoundThread n = BoundThread+  { _runboundIO :: C.MVar n (n (Action n))   -- ^ Run an @IO@ action in the bound thread by writing to this.-  , _getboundIO :: C.MVar n (Action n r)+  , _getboundIO :: C.MVar n (Action n)   -- ^ Get the result of the above by reading from this.   , _boundTId   :: C.ThreadId n   -- ^ Thread ID   }  -- | Construct a thread with just one action-mkthread :: Action n r -> Thread n r+mkthread :: Action n -> Thread n mkthread c = Thread c Nothing [] Unmasked Nothing  --------------------------------------------------------------------------------@@ -68,7 +68,7 @@ data BlockedOn = OnMVarFull MVarId | OnMVarEmpty MVarId | OnTVar [TVarId] | OnMask ThreadId deriving Eq  -- | Determine if a thread is blocked in a certain way.-(~=) :: Thread n r -> BlockedOn -> Bool+(~=) :: Thread n -> BlockedOn -> Bool thread ~= theblock = case (_blocking thread, theblock) of   (Just (OnMVarFull  _), OnMVarFull  _) -> True   (Just (OnMVarEmpty _), OnMVarEmpty _) -> True@@ -80,11 +80,11 @@ -- * Exceptions  -- | An exception handler.-data Handler n r = forall e. Exception e => Handler (e -> MaskingState -> Action n r)+data Handler n = forall e. Exception e => Handler (e -> MaskingState -> Action n)  -- | Propagate an exception upwards, finding the closest handler -- which can deal with it.-propagate :: SomeException -> ThreadId -> Threads n r -> Maybe (Threads n r)+propagate :: SomeException -> ThreadId -> Threads n -> Maybe (Threads n) propagate e tid threads = raise <$> propagate' handlers where   handlers = _handlers (elookup "propagate" tid threads) @@ -94,23 +94,25 @@   propagate' (Handler h:hs) = maybe (propagate' hs) (\act -> Just (act, hs)) $ h <$> fromException e  -- | Check if a thread can be interrupted by an exception.-interruptible :: Thread n r -> Bool-interruptible thread = _masking thread == Unmasked || (_masking thread == MaskedInterruptible && isJust (_blocking thread))+interruptible :: Thread n -> Bool+interruptible thread =+  _masking thread == Unmasked ||+  (_masking thread == MaskedInterruptible && isJust (_blocking thread))  -- | Register a new exception handler.-catching :: Exception e => (e -> Action n r) -> ThreadId -> Threads n r -> Threads n r+catching :: Exception e => (e -> Action n) -> ThreadId -> Threads n -> Threads n catching h = eadjust "catching" $ \thread ->   let ms0 = _masking thread       h'  = Handler $ \e ms -> (if ms /= ms0 then AResetMask False False ms0 else id) (h e)   in thread { _handlers = h' : _handlers thread }  -- | Remove the most recent exception handler.-uncatching :: ThreadId -> Threads n r -> Threads n r+uncatching :: ThreadId -> Threads n -> Threads n uncatching = eadjust "uncatching" $ \thread ->   thread { _handlers = etail "uncatching" (_handlers thread) }  -- | Raise an exception in a thread.-except :: (MaskingState -> Action n r) -> [Handler n r] -> ThreadId -> Threads n r -> Threads n r+except :: (MaskingState -> Action n) -> [Handler n] -> ThreadId -> Threads n -> Threads n except actf hs = eadjust "except" $ \thread -> thread   { _continuation = actf (_masking thread)   , _handlers = hs@@ -118,38 +120,38 @@   }  -- | Set the masking state of a thread.-mask :: MaskingState -> ThreadId -> Threads n r -> Threads n r+mask :: MaskingState -> ThreadId -> Threads n -> Threads n mask ms = eadjust "mask" $ \thread -> thread { _masking = ms }  -------------------------------------------------------------------------------- -- * Manipulating threads  -- | Replace the @Action@ of a thread.-goto :: Action n r -> ThreadId -> Threads n r -> Threads n r+goto :: Action n -> ThreadId -> Threads n -> Threads n goto a = eadjust "goto" $ \thread -> thread { _continuation = a }  -- | Start a thread with the given ID, inheriting the masking state -- from the parent thread. This ID must not already be in use!-launch :: ThreadId -> ThreadId -> ((forall b. M n r b -> M n r b) -> Action n r) -> Threads n r -> Threads n r+launch :: ThreadId -> ThreadId -> ((forall b. ModelConc n b -> ModelConc n b) -> Action n) -> Threads n -> Threads n launch parent tid a threads = launch' ms tid a threads where   ms = _masking (elookup "launch" parent threads)  -- | Start a thread with the given ID and masking state. This must not already be in use!-launch' :: MaskingState -> ThreadId -> ((forall b. M n r b -> M n r b) -> Action n r) -> Threads n r -> Threads n r+launch' :: MaskingState -> ThreadId -> ((forall b. ModelConc n b -> ModelConc n b) -> Action n) -> Threads n -> Threads n launch' ms tid a = einsert "launch'" tid thread where   thread = Thread (a umask) Nothing [] ms Nothing    umask mb = resetMask True Unmasked >> mb >>= \b -> resetMask False ms >> pure b-  resetMask typ m = cont $ \k -> AResetMask typ True m $ k ()+  resetMask typ m = ModelConc $ \k -> AResetMask typ True m $ k ()  -- | Block a thread.-block :: BlockedOn -> ThreadId -> Threads n r -> Threads n r+block :: BlockedOn -> ThreadId -> Threads n -> Threads n block blockedOn = eadjust "block" $ \thread -> thread { _blocking = Just blockedOn }  -- | Unblock all threads waiting on the appropriate block. For 'TVar' -- blocks, this will wake all threads waiting on at least one of the -- given 'TVar's.-wake :: BlockedOn -> Threads n r -> (Threads n r, [ThreadId])+wake :: BlockedOn -> Threads n -> (Threads n, [ThreadId]) wake blockedOn threads = (unblock <$> threads, M.keys $ M.filter isBlocked threads) where   unblock thread     | isBlocked thread = thread { _blocking = Nothing }@@ -163,7 +165,7 @@ -- ** Bound threads  -- | Turn a thread into a bound thread.-makeBound :: C.MonadConc n => ThreadId -> Threads n r -> n (Threads n r)+makeBound :: C.MonadConc n => ThreadId -> Threads n -> n (Threads n) makeBound tid threads = do     runboundIO <- C.newEmptyMVar     getboundIO <- C.newEmptyMVar@@ -178,7 +180,7 @@ -- | Kill a thread and remove it from the thread map. -- -- If the thread is bound, the worker thread is cleaned up.-kill :: C.MonadConc n => ThreadId -> Threads n r -> n (Threads n r)+kill :: C.MonadConc n => ThreadId -> Threads n -> n (Threads n) kill tid threads = do   let thread = elookup "kill" tid threads   maybe (pure ()) (C.killThread . _boundTId) (_bound thread)@@ -187,7 +189,7 @@ -- | Run an action. -- -- If the thread is bound, the action is run in the worker thread.-runLiftedAct :: C.MonadConc n => ThreadId -> Threads n r -> n (Action n r) -> n (Action n r)+runLiftedAct :: C.MonadConc n => ThreadId -> Threads n -> n (Action n) -> n (Action n) runLiftedAct tid threads ma = case _bound =<< M.lookup tid threads of   Just bt -> do     C.putMVar (_runboundIO bt) ma

@@ -15,15 +15,15 @@ -- library. module Test.DejaFu.Internal where -import           Control.DeepSeq    (NFData)-import           Control.Monad.Ref  (MonadRef(..))-import           Data.List.NonEmpty (NonEmpty(..))-import qualified Data.Map.Strict    as M-import           Data.Maybe         (fromMaybe)-import           Data.Set           (Set)-import qualified Data.Set           as S-import           GHC.Generics       (Generic)-import           System.Random      (RandomGen)+import           Control.DeepSeq          (NFData)+import qualified Control.Monad.Conc.Class as C+import           Data.List.NonEmpty       (NonEmpty(..))+import qualified Data.Map.Strict          as M+import           Data.Maybe               (fromMaybe)+import           Data.Set                 (Set)+import qualified Data.Set                 as S+import           GHC.Generics             (Generic)+import           System.Random            (RandomGen)  import           Test.DejaFu.Types @@ -155,50 +155,49 @@     tvarsOf' _ = []  -- | Convert a 'ThreadAction' into a 'Lookahead': \"rewind\" what has--- happened. 'Killed' has no 'Lookahead' counterpart.-rewind :: ThreadAction -> Maybe Lookahead-rewind (Fork _) = Just WillFork-rewind (ForkOS _) = Just WillForkOS-rewind (IsCurrentThreadBound _) = Just WillIsCurrentThreadBound-rewind MyThreadId = Just WillMyThreadId-rewind (GetNumCapabilities _) = Just WillGetNumCapabilities-rewind (SetNumCapabilities i) = Just (WillSetNumCapabilities i)-rewind Yield = Just WillYield-rewind (ThreadDelay n) = Just (WillThreadDelay n)-rewind (NewMVar _) = Just WillNewMVar-rewind (PutMVar c _) = Just (WillPutMVar c)-rewind (BlockedPutMVar c) = Just (WillPutMVar c)-rewind (TryPutMVar c _ _) = Just (WillTryPutMVar c)-rewind (ReadMVar c) = Just (WillReadMVar c)-rewind (BlockedReadMVar c) = Just (WillReadMVar c)-rewind (TryReadMVar c _) = Just (WillTryReadMVar c)-rewind (TakeMVar c _) = Just (WillTakeMVar c)-rewind (BlockedTakeMVar c) = Just (WillTakeMVar c)-rewind (TryTakeMVar c _ _) = Just (WillTryTakeMVar c)-rewind (NewCRef _) = Just WillNewCRef-rewind (ReadCRef c) = Just (WillReadCRef c)-rewind (ReadCRefCas c) = Just (WillReadCRefCas c)-rewind (ModCRef c) = Just (WillModCRef c)-rewind (ModCRefCas c) = Just (WillModCRefCas c)-rewind (WriteCRef c) = Just (WillWriteCRef c)-rewind (CasCRef c _) = Just (WillCasCRef c)-rewind (CommitCRef t c) = Just (WillCommitCRef t c)-rewind (STM _ _) = Just WillSTM-rewind (BlockedSTM _) = Just WillSTM-rewind Catching = Just WillCatching-rewind PopCatching = Just WillPopCatching-rewind Throw = Just WillThrow-rewind (ThrowTo t) = Just (WillThrowTo t)-rewind (BlockedThrowTo t) = Just (WillThrowTo t)-rewind Killed = Nothing-rewind (SetMasking b m) = Just (WillSetMasking b m)-rewind (ResetMasking b m) = Just (WillResetMasking b m)-rewind LiftIO = Just WillLiftIO-rewind Return = Just WillReturn-rewind Stop = Just WillStop-rewind Subconcurrency = Just WillSubconcurrency-rewind StopSubconcurrency = Just WillStopSubconcurrency-rewind (DontCheck _) = Just WillDontCheck+-- happened.+rewind :: ThreadAction -> Lookahead+rewind (Fork _) = WillFork+rewind (ForkOS _) = WillForkOS+rewind (IsCurrentThreadBound _) = WillIsCurrentThreadBound+rewind MyThreadId = WillMyThreadId+rewind (GetNumCapabilities _) = WillGetNumCapabilities+rewind (SetNumCapabilities i) = WillSetNumCapabilities i+rewind Yield = WillYield+rewind (ThreadDelay n) = WillThreadDelay n+rewind (NewMVar _) = WillNewMVar+rewind (PutMVar c _) = WillPutMVar c+rewind (BlockedPutMVar c) = WillPutMVar c+rewind (TryPutMVar c _ _) = WillTryPutMVar c+rewind (ReadMVar c) = WillReadMVar c+rewind (BlockedReadMVar c) = WillReadMVar c+rewind (TryReadMVar c _) = WillTryReadMVar c+rewind (TakeMVar c _) = WillTakeMVar c+rewind (BlockedTakeMVar c) = WillTakeMVar c+rewind (TryTakeMVar c _ _) = WillTryTakeMVar c+rewind (NewCRef _) = WillNewCRef+rewind (ReadCRef c) = WillReadCRef c+rewind (ReadCRefCas c) = WillReadCRefCas c+rewind (ModCRef c) = WillModCRef c+rewind (ModCRefCas c) = WillModCRefCas c+rewind (WriteCRef c) = WillWriteCRef c+rewind (CasCRef c _) = WillCasCRef c+rewind (CommitCRef t c) = WillCommitCRef t c+rewind (STM _ _) = WillSTM+rewind (BlockedSTM _) = WillSTM+rewind Catching = WillCatching+rewind PopCatching = WillPopCatching+rewind Throw = WillThrow+rewind (ThrowTo t) = WillThrowTo t+rewind (BlockedThrowTo t) = WillThrowTo t+rewind (SetMasking b m) = WillSetMasking b m+rewind (ResetMasking b m) = WillResetMasking b m+rewind LiftIO = WillLiftIO+rewind Return = WillReturn+rewind Stop = WillStop+rewind Subconcurrency = WillSubconcurrency+rewind StopSubconcurrency = WillStopSubconcurrency+rewind (DontCheck _) = WillDontCheck  -- | Check if an operation could enable another thread. willRelease :: Lookahead -> Bool@@ -303,7 +302,7 @@ -- This is used in the SCT code to help determine interesting -- alternative scheduling decisions. simplifyAction :: ThreadAction -> ActionType-simplifyAction = maybe UnsynchronisedOther simplifyLookahead . rewind+simplifyAction = simplifyLookahead . rewind  -- | Variant of 'simplifyAction' that takes a 'Lookahead'. simplifyLookahead :: Lookahead -> ActionType@@ -383,8 +382,12 @@ -- | Run with a continuation that writes its value into a reference, -- returning the computation and the reference.  Using the reference -- is non-blocking, it is up to you to ensure you wait sufficiently.-runRefCont :: MonadRef r n => (n () -> x) -> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, r (Maybe b))+runRefCont :: C.MonadConc n+  => (n () -> x)+  -> (a -> Maybe b)+  -> ((a -> x) -> x)+  -> n (x, C.CRef n (Maybe b)) runRefCont act f k = do-  ref <- newRef Nothing-  let c = k (act . writeRef ref . f)+  ref <- C.newCRef Nothing+  let c = k (act . C.writeCRef ref . f)   pure (c, ref)

@@ -37,7 +37,6 @@ import           Control.Applicative               ((<|>)) import           Control.DeepSeq                   (NFData(..), force) import           Control.Monad.Conc.Class          (MonadConc)-import           Control.Monad.Ref                 (MonadRef) import           Data.List                         (foldl') import qualified Data.Map.Strict                   as M import           Data.Maybe                        (fromMaybe)@@ -64,12 +63,12 @@ -- found, is unspecified and may change between releases. -- -- @since 1.0.0.0-runSCT :: (MonadConc n, MonadRef r n)+runSCT :: MonadConc n   => Way   -- ^ How to run the concurrent program.   -> MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to run many times.   -> n [(Either Failure a, Trace)] runSCT way = runSCTWithSettings . fromWayAndMemType way@@ -77,12 +76,12 @@ -- | Return the set of results of a concurrent program. -- -- @since 1.0.0.0-resultsSet :: (MonadConc n, MonadRef r n, Ord a)+resultsSet :: (MonadConc n, Ord a)   => Way   -- ^ How to run the concurrent program.   -> MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to run many times.   -> n (Set (Either Failure a)) resultsSet way = resultsSetWithSettings . fromWayAndMemType way@@ -93,14 +92,14 @@ -- found, is unspecified and may change between releases. -- -- @since 1.0.0.0-runSCTDiscard :: (MonadConc n, MonadRef r n)+runSCTDiscard :: MonadConc n   => (Either Failure a -> Maybe Discard)   -- ^ Selectively discard results.   -> Way   -- ^ How to run the concurrent program.   -> MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to run many times.   -> n [(Either Failure a, Trace)] runSCTDiscard discard way = runSCTWithSettings . set ldiscard (Just discard) . fromWayAndMemType way@@ -109,14 +108,14 @@ -- | A variant of 'resultsSet' which can selectively discard results. -- -- @since 1.0.0.0-resultsSetDiscard :: (MonadConc n, MonadRef r n, Ord a)+resultsSetDiscard :: (MonadConc n, Ord a)   => (Either Failure 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 @CRef@ operations.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to run many times.   -> n (Set (Either Failure a)) resultsSetDiscard discard way memtype conc =@@ -133,8 +132,8 @@ -- found, is unspecified and may change between releases. -- -- @since 1.0.0.0-runSCT' :: (MonadConc n, MonadRef r n, NFData a)-  => Way -> MemType -> ConcT r n a -> n [(Either Failure a, Trace)]+runSCT' :: (MonadConc n, NFData a)+  => Way -> MemType -> ConcT n a -> n [(Either Failure a, Trace)] runSCT' way = runSCTWithSettings' . fromWayAndMemType way  -- | A strict variant of 'resultsSet'.@@ -143,8 +142,8 @@ -- may be more efficient in some situations. -- -- @since 1.0.0.0-resultsSet' :: (MonadConc n, MonadRef r n, Ord a, NFData a)-  => Way -> MemType -> ConcT r n a -> n (Set (Either Failure a))+resultsSet' :: (MonadConc n, Ord a, NFData a)+  => Way -> MemType -> ConcT n a -> n (Set (Either Failure a)) resultsSet' way = resultsSetWithSettings' . fromWayAndMemType way  -- | A strict variant of 'runSCTDiscard'.@@ -156,8 +155,8 @@ -- found, is unspecified and may change between releases. -- -- @since 1.0.0.0-runSCTDiscard' :: (MonadConc n, MonadRef r n, NFData a)-  => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT r n a -> n [(Either Failure a, Trace)]+runSCTDiscard' :: (MonadConc n, NFData a)+  => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT n a -> n [(Either Failure a, Trace)] runSCTDiscard' discard way memtype conc = do   res <- runSCTDiscard discard way memtype conc   rnf res `seq` pure res@@ -169,8 +168,8 @@ -- may be more efficient in some situations. -- -- @since 1.0.0.0-resultsSetDiscard' :: (MonadConc n, MonadRef r n, Ord a, NFData a)-  => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT r n a -> n (Set (Either Failure a))+resultsSetDiscard' :: (MonadConc n, Ord a, NFData a)+  => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT n a -> n (Set (Either Failure a)) resultsSetDiscard' discard way memtype conc = do   res <- resultsSetDiscard discard way memtype conc   rnf res `seq` pure res@@ -185,10 +184,10 @@ -- found, is unspecified and may change between releases. -- -- @since 1.2.0.0-runSCTWithSettings :: (MonadConc n, MonadRef r n)+runSCTWithSettings :: MonadConc n   => Settings n a   -- ^ The SCT settings.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to run many times.   -> n [(Either Failure a, Trace)] runSCTWithSettings settings conc = case _way settings of@@ -240,10 +239,10 @@ -- | A variant of 'resultsSet' which takes a 'Settings' record. -- -- @since 1.2.0.0-resultsSetWithSettings :: (MonadConc n, MonadRef r n, Ord a)+resultsSetWithSettings :: (MonadConc n, Ord a)   => Settings n a   -- ^ The SCT settings.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to run many times.   -> n (Set (Either Failure a)) resultsSetWithSettings settings conc =@@ -259,9 +258,9 @@ -- found, is unspecified and may change between releases. -- -- @since 1.2.0.0-runSCTWithSettings' :: (MonadConc n, MonadRef r n, NFData a)+runSCTWithSettings' :: (MonadConc n, NFData a)   => Settings n a-  -> ConcT r n a+  -> ConcT n a   -> n [(Either Failure a, Trace)] runSCTWithSettings' settings conc = do   res <- runSCTWithSettings settings conc@@ -273,9 +272,9 @@ -- may be more efficient in some situations. -- -- @since 1.2.0.0-resultsSetWithSettings' :: (MonadConc n, MonadRef r n, Ord a, NFData a)+resultsSetWithSettings' :: (MonadConc n, Ord a, NFData a)   => Settings n a-  -> ConcT r n a+  -> ConcT n a   -> n (Set (Either Failure a)) resultsSetWithSettings' settings conc = do   res <- resultsSetWithSettings settings conc@@ -384,12 +383,12 @@ -- found, is unspecified and may change between releases. -- -- @since 1.0.0.0-sctBound :: (MonadConc n, MonadRef r n)+sctBound :: MonadConc n   => MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.   -> Bounds   -- ^ The combined bounds.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to run many times   -> n [(Either Failure a, Trace)] sctBound = sctBoundDiscard (const Nothing)@@ -401,14 +400,14 @@ -- found, is unspecified and may change between releases. -- -- @since 1.0.0.0-sctBoundDiscard :: (MonadConc n, MonadRef r n)+sctBoundDiscard :: MonadConc n   => (Either Failure a -> Maybe Discard)   -- ^ Selectively discard results.   -> MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.   -> Bounds   -- ^ The combined bounds.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to run many times   -> n [(Either Failure a, Trace)] sctBoundDiscard discard memtype cb = runSCTWithSettings $@@ -423,14 +422,14 @@ -- This is not guaranteed to find all distinct results. -- -- @since 1.0.0.0-sctUniformRandom :: (MonadConc n, MonadRef r n, RandomGen g)+sctUniformRandom :: (MonadConc n, RandomGen g)   => MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.   -> g   -- ^ The random number generator.   -> Int   -- ^ The number of executions to perform.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to run many times.   -> n [(Either Failure a, Trace)] sctUniformRandom = sctUniformRandomDiscard (const Nothing)@@ -442,7 +441,7 @@ -- This is not guaranteed to find all distinct results. -- -- @since 1.0.0.0-sctUniformRandomDiscard :: (MonadConc n, MonadRef r n, RandomGen g)+sctUniformRandomDiscard :: (MonadConc n, RandomGen g)   => (Either Failure a -> Maybe Discard)   -- ^ Selectively discard results.   -> MemType@@ -451,7 +450,7 @@   -- ^ The random number generator.   -> Int   -- ^ The number of executions to perform.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to run many times.   -> n [(Either Failure a, Trace)] sctUniformRandomDiscard discard memtype g lim = runSCTWithSettings $@@ -466,7 +465,7 @@ -- This is not guaranteed to find all distinct results. -- -- @since 1.0.0.0-sctWeightedRandom :: (MonadConc n, MonadRef r n, RandomGen g)+sctWeightedRandom :: (MonadConc n, RandomGen g)   => MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.   -> g@@ -475,7 +474,7 @@   -- ^ The number of executions to perform.   -> Int   -- ^ The number of executions to use the same set of weights for.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to run many times.   -> n [(Either Failure a, Trace)] sctWeightedRandom = sctWeightedRandomDiscard (const Nothing)@@ -487,7 +486,7 @@ -- This is not guaranteed to find all distinct results. -- -- @since 1.0.0.0-sctWeightedRandomDiscard :: (MonadConc n, MonadRef r n, RandomGen g)+sctWeightedRandomDiscard :: (MonadConc n, RandomGen g)   => (Either Failure a -> Maybe Discard)   -- ^ Selectively discard results.   -> MemType@@ -498,7 +497,7 @@   -- ^ The number of executions to perform.   -> Int   -- ^ The number of executions to use the same set of weights for.-  -> ConcT r n a+  -> ConcT n a   -- ^ The computation to run many times.   -> n [(Either Failure a, Trace)] sctWeightedRandomDiscard discard memtype g lim use = runSCTWithSettings $

@@ -16,7 +16,6 @@ module Test.DejaFu.SCT.Internal where  import           Control.Monad.Conc.Class         (MonadConc)-import           Control.Monad.Ref                (MonadRef) import           Data.Coerce                      (Coercible, coerce) import qualified Data.IntMap.Strict               as I import           Data.List                        (find, mapAccumL)@@ -35,7 +34,7 @@ -- * Exploration  -- | General-purpose SCT function.-sct :: (MonadConc n, MonadRef r n)+sct :: MonadConc n   => Settings n a   -- ^ The SCT settings ('Way' is ignored)   -> ([ThreadId] -> s)@@ -44,7 +43,7 @@   -- ^ State predicate   -> ((Scheduler g -> g -> n (Either Failure a, g, Trace)) -> s -> t -> n (s, Maybe (Either Failure a, Trace)))   -- ^ Run the computation and update the state-  -> ConcT r n a+  -> ConcT n a   -> n [(Either Failure a, Trace)] sct settings s0 sfun srun conc     | canDCSnapshot conc = runForDCSnapshot conc >>= \case@@ -80,7 +79,7 @@     debugPrint = fromMaybe (const (pure ())) (_debugPrint settings)  -- | Like 'sct' but given a function to run the computation.-sct' :: (MonadConc n, MonadRef r n)+sct' :: MonadConc n   => Settings n a   -- ^ The SCT settings ('Way' is ignored)   -> s@@ -147,7 +146,7 @@ -- Unlike shrinking in randomised property-testing tools like -- QuickCheck or Hedgehog, we only run the test case /once/, at the -- end, rather than after every simplification step.-simplifyExecution :: (MonadConc n, MonadRef r n)+simplifyExecution :: MonadConc n   => Settings n a   -- ^ The SCT settings ('Way' is ignored)   -> (forall x. Scheduler x -> x -> n (Either Failure a, x, Trace))@@ -185,7 +184,7 @@     p = either show debugShow  -- | Replay an execution.-replay :: (MonadConc n, MonadRef r n)+replay :: MonadConc n   => (forall x. Scheduler x -> x -> n (Either Failure a, x, Trace))   -- ^ Run the computation   -> [(ThreadId, ThreadAction)]

@@ -578,6 +578,8 @@   -- actually blocked. 'dependent'' has to assume that all   -- potentially-blocking operations can block, and so is more   -- pessimistic in this case.+  (ThrowTo t, ThrowTo u)+    | t == t2 && u == t1 -> canInterrupt ds t1 a1 || canInterrupt ds t2 a2   (ThrowTo t, _) | t == t2 -> canInterrupt ds t2 a2 && a2 /= Stop   (_, ThrowTo t) | t == t1 -> canInterrupt ds t1 a1 && a1 /= Stop @@ -589,9 +591,8 @@   (BlockedSTM _, STM _ _)      -> checkSTM   (BlockedSTM _, BlockedSTM _) -> checkSTM -  _ -> case (,) <$> rewind a1 <*> rewind a2 of-    Just (l1, l2) -> dependent' ds t1 a1 t2 l2 && dependent' ds t2 a2 t1 l1-    _ -> dependentActions ds (simplifyAction a1) (simplifyAction a2)+  _ -> dependent' ds t1 a1 t2 (rewind a2)+    && dependent' ds t2 a2 t1 (rewind a1)    where     -- STM actions A and B are dependent if A wrote to anything B@@ -612,6 +613,8 @@   -- thread and if the actions can be interrupted. We can also   -- slightly improve on that by not considering interrupting the   -- normal termination of a thread: it doesn't make a difference.+  (ThrowTo t, WillThrowTo u)+    | t == t2 && u == t1 -> canInterrupt ds t1 a1 || canInterruptL ds t2 l2   (ThrowTo t, _)     | t == t2 -> canInterruptL ds t2 l2 && l2 /= WillStop   (_, WillThrowTo t) | t == t1 -> canInterrupt  ds t1 a1 && a1 /= Stop 

@@ -104,7 +104,7 @@  -- | All the actions that a thread can perform. ----- @since 1.1.0.0+-- @since 1.4.0.0 data ThreadAction =     Fork ThreadId   -- ^ Start a new thread.@@ -175,8 +175,6 @@   -- ^ Throw an exception to a thread.   | BlockedThrowTo ThreadId   -- ^ Get blocked on a 'throwTo'.-  | Killed-  -- ^ Killed by an uncaught exception.   | SetMasking Bool MaskingState   -- ^ Set the masking state. If 'True', this is being used to set the   -- masking state to the original state in the argument passed to a@@ -238,7 +236,6 @@   rnf Throw = ()   rnf (ThrowTo t) = rnf t   rnf (BlockedThrowTo t) = rnf t-  rnf Killed = ()   rnf (SetMasking b m) = rnf (b, show m)   rnf (ResetMasking b m) = rnf (b, show m)   rnf LiftIO = ()

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                dejafu-version:             1.3.2.0+version:             1.4.0.0 synopsis:            A library for unit-testing concurrent programs.  description:@@ -33,7 +33,7 @@ source-repository this   type:     git   location: https://github.com/barrucadu/dejafu.git-  tag:      dejafu-1.3.2.0+  tag:      dejafu-1.4.0.0  library   exposed-modules:     Test.DejaFu@@ -66,7 +66,6 @@                      , leancheck         >=0.6 && <0.8                      , profunctors       >=4.0 && <6.0                      , random            >=1.0 && <1.2-                     , ref-fd            >=0.4 && <0.5                      , transformers      >=0.4 && <0.6   -- hs-source-dirs:         default-language:    Haskell2010