diff --git a/dejafu/Test/DejaFu.hs b/dejafu/Test/DejaFu.hs index 1c0d502..2d1b808 100644 --- a/dejafu/Test/DejaFu.hs +++ b/dejafu/Test/DejaFu.hs @@ -198,7 +198,6 @@ import Control.DeepSeq (NFData(..)) import Control.Monad (when, unless) import Data.List.Extra import Test.DejaFu.Deterministic -import Test.DejaFu.Deterministic.IO (ConcIO) import Test.DejaFu.SCT #if __GLASGOW_HASKELL__ < 710 @@ -213,7 +212,7 @@ import Data.Foldable (Foldable(..)) -- 'MonadConc'. If you need to test something which also uses -- 'MonadIO', use 'autocheckIO'. autocheck :: (Eq a, Show a) - => (forall t. Conc t a) + => (forall t. ConcST t a) -- ^ The computation to test -> IO Bool autocheck = autocheck' TotalStoreOrder @@ -223,7 +222,7 @@ autocheck = autocheck' TotalStoreOrder autocheck' :: (Eq a, Show a) => MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to test -> IO Bool autocheck' memtype conc = dejafus' memtype 2 5 conc autocheckCases @@ -247,7 +246,7 @@ autocheckCases = -- | Check a predicate and print the result to stdout, return 'True' -- if it passes. dejafu :: Show a - => (forall t. Conc t a) + => (forall t. ConcST t a) -- ^ The computation to test -> (String, Predicate a) -- ^ The predicate (with a name) to check @@ -275,7 +274,7 @@ dejafu' :: Show a -> Int -- ^ The maximum difference between the number of yield operations -- across all threads. - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to test -> (String, Predicate a) -- ^ The predicate (with a name) to check @@ -285,7 +284,7 @@ dejafu' memtype pb fb conc test = dejafus' memtype pb fb conc [test] -- | Variant of 'dejafu' which takes a collection of predicates to -- test, returning 'True' if all pass. dejafus :: Show a - => (forall t. Conc t a) + => (forall t. ConcST t a) -- ^ The computation to test -> [(String, Predicate a)] -- ^ The list of predicates (with names) to check @@ -303,7 +302,7 @@ dejafus' :: Show a -> Int -- ^ The maximum difference between the number of yield operations -- across all threads. - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to test -> [(String, Predicate a)] -- ^ The list of predicates (with names) to check @@ -369,7 +368,7 @@ instance Foldable Result where runTest :: Predicate a -- ^ The predicate to check - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to test -> Result a runTest = runTest' TotalStoreOrder 2 5 @@ -387,7 +386,7 @@ runTest' :: -- across all threads. -> Predicate a -- ^ The predicate to check - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to test -> Result a runTest' memtype pb fb predicate conc = predicate $ sctPFBound memtype pb fb conc diff --git a/dejafu/Test/DejaFu/Deterministic.hs b/dejafu/Test/DejaFu/Deterministic.hs index 880d3d0..5dac321 100755 --- a/dejafu/Test/DejaFu/Deterministic.hs +++ b/dejafu/Test/DejaFu/Deterministic.hs @@ -1,10 +1,11 @@ {-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeSynonymInstances #-} --- | Deterministic traced execution of concurrent computations which --- don't do @IO@. +-- | Deterministic traced execution of concurrent computations. -- -- This works by executing the computation on a single thread, calling -- out to the supplied scheduler after each step to determine which @@ -12,10 +13,16 @@ module Test.DejaFu.Deterministic ( -- * The @Conc@ Monad Conc + , ConcST + , ConcIO + + -- * Executing computations , Failure(..) , MemType(..) - , runConc - , runConc' + , runConcST + , runConcIO + , runConcST' + , runConcIO' -- * Execution traces , Trace @@ -36,15 +43,17 @@ module Test.DejaFu.Deterministic import Control.Exception (MaskingState(..)) import Control.Monad.ST (ST, runST) +import Data.IORef (IORef) import Data.STRef (STRef) import Test.DejaFu.Deterministic.Internal import Test.DejaFu.Deterministic.Schedule -import Test.DejaFu.Internal (refST) -import Test.DejaFu.STM (STMST, runTransactionST) +import Test.DejaFu.Internal (refST, refIO) +import Test.DejaFu.STM (STMLike, STMIO, STMST, runTransactionIO, runTransactionST) import Test.DejaFu.STM.Internal (CTVar(..)) import qualified Control.Monad.Catch as Ca import qualified Control.Monad.Conc.Class as C +import qualified Control.Monad.IO.Class as IO #if __GLASGOW_HASKELL__ < 710 import Control.Applicative (Applicative(..), (<$>)) @@ -53,49 +62,39 @@ import Control.Applicative (Applicative(..), (<$>)) {-# ANN module ("HLint: ignore Avoid lambda" :: String) #-} {-# ANN module ("HLint: ignore Use const" :: String) #-} --- | The @Conc@ monad itself. This uses the same --- universally-quantified indexing state trick as used by 'ST' and --- 'STRef's to prevent mutable references from leaking out of the --- monad. -newtype Conc t a = C { unC :: M (ST t) (STRef t) (STMST t) a } deriving (Functor, Applicative, Monad) +newtype Conc n r s a = C { unC :: M n r s a } deriving (Functor, Applicative, Monad) -toConc :: ((a -> Action (ST t) (STRef t) (STMST t)) -> Action (ST t) (STRef t) (STMST t)) -> Conc t a +-- | A 'MonadConc' implementation using @ST@, this should be preferred +-- if you do not need 'liftIO'. +type ConcST t = Conc (ST t) (STRef t) (STMST t) + +-- | A 'MonadConc' implementation using @IO@. +type ConcIO = Conc IO IORef STMIO + +toConc :: ((a -> Action n r s) -> Action n r s) -> Conc n r s a toConc = C . cont -wrap :: (M (ST t) (STRef t) (STMST t) a -> M (ST t) (STRef t) (STMST t) a) -> Conc t a -> Conc t a +wrap :: (M n r s a -> M n r s a) -> Conc n r s a -> Conc n r s a wrap f = C . f . unC -fixed :: Fixed (ST t) (STRef t) (STMST t) -fixed = refST $ \ma -> cont (\c -> ALift $ c <$> ma) +instance IO.MonadIO ConcIO where + liftIO ma = toConc (\c -> ALift (fmap c ma)) --- | 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 @CVar@ --- wakes up all threads blocked on reading it, and it is up to the --- scheduler which one runs next. Taking from a @CVar@ behaves --- analogously. -newtype CVar t a = Var (V (STRef t) a) deriving Eq - --- | The mutable non-blocking reference type. These are like 'IORef's, --- but don't have the potential re-ordering problem mentioned in --- Data.IORef. -newtype CRef t a = Ref (R (STRef t) a) deriving Eq - -instance Ca.MonadCatch (Conc t) where +instance Ca.MonadCatch (Conc n r s) where catch ma h = toConc (ACatching (unC . h) (unC ma)) -instance Ca.MonadThrow (Conc t) where +instance Ca.MonadThrow (Conc n r s) where throwM e = toConc (\_ -> AThrow e) -instance Ca.MonadMask (Conc t) where +instance Ca.MonadMask (Conc n r s) where mask mb = toConc (AMasking MaskedInterruptible (\f -> unC $ mb $ wrap f)) uninterruptibleMask mb = toConc (AMasking MaskedUninterruptible (\f -> unC $ mb $ wrap f)) -instance C.MonadConc (Conc t) where - type CVar (Conc t) = CVar t - type CRef (Conc t) = CRef t - type STMLike (Conc t) = STMST t - type ThreadId (Conc t) = Int +instance Monad n => C.MonadConc (Conc n r (STMLike n r)) where + type CVar (Conc n r (STMLike n r)) = CVar r + type CRef (Conc n r (STMLike n r)) = CRef r + type STMLike (Conc n r (STMLike n r)) = STMLike n r + type ThreadId (Conc n r (STMLike n r)) = Int -- ---------- @@ -114,22 +113,22 @@ instance C.MonadConc (Conc t) where -- ---------- - newCRef a = toConc (\c -> ANewRef a (c . Ref)) + newCRef a = toConc (\c -> ANewRef a c) - readCRef (Ref ref) = toConc (AReadRef ref) - writeCRef (Ref ref) a = toConc (\c -> AWriteRef ref a (c ())) - modifyCRef (Ref ref) f = toConc (AModRef ref f) + readCRef ref = toConc (AReadRef ref) + writeCRef ref a = toConc (\c -> AWriteRef ref a (c ())) + modifyCRef ref f = toConc (AModRef ref f) -- ---------- - newEmptyCVar = toConc (\c -> ANewVar (c . Var)) + newEmptyCVar = toConc (\c -> ANewVar c) - putCVar (Var var) a = toConc (\c -> APutVar var a (c ())) - readCVar (Var var) = toConc (AReadVar var) - takeCVar (Var var) = toConc (ATakeVar var) + putCVar var a = toConc (\c -> APutVar var a (c ())) + readCVar var = toConc (AReadVar var) + takeCVar var = toConc (ATakeVar var) - tryPutCVar (Var var) a = toConc (ATryPutVar var a) - tryTakeCVar (Var var) = toConc (ATryTakeVar var) + tryPutCVar var a = toConc (ATryPutVar var a) + tryTakeCVar var = toConc (ATryTakeVar var) -- ---------- @@ -141,11 +140,11 @@ instance C.MonadConc (Conc t) where -- ---------- - _concKnowsAbout (Left (Var (cvarid, _))) = toConc (\c -> AKnowsAbout (Left cvarid) (c ())) - _concKnowsAbout (Right (V (ctvarid, _))) = toConc (\c -> AKnowsAbout (Right ctvarid) (c ())) + _concKnowsAbout (Left (CVar (cvarid, _))) = toConc (\c -> AKnowsAbout (Left cvarid) (c ())) + _concKnowsAbout (Right (CTVar (ctvarid, _))) = toConc (\c -> AKnowsAbout (Right ctvarid) (c ())) - _concForgets (Left (Var (cvarid, _))) = toConc (\c -> AForgets (Left cvarid) (c ())) - _concForgets (Right (V (ctvarid, _))) = toConc (\c -> AForgets (Right ctvarid) (c ())) + _concForgets (Left (CVar (cvarid, _))) = toConc (\c -> AForgets (Left cvarid) (c ())) + _concForgets (Right (CTVar (ctvarid, _))) = toConc (\c -> AForgets (Right ctvarid) (c ())) _concAllKnown = toConc (\c -> AAllKnown (c ())) @@ -156,19 +155,39 @@ instance C.MonadConc (Conc t) where -- Note how the @t@ in 'Conc' is universally quantified, what this -- means in practice is that you can't do something like this: -- --- > runConc roundRobinSched () newEmptyCVar +-- > runConc roundRobinSched SequentialConsistency () newEmptyCVar -- -- So mutable references cannot leak out of the 'Conc' computation. If -- this is making your head hurt, check out the \"How @runST@ works\" -- section of -- --- --- This uses the 'SequentialConsistency' memory model. -runConc :: Scheduler s -> s -> (forall t. Conc t a) -> (Either Failure a, s, Trace) -runConc sched s ma = - let (r, s', t') = runConc' sched SequentialConsistency s ma +runConcST :: Scheduler s -> MemType -> s -> (forall t. ConcST t a) -> (Either Failure a, s, Trace) +runConcST sched memtype s ma = + let (r, s', t') = runConcST' sched memtype s ma in (r, s', toTrace t') --- | Variant of 'runConc' which produces a 'Trace''. -runConc' :: Scheduler s -> MemType -> s -> (forall t. Conc t a) -> (Either Failure a, s, Trace') -runConc' sched memtype s ma = runST $ runFixed fixed runTransactionST sched memtype s $ unC ma +-- | Variant of 'runConcST' which produces a 'Trace''. +runConcST' :: Scheduler s -> MemType -> s -> (forall t. ConcST t a) -> (Either Failure a, s, Trace') +runConcST' sched memtype s ma = runST $ runFixed fixed runTransactionST sched memtype s $ unC ma where + fixed = refST $ \mb -> cont (\c -> ALift $ c <$> mb) + +-- | Run a concurrent computation in the @IO@ monad 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. +-- +-- __Warning:__ Blocking on the action of another thread in 'liftIO' +-- cannot be detected! So if you perform some potentially blocking +-- action in a 'liftIO' the entire collection of threads may deadlock! +-- You should therefore keep @IO@ blocks small, and only perform +-- blocking operations with the supplied primitives, insofar as +-- possible. +runConcIO :: Scheduler s -> MemType -> s -> ConcIO a -> IO (Either Failure a, s, Trace) +runConcIO sched memtype s ma = do + (r, s', t') <- runConcIO' sched memtype s ma + return (r, s', toTrace t') + +-- | Variant of 'runConcIO' which produces a 'Trace''. +runConcIO' :: Scheduler s -> MemType -> s -> ConcIO a -> IO (Either Failure a, s, Trace') +runConcIO' sched memtype s ma = runFixed fixed runTransactionIO sched memtype s $ unC ma where + fixed = refIO $ \mb -> cont (\c -> ALift $ c <$> mb) diff --git a/dejafu/Test/DejaFu/Deterministic/IO.hs b/dejafu/Test/DejaFu/Deterministic/IO.hs deleted file mode 100644 index 6217287..0000000 --- a/dejafu/Test/DejaFu/Deterministic/IO.hs +++ /dev/null @@ -1,162 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE TypeFamilies #-} - --- | Deterministic traced execution of concurrent computations which --- may do @IO@. --- --- __Warning:__ Blocking on the action of another thread in 'liftIO' --- cannot be detected! So if you perform some potentially blocking --- action in a 'liftIO' the entire collection of threads may deadlock! --- You should therefore keep @IO@ blocks small, and only perform --- blocking operations with the supplied primitives, insofar as --- possible. -module Test.DejaFu.Deterministic.IO - ( -- * The @ConcIO@ Monad - ConcIO - , Failure(..) - , MemType(..) - , runConcIO - , runConcIO' - - -- * Execution traces - , Trace - , Trace' - , Decision(..) - , ThreadAction(..) - , Lookahead(..) - , CVarId - , CRefId - , MaskingState(..) - , toTrace - , showTrace - , showFail - - -- * Scheduling - , module Test.DejaFu.Deterministic.Schedule - ) where - -import Control.Exception (MaskingState(..)) -import Data.IORef (IORef) -import Test.DejaFu.Deterministic.Internal -import Test.DejaFu.Deterministic.Schedule -import Test.DejaFu.Internal (refIO) -import Test.DejaFu.STM (STMIO, runTransactionIO) -import Test.DejaFu.STM.Internal (CTVar(..)) - -import qualified Control.Monad.Catch as Ca -import qualified Control.Monad.Conc.Class as C -import qualified Control.Monad.IO.Class as IO - -#if __GLASGOW_HASKELL__ < 710 -import Control.Applicative (Applicative(..), (<$>)) -#endif - -{-# ANN module ("HLint: ignore Avoid lambda" :: String) #-} -{-# ANN module ("HLint: ignore Use const" :: String) #-} - --- | The 'IO' variant of Test.DejaFu.Deterministic's --- 'Test.DejaFu.Deterministic.Conc' monad. -newtype ConcIO a = C { unC :: M IO IORef STMIO a } deriving (Functor, Applicative, Monad) - -toConcIO :: ((a -> Action IO IORef STMIO) -> Action IO IORef STMIO) -> ConcIO a -toConcIO = C . cont - -wrap :: (M IO IORef STMIO a -> M IO IORef STMIO a) -> ConcIO a -> ConcIO a -wrap f = C . f . unC - -fixed :: Fixed IO IORef STMIO -fixed = refIO $ \ma -> cont (\c -> ALift $ c <$> ma) - --- | The concurrent variable type used with the 'ConcIO' monad. These --- behave the same as @Conc@'s @CVar@s -newtype CVar a = Var (V IORef a) deriving Eq - --- | The mutable non-blocking reference type. These behave the same as --- @Conc@'s @CRef@s -newtype CRef a = Ref (R IORef a) deriving Eq - -instance IO.MonadIO ConcIO where - liftIO ma = toConcIO (\c -> ALift (fmap c ma)) - -instance Ca.MonadCatch ConcIO where - catch ma h = toConcIO (ACatching (unC . h) (unC ma)) - -instance Ca.MonadThrow ConcIO where - throwM e = toConcIO (\_ -> AThrow e) - -instance Ca.MonadMask ConcIO where - mask mb = toConcIO (AMasking MaskedInterruptible (\f -> unC $ mb $ wrap f)) - uninterruptibleMask mb = toConcIO (AMasking MaskedUninterruptible (\f -> unC $ mb $ wrap f)) - -instance C.MonadConc ConcIO where - type CVar ConcIO = CVar - type CRef ConcIO = CRef - type STMLike ConcIO = STMIO - type ThreadId ConcIO = Int - - -- ---------- - - forkWithUnmask ma = toConcIO (AFork (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop))) - forkOnWithUnmask _ = C.forkWithUnmask - - -- This implementation lies and always returns 2. There is no way to - -- verify in the computation that this is a lie, and will - -- potentially avoid special-case behaviour for 1 capability, so it - -- seems a sane choice. - getNumCapabilities = return 2 - - myThreadId = toConcIO AMyTId - - yield = toConcIO (\c -> AYield (c ())) - - -- ---------- - - newCRef a = toConcIO (\c -> ANewRef a (c . Ref)) - - readCRef (Ref ref) = toConcIO (AReadRef ref) - writeCRef (Ref ref) a = toConcIO (\c -> AWriteRef ref a (c ())) - modifyCRef (Ref ref) f = toConcIO (AModRef ref f) - - -- ---------- - - newEmptyCVar = toConcIO (\c -> ANewVar (c . Var)) - - putCVar (Var var) a = toConcIO (\c -> APutVar var a (c ())) - readCVar (Var var) = toConcIO (AReadVar var) - takeCVar (Var var) = toConcIO (ATakeVar var) - - tryPutCVar (Var var) a = toConcIO (ATryPutVar var a) - tryTakeCVar (Var var) = toConcIO (ATryTakeVar var) - - -- ---------- - - throwTo tid e = toConcIO (\c -> AThrowTo tid e (c ())) - - -- ---------- - - atomically = toConcIO . AAtom - - -- ---------- - - _concKnowsAbout (Left (Var (cvarid, _))) = toConcIO (\c -> AKnowsAbout (Left cvarid) (c ())) - _concKnowsAbout (Right (V (ctvarid, _))) = toConcIO (\c -> AKnowsAbout (Right ctvarid) (c ())) - - _concForgets (Left (Var (cvarid, _))) = toConcIO (\c -> AForgets (Left cvarid) (c ())) - _concForgets (Right (V (ctvarid, _))) = toConcIO (\c -> AForgets (Right ctvarid) (c ())) - - _concAllKnown = toConcIO (\c -> AAllKnown (c ())) - --- | Run a concurrent computation with a given 'Scheduler' and initial --- state, returning an failure reason on error. Also returned is the --- final state of the scheduler, and an execution trace. --- --- This uses the 'SequentialConsistency' memory model. -runConcIO :: Scheduler s -> s -> ConcIO a -> IO (Either Failure a, s, Trace) -runConcIO sched s ma = do - (r, s', t') <- runConcIO' sched SequentialConsistency s ma - return (r, s', toTrace t') - --- | Variant of 'runConcIO' which produces a 'Trace''. -runConcIO' :: Scheduler s -> MemType -> s -> ConcIO a -> IO (Either Failure a, s, Trace') -runConcIO' sched memtype s ma = runFixed fixed runTransactionIO sched memtype s $ unC ma diff --git a/dejafu/Test/DejaFu/Deterministic/Internal.hs b/dejafu/Test/DejaFu/Deterministic/Internal.hs index 662f649..2e34e8a 100755 --- a/dejafu/Test/DejaFu/Deterministic/Internal.hs +++ b/dejafu/Test/DejaFu/Deterministic/Internal.hs @@ -10,9 +10,9 @@ module Test.DejaFu.Deterministic.Internal , runFixed' -- * The @Conc@ Monad - , M - , V - , R + , M(..) + , CVar(..) + , CRef(..) , Fixed , cont , runCont @@ -170,15 +170,15 @@ lookahead = unsafeToNonEmpty . lookahead' where lookahead' (AFork _ _) = [WillFork] lookahead' (AMyTId _) = [WillMyThreadId] lookahead' (ANewVar _) = [WillNew] - lookahead' (APutVar (c, _) _ k) = WillPut c : lookahead' k - lookahead' (ATryPutVar (c, _) _ _) = [WillTryPut c] - lookahead' (AReadVar (c, _) _) = [WillRead c] - lookahead' (ATakeVar (c, _) _) = [WillTake c] - lookahead' (ATryTakeVar (c, _) _) = [WillTryTake c] + lookahead' (APutVar (CVar (c, _)) _ k) = WillPut c : lookahead' k + lookahead' (ATryPutVar (CVar (c, _)) _ _) = [WillTryPut c] + lookahead' (AReadVar (CVar (c, _)) _) = [WillRead c] + lookahead' (ATakeVar (CVar (c, _)) _) = [WillTake c] + lookahead' (ATryTakeVar (CVar (c, _)) _) = [WillTryTake c] lookahead' (ANewRef _ _) = [WillNewRef] - lookahead' (AReadRef (r, _) _) = [WillReadRef r] - lookahead' (AModRef (r, _) _ _) = [WillModRef r] - lookahead' (AWriteRef (r, _) _ k) = WillWriteRef r : lookahead' k + lookahead' (AReadRef (CRef (r, _)) _) = [WillReadRef r] + lookahead' (AModRef (CRef (r, _)) _ _) = [WillModRef r] + lookahead' (AWriteRef (CRef (r, _)) _ k) = WillWriteRef r : lookahead' k lookahead' (ACommit t c) = [WillCommitRef t c] lookahead' (AAtom _ _) = [WillSTM] lookahead' (AThrow _) = [WillThrow] @@ -220,12 +220,12 @@ stepThread fixed runstm memtype action idSource tid threads wb = case action of AFork a b -> stepFork a b AMyTId c -> stepMyTId c AYield c -> stepYield c - ANewVar c -> stepNew c - APutVar ref a c -> stepPut ref a c - ATryPutVar ref a c -> stepTryPut ref a c - AReadVar ref c -> stepGet ref c - ATakeVar ref c -> stepTake ref c - ATryTakeVar ref c -> stepTryTake ref c + ANewVar c -> stepNewVar c + APutVar var a c -> stepPutVar var a c + ATryPutVar var a c -> stepTryPutVar var a c + AReadVar var c -> stepReadVar var c + ATakeVar var c -> stepTakeVar var c + ATryTakeVar var c -> stepTryTakeVar var c ANewRef a c -> stepNewRef a c AReadRef ref c -> stepReadRef ref c AModRef ref f c -> stepModRef ref f c @@ -259,45 +259,45 @@ stepThread fixed runstm memtype action idSource tid threads wb = case action of -- | Put a value into a @CVar@, blocking the thread until it's -- empty. - stepPut cvar@(cvid, _) a c = synchronised $ do + stepPutVar cvar@(CVar (cvid, _)) a c = synchronised $ do (success, threads', woken) <- putIntoCVar True cvar a (const c) fixed tid threads simple threads' $ if success then Put cvid woken else BlockedPut cvid -- | Try to put a value into a @CVar@, without blocking. - stepTryPut cvar@(cvid, _) a c = synchronised $ do + stepTryPutVar cvar@(CVar (cvid, _)) a c = synchronised $ do (success, threads', woken) <- putIntoCVar False cvar a c fixed tid threads simple threads' $ TryPut cvid success woken -- | Get the value from a @CVar@, without emptying, blocking the -- thread until it's full. - stepGet cvar@(cvid, _) c = synchronised $ do + stepReadVar cvar@(CVar (cvid, _)) c = synchronised $ do (success, threads', _) <- readFromCVar False True cvar (c . fromJust) fixed tid threads simple threads' $ if success then Read cvid else BlockedRead cvid -- | Take the value from a @CVar@, blocking the thread until it's -- full. - stepTake cvar@(cvid, _) c = synchronised $ do + stepTakeVar cvar@(CVar (cvid, _)) c = synchronised $ do (success, threads', woken) <- readFromCVar True True cvar (c . fromJust) fixed tid threads simple threads' $ if success then Take cvid woken else BlockedTake cvid -- | Try to take the value from a @CVar@, without blocking. - stepTryTake cvar@(cvid, _) c = synchronised $ do + stepTryTakeVar cvar@(CVar (cvid, _)) c = synchronised $ do (success, threads', woken) <- readFromCVar True False cvar c fixed tid threads simple threads' $ TryTake cvid success woken -- | Read from a @CRef@. - stepReadRef cref@(crid, _) c = do + stepReadRef cref@(CRef (crid, _)) c = do val <- readCRef fixed cref tid simple (goto (c val) tid threads) $ ReadRef crid -- | Modify a @CRef@. - stepModRef cref@(crid, _) f c = synchronised $ do + stepModRef cref@(CRef (crid, _)) f c = synchronised $ do (new, val) <- f <$> readCRef fixed cref tid writeImmediate fixed cref new simple (goto (c val) tid threads) $ ModRef crid -- | Write to a @CRef@ without synchronising - stepWriteRef cref@(crid, _) a c = case memtype of + stepWriteRef cref@(CRef (crid, _)) a c = case memtype of -- Write immediately. SequentialConsistency -> do writeImmediate fixed cref a @@ -405,17 +405,17 @@ stepThread fixed runstm memtype action idSource tid threads wb = case action of threads' = M.alter (\(Just thread) -> Just $ thread { _continuation = c, _masking = m }) tid threads -- | Create a new @CVar@, using the next 'CVarId'. - stepNew c = do + stepNewVar c = do let (idSource', newcvid) = nextCVId idSource ref <- newRef fixed Nothing - let cvar = (newcvid, ref) + let cvar = CVar (newcvid, ref) return $ Right (knows [Left newcvid] tid $ goto (c cvar) tid threads, idSource', New newcvid, wb) -- | Create a new @CRef@, using the next 'CRefId'. stepNewRef a c = do let (idSource', newcrid) = nextCRId idSource ref <- newRef fixed (I.empty, a) - let cref = (newcrid, ref) + let cref = CRef (newcrid, ref) return $ Right (goto (c cref) tid threads, idSource', NewRef newcrid, wb) -- | Lift an action from the underlying monad into the @Conc@ diff --git a/dejafu/Test/DejaFu/Deterministic/Internal/Common.hs b/dejafu/Test/DejaFu/Deterministic/Internal/Common.hs index dce15cf..a2cc787 100644 --- a/dejafu/Test/DejaFu/Deterministic/Internal/Common.hs +++ b/dejafu/Test/DejaFu/Deterministic/Internal/Common.hs @@ -34,15 +34,24 @@ instance Monad (M n r s) where return = pure m >>= k = M $ \c -> runM m (\x -> runM (k x) c) --- | CVars are represented as a unique numeric identifier, and a +-- | 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 @CVar@ +-- wakes up all threads blocked on reading it, and it is up to the +-- scheduler which one runs next. Taking from a @CVar@ behaves +-- analogously. +-- +-- @CVar@s are represented as a unique numeric identifier, and a -- reference containing a Maybe value. -type V r a = (CVarId, r (Maybe a)) +newtype CVar r a = CVar (CVarId, r (Maybe a)) --- | CRefs are represented as a unique numeric identifier, and 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) and the current value -- visible to all threads. -type R r a = (CRefId, r (IntMap a, a)) +newtype CRef r a = CRef (CRefId, r (IntMap a, a)) -- | Dict of methods for implementations to override. type Fixed n r s = Ref n r (M n r s) @@ -63,30 +72,35 @@ runCont = runM -- primitives of the concurrency. 'spawn' is absent as it is -- implemented in terms of 'newEmptyCVar', 'fork', and 'putCVar'. data Action n r s = - AFork ((forall b. M n r s b -> M n r s b) -> Action n r s) (ThreadId -> Action n r s) + AFork ((forall b. M n r s b -> M n r s b) -> Action n r s) (ThreadId -> Action n r s) | AMyTId (ThreadId -> Action n r s) - | forall a. APutVar (V r a) a (Action n r s) - | forall a. ATryPutVar (V r a) a (Bool -> Action n r s) - | forall a. AReadVar (V r a) (a -> Action n r s) - | forall a. ATakeVar (V r a) (a -> Action n r s) - | forall a. ATryTakeVar (V r a) (Maybe a -> Action n r s) - | forall a. AReadRef (R r a) (a -> Action n r s) - | forall a b. AModRef (R r a) (a -> (a, b)) (b -> Action n r s) - | forall a. AWriteRef (R r a) a (Action n r s) - | forall a. AAtom (s a) (a -> Action n r s) - | forall a. ANewVar (V r a -> Action n r s) - | forall a. ANewRef a (R r a -> Action n r s) - | ALift (n (Action n r s)) - | forall e. Exception e => AThrow e - | forall e. Exception e => AThrowTo ThreadId e (Action n r s) + + | forall a. ANewVar (CVar r a -> Action n r s) + | forall a. APutVar (CVar r a) a (Action n r s) + | forall a. ATryPutVar (CVar r a) a (Bool -> Action n r s) + | forall a. AReadVar (CVar r a) (a -> Action n r s) + | forall a. ATakeVar (CVar r a) (a -> Action n r s) + | forall a. ATryTakeVar (CVar r a) (Maybe a -> Action n r s) + + | forall a. ANewRef a (CRef r a -> Action n r s) + | forall a. AReadRef (CRef r a) (a -> Action n r s) + | forall a b. AModRef (CRef r a) (a -> (a, b)) (b -> Action n r s) + | forall a. AWriteRef (CRef r a) a (Action n r s) + + | forall e. Exception e => AThrow e + | forall e. Exception e => AThrowTo ThreadId e (Action n r s) | forall a e. Exception e => ACatching (e -> M n r s a) (M n r s a) (a -> Action n r s) | APopCatching (Action n r s) | forall a. AMasking MaskingState ((forall b. M n r s b -> M n r s b) -> M n r s a) (a -> Action n r s) | AResetMask Bool Bool MaskingState (Action n r s) + | AKnowsAbout (Either CVarId CTVarId) (Action n r s) - | AForgets (Either CVarId CTVarId) (Action n r s) - | AAllKnown (Action n r s) - | AYield (Action n r s) + | AForgets (Either CVarId CTVarId) (Action n r s) + | AAllKnown (Action n r s) + + | forall a. AAtom (s a) (a -> Action n r s) + | ALift (n (Action n r s)) + | AYield (Action n r s) | AReturn (Action n r s) | ACommit ThreadId CRefId | AStop diff --git a/dejafu/Test/DejaFu/Deterministic/Internal/Memory.hs b/dejafu/Test/DejaFu/Deterministic/Internal/Memory.hs index 7f4252d..1f4b0eb 100755 --- a/dejafu/Test/DejaFu/Deterministic/Internal/Memory.hs +++ b/dejafu/Test/DejaFu/Deterministic/Internal/Memory.hs @@ -34,15 +34,15 @@ newtype WriteBuffer r = WriteBuffer { buffer :: IntMap (Seq (BufferedWrite r)) } -- 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 -> R r a -> a -> BufferedWrite r + BufferedWrite :: ThreadId -> CRef r a -> a -> BufferedWrite r -- | An empty write buffer. emptyBuffer :: WriteBuffer r emptyBuffer = WriteBuffer I.empty -- | Add a new write to the end of a buffer. -bufferWrite :: Monad n => Fixed n r s -> WriteBuffer r -> Int -> R r a -> a -> ThreadId -> n (WriteBuffer r) -bufferWrite fixed (WriteBuffer wb) i cref@(_, ref) new tid = do +bufferWrite :: Monad n => Fixed n r s -> WriteBuffer r -> Int -> CRef r a -> a -> ThreadId -> n (WriteBuffer r) +bufferWrite fixed (WriteBuffer wb) i cref@(CRef (_, ref)) new tid = do -- Construct the new write buffer let write = singleton $ BufferedWrite tid cref new let buffer' = I.insertWith (><) i write wb @@ -64,15 +64,15 @@ commitWrite fixed w@(WriteBuffer wb) i = case maybe EmptyL viewl $ I.lookup i wb -- | Read from a @CRef@, returning a newer thread-local non-committed -- write if there is one. -readCRef :: Monad n => Fixed n r s -> R r a -> ThreadId -> n a -readCRef fixed (_, ref) tid = do +readCRef :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n a +readCRef fixed (CRef (_, ref)) tid = do (map, def) <- readRef fixed ref return $ I.findWithDefault def tid map -- | Write and commit to a @CRef@ immediately, clearing the update -- map. -writeImmediate :: Monad n => Fixed n r s -> R r a -> a -> n () -writeImmediate fixed (_, ref) a = writeRef fixed ref (I.empty, a) +writeImmediate :: Monad n => Fixed n r s -> CRef r a -> a -> n () +writeImmediate fixed (CRef (_, ref)) a = writeRef fixed ref (I.empty, a) -- | Flush all writes in the buffer. writeBarrier :: Monad n => Fixed n r s -> WriteBuffer r -> n () @@ -83,7 +83,7 @@ writeBarrier fixed (WriteBuffer wb) = mapM_ flush $ I.elems wb where addCommitThreads :: WriteBuffer r -> Threads n r s -> Threads n r s addCommitThreads (WriteBuffer wb) ts = ts <> M.fromList phantoms where phantoms = [(negate k - 1, mkthread $ fromJust c) | (k, b) <- I.toList wb, let c = go $ viewl b, isJust c] - go (BufferedWrite tid (crid, _) _ :< _) = Just $ ACommit tid crid + go (BufferedWrite tid (CRef (crid, _)) _ :< _) = Just $ ACommit tid crid go EmptyL = Nothing -- | Remove phantom threads. @@ -96,9 +96,9 @@ delCommitThreads = M.filterWithKey $ \k _ -> k >= 0 -- | Put a value into a @CVar@, in either a blocking or nonblocking -- way. putIntoCVar :: Monad n - => Bool -> V r a -> a -> (Bool -> Action n r s) + => Bool -> CVar r a -> a -> (Bool -> Action n r s) -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId]) -putIntoCVar blocking (cvid, ref) a c fixed threadid threads = do +putIntoCVar blocking (CVar (cvid, ref)) a c fixed threadid threads = do val <- readRef fixed ref case val of @@ -118,9 +118,9 @@ putIntoCVar blocking (cvid, ref) a c fixed threadid threads = do -- | Take a value from a @CVar@, in either a blocking or nonblocking -- way. readFromCVar :: Monad n - => Bool -> Bool -> V r a -> (Maybe a -> Action n r s) + => Bool -> Bool -> CVar r a -> (Maybe a -> Action n r s) -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId]) -readFromCVar emptying blocking (cvid, ref) c fixed threadid threads = do +readFromCVar emptying blocking (CVar (cvid, ref)) c fixed threadid threads = do val <- readRef fixed ref case val of diff --git a/dejafu/Test/DejaFu/SCT.hs b/dejafu/Test/DejaFu/SCT.hs index 687e98d..81db8d3 100755 --- a/dejafu/Test/DejaFu/SCT.hs +++ b/dejafu/Test/DejaFu/SCT.hs @@ -76,7 +76,6 @@ import Data.IntMap.Strict (IntMap) import Data.Sequence (Seq, (|>)) import Data.Maybe (maybeToList, isNothing) import Test.DejaFu.Deterministic -import Test.DejaFu.Deterministic.IO (ConcIO, runConcIO') import Test.DejaFu.SCT.Internal import qualified Data.IntMap.Strict as I @@ -94,7 +93,7 @@ sctPreBound :: MemType -> Int -- ^ The maximum number of pre-emptions to allow in a single -- execution - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to run many times -> [(Either Failure a, Trace)] sctPreBound memtype pb = sctBounded memtype (pbBound pb) pbBacktrack pbInitialise @@ -179,7 +178,7 @@ sctFairBound :: MemType -> Int -- ^ The maximum difference between the number of yield operations -- performed by different threads. - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to run many times -> [(Either Failure a, Trace)] sctFairBound memtype fb = sctBounded memtype (fBound fb) fBacktrack pbInitialise @@ -260,7 +259,7 @@ sctPFBound :: MemType -- ^ The pre-emption bound -> Int -- ^ The fair bound - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to run many times -> [(Either Failure a, Trace)] sctPFBound memtype pb fb = sctBounded memtype (pfBound pb fb) pfBacktrack pbInitialise @@ -302,9 +301,9 @@ sctBounded :: MemType -- backtracking point. -> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> NonEmpty ThreadId) -- ^ Produce possible scheduling decisions, all will be tried. - -> (forall t. Conc t a) -> [(Either Failure a, Trace)] + -> (forall t. ConcST t a) -> [(Either Failure a, Trace)] sctBounded memtype bf backtrack initialise c = runIdentity $ sctBoundedM memtype bf backtrack initialise run where - run memty sched s = Identity $ runConc' sched memty s c + run memty sched s = Identity $ runConcST' sched memty s c -- | Variant of 'sctBounded' for computations which do 'IO'. sctBoundedIO :: MemType diff --git a/dejafu/Test/DejaFu/STM/Internal.hs b/dejafu/Test/DejaFu/STM/Internal.hs index 4cc48cf..4fae03c 100755 --- a/dejafu/Test/DejaFu/STM/Internal.hs +++ b/dejafu/Test/DejaFu/STM/Internal.hs @@ -51,7 +51,7 @@ data STMAction n r -- | A 'CTVar' is a tuple of a unique ID and the value contained. The -- ID is so that blocked transactions can be re-run when a 'CTVar' -- they depend on has changed. -newtype CTVar r a = V (CTVarId, r a) +newtype CTVar r a = CTVar (CTVarId, r a) -- | The unique ID of a 'CTVar'. Only meaningful within a single -- concurrent computation. @@ -141,11 +141,11 @@ stepTrans fixed act newctvid = case act of Just exc' -> transaction (h exc') c Nothing -> return (SThrow exc, nothing, newctvid, [], [])) - stepRead (V (ctvid, ref)) c = do + stepRead (CTVar (ctvid, ref)) c = do val <- readRef fixed ref return (c val, nothing, newctvid, [ctvid], []) - stepWrite (V (ctvid, ref)) a c = do + stepWrite (CTVar (ctvid, ref)) a c = do old <- readRef fixed ref writeRef fixed ref a return (c, writeRef fixed ref old, newctvid, [], [ctvid]) @@ -153,7 +153,7 @@ stepTrans fixed act newctvid = case act of stepNew a c = do let newctvid' = newctvid + 1 ref <- newRef fixed a - let ctvar = V (newctvid, ref) + let ctvar = CTVar (newctvid, ref) return (c ctvar, nothing, newctvid', [], [newctvid]) stepOrElse a b c = onFailure a c diff --git a/dejafu/dejafu.cabal b/dejafu/dejafu.cabal index ecc56f1..f7d63b2 100755 --- a/dejafu/dejafu.cabal +++ b/dejafu/dejafu.cabal @@ -88,7 +88,6 @@ library , Test.DejaFu , Test.DejaFu.Deterministic - , Test.DejaFu.Deterministic.IO , Test.DejaFu.Deterministic.Schedule , Test.DejaFu.SCT , Test.DejaFu.STM diff --git a/hunit-dejafu/Test/HUnit/DejaFu.hs b/hunit-dejafu/Test/HUnit/DejaFu.hs index 76110a5..9ba161c 100755 --- a/hunit-dejafu/Test/HUnit/DejaFu.hs +++ b/hunit-dejafu/Test/HUnit/DejaFu.hs @@ -22,8 +22,7 @@ module Test.HUnit.DejaFu ) where import Test.DejaFu -import Test.DejaFu.Deterministic (Conc, showFail, showTrace) -import Test.DejaFu.Deterministic.IO (ConcIO) +import Test.DejaFu.Deterministic (ConcST, ConcIO, showFail, showTrace) import Test.DejaFu.SCT (sctPFBound, sctPFBoundIO) import Test.HUnit (Test(..), assertString) @@ -37,7 +36,7 @@ import Test.HUnit (Test(..), assertString) -- 'MonadConc'. If you need to test something which also uses -- 'MonadIO', use 'testAutoIO'. testAuto :: (Eq a, Show a) - => (forall t. Conc t a) + => (forall t. ConcST t a) -- ^ The computation to test -> Test testAuto = testAuto' TotalStoreOrder @@ -47,7 +46,7 @@ testAuto = testAuto' TotalStoreOrder testAuto' :: (Eq a, Show a) => MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to test -> Test testAuto' memtype conc = testDejafus' memtype 2 5 conc autocheckCases @@ -73,7 +72,7 @@ autocheckCases = -- | Check that a predicate holds. testDejafu :: Show a - => (forall t. Conc t a) + => (forall t. ConcST t a) -- ^ The computation to test -> String -- ^ The name of the test. @@ -93,7 +92,7 @@ testDejafu' :: Show a -> Int -- ^ The maximum difference between the number of yield operations -- across all threads. - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to test -> String -- ^ The name of the test. @@ -106,7 +105,7 @@ testDejafu' memtype pb fb conc name p = testDejafus' memtype pb fb conc [(name, -- test. This will share work between the predicates, rather than -- running the concurrent computation many times for each predicate. testDejafus :: Show a - => (forall t. Conc t a) + => (forall t. ConcST t a) -- ^ The computation to test -> [(String, Predicate a)] -- ^ The list of predicates (with names) to check @@ -124,7 +123,7 @@ testDejafus' :: Show a -> Int -- ^ The maximum difference between the number of yield operations -- across all threads. - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to test -> [(String, Predicate a)] -- ^ The list of predicates (with names) to check @@ -151,7 +150,7 @@ testDejafusIO' = testio -- HUnit integration -- | Produce a HUnit 'Test' from a Deja Fu test. -test :: Show a => MemType -> Int -> Int -> (forall t. Conc t a) -> [(String, Predicate a)] -> Test +test :: Show a => MemType -> Int -> Int -> (forall t. ConcST t a) -> [(String, Predicate a)] -> Test test memtype pb fb conc tests = case map toTest tests of [t] -> t ts -> TestList ts diff --git a/tasty-dejafu/Test/Tasty/DejaFu.hs b/tasty-dejafu/Test/Tasty/DejaFu.hs index 0f7bdcb..749d9e7 100755 --- a/tasty-dejafu/Test/Tasty/DejaFu.hs +++ b/tasty-dejafu/Test/Tasty/DejaFu.hs @@ -25,8 +25,7 @@ module Test.Tasty.DejaFu import Data.Typeable (Typeable) import Test.DejaFu -import Test.DejaFu.Deterministic (Conc, Trace, showFail, showTrace) -import Test.DejaFu.Deterministic.IO (ConcIO) +import Test.DejaFu.Deterministic (ConcST, ConcIO, Trace, showFail, showTrace) import Test.DejaFu.SCT (sctPFBound, sctPFBoundIO) import Test.Tasty (TestName, TestTree, testGroup) import Test.Tasty.Providers (IsTest(..), singleTest, testPassed, testFailed) @@ -41,7 +40,7 @@ import Test.Tasty.Providers (IsTest(..), singleTest, testPassed, testFailed) -- 'MonadConc'. If you need to test something which also uses -- 'MonadIO', use 'testAutoIO'. testAuto :: (Eq a, Show a) - => (forall t. Conc t a) + => (forall t. ConcST t a) -- ^ The computation to test -> TestTree testAuto = testAuto' TotalStoreOrder @@ -51,7 +50,7 @@ testAuto = testAuto' TotalStoreOrder testAuto' :: (Eq a, Show a) => MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to test -> TestTree testAuto' memtype conc = testDejafus' memtype 2 5 conc autocheckCases @@ -77,7 +76,7 @@ autocheckCases = -- | Check that a predicate holds. testDejafu :: Show a - => (forall t. Conc t a) + => (forall t. ConcST t a) -- ^ The computation to test -> TestName -- ^ The name of the test. @@ -97,7 +96,7 @@ testDejafu' :: Show a -> Int -- ^ The maximum difference between the number of yield operations -- across all threads. - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to test -> TestName -- ^ The name of the test. @@ -110,7 +109,7 @@ testDejafu' memtype pb fb conc name p = testDejafus' memtype pb fb conc [(name, -- test. This will share work between the predicates, rather than -- running the concurrent computation many times for each predicate. testDejafus :: Show a - => (forall t. Conc t a) + => (forall t. ConcST t a) -- ^ The computation to test -> [(TestName, Predicate a)] -- ^ The list of predicates (with names) to check @@ -128,7 +127,7 @@ testDejafus' :: Show a -> Int -- ^ The maximum difference between the number of yield operations -- across all threads. - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to test -> [(TestName, Predicate a)] -- ^ The list of predicates (with names) to check @@ -178,7 +177,7 @@ instance IsTest ConcIOTest where return $ if null err then testPassed "" else testFailed err -- | Produce a Tasty 'TestTree' from a Deja Fu test. -test :: Show a => MemType -> Int -> Int -> (forall t. Conc t a) -> [(TestName, Predicate a)] -> TestTree +test :: Show a => MemType -> Int -> Int -> (forall t. ConcST t a) -> [(TestName, Predicate a)] -> TestTree test memtype pb fb conc tests = case map toTest tests of [t] -> t ts -> testGroup "Deja Fu Tests" ts