mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-11-23 22:23:18 +03:00
Merge Conc and ConcIO implementations
This commit is contained in:
Michael Walker
parent
5f78dc5b99
commit
06a63dcc33
@ -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
|
||||
|
||||
@ -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
|
||||
-- <https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html>
|
||||
--
|
||||
-- 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)
|
||||
|
||||
@ -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
|
||||
@ -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@
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -88,7 +88,6 @@ library
|
||||
|
||||
, Test.DejaFu
|
||||
, Test.DejaFu.Deterministic
|
||||
, Test.DejaFu.Deterministic.IO
|
||||
, Test.DejaFu.Deterministic.Schedule
|
||||
, Test.DejaFu.SCT
|
||||
, Test.DejaFu.STM
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
Loading…
Reference in New Issue
Block a user