diff --git a/CHANGELOG.rst b/CHANGELOG.rst --- a/CHANGELOG.rst +++ b/CHANGELOG.rst @@ -7,6 +7,35 @@ .. _PVP: https://pvp.haskell.org/ +1.4.0.0 (2018-03-17) +-------------------- + +* Git: :tag:`dejafu-1.4.0.0` +* Hackage: :hackage:`dejafu-1.4.0.0` + +Changed +~~~~~~~ + +- (:issue:`201`) ``Test.DejaFu.Conc.ConcT r n a`` drops its ``r`` + parameter, becoming ``ConcT n a``. + +- (:issue:`201`) All functions drop the ``MonadConc`` constraint. + +Removed +~~~~~~~ + +- (:issue:`201`) The ``MonadRef`` and ``MonadAtomicRef`` instances for + ``Test.DejaFu.Conc.ConcT``. + +- (:issue:`198`) The ``Test.DejaFu.Types.Killed`` thread action, which + was unused. + +Fixed +~~~~~ + +- (:issue:`250`) Add missing dependency for ``throwTo`` actions. + + 1.3.2.0 (2018-03-12) -------------------- diff --git a/Test/DejaFu.hs b/Test/DejaFu.hs --- a/Test/DejaFu.hs +++ b/Test/DejaFu.hs @@ -1,5 +1,4 @@ {-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TupleSections #-} {- | @@ -273,7 +272,6 @@ import Control.Monad (unless, when) import Control.Monad.Conc.Class (MonadConc) import Control.Monad.IO.Class (MonadIO(..)) -import Control.Monad.Ref (MonadRef) import Data.Function (on) import Data.List (intercalate, intersperse) import Data.Maybe (catMaybes, isJust, isNothing, @@ -329,8 +327,8 @@ -- False -- -- @since 1.0.0.0 -autocheck :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a) - => ConcT r n a +autocheck :: (MonadConc n, MonadIO n, Eq a, Show a) + => ConcT n a -- ^ The computation to test. -> n Bool autocheck = autocheckWithSettings defaultSettings @@ -363,12 +361,12 @@ -- False -- -- @since 1.0.0.0 -autocheckWay :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a) +autocheckWay :: (MonadConc n, MonadIO n, Eq a, Show a) => Way -- ^ How to run the concurrent program. -> MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. - -> ConcT r n a + -> ConcT n a -- ^ The computation to test. -> n Bool autocheckWay way = autocheckWithSettings . fromWayAndMemType way @@ -400,10 +398,10 @@ -- False -- -- @since 1.2.0.0 -autocheckWithSettings :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a) +autocheckWithSettings :: (MonadConc n, MonadIO n, Eq a, Show a) => Settings n a -- ^ The SCT settings. - -> ConcT r n a + -> ConcT n a -- ^ The computation to test. -> n Bool autocheckWithSettings settings = dejafusWithSettings settings @@ -427,12 +425,12 @@ -- False -- -- @since 1.0.0.0 -dejafu :: (MonadConc n, MonadIO n, MonadRef r n, Show b) +dejafu :: (MonadConc n, MonadIO n, Show b) => String -- ^ The name of the test. -> ProPredicate a b -- ^ The predicate to check. - -> ConcT r n a + -> ConcT n a -- ^ The computation to test. -> n Bool dejafu = dejafuWithSettings defaultSettings @@ -457,7 +455,7 @@ -- False -- -- @since 1.0.0.0 -dejafuWay :: (MonadConc n, MonadIO n, MonadRef r n, Show b) +dejafuWay :: (MonadConc n, MonadIO n, Show b) => Way -- ^ How to run the concurrent program. -> MemType @@ -466,7 +464,7 @@ -- ^ The name of the test. -> ProPredicate a b -- ^ The predicate to check. - -> ConcT r n a + -> ConcT n a -- ^ The computation to test. -> n Bool dejafuWay way = dejafuWithSettings . fromWayAndMemType way @@ -483,14 +481,14 @@ -- False -- -- @since 1.2.0.0 -dejafuWithSettings :: (MonadConc n, MonadIO n, MonadRef r n, Show b) +dejafuWithSettings :: (MonadConc n, MonadIO n, Show b) => Settings n a -- ^ The SCT settings. -> String -- ^ The name of the test. -> ProPredicate a b -- ^ The predicate to check. - -> ConcT r n a + -> ConcT n a -- ^ The computation to test. -> n Bool dejafuWithSettings settings name test = @@ -506,7 +504,7 @@ -- False -- -- @since 1.0.0.0 -dejafuDiscard :: (MonadConc n, MonadIO n, MonadRef r n, Show b) +dejafuDiscard :: (MonadConc n, MonadIO n, Show b) => (Either Failure a -> Maybe Discard) -- ^ Selectively discard results. -> Way @@ -517,7 +515,7 @@ -- ^ The name of the test. -> ProPredicate a b -- ^ The predicate to check. - -> ConcT r n a + -> ConcT n a -- ^ The computation to test. -> n Bool dejafuDiscard discard way = @@ -536,10 +534,10 @@ -- False -- -- @since 1.0.0.0 -dejafus :: (MonadConc n, MonadIO n, MonadRef r n, Show b) +dejafus :: (MonadConc n, MonadIO n, Show b) => [(String, ProPredicate a b)] -- ^ The list of predicates (with names) to check. - -> ConcT r n a + -> ConcT n a -- ^ The computation to test. -> n Bool dejafus = dejafusWithSettings defaultSettings @@ -558,14 +556,14 @@ -- False -- -- @since 1.0.0.0 -dejafusWay :: (MonadConc n, MonadIO n, MonadRef r n, Show b) +dejafusWay :: (MonadConc n, MonadIO n, Show b) => Way -- ^ How to run the concurrent program. -> MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. -> [(String, ProPredicate a b)] -- ^ The list of predicates (with names) to check. - -> ConcT r n a + -> ConcT n a -- ^ The computation to test. -> n Bool dejafusWay way = dejafusWithSettings . fromWayAndMemType way @@ -583,12 +581,12 @@ -- False -- -- @since 1.2.0.0 -dejafusWithSettings :: (MonadConc n, MonadIO n, MonadRef r n, Show b) +dejafusWithSettings :: (MonadConc n, MonadIO n, Show b) => Settings n a -- ^ The SCT settings. -> [(String, ProPredicate a b)] -- ^ The list of predicates (with names) to check. - -> ConcT r n a + -> ConcT n a -- ^ The computation to test. -> n Bool dejafusWithSettings settings tests conc = do @@ -659,10 +657,10 @@ -- affect which failing traces are reported, when there is a failure. -- -- @since 1.0.0.0 -runTest :: (MonadConc n, MonadRef r n) +runTest :: MonadConc n => ProPredicate a b -- ^ The predicate to check - -> ConcT r n a + -> ConcT n a -- ^ The computation to test -> n (Result b) runTest = runTestWithSettings defaultSettings @@ -675,14 +673,14 @@ -- affect which failing traces are reported, when there is a failure. -- -- @since 1.0.0.0 -runTestWay :: (MonadConc n, MonadRef r n) +runTestWay :: MonadConc n => Way -- ^ How to run the concurrent program. -> MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. -> ProPredicate a b -- ^ The predicate to check - -> ConcT r n a + -> ConcT n a -- ^ The computation to test -> n (Result b) runTestWay way = runTestWithSettings . fromWayAndMemType way @@ -694,12 +692,12 @@ -- affect which failing traces are reported, when there is a failure. -- -- @since 1.2.0.0 -runTestWithSettings :: (MonadConc n, MonadRef r n) +runTestWithSettings :: MonadConc n => Settings n a -- ^ The SCT settings. -> ProPredicate a b -- ^ The predicate to check - -> ConcT r n a + -> ConcT n a -- ^ The computation to test -> n (Result b) runTestWithSettings settings p conc = diff --git a/Test/DejaFu/Conc.hs b/Test/DejaFu/Conc.hs --- a/Test/DejaFu/Conc.hs +++ b/Test/DejaFu/Conc.hs @@ -1,7 +1,6 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} @@ -11,7 +10,7 @@ -- License : MIT -- Maintainer : Michael Walker -- Stability : experimental --- Portability : CPP, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, TypeFamilies +-- Portability : CPP, FlexibleInstances, GeneralizedNewtypeDeriving, TypeFamilies -- -- Deterministic traced execution of concurrent computations. -- @@ -59,11 +58,8 @@ import Control.Exception (MaskingState(..)) import qualified Control.Monad.Catch as Ca import qualified Control.Monad.IO.Class as IO -import Control.Monad.Ref (MonadRef) -import qualified Control.Monad.Ref as Re import Control.Monad.Trans.Class (MonadTrans(..)) import qualified Data.Foldable as F -import Data.IORef (IORef) import Data.List (partition) import qualified Data.Map.Strict as M import Data.Maybe (isNothing) @@ -72,9 +68,8 @@ import qualified Control.Monad.Conc.Class as C import Test.DejaFu.Conc.Internal import Test.DejaFu.Conc.Internal.Common -import Test.DejaFu.Conc.Internal.STM -import Test.DejaFu.Conc.Internal.Threading (Thread(_blocking), - Threads) +import Test.DejaFu.Conc.Internal.STM (ModelSTM) +import Test.DejaFu.Conc.Internal.Threading (_blocking) import Test.DejaFu.Internal import Test.DejaFu.Types import Test.DejaFu.Utils @@ -83,52 +78,40 @@ import qualified Control.Monad.Fail as Fail #endif --- | @since 0.6.0.0 -newtype ConcT r n a = C { unC :: M n r a } deriving (Functor, Applicative, Monad) +-- | @since 1.4.0.0 +newtype ConcT n a = C { unC :: ModelConc n a } + deriving (Functor, Applicative, Monad) #if MIN_VERSION_base(4,9,0) --- | @since 0.9.1.0 -instance Fail.MonadFail (ConcT r n) where +instance Fail.MonadFail (ConcT n) where fail = C . fail #endif -- | A 'MonadConc' implementation using @IO@. -- -- @since 0.4.0.0 -type ConcIO = ConcT IORef IO +type ConcIO = ConcT IO -toConc :: ((a -> Action n r) -> Action n r) -> ConcT r n a -toConc = C . cont +toConc :: ((a -> Action n) -> Action n) -> ConcT n a +toConc = C . ModelConc -wrap :: (M n r a -> M n r a) -> ConcT r n a -> ConcT r n a +wrap :: (ModelConc n a -> ModelConc n a) -> ConcT n a -> ConcT n a wrap f = C . f . unC -- | @since 1.0.0.0 -instance IO.MonadIO n => IO.MonadIO (ConcT r n) where +instance IO.MonadIO n => IO.MonadIO (ConcT n) where liftIO ma = toConc (\c -> ALift (fmap c (IO.liftIO ma))) -instance Re.MonadRef (CRef r) (ConcT r n) where - newRef a = toConc (ANewCRef "" a) - - readRef ref = toConc (AReadCRef ref) - - writeRef ref a = toConc (\c -> AWriteCRef ref a (c ())) - - modifyRef ref f = toConc (AModCRef ref (\a -> (f a, ()))) - -instance Re.MonadAtomicRef (CRef r) (ConcT r n) where - atomicModifyRef ref f = toConc (AModCRef ref f) - -instance MonadTrans (ConcT r) where +instance MonadTrans ConcT where lift ma = toConc (\c -> ALift (fmap c ma)) -instance Ca.MonadCatch (ConcT r n) where +instance Ca.MonadCatch (ConcT n) where catch ma h = toConc (ACatching (unC . h) (unC ma)) -instance Ca.MonadThrow (ConcT r n) where +instance Ca.MonadThrow (ConcT n) where throwM e = toConc (\_ -> AThrow e) -instance Ca.MonadMask (ConcT r n) where +instance Ca.MonadMask (ConcT n) where mask mb = toConc (AMasking MaskedInterruptible (\f -> unC $ mb $ wrap f)) uninterruptibleMask mb = toConc (AMasking MaskedUninterruptible (\f -> unC $ mb $ wrap f)) @@ -147,16 +130,16 @@ pure result #endif -instance Monad n => C.MonadConc (ConcT r n) where - type MVar (ConcT r n) = MVar r - type CRef (ConcT r n) = CRef r - type Ticket (ConcT r n) = Ticket - type STM (ConcT r n) = S n r - type ThreadId (ConcT r n) = ThreadId +instance Monad n => C.MonadConc (ConcT n) where + type MVar (ConcT n) = ModelMVar n + type CRef (ConcT n) = ModelCRef n + type Ticket (ConcT n) = ModelTicket + type STM (ConcT n) = ModelSTM n + type ThreadId (ConcT n) = ThreadId -- ---------- - forkWithUnmaskN n ma = toConc (AFork n (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop (pure ())))) + forkWithUnmaskN n ma = toConc (AFork n (\umask -> runModelConc (unC $ ma $ wrap umask) (\_ -> AStop (pure ())))) forkOnWithUnmaskN n _ = C.forkWithUnmaskN n forkOSN n ma = forkOSWithUnmaskN n (const ma) @@ -180,7 +163,7 @@ readCRef ref = toConc (AReadCRef ref) readForCAS ref = toConc (AReadCRefCas ref) - peekTicket' _ = _ticketVal + peekTicket' _ = ticketVal writeCRef ref a = toConc (\c -> AWriteCRef ref a (c ())) casCRef ref tick a = toConc (ACasCRef ref tick a) @@ -209,9 +192,13 @@ atomically = toConc . AAtom -- move this into the instance defn when forkOSWithUnmaskN is added to MonadConc in 2018 -forkOSWithUnmaskN :: Applicative n => String -> ((forall a. ConcT r n a -> ConcT r n a) -> ConcT r n ()) -> ConcT r n ThreadId +forkOSWithUnmaskN :: Applicative n + => String + -> ((forall a. ConcT n a -> ConcT n a) -> ConcT n ()) + -> ConcT n ThreadId forkOSWithUnmaskN n ma - | C.rtsSupportsBoundThreads = toConc (AForkOS n (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop (pure ())))) + | C.rtsSupportsBoundThreads = + toConc (AForkOS n (\umask -> runModelConc (unC $ ma $ wrap umask) (\_ -> AStop (pure ())))) | otherwise = fail "RTS doesn't support multiple OS threads (use ghc -threaded when linking)" -- | Run a concurrent computation with a given 'Scheduler' and initial @@ -238,15 +225,15 @@ -- be halted. -- -- @since 1.0.0.0 -runConcurrent :: (C.MonadConc n, MonadRef r n) +runConcurrent :: C.MonadConc n => Scheduler s -> MemType -> s - -> ConcT r n a + -> ConcT n a -> n (Either Failure a, s, Trace) runConcurrent sched memtype s ma = do res <- runConcurrency False sched memtype s initialIdSource 2 (unC ma) - out <- efromJust "runConcurrent" <$> Re.readRef (finalRef res) + out <- efromJust "runConcurrent" <$> C.readCRef (finalRef res) pure ( out , cSchedState (finalContext res) , F.toList (finalTrace res) @@ -262,7 +249,7 @@ -- a failing computation. -- -- @since 0.6.0.0 -subconcurrency :: ConcT r n a -> ConcT r n (Either Failure a) +subconcurrency :: ConcT n a -> ConcT n (Either Failure a) subconcurrency ma = toConc (ASub (unC ma)) -- | Run an arbitrary action which gets some special treatment: @@ -300,9 +287,9 @@ dontCheck :: Maybe Int -- ^ An optional length bound. - -> ConcT r n a + -> ConcT n a -- ^ The action to execute. - -> ConcT r n a + -> ConcT n a dontCheck lb ma = toConc (ADontCheck lb (unC ma)) ------------------------------------------------------------------------------- @@ -339,7 +326,7 @@ -- To safely use @IO@ in a snapshotted computation, __the combined effect must be idempotent__. -- You should either use actions which set the state to the final -- value directly, rather than modifying it (eg, using a combination --- of @liftIO . readIORef@ and @liftIO . writeIORef@ here), or reset +-- of @liftIO . readCRef@ and @liftIO . writeIORef@ here), or reset -- the state to a known value. Both of these approaches will work: -- -- @ @@ -372,12 +359,12 @@ -- needing to call this function yourself. -- -- @since 1.1.0.0 -runForDCSnapshot :: (C.MonadConc n, MonadRef r n) - => ConcT r n a - -> n (Maybe (Either Failure (DCSnapshot r n a), Trace)) +runForDCSnapshot :: C.MonadConc n + => ConcT n a + -> n (Maybe (Either Failure (DCSnapshot n a), Trace)) runForDCSnapshot ma = do res <- runConcurrency True roundRobinSchedNP SequentialConsistency () initialIdSource 2 (unC ma) - out <- Re.readRef (finalRef res) + out <- C.readCRef (finalRef res) pure $ case (finalRestore res, out) of (Just _, Just (Left f)) -> Just (Left f, F.toList (finalTrace res)) (Just restore, _) -> Just (Right (DCSnapshot (finalContext res) restore (finalRef res)), F.toList (finalTrace res)) @@ -391,18 +378,18 @@ -- needing to call this function yourself. -- -- @since 1.1.0.0 -runWithDCSnapshot :: (C.MonadConc n, MonadRef r n) +runWithDCSnapshot :: C.MonadConc n => Scheduler s -> MemType -> s - -> DCSnapshot r n a + -> DCSnapshot n a -> n (Either Failure a, s, Trace) runWithDCSnapshot sched memtype s snapshot = do let context = (dcsContext snapshot) { cSchedState = s } let restore = dcsRestore snapshot let ref = dcsRef snapshot res <- runConcurrencyWithSnapshot sched memtype context restore ref - out <- efromJust "runWithDCSnapshot" <$> Re.readRef (finalRef res) + out <- efromJust "runWithDCSnapshot" <$> C.readCRef (finalRef res) pure ( out , cSchedState (finalContext res) , F.toList (finalTrace res) @@ -411,14 +398,14 @@ -- | Check if a 'DCSnapshot' can be taken from this computation. -- -- @since 1.1.0.0 -canDCSnapshot :: ConcT r n a -> Bool -canDCSnapshot (C (M k)) = lookahead (k undefined) == WillDontCheck +canDCSnapshot :: ConcT n a -> Bool +canDCSnapshot (C (ModelConc k)) = lookahead (k undefined) == WillDontCheck -- | Get the threads which exist in a snapshot, partitioned into -- runnable and not runnable. -- -- @since 1.1.0.0 -threadsFromDCSnapshot :: DCSnapshot r n a -> ([ThreadId], [ThreadId]) +threadsFromDCSnapshot :: DCSnapshot n a -> ([ThreadId], [ThreadId]) threadsFromDCSnapshot snapshot = partition isRunnable (M.keys threads) where threads = cThreads (dcsContext snapshot) isRunnable tid = isNothing (_blocking =<< M.lookup tid threads) diff --git a/Test/DejaFu/Conc/Internal.hs b/Test/DejaFu/Conc/Internal.hs --- a/Test/DejaFu/Conc/Internal.hs +++ b/Test/DejaFu/Conc/Internal.hs @@ -1,6 +1,6 @@ -{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE MultiWayIf #-} {-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE RecordWildCards #-} -- | -- Module : Test.DejaFu.Conc.Internal @@ -8,19 +8,17 @@ -- License : MIT -- Maintainer : Michael Walker -- Stability : experimental --- Portability : MultiParamTypeClasses, RankNTypes, ScopedTypeVariables +-- Portability : MultiWayIf, RankNTypes, RecordWildCards -- -- Concurrent monads with a fixed scheduler: internal types and -- functions. This module is NOT considered to form part of the public -- interface of this library. module Test.DejaFu.Conc.Internal where -import Control.Exception (MaskingState(..), +import Control.Exception (Exception, + MaskingState(..), toException) -import Control.Monad.Conc.Class (MonadConc, - rtsSupportsBoundThreads) -import Control.Monad.Ref (MonadRef, newRef, readRef, - writeRef) +import qualified Control.Monad.Conc.Class as C import Data.Foldable (foldrM, toList) import Data.Functor (void) import Data.List (sortOn) @@ -40,17 +38,17 @@ import Test.DejaFu.Types -------------------------------------------------------------------------------- --- * Execution +-- * Set-up -- | 'Trace' but as a sequence. type SeqTrace = Seq (Decision, [(ThreadId, Lookahead)], ThreadAction) -- | The result of running a concurrent program. -data CResult n r g a = CResult - { finalContext :: Context n r g - , finalRef :: r (Maybe (Either Failure a)) - , finalRestore :: Maybe (Threads n r -> n ()) +data CResult n g a = CResult + { finalContext :: Context n g + , finalRef :: C.CRef n (Maybe (Either Failure a)) + , finalRestore :: Maybe (Threads n -> n ()) -- ^ Meaningless if this result doesn't come from a snapshotting -- execution. , finalTrace :: SeqTrace @@ -60,29 +58,29 @@ -- | A snapshot of the concurrency state immediately after 'dontCheck' -- finishes. -- --- @since 1.1.0.0 -data DCSnapshot r n a = DCSnapshot - { dcsContext :: Context n r () +-- @since 1.4.0.0 +data DCSnapshot n a = DCSnapshot + { dcsContext :: Context n () -- ^ The execution context. The scheduler state is ignored when -- restoring. - , dcsRestore :: Threads n r -> n () + , dcsRestore :: Threads n -> n () -- ^ Action to restore CRef, MVar, and TVar values. - , dcsRef :: r (Maybe (Either Failure a)) + , dcsRef :: C.CRef n (Maybe (Either Failure a)) -- ^ Reference where the result will be written. } -- | Run a concurrent computation with a given 'Scheduler' and initial -- state, returning a failure reason on error. Also returned is the -- final state of the scheduler, and an execution trace. -runConcurrency :: (MonadConc n, MonadRef r n) +runConcurrency :: C.MonadConc n => Bool -> Scheduler g -> MemType -> g -> IdSource -> Int - -> M n r a - -> n (CResult n r g a) + -> ModelConc n a + -> n (CResult n g a) runConcurrency forSnapshot sched memtype g idsrc caps ma = do let ctx = Context { cSchedState = g , cIdSource = idsrc @@ -94,94 +92,102 @@ killAllThreads (finalContext res) pure res +-- | Run a concurrent program using the given context, and without +-- killing threads which remain at the end. The context must have no +-- main thread. +-- +-- Only a separate function because @ADontCheck@ needs it. +runConcurrency' :: C.MonadConc n + => Bool + -> Scheduler g + -> MemType + -> Context n g + -> ModelConc n a + -> n (CResult n g a) +runConcurrency' forSnapshot sched memtype ctx ma = do + (c, ref) <- runRefCont AStop (Just . Right) (runModelConc ma) + let threads0 = launch' Unmasked initialThread (const c) (cThreads ctx) + threads <- (if C.rtsSupportsBoundThreads then makeBound initialThread else pure) threads0 + runThreads forSnapshot sched memtype ref ctx { cThreads = threads } + -- | Like 'runConcurrency' but starts from a snapshot. -runConcurrencyWithSnapshot :: (MonadConc n, MonadRef r n) +runConcurrencyWithSnapshot :: C.MonadConc n => Scheduler g -> MemType - -> Context n r g - -> (Threads n r -> n ()) - -> r (Maybe (Either Failure a)) - -> n (CResult n r g a) + -> Context n g + -> (Threads n -> n ()) + -> C.CRef n (Maybe (Either Failure a)) + -> n (CResult n g a) runConcurrencyWithSnapshot sched memtype ctx restore ref = do let boundThreads = M.filter (isJust . _bound) (cThreads ctx) threads <- foldrM makeBound (cThreads ctx) (M.keys boundThreads) - let ctx' = ctx { cThreads = threads } - restore (cThreads ctx') - res <- runConcurrency'' False sched memtype ref ctx { cThreads = threads} + restore threads + res <- runThreads False sched memtype ref ctx { cThreads = threads } killAllThreads (finalContext res) pure res -- | Kill the remaining threads -killAllThreads :: MonadConc n => Context n r g -> n () +killAllThreads :: C.MonadConc n => Context n g -> n () killAllThreads ctx = let finalThreads = cThreads ctx in mapM_ (`kill` finalThreads) (M.keys finalThreads) --- | Run a concurrent program using the given context, and without --- killing threads which remain at the end. The context must have no --- main thread. -runConcurrency' :: (MonadConc n, MonadRef r n) - => Bool - -> Scheduler g - -> MemType - -> Context n r g - -> M n r a - -> n (CResult n r g a) -runConcurrency' forSnapshot sched memtype ctx ma = do - (c, ref) <- runRefCont AStop (Just . Right) (runM ma) - let threads0 = launch' Unmasked initialThread (const c) (cThreads ctx) - threads <- (if rtsSupportsBoundThreads then makeBound initialThread else pure) threads0 - runConcurrency'' forSnapshot sched memtype ref ctx { cThreads = threads} - --- | Like 'runConcurrency'' but doesn't do *ANY* set up at all. -runConcurrency'' :: (MonadConc n, MonadRef r n) - => Bool - -> Scheduler g - -> MemType - -> r (Maybe (Either Failure a)) - -> Context n r g - -> n (CResult n r g a) -runConcurrency'' forSnapshot sched memtype ref ctx = do - (finalCtx, trace, finalD, restore) <- runThreads forSnapshot sched memtype ref ctx - pure CResult - { finalContext = finalCtx - , finalRef = ref - , finalRestore = restore - , finalTrace = trace - , finalDecision = finalD - } +------------------------------------------------------------------------------- +-- * Execution -- | The context a collection of threads are running in. -data Context n r g = Context +data Context n g = Context { cSchedState :: g , cIdSource :: IdSource - , cThreads :: Threads n r - , cWriteBuf :: WriteBuffer r + , cThreads :: Threads n + , cWriteBuf :: WriteBuffer n , cCaps :: Int } -- | Run a collection of threads, until there are no threads left. -runThreads :: (MonadConc n, MonadRef r n) +runThreads :: C.MonadConc n => Bool -> Scheduler g -> MemType - -> r (Maybe (Either Failure a)) - -> Context n r g - -> n (Context n r g, SeqTrace, Maybe (ThreadId, ThreadAction), Maybe (Threads n r -> n ())) -runThreads forSnapshot sched memtype ref = go (const $ pure ()) Seq.empty Nothing where - go restore sofar prior ctx + -> C.CRef n (Maybe (Either Failure a)) + -> Context n g + -> n (CResult n g a) +runThreads forSnapshot sched memtype ref = schedule (const $ pure ()) Seq.empty Nothing where + -- signal failure & terminate + die reason finalR finalT finalD finalC = do + C.writeCRef ref (Just $ Left reason) + stop finalR finalT finalD finalC + + -- just terminate; 'ref' must have been written to before calling + -- this + stop finalR finalT finalD finalC = pure CResult + { finalContext = finalC + , finalRef = ref + , finalRestore = if forSnapshot then Just finalR else Nothing + , finalTrace = finalT + , finalDecision = finalD + } + + -- check for termination, pick a thread, and call 'step' + schedule restore sofar prior ctx | isTerminated = stop restore sofar prior ctx - | isDeadlocked = die restore sofar prior Deadlock ctx - | isSTMLocked = die restore sofar prior STMDeadlock ctx + | isDeadlocked = die Deadlock restore sofar prior ctx + | isSTMLocked = die STMDeadlock restore sofar prior ctx | otherwise = let ctx' = ctx { cSchedState = g' } in case choice of Just chosen -> case M.lookup chosen threadsc of Just thread - | isBlocked thread -> die restore sofar prior InternalError ctx' - | otherwise -> step chosen thread ctx' - Nothing -> die restore sofar prior InternalError ctx' - Nothing -> die restore sofar prior Abort ctx' + | isBlocked thread -> die InternalError restore sofar prior ctx' + | otherwise -> + let decision + | Just chosen == (fst <$> prior) = Continue + | (fst <$> prior) `notElem` map (Just . fst) runnable' = Start chosen + | otherwise = SwitchTo chosen + alternatives = filter (\(t, _) -> t /= chosen) runnable' + in step decision alternatives chosen thread restore sofar prior ctx' + Nothing -> die InternalError restore sofar prior ctx' + Nothing -> die Abort restore sofar prior ctx' where (choice, g') = scheduleThread sched prior (efromList "runThreads" runnable') (cSchedState ctx) runnable' = [(t, lookahead (_continuation a)) | (t, a) <- sortOn fst $ M.assocs runnable] @@ -197,59 +203,57 @@ isSTMLocked = M.null (M.filter (not . isBlocked) threads) && ((~= OnTVar []) <$> M.lookup initialThread threads) == Just True - unblockWaitingOn tid = fmap unblock where - unblock thrd = case _blocking thrd of - Just (OnMask t) | t == tid -> thrd { _blocking = Nothing } - _ -> thrd - - die restore' sofar' finalD reason finalCtx = do - writeRef ref (Just $ Left reason) - stop restore' sofar' finalD finalCtx - - stop restore' sofar' finalD finalCtx = - pure (finalCtx, sofar', finalD, if forSnapshot then Just restore' else Nothing) - - step chosen thread ctx' = do - (res, actOrTrc, actionSnap) <- stepThread - forSnapshot - (isNothing prior) - sched - memtype - chosen - (_continuation thread) - ctx { cSchedState = g' } - let trc = getTrc actOrTrc - let sofar' = sofar <> trc - let prior' = getPrior actOrTrc - let restore' threads' = - if forSnapshot - then restore threads' >> actionSnap threads' - else restore threads' - case res of - Succeeded ctx'' -> - let threads' = if (interruptible <$> M.lookup chosen (cThreads ctx'')) /= Just False - then unblockWaitingOn chosen (cThreads ctx'') - else cThreads ctx'' - ctx''' = ctx'' { cThreads = delCommitThreads threads' } - in go restore' sofar' prior' ctx''' - Failed failure -> - let ctx'' = ctx' { cThreads = delCommitThreads threads } - in die restore' sofar' prior' failure ctx'' - Snap ctx'' -> - stop actionSnap sofar' prior' ctx'' - where - decision - | Just chosen == (fst <$> prior) = Continue - | (fst <$> prior) `notElem` map (Just . fst) runnable' = Start chosen - | otherwise = SwitchTo chosen + -- run the chosen thread for one step and then pass control back to + -- 'schedule' + step decision alternatives chosen thread restore sofar prior ctx = do + (res, actOrTrc, actionSnap) <- stepThread + forSnapshot + (isNothing prior) + sched + memtype + chosen + (_continuation thread) + ctx + let sofar' = sofar <> getTrc actOrTrc + let prior' = getPrior actOrTrc + let restore' threads' = + if forSnapshot + then restore threads' >> actionSnap threads' + else restore threads' + let ctx' = fixContext chosen res ctx + case res of + Succeeded _ -> + schedule restore' sofar' prior' ctx' + Failed failure -> + die failure restore' sofar' prior' ctx' + Snap _ -> + stop actionSnap sofar' prior' ctx' + where + getTrc (Single a) = Seq.singleton (decision, alternatives, a) + getTrc (SubC as _) = (decision, alternatives, Subconcurrency) <| as - getTrc (Single a) = Seq.singleton (decision, alternatives, a) - getTrc (SubC as _) = (decision, alternatives, Subconcurrency) <| as + getPrior (Single a) = Just (chosen, a) + getPrior (SubC _ finalD) = finalD - alternatives = filter (\(t, _) -> t /= chosen) runnable' +-- | Apply the context update from stepping an action. +fixContext :: ThreadId -> What n g -> Context n g -> Context n g +fixContext chosen (Succeeded ctx@Context{..}) _ = + ctx { cThreads = delCommitThreads $ + if (interruptible <$> M.lookup chosen cThreads) /= Just False + then unblockWaitingOn chosen cThreads + else cThreads + } +fixContext _ (Failed _) ctx@Context{..} = + ctx { cThreads = delCommitThreads cThreads } +fixContext _ (Snap ctx@Context{..}) _ = + ctx { cThreads = delCommitThreads cThreads } - getPrior (Single a) = Just (chosen, a) - getPrior (SubC _ finalD) = finalD +-- | @unblockWaitingOn tid@ unblocks every thread blocked in a +-- @throwTo tid@. +unblockWaitingOn :: ThreadId -> Threads n -> Threads n +unblockWaitingOn tid = fmap $ \thread -> case _blocking thread of + Just (OnMask t) | t == tid -> thread { _blocking = Nothing } + _ -> thread -------------------------------------------------------------------------------- -- * Single-step execution @@ -263,20 +267,24 @@ deriving (Eq, Show) -- | What a thread did, for execution purposes. -data What n r g - = Succeeded (Context n r g) +data What n g + = Succeeded (Context n g) -- ^ Action succeeded: continue execution. | Failed Failure -- ^ Action caused computation to fail: stop. - | Snap (Context n r g) + | Snap (Context n g) -- ^ Action was a snapshot point and we're in snapshot mode: stop. -- | Run a single thread one step, by dispatching on the type of -- 'Action'. -- +-- Each case looks very similar. This is deliberate, so that the +-- essential differences between actions are more apparent, and not +-- hidden by accidental differences in how things are expressed. +-- -- Note: the returned snapshot action will definitely not do the right -- thing with relaxed memory. -stepThread :: forall n r g. (MonadConc n, MonadRef r n) +stepThread :: C.MonadConc n => Bool -- ^ Should we record a snapshot? -> Bool @@ -287,309 +295,440 @@ -- ^ The memory model to use. -> ThreadId -- ^ ID of the current thread - -> Action n r + -> Action n -- ^ Action to step - -> Context n r g + -> Context n g -- ^ The execution context. - -> n (What n r g, Act, Threads n r -> n ()) -stepThread forSnapshot isFirst sched memtype tid action ctx = case action of - -- start a new thread, assigning it the next 'ThreadId' - AFork n a b -> pure $ - let threads' = launch tid newtid a (cThreads ctx) - (idSource', newtid) = nextTId n (cIdSource ctx) - in (Succeeded ctx { cThreads = goto (b newtid) tid threads', cIdSource = idSource' }, Single (Fork newtid), noSnap) - - -- start a new bound thread, assigning it the next 'ThreadId' - AForkOS n a b -> do - let (idSource', newtid) = nextTId n (cIdSource ctx) - let threads' = launch tid newtid a (cThreads ctx) - threads'' <- makeBound newtid threads' - pure (Succeeded ctx { cThreads = goto (b newtid) tid threads'', cIdSource = idSource' }, Single (ForkOS newtid), noSnap) + -> n (What n g, Act, Threads n -> n ()) +-- start a new thread, assigning it the next 'ThreadId' +stepThread _ _ _ _ tid (AFork n a b) = \ctx@Context{..} -> pure $ + let (idSource', newtid) = nextTId n cIdSource + threads' = launch tid newtid a cThreads + in ( Succeeded ctx { cThreads = goto (b newtid) tid threads', cIdSource = idSource' } + , Single (Fork newtid) + , const (pure ()) + ) - -- check if the current thread is bound - AIsBound c -> - let isBound = isJust . _bound $ elookup "stepThread.AIsBound" tid (cThreads ctx) - in simple (goto (c isBound) tid (cThreads ctx)) (IsCurrentThreadBound isBound) noSnap +-- start a new bound thread, assigning it the next 'ThreadId' +stepThread _ _ _ _ tid (AForkOS n a b) = \ctx@Context{..} -> do + let (idSource', newtid) = nextTId n cIdSource + let threads' = launch tid newtid a cThreads + threads'' <- makeBound newtid threads' + pure ( Succeeded ctx { cThreads = goto (b newtid) tid threads'', cIdSource = idSource' } + , Single (ForkOS newtid) + , const (pure ()) + ) - -- get the 'ThreadId' of the current thread - AMyTId c -> simple (goto (c tid) tid (cThreads ctx)) MyThreadId noSnap +-- check if the current thread is bound +stepThread _ _ _ _ tid (AIsBound c) = \ctx@Context{..} -> do + let isBound = isJust . _bound $ elookup "stepThread.AIsBound" tid cThreads + pure ( Succeeded ctx { cThreads = goto (c isBound) tid cThreads } + , Single (IsCurrentThreadBound isBound) + , const (pure ()) + ) - -- get the number of capabilities - AGetNumCapabilities c -> simple (goto (c (cCaps ctx)) tid (cThreads ctx)) (GetNumCapabilities $ cCaps ctx) noSnap +-- get the 'ThreadId' of the current thread +stepThread _ _ _ _ tid (AMyTId c) = \ctx@Context{..} -> + pure ( Succeeded ctx { cThreads = goto (c tid) tid cThreads } + , Single MyThreadId + , const (pure ()) + ) - -- set the number of capabilities - ASetNumCapabilities i c -> pure - (Succeeded ctx { cThreads = goto c tid (cThreads ctx), cCaps = i }, Single (SetNumCapabilities i), noSnap) +-- get the number of capabilities +stepThread _ _ _ _ tid (AGetNumCapabilities c) = \ctx@Context{..} -> + pure ( Succeeded ctx { cThreads = goto (c cCaps) tid cThreads } + , Single (GetNumCapabilities cCaps) + , const (pure ()) + ) - -- yield the current thread - AYield c -> simple (goto c tid (cThreads ctx)) Yield noSnap +-- set the number of capabilities +stepThread _ _ _ _ tid (ASetNumCapabilities i c) = \ctx@Context{..} -> + pure ( Succeeded ctx { cThreads = goto c tid cThreads, cCaps = i } + , Single (SetNumCapabilities i) + , const (pure ()) + ) - -- yield the current thread (delay is ignored) - ADelay n c -> simple (goto c tid (cThreads ctx)) (ThreadDelay n) noSnap +-- yield the current thread +stepThread _ _ _ _ tid (AYield c) = \ctx@Context{..} -> + pure ( Succeeded ctx { cThreads = goto c tid cThreads } + , Single Yield + , const (pure ()) + ) - -- create a new @MVar@, using the next 'MVarId'. - ANewMVar n c -> do - let (idSource', newmvid) = nextMVId n (cIdSource ctx) - ref <- newRef Nothing - let mvar = MVar newmvid ref - pure ( Succeeded ctx { cThreads = goto (c mvar) tid (cThreads ctx), cIdSource = idSource' } - , Single (NewMVar newmvid) - , const (writeRef ref Nothing) - ) +-- yield the current thread (delay is ignored) +stepThread _ _ _ _ tid (ADelay n c) = \ctx@Context{..} -> + pure ( Succeeded ctx { cThreads = goto c tid cThreads } + , Single (ThreadDelay n) + , const (pure ()) + ) - -- put a value into a @MVar@, blocking the thread until it's empty. - APutMVar cvar@(MVar cvid _) a c -> synchronised $ do - (success, threads', woken, effect) <- putIntoMVar cvar a c tid (cThreads ctx) - simple threads' (if success then PutMVar cvid woken else BlockedPutMVar cvid) (const effect) +-- create a new @MVar@, using the next 'MVarId'. +stepThread _ _ _ _ tid (ANewMVar n c) = \ctx@Context{..} -> do + let (idSource', newmvid) = nextMVId n cIdSource + ref <- C.newCRef Nothing + let mvar = ModelMVar newmvid ref + pure ( Succeeded ctx { cThreads = goto (c mvar) tid cThreads, cIdSource = idSource' } + , Single (NewMVar newmvid) + , const (C.writeCRef ref Nothing) + ) - -- try to put a value into a @MVar@, without blocking. - ATryPutMVar cvar@(MVar cvid _) a c -> synchronised $ do - (success, threads', woken, effect) <- tryPutIntoMVar cvar a c tid (cThreads ctx) - simple threads' (TryPutMVar cvid success woken) (const effect) +-- put a value into a @MVar@, blocking the thread until it's empty. +stepThread _ _ _ _ tid (APutMVar mvar@ModelMVar{..} a c) = synchronised $ \ctx@Context{..} -> do + (success, threads', woken, effect) <- putIntoMVar mvar a c tid cThreads + pure ( Succeeded ctx { cThreads = threads' } + , Single (if success then PutMVar mvarId woken else BlockedPutMVar mvarId) + , const effect + ) - -- get the value from a @MVar@, without emptying, blocking the - -- thread until it's full. - AReadMVar cvar@(MVar cvid _) c -> synchronised $ do - (success, threads', _, _) <- readFromMVar cvar c tid (cThreads ctx) - simple threads' (if success then ReadMVar cvid else BlockedReadMVar cvid) noSnap +-- try to put a value into a @MVar@, without blocking. +stepThread _ _ _ _ tid (ATryPutMVar mvar@ModelMVar{..} a c) = synchronised $ \ctx@Context{..} -> do + (success, threads', woken, effect) <- tryPutIntoMVar mvar a c tid cThreads + pure ( Succeeded ctx { cThreads = threads' } + , Single (TryPutMVar mvarId success woken) + , const effect + ) - -- try to get the value from a @MVar@, without emptying, without - -- blocking. - ATryReadMVar cvar@(MVar cvid _) c -> synchronised $ do - (success, threads', _, _) <- tryReadFromMVar cvar c tid (cThreads ctx) - simple threads' (TryReadMVar cvid success) noSnap +-- get the value from a @MVar@, without emptying, blocking the thread +-- until it's full. +stepThread _ _ _ _ tid (AReadMVar mvar@ModelMVar{..} c) = synchronised $ \ctx@Context{..} -> do + (success, threads', _, _) <- readFromMVar mvar c tid cThreads + pure ( Succeeded ctx { cThreads = threads' } + , Single (if success then ReadMVar mvarId else BlockedReadMVar mvarId) + , const (pure ()) + ) - -- take the value from a @MVar@, blocking the thread until it's - -- full. - ATakeMVar cvar@(MVar cvid _) c -> synchronised $ do - (success, threads', woken, effect) <- takeFromMVar cvar c tid (cThreads ctx) - simple threads' (if success then TakeMVar cvid woken else BlockedTakeMVar cvid) (const effect) +-- try to get the value from a @MVar@, without emptying, without +-- blocking. +stepThread _ _ _ _ tid (ATryReadMVar mvar@ModelMVar{..} c) = synchronised $ \ctx@Context{..} -> do + (success, threads', _, _) <- tryReadFromMVar mvar c tid cThreads + pure ( Succeeded ctx { cThreads = threads' } + , Single (TryReadMVar mvarId success) + , const (pure ()) + ) - -- try to take the value from a @MVar@, without blocking. - ATryTakeMVar cvar@(MVar cvid _) c -> synchronised $ do - (success, threads', woken, effect) <- tryTakeFromMVar cvar c tid (cThreads ctx) - simple threads' (TryTakeMVar cvid success woken) (const effect) +-- take the value from a @MVar@, blocking the thread until it's full. +stepThread _ _ _ _ tid (ATakeMVar mvar@ModelMVar{..} c) = synchronised $ \ctx@Context{..} -> do + (success, threads', woken, effect) <- takeFromMVar mvar c tid cThreads + pure ( Succeeded ctx { cThreads = threads' } + , Single (if success then TakeMVar mvarId woken else BlockedTakeMVar mvarId) + , const effect + ) - -- create a new @CRef@, using the next 'CRefId'. - ANewCRef n a c -> do - let (idSource', newcrid) = nextCRId n (cIdSource ctx) - let val = (M.empty, 0, a) - ref <- newRef val - let cref = CRef newcrid ref - pure ( Succeeded ctx { cThreads = goto (c cref) tid (cThreads ctx), cIdSource = idSource' } - , Single (NewCRef newcrid) - , const (writeRef ref val) - ) +-- try to take the value from a @MVar@, without blocking. +stepThread _ _ _ _ tid (ATryTakeMVar mvar@ModelMVar{..} c) = synchronised $ \ctx@Context{..} -> do + (success, threads', woken, effect) <- tryTakeFromMVar mvar c tid cThreads + pure ( Succeeded ctx { cThreads = threads' } + , Single (TryTakeMVar mvarId success woken) + , const effect + ) - -- read from a @CRef@. - AReadCRef cref@(CRef crid _) c -> do - val <- readCRef cref tid - simple (goto (c val) tid (cThreads ctx)) (ReadCRef crid) noSnap +-- create a new @CRef@, using the next 'CRefId'. +stepThread _ _ _ _ tid (ANewCRef n a c) = \ctx@Context{..} -> do + let (idSource', newcrid) = nextCRId n cIdSource + let val = (M.empty, 0, a) + ref <- C.newCRef val + let cref = ModelCRef newcrid ref + pure ( Succeeded ctx { cThreads = goto (c cref) tid cThreads, cIdSource = idSource' } + , Single (NewCRef newcrid) + , const (C.writeCRef ref val) + ) - -- read from a @CRef@ for future compare-and-swap operations. - AReadCRefCas cref@(CRef crid _) c -> do - tick <- readForTicket cref tid - simple (goto (c tick) tid (cThreads ctx)) (ReadCRefCas crid) noSnap +-- read from a @CRef@. +stepThread _ _ _ _ tid (AReadCRef cref@ModelCRef{..} c) = \ctx@Context{..} -> do + val <- readCRef cref tid + pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads } + , Single (ReadCRef crefId) + , const (pure ()) + ) - -- modify a @CRef@. - AModCRef cref@(CRef crid _) f c -> synchronised $ do - (new, val) <- f <$> readCRef cref tid - effect <- writeImmediate cref new - simple (goto (c val) tid (cThreads ctx)) (ModCRef crid) (const effect) +-- read from a @CRef@ for future compare-and-swap operations. +stepThread _ _ _ _ tid (AReadCRefCas cref@ModelCRef{..} c) = \ctx@Context{..} -> do + tick <- readForTicket cref tid + pure ( Succeeded ctx { cThreads = goto (c tick) tid cThreads } + , Single (ReadCRefCas crefId) + , const (pure ()) + ) - -- modify a @CRef@ using a compare-and-swap. - AModCRefCas cref@(CRef crid _) f c -> synchronised $ do - tick@(Ticket _ _ old) <- readForTicket cref tid - let (new, val) = f old - (_, _, effect) <- casCRef cref tid tick new - simple (goto (c val) tid (cThreads ctx)) (ModCRefCas crid) (const effect) +-- modify a @CRef@. +stepThread _ _ _ _ tid (AModCRef cref@ModelCRef{..} f c) = synchronised $ \ctx@Context{..} -> do + (new, val) <- f <$> readCRef cref tid + effect <- writeImmediate cref new + pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads } + , Single (ModCRef crefId) + , const effect + ) - -- write to a @CRef@ without synchronising. - AWriteCRef cref@(CRef crid _) a c -> case memtype of - -- write immediately. - SequentialConsistency -> do - effect <- writeImmediate cref a - simple (goto c tid (cThreads ctx)) (WriteCRef crid) (const effect) - -- add to buffer using thread id. - TotalStoreOrder -> do - wb' <- bufferWrite (cWriteBuf ctx) (tid, Nothing) cref a - pure (Succeeded ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Single (WriteCRef crid), noSnap) - -- add to buffer using both thread id and cref id - PartialStoreOrder -> do - wb' <- bufferWrite (cWriteBuf ctx) (tid, Just crid) cref a - pure (Succeeded ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Single (WriteCRef crid), noSnap) +-- modify a @CRef@ using a compare-and-swap. +stepThread _ _ _ _ tid (AModCRefCas cref@ModelCRef{..} f c) = synchronised $ \ctx@Context{..} -> do + tick@(ModelTicket _ _ old) <- readForTicket cref tid + let (new, val) = f old + (_, _, effect) <- casCRef cref tid tick new + pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads } + , Single (ModCRefCas crefId) + , const effect + ) - -- perform a compare-and-swap on a @CRef@. - ACasCRef cref@(CRef crid _) tick a c -> synchronised $ do - (suc, tick', effect) <- casCRef cref tid tick a - simple (goto (c (suc, tick')) tid (cThreads ctx)) (CasCRef crid suc) (const effect) +-- write to a @CRef@ without synchronising. +stepThread _ _ _ memtype tid (AWriteCRef cref@ModelCRef{..} a c) = \ctx@Context{..} -> case memtype of + -- write immediately. + SequentialConsistency -> do + effect <- writeImmediate cref a + pure ( Succeeded ctx { cThreads = goto c tid cThreads } + , Single (WriteCRef crefId) + , const effect + ) + -- add to buffer using thread id. + TotalStoreOrder -> do + wb' <- bufferWrite cWriteBuf (tid, Nothing) cref a + pure ( Succeeded ctx { cThreads = goto c tid cThreads, cWriteBuf = wb' } + , Single (WriteCRef crefId) + , const (pure ()) + ) + -- add to buffer using both thread id and cref id + PartialStoreOrder -> do + wb' <- bufferWrite cWriteBuf (tid, Just crefId) cref a + pure ( Succeeded ctx { cThreads = goto c tid cThreads, cWriteBuf = wb' } + , Single (WriteCRef crefId) + , const (pure ()) + ) - -- commit a @CRef@ write - ACommit t c -> do - wb' <- case memtype of - -- shouldn't ever get here - SequentialConsistency -> - fatal "stepThread.ACommit" "Attempting to commit under SequentialConsistency" - -- commit using the thread id. - TotalStoreOrder -> commitWrite (cWriteBuf ctx) (t, Nothing) - -- commit using the cref id. - PartialStoreOrder -> commitWrite (cWriteBuf ctx) (t, Just c) - pure (Succeeded ctx { cWriteBuf = wb' }, Single (CommitCRef t c), noSnap) +-- perform a compare-and-swap on a @CRef@. +stepThread _ _ _ _ tid (ACasCRef cref@ModelCRef{..} tick a c) = synchronised $ \ctx@Context{..} -> do + (suc, tick', effect) <- casCRef cref tid tick a + pure ( Succeeded ctx { cThreads = goto (c (suc, tick')) tid cThreads } + , Single (CasCRef crefId suc) + , const effect + ) - -- run a STM transaction atomically. - AAtom stm c -> synchronised $ do - let transaction = runTransaction stm (cIdSource ctx) - let effect = const (void transaction) - (res, idSource', trace) <- transaction - case res of - Success _ written val -> - let (threads', woken) = wake (OnTVar written) (cThreads ctx) - in pure (Succeeded ctx { cThreads = goto (c val) tid threads', cIdSource = idSource' }, Single (STM trace woken), effect) - Retry touched -> - let threads' = block (OnTVar touched) tid (cThreads ctx) - in pure (Succeeded ctx { cThreads = threads', cIdSource = idSource'}, Single (BlockedSTM trace), effect) - Exception e -> do - let act = STM trace [] - res' <- stepThrow tid (cThreads ctx) act e - pure $ case res' of - (Succeeded ctx', _, effect') -> (Succeeded ctx' { cIdSource = idSource' }, Single act, effect') - (Failed err, _, effect') -> (Failed err, Single act, effect') - (Snap _, _, _) -> fatal "stepThread.AAtom" "Unexpected snapshot while propagating STM exception" +-- commit a @CRef@ write +stepThread _ _ _ memtype _ (ACommit t c) = \ctx@Context{..} -> do + wb' <- case memtype of + -- shouldn't ever get here + SequentialConsistency -> + fatal "stepThread.ACommit" "Attempting to commit under SequentialConsistency" + -- commit using the thread id. + TotalStoreOrder -> + commitWrite cWriteBuf (t, Nothing) + -- commit using the cref id. + PartialStoreOrder -> + commitWrite cWriteBuf (t, Just c) + pure ( Succeeded ctx { cWriteBuf = wb' } + , Single (CommitCRef t c) + , const (pure ()) + ) - -- lift an action from the underlying monad into the @Conc@ - -- computation. - ALift na -> do - let effect threads = runLiftedAct tid threads na - a <- effect (cThreads ctx) - simple (goto a tid (cThreads ctx)) LiftIO (void <$> effect) +-- run a STM transaction atomically. +stepThread _ _ _ _ tid (AAtom stm c) = synchronised $ \ctx@Context{..} -> do + let transaction = runTransaction stm cIdSource + let effect = const (void transaction) + (res, idSource', trace) <- transaction + case res of + Success _ written val -> do + let (threads', woken) = wake (OnTVar written) cThreads + pure ( Succeeded ctx { cThreads = goto (c val) tid threads', cIdSource = idSource' } + , Single (STM trace woken) + , effect + ) + Retry touched -> do + let threads' = block (OnTVar touched) tid cThreads + pure ( Succeeded ctx { cThreads = threads', cIdSource = idSource'} + , Single (BlockedSTM trace) + , effect + ) + Exception e -> do + let act = STM trace [] + res' <- stepThrow act tid e ctx + pure $ case res' of + (Succeeded ctx', _, effect') -> (Succeeded ctx' { cIdSource = idSource' }, Single act, effect') + (Failed err, _, effect') -> (Failed err, Single act, effect') + (Snap _, _, _) -> fatal "stepThread.AAtom" "Unexpected snapshot while propagating STM exception" - -- throw an exception, and propagate it to the appropriate - -- handler. - AThrow e -> stepThrow tid (cThreads ctx) Throw e +-- lift an action from the underlying monad into the @Conc@ +-- computation. +stepThread _ _ _ _ tid (ALift na) = \ctx@Context{..} -> do + let effect threads = runLiftedAct tid threads na + a <- effect cThreads + pure (Succeeded ctx { cThreads = goto a tid cThreads } + , Single LiftIO + , void <$> effect + ) - -- throw an exception to the target thread, and propagate it to - -- the appropriate handler. - AThrowTo t e c -> synchronised $ - let threads' = goto c tid (cThreads ctx) - blocked = block (OnMask t) tid (cThreads ctx) - in case M.lookup t (cThreads ctx) of - Just thread - | interruptible thread -> stepThrow t threads' (ThrowTo t) e - | otherwise -> simple blocked (BlockedThrowTo t) noSnap - Nothing -> simple threads' (ThrowTo t) noSnap +-- throw an exception, and propagate it to the appropriate handler. +stepThread _ _ _ _ tid (AThrow e) = stepThrow Throw tid e - -- run a subcomputation in an exception-catching context. - ACatching h ma c -> - let a = runCont ma (APopCatching . c) - e exc = runCont (h exc) c - threads' = goto a tid (catching e tid (cThreads ctx)) - in simple threads' Catching noSnap +-- throw an exception to the target thread, and propagate it to the +-- appropriate handler. +stepThread _ _ _ _ tid (AThrowTo t e c) = synchronised $ \ctx@Context{..} -> + let threads' = goto c tid cThreads + blocked = block (OnMask t) tid cThreads + in case M.lookup t cThreads of + Just thread + | interruptible thread -> stepThrow (ThrowTo t) t e ctx { cThreads = threads' } + | otherwise -> pure + ( Succeeded ctx { cThreads = blocked } + , Single (BlockedThrowTo t) + , const (pure ()) + ) + Nothing -> pure + (Succeeded ctx { cThreads = threads' } + , Single (ThrowTo t) + , const (pure ()) + ) - -- pop the top exception handler from the thread's stack. - APopCatching a -> - let threads' = goto a tid (uncatching tid (cThreads ctx)) - in simple threads' PopCatching noSnap +-- run a subcomputation in an exception-catching context. +stepThread _ _ _ _ tid (ACatching h ma c) = \ctx@Context{..} -> pure $ + let a = runModelConc ma (APopCatching . c) + e exc = runModelConc (h exc) c + in ( Succeeded ctx { cThreads = goto a tid (catching e tid cThreads) } + , Single Catching + , const (pure ()) + ) - -- execute a subcomputation with a new masking state, and give it - -- a function to run a computation with the current masking state. - AMasking m ma c -> - let a = runCont (ma umask) (AResetMask False False m' . c) - m' = _masking $ elookup "stepThread.AMasking" tid (cThreads ctx) - umask mb = resetMask True m' >> mb >>= \b -> resetMask False m >> pure b - resetMask typ ms = cont $ \k -> AResetMask typ True ms $ k () - threads' = goto a tid (mask m tid (cThreads ctx)) - in simple threads' (SetMasking False m) noSnap +-- pop the top exception handler from the thread's stack. +stepThread _ _ _ _ tid (APopCatching a) = \ctx@Context{..} -> + pure ( Succeeded ctx { cThreads = goto a tid (uncatching tid cThreads) } + , Single PopCatching + , const (pure ()) + ) +-- execute a subcomputation with a new masking state, and give it a +-- function to run a computation with the current masking state. +stepThread _ _ _ _ tid (AMasking m ma c) = \ctx@Context{..} -> pure $ + let resetMask typ ms = ModelConc $ \k -> AResetMask typ True ms $ k () + umask mb = resetMask True m' >> mb >>= \b -> resetMask False m >> pure b + m' = _masking $ elookup "stepThread.AMasking" tid cThreads + a = runModelConc (ma umask) (AResetMask False False m' . c) + in ( Succeeded ctx { cThreads = goto a tid (mask m tid cThreads) } + , Single (SetMasking False m) + , const (pure ()) + ) - -- reset the masking thread of the state. - AResetMask b1 b2 m c -> - let act = (if b1 then SetMasking else ResetMasking) b2 m - threads' = goto c tid (mask m tid (cThreads ctx)) - in simple threads' act noSnap +-- reset the masking thread of the state. +stepThread _ _ _ _ tid (AResetMask b1 b2 m c) = \ctx@Context{..} -> + pure ( Succeeded ctx { cThreads = goto c tid (mask m tid cThreads) } + , Single ((if b1 then SetMasking else ResetMasking) b2 m) + , const (pure ()) + ) - -- execute a 'return' or 'pure'. - AReturn c -> simple (goto c tid (cThreads ctx)) Return noSnap +-- execute a 'return' or 'pure'. +stepThread _ _ _ _ tid (AReturn c) = \ctx@Context{..} -> + pure ( Succeeded ctx { cThreads = goto c tid cThreads } + , Single Return + , const (pure ()) + ) - -- kill the current thread. - AStop na -> do - na - threads' <- kill tid (cThreads ctx) - simple threads' Stop noSnap +-- kill the current thread. +stepThread _ _ _ _ tid (AStop na) = \ctx@Context{..} -> do + na + threads' <- kill tid cThreads + pure ( Succeeded ctx { cThreads = threads' } + , Single Stop + , const (pure ()) + ) - -- run a subconcurrent computation. - ASub ma c - | forSnapshot -> pure (Failed IllegalSubconcurrency, Single Subconcurrency, noSnap) - | M.size (cThreads ctx) > 1 -> pure (Failed IllegalSubconcurrency, Single Subconcurrency, noSnap) - | otherwise -> do - res <- runConcurrency False sched memtype (cSchedState ctx) (cIdSource ctx) (cCaps ctx) ma - out <- efromJust "stepThread.ASub" <$> readRef (finalRef res) - pure (Succeeded ctx +-- run a subconcurrent computation. +stepThread forSnapshot _ sched memtype tid (ASub ma c) = \ctx -> + if | forSnapshot -> pure (Failed IllegalSubconcurrency, Single Subconcurrency, const (pure ())) + | M.size (cThreads ctx) > 1 -> pure (Failed IllegalSubconcurrency, Single Subconcurrency, const (pure ())) + | otherwise -> do + res <- runConcurrency False sched memtype (cSchedState ctx) (cIdSource ctx) (cCaps ctx) ma + out <- efromJust "stepThread.ASub" <$> C.readCRef (finalRef res) + pure ( Succeeded ctx { cThreads = goto (AStopSub (c out)) tid (cThreads ctx) , cIdSource = cIdSource (finalContext res) , cSchedState = cSchedState (finalContext res) } - , SubC (finalTrace res) (finalDecision res) - , noSnap - ) - - -- after the end of a subconcurrent computation. does nothing, - -- only exists so that: there is an entry in the trace for - -- returning to normal computation; and every item in the trace - -- corresponds to a scheduling point. - AStopSub c -> simple (goto c tid (cThreads ctx)) StopSubconcurrency noSnap - - -- run an action atomically, with a non-preemptive length bounded - -- round robin scheduler, under sequential consistency. - ADontCheck lb ma c - | isFirst -> do - -- create a restricted context - threads' <- kill tid (cThreads ctx) - let dcCtx = ctx { cThreads = threads', cSchedState = lb } - res <- runConcurrency' forSnapshot dcSched SequentialConsistency dcCtx ma - out <- efromJust "stepThread.ADontCheck" <$> readRef (finalRef res) - case out of - Right a -> do - let threads'' = launch' Unmasked tid (const (c a)) (cThreads (finalContext res)) - threads''' <- (if rtsSupportsBoundThreads then makeBound tid else pure) threads'' - pure ( (if forSnapshot then Snap else Succeeded) (finalContext res) { cThreads = threads''', cSchedState = cSchedState ctx } - , Single (DontCheck (toList (finalTrace res))) - , fromMaybe noSnap (finalRestore res) - ) - Left f -> - pure (Failed f, Single (DontCheck (toList (finalTrace res))), noSnap) - | otherwise -> pure (Failed IllegalDontCheck, Single (DontCheck []), noSnap) - where - - -- this is not inline in the long @case@ above as it's needed by - -- @AAtom@, @AThrow@, and @AThrowTo@. - stepThrow t ts act e = - let some = toException e - in case propagate some t ts of - Just ts' -> simple ts' act noSnap - Nothing - | t == initialThread -> pure (Failed (UncaughtException some), Single act, noSnap) - | otherwise -> do - ts' <- kill t ts - simple ts' act noSnap + , SubC (finalTrace res) (finalDecision res) + , const (pure ()) + ) - -- helper for actions which only change the threads. - simple threads' act effect = pure (Succeeded ctx { cThreads = threads' }, Single act, effect) +-- after the end of a subconcurrent computation. does nothing, only +-- exists so that: there is an entry in the trace for returning to +-- normal computation; and every item in the trace corresponds to a +-- scheduling point. +stepThread _ _ _ _ tid (AStopSub c) = \ctx@Context{..} -> + pure ( Succeeded ctx { cThreads = goto c tid cThreads } + , Single StopSubconcurrency + , const (pure ()) + ) - -- helper for actions impose a write barrier. - synchronised ma = do - writeBarrier (cWriteBuf ctx) - res <- ma +-- run an action atomically, with a non-preemptive length bounded +-- round robin scheduler, under sequential consistency. +stepThread forSnapshot isFirst _ _ tid (ADontCheck lb ma c) = \ctx -> + if | isFirst -> do + -- create a restricted context + threads' <- kill tid (cThreads ctx) + let dcCtx = ctx { cThreads = threads', cSchedState = lb } + res <- runConcurrency' forSnapshot dcSched SequentialConsistency dcCtx ma + out <- efromJust "stepThread.ADontCheck" <$> C.readCRef (finalRef res) + case out of + Right a -> do + let threads'' = launch' Unmasked tid (const (c a)) (cThreads (finalContext res)) + threads''' <- (if C.rtsSupportsBoundThreads then makeBound tid else pure) threads'' + pure ( (if forSnapshot then Snap else Succeeded) (finalContext res) + { cThreads = threads''', cSchedState = cSchedState ctx } + , Single (DontCheck (toList (finalTrace res))) + , fromMaybe (const (pure ())) (finalRestore res) + ) + Left f -> pure + ( Failed f + , Single (DontCheck (toList (finalTrace res))) + , const (pure ()) + ) + | otherwise -> pure + ( Failed IllegalDontCheck + , Single (DontCheck []) + , const (pure ()) + ) - pure $ case res of - (Succeeded ctx', act, effect) -> (Succeeded ctx' { cWriteBuf = emptyBuffer }, act, effect) - _ -> res +-- | Handle an exception being thrown from an @AAtom@, @AThrow@, or +-- @AThrowTo@. +stepThrow :: (C.MonadConc n, Exception e) + => ThreadAction + -- ^ Action to include in the trace. + -> ThreadId + -- ^ The thread receiving the exception. + -> e + -- ^ Exception to raise. + -> Context n g + -- ^ The execution context. + -> n (What n g, Act, Threads n -> n ()) +stepThrow act tid e ctx@Context{..} = case propagate some tid cThreads of + Just ts' -> pure + ( Succeeded ctx { cThreads = ts' } + , Single act + , const (pure ()) + ) + Nothing + | tid == initialThread -> pure + ( Failed (UncaughtException some) + , Single act + , const (pure ()) + ) + | otherwise -> do + ts' <- kill tid cThreads + pure ( Succeeded ctx { cThreads = ts' } + , Single act + , const (pure ()) + ) + where + some = toException e - -- scheduler for @ADontCheck@ - dcSched = Scheduler go where - go _ _ (Just 0) = (Nothing, Just 0) - go prior threads s = - let (t, _) = scheduleThread roundRobinSchedNP prior threads () - in (t, fmap (\lb -> lb - 1) s) +-- | Helper for actions impose a write barrier. +synchronised :: C.MonadConc n + => (Context n g -> n (What n g, Act, Threads n -> n ())) + -- ^ Action to run after the write barrier. + -> Context n g + -- ^ The original execution context. + -> n (What n g, Act, Threads n -> n ()) +synchronised ma ctx@Context{..} = do + writeBarrier cWriteBuf + ma ctx { cWriteBuf = emptyBuffer } - -- no snapshot - noSnap _ = pure () +-- | scheduler for @ADontCheck@ +dcSched :: Scheduler (Maybe Int) +dcSched = Scheduler go where + go _ _ (Just 0) = (Nothing, Just 0) + go prior threads s = + let (t, _) = scheduleThread roundRobinSchedNP prior threads () + in (t, fmap (\lb -> lb - 1) s) 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 @@ -16,8 +16,9 @@ module Test.DejaFu.Conc.Internal.Common where import Control.Exception (Exception, MaskingState(..)) +import qualified Control.Monad.Conc.Class as C import Data.Map.Strict (Map) -import Test.DejaFu.Conc.Internal.STM (S) +import Test.DejaFu.Conc.Internal.STM (ModelSTM) import Test.DejaFu.Types #if MIN_VERSION_base(4,9,0) @@ -25,7 +26,7 @@ #endif -------------------------------------------------------------------------------- --- * The @Conc@ Monad +-- * The @ModelConc@ Monad -- | The underlying monad is based on continuations over 'Action's. -- @@ -35,73 +36,52 @@ -- current expression of threads and exception handlers very difficult -- (perhaps even not possible without significant reworking), so I -- abandoned the attempt. -newtype M n r a = M { runM :: (a -> Action n r) -> Action n r } +newtype ModelConc n a = ModelConc { runModelConc :: (a -> Action n) -> Action n } -instance Functor (M n r) where - fmap f m = M $ \ c -> runM m (c . f) +instance Functor (ModelConc n) where + fmap f m = ModelConc $ \c -> runModelConc m (c . f) -instance Applicative (M n r) where +instance Applicative (ModelConc n) where -- without the @AReturn@, a thread could lock up testing by -- entering an infinite loop (eg: @forever (return ())@) - pure x = M $ \c -> AReturn $ c x - f <*> v = M $ \c -> runM f (\g -> runM v (c . g)) + pure x = ModelConc $ \c -> AReturn $ c x + f <*> v = ModelConc $ \c -> runModelConc f (\g -> runModelConc v (c . g)) -instance Monad (M n r) where +instance Monad (ModelConc n) where return = pure - m >>= k = M $ \c -> runM m (\x -> runM (k x) c) + m >>= k = ModelConc $ \c -> runModelConc m (\x -> runModelConc (k x) c) #if MIN_VERSION_base(4,9,0) fail = Fail.fail --- | @since 0.7.1.2 -instance Fail.MonadFail (M n r) where +instance Fail.MonadFail (ModelConc n) where #endif - fail e = cont (\_ -> AThrow (MonadFailException e)) + fail e = ModelConc $ \_ -> AThrow (MonadFailException e) --- | The concurrent variable type used with the 'Conc' monad. One --- notable difference between these and 'MVar's is that 'MVar's are --- single-wakeup, and wake up in a FIFO order. Writing to a @MVar@ --- wakes up all threads blocked on reading it, and it is up to the --- scheduler which one runs next. Taking from a @MVar@ behaves --- analogously. -data MVar r a = MVar - { _cvarId :: MVarId - , _cvarVal :: r (Maybe a) +-- | An @MVar@ is modelled as a unique ID and a reference holding a +-- @Maybe@ value. +data ModelMVar n a = ModelMVar + { mvarId :: MVarId + , mvarRef :: C.CRef n (Maybe a) } --- | The mutable non-blocking reference type. These are like 'IORef's. --- --- @CRef@s are represented as a unique numeric identifier and a --- reference containing (a) any thread-local non-synchronised writes --- (so each thread sees its latest write), (b) a commit count (used in --- compare-and-swaps), and (c) the current value visible to all --- threads. -data CRef r a = CRef - { _crefId :: CRefId - , _crefVal :: r (Map ThreadId a, Integer, a) +-- | A @CRef@ is modelled as a unique ID and a reference holding +-- thread-local values, the number of commits, and the most recent +-- committed value. +data ModelCRef n a = ModelCRef + { crefId :: CRefId + , crefRef :: C.CRef n (Map ThreadId a, Integer, a) } --- | The compare-and-swap proof type. --- --- @Ticket@s are represented as just a wrapper around the identifier --- of the 'CRef' it came from, the commit count at the time it was --- produced, and an @a@ value. This doesn't work in the source package --- (atomic-primops) because of the need to use pointer equality. Here --- we can just pack extra information into 'CRef' to avoid that need. -data Ticket a = Ticket - { _ticketCRef :: CRefId - , _ticketWrites :: Integer - , _ticketVal :: a +-- | A @Ticket@ is modelled as the ID of the @ModelCRef@ it came from, +-- the commits to the @ModelCRef@ at the time it was produced, and the +-- value observed. +data ModelTicket a = ModelTicket + { ticketCRef :: CRefId + , ticketWrites :: Integer + , ticketVal :: a } --- | Construct a continuation-passing operation from a function. -cont :: ((a -> Action n r) -> Action n r) -> M n r a -cont = M - --- | Run a CPS computation with the given final computation. -runCont :: M n r a -> (a -> Action n r) -> Action n r -runCont = runM - -------------------------------------------------------------------------------- -- * Primitive Actions @@ -109,55 +89,55 @@ -- only occur as a result of an action, and they cover (most of) the -- primitives of the concurrency. 'spawn' is absent as it is -- implemented in terms of 'newEmptyMVar', 'fork', and 'putMVar'. -data Action n r = - AFork String ((forall b. M n r b -> M n r b) -> Action n r) (ThreadId -> Action n r) - | AForkOS String ((forall b. M n r b -> M n r b) -> Action n r) (ThreadId -> Action n r) - | AIsBound (Bool -> Action n r) - | AMyTId (ThreadId -> Action n r) +data Action n = + AFork String ((forall b. ModelConc n b -> ModelConc n b) -> Action n) (ThreadId -> Action n) + | AForkOS String ((forall b. ModelConc n b -> ModelConc n b) -> Action n) (ThreadId -> Action n) + | AIsBound (Bool -> Action n) + | AMyTId (ThreadId -> Action n) - | AGetNumCapabilities (Int -> Action n r) - | ASetNumCapabilities Int (Action n r) + | AGetNumCapabilities (Int -> Action n) + | ASetNumCapabilities Int (Action n) - | forall a. ANewMVar String (MVar r a -> Action n r) - | forall a. APutMVar (MVar r a) a (Action n r) - | forall a. ATryPutMVar (MVar r a) a (Bool -> Action n r) - | forall a. AReadMVar (MVar r a) (a -> Action n r) - | forall a. ATryReadMVar (MVar r a) (Maybe a -> Action n r) - | forall a. ATakeMVar (MVar r a) (a -> Action n r) - | forall a. ATryTakeMVar (MVar r a) (Maybe a -> Action n r) + | forall a. ANewMVar String (ModelMVar n a -> Action n) + | forall a. APutMVar (ModelMVar n a) a (Action n) + | forall a. ATryPutMVar (ModelMVar n a) a (Bool -> Action n) + | forall a. AReadMVar (ModelMVar n a) (a -> Action n) + | forall a. ATryReadMVar (ModelMVar n a) (Maybe a -> Action n) + | forall a. ATakeMVar (ModelMVar n a) (a -> Action n) + | forall a. ATryTakeMVar (ModelMVar n a) (Maybe a -> Action n) - | forall a. ANewCRef String a (CRef r a -> Action n r) - | forall a. AReadCRef (CRef r a) (a -> Action n r) - | forall a. AReadCRefCas (CRef r a) (Ticket a -> Action n r) - | forall a b. AModCRef (CRef r a) (a -> (a, b)) (b -> Action n r) - | forall a b. AModCRefCas (CRef r a) (a -> (a, b)) (b -> Action n r) - | forall a. AWriteCRef (CRef r a) a (Action n r) - | forall a. ACasCRef (CRef r a) (Ticket a) a ((Bool, Ticket a) -> Action n r) + | forall a. ANewCRef String a (ModelCRef n a -> Action n) + | forall a. AReadCRef (ModelCRef n a) (a -> Action n) + | forall a. AReadCRefCas (ModelCRef n a) (ModelTicket a -> Action n) + | forall a b. AModCRef (ModelCRef n a) (a -> (a, b)) (b -> Action n) + | forall a b. AModCRefCas (ModelCRef n a) (a -> (a, b)) (b -> Action n) + | forall a. AWriteCRef (ModelCRef n a) a (Action n) + | forall a. ACasCRef (ModelCRef n a) (ModelTicket a) a ((Bool, ModelTicket a) -> Action n) | forall e. Exception e => AThrow e - | forall e. Exception e => AThrowTo ThreadId e (Action n r) - | forall a e. Exception e => ACatching (e -> M n r a) (M n r a) (a -> Action n r) - | APopCatching (Action n r) - | forall a. AMasking MaskingState ((forall b. M n r b -> M n r b) -> M n r a) (a -> Action n r) - | AResetMask Bool Bool MaskingState (Action n r) + | forall e. Exception e => AThrowTo ThreadId e (Action n) + | forall a e. Exception e => ACatching (e -> ModelConc n a) (ModelConc n a) (a -> Action n) + | APopCatching (Action n) + | forall a. AMasking MaskingState ((forall b. ModelConc n b -> ModelConc n b) -> ModelConc n a) (a -> Action n) + | AResetMask Bool Bool MaskingState (Action n) - | forall a. AAtom (S n r a) (a -> Action n r) - | ALift (n (Action n r)) - | AYield (Action n r) - | ADelay Int (Action n r) - | AReturn (Action n r) + | forall a. AAtom (ModelSTM n a) (a -> Action n) + | ALift (n (Action n)) + | AYield (Action n) + | ADelay Int (Action n) + | AReturn (Action n) | ACommit ThreadId CRefId | AStop (n ()) - | forall a. ASub (M n r a) (Either Failure a -> Action n r) - | AStopSub (Action n r) - | forall a. ADontCheck (Maybe Int) (M n r a) (a -> Action n r) + | forall a. ASub (ModelConc n a) (Either Failure a -> Action n) + | AStopSub (Action n) + | forall a. ADontCheck (Maybe Int) (ModelConc n a) (a -> Action n) -------------------------------------------------------------------------------- -- * Scheduling & Traces -- | Look as far ahead in the given continuation as possible. -lookahead :: Action n r -> Lookahead +lookahead :: Action n -> Lookahead lookahead (AFork _ _ _) = WillFork lookahead (AForkOS _ _ _) = WillForkOS lookahead (AIsBound _) = WillIsCurrentThreadBound @@ -165,19 +145,19 @@ lookahead (AGetNumCapabilities _) = WillGetNumCapabilities lookahead (ASetNumCapabilities i _) = WillSetNumCapabilities i lookahead (ANewMVar _ _) = WillNewMVar -lookahead (APutMVar (MVar c _) _ _) = WillPutMVar c -lookahead (ATryPutMVar (MVar c _) _ _) = WillTryPutMVar c -lookahead (AReadMVar (MVar c _) _) = WillReadMVar c -lookahead (ATryReadMVar (MVar c _) _) = WillTryReadMVar c -lookahead (ATakeMVar (MVar c _) _) = WillTakeMVar c -lookahead (ATryTakeMVar (MVar c _) _) = WillTryTakeMVar c +lookahead (APutMVar (ModelMVar m _) _ _) = WillPutMVar m +lookahead (ATryPutMVar (ModelMVar m _) _ _) = WillTryPutMVar m +lookahead (AReadMVar (ModelMVar m _) _) = WillReadMVar m +lookahead (ATryReadMVar (ModelMVar m _) _) = WillTryReadMVar m +lookahead (ATakeMVar (ModelMVar m _) _) = WillTakeMVar m +lookahead (ATryTakeMVar (ModelMVar m _) _) = WillTryTakeMVar m lookahead (ANewCRef _ _ _) = WillNewCRef -lookahead (AReadCRef (CRef r _) _) = WillReadCRef r -lookahead (AReadCRefCas (CRef r _) _) = WillReadCRefCas r -lookahead (AModCRef (CRef r _) _ _) = WillModCRef r -lookahead (AModCRefCas (CRef r _) _ _) = WillModCRefCas r -lookahead (AWriteCRef (CRef r _) _ _) = WillWriteCRef r -lookahead (ACasCRef (CRef r _) _ _ _) = WillCasCRef r +lookahead (AReadCRef (ModelCRef r _) _) = WillReadCRef r +lookahead (AReadCRefCas (ModelCRef r _) _) = WillReadCRefCas r +lookahead (AModCRef (ModelCRef r _) _ _) = WillModCRef r +lookahead (AModCRefCas (ModelCRef r _) _ _) = WillModCRefCas r +lookahead (AWriteCRef (ModelCRef r _) _ _) = WillWriteCRef r +lookahead (ACasCRef (ModelCRef r _) _ _ _) = WillCasCRef r lookahead (ACommit t c) = WillCommitCRef t c lookahead (AAtom _ _) = WillSTM lookahead (AThrow _) = WillThrow 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 @@ -1,6 +1,7 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE GADTs #-} -{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RecordWildCards #-} -- | -- Module : Test.DejaFu.Conc.Internal.Memory @@ -8,7 +9,7 @@ -- License : MIT -- Maintainer : Michael Walker -- Stability : experimental --- Portability : BangPatterns, GADTs, MultiParamTypeClasses +-- Portability : BangPatterns, GADTs, LambdaCase, RecordWildCards -- -- Operations over @CRef@s and @MVar@s. This module is NOT considered -- to form part of the public interface of this library. @@ -23,8 +24,7 @@ -- Memory Models/, N. Zhang, M. Kusano, and C. Wang (2015). module Test.DejaFu.Conc.Internal.Memory where -import Control.Monad.Ref (MonadRef, readRef, - writeRef) +import qualified Control.Monad.Conc.Class as C import Data.Map.Strict (Map) import qualified Data.Map.Strict as M import Data.Maybe (maybeToList) @@ -45,60 +45,59 @@ -- -- The @CRefId@ parameter is only used under PSO. Under TSO each -- thread has a single buffer. -newtype WriteBuffer r = WriteBuffer - { buffer :: Map (ThreadId, Maybe CRefId) (Seq (BufferedWrite r)) } +newtype WriteBuffer n = WriteBuffer + { buffer :: Map (ThreadId, Maybe CRefId) (Seq (BufferedWrite n)) } -- | A buffered write is a reference to the variable, and the value to -- write. Universally quantified over the value type so that the only -- thing which can be done with it is to write it to the reference. -data BufferedWrite r where - BufferedWrite :: ThreadId -> CRef r a -> a -> BufferedWrite r +data BufferedWrite n where + BufferedWrite :: ThreadId -> ModelCRef n a -> a -> BufferedWrite n -- | An empty write buffer. -emptyBuffer :: WriteBuffer r +emptyBuffer :: WriteBuffer n emptyBuffer = WriteBuffer M.empty -- | Add a new write to the end of a buffer. -bufferWrite :: MonadRef r n => WriteBuffer r -> (ThreadId, Maybe CRefId) -> CRef r a -> a -> n (WriteBuffer r) -bufferWrite (WriteBuffer wb) k@(tid, _) cref@(CRef _ ref) new = do +bufferWrite :: C.MonadConc n => WriteBuffer n -> (ThreadId, Maybe CRefId) -> ModelCRef n a -> a -> n (WriteBuffer n) +bufferWrite (WriteBuffer wb) k@(tid, _) cref@ModelCRef{..} new = do -- Construct the new write buffer let write = singleton $ BufferedWrite tid cref new let buffer' = M.insertWith (flip (><)) k write wb -- Write the thread-local value to the @CRef@'s update map. - (locals, count, def) <- readRef ref - writeRef ref (M.insert tid new locals, count, def) + (locals, count, def) <- C.readCRef crefRef + C.writeCRef crefRef (M.insert tid new locals, count, def) pure (WriteBuffer buffer') -- | Commit the write at the head of a buffer. -commitWrite :: MonadRef r n => WriteBuffer r -> (ThreadId, Maybe CRefId) -> n (WriteBuffer r) +commitWrite :: C.MonadConc n => WriteBuffer n -> (ThreadId, Maybe CRefId) -> n (WriteBuffer n) commitWrite w@(WriteBuffer wb) k = case maybe EmptyL viewl $ M.lookup k wb of BufferedWrite _ cref a :< rest -> do _ <- writeImmediate cref a pure . WriteBuffer $ M.insert k rest wb - EmptyL -> pure w -- | Read from a @CRef@, returning a newer thread-local non-committed -- write if there is one. -readCRef :: MonadRef r n => CRef r a -> ThreadId -> n a +readCRef :: C.MonadConc n => ModelCRef n a -> ThreadId -> n a readCRef cref tid = do (val, _) <- readCRefPrim cref tid pure val -- | Read from a @CRef@, returning a @Ticket@ representing the current -- view of the thread. -readForTicket :: MonadRef r n => CRef r a -> ThreadId -> n (Ticket a) -readForTicket cref@(CRef crid _) tid = do +readForTicket :: C.MonadConc n => ModelCRef n a -> ThreadId -> n (ModelTicket a) +readForTicket cref@ModelCRef{..} tid = do (val, count) <- readCRefPrim cref tid - pure (Ticket crid count val) + pure (ModelTicket crefId count val) -- | Perform a compare-and-swap on a @CRef@ if the ticket is still -- valid. This is strict in the \"new\" value argument. -casCRef :: MonadRef r n => CRef r a -> ThreadId -> Ticket a -> a -> n (Bool, Ticket a, n ()) -casCRef cref tid (Ticket _ cc _) !new = do - tick'@(Ticket _ cc' _) <- readForTicket cref tid +casCRef :: C.MonadConc n => ModelCRef n a -> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ()) +casCRef cref tid (ModelTicket _ cc _) !new = do + tick'@(ModelTicket _ cc' _) <- readForTicket cref tid if cc == cc' then do @@ -108,34 +107,33 @@ else pure (False, tick', pure ()) -- | Read the local state of a @CRef@. -readCRefPrim :: MonadRef r n => CRef r a -> ThreadId -> n (a, Integer) -readCRefPrim (CRef _ ref) tid = do - (vals, count, def) <- readRef ref - +readCRefPrim :: C.MonadConc n => ModelCRef n a -> ThreadId -> n (a, Integer) +readCRefPrim ModelCRef{..} tid = do + (vals, count, def) <- C.readCRef crefRef pure (M.findWithDefault def tid vals, count) -- | Write and commit to a @CRef@ immediately, clearing the update map -- and incrementing the write count. -writeImmediate :: MonadRef r n => CRef r a -> a -> n (n ()) -writeImmediate (CRef _ ref) a = do - (_, count, _) <- readRef ref - let effect = writeRef ref (M.empty, count + 1, a) +writeImmediate :: C.MonadConc n => ModelCRef n a -> a -> n (n ()) +writeImmediate ModelCRef{..} a = do + (_, count, _) <- C.readCRef crefRef + let effect = C.writeCRef crefRef (M.empty, count + 1, a) effect pure effect -- | Flush all writes in the buffer. -writeBarrier :: MonadRef r n => WriteBuffer r -> n () +writeBarrier :: C.MonadConc n => WriteBuffer n -> n () writeBarrier (WriteBuffer wb) = mapM_ flush $ M.elems wb where flush = mapM_ $ \(BufferedWrite _ cref a) -> writeImmediate cref a -- | Add phantom threads to the thread list to commit pending writes. -addCommitThreads :: WriteBuffer r -> Threads n r -> Threads n r +addCommitThreads :: WriteBuffer n -> Threads n -> Threads n addCommitThreads (WriteBuffer wb) ts = ts <> M.fromList phantoms where phantoms = [ (uncurry commitThreadId k, mkthread c) | (k, b) <- M.toList wb , c <- maybeToList (go $ viewl b) ] - go (BufferedWrite tid (CRef crid _) _ :< _) = Just $ ACommit tid crid + go (BufferedWrite tid ModelCRef{..} _ :< _) = Just $ ACommit tid crefId go EmptyL = Nothing -- | The ID of a commit thread. @@ -145,7 +143,7 @@ go Nothing = t + 1 -- | Remove phantom threads. -delCommitThreads :: Threads n r -> Threads n r +delCommitThreads :: Threads n -> Threads n delCommitThreads = M.filterWithKey $ \k _ -> k >= initialThread -------------------------------------------------------------------------------- @@ -156,76 +154,104 @@ data Emptying = Emptying | NonEmptying -- | Put into a @MVar@, blocking if full. -putIntoMVar :: MonadRef r n => MVar r a -> a -> Action n r - -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ()) +putIntoMVar :: C.MonadConc n + => ModelMVar n a + -> a + -> Action n + -> ThreadId + -> Threads n + -> n (Bool, Threads n, [ThreadId], n ()) putIntoMVar cvar a c = mutMVar Blocking cvar a (const c) -- | Try to put into a @MVar@, not blocking if full. -tryPutIntoMVar :: MonadRef r n => MVar r a -> a -> (Bool -> Action n r) - -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ()) +tryPutIntoMVar :: C.MonadConc n + => ModelMVar n a + -> a + -> (Bool -> Action n) + -> ThreadId + -> Threads n + -> n (Bool, Threads n, [ThreadId], n ()) tryPutIntoMVar = mutMVar NonBlocking -- | Read from a @MVar@, blocking if empty. -readFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r) - -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ()) +readFromMVar :: C.MonadConc n + => ModelMVar n a + -> (a -> Action n) + -> ThreadId + -> Threads n + -> n (Bool, Threads n, [ThreadId], n ()) readFromMVar cvar c = seeMVar NonEmptying Blocking cvar (c . efromJust "readFromMVar") -- | Try to read from a @MVar@, not blocking if empty. -tryReadFromMVar :: MonadRef r n => MVar r a -> (Maybe a -> Action n r) - -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ()) +tryReadFromMVar :: C.MonadConc n + => ModelMVar n a + -> (Maybe a -> Action n) + -> ThreadId + -> Threads n + -> n (Bool, Threads n, [ThreadId], n ()) tryReadFromMVar = seeMVar NonEmptying NonBlocking -- | Take from a @MVar@, blocking if empty. -takeFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r) - -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ()) +takeFromMVar :: C.MonadConc n + => ModelMVar n a + -> (a -> Action n) + -> ThreadId + -> Threads n + -> n (Bool, Threads n, [ThreadId], n ()) takeFromMVar cvar c = seeMVar Emptying Blocking cvar (c . efromJust "takeFromMVar") -- | Try to take from a @MVar@, not blocking if empty. -tryTakeFromMVar :: MonadRef r n => MVar r a -> (Maybe a -> Action n r) - -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ()) +tryTakeFromMVar :: C.MonadConc n + => ModelMVar n a + -> (Maybe a -> Action n) + -> ThreadId + -> Threads n + -> n (Bool, Threads n, [ThreadId], n ()) tryTakeFromMVar = seeMVar Emptying NonBlocking -- | Mutate a @MVar@, in either a blocking or nonblocking way. -mutMVar :: MonadRef r n - => Blocking -> MVar r a -> a -> (Bool -> Action n r) - -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ()) -mutMVar blocking (MVar cvid ref) a c threadid threads = do - val <- readRef ref - - case val of - Just _ -> case blocking of - Blocking -> - let threads' = block (OnMVarEmpty cvid) threadid threads - in pure (False, threads', [], pure ()) - NonBlocking -> - pure (False, goto (c False) threadid threads, [], pure ()) - - Nothing -> do - let effect = writeRef ref $ Just a - let (threads', woken) = wake (OnMVarFull cvid) threads - effect - pure (True, goto (c True) threadid threads', woken, effect) +mutMVar :: C.MonadConc n + => Blocking + -> ModelMVar n a + -> a + -> (Bool -> Action n) + -> ThreadId + -> Threads n + -> n (Bool, Threads n, [ThreadId], n ()) +mutMVar blocking ModelMVar{..} a c threadid threads = C.readCRef mvarRef >>= \case + Just _ -> case blocking of + Blocking -> + let threads' = block (OnMVarEmpty mvarId) threadid threads + in pure (False, threads', [], pure ()) + NonBlocking -> + pure (False, goto (c False) threadid threads, [], pure ()) + Nothing -> do + let effect = C.writeCRef mvarRef $ Just a + let (threads', woken) = wake (OnMVarFull mvarId) threads + effect + pure (True, goto (c True) threadid threads', woken, effect) -- | Read a @MVar@, in either a blocking or nonblocking -- way. -seeMVar :: MonadRef r n - => Emptying -> Blocking -> MVar r a -> (Maybe a -> Action n r) - -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ()) -seeMVar emptying blocking (MVar cvid ref) c threadid threads = do - val <- readRef ref - - case val of - Just _ -> do - let effect = case emptying of - Emptying -> writeRef ref Nothing - NonEmptying -> pure () - let (threads', woken) = wake (OnMVarEmpty cvid) threads - effect - pure (True, goto (c val) threadid threads', woken, effect) - - Nothing -> case blocking of - Blocking -> - let threads' = block (OnMVarFull cvid) threadid threads - in pure (False, threads', [], pure ()) - NonBlocking -> - pure (False, goto (c Nothing) threadid threads, [], pure ()) +seeMVar :: C.MonadConc n + => Emptying + -> Blocking + -> ModelMVar n a + -> (Maybe a -> Action n) + -> ThreadId + -> Threads n + -> n (Bool, Threads n, [ThreadId], n ()) +seeMVar emptying blocking ModelMVar{..} c threadid threads = C.readCRef mvarRef >>= \case + val@(Just _) -> do + let effect = case emptying of + Emptying -> C.writeCRef mvarRef Nothing + NonEmptying -> pure () + let (threads', woken) = wake (OnMVarEmpty mvarId) threads + effect + pure (True, goto (c val) threadid threads', woken, effect) + Nothing -> case blocking of + Blocking -> + let threads' = block (OnMVarFull mvarId) threadid threads + in pure (False, threads', [], pure ()) + NonBlocking -> + pure (False, goto (c Nothing) threadid threads, [], pure ()) 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 @@ -1,6 +1,6 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TypeFamilies #-} -- Must come after TypeFamilies @@ -12,89 +12,89 @@ -- License : MIT -- Maintainer : Michael Walker -- Stability : experimental --- Portability : CPP, ExistentialQuantification, MultiParamTypeClasses, NoMonoLocalBinds, TypeFamilies +-- Portability : CPP, ExistentialQuantification, NoMonoLocalBinds, RecordWildCards, TypeFamilies -- -- 'MonadSTM' testing implementation, internal types and definitions. -- This module is NOT considered to form part of the public interface -- of this library. module Test.DejaFu.Conc.Internal.STM where -import Control.Applicative (Alternative(..)) -import Control.Exception (Exception, SomeException, - fromException, toException) -import Control.Monad (MonadPlus(..)) -import Control.Monad.Catch (MonadCatch(..), MonadThrow(..)) -import Control.Monad.Ref (MonadRef, newRef, readRef, writeRef) -import Data.List (nub) +import Control.Applicative (Alternative(..)) +import Control.Exception (Exception, SomeException, + fromException, toException) +import Control.Monad (MonadPlus(..)) +import Control.Monad.Catch (MonadCatch(..), MonadThrow(..)) +import qualified Control.Monad.Conc.Class as C +import qualified Control.Monad.STM.Class as S +import Data.List (nub) -import qualified Control.Monad.STM.Class as C import Test.DejaFu.Internal import Test.DejaFu.Types #if MIN_VERSION_base(4,9,0) -import qualified Control.Monad.Fail as Fail +import qualified Control.Monad.Fail as Fail #endif -------------------------------------------------------------------------------- --- * The @S@ monad +-- * The @ModelSTM@ monad -- | The underlying monad is based on continuations over primitive -- actions. -- -- This is not @Cont@ because we want to give it a custom @MonadFail@ -- instance. -newtype S n r a = S { runSTM :: (a -> STMAction n r) -> STMAction n r } +newtype ModelSTM n a = ModelSTM { runModelSTM :: (a -> STMAction n) -> STMAction n } -instance Functor (S n r) where - fmap f m = S $ \c -> runSTM m (c . f) +instance Functor (ModelSTM n) where + fmap f m = ModelSTM $ \c -> runModelSTM m (c . f) -instance Applicative (S n r) where - pure x = S $ \c -> c x - f <*> v = S $ \c -> runSTM f (\g -> runSTM v (c . g)) +instance Applicative (ModelSTM n) where + pure x = ModelSTM $ \c -> c x + f <*> v = ModelSTM $ \c -> runModelSTM f (\g -> runModelSTM v (c . g)) -instance Monad (S n r) where +instance Monad (ModelSTM n) where return = pure - m >>= k = S $ \c -> runSTM m (\x -> runSTM (k x) c) + m >>= k = ModelSTM $ \c -> runModelSTM m (\x -> runModelSTM (k x) c) #if MIN_VERSION_base(4,9,0) fail = Fail.fail -instance Fail.MonadFail (S n r) where +instance Fail.MonadFail (ModelSTM n) where #endif - fail e = S $ \_ -> SThrow (MonadFailException e) + fail e = ModelSTM $ \_ -> SThrow (MonadFailException e) -instance MonadThrow (S n r) where - throwM e = S $ \_ -> SThrow e +instance MonadThrow (ModelSTM n) where + throwM e = ModelSTM $ \_ -> SThrow e -instance MonadCatch (S n r) where - catch stm handler = S $ SCatch handler stm +instance MonadCatch (ModelSTM n) where + catch stm handler = ModelSTM $ SCatch handler stm -instance Alternative (S n r) where - a <|> b = S $ SOrElse a b - empty = S $ const SRetry +instance Alternative (ModelSTM n) where + a <|> b = ModelSTM $ SOrElse a b + empty = ModelSTM $ const SRetry -instance MonadPlus (S n r) +instance MonadPlus (ModelSTM n) -instance C.MonadSTM (S n r) where - type TVar (S n r) = TVar r +instance S.MonadSTM (ModelSTM n) where + type TVar (ModelSTM n) = ModelTVar n - newTVarN n = S . SNew n + newTVarN n = ModelSTM . SNew n - readTVar = S . SRead + readTVar = ModelSTM . SRead - writeTVar tvar a = S $ \c -> SWrite tvar a (c ()) + writeTVar tvar a = ModelSTM $ \c -> SWrite tvar a (c ()) -------------------------------------------------------------------------------- -- * Primitive actions -- | STM transactions are represented as a sequence of primitive -- actions. -data STMAction n r - = forall a e. Exception e => SCatch (e -> S n r a) (S n r a) (a -> STMAction n r) - | forall a. SRead (TVar r a) (a -> STMAction n r) - | forall a. SWrite (TVar r a) a (STMAction n r) - | forall a. SOrElse (S n r a) (S n r a) (a -> STMAction n r) - | forall a. SNew String a (TVar r a -> STMAction n r) +data STMAction n + = forall a e. Exception e => SCatch (e -> ModelSTM n a) (ModelSTM n a) (a -> STMAction n) + | forall a. SRead (ModelTVar n a) (a -> STMAction n) + | forall a. SWrite (ModelTVar n a) a (STMAction n) + | forall a. SOrElse (ModelSTM n a) (ModelSTM n a) (a -> STMAction n) + | forall a. SNew String a (ModelTVar n a -> STMAction n) | forall e. Exception e => SThrow e | SRetry | SStop (n ()) @@ -102,10 +102,12 @@ -------------------------------------------------------------------------------- -- * @TVar@s --- | A 'TVar' is a tuple of a unique ID and the value contained. The --- ID is so that blocked transactions can be re-run when a 'TVar' they --- depend on has changed. -newtype TVar r a = TVar (TVarId, r a) +-- | A @TVar@ is modelled as a unique ID and a reference holding a +-- value. +data ModelTVar n a = ModelTVar + { tvarId :: TVarId + , tvarRef :: C.CRef n a + } -------------------------------------------------------------------------------- -- * Output @@ -130,8 +132,8 @@ -- | Run a transaction, returning the result and new initial 'TVarId'. -- If the transaction failed, any effects are undone. -runTransaction :: MonadRef r n - => S n r a +runTransaction :: C.MonadConc n + => ModelSTM n a -> IdSource -> n (Result a, IdSource, [TAction]) runTransaction ma tvid = do @@ -142,14 +144,14 @@ -- -- If the transaction fails, its effects will automatically be undone, -- so the undo action returned will be @pure ()@. -doTransaction :: MonadRef r n - => S n r a +doTransaction :: C.MonadConc n + => ModelSTM n a -> IdSource -> n (Result a, n (), IdSource, [TAction]) doTransaction ma idsource = do - (c, ref) <- runRefCont SStop (Just . Right) (runSTM ma) + (c, ref) <- runRefCont SStop (Just . Right) (runModelSTM ma) (idsource', undo, readen, written, trace) <- go ref c (pure ()) idsource [] [] [] - res <- readRef ref + res <- C.readCRef ref case res of Just (Right val) -> pure (Success (nub readen) (nub written) val, undo, idsource', reverse trace) @@ -170,18 +172,18 @@ case tact of TStop -> pure (newIDSource, newUndo, newReaden, newWritten, TStop:newSofar) TRetry -> do - writeRef ref Nothing + C.writeCRef ref Nothing pure (newIDSource, newUndo, newReaden, newWritten, TRetry:newSofar) TThrow -> do - writeRef ref (Just . Left $ case act of SThrow e -> toException e; _ -> undefined) + C.writeCRef ref (Just . Left $ case act of SThrow e -> toException e; _ -> undefined) pure (newIDSource, newUndo, newReaden, newWritten, TThrow:newSofar) _ -> go ref newAct newUndo newIDSource newReaden newWritten newSofar -- | Run a transaction for one step. -stepTrans :: MonadRef r n - => STMAction n r +stepTrans :: C.MonadConc n + => STMAction n -> IdSource - -> n (STMAction n r, n (), IdSource, [TVarId], [TVarId], TAction) + -> n (STMAction n, n (), IdSource, [TVarId], [TVarId], TAction) stepTrans act idsource = case act of SCatch h stm c -> stepCatch h stm c SRead ref c -> stepRead ref c @@ -202,19 +204,19 @@ Just exc' -> transaction (TCatch trace . Just) (h exc') c Nothing -> pure (SThrow exc, nothing, idsource, [], [], TCatch trace Nothing)) - stepRead (TVar (tvid, ref)) c = do - val <- readRef ref - pure (c val, nothing, idsource, [tvid], [], TRead tvid) + stepRead ModelTVar{..} c = do + val <- C.readCRef tvarRef + pure (c val, nothing, idsource, [tvarId], [], TRead tvarId) - stepWrite (TVar (tvid, ref)) a c = do - old <- readRef ref - writeRef ref a - pure (c, writeRef ref old, idsource, [], [tvid], TWrite tvid) + stepWrite ModelTVar{..} a c = do + old <- C.readCRef tvarRef + C.writeCRef tvarRef a + pure (c, C.writeCRef tvarRef old, idsource, [], [tvarId], TWrite tvarId) stepNew n a c = do let (idsource', tvid) = nextTVId n idsource - ref <- newRef a - let tvar = TVar (tvid, ref) + ref <- C.newCRef a + let tvar = ModelTVar tvid ref pure (c tvar, nothing, idsource', [], [tvid], TNew tvid) stepOrElse a b c = cases TOrElse a c 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 @@ -13,10 +13,10 @@ -- form part of the public interface of this library. module Test.DejaFu.Conc.Internal.Threading where -import qualified Control.Concurrent.Classy as C import Control.Exception (Exception, MaskingState(..), SomeException, fromException) import Control.Monad (forever) +import qualified Control.Monad.Conc.Class as C import Data.List (intersect) import Data.Map.Strict (Map) import qualified Data.Map.Strict as M @@ -30,34 +30,34 @@ -- * Threads -- | Threads are stored in a map index by 'ThreadId'. -type Threads n r = Map ThreadId (Thread n r) +type Threads n = Map ThreadId (Thread n) -- | All the state of a thread. -data Thread n r = Thread - { _continuation :: Action n r +data Thread n = Thread + { _continuation :: Action n -- ^ The next action to execute. , _blocking :: Maybe BlockedOn -- ^ The state of any blocks. - , _handlers :: [Handler n r] + , _handlers :: [Handler n] -- ^ Stack of exception handlers , _masking :: MaskingState -- ^ The exception masking state. - , _bound :: Maybe (BoundThread n r) + , _bound :: Maybe (BoundThread n) -- ^ State for the associated bound thread, if it exists. } -- | The state of a bound thread. -data BoundThread n r = BoundThread - { _runboundIO :: C.MVar n (n (Action n r)) +data BoundThread n = BoundThread + { _runboundIO :: C.MVar n (n (Action n)) -- ^ Run an @IO@ action in the bound thread by writing to this. - , _getboundIO :: C.MVar n (Action n r) + , _getboundIO :: C.MVar n (Action n) -- ^ Get the result of the above by reading from this. , _boundTId :: C.ThreadId n -- ^ Thread ID } -- | Construct a thread with just one action -mkthread :: Action n r -> Thread n r +mkthread :: Action n -> Thread n mkthread c = Thread c Nothing [] Unmasked Nothing -------------------------------------------------------------------------------- @@ -68,7 +68,7 @@ data BlockedOn = OnMVarFull MVarId | OnMVarEmpty MVarId | OnTVar [TVarId] | OnMask ThreadId deriving Eq -- | Determine if a thread is blocked in a certain way. -(~=) :: Thread n r -> BlockedOn -> Bool +(~=) :: Thread n -> BlockedOn -> Bool thread ~= theblock = case (_blocking thread, theblock) of (Just (OnMVarFull _), OnMVarFull _) -> True (Just (OnMVarEmpty _), OnMVarEmpty _) -> True @@ -80,11 +80,11 @@ -- * Exceptions -- | An exception handler. -data Handler n r = forall e. Exception e => Handler (e -> MaskingState -> Action n r) +data Handler n = forall e. Exception e => Handler (e -> MaskingState -> Action n) -- | Propagate an exception upwards, finding the closest handler -- which can deal with it. -propagate :: SomeException -> ThreadId -> Threads n r -> Maybe (Threads n r) +propagate :: SomeException -> ThreadId -> Threads n -> Maybe (Threads n) propagate e tid threads = raise <$> propagate' handlers where handlers = _handlers (elookup "propagate" tid threads) @@ -94,23 +94,25 @@ propagate' (Handler h:hs) = maybe (propagate' hs) (\act -> Just (act, hs)) $ h <$> fromException e -- | Check if a thread can be interrupted by an exception. -interruptible :: Thread n r -> Bool -interruptible thread = _masking thread == Unmasked || (_masking thread == MaskedInterruptible && isJust (_blocking thread)) +interruptible :: Thread n -> Bool +interruptible thread = + _masking thread == Unmasked || + (_masking thread == MaskedInterruptible && isJust (_blocking thread)) -- | Register a new exception handler. -catching :: Exception e => (e -> Action n r) -> ThreadId -> Threads n r -> Threads n r +catching :: Exception e => (e -> Action n) -> ThreadId -> Threads n -> Threads n catching h = eadjust "catching" $ \thread -> let ms0 = _masking thread h' = Handler $ \e ms -> (if ms /= ms0 then AResetMask False False ms0 else id) (h e) in thread { _handlers = h' : _handlers thread } -- | Remove the most recent exception handler. -uncatching :: ThreadId -> Threads n r -> Threads n r +uncatching :: ThreadId -> Threads n -> Threads n uncatching = eadjust "uncatching" $ \thread -> thread { _handlers = etail "uncatching" (_handlers thread) } -- | Raise an exception in a thread. -except :: (MaskingState -> Action n r) -> [Handler n r] -> ThreadId -> Threads n r -> Threads n r +except :: (MaskingState -> Action n) -> [Handler n] -> ThreadId -> Threads n -> Threads n except actf hs = eadjust "except" $ \thread -> thread { _continuation = actf (_masking thread) , _handlers = hs @@ -118,38 +120,38 @@ } -- | Set the masking state of a thread. -mask :: MaskingState -> ThreadId -> Threads n r -> Threads n r +mask :: MaskingState -> ThreadId -> Threads n -> Threads n mask ms = eadjust "mask" $ \thread -> thread { _masking = ms } -------------------------------------------------------------------------------- -- * Manipulating threads -- | Replace the @Action@ of a thread. -goto :: Action n r -> ThreadId -> Threads n r -> Threads n r +goto :: Action n -> ThreadId -> Threads n -> Threads n goto a = eadjust "goto" $ \thread -> thread { _continuation = a } -- | Start a thread with the given ID, inheriting the masking state -- from the parent thread. This ID must not already be in use! -launch :: ThreadId -> ThreadId -> ((forall b. M n r b -> M n r b) -> Action n r) -> Threads n r -> Threads n r +launch :: ThreadId -> ThreadId -> ((forall b. ModelConc n b -> ModelConc n b) -> Action n) -> Threads n -> Threads n launch parent tid a threads = launch' ms tid a threads where ms = _masking (elookup "launch" parent threads) -- | Start a thread with the given ID and masking state. This must not already be in use! -launch' :: MaskingState -> ThreadId -> ((forall b. M n r b -> M n r b) -> Action n r) -> Threads n r -> Threads n r +launch' :: MaskingState -> ThreadId -> ((forall b. ModelConc n b -> ModelConc n b) -> Action n) -> Threads n -> Threads n launch' ms tid a = einsert "launch'" tid thread where thread = Thread (a umask) Nothing [] ms Nothing umask mb = resetMask True Unmasked >> mb >>= \b -> resetMask False ms >> pure b - resetMask typ m = cont $ \k -> AResetMask typ True m $ k () + resetMask typ m = ModelConc $ \k -> AResetMask typ True m $ k () -- | Block a thread. -block :: BlockedOn -> ThreadId -> Threads n r -> Threads n r +block :: BlockedOn -> ThreadId -> Threads n -> Threads n block blockedOn = eadjust "block" $ \thread -> thread { _blocking = Just blockedOn } -- | Unblock all threads waiting on the appropriate block. For 'TVar' -- blocks, this will wake all threads waiting on at least one of the -- given 'TVar's. -wake :: BlockedOn -> Threads n r -> (Threads n r, [ThreadId]) +wake :: BlockedOn -> Threads n -> (Threads n, [ThreadId]) wake blockedOn threads = (unblock <$> threads, M.keys $ M.filter isBlocked threads) where unblock thread | isBlocked thread = thread { _blocking = Nothing } @@ -163,7 +165,7 @@ -- ** Bound threads -- | Turn a thread into a bound thread. -makeBound :: C.MonadConc n => ThreadId -> Threads n r -> n (Threads n r) +makeBound :: C.MonadConc n => ThreadId -> Threads n -> n (Threads n) makeBound tid threads = do runboundIO <- C.newEmptyMVar getboundIO <- C.newEmptyMVar @@ -178,7 +180,7 @@ -- | Kill a thread and remove it from the thread map. -- -- If the thread is bound, the worker thread is cleaned up. -kill :: C.MonadConc n => ThreadId -> Threads n r -> n (Threads n r) +kill :: C.MonadConc n => ThreadId -> Threads n -> n (Threads n) kill tid threads = do let thread = elookup "kill" tid threads maybe (pure ()) (C.killThread . _boundTId) (_bound thread) @@ -187,7 +189,7 @@ -- | Run an action. -- -- If the thread is bound, the action is run in the worker thread. -runLiftedAct :: C.MonadConc n => ThreadId -> Threads n r -> n (Action n r) -> n (Action n r) +runLiftedAct :: C.MonadConc n => ThreadId -> Threads n -> n (Action n) -> n (Action n) runLiftedAct tid threads ma = case _bound =<< M.lookup tid threads of Just bt -> do C.putMVar (_runboundIO bt) ma diff --git a/Test/DejaFu/Internal.hs b/Test/DejaFu/Internal.hs --- a/Test/DejaFu/Internal.hs +++ b/Test/DejaFu/Internal.hs @@ -15,15 +15,15 @@ -- library. module Test.DejaFu.Internal where -import Control.DeepSeq (NFData) -import Control.Monad.Ref (MonadRef(..)) -import Data.List.NonEmpty (NonEmpty(..)) -import qualified Data.Map.Strict as M -import Data.Maybe (fromMaybe) -import Data.Set (Set) -import qualified Data.Set as S -import GHC.Generics (Generic) -import System.Random (RandomGen) +import Control.DeepSeq (NFData) +import qualified Control.Monad.Conc.Class as C +import Data.List.NonEmpty (NonEmpty(..)) +import qualified Data.Map.Strict as M +import Data.Maybe (fromMaybe) +import Data.Set (Set) +import qualified Data.Set as S +import GHC.Generics (Generic) +import System.Random (RandomGen) import Test.DejaFu.Types @@ -155,50 +155,49 @@ tvarsOf' _ = [] -- | Convert a 'ThreadAction' into a 'Lookahead': \"rewind\" what has --- happened. 'Killed' has no 'Lookahead' counterpart. -rewind :: ThreadAction -> Maybe Lookahead -rewind (Fork _) = Just WillFork -rewind (ForkOS _) = Just WillForkOS -rewind (IsCurrentThreadBound _) = Just WillIsCurrentThreadBound -rewind MyThreadId = Just WillMyThreadId -rewind (GetNumCapabilities _) = Just WillGetNumCapabilities -rewind (SetNumCapabilities i) = Just (WillSetNumCapabilities i) -rewind Yield = Just WillYield -rewind (ThreadDelay n) = Just (WillThreadDelay n) -rewind (NewMVar _) = Just WillNewMVar -rewind (PutMVar c _) = Just (WillPutMVar c) -rewind (BlockedPutMVar c) = Just (WillPutMVar c) -rewind (TryPutMVar c _ _) = Just (WillTryPutMVar c) -rewind (ReadMVar c) = Just (WillReadMVar c) -rewind (BlockedReadMVar c) = Just (WillReadMVar c) -rewind (TryReadMVar c _) = Just (WillTryReadMVar c) -rewind (TakeMVar c _) = Just (WillTakeMVar c) -rewind (BlockedTakeMVar c) = Just (WillTakeMVar c) -rewind (TryTakeMVar c _ _) = Just (WillTryTakeMVar c) -rewind (NewCRef _) = Just WillNewCRef -rewind (ReadCRef c) = Just (WillReadCRef c) -rewind (ReadCRefCas c) = Just (WillReadCRefCas c) -rewind (ModCRef c) = Just (WillModCRef c) -rewind (ModCRefCas c) = Just (WillModCRefCas c) -rewind (WriteCRef c) = Just (WillWriteCRef c) -rewind (CasCRef c _) = Just (WillCasCRef c) -rewind (CommitCRef t c) = Just (WillCommitCRef t c) -rewind (STM _ _) = Just WillSTM -rewind (BlockedSTM _) = Just WillSTM -rewind Catching = Just WillCatching -rewind PopCatching = Just WillPopCatching -rewind Throw = Just WillThrow -rewind (ThrowTo t) = Just (WillThrowTo t) -rewind (BlockedThrowTo t) = Just (WillThrowTo t) -rewind Killed = Nothing -rewind (SetMasking b m) = Just (WillSetMasking b m) -rewind (ResetMasking b m) = Just (WillResetMasking b m) -rewind LiftIO = Just WillLiftIO -rewind Return = Just WillReturn -rewind Stop = Just WillStop -rewind Subconcurrency = Just WillSubconcurrency -rewind StopSubconcurrency = Just WillStopSubconcurrency -rewind (DontCheck _) = Just WillDontCheck +-- happened. +rewind :: ThreadAction -> Lookahead +rewind (Fork _) = WillFork +rewind (ForkOS _) = WillForkOS +rewind (IsCurrentThreadBound _) = WillIsCurrentThreadBound +rewind MyThreadId = WillMyThreadId +rewind (GetNumCapabilities _) = WillGetNumCapabilities +rewind (SetNumCapabilities i) = WillSetNumCapabilities i +rewind Yield = WillYield +rewind (ThreadDelay n) = WillThreadDelay n +rewind (NewMVar _) = WillNewMVar +rewind (PutMVar c _) = WillPutMVar c +rewind (BlockedPutMVar c) = WillPutMVar c +rewind (TryPutMVar c _ _) = WillTryPutMVar c +rewind (ReadMVar c) = WillReadMVar c +rewind (BlockedReadMVar c) = WillReadMVar c +rewind (TryReadMVar c _) = WillTryReadMVar c +rewind (TakeMVar c _) = WillTakeMVar c +rewind (BlockedTakeMVar c) = WillTakeMVar c +rewind (TryTakeMVar c _ _) = WillTryTakeMVar c +rewind (NewCRef _) = WillNewCRef +rewind (ReadCRef c) = WillReadCRef c +rewind (ReadCRefCas c) = WillReadCRefCas c +rewind (ModCRef c) = WillModCRef c +rewind (ModCRefCas c) = WillModCRefCas c +rewind (WriteCRef c) = WillWriteCRef c +rewind (CasCRef c _) = WillCasCRef c +rewind (CommitCRef t c) = WillCommitCRef t c +rewind (STM _ _) = WillSTM +rewind (BlockedSTM _) = WillSTM +rewind Catching = WillCatching +rewind PopCatching = WillPopCatching +rewind Throw = WillThrow +rewind (ThrowTo t) = WillThrowTo t +rewind (BlockedThrowTo t) = WillThrowTo t +rewind (SetMasking b m) = WillSetMasking b m +rewind (ResetMasking b m) = WillResetMasking b m +rewind LiftIO = WillLiftIO +rewind Return = WillReturn +rewind Stop = WillStop +rewind Subconcurrency = WillSubconcurrency +rewind StopSubconcurrency = WillStopSubconcurrency +rewind (DontCheck _) = WillDontCheck -- | Check if an operation could enable another thread. willRelease :: Lookahead -> Bool @@ -303,7 +302,7 @@ -- This is used in the SCT code to help determine interesting -- alternative scheduling decisions. simplifyAction :: ThreadAction -> ActionType -simplifyAction = maybe UnsynchronisedOther simplifyLookahead . rewind +simplifyAction = simplifyLookahead . rewind -- | Variant of 'simplifyAction' that takes a 'Lookahead'. simplifyLookahead :: Lookahead -> ActionType @@ -383,8 +382,12 @@ -- | Run with a continuation that writes its value into a reference, -- returning the computation and the reference. Using the reference -- is non-blocking, it is up to you to ensure you wait sufficiently. -runRefCont :: MonadRef r n => (n () -> x) -> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, r (Maybe b)) +runRefCont :: C.MonadConc n + => (n () -> x) + -> (a -> Maybe b) + -> ((a -> x) -> x) + -> n (x, C.CRef n (Maybe b)) runRefCont act f k = do - ref <- newRef Nothing - let c = k (act . writeRef ref . f) + ref <- C.newCRef Nothing + let c = k (act . C.writeCRef ref . f) pure (c, ref) diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -37,7 +37,6 @@ import Control.Applicative ((<|>)) import Control.DeepSeq (NFData(..), force) import Control.Monad.Conc.Class (MonadConc) -import Control.Monad.Ref (MonadRef) import Data.List (foldl') import qualified Data.Map.Strict as M import Data.Maybe (fromMaybe) @@ -64,12 +63,12 @@ -- found, is unspecified and may change between releases. -- -- @since 1.0.0.0 -runSCT :: (MonadConc n, MonadRef r n) +runSCT :: MonadConc n => Way -- ^ How to run the concurrent program. -> MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. - -> ConcT r n a + -> ConcT n a -- ^ The computation to run many times. -> n [(Either Failure a, Trace)] runSCT way = runSCTWithSettings . fromWayAndMemType way @@ -77,12 +76,12 @@ -- | Return the set of results of a concurrent program. -- -- @since 1.0.0.0 -resultsSet :: (MonadConc n, MonadRef r n, Ord a) +resultsSet :: (MonadConc n, Ord a) => Way -- ^ How to run the concurrent program. -> MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. - -> ConcT r n a + -> ConcT n a -- ^ The computation to run many times. -> n (Set (Either Failure a)) resultsSet way = resultsSetWithSettings . fromWayAndMemType way @@ -93,14 +92,14 @@ -- found, is unspecified and may change between releases. -- -- @since 1.0.0.0 -runSCTDiscard :: (MonadConc n, MonadRef r n) +runSCTDiscard :: MonadConc n => (Either Failure a -> Maybe Discard) -- ^ Selectively discard results. -> Way -- ^ How to run the concurrent program. -> MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. - -> ConcT r n a + -> ConcT n a -- ^ The computation to run many times. -> n [(Either Failure a, Trace)] runSCTDiscard discard way = runSCTWithSettings . set ldiscard (Just discard) . fromWayAndMemType way @@ -109,14 +108,14 @@ -- | A variant of 'resultsSet' which can selectively discard results. -- -- @since 1.0.0.0 -resultsSetDiscard :: (MonadConc n, MonadRef r n, Ord a) +resultsSetDiscard :: (MonadConc n, Ord a) => (Either Failure a -> Maybe Discard) -- ^ Selectively discard results. Traces are always discarded. -> Way -- ^ How to run the concurrent program. -> MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. - -> ConcT r n a + -> ConcT n a -- ^ The computation to run many times. -> n (Set (Either Failure a)) resultsSetDiscard discard way memtype conc = @@ -133,8 +132,8 @@ -- found, is unspecified and may change between releases. -- -- @since 1.0.0.0 -runSCT' :: (MonadConc n, MonadRef r n, NFData a) - => Way -> MemType -> ConcT r n a -> n [(Either Failure a, Trace)] +runSCT' :: (MonadConc n, NFData a) + => Way -> MemType -> ConcT n a -> n [(Either Failure a, Trace)] runSCT' way = runSCTWithSettings' . fromWayAndMemType way -- | A strict variant of 'resultsSet'. @@ -143,8 +142,8 @@ -- may be more efficient in some situations. -- -- @since 1.0.0.0 -resultsSet' :: (MonadConc n, MonadRef r n, Ord a, NFData a) - => Way -> MemType -> ConcT r n a -> n (Set (Either Failure a)) +resultsSet' :: (MonadConc n, Ord a, NFData a) + => Way -> MemType -> ConcT n a -> n (Set (Either Failure a)) resultsSet' way = resultsSetWithSettings' . fromWayAndMemType way -- | A strict variant of 'runSCTDiscard'. @@ -156,8 +155,8 @@ -- found, is unspecified and may change between releases. -- -- @since 1.0.0.0 -runSCTDiscard' :: (MonadConc n, MonadRef r n, NFData a) - => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT r n a -> n [(Either Failure a, Trace)] +runSCTDiscard' :: (MonadConc n, NFData a) + => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT n a -> n [(Either Failure a, Trace)] runSCTDiscard' discard way memtype conc = do res <- runSCTDiscard discard way memtype conc rnf res `seq` pure res @@ -169,8 +168,8 @@ -- may be more efficient in some situations. -- -- @since 1.0.0.0 -resultsSetDiscard' :: (MonadConc n, MonadRef r n, Ord a, NFData a) - => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT r n a -> n (Set (Either Failure a)) +resultsSetDiscard' :: (MonadConc n, Ord a, NFData a) + => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT n a -> n (Set (Either Failure a)) resultsSetDiscard' discard way memtype conc = do res <- resultsSetDiscard discard way memtype conc rnf res `seq` pure res @@ -185,10 +184,10 @@ -- found, is unspecified and may change between releases. -- -- @since 1.2.0.0 -runSCTWithSettings :: (MonadConc n, MonadRef r n) +runSCTWithSettings :: MonadConc n => Settings n a -- ^ The SCT settings. - -> ConcT r n a + -> ConcT n a -- ^ The computation to run many times. -> n [(Either Failure a, Trace)] runSCTWithSettings settings conc = case _way settings of @@ -240,10 +239,10 @@ -- | A variant of 'resultsSet' which takes a 'Settings' record. -- -- @since 1.2.0.0 -resultsSetWithSettings :: (MonadConc n, MonadRef r n, Ord a) +resultsSetWithSettings :: (MonadConc n, Ord a) => Settings n a -- ^ The SCT settings. - -> ConcT r n a + -> ConcT n a -- ^ The computation to run many times. -> n (Set (Either Failure a)) resultsSetWithSettings settings conc = @@ -259,9 +258,9 @@ -- found, is unspecified and may change between releases. -- -- @since 1.2.0.0 -runSCTWithSettings' :: (MonadConc n, MonadRef r n, NFData a) +runSCTWithSettings' :: (MonadConc n, NFData a) => Settings n a - -> ConcT r n a + -> ConcT n a -> n [(Either Failure a, Trace)] runSCTWithSettings' settings conc = do res <- runSCTWithSettings settings conc @@ -273,9 +272,9 @@ -- may be more efficient in some situations. -- -- @since 1.2.0.0 -resultsSetWithSettings' :: (MonadConc n, MonadRef r n, Ord a, NFData a) +resultsSetWithSettings' :: (MonadConc n, Ord a, NFData a) => Settings n a - -> ConcT r n a + -> ConcT n a -> n (Set (Either Failure a)) resultsSetWithSettings' settings conc = do res <- resultsSetWithSettings settings conc @@ -384,12 +383,12 @@ -- found, is unspecified and may change between releases. -- -- @since 1.0.0.0 -sctBound :: (MonadConc n, MonadRef r n) +sctBound :: MonadConc n => MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. -> Bounds -- ^ The combined bounds. - -> ConcT r n a + -> ConcT n a -- ^ The computation to run many times -> n [(Either Failure a, Trace)] sctBound = sctBoundDiscard (const Nothing) @@ -401,14 +400,14 @@ -- found, is unspecified and may change between releases. -- -- @since 1.0.0.0 -sctBoundDiscard :: (MonadConc n, MonadRef r n) +sctBoundDiscard :: MonadConc n => (Either Failure a -> Maybe Discard) -- ^ Selectively discard results. -> MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. -> Bounds -- ^ The combined bounds. - -> ConcT r n a + -> ConcT n a -- ^ The computation to run many times -> n [(Either Failure a, Trace)] sctBoundDiscard discard memtype cb = runSCTWithSettings $ @@ -423,14 +422,14 @@ -- This is not guaranteed to find all distinct results. -- -- @since 1.0.0.0 -sctUniformRandom :: (MonadConc n, MonadRef r n, RandomGen g) +sctUniformRandom :: (MonadConc n, RandomGen g) => MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. -> g -- ^ The random number generator. -> Int -- ^ The number of executions to perform. - -> ConcT r n a + -> ConcT n a -- ^ The computation to run many times. -> n [(Either Failure a, Trace)] sctUniformRandom = sctUniformRandomDiscard (const Nothing) @@ -442,7 +441,7 @@ -- This is not guaranteed to find all distinct results. -- -- @since 1.0.0.0 -sctUniformRandomDiscard :: (MonadConc n, MonadRef r n, RandomGen g) +sctUniformRandomDiscard :: (MonadConc n, RandomGen g) => (Either Failure a -> Maybe Discard) -- ^ Selectively discard results. -> MemType @@ -451,7 +450,7 @@ -- ^ The random number generator. -> Int -- ^ The number of executions to perform. - -> ConcT r n a + -> ConcT n a -- ^ The computation to run many times. -> n [(Either Failure a, Trace)] sctUniformRandomDiscard discard memtype g lim = runSCTWithSettings $ @@ -466,7 +465,7 @@ -- This is not guaranteed to find all distinct results. -- -- @since 1.0.0.0 -sctWeightedRandom :: (MonadConc n, MonadRef r n, RandomGen g) +sctWeightedRandom :: (MonadConc n, RandomGen g) => MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. -> g @@ -475,7 +474,7 @@ -- ^ The number of executions to perform. -> Int -- ^ The number of executions to use the same set of weights for. - -> ConcT r n a + -> ConcT n a -- ^ The computation to run many times. -> n [(Either Failure a, Trace)] sctWeightedRandom = sctWeightedRandomDiscard (const Nothing) @@ -487,7 +486,7 @@ -- This is not guaranteed to find all distinct results. -- -- @since 1.0.0.0 -sctWeightedRandomDiscard :: (MonadConc n, MonadRef r n, RandomGen g) +sctWeightedRandomDiscard :: (MonadConc n, RandomGen g) => (Either Failure a -> Maybe Discard) -- ^ Selectively discard results. -> MemType @@ -498,7 +497,7 @@ -- ^ The number of executions to perform. -> Int -- ^ The number of executions to use the same set of weights for. - -> ConcT r n a + -> ConcT n a -- ^ The computation to run many times. -> n [(Either Failure a, Trace)] sctWeightedRandomDiscard discard memtype g lim use = runSCTWithSettings $ 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 @@ -16,7 +16,6 @@ module Test.DejaFu.SCT.Internal where import Control.Monad.Conc.Class (MonadConc) -import Control.Monad.Ref (MonadRef) import Data.Coerce (Coercible, coerce) import qualified Data.IntMap.Strict as I import Data.List (find, mapAccumL) @@ -35,7 +34,7 @@ -- * Exploration -- | General-purpose SCT function. -sct :: (MonadConc n, MonadRef r n) +sct :: MonadConc n => Settings n a -- ^ The SCT settings ('Way' is ignored) -> ([ThreadId] -> s) @@ -44,7 +43,7 @@ -- ^ State predicate -> ((Scheduler g -> g -> n (Either Failure a, g, Trace)) -> s -> t -> n (s, Maybe (Either Failure a, Trace))) -- ^ Run the computation and update the state - -> ConcT r n a + -> ConcT n a -> n [(Either Failure a, Trace)] sct settings s0 sfun srun conc | canDCSnapshot conc = runForDCSnapshot conc >>= \case @@ -80,7 +79,7 @@ debugPrint = fromMaybe (const (pure ())) (_debugPrint settings) -- | Like 'sct' but given a function to run the computation. -sct' :: (MonadConc n, MonadRef r n) +sct' :: MonadConc n => Settings n a -- ^ The SCT settings ('Way' is ignored) -> s @@ -147,7 +146,7 @@ -- Unlike shrinking in randomised property-testing tools like -- QuickCheck or Hedgehog, we only run the test case /once/, at the -- end, rather than after every simplification step. -simplifyExecution :: (MonadConc n, MonadRef r n) +simplifyExecution :: MonadConc n => Settings n a -- ^ The SCT settings ('Way' is ignored) -> (forall x. Scheduler x -> x -> n (Either Failure a, x, Trace)) @@ -185,7 +184,7 @@ p = either show debugShow -- | Replay an execution. -replay :: (MonadConc n, MonadRef r n) +replay :: MonadConc n => (forall x. Scheduler x -> x -> n (Either Failure a, x, Trace)) -- ^ Run the computation -> [(ThreadId, ThreadAction)] diff --git a/Test/DejaFu/SCT/Internal/DPOR.hs b/Test/DejaFu/SCT/Internal/DPOR.hs --- a/Test/DejaFu/SCT/Internal/DPOR.hs +++ b/Test/DejaFu/SCT/Internal/DPOR.hs @@ -578,6 +578,8 @@ -- actually blocked. 'dependent'' has to assume that all -- potentially-blocking operations can block, and so is more -- pessimistic in this case. + (ThrowTo t, ThrowTo u) + | t == t2 && u == t1 -> canInterrupt ds t1 a1 || canInterrupt ds t2 a2 (ThrowTo t, _) | t == t2 -> canInterrupt ds t2 a2 && a2 /= Stop (_, ThrowTo t) | t == t1 -> canInterrupt ds t1 a1 && a1 /= Stop @@ -589,9 +591,8 @@ (BlockedSTM _, STM _ _) -> checkSTM (BlockedSTM _, BlockedSTM _) -> checkSTM - _ -> case (,) <$> rewind a1 <*> rewind a2 of - Just (l1, l2) -> dependent' ds t1 a1 t2 l2 && dependent' ds t2 a2 t1 l1 - _ -> dependentActions ds (simplifyAction a1) (simplifyAction a2) + _ -> dependent' ds t1 a1 t2 (rewind a2) + && dependent' ds t2 a2 t1 (rewind a1) where -- STM actions A and B are dependent if A wrote to anything B @@ -612,6 +613,8 @@ -- thread and if the actions can be interrupted. We can also -- slightly improve on that by not considering interrupting the -- normal termination of a thread: it doesn't make a difference. + (ThrowTo t, WillThrowTo u) + | t == t2 && u == t1 -> canInterrupt ds t1 a1 || canInterruptL ds t2 l2 (ThrowTo t, _) | t == t2 -> canInterruptL ds t2 l2 && l2 /= WillStop (_, WillThrowTo t) | t == t1 -> canInterrupt ds t1 a1 && a1 /= Stop diff --git a/Test/DejaFu/Types.hs b/Test/DejaFu/Types.hs --- a/Test/DejaFu/Types.hs +++ b/Test/DejaFu/Types.hs @@ -104,7 +104,7 @@ -- | All the actions that a thread can perform. -- --- @since 1.1.0.0 +-- @since 1.4.0.0 data ThreadAction = Fork ThreadId -- ^ Start a new thread. @@ -175,8 +175,6 @@ -- ^ Throw an exception to a thread. | BlockedThrowTo ThreadId -- ^ Get blocked on a 'throwTo'. - | Killed - -- ^ Killed by an uncaught exception. | SetMasking Bool MaskingState -- ^ Set the masking state. If 'True', this is being used to set the -- masking state to the original state in the argument passed to a @@ -238,7 +236,6 @@ rnf Throw = () rnf (ThrowTo t) = rnf t rnf (BlockedThrowTo t) = rnf t - rnf Killed = () rnf (SetMasking b m) = rnf (b, show m) rnf (ResetMasking b m) = rnf (b, show m) rnf LiftIO = () 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: 1.3.2.0 +version: 1.4.0.0 synopsis: A library for unit-testing concurrent programs. description: @@ -33,7 +33,7 @@ source-repository this type: git location: https://github.com/barrucadu/dejafu.git - tag: dejafu-1.3.2.0 + tag: dejafu-1.4.0.0 library exposed-modules: Test.DejaFu @@ -66,7 +66,6 @@ , leancheck >=0.6 && <0.8 , profunctors >=4.0 && <6.0 , random >=1.0 && <1.2 - , ref-fd >=0.4 && <0.5 , transformers >=0.4 && <0.6 -- hs-source-dirs: default-language: Haskell2010