diff --git a/CHANGELOG.rst b/CHANGELOG.rst --- a/CHANGELOG.rst +++ b/CHANGELOG.rst @@ -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) -------------------- diff --git a/Test/DejaFu.hs b/Test/DejaFu.hs --- a/Test/DejaFu.hs +++ b/Test/DejaFu.hs @@ -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 diff --git a/Test/DejaFu/Conc/Internal.hs b/Test/DejaFu/Conc/Internal.hs --- a/Test/DejaFu/Conc/Internal.hs +++ b/Test/DejaFu/Conc/Internal.hs @@ -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 -- 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) -> diff --git a/Test/DejaFu/Conc/Internal/Common.hs b/Test/DejaFu/Conc/Internal/Common.hs --- a/Test/DejaFu/Conc/Internal/Common.hs +++ b/Test/DejaFu/Conc/Internal/Common.hs @@ -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 diff --git a/Test/DejaFu/Conc/Internal/Memory.hs b/Test/DejaFu/Conc/Internal/Memory.hs --- a/Test/DejaFu/Conc/Internal/Memory.hs +++ b/Test/DejaFu/Conc/Internal/Memory.hs @@ -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 -- 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 diff --git a/Test/DejaFu/Conc/Internal/Program.hs b/Test/DejaFu/Conc/Internal/Program.hs --- a/Test/DejaFu/Conc/Internal/Program.hs +++ b/Test/DejaFu/Conc/Internal/Program.hs @@ -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 diff --git a/Test/DejaFu/Conc/Internal/STM.hs b/Test/DejaFu/Conc/Internal/STM.hs --- a/Test/DejaFu/Conc/Internal/STM.hs +++ b/Test/DejaFu/Conc/Internal/STM.hs @@ -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 -- 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) diff --git a/Test/DejaFu/Conc/Internal/Threading.hs b/Test/DejaFu/Conc/Internal/Threading.hs --- a/Test/DejaFu/Conc/Internal/Threading.hs +++ b/Test/DejaFu/Conc/Internal/Threading.hs @@ -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 -- 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 diff --git a/Test/DejaFu/Internal.hs b/Test/DejaFu/Internal.hs --- a/Test/DejaFu/Internal.hs +++ b/Test/DejaFu/Internal.hs @@ -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) diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -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 diff --git a/Test/DejaFu/SCT/Internal.hs b/Test/DejaFu/SCT/Internal.hs --- a/Test/DejaFu/SCT/Internal.hs +++ b/Test/DejaFu/SCT/Internal.hs @@ -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 -- 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)] diff --git a/Test/DejaFu/Types.hs b/Test/DejaFu/Types.hs --- a/Test/DejaFu/Types.hs +++ b/Test/DejaFu/Types.hs @@ -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 -- 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 = () diff --git a/dejafu.cabal b/dejafu.cabal --- a/dejafu.cabal +++ b/dejafu.cabal @@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: dejafu -version: 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