From bdb1d82daeab7315310699cbf3fdbea77d44c439 Mon Sep 17 00:00:00 2001 From: Michael Walker Date: Sun, 4 Mar 2018 10:30:19 +0000 Subject: [PATCH] Add *WithSettings to Test.DejaFu and deprecate *Discard --- dejafu/CHANGELOG.rst | 12 +- dejafu/Test/DejaFu.hs | 280 +++++++++++++++------------------ dejafu/Test/DejaFu/Settings.hs | 87 ++++++++++ 3 files changed, 228 insertions(+), 151 deletions(-) diff --git a/dejafu/CHANGELOG.rst b/dejafu/CHANGELOG.rst index 9283fdc..8a4ffde 100644 --- a/dejafu/CHANGELOG.rst +++ b/dejafu/CHANGELOG.rst @@ -14,7 +14,8 @@ Added * (:issue:`221`) A record-based approach to SCT configuration: - * ``Test.DejaFu.Settings`` (re-exported from ``Test.DejaFu.SCT``) + * ``Test.DejaFu.Settings`` + (re-exported from ``Test.Dejafu`` and ``Test.DejaFu.SCT``) * ``Test.DejaFu.Settings.Settings`` * ``Test.DejaFu.Settings.defaultSettings`` * ``Test.DejaFu.Settings.fromWayAndMemType`` @@ -34,6 +35,13 @@ Added * ``Test.DejaFu.SCT.resultsSetWithSettings`` * ``Test.DejaFu.SCT.resultsSetWithSettings'`` +* (:issue:`221`) Settings-based test functions: + + * ``Test.DejaFu.autocheckWithSettings`` + * ``Test.DejaFu.dejafuWithSettings`` + * ``Test.DejaFu.dejafusWithSettings`` + * ``Test.DejaFu.runTestWithSettings`` + Deprecated ~~~~~~~~~~ @@ -53,6 +61,8 @@ Deprecated * (:issue:`221`) The ``Test.DejaFu.Defaults`` module. Import ``Test.DejaFu.Settings`` instead. +* (:issue:`221`) ``Test.DejaFu.dejafuDiscard``. + Removed ~~~~~~~ diff --git a/dejafu/Test/DejaFu.hs b/dejafu/Test/DejaFu.hs index 49a63c8..ad1d04f 100644 --- a/dejafu/Test/DejaFu.hs +++ b/dejafu/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 @@ -120,133 +120,11 @@ few tricks available. , autocheckWay , dejafuWay , dejafusWay - , dejafuDiscard + , autocheckWithSettings + , dejafuWithSettings + , dejafusWithSettings - -- *** Defaults - - , defaultWay - , defaultMemType - - -- *** 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. - --} - - , Discard(..) + , module Test.DejaFu.Settings -- ** Manual testing @@ -390,6 +268,9 @@ interference we have provided: the left term never empties a full -} , module Test.DejaFu.Refinement + + -- * Deprecated + , dejafuDiscard ) where import Control.Arrow (first) @@ -457,7 +338,7 @@ autocheck :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a) => ConcT r n a -- ^ The computation to test. -> n Bool -autocheck = autocheckWay defaultWay defaultMemType +autocheck = autocheckWithSettings defaultSettings -- | Variant of 'autocheck' which takes a way to run the program and a -- memory model. @@ -495,11 +376,42 @@ autocheckWay :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a) -> ConcT r n a -- ^ The computation to test. -> n Bool -autocheckWay way memtype = dejafusWay way memtype autocheckCases +autocheckWay way = autocheckWithSettings . fromWayAndMemType way --- | Predicates for the various autocheck functions. -autocheckCases :: Eq a => [(String, Predicate a)] -autocheckCases = +-- | Variant of 'autocheck' which takes a settings record. +-- +-- >>> autocheckWithSettings (fromWayAndMemType defaultWay defaultMemType) relaxed +-- [pass] Never Deadlocks +-- [pass] No Exceptions +-- [fail] Consistent Result +-- (False,True) S0---------S1----S0--S2----S0-- +-- +-- (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 unreleased +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 @@ -528,7 +440,7 @@ dejafu :: (MonadConc n, MonadIO n, MonadRef r n, Show b) -> ConcT r n a -- ^ The computation to test. -> n Bool -dejafu = dejafuWay defaultWay defaultMemType +dejafu = dejafuWithSettings defaultSettings -- | Variant of 'dejafu' which takes a way to run the program and a -- memory model. @@ -562,7 +474,32 @@ dejafuWay :: (MonadConc n, MonadIO n, MonadRef r n, Show b) -> ConcT r n a -- ^ The computation to test. -> n Bool -dejafuWay = dejafuDiscard (const Nothing) +dejafuWay way = dejafuWithSettings . fromWayAndMemType way + +-- | Variant of 'dejafu' which takes a settings record. +-- +-- >>> import System.Random +-- +-- >>> dejafuWithSettings (fromWayAndMemType (randomly (mkStdGen 1) 100) defaultMemType) "Randomly!" alwaysSame example +-- [fail] Randomly! +-- "hello" S0----S1--S0-- +-- +-- "world" S0----S2--S1-S0-- +-- False +-- +-- @since unreleased +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. -- @@ -588,10 +525,9 @@ dejafuDiscard :: (MonadConc n, MonadIO n, MonadRef r n, Show b) -> ConcT r n a -- ^ The computation to test. -> n Bool -dejafuDiscard discard way memtype name test conc = do - let discarder = strengthenDiscard discard (pdiscard test) - traces <- runSCTDiscard discarder way memtype conc - liftIO $ doTest name (peval test traces) +dejafuDiscard discard way = + dejafuWithSettings . set ldiscard (Just discard) . fromWayAndMemType way +{-# DEPRECATED dejafuDiscard "Use dejafuWithSettings instead" #-} -- | Variant of 'dejafu' which takes a collection of predicates to -- test, returning 'True' if all pass. @@ -611,7 +547,7 @@ dejafus :: (MonadConc n, MonadIO n, MonadRef r n, Show b) -> ConcT r n a -- ^ The computation to test. -> n Bool -dejafus = dejafusWay defaultWay defaultMemType +dejafus = dejafusWithSettings defaultSettings -- | Variant of 'dejafus' which takes a way to run the program and a -- memory model. @@ -637,12 +573,35 @@ dejafusWay :: (MonadConc n, MonadIO n, MonadRef r n, Show b) -> ConcT r n a -- ^ The computation to test. -> n Bool -dejafusWay way memtype tests conc = do - traces <- runSCTDiscard discarder way memtype conc +dejafusWay way = dejafusWithSettings . fromWayAndMemType way + +-- | Variant of 'dejafus' which takes a settings record. +-- +-- >>> dejafusWithSettings (fromWayAndMemType defaultWay SequentialConsistency) [("A", alwaysSame), ("B", exceptionsNever)] relaxed +-- [fail] A +-- (False,True) S0---------S1----S0--S2----S0-- +-- +-- (True,True) S0---------S1-P2----S1---S0--- +-- +-- (True,False) S0---------S2----S1----S0--- +-- [pass] B +-- False +-- +-- @since unreleased +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 @@ -652,11 +611,14 @@ dejafusWay way memtype tests conc = do -- include more than this if the different predicates have -- different discard functions, so we do another pass of -- discarding. - chk p = peval p . mapMaybe go where - go r@(efa, _) = case pdiscard p efa of - Just DiscardResultAndTrace -> Nothing - Just DiscardTrace -> Just (efa, []) - Nothing -> Just r + chk p rs + | moreThan 1 rs = + let go r@(efa, _) = case pdiscard p efa of + Just DiscardResultAndTrace -> Nothing + Just DiscardTrace -> Just (efa, []) + Nothing -> Just r + in peval p (mapMaybe go rs) + | otherwise = peval p rs ------------------------------------------------------------------------------- -- Test cases @@ -708,7 +670,7 @@ runTest :: (MonadConc n, MonadRef r n) -> ConcT r n a -- ^ The computation to test -> n (Result b) -runTest = runTestWay defaultWay defaultMemType +runTest = runTestWithSettings defaultSettings -- | Variant of 'runTest' which takes a way to run the program and a -- memory model. @@ -728,8 +690,26 @@ runTestWay :: (MonadConc n, MonadRef r n) -> ConcT r n a -- ^ The computation to test -> n (Result b) -runTestWay way memtype p conc = - peval p <$> runSCTDiscard (pdiscard p) way memtype conc +runTestWay way = runTestWithSettings . fromWayAndMemType way + +-- | Variant of 'runTest' which takes a settings record. +-- +-- The exact executions tried, and the order in which results are +-- found, is unspecified and may change between releases. This may +-- affect which failing traces are reported, when there is a failure. +-- +-- @since unreleased +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/dejafu/Test/DejaFu/Settings.hs b/dejafu/Test/DejaFu/Settings.hs index ebf22fd..8474713 100644 --- a/dejafu/Test/DejaFu/Settings.hs +++ b/dejafu/Test/DejaFu/Settings.hs @@ -25,6 +25,29 @@ module Test.DejaFu.Settings , 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(..) @@ -36,11 +59,75 @@ module Test.DejaFu.Settings , 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