mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-18 11:01:50 +03:00
Merge branch 'discard'
This commit is contained in:
Michael Walker
commit
50712c54cd
@ -7,6 +7,7 @@ import qualified Cases.MultiThreaded as M
|
||||
import qualified Cases.Refinement as R
|
||||
import qualified Cases.Litmus as L
|
||||
import qualified Cases.Async as A
|
||||
import qualified Cases.Discard as D
|
||||
|
||||
-- | Run all the test cases.
|
||||
testCases :: [Test]
|
||||
@ -16,4 +17,5 @@ testCases = map (uncurry testGroup)
|
||||
, ("Refinement", R.tests)
|
||||
, ("Litmus", L.tests)
|
||||
, ("Async", A.tests)
|
||||
, ("Discard", D.tests)
|
||||
]
|
||||
|
||||
25
dejafu-tests/Cases/Discard.hs
Normal file
25
dejafu-tests/Cases/Discard.hs
Normal file
@ -0,0 +1,25 @@
|
||||
module Cases.Discard where
|
||||
|
||||
import Control.Concurrent.Classy
|
||||
import Test.DejaFu (gives')
|
||||
import Test.Framework (Test)
|
||||
import Test.Framework.Providers.HUnit (hUnitTestToTests)
|
||||
import Test.HUnit (test)
|
||||
import Test.HUnit.DejaFu (Discard(..), defaultMemType, defaultWay, testDejafuDiscard)
|
||||
|
||||
tests :: [Test]
|
||||
tests = hUnitTestToTests $ test
|
||||
[ check "all results" [1, 2, 3] (const Nothing)
|
||||
, check "no results" [] (const $ Just DiscardResultAndTrace)
|
||||
, check "some results" [1, 2] (\x -> if x == Right 3 then Just DiscardResultAndTrace else Nothing)
|
||||
]
|
||||
where
|
||||
check name xs f = testDejafuDiscard f defaultWay defaultMemType nondet name (gives' xs)
|
||||
|
||||
nondet :: MonadConc m => m Int
|
||||
nondet = do
|
||||
mvar <- newEmptyMVar
|
||||
fork $ putMVar mvar 1
|
||||
fork $ putMVar mvar 2
|
||||
fork $ putMVar mvar 3
|
||||
readMVar mvar
|
||||
@ -25,6 +25,7 @@ executable dejafu-tests
|
||||
, Cases.MultiThreaded
|
||||
, Cases.Refinement
|
||||
, Cases.Litmus
|
||||
, Cases.Discard
|
||||
|
||||
, Examples
|
||||
, Examples.AutoUpdate
|
||||
|
||||
@ -6,6 +6,35 @@ All notable changes to this project will be documented in this file.
|
||||
This project is versioned according to the [Package Versioning Policy](https://pvp.haskell.org), the
|
||||
*de facto* standard Haskell versioning scheme.
|
||||
|
||||
unreleased
|
||||
----------
|
||||
|
||||
### Test.DejaFu
|
||||
|
||||
- Exposed the new SCT discard functions through `dejafuDiscard` and `dejafuDiscardIO`.
|
||||
|
||||
There are no `dejafusDiscard` and `dejafusDiscardIO` functions because this would probably be
|
||||
confusing, as the traces are shared.
|
||||
|
||||
- The `Discard` type and `defaultDiscard` function are also exposed.
|
||||
|
||||
### Test.DejaFu.Defaults
|
||||
|
||||
- Added a new `defaultDiscarder` function, which discards nothing.
|
||||
|
||||
### Test.DejaFu.SCT
|
||||
|
||||
- Added new SCT functions to selectively discard results or traces, which can be a significant
|
||||
memory saving if you know what sorts of results you are interested in:
|
||||
- New type: `Discard`.
|
||||
- New functions: `runSCTDiscard`, `resultsSetDiscard`, `sctBoundDiscard`,
|
||||
`sctUniformRandomDiscard`, and `sctWeightedRandomDiscard`.
|
||||
- `resultsSet` and `resultsSet'` now discard traces as they are produced, rather than all at the
|
||||
end, greatly improving performance when traces are large.
|
||||
|
||||
|
||||
---------------------------------------------------------------------------------------------------
|
||||
|
||||
|
||||
0.7.0.2 [2017-06-12] (git tag: [dejafu-0.7.0.2][])
|
||||
-------
|
||||
|
||||
@ -107,6 +107,12 @@ module Test.DejaFu
|
||||
, dejafusWay
|
||||
, dejafusWayIO
|
||||
|
||||
, Discard(..)
|
||||
, defaultDiscarder
|
||||
|
||||
, dejafuDiscard
|
||||
, dejafuDiscardIO
|
||||
|
||||
-- ** Memory Models
|
||||
|
||||
-- | Threads running under modern multicore processors do not behave
|
||||
@ -378,7 +384,26 @@ dejafuWay :: Show a
|
||||
-> (String, Predicate a)
|
||||
-- ^ The predicate (with a name) to check
|
||||
-> IO Bool
|
||||
dejafuWay way memtype conc test = dejafusWay way memtype conc [test]
|
||||
dejafuWay = dejafuDiscard (const Nothing)
|
||||
|
||||
-- | Variant of 'dejafuWay' which can selectively discard results.
|
||||
--
|
||||
-- @since unreleased
|
||||
dejafuDiscard :: 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)
|
||||
-- ^ The computation to test
|
||||
-> (String, Predicate a)
|
||||
-- ^ The predicate (with a name) to check
|
||||
-> IO Bool
|
||||
dejafuDiscard discard way memtype conc (name, test) = do
|
||||
let traces = runST (runSCTDiscard discard way memtype conc)
|
||||
doTest name (test traces)
|
||||
|
||||
-- | Variant of 'dejafu' which takes a collection of predicates to
|
||||
-- test, returning 'True' if all pass.
|
||||
@ -421,8 +446,15 @@ dejafuIO = dejafuWayIO defaultWay defaultMemType
|
||||
--
|
||||
-- @since 0.6.0.0
|
||||
dejafuWayIO :: Show a => Way -> MemType -> ConcIO a -> (String, Predicate a) -> IO Bool
|
||||
dejafuWayIO way memtype concio test =
|
||||
dejafusWayIO way memtype concio [test]
|
||||
dejafuWayIO = dejafuDiscardIO (const Nothing)
|
||||
|
||||
-- | Variant of 'dejafuDiscard' for computations which do 'IO'.
|
||||
--
|
||||
-- @since unreleased
|
||||
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'.
|
||||
--
|
||||
|
||||
@ -742,6 +742,7 @@ instance NFData Decision where
|
||||
--
|
||||
-- @since 0.5.0.0
|
||||
showTrace :: Trace -> String
|
||||
showTrace [] = "<trace discarded>"
|
||||
showTrace trc = intercalate "\n" $ concatMap go trc : strkey where
|
||||
go (_,_,CommitCRef _ _) = "C-"
|
||||
go (Start (ThreadId _ i),_,_) = "S" ++ show i ++ "-"
|
||||
|
||||
@ -19,6 +19,12 @@ import Test.DejaFu.SCT
|
||||
defaultWay :: Way
|
||||
defaultWay = systematically defaultBounds
|
||||
|
||||
-- | Do not discard any results.
|
||||
--
|
||||
-- @since unreleased
|
||||
defaultDiscarder :: Either Failure a -> Maybe Discard
|
||||
defaultDiscarder = const Nothing
|
||||
|
||||
-- | The default memory model: @TotalStoreOrder@
|
||||
--
|
||||
-- @since 0.2.0.0
|
||||
|
||||
@ -18,9 +18,18 @@ module Test.DejaFu.SCT
|
||||
, uniformly
|
||||
, swarmy
|
||||
, runSCT
|
||||
, runSCT'
|
||||
, resultsSet
|
||||
|
||||
-- ** Discarding variants
|
||||
, Discard(..)
|
||||
, runSCTDiscard
|
||||
, resultsSetDiscard
|
||||
|
||||
-- ** Strict variants
|
||||
, runSCT'
|
||||
, resultsSet'
|
||||
, runSCTDiscard'
|
||||
, resultsSetDiscard'
|
||||
|
||||
-- * Bounded Partial-order Reduction
|
||||
|
||||
@ -51,6 +60,7 @@ module Test.DejaFu.SCT
|
||||
, Bounds(..)
|
||||
, noBounds
|
||||
, sctBound
|
||||
, sctBoundDiscard
|
||||
|
||||
-- ** Pre-emption Bounding
|
||||
|
||||
@ -91,8 +101,11 @@ module Test.DejaFu.SCT
|
||||
|
||||
, sctUniformRandom
|
||||
, sctWeightedRandom
|
||||
, sctUniformRandomDiscard
|
||||
, sctWeightedRandomDiscard
|
||||
) where
|
||||
|
||||
import Control.Applicative ((<|>))
|
||||
import Control.DeepSeq (NFData(..))
|
||||
import Control.Monad.Ref (MonadRef)
|
||||
import Data.List (foldl')
|
||||
@ -201,21 +214,7 @@ runSCT :: MonadRef r n
|
||||
-> ConcT r n a
|
||||
-- ^ The computation to run many times.
|
||||
-> n [(Either Failure a, Trace)]
|
||||
runSCT (Systematic cb) memtype = sctBound memtype cb
|
||||
runSCT (Weighted g lim use) memtype = sctWeightedRandom memtype g lim use
|
||||
runSCT (Uniform g lim) memtype = sctUniformRandom memtype g lim
|
||||
|
||||
-- | A strict variant of 'runSCT'.
|
||||
--
|
||||
-- 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)
|
||||
=> Way -> MemType -> ConcT r n a -> n [(Either Failure a, Trace)]
|
||||
runSCT' way memtype conc = do
|
||||
res <- runSCT way memtype conc
|
||||
rnf res `seq` pure res
|
||||
runSCT = runSCTDiscard (const Nothing)
|
||||
|
||||
-- | Return the set of results of a concurrent program.
|
||||
--
|
||||
@ -228,8 +227,67 @@ resultsSet :: (MonadRef r n, Ord a)
|
||||
-> ConcT r n a
|
||||
-- ^ The computation to run many times.
|
||||
-> n (Set (Either Failure a))
|
||||
resultsSet way memtype conc =
|
||||
S.fromList . map fst <$> runSCT way memtype conc
|
||||
resultsSet = resultsSetDiscard (const Nothing)
|
||||
|
||||
-- | An @Either Failure a -> Maybe Discard@ value can be used to
|
||||
-- selectively discard results.
|
||||
--
|
||||
-- @since unreleased
|
||||
data Discard
|
||||
= DiscardTrace
|
||||
-- ^ Discard the trace but keep the result. The result will appear
|
||||
-- to have an empty trace.
|
||||
| DiscardResultAndTrace
|
||||
-- ^ Discard the result and the trace. It will simply not be
|
||||
-- reported as a possible behaviour of the program.
|
||||
deriving (Eq, Show, Read, Ord, Enum, Bounded)
|
||||
|
||||
instance NFData Discard where
|
||||
rnf d = d `seq` ()
|
||||
|
||||
-- | A variant of 'runSCT' which can selectively discard results.
|
||||
--
|
||||
-- @since unreleased
|
||||
runSCTDiscard :: MonadRef r n
|
||||
=> (Either Failure a -> Maybe Discard)
|
||||
-- ^ Selectively discard results.
|
||||
-> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-> ConcT r n a
|
||||
-- ^ The computation to run many times.
|
||||
-> n [(Either Failure a, Trace)]
|
||||
runSCTDiscard discard (Systematic cb) memtype = sctBoundDiscard discard memtype cb
|
||||
runSCTDiscard discard (Weighted g lim use) memtype = sctWeightedRandomDiscard discard memtype g lim use
|
||||
runSCTDiscard discard (Uniform g lim) memtype = sctUniformRandomDiscard discard memtype g lim
|
||||
|
||||
-- | A variant of 'resultsSet' which can selectively discard results.
|
||||
--
|
||||
-- @since unreleased
|
||||
resultsSetDiscard :: (MonadRef r n, Ord a)
|
||||
=> (Either Failure a -> Maybe Discard)
|
||||
-- ^ Selectively discard results. Traces are always discarded.
|
||||
-> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-> ConcT r n a
|
||||
-- ^ The computation to run many times.
|
||||
-> n (Set (Either Failure a))
|
||||
resultsSetDiscard discard way memtype conc =
|
||||
let discard' efa = discard efa <|> Just DiscardTrace
|
||||
in S.fromList . map fst <$> runSCTDiscard discard' way memtype conc
|
||||
|
||||
-- | A strict variant of 'runSCT'.
|
||||
--
|
||||
-- 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)
|
||||
=> Way -> MemType -> ConcT r n a -> n [(Either Failure a, Trace)]
|
||||
runSCT' = runSCTDiscard' (const Nothing)
|
||||
|
||||
-- | A strict variant of 'resultsSet'.
|
||||
--
|
||||
@ -239,8 +297,30 @@ resultsSet way memtype conc =
|
||||
-- @since 0.6.0.0
|
||||
resultsSet' :: (MonadRef r n, Ord a, NFData a)
|
||||
=> Way -> MemType -> ConcT r n a -> n (Set (Either Failure a))
|
||||
resultsSet' way memtype conc = do
|
||||
res <- resultsSet' way memtype conc
|
||||
resultsSet' = resultsSetDiscard' (const Nothing)
|
||||
|
||||
-- | A strict variant of 'runSCTDiscard'.
|
||||
--
|
||||
-- Demanding the result of this will force it to normal form, which
|
||||
-- may be more efficient in some situations.
|
||||
--
|
||||
-- @since unreleased
|
||||
runSCTDiscard' :: (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
|
||||
rnf res `seq` pure res
|
||||
|
||||
-- | A strict variant of 'resultsSetDiscard'.
|
||||
--
|
||||
-- Demanding the result of this will force it to normal form, which
|
||||
-- may be more efficient in some situations.
|
||||
--
|
||||
-- @since unreleased
|
||||
resultsSetDiscard' :: (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
|
||||
rnf res `seq` pure res
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
@ -394,7 +474,22 @@ sctBound :: MonadRef r n
|
||||
-> ConcT r n a
|
||||
-- ^ The computation to run many times
|
||||
-> n [(Either Failure a, Trace)]
|
||||
sctBound memtype cb conc = go initialState where
|
||||
sctBound = sctBoundDiscard (const Nothing)
|
||||
|
||||
-- | A variant of 'sctBound' which can selectively discard results.
|
||||
--
|
||||
-- @since unreleased
|
||||
sctBoundDiscard :: MonadRef r n
|
||||
=> (Either Failure a -> Maybe Discard)
|
||||
-- ^ Selectively discard results.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-> Bounds
|
||||
-- ^ The combined bounds.
|
||||
-> ConcT r n a
|
||||
-- ^ The computation to run many times
|
||||
-> n [(Either Failure a, Trace)]
|
||||
sctBoundDiscard discard memtype cb conc = go initialState where
|
||||
-- Repeatedly run the computation gathering all the results and
|
||||
-- traces into a list until there are no schedules remaining to try.
|
||||
go dp = case findSchedulePrefix dp of
|
||||
@ -408,8 +503,8 @@ sctBound memtype cb conc = go initialState where
|
||||
let newDPOR = addTrace conservative trace dp
|
||||
|
||||
if schedIgnore s
|
||||
then go newDPOR
|
||||
else ((res, trace):) <$> go (addBacktracks bpoints newDPOR)
|
||||
then go newDPOR
|
||||
else checkDiscard discard res trace $ go (addBacktracks bpoints newDPOR)
|
||||
|
||||
Nothing -> pure []
|
||||
|
||||
@ -443,14 +538,32 @@ sctUniformRandom :: (MonadRef r n, RandomGen g)
|
||||
-> ConcT r n a
|
||||
-- ^ The computation to run many times.
|
||||
-> n [(Either Failure a, Trace)]
|
||||
sctUniformRandom memtype g0 lim0 conc = go g0 (max 0 lim0) where
|
||||
sctUniformRandom = sctUniformRandomDiscard (const Nothing)
|
||||
|
||||
-- | A variant of 'sctUniformRandom' which can selectively discard
|
||||
-- results.
|
||||
--
|
||||
-- @since unreleased
|
||||
sctUniformRandomDiscard :: (MonadRef r n, RandomGen g)
|
||||
=> (Either Failure a -> Maybe Discard)
|
||||
-- ^ Selectively discard results.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-> g
|
||||
-- ^ The random number generator.
|
||||
-> Int
|
||||
-- ^ The number of executions to perform.
|
||||
-> ConcT r n a
|
||||
-- ^ The computation to run many times.
|
||||
-> n [(Either Failure a, Trace)]
|
||||
sctUniformRandomDiscard discard memtype g0 lim0 conc = go g0 (max 0 lim0) where
|
||||
go _ 0 = pure []
|
||||
go g n = do
|
||||
(res, s, trace) <- runConcurrent (randSched $ \g' -> (1, g'))
|
||||
memtype
|
||||
(initialRandSchedState Nothing g)
|
||||
conc
|
||||
((res, trace):) <$> go (schedGen s) (n-1)
|
||||
checkDiscard discard res trace $ go (schedGen s) (n-1)
|
||||
|
||||
-- | SCT via weighted random scheduling.
|
||||
--
|
||||
@ -472,7 +585,27 @@ sctWeightedRandom :: (MonadRef r n, RandomGen g)
|
||||
-> ConcT r n a
|
||||
-- ^ The computation to run many times.
|
||||
-> n [(Either Failure a, Trace)]
|
||||
sctWeightedRandom memtype g0 lim0 use0 conc = go g0 (max 0 lim0) (max 1 use0) M.empty where
|
||||
sctWeightedRandom = sctWeightedRandomDiscard (const Nothing)
|
||||
|
||||
-- | A variant of 'sctWeightedRandom' which can selectively discard
|
||||
-- results.
|
||||
--
|
||||
-- @since unreleased
|
||||
sctWeightedRandomDiscard :: (MonadRef r n, RandomGen g)
|
||||
=> (Either Failure a -> Maybe Discard)
|
||||
-- ^ Selectively discard results.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-> g
|
||||
-- ^ The random number generator.
|
||||
-> Int
|
||||
-- ^ The number of executions to perform.
|
||||
-> Int
|
||||
-- ^ The number of executions to use the same set of weights for.
|
||||
-> ConcT r n a
|
||||
-- ^ The computation to run many times.
|
||||
-> n [(Either Failure a, Trace)]
|
||||
sctWeightedRandomDiscard discard memtype g0 lim0 use0 conc = go g0 (max 0 lim0) (max 1 use0) M.empty where
|
||||
go _ 0 _ _ = pure []
|
||||
go g n 0 _ = go g n (max 1 use0) M.empty
|
||||
go g n use ws = do
|
||||
@ -480,7 +613,7 @@ sctWeightedRandom memtype g0 lim0 use0 conc = go g0 (max 0 lim0) (max 1 use0) M.
|
||||
memtype
|
||||
(initialRandSchedState (Just ws) g)
|
||||
conc
|
||||
((res, trace):) <$> go (schedGen s) (n-1) (use-1) (schedWeights s)
|
||||
checkDiscard discard res trace $ go (schedGen s) (n-1) (use-1) (schedWeights s)
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
-- Utilities
|
||||
@ -542,3 +675,10 @@ trueBound _ _ = True
|
||||
-- satisfied.
|
||||
(&+&) :: BoundFunc -> BoundFunc -> BoundFunc
|
||||
(&+&) b1 b2 ts dl = b1 ts dl && b2 ts dl
|
||||
|
||||
-- | Apply the discard function.
|
||||
checkDiscard :: Functor f => (a -> Maybe Discard) -> a -> [b] -> f [(a, [b])] -> f [(a, [b])]
|
||||
checkDiscard discard res trace rest = case discard res of
|
||||
Just DiscardResultAndTrace -> rest
|
||||
Just DiscardTrace -> ((res, []):) <$> rest
|
||||
Nothing -> ((res, trace):) <$> rest
|
||||
|
||||
@ -7,6 +7,23 @@ This project is versioned according to the [Package Versioning Policy](https://p
|
||||
*de facto* standard Haskell versioning scheme.
|
||||
|
||||
|
||||
unreleased
|
||||
----------
|
||||
|
||||
### Test.HUnit.DejaFu
|
||||
|
||||
- Two new functions: `testDejafuDiscard` and `testDejafuDiscardIO`, allowing you to selectively
|
||||
discard results or traces.
|
||||
- The `Discard` type and `defaultDiscarder` function from dejafu is now re-exported.
|
||||
|
||||
### Miscellaneous
|
||||
|
||||
- Only dejafu UNRELEASED is supported.
|
||||
|
||||
|
||||
---------------------------------------------------------------------------------------------------
|
||||
|
||||
|
||||
0.6.0.0 [2017-06-07] (git tag: [hunit-dejafu-0.6.0.0][])
|
||||
-------
|
||||
|
||||
|
||||
@ -45,6 +45,8 @@ module Test.HUnit.DejaFu
|
||||
, testDejafuWay
|
||||
, testDejafusWay
|
||||
|
||||
, testDejafuDiscard
|
||||
|
||||
-- ** @IO@
|
||||
, testAutoIO
|
||||
, testDejafuIO
|
||||
@ -54,6 +56,8 @@ module Test.HUnit.DejaFu
|
||||
, testDejafuWayIO
|
||||
, testDejafusWayIO
|
||||
|
||||
, testDejafuDiscardIO
|
||||
|
||||
-- ** Re-exports
|
||||
, Way
|
||||
, defaultWay
|
||||
@ -65,6 +69,8 @@ module Test.HUnit.DejaFu
|
||||
, defaultBounds
|
||||
, MemType(..)
|
||||
, defaultMemType
|
||||
, Discard(..)
|
||||
, defaultDiscarder
|
||||
|
||||
-- * Refinement property testing
|
||||
, testProperty
|
||||
@ -96,11 +102,11 @@ import Test.HUnit.Lang (HUnitFailure(..))
|
||||
-- instance :(
|
||||
import Unsafe.Coerce (unsafeCoerce)
|
||||
|
||||
runSCTst :: Way -> MemType -> (forall t. Conc.ConcST t a) -> [(Either Failure a, Conc.Trace)]
|
||||
runSCTst way memtype conc = runST (SCT.runSCT way memtype conc)
|
||||
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 :: Way -> MemType -> Conc.ConcIO a -> IO [(Either Failure a, Conc.Trace)]
|
||||
runSCTio = SCT.runSCT
|
||||
runSCTio :: (Either Failure a -> Maybe Discard) -> Way -> MemType -> Conc.ConcIO a -> IO [(Either Failure a, Conc.Trace)]
|
||||
runSCTio = SCT.runSCTDiscard
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- HUnit-style unit testing
|
||||
@ -124,12 +130,12 @@ instance Assertable (Conc.ConcST t ()) where
|
||||
conc' = try conc
|
||||
|
||||
runSCTst' :: Conc.ConcST t (Either HUnitFailure ()) -> [(Either Failure (Either HUnitFailure ()), Conc.Trace)]
|
||||
runSCTst' = unsafeCoerce $ runSCTst defaultWay defaultMemType
|
||||
runSCTst' = unsafeCoerce $ runSCTst (const Nothing) defaultWay defaultMemType
|
||||
|
||||
-- | @since 0.3.0.0
|
||||
instance Assertable (Conc.ConcIO ()) where
|
||||
assert conc = do
|
||||
traces <- runSCTio defaultWay defaultMemType (try conc)
|
||||
traces <- runSCTio (const Nothing) defaultWay defaultMemType (try conc)
|
||||
assertString . showErr $ assertableP traces
|
||||
|
||||
assertableP :: Predicate (Either HUnitFailure ())
|
||||
@ -221,8 +227,27 @@ testDejafuWay :: Show a
|
||||
-> Predicate a
|
||||
-- ^ The predicate to check
|
||||
-> Test
|
||||
testDejafuWay way memtype conc name p =
|
||||
testDejafusWay way memtype conc [(name, p)]
|
||||
testDejafuWay = testDejafuDiscard (const Nothing)
|
||||
|
||||
-- | Variant of 'testDejafuWay' which can selectively discard results.
|
||||
--
|
||||
-- @since unreleased
|
||||
testDejafuDiscard :: Show a
|
||||
=> (Either Failure a -> Maybe Discard)
|
||||
-- ^ Selectively discard results.
|
||||
-> Way
|
||||
-- ^ How to execute the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-> (forall t. Conc.ConcST t a)
|
||||
-- ^ The computation to test
|
||||
-> String
|
||||
-- ^ The name of the test.
|
||||
-> Predicate a
|
||||
-- ^ The predicate to check
|
||||
-> Test
|
||||
testDejafuDiscard discard way memtype conc name test =
|
||||
testst 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
|
||||
@ -251,7 +276,7 @@ testDejafusWay :: Show a
|
||||
-> [(String, Predicate a)]
|
||||
-- ^ The list of predicates (with names) to check
|
||||
-> Test
|
||||
testDejafusWay = testst
|
||||
testDejafusWay = testst (const Nothing)
|
||||
|
||||
-- | Variant of 'testDejafu' for computations which do 'IO'.
|
||||
--
|
||||
@ -264,8 +289,14 @@ testDejafuIO = testDejafuWayIO defaultWay defaultMemType
|
||||
-- @since 0.5.0.0
|
||||
testDejafuWayIO :: Show a
|
||||
=> Way -> MemType -> Conc.ConcIO a -> String -> Predicate a -> Test
|
||||
testDejafuWayIO way memtype concio name p =
|
||||
testDejafusWayIO way memtype concio [(name, p)]
|
||||
testDejafuWayIO = testDejafuDiscardIO (const Nothing)
|
||||
|
||||
-- | Variant of 'testDejafuDiscard' for computations which do 'IO'.
|
||||
--
|
||||
-- @since unreleased
|
||||
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'.
|
||||
--
|
||||
@ -278,7 +309,7 @@ testDejafusIO = testDejafusWayIO defaultWay defaultMemType
|
||||
-- @since 0.5.0.0
|
||||
testDejafusWayIO :: Show a
|
||||
=> Way -> MemType -> Conc.ConcIO a -> [(String, Predicate a)] -> Test
|
||||
testDejafusWayIO = testio
|
||||
testDejafusWayIO = testio (const Nothing)
|
||||
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
@ -302,8 +333,13 @@ testProperty = testprop
|
||||
|
||||
-- | Produce a HUnit 'Test' from a Deja Fu test.
|
||||
testst :: Show a
|
||||
=> Way -> MemType -> (forall t. Conc.ConcST t a) -> [(String, Predicate a)] -> Test
|
||||
testst way memtype conc tests = case map toTest tests of
|
||||
=> (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
|
||||
|
||||
@ -311,12 +347,17 @@ testst way memtype conc tests = case map toTest tests of
|
||||
toTest (name, p) = TestLabel name . TestCase $
|
||||
assertString . showErr $ p traces
|
||||
|
||||
traces = runSCTst way memtype conc
|
||||
traces = runSCTst discard way memtype conc
|
||||
|
||||
-- | Produce a HUnit 'Test' from an IO-using Deja Fu test.
|
||||
testio :: Show a
|
||||
=> Way -> MemType -> Conc.ConcIO a -> [(String, Predicate a)] -> Test
|
||||
testio way memtype concio tests = case map toTest tests of
|
||||
=> (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
|
||||
[t] -> t
|
||||
ts -> TestList ts
|
||||
|
||||
@ -326,7 +367,7 @@ testio 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 way memtype concio
|
||||
traces <- runSCTio discard way memtype concio
|
||||
assertString . showErr $ p traces
|
||||
|
||||
-- | Produce a HUnit 'Test' from a Deja Fu refinement property test.
|
||||
|
||||
@ -7,6 +7,23 @@ This project is versioned according to the [Package Versioning Policy](https://p
|
||||
*de facto* standard Haskell versioning scheme.
|
||||
|
||||
|
||||
unreleased
|
||||
----------
|
||||
|
||||
### Test.Tasty.DejaFu
|
||||
|
||||
- Two new functions: `testDejafuDiscard` and `testDejafuDiscardIO`, allowing you to selectively
|
||||
discard results or traces.
|
||||
- The `Discard` type and `defaultDiscarder` function from dejafu is now re-exported.
|
||||
|
||||
### Miscellaneous
|
||||
|
||||
- Only dejafu UNRELEASED is supported.
|
||||
|
||||
|
||||
---------------------------------------------------------------------------------------------------
|
||||
|
||||
|
||||
0.6.0.0 [2017-04-08] (git tag: [tasty-dejafu-0.6.0.0][])
|
||||
-------
|
||||
|
||||
|
||||
@ -42,6 +42,8 @@ module Test.Tasty.DejaFu
|
||||
, testDejafuWay
|
||||
, testDejafusWay
|
||||
|
||||
, testDejafuDiscard
|
||||
|
||||
-- ** @IO@
|
||||
, testAutoIO
|
||||
, testDejafuIO
|
||||
@ -51,6 +53,8 @@ module Test.Tasty.DejaFu
|
||||
, testDejafuWayIO
|
||||
, testDejafusWayIO
|
||||
|
||||
, testDejafuDiscardIO
|
||||
|
||||
-- ** Re-exports
|
||||
, Way
|
||||
, defaultWay
|
||||
@ -62,6 +66,8 @@ module Test.Tasty.DejaFu
|
||||
, defaultBounds
|
||||
, MemType(..)
|
||||
, defaultMemType
|
||||
, Discard(..)
|
||||
, defaultDiscarder
|
||||
|
||||
-- * Refinement property testing
|
||||
, testProperty
|
||||
@ -99,11 +105,11 @@ import Test.Tasty.Providers (IsTest(..), singleTest, testFailed,
|
||||
-- instance :(
|
||||
import Unsafe.Coerce (unsafeCoerce)
|
||||
|
||||
runSCTst :: Way -> MemType -> (forall t. Conc.ConcST t a) -> [(Either Failure a, Conc.Trace)]
|
||||
runSCTst way memtype conc = runST (SCT.runSCT way memtype conc)
|
||||
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 :: Way -> MemType -> Conc.ConcIO a -> IO [(Either Failure a, Conc.Trace)]
|
||||
runSCTio = SCT.runSCT
|
||||
runSCTio :: (Either Failure a -> Maybe Discard) -> Way -> MemType -> Conc.ConcIO a -> IO [(Either Failure a, Conc.Trace)]
|
||||
runSCTio = SCT.runSCTDiscard
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Tasty-style unit testing
|
||||
@ -116,7 +122,7 @@ instance Typeable t => IsTest (Conc.ConcST t (Maybe String)) where
|
||||
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 way memtype
|
||||
runSCTst' = unsafeCoerce $ runSCTst (const Nothing) way memtype
|
||||
let traces = runSCTst' conc
|
||||
run options (ConcTest traces assertableP) callback
|
||||
|
||||
@ -127,7 +133,7 @@ instance IsTest (Conc.ConcIO (Maybe String)) where
|
||||
run options conc callback = do
|
||||
let memtype = lookupOption options
|
||||
let way = lookupOption options
|
||||
let traces = runSCTio way memtype conc
|
||||
let traces = runSCTio (const Nothing) way memtype conc
|
||||
run options (ConcIOTest traces assertableP) callback
|
||||
|
||||
concOptions :: [OptionDescription]
|
||||
@ -245,8 +251,27 @@ testDejafuWay :: Show a
|
||||
-> Predicate a
|
||||
-- ^ The predicate to check
|
||||
-> TestTree
|
||||
testDejafuWay way memtype conc name p =
|
||||
testDejafusWay way memtype conc [(name, p)]
|
||||
testDejafuWay = testDejafuDiscard (const Nothing)
|
||||
|
||||
-- | Variant of 'testDejafuWay' which can selectively discard results.
|
||||
--
|
||||
-- @since unreleased
|
||||
testDejafuDiscard :: Show a
|
||||
=> (Either Failure a -> Maybe Discard)
|
||||
-- ^ Selectively discard results.
|
||||
-> Way
|
||||
-- ^ How to execute the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-> (forall t. Conc.ConcST t a)
|
||||
-- ^ The computation to test
|
||||
-> String
|
||||
-- ^ The name of the test.
|
||||
-> Predicate a
|
||||
-- ^ The predicate to check
|
||||
-> TestTree
|
||||
testDejafuDiscard discard way memtype conc name test =
|
||||
testst 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
|
||||
@ -275,7 +300,7 @@ testDejafusWay :: Show a
|
||||
-> [(TestName, Predicate a)]
|
||||
-- ^ The list of predicates (with names) to check
|
||||
-> TestTree
|
||||
testDejafusWay = testst
|
||||
testDejafusWay = testst (const Nothing)
|
||||
|
||||
-- | Variant of 'testDejafu' for computations which do 'IO'.
|
||||
--
|
||||
@ -288,8 +313,14 @@ testDejafuIO = testDejafuWayIO defaultWay defaultMemType
|
||||
-- @since 0.5.0.0
|
||||
testDejafuWayIO :: Show a
|
||||
=> Way -> MemType -> Conc.ConcIO a -> TestName -> Predicate a -> TestTree
|
||||
testDejafuWayIO way memtype concio name p =
|
||||
testDejafusWayIO way memtype concio [(name, p)]
|
||||
testDejafuWayIO = testDejafuDiscardIO (const Nothing)
|
||||
|
||||
-- | Variant of 'testDejafuDiscard' for computations which do 'IO'.
|
||||
--
|
||||
-- @since unreleased
|
||||
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'.
|
||||
--
|
||||
@ -302,7 +333,7 @@ testDejafusIO = testDejafusWayIO defaultWay defaultMemType
|
||||
-- @since 0.5.0.0
|
||||
testDejafusWayIO :: Show a
|
||||
=> Way -> MemType -> Conc.ConcIO a -> [(TestName, Predicate a)] -> TestTree
|
||||
testDejafusWayIO = testio
|
||||
testDejafusWayIO = testio (const Nothing)
|
||||
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
@ -368,20 +399,30 @@ instance IsTest PropTest where
|
||||
|
||||
-- | Produce a Tasty 'TestTree' from a Deja Fu test.
|
||||
testst :: Show a
|
||||
=> Way -> MemType -> (forall t. Conc.ConcST t a) -> [(TestName, Predicate a)] -> TestTree
|
||||
testst way memtype conc tests = case map toTest tests of
|
||||
=> (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 way memtype conc
|
||||
traces = runSCTst discard way memtype conc
|
||||
|
||||
-- | Produce a Tasty 'Test' from an IO-using Deja Fu test.
|
||||
testio :: Show a
|
||||
=> Way -> MemType -> Conc.ConcIO a -> [(TestName, Predicate a)] -> TestTree
|
||||
testio way memtype concio tests = case map toTest tests of
|
||||
=> (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
|
||||
[t] -> t
|
||||
ts -> testGroup "Deja Fu Tests" ts
|
||||
|
||||
@ -390,7 +431,7 @@ testio way memtype concio tests = case map toTest tests of
|
||||
|
||||
-- As with HUnit, constructing a test is side-effect free, so
|
||||
-- sharing of traces can't happen here.
|
||||
traces = runSCTio way memtype concio
|
||||
traces = runSCTio 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))
|
||||
|
||||
Loading…
Reference in New Issue
Block a user