barrucadu/dejafu
1
1
Fork 0
mirror of https://github.com/barrucadu/dejafu.git synced 2024-12-29 00:22:38 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #238 from barrucadu/221-opaque-settings

Browse Source 
(wip) Add an SCT "Settings" type
This commit is contained in:
Michael Walker 2018-03-06 17:47:54 +00:00 committed by GitHub
commit 7759890981
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
26 changed files with 1180 additions and 636 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.hlint.yaml
View File

@ -30,4 +30,5 @@
- ignore: {name: Reduce duplication, within: Unit.Properties}
- ignore: {name: Reduce duplication, within: Integration.Litmus}
- ignore: {name: Reduce duplication, within: Integration.MultiThreaded}
- ignore: {name: Reduce duplication, within: Integration.SCT}
- ignore: {name: Reduce duplication, within: Integration.SingleThreaded}

6
README.markdown
View File

@ -46,9 +46,9 @@ There are a few different packages under the Déjà Fu umbrella:
| | Version | Summary |
| - | ------- | ------- |
| [concurrency][h:conc] | 1.4.0.1 | Typeclasses, functions, and data types for concurrency and STM. |
| [dejafu][h:dejafu] | 1.1.0.2 | Systematic testing for Haskell concurrency. |
| [hunit-dejafu][h:hunit] | 1.0.1.2 | Deja Fu support for the HUnit test framework. |
| [tasty-dejafu][h:tasty] | 1.0.1.1 | Deja Fu support for the Tasty test framework. |
| [dejafu][h:dejafu] | 1.2.0.0 | Systematic testing for Haskell concurrency. |
| [hunit-dejafu][h:hunit] | 1.1.0.0 | Deja Fu support for the HUnit test framework. |
| [tasty-dejafu][h:tasty] | 1.1.0.0 | Deja Fu support for the Tasty test framework. |
Each package has its own README and CHANGELOG in its subdirectory.

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

@ -26,7 +26,6 @@ library
, Integration.MultiThreaded
, Integration.Refinement
, Integration.Litmus
, Integration.Discard
, Integration.Regressions
, Integration.SCT
, Integration.Names

22
dejafu-tests/lib/Common.hs
View File

@ -2,6 +2,7 @@
module Common (module Common, module Test.Tasty.DejaFu, T.TestTree, T.expectFail) where
import Control.Arrow (second)
import Control.Exception (ArithException, ArrayException,
SomeException, displayException)
import Control.Monad (void)
@ -38,12 +39,12 @@ instance IsTest T.TestTree where
toTestList t = [t]
instance IsTest T where
toTestList (T n c p) = toTestList (TEST n c p defaultWays True)
toTestList (W n c p w) = toTestList (TEST n c p [w] True)
toTestList (B n c p b) = toTestList (TEST n c p (defaultWaysFor b) True)
toTestList (TEST n c p w subc) = toTestList . testGroup n $
let mk (name, way) = testDejafuWay way defaultMemType name p c
in map mk w ++ [H.testProperty "dependency func." (prop_dep_fun c) | subc]
toTestList (T n c p) = toTestList (TEST n c p (map (second toSettings) defaultWays) True)
toTestList (W n c p w) = toTestList (TEST n c p [second toSettings w] True)
toTestList (B n c p b) = toTestList (TEST n c p (map (second toSettings) (defaultWaysFor b)) True)
toTestList (TEST n c p ss subc) = toTestList . testGroup n $
let mk (name, settings) = testDejafuWithSettings settings name p c
in map mk ss ++ [H.testProperty "dependency func." (prop_dep_fun c) | subc]
instance IsTest t => IsTest [t] where
toTestList = concatMap toTestList
@ -52,7 +53,10 @@ data T where
T :: (Eq a, Show a) => String -> ConcIO a -> Predicate a -> T
W :: (Eq a, Show a) => String -> ConcIO a -> Predicate a -> (String, Way) -> T
B :: (Eq a, Show a) => String -> ConcIO a -> Predicate a -> Bounds -> T
TEST :: (Eq a, Show a) => String -> ConcIO a -> Predicate a -> [(String, Way)] -> Bool -> T
TEST :: (Eq a, Show a) => String -> ConcIO a -> Predicate a -> [(String, Settings IO a)] -> Bool -> T
toSettings :: Applicative f => Way -> Settings f a
toSettings w = fromWayAndMemType w defaultMemType
defaultWays :: [(String, Way)]
defaultWays = defaultWaysFor defaultBounds
@ -72,13 +76,13 @@ djfu :: (Eq a, Show a) => String -> Predicate a -> ConcIO a -> [T.TestTree]
djfu name p c = toTestList $ W name c p ("systematically", systematically defaultBounds)
djfuS :: (Eq a, Show a) => String -> Predicate a -> ConcIO a -> [T.TestTree]
djfuS name p c = toTestList $ TEST name c p [("systematically", systematically defaultBounds)] False
djfuS name p c = toTestList $ TEST name c p [("systematically", toSettings (systematically defaultBounds))] False
djfuT :: (Eq a, Show a) => String -> Predicate a -> ConcIO a -> [T.TestTree]
djfuT name p c = toTestList $ T name c p
djfuTS :: (Eq a, Show a) => String -> Predicate a -> ConcIO a -> [T.TestTree]
djfuTS name p c = toTestList $ TEST name c p defaultWays False
djfuTS name p c = toTestList $ TEST name c p (map (second toSettings) defaultWays) False
alwaysFailsWith :: (Failure -> Bool) -> Predicate a
alwaysFailsWith p = alwaysTrue (either p (const False))

8
dejafu-tests/lib/Examples/ClassLaws.hs
View File

@ -13,9 +13,9 @@ import Control.Monad.IO.Class (MonadIO, liftIO)
import Data.Maybe (isJust)
import Data.Set (fromList)
import qualified Hedgehog as H
import Test.DejaFu (defaultBounds, defaultMemType)
import Test.DejaFu (defaultMemType, defaultWay)
import Test.DejaFu.Conc (ConcIO)
import Test.DejaFu.SCT (sctBound)
import Test.DejaFu.SCT (runSCT)
import Common
@ -192,8 +192,8 @@ eq left right = runConcurrently left `eq'` runConcurrently right
eq' :: (MonadIO m, Ord a) => ConcIO a -> ConcIO a -> m Bool
eq' left right = liftIO $ do
leftTraces <- sctBound defaultMemType defaultBounds left
rightTraces <- sctBound defaultMemType defaultBounds right
leftTraces <- runSCT defaultWay defaultMemType left
rightTraces <- runSCT defaultWay defaultMemType right
let toSet = fromList . map fst
pure (toSet leftTraces == toSet rightTraces)

2
dejafu-tests/lib/Integration.hs
View File

@ -3,7 +3,6 @@ module Integration where
import Test.Tasty.Options (OptionDescription)
import qualified Integration.Async as A
import qualified Integration.Discard as D
import qualified Integration.Litmus as L
import qualified Integration.MultiThreaded as M
import qualified Integration.Names as N
@ -18,7 +17,6 @@ import Common
tests :: [TestTree]
tests =
[ testGroup "Async" A.tests
, testGroup "Discard" D.tests
, testGroup "Litmus" L.tests
, testGroup "MultiThreaded" M.tests
, testGroup "Names" N.tests

43
dejafu-tests/lib/Integration/Discard.hs
View File

@ -1,43 +0,0 @@
module Integration.Discard where
import Control.Concurrent.Classy hiding (check)
import Data.Foldable (for_)
import Test.DejaFu (gives')
import Test.DejaFu.Conc (ConcIO)
import Test.DejaFu.SCT
import Test.DejaFu.Types (Failure)
import Test.Tasty.HUnit
import Common
tests :: [TestTree]
tests = toTestList
[ check "All results are kept when none are discarded" [1, 2, 3] $
const Nothing
, check "No results are kept when all are discarded" [] $
const (Just DiscardResultAndTrace)
, check "Results failing the test are not present" [1, 2] $
\x -> if x == Right 3 then Just DiscardResultAndTrace else Nothing
, testCase "No traces kept when they get discared" $ testDiscardTrace discarder testAction
]
where
check name xs f = testDejafuDiscard f defaultWay defaultMemType name (gives' xs) testAction
testAction = do
mvar <- newEmptyMVarInt
_ <- fork $ putMVar mvar 1
_ <- fork $ putMVar mvar 2
_ <- fork $ putMVar mvar 3
readMVar mvar
discarder (Right 2) = Just DiscardTrace
discarder (Right 3) = Just DiscardResultAndTrace
discarder _ = Nothing
testDiscardTrace :: (Either Failure a -> Maybe Discard) -> ConcIO a -> Assertion
testDiscardTrace discarder action = do
results <- runSCTDiscard discarder defaultWay defaultMemType action
for_ results $ \(efa, trace) -> case discarder efa of
Just DiscardResultAndTrace -> assertFailure "expected result to be discarded"
Just DiscardTrace
| null trace -> pure ()
| otherwise -> assertFailure "expected trace to be discarded"
Nothing -> pure ()

72
dejafu-tests/lib/Integration/SCT.hs
View File

@ -1,8 +1,13 @@
module Integration.SCT where
import Control.Concurrent.Classy
import Control.Concurrent.Classy hiding (check)
import Control.Monad (void)
import Control.Monad.IO.Class (liftIO)
import Data.Foldable (for_)
import qualified Data.IORef as IORef
import qualified Data.Set as S
import System.Random (mkStdGen)
import Test.DejaFu (gives')
import Test.DejaFu.SCT
import Test.DejaFu.Types (Failure(..))
import Test.Tasty.HUnit
@ -11,7 +16,70 @@ import Common
tests :: [TestTree]
tests =
toTestList
[ testGroup "Discard" discardTests
, testGroup "EarlyExit" earlyExitTests
, testGroup "Results" resultsSetTests
]
-------------------------------------------------------------------------------
discardTests :: [TestTree]
discardTests = toTestList
[ check "All results are kept when none are discarded" [1, 2, 3] $
const Nothing
, check "No results are kept when all are discarded" [] $
const (Just DiscardResultAndTrace)
, check "Results failing the test are not present" [1, 2] $
\x -> if x == Right 3 then Just DiscardResultAndTrace else Nothing
, testCase "No traces kept when they get discared" $ testDiscardTrace discarder testAction
]
where
check name xs f = testDejafuWithSettings (set ldiscard (Just f) defaultSettings) name (gives' xs) testAction
testAction = do
mvar <- newEmptyMVarInt
_ <- fork $ putMVar mvar 1
_ <- fork $ putMVar mvar 2
_ <- fork $ putMVar mvar 3
readMVar mvar
discarder (Right 2) = Just DiscardTrace
discarder (Right 3) = Just DiscardResultAndTrace
discarder _ = Nothing
testDiscardTrace discarder action = do
results <- runSCTWithSettings (set ldiscard (Just discarder) defaultSettings) action
for_ results $ \(efa, trace) -> case discarder efa of
Just DiscardResultAndTrace -> assertFailure "expected result to be discarded"
Just DiscardTrace
| null trace -> pure ()
| otherwise -> assertFailure "expected trace to be discarded"
Nothing -> pure ()
-------------------------------------------------------------------------------
earlyExitTests :: [TestTree]
earlyExitTests = toTestList
[ eeTest "Without discarding" [1,2,3,4,5] Nothing
, eeTest "Discarding some result" [1,2,4,5] $ Just (\efa -> if efa == Right 3 then Just DiscardResultAndTrace else Nothing)
, eeTest "Discarding the stop condition" [1,2,3,4] $ Just (\efa -> if efa == Right 5 then Just DiscardResultAndTrace else Nothing)
]
where
eeTest name expected d = testCase name $ do
-- abuse IO to get a different result form every execution
r <- liftIO (IORef.newIORef (0::Int))
actual <- resultsSetWithSettings (eeSettings d) $ do
liftIO (IORef.modifyIORef r (+1))
liftIO (IORef.readIORef r)
S.fromList (map Right expected) @=? actual
eeSettings d =
set ldiscard d $
set learlyExit (Just (==Right 5)) $
fromWayAndMemType (randomly (mkStdGen 0) 150) defaultMemType
-------------------------------------------------------------------------------
resultsSetTests :: [TestTree]
resultsSetTests = toTestList
[ testCase "Proper results from resultsSet" $ do
tested <- resultsSet defaultWay defaultMemType testAction
results @=? tested

2
dejafu-tests/lib/Integration/SingleThreaded.hs
View File

@ -7,7 +7,7 @@ import Control.Exception (ArithException(..),
import Test.DejaFu (Failure(..), gives, gives', isAbort,
isDeadlock, isIllegalDontCheck,
isUncaughtException)
import Test.DejaFu.Defaults (defaultLengthBound)
import Test.DejaFu.Settings (defaultLengthBound)
import Control.Concurrent.Classy
import Control.Monad (replicateM_)

68
dejafu/CHANGELOG.rst
View File

@ -6,6 +6,74 @@ standard Haskell versioning scheme.
.. _PVP: https://pvp.haskell.org/
1.2.0.0 - The Settings Release (2018-03-06)
-------------------------------------------
* Git: :tag:`dejafu-1.2.0.0`
* Hackage: :hackage:`dejafu-1.2.0.0`
**Contributors:** :u:`qrilka` (:pull:`236`).
Added
~~~~~
* (:pull:`238`) A record-based approach to SCT configuration:
* ``Test.DejaFu.Settings``
(re-exported from ``Test.Dejafu`` and ``Test.DejaFu.SCT``)
* ``Test.DejaFu.Settings.Settings``
* ``Test.DejaFu.Settings.defaultSettings``
* ``Test.DejaFu.Settings.fromWayAndMemType``
* Lenses:
* ``Test.DejaFu.Settings.lway``
* ``Test.DejaFu.Settings.lmemtype``
* ``Test.DejaFu.Settings.ldiscard``
* ``Test.DejaFu.Settings.learlyExit``
* ``Test.DejaFu.Settings.ldebugShow``
* ``Test.DejaFu.Settings.ldebugPrint``
* Lens helpers:
* ``Test.DejaFu.Settings.get``
* ``Test.DejaFu.Settings.set``
* Runners:
* ``Test.DejaFu.SCT.runSCTWithSettings``
* ``Test.DejaFu.SCT.runSCTWithSettings'``
* ``Test.DejaFu.SCT.resultsSetWithSettings``
* ``Test.DejaFu.SCT.resultsSetWithSettings'``
* (:pull:`238`) Settings-based test functions:
* ``Test.DejaFu.autocheckWithSettings``
* ``Test.DejaFu.dejafuWithSettings``
* ``Test.DejaFu.dejafusWithSettings``
* ``Test.DejaFu.runTestWithSettings``
Deprecated
~~~~~~~~~~
* (:pull:`238`) SCT function variants:
* ``Test.DejaFu.SCT.runSCTDiscard``
* ``Test.DejaFu.SCT.resultSetDiscard``
* ``Test.DejaFu.SCT.runSCTDiscard'``
* ``Test.DejaFu.SCT.resultSetDiscard'``
* ``Test.DejaFu.SCT.sctBound``
* ``Test.DejaFu.SCT.sctBoundDiscard``
* ``Test.DejaFu.SCT.sctUniformRandom``
* ``Test.DejaFu.SCT.sctUniformRandomDiscard``
* ``Test.DejaFu.SCT.sctWeightedRandom``
* ``Test.DejaFu.SCT.sctWeightedRandomDiscard``
* (:pull:`238`) The ``Test.DejaFu.Defaults`` module. Import
``Test.DejaFu.Settings`` instead.
* (:pull:`238`) ``Test.DejaFu.dejafuDiscard``.
Removed
~~~~~~~
* (:pull:`238`) ``Test.DejaFu.Defaults.defaultDiscarder``, as the
discard function is optional.
1.1.0.2 (2018-03-01)
--------------------

296
dejafu/Test/DejaFu.hs
View File

@ -4,7 +4,7 @@
{- |
Module : Test.DejaFu
Copyright : (c) 2015--2017 Michael Walker
Copyright : (c) 2015--2018 Michael Walker
License : MIT
Maintainer : Michael Walker <mike@barrucadu.co.uk>
Stability : experimental
@ -105,149 +105,21 @@ module Test.DejaFu
There are a few knobs to tweak to control the behaviour of dejafu.
The defaults should generally be good enough, but if not you have a
few tricks available.
* The 'Way', which controls how schedules are explored.
* The 'MemType', which controls how reads and writes to @CRef@s (or
@IORef@s) behave.
* The 'Discard' function, which saves memory by throwing away
uninteresting results during exploration.
few tricks available. The main two are: the 'Way', which controls how
schedules are explored; and the 'MemType', which controls how reads
and writes to @CRef@s behave; see "Test.DejaFu.Settings" for a
complete listing.
-}
, autocheckWay
, dejafuWay
, dejafusWay
, dejafuDiscard
, autocheckWithSettings
, dejafuWithSettings
, dejafusWithSettings
-- *** Defaults
, defaultWay
, defaultMemType
, defaultDiscarder
-- *** Exploration
, Way
, systematically
, randomly
, uniformly
, swarmy
-- **** Schedule bounding
{- |
Schedule bounding is used by the 'systematically' approach to limit
the search-space, which in general will be huge.
There are three types of bounds used:
* The 'PreemptionBound', which bounds the number of pre-emptive
context switches. Empirical evidence suggests @2@ is a good value
for this, if you have a small test case.
* The 'FairBound', which bounds the difference between how many times
threads can yield. This is necessary to test certain kinds of
potentially non-terminating behaviour, such as spinlocks.
* The 'LengthBound', which bounds how long a test case can run, in
terms of scheduling decisions. This is necessary to test certain
kinds of potentially non-terminating behaviour, such as livelocks.
Schedule bounding is not used by the non-systematic exploration
behaviours.
-}
, Bounds(..)
, defaultBounds
, noBounds
, PreemptionBound(..)
, defaultPreemptionBound
, FairBound(..)
, defaultFairBound
, LengthBound(..)
, defaultLengthBound
-- *** Memory model
{- |
When executed on a multi-core processor some @CRef@ / @IORef@ programs
can exhibit \"relaxed memory\" behaviours, where the apparent
behaviour of the program is not a simple interleaving of the actions
of each thread.
__Example:__ This is a simple program which creates two @CRef@s
containing @False@, and forks two threads. Each thread writes @True@
to one of the @CRef@s and reads the other. The value that each thread
reads is communicated back through an @MVar@:
>>> :{
let relaxed = do
r1 <- newCRef False
r2 <- newCRef False
x <- spawn $ writeCRef r1 True >> readCRef r2
y <- spawn $ writeCRef r2 True >> readCRef r1
(,) <$> readMVar x <*> readMVar y
:}
We see something surprising if we ask for the results:
>>> autocheck relaxed
[pass] Never Deadlocks
[pass] No Exceptions
[fail] Consistent Result
(False,True) S0---------S1----S0--S2----S0--
<BLANKLINE>
(False,False) S0---------S1--P2----S1--S0---
<BLANKLINE>
(True,False) S0---------S2----S1----S0---
<BLANKLINE>
(True,True) S0---------S1-C-S2----S1---S0---
False
It's possible for both threads to read the value @False@, even though
each writes @True@ to the other @CRef@ before reading. This is
because processors are free to re-order reads and writes to
independent memory addresses in the name of performance.
Execution traces for relaxed memory computations can include \"C\"
actions, as above, which show where @CRef@ writes were explicitly
/committed/, and made visible to other threads.
However, modelling this behaviour can require more executions. If you
do not care about the relaxed-memory behaviour of your program, use
the 'SequentialConsistency' model.
-}
, MemType(..)
-- *** Reducing memory usage
{- |
Sometimes we know that a result is uninteresting and cannot affect the
result of a test, in which case there is no point in keeping it
around. Execution traces can be large, so any opportunity to get rid
of them early is possibly a great saving of memory.
A discard function, which has type @Either Failure a -> Maybe
Discard@, can selectively discard results or execution traces before
the schedule exploration finishes, allowing them to be garbage
collected sooner.
__Note:__ This is only relevant if you are producing your own
predicates. The predicates and helper functions provided by this
module do discard results and traces wherever possible.
-}
, Discard(..)
, module Test.DejaFu.Settings
-- ** Manual testing
@ -391,6 +263,9 @@ interference we have provided: the left term never empties a full
-}
, module Test.DejaFu.Refinement
-- * Deprecated
, dejafuDiscard
) where
import Control.Arrow (first)
@ -407,9 +282,9 @@ import Data.Profunctor (Profunctor(..))
import System.Environment (lookupEnv)
import Test.DejaFu.Conc
import Test.DejaFu.Defaults
import Test.DejaFu.Refinement
import Test.DejaFu.SCT
import Test.DejaFu.Settings
import Test.DejaFu.Types
import Test.DejaFu.Utils
@ -458,7 +333,7 @@ autocheck :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a)
=> ConcT r n a
-- ^ The computation to test.
-> n Bool
autocheck = autocheckWay defaultWay defaultMemType
autocheck = autocheckWithSettings defaultSettings
-- | Variant of 'autocheck' which takes a way to run the program and a
-- memory model.
@ -496,11 +371,42 @@ autocheckWay :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a)
-> ConcT r n a
-- ^ The computation to test.
-> n Bool
autocheckWay way memtype = dejafusWay way memtype autocheckCases
autocheckWay way = autocheckWithSettings . fromWayAndMemType way
-- | Predicates for the various autocheck functions.
autocheckCases :: Eq a => [(String, Predicate a)]
autocheckCases =
-- | Variant of 'autocheck' which takes a settings record.
--
-- >>> autocheckWithSettings (fromWayAndMemType defaultWay defaultMemType) relaxed
-- [pass] Never Deadlocks
-- [pass] No Exceptions
-- [fail] Consistent Result
-- (False,True) S0---------S1----S0--S2----S0--
-- <BLANKLINE>
-- (False,False) S0---------S1--P2----S1--S0---
-- <BLANKLINE>
-- (True,False) S0---------S2----S1----S0---
-- <BLANKLINE>
-- (True,True) S0---------S1-C-S2----S1---S0---
-- False
--
-- >>> autocheckWithSettings (fromWayAndMemType defaultWay SequentialConsistency) relaxed
-- [pass] Never Deadlocks
-- [pass] No Exceptions
-- [fail] Consistent Result
-- (False,True) S0---------S1----S0--S2----S0--
-- <BLANKLINE>
-- (True,True) S0---------S1-P2----S1---S0---
-- <BLANKLINE>
-- (True,False) S0---------S2----S1----S0---
-- False
--
-- @since 1.2.0.0
autocheckWithSettings :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a)
=> Settings n a
-- ^ The SCT settings.
-> ConcT r n a
-- ^ The computation to test.
-> n Bool
autocheckWithSettings settings = dejafusWithSettings settings
[ ("Never Deadlocks", representative deadlocksNever)
, ("No Exceptions", representative exceptionsNever)
, ("Consistent Result", alwaysSame) -- already representative
@ -529,7 +435,7 @@ dejafu :: (MonadConc n, MonadIO n, MonadRef r n, Show b)
-> ConcT r n a
-- ^ The computation to test.
-> n Bool
dejafu = dejafuWay defaultWay defaultMemType
dejafu = dejafuWithSettings defaultSettings
-- | Variant of 'dejafu' which takes a way to run the program and a
-- memory model.
@ -563,7 +469,32 @@ dejafuWay :: (MonadConc n, MonadIO n, MonadRef r n, Show b)
-> ConcT r n a
-- ^ The computation to test.
-> n Bool
dejafuWay = dejafuDiscard (const Nothing)
dejafuWay way = dejafuWithSettings . fromWayAndMemType way
-- | Variant of 'dejafu' which takes a settings record.
--
-- >>> import System.Random
--
-- >>> dejafuWithSettings (fromWayAndMemType (randomly (mkStdGen 1) 100) defaultMemType) "Randomly!" alwaysSame example
-- [fail] Randomly!
-- "hello" S0----S1--S0--
-- <BLANKLINE>
-- "world" S0----S2--S1-S0--
-- False
--
-- @since 1.2.0.0
dejafuWithSettings :: (MonadConc n, MonadIO n, MonadRef r n, Show b)
=> Settings n a
-- ^ The SCT settings.
-> String
-- ^ The name of the test.
-> ProPredicate a b
-- ^ The predicate to check.
-> ConcT r n a
-- ^ The computation to test.
-> n Bool
dejafuWithSettings settings name test =
dejafusWithSettings settings [(name, test)]
-- | Variant of 'dejafuWay' which can selectively discard results.
--
@ -589,10 +520,9 @@ dejafuDiscard :: (MonadConc n, MonadIO n, MonadRef r n, Show b)
-> ConcT r n a
-- ^ The computation to test.
-> n Bool
dejafuDiscard discard way memtype name test conc = do
let discarder = strengthenDiscard discard (pdiscard test)
traces <- runSCTDiscard discarder way memtype conc
liftIO $ doTest name (peval test traces)
dejafuDiscard discard way =
dejafuWithSettings . set ldiscard (Just discard) . fromWayAndMemType way
{-# DEPRECATED dejafuDiscard "Use dejafuWithSettings instead" #-}
-- | Variant of 'dejafu' which takes a collection of predicates to
-- test, returning 'True' if all pass.
@ -612,7 +542,7 @@ dejafus :: (MonadConc n, MonadIO n, MonadRef r n, Show b)
-> ConcT r n a
-- ^ The computation to test.
-> n Bool
dejafus = dejafusWay defaultWay defaultMemType
dejafus = dejafusWithSettings defaultSettings
-- | Variant of 'dejafus' which takes a way to run the program and a
-- memory model.
@ -638,12 +568,35 @@ dejafusWay :: (MonadConc n, MonadIO n, MonadRef r n, Show b)
-> ConcT r n a
-- ^ The computation to test.
-> n Bool
dejafusWay way memtype tests conc = do
traces <- runSCTDiscard discarder way memtype conc
dejafusWay way = dejafusWithSettings . fromWayAndMemType way
-- | Variant of 'dejafus' which takes a settings record.
--
-- >>> dejafusWithSettings (fromWayAndMemType defaultWay SequentialConsistency) [("A", alwaysSame), ("B", exceptionsNever)] relaxed
-- [fail] A
-- (False,True) S0---------S1----S0--S2----S0--
-- <BLANKLINE>
-- (True,True) S0---------S1-P2----S1---S0---
-- <BLANKLINE>
-- (True,False) S0---------S2----S1----S0---
-- [pass] B
-- False
--
-- @since 1.2.0.0
dejafusWithSettings :: (MonadConc n, MonadIO n, MonadRef r n, Show b)
=> Settings n a
-- ^ The SCT settings.
-> [(String, ProPredicate a b)]
-- ^ The list of predicates (with names) to check.
-> ConcT r n a
-- ^ The computation to test.
-> n Bool
dejafusWithSettings settings tests conc = do
traces <- runSCTWithSettings (set ldiscard (Just discarder) settings) conc
results <- mapM (\(name, test) -> liftIO . doTest name $ chk test traces) tests
pure (and results)
where
discarder = foldr
discarder = maybe id strengthenDiscard (get ldiscard settings) $ foldr
(weakenDiscard . pdiscard . snd)
(const (Just DiscardResultAndTrace))
tests
@ -653,11 +606,14 @@ dejafusWay way memtype tests conc = do
-- include more than this if the different predicates have
-- different discard functions, so we do another pass of
-- discarding.
chk p = peval p . mapMaybe go where
go r@(efa, _) = case pdiscard p efa of
Just DiscardResultAndTrace -> Nothing
Just DiscardTrace -> Just (efa, [])
Nothing -> Just r
chk p rs
| moreThan 1 rs =
let go r@(efa, _) = case pdiscard p efa of
Just DiscardResultAndTrace -> Nothing
Just DiscardTrace -> Just (efa, [])
Nothing -> Just r
in peval p (mapMaybe go rs)
| otherwise = peval p rs
-------------------------------------------------------------------------------
-- Test cases
@ -709,7 +665,7 @@ runTest :: (MonadConc n, MonadRef r n)
-> ConcT r n a
-- ^ The computation to test
-> n (Result b)
runTest = runTestWay defaultWay defaultMemType
runTest = runTestWithSettings defaultSettings
-- | Variant of 'runTest' which takes a way to run the program and a
-- memory model.
@ -729,8 +685,26 @@ runTestWay :: (MonadConc n, MonadRef r n)
-> ConcT r n a
-- ^ The computation to test
-> n (Result b)
runTestWay way memtype p conc =
peval p <$> runSCTDiscard (pdiscard p) way memtype conc
runTestWay way = runTestWithSettings . fromWayAndMemType way
-- | Variant of 'runTest' which takes a settings record.
--
-- The exact executions tried, and the order in which results are
-- found, is unspecified and may change between releases. This may
-- affect which failing traces are reported, when there is a failure.
--
-- @since 1.2.0.0
runTestWithSettings :: (MonadConc n, MonadRef r n)
=> Settings n a
-- ^ The SCT settings.
-> ProPredicate a b
-- ^ The predicate to check
-> ConcT r n a
-- ^ The computation to test
-> n (Result b)
runTestWithSettings settings p conc =
let discarder = maybe id strengthenDiscard (get ldiscard settings) (pdiscard p)
in peval p <$> runSCTWithSettings (set ldiscard (Just discarder) settings) conc
-------------------------------------------------------------------------------

71
dejafu/Test/DejaFu/Defaults.hs
View File

@ -1,69 +1,20 @@
-- |
-- Module : Test.DejaFu.Defaults
-- Copyright : (c) 2017 Michael Walker
-- Copyright : (c) 2017--2018 Michael Walker
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : experimental
-- Portability : portable
--
-- Default parameters for test execution.
module Test.DejaFu.Defaults where
module Test.DejaFu.Defaults {-# DEPRECATED "Import Test.DejaFu.Settings instead" #-}
( defaultSettings
, defaultWay
, defaultBounds
, defaultPreemptionBound
, defaultFairBound
, defaultLengthBound
, defaultMemType
) where
import Test.DejaFu.SCT
import Test.DejaFu.Types
-- | A default way to execute concurrent programs: systematically
-- using 'defaultBounds'.
--
-- @since 0.6.0.0
defaultWay :: Way
defaultWay = systematically defaultBounds
-- | Do not discard any results.
--
-- @since 0.7.1.0
defaultDiscarder :: Either Failure a -> Maybe Discard
defaultDiscarder = const Nothing
-- | The default memory model: @TotalStoreOrder@
--
-- @since 0.2.0.0
defaultMemType :: MemType
defaultMemType = TotalStoreOrder
-- | All bounds enabled, using their default values.
--
-- @since 0.2.0.0
defaultBounds :: Bounds
defaultBounds = Bounds
{ boundPreemp = Just defaultPreemptionBound
, boundFair = Just defaultFairBound
, boundLength = Just defaultLengthBound
}
-- | A sensible default preemption bound: 2.
--
-- See /Concurrency Testing Using Schedule Bounding: an Empirical Study/,
-- P. Thomson, A. F. Donaldson, A. Betts for justification.
--
-- @since 0.2.0.0
defaultPreemptionBound :: PreemptionBound
defaultPreemptionBound = 2
-- | A sensible default fair bound: 5.
--
-- This comes from playing around myself, but there is probably a
-- better default.
--
-- @since 0.2.0.0
defaultFairBound :: FairBound
defaultFairBound = 5
-- | A sensible default length bound: 250.
--
-- Based on the assumption that anything which executes for much
-- longer (or even this long) will take ages to test.
--
-- @since 0.2.0.0
defaultLengthBound :: LengthBound
defaultLengthBound = 250
import Test.DejaFu.Settings

35
dejafu/Test/DejaFu/Internal.hs
View File

@ -1,10 +1,12 @@
{-# LANGUAGE GADTs #-}
-- |
-- Module : Test.DejaFu.Internal
-- Copyright : (c) 2017 Michael Walker
-- Copyright : (c) 2017--2018 Michael Walker
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : experimental
-- Portability : portable
-- Portability : GADTs
--
-- Internal types and functions used throughout DejaFu. This module
-- is NOT considered to form part of the public interface of this
@ -18,9 +20,38 @@ import qualified Data.Map.Strict as M
import Data.Maybe (fromMaybe)
import Data.Set (Set)
import qualified Data.Set as S
import System.Random (RandomGen)
import Test.DejaFu.Types
-------------------------------------------------------------------------------
-- * SCT settings
-- | SCT configuration record.
--
-- @since 1.2.0.0
data Settings n a = Settings
{ _way :: Way
, _memtype :: MemType
, _discard :: Maybe (Either Failure a -> Maybe Discard)
, _debugShow :: Maybe (a -> String)
, _debugPrint :: Maybe (String -> n ())
, _earlyExit :: Maybe (Either Failure a -> Bool)
}
-- | How to explore the possible executions of a concurrent program.
--
-- @since 0.7.0.0
data Way where
Systematic :: Bounds -> Way
Weighted :: RandomGen g => g -> Int -> Int -> Way
Uniform :: RandomGen g => g -> Int -> Way
instance Show Way where
show (Systematic bs) = "Systematic (" ++ show bs ++ ")"
show (Weighted _ n t) = "Weighted <gen> " ++ show (n, t)
show (Uniform _ n) = "Uniform <gen> " ++ show n
-------------------------------------------------------------------------------
-- * Identifiers

2
dejafu/Test/DejaFu/Refinement.hs
View File

@ -115,8 +115,8 @@ import qualified Data.Set as S
import Test.LeanCheck (Listable(..), concatMapT, mapT)
import Test.DejaFu.Conc (ConcIO, Failure, subconcurrency)
import Test.DejaFu.Defaults (defaultMemType, defaultWay)
import Test.DejaFu.SCT (runSCT)
import Test.DejaFu.Settings (defaultMemType, defaultWay)
-- $setup
-- >>> import Control.Concurrent.Classy hiding (check)

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

@ -1,84 +1,39 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
-- |
-- Module : Test.DejaFu.SCT
-- Copyright : (c) 2015--2017 Michael Walker
-- Copyright : (c) 2015--2018 Michael Walker
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : experimental
-- Portability : BangPatterns, GADTs, GeneralizedNewtypeDeriving, LambdaCase
-- Portability : BangPatterns, LambdaCase
--
-- Systematic testing for concurrent computations.
module Test.DejaFu.SCT
( -- * Running Concurrent Programs
Way
, systematically
, randomly
, uniformly
, swarmy
, runSCT
, resultsSet
-- ** Discarding variants
, Discard(..)
, runSCTDiscard
, resultsSetDiscard
-- ** Strict variants
runSCT
, runSCT'
, resultsSet
, resultsSet'
-- ** Configuration
, runSCTWithSettings
, runSCTWithSettings'
, resultsSetWithSettings
, resultsSetWithSettings'
, module Test.DejaFu.Settings
-- * Deprecated
, runSCTDiscard
, runSCTDiscard'
, resultsSetDiscard
, resultsSetDiscard'
-- * Bounded Partial-order Reduction
-- | We can characterise the state of a concurrent computation by
-- considering the ordering of dependent events. This is a partial
-- order: independent events can be performed in any order without
-- affecting the result, and so are /not/ ordered.
--
-- Partial-order reduction is a technique for computing these
-- partial orders, and only testing one total order for each partial
-- order. This cuts down the amount of work to be done
-- significantly. /Bounded/ partial-order reduction is a further
-- optimisation, which only considers schedules within some bound.
--
-- This module provides a combination pre-emption, fair, and length
-- bounding runner:
--
-- * Pre-emption + fair bounding is useful for programs which use
-- loop/yield control flows but are otherwise terminating.
--
-- * Pre-emption, fair + length bounding is useful for
-- non-terminating programs, and used by the testing functionality
-- in @Test.DejaFu@.
--
-- See /Bounded partial-order reduction/, K. Coons, M. Musuvathi,
-- K. McKinley for more details.
, Bounds(..)
, PreemptionBound(..)
, FairBound(..)
, LengthBound(..)
, noBounds
, sctBound
, sctBoundDiscard
-- * Random Scheduling
-- | By greatly sacrificing completeness, testing of a large
-- concurrent system can be greatly sped-up. Counter-intuitively,
-- random scheduling has better bug-finding behaviour than just
-- executing a program \"for real\" many times. This is perhaps
-- because a random scheduler is more chaotic than the real
-- scheduler.
, sctUniformRandom
, sctWeightedRandom
, sctUniformRandomDiscard
, sctWeightedRandom
, sctWeightedRandomDiscard
) where
@ -97,93 +52,13 @@ import Test.DejaFu.Conc
import Test.DejaFu.Internal
import Test.DejaFu.SCT.Internal.DPOR
import Test.DejaFu.SCT.Internal.Weighted
import Test.DejaFu.Settings
import Test.DejaFu.Types
import Test.DejaFu.Utils
-------------------------------------------------------------------------------
-- Running Concurrent Programs
-- | How to explore the possible executions of a concurrent program.
--
-- @since 0.7.0.0
data Way where
Systematic :: Bounds -> Way
Weighted :: RandomGen g => g -> Int -> Int -> Way
Uniform :: RandomGen g => g -> Int -> Way
instance Show Way where
show (Systematic bs) = "Systematic (" ++ show bs ++ ")"
show (Weighted _ n t) = "Weighted <gen> " ++ show (n, t)
show (Uniform _ n) = "Uniform <gen> " ++ show n
-- | Systematically execute a program, trying all distinct executions
-- within the bounds.
--
-- This corresponds to 'sctBound'.
--
-- @since 0.7.0.0
systematically
:: Bounds
-- ^ The bounds to constrain the exploration.
-> Way
systematically = Systematic
-- | Randomly execute a program, exploring a fixed number of
-- executions.
--
-- Threads are scheduled by a weighted random selection, where weights
-- are assigned randomly on thread creation.
--
-- This corresponds to 'sctWeightedRandom' with weight re-use
-- disabled, and is not guaranteed to find all distinct results
-- (unlike 'systematically' / 'sctBound').
--
-- @since 0.7.0.0
randomly :: RandomGen g
=> g
-- ^ The random generator to drive the scheduling.
-> Int
-- ^ The number of executions to try.
-> Way
randomly g lim = swarmy g lim 1
-- | Randomly execute a program, exploring a fixed number of
-- executions.
--
-- Threads are scheduled by a uniform random selection.
--
-- This corresponds to 'sctUniformRandom', and is not guaranteed to
-- find all distinct results (unlike 'systematically' / 'sctBound').
--
-- @since 0.7.0.0
uniformly :: RandomGen g
=> g
-- ^ The random generator to drive the scheduling.
-> Int
-- ^ The number of executions to try.
-> Way
uniformly = Uniform
-- | Randomly execute a program, exploring a fixed number of
-- executions.
--
-- Threads are scheduled by a weighted random selection, where weights
-- are assigned randomly on thread creation.
--
-- This corresponds to 'sctWeightedRandom', and is not guaranteed to
-- find all distinct results (unlike 'systematically' / 'sctBound').
--
-- @since 0.7.0.0
swarmy :: RandomGen g
=> g
-- ^ The random generator to drive the scheduling.
-> Int
-- ^ The number of executions to try.
-> Int
-- ^ The number of executions to use the thread weights for.
-> Way
swarmy = Weighted
-- | Explore possible executions of a concurrent program according to
-- the given 'Way'.
--
@ -199,7 +74,7 @@ runSCT :: (MonadConc n, MonadRef r n)
-> ConcT r n a
-- ^ The computation to run many times.
-> n [(Either Failure a, Trace)]
runSCT = runSCTDiscard (const Nothing)
runSCT way = runSCTWithSettings . fromWayAndMemType way
-- | Return the set of results of a concurrent program.
--
@ -212,7 +87,7 @@ resultsSet :: (MonadConc n, MonadRef r n, Ord a)
-> ConcT r n a
-- ^ The computation to run many times.
-> n (Set (Either Failure a))
resultsSet = resultsSetDiscard (const Nothing)
resultsSet way = resultsSetWithSettings . fromWayAndMemType way
-- | A variant of 'runSCT' which can selectively discard results.
--
@ -230,9 +105,8 @@ runSCTDiscard :: (MonadConc n, MonadRef r n)
-> 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
runSCTDiscard discard way = runSCTWithSettings . set ldiscard (Just discard) . fromWayAndMemType way
{-# DEPRECATED runSCTDiscard "Use runSCTWithSettings instead" #-}
-- | A variant of 'resultsSet' which can selectively discard results.
--
@ -250,6 +124,7 @@ resultsSetDiscard :: (MonadConc n, MonadRef r n, Ord a)
resultsSetDiscard discard way memtype conc =
let discard' efa = discard efa <|> Just DiscardTrace
in S.fromList . map fst <$> runSCTDiscard discard' way memtype conc
{-# DEPRECATED resultsSetDiscard "Use resultsSetWithSettings instead" #-}
-- | A strict variant of 'runSCT'.
--
@ -262,7 +137,7 @@ resultsSetDiscard discard way memtype conc =
-- @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)
runSCT' way = runSCTWithSettings' . fromWayAndMemType way
-- | A strict variant of 'resultsSet'.
--
@ -272,7 +147,7 @@ runSCT' = runSCTDiscard' (const Nothing)
-- @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)
resultsSet' way = resultsSetWithSettings' . fromWayAndMemType way
-- | A strict variant of 'runSCTDiscard'.
--
@ -288,6 +163,7 @@ runSCTDiscard' :: (MonadConc n, MonadRef r n, NFData a)
runSCTDiscard' discard way memtype conc = do
res <- runSCTDiscard discard way memtype conc
rnf res `seq` pure res
{-# DEPRECATED runSCTDiscard' "Use runSCTWithSettings' instead" #-}
-- | A strict variant of 'resultsSetDiscard'.
--
@ -300,36 +176,116 @@ resultsSetDiscard' :: (MonadConc n, MonadRef r n, Ord a, NFData a)
resultsSetDiscard' discard way memtype conc = do
res <- resultsSetDiscard discard way memtype conc
rnf res `seq` pure res
{-# DEPRECATED resultsSetDiscard' "Use resultsSetWithSettings' instead" #-}
-------------------------------------------------------------------------------
-- Configuration
-- | A variant of 'runSCT' which takes a 'Settings' record.
--
-- The exact executions tried, and the order in which results are
-- found, is unspecified and may change between releases.
--
-- @since 1.2.0.0
runSCTWithSettings :: (MonadConc n, MonadRef r n)
=> Settings n a
-- ^ The SCT settings.
-> ConcT r n a
-- ^ The computation to run many times.
-> n [(Either Failure a, Trace)]
runSCTWithSettings settings conc = case _way settings of
Systematic cb0 ->
let initial = initialState
check = findSchedulePrefix
step dp (prefix, conservative, sleep) run = do
(res, s, trace) <- run
(dporSched (cBound cb0))
(initialDPORSchedState sleep prefix)
let bpoints = findBacktrackSteps (cBacktrack cb0) (schedBoundKill s) (schedBPoints s) trace
let newDPOR = incorporateTrace conservative trace dp
pure $ if schedIgnore s
then (force newDPOR, Nothing)
else (force (incorporateBacktrackSteps bpoints newDPOR), Just (res, trace))
in sct settings initial check step conc
Uniform g0 lim0 ->
let initial _ = (g0, max 0 lim0)
check (_, 0) = Nothing
check s = Just s
step _ (g, n) run = do
(res, s, trace) <- run
(randSched $ \g' -> (1, g'))
(initialRandSchedState Nothing g)
pure ((schedGen s, n-1), Just (res, trace))
in sct settings initial check step conc
Weighted g0 lim0 use0 ->
let initial _ = (g0, max 0 lim0, max 1 use0, M.empty)
check (_, 0, _, _) = Nothing
check s = Just s
step s (g, n, 0, _) run = step s (g, n, max 1 use0, M.empty) run
step _ (g, n, use, ws) run = do
(res, s, trace) <- run
(randSched $ randomR (1, 50))
(initialRandSchedState (Just ws) g)
pure ((schedGen s, n-1, use-1, schedWeights s), Just (res, trace))
in sct settings initial check step conc
-- | A variant of 'resultsSet' which takes a 'Settings' record.
--
-- @since 1.2.0.0
resultsSetWithSettings :: (MonadConc n, MonadRef r n, Ord a)
=> Settings n a
-- ^ The SCT settings.
-> ConcT r n a
-- ^ The computation to run many times.
-> n (Set (Either Failure a))
resultsSetWithSettings settings conc =
let settings' = settings { _discard = Just $ \efa -> fromMaybe (const Nothing) (_discard settings) efa <|> Just DiscardTrace }
in S.fromList . map fst <$> runSCTWithSettings settings' conc
-- | A strict variant of 'runSCTWithSettings'.
--
-- Demanding the result of this will force it to normal form, which
-- may be more efficient in some situations.
--
-- The exact executions tried, and the order in which results are
-- found, is unspecified and may change between releases.
--
-- @since 1.2.0.0
runSCTWithSettings' :: (MonadConc n, MonadRef r n, NFData a)
=> Settings n a
-> ConcT r n a
-> n [(Either Failure a, Trace)]
runSCTWithSettings' settings conc = do
res <- runSCTWithSettings settings conc
rnf res `seq` pure res
-- | A strict variant of 'resultsSetWithSettings'.
--
-- Demanding the result of this will force it to normal form, which
-- may be more efficient in some situations.
--
-- @since 1.2.0.0
resultsSetWithSettings' :: (MonadConc n, MonadRef r n, Ord a, NFData a)
=> Settings n a
-> ConcT r n a
-> n (Set (Either Failure a))
resultsSetWithSettings' settings conc = do
res <- resultsSetWithSettings settings conc
rnf res `seq` pure res
-------------------------------------------------------------------------------
-- Combined Bounds
-- | @since 0.2.0.0
data Bounds = Bounds
{ boundPreemp :: Maybe PreemptionBound
, boundFair :: Maybe FairBound
, boundLength :: Maybe LengthBound
} deriving (Eq, Ord, Read, Show)
-- | @since 0.5.1.0
instance NFData Bounds where
rnf bs = rnf ( boundPreemp bs
, boundFair bs
, boundLength bs
)
-- | No bounds enabled. This forces the scheduler to just use
-- partial-order reduction and sleep sets to prune the search
-- space. This will /ONLY/ work if your computation always terminates!
--
-- @since 0.3.0.0
noBounds :: Bounds
noBounds = Bounds
{ boundPreemp = Nothing
, boundFair = Nothing
, boundLength = Nothing
}
-- | Combination bound function
cBound :: Bounds -> IncrementalBoundFunc ((Int, Maybe ThreadId), M.Map ThreadId Int, Int)
cBound (Bounds pb fb lb) (Just (k1, k2, k3)) prior lh =
@ -352,22 +308,6 @@ cBacktrack _ = backtrackAt (\_ _ -> False)
-------------------------------------------------------------------------------
-- Pre-emption bounding
-- | BPOR using pre-emption bounding. This adds conservative
-- backtracking points at the prior context switch whenever a
-- non-conervative backtracking point is added, as alternative
-- decisions can influence the reachability of different states.
--
-- See the BPOR paper for more details.
--
-- @since 0.2.0.0
newtype PreemptionBound = PreemptionBound Int
deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show)
-- | @since 0.5.1.0
instance NFData PreemptionBound where
-- not derived, so it can have a separate @since annotation
rnf (PreemptionBound i) = rnf i
-- | Pre-emption bound function. This does not count pre-emptive
-- context switches to a commit thread.
pBound :: PreemptionBound -> IncrementalBoundFunc (Int, Maybe ThreadId)
@ -398,21 +338,6 @@ pBacktrack bs = backtrackAt (\_ _ -> False) bs . concatMap addConservative where
-------------------------------------------------------------------------------
-- Fair bounding
-- | BPOR using fair bounding. This bounds the maximum difference
-- between the number of yield operations different threads have
-- performed.
--
-- See the BPOR paper for more details.
--
-- @since 0.2.0.0
newtype FairBound = FairBound Int
deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show)
-- | @since 0.5.1.0
instance NFData FairBound where
-- not derived, so it can have a separate @since annotation
rnf (FairBound i) = rnf i
-- | Fair bound function
fBound :: FairBound -> IncrementalBoundFunc (M.Map ThreadId Int)
fBound (FairBound fb) k prior lhead =
@ -431,18 +356,6 @@ fBacktrack = backtrackAt check where
-------------------------------------------------------------------------------
-- Length bounding
-- | BPOR using length bounding. This bounds the maximum length (in
-- terms of primitive actions) of an execution.
--
-- @since 0.2.0.0
newtype LengthBound = LengthBound Int
deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show)
-- | @since 0.5.1.0
instance NFData LengthBound where
-- not derived, so it can have a separate @since annotation
rnf (LengthBound i) = rnf i
-- | Length bound function
lBound :: LengthBound -> IncrementalBoundFunc Int
lBound (LengthBound lb) len _ _ =
@ -482,6 +395,7 @@ sctBound :: (MonadConc n, MonadRef r n)
-- ^ The computation to run many times
-> n [(Either Failure a, Trace)]
sctBound = sctBoundDiscard (const Nothing)
{-# DEPRECATED sctBound "Use runSCT instead" #-}
-- | A variant of 'sctBound' which can selectively discard results.
--
@ -499,18 +413,9 @@ sctBoundDiscard :: (MonadConc n, MonadRef r n)
-> ConcT r n a
-- ^ The computation to run many times
-> n [(Either Failure a, Trace)]
sctBoundDiscard discard0 memtype0 cb0 = sct initialState findSchedulePrefix step discard0 memtype0 where
step dp (prefix, conservative, sleep) run = do
(res, s, trace) <- run
(dporSched (cBound cb0))
(initialDPORSchedState sleep prefix)
let bpoints = findBacktrackSteps (cBacktrack cb0) (schedBoundKill s) (schedBPoints s) trace
let newDPOR = incorporateTrace conservative trace dp
pure $ if schedIgnore s
then (force newDPOR, Nothing)
else (force (incorporateBacktrackSteps bpoints newDPOR), Just (res, trace))
sctBoundDiscard discard memtype cb = runSCTWithSettings $
set ldiscard (Just discard) (fromWayAndMemType (systematically cb) memtype)
{-# DEPRECATED sctBoundDiscard "Use runSCTWithSettings instead" #-}
-- | SCT via uniform random scheduling.
--
@ -531,6 +436,7 @@ sctUniformRandom :: (MonadConc n, MonadRef r n, RandomGen g)
-- ^ The computation to run many times.
-> n [(Either Failure a, Trace)]
sctUniformRandom = sctUniformRandomDiscard (const Nothing)
{-# DEPRECATED sctUniformRandom "Use runSCT instead" #-}
-- | A variant of 'sctUniformRandom' which can selectively discard
-- results.
@ -550,15 +456,9 @@ sctUniformRandomDiscard :: (MonadConc n, MonadRef r n, RandomGen g)
-> ConcT r n a
-- ^ The computation to run many times.
-> n [(Either Failure a, Trace)]
sctUniformRandomDiscard discard0 memtype0 g0 lim0 = sct (const (g0, max 0 lim0)) check step discard0 memtype0 where
check (_, 0) = Nothing
check s = Just s
step _ (g, n) run = do
(res, s, trace) <- run
(randSched $ \g' -> (1, g'))
(initialRandSchedState Nothing g)
pure ((schedGen s, n-1), Just (res, trace))
sctUniformRandomDiscard discard memtype g lim = runSCTWithSettings $
set ldiscard (Just discard) (fromWayAndMemType (uniformly g lim) memtype)
{-# DEPRECATED sctUniformRandomDiscard "Use runSCTWithSettings instead" #-}
-- | SCT via weighted random scheduling.
--
@ -581,6 +481,7 @@ sctWeightedRandom :: (MonadConc n, MonadRef r n, RandomGen g)
-- ^ The computation to run many times.
-> n [(Either Failure a, Trace)]
sctWeightedRandom = sctWeightedRandomDiscard (const Nothing)
{-# DEPRECATED sctWeightedRandom "Use runSCT instead" #-}
-- | A variant of 'sctWeightedRandom' which can selectively discard
-- results.
@ -602,48 +503,48 @@ sctWeightedRandomDiscard :: (MonadConc n, MonadRef r n, RandomGen g)
-> ConcT r n a
-- ^ The computation to run many times.
-> n [(Either Failure a, Trace)]
sctWeightedRandomDiscard discard0 memtype0 g0 lim0 use0 = sct (const (g0, max 0 lim0, max 1 use0, M.empty)) check step discard0 memtype0 where
check (_, 0, _, _) = Nothing
check s = Just s
step s (g, n, 0, _) run = step s (g, n, max 1 use0, M.empty) run
step _ (g, n, use, ws) run = do
(res, s, trace) <- run
(randSched $ randomR (1, 50))
(initialRandSchedState (Just ws) g)
pure ((schedGen s, n-1, use-1, schedWeights s), Just (res, trace))
sctWeightedRandomDiscard discard memtype g lim use = runSCTWithSettings $
set ldiscard (Just discard) (fromWayAndMemType (swarmy g lim use) memtype)
{-# DEPRECATED sctWeightedRandomDiscard "Use runSCTWithSettings instead" #-}
-- | General-purpose SCT function.
sct :: (MonadConc n, MonadRef r n)
=> ([ThreadId] -> s)
=> Settings n a
-- ^ The SCT settings ('Way' is ignored)
-> ([ThreadId] -> s)
-- ^ Initial state
-> (s -> Maybe t)
-- ^ State predicate
-> (s -> t -> (Scheduler g -> g -> n (Either Failure a, g, Trace)) -> n (s, Maybe (Either Failure a, Trace)))
-- ^ Run the computation and update the state
-> (Either Failure a -> Maybe Discard)
-> MemType
-> ConcT r n a
-> n [(Either Failure a, Trace)]
sct s0 sfun srun discard memtype conc
sct settings s0 sfun srun conc
| canDCSnapshot conc = runForDCSnapshot conc >>= \case
Just (Right snap, _) -> go (runSnap snap) (fst (threadsFromDCSnapshot snap))
Just (Left f, trace) -> pure [(Left f, trace)]
_ -> fatal "sct" "Failed to construct snapshot"
_ -> do
debugPrint "Failed to construct snapshot, continuing without."
go runFull [initialThread]
| otherwise = go runFull [initialThread]
where
go run = go' . s0 where
go' !s = case sfun s of
go run = go' Nothing . s0 where
go' (Just res) _ | earlyExit res = pure []
go' _ !s = case sfun s of
Just t -> srun s t run >>= \case
(s', Just (res, trace)) -> case discard res of
Just DiscardResultAndTrace -> go' s'
Just DiscardTrace -> ((res, []):) <$> go' s'
Nothing -> ((res, trace):) <$> go' s'
(s', Nothing) -> go' s'
Just DiscardResultAndTrace -> go' (Just res) s'
Just DiscardTrace -> ((res, []):) <$> go' (Just res) s'
Nothing -> ((res, trace):) <$> go' (Just res) s'
(s', Nothing) -> go' Nothing s'
Nothing -> pure []
runFull sched s = runConcurrent sched memtype s conc
runSnap snap sched s = runWithDCSnapshot sched memtype s snap
runFull sched s = runConcurrent sched (_memtype settings) s conc
runSnap snap sched s = runWithDCSnapshot sched (_memtype settings) s snap
debugPrint = fromMaybe (const (pure ())) (_debugPrint settings)
earlyExit = fromMaybe (const False) (_earlyExit settings)
discard = fromMaybe (const Nothing) (_discard settings)
-------------------------------------------------------------------------------
-- Utilities

398
dejafu/Test/DejaFu/Settings.hs Normal file
View File

@ -0,0 +1,398 @@
{-# LANGUAGE RankNTypes #-}
-- |
-- Module : Test.DejaFu.Settings
-- Copyright : (c) 2018 Michael Walker
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : experimental
-- Portability : RankNTypes
--
-- Configuration for the SCT functions.
module Test.DejaFu.Settings
( -- * SCT configuration
Settings
, defaultSettings
, fromWayAndMemType
-- ** The @Way@
, Way
, defaultWay
, lway
, systematically
, randomly
, uniformly
, swarmy
-- *** Schedule bounds
-- | Schedule bounding is used by the 'systematically' approach to
-- limit the search-space, which in general will be huge.
--
-- There are three types of bound:
--
-- * The 'PreemptionBound', which bounds the number of pre-emptive
-- context switches. Empirical evidence suggests @2@ is a good
-- value for this, if you have a small test case.
--
-- * The 'FairBound', which bounds the difference between how many
-- times threads can yield. This is necessary to test certain
-- kinds of potentially non-terminating behaviour, such as
-- spinlocks.
--
-- * The 'LengthBound', which bounds how long a test case can run,
-- in terms of scheduling decisions. This is necessary to test
-- certain kinds of potentially non-terminating behaviour, such
-- as livelocks.
--
-- Schedule bounding is not used by the non-systematic exploration
-- behaviours.
, Bounds(..)
, PreemptionBound(..)
, FairBound(..)
, LengthBound(..)
, defaultBounds
, defaultPreemptionBound
, defaultFairBound
, defaultLengthBound
, noBounds
-- ** The @MemType@
-- | When executed on a multi-core processor some @CRef@ / @IORef@
-- programs can exhibit \"relaxed memory\" behaviours, where the
-- apparent behaviour of the program is not a simple interleaving of
-- the actions of each thread.
--
-- __Example:__ This is a simple program which creates two @CRef@s
-- containing @False@, and forks two threads. Each thread writes
-- @True@ to one of the @CRef@s and reads the other. The value that
-- each thread reads is communicated back through an @MVar@:
--
-- > >>> :{
-- > let relaxed = do
-- > r1 <- newCRef False
-- > r2 <- newCRef False
-- > x <- spawn $ writeCRef r1 True >> readCRef r2
-- > y <- spawn $ writeCRef r2 True >> readCRef r1
-- > (,) <$> readMVar x <*> readMVar y
-- > :}
--
-- We see something surprising if we ask for the results:
--
-- > >>> autocheck relaxed
-- > [pass] Never Deadlocks
-- > [pass] No Exceptions
-- > [fail] Consistent Result
-- > (False,True) S0---------S1----S0--S2----S0--
-- >
-- > (False,False) S0---------S1--P2----S1--S0---
-- >
-- > (True,False) S0---------S2----S1----S0---
-- >
-- > (True,True) S0---------S1-C-S2----S1---S0---
-- > False
--
-- It's possible for both threads to read the value @False@, even
-- though each writes @True@ to the other @CRef@ before reading.
-- This is because processors are free to re-order reads and writes
-- to independent memory addresses in the name of performance.
--
-- Execution traces for relaxed memory computations can include
-- \"C\" actions, as above, which show where @CRef@ writes were
-- explicitly /committed/, and made visible to other threads.
--
-- However, modelling this behaviour can require more executions.
-- If you do not care about the relaxed-memory behaviour of your
-- program, use the 'SequentialConsistency' model.
, MemType(..)
, defaultMemType
, lmemtype
-- ** Discard functions
-- | Sometimes we know that a result is uninteresting and cannot
-- affect the result of a test, in which case there is no point in
-- keeping it around. Execution traces can be large, so any
-- opportunity to get rid of them early is possibly a great saving
-- of memory.
--
-- A discard function, which has type @Either Failure a -> Maybe
-- Discard@, can selectively discard results or execution traces
-- before the schedule exploration finishes, allowing them to be
-- garbage collected sooner.
--
-- __Note:__ The predicates and helper functions in Test.DejaFu come
-- with discard functions built in, to discard results and traces
-- wherever possible.
, Discard(..)
, ldiscard
-- ** Early exit
-- | Sometimes we don't want to wait for all executions to be
-- explored, we just want to stop as soon as a particular result is
-- found. An early-exit predicate, which has type @Either Failure a
-- -> Bool@, can opt to halt execution when such a result is found.
--
-- All results found up to, and including, the one which terminates
-- the exploration are reported.
--
-- __Usage in combination with a discard function:__ A discard
-- function can be used in combination with early-exit. As usual,
-- results or traces will be discarded as appropriate. If a single
-- result causes the early-exit function to return @True@ and the
-- discard function to return @Just DiscardResultAndTrace@, the
-- exploration will end early, but the result will not be included
-- in the output.
, learlyExit
-- ** Debug output
-- | You can opt to receive debugging messages by setting debugging
-- print and show functions. Enabling debugging doesn't change any
-- behaviour, it just causes messages to be printed. These options
-- are most likely not useful for anyone not developing dejafu.
, ldebugShow
, ldebugPrint
-- * Lens helpers
, get
, set
) where
import Control.Applicative (Const(..))
import Data.Functor.Identity (Identity(..))
import System.Random (RandomGen)
import Test.DejaFu.Internal (Settings(..), Way(..))
import Test.DejaFu.Types
-------------------------------------------------------------------------------
-- SCT configuration
-- | Default SCT settings: just combine all the other defaults.
--
-- @since 1.2.0.0
defaultSettings :: Applicative n => Settings n a
defaultSettings = fromWayAndMemType defaultWay defaultMemType
-- | Construct a 'Settings' record from a 'Way' and a 'MemType'.
--
-- All other settings take on their default values.
--
-- @since 1.2.0.0
fromWayAndMemType :: Applicative n => Way -> MemType -> Settings n a
fromWayAndMemType way memtype = Settings
{ _way = way
, _memtype = memtype
, _discard = Nothing
, _debugShow = Nothing
, _debugPrint = Nothing
, _earlyExit = Nothing
}
-------------------------------------------------------------------------------
-- The @Way@
-- | A default way to execute concurrent programs: systematically
-- using 'defaultBounds'.
--
-- @since 0.6.0.0
defaultWay :: Way
defaultWay = systematically defaultBounds
-- | A lens into the 'Way'.
--
-- @since 1.2.0.0
lway :: Lens' (Settings n a) Way
lway afb s = (\b -> s {_way = b}) <$> afb (_way s)
-- | Systematically execute a program, trying all distinct executions
-- within the bounds.
--
-- @since 0.7.0.0
systematically
:: Bounds
-- ^ The bounds to constrain the exploration.
-> Way
systematically = Systematic
-- | Randomly execute a program, exploring a fixed number of
-- executions.
--
-- Threads are scheduled by a weighted random selection, where weights
-- are assigned randomly on thread creation.
--
-- This is not guaranteed to find all distinct results (unlike
-- 'systematically').
--
-- @since 0.7.0.0
randomly :: RandomGen g
=> g
-- ^ The random generator to drive the scheduling.
-> Int
-- ^ The number of executions to try.
-> Way
randomly g lim = swarmy g lim 1
-- | Randomly execute a program, exploring a fixed number of
-- executions.
--
-- Threads are scheduled by a uniform random selection.
--
-- This is not guaranteed to find all distinct results (unlike
-- 'systematically').
--
-- @since 0.7.0.0
uniformly :: RandomGen g
=> g
-- ^ The random generator to drive the scheduling.
-> Int
-- ^ The number of executions to try.
-> Way
uniformly = Uniform
-- | Randomly execute a program, exploring a fixed number of
-- executions.
--
-- Threads are scheduled by a weighted random selection, where weights
-- are assigned randomly on thread creation.
--
-- This is not guaranteed to find all distinct results (unlike
-- 'systematically').
--
-- @since 0.7.0.0
swarmy :: RandomGen g
=> g
-- ^ The random generator to drive the scheduling.
-> Int
-- ^ The number of executions to try.
-> Int
-- ^ The number of executions to use the thread weights for.
-> Way
swarmy = Weighted
-------------------------------------------------------------------------------
-- Schedule bounds
-- | All bounds enabled, using their default values.
--
-- @since 0.2.0.0
defaultBounds :: Bounds
defaultBounds = Bounds
{ boundPreemp = Just defaultPreemptionBound
, boundFair = Just defaultFairBound
, boundLength = Just defaultLengthBound
}
-- | A sensible default preemption bound: 2.
--
-- See /Concurrency Testing Using Schedule Bounding: an Empirical Study/,
-- P. Thomson, A. F. Donaldson, A. Betts for justification.
--
-- @since 0.2.0.0
defaultPreemptionBound :: PreemptionBound
defaultPreemptionBound = 2
-- | A sensible default fair bound: 5.
--
-- This comes from playing around myself, but there is probably a
-- better default.
--
-- @since 0.2.0.0
defaultFairBound :: FairBound
defaultFairBound = 5
-- | A sensible default length bound: 250.
--
-- Based on the assumption that anything which executes for much
-- longer (or even this long) will take ages to test.
--
-- @since 0.2.0.0
defaultLengthBound :: LengthBound
defaultLengthBound = 250
-- | No bounds enabled. This forces the scheduler to just use
-- partial-order reduction and sleep sets to prune the search
-- space. This will /ONLY/ work if your computation always terminates!
--
-- @since 0.3.0.0
noBounds :: Bounds
noBounds = Bounds
{ boundPreemp = Nothing
, boundFair = Nothing
, boundLength = Nothing
}
-------------------------------------------------------------------------------
-- The @MemType@
-- | The default memory model: @TotalStoreOrder@
--
-- @since 0.2.0.0
defaultMemType :: MemType
defaultMemType = TotalStoreOrder
-- | A lens into the 'MemType'.
--
-- @since 1.2.0.0
lmemtype :: Lens' (Settings n a) MemType
lmemtype afb s = (\b -> s {_memtype = b}) <$> afb (_memtype s)
-------------------------------------------------------------------------------
-- Discard functions
-- | A lens into the discard function.
--
-- @since 1.2.0.0
ldiscard :: Lens' (Settings n a) (Maybe (Either Failure a -> Maybe Discard))
ldiscard afb s = (\b -> s {_discard = b}) <$> afb (_discard s)
-------------------------------------------------------------------------------
-- Early exit
-- | A lens into the early-exit predicate.
--
-- @since 1.2.0.0
learlyExit :: Lens' (Settings n a) (Maybe (Either Failure a -> Bool))
learlyExit afb s = (\b -> s {_earlyExit = b}) <$> afb (_earlyExit s)
-------------------------------------------------------------------------------
-- Debug output
-- | A lens into the debug 'show' function.
--
-- @since 1.2.0.0
ldebugShow :: Lens' (Settings n a) (Maybe (a -> String))
ldebugShow afb s = (\b -> s {_debugShow = b}) <$> afb (_debugShow s)
-- | A lens into the debug 'print' function.
--
-- @since 1.2.0.0
ldebugPrint :: Lens' (Settings n a) (Maybe (String -> n ()))
ldebugPrint afb s = (\b -> s {_debugPrint = b}) <$> afb (_debugPrint s)
-------------------------------------------------------------------------------
-- Lens helpers
-- lens type synonyms, unexported
type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t
type Lens' s a = Lens s s a a
-- | Get a value from a lens.
--
-- @since 1.2.0.0
get :: Lens' s a -> s -> a
get lens = getConst . lens Const
-- | Set a value in a lens.
--
-- @since 1.2.0.0
set :: Lens' s a -> a -> s -> s
set lens a = runIdentity . lens (\_ -> Identity a)

59
dejafu/Test/DejaFu/Types.hs
View File

@ -490,6 +490,65 @@ isIllegalDontCheck :: Failure -> Bool
isIllegalDontCheck IllegalDontCheck = True
isIllegalDontCheck _ = False
-------------------------------------------------------------------------------
-- * Schedule bounding
-- | @since 0.2.0.0
data Bounds = Bounds
{ boundPreemp :: Maybe PreemptionBound
, boundFair :: Maybe FairBound
, boundLength :: Maybe LengthBound
} deriving (Eq, Ord, Read, Show)
-- | @since 0.5.1.0
instance NFData Bounds where
rnf bs = rnf ( boundPreemp bs
, boundFair bs
, boundLength bs
)
-- | Restrict the number of pre-emptive context switches allowed in an
-- execution.
--
-- A pre-emption bound of zero disables pre-emptions entirely.
--
-- @since 0.2.0.0
newtype PreemptionBound = PreemptionBound Int
deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show)
-- | @since 0.5.1.0
instance NFData PreemptionBound where
-- not derived, so it can have a separate @since annotation
rnf (PreemptionBound i) = rnf i
-- | Restrict the maximum difference between the number of yield or
-- delay operations different threads have performed.
--
-- A fair bound of zero disables yields and delays entirely.
--
-- @since 0.2.0.0
newtype FairBound = FairBound Int
deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show)
-- | @since 0.5.1.0
instance NFData FairBound where
-- not derived, so it can have a separate @since annotation
rnf (FairBound i) = rnf i
-- | Restrict the maximum length (in terms of primitive actions) of an
-- execution.
--
-- A length bound of zero immediately aborts the execution.
--
-- @since 0.2.0.0
newtype LengthBound = LengthBound Int
deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show)
-- | @since 0.5.1.0
instance NFData LengthBound where
-- not derived, so it can have a separate @since annotation
rnf (LengthBound i) = rnf i
-------------------------------------------------------------------------------
-- * Discarding results and traces

5
dejafu/dejafu.cabal
View File

@ -2,7 +2,7 @@
-- documentation, see http://haskell.org/cabal/users-guide/
name: dejafu
version: 1.1.0.2
version: 1.2.0.0
synopsis: A library for unit-testing concurrent programs.
description:
@ -33,7 +33,7 @@ source-repository head
source-repository this
type: git
location: https://github.com/barrucadu/dejafu.git
tag: dejafu-1.1.0.2
tag: dejafu-1.2.0.0
library
exposed-modules: Test.DejaFu
@ -41,6 +41,7 @@ library
, Test.DejaFu.Defaults
, Test.DejaFu.Refinement
, Test.DejaFu.SCT
, Test.DejaFu.Settings
, Test.DejaFu.Schedule
, Test.DejaFu.Types
, Test.DejaFu.Utils

6
doc/getting_started.rst
View File

@ -28,9 +28,9 @@ There are a few different packages under the Déjà Fu umbrella:
:header: "Package", "Version", "Summary"
":hackage:`concurrency`", "1.4.0.1", "Typeclasses, functions, and data types for concurrency and STM"
":hackage:`dejafu`", "1.1.0.2", "Systematic testing for Haskell concurrency"
":hackage:`hunit-dejafu`", "1.0.1.2", "Déjà Fu support for the HUnit test framework"
":hackage:`tasty-dejafu`", "1.0.1.1", "Déjà Fu support for the tasty test framework"
":hackage:`dejafu`", "1.2.0.0", "Systematic testing for Haskell concurrency"
":hackage:`hunit-dejafu`", "1.1.0.0", "Déjà Fu support for the HUnit test framework"
":hackage:`tasty-dejafu`", "1.1.0.0", "Déjà Fu support for the tasty test framework"
Installation

15
doc/release_process.rst
View File

@ -26,22 +26,25 @@ Release Process
**If it's early in the year (like January or February), make sure
you don't put down the wrong year.**
* Add the git tag name and a link to where it will be on github
* Add the git tag name
* Add the Hackage URL
* Add the contributors list
7. Commit.
8. Push to GitHub and wait for Travis to confirm everything is OK. If
it's not OK, fix what is broken before continuing.
9. Tag. Tags are in the form ``<package>-<version>``, and the message
is the changelog entry.
9. Merge the PR.
10. Push tags to GitHub.
10. Tag the merge commit. Tags are in the form
``<package>-<version>``, and the message is the changelog entry.
11. Upload updated packages to Hackage.
11. Push tags to GitHub.
See :commit:`44181e6` and :tag:`dejafu-0.7.1.3` if any of this is
12. Upload updated packages to Hackage.
See :commit:`75a02b9` and :tag:`dejafu-1.1.0.1` if any of this is
unclear.
.. _PVP: https://pvp.haskell.org/

34
hunit-dejafu/CHANGELOG.rst
View File

@ -6,6 +6,40 @@ standard Haskell versioning scheme.
.. _PVP: https://pvp.haskell.org/
1.1.0.0 - The Settings Release (2018-03-06)
-------------------------------------------
* Git: :tag:`hunit-dejafu-1.1.0.0`
* Hackage: :hackage:`hunit-dejafu-1.1.0.0`
Added
~~~~~
* (:pull:`238`) Settings-based test functions:
* ``Test.HUnit.DejaFu.testAutoWithSettings``
* ``Test.HUnit.DejaFu.testDejafuWithSettings``
* ``Test.HUnit.DejaFu.testDejafusWithSettings``
* (:pull:`238`) Re-export of ``Test.DejaFu.Settings``.
Deprecated
~~~~~~~~~~
* (:pull:`238`) ``Test.HUnit.DejaFu.testDejafuDiscard`` and
``testDejafusDiscard``.
Removed
~~~~~~~
* (:pull:`238`) The re-export of
``Test.DejaFu.Defaults.defaultDiscarder``.
Miscellaneous
~~~~~~~~~~~~~
* The version bounds on :hackage:`dejafu` are >=1.2 && <1.3.
1.0.1.2 (2018-02-26)
--------------------

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

@ -5,7 +5,7 @@
-- |
-- Module : Test.HUnit.DejaFu
-- Copyright : (c) 2015--2017 Michael Walker
-- Copyright : (c) 2015--2018 Michael Walker
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : stable
@ -34,23 +34,14 @@ module Test.HUnit.DejaFu
, testDejafuWay
, testDejafusWay
, testDejafuDiscard
, testAutoWithSettings
, testDejafuWithSettings
, testDejafusWithSettings
-- ** Re-exports
, Predicate
, ProPredicate(..)
, Way
, defaultWay
, systematically
, randomly
, uniformly
, swarmy
, Bounds(..)
, defaultBounds
, MemType(..)
, defaultMemType
, Discard(..)
, defaultDiscarder
, module Test.DejaFu.Settings
-- * Refinement property testing
, testProperty
@ -65,6 +56,10 @@ module Test.HUnit.DejaFu
, R.refines, (R.=>=)
, R.strictlyRefines, (R.->-)
, R.equivalentTo, (R.===)
-- * Deprecated
, testDejafuDiscard
, testDejafusDiscard
) where
import Control.Monad.Catch (try)
@ -74,6 +69,7 @@ import Test.DejaFu hiding (Testable(..))
import qualified Test.DejaFu.Conc as Conc
import qualified Test.DejaFu.Refinement as R
import qualified Test.DejaFu.SCT as SCT
import qualified Test.DejaFu.Settings
import qualified Test.DejaFu.Types as D
import Test.HUnit (Assertable(..), Test(..), Testable(..),
assertFailure, assertString)
@ -89,7 +85,7 @@ instance Testable (Conc.ConcIO ()) where
-- | @since 0.3.0.0
instance Assertable (Conc.ConcIO ()) where
assert conc = do
traces <- SCT.runSCTDiscard (pdiscard assertableP) defaultWay defaultMemType (try conc)
traces <- SCT.runSCTWithSettings (set ldiscard (Just (pdiscard assertableP)) defaultSettings) (try conc)
assertString . showErr $ peval assertableP traces
assertableP :: Predicate (Either HUnitFailure ())
@ -109,7 +105,7 @@ testAuto :: (Eq a, Show a)
=> Conc.ConcIO a
-- ^ The computation to test.
-> Test
testAuto = testAutoWay defaultWay defaultMemType
testAuto = testAutoWithSettings defaultSettings
-- | Variant of 'testAuto' which tests a computation under a given
-- execution way and memory model.
@ -123,11 +119,18 @@ testAutoWay :: (Eq a, Show a)
-> Conc.ConcIO a
-- ^ The computation to test.
-> Test
testAutoWay way memtype = testDejafusWay way memtype autocheckCases
testAutoWay way = testAutoWithSettings . fromWayAndMemType way
-- | Predicates for the various autocheck functions.
autocheckCases :: Eq a => [(String, Predicate a)]
autocheckCases =
-- | Variant of 'testAuto' which takes a settings record.
--
-- @since 1.1.0.0
testAutoWithSettings :: (Eq a, Show a)
=> Settings IO a
-- ^ The SCT settings.
-> Conc.ConcIO a
-- ^ The computation to test.
-> Test
testAutoWithSettings settings = testDejafusWithSettings settings
[("Never Deadlocks", representative deadlocksNever)
, ("No Exceptions", representative exceptionsNever)
, ("Consistent Result", alwaysSame)
@ -144,7 +147,7 @@ testDejafu :: Show b
-> Conc.ConcIO a
-- ^ The computation to test.
-> Test
testDejafu = testDejafuWay defaultWay defaultMemType
testDejafu = testDejafuWithSettings defaultSettings
-- | Variant of 'testDejafu' which takes a way to execute the program
-- and a memory model.
@ -162,7 +165,22 @@ testDejafuWay :: Show b
-> Conc.ConcIO a
-- ^ The computation to test.
-> Test
testDejafuWay = testDejafuDiscard (const Nothing)
testDejafuWay way = testDejafuWithSettings . fromWayAndMemType way
-- | Variant of 'testDejafu' which takes a settings record.
--
-- @since 1.1.0.0
testDejafuWithSettings :: Show b
=> Settings IO a
-- ^ The SCT settings.
-> String
-- ^ The name of the test.
-> ProPredicate a b
-- ^ The predicate to check.
-> Conc.ConcIO a
-- ^ The computation to test.
-> Test
testDejafuWithSettings settings name p = testDejafusWithSettings settings [(name, p)]
-- | Variant of 'testDejafuWay' which can selectively discard results.
--
@ -181,8 +199,9 @@ testDejafuDiscard :: Show b
-> Conc.ConcIO a
-- ^ The computation to test.
-> Test
testDejafuDiscard discard way memtype name test =
testconc discard way memtype [(name, test)]
testDejafuDiscard discard way =
testDejafuWithSettings . set ldiscard (Just discard) . fromWayAndMemType way
{-# DEPRECATED testDejafuDiscard "Use testDejafuWithSettings instead" #-}
-- | Variant of 'testDejafu' which takes a collection of predicates to
-- test. This will share work between the predicates, rather than
@ -195,7 +214,7 @@ testDejafus :: Show b
-> Conc.ConcIO a
-- ^ The computation to test.
-> Test
testDejafus = testDejafusWay defaultWay defaultMemType
testDejafus = testDejafusWithSettings defaultSettings
-- | Variant of 'testDejafus' which takes a way to execute the program
-- and a memory model.
@ -211,7 +230,20 @@ testDejafusWay :: Show b
-> Conc.ConcIO a
-- ^ The computation to test.
-> Test
testDejafusWay = testconc (const Nothing)
testDejafusWay way = testDejafusWithSettings . fromWayAndMemType way
-- | Variant of 'testDejafus' which takes a settings record.
--
-- @since 1.1.0.0
testDejafusWithSettings :: Show b
=> Settings IO a
-- ^ The SCT settings.
-> [(String, ProPredicate a b)]
-- ^ The list of predicates (with names) to check.
-> Conc.ConcIO a
-- ^ The computation to test.
-> Test
testDejafusWithSettings = testconc
-- | Variant of 'testDejafusWay' which can selectively discard
-- results, beyond what each predicate already discards.
@ -229,7 +261,9 @@ testDejafusDiscard :: Show b
-> Conc.ConcIO a
-- ^ The computation to test.
-> Test
testDejafusDiscard = testconc
testDejafusDiscard discard way =
testDejafusWithSettings . set ldiscard (Just discard) . fromWayAndMemType way
{-# DEPRECATED testDejafusDiscard "Use testDejafusWithSettings instead" #-}
-------------------------------------------------------------------------------
@ -271,20 +305,18 @@ testPropertyFor = testprop
-- | Produce a HUnit 'Test' from a Deja Fu unit test.
testconc :: Show b
=> (Either Failure a -> Maybe Discard)
-> Way
-> MemType
=> Settings IO a
-> [(String, ProPredicate a b)]
-> Conc.ConcIO a
-> Test
testconc discard way memtype tests concio = case map toTest tests of
testconc settings tests concio = case map toTest tests of
[t] -> t
ts -> TestList ts
where
toTest (name, p) = TestLabel name . TestCase $ do
let discarder = D.strengthenDiscard discard (pdiscard p)
traces <- SCT.runSCTDiscard discarder way memtype concio
let discarder = maybe id D.strengthenDiscard (get ldiscard settings) (pdiscard p)
traces <- SCT.runSCTWithSettings (set ldiscard (Just discarder) settings) concio
assertString . showErr $ peval p traces
-- | Produce a HUnit 'Test' from a Deja Fu refinement property test.

6
hunit-dejafu/hunit-dejafu.cabal
View File

@ -2,7 +2,7 @@
-- documentation, see http://haskell.org/cabal/users-guide/
name: hunit-dejafu
version: 1.0.1.2
version: 1.1.0.0
synopsis: Deja Fu support for the HUnit test framework.
description:
@ -30,7 +30,7 @@ source-repository head
source-repository this
type: git
location: https://github.com/barrucadu/dejafu.git
tag: hunit-dejafu-1.0.1.2
tag: hunit-dejafu-1.1.0.0
library
exposed-modules: Test.HUnit.DejaFu
@ -38,7 +38,7 @@ library
-- other-extensions:
build-depends: base >=4.8 && <5
, exceptions >=0.7 && <0.10
, dejafu >=1.0 && <1.2
, dejafu >=1.2 && <1.3
, HUnit >=1.2 && <1.7
-- hs-source-dirs:
default-language: Haskell2010

34
tasty-dejafu/CHANGELOG.rst
View File

@ -6,6 +6,40 @@ standard Haskell versioning scheme.
.. _PVP: https://pvp.haskell.org/
1.1.0.0 - The Settings Release (2018-03-06)
-------------------------------------------
* Git: :tag:`tasty-dejafu-1.1.0.0`
* Hackage: :hackage:`tasty-dejafu-1.1.0.0`
Added
~~~~~
* (:pull:`238`) Settings-based test functions:
* ``Test.Tasty.DejaFu.testAutoWithSettings``
* ``Test.Tasty.DejaFu.testDejafuWithSettings``
* ``Test.Tasty.DejaFu.testDejafusWithSettings``
* (:pull:`238`) Re-export of ``Test.DejaFu.Settings``.
Deprecated
~~~~~~~~~~
* (:pull:`238`) ``Test.Tasty.DejaFu.testDejafuDiscard`` and
``testDejafusDiscard``.
Removed
~~~~~~~
* (:pull:`238`) The re-export of
``Test.DejaFu.Defaults.defaultDiscarder``.
Miscellaneous
~~~~~~~~~~~~~
* The version bounds on :hackage:`dejafu` are >=1.2 && <1.3.
1.0.1.1 (2018-02-22)
--------------------

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

@ -6,7 +6,7 @@
-- |
-- Module : Test.Tasty.DejaFu
-- Copyright : (c) 2015--2017 Michael Walker
-- Copyright : (c) 2015--2018 Michael Walker
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : stable
@ -34,24 +34,14 @@ module Test.Tasty.DejaFu
, testDejafuWay
, testDejafusWay
, testDejafuDiscard
, testDejafusDiscard
, testAutoWithSettings
, testDejafuWithSettings
, testDejafusWithSettings
-- ** Re-exports
, Predicate
, ProPredicate(..)
, Way
, defaultWay
, systematically
, randomly
, uniformly
, swarmy
, Bounds(..)
, defaultBounds
, MemType(..)
, defaultMemType
, Discard(..)
, defaultDiscarder
, module Test.DejaFu.Settings
-- * Refinement property testing
, testProperty
@ -66,7 +56,11 @@ module Test.Tasty.DejaFu
, R.refines, (R.=>=)
, R.strictlyRefines, (R.->-)
, R.equivalentTo, (R.===)
) where
-- * Deprecated
, testDejafuDiscard
, testDejafusDiscard
) where
import Data.Char (toUpper)
import qualified Data.Foldable as F
@ -79,6 +73,7 @@ import Test.DejaFu hiding (Testable(..))
import qualified Test.DejaFu.Conc as Conc
import qualified Test.DejaFu.Refinement as R
import qualified Test.DejaFu.SCT as SCT
import qualified Test.DejaFu.Settings
import qualified Test.DejaFu.Types as D
import Test.Tasty (TestName, TestTree, testGroup)
import Test.Tasty.Options (IsOption(..), OptionDescription(..),
@ -96,7 +91,7 @@ instance IsTest (Conc.ConcIO (Maybe String)) where
run options conc callback = do
let memtype = lookupOption options
let way = lookupOption options
let traces = SCT.runSCTDiscard (pdiscard assertableP) way memtype conc
let traces = SCT.runSCTWithSettings (set ldiscard (Just (pdiscard assertableP)) (fromWayAndMemType way memtype)) conc
run options (ConcTest traces (peval assertableP)) callback
concOptions :: [OptionDescription]
@ -143,7 +138,7 @@ testAuto :: (Eq a, Show a)
=> Conc.ConcIO a
-- ^ The computation to test.
-> TestTree
testAuto = testAutoWay defaultWay defaultMemType
testAuto = testAutoWithSettings defaultSettings
-- | Variant of 'testAuto' which tests a computation under a given
-- execution way and memory model.
@ -157,11 +152,18 @@ testAutoWay :: (Eq a, Show a)
-> Conc.ConcIO a
-- ^ The computation to test.
-> TestTree
testAutoWay way memtype = testDejafusWay way memtype autocheckCases
testAutoWay way = testAutoWithSettings . fromWayAndMemType way
-- | Predicates for the various autocheck functions.
autocheckCases :: Eq a => [(TestName, Predicate a)]
autocheckCases =
-- | Variant of 'testAuto' which takes a settings record.
--
-- @since 1.1.0.0
testAutoWithSettings :: (Eq a, Show a)
=> Settings IO a
-- ^ The SCT settings.
-> Conc.ConcIO a
-- ^ The computation to test.
-> TestTree
testAutoWithSettings settings = testDejafusWithSettings settings
[("Never Deadlocks", representative deadlocksNever)
, ("No Exceptions", representative exceptionsNever)
, ("Consistent Result", alwaysSame)
@ -178,7 +180,7 @@ testDejafu :: Show b
-> Conc.ConcIO a
-- ^ The computation to test.
-> TestTree
testDejafu = testDejafuWay defaultWay defaultMemType
testDejafu = testDejafuWithSettings defaultSettings
-- | Variant of 'testDejafu' which takes a way to execute the program
-- and a memory model.
@ -196,7 +198,22 @@ testDejafuWay :: Show b
-> Conc.ConcIO a
-- ^ The computation to test.
-> TestTree
testDejafuWay = testDejafuDiscard (const Nothing)
testDejafuWay way = testDejafuWithSettings . fromWayAndMemType way
-- | Variant of 'testDejafu' which takes a settings record.
--
-- @since 1.1.0.0
testDejafuWithSettings :: Show b
=> Settings IO a
-- ^ The settings record
-> TestName
-- ^ The name of the test.
-> ProPredicate a b
-- ^ The predicate to check.
-> Conc.ConcIO a
-- ^ The computation to test.
-> TestTree
testDejafuWithSettings settings name p = testDejafusWithSettings settings [(name, p)]
-- | Variant of 'testDejafuWay' which can selectively discard results.
--
@ -215,8 +232,9 @@ testDejafuDiscard :: Show b
-> Conc.ConcIO a
-- ^ The computation to test.
-> TestTree
testDejafuDiscard discard way memtype name test =
testconc discard way memtype [(name, test)]
testDejafuDiscard discard way =
testDejafuWithSettings . set ldiscard (Just discard) . fromWayAndMemType way
{-# DEPRECATED testDejafuDiscard "Use testDejafuWithSettings instead" #-}
-- | Variant of 'testDejafu' which takes a collection of predicates to
-- test. This will share work between the predicates, rather than
@ -229,7 +247,7 @@ testDejafus :: Show b
-> Conc.ConcIO a
-- ^ The computation to test.
-> TestTree
testDejafus = testDejafusWay defaultWay defaultMemType
testDejafus = testDejafusWithSettings defaultSettings
-- | Variant of 'testDejafus' which takes a way to execute the program
-- and a memory model.
@ -245,7 +263,20 @@ testDejafusWay :: Show b
-> Conc.ConcIO a
-- ^ The computation to test.
-> TestTree
testDejafusWay = testconc (const Nothing)
testDejafusWay way = testDejafusWithSettings . fromWayAndMemType way
-- | Variant of 'testDejafus' which takes a settings record.
--
-- @since 1.1.0.0
testDejafusWithSettings :: Show b
=> Settings IO a
-- ^ The SCT settings.
-> [(TestName, ProPredicate a b)]
-- ^ The list of predicates (with names) to check.
-> Conc.ConcIO a
-- ^ The computation to test.
-> TestTree
testDejafusWithSettings = testconc
-- | Variant of 'testDejafusWay' which can selectively discard
-- results, beyond what each predicate already discards.
@ -263,7 +294,9 @@ testDejafusDiscard :: Show b
-> Conc.ConcIO a
-- ^ The computation to test.
-> TestTree
testDejafusDiscard = testconc
testDejafusDiscard discard way =
testDejafusWithSettings . set ldiscard (Just discard) . fromWayAndMemType way
{-# DEPRECATED testDejafusDiscard "Use testDejafusWithSettings instead" #-}
-------------------------------------------------------------------------------
@ -336,20 +369,18 @@ instance IsTest PropTest where
-- | Produce a Tasty 'Test' from a Deja Fu unit test.
testconc :: Show b
=> (Either Failure a -> Maybe Discard)
-> Way
-> MemType
=> Settings IO a
-> [(TestName, ProPredicate a b)]
-> Conc.ConcIO a
-> TestTree
testconc discard way memtype tests concio = case map toTest tests of
testconc settings tests concio = case map toTest tests of
[t] -> t
ts -> testGroup "Deja Fu Tests" ts
where
toTest (name, p) =
let discarder = D.strengthenDiscard discard (pdiscard p)
traces = SCT.runSCTDiscard discarder way memtype concio
let discarder = maybe id D.strengthenDiscard (get ldiscard settings) (pdiscard p)
traces = SCT.runSCTWithSettings (set ldiscard (Just discarder) settings) concio
in singleTest name $ ConcTest traces (peval p)
-- | Produce a Tasty 'TestTree' from a Deja Fu refinement property test.

6
tasty-dejafu/tasty-dejafu.cabal
View File

@ -2,7 +2,7 @@
-- documentation, see http://haskell.org/cabal/users-guide/
name: tasty-dejafu
version: 1.0.1.1
version: 1.1.0.0
synopsis: Deja Fu support for the Tasty test framework.
description:
@ -30,14 +30,14 @@ source-repository head
source-repository this
type: git
location: https://github.com/barrucadu/dejafu.git
tag: tasty-dejafu-1.0.1.1
tag: tasty-dejafu-1.1.0.0
library
exposed-modules: Test.Tasty.DejaFu
-- other-modules:
-- other-extensions:
build-depends: base >=4.8 && <5
, dejafu >=1.0 && <1.2
, dejafu >=1.2 && <1.3
, random >=1.0 && <1.2
, tagged >=0.8 && <0.9
, tasty >=0.10 && <1.1