dejafu 1.1.0.2 → 1.2.0.0
raw patch · 9 files changed
+882/−484 lines, 9 files
Files
- CHANGELOG.rst +68/−0
- Test/DejaFu.hs +135/−161
- Test/DejaFu/Defaults.hs +11/−60
- Test/DejaFu/Internal.hs +48/−2
- Test/DejaFu/Refinement.hs +1/−1
- Test/DejaFu/SCT.hs +159/−258
- Test/DejaFu/Settings.hs +398/−0
- Test/DejaFu/Types.hs +59/−0
- dejafu.cabal +3/−2
CHANGELOG.rst view
@@ -6,6 +6,74 @@ .. _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) --------------------
Test/DejaFu.hs view
@@ -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 @@ 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-- -- *** 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.---}+ , autocheckWithSettings+ , dejafuWithSettings+ , dejafusWithSettings - , Discard(..)+ , module Test.DejaFu.Settings -- ** Manual testing @@ -391,6 +263,9 @@ -} , module Test.DejaFu.Refinement++ -- * Deprecated+ , dejafuDiscard ) where import Control.Arrow (first)@@ -407,9 +282,9 @@ 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 @@ => 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 @@ -> 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 @@ -> 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,8 +469,33 @@ -> 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. -- -- >>> dejafuDiscard (\_ -> Just DiscardTrace) defaultWay defaultMemType "Discarding" alwaysSame example@@ -589,10 +520,9 @@ -> 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 @@ -> 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 @@ -> 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 @@ -- 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 @@ -> 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 @@ -> 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 -------------------------------------------------------------------------------
Test/DejaFu/Defaults.hs view
@@ -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--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+module Test.DejaFu.Defaults {-# DEPRECATED "Import Test.DejaFu.Settings instead" #-}+ ( defaultSettings+ , defaultWay+ , defaultBounds+ , defaultPreemptionBound+ , defaultFairBound+ , defaultLengthBound+ , defaultMemType+ ) where --- | 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
Test/DejaFu/Internal.hs view
@@ -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,10 +20,39 @@ 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 -- | The number of ID parameters was getting a bit unwieldy, so this@@ -105,6 +136,7 @@ _ -> [] where+ tvarsOf' (TNew tv) = [tv] tvarsOf' (TWrite tv) = [tv] tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) tvarsOf' (TCatch ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)@@ -262,6 +294,20 @@ mvarOf (SynchronisedRead c) = Just c mvarOf (SynchronisedWrite c) = Just c mvarOf _ = Nothing++-- | Get the @ThreadId@s involved in a @ThreadAction@.+tidsOf :: ThreadAction -> Set ThreadId+tidsOf (Fork tid) = S.singleton tid+tidsOf (ForkOS tid) = S.singleton tid+tidsOf (PutMVar _ tids) = S.fromList tids+tidsOf (TryPutMVar _ _ tids) = S.fromList tids+tidsOf (TakeMVar _ tids) = S.fromList tids+tidsOf (TryTakeMVar _ _ tids) = S.fromList tids+tidsOf (CommitCRef tid _) = S.singleton tid+tidsOf (STM _ tids) = S.fromList tids+tidsOf (ThrowTo tid) = S.singleton tid+tidsOf (BlockedThrowTo tid) = S.singleton tid+tidsOf _ = S.empty -- | Throw away information from a 'ThreadAction' and give a -- simplified view of what is happening.
Test/DejaFu/Refinement.hs view
@@ -115,8 +115,8 @@ 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)
Test/DejaFu/SCT.hs view
@@ -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+ runSCT+ , runSCT' , resultsSet+ , resultsSet' - -- ** Discarding variants- , Discard(..)- , runSCTDiscard- , resultsSetDiscard+ -- ** Configuration+ , runSCTWithSettings+ , runSCTWithSettings'+ , resultsSetWithSettings+ , resultsSetWithSettings'+ , module Test.DejaFu.Settings - -- ** Strict variants- , runSCT'- , resultsSet'+ -- * 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.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 @@ -> 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 @@ -> 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 @@ -> 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 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 @@ -- @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 @@ -- @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' 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' discard way memtype conc = do res <- resultsSetDiscard discard way memtype conc rnf res `seq` pure res+{-# DEPRECATED resultsSetDiscard' "Use resultsSetWithSettings' instead" #-} ---------------------------------------------------------------------------------- Combined Bounds+-- Configuration --- | @since 0.2.0.0-data Bounds = Bounds- { boundPreemp :: Maybe PreemptionBound- , boundFair :: Maybe FairBound- , boundLength :: Maybe LengthBound- } deriving (Eq, Ord, Read, Show)+-- | 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 --- | @since 0.5.1.0-instance NFData Bounds where- rnf bs = rnf ( boundPreemp bs- , boundFair bs- , boundLength bs- )+ check = findSchedulePrefix --- | 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!+ 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 0.3.0.0-noBounds :: Bounds-noBounds = Bounds- { boundPreemp = Nothing- , boundFair = Nothing- , boundLength = Nothing- }+-- @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+ -- | 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 @@ ------------------------------------------------------------------------------- -- 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 @@ ------------------------------------------------------------------------------- -- 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 @@ ------------------------------------------------------------------------------- -- 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 @@ -- ^ 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 @@ -> 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 @@ -- ^ 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 @@ -> 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 @@ -- ^ 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 @@ -> 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
+ Test/DejaFu/Settings.hs view
@@ -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)
Test/DejaFu/Types.hs view
@@ -491,6 +491,65 @@ 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 -- | An @Either Failure a -> Maybe Discard@ value can be used to
dejafu.cabal view
@@ -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 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 @@ , Test.DejaFu.Defaults , Test.DejaFu.Refinement , Test.DejaFu.SCT+ , Test.DejaFu.Settings , Test.DejaFu.Schedule , Test.DejaFu.Types , Test.DejaFu.Utils