dejafu 2.0.0.1 → 2.1.0.0

raw patch · 13 files changed

+395/−223 lines, 13 filesdep ~concurrencyPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: concurrency

API changes (from Hackage documentation)

Files

• CHANGELOG.rst +61/−0
• Test/DejaFu.hs +34/−36
• Test/DejaFu/Conc/Internal.hs +53/−37
• Test/DejaFu/Conc/Internal/Common.hs +5/−3
• Test/DejaFu/Conc/Internal/Memory.hs +28/−29
• Test/DejaFu/Conc/Internal/Program.hs +15/−17
• Test/DejaFu/Conc/Internal/STM.hs +21/−22
• Test/DejaFu/Conc/Internal/Threading.hs +11/−32
• Test/DejaFu/Internal.hs +16/−16
• Test/DejaFu/SCT.hs +16/−19
• Test/DejaFu/SCT/Internal.hs +5/−6
• Test/DejaFu/Types.hs +126/−2
• dejafu.cabal +4/−4

@@ -6,6 +6,67 @@  .. _PVP: https://pvp.haskell.org/ ++2.1.0.0 (2019-03-24)+--------------------++* Git: :tag:`dejafu-2.1.0.0`+* Hackage: :hackage:`dejafu-2.1.0.0`++Added+~~~~~++* The ``Test.DejaFu.Types.MonadDejaFu`` typeclass, containing the+  primitives needed to run a concurrent program.  There are instances+  for:+    * ``IO``, which is probably the ``MonadConc`` instance people used+      previously, so there is no breaking change there.+    * ``CatchT (ST t)``, meaning that concurrent programs can be run+      without ``IO`` once more.++* Thread action constructors for ``MonadConc``+  ``supportsBoundThreads`` function:+    * ``Test.DejaFu.Types.ThreadAction``, ``SupportsBoundThreads``+    * ``Test.DejaFu.Types.Lookahead``, ``WillSupportsBoundThreads``++Changed+~~~~~~~++* Many functions which had a ``MonadConc`` constraint now have a+  ``MonadDejaFu`` constraint:+    * In ``Test.DejaFu``+        * ``autocheck``+        * ``autocheckWay``+        * ``autocheckWithSettings``+        * ``dejafu``+        * ``dejafuWay``+        * ``dejafuWithSettings``+        * ``dejafus``+        * ``dejafusWay``+        * ``dejafusWithSettings``+        * ``runTest``+        * ``runTestWay``+        * ``runTestWithSettings``+    * In ``Test.DejaFu.Conc``+        * ``runConcurrent``+        * ``recordSnapshot``+        * ``runSnapshot``+    * In ``Test.DejaFu.SCT``+        * ``runSCT``+        * ``resultsSet``+        * ``runSCT'``+        * ``resultsSet'``+        * ``runSCTWithSettings``+        * ``resultsSetWithSettings``+        * ``runSCTWithSettings'``+        * ``resultsSetWithSettings'``++Miscellaneous+~~~~~~~~~~~~~++* The version bound on :hackage:`concurrency` is >=1.7 and <1.8.++ 2.0.0.1 (2019-03-14) -------------------- 

@@ -313,18 +313,16 @@   , inspectTVar ) where -import           Control.Arrow            (first)-import           Control.DeepSeq          (NFData(..))-import           Control.Monad            (unless, when)-import           Control.Monad.Conc.Class (MonadConc)-import           Control.Monad.IO.Class   (MonadIO(..))-import           Data.Either              (isLeft)-import           Data.Function            (on)-import           Data.List                (intercalate, intersperse, partition)-import           Data.Maybe               (catMaybes, isJust, isNothing,-                                           mapMaybe)-import           Data.Profunctor          (Profunctor(..))-import           System.Environment       (lookupEnv)+import           Control.Arrow          (first)+import           Control.DeepSeq        (NFData(..))+import           Control.Monad          (unless, when)+import           Control.Monad.IO.Class (MonadIO(..))+import           Data.Either            (isLeft)+import           Data.Function          (on)+import           Data.List              (intercalate, intersperse, partition)+import           Data.Maybe             (catMaybes, isJust, isNothing, mapMaybe)+import           Data.Profunctor        (Profunctor(..))+import           System.Environment     (lookupEnv)  import           Test.DejaFu.Conc import           Test.DejaFu.Internal@@ -373,8 +371,8 @@ --     "world" S0----S2--S0-- -- False ----- @since 2.0.0.0-autocheck :: (MonadConc n, MonadIO n, Eq a, Show a)+-- @since 2.1.0.0+autocheck :: (MonadDejaFu n, MonadIO n, Eq a, Show a)   => Program pty n a   -- ^ The computation to test.   -> n Bool@@ -405,8 +403,8 @@ --     (True,False) S0---------S2----S1----S0--- -- False ----- @since 2.0.0.0-autocheckWay :: (MonadConc n, MonadIO n, Eq a, Show a)+-- @since 2.1.0.0+autocheckWay :: (MonadDejaFu n, MonadIO n, Eq a, Show a)   => Way   -- ^ How to run the concurrent program.   -> MemType@@ -440,8 +438,8 @@ --     (True,False) S0---------S2----S1----S0--- -- False ----- @since 2.0.0.0-autocheckWithSettings :: (MonadConc n, MonadIO n, Eq a, Show a)+-- @since 2.1.0.0+autocheckWithSettings :: (MonadDejaFu n, MonadIO n, Eq a, Show a)   => Settings n a   -- ^ The SCT settings.   -> Program pty n a@@ -466,8 +464,8 @@ --     "world" S0----S2--S0-- -- False ----- @since 2.0.0.0-dejafu :: (MonadConc n, MonadIO n, Show b)+-- @since 2.1.0.0+dejafu :: (MonadDejaFu n, MonadIO n, Show b)   => String   -- ^ The name of the test.   -> ProPredicate a b@@ -496,8 +494,8 @@ --     "world" S0----S2--S1-S0-- -- False ----- @since 2.0.0.0-dejafuWay :: (MonadConc n, MonadIO n, Show b)+-- @since 2.1.0.0+dejafuWay :: (MonadDejaFu n, MonadIO n, Show b)   => Way   -- ^ How to run the concurrent program.   -> MemType@@ -522,8 +520,8 @@ --     "world" S0----S2--S1-S0-- -- False ----- @since 2.0.0.0-dejafuWithSettings :: (MonadConc n, MonadIO n, Show b)+-- @since 2.1.0.0+dejafuWithSettings :: (MonadDejaFu n, MonadIO n, Show b)   => Settings n a   -- ^ The SCT settings.   -> String@@ -547,8 +545,8 @@ -- [pass] B -- False ----- @since 2.0.0.0-dejafus :: (MonadConc n, MonadIO n, Show b)+-- @since 2.1.0.0+dejafus :: (MonadDejaFu n, MonadIO n, Show b)   => [(String, ProPredicate a b)]   -- ^ The list of predicates (with names) to check.   -> Program pty n a@@ -569,8 +567,8 @@ -- [pass] B -- False ----- @since 2.0.0.0-dejafusWay :: (MonadConc n, MonadIO n, Show b)+-- @since 2.1.0.0+dejafusWay :: (MonadDejaFu n, MonadIO n, Show b)   => Way   -- ^ How to run the concurrent program.   -> MemType@@ -594,8 +592,8 @@ -- [pass] B -- False ----- @since 2.0.0.0-dejafusWithSettings :: (MonadConc n, MonadIO n, Show b)+-- @since 2.1.0.0+dejafusWithSettings :: (MonadDejaFu n, MonadIO n, Show b)   => Settings n a   -- ^ The SCT settings.   -> [(String, ProPredicate a b)]@@ -670,8 +668,8 @@ -- found, is unspecified and may change between releases.  This may -- affect which failing traces are reported, when there is a failure. ----- @since 2.0.0.0-runTest :: MonadConc n+-- @since 2.1.0.0+runTest :: MonadDejaFu n   => ProPredicate a b   -- ^ The predicate to check   -> Program pty n a@@ -686,8 +684,8 @@ -- found, is unspecified and may change between releases.  This may -- affect which failing traces are reported, when there is a failure. ----- @since 2.0.0.0-runTestWay :: MonadConc n+-- @since 2.1.0.0+runTestWay :: MonadDejaFu n   => Way   -- ^ How to run the concurrent program.   -> MemType@@ -705,8 +703,8 @@ -- found, is unspecified and may change between releases.  This may -- affect which failing traces are reported, when there is a failure. ----- @since 2.0.0.0-runTestWithSettings :: MonadConc n+-- @since 2.1.0.0+runTestWithSettings :: MonadDejaFu n   => Settings n a   -- ^ The SCT settings.   -> ProPredicate a b

@@ -3,14 +3,15 @@ {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}  -- | -- Module      : Test.DejaFu.Conc.Internal--- Copyright   : (c) 2016--2018 Michael Walker+-- Copyright   : (c) 2016--2019 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : FlexibleContexts, LambdaCase, MultiWayIf, RankNTypes, RecordWildCards+-- Portability : FlexibleContexts, LambdaCase, MultiWayIf, RankNTypes, RecordWildCards, ScopedTypeVariables -- -- Concurrent monads with a fixed scheduler: internal types and -- functions. This module is NOT considered to form part of the public@@ -21,7 +22,6 @@                                                       MaskingState(..),                                                       toException) import qualified Control.Monad.Catch                 as E-import qualified Control.Monad.Conc.Class            as C import           Data.Foldable                       (foldrM) import           Data.Functor                        (void) import           Data.List                           (nub, partition, sortOn)@@ -50,7 +50,7 @@ -- | The result of running a concurrent program. data CResult n g a = CResult   { finalContext :: Context n g-  , finalRef :: C.IORef n (Maybe (Either Condition a))+  , finalRef :: Ref n (Maybe (Either Condition a))   , finalRestore :: Threads n -> n ()   -- ^ Meaningless if this result doesn't come from a snapshotting   -- execution.@@ -61,7 +61,7 @@ -- | Run a concurrent computation with a given 'Scheduler' and initial -- state, returning a Condition reason on error. Also returned is the -- final state of the scheduler, and an execution trace.-runConcurrency :: (C.MonadConc n, HasCallStack)+runConcurrency :: (MonadDejaFu n, HasCallStack)   => [Invariant n ()]   -> Bool   -> Scheduler g@@ -83,13 +83,15 @@                     }   (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+  threads <- case forkBoundThread of+    Just fbt -> makeBound fbt initialThread threads0+    Nothing  -> pure threads0   res <- runThreads forSnapshot sched memtype ref ctx { cThreads = threads }   killAllThreads (finalContext res)   pure res  -- | Like 'runConcurrency' but starts from a snapshot.-runConcurrencyWithSnapshot :: (C.MonadConc n, HasCallStack)+runConcurrencyWithSnapshot :: (MonadDejaFu n, HasCallStack)   => Scheduler g   -> MemType   -> Context n g@@ -100,16 +102,19 @@   (c, ref) <- runRefCont AStop (Just . Right) (runModelConc ma)   let threads0 = M.delete initialThread (cThreads ctx)   let threads1 = launch' Unmasked initialThread (const c) threads0-  let boundThreads = M.filter (isJust . _bound) threads1-  threads2 <- (if C.rtsSupportsBoundThreads then makeBound initialThread else pure) threads1-  threads3 <- foldrM makeBound threads2 (M.keys boundThreads)-  restore threads3-  res <- runThreads False sched memtype ref ctx { cThreads = threads3 }+  threads <- case forkBoundThread of+    Just fbt -> do+      let boundThreads = M.filter (isJust . _bound) threads1+      threads' <- makeBound fbt initialThread threads1+      foldrM (makeBound fbt) threads' (M.keys boundThreads)+    Nothing -> pure threads1+  restore threads+  res <- runThreads False sched memtype ref ctx { cThreads = threads }   killAllThreads (finalContext res)   pure res  -- | Kill the remaining threads-killAllThreads :: (C.MonadConc n, HasCallStack) => Context n g -> n ()+killAllThreads :: (MonadDejaFu n, HasCallStack) => Context n g -> n () killAllThreads ctx =   let finalThreads = cThreads ctx   in mapM_ (`kill` finalThreads) (M.keys finalThreads)@@ -130,17 +135,17 @@   }  -- | Run a collection of threads, until there are no threads left.-runThreads :: (C.MonadConc n, HasCallStack)+runThreads :: (MonadDejaFu n, HasCallStack)   => Bool   -> Scheduler g   -> MemType-  -> C.IORef n (Maybe (Either Condition a))+  -> Ref n (Maybe (Either Condition 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.writeIORef ref (Just $ Left reason)+    writeRef ref (Just $ Left reason)     stop finalR finalT finalD finalC    -- just terminate; 'ref' must have been written to before calling@@ -256,7 +261,7 @@ -- -- Note: the returned snapshot action will definitely not do the right -- thing with relaxed memory.-stepThread :: (C.MonadConc n, HasCallStack)+stepThread :: forall n g. (MonadDejaFu n, HasCallStack)   => Bool   -- ^ Should we record a snapshot?   -> Bool@@ -282,12 +287,23 @@      )  -- 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' }-       , ForkOS newtid+stepThread _ _ _ _ tid (AForkOS n a b) = \ctx@Context{..} -> case forkBoundThread of+  Just fbt -> do+    let (idSource', newtid) = nextTId n cIdSource+    let threads' = launch tid newtid a cThreads+    threads'' <- makeBound fbt newtid threads'+    pure ( Succeeded ctx { cThreads = goto (b newtid) tid threads'', cIdSource = idSource' }+         , ForkOS newtid+         , const (pure ())+         )+  Nothing ->+    stepThrow Throw tid (MonadFailException "dejafu is running with bound threads disabled - do not use forkOS") ctx++-- check if we support bound threads+stepThread _ _ _ _ tid (ASupportsBoundThreads c) = \ctx@Context{..} -> do+  let sbt = isJust (forkBoundThread :: Maybe (n (BoundThread n ())))+  pure ( Succeeded ctx { cThreads = goto (c sbt) tid cThreads }+       , SupportsBoundThreads sbt        , const (pure ())        ) @@ -337,11 +353,11 @@ -- create a new @MVar@, using the next 'MVarId'. stepThread _ _ _ _ tid (ANewMVar n c) = \ctx@Context{..} -> do   let (idSource', newmvid) = nextMVId n cIdSource-  ref <- C.newIORef Nothing+  ref <- newRef Nothing   let mvar = ModelMVar newmvid ref   pure ( Succeeded ctx { cThreads = goto (c mvar) tid cThreads, cIdSource = idSource' }        , NewMVar newmvid-       , const (C.writeIORef ref Nothing)+       , const (writeRef ref Nothing)        )  -- put a value into a @MVar@, blocking the thread until it's empty.@@ -398,11 +414,11 @@ stepThread _ _ _ _  tid (ANewIORef n a c) = \ctx@Context{..} -> do   let (idSource', newiorid) = nextIORId n cIdSource   let val = (M.empty, 0, a)-  ioref <- C.newIORef val+  ioref <- newRef val   let ref = ModelIORef newiorid ioref   pure ( Succeeded ctx { cThreads = goto (c ref) tid cThreads, cIdSource = idSource' }        , NewIORef newiorid-       , const (C.writeIORef ioref val)+       , const (writeRef ioref val)        )  -- read from a @IORef@.@@ -609,7 +625,7 @@  -- | Handle an exception being thrown from an @AAtom@, @AThrow@, or -- @AThrowTo@.-stepThrow :: (C.MonadConc n, Exception e)+stepThrow :: (MonadDejaFu n, Exception e)   => (Bool -> ThreadAction)   -- ^ Action to include in the trace.   -> ThreadId@@ -641,7 +657,7 @@     some = toException e  -- | Helper for actions impose a write barrier.-synchronised :: C.MonadConc n+synchronised :: MonadDejaFu n   => (Context n g -> n x)   -- ^ Action to run after the write barrier.   -> Context n g@@ -674,7 +690,7 @@  -- | Check all active invariants, returning an arbitrary failure if -- multiple ones fail.-checkInvariants :: C.MonadConc n+checkInvariants :: MonadDejaFu n   => InvariantContext n   -> n (Either E.SomeException (InvariantContext n)) checkInvariants ic = go (icActive ic) >>= \case@@ -687,7 +703,7 @@     go [] = pure (Right [])  -- | Check an invariant.-checkInvariant :: C.MonadConc n+checkInvariant :: MonadDejaFu n   => Invariant n a   -> n (Either E.SomeException ([IORefId], [MVarId], [TVarId])) checkInvariant inv = doInvariant inv >>= \case@@ -695,13 +711,13 @@   (Left exc, _, _, _) -> pure (Left exc)  -- | Run an invariant (more primitive)-doInvariant :: C.MonadConc n+doInvariant :: MonadDejaFu n   => Invariant n a   -> n (Either E.SomeException a, [IORefId], [MVarId], [TVarId]) doInvariant inv = do     (c, ref) <- runRefCont IStop (Just . Right) (runInvariant inv)     (iorefs, mvars, tvars) <- go ref c [] [] []-    val <- C.readIORef ref+    val <- readRef ref     pure (efromJust val, nub iorefs, nub mvars, nub tvars)   where     go ref act iorefs mvars tvars = do@@ -715,21 +731,21 @@         Right Nothing ->           pure (newIORefs, newMVars, newTVars)         Left exc -> do-          C.writeIORef ref (Just (Left exc))+          writeRef ref (Just (Left exc))           pure (newIORefs, newMVars, newTVars)  -- | Run an invariant for one step-stepInvariant :: C.MonadConc n+stepInvariant :: MonadDejaFu n   => IAction n   -> n (Either E.SomeException (Maybe (IAction n)), [IORefId], [MVarId], [TVarId]) stepInvariant (IInspectIORef ioref@ModelIORef{..} k) = do   a <- readIORefGlobal ioref   pure (Right (Just (k a)), [iorefId], [], []) stepInvariant (IInspectMVar ModelMVar{..} k) = do-  a <- C.readIORef mvarRef+  a <- readRef mvarRef   pure (Right (Just (k a)), [], [mvarId], []) stepInvariant (IInspectTVar ModelTVar{..} k) = do-  a <- C.readIORef tvarRef+  a <- readRef tvarRef   pure (Right (Just (k a)), [], [], [tvarId]) stepInvariant (ICatch h nx k) = doInvariant nx >>= \case   (Right a, iorefs, mvars, tvars) ->

@@ -17,7 +17,6 @@  import           Control.Exception             (Exception, MaskingState(..)) import           Control.Monad.Catch           (MonadCatch(..), MonadThrow(..))-import qualified Control.Monad.Conc.Class      as C import qualified Control.Monad.Fail            as Fail import           Data.Map.Strict               (Map) @@ -106,7 +105,7 @@ -- @Maybe@ value. data ModelMVar n a = ModelMVar   { mvarId  :: MVarId-  , mvarRef :: C.IORef n (Maybe a)+  , mvarRef :: Ref n (Maybe a)   }  -- | A @IORef@ is modelled as a unique ID and a reference holding@@ -114,7 +113,7 @@ -- committed value. data ModelIORef n a = ModelIORef   { iorefId  :: IORefId-  , iorefRef :: C.IORef n (Map ThreadId a, Integer, a)+  , iorefRef :: Ref n (Map ThreadId a, Integer, a)   }  -- | A @Ticket@ is modelled as the ID of the @ModelIORef@ it came from,@@ -136,6 +135,8 @@ 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)++  | ASupportsBoundThreads (Bool -> Action n)   | AIsBound (Bool -> Action n)   | AMyTId (ThreadId -> Action n) @@ -182,6 +183,7 @@ lookahead :: Action n -> Lookahead lookahead (AFork _ _ _) = WillFork lookahead (AForkOS _ _ _) = WillForkOS+lookahead (ASupportsBoundThreads _) = WillSupportsBoundThreads lookahead (AIsBound _) = WillIsCurrentThreadBound lookahead (AMyTId _) = WillMyThreadId lookahead (AGetNumCapabilities _) = WillGetNumCapabilities

@@ -6,7 +6,7 @@  -- | -- Module      : Test.DejaFu.Conc.Internal.Memory--- Copyright   : (c) 2016--2018 Michael Walker+-- Copyright   : (c) 2016--2019 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental@@ -25,7 +25,6 @@ -- Memory Models/, N. Zhang, M. Kusano, and C. Wang (2015). module Test.DejaFu.Conc.Internal.Memory where -import qualified Control.Monad.Conc.Class            as C import           Data.Map.Strict                     (Map) import qualified Data.Map.Strict                     as M import           Data.Maybe                          (maybeToList)@@ -61,20 +60,20 @@ emptyBuffer = WriteBuffer M.empty  -- | Add a new write to the end of a buffer.-bufferWrite :: C.MonadConc n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> ModelIORef n a -> a -> n (WriteBuffer n)+bufferWrite :: MonadDejaFu n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> ModelIORef n a -> a -> n (WriteBuffer n) bufferWrite (WriteBuffer wb) k@(tid, _) ref@ModelIORef{..} new = do   -- Construct the new write buffer   let write = singleton $ BufferedWrite tid ref new   let buffer' = M.insertWith (flip (><)) k write wb    -- Write the thread-local value to the @IORef@'s update map.-  (locals, count, def) <- C.readIORef iorefRef-  C.writeIORef iorefRef (M.insert tid new locals, count, def)+  (locals, count, def) <- readRef iorefRef+  writeRef iorefRef (M.insert tid new locals, count, def)    pure (WriteBuffer buffer')  -- | Commit the write at the head of a buffer.-commitWrite :: C.MonadConc n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> n (WriteBuffer n)+commitWrite :: MonadDejaFu n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> n (WriteBuffer n) commitWrite w@(WriteBuffer wb) k = case maybe EmptyL viewl $ M.lookup k wb of   BufferedWrite _ ref a :< rest -> do     _ <- writeImmediate ref a@@ -83,21 +82,21 @@  -- | Read from a @IORef@, returning a newer thread-local non-committed -- write if there is one.-readIORef :: C.MonadConc n => ModelIORef n a -> ThreadId -> n a+readIORef :: MonadDejaFu n => ModelIORef n a -> ThreadId -> n a readIORef ref tid = do   (val, _) <- readIORefPrim ref tid   pure val  -- | Read from a @IORef@, returning a @Ticket@ representing the current -- view of the thread.-readForTicket :: C.MonadConc n => ModelIORef n a -> ThreadId -> n (ModelTicket a)+readForTicket :: MonadDejaFu n => ModelIORef n a -> ThreadId -> n (ModelTicket a) readForTicket ref@ModelIORef{..} tid = do   (val, count) <- readIORefPrim ref tid   pure (ModelTicket iorefId count val)  -- | Perform a compare-and-swap on a @IORef@ if the ticket is still -- valid. This is strict in the \"new\" value argument.-casIORef :: C.MonadConc n => ModelIORef n a -> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ())+casIORef :: MonadDejaFu n => ModelIORef n a -> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ()) casIORef ref tid (ModelTicket _ cc _) !new = do   tick'@(ModelTicket _ cc' _) <- readForTicket ref tid @@ -109,28 +108,28 @@   else pure (False, tick', pure ())  -- | Read the local state of a @IORef@.-readIORefPrim :: C.MonadConc n => ModelIORef n a -> ThreadId -> n (a, Integer)+readIORefPrim :: MonadDejaFu n => ModelIORef n a -> ThreadId -> n (a, Integer) readIORefPrim ModelIORef{..} tid = do-  (vals, count, def) <- C.readIORef iorefRef+  (vals, count, def) <- readRef iorefRef   pure (M.findWithDefault def tid vals, count)  -- | Read the global state of a @IORef@.-readIORefGlobal :: C.MonadConc n => ModelIORef n a -> n a+readIORefGlobal :: MonadDejaFu n => ModelIORef n a -> n a readIORefGlobal ModelIORef{..} = do-  (_, _, def) <- C.readIORef iorefRef+  (_, _, def) <- readRef iorefRef   pure def  -- | Write and commit to a @IORef@ immediately, clearing the update map -- and incrementing the write count.-writeImmediate :: C.MonadConc n => ModelIORef n a -> a -> n (n ())+writeImmediate :: MonadDejaFu n => ModelIORef n a -> a -> n (n ()) writeImmediate ModelIORef{..} a = do-  (_, count, _) <- C.readIORef iorefRef-  let effect = C.writeIORef iorefRef (M.empty, count + 1, a)+  (_, count, _) <- readRef iorefRef+  let effect = writeRef iorefRef (M.empty, count + 1, a)   effect   pure effect  -- | Flush all writes in the buffer.-writeBarrier :: C.MonadConc n => WriteBuffer n -> n ()+writeBarrier :: MonadDejaFu n => WriteBuffer n -> n () writeBarrier (WriteBuffer wb) = mapM_ flush $ M.elems wb where   flush = mapM_ $ \(BufferedWrite _ ref a) -> writeImmediate ref a @@ -162,7 +161,7 @@ data Emptying = Emptying | NonEmptying  -- | Put into a @MVar@, blocking if full.-putIntoMVar :: C.MonadConc n+putIntoMVar :: MonadDejaFu n   => ModelMVar n a   -> a   -> Action n@@ -172,7 +171,7 @@ putIntoMVar cvar a c = mutMVar Blocking cvar a (const c)  -- | Try to put into a @MVar@, not blocking if full.-tryPutIntoMVar :: C.MonadConc n+tryPutIntoMVar :: MonadDejaFu n   => ModelMVar n a   -> a   -> (Bool -> Action n)@@ -182,7 +181,7 @@ tryPutIntoMVar = mutMVar NonBlocking  -- | Read from a @MVar@, blocking if empty.-readFromMVar :: (C.MonadConc n, HasCallStack)+readFromMVar :: (MonadDejaFu n, HasCallStack)   => ModelMVar n a   -> (a -> Action n)   -> ThreadId@@ -191,7 +190,7 @@ readFromMVar cvar c = seeMVar NonEmptying Blocking cvar (c . efromJust)  -- | Try to read from a @MVar@, not blocking if empty.-tryReadFromMVar :: C.MonadConc n+tryReadFromMVar :: MonadDejaFu n   => ModelMVar n a   -> (Maybe a -> Action n)   -> ThreadId@@ -200,7 +199,7 @@ tryReadFromMVar = seeMVar NonEmptying NonBlocking  -- | Take from a @MVar@, blocking if empty.-takeFromMVar :: (C.MonadConc n, HasCallStack)+takeFromMVar :: (MonadDejaFu n, HasCallStack)   => ModelMVar n a   -> (a -> Action n)   -> ThreadId@@ -209,7 +208,7 @@ takeFromMVar cvar c = seeMVar Emptying Blocking cvar (c . efromJust)  -- | Try to take from a @MVar@, not blocking if empty.-tryTakeFromMVar :: C.MonadConc n+tryTakeFromMVar :: MonadDejaFu n   => ModelMVar n a   -> (Maybe a -> Action n)   -> ThreadId@@ -218,7 +217,7 @@ tryTakeFromMVar = seeMVar Emptying NonBlocking  -- | Mutate a @MVar@, in either a blocking or nonblocking way.-mutMVar :: C.MonadConc n+mutMVar :: MonadDejaFu n   => Blocking   -> ModelMVar n a   -> a@@ -226,7 +225,7 @@   -> ThreadId   -> Threads n   -> n (Bool, Threads n, [ThreadId], n ())-mutMVar blocking ModelMVar{..} a c threadid threads = C.readIORef mvarRef >>= \case+mutMVar blocking ModelMVar{..} a c threadid threads = readRef mvarRef >>= \case   Just _ -> case blocking of     Blocking ->       let threads' = block (OnMVarEmpty mvarId) threadid threads@@ -234,14 +233,14 @@     NonBlocking ->       pure (False, goto (c False) threadid threads, [], pure ())   Nothing -> do-    let effect = C.writeIORef mvarRef $ Just a+    let effect = writeRef 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 :: C.MonadConc n+seeMVar :: MonadDejaFu n   => Emptying   -> Blocking   -> ModelMVar n a@@ -249,10 +248,10 @@   -> ThreadId   -> Threads n   -> n (Bool, Threads n, [ThreadId], n ())-seeMVar emptying blocking ModelMVar{..} c threadid threads = C.readIORef mvarRef >>= \case+seeMVar emptying blocking ModelMVar{..} c threadid threads = readRef mvarRef >>= \case   val@(Just _) -> do     let effect = case emptying of-          Emptying -> C.writeIORef mvarRef Nothing+          Emptying -> writeRef mvarRef Nothing           NonEmptying -> pure ()     let (threads', woken) = wake (OnMVarEmpty mvarId) threads     effect

@@ -92,11 +92,9 @@    forkWithUnmaskN   n ma = ModelConc (AFork n (\umask -> runModelConc (ma umask) (\_ -> AStop (pure ()))))   forkOnWithUnmaskN n _  = C.forkWithUnmaskN n-  forkOSWithUnmaskN n ma-    | C.rtsSupportsBoundThreads =-      ModelConc (AForkOS n (\umask -> runModelConc (ma umask) (\_ -> AStop (pure ()))))-    | otherwise = fail "RTS doesn't support multiple OS threads (use ghc -threaded when linking)"+  forkOSWithUnmaskN n ma = ModelConc (AForkOS n (\umask -> runModelConc (ma umask) (\_ -> AStop (pure ())))) +  supportsBoundThreads = ModelConc ASupportsBoundThreads   isCurrentThreadBound = ModelConc AIsBound    -- This implementation lies and returns 2 until a value is set. This@@ -172,8 +170,8 @@ -- nonexistent thread. In either of those cases, the computation will -- be halted. ----- @since 2.0.0.0-runConcurrent :: C.MonadConc n+-- @since 2.1.0.0+runConcurrent :: MonadDejaFu n   => Scheduler s   -> MemType   -> s@@ -181,7 +179,7 @@   -> n (Either Condition a, s, Trace) runConcurrent sched memtype s ma@(ModelConc _) = do   res <- runConcurrency [] False sched memtype s initialIdSource 2 ma-  out <- efromJust <$> C.readIORef (finalRef res)+  out <- efromJust <$> readRef (finalRef res)   pure ( out        , cSchedState (finalContext res)        , F.toList (finalTrace res)@@ -252,9 +250,9 @@ --   (liftIO . readIORef) -- @ ----- @since 2.0.0.0+-- @since 2.1.0.0 recordSnapshot-  :: C.MonadConc n+  :: MonadDejaFu n   => Program pty n a   -> n (Maybe (Either Condition (Snapshot pty n a), Trace)) recordSnapshot ModelConc{..} = pure Nothing@@ -267,9 +265,9 @@  -- | Runs a program with snapshotted setup to completion. ----- @since 2.0.0.0+-- @since 2.1.0.0 runSnapshot-  :: C.MonadConc n+  :: MonadDejaFu n   => Scheduler s   -> MemType   -> s@@ -278,7 +276,7 @@ runSnapshot sched memtype s (WS SimpleSnapshot{..}) = do   let context = fromSnapContext s snapContext   CResult{..} <- runConcurrencyWithSnapshot sched memtype context snapRestore snapNext-  out <- efromJust <$> C.readIORef finalRef+  out <- efromJust <$> readRef finalRef   pure ( out        , cSchedState finalContext        , F.toList finalTrace@@ -287,9 +285,9 @@   let context = fromSnapContext s snapContext   intermediateResult <- runConcurrencyWithSnapshot sched memtype context snapRestore snapNext   let idsrc = cIdSource (finalContext intermediateResult)-  out1 <- efromJust <$> C.readIORef (finalRef intermediateResult)+  out1 <- efromJust <$> readRef (finalRef intermediateResult)   teardownResult <- simpleRunConcurrency False idsrc (teardown out1)-  out2 <- efromJust <$> C.readIORef (finalRef teardownResult)+  out2 <- efromJust <$> readRef (finalRef teardownResult)   pure ( out2        , cSchedState (finalContext intermediateResult)        , F.toList (finalTrace intermediateResult)@@ -328,7 +326,7 @@ -- | 'recordSnapshot' implemented generically. -- -- Throws an error if the snapshot could not be produced.-defaultRecordSnapshot :: C.MonadConc n+defaultRecordSnapshot :: MonadDejaFu n   => (SimpleSnapshot n a -> x -> snap)   -> ModelConc n x   -> (x -> ModelConc n a)@@ -336,7 +334,7 @@ defaultRecordSnapshot mkSnapshot setup program = do   CResult{..} <- simpleRunConcurrency True initialIdSource setup   let trc = F.toList finalTrace-  out <- C.readIORef finalRef+  out <- readRef finalRef   pure . Just $ case out of     Just (Right a) ->       let snap = mkSnapshot (SimpleSnapshot finalContext finalRestore (program a)) a@@ -351,7 +349,7 @@  -- | Run a concurrent program with a deterministic scheduler in -- snapshotting or non-snapshotting mode.-simpleRunConcurrency ::(C.MonadConc n, HasCallStack)+simpleRunConcurrency ::(MonadDejaFu n, HasCallStack)   => Bool   -> IdSource   -> ModelConc n a

@@ -7,7 +7,7 @@  -- | -- Module      : Test.DejaFu.Conc.Internal.STM--- Copyright   : (c) 2017--2018 Michael Walker+-- Copyright   : (c) 2017--2019 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental@@ -18,15 +18,14 @@ -- 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 qualified Control.Monad.Conc.Class as C-import qualified Control.Monad.Fail       as Fail-import qualified Control.Monad.STM.Class  as S-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.Fail      as Fail+import qualified Control.Monad.STM.Class as S+import           Data.List               (nub)  import           Test.DejaFu.Internal import           Test.DejaFu.Types@@ -100,7 +99,7 @@ -- value. data ModelTVar n a = ModelTVar   { tvarId  :: TVarId-  , tvarRef :: C.IORef n a+  , tvarRef :: Ref n a   }  --------------------------------------------------------------------------------@@ -126,7 +125,7 @@  -- | Run a transaction, returning the result and new initial 'TVarId'. -- If the transaction failed, any effects are undone.-runTransaction :: C.MonadConc n+runTransaction :: MonadDejaFu n   => ModelSTM n a   -> IdSource   -> n (Result a, IdSource, [TAction])@@ -138,14 +137,14 @@ -- -- If the transaction fails, its effects will automatically be undone, -- so the undo action returned will be @pure ()@.-doTransaction :: C.MonadConc n+doTransaction :: MonadDejaFu n   => ModelSTM n a   -> IdSource   -> n (Result a, n (), IdSource, [TAction]) doTransaction ma idsource = do   (c, ref) <- runRefCont SStop (Just . Right) (runModelSTM ma)   (idsource', undo, readen, written, trace) <- go ref c (pure ()) idsource [] [] []-  res <- C.readIORef ref+  res <- readRef ref    case res of     Just (Right val) -> pure (Success (nub readen) (nub written) val, undo, idsource', reverse trace)@@ -166,15 +165,15 @@       case tact of         TStop  -> pure (newIDSource, newUndo, newReaden, newWritten, TStop:newSofar)         TRetry -> do-          C.writeIORef ref Nothing+          writeRef ref Nothing           pure (newIDSource, newUndo, newReaden, newWritten, TRetry:newSofar)         TThrow -> do-          C.writeIORef ref (Just . Left $ case act of SThrow e -> toException e; _ -> undefined)+          writeRef 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 :: C.MonadConc n+stepTrans :: MonadDejaFu n   => STMAction n   -> IdSource   -> n (STMAction n, n (), IdSource, [TVarId], [TVarId], TAction)@@ -199,17 +198,17 @@         Nothing   -> pure (SThrow exc, nothing, idsource, [], [], TCatch trace Nothing))      stepRead ModelTVar{..} c = do-      val <- C.readIORef tvarRef+      val <- readRef tvarRef       pure (c val, nothing, idsource, [tvarId], [], TRead tvarId)      stepWrite ModelTVar{..} a c = do-      old <- C.readIORef tvarRef-      C.writeIORef tvarRef a-      pure (c, C.writeIORef tvarRef old, idsource, [], [tvarId], TWrite tvarId)+      old <- readRef tvarRef+      writeRef tvarRef a+      pure (c, writeRef tvarRef old, idsource, [], [tvarId], TWrite tvarId)      stepNew n a c = do       let (idsource', tvid) = nextTVId n idsource-      ref <- C.newIORef a+      ref <- newRef a       let tvar = ModelTVar tvid ref       pure (c tvar, nothing, idsource', [], [tvid], TNew tvid) 

@@ -4,7 +4,7 @@  -- | -- Module      : Test.DejaFu.Conc.Internal.Threading--- Copyright   : (c) 2016--2018 Michael Walker+-- Copyright   : (c) 2016--2019 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental@@ -16,8 +16,6 @@  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@@ -44,20 +42,10 @@   -- ^ Stack of exception handlers   , _masking      :: MaskingState   -- ^ The exception masking state.-  , _bound        :: Maybe (BoundThread n)+  , _bound        :: Maybe (BoundThread n (Action n))   -- ^ State for the associated bound thread, if it exists.   } --- | The state of a bound thread.-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)-  -- ^ 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 -> Thread n mkthread c = Thread c Nothing [] Unmasked Nothing@@ -167,33 +155,24 @@ -- ** Bound threads  -- | Turn a thread into a bound thread.-makeBound :: (C.MonadConc n, HasCallStack) => ThreadId -> Threads n -> n (Threads n)-makeBound tid threads = do-    runboundIO <- C.newEmptyMVar-    getboundIO <- C.newEmptyMVar-    btid <- C.forkOSN ("bound worker for '" ++ show tid ++ "'") (go runboundIO getboundIO)-    let bt = BoundThread runboundIO getboundIO btid-    pure (eadjust (\t -> t { _bound = Just bt }) tid threads)-  where-    go runboundIO getboundIO = forever $ do-      na <- C.takeMVar runboundIO-      C.putMVar getboundIO =<< na+makeBound :: (MonadDejaFu n, HasCallStack)+  => n (BoundThread n (Action n)) -> ThreadId -> Threads n -> n (Threads n)+makeBound fbt tid threads = do+  bt <- fbt+  pure (eadjust (\t -> t { _bound = Just bt }) tid threads)  -- | 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, HasCallStack) => ThreadId -> Threads n -> n (Threads n)+kill :: (MonadDejaFu n, HasCallStack) => ThreadId -> Threads n -> n (Threads n) kill tid threads = do   let thread = elookup tid threads-  maybe (pure ()) (C.killThread . _boundTId) (_bound thread)+  maybe (pure ()) killBoundThread (_bound thread)   pure (M.delete tid threads)- -- | Run an action. -- -- If the thread is bound, the action is run in the worker thread.-runLiftedAct :: C.MonadConc n => ThreadId -> Threads n -> n (Action n) -> n (Action n)+runLiftedAct :: MonadDejaFu 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-    C.takeMVar (_getboundIO bt)+  Just bt -> runInBoundThread bt ma   Nothing -> ma

@@ -17,18 +17,17 @@ -- library. module Test.DejaFu.Internal where -import           Control.DeepSeq          (NFData(..))-import           Control.Exception        (MaskingState(..))-import qualified Control.Monad.Conc.Class as C-import           Data.List.NonEmpty       (NonEmpty(..))-import           Data.Map.Strict          (Map)-import qualified Data.Map.Strict          as M-import           Data.Maybe               (fromMaybe)-import           Data.Set                 (Set)-import qualified Data.Set                 as S-import           GHC.Generics             (Generic)-import           GHC.Stack                (HasCallStack, withFrozenCallStack)-import           System.Random            (RandomGen)+import           Control.DeepSeq    (NFData(..))+import           Control.Exception  (MaskingState(..))+import           Data.List.NonEmpty (NonEmpty(..))+import           Data.Map.Strict    (Map)+import qualified Data.Map.Strict    as M+import           Data.Maybe         (fromMaybe)+import           Data.Set           (Set)+import qualified Data.Set           as S+import           GHC.Generics       (Generic)+import           GHC.Stack          (HasCallStack, withFrozenCallStack)+import           System.Random      (RandomGen)  import           Test.DejaFu.Types @@ -165,6 +164,7 @@ rewind :: ThreadAction -> Lookahead rewind (Fork _) = WillFork rewind (ForkOS _) = WillForkOS+rewind (SupportsBoundThreads _) = WillSupportsBoundThreads rewind (IsCurrentThreadBound _) = WillIsCurrentThreadBound rewind MyThreadId = WillMyThreadId rewind (GetNumCapabilities _) = WillGetNumCapabilities@@ -449,12 +449,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 :: C.MonadConc n+runRefCont :: MonadDejaFu n   => (n () -> x)   -> (a -> Maybe b)   -> ((a -> x) -> x)-  -> n (x, C.IORef n (Maybe b))+  -> n (x, Ref n (Maybe b)) runRefCont act f k = do-  ref <- C.newIORef Nothing-  let c = k (act . C.writeIORef ref . f)+  ref <- newRef Nothing+  let c = k (act . writeRef ref . f)   pure (c, ref)

@@ -1,5 +1,3 @@-{-# OPTIONS_GHC -Wno-deprecations #-}- -- | -- Module      : Test.DejaFu.SCT -- Copyright   : (c) 2015--2019 Michael Walker@@ -26,7 +24,6 @@  import           Control.Applicative               ((<|>)) import           Control.DeepSeq                   (NFData(..), force)-import           Control.Monad.Conc.Class          (MonadConc) import           Data.List                         (foldl') import qualified Data.Map.Strict                   as M import           Data.Maybe                        (fromMaybe)@@ -51,8 +48,8 @@ -- The exact executions tried, and the order in which results are -- found, is unspecified and may change between releases. ----- @since 2.0.0.0-runSCT :: MonadConc n+-- @since 2.1.0.0+runSCT :: MonadDejaFu n   => Way   -- ^ How to run the concurrent program.   -> MemType@@ -64,8 +61,8 @@  -- | Return the set of results of a concurrent program. ----- @since 2.0.0.0-resultsSet :: (MonadConc n, Ord a)+-- @since 2.1.0.0+resultsSet :: (MonadDejaFu n, Ord a)   => Way   -- ^ How to run the concurrent program.   -> MemType@@ -83,8 +80,8 @@ -- The exact executions tried, and the order in which results are -- found, is unspecified and may change between releases. ----- @since 2.0.0.0-runSCT' :: (MonadConc n, NFData a)+-- @since 2.1.0.0+runSCT' :: (MonadDejaFu n, NFData a)   => Way   -- ^ How to run the concurrent program.   -> MemType@@ -99,8 +96,8 @@ -- Demanding the result of this will force it to normal form, which -- may be more efficient in some situations. ----- @since 2.0.0.0-resultsSet' :: (MonadConc n, Ord a, NFData a)+-- @since 2.1.0.0+resultsSet' :: (MonadDejaFu n, Ord a, NFData a)   => Way   -- ^ How to run the concurrent program.   -> MemType@@ -118,8 +115,8 @@ -- The exact executions tried, and the order in which results are -- found, is unspecified and may change between releases. ----- @since 2.0.0.0-runSCTWithSettings :: MonadConc n+-- @since 2.1.0.0+runSCTWithSettings :: MonadDejaFu n   => Settings n a   -- ^ The SCT settings.   -> Program pty n a@@ -159,8 +156,8 @@  -- | A variant of 'resultsSet' which takes a 'Settings' record. ----- @since 2.0.0.0-resultsSetWithSettings :: (MonadConc n, Ord a)+-- @since 2.1.0.0+resultsSetWithSettings :: (MonadDejaFu n, Ord a)   => Settings n a   -- ^ The SCT settings.   -> Program pty n a@@ -178,8 +175,8 @@ -- The exact executions tried, and the order in which results are -- found, is unspecified and may change between releases. ----- @since 2.0.0.0-runSCTWithSettings' :: (MonadConc n, NFData a)+-- @since 2.1.0.0+runSCTWithSettings' :: (MonadDejaFu n, NFData a)   => Settings n a   -- ^ The SCT settings.   -> Program pty n a@@ -194,8 +191,8 @@ -- Demanding the result of this will force it to normal form, which -- may be more efficient in some situations. ----- @since 2.0.0.0-resultsSetWithSettings' :: (MonadConc n, Ord a, NFData a)+-- @since 2.1.0.0+resultsSetWithSettings' :: (MonadDejaFu n, Ord a, NFData a)   => Settings n a   -- ^ The SCT settings.   -> Program pty n a

@@ -5,7 +5,7 @@  -- | -- Module      : Test.DejaFu.SCT.Internal--- Copyright   : (c) 2018 Michael Walker+-- Copyright   : (c) 2018--2019 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental@@ -15,7 +15,6 @@ -- considered to form part of the public interface of this library. module Test.DejaFu.SCT.Internal where -import           Control.Monad.Conc.Class          (MonadConc) import           Data.Coerce                       (Coercible, coerce) import qualified Data.IntMap.Strict                as I import           Data.List                         (find, mapAccumL)@@ -36,7 +35,7 @@ -- * Exploration  -- | General-purpose SCT function.-sct :: (MonadConc n, HasCallStack)+sct :: (MonadDejaFu n, HasCallStack)   => Settings n a   -- ^ The SCT settings ('Way' is ignored)   -> ([ThreadId] -> s)@@ -79,7 +78,7 @@     runSnap snap sched s = runSnapshot sched (_memtype settings) s snap  -- | Like 'sct' but given a function to run the computation.-sct' :: (MonadConc n, HasCallStack)+sct' :: (MonadDejaFu n, HasCallStack)   => Settings n a   -- ^ The SCT settings ('Way' is ignored)   -> ConcurrencyState@@ -150,7 +149,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, HasCallStack)+simplifyExecution :: (MonadDejaFu n, HasCallStack)   => Settings n a   -- ^ The SCT settings ('Way' is ignored)   -> ConcurrencyState@@ -190,7 +189,7 @@     p = either show debugShow  -- | Replay an execution.-replay :: MonadConc n+replay :: MonadDejaFu n   => (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))   -- ^ Run the computation   -> [(ThreadId, ThreadAction)]

@@ -1,7 +1,10 @@ {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}  -- | -- Module      : Test.DejaFu.Types@@ -9,26 +12,141 @@ -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : DeriveGeneric, GeneralizedNewtypeDeriving, LambdaCase, StandaloneDeriving+-- Portability : DeriveGeneric, FlexibleInstances, GeneralizedNewtypeDeriving, LambdaCase, RankNTypes, StandaloneDeriving, TypeFamilies -- -- Common types and functions used throughout DejaFu. module Test.DejaFu.Types where +import qualified Control.Concurrent                   as IO import           Control.DeepSeq                      (NFData(..)) import           Control.Exception                    (Exception(..),                                                        MaskingState(..),                                                        SomeException)+import           Control.Monad                        (forever)+import           Control.Monad.Catch                  (MonadThrow)+import           Control.Monad.Catch.Pure             (CatchT)+import qualified Control.Monad.ST                     as ST+import           Control.Monad.Trans.Class            (lift) import           Data.Function                        (on) import           Data.Functor.Contravariant           (Contravariant(..)) import           Data.Functor.Contravariant.Divisible (Divisible(..))+import qualified Data.IORef                           as IO import           Data.Map.Strict                      (Map) import qualified Data.Map.Strict                      as M import           Data.Semigroup                       (Semigroup(..)) import           Data.Set                             (Set) import qualified Data.Set                             as S-import           GHC.Generics                         (Generic)+import qualified Data.STRef                           as ST+import           GHC.Generics                         (Generic, V1)  -------------------------------------------------------------------------------+-- * The @MonadDejaFu@ typeclass++-- | The @MonadDejaFu@ class captures the two things needed to run a+-- concurrent program which we can't implement in normal Haskell:+-- mutable references, and the ability to create a bound thread in+-- @IO@.+--+-- In addition to needing the operations in this class, dejafu also+-- needs the ability to throw exceptions, as these are used to+-- communicate 'Error's, so there is a 'MonadThrow' constraint.+--+-- @since 2.1.0.0+class MonadThrow m => MonadDejaFu m where+  -- | The type of mutable references.  These references will always+  -- contain a value, and so don't need to handle emptiness (like+  -- @MVar@ does).+  --+  -- These references are always used from the same Haskell thread, so+  -- it's safe to implement these using unsynchronised primitives with+  -- relaxed-memory behaviours (like @IORef@s).+  type Ref m :: * -> *++  -- | Create a new reference holding a given initial value.+  newRef :: a -> m (Ref m a)++  -- | Read the current value in the reference.+  readRef :: Ref m a -> m a++  -- | Replace the value in the reference.+  writeRef :: Ref m a -> a -> m ()++  -- | A handle to a bound thread.  If the monad doesn't support bound+  -- threads (for example, if it's not based on @IO@), then this+  -- should be some type which can't be constructed, like 'V1'.+  type BoundThread m :: * -> *++  -- | Fork a new bound thread, if the monad supports them.+  forkBoundThread :: Maybe (m (BoundThread m a))++  -- | Run an action in a previously created bound thread.+  runInBoundThread :: BoundThread m a -> m a -> m a++  -- | Terminate a previously created bound thread.+  --+  -- After termination, 'runInBoundThread' and 'killBoundThread' will+  -- never be called on this @BoundThread m a@ value again.+  killBoundThread :: BoundThread m a -> m ()++-- | A bound thread in @IO@.+--+-- @since 2.1.0.0+data IOBoundThread a = IOBoundThread+  { iobtRunInBoundThread :: IO a -> IO a+    -- ^ Pass an action to the bound thread, run it, and return the+    -- result to this thread.+  , iobtKillBoundThread  :: IO ()+    -- ^ Terminate the bound thread.+  }++-- | @since 2.1.0.0+instance MonadDejaFu IO where+  type Ref IO = IO.IORef++  newRef   = IO.newIORef+  readRef  = IO.readIORef+  writeRef = IO.writeIORef++  type BoundThread IO = IOBoundThread++  forkBoundThread = Just $ do+      runboundIO <- IO.newEmptyMVar+      getboundIO <- IO.newEmptyMVar+      tid <- IO.forkOS (go runboundIO getboundIO)+      pure IOBoundThread+        { iobtRunInBoundThread = run runboundIO getboundIO+        , iobtKillBoundThread  = IO.killThread tid+        }+    where+      go runboundIO getboundIO = forever $ do+        na <- IO.takeMVar runboundIO+        IO.putMVar getboundIO =<< na++      run runboundIO getboundIO ma = do+        IO.putMVar runboundIO ma+        IO.takeMVar getboundIO++  runInBoundThread = iobtRunInBoundThread+  killBoundThread  = iobtKillBoundThread++-- | This instance does not support bound threads.+--+-- @since 2.1.0.0+instance MonadDejaFu (CatchT (ST.ST t)) where+  type Ref (CatchT (ST.ST t)) = ST.STRef t++  newRef     = lift . ST.newSTRef+  readRef    = lift . ST.readSTRef+  writeRef r = lift . ST.writeSTRef r++  -- V1 has no constructors+  type BoundThread (CatchT (ST.ST t)) = V1++  forkBoundThread  = Nothing+  runInBoundThread = undefined+  killBoundThread  = undefined++------------------------------------------------------------------------------- -- * Identifiers  -- | Every thread has a unique identitifer.@@ -116,6 +234,8 @@   -- ^ Start a new thread.   | ForkOS ThreadId   -- ^ Start a new bound thread.+  | SupportsBoundThreads Bool+  -- ^ Check if bound threads are supported.   | IsCurrentThreadBound Bool   -- ^ Check if the current thread is bound.   | MyThreadId@@ -206,6 +326,7 @@ instance NFData ThreadAction where   rnf (Fork t) = rnf t   rnf (ForkOS t) = rnf t+  rnf (SupportsBoundThreads b) = rnf b   rnf (IsCurrentThreadBound b) = rnf b   rnf MyThreadId = ()   rnf (GetNumCapabilities i) = rnf i@@ -252,6 +373,8 @@   -- ^ Will start a new thread.   | WillForkOS   -- ^ Will start a new bound thread.+  | WillSupportsBoundThreads+  -- ^ Will check if bound threads are supported.   | WillIsCurrentThreadBound   -- ^ Will check if the current thread is bound.   | WillMyThreadId@@ -331,6 +454,7 @@ instance NFData Lookahead where   rnf WillFork = ()   rnf WillForkOS = ()+  rnf WillSupportsBoundThreads = ()   rnf WillIsCurrentThreadBound = ()   rnf WillMyThreadId = ()   rnf WillGetNumCapabilities = ()

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                dejafu-version:             2.0.0.1+version:             2.1.0.0 synopsis:            A library for unit-testing concurrent programs.  description:@@ -20,7 +20,7 @@ license-file:        LICENSE author:              Michael Walker maintainer:          mike@barrucadu.co.uk-copyright:           (c) 2015--2018 Michael Walker+copyright:           (c) 2015--2019 Michael Walker category:            Concurrency build-type:          Simple extra-source-files:  README.markdown CHANGELOG.rst@@ -33,7 +33,7 @@ source-repository this   type:     git   location: https://github.com/barrucadu/dejafu.git-  tag:      dejafu-2.0.0.1+  tag:      dejafu-2.1.0.0  library   exposed-modules:     Test.DejaFu@@ -59,7 +59,7 @@   -- other-modules:          -- other-extensions:       build-depends:       base              >=4.9 && <5-                     , concurrency       >=1.6 && <1.7+                     , concurrency       >=1.7 && <1.8                      , containers        >=0.5 && <0.7                      , contravariant     >=1.2 && <1.6                      , deepseq           >=1.1 && <2