dejafu 0.6.0.0 → 0.7.0.0

raw patch · 10 files changed

+694/−154 lines, 10 filesdep +leancheckPVP ok

version bump matches the API change (PVP)

Dependencies added: leancheck

API changes (from Hackage documentation)

Files

• CHANGELOG.markdown +47/−0
• Test/DejaFu.hs +41/−63
• Test/DejaFu/Conc.hs +2/−2
• Test/DejaFu/Conc/Internal.hs +15/−7
• Test/DejaFu/Conc/Internal/Memory.hs +1/−1
• Test/DejaFu/Defaults.hs +63/−0
• Test/DejaFu/Refinement.hs +389/−0
• Test/DejaFu/SCT.hs +123/−70
• Test/DejaFu/SCT/Internal.hs +8/−9
• dejafu.cabal +5/−2

@@ -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][]) ------- 

@@ -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   -------------------------------------------------------------------------------

@@ -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. --

@@ -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

@@ -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

@@ -0,0 +1,63 @@+-- |+-- Module      : Test.DejaFu.Defaults+-- Copyright   : (c) 2017 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- Stability   : experimental+-- Portability : portable+--+-- Default parameters for test execution.+module Test.DejaFu.Defaults where++import           Test.DejaFu.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

@@ -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 <mike@barrucadu.co.uk>+-- 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

@@ -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 <gen> " ++ show n+  show (Systematic bs)  = "Systematic (" ++ show bs ++ ")"+  show (Weighted _ n t) = "Weighted <gen> " ++ show (n, t)+  show (Uniform  _ n)   = "Uniform <gen> " ++ 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

@@ -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.

@@ -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