dejafu 0.5.1.3 → 0.6.0.0

raw patch · 16 files changed

+955/−362 lines, 16 filessetup-changedPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.markdown +377/−0
• README.markdown +72/−0
• Setup.hs +1/−1
• Test/DejaFu.hs +111/−32
• Test/DejaFu/Common.hs +88/−10
• Test/DejaFu/Conc.hs +57/−47
• Test/DejaFu/Conc/Internal.hs +23/−22
• Test/DejaFu/Conc/Internal/Common.hs +6/−8
• Test/DejaFu/Conc/Internal/Memory.hs +27/−25
• Test/DejaFu/Conc/Internal/Threading.hs +10/−9
• Test/DejaFu/SCT.hs +84/−45
• Test/DejaFu/SCT/Internal.hs +23/−78
• Test/DejaFu/STM.hs +19/−12
• Test/DejaFu/STM/Internal.hs +35/−30
• Test/DejaFu/Schedule.hs +19/−3
• dejafu.cabal +3/−40

@@ -0,0 +1,377 @@+Release Notes+=============++All notable changes to this project will be documented in this file.++This project is versioned according to the [Package Versioning Policy](https://pvp.haskell.org), the+*de facto* standard Haskell versioning scheme.+++0.6.0.0 [2017-04-08] (git tag: [dejafu-0.6.0.0][])+-------++https://hackage.haskell.org/package/dejafu-0.6.0.0++### Test.DejaFu.Conc++- The `Conc n r a` type is now `ConcT r n a`, and has been given a `MonadTrans` instance. Uses of+  `lift` appear in the execution trace in the same way as `liftBase` and `liftIO`.+    - The `ConcIO` and `ConcST` aliases have been updated, so this should be an invisible change to+      most users.++### Test.DejaFu.SCT++- `Way` is now a GADT, no longer taking a type parameter. This greatly improves type inference when+  the `Systematically` constructor is used.+    - The `NFData` instance for `Way` is now gone. The alternative was requiring that any+      `RandomGen` used also implement `NFData`, which is *very* restrictive++### Miscellaneous++- There is now a changelog.+- Test.DejaFu.Common is now considered to form part of the public API of the library.+- Every definition and instance now has a Haddock "@since" annotation.++[dejafu-0.6.0.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.6.0.0+++---------------------------------------------------------------------------------------------------+++0.5.1.3 [2017-04-05] (git tag: [dejafu-0.5.1.3][])+-------++https://hackage.haskell.org/package/dejafu-0.5.1.3++### Miscellaneous++- The version range on the concurrency package has been changed to 1.1.*.++[dejafu-0.5.1.3]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.5.1.3+++---------------------------------------------------------------------------------------------------+++0.5.1.2 [2017-03-04] (git tag: [dejafu-0.5.1.2][])+-------++https://hackage.haskell.org/package/dejafu-0.5.1.2++**This version was misnumbered! It should have caused a minor version bump!**++### Test.DejaFu.Conc++- New `MonadRef` and `MonadAtomicRef` instances for the `Conc` type using `CRef`.++### Fixed++- A long-standing bug where if the main thread is killed with a `throwTo`, the throwing neither+  appears in the trace nor correctly terminates the execution.++### Miscellaneous++- The maximum supported version of the concurrency package has been changed to 1.1.1.*.++[dejafu-0.5.1.2]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.5.1.2+++---------------------------------------------------------------------------------------------------+++0.5.1.1 [2017-02-25] (git tag: [dejafu-0.5.1.1][])+-------++https://hackage.haskell.org/package/dejafu-0.5.1.1++### Fixed++- The correct scheduler state is now passed to the scheduler immediately after the termination of a+  `subconcurrency` action.+- SCT of subconcurrency no longer loops infinitely.++[dejafu-0.5.1.1]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.5.1.1+++---------------------------------------------------------------------------------------------------+++0.5.1.0 [2017-02-25] (git tag: [dejafu-0.5.1.0][])+-------++https://hackage.haskell.org/package/dejafu-0.5.1.0++### Test.DejaFu++- A new `NFData` instance for `Result`.++### Test.DejaFu.Common++- New instances:+    - `NFData` for `ThreadId`, `CRefId`, `MVarId`, `TVarId`, `IdSource`, `ThreadAction`,+      `Lookahead`, `ActionType`, `TAction`, `Decision`, `Failure`, and `MemType`.+    - `Eq`, `Ord`, and `Show` instances for `IdSource`.++### Test.DejaFu.SCT++- New `NFData` instances for `Way`, `Bounds`, `PreemptionBound`, `FairBound`, and `LengthBound`.+- New strict variants of `runSCT` and `resultsSet`: `runSCT'` and `resultsSet'`.++### Test.DejaFu.STM++- A new `NFData` instance for `Result`.++[dejafu-0.5.1.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.5.1.0+++---------------------------------------------------------------------------------------------------+++0.5.0.2 [2017-02-22] (git tag: [dejafu-0.5.0.2][])+-------++https://hackage.haskell.org/package/dejafu-0.5.0.2++**This version was misnumbered! It should have caused a major version bump!**++### Test.DejaFu.Common++- A new `StopSubconcurrency` constructor of `ThreadAction`.++### Changed++- A `StopConcurrency` action appears in the execution trace immediately after the end of a+  `subconcurrency` action (much like the `PopCatching` and `ResetMasking` actions which appear after+  a catch and mask).+- A `subconcurrency` action now inherits the number of capabilities from the outer computation,+  rather than being reset to 2 as before.++### Miscellaneous++- Test.DejaFu.SCT now compiles with MonoLocalBinds enabled (implied by GADTs and TypeFamilies),+  which may be relevant to hackers.++[dejafu-0.5.0.2]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.5.0.2+++---------------------------------------------------------------------------------------------------+++0.5.0.1 [2017-02-21] (git tag: [dejafu-0.5.0.1][])+-------++**This version was never pushed to hackage, whoops!**++### Fixed++- `readMVar` is once again considered a "release action" for the purposes of fair-bounding.++[dejafu-0.5.0.1]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.5.0.1+++---------------------------------------------------------------------------------------------------+++0.5.0.0 [2017-02-21] (git tag: [dejafu-0.5.0.0][])+-------++https://hackage.haskell.org/package/dejafu-0.5.0.0++### Test.DejaFu++- All the functions which did take a `Bounds` now take a `Way` instead and support random scheduling+  as well.++### Test.DejaFu.Common++- New `Eq` instances for `ThreadAction` and `Lookahead`.+- A `TryReadMVar` constructor for `ThreadAction` and a corresponding `WillTryReadMVar` constructor+  for `Lookahead`.++### Test.DejaFu.Conc++- A new testing-only `subconcurrency` function, to run a concurrent action and do something with its+  result in the same concurrent context, even if it fails.++### Test.DejaFu.SCT++- An `sctRandom` function to run a fixed number of randomly-scheduled executions of a program.+- The `Way` type, to abstract over how to run a concurrent program, used by new functions `runSCT`+  and `resultsSet`.++### Fixed++- Some previously-missed `CRef` action dependencies are no longer missed.++### Miscellaneous++- The supported version of the concurrency package was bumped to 1.1.0.0, introducing `tryReadMVar`.+- A bunch of things were called "Var" or "Ref", these are now consistently "MVar" and "CRef".+- Significant performance improvements in both time and space.+- The dpor package has been merged back into this, as it turned out not to be very generally+  useful. There is no direct replacement, but I have no intent to update it, so the dpor package is+  now __deprecated__.++[dejafu-0.5.0.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.5.0.0+++---------------------------------------------------------------------------------------------------+++0.4.0.0 [2016-09-10] (git tag: [dejafu-0.4.0.0][])+-------++https://hackage.haskell.org/package/dejafu-0.4.0.0++### Test.DejaFu++- The `autocheck'` function now takes the schedule bounds as a parameter.+- New `runTestM` and `runTestM'` functions, monad-polymorphic variants of the now-removed+  `runTestIO` and `runTestIO'` functions.++### Test.DejaFu.Conc++- The `Conc` type no longer has the STM type as a parameter.+- A new `runConcurrent` function, a monad-polymorphic version of the now-removed `runConcST` and+  `runConcIO` functions.++### Test.DejaFu.SCT++- The `ST`-specific functions are now monad-polymorphic.+- The `IO` function variants have been removed.++### Test.DejaFu.STM++- A new `runTransaction` function, a monad-polymorphic version of the now-removed `runTransactionST`+  and `runTransactionIO` functions.++### Changed++- The termination of the main thread in execution traces now appears as a single `Stop`, rather than+  the sequence `Lift, Stop`.+- Execution traces printed by the helpful functions in Test.DejaFu now include a key of thread+  names.++### Miscellaneous++- Remodularisation:+    - The Control.* modules have all been split out into a separate "concurrency" package.+    - Many definitions from other modules have been moved to the new Test.DejaFu.Common module.+    - The Test.DejaFu.Deterministic module has been renamed to Test.DejaFu.Conc++[dejafu-0.4.0.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.4.0.0+++---------------------------------------------------------------------------------------------------+++0.3.2.1 [2016-07-21] (git tag: [dejafu-0.3.2.1][])+-------++https://hackage.haskell.org/package/dejafu-0.3.2.1++### Fixed++- The implementation of the STM `orElse` for `STMLike` incorrectly handled some state+  non-associatively, leading to false deadlocks being reported in some cases.++[dejafu-0.3.2.1]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.3.2.1+++---------------------------------------------------------------------------------------------------+++0.3.2.0 [2016-06-06] (git tag: [dejafu-0.3.2.0][])+-------++https://hackage.haskell.org/package/dejafu-0.3.2.0++**Builds with both dpor-0.1 and dpor-0.2, however some improvements require dpor-0.2.**++### Fixed++- (faster with dpor-0.2) Executions missed due to daemon threads with uninteresting first actions+  are no longer missed.++### Changed++- (requires dpor-0.2) Significantly improved dependency inference of exceptions, greatly improving+  performance of testcases using exceptions.+- Significantly improved dependency inference of STM transactions, greatly improving performance of+  testcases using STM.++[dejafu-0.3.2.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.3.2.0+++---------------------------------------------------------------------------------------------------+++0.3.1.1 [2016-05-26] (git tag: [dejafu-0.3.1.1][])+-------++https://hackage.haskell.org/package/dejafu-0.3.1.1++### Miscellaneous++- Now supports GHC 8.++[dejafu-0.3.1.1]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.3.1.1+++---------------------------------------------------------------------------------------------------+++0.3.1.0 [2016-05-02] (git tag: [dejafu-0.3.1.0][])+-------++https://hackage.haskell.org/package/dejafu-0.3.1.0++### Fixed++- Context switches around relaxed memory commit actions could cause the number of pre-emptions in an+  execution to be miscounted, leading to the pre-emption bounding being too lenient.++[dejafu-0.3.1.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.3.1.0+++---------------------------------------------------------------------------------------------------+++0.3.0.0 [2016-04-03] (git tag: [dejafu-0.3.0.0][])+-------++https://hackage.haskell.org/package/dejafu-0.3.0.0++**The minimum supported version of GHC is now 7.10.**++I didn't write proper release notes, and this is so far back I don't really care to dig through the+logs.++[dejafu-0.3.0.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.3.0.0+++---------------------------------------------------------------------------------------------------+++0.2.0.0 [2015-12-01] (git tag: [0.2.0.0][])+-------++https://hackage.haskell.org/package/dejafu-0.2.0.0++I didn't write proper release notes, and this is so far back I don't really care to dig through the+logs.++[0.2.0.0]: https://github.com/barrucadu/dejafu/releases/tag/0.2.0.0+++---------------------------------------------------------------------------------------------------+++0.1.0.0 [2015-08-27] (git tag: [0.1.0.0][])+-------++https://hackage.haskell.org/package/dejafu-0.1.0.0++Initial release. Go read the API docs.++[0.1.0.0]: https://github.com/barrucadu/dejafu/releases/tag/0.1.0.0

@@ -0,0 +1,72 @@+dejafu+======++> [Déjà Fu is] A martial art in which the user's limbs move in time as+> well as space, […] It is best described as "the feeling that you+> have been kicked in the head this way before"+>+> -- Terry Pratchett, Thief of Time++Concurrency is nice, deadlocks and race conditions not so much. The+`Par` monad family, as defined in [abstract-par][] provides+deterministic parallelism, but sometimes we can tolerate a bit of+nondeterminism.++This package builds on the concurrency package (also in this+repository) by enabling you to systematically and deterministically+test your concurrent programs.++The documentation of the latest developmental version is+[available online][docs]. Examples can be found in the test suite.++**Note on the test suite:** This is in a separate project+(dejafu-tests) because Cabal-the-library is a bit naff. See this+[issue][].++Déjà Fu and `IO`+----------------++The core assumption underlying Déjà Fu is that any apparent+nondeterminism arises purely from the scheduling behaviour. To put it+another way, a given computation, parametrised with a fixed set of+scheduling decisions, is deterministic.++Whilst this assumption may not hold in general when `IO` is involved,+you should strive to produce test cases where it does.++Memory Model+------------++The testing functionality supports a few different memory models, for+computations which use non-synchronised `CRef` operations. The+supported models are:++- **Sequential Consistency:** A program behaves as a simple+    interleaving of the actions in different threads. When a CRef is+    written to, that write is immediately visible to all threads.++- **Total Store Order (TSO):** Each thread has a write buffer. A+    thread sees its writes immediately, but other threads will only+    see writes when they are committed, which may happen later. Writes+    are committed in the same order that they are created.++- **Partial Store Order (PSO):** Each CRef has a write buffer. A+    thread sees its writes immediately, but other threads will only+    see writes when they are committed, which may happen later. Writes+    to different CRefs are not necessarily committed in the same order+    that they are created.++If a testing function does not take the memory model as a parameter,+it uses TSO.++Contributing+------------++Bug reports, pull requests, and comments are very welcome!++Feel free to contact me on GitHub, through IRC (#haskell on freenode),+or email (mike@barrucadu.co.uk).++[docs]:         https://docs.barrucadu.co.uk/dejafu+[abstract-par]: https://hackage.haskell.org/package/abstract-par/docs/Control-Monad-Par-Class.html+[issue]:        https://github.com/commercialhaskell/stack/issues/1122

@@ -1,2 +1,2 @@-import Distribution.Simple+import           Distribution.Simple main = defaultMain

@@ -242,19 +242,18 @@   , gives'   ) where -import Control.Arrow (first)-import Control.DeepSeq (NFData(..))-import Control.Monad (when, unless)-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 System.Random (RandomGen, StdGen)+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.SCT+import           Test.DejaFu.Common+import           Test.DejaFu.Conc+import           Test.DejaFu.SCT   -------------------------------------------------------------------------------@@ -266,6 +265,8 @@ -- This uses the 'Conc' monad for testing, which is an instance of -- 'MonadConc'. If you need to test something which also uses -- 'MonadIO', use 'autocheckIO'.+--+-- @since 0.1.0.0 autocheck :: (Eq a, Show a)   => (forall t. ConcST t a)   -- ^ The computation to test@@ -285,8 +286,10 @@ -- -- __Warning:__ Using largers bounds will almost certainly -- significantly increase the time taken to test!-autocheckWay :: (Eq a, Show a, RandomGen g)-  => Way g+--+-- @since 0.6.0.0+autocheckWay :: (Eq a, Show a)+  => Way   -- ^ How to run the concurrent program.   -> MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.@@ -297,11 +300,15 @@   dejafusWay way memtype conc autocheckCases  -- | Variant of 'autocheck' for computations which do 'IO'.+--+-- @since 0.2.0.0 autocheckIO :: (Eq a, Show a) => ConcIO a -> IO Bool autocheckIO = autocheckWayIO defaultWay defaultMemType  -- | Variant of 'autocheckWay' for computations which do 'IO'.-autocheckWayIO :: (Eq a, Show a, RandomGen g) => Way g -> MemType -> ConcIO a -> IO Bool+--+-- @since 0.6.0.0+autocheckWayIO :: (Eq a, Show a) => Way -> MemType -> ConcIO a -> IO Bool autocheckWayIO way memtype concio =   dejafusWayIO way memtype concio autocheckCases @@ -315,6 +322,8 @@  -- | Check a predicate and print the result to stdout, return 'True' -- if it passes.+--+-- @since 0.1.0.0 dejafu :: Show a   => (forall t. ConcST t a)   -- ^ The computation to test@@ -325,8 +334,10 @@  -- | Variant of 'dejafu' which takes a way to run the program and a -- memory model.-dejafuWay :: (Show a, RandomGen g)-  => Way g+--+-- @since 0.6.0.0+dejafuWay :: Show a+  => Way   -- ^ How to run the concurrent program.   -> MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.@@ -339,6 +350,8 @@  -- | Variant of 'dejafu' which takes a collection of predicates to -- test, returning 'True' if all pass.+--+-- @since 0.1.0.0 dejafus :: Show a   => (forall t. ConcST t a)   -- ^ The computation to test@@ -349,8 +362,10 @@  -- | Variant of 'dejafus' which takes a way to run the program and a -- memory model.-dejafusWay :: (Show a, RandomGen g)-  => Way g+--+-- @since 0.6.0.0+dejafusWay :: Show a+  => Way   -- ^ How to run the concurrent program.   -> MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.@@ -362,27 +377,35 @@ dejafusWay way memtype conc tests = do   let traces = runST (runSCT way memtype conc)   results <- mapM (\(name, test) -> doTest name $ test traces) tests-  return $ and results+  pure (and results)  -- | Variant of 'dejafu' for computations which do 'IO'.+--+-- @since 0.2.0.0 dejafuIO :: Show a => ConcIO a -> (String, Predicate a) -> IO Bool dejafuIO = dejafuWayIO defaultWay defaultMemType  -- | Variant of 'dejafuWay' for computations which do 'IO'.-dejafuWayIO :: (Show a, RandomGen g) => Way g -> MemType -> ConcIO a -> (String, Predicate a) -> IO Bool+--+-- @since 0.6.0.0+dejafuWayIO :: Show a => Way -> MemType -> ConcIO a -> (String, Predicate a) -> IO Bool dejafuWayIO way memtype concio test =   dejafusWayIO way memtype concio [test]  -- | Variant of 'dejafus' for computations which do 'IO'.+--+-- @since 0.2.0.0 dejafusIO :: Show a => ConcIO a -> [(String, Predicate a)] -> IO Bool dejafusIO = dejafusWayIO defaultWay defaultMemType  -- | Variant of 'dejafusWay' for computations which do 'IO'.-dejafusWayIO :: (Show a, RandomGen g) => Way g -> MemType -> ConcIO a -> [(String, Predicate a)] -> IO Bool+--+-- @since 0.6.0.0+dejafusWayIO :: Show a => Way -> MemType -> ConcIO a -> [(String, Predicate a)] -> IO Bool dejafusWayIO way memtype concio tests = do   traces  <- runSCT way memtype concio   results <- mapM (\(name, test) -> doTest name $ test traces) tests-  return $ and results+  pure (and results)   -------------------------------------------------------------------------------@@ -390,6 +413,8 @@  -- | The results of a test, including the number of cases checked to -- determine the final boolean outcome.+--+-- @since 0.2.0.0 data Result a = Result   { _pass         :: Bool   -- ^ Whether the test passed or not.@@ -401,6 +426,7 @@   -- ^ A message to display on failure, if nonempty   } deriving (Eq, Show) +-- | @since 0.5.1.0 instance NFData a => NFData (Result a) where   rnf r = rnf ( _pass         r               , _casesChecked r@@ -424,6 +450,8 @@  -- | Run a predicate over all executions within the default schedule -- bounds.+--+-- @since 0.1.0.0 runTest ::     Predicate a   -- ^ The predicate to check@@ -435,8 +463,10 @@  -- | Variant of 'runTest' which takes a way to run the program and a -- memory model.-runTestWay :: RandomGen g-  => Way g+--+-- @since 0.6.0.0+runTestWay+  :: Way   -- ^ How to run the concurrent program.   -> MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.@@ -449,13 +479,17 @@   runST (runTestWayM way memtype predicate conc)  -- | Monad-polymorphic variant of 'runTest'.+--+-- @since 0.4.0.0 runTestM :: MonadRef r n-         => Predicate a -> Conc n r a -> n (Result a)+         => Predicate a -> ConcT r n a -> n (Result a) runTestM = runTestWayM defaultWay defaultMemType  -- | Monad-polymorphic variant of 'runTest''.-runTestWayM :: (MonadRef r n, RandomGen g)-            => Way g -> MemType -> Predicate a -> Conc n r a -> n (Result a)+--+-- @since 0.6.0.0+runTestWayM :: MonadRef r n+            => Way -> MemType -> Predicate a -> ConcT r n a -> n (Result a) runTestWayM way memtype predicate conc =   predicate <$> runSCT way memtype conc @@ -465,6 +499,8 @@  -- | A @Predicate@ is a function which collapses a list of results -- into a 'Result'.+--+-- @since 0.1.0.0 type Predicate a = [(Either Failure a, Trace)] -> Result a  -- | Reduce the list of failures in a @Predicate@ to one@@ -473,6 +509,8 @@ -- This may throw away \"duplicate\" failures which have a unique -- cause but happen to manifest in the same way. However, it is -- convenient for filtering out true duplicates.+--+-- @since 0.2.0.0 representative :: Eq a => Predicate a -> Predicate a representative p xs = result { _failures = choose . collect $ _failures result } where   result  = p xs@@ -491,48 +529,70 @@   insert' _ _ ([]:_) = undefined  -- | Check that a computation never aborts.+--+-- @since 0.2.0.0 abortsNever :: Predicate a abortsNever = alwaysTrue (not . either (==Abort) (const False))  -- | Check that a computation always aborts.+--+-- @since 0.2.0.0 abortsAlways :: Predicate a abortsAlways = alwaysTrue $ either (==Abort) (const False)  -- | Check that a computation aborts at least once.+--+-- @since 0.2.0.0 abortsSometimes :: Predicate a abortsSometimes = somewhereTrue $ either (==Abort) (const False)  -- | Check that a computation never deadlocks.+--+-- @since 0.1.0.0 deadlocksNever :: Predicate a deadlocksNever = alwaysTrue (not . either (`elem` [Deadlock, STMDeadlock]) (const False))  -- | Check that a computation always deadlocks.+--+-- @since 0.1.0.0 deadlocksAlways :: Predicate a deadlocksAlways = alwaysTrue $ either (`elem` [Deadlock, STMDeadlock]) (const False)  -- | Check that a computation deadlocks at least once.+--+-- @since 0.1.0.0 deadlocksSometimes :: Predicate a deadlocksSometimes = somewhereTrue $ either (`elem` [Deadlock, STMDeadlock]) (const False)  -- | Check that a computation never fails with an uncaught exception.+--+-- @since 0.1.0.0 exceptionsNever :: Predicate a exceptionsNever = alwaysTrue (not . either (==UncaughtException) (const False))  -- | Check that a computation always fails with an uncaught exception.+--+-- @since 0.1.0.0 exceptionsAlways :: Predicate a exceptionsAlways = alwaysTrue $ either (==UncaughtException) (const False)  -- | Check that a computation fails with an uncaught exception at least once.+--+-- @since 0.1.0.0 exceptionsSometimes :: Predicate a exceptionsSometimes = somewhereTrue $ either (==UncaughtException) (const False)  -- | Check that the result of a computation is always the same. In -- particular this means either: (a) it always fails in the same way, -- or (b) it never fails and the values returned are all equal.+--+-- @since 0.1.0.0 alwaysSame :: Eq a => Predicate a alwaysSame = representative $ alwaysTrue2 (==)  -- | Check that the result of a computation is not always the same.+--+-- @since 0.1.0.0 notAlwaysSame :: Eq a => Predicate a notAlwaysSame [x] = (defaultFail [x]) { _casesChecked = 1 } notAlwaysSame xs = go xs $ defaultFail [] where@@ -546,6 +606,8 @@  -- | Check that the result of a unary boolean predicate is always -- true.+--+-- @since 0.1.0.0 alwaysTrue :: (Either Failure a -> Bool) -> Predicate a alwaysTrue p xs = go xs $ (defaultFail failures) { _pass = True } where   go (y:ys) res@@ -561,6 +623,8 @@ -- -- If the predicate fails, /both/ (result,trace) tuples will be added -- to the failures list.+--+-- @since 0.1.0.0 alwaysTrue2 :: (Either Failure a -> Either Failure a -> Bool) -> Predicate a alwaysTrue2 _ [_] = defaultPass { _casesChecked = 1 } alwaysTrue2 p xs = go xs $ defaultPass { _failures = failures } where@@ -585,6 +649,8 @@  -- | Check that the result of a unary boolean predicate is true at -- least once.+--+-- @since 0.1.0.0 somewhereTrue :: (Either Failure a -> Bool) -> Predicate a somewhereTrue p xs = go xs $ defaultFail failures where   go (y:ys) res@@ -596,6 +662,8 @@  -- | Predicate for when there is a known set of results where every -- result must be exhibited at least once.+--+-- @since 0.2.0.0 gives :: (Eq a, Show a) => [Either Failure a] -> Predicate a gives expected results = go expected [] results $ defaultFail failures where   go waitingFor alreadySeen ((x, _):xs) res@@ -615,6 +683,8 @@   failures = filter (\(r, _) -> r `notElem` expected) results  -- | Variant of 'gives' that doesn't allow for expected failures.+--+-- @since 0.2.0.0 gives' :: (Eq a, Show a) => [a] -> Predicate a gives' = gives . map Right @@ -625,16 +695,19 @@ -- | A default way to execute concurrent programs: systematically -- using 'defaultBounds'. ----- The type parameter is constrained to 'StdGen', even though it is--- unused, to avoid ambiguity errors.-defaultWay :: Way StdGen+-- @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@@ -646,6 +719,8 @@ -- -- 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 @@ -653,6 +728,8 @@ -- -- This comes from playing around myself, but there is probably a -- better default.+--+-- @since 0.2.0.0 defaultFairBound :: FairBound defaultFairBound = 5 @@ -660,6 +737,8 @@ -- -- 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 @@ -687,7 +766,7 @@     when (moreThan 5 failures) $       putStrLn (indent "...") -  return $ _pass result+  pure (_pass result)  -- | Check if a list is longer than some value, without needing to -- compute the entire length.

@@ -6,9 +6,7 @@ -- Stability   : experimental -- Portability : portable ----- Common types and functions used throughout DejaFu. This module is--- NOT considered to form part of the public interface of this--- library.+-- Common types and functions used throughout DejaFu. module Test.DejaFu.Common   ( -- * Identifiers     ThreadId(..)@@ -60,18 +58,20 @@   , MemType(..)   ) where -import Control.DeepSeq (NFData(..))-import Control.Exception (MaskingState(..))-import Data.List (sort, nub, intercalate)-import Data.List.NonEmpty (NonEmpty)-import Data.Maybe (fromMaybe, mapMaybe)-import Data.Set (Set)-import qualified Data.Set as S+import           Control.DeepSeq    (NFData(..))+import           Control.Exception  (MaskingState(..))+import           Data.List          (intercalate, nub, sort)+import           Data.List.NonEmpty (NonEmpty)+import           Data.Maybe         (fromMaybe, mapMaybe)+import           Data.Set           (Set)+import qualified Data.Set           as S  ------------------------------------------------------------------------------- -- Identifiers  -- | Every live thread has a unique identitifer.+--+-- @since 0.4.0.0 data ThreadId = ThreadId (Maybe String) Int   deriving Eq @@ -82,10 +82,13 @@   show (ThreadId (Just n) _) = n   show (ThreadId Nothing  i) = show i +-- | @since 0.5.1.0 instance NFData ThreadId where   rnf (ThreadId n i) = rnf (n, i)  -- | Every @CRef@ has a unique identifier.+--+-- @since 0.4.0.0 data CRefId = CRefId (Maybe String) Int   deriving Eq @@ -96,10 +99,13 @@   show (CRefId (Just n) _) = n   show (CRefId Nothing  i) = show i +-- | @since 0.5.1.0 instance NFData CRefId where   rnf (CRefId n i) = rnf (n, i)  -- | Every @MVar@ has a unique identifier.+--+-- @since 0.4.0.0 data MVarId = MVarId (Maybe String) Int   deriving Eq @@ -110,10 +116,13 @@   show (MVarId (Just n) _) = n   show (MVarId Nothing  i) = show i +-- | @since 0.5.1.0 instance NFData MVarId where   rnf (MVarId n i) = rnf (n, i)  -- | Every @TVar@ has a unique identifier.+--+-- @since 0.4.0.0 data TVarId = TVarId (Maybe String) Int   deriving Eq @@ -124,10 +133,13 @@   show (TVarId (Just n) _) = n   show (TVarId Nothing  i) = show i +-- | @since 0.5.1.0 instance NFData TVarId where   rnf (TVarId n i) = rnf (n, i)  -- | The ID of the initial thread.+--+-- @since 0.4.0.0 initialThread :: ThreadId initialThread = ThreadId (Just "main") 0 @@ -136,6 +148,8 @@  -- | The number of ID parameters was getting a bit unwieldy, so this -- hides them all away.+--+-- @since 0.4.0.0 data IdSource = Id   { _nextCRId  :: Int   , _nextMVId  :: Int@@ -147,6 +161,7 @@   , _usedTNames  :: [String]   } deriving (Eq, Ord, Show) +-- | @since 0.5.1.0 instance NFData IdSource where   rnf idsource = rnf ( _nextCRId idsource                      , _nextMVId idsource@@ -159,6 +174,8 @@                      )  -- | Get the next free 'CRefId'.+--+-- @since 0.4.0.0 nextCRId :: String -> IdSource -> (IdSource, CRefId) nextCRId name idsource = (newIdSource, newCRId) where   newIdSource = idsource { _nextCRId = newId, _usedCRNames = newUsed }@@ -167,6 +184,8 @@   (newName, newUsed) = nextId name (_usedCRNames idsource)  -- | Get the next free 'MVarId'.+--+-- @since 0.4.0.0 nextMVId :: String -> IdSource -> (IdSource, MVarId) nextMVId name idsource = (newIdSource, newMVId) where   newIdSource = idsource { _nextMVId = newId, _usedMVNames = newUsed }@@ -175,6 +194,8 @@   (newName, newUsed) = nextId name (_usedMVNames idsource)  -- | Get the next free 'TVarId'.+--+-- @since 0.4.0.0 nextTVId :: String -> IdSource -> (IdSource, TVarId) nextTVId name idsource = (newIdSource, newTVId) where   newIdSource = idsource { _nextTVId = newId, _usedTVNames = newUsed }@@ -183,6 +204,8 @@   (newName, newUsed) = nextId name (_usedTVNames idsource)  -- | Get the next free 'ThreadId'.+--+-- @since 0.4.0.0 nextTId :: String -> IdSource -> (IdSource, ThreadId) nextTId name idsource = (newIdSource, newTId) where   newIdSource = idsource { _nextTId = newId, _usedTNames = newUsed }@@ -191,6 +214,8 @@   (newName, newUsed) = nextId name (_usedTNames idsource)  -- | The initial ID source.+--+-- @since 0.4.0.0 initialIdSource :: IdSource initialIdSource = Id 0 0 0 0 [] [] [] [] @@ -201,6 +226,8 @@ -- Thread actions  -- | All the actions that a thread can perform.+--+-- @since 0.5.0.2 data ThreadAction =     Fork ThreadId   -- ^ Start a new thread.@@ -288,6 +315,7 @@   -- ^ Stop executing an action with @subconcurrency@.   deriving (Eq, Show) +-- | @since 0.5.1.0 instance NFData ThreadAction where   rnf (Fork t) = rnf t   rnf (GetNumCapabilities c) = rnf c@@ -319,6 +347,8 @@   rnf a = a `seq` ()  -- | Check if a @ThreadAction@ immediately blocks.+--+-- @since 0.4.0.0 isBlock :: ThreadAction -> Bool isBlock (BlockedThrowTo  _) = True isBlock (BlockedTakeMVar _) = True@@ -328,6 +358,8 @@ isBlock _ = False  -- | Get the @TVar@s affected by a @ThreadAction@.+--+-- @since 0.4.0.0 tvarsOf :: ThreadAction -> Set TVarId tvarsOf act = S.fromList $ case act of   STM trc _ -> concatMap tvarsOf' trc@@ -345,6 +377,8 @@ -- Lookahead  -- | A one-step look-ahead at what a thread will do next.+--+-- @since 0.5.0.2 data Lookahead =     WillFork   -- ^ Will start a new thread.@@ -421,6 +455,7 @@   -- ^ Will stop executing an extion with @subconcurrency@.   deriving (Eq, Show) +-- | @since 0.5.1.0 instance NFData Lookahead where   rnf (WillSetNumCapabilities c) = rnf c   rnf (WillPutMVar m) = rnf m@@ -443,6 +478,8 @@  -- | Convert a 'ThreadAction' into a 'Lookahead': \"rewind\" what has -- happened. 'Killed' has no 'Lookahead' counterpart.+--+-- @since 0.4.0.0 rewind :: ThreadAction -> Maybe Lookahead rewind (Fork _) = Just WillFork rewind MyThreadId = Just WillMyThreadId@@ -484,6 +521,8 @@ rewind StopSubconcurrency = Just WillStopSubconcurrency  -- | Check if an operation could enable another thread.+--+-- @since 0.4.0.0 willRelease :: Lookahead -> Bool willRelease WillFork = True willRelease WillYield = True@@ -503,6 +542,8 @@ -- Simplified actions  -- | A simplified view of the possible actions a thread can perform.+--+-- @since 0.4.0.0 data ActionType =     UnsynchronisedRead  CRefId   -- ^ A 'readCRef' or a 'readForCAS'.@@ -528,6 +569,7 @@   -- communication.   deriving (Eq, Show) +-- | @since 0.5.1.0 instance NFData ActionType where   rnf (UnsynchronisedRead c) = rnf c   rnf (UnsynchronisedWrite c) = rnf c@@ -540,6 +582,8 @@   rnf a = a `seq` ()  -- | Check if an action imposes a write barrier.+--+-- @since 0.4.0.0 isBarrier :: ActionType -> Bool isBarrier (SynchronisedModify _) = True isBarrier (SynchronisedRead   _) = True@@ -548,6 +592,8 @@ isBarrier _ = False  -- | Check if an action commits a given 'CRef'.+--+-- @since 0.4.0.0 isCommit :: ActionType -> CRefId -> Bool isCommit (PartiallySynchronisedCommit c) r = c == r isCommit (PartiallySynchronisedWrite  c) r = c == r@@ -555,10 +601,14 @@ isCommit _ _ = False  -- | Check if an action synchronises a given 'CRef'.+--+-- @since 0.4.0.0 synchronises :: ActionType -> CRefId -> Bool synchronises a r = isCommit a r || isBarrier a  -- | Get the 'CRef' affected.+--+-- @since 0.4.0.0 crefOf :: ActionType -> Maybe CRefId crefOf (UnsynchronisedRead  r) = Just r crefOf (UnsynchronisedWrite r) = Just r@@ -569,6 +619,8 @@ crefOf _ = Nothing  -- | Get the 'MVar' affected.+--+-- @since 0.4.0.0 mvarOf :: ActionType -> Maybe MVarId mvarOf (SynchronisedRead  c) = Just c mvarOf (SynchronisedWrite c) = Just c@@ -579,10 +631,14 @@ -- -- This is used in the SCT code to help determine interesting -- alternative scheduling decisions.+--+-- @since 0.4.0.0 simplifyAction :: ThreadAction -> ActionType simplifyAction = maybe UnsynchronisedOther simplifyLookahead . rewind  -- | Variant of 'simplifyAction' that takes a 'Lookahead'.+--+-- @since 0.4.0.0 simplifyLookahead :: Lookahead -> ActionType simplifyLookahead (WillPutMVar c)     = SynchronisedWrite c simplifyLookahead (WillTryPutMVar c)  = SynchronisedWrite c@@ -606,9 +662,13 @@  -- | A trace of an STM transaction is just a list of actions that -- occurred, as there are no scheduling decisions to make.+--+-- @since 0.4.0.0 type TTrace = [TAction]  -- | All the actions that an STM transaction can perform.+--+-- @since 0.4.0.0 data TAction =     TNew   -- ^ Create a new @TVar@@@ -632,6 +692,7 @@   -- ^ Terminate successfully and commit effects.   deriving (Eq, Show) +-- | @since 0.5.1.0 instance NFData TAction where   rnf (TRead t) = rnf t   rnf (TWrite t) = rnf t@@ -645,12 +706,16 @@ -- | One of the outputs of the runner is a @Trace@, which is a log of -- decisions made, all the runnable threads and what they would do, -- and the action a thread took in its step.+--+-- @since 0.5.0.0 type Trace   = [(Decision, [(ThreadId, NonEmpty Lookahead)], ThreadAction)]  -- | Scheduling decisions are based on the state of the running -- program, and so we can capture some of that state in recording what -- specific decision we made.+--+-- @since 0.5.0.0 data Decision =     Start ThreadId   -- ^ Start a new thread, because the last was blocked (or it's the@@ -661,6 +726,7 @@   -- ^ Pre-empt the running thread, and switch to another.   deriving (Eq, Show) +-- | @since 0.5.1.0 instance NFData Decision where   rnf (Start t) = rnf t   rnf (SwitchTo t) = rnf t@@ -669,6 +735,8 @@ -- | Pretty-print a trace, including a key of the thread IDs (not -- including thread 0). Each line of the key is indented by two -- spaces.+--+-- @since 0.5.0.0 showTrace :: Trace -> String showTrace trc = intercalate "\n" $ concatMap go trc : strkey where   go (_,_,CommitCRef _ _) = "C-"@@ -693,6 +761,8 @@ -- SO, we don't count a switch TO a commit thread as a -- preemption. HOWEVER, the switch FROM a commit thread counts as a -- preemption if it is not to the thread that the commit interrupted.+--+-- @since 0.5.0.0 preEmpCount :: [(Decision, ThreadAction)]             -> (Decision, Lookahead)             -> Int@@ -722,6 +792,8 @@   -- | An indication of how a concurrent computation failed.+--+-- @since 0.5.0.0 data Failure =     InternalError   -- ^ Will be raised if the scheduler does something bad. This should@@ -743,10 +815,13 @@   -- multiple threads existed.   deriving (Eq, Show, Read, Ord, Enum, Bounded) +-- | @since 0.5.1.0 instance NFData Failure where   rnf f = f `seq` ()  -- | Pretty-print a failure+--+-- @since 0.4.0.0 showFail :: Failure -> String showFail Abort = "[abort]" showFail Deadlock = "[deadlock]"@@ -759,6 +834,8 @@ -- Memory Models  -- | The memory model to use for non-synchronised 'CRef' operations.+--+-- @since 0.4.0.0 data MemType =     SequentialConsistency   -- ^ The most intuitive model: a program behaves as a simple@@ -777,6 +854,7 @@   -- created.   deriving (Eq, Show, Read, Ord, Enum, Bounded) +-- | @since 0.5.1.0 instance NFData MemType where   rnf m = m `seq` () 

@@ -1,9 +1,9 @@-{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE MultiParamTypeClasses      #-}-{-# LANGUAGE RankNTypes                 #-}-{-# LANGUAGE TypeFamilies               #-}-{-# LANGUAGE TypeSynonymInstances       #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeSynonymInstances #-}  -- | -- Module      : Test.DejaFu.Conc@@ -19,8 +19,8 @@ -- out to the supplied scheduler after each step to determine which -- thread runs next. module Test.DejaFu.Conc-  ( -- * The @Conc@ Monad-    Conc+  ( -- * The @ConcT@ monad transformer+    ConcT   , ConcST   , ConcIO @@ -46,40 +46,43 @@   , module Test.DejaFu.Schedule   ) where -import Control.Exception (MaskingState(..))-import qualified Control.Monad.Base as Ba-import qualified Control.Monad.Catch as Ca-import qualified Control.Monad.IO.Class as IO-import Control.Monad.Ref (MonadRef)-import qualified Control.Monad.Ref as Re-import Control.Monad.ST (ST)-import qualified Data.Foldable as F-import Data.IORef (IORef)-import Data.STRef (STRef)-import Test.DejaFu.Schedule--import qualified Control.Monad.Conc.Class as C-import Test.DejaFu.Common-import Test.DejaFu.Conc.Internal-import Test.DejaFu.Conc.Internal.Common-import Test.DejaFu.STM+import           Control.Exception                (MaskingState(..))+import qualified Control.Monad.Base               as Ba+import qualified Control.Monad.Catch              as Ca+import qualified Control.Monad.IO.Class           as IO+import           Control.Monad.Ref                (MonadRef)+import qualified Control.Monad.Ref                as Re+import           Control.Monad.ST                 (ST)+import           Control.Monad.Trans.Class        (MonadTrans(..))+import qualified Data.Foldable                    as F+import           Data.IORef                       (IORef)+import           Data.STRef                       (STRef)+import           Test.DejaFu.Schedule -{-# ANN module ("HLint: ignore Avoid lambda" :: String) #-}-{-# ANN module ("HLint: ignore Use const"    :: String) #-}+import qualified Control.Monad.Conc.Class         as C+import           Test.DejaFu.Common+import           Test.DejaFu.Conc.Internal+import           Test.DejaFu.Conc.Internal.Common+import           Test.DejaFu.STM -newtype Conc n r a = C { unC :: M n r a } deriving (Functor, Applicative, Monad)+-- | @since 0.6.0.0+newtype ConcT r n a = C { unC :: M n r a } deriving (Functor, Applicative, Monad)  -- | A 'MonadConc' implementation using @ST@, this should be preferred -- if you do not need 'liftIO'.-type ConcST t = Conc (ST t) (STRef t)+--+-- @since 0.4.0.0+type ConcST t = ConcT (STRef t) (ST t)  -- | A 'MonadConc' implementation using @IO@.-type ConcIO = Conc IO IORef+--+-- @since 0.4.0.0+type ConcIO = ConcT IORef IO -toConc :: ((a -> Action n r) -> Action n r) -> Conc n r a+toConc :: ((a -> Action n r) -> Action n r) -> ConcT r n a toConc = C . cont -wrap :: (M n r a -> M n r a) -> Conc n r a -> Conc n r a+wrap :: (M n r a -> M n r a) -> ConcT r n a -> ConcT r n a wrap f = C . f . unC  instance IO.MonadIO ConcIO where@@ -88,8 +91,8 @@ instance Ba.MonadBase IO ConcIO where   liftBase = IO.liftIO -instance Re.MonadRef (CRef r) (Conc n r) where-  newRef a = toConc (\c -> ANewCRef "" a c)+instance Re.MonadRef (CRef r) (ConcT r n) where+  newRef a = toConc (ANewCRef "" a)    readRef ref = toConc (AReadCRef ref) @@ -97,25 +100,28 @@    modifyRef ref f = toConc (AModCRef ref (\a -> (f a, ()))) -instance Re.MonadAtomicRef (CRef r) (Conc n r) where+instance Re.MonadAtomicRef (CRef r) (ConcT r n) where   atomicModifyRef ref f = toConc (AModCRef ref f) -instance Ca.MonadCatch (Conc n r) where+instance MonadTrans (ConcT r) where+  lift ma = toConc (\c -> ALift (fmap c ma))++instance Ca.MonadCatch (ConcT r n) where   catch ma h = toConc (ACatching (unC . h) (unC ma)) -instance Ca.MonadThrow (Conc n r) where+instance Ca.MonadThrow (ConcT r n) where   throwM e = toConc (\_ -> AThrow e) -instance Ca.MonadMask (Conc n r) where+instance Ca.MonadMask (ConcT r n) where   mask                mb = toConc (AMasking MaskedInterruptible   (\f -> unC $ mb $ wrap f))   uninterruptibleMask mb = toConc (AMasking MaskedUninterruptible (\f -> unC $ mb $ wrap f)) -instance Monad n => C.MonadConc (Conc n r) where-  type MVar     (Conc n r) = MVar r-  type CRef     (Conc n r) = CRef r-  type Ticket   (Conc n r) = Ticket-  type STM      (Conc n r) = STMLike n r-  type ThreadId (Conc n r) = ThreadId+instance Monad n => C.MonadConc (ConcT r n) where+  type MVar     (ConcT r n) = MVar r+  type CRef     (ConcT r n) = CRef r+  type Ticket   (ConcT r n) = Ticket+  type STM      (ConcT r n) = STMLike n r+  type ThreadId (ConcT r n) = ThreadId    -- ---------- @@ -134,7 +140,7 @@    -- ---------- -  newCRefN n a = toConc (\c -> ANewCRef n a c)+  newCRefN n a = toConc (ANewCRef n a)    readCRef   ref = toConc (AReadCRef    ref)   readForCAS ref = toConc (AReadCRefCas ref)@@ -149,7 +155,7 @@    -- ---------- -  newEmptyMVarN n = toConc (\c -> ANewMVar n c)+  newEmptyMVarN n = toConc (ANewMVar n)    putMVar  var a = toConc (\c -> APutMVar var a (c ()))   readMVar var   = toConc (AReadMVar var)@@ -183,11 +189,13 @@ -- attempts to (a) schedule a blocked thread, or (b) schedule a -- nonexistent thread. In either of those cases, the computation will -- be halted.+--+-- @since 0.6.0.0 runConcurrent :: MonadRef r n               => Scheduler s               -> MemType               -> s-              -> Conc n r a+              -> 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)@@ -199,5 +207,7 @@ -- exist. Calls to 'subconcurrency' cannot be nested. Violating either -- of these conditions will result in the computation failing with -- @IllegalSubconcurrency@.-subconcurrency :: Conc n r a -> Conc n r (Either Failure a)+--+-- @since 0.6.0.0+subconcurrency :: ConcT r n a -> ConcT r n (Either Failure a) subconcurrency ma = toConc (ASub (unC ma))

@@ -1,5 +1,5 @@ {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}  -- |@@ -15,27 +15,28 @@ -- interface of this library. module Test.DejaFu.Conc.Internal where -import Control.Exception (MaskingState(..), toException)-import Control.Monad.Ref (MonadRef, newRef, readRef, writeRef)-import qualified Data.Foldable as F-import Data.Functor (void)-import Data.List (sort)-import Data.List.NonEmpty (NonEmpty(..), fromList)-import qualified Data.Map.Strict as M-import Data.Maybe (fromJust, isJust, isNothing)-import Data.Monoid ((<>))-import Data.Sequence (Seq, (<|))-import qualified Data.Sequence as Seq--import Test.DejaFu.Common-import Test.DejaFu.Conc.Internal.Common-import Test.DejaFu.Conc.Internal.Memory-import Test.DejaFu.Conc.Internal.Threading-import Test.DejaFu.Schedule-import Test.DejaFu.STM (Result(..), runTransaction)+import           Control.Exception                   (MaskingState(..),+                                                      toException)+import           Control.Monad.Ref                   (MonadRef, newRef, readRef,+                                                      writeRef)+import qualified Data.Foldable                       as F+import           Data.Functor                        (void)+import           Data.List                           (sort)+import           Data.List.NonEmpty                  (NonEmpty(..), fromList)+import qualified Data.Map.Strict                     as M+import           Data.Maybe                          (fromJust, isJust,+                                                      isNothing)+import           Data.Monoid                         ((<>))+import           Data.Sequence                       (Seq, (<|))+import qualified Data.Sequence                       as Seq -{-# ANN module ("HLint: ignore Use record patterns" :: String) #-}-{-# ANN module ("HLint: ignore Use const"           :: String) #-}+import           Test.DejaFu.Common+import           Test.DejaFu.Conc.Internal.Common+import           Test.DejaFu.Conc.Internal.Memory+import           Test.DejaFu.Conc.Internal.Threading+import           Test.DejaFu.Schedule+import           Test.DejaFu.STM                     (Result(..),+                                                      runTransaction)  -------------------------------------------------------------------------------- -- * Execution@@ -91,7 +92,7 @@       stepped <- stepThread sched memtype chosen (_continuation $ fromJust thread) $ ctx { cSchedState = g' }       case stepped of         (Right ctx', actOrTrc) ->-          let (act, trc) = getActAndTrc actOrTrc+          let (_, trc) = getActAndTrc actOrTrc               threads' = if (interruptible <$> M.lookup chosen (cThreads ctx')) /= Just False                          then unblockWaitingOn chosen (cThreads ctx')                          else cThreads ctx'

@@ -1,5 +1,5 @@ {-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE RankNTypes                #-}+{-# LANGUAGE RankNTypes #-}  -- | -- Module      : Test.DejaFu.Conc.Internal.Common@@ -13,13 +13,11 @@ -- 'MonadConc' implementations. This module is NOT considered to form module Test.DejaFu.Conc.Internal.Common where -import Control.Exception (Exception, MaskingState(..))-import Data.Map.Strict (Map)-import Data.List.NonEmpty (NonEmpty, fromList)-import Test.DejaFu.Common-import Test.DejaFu.STM (STMLike)--{-# ANN module ("HLint: ignore Use record patterns" :: String) #-}+import           Control.Exception  (Exception, MaskingState(..))+import           Data.List.NonEmpty (NonEmpty, fromList)+import           Data.Map.Strict    (Map)+import           Test.DejaFu.Common+import           Test.DejaFu.STM    (STMLike)  -------------------------------------------------------------------------------- -- * The @Conc@ Monad

@@ -1,5 +1,5 @@ {-# LANGUAGE BangPatterns #-}-{-# LANGUAGE GADTs        #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-}  -- |@@ -23,18 +23,20 @@ -- Memory Models/, N. Zhang, M. Kusano, and C. Wang (2015). module Test.DejaFu.Conc.Internal.Memory where -import Control.Monad (when)-import Control.Monad.Ref (MonadRef, readRef, writeRef)-import Data.Map.Strict (Map)-import Data.Maybe (isJust, fromJust)-import Data.Monoid ((<>))-import Data.Sequence (Seq, ViewL(..), (><), singleton, viewl)+import           Control.Monad                       (when)+import           Control.Monad.Ref                   (MonadRef, readRef,+                                                      writeRef)+import           Data.Map.Strict                     (Map)+import           Data.Maybe                          (fromJust, isJust)+import           Data.Monoid                         ((<>))+import           Data.Sequence                       (Seq, ViewL(..), singleton,+                                                      viewl, (><)) -import Test.DejaFu.Common-import Test.DejaFu.Conc.Internal.Common-import Test.DejaFu.Conc.Internal.Threading+import           Test.DejaFu.Common+import           Test.DejaFu.Conc.Internal.Common+import           Test.DejaFu.Conc.Internal.Threading -import qualified Data.Map.Strict as M+import qualified Data.Map.Strict                     as M  -------------------------------------------------------------------------------- -- * Manipulating @CRef@s@@ -68,30 +70,30 @@   (locals, count, def) <- readRef ref   writeRef ref (M.insert tid new locals, count, def) -  return $ WriteBuffer buffer'+  pure (WriteBuffer buffer')  -- | Commit the write at the head of a buffer. commitWrite :: MonadRef r n => WriteBuffer r -> (ThreadId, Maybe CRefId) -> n (WriteBuffer r) commitWrite w@(WriteBuffer wb) k = case maybe EmptyL viewl $ M.lookup k wb of   BufferedWrite _ cref a :< rest -> do     writeImmediate cref a-    return . WriteBuffer $ M.insert k rest wb+    pure . WriteBuffer $ M.insert k rest wb -  EmptyL -> return w+  EmptyL -> pure w  -- | Read from a @CRef@, returning a newer thread-local non-committed -- write if there is one. readCRef :: MonadRef r n => CRef r a -> ThreadId -> n a readCRef cref tid = do   (val, _) <- readCRefPrim cref tid-  return val+  pure val  -- | Read from a @CRef@, returning a @Ticket@ representing the current -- view of the thread. readForTicket :: MonadRef r n => CRef r a -> ThreadId -> n (Ticket a) readForTicket cref@(CRef crid _) tid = do   (val, count) <- readCRefPrim cref tid-  return $ Ticket crid count val+  pure (Ticket crid count val)  -- | Perform a compare-and-swap on a @CRef@ if the ticket is still -- valid. This is strict in the \"new\" value argument.@@ -103,15 +105,15 @@   then do     writeImmediate cref new     tick'' <- readForTicket cref tid-    return (True, tick'')-  else return (False, tick')+    pure (True, tick'')+  else pure (False, tick')  -- | Read the local state of a @CRef@. readCRefPrim :: MonadRef r n => CRef r a -> ThreadId -> n (a, Integer) readCRefPrim (CRef _ ref) tid = do   (vals, count, def) <- readRef ref -  return (M.findWithDefault def tid vals, count)+  pure (M.findWithDefault def tid vals, count)  -- | Write and commit to a @CRef@ immediately, clearing the update map -- and incrementing the write count.@@ -183,15 +185,15 @@     Just _       | blocking ->         let threads' = block (OnMVarEmpty cvid) threadid threads-        in return (False, threads', [])+        in pure (False, threads', [])        | otherwise ->-        return (False, goto (c False) threadid threads, [])+        pure (False, goto (c False) threadid threads, [])      Nothing -> do       writeRef ref $ Just a       let (threads', woken) = wake (OnMVarFull cvid) threads-      return (True, goto (c True) threadid threads', woken)+      pure (True, goto (c True) threadid threads', woken)  -- | Read a @MVar@, in either a blocking or nonblocking -- way.@@ -205,12 +207,12 @@     Just _ -> do       when emptying $ writeRef ref Nothing       let (threads', woken) = wake (OnMVarEmpty cvid) threads-      return (True, goto (c val) threadid threads', woken)+      pure (True, goto (c val) threadid threads', woken)      Nothing       | blocking ->         let threads' = block (OnMVarFull cvid) threadid threads-        in return (False, threads', [])+        in pure (False, threads', [])        | otherwise ->-        return (False, goto (c Nothing) threadid threads, [])+        pure (False, goto (c Nothing) threadid threads, [])

@@ -1,5 +1,5 @@ {-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE RankNTypes                #-}+{-# LANGUAGE RankNTypes #-}  -- | -- Module      : Test.DejaFu.Conc.Internal.Threading@@ -13,15 +13,16 @@ -- form part of the public interface of this library. module Test.DejaFu.Conc.Internal.Threading where -import Control.Exception (Exception, MaskingState(..), SomeException, fromException)-import Data.List (intersect)-import Data.Map.Strict (Map)-import Data.Maybe (fromMaybe, isJust)+import           Control.Exception                (Exception, MaskingState(..),+                                                   SomeException, fromException)+import           Data.List                        (intersect)+import           Data.Map.Strict                  (Map)+import           Data.Maybe                       (fromMaybe, isJust) -import Test.DejaFu.Common-import Test.DejaFu.Conc.Internal.Common+import           Test.DejaFu.Common+import           Test.DejaFu.Conc.Internal.Common -import qualified Data.Map.Strict as M+import qualified Data.Map.Strict                  as M  -------------------------------------------------------------------------------- -- * Threads@@ -116,7 +117,7 @@ launch' ms tid a = M.insert tid thread where   thread = Thread { _continuation = a umask, _blocking = Nothing, _handlers = [], _masking = ms } -  umask mb = resetMask True Unmasked >> mb >>= \b -> resetMask False ms >> return b+  umask mb = resetMask True Unmasked >> mb >>= \b -> resetMask False ms >> pure b   resetMask typ m = cont $ \k -> AResetMask typ True m $ k ()  -- | Kill a thread.

@@ -1,3 +1,4 @@+{-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}  -- |@@ -6,7 +7,7 @@ -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : GeneralizedNewtypeDeriving+-- Portability : GADTs, GeneralizedNewtypeDeriving -- -- Systematic testing for concurrent computations. module Test.DejaFu.SCT@@ -90,46 +91,49 @@   , sctRandom   ) where -import Control.DeepSeq (NFData(..))-import Control.Monad.Ref (MonadRef)-import Data.List (foldl')-import qualified Data.Map.Strict as M-import Data.Maybe (fromJust)-import Data.Set (Set)-import qualified Data.Set as S-import System.Random (RandomGen)+import           Control.DeepSeq          (NFData(..))+import           Control.Monad.Ref        (MonadRef)+import           Data.List                (foldl')+import qualified Data.Map.Strict          as M+import           Data.Set                 (Set)+import qualified Data.Set                 as S+import           System.Random            (RandomGen) -import Test.DejaFu.Common-import Test.DejaFu.Conc-import Test.DejaFu.SCT.Internal+import           Test.DejaFu.Common+import           Test.DejaFu.Conc+import           Test.DejaFu.SCT.Internal  ------------------------------------------------------------------------------- -- Running Concurrent Programs --- | How to explore the possible executions of a concurrent program.-data Way g-  = Systematically Bounds-  -- ^ Systematically explore all executions within the bounds.-  | Randomly g Int-  -- ^ Explore a fixed number of random executions, with the given-  -- PRNG.-  deriving (Eq, Ord, Read, Show)+-- | 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.+--+-- @since 0.6.0.0+data Way where+  Systematically :: Bounds -> Way+  Randomly :: RandomGen g => g -> Int -> Way -instance NFData g => NFData (Way g) where-  rnf (Systematically bs) = rnf bs-  rnf (Randomly g n) = rnf (g, n)+instance Show Way where+  show (Systematically bs) = "Systematically (" ++ show bs ++ ")"+  show (Randomly _ n)      = "Randomly <gen> " ++ show n  -- | Explore possible executions of a concurrent program. -- -- * If the 'Way' is @Systematically@, 'sctBound' is used. -- -- * If the 'Way' is @Randomly@, 'sctRandom' is used.-runSCT :: (MonadRef r n, RandomGen g)-  => Way g+--+-- @since 0.6.0.0+runSCT :: MonadRef r n+  => Way   -- ^ How to run the concurrent program.   -> MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.-  -> Conc n r a+  -> ConcT r n a   -- ^ The computation to run many times.   -> n [(Either Failure a, Trace)] runSCT (Systematically cb) memtype = sctBound memtype cb@@ -139,19 +143,23 @@ -- -- Demanding the result of this will force it to normal form, which -- may be more efficient in some situations.-runSCT' :: (MonadRef r n, RandomGen g, NFData a)-  => Way g -> MemType -> Conc n r a -> n [(Either Failure a, Trace)]+--+-- @since 0.6.0.0+runSCT' :: (MonadRef r n, NFData a)+  => Way -> MemType -> ConcT r n a -> n [(Either Failure a, Trace)] runSCT' way memtype conc = do   res <- runSCT way memtype conc   rnf res `seq` pure res  -- | Return the set of results of a concurrent program.-resultsSet :: (MonadRef r n, RandomGen g, Ord a)-  => Way g+--+-- @since 0.6.0.0+resultsSet :: (MonadRef r n, Ord a)+  => Way   -- ^ How to run the concurrent program.   -> MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.-  -> Conc n r a+  -> ConcT r n a   -- ^ The computation to run many times.   -> n (Set (Either Failure a)) resultsSet way memtype conc =@@ -161,8 +169,10 @@ -- -- Demanding the result of this will force it to normal form, which -- may be more efficient in some situations.-resultsSet' :: (MonadRef r n, RandomGen g, Ord a, NFData a)-  => Way g -> MemType -> Conc n r a -> n (Set (Either Failure a))+--+-- @since 0.6.0.0+resultsSet' :: (MonadRef r n, Ord a, NFData a)+  => Way -> MemType -> ConcT r n a -> n (Set (Either Failure a)) resultsSet' way memtype conc = do   res <- resultsSet' way memtype conc   rnf res `seq` pure res@@ -170,12 +180,14 @@ ------------------------------------------------------------------------------- -- Combined Bounds +-- | @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@@ -185,6 +197,8 @@ -- | 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@@ -212,17 +226,25 @@ ------------------------------------------------------------------------------- -- Pre-emption bounding +-- | @since 0.2.0.0 newtype PreemptionBound = PreemptionBound Int-  deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show, NFData)+  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+ -- | 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-  -> Conc n r a+  -> 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@@ -255,17 +277,25 @@ ------------------------------------------------------------------------------- -- Fair bounding +-- | @since 0.2.0.0 newtype FairBound = FairBound Int-  deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show, NFData)+  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+ -- | 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.-  -> Conc n r a+  -> 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@@ -284,17 +314,25 @@ ------------------------------------------------------------------------------- -- Length bounding +-- | @since 0.2.0.0 newtype LengthBound = LengthBound Int-  deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show, NFData)+  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+ -- | 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.-  -> Conc n r a+  -> 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)@@ -322,18 +360,20 @@ -- Note that unlike with non-bounded partial-order reduction, this may -- do some redundant work as the introduction of a bound can make -- previously non-interfering events interfere with each other.+--+-- @since 0.5.0.0 sctBound :: MonadRef r n   => MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.   -> Bounds   -- ^ The combined bounds.-  -> Conc n r a+  -> ConcT r n a   -- ^ The computation to run many times   -> n [(Either Failure a, Trace)] sctBound memtype cb conc = go initialState where   -- Repeatedly run the computation gathering all the results and   -- traces into a list until there are no schedules remaining to try.-  go dp = case nextPrefix dp of+  go dp = case findSchedulePrefix dp of     Just (prefix, conservative, sleep) -> do       (res, s, trace) <- runConcurrent scheduler                                        memtype@@ -349,9 +389,6 @@      Nothing -> pure [] -  -- Find the next schedule prefix.-  nextPrefix = findSchedulePrefix (>=initialThread)-   -- The DPOR scheduler.   scheduler = dporSched memtype (cBound cb) @@ -370,6 +407,8 @@ -- 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)   => MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.@@ -377,7 +416,7 @@   -- ^ The random number generator.   -> Int   -- ^ The number of executions to perform.-  -> Conc n r a+  -> ConcT r n a   -- ^ The computation to run many times.   -> n [(Either Failure a, Trace)] sctRandom memtype g0 lim0 conc = go g0 lim0 where

@@ -11,24 +11,26 @@ -- interface of this library. module Test.DejaFu.SCT.Internal where -import Control.DeepSeq (NFData(..))-import Control.Exception (MaskingState(..))-import Data.Char (ord)-import Data.Function (on)-import qualified Data.Foldable as F-import Data.List (intercalate, nubBy, partition, sortOn)-import Data.List.NonEmpty (NonEmpty(..), toList)-import Data.Map.Strict (Map)-import Data.Maybe (catMaybes, fromJust, isJust, isNothing, listToMaybe)-import qualified Data.Map.Strict as M-import Data.Set (Set)-import qualified Data.Set as S-import Data.Sequence (Seq, (|>))-import qualified Data.Sequence as Sq-import System.Random (RandomGen, randomR)+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.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.Sequence        (Seq, (|>))+import qualified Data.Sequence        as Sq+import           Data.Set             (Set)+import qualified Data.Set             as S+import           System.Random        (RandomGen, randomR) -import Test.DejaFu.Common-import Test.DejaFu.Schedule (Decision(..), Scheduler, decisionOf, tidOf)+import           Test.DejaFu.Common+import           Test.DejaFu.Schedule (Decision(..), Scheduler, decisionOf,+                                       tidOf)  ------------------------------------------------------------------------------- -- * Dynamic partial-order reduction@@ -114,18 +116,12 @@ -- to-do set. The intent is to put the system into a new state when -- executed with this initial sequence of scheduling decisions. findSchedulePrefix-  :: (ThreadId -> Bool)-  -- ^ Some partitioning function, applied to the to-do decisions. If-  -- there is an identifier which passes the test, it will be used,-  -- rather than any which fail it. This allows a very basic way of-  -- domain-specific prioritisation between otherwise equal choices,-  -- which may be useful in some cases.-  -> DPOR+  :: DPOR   -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)-findSchedulePrefix predicate = listToMaybe . go where+findSchedulePrefix = listToMaybe . go where   go dpor =     let prefixes = here dpor : map go' (M.toList $ dporDone dpor)-    in case concatPartition (\(t:_,_,_) -> predicate t) prefixes of+    in case concatPartition (\(t:_,_,_) -> t >= initialThread) prefixes of          ([], choices) -> choices          (choices, _)  -> choices @@ -172,7 +168,7 @@   -- Construct a new subtree corresponding to a trace suffix.   subtree state tid sleep ((_, _, a):rest) =     let state' = updateDepState state tid a-        sleep' = M.filterWithKey (\t a' -> not $ (dependent memtype) state' tid a t a') sleep+        sleep' = M.filterWithKey (\t a' -> not $ dependent memtype state' tid a t a') sleep     in DPOR         { dporRunnable = S.fromList $ case rest of             ((_, runnable, _):_) -> map fst runnable@@ -796,57 +792,6 @@ killsDaemons :: ThreadId -> Lookahead -> Bool killsDaemons t WillStop = t == initialThread killsDaemons _ _ = False---- | Render a 'DPOR' value as a graph in GraphViz \"dot\" format.-toDot :: (ThreadId -> String)-  -- ^ Show a @tid@ - this should produce a string suitable for-  -- use as a node identifier.-  -> (ThreadAction -> String)-  -- ^ Show a @action@.-  -> DPOR-  -> String-toDot = toDotFiltered (\_ _ -> True)---- | Render a 'DPOR' value as a graph in GraphViz \"dot\" format, with--- a function to determine if a subtree should be included or not.-toDotFiltered :: (ThreadId -> DPOR -> Bool)-  -- ^ Subtree predicate.-  -> (ThreadId -> String)-  -> (ThreadAction -> String)-  -> DPOR-  -> String-toDotFiltered check showTid showAct = digraph . go "L" where-  digraph str = "digraph {\n" ++ str ++ "\n}"--  go l b = unlines $ node l b : edges l b--  -- Display a labelled node.-  node n b = n ++ " [label=\"" ++ label b ++ "\"]"--  -- Display the edges.-  edges l b = [ edge l l' i ++ go l' b'-              | (i, b') <- M.toList (dporDone b)-              , check i b'-              , let l' = l ++ tidId i-              ]--  -- A node label, summary of the DPOR state at that node.-  label b = showLst id-    [ maybe "Nothing" (("Just " ++) . showAct) $ dporAction b-    , "Run:" ++ showLst showTid (S.toList $ dporRunnable b)-    , "Tod:" ++ showLst showTid (M.keys   $ dporTodo     b)-    , "Slp:" ++ showLst (\(t,a) -> "(" ++ showTid t ++ ", " ++ showAct a ++ ")")-        (M.toList $ dporSleep b)-    ]--  -- Display a labelled edge-  edge n1 n2 l = n1 ++ " -> " ++ n2 ++ " [label=\"" ++ showTid l ++ "\"]\n"--  -- Show a list of values-  showLst showf xs = "[" ++ intercalate ", " (map showf xs) ++ "]"--  -- Generate a graphviz-friendly identifier from a tid.-  tidId = concatMap (show . ord) . showTid  -- | Internal errors. err :: String -> String -> a

@@ -1,6 +1,6 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE RankNTypes                 #-}-{-# LANGUAGE TypeFamilies               #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}  -- | -- Module      : Test.DejaFu.STM@@ -26,18 +26,19 @@   , runTransaction   ) where -import Control.Monad (unless)-import Control.Monad.Catch (MonadCatch(..), MonadThrow(..))-import Control.Monad.Cont (cont)-import Control.Monad.Ref (MonadRef)-import Control.Monad.ST (ST)-import Data.IORef (IORef)-import Data.STRef (STRef)+import           Control.Monad            (unless)+import           Control.Monad.Catch      (MonadCatch(..), MonadThrow(..))+import           Control.Monad.Cont       (cont)+import           Control.Monad.Ref        (MonadRef)+import           Control.Monad.ST         (ST)+import           Data.IORef               (IORef)+import           Data.STRef               (STRef) -import qualified Control.Monad.STM.Class as C-import Test.DejaFu.Common-import Test.DejaFu.STM.Internal+import qualified Control.Monad.STM.Class  as C+import           Test.DejaFu.Common+import           Test.DejaFu.STM.Internal +-- | @since 0.3.0.0 newtype STMLike n r a = S { runSTM :: M n r a } deriving (Functor, Applicative, Monad)  -- | Create a new STM continuation.@@ -50,6 +51,8 @@ -- purely as references. This makes the types simpler, but means you -- can't really get an aggregate of them (if you ever wanted to for -- some reason).+--+-- @since 0.3.0.0 type STMST t = STMLike (ST t) (STRef t)  -- | A 'MonadSTM' implementation using @ST@, it encapsulates a single@@ -58,6 +61,8 @@ -- purely as references. This makes the types simpler, but means you -- can't really get an aggregate of them (if you ever wanted to for -- some reason).+--+-- @since 0.3.0.0 type STMIO = STMLike IO IORef  instance MonadThrow (STMLike n r) where@@ -82,6 +87,8 @@ -- | Run a transaction, returning the result and new initial -- 'TVarId'. If the transaction ended by calling 'retry', any 'TVar' -- modifications are undone.+--+-- @since 0.4.0.0 runTransaction :: MonadRef r n                => STMLike n r a -> IdSource -> n (Result a, IdSource, TTrace) runTransaction ma tvid = do

@@ -15,15 +15,14 @@ -- public interface of this library. module Test.DejaFu.STM.Internal where -import Control.DeepSeq (NFData(..))-import Control.Exception (Exception, SomeException, fromException, toException)-import Control.Monad.Cont (Cont, runCont)-import Control.Monad.Ref (MonadRef, newRef, readRef, writeRef)-import Data.List (nub)--import Test.DejaFu.Common+import           Control.DeepSeq    (NFData(..))+import           Control.Exception  (Exception, SomeException, fromException,+                                     toException)+import           Control.Monad.Cont (Cont, runCont)+import           Control.Monad.Ref  (MonadRef, newRef, readRef, writeRef)+import           Data.List          (nub) -{-# ANN module ("HLint: ignore Use record patterns" :: String) #-}+import           Test.DejaFu.Common  -------------------------------------------------------------------------------- -- The @STMLike@ monad@@ -60,6 +59,8 @@  -- | The result of an STM transaction, along with which 'TVar's it -- touched whilst executing.+--+-- @since 0.1.0.0 data Result a =     Success [TVarId] [TVarId] a   -- ^ The transaction completed successfully, reading the first list@@ -73,6 +74,8 @@   deriving Show  -- | This only reduces a 'SomeException' to WHNF.+--+-- @since 0.5.1.0 instance NFData a => NFData (Result a) where   rnf (Success tr1 tr2 a) = rnf (tr1, tr2, a)   rnf (Retry tr) = rnf tr@@ -102,15 +105,15 @@    let c = runCont ma (SStop . writeRef ref . Just . Right) -  (idsource', undo, readen, written, trace) <- go ref c (return ()) idsource [] [] []+  (idsource', undo, readen, written, trace) <- go ref c (pure ()) idsource [] [] []    res <- readRef ref    case res of-    Just (Right val) -> return (Success (nub readen) (nub written) val, undo, idsource', reverse trace)+    Just (Right val) -> pure (Success (nub readen) (nub written) val, undo, idsource', reverse trace) -    Just (Left  exc) -> undo >> return (Exception exc,      return (), idsource, reverse trace)-    Nothing          -> undo >> return (Retry $ nub readen, return (), idsource, reverse trace)+    Just (Left  exc) -> undo >> pure (Exception exc,      pure (), idsource, reverse trace)+    Nothing          -> undo >> pure (Retry $ nub readen, pure (), idsource, reverse trace)    where     go ref act undo nidsrc readen written sofar = do@@ -124,11 +127,13 @@           newSofar = tact : sofar        case tact of-        TStop  -> return (newIDSource, newUndo, newReaden, newWritten, TStop:newSofar)-        TRetry -> writeRef ref Nothing-          >> return (newIDSource, newUndo, newReaden, newWritten, TRetry:newSofar)-        TThrow -> writeRef ref (Just . Left $ case act of SThrow e -> toException e; _ -> undefined)-          >> return (newIDSource, newUndo, newReaden, newWritten, TThrow:newSofar)+        TStop  -> pure (newIDSource, newUndo, newReaden, newWritten, TStop:newSofar)+        TRetry -> do+          writeRef ref Nothing+          pure (newIDSource, newUndo, newReaden, newWritten, TRetry:newSofar)+        TThrow -> do+          writeRef ref (Just . Left $ case act of SThrow e -> toException e; _ -> undefined)+          pure (newIDSource, newUndo, newReaden, newWritten, TThrow:newSofar)         _ -> go ref newAct newUndo newIDSource newReaden newWritten newSofar  -- | Run a transaction for one step.@@ -141,50 +146,50 @@   SOrElse a b c   -> stepOrElse a b c   SStop   na      -> stepStop na -  SThrow e -> return (SThrow e, nothing, idsource, [], [], TThrow)-  SRetry   -> return (SRetry,   nothing, idsource, [], [], TRetry)+  SThrow e -> pure (SThrow e, nothing, idsource, [], [], TThrow)+  SRetry   -> pure (SRetry,   nothing, idsource, [], [], TRetry)    where-    nothing = return ()+    nothing = pure ()      stepCatch h stm c = cases TCatch stm c-      (\trace -> return (SRetry, nothing, idsource, [], [], TCatch trace Nothing))+      (\trace -> pure (SRetry, nothing, idsource, [], [], TCatch trace Nothing))       (\trace exc    -> case fromException exc of         Just exc' -> transaction (TCatch trace . Just) (h exc') c-        Nothing   -> return (SThrow exc, nothing, idsource, [], [], TCatch trace Nothing))+        Nothing   -> pure (SThrow exc, nothing, idsource, [], [], TCatch trace Nothing))      stepRead (TVar (tvid, ref)) c = do       val <- readRef ref-      return (c val, nothing, idsource, [tvid], [], TRead tvid)+      pure (c val, nothing, idsource, [tvid], [], TRead tvid)      stepWrite (TVar (tvid, ref)) a c = do       old <- readRef ref       writeRef ref a-      return (c, writeRef ref old, idsource, [], [tvid], TWrite tvid)+      pure (c, writeRef ref old, idsource, [], [tvid], TWrite tvid)      stepNew n a c = do       let (idsource', tvid) = nextTVId n idsource       ref <- newRef a       let tvar = TVar (tvid, ref)-      return (c tvar, nothing, idsource', [], [tvid], TNew)+      pure (c tvar, nothing, idsource', [], [tvid], TNew)      stepOrElse a b c = cases TOrElse a c       (\trace   -> transaction (TOrElse trace . Just) b c)-      (\trace exc -> return (SThrow exc, nothing, idsource, [], [], TOrElse trace Nothing))+      (\trace exc -> pure (SThrow exc, nothing, idsource, [], [], TOrElse trace Nothing))      stepStop na = do       na-      return (SStop na, nothing, idsource, [], [], TStop)+      pure (SStop na, nothing, idsource, [], [], TStop)      cases tact stm onSuccess onRetry onException = do       (res, undo, idsource', trace) <- doTransaction stm idsource       case res of-        Success readen written val -> return (onSuccess val, undo, idsource', readen, written, tact trace Nothing)+        Success readen written val -> pure (onSuccess val, undo, idsource', readen, written, tact trace Nothing)         Retry readen -> do           (res', undo', idsource'', readen', written', trace') <- onRetry trace           pure (res', undo', idsource'', readen ++ readen', written', trace')         Exception exc -> onException trace exc      transaction tact stm onSuccess = cases (\t _ -> tact t) stm onSuccess-      (\trace     -> return (SRetry, nothing, idsource, [], [], tact trace))-      (\trace exc -> return (SThrow exc, nothing, idsource, [], [], tact trace))+      (\trace     -> pure (SRetry, nothing, idsource, [], [], tact trace))+      (\trace exc -> pure (SThrow exc, nothing, idsource, [], [], tact trace))

@@ -29,10 +29,10 @@   , makeNonPreemptive   ) where -import Data.List.NonEmpty (NonEmpty(..), toList)-import System.Random (RandomGen, randomR)+import           Data.List.NonEmpty (NonEmpty(..), toList)+import           System.Random      (RandomGen, randomR) -import Test.DejaFu.Common+import           Test.DejaFu.Common  -- | A @Scheduler@ drives the execution of a concurrent program. The -- parameters it takes are:@@ -48,6 +48,8 @@ -- -- It returns a thread to execute, or @Nothing@ if execution should -- abort here, and also a new state.+--+-- @since 0.5.0.0 type Scheduler state   = [(Decision, ThreadAction)]   -> Maybe (ThreadId, ThreadAction)@@ -60,6 +62,8 @@  -- | Get the resultant thread identifier of a 'Decision', with a default case -- for 'Continue'.+--+-- @since 0.5.0.0 tidOf :: ThreadId -> Decision -> ThreadId tidOf _ (Start t)    = t tidOf _ (SwitchTo t) = t@@ -67,6 +71,8 @@  -- | Get the 'Decision' that would have resulted in this thread identifier, -- given a prior thread (if any) and list of runnable threads.+--+-- @since 0.5.0.0 decisionOf :: Foldable f   => Maybe ThreadId   -- ^ The prior thread.@@ -86,6 +92,8 @@  -- | A simple random scheduler which, at every step, picks a random -- thread to run.+--+-- @since 0.5.0.0 randomSched :: RandomGen g => Scheduler g randomSched _ _ threads g = (Just $ threads' !! choice, g') where   (choice, g') = randomR (0, length threads' - 1) g@@ -93,6 +101,8 @@  -- | A round-robin scheduler which, at every step, schedules the -- thread with the next 'ThreadId'.+--+-- @since 0.5.0.0 roundRobinSched :: Scheduler () roundRobinSched _ Nothing ((tid,_):|_) _ = (Just tid, ()) roundRobinSched _ (Just (prior, _)) threads _@@ -108,11 +118,15 @@ -- | A random scheduler which doesn't preempt the running -- thread. That is, if the last thread scheduled is still runnable, -- run that, otherwise schedule randomly.+--+-- @since 0.5.0.0 randomSchedNP :: RandomGen g => Scheduler g randomSchedNP = makeNonPreemptive randomSched  -- | A round-robin scheduler which doesn't preempt the running -- thread.+--+-- @since 0.5.0.0 roundRobinSchedNP :: Scheduler () roundRobinSchedNP = makeNonPreemptive roundRobinSched @@ -121,6 +135,8 @@  -- | Turn a potentially preemptive scheduler into a non-preemptive -- one.+--+-- @since 0.5.0.0 makeNonPreemptive :: Scheduler s -> Scheduler s makeNonPreemptive sched = newsched where   newsched trc p@(Just (prior, _)) threads s

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                dejafu-version:             0.5.1.3+version:             0.6.0.0 synopsis:            Systematic testing for Haskell concurrency.  description:@@ -18,43 +18,6 @@   <https://hackage.haskell.org/package/concurrency concurrency>   package by enabling you to systematically and deterministically test   your concurrent programs.-  .-  == Déjà Fu with 'IO':-  .-  The core assumption underlying Déjà Fu is that any apparent-  nondeterminism arises purely from the scheduling behaviour. To put-  it another way, a given computation, parametrised with a fixed set-  of scheduling decisions, is deterministic.-  .-  Whilst this assumption may not hold in general when 'IO' is-  involved, you should strive to produce test cases where it does.-  .-  == Memory Model-  .-  The testing functionality supports a few different memory models,-  for computations which use non-synchronised `CRef` operations. The-  supported models are:-  .-  * __Sequential Consistency:__ A program behaves as a simple-    interleaving of the actions in different threads. When a CRef is-    written to, that write is immediately visible to all threads.-  .-  * __Total Store Order (TSO):__ Each thread has a write buffer. A-    thread sees its writes immediately, but other threads will only-    see writes when they are committed, which may happen later. Writes-    are committed in the same order that they are created.-  .-  * __Partial Store Order (PSO):__ Each CRef has a write buffer. A-    thread sees its writes immediately, but other threads will only-    see writes when they are committed, which may happen later. Writes-    to different CRefs are not necessarily committed in the same order-    that they are created.-  .-  If a testing function does not take the memory model as a parameter,-  it uses TSO.-  .-  See the <https://github.com/barrucadu/dejafu README> for more-  details.  homepage:            https://github.com/barrucadu/dejafu license:             MIT@@ -64,7 +27,7 @@ -- copyright:            category:            Concurrency build-type:          Simple--- extra-source-files:  +extra-source-files:  README.markdown CHANGELOG.markdown cabal-version:       >=1.10  source-repository head@@ -74,7 +37,7 @@ source-repository this   type:     git   location: https://github.com/barrucadu/dejafu.git-  tag:      dejafu-0.5.1.3+  tag:      dejafu-0.6.0.0  library   exposed-modules:     Test.DejaFu