barrucadu/dejafu
1
1
Fork 0
mirror of https://github.com/barrucadu/dejafu.git synced 2024-09-11 06:25:45 +03:00
Code Issues Projects Releases Wiki Activity

Require a 'MonadConc n' instance to run 'ConcT r n' expressions

Browse Source 
This is preparation for adding bound threads.  The instance isn't used
in this commit, but the diff is large enough that I feel this should
be a separate commit for ease of review.

Fallout:

- The MonadBaseControl IO instance is gone, as I'm not sure how to do
  it generally.
- The pure/IO split is gone, everything is now monadic.
- The execution, SCT, and dejafu functions are of the form (MonadConc
  n, MonadRef r n) => ...
This commit is contained in:
Michael Walker 2017-10-09 18:48:41 +01:00
parent 99cae72b42
commit 31d29c11ea
17 changed files with 228 additions and 543 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.weeder.yaml
View File

@ -109,7 +109,7 @@
- module:
- name: Examples.ClassLaws
- identifier:
- CST
- C
- Concurrently
- concurrently
- concurrently'

5
dejafu-tests/Cases/Async.hs
View File

@ -1,6 +1,5 @@
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
module Cases.Async where
@ -15,7 +14,7 @@ import Data.List (sort)
import Data.Maybe (isJust, isNothing)
import Data.Typeable (Typeable)
import Test.DejaFu (alwaysTrue)
import Test.DejaFu.Conc (ConcST)
import Test.DejaFu.Conc (ConcIO)
import Common
@ -180,7 +179,7 @@ assertEqual err a1 a2
| a1 == a2 = pure ()
| otherwise = assertFailure err
testCase :: String -> (forall t. ConcST t ()) -> Test
testCase :: String -> ConcIO () -> Test
testCase name c = djfu name (alwaysTrue p) (try c) where
p (Right (Left (e::SomeException))) = False
p (Right _) = True

16
dejafu-tests/Cases/Litmus.hs
View File

@ -6,7 +6,7 @@ import Control.Monad (replicateM)
import Control.Monad.ST (runST)
import Data.List (nub, sort)
import Test.DejaFu (MemType(..), defaultWay, gives')
import Test.DejaFu.Conc (ConcST)
import Test.DejaFu.Conc (ConcIO)
import Test.DejaFu.SCT (runSCT)
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (hUnitTestToTests)
@ -46,7 +46,7 @@ tests =
in litmusTest "Independent Read Independent Write" intelWP28 out out out
]
litmusTest :: (Eq a, Show a) => String -> (forall t. ConcST t a) -> [a] -> [a] -> [a] -> Test
litmusTest :: (Eq a, Show a) => String -> ConcIO a -> [a] -> [a] -> [a] -> Test
litmusTest name act sq tso pso = testGroup name . hUnitTestToTests $ test
[ testDejafuWay defaultWay SequentialConsistency act "SQ" (gives' sq)
, testDejafuWay defaultWay TotalStoreOrder act "TSO" (gives' tso)
@ -62,14 +62,14 @@ litmusTest name act sq tso pso = testGroup name . hUnitTestToTests $ test
-- possible results. This is why dejafu is good!
compareTest :: forall a. (Ord a, Show a) => (forall m. MonadConc m => m a) -> IO ()
compareTest act = do
putStrLn $ "DejaFu-SQ: " ++ results SequentialConsistency
putStrLn $ "DejaFu-TSO: " ++ results TotalStoreOrder
putStrLn $ "DejaFu-PSO: " ++ results PartialStoreOrder
putStr "IO: " >> ioResults >>= putStrLn
putStr "DejaFu-SQ: " >> results SequentialConsistency
putStr "DejaFu-TSO: " >> results TotalStoreOrder
putStr "DejaFu-PSO: " >> results PartialStoreOrder
putStr "IO: " >> ioResults >>= putStrLn
where
results memtype = show . nub . sort . map (\(Right a,_) -> a) $
runST (runSCT defaultWay memtype act)
results memtype = show . nub . sort . map (\(Right a,_) -> a) <$>
runSCT defaultWay memtype act
ioResults = show . nub . sort <$> replicateM 99999 act

11
dejafu-tests/Common.hs
View File

@ -1,5 +1,4 @@
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
module Common
( module Common
@ -13,7 +12,7 @@ import Control.Monad.Conc.Class
import Control.Monad.STM.Class
import System.Random (mkStdGen)
import Test.DejaFu (Predicate, Failure, Result(..), alwaysTrue)
import Test.DejaFu.Conc (ConcST)
import Test.DejaFu.Conc (ConcIO)
import qualified Test.Framework as TF
import Test.Framework.Providers.HUnit (hUnitTestToTests)
import qualified Test.HUnit as TH
@ -47,16 +46,16 @@ instance IsTest t => IsTest [t] where
toTestList = concatMap toTestList
data T where
T :: Show a => String -> (forall t. ConcST t a) -> Predicate a -> T
BT :: Show a => String -> (forall t. ConcST t a) -> Predicate a -> Bounds -> T
T :: Show a => String -> ConcIO a -> Predicate a -> T
BT :: Show a => String -> ConcIO a -> Predicate a -> Bounds -> T
testGroup :: IsTest t => String -> t -> TF.Test
testGroup name = TF.testGroup name . toTestList
djfu :: Show a => String -> Predicate a -> (forall t. ConcST t a) -> TF.Test
djfu :: Show a => String -> Predicate a -> ConcIO a -> TF.Test
djfu name p c = hunitTest $ testDejafu c name p
djfuT :: Show a => String -> Predicate a -> (forall t. ConcST t a) -> [TF.Test]
djfuT :: Show a => String -> Predicate a -> ConcIO a -> [TF.Test]
djfuT name p c = toTestList $ T name c p
alwaysFailsWith :: (Failure -> Bool) -> Predicate a

61
dejafu-tests/Examples/ClassLaws.hs
View File

@ -1,5 +1,3 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ViewPatterns #-}
@ -15,14 +13,13 @@ import Control.Monad.Conc.Class
import Data.Maybe (isJust)
import Data.Set (fromList)
import Test.DejaFu (defaultBounds, defaultMemType)
import Test.DejaFu.Conc (ConcST)
import Test.DejaFu.Conc (ConcIO)
import Test.DejaFu.SCT (sctBound)
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.QuickCheck2 (testProperty)
import Test.QuickCheck (Arbitrary(..), expectFailure, monomorphic)
import Test.QuickCheck (Arbitrary(..), Property, expectFailure, monomorphic)
import Test.QuickCheck.Function (Fun, apply)
import Examples.ClassLaws.Impredicative
import Test.QuickCheck.Monadic (assert, monadicIO, run)
-- Tests at bottom of file due to Template Haskell silliness.
@ -37,7 +34,7 @@ import Examples.ClassLaws.Impredicative
-- before delivering the result of type @a@.
newtype Concurrently m a = Concurrently { runConcurrently :: m a }
type CST t = Concurrently (ConcST t)
type C = Concurrently ConcIO
--------------------------------------------------------------------------------
-- Functor
@ -46,11 +43,11 @@ instance MonadConc m => Functor (Concurrently m) where
fmap f (Concurrently a) = Concurrently $ f <$> a
-- fmap id a = a
prop_functor_id :: Ord a => CST t a -> Bool
prop_functor_id :: Ord a => C a -> Property
prop_functor_id ca = ca `eq` (fmap id ca)
-- fmap f . fmap g = fmap (f . g)
prop_functor_comp :: Ord c => CST t a -> Fun a b -> Fun b c -> Bool
prop_functor_comp :: Ord c => C a -> Fun a b -> Fun b c -> Property
prop_functor_comp ca (apply -> f) (apply -> g) = (g . f <$> ca) `eq` (g <$> (f <$> ca))
--------------------------------------------------------------------------------
@ -62,26 +59,26 @@ instance MonadConc m => Applicative (Concurrently m) where
Concurrently fs <*> Concurrently as = Concurrently $ (\(f, a) -> f a) <$> concurrently fs as
-- pure id <*> a = a
prop_applicative_id :: Ord a => CST t a -> Bool
prop_applicative_id :: Ord a => C a -> Property
prop_applicative_id ca = ca `eq` (pure id <*> ca)
-- pure f <*> pure x = pure (f x)
prop_applicative_homo :: Ord b => a -> Fun a b -> Bool
prop_applicative_homo :: Ord b => a -> Fun a b -> Property
prop_applicative_homo a (apply -> f) = (pure $ f a) `eq` (pure f <*> pure a)
-- u <*> pure y = pure ($ y) <*> u
prop_applicative_inter :: Ord b => CST t (Fun a b) -> a -> Bool
prop_applicative_inter :: Ord b => C (Fun a b) -> a -> Property
prop_applicative_inter u y = (u' <*> pure y) `eq` (pure ($ y) <*> u') where
u' = apply <$> u
-- u <*> (v <*> w) = pure (.) <*> u <*> v <*> w
prop_applicative_comp :: Ord c => CST t (Fun b c) -> CST t (Fun a b) -> CST t a -> Bool
prop_applicative_comp :: Ord c => C (Fun b c) -> C (Fun a b) -> C a -> Property
prop_applicative_comp u v w = (u' <*> (v' <*> w)) `eq` (pure (.) <*> u' <*> v' <*> w) where
u' = apply <$> u
v' = apply <$> v
-- f <$> x = pure f <*> x
prop_applicative_fmap :: Ord b => Fun a b -> CST t a -> Bool
prop_applicative_fmap :: Ord b => Fun a b -> C a -> Property
prop_applicative_fmap (apply -> f) a = (f <$> a) `eq` (pure f <*> a)
--------------------------------------------------------------------------------
@ -93,33 +90,33 @@ instance MonadConc m => Monad (Concurrently m) where
Concurrently a >>= f = Concurrently $ a >>= runConcurrently . f
-- return >=> f = f
prop_monad_left_id :: Ord b => Fun a (CST t b) -> a -> Bool
prop_monad_left_id :: Ord b => Fun a (C b) -> a -> Property
prop_monad_left_id (apply -> f) = f `eqf` (return >=> f)
-- f >=> return = f
prop_monad_right_id :: Ord b => Fun a (CST t b) -> a -> Bool
prop_monad_right_id :: Ord b => Fun a (C b) -> a -> Property
prop_monad_right_id (apply -> f) = f `eqf` (f >=> return)
-- (f >=> g) >=> h = f >=> (g >=> h)
prop_monad_assoc :: Ord d => Fun a (CST t b) -> Fun b (CST t c) -> Fun c (CST t d) -> a -> Bool
prop_monad_assoc :: Ord d => Fun a (C b) -> Fun b (C c) -> Fun c (C d) -> a -> Property
prop_monad_assoc (apply -> f) (apply -> g) (apply -> h) = ((f >=> g) >=> h) `eqf` (f >=> (g >=> h))
-- f <$> a = f `liftM` a
prop_monad_fmap :: Ord b => Fun a b -> CST t a -> Bool
prop_monad_fmap :: Ord b => Fun a b -> C a -> Property
prop_monad_fmap (apply -> f) a = (f <$> a) `eq` (f `liftM` a)
-- return = pure
prop_monad_pure :: Ord a => a -> Bool
prop_monad_pure :: Ord a => a -> Property
prop_monad_pure = pure `eqf` return
-- (<*>) = ap
prop_monad_ap :: Ord b => Fun a b -> a -> Bool
prop_monad_ap :: Ord b => Fun a b -> a -> Property
prop_monad_ap (apply -> f) a = (pure f <*> pure a) `eq` (return f `ap` return a)
-- (<*>) = ap, side-effect-testing version
prop_monad_ap' :: forall a b. Ord b => Fun a b -> Fun a b -> a -> Bool
prop_monad_ap' :: forall a b. Ord b => Fun a b -> Fun a b -> a -> Property
prop_monad_ap' (apply -> f) (apply -> g) a = go (<*>) `eq'` go ap where
go :: (CST t (a -> b) -> CST t a -> CST t b) -> ConcST t b
go :: (C (a -> b) -> C a -> C b) -> ConcIO b
go combine = do
var <- newEmptyMVar
let cf = do { res <- tryTakeMVar var; pure $ if isJust res then f else g }
@ -136,15 +133,15 @@ instance MonadConc m => Alternative (Concurrently m) where
Concurrently $ either id id <$> race as bs
-- x <|> (y <|> z) = (x <|> y) <|> z
prop_alternative_assoc :: Ord a => CST t a -> CST t a -> CST t a -> Bool
prop_alternative_assoc :: Ord a => C a -> C a -> C a -> Property
prop_alternative_assoc x y z = (x <|> (y <|> z)) `eq` ((x <|> y) <|> z)
-- x = x <|> empty
prop_alternative_right_id :: Ord a => CST t a -> Bool
prop_alternative_right_id :: Ord a => C a -> Property
prop_alternative_right_id x = x `eq` (x <|> empty)
-- x = empty <|> x
prop_alternative_left_id :: Ord a => CST t a -> Bool
prop_alternative_left_id :: Ord a => C a -> Property
prop_alternative_left_id x = x `eq` (empty <|> x)
--------------------------------------------------------------------------------
@ -160,17 +157,17 @@ instance Monoid Integer where
mempty = 0
mappend = (+)
eq :: Ord a => CST t a -> CST t a -> Bool
eq :: Ord a => C a -> C a -> Property
eq left right = runConcurrently left `eq'` runConcurrently right
eq' :: forall t a. Ord a => ConcST t a -> ConcST t a -> Bool
eq' left right = runST' $ do
leftTraces <- sctBound defaultMemType defaultBounds left
rightTraces <- sctBound defaultMemType defaultBounds right
eq' :: forall t a. Ord a => ConcIO a -> ConcIO a -> Property
eq' left right = monadicIO $ do
leftTraces <- run $ sctBound defaultMemType defaultBounds left
rightTraces <- run $ sctBound defaultMemType defaultBounds right
let toSet = fromList . map fst
pure (toSet leftTraces == toSet rightTraces)
assert (toSet leftTraces == toSet rightTraces)
eqf :: Ord b => (a -> CST t b) -> (a -> CST t b) -> a -> Bool
eqf :: Ord b => (a -> C b) -> (a -> C b) -> a -> Property
eqf left right a = left a `eq` right a
--------------------------------------------------------------------------------

12
dejafu-tests/Examples/ClassLaws/Impredicative.hs
View File

@ -1,12 +0,0 @@
{-# LANGUAGE ImpredicativeTypes #-}
-- | This is a separate module because of the need for
-- ImpredicativeTypes, which breaks things elsewhere in the main
-- SearchParty module.
module Examples.ClassLaws.Impredicative where
import Control.Monad.ST (ST, runST)
import Unsafe.Coerce (unsafeCoerce)
runST' :: ST t Bool -> Bool
runST' = unsafeCoerce runST

1
dejafu-tests/dejafu-tests.cabal
View File

@ -32,7 +32,6 @@ executable dejafu-tests
, Examples
, Examples.AutoUpdate
, Examples.ClassLaws
, Examples.ClassLaws.Impredicative
, Examples.Logger
, Examples.Philosophers
, Examples.SearchParty

26
dejafu/CHANGELOG.markdown
View File

@ -14,6 +14,32 @@ This project is versioned according to the [Package Versioning Policy](https://p
- **Git tag** [dejafu-1.0.0.0][]
- **Hackage** https://hackage.haskell.org/package/dejafu-1.0.0.0
### Test.DejaFu
- All testing functions now require a `MonadConc`, `MonadRef`, and `MonadIO` constraint:
It is no longer possible to test things in `ST`.
- The `autocheckIO`, `dejafuIO`, `dejafusIO`, `autocheckWayIO`, `dejafuWayIO`, `dejafusWayIO`,
`dejafuDiscardIO`, `runTestM`, and `runTestWayM` functions are now gone.
### Test.DejaFu.Conc
- The `ConcST` type alias is gone.
- The `MonadBase IO ConcIO` instance is gone.
- The `MonadIO ConcIO` instance is replaces with a more general `MonadIO n => MonadIO (ConcT r n)`
instance.
- The `runConcurrent` function now has a `MonadConc` constraint.
### Test.DejaFu.SCT
- All testing functions now require a `MonadConc` constraint:
It is no longer possible to test things in `ST`.
### Miscellaneous
- The minimum supported version of concurrency is now 1.3.0.0.

183
dejafu/Test/DejaFu.hs
View File

@ -1,5 +1,4 @@
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
-- |
-- Module : Test.DejaFu
@ -7,7 +6,7 @@
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : experimental
-- Portability : RankNTypes
-- Portability : MultiParamTypeClasses
--
-- Deterministic testing for concurrent computations.
--
@ -87,9 +86,6 @@ module Test.DejaFu
autocheck
, dejafu
, dejafus
, autocheckIO
, dejafuIO
, dejafusIO
-- * Testing with different settings
@ -101,17 +97,13 @@ module Test.DejaFu
, swarmy
, autocheckWay
, autocheckWayIO
, dejafuWay
, dejafuWayIO
, dejafusWay
, dejafusWayIO
, Discard(..)
, defaultDiscarder
, dejafuDiscard
, dejafuDiscardIO
-- ** Memory Models
@ -216,8 +208,6 @@ module Test.DejaFu
, Failure(..)
, runTest
, runTestWay
, runTestM
, runTestWayM
-- * Predicates
@ -286,14 +276,15 @@ module Test.DejaFu
, module Test.DejaFu.Refinement
) where
import Control.Arrow (first)
import Control.DeepSeq (NFData(..))
import Control.Monad (unless, when)
import Control.Monad.Ref (MonadRef)
import Control.Monad.ST (runST)
import Data.Function (on)
import Data.List (intercalate, intersperse, minimumBy)
import Data.Ord (comparing)
import Control.Arrow (first)
import Control.DeepSeq (NFData(..))
import Control.Monad (unless, when)
import Control.Monad.Conc.Class (MonadConc)
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.Ref (MonadRef)
import Data.Function (on)
import Data.List (intercalate, intersperse, minimumBy)
import Data.Ord (comparing)
import Test.DejaFu.Common
import Test.DejaFu.Conc
@ -308,15 +299,11 @@ import Test.DejaFu.SCT
-- | Automatically test a computation. In particular, look for
-- deadlocks, uncaught exceptions, and multiple return values.
--
-- This uses the 'Conc' monad for testing, which is an instance of
-- 'MonadConc'. If you need to test something which also uses
-- 'MonadIO', use 'autocheckIO'.
--
-- @since 0.1.0.0
autocheck :: (Eq a, Show a)
=> (forall t. ConcST t a)
-- @since 1.0.0.0
autocheck :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a)
=> ConcT r n a
-- ^ The computation to test
-> IO Bool
-> n Bool
autocheck = autocheckWay defaultWay defaultMemType
-- | Variant of 'autocheck' which takes a way to run the program and a
@ -333,31 +320,18 @@ autocheck = autocheckWay defaultWay defaultMemType
-- __Warning:__ Using largers bounds will almost certainly
-- significantly increase the time taken to test!
--
-- @since 0.6.0.0
autocheckWay :: (Eq a, Show a)
-- @since 1.0.0.0
autocheckWay :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a)
=> Way
-- ^ How to run the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> (forall t. ConcST t a)
-> ConcT r n a
-- ^ The computation to test
-> IO Bool
-> n Bool
autocheckWay way memtype conc =
dejafusWay way memtype conc autocheckCases
-- | Variant of 'autocheck' for computations which do 'IO'.
--
-- @since 0.2.0.0
autocheckIO :: (Eq a, Show a) => ConcIO a -> IO Bool
autocheckIO = autocheckWayIO defaultWay defaultMemType
-- | Variant of 'autocheckWay' for computations which do 'IO'.
--
-- @since 0.6.0.0
autocheckWayIO :: (Eq a, Show a) => Way -> MemType -> ConcIO a -> IO Bool
autocheckWayIO way memtype concio =
dejafusWayIO way memtype concio autocheckCases
-- | Predicates for the various autocheck functions.
autocheckCases :: Eq a => [(String, Predicate a)]
autocheckCases =
@ -369,114 +343,79 @@ autocheckCases =
-- | Check a predicate and print the result to stdout, return 'True'
-- if it passes.
--
-- @since 0.1.0.0
dejafu :: Show a
=> (forall t. ConcST t a)
-- @since 1.0.0.0
dejafu :: (MonadConc n, MonadIO n, MonadRef r n, Show a)
=> ConcT r n a
-- ^ The computation to test
-> (String, Predicate a)
-- ^ The predicate (with a name) to check
-> IO Bool
-> n Bool
dejafu = dejafuWay defaultWay defaultMemType
-- | Variant of 'dejafu' which takes a way to run the program and a
-- memory model.
--
-- @since 0.6.0.0
dejafuWay :: Show a
-- @since 1.0.0.0
dejafuWay :: (MonadConc n, MonadIO n, MonadRef r n, Show a)
=> Way
-- ^ How to run the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> (forall t. ConcST t a)
-> ConcT r n a
-- ^ The computation to test
-> (String, Predicate a)
-- ^ The predicate (with a name) to check
-> IO Bool
-> n Bool
dejafuWay = dejafuDiscard (const Nothing)
-- | Variant of 'dejafuWay' which can selectively discard results.
--
-- @since 0.7.1.0
dejafuDiscard :: Show a
-- @since 1.0.0.0
dejafuDiscard :: (MonadConc n, MonadIO n, MonadRef r n, Show a)
=> (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.
-> (forall t. ConcST t a)
-> ConcT r n a
-- ^ The computation to test
-> (String, Predicate a)
-- ^ The predicate (with a name) to check
-> IO Bool
-> n Bool
dejafuDiscard discard way memtype conc (name, test) = do
let traces = runST (runSCTDiscard discard way memtype conc)
doTest name (test traces)
traces <- runSCTDiscard discard way memtype conc
liftIO $ doTest name (test traces)
-- | Variant of 'dejafu' which takes a collection of predicates to
-- test, returning 'True' if all pass.
--
-- @since 0.1.0.0
dejafus :: Show a
=> (forall t. ConcST t a)
-- @since 1.0.0.0
dejafus :: (MonadConc n, MonadIO n, MonadRef r n, Show a)
=> ConcT r n a
-- ^ The computation to test
-> [(String, Predicate a)]
-- ^ The list of predicates (with names) to check
-> IO Bool
-> n Bool
dejafus = dejafusWay defaultWay defaultMemType
-- | Variant of 'dejafus' which takes a way to run the program and a
-- memory model.
--
-- @since 0.6.0.0
dejafusWay :: Show a
-- @since 1.0.0.0
dejafusWay :: (MonadConc n, MonadIO n, MonadRef r n, Show a)
=> Way
-- ^ How to run the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> (forall t. ConcST t a)
-> ConcT r n a
-- ^ The computation to test
-> [(String, Predicate a)]
-- ^ The list of predicates (with names) to check
-> IO Bool
-> n Bool
dejafusWay way memtype conc tests = do
let traces = runST (runSCT way memtype conc)
results <- mapM (\(name, test) -> doTest name $ test traces) tests
pure (and results)
-- | Variant of 'dejafu' for computations which do 'IO'.
--
-- @since 0.2.0.0
dejafuIO :: Show a => ConcIO a -> (String, Predicate a) -> IO Bool
dejafuIO = dejafuWayIO defaultWay defaultMemType
-- | Variant of 'dejafuWay' for computations which do 'IO'.
--
-- @since 0.6.0.0
dejafuWayIO :: Show a => Way -> MemType -> ConcIO a -> (String, Predicate a) -> IO Bool
dejafuWayIO = dejafuDiscardIO (const Nothing)
-- | Variant of 'dejafuDiscard' for computations which do 'IO'.
--
-- @since 0.7.1.0
dejafuDiscardIO :: Show a => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcIO a -> (String, Predicate a) -> IO Bool
dejafuDiscardIO discard way memtype concio (name, test) = do
traces <- runSCTDiscard discard way memtype concio
doTest name (test traces)
-- | Variant of 'dejafus' for computations which do 'IO'.
--
-- @since 0.2.0.0
dejafusIO :: Show a => ConcIO a -> [(String, Predicate a)] -> IO Bool
dejafusIO = dejafusWayIO defaultWay defaultMemType
-- | Variant of 'dejafusWay' for computations which do 'IO'.
--
-- @since 0.6.0.0
dejafusWayIO :: Show a => Way -> MemType -> ConcIO a -> [(String, Predicate a)] -> IO Bool
dejafusWayIO way memtype concio tests = do
traces <- runSCT way memtype concio
results <- mapM (\(name, test) -> doTest name $ test traces) tests
traces <- runSCT way memtype conc
results <- mapM (\(name, test) -> liftIO . doTest name $ test traces) tests
pure (and results)
@ -523,46 +462,30 @@ instance Foldable Result where
-- | Run a predicate over all executions within the default schedule
-- bounds.
--
-- @since 0.1.0.0
runTest ::
Predicate a
-- @since 1.0.0.0
runTest :: (MonadConc n, MonadRef r n)
=> Predicate a
-- ^ The predicate to check
-> (forall t. ConcST t a)
-> ConcT r n a
-- ^ The computation to test
-> Result a
runTest test conc =
runST (runTestM test conc)
-> n (Result a)
runTest = runTestWay defaultWay defaultMemType
-- | Variant of 'runTest' which takes a way to run the program and a
-- memory model.
--
-- @since 0.6.0.0
runTestWay
:: Way
-- @since 1.0.0.0
runTestWay :: (MonadConc n, MonadRef r n)
=> Way
-- ^ How to run the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> Predicate a
-- ^ The predicate to check
-> (forall t. ConcST t a)
-> ConcT r n a
-- ^ The computation to test
-> Result a
-> n (Result a)
runTestWay way memtype predicate conc =
runST (runTestWayM way memtype predicate conc)
-- | Monad-polymorphic variant of 'runTest'.
--
-- @since 0.4.0.0
runTestM :: MonadRef r n
=> Predicate a -> ConcT r n a -> n (Result a)
runTestM = runTestWayM defaultWay defaultMemType
-- | Monad-polymorphic variant of 'runTest''.
--
-- @since 0.6.0.0
runTestWayM :: MonadRef r n
=> Way -> MemType -> Predicate a -> ConcT r n a -> n (Result a)
runTestWayM way memtype predicate conc =
predicate <$> runSCT way memtype conc

26
dejafu/Test/DejaFu/Conc.hs
View File

@ -2,9 +2,7 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}
-- |
-- Module : Test.DejaFu.Conc
@ -12,7 +10,7 @@
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : experimental
-- Portability : CPP, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, RankNTypes, TypeFamilies, TypeSynonymInstances
-- Portability : CPP, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, TypeFamilies
--
-- Deterministic traced execution of concurrent computations.
--
@ -22,7 +20,6 @@
module Test.DejaFu.Conc
( -- * The @ConcT@ monad transformer
ConcT
, ConcST
, ConcIO
-- * Executing computations
@ -48,16 +45,13 @@ module Test.DejaFu.Conc
) where
import Control.Exception (MaskingState(..))
import qualified Control.Monad.Base as Ba
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.ST (ST)
import Control.Monad.Trans.Class (MonadTrans(..))
import qualified Data.Foldable as F
import Data.IORef (IORef)
import Data.STRef (STRef)
import Test.DejaFu.Schedule
import qualified Control.Monad.Conc.Class as C
@ -79,12 +73,6 @@ instance Fail.MonadFail (ConcT r n) where
fail = C . fail
#endif
-- | A 'MonadConc' implementation using @ST@, this should be preferred
-- if you do not need 'liftIO'.
--
-- @since 0.4.0.0
type ConcST t = ConcT (STRef t) (ST t)
-- | A 'MonadConc' implementation using @IO@.
--
-- @since 0.4.0.0
@ -96,11 +84,9 @@ toConc = C . cont
wrap :: (M n r a -> M n r a) -> ConcT r n a -> ConcT r n a
wrap f = C . f . unC
instance IO.MonadIO ConcIO where
liftIO ma = toConc (\c -> ALift (fmap c ma))
instance Ba.MonadBase IO ConcIO where
liftBase = IO.liftIO
-- | @since 1.0.0.0
instance IO.MonadIO n => IO.MonadIO (ConcT r 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)
@ -202,8 +188,8 @@ instance Monad n => C.MonadConc (ConcT r n) where
-- nonexistent thread. In either of those cases, the computation will
-- be halted.
--
-- @since 0.8.0.0
runConcurrent :: MonadRef r n
-- @since 1.0.0.0
runConcurrent :: (C.MonadConc n, MonadRef r n)
=> Scheduler s
-> MemType
-> s

57
dejafu/Test/DejaFu/SCT.hs
View File

@ -108,6 +108,7 @@ module Test.DejaFu.SCT
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
@ -207,8 +208,8 @@ swarmy = Weighted
-- | Explore possible executions of a concurrent program according to
-- the given 'Way'.
--
-- @since 0.6.0.0
runSCT :: MonadRef r n
-- @since 1.0.0.0
runSCT :: (MonadConc n, MonadRef r n)
=> Way
-- ^ How to run the concurrent program.
-> MemType
@ -220,8 +221,8 @@ runSCT = runSCTDiscard (const Nothing)
-- | Return the set of results of a concurrent program.
--
-- @since 0.6.0.0
resultsSet :: (MonadRef r n, Ord a)
-- @since 1.0.0.0
resultsSet :: (MonadConc n, MonadRef r n, Ord a)
=> Way
-- ^ How to run the concurrent program.
-> MemType
@ -249,8 +250,8 @@ instance NFData Discard where
-- | A variant of 'runSCT' which can selectively discard results.
--
-- @since 0.7.1.0
runSCTDiscard :: MonadRef r n
-- @since 1.0.0.0
runSCTDiscard :: (MonadConc n, MonadRef r n)
=> (Either Failure a -> Maybe Discard)
-- ^ Selectively discard results.
-> Way
@ -266,8 +267,8 @@ runSCTDiscard discard (Uniform g lim) memtype = sctUniformRandomDiscard di
-- | A variant of 'resultsSet' which can selectively discard results.
--
-- @since 0.7.1.0
resultsSetDiscard :: (MonadRef r n, Ord a)
-- @since 1.0.0.0
resultsSetDiscard :: (MonadConc n, MonadRef r n, Ord a)
=> (Either Failure a -> Maybe Discard)
-- ^ Selectively discard results. Traces are always discarded.
-> Way
@ -286,8 +287,8 @@ resultsSetDiscard discard way memtype conc =
-- Demanding the result of this will force it to normal form, which
-- may be more efficient in some situations.
--
-- @since 0.6.0.0
runSCT' :: (MonadRef r n, NFData a)
-- @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' = runSCTDiscard' (const Nothing)
@ -296,8 +297,8 @@ runSCT' = runSCTDiscard' (const Nothing)
-- Demanding the result of this will force it to normal form, which
-- may be more efficient in some situations.
--
-- @since 0.6.0.0
resultsSet' :: (MonadRef r n, Ord a, NFData a)
-- @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' = resultsSetDiscard' (const Nothing)
@ -306,8 +307,8 @@ resultsSet' = resultsSetDiscard' (const Nothing)
-- Demanding the result of this will force it to normal form, which
-- may be more efficient in some situations.
--
-- @since 0.7.1.0
runSCTDiscard' :: (MonadRef r n, NFData a)
-- @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' discard way memtype conc = do
res <- runSCTDiscard discard way memtype conc
@ -318,8 +319,8 @@ runSCTDiscard' discard way memtype conc = do
-- Demanding the result of this will force it to normal form, which
-- may be more efficient in some situations.
--
-- @since 0.7.1.0
resultsSetDiscard' :: (MonadRef r n, Ord a, NFData a)
-- @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' discard way memtype conc = do
res <- resultsSetDiscard discard way memtype conc
@ -477,8 +478,8 @@ lBacktrack = backtrackAt (\_ _ -> False)
-- do some redundant work as the introduction of a bound can make
-- previously non-interfering events interfere with each other.
--
-- @since 0.5.0.0
sctBound :: MonadRef r n
-- @since 1.0.0.0
sctBound :: (MonadConc n, MonadRef r n)
=> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> Bounds
@ -490,8 +491,8 @@ sctBound = sctBoundDiscard (const Nothing)
-- | A variant of 'sctBound' which can selectively discard results.
--
-- @since 0.7.1.0
sctBoundDiscard :: MonadRef r n
-- @since 1.0.0.0
sctBoundDiscard :: (MonadConc n, MonadRef r n)
=> (Either Failure a -> Maybe Discard)
-- ^ Selectively discard results.
-> MemType
@ -533,8 +534,8 @@ sctBoundDiscard discard memtype cb conc = go initialState where
--
-- This is not guaranteed to find all distinct results.
--
-- @since 0.7.0.0
sctUniformRandom :: (MonadRef r n, RandomGen g)
-- @since 1.0.0.0
sctUniformRandom :: (MonadConc n, MonadRef r n, RandomGen g)
=> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> g
@ -549,8 +550,8 @@ sctUniformRandom = sctUniformRandomDiscard (const Nothing)
-- | A variant of 'sctUniformRandom' which can selectively discard
-- results.
--
-- @since 0.7.1.0
sctUniformRandomDiscard :: (MonadRef r n, RandomGen g)
-- @since 1.0.0.0
sctUniformRandomDiscard :: (MonadConc n, MonadRef r n, RandomGen g)
=> (Either Failure a -> Maybe Discard)
-- ^ Selectively discard results.
-> MemType
@ -578,8 +579,8 @@ sctUniformRandomDiscard discard memtype g0 lim0 conc = go g0 (max 0 lim0) where
--
-- This is not guaranteed to find all distinct results.
--
-- @since 0.7.0.0
sctWeightedRandom :: (MonadRef r n, RandomGen g)
-- @since 1.0.0.0
sctWeightedRandom :: (MonadConc n, MonadRef r n, RandomGen g)
=> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> g
@ -596,8 +597,8 @@ sctWeightedRandom = sctWeightedRandomDiscard (const Nothing)
-- | A variant of 'sctWeightedRandom' which can selectively discard
-- results.
--
-- @since 0.7.1.0
sctWeightedRandomDiscard :: (MonadRef r n, RandomGen g)
-- @since 1.0.0.0
sctWeightedRandomDiscard :: (MonadConc n, MonadRef r n, RandomGen g)
=> (Either Failure a -> Maybe Discard)
-- ^ Selectively discard results.
-> MemType

3
dejafu/Test/DejaFu/STM.hs
View File

@ -1,6 +1,5 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
-- |
@ -9,7 +8,7 @@
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : experimental
-- Portability : CPP, GeneralizedNewtypeDeriving, RankNTypes, TypeFamilies
-- Portability : CPP, GeneralizedNewtypeDeriving, TypeFamilies
--
-- A 'MonadSTM' implementation, which can be run on top of 'IO' or
-- 'ST'.

1
dejafu/dejafu.cabal
View File

@ -67,7 +67,6 @@ library
, random >=1.0 && <1.2
, ref-fd >=0.4 && <0.5
, transformers >=0.4 && <0.6
, transformers-base >=0.4 && <0.5
-- hs-source-dirs:
default-language: Haskell2010
ghc-options: -Wall

5
hunit-dejafu/CHANGELOG.markdown
View File

@ -14,6 +14,11 @@ This project is versioned according to the [Package Versioning Policy](https://p
- **Git tag** [hunit-dejafu-1.0.0.0][]
- **Hackage** https://hackage.haskell.org/package/hunit-dejafu-1.0.0.0
### Test.HUnit.DejaFu
- The `ConcST` functions have been removed and replaced by the `ConcIO` functions.
- The `Testable` and `Assertable` instances for `ConcST t ()` are gone.
### Miscellaneous
- The minimum supported version of dejafu is now 1.0.0.0.

175
hunit-dejafu/Test/HUnit/DejaFu.hs
View File

@ -1,39 +1,28 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeSynonymInstances #-}
#if MIN_TOOL_VERSION_ghc(8,0,0)
-- Impredicative polymorphism checks got stronger in GHC 8, breaking
-- the use of 'unsafeCoerce' below.
{-# LANGUAGE ImpredicativeTypes #-}
#endif
-- |
-- Module : Test.HUnit.DejaFu
-- Copyright : (c) 2017 Michael Walker
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : stable
-- Portability : CPP, FlexibleContexts, FlexibleInstances, ImpredicativeTypes, LambdaCase, RankNTypes, ScopedTypeVariables, TypeSynonymInstances
-- Portability : FlexibleContexts, FlexibleInstances, LambdaCase, TypeSynonymInstances
--
-- This module allows using Deja Fu predicates with HUnit to test the
-- behaviour of concurrent systems.
module Test.HUnit.DejaFu
( -- * Unit testing
-- | This is supported by the 'Assertable' and 'Testable'
-- instances for 'ConcST' and 'ConcIO'. These instances try all
-- executions, reporting as failures the cases which throw an
-- 'HUnitFailure' exception.
-- | This is supported by the 'Assertable' and 'Testable' instances
-- for 'ConcIO'. These instances tries all executions,
-- reporting as failures the cases which throw an 'HUnitFailure'
-- exception.
--
-- @instance Testable (ConcST t ())@
-- @instance Assertable (ConcST t ())@
-- @instance Testable (ConcIO ())@
-- @instance Assertable (ConcIO ())@
-- @instance Testable (ConcIO ())@
-- @instance Assertable (ConcIO ())@
--
-- These instances use 'defaultWay' and 'defaultMemType'.
@ -48,17 +37,6 @@ module Test.HUnit.DejaFu
, testDejafuDiscard
-- ** @IO@
, testAutoIO
, testDejafuIO
, testDejafusIO
, testAutoWayIO
, testDejafuWayIO
, testDejafusWayIO
, testDejafuDiscardIO
-- ** Re-exports
, Way
, defaultWay
@ -89,7 +67,6 @@ module Test.HUnit.DejaFu
) where
import Control.Monad.Catch (try)
import Control.Monad.ST (runST)
import qualified Data.Foldable as F
import Data.List (intercalate, intersperse)
import Test.DejaFu hiding (Testable(..))
@ -100,44 +77,17 @@ import Test.HUnit (Assertable(..), Test(..), Testable(..),
assertFailure, assertString)
import Test.HUnit.Lang (HUnitFailure(..))
-- Can't put the necessary forall in the @Assertable Conc.ConcST t@
-- instance :(
import Unsafe.Coerce (unsafeCoerce)
runSCTst :: (Either Failure a -> Maybe Discard) -> Way -> MemType -> (forall t. Conc.ConcST t a) -> [(Either Failure a, Conc.Trace)]
runSCTst discard way memtype conc = runST (SCT.runSCTDiscard discard way memtype conc)
runSCTio :: (Either Failure a -> Maybe Discard) -> Way -> MemType -> Conc.ConcIO a -> IO [(Either Failure a, Conc.Trace)]
runSCTio = SCT.runSCTDiscard
--------------------------------------------------------------------------------
-- HUnit-style unit testing
-- | @since 0.3.0.0
instance Testable (Conc.ConcST t ()) where
test conc = TestCase (assert conc)
-- | @since 0.3.0.0
instance Testable (Conc.ConcIO ()) where
test conc = TestCase (assert conc)
-- | @since 0.3.0.0
instance Assertable (Conc.ConcST t ()) where
assert conc = do
let traces = runSCTst' conc'
assertString . showErr $ assertableP traces
where
conc' :: Conc.ConcST t (Either HUnitFailure ())
conc' = try conc
runSCTst' :: Conc.ConcST t (Either HUnitFailure ()) -> [(Either Failure (Either HUnitFailure ()), Conc.Trace)]
runSCTst' = unsafeCoerce $ runSCTst (const Nothing) defaultWay defaultMemType
-- | @since 0.3.0.0
instance Assertable (Conc.ConcIO ()) where
assert conc = do
traces <- runSCTio (const Nothing) defaultWay defaultMemType (try conc)
traces <- SCT.runSCTDiscard (const Nothing) defaultWay defaultMemType (try conc)
assertString . showErr $ assertableP traces
assertableP :: Predicate (Either HUnitFailure ())
@ -152,13 +102,9 @@ assertableP = alwaysTrue $ \case
-- | Automatically test a computation. In particular, look for
-- deadlocks, uncaught exceptions, and multiple return values.
--
-- This uses the 'Conc' monad for testing, which is an instance of
-- 'MonadConc'. If you need to test something which also uses
-- 'MonadIO', use 'testAutoIO'.
--
-- @since 0.2.0.0
-- @since 1.0.0.0
testAuto :: (Eq a, Show a)
=> (forall t. Conc.ConcST t a)
=> Conc.ConcIO a
-- ^ The computation to test
-> Test
testAuto = testAutoWay defaultWay defaultMemType
@ -166,32 +112,18 @@ testAuto = testAutoWay defaultWay defaultMemType
-- | Variant of 'testAuto' which tests a computation under a given
-- execution way and memory model.
--
-- @since 0.5.0.0
-- @since 1.0.0.0
testAutoWay :: (Eq a, Show a)
=> Way
-- ^ How to execute the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> (forall t. Conc.ConcST t a)
-> Conc.ConcIO a
-- ^ The computation to test
-> Test
testAutoWay way memtype conc =
testDejafusWay way memtype conc autocheckCases
-- | Variant of 'testAuto' for computations which do 'IO'.
--
-- @since 0.2.0.0
testAutoIO :: (Eq a, Show a) => Conc.ConcIO a -> Test
testAutoIO = testAutoWayIO defaultWay defaultMemType
-- | Variant of 'testAutoWay' for computations which do 'IO'.
--
-- @since 0.5.0.0
testAutoWayIO :: (Eq a, Show a)
=> Way -> MemType -> Conc.ConcIO a -> Test
testAutoWayIO way memtype concio =
testDejafusWayIO way memtype concio autocheckCases
-- | Predicates for the various autocheck functions.
autocheckCases :: Eq a => [(String, Predicate a)]
autocheckCases =
@ -202,9 +134,9 @@ autocheckCases =
-- | Check that a predicate holds.
--
-- @since 0.2.0.0
-- @since 1.0.0.0
testDejafu :: Show a
=> (forall t. Conc.ConcST t a)
=> Conc.ConcIO a
-- ^ The computation to test
-> String
-- ^ The name of the test.
@ -216,13 +148,13 @@ testDejafu = testDejafuWay defaultWay defaultMemType
-- | Variant of 'testDejafu' which takes a way to execute the program
-- and a memory model.
--
-- @since 0.5.0.0
-- @since 1.0.0.0
testDejafuWay :: Show a
=> Way
-- ^ How to execute the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> (forall t. Conc.ConcST t a)
-> Conc.ConcIO a
-- ^ The computation to test
-> String
-- ^ The name of the test.
@ -233,7 +165,7 @@ testDejafuWay = testDejafuDiscard (const Nothing)
-- | Variant of 'testDejafuWay' which can selectively discard results.
--
-- @since 0.7.0.0
-- @since 1.0.0.0
testDejafuDiscard :: Show a
=> (Either Failure a -> Maybe Discard)
-- ^ Selectively discard results.
@ -241,7 +173,7 @@ testDejafuDiscard :: Show a
-- ^ How to execute the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> (forall t. Conc.ConcST t a)
-> Conc.ConcIO a
-- ^ The computation to test
-> String
-- ^ The name of the test.
@ -249,15 +181,15 @@ testDejafuDiscard :: Show a
-- ^ The predicate to check
-> Test
testDejafuDiscard discard way memtype conc name test =
testst discard way memtype conc [(name, test)]
testconc discard way memtype conc [(name, test)]
-- | Variant of 'testDejafu' which takes a collection of predicates to
-- test. This will share work between the predicates, rather than
-- running the concurrent computation many times for each predicate.
--
-- @since 0.2.0.0
-- @since 1.0.0.0
testDejafus :: Show a
=> (forall t. Conc.ConcST t a)
=> Conc.ConcIO a
-- ^ The computation to test
-> [(String, Predicate a)]
-- ^ The list of predicates (with names) to check
@ -267,51 +199,18 @@ testDejafus = testDejafusWay defaultWay defaultMemType
-- | Variant of 'testDejafus' which takes a way to execute the program
-- and a memory model.
--
-- @since 0.5.0.0
-- @since 1.0.0.0
testDejafusWay :: Show a
=> Way
-- ^ How to execute the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> (forall t. Conc.ConcST t a)
-> Conc.ConcIO a
-- ^ The computation to test
-> [(String, Predicate a)]
-- ^ The list of predicates (with names) to check
-> Test
testDejafusWay = testst (const Nothing)
-- | Variant of 'testDejafu' for computations which do 'IO'.
--
-- @since 0.2.0.0
testDejafuIO :: Show a => Conc.ConcIO a -> String -> Predicate a -> Test
testDejafuIO = testDejafuWayIO defaultWay defaultMemType
-- | Variant of 'testDejafuWay' for computations which do 'IO'.
--
-- @since 0.5.0.0
testDejafuWayIO :: Show a
=> Way -> MemType -> Conc.ConcIO a -> String -> Predicate a -> Test
testDejafuWayIO = testDejafuDiscardIO (const Nothing)
-- | Variant of 'testDejafuDiscard' for computations which do 'IO'.
--
-- @since 0.7.0.0
testDejafuDiscardIO :: Show a => (Either Failure a -> Maybe Discard) -> Way -> MemType -> Conc.ConcIO a -> String -> Predicate a -> Test
testDejafuDiscardIO discard way memtype concio name test =
testio discard way memtype concio [(name, test)]
-- | Variant of 'testDejafus' for computations which do 'IO'.
--
-- @since 0.2.0.0
testDejafusIO :: Show a => Conc.ConcIO a -> [(String, Predicate a)] -> Test
testDejafusIO = testDejafusWayIO defaultWay defaultMemType
-- | Variant of 'dejafusWay' for computations which do 'IO'.
--
-- @since 0.5.0.0
testDejafusWayIO :: Show a
=> Way -> MemType -> Conc.ConcIO a -> [(String, Predicate a)] -> Test
testDejafusWayIO = testio (const Nothing)
testDejafusWay = testconc (const Nothing)
-------------------------------------------------------------------------------
@ -351,33 +250,15 @@ testPropertyFor = testprop
--------------------------------------------------------------------------------
-- HUnit integration
-- | Produce a HUnit 'Test' from a Deja Fu test.
testst :: Show a
=> (Either Failure a -> Maybe Discard)
-> Way
-> MemType
-> (forall t. Conc.ConcST t a)
-> [(String, Predicate a)]
-> Test
testst discard way memtype conc tests = case map toTest tests of
[t] -> t
ts -> TestList ts
where
toTest (name, p) = TestLabel name . TestCase $
assertString . showErr $ p traces
traces = runSCTst discard way memtype conc
-- | Produce a HUnit 'Test' from an IO-using Deja Fu test.
testio :: Show a
-- | Produce a HUnit 'Test' from a Deja Fu unit test.
testconc :: Show a
=> (Either Failure a -> Maybe Discard)
-> Way
-> MemType
-> Conc.ConcIO a
-> [(String, Predicate a)]
-> Test
testio discard way memtype concio tests = case map toTest tests of
testconc discard way memtype concio tests = case map toTest tests of
[t] -> t
ts -> TestList ts
@ -387,7 +268,7 @@ testio discard way memtype concio tests = case map toTest tests of
-- really unsafe) here, as 'test' doesn't allow side-effects
-- (eg, constructing an 'MVar' to share the traces after one
-- test computed them).
traces <- runSCTio discard way memtype concio
traces <- SCT.runSCTDiscard discard way memtype concio
assertString . showErr $ p traces
-- | Produce a HUnit 'Test' from a Deja Fu refinement property test.

5
tasty-dejafu/CHANGELOG.markdown
View File

@ -14,6 +14,11 @@ This project is versioned according to the [Package Versioning Policy](https://p
- **Git tag** [tasty-dejafu-1.0.0.0][]
- **Hackage** https://hackage.haskell.org/package/tasty-dejafu-1.0.0.0
### Test.Tasty.DejaFu
- The `ConcST` functions have been removed and replaced by the `ConcIO` functions.
- The `IsTest` instance for `ConcST t (Maybe String)` is gone.
### Miscellaneous
- The minimum supported version of dejafu is now 1.0.0.0.

182
tasty-dejafu/Test/Tasty/DejaFu.hs
View File

@ -1,36 +1,27 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeSynonymInstances #-}
#if MIN_TOOL_VERSION_ghc(8,0,0)
-- Impredicative polymorphism checks got stronger in GHC 8, breaking
-- the use of 'unsafeCoerce' below.
{-# LANGUAGE ImpredicativeTypes #-}
#endif
-- |
-- Module : Test.Tasty.DejaFu
-- Copyright : (c) 2016 Michael Walker
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : stable
-- Portability : CPP, FlexibleContexts, FlexibleInstances, GADTs, ImpredicativeTypes, LambdaCase, RankNTypes, TypeSynonymInstances
-- Portability : FlexibleContexts, FlexibleInstances, GADTs, LambdaCase, TypeSynonymInstances
--
-- This module allows using Deja Fu predicates with Tasty to test the
-- behaviour of concurrent systems.
module Test.Tasty.DejaFu
( -- * Unit testing
-- | This is supported by the 'IsTest' instances for 'ConcST' and
-- 'ConcIO'. These instances try all executions, reporting as
-- failures the cases which return a 'Just' string.
-- | This is supported by an 'IsTest' instance for 'ConcIO'. This
-- instance tries all executions, reporting as failures the cases
-- which return a 'Just' string.
--
-- @instance Typeable t => IsTest (ConcST t (Maybe String))@
-- @instance IsTest (ConcIO (Maybe String))@
-- @instance IsTest (ConcIO (Maybe String))@
-- @instance IsOption Bounds@
-- @instance IsOption MemType@
@ -45,17 +36,6 @@ module Test.Tasty.DejaFu
, testDejafuDiscard
-- ** @IO@
, testAutoIO
, testDejafuIO
, testDejafusIO
, testAutoWayIO
, testDejafuWayIO
, testDejafusWayIO
, testDejafuDiscardIO
-- ** Re-exports
, Way
, defaultWay
@ -85,7 +65,6 @@ module Test.Tasty.DejaFu
, R.equivalentTo, (R.===)
) where
import Control.Monad.ST (runST)
import Data.Char (toUpper)
import qualified Data.Foldable as F
import Data.List (intercalate, intersperse)
@ -103,31 +82,9 @@ import Test.Tasty.Options (IsOption(..), OptionDescription(..),
import Test.Tasty.Providers (IsTest(..), singleTest, testFailed,
testPassed)
-- Can't put the necessary forall in the @IsTest ConcST t@
-- instance :(
import Unsafe.Coerce (unsafeCoerce)
runSCTst :: (Either Failure a -> Maybe Discard) -> Way -> MemType -> (forall t. Conc.ConcST t a) -> [(Either Failure a, Conc.Trace)]
runSCTst discard way memtype conc = runST (SCT.runSCTDiscard discard way memtype conc)
runSCTio :: (Either Failure a -> Maybe Discard) -> Way -> MemType -> Conc.ConcIO a -> IO [(Either Failure a, Conc.Trace)]
runSCTio = SCT.runSCTDiscard
--------------------------------------------------------------------------------
-- Tasty-style unit testing
-- | @since 0.3.0.0
instance Typeable t => IsTest (Conc.ConcST t (Maybe String)) where
testOptions = Tagged concOptions
run options conc callback = do
let memtype = lookupOption options :: MemType
let way = lookupOption options :: Way
let runSCTst' :: Conc.ConcST t (Maybe String) -> [(Either Failure (Maybe String), Conc.Trace)]
runSCTst' = unsafeCoerce $ runSCTst (const Nothing) way memtype
let traces = runSCTst' conc
run options (ConcTest traces assertableP) callback
-- | @since 0.3.0.0
instance IsTest (Conc.ConcIO (Maybe String)) where
testOptions = Tagged concOptions
@ -135,8 +92,8 @@ instance IsTest (Conc.ConcIO (Maybe String)) where
run options conc callback = do
let memtype = lookupOption options
let way = lookupOption options
let traces = runSCTio (const Nothing) way memtype conc
run options (ConcIOTest traces assertableP) callback
let traces = SCT.runSCTDiscard (const Nothing) way memtype conc
run options (ConcTest traces assertableP) callback
concOptions :: [OptionDescription]
concOptions =
@ -177,13 +134,9 @@ instance IsOption Way where
-- | Automatically test a computation. In particular, look for
-- deadlocks, uncaught exceptions, and multiple return values.
--
-- This uses the 'Conc' monad for testing, which is an instance of
-- 'MonadConc'. If you need to test something which also uses
-- 'MonadIO', use 'testAutoIO'.
--
-- @since 0.2.0.0
-- @since 1.0.0.0
testAuto :: (Eq a, Show a)
=> (forall t. Conc.ConcST t a)
=> Conc.ConcIO a
-- ^ The computation to test
-> TestTree
testAuto = testAutoWay defaultWay defaultMemType
@ -191,31 +144,17 @@ testAuto = testAutoWay defaultWay defaultMemType
-- | Variant of 'testAuto' which tests a computation under a given
-- execution way and memory model.
--
-- @since 0.5.0.0
-- @since 1.0.0.0
testAutoWay :: (Eq a, Show a)
=> Way
-- ^ How to execute the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> (forall t. Conc.ConcST t a)
-> Conc.ConcIO a
-- ^ The computation to test
-> TestTree
testAutoWay way memtype conc = testDejafusWay way memtype conc autocheckCases
-- | Variant of 'testAuto' for computations which do 'IO'.
--
-- @since 0.2.0.0
testAutoIO :: (Eq a, Show a) => Conc.ConcIO a -> TestTree
testAutoIO = testAutoWayIO defaultWay defaultMemType
-- | Variant of 'testAutoWay' for computations which do 'IO'.
--
-- @since 0.5.0.0
testAutoWayIO :: (Eq a, Show a)
=> Way -> MemType -> Conc.ConcIO a -> TestTree
testAutoWayIO way memtype concio =
testDejafusWayIO way memtype concio autocheckCases
-- | Predicates for the various autocheck functions.
autocheckCases :: Eq a => [(TestName, Predicate a)]
autocheckCases =
@ -226,9 +165,9 @@ autocheckCases =
-- | Check that a predicate holds.
--
-- @since 0.2.0.0
-- @since 1.0.0.0
testDejafu :: Show a
=> (forall t. Conc.ConcST t a)
=> Conc.ConcIO a
-- ^ The computation to test
-> TestName
-- ^ The name of the test.
@ -240,13 +179,13 @@ testDejafu = testDejafuWay defaultWay defaultMemType
-- | Variant of 'testDejafu' which takes a way to execute the program
-- and a memory model.
--
-- @since 0.5.0.0
-- @since 1.0.0.0
testDejafuWay :: Show a
=> Way
-- ^ How to execute the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> (forall t. Conc.ConcST t a)
-> Conc.ConcIO a
-- ^ The computation to test
-> TestName
-- ^ The name of the test.
@ -257,7 +196,7 @@ testDejafuWay = testDejafuDiscard (const Nothing)
-- | Variant of 'testDejafuWay' which can selectively discard results.
--
-- @since 0.7.0.0
-- @since 1.0.0.0
testDejafuDiscard :: Show a
=> (Either Failure a -> Maybe Discard)
-- ^ Selectively discard results.
@ -265,7 +204,7 @@ testDejafuDiscard :: Show a
-- ^ How to execute the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> (forall t. Conc.ConcST t a)
-> Conc.ConcIO a
-- ^ The computation to test
-> String
-- ^ The name of the test.
@ -273,15 +212,15 @@ testDejafuDiscard :: Show a
-- ^ The predicate to check
-> TestTree
testDejafuDiscard discard way memtype conc name test =
testst discard way memtype conc [(name, test)]
testconc discard way memtype conc [(name, test)]
-- | Variant of 'testDejafu' which takes a collection of predicates to
-- test. This will share work between the predicates, rather than
-- running the concurrent computation many times for each predicate.
--
-- @since 0.2.0.0
-- @since 1.0.0.0
testDejafus :: Show a
=> (forall t. Conc.ConcST t a)
=> Conc.ConcIO a
-- ^ The computation to test
-> [(TestName, Predicate a)]
-- ^ The list of predicates (with names) to check
@ -291,51 +230,18 @@ testDejafus = testDejafusWay defaultWay defaultMemType
-- | Variant of 'testDejafus' which takes a way to execute the program
-- and a memory model.
--
-- @since 0.5.0.0
-- @since 1.0.0.0
testDejafusWay :: Show a
=> Way
-- ^ How to execute the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> (forall t. Conc.ConcST t a)
-> Conc.ConcIO a
-- ^ The computation to test
-> [(TestName, Predicate a)]
-- ^ The list of predicates (with names) to check
-> TestTree
testDejafusWay = testst (const Nothing)
-- | Variant of 'testDejafu' for computations which do 'IO'.
--
-- @since 0.2.0.0
testDejafuIO :: Show a => Conc.ConcIO a -> TestName -> Predicate a -> TestTree
testDejafuIO = testDejafuWayIO defaultWay defaultMemType
-- | Variant of 'testDejafuWay' for computations which do 'IO'.
--
-- @since 0.5.0.0
testDejafuWayIO :: Show a
=> Way -> MemType -> Conc.ConcIO a -> TestName -> Predicate a -> TestTree
testDejafuWayIO = testDejafuDiscardIO (const Nothing)
-- | Variant of 'testDejafuDiscard' for computations which do 'IO'.
--
-- @since 0.7.0.0
testDejafuDiscardIO :: Show a => (Either Failure a -> Maybe Discard) -> Way -> MemType -> Conc.ConcIO a -> String -> Predicate a -> TestTree
testDejafuDiscardIO discard way memtype concio name test =
testio discard way memtype concio [(name, test)]
-- | Variant of 'testDejafus' for computations which do 'IO'.
--
-- @since 0.2.0.0
testDejafusIO :: Show a => Conc.ConcIO a -> [(TestName, Predicate a)] -> TestTree
testDejafusIO = testDejafusWayIO defaultWay defaultMemType
-- | Variant of 'dejafusWay' for computations which do 'IO'.
--
-- @since 0.5.0.0
testDejafusWayIO :: Show a
=> Way -> MemType -> Conc.ConcIO a -> [(TestName, Predicate a)] -> TestTree
testDejafusWayIO = testio (const Nothing)
testDejafusWay = testconc (const Nothing)
-------------------------------------------------------------------------------
@ -376,11 +282,7 @@ testPropertyFor = testprop
-- Tasty integration
data ConcTest where
ConcTest :: Show a => [(Either Failure a, Conc.Trace)] -> Predicate a -> ConcTest
deriving Typeable
data ConcIOTest where
ConcIOTest :: Show a => IO [(Either Failure a, Conc.Trace)] -> Predicate a -> ConcIOTest
ConcTest :: Show a => IO [(Either Failure a, Conc.Trace)] -> Predicate a -> ConcTest
deriving Typeable
data PropTest where
@ -390,14 +292,7 @@ data PropTest where
instance IsTest ConcTest where
testOptions = pure []
run _ (ConcTest traces p) _ =
let err = showErr $ p traces
in pure (if null err then testPassed "" else testFailed err)
instance IsTest ConcIOTest where
testOptions = pure []
run _ (ConcIOTest iotraces p) _ = do
run _ (ConcTest iotraces p) _ = do
traces <- iotraces
let err = showErr $ p traces
pure (if null err then testPassed "" else testFailed err)
@ -417,41 +312,24 @@ instance IsTest PropTest where
]
Nothing -> testPassed ""
-- | Produce a Tasty 'TestTree' from a Deja Fu test.
testst :: Show a
=> (Either Failure a -> Maybe Discard)
-> Way
-> MemType
-> (forall t. Conc.ConcST t a)
-> [(TestName, Predicate a)]
-> TestTree
testst discard way memtype conc tests = case map toTest tests of
[t] -> t
ts -> testGroup "Deja Fu Tests" ts
where
toTest (name, p) = singleTest name $ ConcTest traces p
traces = runSCTst discard way memtype conc
-- | Produce a Tasty 'Test' from an IO-using Deja Fu test.
testio :: Show a
-- | Produce a Tasty 'Test' from a Deja Fu unit test.
testconc :: Show a
=> (Either Failure a -> Maybe Discard)
-> Way
-> MemType
-> Conc.ConcIO a
-> [(TestName, Predicate a)]
-> TestTree
testio discard way memtype concio tests = case map toTest tests of
testconc discard way memtype concio tests = case map toTest tests of
[t] -> t
ts -> testGroup "Deja Fu Tests" ts
where
toTest (name, p) = singleTest name $ ConcIOTest traces p
toTest (name, p) = singleTest name $ ConcTest traces p
-- As with HUnit, constructing a test is side-effect free, so
-- sharing of traces can't happen here.
traces = runSCTio discard way memtype concio
traces = SCT.runSCTDiscard discard way memtype concio
-- | Produce a Tasty 'TestTree' from a Deja Fu refinement property test.
testprop :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p))