diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown new file mode 100644 --- /dev/null +++ b/CHANGELOG.markdown @@ -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 diff --git a/README.markdown b/README.markdown new file mode 100644 --- /dev/null +++ b/README.markdown @@ -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 diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -1,2 +1,2 @@ -import Distribution.Simple +import Distribution.Simple main = defaultMain diff --git a/Test/DejaFu.hs b/Test/DejaFu.hs --- a/Test/DejaFu.hs +++ b/Test/DejaFu.hs @@ -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. diff --git a/Test/DejaFu/Common.hs b/Test/DejaFu/Common.hs --- a/Test/DejaFu/Common.hs +++ b/Test/DejaFu/Common.hs @@ -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` () diff --git a/Test/DejaFu/Conc.hs b/Test/DejaFu/Conc.hs --- a/Test/DejaFu/Conc.hs +++ b/Test/DejaFu/Conc.hs @@ -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)) diff --git a/Test/DejaFu/Conc/Internal.hs b/Test/DejaFu/Conc/Internal.hs --- a/Test/DejaFu/Conc/Internal.hs +++ b/Test/DejaFu/Conc/Internal.hs @@ -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' diff --git a/Test/DejaFu/Conc/Internal/Common.hs b/Test/DejaFu/Conc/Internal/Common.hs --- a/Test/DejaFu/Conc/Internal/Common.hs +++ b/Test/DejaFu/Conc/Internal/Common.hs @@ -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 diff --git a/Test/DejaFu/Conc/Internal/Memory.hs b/Test/DejaFu/Conc/Internal/Memory.hs --- a/Test/DejaFu/Conc/Internal/Memory.hs +++ b/Test/DejaFu/Conc/Internal/Memory.hs @@ -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, []) diff --git a/Test/DejaFu/Conc/Internal/Threading.hs b/Test/DejaFu/Conc/Internal/Threading.hs --- a/Test/DejaFu/Conc/Internal/Threading.hs +++ b/Test/DejaFu/Conc/Internal/Threading.hs @@ -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. diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} -- | @@ -6,7 +7,7 @@ -- License : MIT -- Maintainer : Michael Walker -- 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 " ++ 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 diff --git a/Test/DejaFu/SCT/Internal.hs b/Test/DejaFu/SCT/Internal.hs --- a/Test/DejaFu/SCT/Internal.hs +++ b/Test/DejaFu/SCT/Internal.hs @@ -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 diff --git a/Test/DejaFu/STM.hs b/Test/DejaFu/STM.hs --- a/Test/DejaFu/STM.hs +++ b/Test/DejaFu/STM.hs @@ -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 diff --git a/Test/DejaFu/STM/Internal.hs b/Test/DejaFu/STM/Internal.hs --- a/Test/DejaFu/STM/Internal.hs +++ b/Test/DejaFu/STM/Internal.hs @@ -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)) diff --git a/Test/DejaFu/Schedule.hs b/Test/DejaFu/Schedule.hs --- a/Test/DejaFu/Schedule.hs +++ b/Test/DejaFu/Schedule.hs @@ -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 diff --git a/dejafu.cabal b/dejafu.cabal --- a/dejafu.cabal +++ b/dejafu.cabal @@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: dejafu -version: 0.5.1.3 +version: 0.6.0.0 synopsis: Systematic testing for Haskell concurrency. description: @@ -18,43 +18,6 @@ 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 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