diff --git a/CHANGELOG.rst b/CHANGELOG.rst --- a/CHANGELOG.rst +++ b/CHANGELOG.rst @@ -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) -------------------- diff --git a/Test/DejaFu.hs b/Test/DejaFu.hs --- a/Test/DejaFu.hs +++ b/Test/DejaFu.hs @@ -4,7 +4,7 @@ {- | Module : Test.DejaFu -Copyright : (c) 2015--2017 Michael Walker +Copyright : (c) 2015--2018 Michael Walker License : MIT Maintainer : Michael Walker 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-- - - (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(..) - - -- *** 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-- +-- +-- (False,False) S0---------S1--P2----S1--S0--- +-- +-- (True,False) S0---------S2----S1----S0--- +-- +-- (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-- +-- +-- (True,True) S0---------S1-P2----S1---S0--- +-- +-- (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-- +-- +-- "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-- +-- +-- (True,True) S0---------S1-P2----S1---S0--- +-- +-- (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 ------------------------------------------------------------------------------- diff --git a/Test/DejaFu/Defaults.hs b/Test/DejaFu/Defaults.hs --- a/Test/DejaFu/Defaults.hs +++ b/Test/DejaFu/Defaults.hs @@ -1,69 +1,20 @@ -- | -- Module : Test.DejaFu.Defaults --- Copyright : (c) 2017 Michael Walker +-- Copyright : (c) 2017--2018 Michael Walker -- License : MIT -- Maintainer : Michael Walker -- 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 diff --git a/Test/DejaFu/Internal.hs b/Test/DejaFu/Internal.hs --- a/Test/DejaFu/Internal.hs +++ b/Test/DejaFu/Internal.hs @@ -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 -- 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 " ++ show (n, t) + show (Uniform _ n) = "Uniform " ++ 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. diff --git a/Test/DejaFu/Refinement.hs b/Test/DejaFu/Refinement.hs --- a/Test/DejaFu/Refinement.hs +++ b/Test/DejaFu/Refinement.hs @@ -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) diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -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 -- 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 " ++ show (n, t) - show (Uniform _ n) = "Uniform " ++ 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 diff --git a/Test/DejaFu/Settings.hs b/Test/DejaFu/Settings.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Settings.hs @@ -0,0 +1,398 @@ +{-# LANGUAGE RankNTypes #-} + +-- | +-- Module : Test.DejaFu.Settings +-- Copyright : (c) 2018 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- 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) diff --git a/Test/DejaFu/Types.hs b/Test/DejaFu/Types.hs --- a/Test/DejaFu/Types.hs +++ b/Test/DejaFu/Types.hs @@ -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 diff --git a/dejafu.cabal b/dejafu.cabal --- a/dejafu.cabal +++ b/dejafu.cabal @@ -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