diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown --- a/CHANGELOG.markdown +++ b/CHANGELOG.markdown @@ -7,6 +7,53 @@ *de facto* standard Haskell versioning scheme. +0.7.0.0 [2017-06-07] (git tag: [dejafu-0.7.0.0][]) +------- + +https://hackage.haskell.org/package/dejafu-0.7.0.0 + +### Test.DejaFu + +- The new Test.DejaFu.Defaults and Test.DejaFu.Refinement modules are re-exported. +- The new smart constructors from Test.DejaFu.SCT are exported. + +### Test.DejaFu.Defaults + +- The `default*` values are now defined in the new Test.DejaFu.Defaults module. There is no breaking + API change as they are re-exported from Test.DejaFu. + +### Test.DejaFu.Refinement + +- A new module for checking observational properties of the side-effects of stateful, concurrent + functions. + + This is related to my work on [CoCo][], allowing dejafu to test what CoCo discovers. + +### Test.DejaFu.SCT + +- The `Way` type is now abstract and exposes smart constructor functions: + - `systematically`, corresponding to the old `Systematically`. + - `randomly`, corresponding to the old `Randomly`, + - `uniformly`, a new uniform random (as opposed to weighted random) scheduler. + - `swarmy`, corresponding to the old `Randomly` and specifying how many executions to use the + same weights for. +- A new `sctUniformRandom` function to do uniform (non-weighted) scheduling. +- The `sctRandom` function is now called `sctWeightedRandom` and can now re-use the same weights for + multiple executions. +- The `sctPreBound`, `sctFairBound`, and `sctLengthBound` functions have been removed. + +### Fixed + +- An issue where `subconcurrency` would re-use `MVar` IDs, leading to false reports of deadlock on + occasion (issue #81). + +[CoCo]: https://github.com/barrucadu/coco +[dejafu-0.7.0.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.7.0.0 + + +--------------------------------------------------------------------------------------------------- + + 0.6.0.0 [2017-04-08] (git tag: [dejafu-0.6.0.0][]) ------- diff --git a/Test/DejaFu.hs b/Test/DejaFu.hs --- a/Test/DejaFu.hs +++ b/Test/DejaFu.hs @@ -93,8 +93,12 @@ -- * Testing with different settings - , Way(..) + , Way , defaultWay + , systematically + , randomly + , uniformly + , swarmy , autocheckWay , autocheckWayIO @@ -240,19 +244,47 @@ , somewhereTrue , gives , gives' + + -- * Refinement property testing + + -- | Consider this statement about @MVar@s: \"using @readMVar@ is + -- better than @takeMVar@ followed by @putMVar@ because the former + -- is atomic but the latter is not.\" + -- + -- Deja Fu can test properties like that: + -- + -- @ + -- sig e = Sig + -- { initialise = maybe newEmptyMVar newMVar + -- , observe = \\v _ -> tryReadMVar v + -- , interfere = \\v s -> tryTakeMVar v >> maybe (pure ()) (void . tryPutMVar v) s + -- , expression = e + -- } + -- + -- > check $ sig (void . readMVar) \`equivalentTo\` sig (\\v -> takeMVar v >>= putMVar v) + -- *** Failure: (seed Just ()) + -- left: [(Nothing,Just ())] + -- right: [(Nothing,Just ()),(Just Deadlock,Just ())] + -- @ + -- + -- The two expressions are not equivalent, and we get given the + -- counterexample! + , module Test.DejaFu.Refinement ) where -import Control.Arrow (first) -import Control.DeepSeq (NFData(..)) -import Control.Monad (unless, when) -import Control.Monad.Ref (MonadRef) -import Control.Monad.ST (runST) -import Data.Function (on) -import Data.List (intercalate, intersperse, minimumBy) -import Data.Ord (comparing) +import Control.Arrow (first) +import Control.DeepSeq (NFData(..)) +import Control.Monad (unless, when) +import Control.Monad.Ref (MonadRef) +import Control.Monad.ST (runST) +import Data.Function (on) +import Data.List (intercalate, intersperse, minimumBy) +import Data.Ord (comparing) import Test.DejaFu.Common import Test.DejaFu.Conc +import Test.DejaFu.Defaults +import Test.DejaFu.Refinement import Test.DejaFu.SCT @@ -687,60 +719,6 @@ -- @since 0.2.0.0 gives' :: (Eq a, Show a) => [a] -> Predicate a gives' = gives . map Right - - -------------------------------------------------------------------------------- --- Defaults - --- | A default way to execute concurrent programs: systematically --- using 'defaultBounds'. --- --- @since 0.6.0.0 -defaultWay :: Way -defaultWay = Systematically defaultBounds - --- | The default memory model: @TotalStoreOrder@ --- --- @since 0.2.0.0 -defaultMemType :: MemType -defaultMemType = TotalStoreOrder - --- | All bounds enabled, using their default values. --- --- @since 0.2.0.0 -defaultBounds :: Bounds -defaultBounds = Bounds - { boundPreemp = Just defaultPreemptionBound - , boundFair = Just defaultFairBound - , boundLength = Just defaultLengthBound - } - --- | A sensible default preemption bound: 2. --- --- See /Concurrency Testing Using Schedule Bounding: an Empirical Study/, --- P. Thomson, A. F. Donaldson, A. Betts for justification. --- --- @since 0.2.0.0 -defaultPreemptionBound :: PreemptionBound -defaultPreemptionBound = 2 - --- | A sensible default fair bound: 5. --- --- This comes from playing around myself, but there is probably a --- better default. --- --- @since 0.2.0.0 -defaultFairBound :: FairBound -defaultFairBound = 5 - --- | A sensible default length bound: 250. --- --- Based on the assumption that anything which executes for much --- longer (or even this long) will take ages to test. --- --- @since 0.2.0.0 -defaultLengthBound :: LengthBound -defaultLengthBound = 250 ------------------------------------------------------------------------------- diff --git a/Test/DejaFu/Conc.hs b/Test/DejaFu/Conc.hs --- a/Test/DejaFu/Conc.hs +++ b/Test/DejaFu/Conc.hs @@ -198,8 +198,8 @@ -> ConcT r n a -> n (Either Failure a, s, Trace) runConcurrent sched memtype s ma = do - (res, s', trace, _) <- runConcurrency sched memtype s 2 (unC ma) - pure (res, s', F.toList trace) + (res, ctx, trace, _) <- runConcurrency sched memtype s initialIdSource 2 (unC ma) + pure (res, cSchedState ctx, F.toList trace) -- | Run a concurrent computation and return its result. -- diff --git a/Test/DejaFu/Conc/Internal.hs b/Test/DejaFu/Conc/Internal.hs --- a/Test/DejaFu/Conc/Internal.hs +++ b/Test/DejaFu/Conc/Internal.hs @@ -52,19 +52,24 @@ => Scheduler g -> MemType -> g + -> IdSource -> Int -> M n r a - -> n (Either Failure a, g, SeqTrace, Maybe (ThreadId, ThreadAction)) -runConcurrency sched memtype g caps ma = do + -> n (Either Failure a, Context n r g, SeqTrace, Maybe (ThreadId, ThreadAction)) +runConcurrency sched memtype g idsrc caps ma = do ref <- newRef Nothing let c = runCont ma (AStop . writeRef ref . Just . Right) - let threads = launch' Unmasked initialThread (const c) M.empty - let ctx = Context { cSchedState = g, cIdSource = initialIdSource, cThreads = threads, cWriteBuf = emptyBuffer, cCaps = caps } + let ctx = Context { cSchedState = g + , cIdSource = idsrc + , cThreads = launch' Unmasked initialThread (const c) M.empty + , cWriteBuf = emptyBuffer + , cCaps = caps + } (finalCtx, trace, finalAction) <- runThreads sched memtype ref ctx out <- readRef ref - pure (fromJust out, cSchedState finalCtx, trace, finalAction) + pure (fromJust out, finalCtx, trace, finalAction) -- | The context a collection of threads are running in. data Context n r g = Context @@ -369,8 +374,11 @@ ASub ma c | M.size (cThreads ctx) > 1 -> pure (Left IllegalSubconcurrency, Single Subconcurrency) | otherwise -> do - (res, g', trace, finalDecision) <- runConcurrency sched memtype (cSchedState ctx) (cCaps ctx) ma - pure (Right ctx { cThreads = goto (AStopSub (c res)) tid (cThreads ctx), cSchedState = g' }, SubC trace finalDecision) + (res, ctx', trace, finalDecision) <- + runConcurrency sched memtype (cSchedState ctx) (cIdSource ctx) (cCaps ctx) ma + pure (Right ctx { cThreads = goto (AStopSub (c res)) tid (cThreads ctx) + , cIdSource = cIdSource ctx' + , cSchedState = cSchedState ctx' }, SubC trace finalDecision) -- after the end of a subconcurrent computation. does nothing, -- only exists so that: there is an entry in the trace for diff --git a/Test/DejaFu/Conc/Internal/Memory.hs b/Test/DejaFu/Conc/Internal/Memory.hs --- a/Test/DejaFu/Conc/Internal/Memory.hs +++ b/Test/DejaFu/Conc/Internal/Memory.hs @@ -131,7 +131,7 @@ addCommitThreads :: WriteBuffer r -> Threads n r -> Threads n r addCommitThreads (WriteBuffer wb) ts = ts <> M.fromList phantoms where phantoms = [ (ThreadId Nothing $ negate tid, mkthread $ fromJust c) - | ((k, b), tid) <- zip (M.toList wb) [1..] + | ((_, b), tid) <- zip (M.toList wb) [1..] , let c = go $ viewl b , isJust c] go (BufferedWrite tid (CRef crid _) _ :< _) = Just $ ACommit tid crid diff --git a/Test/DejaFu/Defaults.hs b/Test/DejaFu/Defaults.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Defaults.hs @@ -0,0 +1,63 @@ +-- | +-- Module : Test.DejaFu.Defaults +-- Copyright : (c) 2017 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : portable +-- +-- Default parameters for test execution. +module Test.DejaFu.Defaults where + +import Test.DejaFu.Common +import Test.DejaFu.SCT + +-- | A default way to execute concurrent programs: systematically +-- using 'defaultBounds'. +-- +-- @since 0.6.0.0 +defaultWay :: Way +defaultWay = systematically defaultBounds + +-- | The default memory model: @TotalStoreOrder@ +-- +-- @since 0.2.0.0 +defaultMemType :: MemType +defaultMemType = TotalStoreOrder + +-- | All bounds enabled, using their default values. +-- +-- @since 0.2.0.0 +defaultBounds :: Bounds +defaultBounds = Bounds + { boundPreemp = Just defaultPreemptionBound + , boundFair = Just defaultFairBound + , boundLength = Just defaultLengthBound + } + +-- | A sensible default preemption bound: 2. +-- +-- See /Concurrency Testing Using Schedule Bounding: an Empirical Study/, +-- P. Thomson, A. F. Donaldson, A. Betts for justification. +-- +-- @since 0.2.0.0 +defaultPreemptionBound :: PreemptionBound +defaultPreemptionBound = 2 + +-- | A sensible default fair bound: 5. +-- +-- This comes from playing around myself, but there is probably a +-- better default. +-- +-- @since 0.2.0.0 +defaultFairBound :: FairBound +defaultFairBound = 5 + +-- | A sensible default length bound: 250. +-- +-- Based on the assumption that anything which executes for much +-- longer (or even this long) will take ages to test. +-- +-- @since 0.2.0.0 +defaultLengthBound :: LengthBound +defaultLengthBound = 250 diff --git a/Test/DejaFu/Refinement.hs b/Test/DejaFu/Refinement.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Refinement.hs @@ -0,0 +1,389 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeFamilies #-} + +-- | +-- Module : Test.DejaFu.Refinement +-- Copyright : (c) 2017 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : FlexibleContexts, FlexibleInstances, GADTs, TupleSections, TypeFamilies +-- +-- Properties about the side-effects of concurrent functions on some +-- shared state. +-- +-- Consider this statement about @MVar@s: \"using @readMVar@ is better +-- than @takeMVar@ followed by @putMVar@ because the former is atomic +-- but the latter is not.\" +-- +-- This module can test properties like that: +-- +-- @ +-- sig e = Sig +-- { initialise = maybe newEmptyMVar newMVar +-- , observe = \\v _ -> tryReadMVar v +-- , interfere = \\v s -> tryTakeMVar v >> maybe (pure ()) (void . tryPutMVar v) s +-- , expression = e +-- } +-- +-- > check $ sig (void . readMVar) \`equivalentTo\` sig (\\v -> takeMVar v >>= putMVar v) +-- *** Failure: (seed Just ()) +-- left: [(Nothing,Just ())] +-- right: [(Nothing,Just ()),(Just Deadlock,Just ())] +-- @ +-- +-- The two expressions are not equivalent, and we get given the +-- counterexample! +-- +-- There are quite a few things going on here, so let's unpack this: +-- +-- (1) Properties are specified in terms of an __initialisation__ +-- function, an __observation__ function, an __interference__ +-- function, and the expression of interest. +-- +-- (2) The initialisation function ('initialise') says how to +-- construct some __state__ value from a __seed__ value, which is +-- supplied by 'check'. In this case the seed is of type @Maybe +-- a@ and the state @MVar ConcIO a@. +-- +-- (3) The observation ('observe') function says how to take the state +-- and the seed, and produce some value which will be used to +-- compare the expressions. In this case the observation value is +-- of type @Maybe a@. +-- +-- (4) The interference ('interfere') function says what sort of +-- concurrent interference can happen. In this case we just try +-- to set the @MVar@ to its original value. +-- +-- The 'check' function takes a property, consisting of two signatures +-- and a way to compare them, evaluates all the results of each +-- signature, and then compares them in the appropriate way. +-- +-- See the sections later in the documentation for what +-- \"refinement\", \"strict refinement\", and \"equivalence\" mean +-- exactly. +module Test.DejaFu.Refinement + ( -- * Defining properties + Sig(..) + , RefinementProperty + , expectFailure + + -- ** A refines B + + -- | Refinement (or \"weak refinement\") means that all of the + -- results of the left are also results of the right. If you think + -- in terms of sets of results, refinement is subset. + , refines, (=>=) + + -- ** A strictly refines B + + -- | Strict refinement means that the left refines the right, but + -- the right does not refine the left. If you think in terms of + -- sets of results, strict refinement is proper subset. + , strictlyRefines, (->-) + + -- ** A is equivalent to B + + -- | Equivalence means that the left and right refine each other. + -- If you think in terms of sets of results, equivalence is + -- equality. + , equivalentTo, (===) + + -- * Testing properties + , FailedProperty(..) + , Testable(O,X) + , check + , check' + , checkFor + , counterExamples + + -- * Re-exports + , Listable(..) + ) where + +import Control.Arrow (first) +import Control.Monad (void) +import Control.Monad.Conc.Class (readMVar, spawn) +import Data.Maybe (isNothing, listToMaybe) +import Data.Set (Set) +import qualified Data.Set as S +import Test.LeanCheck (Listable(..), concatMapT, mapT) + +import Test.DejaFu.Conc (ConcIO, Failure, subconcurrency) +import Test.DejaFu.Defaults (defaultMemType, defaultWay) +import Test.DejaFu.SCT (runSCT) + +------------------------------------------------------------------------------- +-- Specifying properties + +-- | What to check. +data How = Weak | Equiv | Strict deriving Eq + +-- | A property which can be given to 'check'. +-- +-- @since 0.7.0.0 +data RefinementProperty o x where + RP :: Ord o => How -> Sig s1 o x -> Sig s2 o x -> RefinementProperty o x + Neg :: RefinementProperty o x -> RefinementProperty o x + +-- | A concurrent function and some information about how to execute +-- it and observe its effect. +-- +-- * @s@ is the state type (@MVar ConcIO a@ in the example) +-- * @o@ is the observation type (@Maybe a@ in the example) +-- * @x@ is the seed type (@Maybe a@ in the example) +-- +-- @since 0.7.0.0 +data Sig s o x = Sig + { initialise :: x -> ConcIO s + -- ^ Create a new instance of the state variable. + , observe :: s -> x -> ConcIO o + -- ^ The observation to make. + , interfere :: s -> x -> ConcIO () + -- ^ Set the state value. This doesn't need to be atomic, or even + -- guaranteed to work, its purpose is to cause interference. + , expression :: s -> ConcIO () + -- ^ The expression to evaluate. + } + +-- | Indicates that the property is supposed to fail. +expectFailure :: RefinementProperty o x -> RefinementProperty o x +expectFailure = Neg + +-- | Observational refinement. +-- +-- True iff the result-set of the left expression is a subset (not +-- necessarily proper) of the result-set of the right expression. +-- +-- The two signatures can have different state types, this lets you +-- compare the behaviour of different data structures. The +-- observation and seed types must match, however. +-- +-- @since 0.7.0.0 +refines :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x +refines = RP Weak + +-- | Infix synonym for 'refines'. +-- +-- You might think this should be '=<=', so it looks kind of like a +-- funny subset operator, with @A =<= B@ meaning \"the result-set of A +-- is a subset of the result-set of B\". Unfortunately you would be +-- wrong. The operator used in the literature for refinement has the +-- open end pointing at the LESS general term and the closed end at +-- the MORE general term. It is read as \"is refined by\", not +-- \"refines\". So for consistency with the literature, the open end +-- of @=>=@ points at the less general term, and the closed end at the +-- more general term, to give the same argument order as 'refines'. +-- +-- @since 0.7.0.0 +(=>=) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x +(=>=) = refines + +-- | Observational equivalence. +-- +-- True iff the result-set of the left expression is equal to the +-- result-set of the right expression. +-- +-- The two signatures can have different state types, this lets you +-- compare the behaviour of different data structures. The +-- observation and seed types must match, however. +-- +-- @since 0.7.0.0 +equivalentTo :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x +equivalentTo = RP Equiv + +-- | Infix synonym for 'equivalentTo'. +-- +-- @since 0.7.0.0 +(===) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x +(===) = equivalentTo + +-- | Strict observational refinement. +-- +-- True iff the result-set of the left expression is a proper subset +-- of the result-set of the right expression. +-- +-- The two signatures can have different state types, this lets you +-- compare the behaviour of different data structures. The +-- observation and seed types must match, however. +-- +-- @since 0.7.0.0 +strictlyRefines :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x +strictlyRefines = RP Strict + +-- | Infix synonym for 'strictlyRefines' +-- +-- @since 0.7.0.0 +(->-) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x +(->-) = strictlyRefines + + +------------------------------------------------------------------------------- +-- Property testing + +-- | Things which can be tested. +-- +-- @since 0.7.0.0 +class Testable a where + -- | The observation value type. This is used to compare the + -- results. + type O a :: * + + -- | The seed value type. This is used to construct the concurrent + -- states. + type X a :: * + + rpropTiers :: a -> [[([String], RefinementProperty (O a) (X a))]] + +instance Testable (RefinementProperty o x) where + type O (RefinementProperty o x) = o + type X (RefinementProperty o x) = x + + rpropTiers p = [[([], p)]] + +instance (Listable a, Show a, Testable b) => Testable (a -> b) where + type O (a -> b) = O b + type X (a -> b) = X b + + rpropTiers p = concatMapT resultiersFor tiers where + resultiersFor x = first (show x:) `mapT` rpropTiers (p x) + +-- | A counter example is a seed value and a list of variable +-- assignments. +-- +-- @since 0.7.0.0 +data FailedProperty o x + = CounterExample + { failingSeed :: x + -- ^ The seed for this set of executions. + , failingArgs :: [String] + -- ^ The values of free variables, as strings. + , leftResults :: Set (Maybe Failure, o) + -- ^ The set of results of the left signature. + , rightResults :: Set (Maybe Failure, o) + -- ^ The set of results of the right signature. + } + | NoExpectedFailure + deriving Show + +-- | Check a refinement property with a variety of seed values and +-- variable assignments. +-- +-- @since 0.7.0.0 +check :: (Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) + => p + -- ^ The property to check. + -> IO Bool +check p = do + ce <- check' p + putStrLn $ case ce of + Just NoExpectedFailure -> "*** Failure: passed, but expected failure." + Just c -> init $ unlines + [ "*** Failure: " ++ + (if null (failingArgs c) then "" else unwords (failingArgs c) ++ " ") ++ + "(seed " ++ show (failingSeed c) ++ ")" + , " left: " ++ show (S.toList $ leftResults c) + , " right: " ++ show (S.toList $ rightResults c) + ] + Nothing -> "+++ OK" + pure (isNothing ce) + +-- | A version of 'check' that doesn't print, and returns the +-- counterexample. +-- +-- @since 0.7.0.0 +check' :: (Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) + => p + -- ^ The property to check. + -> IO (Maybe (FailedProperty (O p) (X p))) +check' = checkFor 10 100 + +-- | Like 'check', but take a number of cases to try, also returns the +-- counter example found rather than printing it. +-- +-- @since 0.7.0.0 +checkFor :: (Testable p, Listable (X p), Eq (X p), Show (X p)) + => Int + -- ^ Number of seed values per variable-assignment. + -> Int + -- ^ Number of variable assignments. + -> p + -- ^ The property to check. + -> IO (Maybe (FailedProperty (O p) (X p))) +checkFor sn vn p = listToMaybe <$> counterExamples sn vn p + +-- | Find all counterexamples up to a limit. +-- +-- @since 0.7.0.0 +counterExamples :: (Testable p, Listable (X p), Eq (X p)) + => Int + -- ^ Number of seed values per variable-assignment. + -> Int + -- ^ Number of variable assignments + -> p + -- ^ The property to check. + -> IO [FailedProperty (O p) (X p)] +counterExamples sn vn p = do + let seeds = take sn $ concat tiers + let cases = take vn $ concat (rpropTiers p) + rs <- mapM (\(vs, p') -> (vs,) <$> checkWithSeeds seeds p') cases + pure [ cf vs | (vs, Just cf) <- rs ] + + +------------------------------------------------------------------------------- +-- Internal + +-- | Check a refinement property with given seed values. Returns the +-- counterexample if the property is false. +checkWithSeeds + :: [x] + -- ^ Seed values to use. + -> RefinementProperty o x + -- ^ The property to check. + -> IO (Maybe ([String] -> FailedProperty o x)) +checkWithSeeds seeds (RP how l r) = do + ls <- mapM (\x -> (x,) <$> evalSigWithSeed l x) seeds + rs <- mapM (evalSigWithSeed r) seeds + let resultsf f = zipWith (\(x, l') r' -> (l' `f` r', x, l', r')) ls rs + pure . listToMaybe $ case how of + Weak -> ces (resultsf S.isSubsetOf) + Strict -> + -- strict fails if (a) any left result-set is not a subset of + -- the corresponding right result-set, or (b) every left + -- result-set is equal to the corresponding right result-set + let equiv = null (ces (resultsf (==))) + in ces (resultsf S.isSubsetOf) ++ if equiv then ces (resultsf S.isProperSubsetOf) else [] + Equiv -> ces (resultsf (==)) + where + ces results = [toCE x lrs rrs | (False, x, lrs, rrs) <- results] + + toCE x lrs rrs args = CounterExample + { failingSeed = x + , failingArgs = args + , leftResults = lrs + , rightResults = rrs + } +checkWithSeeds seeds (Neg rp) = do + r <- checkWithSeeds seeds rp + pure $ case r of + Just _ -> Nothing + Nothing -> Just (const NoExpectedFailure) + +-- | Evaluate a signature with a given seed value +evalSigWithSeed :: Ord o + => Sig s o x + -> x + -> IO (Set (Maybe Failure, o)) +evalSigWithSeed sig x = do + results <- runSCT defaultWay defaultMemType $ do + s <- initialise sig x + r <- subconcurrency $ do + j <- spawn (interfere sig s x) + void (expression sig s) + void (readMVar j) + o <- observe sig s x + pure (either Just (const Nothing) r, o) + pure . S.fromList $ map (\(Right a, _) -> a) results diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -12,7 +12,11 @@ -- Systematic testing for concurrent computations. module Test.DejaFu.SCT ( -- * Running Concurrent Programs - Way(..) + Way + , systematically + , randomly + , uniformly + , swarmy , runSCT , runSCT' , resultsSet @@ -58,7 +62,6 @@ -- See the BPOR paper for more details. , PreemptionBound(..) - , sctPreBound -- ** Fair Bounding @@ -69,7 +72,6 @@ -- See the BPOR paper for more details. , FairBound(..) - , sctFairBound -- ** Length Bounding @@ -77,7 +79,6 @@ -- terms of primitive actions) of an execution. , LengthBound(..) - , sctLengthBound -- * Random Scheduling @@ -88,7 +89,8 @@ -- because a random scheduler is more chaotic than the real -- scheduler. - , sctRandom + , sctUniformRandom + , sctWeightedRandom ) where import Control.DeepSeq (NFData(..)) @@ -97,7 +99,7 @@ import qualified Data.Map.Strict as M import Data.Set (Set) import qualified Data.Set as S -import System.Random (RandomGen) +import System.Random (RandomGen, randomR) import Test.DejaFu.Common import Test.DejaFu.Conc @@ -106,27 +108,90 @@ ------------------------------------------------------------------------------- -- Running Concurrent Programs --- | How to explore the possible executions of a concurrent program: --- --- * Systematically explore all executions within the bounds; or --- --- * Explore a fixed number of random executions, with the given PRNG. +-- | How to explore the possible executions of a concurrent program. -- --- @since 0.6.0.0 +-- @since 0.7.0.0 data Way where - Systematically :: Bounds -> Way - Randomly :: RandomGen g => g -> Int -> Way + Systematic :: Bounds -> Way + Weighted :: RandomGen g => g -> Int -> Int -> Way + Uniform :: RandomGen g => g -> Int -> Way instance Show Way where - show (Systematically bs) = "Systematically (" ++ show bs ++ ")" - show (Randomly _ n) = "Randomly " ++ show n + show (Systematic bs) = "Systematic (" ++ show bs ++ ")" + show (Weighted _ n t) = "Weighted " ++ show (n, t) + show (Uniform _ n) = "Uniform " ++ show n --- | Explore possible executions of a concurrent program. +-- | Systematically execute a program, trying all distinct executions +-- within the bounds. -- --- * If the 'Way' is @Systematically@, 'sctBound' is used. +-- This corresponds to 'sctBound'. -- --- * If the 'Way' is @Randomly@, 'sctRandom' is used. +-- @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'. +-- -- @since 0.6.0.0 runSCT :: MonadRef r n => Way @@ -136,8 +201,9 @@ -> ConcT r n a -- ^ The computation to run many times. -> n [(Either Failure a, Trace)] -runSCT (Systematically cb) memtype = sctBound memtype cb -runSCT (Randomly g lim) memtype = sctRandom memtype g lim +runSCT (Systematic cb) memtype = sctBound memtype cb +runSCT (Weighted g lim use) memtype = sctWeightedRandom memtype g lim use +runSCT (Uniform g lim) memtype = sctUniformRandom memtype g lim -- | A strict variant of 'runSCT'. -- @@ -235,20 +301,6 @@ -- not derived, so it can have a separate @since annotation rnf (PreemptionBound i) = rnf i --- | An SCT runner using a pre-emption bounding scheduler. --- --- @since 0.4.0.0 -sctPreBound :: MonadRef r n - => MemType - -- ^ The memory model to use for non-synchronised @CRef@ operations. - -> PreemptionBound - -- ^ The maximum number of pre-emptions to allow in a single - -- execution - -> ConcT r n a - -- ^ The computation to run many times - -> n [(Either Failure a, Trace)] -sctPreBound memtype pb = sctBound memtype $ Bounds (Just pb) Nothing Nothing - -- | Pre-emption bound function. This does not count pre-emptive -- context switches to a commit thread. pBound :: PreemptionBound -> BoundFunc @@ -286,20 +338,6 @@ -- not derived, so it can have a separate @since annotation rnf (FairBound i) = rnf i --- | An SCT runner using a fair bounding scheduler. --- --- @since 0.4.0.0 -sctFairBound :: MonadRef r n - => MemType - -- ^ The memory model to use for non-synchronised @CRef@ operations. - -> FairBound - -- ^ The maximum difference between the number of yield operations - -- performed by different threads. - -> ConcT r n a - -- ^ The computation to run many times - -> n [(Either Failure a, Trace)] -sctFairBound memtype fb = sctBound memtype $ Bounds Nothing (Just fb) Nothing - -- | Fair bound function fBound :: FairBound -> BoundFunc fBound (FairBound fb) ts (_, l) = maxYieldCountDiff ts l <= fb @@ -323,20 +361,6 @@ -- not derived, so it can have a separate @since annotation rnf (LengthBound i) = rnf i --- | An SCT runner using a length bounding scheduler. --- --- @since 0.4.0.0 -sctLengthBound :: MonadRef r n - => MemType - -- ^ The memory model to use for non-synchronised @CRef@ operations. - -> LengthBound - -- ^ The maximum length of a schedule, in terms of primitive - -- actions. - -> ConcT r n a - -- ^ The computation to run many times - -> n [(Either Failure a, Trace)] -sctLengthBound memtype lb = sctBound memtype $ Bounds Nothing Nothing (Just lb) - -- | Length bound function lBound :: LengthBound -> BoundFunc lBound (LengthBound lb) ts _ = length ts < lb @@ -401,15 +425,15 @@ -- Incorporate the new backtracking steps into the DPOR tree. addBacktracks = incorporateBacktrackSteps (cBound cb) --- | SCT via random scheduling. +-- | SCT via uniform random scheduling. -- -- Schedules are generated by assigning to each new thread a random -- weight. Threads are then scheduled by a weighted random selection. -- -- This is not guaranteed to find all distinct results. -- --- @since 0.5.0.0 -sctRandom :: (MonadRef r n, RandomGen g) +-- @since 0.7.0.0 +sctUniformRandom :: (MonadRef r n, RandomGen g) => MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. -> g @@ -419,15 +443,44 @@ -> ConcT r n a -- ^ The computation to run many times. -> n [(Either Failure a, Trace)] -sctRandom memtype g0 lim0 conc = go g0 lim0 where +sctUniformRandom memtype g0 lim0 conc = go g0 (max 0 lim0) where go _ 0 = pure [] go g n = do - (res, s, trace) <- runConcurrent randSched + (res, s, trace) <- runConcurrent (randSched $ \g' -> (1, g')) memtype - (initialRandSchedState g) + (initialRandSchedState Nothing g) conc - ((res, trace):) <$> go (schedGen s) (n-1) + +-- | SCT via weighted random scheduling. +-- +-- Schedules are generated by assigning to each new thread a random +-- weight. Threads are then scheduled by a weighted random selection. +-- +-- This is not guaranteed to find all distinct results. +-- +-- @since 0.7.0.0 +sctWeightedRandom :: (MonadRef r n, RandomGen g) + => MemType + -- ^ The memory model to use for non-synchronised @CRef@ operations. + -> g + -- ^ The random number generator. + -> Int + -- ^ The number of executions to perform. + -> Int + -- ^ The number of executions to use the same set of weights for. + -> ConcT r n a + -- ^ The computation to run many times. + -> n [(Either Failure a, Trace)] +sctWeightedRandom memtype g0 lim0 use0 conc = go g0 (max 0 lim0) (max 1 use0) M.empty where + go _ 0 _ _ = pure [] + go g n 0 _ = go g n (max 1 use0) M.empty + go g n use ws = do + (res, s, trace) <- runConcurrent (randSched $ randomR (1, 50)) + memtype + (initialRandSchedState (Just ws) g) + conc + ((res, trace):) <$> go (schedGen s) (n-1) (use-1) (schedWeights s) ------------------------------------------------------------------------------- -- Utilities diff --git a/Test/DejaFu/SCT/Internal.hs b/Test/DejaFu/SCT/Internal.hs --- a/Test/DejaFu/SCT/Internal.hs +++ b/Test/DejaFu/SCT/Internal.hs @@ -13,15 +13,14 @@ import Control.DeepSeq (NFData(..)) import Control.Exception (MaskingState(..)) -import Data.Char (ord) import qualified Data.Foldable as F import Data.Function (on) -import Data.List (intercalate, nubBy, partition, sortOn) +import Data.List (nubBy, partition, sortOn) import Data.List.NonEmpty (NonEmpty(..), toList) import Data.Map.Strict (Map) import qualified Data.Map.Strict as M -import Data.Maybe (catMaybes, fromJust, isJust, isNothing, - listToMaybe) +import Data.Maybe (catMaybes, fromJust, fromMaybe, isJust, + isNothing, listToMaybe) import Data.Sequence (Seq, (|>)) import qualified Data.Sequence as Sq import Data.Set (Set) @@ -531,14 +530,14 @@ ) -- | Initial weighted random scheduler state. -initialRandSchedState :: g -> RandSchedState g -initialRandSchedState = RandSchedState M.empty +initialRandSchedState :: Maybe (Map ThreadId Int) -> g -> RandSchedState g +initialRandSchedState = RandSchedState . fromMaybe M.empty -- | Weighted random scheduler: assigns to each new thread a weight, -- and makes a weighted random choice out of the runnable threads at -- every step. -randSched :: RandomGen g => Scheduler (RandSchedState g) -randSched _ _ threads s = (pick choice enabled, RandSchedState weights' g'') where +randSched :: RandomGen g => (g -> (Int, g)) -> Scheduler (RandSchedState g) +randSched weightf _ _ threads s = (pick choice enabled, RandSchedState weights' g'') where -- Select a thread pick idx ((x, f):xs) | idx < f = Just x @@ -551,7 +550,7 @@ weights' = schedWeights s `M.union` M.fromList newWeights (newWeights, g') = foldr assignWeight ([], schedGen s) $ filter (`M.notMember` schedWeights s) tids assignWeight tid ~(ws, g0) = - let (w, g) = randomR (1, 50) g0 + let (w, g) = weightf g0 in ((tid, w):ws, g) -- The runnable threads. 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: 0.6.0.0 +version: 0.7.0.0 synopsis: Systematic testing for Haskell concurrency. description: @@ -37,12 +37,14 @@ source-repository this type: git location: https://github.com/barrucadu/dejafu.git - tag: dejafu-0.6.0.0 + tag: dejafu-0.7.0.0 library exposed-modules: Test.DejaFu , Test.DejaFu.Conc , Test.DejaFu.Common + , Test.DejaFu.Defaults + , Test.DejaFu.Refinement , Test.DejaFu.Schedule , Test.DejaFu.SCT , Test.DejaFu.STM @@ -61,6 +63,7 @@ , containers >=0.5 && <0.6 , deepseq >=1.1 && <2 , exceptions >=0.7 && <0.9 + , leancheck >=0.6 && <0.7 , monad-loops >=0.4 && <0.5 , mtl >=2.2 && <2.3 , random >=1.0 && <1.2