diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown --- a/CHANGELOG.markdown +++ b/CHANGELOG.markdown @@ -7,6 +7,118 @@ *de facto* standard Haskell versioning scheme. +1.0.0.0 +------- + +- **Date** 2017-12-23 +- **Git tag** [dejafu-1.0.0.0][] +- **Hackage** https://hackage.haskell.org/package/dejafu-1.0.0.0 + +### Test.DejaFu + +- All testing functions now require a `MonadConc`, `MonadRef`, and `MonadIO` constraint: + + It is no longer possible to test things in `ST`. + +- All testing functions now take the action to test as the last parameter. + +- The `autocheckIO`, `dejafuIO`, `dejafusIO`, `autocheckWayIO`, `dejafuWayIO`, `dejafusWayIO`, + `dejafuDiscardIO`, `runTestM`, and `runTestWayM` functions are now gone. + +- The `Predicate` type has been replaced with a more general `ProPredicate` type which is a + profunctor and (b) can discard results not needed to determine if the predicate passes. (#124) + + All testing functions have been generalised to take a `ProPredicate` instead. The `Predicate a` + type remains as an alias for `ProPredicate a a`. Passing tests have their resident memory usage + significantly decreased. + +- The `Result` type no longer includes a number of cases checked, as this is not meaningful with + predicates including discard functions. + +- New `alwaysNothing` and `somewhereNothing` functions, like `alwaysTrue` and `somewhereTrue`, to + lift functions to `ProPredicate`s. + +- The `alwaysTrue2` function is gone, as its behaviour was unintuitive and easy to get wrong, and + has been replaced with new `alwaysSameOn` and `alwaysSameBy` predicates, which generalise + `alwaysSame`. + +- The `alwaysSame`, `alwaysSameOn`, and `alwaysSameBy` predicates now gives the simplest execution + trace leading to each distinct result. + +### Test.DejaFu.Common + +- This module has been split up into new Test.DejaFu.Internal, Types, and Utils modules. (#155) + +- New `ForkOS` and `IsCurrentThreadBound` thread actions. (#126) + +- New `WillForkOS` and `WillIsCurrentThreadBound` lookaheads. (#126) + +- The `TTrace` type synonym for `[TAction]` has been removed. + +- The `preEmpCount` function has been removed. + +- New functions `strengthenDiscard` and `weakenDiscard` to combine discard functions. + +- The `Discard` type is now defined here and re-exported from Test.DejaFu.SCT. + +- The `ThreadId`, `CRefId`, `MVarId`, and `TVarId` types are now newtypes over a common `Id` + type. (#137) + +### Test.DejaFu.Conc + +- The `ConcST` type alias is gone. + +- The `MonadBase IO ConcIO` instance is gone. + +- The `MonadIO ConcIO` instance is replaces with a more general `MonadIO n => MonadIO (ConcT r n)` + instance. + +- The `runConcurrent` function now has a `MonadConc` constraint. + +- If bound threads are supported, the main thread when testing is bound. (#126) + +- Each entry in an execution trace is now in the form `(decision, alternatives, action)`. The + chosen thread is no longer in the list of alternatives, which makes raw traces easier to + read. (#121) + +- Due to changes in Test.DejaFu.Schedule, no longer re-exports `Decision`, `NonEmpty`, `tidOf`, or + `decisionOf`. + +### Test.DejaFu.Refinement + +- A blocking interference function is no longer reported as a deadlocking execution. + +### Test.DejaFu.Schedule + +- No longer re-exports `Decision` or `NonEmpty`. + +- The `tidOf` and `decisionOf` functions have moved to Test.DejaFu.Utils. + +### Test.DejaFu.SCT + +- All testing functions now require a `MonadConc` constraint: + + It is no longer possible to test things in `ST`. + +### Test.DejaFu.STM + +- This is now an internal module. (#155) + +### Performance + +- Significant resident memory reduction for most passing tests. +- Improved dependency detection for `MVar` actions, leading to fewer executions. + +### Miscellaneous + +- The minimum supported version of concurrency is now 1.3.0.0. + +[dejafu-1.0.0.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-1.0.0.0 + + +--------------------------------------------------------------------------------------------------- + + 0.9.1.2 ------- diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c) 2015, Michael Walker +Copyright (c) 2015--2017, Michael Walker Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the diff --git a/README.markdown b/README.markdown --- a/README.markdown +++ b/README.markdown @@ -7,58 +7,125 @@ > > -- 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. +- [Installation](#installation) +- [Quick start guide](#quick-start-guide) +- [Why Déjà Fu?](#why-déjà-fu) +- [Contributing](#contributing) +- [Release notes](#release-notes) +- [Questions, feedback, discussion](#questions-feedback-discussion) +- [Bibliography](#bibliography) +- **[The website!](http://dejafu.readthedocs.io/)** -This package builds on the concurrency package (also in this -repository) by enabling you to systematically and deterministically -test your concurrent programs. +Déjà Fu is a unit-testing library for concurrent Haskell programs. +Tests are deterministic and expressive, making it easy and convenient +to test your threaded code. Available on [GitHub][], [Hackage][], and +[Stackage][]. -The documentation of the latest developmental version is -[available online][docs]. Examples can be found in the test suite. +[GitHub]: https://github.com/barrucadu/dejafu +[Hackage]: https://hackage.haskell.org/package/dejafu +[Stackage]: https://www.stackage.org/package/dejafu -**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` ----------------- +Installation +------------ -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. +Install from Hackage globally: -Whilst this assumption may not hold in general when `IO` is involved, -you should strive to produce test cases where it does. +``` +$ cabal install dejafu +``` -Memory Model +Or add it to your cabal file: + +``` +build-depends: ... + , dejafu +``` + +Or to your package.yaml: + +``` +dependencies: + ... + - dejafu +``` + + +Quick start guide +----------------- + +Déjà Fu supports unit testing, and comes with a helper function called +`autocheck` to look for some common issues. Let's see it in action: + +```haskell +import Control.Concurrent.Classy + +myFunction :: MonadConc m => m String +myFunction = do + var <- newEmptyMVar + fork (putMVar var "hello") + fork (putMVar var "world") + readMVar var +``` + +That `MonadConc` is a typeclass abstraction over concurrency, but +we'll get onto that shortly. First, the result of testing: + +``` +> autocheck myFunction +[pass] Never Deadlocks +[pass] No Exceptions +[fail] Consistent Result + "hello" S0----S1--S0-- + + "world" S0----S2--S0-- +False +``` + +There are no deadlocks or uncaught exceptions, which is good; but the +program is (as you probably spotted) nondeterministic! + +Along with each result, Déjà Fu gives us a representative execution +trace in an abbreviated form. `Sn` means that thread `n` started +executing, and `Pn` means that thread `n` pre-empted the previously +running thread. + + +Why Déjà Fu? ------------ -The testing functionality supports a few different memory models, for -computations which use non-synchronised `CRef` operations. The -supported models are: +Testing concurrent programs is difficult, because in general they are +nondeterministic. This leads to people using work-arounds like +running their testsuite many thousands of times; or running their +testsuite while putting their machine under heavy load. -- **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. +These approaches are inadequate for a few reasons: -- **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. +- **How many runs is enough?** When you are just hopping to spot a bug + by coincidence, how do you know to stop? +- **How do you know if you've fixed a bug you saw previously?** + Because the scheduler is a black box, you don't know if the + previously buggy schedule has been re-run. +- **You won't get that much scheduling variety!** Operating systems + and language runtimes like to run threads for long periods of time, + which reduces the variety you get (and so drives up the number of + runs you need). -- **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. +Déjà Fu addresses these points by offering *complete* testing. You +can run a test case and be guaranteed to find all results with some +bounds. These bounds can be configured, or even disabled! The +underlying approach used is smarter than merely trying all possible +executions, and will in general explore the state-space quickly. -If a testing function does not take the memory model as a parameter, -it uses TSO. +If your test case is just too big for complete testing, there is also +a random scheduling mode, which is necessarily *incomplete*. However, +Déjà Fu will tend to produce much more schedule variety than just +running your test case in `IO` the same number of times, and so bugs +will tend to crop up sooner. Furthermore, as you get execution traces +out, you can be certain that a bug has been fixed by simply following +the trace by eye. + Contributing ------------ @@ -66,7 +133,3 @@ 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/Test/DejaFu.hs b/Test/DejaFu.hs --- a/Test/DejaFu.hs +++ b/Test/DejaFu.hs @@ -1,801 +1,942 @@ -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE RankNTypes #-} - --- | --- Module : Test.DejaFu --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- Stability : experimental --- Portability : RankNTypes --- --- Deterministic testing for concurrent computations. --- --- As an example, consider this program, which has two locks and a --- shared variable. Two threads are spawned, which claim the locks, --- update the shared variable, and release the locks. The main thread --- waits for them both to terminate, and returns the final result. --- --- > example1 :: MonadConc m => m Int --- > example1 = do --- > a <- newEmptyMVar --- > b <- newEmptyMVar --- > --- > c <- newMVar 0 --- > --- > let lock m = putMVar m () --- > let unlock = takeMVar --- > --- > j1 <- spawn $ lock a >> lock b >> modifyMVar_ c (return . succ) >> unlock b >> unlock a --- > j2 <- spawn $ lock b >> lock a >> modifyMVar_ c (return . pred) >> unlock a >> unlock b --- > --- > takeMVar j1 --- > takeMVar j2 --- > --- > takeMVar c --- --- The correct result is 0, as it starts out as 0 and is incremented --- and decremented by threads 1 and 2, respectively. However, note the --- order of acquisition of the locks in the two threads. If thread 2 --- pre-empts thread 1 between the acquisition of the locks (or if --- thread 1 pre-empts thread 2), a deadlock situation will arise, as --- thread 1 will have lock @a@ and be waiting on @b@, and thread 2 --- will have @b@ and be waiting on @a@. --- --- Here is what Deja Fu has to say about it: --- --- > > autocheck example1 --- > [fail] Never Deadlocks (checked: 5) --- > [deadlock] S0------------S1-P2--S1- --- > [pass] No Exceptions (checked: 12) --- > [fail] Consistent Result (checked: 11) --- > 0 S0------------S2-----------------S1-----------------S0---- --- > --- > [deadlock] S0------------S1-P2--S1- --- > False --- --- It identifies the deadlock, and also the possible results the --- computation can produce, and displays a simplified trace leading to --- each failing outcome. The trace contains thread numbers, and the --- names (which can be set by the programmer) are displayed beneath. --- It also returns @False@ as there are test failures. The automatic --- testing functionality is good enough if you only want to check your --- computation is deterministic, but if you have more specific --- requirements (or have some expected and tolerated level of --- nondeterminism), you can write tests yourself using the @dejafu*@ --- functions. --- --- __Warning:__ If your computation under test does @IO@, the @IO@ --- will be executed lots of times! Be sure that it is deterministic --- enough not to invalidate your test results. Mocking may be useful --- where possible. -module Test.DejaFu - ( -- * Testing - - -- | Testing in Deja Fu is similar to unit testing, the programmer - -- produces a self-contained monadic action to execute under - -- different schedules, and supplies a list of predicates to apply - -- to the list of results produced. - -- - -- If you simply wish to check that something is deterministic, see - -- the 'autocheck' and 'autocheckIO' functions. - -- - -- These functions use a Total Store Order (TSO) memory model for - -- unsynchronised actions, see \"Testing under Alternative Memory - -- Models\" for some explanation of this. - - autocheck - , dejafu - , dejafus - , autocheckIO - , dejafuIO - , dejafusIO - - -- * Testing with different settings - - , Way - , defaultWay - , systematically - , randomly - , uniformly - , swarmy - - , autocheckWay - , autocheckWayIO - , dejafuWay - , dejafuWayIO - , dejafusWay - , dejafusWayIO - - , Discard(..) - , defaultDiscarder - - , dejafuDiscard - , dejafuDiscardIO - - -- ** Memory Models - - -- | Threads running under modern multicore processors do not behave - -- as a simple interleaving of the individual thread - -- actions. Processors do all sorts of complex things to increase - -- speed, such as buffering writes. For concurrent programs which - -- make use of non-synchronised functions (such as 'readCRef' - -- coupled with 'writeCRef') different memory models may yield - -- different results. - -- - -- As an example, consider this program (modified from the - -- Data.IORef documentation). Two @CRef@s are created, and two - -- threads spawned to write to and read from both. Each thread - -- returns the value it observes. - -- - -- > example2 :: MonadConc m => m (Bool, Bool) - -- > example2 = do - -- > r1 <- newCRef False - -- > r2 <- newCRef False - -- > - -- > x <- spawn $ writeCRef r1 True >> readCRef r2 - -- > y <- spawn $ writeCRef r2 True >> readCRef r1 - -- > - -- > (,) <$> readMVar x <*> readMVar y - -- - -- Under a sequentially consistent memory model the possible results - -- are @(True, True)@, @(True, False)@, and @(False, True)@. Under - -- total or partial store order, @(False, False)@ is also a possible - -- result, even though there is no interleaving of the threads which - -- can lead to this. - -- - -- We can see this by testing with different memory models: - -- - -- > > autocheckWay defaultWay SequentialConsistency example2 - -- > [pass] Never Deadlocks (checked: 6) - -- > [pass] No Exceptions (checked: 6) - -- > [fail] Consistent Result (checked: 5) - -- > (False,True) S0-------S1-----S0--S2-----S0--- - -- > (True,False) S0-------S1-P2-----S1----S0---- - -- > (True,True) S0-------S1--P2-----S1---S0---- - -- > (False,True) S0-------S1---P2-----S1--S0---- - -- > (True,False) S0-------S2-----S1-----S0---- - -- > ... - -- > False - -- - -- > > autocheckWay defaultWay TotalStoreOrder example2 - -- > [pass] Never Deadlocks (checked: 303) - -- > [pass] No Exceptions (checked: 303) - -- > [fail] Consistent Result (checked: 302) - -- > (False,True) S0-------S1-----C-S0--S2-----C-S0--- - -- > (True,False) S0-------S1-P2-----C-S1----S0---- - -- > (True,True) S0-------S1-P2--C-S1----C-S0--S2---S0--- - -- > (False,True) S0-------S1-P2--P1--C-C-S1--S0--S2---S0--- - -- > (False,False) S0-------S1-P2--P1----S2---C-C-S0---- - -- > ... - -- > False - -- - -- Traces for non-sequentially-consistent memory models show where - -- writes to @CRef@s are /committed/, which makes a write visible to - -- all threads rather than just the one which performed the - -- write. Only 'writeCRef' is broken up into separate write and - -- commit steps, 'atomicModifyCRef' is still atomic and imposes a - -- memory barrier. - - , MemType(..) - , defaultMemType - - -- ** Schedule Bounding - - -- | Schedule bounding is an optimisation which only considers - -- schedules within some /bound/. This sacrifices completeness - -- outside of the bound, but can drastically reduce the number of - -- schedules to test, and is in fact necessary for non-terminating - -- programs. - -- - -- The standard testing mechanism uses a combination of pre-emption - -- bounding, fair bounding, and length bounding. Pre-emption + fair - -- bounding is useful for programs which use loop/yield control - -- flows but are otherwise terminating. Length bounding makes it - -- possible to test potentially non-terminating programs. - - , Bounds(..) - , defaultBounds - , noBounds - , PreemptionBound(..) - , defaultPreemptionBound - , FairBound(..) - , defaultFairBound - , LengthBound(..) - , defaultLengthBound - - -- * Results - - -- | The results of a test can be pretty-printed to the console, as - -- with the above functions, or used in their original, much richer, - -- form for debugging purposes. These functions provide full access - -- to this data type which, most usefully, contains a detailed trace - -- of execution, showing what each thread did at each point. - - , Result(..) - , Failure(..) - , runTest - , runTestWay - , runTestM - , runTestWayM - - -- * Predicates - - -- | Predicates evaluate a list of results of execution and decide - -- whether some test case has passed or failed. They can be lazy and - -- make use of short-circuit evaluation to avoid needing to examine - -- the entire list of results, and can check any property which can - -- be defined for the return type of your monadic action. - -- - -- A collection of common predicates are provided, along with the - -- helper functions 'alwaysTrue', 'alwaysTrue2' and 'somewhereTrue' - -- to lfit predicates over a single result to over a collection of - -- results. - - , Predicate - , representative - , abortsNever - , abortsAlways - , abortsSometimes - , deadlocksNever - , deadlocksAlways - , deadlocksSometimes - , exceptionsNever - , exceptionsAlways - , exceptionsSometimes - , alwaysSame - , notAlwaysSame - , alwaysTrue - , alwaysTrue2 - , somewhereTrue - , gives - , gives' - - -- ** Failures - - , isInternalError - , isAbort - , isDeadlock - , isUncaughtException - , isIllegalSubconcurrency - - -- * Refinement property testing - - -- | Consider this statement about @MVar@s: \"using @readMVar@ is - -- better than @takeMVar@ followed by @putMVar@ because the former - -- is atomic but the latter is not.\" - -- - -- Deja Fu can test properties like that: - -- - -- @ - -- sig e = Sig - -- { initialise = maybe newEmptyMVar newMVar - -- , observe = \\v _ -> tryReadMVar v - -- , interfere = \\v s -> tryTakeMVar v >> maybe (pure ()) (void . tryPutMVar v) s - -- , expression = e - -- } - -- - -- > check $ sig (void . readMVar) \`equivalentTo\` sig (\\v -> takeMVar v >>= putMVar v) - -- *** Failure: (seed Just ()) - -- left: [(Nothing,Just ())] - -- right: [(Nothing,Just ()),(Just Deadlock,Just ())] - -- @ - -- - -- The two expressions are not equivalent, and we get given the - -- counterexample! - , module Test.DejaFu.Refinement - ) where - -import Control.Arrow (first) -import Control.DeepSeq (NFData(..)) -import Control.Monad (unless, when) -import Control.Monad.Ref (MonadRef) -import Control.Monad.ST (runST) -import Data.Function (on) -import Data.List (intercalate, intersperse, minimumBy) -import Data.Ord (comparing) - -import Test.DejaFu.Common -import Test.DejaFu.Conc -import Test.DejaFu.Defaults -import Test.DejaFu.Refinement -import Test.DejaFu.SCT - - -------------------------------------------------------------------------------- --- DejaFu - --- | Automatically test a computation. In particular, look for --- deadlocks, uncaught exceptions, and multiple return values. --- --- 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 - -> IO Bool -autocheck = autocheckWay defaultWay defaultMemType - --- | Variant of 'autocheck' which takes a way to run the program and a --- memory model. --- --- Schedule bounding is used to filter the large number of possible --- schedules, and can be iteratively increased for further coverage --- guarantees. Empirical studies (/Concurrency Testing Using Schedule --- Bounding: an Empirical Study/, P. Thompson, A. Donaldson, and --- A. Betts) have found that many concurrency bugs can be exhibited --- with as few as two threads and two pre-emptions, which is part of --- what 'dejafus' uses. --- --- __Warning:__ Using largers bounds will almost certainly --- significantly increase the time taken to test! --- --- @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. - -> (forall t. ConcST t a) - -- ^ The computation to test - -> IO Bool -autocheckWay way memtype conc = - 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'. --- --- @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 - --- | Predicates for the various autocheck functions. -autocheckCases :: Eq a => [(String, Predicate a)] -autocheckCases = - [ ("Never Deadlocks", representative deadlocksNever) - , ("No Exceptions", representative exceptionsNever) - , ("Consistent Result", alwaysSame) -- already representative - ] - --- | 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 - -> (String, Predicate a) - -- ^ The predicate (with a name) to check - -> IO Bool -dejafu = dejafuWay defaultWay defaultMemType - --- | Variant of 'dejafu' which takes a way to run the program and a --- memory model. --- --- @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. - -> (forall t. ConcST t a) - -- ^ The computation to test - -> (String, Predicate a) - -- ^ The predicate (with a name) to check - -> IO Bool -dejafuWay = dejafuDiscard (const Nothing) - --- | Variant of 'dejafuWay' which can selectively discard results. --- --- @since 0.7.1.0 -dejafuDiscard :: Show a - => (Either Failure a -> Maybe Discard) - -- ^ Selectively discard results. - -> Way - -- ^ How to run the concurrent program. - -> MemType - -- ^ The memory model to use for non-synchronised @CRef@ operations. - -> (forall t. ConcST t a) - -- ^ The computation to test - -> (String, Predicate a) - -- ^ The predicate (with a name) to check - -> IO Bool -dejafuDiscard discard way memtype conc (name, test) = do - let traces = runST (runSCTDiscard discard way memtype conc) - doTest name (test traces) - --- | 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 - -> [(String, Predicate a)] - -- ^ The list of predicates (with names) to check - -> IO Bool -dejafus = dejafusWay defaultWay defaultMemType - --- | Variant of 'dejafus' which takes a way to run the program and a --- memory model. --- --- @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. - -> (forall t. ConcST t a) - -- ^ The computation to test - -> [(String, Predicate a)] - -- ^ The list of predicates (with names) to check - -> IO Bool -dejafusWay way memtype conc tests = do - let traces = runST (runSCT way memtype conc) - results <- mapM (\(name, test) -> doTest name $ test traces) tests - 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'. --- --- @since 0.6.0.0 -dejafuWayIO :: Show a => Way -> MemType -> ConcIO a -> (String, Predicate a) -> IO Bool -dejafuWayIO = dejafuDiscardIO (const Nothing) - --- | Variant of 'dejafuDiscard' for computations which do 'IO'. --- --- @since 0.7.1.0 -dejafuDiscardIO :: Show a => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcIO a -> (String, Predicate a) -> IO Bool -dejafuDiscardIO discard way memtype concio (name, test) = do - traces <- runSCTDiscard discard way memtype concio - doTest name (test traces) - --- | 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'. --- --- @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 - pure (and results) - - -------------------------------------------------------------------------------- --- Test cases - --- | 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. - , _casesChecked :: Int - -- ^ The number of cases checked. - , _failures :: [(Either Failure a, Trace)] - -- ^ The failing cases, if any. - , _failureMsg :: String - -- ^ 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 - , _failures r - , _failureMsg r - ) - --- | A failed result, taking the given list of failures. -defaultFail :: [(Either Failure a, Trace)] -> Result a -defaultFail failures = Result False 0 failures "" - --- | A passed result. -defaultPass :: Result a -defaultPass = Result True 0 [] "" - -instance Functor Result where - fmap f r = r { _failures = map (first $ fmap f) $ _failures r } - -instance Foldable Result where - foldMap f r = foldMap f [a | (Right a, _) <- _failures r] - --- | Run a predicate over all executions within the default schedule --- bounds. --- --- @since 0.1.0.0 -runTest :: - Predicate a - -- ^ The predicate to check - -> (forall t. ConcST t a) - -- ^ The computation to test - -> Result a -runTest test conc = - runST (runTestM test conc) - --- | Variant of 'runTest' which takes a way to run the program and a --- memory model. --- --- @since 0.6.0.0 -runTestWay - :: Way - -- ^ How to run the concurrent program. - -> MemType - -- ^ The memory model to use for non-synchronised @CRef@ operations. - -> Predicate a - -- ^ The predicate to check - -> (forall t. ConcST t a) - -- ^ The computation to test - -> Result a -runTestWay way memtype predicate conc = - runST (runTestWayM way memtype predicate conc) - --- | Monad-polymorphic variant of 'runTest'. --- --- @since 0.4.0.0 -runTestM :: MonadRef r n - => Predicate a -> ConcT r n a -> n (Result a) -runTestM = runTestWayM defaultWay defaultMemType - --- | Monad-polymorphic variant of 'runTest''. --- --- @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 - - -------------------------------------------------------------------------------- --- Predicates - --- | 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 --- representative trace for each unique result. --- --- 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 - collect = groupBy' [] ((==) `on` fst) - choose = map $ minimumBy (comparing $ \(_, trc) -> (preEmps trc, length trc)) - - preEmps trc = preEmpCount (map (\(d,_,a) -> (d, a)) trc) (Continue, WillStop) - - groupBy' res _ [] = res - groupBy' res eq (y:ys) = groupBy' (insert' eq y res) eq ys - - insert' _ x [] = [[x]] - insert' eq x (ys@(y:_):yss) - | x `eq` y = (x:ys) : yss - | otherwise = ys : insert' eq x yss - 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 isDeadlock (const False)) - --- | Check that a computation always deadlocks. --- --- @since 0.1.0.0 -deadlocksAlways :: Predicate a -deadlocksAlways = alwaysTrue $ either isDeadlock (const False) - --- | Check that a computation deadlocks at least once. --- --- @since 0.1.0.0 -deadlocksSometimes :: Predicate a -deadlocksSometimes = somewhereTrue $ either isDeadlock (const False) - --- | Check that a computation never fails with an uncaught exception. --- --- @since 0.1.0.0 -exceptionsNever :: Predicate a -exceptionsNever = alwaysTrue (not . either isUncaughtException (const False)) - --- | Check that a computation always fails with an uncaught exception. --- --- @since 0.1.0.0 -exceptionsAlways :: Predicate a -exceptionsAlways = alwaysTrue $ either isUncaughtException (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 isUncaughtException (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 - go [y1,y2] res - | fst y1 /= fst y2 = incCC res { _pass = True } - | otherwise = incCC res { _failures = y1 : y2 : _failures res } - go (y1:y2:ys) res - | fst y1 /= fst y2 = go (y2:ys) . incCC $ res { _pass = True } - | otherwise = go (y2:ys) . incCC $ res { _failures = y1 : y2 : _failures res } - go _ res = res - --- | 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 - | p (fst y) = go ys . incCC $ res - | otherwise = incCC $ res { _pass = False } - go [] res = res - - failures = filter (not . p . fst) xs - --- | Check that the result of a binary boolean predicate is true --- between all pairs of results. Only properties which are transitive --- and symmetric should be used here. --- --- 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 - go [y1,y2] res - | p (fst y1) (fst y2) = incCC res - | otherwise = incCC res { _pass = False } - go (y1:y2:ys) res - | p (fst y1) (fst y2) = go (y2:ys) . incCC $ res - | otherwise = go (y2:ys) . incCC $ res { _pass = False } - go _ res = res - - failures = fgo xs where - fgo (y1:y2:ys) - | p (fst y1) (fst y2) = fgo (y2:ys) - | otherwise = y1 : y2 : fgo2 y2 ys - fgo _ = [] - - fgo2 y1 (y2:ys) - | p (fst y1) (fst y2) = fgo (y2:ys) - | otherwise = y2 : fgo2 y2 ys - fgo2 _ _ = [] - --- | 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 - | p (fst y) = incCC $ res { _pass = True } - | otherwise = go ys . incCC $ res { _failures = y : _failures res } - go [] res = res - - failures = filter (not . p . fst) xs - --- | 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 - -- If it's a result we're waiting for, move it to the - -- @alreadySeen@ list and continue. - | x `elem` waitingFor = go (filter (/=x) waitingFor) (x:alreadySeen) xs res { _casesChecked = _casesChecked res + 1 } - - -- If it's a result we've already seen, continue. - | x `elem` alreadySeen = go waitingFor alreadySeen xs res { _casesChecked = _casesChecked res + 1 } - - -- If it's not a result we expected, fail. - | otherwise = res { _casesChecked = _casesChecked res + 1 } - - go [] _ [] res = res { _pass = True } - go es _ [] res = res { _failureMsg = unlines $ map (\e -> "Expected: " ++ show e) es } - - 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 - - -------------------------------------------------------------------------------- --- Utils - --- | Run a test and print to stdout -doTest :: Show a => String -> Result a -> IO Bool -doTest name result = do - if _pass result - then - -- Display a pass message. - putStrLn $ "\27[32m[pass]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")" - else do - -- Display a failure message, and the first 5 (simplified) failed traces - putStrLn ("\27[31m[fail]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")") - - unless (null $ _failureMsg result) $ - putStrLn $ _failureMsg result - - let failures = _failures result - let output = map (\(r, t) -> putStrLn . indent $ either showFail show r ++ " " ++ showTrace t) $ take 5 failures - sequence_ $ intersperse (putStrLn "") output - when (moreThan 5 failures) $ - putStrLn (indent "...") - - pure (_pass result) - --- | Check if a list is longer than some value, without needing to --- compute the entire length. -moreThan :: Int -> [a] -> Bool -moreThan n [] = n < 0 -moreThan 0 _ = True -moreThan n (_:rest) = moreThan (n-1) rest - --- | Increment the cases -incCC :: Result a -> Result a -incCC r = r { _casesChecked = _casesChecked r + 1 } +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TupleSections #-} + +{- | +Module : Test.DejaFu +Copyright : (c) 2015--2017 Michael Walker +License : MIT +Maintainer : Michael Walker +Stability : experimental +Portability : LambdaCase, MultiParamTypeClasses, TupleSections + +dejafu is a library for unit-testing concurrent Haskell programs, +written using the [concurrency](https://hackage.haskell.org/package/concurrency) +package's 'MonadConc' typeclass. + +__A first test:__ This is a simple concurrent program which forks two +threads and each races to write to the same @MVar@: + +> example = do +> var <- newEmptyMVar +> fork (putMVar var "hello") +> fork (putMVar var "world") +> readMVar var + +We can test it with dejafu like so: + +> > autocheck example +> [pass] Never Deadlocks +> [pass] No Exceptions +> [fail] Consistent Result +> "hello" S0----S1--S0-- +> +> "world" S0----S2--S0-- + +The 'autocheck' function takes a concurrent program to test and looks +for some common unwanted behaviours: deadlocks, uncaught exceptions in +the main thread, and nondeterminism. Here we see the program is +nondeterministic, dejafu gives us all the distinct results it found +and, for each, a summarised execution trace leading to that result: + + * \"Sn\" means that thread \"n\" started executing after the previous + thread terminated or blocked. + + * \"Pn\" means that thread \"n\" started executing, even though the + previous thread could have continued running. + + * Each \"-\" represents one \"step\" of the computation. + +__Failures:__ If a program doesn't terminate successfully, we say it +has /failed/. dejafu can detect a few different types of failure: + + * 'Deadlock', if every thread is blocked. + + * 'STMDeadlock', if every thread is blocked /and/ the main thread is + blocked in an STM transaction. + + * 'UncaughtException', if the main thread is killed by an exception. + +There are two types of failure which dejafu itself may raise: + + * 'Abort', used in systematic testing (the default) if there are no + allowed decisions remaining. For example, by default any test case + which takes more than 250 scheduling points to finish will be + aborted. You can use the 'systematically' function to supply (or + disable) your own bounds. + + * 'InternalError', used if something goes wrong. If you get this and + aren't using a scheduler you wrote yourself, please [file a + bug](https://github.com/barrucadu/dejafu/issues). + +Finally, there is one failure which can arise through improper use of +dejafu: + + * 'IllegalSubconcurrency', the "Test.DejaFu.Conc.subconcurrency" + function is used when multiple threads exist, or is used inside + another @subconcurrency@ call. + +__Beware of 'liftIO':__ dejafu works by running your test case lots of +times with different schedules. If you use 'liftIO' at all, make sure +that any @IO@ you perform is deterministic when executed in the same +order. + +If you need to test things with /nondeterministc/ @IO@, see the +'autocheckWay', 'dejafuWay', and 'dejafusWay' functions: the +'randomly', 'uniformly', and 'swarmy' testing modes can cope with +nondeterminism. +-} +module Test.DejaFu + ( -- * Unit testing + + autocheck + , dejafu + , dejafus + + -- ** Configuration + + {- | + +There are a few knobs to tweak to control the behaviour of dejafu. +The defaults should generally be good enough, but if not you have a +few tricks available. + + * The 'Way', which controls how schedules are explored. + + * The 'MemType', which controls how reads and writes to @CRef@s (or + @IORef@s) behave. + + * The 'Discard' function, which saves memory by throwing away + uninteresting results during exploration. + +-} + + , autocheckWay + , dejafuWay + , dejafusWay + , dejafuDiscard + + -- *** Defaults + + , defaultWay + , defaultMemType + , defaultDiscarder + + -- *** Exploration + + , Way + , systematically + , randomly + , uniformly + , swarmy + + -- **** Schedule bounding + + {- | + +Schedule bounding is used by the 'systematically' approach to limit +the search-space, which in general will be huge. + +There are three types of bounds used: + + * The 'PreemptionBound', which bounds the number of pre-emptive + context switches. Empirical evidence suggests @2@ is a good value + for this, if you have a small test case. + + * The 'FairBound', which bounds the difference between how many times + threads can yield. This is necessary to test certain kinds of + potentially non-terminating behaviour, such as spinlocks. + + * The 'LengthBound', which bounds how long a test case can run, in + terms of scheduling decisions. This is necessary to test certain + kinds of potentially non-terminating behaviour, such as livelocks. + +Schedule bounding is not used by the non-systematic exploration +behaviours. + +-} + + , Bounds(..) + , defaultBounds + , noBounds + , PreemptionBound(..) + , defaultPreemptionBound + , FairBound(..) + , defaultFairBound + , LengthBound(..) + , defaultLengthBound + + -- *** Memory model + + {- | + +When executed on a multi-core processor some @CRef@ / @IORef@ programs +can exhibit \"relaxed memory\" behaviours, where the apparent +behaviour of the program is not a simple interleaving of the actions +of each thread. + +__Example:__ This is a simple program which creates two @CRef@s +containing @False@, and forks two threads. Each thread writes @True@ +to one of the @CRef@s and reads the other. The value that each thread +reads is communicated back through an @MVar@: + +> relaxed = do +> r1 <- newCRef False +> r2 <- newCRef False +> x <- spawn $ writeCRef r1 True >> readCRef r2 +> y <- spawn $ writeCRef r2 True >> readCRef r1 +> (,) <$> readMVar x <*> readMVar y + +We see something surprising if we ask for the results: + +> > autocheck relaxed +> [pass] Never Deadlocks +> [pass] No Exceptions +> [fail] Consistent Result +> (False,True) S0---------S1----S0--S2----S0-- +> +> (False,False) S0---------S1--P2----S1--S0--- +> +> (True,False) S0---------S2----S1----S0--- +> +> (True,True) S0---------S1-C-S2----S1---S0--- + +It's possible for both threads to read the value @False@, even though +each writes @True@ to the other @CRef@ before reading. This is +because processors are free to re-order reads and writes to +independent memory addresses in the name of performance. + +Execution traces for relaxed memory computations can include \"C\" +actions, as above, which show where @CRef@ writes were explicitly +/committed/, and made visible to other threads. + +However, modelling this behaviour can require more executions. If you +do not care about the relaxed-memory behaviour of your program, use +the 'SequentialConsistency' model. + +-} + + , MemType(..) + + -- *** Reducing memory usage + + {- | + +Sometimes we know that a result is uninteresting and cannot affect the +result of a test, in which case there is no point in keeping it +around. Execution traces can be large, so any opportunity to get rid +of them early is possibly a great saving of memory. + +A discard function, which has type @Either Failure a -> Maybe +Discard@, can selectively discard results or execution traces before +the schedule exploration finishes, allowing them to be garbage +collected sooner. + +__Note:__ This is only relevant if you are producing your own +predicates. The predicates and helper functions provided by this +module do discard results and traces wherever possible. + +-} + + , Discard(..) + + -- ** Manual testing + + {- | + +The standard testing functions print their result to stdout, and throw +away some information. The traces are pretty-printed, and if there +are many failures, only the first few are shown. + +If you need more information, use these functions. + +-} + + , Result(..) + , Failure(..) + , runTest + , runTestWay + + -- ** Predicates + + {- | + +A dejafu test has two parts: the concurrent program to test, and a +predicate to determine if the test passes, based on the results of the +schedule exploration. + +All of these predicates discard results and traces as eagerly as +possible, to reduce memory usage. + +-} + + , Predicate + , ProPredicate(..) + , abortsNever + , abortsAlways + , abortsSometimes + , deadlocksNever + , deadlocksAlways + , deadlocksSometimes + , exceptionsNever + , exceptionsAlways + , exceptionsSometimes + + -- *** Helpers + + {- | + +Helper functions to produce your own predicates. Such predicates +discard results and traces as eagerly as possible, to reduce memory +usage. + +-} + + , representative + , alwaysSame + , alwaysSameOn + , alwaysSameBy + , notAlwaysSame + , alwaysTrue + , somewhereTrue + , alwaysNothing + , somewhereNothing + , gives + , gives' + + -- *** Failures + + {- | + +Helper functions to identify failures. + +-} + + , isInternalError + , isAbort + , isDeadlock + , isUncaughtException + , isIllegalSubconcurrency + + -- * Property testing + + {- | + +dejafu can also use a property-testing style to test stateful +operations for a variety of inputs. Inputs are generated using the +[leancheck](https://hackage.haskell.org/package/leancheck) library for +enumerative testing. + +__Testing @MVar@ operations with multiple producers__: + +These are a little different to the property tests you may be familiar +with from libraries like QuickCheck (and leancheck). As we're testing +properties of /stateful/ and /concurrent/ things, we need to provide +some extra information. + +A property consists of two /signatures/ and a relation between them. +A signature contains: + + * An initialisation function, to construct the initial state. + + * An observation function, to take a snapshot of the state at the + end. + + * An interference function, to mess with the state in some way. + + * The expression to evaluate, as a function over the state. + +> sig e = Sig +> { initialise = maybe newEmptyMVar newMVar +> , observe = \v _ -> tryReadMVar v +> , interfere = \v _ -> putMVar v 42 +> , expression = void . e +> } + +This is a signature for operations over @Num n => MVar n@ values where +there are multiple producers. The initialisation function takes a +@Maybe n@ and constructs an @MVar n@, empty if it gets @Nothing@; the +observation function reads the @MVar@; and the interference function +puts a new value in. + +Given this signature, we can check if @readMVar@ is the same as a +@takeMVar@ followed by a @putMVar@: + +> > check $ sig readMVar === sig (\v -> takeMVar v >>= putMVar v) +> *** Failure: (seed Just 0) +> left: [(Nothing,Just 0)] +> right: [(Nothing,Just 0),(Just Deadlock,Just 42)] + +The two expressions are not equivalent, and we get a counterexample: +if the @MVar@ is nonempty, then the left expression (@readMVar@) will +preserve the value, but the right expression (@\v -> takeMVar v >>= +putMVar v@) may cause it to change. This is because of the concurrent +interference we have provided: the left term never empties a full +@MVar@, but the Right term does. + +-} + + , module Test.DejaFu.Refinement + ) where + +import Control.Arrow (first) +import Control.DeepSeq (NFData(..)) +import Control.Monad (unless, when) +import Control.Monad.Conc.Class (MonadConc) +import Control.Monad.IO.Class (MonadIO(..)) +import Control.Monad.Ref (MonadRef) +import Data.Function (on) +import Data.List (intercalate, intersperse) +import Data.Maybe (catMaybes, isNothing, mapMaybe) +import Data.Profunctor (Profunctor(..)) + +import Test.DejaFu.Conc +import Test.DejaFu.Defaults +import Test.DejaFu.Refinement +import Test.DejaFu.SCT +import Test.DejaFu.Types +import Test.DejaFu.Utils + + +------------------------------------------------------------------------------- +-- DejaFu + +-- | Automatically test a computation. +-- +-- In particular, look for deadlocks, uncaught exceptions, and +-- multiple return values. Returns @True@ if all tests pass +-- +-- > > autocheck example +-- > [pass] Never Deadlocks +-- > [pass] No Exceptions +-- > [fail] Consistent Result +-- > "hello" S0----S1--S0-- +-- > +-- > "world" S0----S2--S0-- +-- +-- @since 1.0.0.0 +autocheck :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a) + => ConcT r n a + -- ^ The computation to test. + -> n Bool +autocheck = autocheckWay defaultWay defaultMemType + +-- | Variant of 'autocheck' which takes a way to run the program and a +-- memory model. +-- +-- > > autocheckWay defaultWay defaultMemType relaxed +-- > [pass] Never Deadlocks +-- > [pass] No Exceptions +-- > [fail] Consistent Result +-- > (False,True) S0---------S1----S0--S2----S0-- +-- > +-- > (False,False) S0---------S1--P2----S1--S0--- +-- > +-- > (True,False) S0---------S2----S1----S0--- +-- > +-- > (True,True) S0---------S1-C-S2----S1---S0--- +-- > +-- > > autocheckWay defaultWay SequentialConsistency relaxed +-- > [pass] Never Deadlocks +-- > [pass] No Exceptions +-- > [fail] Consistent Result +-- > (False,True) S0---------S1----S0--S2----S0-- +-- > +-- > (True,True) S0---------S1-P2----S1---S0--- +-- > +-- > (True,False) S0---------S2----S1----S0--- +-- +-- @since 1.0.0.0 +autocheckWay :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a) + => Way + -- ^ How to run the concurrent program. + -> MemType + -- ^ The memory model to use for non-synchronised @CRef@ operations. + -> ConcT r n a + -- ^ The computation to test. + -> n Bool +autocheckWay way memtype = dejafusWay way memtype autocheckCases + +-- | Predicates for the various autocheck functions. +autocheckCases :: Eq a => [(String, Predicate a)] +autocheckCases = + [ ("Never Deadlocks", representative deadlocksNever) + , ("No Exceptions", representative exceptionsNever) + , ("Consistent Result", alwaysSame) -- already representative + ] + +-- | Check a predicate and print the result to stdout, return 'True' +-- if it passes. +-- +-- A dejafu test has two parts: the program you are testing, and a +-- predicate to determine if the test passes. Predicates can look for +-- anything, including checking for some expected nondeterminism. +-- +-- > > dejafu "Test Name" alwaysSame example +-- > [fail] Test Name +-- > "hello" S0----S1--S0-- +-- > +-- > "world" S0----S2--S0-- +-- +-- @since 1.0.0.0 +dejafu :: (MonadConc n, MonadIO n, MonadRef r n, Show b) + => String + -- ^ The name of the test. + -> ProPredicate a b + -- ^ The predicate to check. + -> ConcT r n a + -- ^ The computation to test. + -> n Bool +dejafu = dejafuWay defaultWay defaultMemType + +-- | Variant of 'dejafu' which takes a way to run the program and a +-- memory model. +-- +-- > > import System.Random +-- > +-- > > dejafuWay (randomly (mkStdGen 0) 100) defaultMemType "Randomly!" alwaysSame example +-- > [fail] Randomly! +-- > "hello" S0----S1--S0-- +-- > +-- > "world" S0----S2--S0-- +-- > +-- > > dejafuWay (randomly (mkStdGen 1) 100) defaultMemType "Randomly!" alwaysSame example +-- > [fail] Randomly! +-- > "hello" S0----S1--S0-- +-- > +-- > "world" S0----S2--S1-S0-- +-- +-- @since 1.0.0.0 +dejafuWay :: (MonadConc n, MonadIO n, MonadRef r n, Show b) + => Way + -- ^ How to run the concurrent program. + -> MemType + -- ^ The memory model to use for non-synchronised @CRef@ operations. + -> String + -- ^ The name of the test. + -> ProPredicate a b + -- ^ The predicate to check. + -> ConcT r n a + -- ^ The computation to test. + -> n Bool +dejafuWay = dejafuDiscard (const Nothing) + +-- | Variant of 'dejafuWay' which can selectively discard results. +-- +-- > > dejafuDiscard (\_ -> Just DiscardTrace) defaultWay defaultMemType "Discarding" alwaysSame example +-- > [fail] Discarding +-- > "hello" +-- > +-- > "world" +-- +-- @since 1.0.0.0 +dejafuDiscard :: (MonadConc n, MonadIO n, MonadRef r n, Show b) + => (Either Failure a -> Maybe Discard) + -- ^ Selectively discard results. + -> Way + -- ^ How to run the concurrent program. + -> MemType + -- ^ The memory model to use for non-synchronised @CRef@ operations. + -> String + -- ^ The name of the test. + -> ProPredicate a b + -- ^ The predicate to check. + -> ConcT r n a + -- ^ The computation to test. + -> n Bool +dejafuDiscard discard way memtype name test conc = do + let discarder = strengthenDiscard discard (pdiscard test) + traces <- runSCTDiscard discarder way memtype conc + liftIO $ doTest name (peval test traces) + +-- | Variant of 'dejafu' which takes a collection of predicates to +-- test, returning 'True' if all pass. +-- +-- > > dejafus [("A", alwaysSame), ("B", deadlocksNever)] example +-- > [fail] A +-- > "hello" S0----S1--S0-- +-- > +-- > "world" S0----S2--S0-- +-- > [pass] B +-- +-- @since 1.0.0.0 +dejafus :: (MonadConc n, MonadIO n, MonadRef r n, Show b) + => [(String, ProPredicate a b)] + -- ^ The list of predicates (with names) to check. + -> ConcT r n a + -- ^ The computation to test. + -> n Bool +dejafus = dejafusWay defaultWay defaultMemType + +-- | Variant of 'dejafus' which takes a way to run the program and a +-- memory model. +-- +-- > > dejafusWay defaultWay SequentialConsistency [("A", alwaysSame), ("B", exceptionsNever)] relaxed +-- > [fail] A +-- > (False,True) S0---------S1----S0--S2----S0-- +-- > +-- > (True,True) S0---------S1-P2----S1---S0--- +-- > +-- > (True,False) S0---------S2----S1----S0--- +-- > [pass] B +-- +-- @since 1.0.0.0 +dejafusWay :: (MonadConc n, MonadIO n, MonadRef r n, Show b) + => Way + -- ^ How to run the concurrent program. + -> MemType + -- ^ The memory model to use for non-synchronised @CRef@ operations. + -> [(String, ProPredicate a b)] + -- ^ The list of predicates (with names) to check. + -> ConcT r n a + -- ^ The computation to test. + -> n Bool +dejafusWay way memtype tests conc = do + traces <- runSCTDiscard discarder way memtype conc + results <- mapM (\(name, test) -> liftIO . doTest name $ chk test traces) tests + pure (and results) + where + discarder = foldr + (weakenDiscard . pdiscard . snd) + (const (Just DiscardResultAndTrace)) + tests + + -- for evaluating each individual predicate, we only want the + -- results/traces it would not discard, but the traces set may + -- include more than this if the different predicates have + -- different discard functions, so we do another pass of + -- discarding. + chk p = peval p . mapMaybe go where + go r@(efa, _) = case pdiscard p efa of + Just DiscardResultAndTrace -> Nothing + Just DiscardTrace -> Just (efa, []) + Nothing -> Just r + +------------------------------------------------------------------------------- +-- Test cases + +-- | The results of a test, including the number of cases checked to +-- determine the final boolean outcome. +-- +-- @since 1.0.0.0 +data Result a = Result + { _pass :: Bool + -- ^ Whether the test passed or not. + , _failures :: [(Either Failure a, Trace)] + -- ^ The failing cases, if any. + , _failureMsg :: String + -- ^ A message to display on failure, if nonempty + } deriving (Eq, Show) + +instance NFData a => NFData (Result a) where + rnf r = rnf ( _pass r + , _failures r + , _failureMsg r + ) + +-- | A failed result, taking the given list of failures. +defaultFail :: [(Either Failure a, Trace)] -> Result a +defaultFail failures = Result False failures "" + +-- | A passed result. +defaultPass :: Result a +defaultPass = Result True [] "" + +instance Functor Result where + fmap f r = r { _failures = map (first $ fmap f) $ _failures r } + +instance Foldable Result where + foldMap f r = foldMap f [a | (Right a, _) <- _failures r] + +-- | Run a predicate over all executions within the default schedule +-- bounds. +-- +-- The exact executions tried, and the order in which results are +-- found, is unspecified and may change between releases. This may +-- affect which failing traces are reported, when there is a failure. +-- +-- @since 1.0.0.0 +runTest :: (MonadConc n, MonadRef r n) + => ProPredicate a b + -- ^ The predicate to check + -> ConcT r n a + -- ^ The computation to test + -> n (Result b) +runTest = runTestWay defaultWay defaultMemType + +-- | Variant of 'runTest' which takes a way to run the program and a +-- memory model. +-- +-- The exact executions tried, and the order in which results are +-- found, is unspecified and may change between releases. This may +-- affect which failing traces are reported, when there is a failure. +-- +-- @since 1.0.0.0 +runTestWay :: (MonadConc n, MonadRef r n) + => Way + -- ^ How to run the concurrent program. + -> MemType + -- ^ The memory model to use for non-synchronised @CRef@ operations. + -> ProPredicate a b + -- ^ The predicate to check + -> ConcT r n a + -- ^ The computation to test + -> n (Result b) +runTestWay way memtype p conc = + peval p <$> runSCTDiscard (pdiscard p) way memtype conc + + +------------------------------------------------------------------------------- +-- Predicates + +-- | A @Predicate@ is a function which collapses a list of results +-- into a 'Result', possibly discarding some on the way. +-- +-- @Predicate@ cannot be a functor as the type parameter is used both +-- co- and contravariantly. +-- +-- @since 1.0.0.0 +type Predicate a = ProPredicate a a + +-- | A @ProPredicate@ is a function which collapses a list of results +-- into a 'Result', possibly discarding some on the way. +-- +-- @since 1.0.0.0 +data ProPredicate a b = ProPredicate + { pdiscard :: Either Failure a -> Maybe Discard + -- ^ Selectively discard results before computing the result. + , peval :: [(Either Failure a, Trace)] -> Result b + -- ^ Compute the result with the un-discarded results. + } + +instance Profunctor ProPredicate where + dimap f g p = ProPredicate + { pdiscard = pdiscard p . fmap f + , peval = fmap g . peval p . map (first (fmap f)) + } + +instance Functor (ProPredicate x) where + fmap = dimap id + +-- | Reduce the list of failures in a @ProPredicate@ to one +-- representative trace for each unique result. +-- +-- 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 1.0.0.0 +representative :: Eq b => ProPredicate a b -> ProPredicate a b +representative p = p + { peval = \xs -> + let result = peval p xs + in result { _failures = simplestsBy (==) (_failures result) } + } + +-- | Check that a computation never aborts. +-- +-- @since 1.0.0.0 +abortsNever :: Predicate a +abortsNever = alwaysTrue (not . either (==Abort) (const False)) + +-- | Check that a computation always aborts. +-- +-- @since 1.0.0.0 +abortsAlways :: Predicate a +abortsAlways = alwaysTrue $ either (==Abort) (const False) + +-- | Check that a computation aborts at least once. +-- +-- @since 1.0.0.0 +abortsSometimes :: Predicate a +abortsSometimes = somewhereTrue $ either (==Abort) (const False) + +-- | Check that a computation never deadlocks. +-- +-- @since 1.0.0.0 +deadlocksNever :: Predicate a +deadlocksNever = alwaysTrue (not . either isDeadlock (const False)) + +-- | Check that a computation always deadlocks. +-- +-- @since 1.0.0.0 +deadlocksAlways :: Predicate a +deadlocksAlways = alwaysTrue $ either isDeadlock (const False) + +-- | Check that a computation deadlocks at least once. +-- +-- @since 1.0.0.0 +deadlocksSometimes :: Predicate a +deadlocksSometimes = somewhereTrue $ either isDeadlock (const False) + +-- | Check that a computation never fails with an uncaught exception. +-- +-- @since 1.0.0.0 +exceptionsNever :: Predicate a +exceptionsNever = alwaysTrue (not . either isUncaughtException (const False)) + +-- | Check that a computation always fails with an uncaught exception. +-- +-- @since 1.0.0.0 +exceptionsAlways :: Predicate a +exceptionsAlways = alwaysTrue $ either isUncaughtException (const False) + +-- | Check that a computation fails with an uncaught exception at least once. +-- +-- @since 1.0.0.0 +exceptionsSometimes :: Predicate a +exceptionsSometimes = somewhereTrue $ either isUncaughtException (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. +-- +-- > alwaysSame = alwaysSameBy (==) +-- +-- @since 1.0.0.0 +alwaysSame :: Eq a => Predicate a +alwaysSame = alwaysSameBy (==) + +-- | Check that the result of a computation is always the same by +-- comparing the result of a function on every result. +-- +-- > alwaysSameOn = alwaysSameBy ((==) `on` f) +-- +-- @since 1.0.0.0 +alwaysSameOn :: Eq b => (Either Failure a -> b) -> Predicate a +alwaysSameOn f = alwaysSameBy ((==) `on` f) + +-- | Check that the result of a computation is always the same, using +-- some transformation on results. +-- +-- @since 1.0.0.0 +alwaysSameBy :: (Either Failure a -> Either Failure a -> Bool) -> Predicate a +alwaysSameBy f = ProPredicate + { pdiscard = const Nothing + , peval = \xs -> case simplestsBy f xs of + [] -> defaultPass + [_] -> defaultPass + xs' -> defaultFail xs' + } + +-- | Check that the result of a computation is not always the same. +-- +-- @since 1.0.0.0 +notAlwaysSame :: Eq a => Predicate a +notAlwaysSame = ProPredicate + { pdiscard = const Nothing + , peval = \case + [x] -> defaultFail [x] + xs -> go xs (defaultFail []) + } + where + go [y1,y2] res + | fst y1 /= fst y2 = res { _pass = True } + | otherwise = res { _failures = y1 : y2 : _failures res } + go (y1:y2:ys) res + | fst y1 /= fst y2 = go (y2:ys) res { _pass = True } + | otherwise = go (y2:ys) res { _failures = y1 : y2 : _failures res } + go _ res = res + +-- | Check that a @Maybe@-producing function always returns 'Nothing'. +-- +-- @since 1.0.0.0 +alwaysNothing :: (Either Failure a -> Maybe (Either Failure b)) -> ProPredicate a b +alwaysNothing f = ProPredicate + { pdiscard = maybe (Just DiscardResultAndTrace) (const Nothing) . f + , peval = \xs -> + let failures = mapMaybe (\(efa,trc) -> (,trc) <$> f efa) xs + in Result (null failures) failures "" + } + +-- | Check that the result of a unary boolean predicate is always +-- true. +-- +-- @since 1.0.0.0 +alwaysTrue :: (Either Failure a -> Bool) -> Predicate a +alwaysTrue p = alwaysNothing (\efa -> if p efa then Nothing else Just efa) + +-- | Check that a @Maybe@-producing function returns 'Nothing' at +-- least once. +-- +-- @since 1.0.0.0 +somewhereNothing :: (Either Failure a -> Maybe (Either Failure b)) -> ProPredicate a b +somewhereNothing f = ProPredicate + { pdiscard = maybe (Just DiscardTrace) (const Nothing) . f + , peval = \xs -> + let failures = map (\(efa,trc) -> (,trc) <$> f efa) xs + in Result (any isNothing failures) (catMaybes failures) "" + } + +-- | Check that the result of a unary boolean predicate is true at +-- least once. +-- +-- @since 1.0.0.0 +somewhereTrue :: (Either Failure a -> Bool) -> Predicate a +somewhereTrue p = somewhereNothing (\efa -> if p efa then Nothing else Just efa) + +-- | Predicate for when there is a known set of results where every +-- result must be exhibited at least once. +-- +-- @since 1.0.0.0 +gives :: (Eq a, Show a) => [Either Failure a] -> Predicate a +gives expected = ProPredicate + { pdiscard = \efa -> if efa `elem` expected then Just DiscardTrace else Nothing + , peval = \xs -> go expected [] xs $ defaultFail (failures xs) + } + where + go waitingFor alreadySeen ((x, _):xs) res + -- If it's a result we're waiting for, move it to the + -- @alreadySeen@ list and continue. + | x `elem` waitingFor = go (filter (/=x) waitingFor) (x:alreadySeen) xs res + -- If it's a result we've already seen, continue. + | x `elem` alreadySeen = go waitingFor alreadySeen xs res + -- If it's not a result we expected, fail. + | otherwise = res + + go [] _ [] res = res { _pass = True } + go es _ [] res = res { _failureMsg = unlines $ map (\e -> "Expected: " ++ show e) es } + + failures = filter (\(r, _) -> r `notElem` expected) + +-- | Variant of 'gives' that doesn't allow for expected failures. +-- +-- @since 1.0.0.0 +gives' :: (Eq a, Show a) => [a] -> Predicate a +gives' = gives . map Right + + +------------------------------------------------------------------------------- +-- Utils + +-- | Run a test and print to stdout +doTest :: Show a => String -> Result a -> IO Bool +doTest name result = do + if _pass result + then + -- Display a pass message. + putStrLn ("\27[32m[pass]\27[0m " ++ name) + else do + -- Display a failure message, and the first 5 (simplified) failed traces + putStrLn ("\27[31m[fail]\27[0m " ++ name) + + unless (null $ _failureMsg result) $ + putStrLn $ _failureMsg result + + let failures = _failures result + let output = map (\(r, t) -> putStrLn . indent $ either showFail show r ++ " " ++ showTrace t) $ take 5 failures + sequence_ $ intersperse (putStrLn "") output + when (moreThan 5 failures) $ + putStrLn (indent "...") + + pure (_pass result) + +-- | Check if a list is longer than some value, without needing to +-- compute the entire length. +moreThan :: Int -> [a] -> Bool +moreThan n [] = n < 0 +moreThan 0 _ = True +moreThan n (_:rest) = moreThan (n-1) rest -- | Indent every line of a string. indent :: String -> String diff --git a/Test/DejaFu/Common.hs b/Test/DejaFu/Common.hs deleted file mode 100644 --- a/Test/DejaFu/Common.hs +++ /dev/null @@ -1,1070 +0,0 @@ --- | --- Module : Test.DejaFu.Common --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- Stability : experimental --- Portability : portable --- --- Common types and functions used throughout DejaFu. -module Test.DejaFu.Common - ( -- * Identifiers - ThreadId(..) - , CRefId(..) - , MVarId(..) - , TVarId(..) - , initialThread - -- ** Identifier source - , IdSource(..) - , nextCRId - , nextMVId - , nextTVId - , nextTId - , initialIdSource - - -- * Actions - -- ** Thread actions - , ThreadAction(..) - , isBlock - , tvarsOf - , tvarsWritten - , tvarsRead - -- ** Lookahead - , Lookahead(..) - , rewind - , willRelease - -- ** Simplified actions - , ActionType(..) - , isBarrier - , isCommit - , synchronises - , crefOf - , mvarOf - , simplifyAction - , simplifyLookahead - -- ** STM actions - , TTrace - , TAction(..) - - -- * Traces - , Trace - , Decision(..) - , showTrace - , threadNames - , preEmpCount - - -- * Failures - , Failure(..) - , isInternalError - , isAbort - , isDeadlock - , isUncaughtException - , isIllegalSubconcurrency - , showFail - - -- * Memory models - , MemType(..) - - -- * Miscellaneous - , MonadFailException(..) - , runRefCont - , ehead - , etail - , eidx - , efromJust - , efromList - , fatal - ) where - -import Control.DeepSeq (NFData(..)) -import Control.Exception (Exception(..), MaskingState(..), - SomeException, displayException) -import Control.Monad.Ref (MonadRef(..)) -import Data.Function (on) -import Data.List (intercalate) -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. --- --- The @Eq@ and @Ord@ instances only consider the int, not the name. --- --- @since 0.4.0.0 -data ThreadId = ThreadId (Maybe String) {-# UNPACK #-} !Int - --- | Previously this was a derived instance. --- --- @since 0.7.2.0 -instance Eq ThreadId where - (ThreadId _ i) == (ThreadId _ j) = i == j - -instance Ord ThreadId where - compare (ThreadId _ i) (ThreadId _ j) = compare i j - -instance Show ThreadId where - 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. --- --- The @Eq@ and @Ord@ instances only consider the int, not the name. --- --- @since 0.4.0.0 -data CRefId = CRefId (Maybe String) {-# UNPACK #-} !Int - --- | Previously this was a derived instance. --- --- @since 0.7.2.0 -instance Eq CRefId where - (CRefId _ i) == (CRefId _ j) = i == j - -instance Ord CRefId where - compare (CRefId _ i) (CRefId _ j) = compare i j - -instance Show CRefId where - 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. --- --- The @Eq@ and @Ord@ instances only consider the int, not the name. --- --- @since 0.4.0.0 -data MVarId = MVarId (Maybe String) {-# UNPACK #-} !Int - --- | Previously this was a derived instance. --- --- @since 0.7.2.0 -instance Eq MVarId where - (MVarId _ i) == (MVarId _ j) = i == j - -instance Ord MVarId where - compare (MVarId _ i) (MVarId _ j) = compare i j - -instance Show MVarId where - 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. --- --- The @Eq@ and @Ord@ instances only consider the int, not the name. --- --- @since 0.4.0.0 -data TVarId = TVarId (Maybe String) {-# UNPACK #-} !Int - --- | Previously this was a derived instance. --- --- @since 0.7.2.0 -instance Eq TVarId where - (TVarId _ i) == (TVarId _ j) = i == j - -instance Ord TVarId where - compare (TVarId _ i) (TVarId _ j) = compare i j - -instance Show TVarId where - 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 - ---------------------------------------- --- Identifier source - --- | 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 - , _nextTVId :: Int - , _nextTId :: Int - , _usedCRNames :: [String] - , _usedMVNames :: [String] - , _usedTVNames :: [String] - , _usedTNames :: [String] - } deriving (Eq, Ord, Show) - --- | @since 0.5.1.0 -instance NFData IdSource where - rnf idsource = rnf ( _nextCRId idsource - , _nextMVId idsource - , _nextTVId idsource - , _nextTId idsource - , _usedCRNames idsource - , _usedMVNames idsource - , _usedTVNames idsource - , _usedTNames idsource - ) - --- | 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 } - newCRId = CRefId newName newId - newId = _nextCRId idsource + 1 - (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 } - newMVId = MVarId newName newId - newId = _nextMVId idsource + 1 - (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 } - newTVId = TVarId newName newId - newId = _nextTVId idsource + 1 - (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 } - newTId = ThreadId newName newId - newId = _nextTId idsource + 1 - (newName, newUsed) = nextId name (_usedTNames idsource) - --- | The initial ID source. --- --- @since 0.4.0.0 -initialIdSource :: IdSource -initialIdSource = Id 0 0 0 0 [] [] [] [] - -------------------------------------------------------------------------------- --- Actions - ---------------------------------------- --- Thread actions - --- | All the actions that a thread can perform. --- --- @since 0.9.0.0 -data ThreadAction = - Fork ThreadId - -- ^ Start a new thread. - | MyThreadId - -- ^ Get the 'ThreadId' of the current thread. - | GetNumCapabilities Int - -- ^ Get the number of Haskell threads that can run simultaneously. - | SetNumCapabilities Int - -- ^ Set the number of Haskell threads that can run simultaneously. - | Yield - -- ^ Yield the current thread. - | ThreadDelay Int - -- ^ Yield/delay the current thread. - | NewMVar MVarId - -- ^ Create a new 'MVar'. - | PutMVar MVarId [ThreadId] - -- ^ Put into a 'MVar', possibly waking up some threads. - | BlockedPutMVar MVarId - -- ^ Get blocked on a put. - | TryPutMVar MVarId Bool [ThreadId] - -- ^ Try to put into a 'MVar', possibly waking up some threads. - | ReadMVar MVarId - -- ^ Read from a 'MVar'. - | TryReadMVar MVarId Bool - -- ^ Try to read from a 'MVar'. - | BlockedReadMVar MVarId - -- ^ Get blocked on a read. - | TakeMVar MVarId [ThreadId] - -- ^ Take from a 'MVar', possibly waking up some threads. - | BlockedTakeMVar MVarId - -- ^ Get blocked on a take. - | TryTakeMVar MVarId Bool [ThreadId] - -- ^ Try to take from a 'MVar', possibly waking up some threads. - | NewCRef CRefId - -- ^ Create a new 'CRef'. - | ReadCRef CRefId - -- ^ Read from a 'CRef'. - | ReadCRefCas CRefId - -- ^ Read from a 'CRef' for a future compare-and-swap. - | ModCRef CRefId - -- ^ Modify a 'CRef'. - | ModCRefCas CRefId - -- ^ Modify a 'CRef' using a compare-and-swap. - | WriteCRef CRefId - -- ^ Write to a 'CRef' without synchronising. - | CasCRef CRefId Bool - -- ^ Attempt to to a 'CRef' using a compare-and-swap, synchronising - -- it. - | CommitCRef ThreadId CRefId - -- ^ Commit the last write to the given 'CRef' by the given thread, - -- so that all threads can see the updated value. - | STM TTrace [ThreadId] - -- ^ An STM transaction was executed, possibly waking up some - -- threads. - | BlockedSTM TTrace - -- ^ Got blocked in an STM transaction. - | Catching - -- ^ Register a new exception handler - | PopCatching - -- ^ Pop the innermost exception handler from the stack. - | Throw - -- ^ Throw an exception. - | ThrowTo ThreadId - -- ^ Throw an exception to a thread. - | BlockedThrowTo ThreadId - -- ^ Get blocked on a 'throwTo'. - | Killed - -- ^ Killed by an uncaught exception. - | SetMasking Bool MaskingState - -- ^ Set the masking state. If 'True', this is being used to set the - -- masking state to the original state in the argument passed to a - -- 'mask'ed function. - | ResetMasking Bool MaskingState - -- ^ Return to an earlier masking state. If 'True', this is being - -- used to return to the state of the masked block in the argument - -- passed to a 'mask'ed function. - | LiftIO - -- ^ Lift an IO action. Note that this can only happen with - -- 'ConcIO'. - | Return - -- ^ A 'return' or 'pure' action was executed. - | Stop - -- ^ Cease execution and terminate. - | Subconcurrency - -- ^ Start executing an action with @subconcurrency@. - | StopSubconcurrency - -- ^ Stop executing an action with @subconcurrency@. - deriving (Eq, Show) - -instance NFData ThreadAction where - rnf (Fork t) = rnf t - rnf (ThreadDelay n) = rnf n - rnf (GetNumCapabilities c) = rnf c - rnf (SetNumCapabilities c) = rnf c - rnf (NewMVar m) = rnf m - rnf (PutMVar m ts) = rnf (m, ts) - rnf (BlockedPutMVar m) = rnf m - rnf (TryPutMVar m b ts) = rnf (m, b, ts) - rnf (ReadMVar m) = rnf m - rnf (TryReadMVar m b) = rnf (m, b) - rnf (BlockedReadMVar m) = rnf m - rnf (TakeMVar m ts) = rnf (m, ts) - rnf (BlockedTakeMVar m) = rnf m - rnf (TryTakeMVar m b ts) = rnf (m, b, ts) - rnf (NewCRef c) = rnf c - rnf (ReadCRef c) = rnf c - rnf (ReadCRefCas c) = rnf c - rnf (ModCRef c) = rnf c - rnf (ModCRefCas c) = rnf c - rnf (WriteCRef c) = rnf c - rnf (CasCRef c b) = rnf (c, b) - rnf (CommitCRef t c) = rnf (t, c) - rnf (STM tr ts) = rnf (tr, ts) - rnf (BlockedSTM tr) = rnf tr - rnf (ThrowTo t) = rnf t - rnf (BlockedThrowTo t) = rnf t - rnf (SetMasking b m) = b `seq` m `seq` () - rnf (ResetMasking b m) = b `seq` m `seq` () - rnf a = a `seq` () - --- | Check if a @ThreadAction@ immediately blocks. --- --- @since 0.4.0.0 -isBlock :: ThreadAction -> Bool -isBlock (BlockedThrowTo _) = True -isBlock (BlockedTakeMVar _) = True -isBlock (BlockedReadMVar _) = True -isBlock (BlockedPutMVar _) = True -isBlock (BlockedSTM _) = True -isBlock _ = False - --- | Get the @TVar@s affected by a @ThreadAction@. --- --- @since 0.4.0.0 -tvarsOf :: ThreadAction -> Set TVarId -tvarsOf act = tvarsRead act `S.union` tvarsWritten act - --- | Get the @TVar@s a transaction wrote to (or would have, if it --- didn't @retry@). --- --- @since 0.9.0.2 -tvarsWritten :: ThreadAction -> Set TVarId -tvarsWritten act = S.fromList $ case act of - STM trc _ -> concatMap tvarsOf' trc - BlockedSTM trc -> concatMap tvarsOf' trc - _ -> [] - - where - tvarsOf' (TWrite tv) = [tv] - tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) - tvarsOf' (TCatch ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) - tvarsOf' _ = [] - --- | Get the @TVar@s a transaction read from. --- --- @since 0.9.0.2 -tvarsRead :: ThreadAction -> Set TVarId -tvarsRead act = S.fromList $ case act of - STM trc _ -> concatMap tvarsOf' trc - BlockedSTM trc -> concatMap tvarsOf' trc - _ -> [] - - where - tvarsOf' (TRead tv) = [tv] - tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) - tvarsOf' (TCatch ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) - tvarsOf' _ = [] - ---------------------------------------- --- Lookahead - --- | A one-step look-ahead at what a thread will do next. --- --- @since 0.9.0.0 -data Lookahead = - WillFork - -- ^ Will start a new thread. - | WillMyThreadId - -- ^ Will get the 'ThreadId'. - | WillGetNumCapabilities - -- ^ Will get the number of Haskell threads that can run - -- simultaneously. - | WillSetNumCapabilities Int - -- ^ Will set the number of Haskell threads that can run - -- simultaneously. - | WillYield - -- ^ Will yield the current thread. - | WillThreadDelay Int - -- ^ Will yield/delay the current thread. - | WillNewMVar - -- ^ Will create a new 'MVar'. - | WillPutMVar MVarId - -- ^ Will put into a 'MVar', possibly waking up some threads. - | WillTryPutMVar MVarId - -- ^ Will try to put into a 'MVar', possibly waking up some threads. - | WillReadMVar MVarId - -- ^ Will read from a 'MVar'. - | WillTryReadMVar MVarId - -- ^ Will try to read from a 'MVar'. - | WillTakeMVar MVarId - -- ^ Will take from a 'MVar', possibly waking up some threads. - | WillTryTakeMVar MVarId - -- ^ Will try to take from a 'MVar', possibly waking up some threads. - | WillNewCRef - -- ^ Will create a new 'CRef'. - | WillReadCRef CRefId - -- ^ Will read from a 'CRef'. - | WillReadCRefCas CRefId - -- ^ Will read from a 'CRef' for a future compare-and-swap. - | WillModCRef CRefId - -- ^ Will modify a 'CRef'. - | WillModCRefCas CRefId - -- ^ Will modify a 'CRef' using a compare-and-swap. - | WillWriteCRef CRefId - -- ^ Will write to a 'CRef' without synchronising. - | WillCasCRef CRefId - -- ^ Will attempt to to a 'CRef' using a compare-and-swap, - -- synchronising it. - | WillCommitCRef ThreadId CRefId - -- ^ Will commit the last write by the given thread to the 'CRef'. - | WillSTM - -- ^ Will execute an STM transaction, possibly waking up some - -- threads. - | WillCatching - -- ^ Will register a new exception handler - | WillPopCatching - -- ^ Will pop the innermost exception handler from the stack. - | WillThrow - -- ^ Will throw an exception. - | WillThrowTo ThreadId - -- ^ Will throw an exception to a thread. - | WillSetMasking Bool MaskingState - -- ^ Will set the masking state. If 'True', this is being used to - -- set the masking state to the original state in the argument - -- passed to a 'mask'ed function. - | WillResetMasking Bool MaskingState - -- ^ Will return to an earlier masking state. If 'True', this is - -- being used to return to the state of the masked block in the - -- argument passed to a 'mask'ed function. - | WillLiftIO - -- ^ Will lift an IO action. Note that this can only happen with - -- 'ConcIO'. - | WillReturn - -- ^ Will execute a 'return' or 'pure' action. - | WillStop - -- ^ Will cease execution and terminate. - | WillSubconcurrency - -- ^ Will execute an action with @subconcurrency@. - | WillStopSubconcurrency - -- ^ Will stop executing an extion with @subconcurrency@. - deriving (Eq, Show) - -instance NFData Lookahead where - rnf (WillThreadDelay n) = rnf n - rnf (WillSetNumCapabilities c) = rnf c - rnf (WillPutMVar m) = rnf m - rnf (WillTryPutMVar m) = rnf m - rnf (WillReadMVar m) = rnf m - rnf (WillTryReadMVar m) = rnf m - rnf (WillTakeMVar m) = rnf m - rnf (WillTryTakeMVar m) = rnf m - rnf (WillReadCRef c) = rnf c - rnf (WillReadCRefCas c) = rnf c - rnf (WillModCRef c) = rnf c - rnf (WillModCRefCas c) = rnf c - rnf (WillWriteCRef c) = rnf c - rnf (WillCasCRef c) = rnf c - rnf (WillCommitCRef t c) = rnf (t, c) - rnf (WillThrowTo t) = rnf t - rnf (WillSetMasking b m) = b `seq` m `seq` () - rnf (WillResetMasking b m) = b `seq` m `seq` () - rnf l = l `seq` () - --- | 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 -rewind (GetNumCapabilities _) = Just WillGetNumCapabilities -rewind (SetNumCapabilities i) = Just (WillSetNumCapabilities i) -rewind Yield = Just WillYield -rewind (ThreadDelay n) = Just (WillThreadDelay n) -rewind (NewMVar _) = Just WillNewMVar -rewind (PutMVar c _) = Just (WillPutMVar c) -rewind (BlockedPutMVar c) = Just (WillPutMVar c) -rewind (TryPutMVar c _ _) = Just (WillTryPutMVar c) -rewind (ReadMVar c) = Just (WillReadMVar c) -rewind (BlockedReadMVar c) = Just (WillReadMVar c) -rewind (TryReadMVar c _) = Just (WillTryReadMVar c) -rewind (TakeMVar c _) = Just (WillTakeMVar c) -rewind (BlockedTakeMVar c) = Just (WillTakeMVar c) -rewind (TryTakeMVar c _ _) = Just (WillTryTakeMVar c) -rewind (NewCRef _) = Just WillNewCRef -rewind (ReadCRef c) = Just (WillReadCRef c) -rewind (ReadCRefCas c) = Just (WillReadCRefCas c) -rewind (ModCRef c) = Just (WillModCRef c) -rewind (ModCRefCas c) = Just (WillModCRefCas c) -rewind (WriteCRef c) = Just (WillWriteCRef c) -rewind (CasCRef c _) = Just (WillCasCRef c) -rewind (CommitCRef t c) = Just (WillCommitCRef t c) -rewind (STM _ _) = Just WillSTM -rewind (BlockedSTM _) = Just WillSTM -rewind Catching = Just WillCatching -rewind PopCatching = Just WillPopCatching -rewind Throw = Just WillThrow -rewind (ThrowTo t) = Just (WillThrowTo t) -rewind (BlockedThrowTo t) = Just (WillThrowTo t) -rewind Killed = Nothing -rewind (SetMasking b m) = Just (WillSetMasking b m) -rewind (ResetMasking b m) = Just (WillResetMasking b m) -rewind LiftIO = Just WillLiftIO -rewind Return = Just WillReturn -rewind Stop = Just WillStop -rewind Subconcurrency = Just WillSubconcurrency -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 -willRelease (WillThreadDelay _) = True -willRelease (WillPutMVar _) = True -willRelease (WillTryPutMVar _) = True -willRelease (WillReadMVar _) = True -willRelease (WillTakeMVar _) = True -willRelease (WillTryTakeMVar _) = True -willRelease WillSTM = True -willRelease WillThrow = True -willRelease (WillSetMasking _ _) = True -willRelease (WillResetMasking _ _) = True -willRelease WillStop = True -willRelease _ = False - ---------------------------------------- --- 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'. - | UnsynchronisedWrite CRefId - -- ^ A 'writeCRef'. - | UnsynchronisedOther - -- ^ Some other action which doesn't require cross-thread - -- communication. - | PartiallySynchronisedCommit CRefId - -- ^ A commit. - | PartiallySynchronisedWrite CRefId - -- ^ A 'casCRef' - | PartiallySynchronisedModify CRefId - -- ^ A 'modifyCRefCAS' - | SynchronisedModify CRefId - -- ^ An 'atomicModifyCRef'. - | SynchronisedRead MVarId - -- ^ A 'readMVar' or 'takeMVar' (or @try@/@blocked@ variants). - | SynchronisedWrite MVarId - -- ^ A 'putMVar' (or @try@/@blocked@ variant). - | SynchronisedOther - -- ^ Some other action which does require cross-thread - -- communication. - deriving (Eq, Show) - --- | @since 0.5.1.0 -instance NFData ActionType where - rnf (UnsynchronisedRead c) = rnf c - rnf (UnsynchronisedWrite c) = rnf c - rnf (PartiallySynchronisedCommit c) = rnf c - rnf (PartiallySynchronisedWrite c) = rnf c - rnf (PartiallySynchronisedModify c) = rnf c - rnf (SynchronisedModify c) = rnf c - rnf (SynchronisedRead m) = rnf m - rnf (SynchronisedWrite m) = rnf m - 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 -isBarrier (SynchronisedWrite _) = True -isBarrier SynchronisedOther = True -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 -isCommit (PartiallySynchronisedModify c) r = c == r -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 -crefOf (SynchronisedModify r) = Just r -crefOf (PartiallySynchronisedCommit r) = Just r -crefOf (PartiallySynchronisedWrite r) = Just r -crefOf (PartiallySynchronisedModify r) = Just r -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 -mvarOf _ = Nothing - --- | Throw away information from a 'ThreadAction' and give a --- simplified view of what is happening. --- --- 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 -simplifyLookahead (WillReadMVar c) = SynchronisedRead c -simplifyLookahead (WillTryReadMVar c) = SynchronisedRead c -simplifyLookahead (WillTakeMVar c) = SynchronisedRead c -simplifyLookahead (WillTryTakeMVar c) = SynchronisedRead c -simplifyLookahead (WillReadCRef r) = UnsynchronisedRead r -simplifyLookahead (WillReadCRefCas r) = UnsynchronisedRead r -simplifyLookahead (WillModCRef r) = SynchronisedModify r -simplifyLookahead (WillModCRefCas r) = PartiallySynchronisedModify r -simplifyLookahead (WillWriteCRef r) = UnsynchronisedWrite r -simplifyLookahead (WillCasCRef r) = PartiallySynchronisedWrite r -simplifyLookahead (WillCommitCRef _ r) = PartiallySynchronisedCommit r -simplifyLookahead WillSTM = SynchronisedOther -simplifyLookahead (WillThrowTo _) = SynchronisedOther -simplifyLookahead _ = UnsynchronisedOther - ---------------------------------------- --- STM actions - --- | 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.8.0.0 -data TAction = - TNew TVarId - -- ^ Create a new @TVar@ - | TRead TVarId - -- ^ Read from a @TVar@. - | TWrite TVarId - -- ^ Write to a @TVar@. - | TRetry - -- ^ Abort and discard effects. - | TOrElse TTrace (Maybe TTrace) - -- ^ Execute a transaction until it succeeds (@STMStop@) or aborts - -- (@STMRetry@) and, if it aborts, execute the other transaction. - | TThrow - -- ^ Throw an exception, abort, and discard effects. - | TCatch TTrace (Maybe TTrace) - -- ^ Execute a transaction until it succeeds (@STMStop@) or aborts - -- (@STMThrow@). If the exception is of the appropriate type, it is - -- handled and execution continues; otherwise aborts, propagating - -- the exception upwards. - | TStop - -- ^ 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 - rnf (TOrElse tr mtr) = rnf (tr, mtr) - rnf (TCatch tr mtr) = rnf (tr, mtr) - rnf ta = ta `seq` () - -------------------------------------------------------------------------------- --- Traces - --- | 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.8.0.0 -type Trace - = [(Decision, [(ThreadId, 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 - -- start of computation). - | Continue - -- ^ Continue running the last thread for another step. - | SwitchTo ThreadId - -- ^ 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 - rnf d = d `seq` () - --- | 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 [] = "" -showTrace trc = intercalate "\n" $ go False trc : strkey where - go _ ((_,_,CommitCRef _ _):rest) = "C-" ++ go False rest - go _ ((Start (ThreadId _ i),_,a):rest) = "S" ++ show i ++ "-" ++ go (didYield a) rest - go y ((SwitchTo (ThreadId _ i),_,a):rest) = (if y then "p" else "P") ++ show i ++ "-" ++ go (didYield a) rest - go _ ((Continue,_,a):rest) = '-' : go (didYield a) rest - go _ _ = "" - - strkey = - [" " ++ show i ++ ": " ++ name | (i, name) <- threadNames trc] - - didYield Yield = True - didYield (ThreadDelay _) = True - didYield _ = False - --- | Get all named threads in the trace. --- --- @since 0.7.3.0 -threadNames :: Trace -> [(Int, String)] -threadNames = mapMaybe go where - go (_, _, Fork (ThreadId (Just name) i)) = Just (i, name) - go _ = Nothing - --- | Count the number of pre-emptions in a schedule prefix. --- --- Commit threads complicate this a bit. Conceptually, commits are --- happening truly in parallel, nondeterministically. The commit --- thread implementation is just there to unify the two sources of --- nondeterminism: commit timing and thread scheduling. --- --- 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 -preEmpCount (x:xs) (d, _) = go initialThread x xs where - go _ (_, Yield) (r@(SwitchTo t, _):rest) = go t r rest - go _ (_, ThreadDelay _) (r@(SwitchTo t, _):rest) = go t r rest - go tid prior (r@(SwitchTo t, _):rest) - | isCommitThread t = go tid prior (skip rest) - | otherwise = 1 + go t r rest - go _ _ (r@(Start t, _):rest) = go t r rest - go tid _ (r@(Continue, _):rest) = go tid r rest - go _ prior [] = case (prior, d) of - ((_, Yield), SwitchTo _) -> 0 - ((_, ThreadDelay _), SwitchTo _) -> 0 - (_, SwitchTo _) -> 1 - _ -> 0 - - -- Commit threads have negative thread IDs for easy identification. - isCommitThread = (< initialThread) - - -- Skip until the next context switch. - skip = dropWhile (not . isContextSwitch . fst) - isContextSwitch Continue = False - isContextSwitch _ = True -preEmpCount [] _ = 0 - -------------------------------------------------------------------------------- --- Failures - - --- | An indication of how a concurrent computation failed. --- --- The @Eq@, @Ord@, and @NFData@ instances compare/evaluate the --- exception with @show@ in the @UncaughtException@ case. --- --- @since 0.9.0.0 -data Failure - = InternalError - -- ^ Will be raised if the scheduler does something bad. This should - -- never arise unless you write your own, faulty, scheduler! If it - -- does, please file a bug report. - | Abort - -- ^ The scheduler chose to abort execution. This will be produced - -- if, for example, all possible decisions exceed the specified - -- bounds (there have been too many pre-emptions, the computation - -- has executed for too long, or there have been too many yields). - | Deadlock - -- ^ The computation became blocked indefinitely on @MVar@s. - | STMDeadlock - -- ^ The computation became blocked indefinitely on @TVar@s. - | UncaughtException SomeException - -- ^ An uncaught exception bubbled to the top of the computation. - | IllegalSubconcurrency - -- ^ Calls to @subconcurrency@ were nested, or attempted when - -- multiple threads existed. - deriving Show - -instance Eq Failure where - (==) = (==) `on` _other - -instance Ord Failure where - compare = compare `on` _other - -instance NFData Failure where - rnf = rnf . _other - --- | Convert failures into a different representation we can Eq / Ord --- / NFData. -_other :: Failure -> (Int, Maybe String) -_other InternalError = (0, Nothing) -_other Abort = (1, Nothing) -_other Deadlock = (2, Nothing) -_other STMDeadlock = (3, Nothing) -_other (UncaughtException e) = (4, Just (show e)) -_other IllegalSubconcurrency = (5, Nothing) - --- | Pretty-print a failure --- --- @since 0.4.0.0 -showFail :: Failure -> String -showFail Abort = "[abort]" -showFail Deadlock = "[deadlock]" -showFail STMDeadlock = "[stm-deadlock]" -showFail InternalError = "[internal-error]" -showFail (UncaughtException exc) = "[" ++ displayException exc ++ "]" -showFail IllegalSubconcurrency = "[illegal-subconcurrency]" - --- | Check if a failure is an @InternalError@. --- --- @since 0.9.0.0 -isInternalError :: Failure -> Bool -isInternalError InternalError = True -isInternalError _ = False - --- | Check if a failure is an @Abort@. --- --- @since 0.9.0.0 -isAbort :: Failure -> Bool -isAbort Abort = True -isAbort _ = False - --- | Check if a failure is a @Deadlock@ or an @STMDeadlock@. --- --- @since 0.9.0.0 -isDeadlock :: Failure -> Bool -isDeadlock Deadlock = True -isDeadlock STMDeadlock = True -isDeadlock _ = False - --- | Check if a failure is an @UncaughtException@ --- --- @since 0.9.0.0 -isUncaughtException :: Failure -> Bool -isUncaughtException (UncaughtException _) = True -isUncaughtException _ = False - --- | Check if a failure is an @IllegalSubconcurrency@ --- --- @since 0.9.0.0 -isIllegalSubconcurrency :: Failure -> Bool -isIllegalSubconcurrency IllegalSubconcurrency = True -isIllegalSubconcurrency _ = False - -------------------------------------------------------------------------------- --- 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 - -- interleaving of the actions in different threads. When a 'CRef' - -- is written to, that write is immediately visible to all threads. - | TotalStoreOrder - -- ^ 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. - | PartialStoreOrder - -- ^ 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 'CRef's - -- are not necessarily committed in the same order that they are - -- created. - deriving (Eq, Show, Read, Ord, Enum, Bounded) - --- | @since 0.5.1.0 -instance NFData MemType where - rnf m = m `seq` () - -------------------------------------------------------------------------------- --- Miscellaneous - --- | An exception for errors in testing caused by use of 'fail'. -newtype MonadFailException = MonadFailException String - deriving Show - -instance Exception MonadFailException - --- | Run with a continuation that writes its value into a reference, --- returning the computation and the reference. Using the reference --- is non-blocking, it is up to you to ensure you wait sufficiently. -runRefCont :: MonadRef r n => (n () -> x) -> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, r (Maybe b)) -runRefCont act f k = do - ref <- newRef Nothing - let c = k (act . writeRef ref . f) - pure (c, ref) - --- | 'head' but with a better error message if it fails. Use this --- only where it shouldn't fail! -ehead :: String -> [a] -> a -ehead _ (x:_) = x -ehead src _ = fatal src "head: empty list" - --- | 'tail' but with a better error message if it fails. Use this --- only where it shouldn't fail! -etail :: String -> [a] -> [a] -etail _ (_:xs) = xs -etail src _ = fatal src "tail: empty list" - --- | '(!!)' but with a better error message if it fails. Use this --- only where it shouldn't fail! -eidx :: String -> [a] -> Int -> a -eidx src xs i - | i < length xs = xs !! i - | otherwise = fatal src "(!!): index too large" - --- | 'fromJust' but with a better error message if it fails. Use this --- only where it shouldn't fail! -efromJust :: String -> Maybe a -> a -efromJust _ (Just x) = x -efromJust src _ = fatal src "fromJust: Nothing" - --- | 'fromList' but with a better error message if it fails. Use this --- only where it shouldn't fail! -efromList :: String -> [a] -> NonEmpty a -efromList _ (x:xs) = x:|xs -efromList src _ = fatal src "fromList: empty list" - --- | 'error' but saying where it came from -fatal :: String -> String -> a -fatal src msg = error ("(dejafu: " ++ src ++ ") " ++ msg) - - -------------------------------------------------------------------------------- --- Utilities - --- | Helper for @next*@ -nextId :: String -> [String] -> (Maybe String, [String]) -nextId name used = (newName, newUsed) where - newName - | null name = Nothing - | occurrences > 0 = Just (name ++ "-" ++ show occurrences) - | otherwise = Just name - newUsed - | null name = used - | otherwise = name : used - occurrences = length (filter (==name) used) diff --git a/Test/DejaFu/Conc.hs b/Test/DejaFu/Conc.hs --- a/Test/DejaFu/Conc.hs +++ b/Test/DejaFu/Conc.hs @@ -4,15 +4,14 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeSynonymInstances #-} -- | -- Module : Test.DejaFu.Conc --- Copyright : (c) 2016 Michael Walker +-- Copyright : (c) 2016--2017 Michael Walker -- License : MIT -- Maintainer : Michael Walker -- Stability : experimental --- Portability : CPP, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, RankNTypes, TypeFamilies, TypeSynonymInstances +-- Portability : CPP, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, TypeFamilies -- -- Deterministic traced execution of concurrent computations. -- @@ -22,7 +21,6 @@ module Test.DejaFu.Conc ( -- * The @ConcT@ monad transformer ConcT - , ConcST , ConcIO -- * Executing computations @@ -48,23 +46,22 @@ ) 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 Control.Monad.Trans.Class (MonadTrans(..)) 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 Test.DejaFu.Conc.Internal.STM +import Test.DejaFu.Internal +import Test.DejaFu.Types +import Test.DejaFu.Utils #if MIN_VERSION_base(4,9,0) import qualified Control.Monad.Fail as Fail @@ -79,12 +76,6 @@ fail = C . fail #endif --- | A 'MonadConc' implementation using @ST@, this should be preferred --- if you do not need 'liftIO'. --- --- @since 0.4.0.0 -type ConcST t = ConcT (STRef t) (ST t) - -- | A 'MonadConc' implementation using @IO@. -- -- @since 0.4.0.0 @@ -96,11 +87,9 @@ 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 - liftIO ma = toConc (\c -> ALift (fmap c ma)) - -instance Ba.MonadBase IO ConcIO where - liftBase = IO.liftIO +-- | @since 1.0.0.0 +instance IO.MonadIO n => IO.MonadIO (ConcT r n) where + liftIO ma = toConc (\c -> ALift (fmap c (IO.liftIO ma))) instance Re.MonadRef (CRef r) (ConcT r n) where newRef a = toConc (ANewCRef "" a) @@ -131,14 +120,17 @@ 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 STM (ConcT r n) = S n r type ThreadId (ConcT r n) = ThreadId -- ---------- - forkWithUnmaskN n ma = toConc (AFork n (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop (pure ())))) + forkWithUnmaskN n ma = toConc (AFork n (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop (pure ())))) forkOnWithUnmaskN n _ = C.forkWithUnmaskN n + forkOSN n ma = forkOSWithUnmaskN n (const ma) + isCurrentThreadBound = toConc AIsBound + -- This implementation lies and returns 2 until a value is set. This -- will potentially avoid special-case behaviour for 1 capability, -- so it seems a sane choice. @@ -185,10 +177,22 @@ atomically = toConc . AAtom +-- move this into the instance defn when forkOSWithUnmaskN is added to MonadConc in 2018 +forkOSWithUnmaskN :: Applicative n => String -> ((forall a. ConcT r n a -> ConcT r n a) -> ConcT r n ()) -> ConcT r n ThreadId +forkOSWithUnmaskN n ma + | C.rtsSupportsBoundThreads = toConc (AForkOS n (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop (pure ())))) + | otherwise = fail "RTS doesn't support multiple OS threads (use ghc -threaded when linking)" + -- | Run a concurrent computation with a given 'Scheduler' and initial -- state, returning a failure reason on error. Also returned is the -- final state of the scheduler, and an execution trace. -- +-- If the RTS supports bound threads (ghc -threaded when linking) then +-- the main thread of the concurrent computation will be bound, and +-- @forkOS@ / @forkOSN@ will work during execution. If not, then the +-- main thread will not be found, and attempting to fork a bound +-- thread will raise an error. +-- -- __Warning:__ Blocking on the action of another thread in 'liftIO' -- cannot be detected! So if you perform some potentially blocking -- action in a 'liftIO' the entire collection of threads may deadlock! @@ -202,8 +206,8 @@ -- nonexistent thread. In either of those cases, the computation will -- be halted. -- --- @since 0.8.0.0 -runConcurrent :: MonadRef r n +-- @since 1.0.0.0 +runConcurrent :: (C.MonadConc n, MonadRef r n) => Scheduler s -> MemType -> s 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 @@ -4,7 +4,7 @@ -- | -- Module : Test.DejaFu.Conc.Internal --- Copyright : (c) 2016 Michael Walker +-- Copyright : (c) 2016--2017 Michael Walker -- License : MIT -- Maintainer : Michael Walker -- Stability : experimental @@ -17,6 +17,8 @@ import Control.Exception (MaskingState(..), toException) +import Control.Monad.Conc.Class (MonadConc, + rtsSupportsBoundThreads) import Control.Monad.Ref (MonadRef, newRef, readRef, writeRef) import Data.Functor (void) @@ -27,13 +29,13 @@ 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.STM import Test.DejaFu.Conc.Internal.Threading +import Test.DejaFu.Internal import Test.DejaFu.Schedule -import Test.DejaFu.STM (Result(..), - runTransaction) +import Test.DejaFu.Types -------------------------------------------------------------------------------- -- * Execution @@ -45,23 +47,27 @@ -- | Run a concurrent computation with a given 'Scheduler' and initial -- state, returning a failure reason on error. Also returned is the -- final state of the scheduler, and an execution trace. -runConcurrency :: MonadRef r n - => Scheduler g - -> MemType - -> g - -> IdSource - -> Int - -> M n r a - -> n (Either Failure a, Context n r g, SeqTrace, Maybe (ThreadId, ThreadAction)) +runConcurrency :: (MonadConc n, MonadRef r n) + => Scheduler g + -> MemType + -> g + -> IdSource + -> Int + -> M n r a + -> n (Either Failure a, Context n r g, SeqTrace, Maybe (ThreadId, ThreadAction)) runConcurrency sched memtype g idsrc caps ma = do (c, ref) <- runRefCont AStop (Just . Right) (runM ma) + let threads0 = launch' Unmasked initialThread (const c) M.empty + threads <- (if rtsSupportsBoundThreads then makeBound initialThread else pure) threads0 let ctx = Context { cSchedState = g , cIdSource = idsrc - , cThreads = launch' Unmasked initialThread (const c) M.empty + , cThreads = threads , cWriteBuf = emptyBuffer , cCaps = caps } (finalCtx, trace, finalAction) <- runThreads sched memtype ref ctx + let finalThreads = cThreads finalCtx + mapM_ (`kill` finalThreads) (M.keys finalThreads) out <- readRef ref pure (efromJust "runConcurrency" out, finalCtx, trace, finalAction) @@ -75,7 +81,7 @@ } -- | Run a collection of threads, until there are no threads left. -runThreads :: MonadRef r n +runThreads :: (MonadConc n, MonadRef r n) => Scheduler g -> MemType -> r (Maybe (Either Failure a)) @@ -140,9 +146,11 @@ | (fst <$> prior) `notElem` map (Just . fst) runnable' = Start chosen | otherwise = SwitchTo chosen - getTrc (Single a) = Seq.singleton (decision, runnable', a) - getTrc (SubC as _) = (decision, runnable', Subconcurrency) <| as + getTrc (Single a) = Seq.singleton (decision, alternatives, a) + getTrc (SubC as _) = (decision, alternatives, Subconcurrency) <| as + alternatives = filter (\(t, _) -> t /= chosen) runnable' + getPrior (Single a) = Just (chosen, a) getPrior (SubC _ finalD) = finalD @@ -159,7 +167,7 @@ -- | Run a single thread one step, by dispatching on the type of -- 'Action'. -stepThread :: forall n r g. MonadRef r n +stepThread :: forall n r g. (MonadConc n, MonadRef r n) => Scheduler g -- ^ The scheduler. -> MemType @@ -174,10 +182,22 @@ stepThread sched memtype tid action ctx = case action of -- start a new thread, assigning it the next 'ThreadId' AFork n a b -> pure $ - let threads' = launch tid newtid a (cThreads ctx) - (idSource', newtid) = nextTId n (cIdSource ctx) - in (Right ctx { cThreads = goto (b newtid) tid threads', cIdSource = idSource' }, Single (Fork newtid)) + let threads' = launch tid newtid a (cThreads ctx) + (idSource', newtid) = nextTId n (cIdSource ctx) + in (Right ctx { cThreads = goto (b newtid) tid threads', cIdSource = idSource' }, Single (Fork newtid)) + -- start a new bound thread, assigning it the next 'ThreadId' + AForkOS n a b -> do + let (idSource', newtid) = nextTId n (cIdSource ctx) + let threads' = launch tid newtid a (cThreads ctx) + threads'' <- makeBound newtid threads' + pure (Right ctx { cThreads = goto (b newtid) tid threads'', cIdSource = idSource' }, Single (Fork newtid)) + + -- check if the current thread is bound + AIsBound c -> + let isBound = isJust (_bound =<< M.lookup tid (cThreads ctx)) + in simple (goto (c isBound) tid (cThreads ctx)) (IsCurrentThreadBound isBound) + -- get the 'ThreadId' of the current thread AMyTId c -> simple (goto (c tid) tid (cThreads ctx)) MyThreadId @@ -316,7 +336,7 @@ -- lift an action from the underlying monad into the @Conc@ -- computation. ALift na -> do - a <- na + a <- runLiftedAct tid (cThreads ctx) na simple (goto a tid (cThreads ctx)) LiftIO -- throw an exception, and propagate it to the appropriate @@ -367,7 +387,10 @@ AReturn c -> simple (goto c tid (cThreads ctx)) Return -- kill the current thread. - AStop na -> na >> simple (kill tid (cThreads ctx)) Stop + AStop na -> do + na + threads' <- kill tid (cThreads ctx) + simple threads' Stop -- run a subconcurrent computation. ASub ma c @@ -394,7 +417,9 @@ Just ts' -> simple ts' act Nothing | t == initialThread -> pure (Left (UncaughtException some), Single act) - | otherwise -> simple (kill t ts) act + | otherwise -> do + ts' <- kill t ts + simple ts' act -- helper for actions which only change the threads. simple threads' act = pure (Right ctx { cThreads = threads' }, Single act) 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 @@ -4,7 +4,7 @@ -- | -- Module : Test.DejaFu.Conc.Internal.Common --- Copyright : (c) 2016 Michael Walker +-- Copyright : (c) 2016--2017 Michael Walker -- License : MIT -- Maintainer : Michael Walker -- Stability : experimental @@ -12,15 +12,16 @@ -- -- Common types and utility functions for deterministic execution of -- 'MonadConc' implementations. This module is NOT considered to form +-- part of the public interface of this library. module Test.DejaFu.Conc.Internal.Common where -import Control.Exception (Exception, MaskingState(..)) -import Data.Map.Strict (Map) -import Test.DejaFu.Common -import Test.DejaFu.STM (STMLike) +import Control.Exception (Exception, MaskingState(..)) +import Data.Map.Strict (Map) +import Test.DejaFu.Conc.Internal.STM (S) +import Test.DejaFu.Types #if MIN_VERSION_base(4,9,0) -import qualified Control.Monad.Fail as Fail +import qualified Control.Monad.Fail as Fail #endif -------------------------------------------------------------------------------- @@ -109,7 +110,9 @@ -- primitives of the concurrency. 'spawn' is absent as it is -- implemented in terms of 'newEmptyMVar', 'fork', and 'putMVar'. data Action n r = - AFork String ((forall b. M n r b -> M n r b) -> Action n r) (ThreadId -> Action n r) + AFork String ((forall b. M n r b -> M n r b) -> Action n r) (ThreadId -> Action n r) + | AForkOS String ((forall b. M n r b -> M n r b) -> Action n r) (ThreadId -> Action n r) + | AIsBound (Bool -> Action n r) | AMyTId (ThreadId -> Action n r) | AGetNumCapabilities (Int -> Action n r) @@ -138,7 +141,7 @@ | forall a. AMasking MaskingState ((forall b. M n r b -> M n r b) -> M n r a) (a -> Action n r) | AResetMask Bool Bool MaskingState (Action n r) - | forall a. AAtom (STMLike n r a) (a -> Action n r) + | forall a. AAtom (S n r a) (a -> Action n r) | ALift (n (Action n r)) | AYield (Action n r) | ADelay Int (Action n r) @@ -155,6 +158,8 @@ -- | Look as far ahead in the given continuation as possible. lookahead :: Action n r -> Lookahead lookahead (AFork _ _ _) = WillFork +lookahead (AForkOS _ _ _) = WillForkOS +lookahead (AIsBound _) = WillIsCurrentThreadBound lookahead (AMyTId _) = WillMyThreadId lookahead (AGetNumCapabilities _) = WillGetNumCapabilities lookahead (ASetNumCapabilities i _) = WillSetNumCapabilities i 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 @@ -4,7 +4,7 @@ -- | -- Module : Test.DejaFu.Conc.Internal.Memory --- Copyright : (c) 2016 Michael Walker +-- Copyright : (c) 2016--2017 Michael Walker -- License : MIT -- Maintainer : Michael Walker -- Stability : experimental @@ -26,16 +26,16 @@ import Control.Monad.Ref (MonadRef, readRef, writeRef) import Data.Map.Strict (Map) +import qualified Data.Map.Strict as M import Data.Maybe (maybeToList) 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 qualified Data.Map.Strict as M +import Test.DejaFu.Internal +import Test.DejaFu.Types -------------------------------------------------------------------------------- -- * Manipulating @CRef@s @@ -129,7 +129,7 @@ -- | Add phantom threads to the thread list to commit pending writes. addCommitThreads :: WriteBuffer r -> Threads n r -> Threads n r addCommitThreads (WriteBuffer wb) ts = ts <> M.fromList phantoms where - phantoms = [ (ThreadId Nothing $ negate tid, mkthread c) + phantoms = [ (ThreadId (Id Nothing $ negate tid), mkthread c) | ((_, b), tid) <- zip (M.toList wb) [1..] , c <- maybeToList (go $ viewl b) ] diff --git a/Test/DejaFu/Conc/Internal/STM.hs b/Test/DejaFu/Conc/Internal/STM.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Conc/Internal/STM.hs @@ -0,0 +1,239 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeFamilies #-} + +-- Must come after TypeFamilies +{-# LANGUAGE NoMonoLocalBinds #-} + +-- | +-- Module : Test.DejaFu.Conc.Internal.STM +-- Copyright : (c) 2017 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : CPP, ExistentialQuantification, MultiParamTypeClasses, NoMonoLocalBinds, TypeFamilies +-- +-- 'MonadSTM' testing implementation, internal types and definitions. +-- This module is NOT considered to form part of the public interface +-- of this library. +module Test.DejaFu.Conc.Internal.STM where + +import Control.Applicative (Alternative(..)) +import Control.Exception (Exception, SomeException, + fromException, toException) +import Control.Monad (MonadPlus(..)) +import Control.Monad.Catch (MonadCatch(..), MonadThrow(..)) +import Control.Monad.Ref (MonadRef, newRef, readRef, writeRef) +import Data.List (nub) + +import qualified Control.Monad.STM.Class as C +import Test.DejaFu.Internal +import Test.DejaFu.Types + +#if MIN_VERSION_base(4,9,0) +import qualified Control.Monad.Fail as Fail +#endif + +-------------------------------------------------------------------------------- +-- * The @S@ monad + +-- | The underlying monad is based on continuations over primitive +-- actions. +-- +-- This is not @Cont@ because we want to give it a custom @MonadFail@ +-- instance. +newtype S n r a = S { runSTM :: (a -> STMAction n r) -> STMAction n r } + +instance Functor (S n r) where + fmap f m = S $ \c -> runSTM m (c . f) + +instance Applicative (S n r) where + pure x = S $ \c -> c x + f <*> v = S $ \c -> runSTM f (\g -> runSTM v (c . g)) + +instance Monad (S n r) where + return = pure + m >>= k = S $ \c -> runSTM m (\x -> runSTM (k x) c) + +#if MIN_VERSION_base(4,9,0) + fail = Fail.fail + +instance Fail.MonadFail (S n r) where +#endif + fail e = S $ \_ -> SThrow (MonadFailException e) + +instance MonadThrow (S n r) where + throwM e = S $ \_ -> SThrow e + +instance MonadCatch (S n r) where + catch stm handler = S $ SCatch handler stm + +instance Alternative (S n r) where + a <|> b = S $ SOrElse a b + empty = S $ const SRetry + +instance MonadPlus (S n r) + +instance C.MonadSTM (S n r) where + type TVar (S n r) = TVar r + + newTVarN n = S . SNew n + + readTVar = S . SRead + + writeTVar tvar a = S $ \c -> SWrite tvar a (c ()) + +-------------------------------------------------------------------------------- +-- * Primitive actions + +-- | STM transactions are represented as a sequence of primitive +-- actions. +data STMAction n r + = forall a e. Exception e => SCatch (e -> S n r a) (S n r a) (a -> STMAction n r) + | forall a. SRead (TVar r a) (a -> STMAction n r) + | forall a. SWrite (TVar r a) a (STMAction n r) + | forall a. SOrElse (S n r a) (S n r a) (a -> STMAction n r) + | forall a. SNew String a (TVar r a -> STMAction n r) + | forall e. Exception e => SThrow e + | SRetry + | SStop (n ()) + +-------------------------------------------------------------------------------- +-- * @TVar@s + +-- | A 'TVar' is a tuple of a unique ID and the value contained. The +-- ID is so that blocked transactions can be re-run when a 'TVar' they +-- depend on has changed. +newtype TVar r a = TVar (TVarId, r a) + +-------------------------------------------------------------------------------- +-- * Output + +-- | The result of an STM transaction, along with which 'TVar's it +-- touched whilst executing. +data Result a = + Success [TVarId] [TVarId] a + -- ^ The transaction completed successfully, reading the first list + -- 'TVar's and writing to the second. + | Retry [TVarId] + -- ^ The transaction aborted by calling 'retry', and read the + -- returned 'TVar's. It should be retried when at least one of the + -- 'TVar's has been mutated. + | Exception SomeException + -- ^ The transaction aborted by throwing an exception. + deriving Show + + +-------------------------------------------------------------------------------- +-- * Execution + +-- | Run a transaction, returning the result and new initial 'TVarId'. +-- If the transaction failed, any effects are undone. +runTransaction :: MonadRef r n + => S n r a + -> IdSource + -> n (Result a, IdSource, [TAction]) +runTransaction ma tvid = do + (res, _, tvid', trace) <- doTransaction ma tvid + pure (res, tvid', trace) + +-- | Run a STM transaction, returning an action to undo its effects. +-- +-- If the transaction fails, its effects will automatically be undone, +-- so the undo action returned will be @pure ()@. +doTransaction :: MonadRef r n + => S n r a + -> IdSource + -> n (Result a, n (), IdSource, [TAction]) +doTransaction ma idsource = do + (c, ref) <- runRefCont SStop (Just . Right) (runSTM ma) + (idsource', undo, readen, written, trace) <- go ref c (pure ()) idsource [] [] [] + res <- readRef ref + + case res of + Just (Right val) -> pure (Success (nub readen) (nub written) val, undo, 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 + (act', undo', nidsrc', readen', written', tact) <- stepTrans act nidsrc + + let newIDSource = nidsrc' + newAct = act' + newUndo = undo' >> undo + newReaden = readen' ++ readen + newWritten = written' ++ written + newSofar = tact : sofar + + case tact of + 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. +stepTrans :: MonadRef r n + => STMAction n r + -> IdSource + -> n (STMAction n r, n (), IdSource, [TVarId], [TVarId], TAction) +stepTrans act idsource = case act of + SCatch h stm c -> stepCatch h stm c + SRead ref c -> stepRead ref c + SWrite ref a c -> stepWrite ref a c + SNew n a c -> stepNew n a c + SOrElse a b c -> stepOrElse a b c + SStop na -> stepStop na + + SThrow e -> pure (SThrow e, nothing, idsource, [], [], TThrow) + SRetry -> pure (SRetry, nothing, idsource, [], [], TRetry) + + where + nothing = pure () + + stepCatch h stm c = cases TCatch stm c + (\trace -> pure (SRetry, nothing, idsource, [], [], TCatch trace Nothing)) + (\trace exc -> case fromException exc of + Just exc' -> transaction (TCatch trace . Just) (h exc') c + Nothing -> pure (SThrow exc, nothing, idsource, [], [], TCatch trace Nothing)) + + stepRead (TVar (tvid, ref)) c = do + val <- readRef ref + pure (c val, nothing, idsource, [tvid], [], TRead tvid) + + stepWrite (TVar (tvid, ref)) a c = do + old <- readRef ref + writeRef ref a + 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) + pure (c tvar, nothing, idsource', [], [tvid], TNew tvid) + + stepOrElse a b c = cases TOrElse a c + (\trace -> transaction (TOrElse trace . Just) b c) + (\trace exc -> pure (SThrow exc, nothing, idsource, [], [], TOrElse trace Nothing)) + + stepStop na = do + na + 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 -> 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 -> pure (SRetry, nothing, idsource, [], [], tact trace)) + (\trace exc -> pure (SThrow exc, nothing, idsource, [], [], tact trace)) 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 @@ -3,7 +3,7 @@ -- | -- Module : Test.DejaFu.Conc.Internal.Threading --- Copyright : (c) 2016 Michael Walker +-- Copyright : (c) 2016--2017 Michael Walker -- License : MIT -- Maintainer : Michael Walker -- Stability : experimental @@ -13,14 +13,16 @@ -- form part of the public interface of this library. module Test.DejaFu.Conc.Internal.Threading where +import qualified Control.Concurrent.Classy as C import Control.Exception (Exception, MaskingState(..), SomeException, fromException) import Data.List (intersect) import Data.Map.Strict (Map) import Data.Maybe (isJust) -import Test.DejaFu.Common import Test.DejaFu.Conc.Internal.Common +import Test.DejaFu.Internal +import Test.DejaFu.Types import qualified Data.Map.Strict as M @@ -40,11 +42,23 @@ -- ^ Stack of exception handlers , _masking :: MaskingState -- ^ The exception masking state. + , _bound :: Maybe (BoundThread n r) + -- ^ State for the associated bound thread, if it exists. } +-- | The state of a bound thread. +data BoundThread n r = BoundThread + { _runboundIO :: C.MVar n (n (Action n r)) + -- ^ Run an @IO@ action in the bound thread by writing to this. + , _getboundIO :: C.MVar n (Action n r) + -- ^ Get the result of the above by reading from this. + , _boundTId :: C.ThreadId n + -- ^ Thread ID + } + -- | Construct a thread with just one action mkthread :: Action n r -> Thread n r -mkthread c = Thread c Nothing [] Unmasked +mkthread c = Thread c Nothing [] Unmasked Nothing -------------------------------------------------------------------------------- -- * Blocking @@ -122,15 +136,11 @@ -- | Start a thread with the given ID and masking state. This must not already be in use! launch' :: MaskingState -> ThreadId -> ((forall b. M n r b -> M n r b) -> Action n r) -> Threads n r -> Threads n r launch' ms tid a = M.insert tid thread where - thread = Thread { _continuation = a umask, _blocking = Nothing, _handlers = [], _masking = ms } + thread = Thread (a umask) Nothing [] ms Nothing 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. -kill :: ThreadId -> Threads n r -> Threads n r -kill = M.delete - -- | Block a thread. block :: BlockedOn -> ThreadId -> Threads n r -> Threads n r block blockedOn = M.adjust $ \thread -> thread { _blocking = Just blockedOn } @@ -147,3 +157,44 @@ isBlocked thread = case (_blocking thread, blockedOn) of (Just (OnTVar tvids), OnTVar blockedOn') -> tvids `intersect` blockedOn' /= [] (theblock, _) -> theblock == Just blockedOn + +------------------------------------------------------------------------------- +-- ** Bound threads + +-- | Turn a thread into a bound thread. +makeBound :: C.MonadConc n => ThreadId -> Threads n r -> n (Threads n r) +makeBound tid threads = do + runboundIO <- C.newEmptyMVar + getboundIO <- C.newEmptyMVar + btid <- C.forkOSN ("bound worker for '" ++ show tid ++ "'") (go runboundIO getboundIO) + let bt = BoundThread runboundIO getboundIO btid + pure (M.adjust (\t -> t { _bound = Just bt }) tid threads) + where + go runboundIO getboundIO = + let loop = do + na <- C.takeMVar runboundIO + C.putMVar getboundIO =<< na + loop + in loop + +-- | Kill a thread and remove it from the thread map. +-- +-- If the thread is bound, the worker thread is cleaned up. +kill :: C.MonadConc n => ThreadId -> Threads n r -> n (Threads n r) +kill tid threads = case M.lookup tid threads of + Just thread -> case _bound thread of + Just bt -> do + C.killThread (_boundTId bt) + pure (M.delete tid threads) + Nothing -> pure (M.delete tid threads) + Nothing -> pure threads + +-- | Run an action. +-- +-- If the thread is bound, the action is run in the worker thread. +runLiftedAct :: C.MonadConc n => ThreadId -> Threads n r -> n (Action n r) -> n (Action n r) +runLiftedAct tid threads ma = case _bound =<< M.lookup tid threads of + Just bt -> do + C.putMVar (_runboundIO bt) ma + C.takeMVar (_getboundIO bt) + Nothing -> ma diff --git a/Test/DejaFu/Defaults.hs b/Test/DejaFu/Defaults.hs --- a/Test/DejaFu/Defaults.hs +++ b/Test/DejaFu/Defaults.hs @@ -9,8 +9,8 @@ -- Default parameters for test execution. module Test.DejaFu.Defaults where -import Test.DejaFu.Common import Test.DejaFu.SCT +import Test.DejaFu.Types -- | A default way to execute concurrent programs: systematically -- using 'defaultBounds'. diff --git a/Test/DejaFu/Internal.hs b/Test/DejaFu/Internal.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Internal.hs @@ -0,0 +1,338 @@ +-- | +-- Module : Test.DejaFu.Internal +-- Copyright : (c) 2017 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : portable +-- +-- Internal types and functions used throughout DejaFu. This module +-- is NOT considered to form part of the public interface of this +-- library. +module Test.DejaFu.Internal where + +import Control.DeepSeq (NFData(..)) +import Control.Monad.Ref (MonadRef(..)) +import Data.List.NonEmpty (NonEmpty(..)) +import Data.Maybe (fromMaybe) +import Data.Set (Set) +import qualified Data.Set as S + +import Test.DejaFu.Types + +------------------------------------------------------------------------------- +-- * Identifiers + +-- | The number of ID parameters was getting a bit unwieldy, so this +-- hides them all away. +data IdSource = IdSource + { _crids :: (Int, [String]) + , _mvids :: (Int, [String]) + , _tvids :: (Int, [String]) + , _tids :: (Int, [String]) + } deriving (Eq, Ord, Show) + +instance NFData IdSource where + rnf idsource = rnf ( _crids idsource + , _mvids idsource + , _tvids idsource + , _tids idsource + ) + +-- | Get the next free 'CRefId'. +nextCRId :: String -> IdSource -> (IdSource, CRefId) +nextCRId name idsource = + let (crid, crids') = nextId name (_crids idsource) + in (idsource { _crids = crids' }, CRefId crid) + +-- | Get the next free 'MVarId'. +nextMVId :: String -> IdSource -> (IdSource, MVarId) +nextMVId name idsource = + let (mvid, mvids') = nextId name (_mvids idsource) + in (idsource { _mvids = mvids' }, MVarId mvid) + +-- | Get the next free 'TVarId'. +nextTVId :: String -> IdSource -> (IdSource, TVarId) +nextTVId name idsource = + let (tvid, tvids') = nextId name (_tvids idsource) + in (idsource { _tvids = tvids' }, TVarId tvid) + +-- | Get the next free 'ThreadId'. +nextTId :: String -> IdSource -> (IdSource, ThreadId) +nextTId name idsource = + let (tid, tids') = nextId name (_tids idsource) + in (idsource { _tids = tids' }, ThreadId tid) + +-- | Helper for @next*@ +nextId :: String -> (Int, [String]) -> (Id, (Int, [String])) +nextId name (num, used) = (Id newName (num+1), (num+1, newUsed)) where + newName + | null name = Nothing + | occurrences > 0 = Just (name ++ "-" ++ show occurrences) + | otherwise = Just name + newUsed + | null name = used + | otherwise = name : used + occurrences = length (filter (==name) used) + +-- | The initial ID source. +initialIdSource :: IdSource +initialIdSource = IdSource (0, []) (0, []) (0, []) (0, []) + +------------------------------------------------------------------------------- +-- * Actions + +-- | Check if a @ThreadAction@ immediately blocks. +isBlock :: ThreadAction -> Bool +isBlock (BlockedThrowTo _) = True +isBlock (BlockedTakeMVar _) = True +isBlock (BlockedReadMVar _) = True +isBlock (BlockedPutMVar _) = True +isBlock (BlockedSTM _) = True +isBlock _ = False + +-- | Get the @TVar@s affected by a @ThreadAction@. +tvarsOf :: ThreadAction -> Set TVarId +tvarsOf act = tvarsRead act `S.union` tvarsWritten act + +-- | Get the @TVar@s a transaction wrote to (or would have, if it +-- didn't @retry@). +tvarsWritten :: ThreadAction -> Set TVarId +tvarsWritten act = S.fromList $ case act of + STM trc _ -> concatMap tvarsOf' trc + BlockedSTM trc -> concatMap tvarsOf' trc + _ -> [] + + where + tvarsOf' (TWrite tv) = [tv] + tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) + tvarsOf' (TCatch ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) + tvarsOf' _ = [] + +-- | Get the @TVar@s a transaction read from. +tvarsRead :: ThreadAction -> Set TVarId +tvarsRead act = S.fromList $ case act of + STM trc _ -> concatMap tvarsOf' trc + BlockedSTM trc -> concatMap tvarsOf' trc + _ -> [] + + where + tvarsOf' (TRead tv) = [tv] + tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) + tvarsOf' (TCatch ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) + tvarsOf' _ = [] + +-- | Convert a 'ThreadAction' into a 'Lookahead': \"rewind\" what has +-- happened. 'Killed' has no 'Lookahead' counterpart. +rewind :: ThreadAction -> Maybe Lookahead +rewind (Fork _) = Just WillFork +rewind (ForkOS _) = Just WillForkOS +rewind (IsCurrentThreadBound _) = Just WillIsCurrentThreadBound +rewind MyThreadId = Just WillMyThreadId +rewind (GetNumCapabilities _) = Just WillGetNumCapabilities +rewind (SetNumCapabilities i) = Just (WillSetNumCapabilities i) +rewind Yield = Just WillYield +rewind (ThreadDelay n) = Just (WillThreadDelay n) +rewind (NewMVar _) = Just WillNewMVar +rewind (PutMVar c _) = Just (WillPutMVar c) +rewind (BlockedPutMVar c) = Just (WillPutMVar c) +rewind (TryPutMVar c _ _) = Just (WillTryPutMVar c) +rewind (ReadMVar c) = Just (WillReadMVar c) +rewind (BlockedReadMVar c) = Just (WillReadMVar c) +rewind (TryReadMVar c _) = Just (WillTryReadMVar c) +rewind (TakeMVar c _) = Just (WillTakeMVar c) +rewind (BlockedTakeMVar c) = Just (WillTakeMVar c) +rewind (TryTakeMVar c _ _) = Just (WillTryTakeMVar c) +rewind (NewCRef _) = Just WillNewCRef +rewind (ReadCRef c) = Just (WillReadCRef c) +rewind (ReadCRefCas c) = Just (WillReadCRefCas c) +rewind (ModCRef c) = Just (WillModCRef c) +rewind (ModCRefCas c) = Just (WillModCRefCas c) +rewind (WriteCRef c) = Just (WillWriteCRef c) +rewind (CasCRef c _) = Just (WillCasCRef c) +rewind (CommitCRef t c) = Just (WillCommitCRef t c) +rewind (STM _ _) = Just WillSTM +rewind (BlockedSTM _) = Just WillSTM +rewind Catching = Just WillCatching +rewind PopCatching = Just WillPopCatching +rewind Throw = Just WillThrow +rewind (ThrowTo t) = Just (WillThrowTo t) +rewind (BlockedThrowTo t) = Just (WillThrowTo t) +rewind Killed = Nothing +rewind (SetMasking b m) = Just (WillSetMasking b m) +rewind (ResetMasking b m) = Just (WillResetMasking b m) +rewind LiftIO = Just WillLiftIO +rewind Return = Just WillReturn +rewind Stop = Just WillStop +rewind Subconcurrency = Just WillSubconcurrency +rewind StopSubconcurrency = Just WillStopSubconcurrency + +-- | Check if an operation could enable another thread. +willRelease :: Lookahead -> Bool +willRelease WillFork = True +willRelease WillForkOS = True +willRelease WillYield = True +willRelease (WillThreadDelay _) = True +willRelease (WillPutMVar _) = True +willRelease (WillTryPutMVar _) = True +willRelease (WillReadMVar _) = True +willRelease (WillTakeMVar _) = True +willRelease (WillTryTakeMVar _) = True +willRelease WillSTM = True +willRelease WillThrow = True +willRelease (WillSetMasking _ _) = True +willRelease (WillResetMasking _ _) = True +willRelease WillStop = True +willRelease _ = False + +------------------------------------------------------------------------------- +-- * Simplified actions + +-- | A simplified view of the possible actions a thread can perform. +data ActionType = + UnsynchronisedRead CRefId + -- ^ A 'readCRef' or a 'readForCAS'. + | UnsynchronisedWrite CRefId + -- ^ A 'writeCRef'. + | UnsynchronisedOther + -- ^ Some other action which doesn't require cross-thread + -- communication. + | PartiallySynchronisedCommit CRefId + -- ^ A commit. + | PartiallySynchronisedWrite CRefId + -- ^ A 'casCRef' + | PartiallySynchronisedModify CRefId + -- ^ A 'modifyCRefCAS' + | SynchronisedModify CRefId + -- ^ An 'atomicModifyCRef'. + | SynchronisedRead MVarId + -- ^ A 'readMVar' or 'takeMVar' (or @try@/@blocked@ variants). + | SynchronisedWrite MVarId + -- ^ A 'putMVar' (or @try@/@blocked@ variant). + | SynchronisedOther + -- ^ Some other action which does require cross-thread + -- communication. + deriving (Eq, Show) + +instance NFData ActionType where + rnf (UnsynchronisedRead c) = rnf c + rnf (UnsynchronisedWrite c) = rnf c + rnf (PartiallySynchronisedCommit c) = rnf c + rnf (PartiallySynchronisedWrite c) = rnf c + rnf (PartiallySynchronisedModify c) = rnf c + rnf (SynchronisedModify c) = rnf c + rnf (SynchronisedRead m) = rnf m + rnf (SynchronisedWrite m) = rnf m + rnf a = a `seq` () + +-- | Check if an action imposes a write barrier. +isBarrier :: ActionType -> Bool +isBarrier (SynchronisedModify _) = True +isBarrier (SynchronisedRead _) = True +isBarrier (SynchronisedWrite _) = True +isBarrier SynchronisedOther = True +isBarrier _ = False + +-- | Check if an action commits a given 'CRef'. +isCommit :: ActionType -> CRefId -> Bool +isCommit (PartiallySynchronisedCommit c) r = c == r +isCommit (PartiallySynchronisedWrite c) r = c == r +isCommit (PartiallySynchronisedModify c) r = c == r +isCommit _ _ = False + +-- | Check if an action synchronises a given 'CRef'. +synchronises :: ActionType -> CRefId -> Bool +synchronises a r = isCommit a r || isBarrier a + +-- | Get the 'CRef' affected. +crefOf :: ActionType -> Maybe CRefId +crefOf (UnsynchronisedRead r) = Just r +crefOf (UnsynchronisedWrite r) = Just r +crefOf (SynchronisedModify r) = Just r +crefOf (PartiallySynchronisedCommit r) = Just r +crefOf (PartiallySynchronisedWrite r) = Just r +crefOf (PartiallySynchronisedModify r) = Just r +crefOf _ = Nothing + +-- | Get the 'MVar' affected. +mvarOf :: ActionType -> Maybe MVarId +mvarOf (SynchronisedRead c) = Just c +mvarOf (SynchronisedWrite c) = Just c +mvarOf _ = Nothing + +-- | Throw away information from a 'ThreadAction' and give a +-- simplified view of what is happening. +-- +-- This is used in the SCT code to help determine interesting +-- alternative scheduling decisions. +simplifyAction :: ThreadAction -> ActionType +simplifyAction = maybe UnsynchronisedOther simplifyLookahead . rewind + +-- | Variant of 'simplifyAction' that takes a 'Lookahead'. +simplifyLookahead :: Lookahead -> ActionType +simplifyLookahead (WillPutMVar c) = SynchronisedWrite c +simplifyLookahead (WillTryPutMVar c) = SynchronisedWrite c +simplifyLookahead (WillReadMVar c) = SynchronisedRead c +simplifyLookahead (WillTryReadMVar c) = SynchronisedRead c +simplifyLookahead (WillTakeMVar c) = SynchronisedRead c +simplifyLookahead (WillTryTakeMVar c) = SynchronisedRead c +simplifyLookahead (WillReadCRef r) = UnsynchronisedRead r +simplifyLookahead (WillReadCRefCas r) = UnsynchronisedRead r +simplifyLookahead (WillModCRef r) = SynchronisedModify r +simplifyLookahead (WillModCRefCas r) = PartiallySynchronisedModify r +simplifyLookahead (WillWriteCRef r) = UnsynchronisedWrite r +simplifyLookahead (WillCasCRef r) = PartiallySynchronisedWrite r +simplifyLookahead (WillCommitCRef _ r) = PartiallySynchronisedCommit r +simplifyLookahead WillSTM = SynchronisedOther +simplifyLookahead (WillThrowTo _) = SynchronisedOther +simplifyLookahead _ = UnsynchronisedOther + +------------------------------------------------------------------------------- +-- * Error reporting + +-- | 'head' but with a better error message if it fails. Use this +-- only where it shouldn't fail! +ehead :: String -> [a] -> a +ehead _ (x:_) = x +ehead src _ = fatal src "head: empty list" + +-- | 'tail' but with a better error message if it fails. Use this +-- only where it shouldn't fail! +etail :: String -> [a] -> [a] +etail _ (_:xs) = xs +etail src _ = fatal src "tail: empty list" + +-- | '(!!)' but with a better error message if it fails. Use this +-- only where it shouldn't fail! +eidx :: String -> [a] -> Int -> a +eidx src xs i + | i < length xs = xs !! i + | otherwise = fatal src "(!!): index too large" + +-- | 'fromJust' but with a better error message if it fails. Use this +-- only where it shouldn't fail! +efromJust :: String -> Maybe a -> a +efromJust _ (Just x) = x +efromJust src _ = fatal src "fromJust: Nothing" + +-- | 'fromList' but with a better error message if it fails. Use this +-- only where it shouldn't fail! +efromList :: String -> [a] -> NonEmpty a +efromList _ (x:xs) = x:|xs +efromList src _ = fatal src "fromList: empty list" + +-- | 'error' but saying where it came from +fatal :: String -> String -> a +fatal src msg = error ("(dejafu: " ++ src ++ ") " ++ msg) + +------------------------------------------------------------------------------- +-- * Miscellaneous + +-- | Run with a continuation that writes its value into a reference, +-- returning the computation and the reference. Using the reference +-- is non-blocking, it is up to you to ensure you wait sufficiently. +runRefCont :: MonadRef r n => (n () -> x) -> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, r (Maybe b)) +runRefCont act f k = do + ref <- newRef Nothing + let c = k (act . writeRef ref . f) + pure (c, ref) diff --git a/Test/DejaFu/Refinement.hs b/Test/DejaFu/Refinement.hs --- a/Test/DejaFu/Refinement.hs +++ b/Test/DejaFu/Refinement.hs @@ -106,8 +106,7 @@ ) where import Control.Arrow (first) -import Control.Monad (void) -import Control.Monad.Conc.Class (readMVar, spawn) +import Control.Monad.Conc.Class (fork) import Data.Maybe (isNothing) import Data.Set (Set) import qualified Data.Set as S @@ -410,9 +409,9 @@ results <- runSCT defaultWay defaultMemType $ do s <- initialise sig x r <- subconcurrency $ do - j <- spawn (interfere sig s x) - void (expression sig s) - void (readMVar j) + _ <- fork (interfere sig s x) + _ <- expression sig s + pure () o <- observe sig s x pure (either Just (const Nothing) r, o) pure . S.fromList $ map (\(Right a, _) -> a) results diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -4,7 +4,7 @@ -- | -- Module : Test.DejaFu.SCT --- Copyright : (c) 2016 Michael Walker +-- Copyright : (c) 2015--2017 Michael Walker -- License : MIT -- Maintainer : Michael Walker -- Stability : experimental @@ -59,37 +59,12 @@ -- K. McKinley for more details. , Bounds(..) - , noBounds - , sctBound - , sctBoundDiscard - - -- ** Pre-emption Bounding - - -- | BPOR using pre-emption bounding. This adds conservative - -- backtracking points at the prior context switch whenever a - -- non-conervative backtracking point is added, as alternative - -- decisions can influence the reachability of different states. - -- - -- See the BPOR paper for more details. - , PreemptionBound(..) - - -- ** Fair Bounding - - -- | BPOR using fair bounding. This bounds the maximum difference - -- between the number of yield operations different threads have - -- performed. - -- - -- See the BPOR paper for more details. - , FairBound(..) - - -- ** Length Bounding - - -- | BPOR using length bounding. This bounds the maximum length (in - -- terms of primitive actions) of an execution. - , LengthBound(..) + , noBounds + , sctBound + , sctBoundDiscard -- * Random Scheduling @@ -106,19 +81,23 @@ , sctWeightedRandomDiscard ) where -import Control.Applicative ((<|>)) -import Control.DeepSeq (NFData(..), force) -import Control.Monad.Ref (MonadRef) -import Data.List (foldl') -import qualified Data.Map.Strict as M -import Data.Maybe (fromMaybe) -import Data.Set (Set) -import qualified Data.Set as S -import System.Random (RandomGen, randomR) +import Control.Applicative ((<|>)) +import Control.DeepSeq (NFData(..), force) +import Control.Monad.Conc.Class (MonadConc) +import Control.Monad.Ref (MonadRef) +import Data.List (foldl') +import qualified Data.Map.Strict as M +import Data.Maybe (fromMaybe) +import Data.Set (Set) +import qualified Data.Set as S +import System.Random (RandomGen, randomR) -import Test.DejaFu.Common import Test.DejaFu.Conc -import Test.DejaFu.SCT.Internal +import Test.DejaFu.Internal +import Test.DejaFu.SCT.Internal.DPOR +import Test.DejaFu.SCT.Internal.Weighted +import Test.DejaFu.Types +import Test.DejaFu.Utils ------------------------------------------------------------------------------- -- Running Concurrent Programs @@ -207,8 +186,11 @@ -- | Explore possible executions of a concurrent program according to -- the given 'Way'. -- --- @since 0.6.0.0 -runSCT :: MonadRef r n +-- The exact executions tried, and the order in which results are +-- found, is unspecified and may change between releases. +-- +-- @since 1.0.0.0 +runSCT :: (MonadConc n, MonadRef r n) => Way -- ^ How to run the concurrent program. -> MemType @@ -220,8 +202,8 @@ -- | Return the set of results of a concurrent program. -- --- @since 0.6.0.0 -resultsSet :: (MonadRef r n, Ord a) +-- @since 1.0.0.0 +resultsSet :: (MonadConc n, MonadRef r n, Ord a) => Way -- ^ How to run the concurrent program. -> MemType @@ -231,26 +213,13 @@ -> n (Set (Either Failure a)) resultsSet = resultsSetDiscard (const Nothing) --- | An @Either Failure a -> Maybe Discard@ value can be used to --- selectively discard results. --- --- @since 0.7.1.0 -data Discard - = DiscardTrace - -- ^ Discard the trace but keep the result. The result will appear - -- to have an empty trace. - | DiscardResultAndTrace - -- ^ Discard the result and the trace. It will simply not be - -- reported as a possible behaviour of the program. - deriving (Eq, Show, Read, Ord, Enum, Bounded) - -instance NFData Discard where - rnf d = d `seq` () - -- | A variant of 'runSCT' which can selectively discard results. -- --- @since 0.7.1.0 -runSCTDiscard :: MonadRef r n +-- The exact executions tried, and the order in which results are +-- found, is unspecified and may change between releases. +-- +-- @since 1.0.0.0 +runSCTDiscard :: (MonadConc n, MonadRef r n) => (Either Failure a -> Maybe Discard) -- ^ Selectively discard results. -> Way @@ -266,8 +235,8 @@ -- | A variant of 'resultsSet' which can selectively discard results. -- --- @since 0.7.1.0 -resultsSetDiscard :: (MonadRef r n, Ord a) +-- @since 1.0.0.0 +resultsSetDiscard :: (MonadConc n, MonadRef r n, Ord a) => (Either Failure a -> Maybe Discard) -- ^ Selectively discard results. Traces are always discarded. -> Way @@ -286,8 +255,11 @@ -- Demanding the result of this will force it to normal form, which -- may be more efficient in some situations. -- --- @since 0.6.0.0 -runSCT' :: (MonadRef r n, NFData a) +-- The exact executions tried, and the order in which results are +-- found, is unspecified and may change between releases. +-- +-- @since 1.0.0.0 +runSCT' :: (MonadConc n, MonadRef r n, NFData a) => Way -> MemType -> ConcT r n a -> n [(Either Failure a, Trace)] runSCT' = runSCTDiscard' (const Nothing) @@ -296,8 +268,8 @@ -- Demanding the result of this will force it to normal form, which -- may be more efficient in some situations. -- --- @since 0.6.0.0 -resultsSet' :: (MonadRef r n, Ord a, NFData a) +-- @since 1.0.0.0 +resultsSet' :: (MonadConc n, MonadRef r n, Ord a, NFData a) => Way -> MemType -> ConcT r n a -> n (Set (Either Failure a)) resultsSet' = resultsSetDiscard' (const Nothing) @@ -306,8 +278,11 @@ -- Demanding the result of this will force it to normal form, which -- may be more efficient in some situations. -- --- @since 0.7.1.0 -runSCTDiscard' :: (MonadRef r n, NFData a) +-- The exact executions tried, and the order in which results are +-- found, is unspecified and may change between releases. +-- +-- @since 1.0.0.0 +runSCTDiscard' :: (MonadConc n, MonadRef r n, NFData a) => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT r n a -> n [(Either Failure a, Trace)] runSCTDiscard' discard way memtype conc = do res <- runSCTDiscard discard way memtype conc @@ -318,8 +293,8 @@ -- Demanding the result of this will force it to normal form, which -- may be more efficient in some situations. -- --- @since 0.7.1.0 -resultsSetDiscard' :: (MonadRef r n, Ord a, NFData a) +-- @since 1.0.0.0 +resultsSetDiscard' :: (MonadConc n, MonadRef r n, Ord a, NFData a) => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT r n a -> n (Set (Either Failure a)) resultsSetDiscard' discard way memtype conc = do res <- resultsSetDiscard discard way memtype conc @@ -376,7 +351,14 @@ ------------------------------------------------------------------------------- -- Pre-emption bounding --- | @since 0.2.0.0 +-- | BPOR using pre-emption bounding. This adds conservative +-- backtracking points at the prior context switch whenever a +-- non-conervative backtracking point is added, as alternative +-- decisions can influence the reachability of different states. +-- +-- See the BPOR paper for more details. +-- +-- @since 0.2.0.0 newtype PreemptionBound = PreemptionBound Int deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show) @@ -415,7 +397,13 @@ ------------------------------------------------------------------------------- -- Fair bounding --- | @since 0.2.0.0 +-- | BPOR using fair bounding. This bounds the maximum difference +-- between the number of yield operations different threads have +-- performed. +-- +-- See the BPOR paper for more details. +-- +-- @since 0.2.0.0 newtype FairBound = FairBound Int deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show) @@ -432,8 +420,8 @@ then Just k' else Nothing --- | Add a backtrack point. If the thread isn't runnable, or performs --- a release operation, add all runnable threads. +-- | Add a backtrack point. If the thread doesn't exist or is blocked, +-- or performs a release operation, add all unblocked threads. fBacktrack :: BacktrackFunc fBacktrack = backtrackAt check where -- True if a release operation is performed. @@ -442,7 +430,10 @@ ------------------------------------------------------------------------------- -- Length bounding --- | @since 0.2.0.0 +-- | BPOR using length bounding. This bounds the maximum length (in +-- terms of primitive actions) of an execution. +-- +-- @since 0.2.0.0 newtype LengthBound = LengthBound Int deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show) @@ -457,8 +448,8 @@ let len' = maybe 1 (+1) len in if len' < lb then Just len' else Nothing --- | Add a backtrack point. If the thread isn't runnable, add all --- runnable threads. +-- | Add a backtrack point. If the thread doesn't exist or is blocked, +-- add all unblocked threads. lBacktrack :: BacktrackFunc lBacktrack = backtrackAt (\_ _ -> False) @@ -477,8 +468,11 @@ -- 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 +-- The exact executions tried, and the order in which results are +-- found, is unspecified and may change between releases. +-- +-- @since 1.0.0.0 +sctBound :: (MonadConc n, MonadRef r n) => MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. -> Bounds @@ -490,8 +484,11 @@ -- | A variant of 'sctBound' which can selectively discard results. -- --- @since 0.7.1.0 -sctBoundDiscard :: MonadRef r n +-- The exact executions tried, and the order in which results are +-- found, is unspecified and may change between releases. +-- +-- @since 1.0.0.0 +sctBoundDiscard :: (MonadConc n, MonadRef r n) => (Either Failure a -> Maybe Discard) -- ^ Selectively discard results. -> MemType @@ -533,8 +530,8 @@ -- -- This is not guaranteed to find all distinct results. -- --- @since 0.7.0.0 -sctUniformRandom :: (MonadRef r n, RandomGen g) +-- @since 1.0.0.0 +sctUniformRandom :: (MonadConc n, MonadRef r n, RandomGen g) => MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. -> g @@ -549,8 +546,10 @@ -- | A variant of 'sctUniformRandom' which can selectively discard -- results. -- --- @since 0.7.1.0 -sctUniformRandomDiscard :: (MonadRef r n, RandomGen g) +-- This is not guaranteed to find all distinct results. +-- +-- @since 1.0.0.0 +sctUniformRandomDiscard :: (MonadConc n, MonadRef r n, RandomGen g) => (Either Failure a -> Maybe Discard) -- ^ Selectively discard results. -> MemType @@ -578,8 +577,8 @@ -- -- This is not guaranteed to find all distinct results. -- --- @since 0.7.0.0 -sctWeightedRandom :: (MonadRef r n, RandomGen g) +-- @since 1.0.0.0 +sctWeightedRandom :: (MonadConc n, MonadRef r n, RandomGen g) => MemType -- ^ The memory model to use for non-synchronised @CRef@ operations. -> g @@ -596,8 +595,10 @@ -- | A variant of 'sctWeightedRandom' which can selectively discard -- results. -- --- @since 0.7.1.0 -sctWeightedRandomDiscard :: (MonadRef r n, RandomGen g) +-- This is not guaranteed to find all distinct results. +-- +-- @since 1.0.0.0 +sctWeightedRandomDiscard :: (MonadConc n, MonadRef r n, RandomGen g) => (Either Failure a -> Maybe Discard) -- ^ Selectively discard results. -> MemType diff --git a/Test/DejaFu/SCT/Internal.hs b/Test/DejaFu/SCT/Internal.hs deleted file mode 100644 --- a/Test/DejaFu/SCT/Internal.hs +++ /dev/null @@ -1,816 +0,0 @@ -{-# LANGUAGE TupleSections #-} - --- | --- Module : Test.DejaFu.SCT.Internal --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- Stability : experimental --- Portability : TupleSections --- --- Internal types and functions for dynamic partial-order --- reduction. This module is NOT considered to form part of the public --- interface of this library. -module Test.DejaFu.SCT.Internal where - -import Control.Applicative ((<|>)) -import Control.DeepSeq (NFData(..)) -import Control.Exception (MaskingState(..)) -import qualified Data.Foldable as F -import Data.Function (on) -import Data.List (nubBy, partition, sortOn) -import Data.List.NonEmpty (toList) -import Data.Map.Strict (Map) -import qualified Data.Map.Strict as M -import Data.Maybe (fromMaybe, 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 (Scheduler(..), decisionOf, tidOf) - -------------------------------------------------------------------------------- --- * Dynamic partial-order reduction - --- | DPOR execution is represented as a tree of states, characterised --- by the decisions that lead to that state. -data DPOR = DPOR - { dporRunnable :: Set ThreadId - -- ^ What threads are runnable at this step. - , dporTodo :: Map ThreadId Bool - -- ^ Follow-on decisions still to make, and whether that decision - -- was added conservatively due to the bound. - , dporNext :: Maybe (ThreadId, DPOR) - -- ^ The next decision made. Executions are explored in a - -- depth-first fashion, so this changes as old subtrees are - -- exhausted and new ones explored. - , dporDone :: Set ThreadId - -- ^ All transitions which have been taken from this point, - -- including conservatively-added ones. - , dporSleep :: Map ThreadId ThreadAction - -- ^ Transitions to ignore (in this node and children) until a - -- dependent transition happens. - , dporTaken :: Map ThreadId ThreadAction - -- ^ Transitions which have been taken, excluding - -- conservatively-added ones. This is used in implementing sleep - -- sets. - } deriving (Eq, Show) - -instance NFData DPOR where - rnf dpor = rnf ( dporRunnable dpor - , dporTodo dpor - , dporNext dpor - , dporDone dpor - , dporSleep dpor - , dporTaken dpor - ) - --- | One step of the execution, including information for backtracking --- purposes. This backtracking information is used to generate new --- schedules. -data BacktrackStep = BacktrackStep - { bcktThreadid :: ThreadId - -- ^ The thread running at this step - , bcktDecision :: Decision - -- ^ What was decided at this step. - , bcktAction :: ThreadAction - -- ^ What happened at this step. - , bcktRunnable :: Map ThreadId Lookahead - -- ^ The threads runnable at this step - , bcktBacktracks :: Map ThreadId Bool - -- ^ The list of alternative threads to run, and whether those - -- alternatives were added conservatively due to the bound. - , bcktState :: DepState - -- ^ Some domain-specific state at this point. - } deriving (Eq, Show) - -instance NFData BacktrackStep where - rnf bs = rnf ( bcktThreadid bs - , bcktDecision bs - , bcktAction bs - , bcktRunnable bs - , bcktBacktracks bs - , bcktState bs - ) - --- | Initial DPOR state, given an initial thread ID. This initial --- thread should exist and be runnable at the start of execution. -initialState :: DPOR -initialState = DPOR - { dporRunnable = S.singleton initialThread - , dporTodo = M.singleton initialThread False - , dporNext = Nothing - , dporDone = S.empty - , dporSleep = M.empty - , dporTaken = M.empty - } - --- | Produce a new schedule prefix from a @DPOR@ tree. If there are no new --- prefixes remaining, return 'Nothing'. Also returns whether the --- decision was added conservatively, and the sleep set at the point --- where divergence happens. --- --- A schedule prefix is a possibly empty sequence of decisions that --- have already been made, terminated by a single decision from the --- to-do set. The intent is to put the system into a new state when --- executed with this initial sequence of scheduling decisions. -findSchedulePrefix - :: DPOR - -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction) -findSchedulePrefix dpor = case dporNext dpor of - Just (tid, child) -> go tid child <|> here - Nothing -> here - where - go tid child = (\(ts,c,slp) -> (tid:ts,c,slp)) <$> findSchedulePrefix child - - -- Prefix traces terminating with a to-do decision at this point. - here = - let todos = [([t], c, sleeps) | (t, c) <- M.toList $ dporTodo dpor] - (best, worst) = partition (\([t],_,_) -> t >= initialThread) todos - in listToMaybe best <|> listToMaybe worst - - -- The new sleep set is the union of the sleep set of the node - -- we're branching from, plus all the decisions we've already - -- explored. - sleeps = dporSleep dpor `M.union` dporTaken dpor - --- | Add a new trace to the stack. This won't work if to-dos aren't explored depth-first. -incorporateTrace - :: Bool - -- ^ Whether the \"to-do\" point which was used to create this new - -- execution was conservative or not. - -> Trace - -- ^ The execution trace: the decision made, the runnable threads, - -- and the action performed. - -> DPOR - -> DPOR -incorporateTrace conservative trace dpor0 = grow initialDepState (initialDPORThread dpor0) trace dpor0 where - grow state tid trc@((d, _, a):rest) dpor = - let tid' = tidOf tid d - state' = updateDepState state tid' a - in case dporNext dpor of - Just (t, child) - | t == tid' -> dpor { dporNext = Just (tid', grow state' tid' rest child) } - | hasTodos child -> fatal "incorporateTrace" "replacing child with todos!" - _ -> - let taken = M.insert tid' a (dporTaken dpor) - sleep = dporSleep dpor `M.union` dporTaken dpor - in dpor { dporTaken = if conservative then dporTaken dpor else taken - , dporTodo = M.delete tid' (dporTodo dpor) - , dporNext = Just (tid', subtree state' tid' sleep trc) - , dporDone = S.insert tid' (dporDone dpor) - } - grow _ _ [] _ = fatal "incorporateTrace" "trace exhausted without reading a to-do point!" - - -- check if there are to-do points in a tree - hasTodos dpor = not (M.null (dporTodo dpor)) || (case dporNext dpor of Just (_, dpor') -> hasTodos dpor'; _ -> False) - - -- 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 state' tid a t a') sleep - in DPOR - { dporRunnable = S.fromList $ case rest of - ((_, runnable, _):_) -> map fst runnable - [] -> [] - , dporTodo = M.empty - , dporNext = case rest of - ((d', _, _):_) -> - let tid' = tidOf tid d' - in Just (tid', subtree state' tid' sleep' rest) - [] -> Nothing - , dporDone = case rest of - ((d', _, _):_) -> S.singleton (tidOf tid d') - [] -> S.empty - , dporSleep = sleep' - , dporTaken = case rest of - ((d', _, a'):_) -> M.singleton (tidOf tid d') a' - [] -> M.empty - } - subtree _ _ _ [] = fatal "incorporateTrace" "subtree suffix empty!" - --- | Produce a list of new backtracking points from an execution --- trace. These are then used to inform new \"to-do\" points in the --- @DPOR@ tree. --- --- Two traces are passed in to this function: the first is generated --- from the special DPOR scheduler, the other from the execution of --- the concurrent program. --- --- If the trace ends with any threads other than the initial one still --- runnable, a dependency is imposed between this final action and --- everything else. -findBacktrackSteps - :: BacktrackFunc - -- ^ Backtracking function. Given a list of backtracking points, and - -- a thread to backtrack to at a specific point in that list, add - -- the new backtracking points. There will be at least one: this - -- chosen one, but the function may add others. - -> Bool - -- ^ Whether the computation was aborted due to no decisions being - -- in-bounds. - -> Seq ([(ThreadId, Lookahead)], [ThreadId]) - -- ^ A sequence of threads at each step: the list of runnable - -- in-bound threads (with lookahead values), and the list of threads - -- still to try. The reason for the two separate lists is because - -- the threads chosen to try will be dependent on the specific - -- domain. - -> Trace - -- ^ The execution trace. - -> [BacktrackStep] -findBacktrackSteps backtrack boundKill = go initialDepState S.empty initialThread [] . F.toList where - -- Walk through the traces one step at a time, building up a list of - -- new backtracking points. - go state allThreads tid bs ((e,i):is) ((d,_,a):ts) = - let tid' = tidOf tid d - state' = updateDepState state tid' a - this = BacktrackStep - { bcktThreadid = tid' - , bcktDecision = d - , bcktAction = a - , bcktRunnable = M.fromList e - , bcktBacktracks = M.fromList $ map (\i' -> (i', False)) i - , bcktState = state - } - bs' = doBacktrack killsEarly allThreads' e (bs++[this]) - runnable = S.fromList (M.keys $ bcktRunnable this) - allThreads' = allThreads `S.union` runnable - killsEarly = null ts && boundKill - in go state' allThreads' tid' bs' is ts - go _ _ _ bs _ _ = bs - - -- Find the prior actions dependent with this one and add - -- backtracking points. - doBacktrack killsEarly allThreads enabledThreads bs = - let tagged = reverse $ zip [0..] bs - idxs = [ (ehead "doBacktrack.idxs" is, False, u) - | (u, n) <- enabledThreads - , v <- S.toList allThreads - , u /= v - , let is = idxs' u n v tagged - , not $ null is] - - idxs' u n v = go' True where - {-# INLINE go' #-} - go' final ((i,b):rest) - -- Don't cross subconcurrency boundaries - | isSubC final b = [] - -- If this is the final action in the trace and the - -- execution was killed due to nothing being within bounds - -- (@killsEarly == True@) assume worst-case dependency. - | bcktThreadid b == v && (killsEarly || isDependent b) = i : go' False rest - | otherwise = go' False rest - go' _ [] = [] - - {-# INLINE isSubC #-} - isSubC final b = case bcktAction b of - Stop -> not final && bcktThreadid b == initialThread - Subconcurrency -> bcktThreadid b == initialThread - _ -> False - - {-# INLINE isDependent #-} - isDependent b - -- Don't impose a dependency if the other thread will - -- immediately block already. This is safe because a - -- context switch will occur anyway so there's no point - -- pre-empting the action UNLESS the pre-emption would - -- possibly allow for a different relaxed memory stage. - | isBlock (bcktAction b) && isBarrier (simplifyLookahead n) = False - | otherwise = dependent' (bcktState b) (bcktThreadid b) (bcktAction b) u n - in backtrack bs idxs - --- | Add new backtracking points, if they have not already been --- visited and aren't in the sleep set. -incorporateBacktrackSteps :: [BacktrackStep] -> DPOR -> DPOR -incorporateBacktrackSteps (b:bs) dpor = dpor' where - tid = bcktThreadid b - - dpor' = dpor - { dporTodo = dporTodo dpor `M.union` M.fromList todo - , dporNext = Just (tid, child) - } - - todo = - [ x - | x@(t,c) <- M.toList $ bcktBacktracks b - , Just t /= (fst <$> dporNext dpor) - , S.notMember t (dporDone dpor) - , c || M.notMember t (dporSleep dpor) - ] - - child = case dporNext dpor of - Just (t, d) - | t /= tid -> fatal "incorporateBacktrackSteps" "incorporating wrong trace!" - | otherwise -> incorporateBacktrackSteps bs d - Nothing -> fatal "incorporateBacktrackSteps" "child is missing!" -incorporateBacktrackSteps [] dpor = dpor - -------------------------------------------------------------------------------- --- * DPOR scheduler - --- | The scheduler state -data DPORSchedState k = DPORSchedState - { schedSleep :: Map ThreadId ThreadAction - -- ^ The sleep set: decisions not to make until something dependent - -- with them happens. - , schedPrefix :: [ThreadId] - -- ^ Decisions still to make - , schedBPoints :: Seq ([(ThreadId, Lookahead)], [ThreadId]) - -- ^ Which threads are runnable and in-bound at each step, and the - -- alternative decisions still to make. - , schedIgnore :: Bool - -- ^ Whether to ignore this execution or not: @True@ if the - -- execution is aborted due to all possible decisions being in the - -- sleep set, as then everything in this execution is covered by - -- another. - , schedBoundKill :: Bool - -- ^ Whether the execution was terminated due to all decisions being - -- out of bounds. - , schedDepState :: DepState - -- ^ State used by the dependency function to determine when to - -- remove decisions from the sleep set. - , schedBState :: Maybe k - -- ^ State used by the incremental bounding function. - } deriving (Eq, Show) - -instance NFData k => NFData (DPORSchedState k) where - rnf s = rnf ( schedSleep s - , schedPrefix s - , schedBPoints s - , schedIgnore s - , schedBoundKill s - , schedDepState s - , schedBState s - ) - --- | Initial DPOR scheduler state for a given prefix -initialDPORSchedState :: Map ThreadId ThreadAction - -- ^ The initial sleep set. - -> [ThreadId] - -- ^ The schedule prefix. - -> DPORSchedState k -initialDPORSchedState sleep prefix = DPORSchedState - { schedSleep = sleep - , schedPrefix = prefix - , schedBPoints = Sq.empty - , schedIgnore = False - , schedBoundKill = False - , schedDepState = initialDepState - , schedBState = Nothing - } - --- | An incremental bounding function is a stateful function that --- takes the last and next decisions, and returns a new state only if --- the next decision is within the bound. -type IncrementalBoundFunc k - = Maybe k -> Maybe (ThreadId, ThreadAction) -> (Decision, Lookahead) -> Maybe k - --- | A backtracking step is a point in the execution where another --- decision needs to be made, in order to explore interesting new --- schedules. A backtracking /function/ takes the steps identified so --- far and a list of points and thread at that point to backtrack --- to. More points be added to compensate for the effects of the --- bounding function. For example, under pre-emption bounding a --- conservative backtracking point is added at the prior context --- switch. The bool is whether the point is conservative. Conservative --- points are always explored, whereas non-conservative ones might be --- skipped based on future information. --- --- In general, a backtracking function should identify one or more --- backtracking points, and then use @backtrackAt@ to do the actual --- work. -type BacktrackFunc - = [BacktrackStep] -> [(Int, Bool, ThreadId)] -> [BacktrackStep] - --- | Add a backtracking point. If the thread isn't runnable, add all --- runnable threads. If the backtracking point is already present, --- don't re-add it UNLESS this would make it conservative. -backtrackAt - :: (ThreadId -> BacktrackStep -> Bool) - -- ^ If this returns @True@, backtrack to all runnable threads, - -- rather than just the given thread. - -> BacktrackFunc -backtrackAt toAll bs0 = backtrackAt' . nubBy ((==) `on` fst') . sortOn fst' where - fst' (x,_,_) = x - - backtrackAt' ((i,c,t):is) = go i bs0 i c t is - backtrackAt' [] = bs0 - - go i0 (b:bs) 0 c tid is - -- If the backtracking point is already present, don't re-add it, - -- UNLESS this would force it to backtrack (it's conservative) - -- where before it might not. - | not (toAll tid b) && tid `M.member` bcktRunnable b = - let val = M.lookup tid $ bcktBacktracks b - b' = if isNothing val || (val == Just False && c) - then b { bcktBacktracks = backtrackTo tid c b } - else b - in b' : case is of - ((i',c',t'):is') -> go i' bs (i'-i0-1) c' t' is' - [] -> bs - -- Otherwise just backtrack to everything runnable. - | otherwise = - let b' = b { bcktBacktracks = backtrackAll c b } - in b' : case is of - ((i',c',t'):is') -> go i' bs (i'-i0-1) c' t' is' - [] -> bs - go i0 (b:bs) i c tid is = b : go i0 bs (i-1) c tid is - go _ [] _ _ _ _ = fatal "backtrackAt" "ran out of schedule whilst backtracking!" - - -- Backtrack to a single thread - backtrackTo tid c = M.insert tid c . bcktBacktracks - - -- Backtrack to all runnable threads - backtrackAll c = M.map (const c) . bcktRunnable - --- | DPOR scheduler: takes a list of decisions, and maintains a trace --- including the runnable threads, and the alternative choices allowed --- by the bound-specific initialise function. --- --- After the initial decisions are exhausted, this prefers choosing --- the prior thread if it's (1) still runnable and (2) hasn't just --- yielded. Furthermore, threads which /will/ yield are ignored in --- preference of those which will not. -dporSched - :: IncrementalBoundFunc k - -- ^ Bound function: returns true if that schedule prefix terminated - -- with the lookahead decision fits within the bound. - -> Scheduler (DPORSchedState k) -dporSched boundf = Scheduler $ \prior threads s -> - let - -- The next scheduler state - nextState rest = s - { schedBPoints = schedBPoints s |> (restrictToBound fst threads', rest) - , schedDepState = nextDepState - } - nextDepState = let ds = schedDepState s in maybe ds (uncurry $ updateDepState ds) prior - - -- Pick a new thread to run, not considering bounds. Choose the - -- current thread if available and it hasn't just yielded, - -- otherwise add all runnable threads. - initialise = tryDaemons . yieldsToEnd $ case prior of - Just (tid, act) - | not (didYield act) && tid `elem` tids && isInBound tid -> [tid] - _ -> tids - - -- If one of the chosen actions will kill the computation, and - -- there are daemon threads, try them instead. - -- - -- This is necessary if the killing action is NOT dependent with - -- every other action, according to the dependency function. This - -- is, strictly speaking, wrong; an action that kills another - -- thread is definitely dependent with everything in that - -- thread. HOWEVER, implementing it that way leads to an explosion - -- of schedules tried. Really, all that needs to happen is for the - -- thread-that-would-be-killed to be executed fully ONCE, and then - -- the normal dependency mechanism will identify any other - -- backtracking points that should be tried. This is achieved by - -- adding every thread that would be killed to the to-do list. - -- Furthermore, these threads MUST be ahead of the killing thread, - -- or the killing thread will end up in the sleep set and so the - -- killing action not performed. This is, again, because of the - -- lack of the dependency messing things up in the name of - -- performance. - -- - -- See commits a056f54 and 8554ce9, and my 4th June comment in - -- issue #52. - tryDaemons ts - | any doesKill ts = case partition doesKill tids of - (kills, nokills) -> nokills ++ kills - | otherwise = ts - doesKill t = killsDaemons t (action t) - - -- Restrict the possible decisions to those in the bound. - restrictToBound f = filter (isInBound . f) - isInBound t = isJust $ boundf (schedBState s) prior (decision t, action t) - - -- Move the threads which will immediately yield to the end of the list - yieldsToEnd ts = case partition (willYield . action) ts of - (yields, noyields) -> noyields ++ yields - - -- Get the decision that will lead to a thread being scheduled. - decision = decisionOf (fst <$> prior) (S.fromList tids) - - -- Get the action of a thread - action t = efromJust "dporSched.action" (lookup t threads') - - -- The runnable thread IDs - tids = map fst threads' - - -- The runnable threads as a normal list. - threads' = toList threads - in case schedPrefix s of - -- If there is a decision available, make it - (t:ts) -> - let bstate' = boundf (schedBState s) prior (decision t, action t) - in (Just t, (nextState []) { schedPrefix = ts, schedBState = bstate' }) - - -- Otherwise query the initialise function for a list of possible - -- choices, filter out anything in the sleep set, and make one of - -- them arbitrarily (recording the others). - [] -> - let choices = restrictToBound id initialise - checkDep t a = case prior of - Just (tid, act) -> dependent (schedDepState s) tid act t a - Nothing -> False - ssleep' = M.filterWithKey (\t a -> not $ checkDep t a) $ schedSleep s - choices' = filter (`notElem` M.keys ssleep') choices - signore' = not (null choices) && all (`elem` M.keys ssleep') choices - sbkill' = not (null initialise) && null choices - in case choices' of - (nextTid:rest) -> - let bstate' = boundf (schedBState s) prior (decision nextTid, action nextTid) - in (Just nextTid, (nextState rest) { schedSleep = ssleep', schedBState = bstate' }) - [] -> - (Nothing, (nextState []) { schedIgnore = signore', schedBoundKill = sbkill', schedBState = Nothing }) - -------------------------------------------------------------------------------- --- Weighted random scheduler - --- | The scheduler state -data RandSchedState g = RandSchedState - { schedWeights :: Map ThreadId Int - -- ^ The thread weights: used in determining which to run. - , schedGen :: g - -- ^ The random number generator. - } deriving (Eq, Show) - -instance NFData g => NFData (RandSchedState g) where - rnf s = rnf ( schedWeights s - , schedGen s - ) - --- | Initial weighted random scheduler state. -initialRandSchedState :: Maybe (Map ThreadId Int) -> g -> RandSchedState g -initialRandSchedState = RandSchedState . fromMaybe M.empty - --- | Weighted random scheduler: assigns to each new thread a weight, --- and makes a weighted random choice out of the runnable threads at --- every step. -randSched :: RandomGen g => (g -> (Int, g)) -> Scheduler (RandSchedState g) -randSched weightf = Scheduler $ \_ threads s -> - let - -- Select a thread - pick idx ((x, f):xs) - | idx < f = Just x - | otherwise = pick (idx - f) xs - pick _ [] = Nothing - (choice, g'') = randomR (0, sum (map snd enabled) - 1) g' - enabled = M.toList $ M.filterWithKey (\tid _ -> tid `elem` tids) weights' - - -- The weights, with any new threads added. - (weights', g') = foldr assignWeight (M.empty, schedGen s) tids - assignWeight tid ~(ws, g0) = - let (w, g) = maybe (weightf g0) (,g0) (M.lookup tid (schedWeights s)) - in (M.insert tid w ws, g) - - -- The runnable threads. - tids = map fst (toList threads) - in (pick choice enabled, RandSchedState weights' g'') - -------------------------------------------------------------------------------- --- Dependency function - --- | Check if an action is dependent on another. --- --- This is basically the same as 'dependent'', but can make use of the --- additional information in a 'ThreadAction' to make better decisions --- in a few cases. -dependent :: DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool -dependent ds t1 a1 t2 a2 = case (a1, a2) of - -- @SetNumCapabilities@ and @GetNumCapabilities@ are NOT dependent - -- IF the value read is the same as the value written. 'dependent'' - -- can not see the value read (as it hasn't happened yet!), and so - -- is more pessimistic here. - (SetNumCapabilities a, GetNumCapabilities b) | a == b -> False - (GetNumCapabilities a, SetNumCapabilities b) | a == b -> False - - -- When masked interruptible, a thread can only be interrupted when - -- actually blocked. 'dependent'' has to assume that all - -- potentially-blocking operations can block, and so is more - -- pessimistic in this case. - (ThrowTo t, _) | t == t2 -> canInterrupt ds t2 a2 && a2 /= Stop - (_, ThrowTo t) | t == t1 -> canInterrupt ds t1 a1 && a1 /= Stop - - -- Dependency of STM transactions can be /greatly/ improved here, as - -- the 'Lookahead' does not know which @TVar@s will be touched, and - -- so has to assume all transactions are dependent. - (STM _ _, STM _ _) -> checkSTM - (STM _ _, BlockedSTM _) -> checkSTM - (BlockedSTM _, STM _ _) -> checkSTM - (BlockedSTM _, BlockedSTM _) -> checkSTM - - _ -> case (,) <$> rewind a1 <*> rewind a2 of - Just (l1, l2) -> dependent' ds t1 a1 t2 l2 && dependent' ds t2 a2 t1 l1 - _ -> dependentActions ds (simplifyAction a1) (simplifyAction a2) - - where - -- STM actions A and B are dependent if A wrote to anything B - -- touched, or vice versa. - checkSTM = checkSTM' a1 a2 || checkSTM' a2 a1 - checkSTM' a b = not . S.null $ tvarsWritten a `S.intersection` tvarsOf b - --- | Variant of 'dependent' to handle 'Lookahead'. --- --- Termination of the initial thread is handled specially in the DPOR --- implementation. -dependent' :: DepState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool -dependent' ds t1 a1 t2 l2 = case (a1, l2) of - -- Worst-case assumption: all IO is dependent. - (LiftIO, WillLiftIO) -> True - - -- Throwing an exception is only dependent with actions in that - -- thread and if the actions can be interrupted. We can also - -- slightly improve on that by not considering interrupting the - -- normal termination of a thread: it doesn't make a difference. - (ThrowTo t, WillStop) | t == t2 -> False - (Stop, WillThrowTo t) | t == t1 -> False - (ThrowTo t, _) | t == t2 -> canInterruptL ds t2 l2 - (_, WillThrowTo t) | t == t1 -> canInterrupt ds t1 a1 - - -- Another worst-case: assume all STM is dependent. - (STM _ _, WillSTM) -> True - - -- This is a bit pessimistic: Set/Get are only dependent if the - -- value set is not the same as the value that will be got, but we - -- can't know that here. 'dependent' optimises this case. - (GetNumCapabilities a, WillSetNumCapabilities b) -> a /= b - (SetNumCapabilities _, WillGetNumCapabilities) -> True - (SetNumCapabilities a, WillSetNumCapabilities b) -> a /= b - - _ -> dependentActions ds (simplifyAction a1) (simplifyLookahead l2) - --- | Check if two 'ActionType's are dependent. Note that this is not --- sufficient to know if two 'ThreadAction's are dependent, without --- being so great an over-approximation as to be useless! -dependentActions :: DepState -> ActionType -> ActionType -> Bool -dependentActions ds a1 a2 = case (a1, a2) of - -- Unsynchronised reads and writes are always dependent, even under - -- a relaxed memory model, as an unsynchronised write gives rise to - -- a commit, which synchronises. - (UnsynchronisedRead r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> a2 /= UnsynchronisedRead r1 - (UnsynchronisedWrite r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True - (PartiallySynchronisedWrite r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True - (PartiallySynchronisedModify r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True - (SynchronisedModify r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True - - -- Unsynchronised writes and synchronisation where the buffer is not - -- empty. - -- - -- See [RMMVerification], lemma 5.25. - (UnsynchronisedWrite r1, PartiallySynchronisedCommit _) | same crefOf && isBuffered ds r1 -> False - (PartiallySynchronisedCommit _, UnsynchronisedWrite r2) | same crefOf && isBuffered ds r2 -> False - - -- Unsynchronised reads where a memory barrier would flush a - -- buffered write - (UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered ds r1 - (_, UnsynchronisedRead r2) | isBarrier a1 -> isBuffered ds r2 - - -- Commits and memory barriers must be dependent, as memory barriers - -- (currently) flush in a consistent order. Alternative orders need - -- to be explored as well. Perhaps a better implementation of - -- memory barriers would just block every non-commit thread while - -- any buffer is nonempty. - (PartiallySynchronisedCommit _, _) | isBarrier a2 -> True - (_, PartiallySynchronisedCommit _) | isBarrier a1 -> True - - (_, _) -> case getSame crefOf of - -- Two actions on the same CRef where at least one is synchronised - Just r -> synchronises a1 r || synchronises a2 r - -- Two actions on the same MVar - _ -> same mvarOf - - where - same :: Eq a => (ActionType -> Maybe a) -> Bool - same = isJust . getSame - - getSame :: Eq a => (ActionType -> Maybe a) -> Maybe a - getSame f = - let f1 = f a1 - f2 = f a2 - in if f1 == f2 then f1 else Nothing - -------------------------------------------------------------------------------- --- Dependency function state - -data DepState = DepState - { depCRState :: Map CRefId Bool - -- ^ Keep track of which @CRef@s have buffered writes. - , depMaskState :: Map ThreadId MaskingState - -- ^ Keep track of thread masking states. If a thread isn't present, - -- the masking state is assumed to be @Unmasked@. This nicely - -- provides compatibility with dpor-0.1, where the thread IDs are - -- not available. - } deriving (Eq, Show) - -instance NFData DepState where - rnf depstate = rnf ( depCRState depstate - , [(t, m `seq` ()) | (t, m) <- M.toList (depMaskState depstate)] - ) - --- | Initial dependency state. -initialDepState :: DepState -initialDepState = DepState M.empty M.empty - --- | Update the 'CRef' buffer state with the action that has just --- happened. -updateDepState :: DepState -> ThreadId -> ThreadAction -> DepState -updateDepState depstate tid act = DepState - { depCRState = updateCRState act $ depCRState depstate - , depMaskState = updateMaskState tid act $ depMaskState depstate - } - --- | Update the 'CRef' buffer state with the action that has just --- happened. -updateCRState :: ThreadAction -> Map CRefId Bool -> Map CRefId Bool -updateCRState (CommitCRef _ r) = M.delete r -updateCRState (WriteCRef r) = M.insert r True -updateCRState ta - | isBarrier $ simplifyAction ta = const M.empty - | otherwise = id - --- | Update the thread masking state with the action that has just --- happened. -updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState -updateMaskState tid (Fork tid2) = \masks -> case M.lookup tid masks of - -- A thread inherits the masking state of its parent. - Just ms -> M.insert tid2 ms masks - Nothing -> masks -updateMaskState tid (SetMasking _ ms) = M.insert tid ms -updateMaskState tid (ResetMasking _ ms) = M.insert tid ms -updateMaskState _ _ = id - --- | Check if a 'CRef' has a buffered write pending. -isBuffered :: DepState -> CRefId -> Bool -isBuffered depstate r = M.findWithDefault False r (depCRState depstate) - --- | Check if an exception can interrupt a thread (action). -canInterrupt :: DepState -> ThreadId -> ThreadAction -> Bool -canInterrupt depstate tid act - -- If masked interruptible, blocked actions can be interrupted. - | isMaskedInterruptible depstate tid = case act of - BlockedPutMVar _ -> True - BlockedReadMVar _ -> True - BlockedTakeMVar _ -> True - BlockedSTM _ -> True - BlockedThrowTo _ -> True - _ -> False - -- If masked uninterruptible, nothing can be. - | isMaskedUninterruptible depstate tid = False - -- If no mask, anything can be. - | otherwise = True - --- | Check if an exception can interrupt a thread (lookahead). -canInterruptL :: DepState -> ThreadId -> Lookahead -> Bool -canInterruptL depstate tid lh - -- If masked interruptible, actions which can block may be - -- interrupted. - | isMaskedInterruptible depstate tid = case lh of - WillPutMVar _ -> True - WillReadMVar _ -> True - WillTakeMVar _ -> True - WillSTM -> True - WillThrowTo _ -> True - _ -> False - -- If masked uninterruptible, nothing can be. - | isMaskedUninterruptible depstate tid = False - -- If no mask, anything can be. - | otherwise = True - --- | Check if a thread is masked interruptible. -isMaskedInterruptible :: DepState -> ThreadId -> Bool -isMaskedInterruptible depstate tid = - M.lookup tid (depMaskState depstate) == Just MaskedInterruptible - --- | Check if a thread is masked uninterruptible. -isMaskedUninterruptible :: DepState -> ThreadId -> Bool -isMaskedUninterruptible depstate tid = - M.lookup tid (depMaskState depstate) == Just MaskedUninterruptible - -------------------------------------------------------------------------------- --- * Utilities - --- The initial thread of a DPOR tree. -initialDPORThread :: DPOR -> ThreadId -initialDPORThread = S.elemAt 0 . dporRunnable - --- | Check if a thread yielded. -didYield :: ThreadAction -> Bool -didYield Yield = True -didYield (ThreadDelay _) = True -didYield _ = False - --- | Check if a thread will yield. -willYield :: Lookahead -> Bool -willYield WillYield = True -willYield (WillThreadDelay _) = True -willYield _ = False - --- | Check if an action will kill daemon threads. -killsDaemons :: ThreadId -> Lookahead -> Bool -killsDaemons t WillStop = t == initialThread -killsDaemons _ _ = False diff --git a/Test/DejaFu/SCT/Internal/DPOR.hs b/Test/DejaFu/SCT/Internal/DPOR.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/SCT/Internal/DPOR.hs @@ -0,0 +1,793 @@ +-- | +-- Module : Test.DejaFu.SCT.Internal.DPOR +-- Copyright : (c) 2015--2017 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : portable +-- +-- Internal types and functions for SCT via dynamic partial-order +-- reduction. This module is NOT considered to form part of the +-- public interface of this library. +module Test.DejaFu.SCT.Internal.DPOR where + +import Control.Applicative ((<|>)) +import Control.DeepSeq (NFData(..)) +import Control.Exception (MaskingState(..)) +import qualified Data.Foldable as F +import Data.Function (on) +import Data.List (nubBy, partition, sortOn) +import Data.List.NonEmpty (toList) +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as M +import Data.Maybe (isJust, isNothing, listToMaybe) +import Data.Sequence (Seq, (|>)) +import qualified Data.Sequence as Sq +import Data.Set (Set) +import qualified Data.Set as S + +import Test.DejaFu.Internal +import Test.DejaFu.Schedule (Scheduler(..)) +import Test.DejaFu.Types +import Test.DejaFu.Utils (decisionOf, tidOf) + +------------------------------------------------------------------------------- +-- * Dynamic partial-order reduction + +-- | DPOR execution is represented as a tree of states, characterised +-- by the decisions that lead to that state. +data DPOR = DPOR + { dporRunnable :: Set ThreadId + -- ^ What threads are runnable at this step. + , dporTodo :: Map ThreadId Bool + -- ^ Follow-on decisions still to make, and whether that decision + -- was added conservatively due to the bound. + , dporNext :: Maybe (ThreadId, DPOR) + -- ^ The next decision made. Executions are explored in a + -- depth-first fashion, so this changes as old subtrees are + -- exhausted and new ones explored. + , dporDone :: Set ThreadId + -- ^ All transitions which have been taken from this point, + -- including conservatively-added ones. + , dporSleep :: Map ThreadId ThreadAction + -- ^ Transitions to ignore (in this node and children) until a + -- dependent transition happens. + , dporTaken :: Map ThreadId ThreadAction + -- ^ Transitions which have been taken, excluding + -- conservatively-added ones. This is used in implementing sleep + -- sets. + } deriving (Eq, Show) + +instance NFData DPOR where + rnf dpor = rnf ( dporRunnable dpor + , dporTodo dpor + , dporNext dpor + , dporDone dpor + , dporSleep dpor + , dporTaken dpor + ) + +-- | One step of the execution, including information for backtracking +-- purposes. This backtracking information is used to generate new +-- schedules. +data BacktrackStep = BacktrackStep + { bcktThreadid :: ThreadId + -- ^ The thread running at this step + , bcktDecision :: Decision + -- ^ What was decided at this step. + , bcktAction :: ThreadAction + -- ^ What happened at this step. + , bcktRunnable :: Map ThreadId Lookahead + -- ^ The threads runnable at this step + , bcktBacktracks :: Map ThreadId Bool + -- ^ The list of alternative threads to run, and whether those + -- alternatives were added conservatively due to the bound. + , bcktState :: DepState + -- ^ Some domain-specific state at this point. + } deriving (Eq, Show) + +instance NFData BacktrackStep where + rnf bs = rnf ( bcktThreadid bs + , bcktDecision bs + , bcktAction bs + , bcktRunnable bs + , bcktBacktracks bs + , bcktState bs + ) + +-- | Initial DPOR state, given an initial thread ID. This initial +-- thread should exist and be runnable at the start of execution. +initialState :: DPOR +initialState = DPOR + { dporRunnable = S.singleton initialThread + , dporTodo = M.singleton initialThread False + , dporNext = Nothing + , dporDone = S.empty + , dporSleep = M.empty + , dporTaken = M.empty + } + +-- | Produce a new schedule prefix from a @DPOR@ tree. If there are no new +-- prefixes remaining, return 'Nothing'. Also returns whether the +-- decision was added conservatively, and the sleep set at the point +-- where divergence happens. +-- +-- A schedule prefix is a possibly empty sequence of decisions that +-- have already been made, terminated by a single decision from the +-- to-do set. The intent is to put the system into a new state when +-- executed with this initial sequence of scheduling decisions. +findSchedulePrefix + :: DPOR + -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction) +findSchedulePrefix dpor = case dporNext dpor of + Just (tid, child) -> go tid child <|> here + Nothing -> here + where + go tid child = (\(ts,c,slp) -> (tid:ts,c,slp)) <$> findSchedulePrefix child + + -- Prefix traces terminating with a to-do decision at this point. + here = + let todos = [([t], c, sleeps) | (t, c) <- M.toList $ dporTodo dpor] + (best, worst) = partition (\([t],_,_) -> t >= initialThread) todos + in listToMaybe best <|> listToMaybe worst + + -- The new sleep set is the union of the sleep set of the node + -- we're branching from, plus all the decisions we've already + -- explored. + sleeps = dporSleep dpor `M.union` dporTaken dpor + +-- | Add a new trace to the stack. This won't work if to-dos aren't explored depth-first. +incorporateTrace + :: Bool + -- ^ Whether the \"to-do\" point which was used to create this new + -- execution was conservative or not. + -> Trace + -- ^ The execution trace: the decision made, the runnable threads, + -- and the action performed. + -> DPOR + -> DPOR +incorporateTrace conservative trace dpor0 = grow initialDepState (initialDPORThread dpor0) trace dpor0 where + grow state tid trc@((d, _, a):rest) dpor = + let tid' = tidOf tid d + state' = updateDepState state tid' a + in case dporNext dpor of + Just (t, child) + | t == tid' -> dpor { dporNext = Just (tid', grow state' tid' rest child) } + | hasTodos child -> fatal "incorporateTrace" "replacing child with todos!" + _ -> + let taken = M.insert tid' a (dporTaken dpor) + sleep = dporSleep dpor `M.union` dporTaken dpor + in dpor { dporTaken = if conservative then dporTaken dpor else taken + , dporTodo = M.delete tid' (dporTodo dpor) + , dporNext = Just (tid', subtree state' tid' sleep trc) + , dporDone = S.insert tid' (dporDone dpor) + } + grow _ _ [] _ = fatal "incorporateTrace" "trace exhausted without reading a to-do point!" + + -- check if there are to-do points in a tree + hasTodos dpor = not (M.null (dporTodo dpor)) || (case dporNext dpor of Just (_, dpor') -> hasTodos dpor'; _ -> False) + + -- 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 state' tid a t a') sleep + in DPOR + { dporRunnable = S.fromList $ case rest of + ((_, runnable, _):_) -> map fst runnable + [] -> [] + , dporTodo = M.empty + , dporNext = case rest of + ((d', _, _):_) -> + let tid' = tidOf tid d' + in Just (tid', subtree state' tid' sleep' rest) + [] -> Nothing + , dporDone = case rest of + ((d', _, _):_) -> S.singleton (tidOf tid d') + [] -> S.empty + , dporSleep = sleep' + , dporTaken = case rest of + ((d', _, a'):_) -> M.singleton (tidOf tid d') a' + [] -> M.empty + } + subtree _ _ _ [] = fatal "incorporateTrace" "subtree suffix empty!" + +-- | Produce a list of new backtracking points from an execution +-- trace. These are then used to inform new \"to-do\" points in the +-- @DPOR@ tree. +-- +-- Two traces are passed in to this function: the first is generated +-- from the special DPOR scheduler, the other from the execution of +-- the concurrent program. +-- +-- If the trace ends with any threads other than the initial one still +-- runnable, a dependency is imposed between this final action and +-- everything else. +findBacktrackSteps + :: BacktrackFunc + -- ^ Backtracking function. Given a list of backtracking points, and + -- a thread to backtrack to at a specific point in that list, add + -- the new backtracking points. There will be at least one: this + -- chosen one, but the function may add others. + -> Bool + -- ^ Whether the computation was aborted due to no decisions being + -- in-bounds. + -> Seq ([(ThreadId, Lookahead)], [ThreadId]) + -- ^ A sequence of threads at each step: the list of runnable + -- in-bound threads (with lookahead values), and the list of threads + -- still to try. The reason for the two separate lists is because + -- the threads chosen to try will be dependent on the specific + -- domain. + -> Trace + -- ^ The execution trace. + -> [BacktrackStep] +findBacktrackSteps backtrack boundKill = go initialDepState S.empty initialThread [] . F.toList where + -- Walk through the traces one step at a time, building up a list of + -- new backtracking points. + go state allThreads tid bs ((e,i):is) ((d,_,a):ts) = + let tid' = tidOf tid d + state' = updateDepState state tid' a + this = BacktrackStep + { bcktThreadid = tid' + , bcktDecision = d + , bcktAction = a + , bcktRunnable = M.fromList e + , bcktBacktracks = M.fromList $ map (\i' -> (i', False)) i + , bcktState = state + } + bs' = doBacktrack killsEarly allThreads' e (bs++[this]) + runnable = S.fromList (M.keys $ bcktRunnable this) + allThreads' = allThreads `S.union` runnable + killsEarly = null ts && boundKill + in go state' allThreads' tid' bs' is ts + go _ _ _ bs _ _ = bs + + -- Find the prior actions dependent with this one and add + -- backtracking points. + doBacktrack killsEarly allThreads enabledThreads bs = + let tagged = reverse $ zip [0..] bs + idxs = [ (ehead "doBacktrack.idxs" is, False, u) + | (u, n) <- enabledThreads + , v <- S.toList allThreads + , u /= v + , let is = idxs' u n v tagged + , not $ null is] + + idxs' u n v = go' True where + {-# INLINE go' #-} + go' final ((i,b):rest) + -- Don't cross subconcurrency boundaries + | isSubC final b = [] + -- If this is the final action in the trace and the + -- execution was killed due to nothing being within bounds + -- (@killsEarly == True@) assume worst-case dependency. + | bcktThreadid b == v && (killsEarly || isDependent b) = i : go' False rest + | otherwise = go' False rest + go' _ [] = [] + + {-# INLINE isSubC #-} + isSubC final b = case bcktAction b of + Stop -> not final && bcktThreadid b == initialThread + Subconcurrency -> bcktThreadid b == initialThread + _ -> False + + {-# INLINE isDependent #-} + isDependent b + -- Don't impose a dependency if the other thread will + -- immediately block already. This is safe because a + -- context switch will occur anyway so there's no point + -- pre-empting the action UNLESS the pre-emption would + -- possibly allow for a different relaxed memory stage. + | isBlock (bcktAction b) && isBarrier (simplifyLookahead n) = False + | otherwise = dependent' (bcktState b) (bcktThreadid b) (bcktAction b) u n + in backtrack bs idxs + +-- | Add new backtracking points, if they have not already been +-- visited and aren't in the sleep set. +incorporateBacktrackSteps :: [BacktrackStep] -> DPOR -> DPOR +incorporateBacktrackSteps (b:bs) dpor = dpor' where + tid = bcktThreadid b + + dpor' = dpor + { dporTodo = dporTodo dpor `M.union` M.fromList todo + , dporNext = Just (tid, child) + } + + todo = + [ x + | x@(t,c) <- M.toList $ bcktBacktracks b + , Just t /= (fst <$> dporNext dpor) + , S.notMember t (dporDone dpor) + , c || M.notMember t (dporSleep dpor) + ] + + child = case dporNext dpor of + Just (t, d) + | t /= tid -> fatal "incorporateBacktrackSteps" "incorporating wrong trace!" + | otherwise -> incorporateBacktrackSteps bs d + Nothing -> fatal "incorporateBacktrackSteps" "child is missing!" +incorporateBacktrackSteps [] dpor = dpor + +------------------------------------------------------------------------------- +-- * DPOR scheduler + +-- | The scheduler state +data DPORSchedState k = DPORSchedState + { schedSleep :: Map ThreadId ThreadAction + -- ^ The sleep set: decisions not to make until something dependent + -- with them happens. + , schedPrefix :: [ThreadId] + -- ^ Decisions still to make + , schedBPoints :: Seq ([(ThreadId, Lookahead)], [ThreadId]) + -- ^ Which threads are runnable and in-bound at each step, and the + -- alternative decisions still to make. + , schedIgnore :: Bool + -- ^ Whether to ignore this execution or not: @True@ if the + -- execution is aborted due to all possible decisions being in the + -- sleep set, as then everything in this execution is covered by + -- another. + , schedBoundKill :: Bool + -- ^ Whether the execution was terminated due to all decisions being + -- out of bounds. + , schedDepState :: DepState + -- ^ State used by the dependency function to determine when to + -- remove decisions from the sleep set. + , schedBState :: Maybe k + -- ^ State used by the incremental bounding function. + } deriving (Eq, Show) + +instance NFData k => NFData (DPORSchedState k) where + rnf s = rnf ( schedSleep s + , schedPrefix s + , schedBPoints s + , schedIgnore s + , schedBoundKill s + , schedDepState s + , schedBState s + ) + +-- | Initial DPOR scheduler state for a given prefix +initialDPORSchedState :: Map ThreadId ThreadAction + -- ^ The initial sleep set. + -> [ThreadId] + -- ^ The schedule prefix. + -> DPORSchedState k +initialDPORSchedState sleep prefix = DPORSchedState + { schedSleep = sleep + , schedPrefix = prefix + , schedBPoints = Sq.empty + , schedIgnore = False + , schedBoundKill = False + , schedDepState = initialDepState + , schedBState = Nothing + } + +-- | An incremental bounding function is a stateful function that +-- takes the last and next decisions, and returns a new state only if +-- the next decision is within the bound. +type IncrementalBoundFunc k + = Maybe k -> Maybe (ThreadId, ThreadAction) -> (Decision, Lookahead) -> Maybe k + +-- | A backtracking step is a point in the execution where another +-- decision needs to be made, in order to explore interesting new +-- schedules. A backtracking /function/ takes the steps identified so +-- far and a list of points and thread at that point to backtrack +-- to. More points be added to compensate for the effects of the +-- bounding function. For example, under pre-emption bounding a +-- conservative backtracking point is added at the prior context +-- switch. The bool is whether the point is conservative. Conservative +-- points are always explored, whereas non-conservative ones might be +-- skipped based on future information. +-- +-- In general, a backtracking function should identify one or more +-- backtracking points, and then use @backtrackAt@ to do the actual +-- work. +type BacktrackFunc + = [BacktrackStep] -> [(Int, Bool, ThreadId)] -> [BacktrackStep] + +-- | Add a backtracking point. If the thread isn't runnable, add all +-- runnable threads. If the backtracking point is already present, +-- don't re-add it UNLESS this would make it conservative. +backtrackAt + :: (ThreadId -> BacktrackStep -> Bool) + -- ^ If this returns @True@, backtrack to all runnable threads, + -- rather than just the given thread. + -> BacktrackFunc +backtrackAt toAll bs0 = backtrackAt' . nubBy ((==) `on` fst') . sortOn fst' where + fst' (x,_,_) = x + + backtrackAt' ((i,c,t):is) = go i bs0 i c t is + backtrackAt' [] = bs0 + + go i0 (b:bs) 0 c tid is + -- If the backtracking point is already present, don't re-add it, + -- UNLESS this would force it to backtrack (it's conservative) + -- where before it might not. + | not (toAll tid b) && tid `M.member` bcktRunnable b = + let val = M.lookup tid $ bcktBacktracks b + b' = if isNothing val || (val == Just False && c) + then b { bcktBacktracks = backtrackTo tid c b } + else b + in b' : case is of + ((i',c',t'):is') -> go i' bs (i'-i0-1) c' t' is' + [] -> bs + -- Otherwise just backtrack to everything runnable. + | otherwise = + let b' = b { bcktBacktracks = backtrackAll c b } + in b' : case is of + ((i',c',t'):is') -> go i' bs (i'-i0-1) c' t' is' + [] -> bs + go i0 (b:bs) i c tid is = b : go i0 bs (i-1) c tid is + go _ [] _ _ _ _ = fatal "backtrackAt" "ran out of schedule whilst backtracking!" + + -- Backtrack to a single thread + backtrackTo tid c = M.insert tid c . bcktBacktracks + + -- Backtrack to all runnable threads + backtrackAll c = M.map (const c) . bcktRunnable + +-- | DPOR scheduler: takes a list of decisions, and maintains a trace +-- including the runnable threads, and the alternative choices allowed +-- by the bound-specific initialise function. +-- +-- After the initial decisions are exhausted, this prefers choosing +-- the prior thread if it's (1) still runnable and (2) hasn't just +-- yielded. Furthermore, threads which /will/ yield are ignored in +-- preference of those which will not. +dporSched + :: IncrementalBoundFunc k + -- ^ Bound function: returns true if that schedule prefix terminated + -- with the lookahead decision fits within the bound. + -> Scheduler (DPORSchedState k) +dporSched boundf = Scheduler $ \prior threads s -> + let + -- The next scheduler state + nextState rest = s + { schedBPoints = schedBPoints s |> (restrictToBound fst threads', rest) + , schedDepState = nextDepState + } + nextDepState = let ds = schedDepState s in maybe ds (uncurry $ updateDepState ds) prior + + -- Pick a new thread to run, not considering bounds. Choose the + -- current thread if available and it hasn't just yielded, + -- otherwise add all runnable threads. + initialise = tryDaemons . yieldsToEnd $ case prior of + Just (tid, act) + | not (didYield act) && tid `elem` tids && isInBound tid -> [tid] + _ -> tids + + -- If one of the chosen actions will kill the computation, and + -- there are daemon threads, try them instead. + -- + -- This is necessary if the killing action is NOT dependent with + -- every other action, according to the dependency function. This + -- is, strictly speaking, wrong; an action that kills another + -- thread is definitely dependent with everything in that + -- thread. HOWEVER, implementing it that way leads to an explosion + -- of schedules tried. Really, all that needs to happen is for the + -- thread-that-would-be-killed to be executed fully ONCE, and then + -- the normal dependency mechanism will identify any other + -- backtracking points that should be tried. This is achieved by + -- adding every thread that would be killed to the to-do list. + -- Furthermore, these threads MUST be ahead of the killing thread, + -- or the killing thread will end up in the sleep set and so the + -- killing action not performed. This is, again, because of the + -- lack of the dependency messing things up in the name of + -- performance. + -- + -- See commits a056f54 and 8554ce9, and my 4th June comment in + -- issue #52. + tryDaemons ts + | any doesKill ts = case partition doesKill tids of + (kills, nokills) -> nokills ++ kills + | otherwise = ts + doesKill t = killsDaemons t (action t) + + -- Restrict the possible decisions to those in the bound. + restrictToBound f = filter (isInBound . f) + isInBound t = isJust $ boundf (schedBState s) prior (decision t, action t) + + -- Move the threads which will immediately yield to the end of the list + yieldsToEnd ts = case partition (willYield . action) ts of + (yields, noyields) -> noyields ++ yields + + -- Get the decision that will lead to a thread being scheduled. + decision = decisionOf (fst <$> prior) (S.fromList tids) + + -- Get the action of a thread + action t = efromJust "dporSched.action" (lookup t threads') + + -- The runnable thread IDs + tids = map fst threads' + + -- The runnable threads as a normal list. + threads' = toList threads + in case schedPrefix s of + -- If there is a decision available, make it + (t:ts) -> + let bstate' = boundf (schedBState s) prior (decision t, action t) + in (Just t, (nextState []) { schedPrefix = ts, schedBState = bstate' }) + + -- Otherwise query the initialise function for a list of possible + -- choices, filter out anything in the sleep set, and make one of + -- them arbitrarily (recording the others). + [] -> + let choices = restrictToBound id initialise + checkDep t a = case prior of + Just (tid, act) -> dependent (schedDepState s) tid act t a + Nothing -> False + ssleep' = M.filterWithKey (\t a -> not $ checkDep t a) $ schedSleep s + choices' = filter (`notElem` M.keys ssleep') choices + signore' = not (null choices) && all (`elem` M.keys ssleep') choices + sbkill' = not (null initialise) && null choices + in case choices' of + (nextTid:rest) -> + let bstate' = boundf (schedBState s) prior (decision nextTid, action nextTid) + in (Just nextTid, (nextState rest) { schedSleep = ssleep', schedBState = bstate' }) + [] -> + (Nothing, (nextState []) { schedIgnore = signore', schedBoundKill = sbkill', schedBState = Nothing }) + +------------------------------------------------------------------------------- +-- * Dependency function + +-- | Check if an action is dependent on another. +-- +-- This is basically the same as 'dependent'', but can make use of the +-- additional information in a 'ThreadAction' to make better decisions +-- in a few cases. +dependent :: DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool +dependent ds t1 a1 t2 a2 = case (a1, a2) of + -- @SetNumCapabilities@ and @GetNumCapabilities@ are NOT dependent + -- IF the value read is the same as the value written. 'dependent'' + -- can not see the value read (as it hasn't happened yet!), and so + -- is more pessimistic here. + (SetNumCapabilities a, GetNumCapabilities b) | a == b -> False + (GetNumCapabilities a, SetNumCapabilities b) | a == b -> False + + -- When masked interruptible, a thread can only be interrupted when + -- actually blocked. 'dependent'' has to assume that all + -- potentially-blocking operations can block, and so is more + -- pessimistic in this case. + (ThrowTo t, _) | t == t2 -> canInterrupt ds t2 a2 && a2 /= Stop + (_, ThrowTo t) | t == t1 -> canInterrupt ds t1 a1 && a1 /= Stop + + -- Dependency of STM transactions can be /greatly/ improved here, as + -- the 'Lookahead' does not know which @TVar@s will be touched, and + -- so has to assume all transactions are dependent. + (STM _ _, STM _ _) -> checkSTM + (STM _ _, BlockedSTM _) -> checkSTM + (BlockedSTM _, STM _ _) -> checkSTM + (BlockedSTM _, BlockedSTM _) -> checkSTM + + _ -> case (,) <$> rewind a1 <*> rewind a2 of + Just (l1, l2) -> dependent' ds t1 a1 t2 l2 && dependent' ds t2 a2 t1 l1 + _ -> dependentActions ds (simplifyAction a1) (simplifyAction a2) + + where + -- STM actions A and B are dependent if A wrote to anything B + -- touched, or vice versa. + checkSTM = checkSTM' a1 a2 || checkSTM' a2 a1 + checkSTM' a b = not . S.null $ tvarsWritten a `S.intersection` tvarsOf b + +-- | Variant of 'dependent' to handle 'Lookahead'. +-- +-- Termination of the initial thread is handled specially in the DPOR +-- implementation. +dependent' :: DepState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool +dependent' ds t1 a1 t2 l2 = case (a1, l2) of + -- Worst-case assumption: all IO is dependent. + (LiftIO, WillLiftIO) -> True + + -- Throwing an exception is only dependent with actions in that + -- thread and if the actions can be interrupted. We can also + -- slightly improve on that by not considering interrupting the + -- normal termination of a thread: it doesn't make a difference. + (ThrowTo t, WillStop) | t == t2 -> False + (Stop, WillThrowTo t) | t == t1 -> False + (ThrowTo t, _) | t == t2 -> canInterruptL ds t2 l2 + (_, WillThrowTo t) | t == t1 -> canInterrupt ds t1 a1 + + -- Another worst-case: assume all STM is dependent. + (STM _ _, WillSTM) -> True + + -- This is a bit pessimistic: Set/Get are only dependent if the + -- value set is not the same as the value that will be got, but we + -- can't know that here. 'dependent' optimises this case. + (GetNumCapabilities a, WillSetNumCapabilities b) -> a /= b + (SetNumCapabilities _, WillGetNumCapabilities) -> True + (SetNumCapabilities a, WillSetNumCapabilities b) -> a /= b + + _ -> dependentActions ds (simplifyAction a1) (simplifyLookahead l2) + +-- | Check if two 'ActionType's are dependent. Note that this is not +-- sufficient to know if two 'ThreadAction's are dependent, without +-- being so great an over-approximation as to be useless! +dependentActions :: DepState -> ActionType -> ActionType -> Bool +dependentActions ds a1 a2 = case (a1, a2) of + -- Unsynchronised reads and writes are always dependent, even under + -- a relaxed memory model, as an unsynchronised write gives rise to + -- a commit, which synchronises. + (UnsynchronisedRead r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> a2 /= UnsynchronisedRead r1 + (UnsynchronisedWrite r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True + (PartiallySynchronisedWrite r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True + (PartiallySynchronisedModify r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True + (SynchronisedModify r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True + + -- Unsynchronised writes and synchronisation where the buffer is not + -- empty. + -- + -- See [RMMVerification], lemma 5.25. + (UnsynchronisedWrite r1, PartiallySynchronisedCommit _) | same crefOf && isBuffered ds r1 -> False + (PartiallySynchronisedCommit _, UnsynchronisedWrite r2) | same crefOf && isBuffered ds r2 -> False + + -- Unsynchronised reads where a memory barrier would flush a + -- buffered write + (UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered ds r1 + (_, UnsynchronisedRead r2) | isBarrier a1 -> isBuffered ds r2 + + -- Commits and memory barriers must be dependent, as memory barriers + -- (currently) flush in a consistent order. Alternative orders need + -- to be explored as well. Perhaps a better implementation of + -- memory barriers would just block every non-commit thread while + -- any buffer is nonempty. + (PartiallySynchronisedCommit _, _) | isBarrier a2 -> True + (_, PartiallySynchronisedCommit _) | isBarrier a1 -> True + + -- Two @MVar@ puts are dependent if they're to the same empty + -- @MVar@, and two takes are dependent if they're to the same full + -- @MVar@. + (SynchronisedWrite v1, SynchronisedWrite v2) -> v1 == v2 && not (isFull ds v1) + (SynchronisedRead v1, SynchronisedRead v2) -> v1 == v2 && isFull ds v1 + + (_, _) -> case getSame crefOf of + -- Two actions on the same CRef where at least one is synchronised + Just r -> synchronises a1 r || synchronises a2 r + -- Two actions on the same MVar + _ -> same mvarOf + + where + same :: Eq a => (ActionType -> Maybe a) -> Bool + same = isJust . getSame + + getSame :: Eq a => (ActionType -> Maybe a) -> Maybe a + getSame f = + let f1 = f a1 + f2 = f a2 + in if f1 == f2 then f1 else Nothing + +------------------------------------------------------------------------------- +-- ** Dependency function state + +data DepState = DepState + { depCRState :: Map CRefId Bool + -- ^ Keep track of which @CRef@s have buffered writes. + , depMVState :: Set MVarId + -- ^ Keep track of which @MVar@s are full. + , depMaskState :: Map ThreadId MaskingState + -- ^ Keep track of thread masking states. If a thread isn't present, + -- the masking state is assumed to be @Unmasked@. This nicely + -- provides compatibility with dpor-0.1, where the thread IDs are + -- not available. + } deriving (Eq, Show) + +instance NFData DepState where + rnf depstate = rnf ( depCRState depstate + , depMVState depstate + , [(t, m `seq` ()) | (t, m) <- M.toList (depMaskState depstate)] + ) + +-- | Initial dependency state. +initialDepState :: DepState +initialDepState = DepState M.empty S.empty M.empty + +-- | Update the dependency state with the action that has just +-- happened. +updateDepState :: DepState -> ThreadId -> ThreadAction -> DepState +updateDepState depstate tid act = DepState + { depCRState = updateCRState act $ depCRState depstate + , depMVState = updateMVState act $ depMVState depstate + , depMaskState = updateMaskState tid act $ depMaskState depstate + } + +-- | Update the @CRef@ buffer state with the action that has just +-- happened. +updateCRState :: ThreadAction -> Map CRefId Bool -> Map CRefId Bool +updateCRState (CommitCRef _ r) = M.delete r +updateCRState (WriteCRef r) = M.insert r True +updateCRState ta + | isBarrier $ simplifyAction ta = const M.empty + | otherwise = id + +-- | Update the @MVar@ full/empty state with the action that has just +-- happened. +updateMVState :: ThreadAction -> Set MVarId -> Set MVarId +updateMVState (PutMVar mvid _) = S.insert mvid +updateMVState (TryPutMVar mvid True _) = S.insert mvid +updateMVState (TakeMVar mvid _) = S.delete mvid +updateMVState (TryTakeMVar mvid True _) = S.delete mvid +updateMVState _ = id + +-- | Update the thread masking state with the action that has just +-- happened. +updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState +updateMaskState tid (Fork tid2) = \masks -> case M.lookup tid masks of + -- A thread inherits the masking state of its parent. + Just ms -> M.insert tid2 ms masks + Nothing -> masks +updateMaskState tid (SetMasking _ ms) = M.insert tid ms +updateMaskState tid (ResetMasking _ ms) = M.insert tid ms +updateMaskState _ _ = id + +-- | Check if a @CRef@ has a buffered write pending. +isBuffered :: DepState -> CRefId -> Bool +isBuffered depstate r = M.findWithDefault False r (depCRState depstate) + +-- | Check if an @MVar@ is full. +isFull :: DepState -> MVarId -> Bool +isFull depstate v = S.member v (depMVState depstate) + +-- | Check if an exception can interrupt a thread (action). +canInterrupt :: DepState -> ThreadId -> ThreadAction -> Bool +canInterrupt depstate tid act + -- If masked interruptible, blocked actions can be interrupted. + | isMaskedInterruptible depstate tid = case act of + BlockedPutMVar _ -> True + BlockedReadMVar _ -> True + BlockedTakeMVar _ -> True + BlockedSTM _ -> True + BlockedThrowTo _ -> True + _ -> False + -- If masked uninterruptible, nothing can be. + | isMaskedUninterruptible depstate tid = False + -- If no mask, anything can be. + | otherwise = True + +-- | Check if an exception can interrupt a thread (lookahead). +canInterruptL :: DepState -> ThreadId -> Lookahead -> Bool +canInterruptL depstate tid lh + -- If masked interruptible, actions which can block may be + -- interrupted. + | isMaskedInterruptible depstate tid = case lh of + WillPutMVar _ -> True + WillReadMVar _ -> True + WillTakeMVar _ -> True + WillSTM -> True + WillThrowTo _ -> True + _ -> False + -- If masked uninterruptible, nothing can be. + | isMaskedUninterruptible depstate tid = False + -- If no mask, anything can be. + | otherwise = True + +-- | Check if a thread is masked interruptible. +isMaskedInterruptible :: DepState -> ThreadId -> Bool +isMaskedInterruptible depstate tid = + M.lookup tid (depMaskState depstate) == Just MaskedInterruptible + +-- | Check if a thread is masked uninterruptible. +isMaskedUninterruptible :: DepState -> ThreadId -> Bool +isMaskedUninterruptible depstate tid = + M.lookup tid (depMaskState depstate) == Just MaskedUninterruptible + +------------------------------------------------------------------------------- +-- * Utilities + +-- The initial thread of a DPOR tree. +initialDPORThread :: DPOR -> ThreadId +initialDPORThread = S.elemAt 0 . dporRunnable + +-- | Check if a thread yielded. +didYield :: ThreadAction -> Bool +didYield Yield = True +didYield (ThreadDelay _) = True +didYield _ = False + +-- | Check if a thread will yield. +willYield :: Lookahead -> Bool +willYield WillYield = True +willYield (WillThreadDelay _) = True +willYield _ = False + +-- | Check if an action will kill daemon threads. +killsDaemons :: ThreadId -> Lookahead -> Bool +killsDaemons t WillStop = t == initialThread +killsDaemons _ _ = False diff --git a/Test/DejaFu/SCT/Internal/Weighted.hs b/Test/DejaFu/SCT/Internal/Weighted.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/SCT/Internal/Weighted.hs @@ -0,0 +1,66 @@ +-- | +-- Module : Test.DejaFu.SCT.Internal.Weighted +-- Copyright : (c) 2015--2017 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : portable +-- +-- Internal types and functions for SCT via weighted random +-- scheduling. This module is NOT considered to form part of the +-- public interface of this library. +module Test.DejaFu.SCT.Internal.Weighted where + +import Control.DeepSeq (NFData(..)) +import Data.List.NonEmpty (toList) +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as M +import Data.Maybe (fromMaybe) +import System.Random (RandomGen, randomR) + +import Test.DejaFu.Schedule (Scheduler(..)) +import Test.DejaFu.Types + +------------------------------------------------------------------------------- +-- * Weighted random scheduler + +-- | The scheduler state +data RandSchedState g = RandSchedState + { schedWeights :: Map ThreadId Int + -- ^ The thread weights: used in determining which to run. + , schedGen :: g + -- ^ The random number generator. + } deriving (Eq, Show) + +instance NFData g => NFData (RandSchedState g) where + rnf s = rnf ( schedWeights s + , schedGen s + ) + +-- | Initial weighted random scheduler state. +initialRandSchedState :: Maybe (Map ThreadId Int) -> g -> RandSchedState g +initialRandSchedState = RandSchedState . fromMaybe M.empty + +-- | Weighted random scheduler: assigns to each new thread a weight, +-- and makes a weighted random choice out of the runnable threads at +-- every step. +randSched :: RandomGen g => (g -> (Int, g)) -> Scheduler (RandSchedState g) +randSched weightf = Scheduler $ \_ threads s -> + let + -- Select a thread + pick idx ((x, f):xs) + | idx < f = Just x + | otherwise = pick (idx - f) xs + pick _ [] = Nothing + (choice, g'') = randomR (0, sum (map snd enabled) - 1) g' + enabled = M.toList $ M.filterWithKey (\tid _ -> tid `elem` tids) weights' + + -- The weights, with any new threads added. + (weights', g') = foldr assignWeight (M.empty, schedGen s) tids + assignWeight tid ~(ws, g0) = + let (w, g) = maybe (weightf g0) (\w0 -> (w0, g0)) (M.lookup tid (schedWeights s)) + in (M.insert tid w ws, g) + + -- The runnable threads. + tids = map fst (toList threads) + in (pick choice enabled, RandSchedState weights' g'') diff --git a/Test/DejaFu/STM.hs b/Test/DejaFu/STM.hs deleted file mode 100644 --- a/Test/DejaFu/STM.hs +++ /dev/null @@ -1,122 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE TypeFamilies #-} - --- | --- Module : Test.DejaFu.STM --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- Stability : experimental --- Portability : CPP, GeneralizedNewtypeDeriving, RankNTypes, TypeFamilies --- --- A 'MonadSTM' implementation, which can be run on top of 'IO' or --- 'ST'. -module Test.DejaFu.STM - ( -- * The @STMLike@ Monad - STMLike - , STMST - , STMIO - - -- * Executing Transactions - , Result(..) - , TTrace - , TAction(..) - , TVarId - , runTransaction - ) where - -import Control.Applicative (Alternative(..)) -import Control.Monad (MonadPlus(..), unless) -import Control.Monad.Catch (MonadCatch(..), MonadThrow(..)) -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 - -#if MIN_VERSION_base(4,9,0) -import qualified Control.Monad.Fail as Fail -#endif - --- | @since 0.3.0.0 -newtype STMLike n r a = S { runSTM :: M n r a } deriving (Functor, Applicative, Monad) - -#if MIN_VERSION_base(4,9,0) --- | @since 0.9.1.0 -instance Fail.MonadFail (STMLike r n) where - fail = S . fail -#endif - --- | Create a new STM continuation. -toSTM :: ((a -> STMAction n r) -> STMAction n r) -> STMLike n r a -toSTM = S . cont - --- | A 'MonadSTM' implementation using @ST@, it encapsulates a single --- atomic transaction. The environment, that is, the collection of --- defined 'TVar's is implicit, there is no list of them, they exist --- 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 --- atomic transaction. The environment, that is, the collection of --- defined 'TVar's is implicit, there is no list of them, they exist --- 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 - throwM = toSTM . const . SThrow - -instance MonadCatch (STMLike n r) where - catch (S stm) handler = toSTM (SCatch (runSTM . handler) stm) - --- | @since 0.7.2.0 -instance Alternative (STMLike n r) where - S a <|> S b = toSTM (SOrElse a b) - empty = toSTM (const SRetry) - --- | @since 0.7.2.0 -instance MonadPlus (STMLike n r) - -instance C.MonadSTM (STMLike n r) where - type TVar (STMLike n r) = TVar r - -#if MIN_VERSION_concurrency(1,2,0) - -- retry and orElse are top-level definitions in - -- Control.Monad.STM.Class in 1.2 and up -#else - retry = empty - orElse = (<|>) -#endif - - newTVarN n = toSTM . SNew n - - readTVar = toSTM . SRead - - writeTVar tvar a = toSTM (\c -> SWrite tvar a (c ())) - --- | 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 - (res, undo, tvid', trace) <- doTransaction (runSTM ma) tvid - - unless (isSTMSuccess res) undo - - pure (res, tvid', trace) diff --git a/Test/DejaFu/STM/Internal.hs b/Test/DejaFu/STM/Internal.hs deleted file mode 100644 --- a/Test/DejaFu/STM/Internal.hs +++ /dev/null @@ -1,225 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE RankNTypes #-} - --- | --- Module : Test.DejaFu.STM.Internal --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- Stability : experimental --- Portability : CPP, ExistentialQuantification, MultiParamTypeClasses, RankNTypes --- --- 'MonadSTM' testing implementation, internal types and --- definitions. This module is NOT considered to form part of the --- 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.Ref (MonadRef, newRef, readRef, writeRef) -import Data.List (nub) - -import Test.DejaFu.Common - -#if MIN_VERSION_base(4,9,0) -import qualified Control.Monad.Fail as Fail -#endif - --------------------------------------------------------------------------------- --- The @STMLike@ monad - --- | The underlying monad is based on continuations over primitive --- actions. --- --- This is not @Cont@ because we want to give it a custom @MonadFail@ --- instance. -newtype M n r a = M { runM :: (a -> STMAction n r) -> STMAction n r } - -instance Functor (M n r) where - fmap f m = M $ \ c -> runM m (c . f) - -instance Applicative (M n r) where - pure x = M $ \c -> c x - f <*> v = M $ \c -> runM f (\g -> runM v (c . g)) - -instance Monad (M n r) where - return = pure - m >>= k = M $ \c -> runM m (\x -> runM (k x) c) - -#if MIN_VERSION_base(4,9,0) - fail = Fail.fail - --- | @since 0.7.1.2 -instance Fail.MonadFail (M n r) where -#endif - fail e = cont (\_ -> SThrow (MonadFailException e)) - --- | Construct a continuation-passing operation from a function. -cont :: ((a -> STMAction n r) -> STMAction n r) -> M n r a -cont = M - --- | Run a CPS computation with the given final computation. -runCont :: M n r a -> (a -> STMAction n r) -> STMAction n r -runCont = runM - --------------------------------------------------------------------------------- --- * Primitive actions - --- | STM transactions are represented as a sequence of primitive --- actions. -data STMAction n r - = forall a e. Exception e => SCatch (e -> M n r a) (M n r a) (a -> STMAction n r) - | forall a. SRead (TVar r a) (a -> STMAction n r) - | forall a. SWrite (TVar r a) a (STMAction n r) - | forall a. SOrElse (M n r a) (M n r a) (a -> STMAction n r) - | forall a. SNew String a (TVar r a -> STMAction n r) - | forall e. Exception e => SThrow e - | SRetry - | SStop (n ()) - --------------------------------------------------------------------------------- --- * @TVar@s - --- | A 'TVar' is a tuple of a unique ID and the value contained. The --- ID is so that blocked transactions can be re-run when a 'TVar' they --- depend on has changed. -newtype TVar r a = TVar (TVarId, r a) - --------------------------------------------------------------------------------- --- * Output - --- | 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 - -- 'TVar's and writing to the second. - | Retry [TVarId] - -- ^ The transaction aborted by calling 'retry', and read the - -- returned 'TVar's. It should be retried when at least one of the - -- 'TVar's has been mutated. - | Exception SomeException - -- ^ The transaction aborted by throwing an exception. - 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 - rnf (Exception e) = e `seq` () - --- | Check if a 'Result' is a @Success@. -isSTMSuccess :: Result a -> Bool -isSTMSuccess (Success _ _ _) = True -isSTMSuccess _ = False - -instance Functor Result where - fmap f (Success rs ws a) = Success rs ws $ f a - fmap _ (Retry rs) = Retry rs - fmap _ (Exception e) = Exception e - -instance Foldable Result where - foldMap f (Success _ _ a) = f a - foldMap _ _ = mempty - --------------------------------------------------------------------------------- --- * Execution - --- | Run a STM transaction, returning an action to undo its effects. -doTransaction :: MonadRef r n => M n r a -> IdSource -> n (Result a, n (), IdSource, TTrace) -doTransaction ma idsource = do - (c, ref) <- runRefCont SStop (Just . Right) (runCont ma) - (idsource', undo, readen, written, trace) <- go ref c (pure ()) idsource [] [] [] - res <- readRef ref - - case res of - Just (Right val) -> pure (Success (nub readen) (nub written) val, undo, 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 - (act', undo', nidsrc', readen', written', tact) <- stepTrans act nidsrc - - let newIDSource = nidsrc' - newAct = act' - newUndo = undo' >> undo - newReaden = readen' ++ readen - newWritten = written' ++ written - newSofar = tact : sofar - - case tact of - 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. -stepTrans :: MonadRef r n => STMAction n r -> IdSource -> n (STMAction n r, n (), IdSource, [TVarId], [TVarId], TAction) -stepTrans act idsource = case act of - SCatch h stm c -> stepCatch h stm c - SRead ref c -> stepRead ref c - SWrite ref a c -> stepWrite ref a c - SNew n a c -> stepNew n a c - SOrElse a b c -> stepOrElse a b c - SStop na -> stepStop na - - SThrow e -> pure (SThrow e, nothing, idsource, [], [], TThrow) - SRetry -> pure (SRetry, nothing, idsource, [], [], TRetry) - - where - nothing = pure () - - stepCatch h stm c = cases TCatch stm c - (\trace -> pure (SRetry, nothing, idsource, [], [], TCatch trace Nothing)) - (\trace exc -> case fromException exc of - Just exc' -> transaction (TCatch trace . Just) (h exc') c - Nothing -> pure (SThrow exc, nothing, idsource, [], [], TCatch trace Nothing)) - - stepRead (TVar (tvid, ref)) c = do - val <- readRef ref - pure (c val, nothing, idsource, [tvid], [], TRead tvid) - - stepWrite (TVar (tvid, ref)) a c = do - old <- readRef ref - writeRef ref a - 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) - pure (c tvar, nothing, idsource', [], [tvid], TNew tvid) - - stepOrElse a b c = cases TOrElse a c - (\trace -> transaction (TOrElse trace . Just) b c) - (\trace exc -> pure (SThrow exc, nothing, idsource, [], [], TOrElse trace Nothing)) - - stepStop na = do - na - 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 -> 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 -> 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 @@ -1,6 +1,6 @@ -- | -- Module : Test.DejaFu.Schedule --- Copyright : (c) 2016 Michael Walker +-- Copyright : (c) 2016--2017 Michael Walker -- License : MIT -- Maintainer : Michael Walker -- Stability : experimental @@ -11,12 +11,6 @@ ( -- * Scheduling Scheduler(..) - , Decision(..) - , tidOf - , decisionOf - - , NonEmpty(..) - -- ** Preemptive , randomSched , roundRobinSched @@ -29,10 +23,11 @@ , 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.Internal +import Test.DejaFu.Types -- | A @Scheduler@ drives the execution of a concurrent program. The -- parameters it takes are: @@ -40,7 +35,7 @@ -- 1. The last thread executed (if this is the first invocation, this -- is @Nothing@). -- --- 2. The runnable threads at this point. +-- 2. The unblocked threads. -- -- 3. The state. -- @@ -57,36 +52,6 @@ } ------------------------------------------------------------------------------- --- Scheduling decisions - --- | 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 -tidOf tid _ = tid - --- | 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. - -> f ThreadId - -- ^ The runnable threads. - -> ThreadId - -- ^ The current thread. - -> Decision -decisionOf Nothing _ chosen = Start chosen -decisionOf (Just prior) runnable chosen - | prior == chosen = Continue - | prior `elem` runnable = SwitchTo chosen - | otherwise = Start chosen - -------------------------------------------------------------------------------- -- Preemptive -- | A simple random scheduler which, at every step, picks a random @@ -118,16 +83,18 @@ ------------------------------------------------------------------------------- -- Non-preemptive --- | 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. +-- | A random scheduler which doesn't preempt the running thread. That +-- is, if the previously scheduled thread is not blocked, it is picked +-- again, otherwise schedule randomly. -- -- @since 0.8.0.0 randomSchedNP :: RandomGen g => Scheduler g randomSchedNP = makeNonPreemptive randomSched -- | A round-robin scheduler which doesn't preempt the running --- thread. +-- thread. That is, if the previously scheduled thread is not blocked, +-- it is picked again, otherwise schedule the thread with the next +-- 'ThreadId'. -- -- @since 0.8.0.0 roundRobinSchedNP :: Scheduler () diff --git a/Test/DejaFu/Types.hs b/Test/DejaFu/Types.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Types.hs @@ -0,0 +1,566 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +-- | +-- Module : Test.DejaFu.Types +-- Copyright : (c) 2017 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : GeneralizedNewtypeDeriving +-- +-- Common types and functions used throughout DejaFu. +module Test.DejaFu.Types where + +import Control.DeepSeq (NFData(..)) +import Control.Exception (Exception(..), MaskingState(..), + SomeException) +import Data.Function (on) + +------------------------------------------------------------------------------- +-- * Identifiers + +-- | Every thread has a unique identitifer. +-- +-- @since 1.0.0.0 +newtype ThreadId = ThreadId Id + deriving (Eq, Ord, NFData) + +instance Show ThreadId where + show (ThreadId id_) = show id_ + +-- | Every @CRef@ has a unique identifier. +-- +-- @since 1.0.0.0 +newtype CRefId = CRefId Id + deriving (Eq, Ord, NFData) + +instance Show CRefId where + show (CRefId id_) = show id_ + +-- | Every @MVar@ has a unique identifier. +-- +-- @since 1.0.0.0 +newtype MVarId = MVarId Id + deriving (Eq, Ord, NFData) + +instance Show MVarId where + show (MVarId id_) = show id_ + +-- | Every @TVar@ has a unique identifier. +-- +-- @since 1.0.0.0 +newtype TVarId = TVarId Id + deriving (Eq, Ord, NFData) + +instance Show TVarId where + show (TVarId id_) = show id_ + +-- | An identifier for a thread, @MVar@, @CRef@, or @TVar@. +-- +-- The number is the important bit. The string is to make execution +-- traces easier to read, but is meaningless. +data Id = Id (Maybe String) {-# UNPACK #-} !Int + +instance Eq Id where + (Id _ i) == (Id _ j) = i == j + +instance Ord Id where + compare (Id _ i) (Id _ j) = compare i j + +instance Show Id where + show (Id (Just n) _) = n + show (Id _ i) = show i + +instance NFData Id where + rnf (Id n i) = rnf (n, i) + +-- | The ID of the initial thread. +-- +-- @since 0.4.0.0 +initialThread :: ThreadId +initialThread = ThreadId (Id (Just "main") 0) + +------------------------------------------------------------------------------- +-- * Actions + +-- | All the actions that a thread can perform. +-- +-- @since 1.0.0.0 +data ThreadAction = + Fork ThreadId + -- ^ Start a new thread. + | ForkOS ThreadId + -- ^ Start a new bound thread. + | IsCurrentThreadBound Bool + -- ^ Check if the current thread is bound. + | MyThreadId + -- ^ Get the 'ThreadId' of the current thread. + | GetNumCapabilities Int + -- ^ Get the number of Haskell threads that can run simultaneously. + | SetNumCapabilities Int + -- ^ Set the number of Haskell threads that can run simultaneously. + | Yield + -- ^ Yield the current thread. + | ThreadDelay Int + -- ^ Yield/delay the current thread. + | NewMVar MVarId + -- ^ Create a new 'MVar'. + | PutMVar MVarId [ThreadId] + -- ^ Put into a 'MVar', possibly waking up some threads. + | BlockedPutMVar MVarId + -- ^ Get blocked on a put. + | TryPutMVar MVarId Bool [ThreadId] + -- ^ Try to put into a 'MVar', possibly waking up some threads. + | ReadMVar MVarId + -- ^ Read from a 'MVar'. + | TryReadMVar MVarId Bool + -- ^ Try to read from a 'MVar'. + | BlockedReadMVar MVarId + -- ^ Get blocked on a read. + | TakeMVar MVarId [ThreadId] + -- ^ Take from a 'MVar', possibly waking up some threads. + | BlockedTakeMVar MVarId + -- ^ Get blocked on a take. + | TryTakeMVar MVarId Bool [ThreadId] + -- ^ Try to take from a 'MVar', possibly waking up some threads. + | NewCRef CRefId + -- ^ Create a new 'CRef'. + | ReadCRef CRefId + -- ^ Read from a 'CRef'. + | ReadCRefCas CRefId + -- ^ Read from a 'CRef' for a future compare-and-swap. + | ModCRef CRefId + -- ^ Modify a 'CRef'. + | ModCRefCas CRefId + -- ^ Modify a 'CRef' using a compare-and-swap. + | WriteCRef CRefId + -- ^ Write to a 'CRef' without synchronising. + | CasCRef CRefId Bool + -- ^ Attempt to to a 'CRef' using a compare-and-swap, synchronising + -- it. + | CommitCRef ThreadId CRefId + -- ^ Commit the last write to the given 'CRef' by the given thread, + -- so that all threads can see the updated value. + | STM [TAction] [ThreadId] + -- ^ An STM transaction was executed, possibly waking up some + -- threads. + | BlockedSTM [TAction] + -- ^ Got blocked in an STM transaction. + | Catching + -- ^ Register a new exception handler + | PopCatching + -- ^ Pop the innermost exception handler from the stack. + | Throw + -- ^ Throw an exception. + | ThrowTo ThreadId + -- ^ Throw an exception to a thread. + | BlockedThrowTo ThreadId + -- ^ Get blocked on a 'throwTo'. + | Killed + -- ^ Killed by an uncaught exception. + | SetMasking Bool MaskingState + -- ^ Set the masking state. If 'True', this is being used to set the + -- masking state to the original state in the argument passed to a + -- 'mask'ed function. + | ResetMasking Bool MaskingState + -- ^ Return to an earlier masking state. If 'True', this is being + -- used to return to the state of the masked block in the argument + -- passed to a 'mask'ed function. + | LiftIO + -- ^ Lift an IO action. Note that this can only happen with + -- 'ConcIO'. + | Return + -- ^ A 'return' or 'pure' action was executed. + | Stop + -- ^ Cease execution and terminate. + | Subconcurrency + -- ^ Start executing an action with @subconcurrency@. + | StopSubconcurrency + -- ^ Stop executing an action with @subconcurrency@. + deriving (Eq, Show) + +instance NFData ThreadAction where + rnf (Fork t) = rnf t + rnf (ForkOS t) = rnf t + rnf (ThreadDelay n) = rnf n + rnf (GetNumCapabilities c) = rnf c + rnf (SetNumCapabilities c) = rnf c + rnf (NewMVar m) = rnf m + rnf (PutMVar m ts) = rnf (m, ts) + rnf (BlockedPutMVar m) = rnf m + rnf (TryPutMVar m b ts) = rnf (m, b, ts) + rnf (ReadMVar m) = rnf m + rnf (TryReadMVar m b) = rnf (m, b) + rnf (BlockedReadMVar m) = rnf m + rnf (TakeMVar m ts) = rnf (m, ts) + rnf (BlockedTakeMVar m) = rnf m + rnf (TryTakeMVar m b ts) = rnf (m, b, ts) + rnf (NewCRef c) = rnf c + rnf (ReadCRef c) = rnf c + rnf (ReadCRefCas c) = rnf c + rnf (ModCRef c) = rnf c + rnf (ModCRefCas c) = rnf c + rnf (WriteCRef c) = rnf c + rnf (CasCRef c b) = rnf (c, b) + rnf (CommitCRef t c) = rnf (t, c) + rnf (STM tr ts) = rnf (tr, ts) + rnf (BlockedSTM tr) = rnf tr + rnf (ThrowTo t) = rnf t + rnf (BlockedThrowTo t) = rnf t + rnf (SetMasking b m) = b `seq` m `seq` () + rnf (ResetMasking b m) = b `seq` m `seq` () + rnf a = a `seq` () + +-- | A one-step look-ahead at what a thread will do next. +-- +-- @since 1.0.0.0 +data Lookahead = + WillFork + -- ^ Will start a new thread. + | WillForkOS + -- ^ Will start a new bound thread. + | WillIsCurrentThreadBound + -- ^ Will check if the current thread is bound. + | WillMyThreadId + -- ^ Will get the 'ThreadId'. + | WillGetNumCapabilities + -- ^ Will get the number of Haskell threads that can run + -- simultaneously. + | WillSetNumCapabilities Int + -- ^ Will set the number of Haskell threads that can run + -- simultaneously. + | WillYield + -- ^ Will yield the current thread. + | WillThreadDelay Int + -- ^ Will yield/delay the current thread. + | WillNewMVar + -- ^ Will create a new 'MVar'. + | WillPutMVar MVarId + -- ^ Will put into a 'MVar', possibly waking up some threads. + | WillTryPutMVar MVarId + -- ^ Will try to put into a 'MVar', possibly waking up some threads. + | WillReadMVar MVarId + -- ^ Will read from a 'MVar'. + | WillTryReadMVar MVarId + -- ^ Will try to read from a 'MVar'. + | WillTakeMVar MVarId + -- ^ Will take from a 'MVar', possibly waking up some threads. + | WillTryTakeMVar MVarId + -- ^ Will try to take from a 'MVar', possibly waking up some threads. + | WillNewCRef + -- ^ Will create a new 'CRef'. + | WillReadCRef CRefId + -- ^ Will read from a 'CRef'. + | WillReadCRefCas CRefId + -- ^ Will read from a 'CRef' for a future compare-and-swap. + | WillModCRef CRefId + -- ^ Will modify a 'CRef'. + | WillModCRefCas CRefId + -- ^ Will modify a 'CRef' using a compare-and-swap. + | WillWriteCRef CRefId + -- ^ Will write to a 'CRef' without synchronising. + | WillCasCRef CRefId + -- ^ Will attempt to to a 'CRef' using a compare-and-swap, + -- synchronising it. + | WillCommitCRef ThreadId CRefId + -- ^ Will commit the last write by the given thread to the 'CRef'. + | WillSTM + -- ^ Will execute an STM transaction, possibly waking up some + -- threads. + | WillCatching + -- ^ Will register a new exception handler + | WillPopCatching + -- ^ Will pop the innermost exception handler from the stack. + | WillThrow + -- ^ Will throw an exception. + | WillThrowTo ThreadId + -- ^ Will throw an exception to a thread. + | WillSetMasking Bool MaskingState + -- ^ Will set the masking state. If 'True', this is being used to + -- set the masking state to the original state in the argument + -- passed to a 'mask'ed function. + | WillResetMasking Bool MaskingState + -- ^ Will return to an earlier masking state. If 'True', this is + -- being used to return to the state of the masked block in the + -- argument passed to a 'mask'ed function. + | WillLiftIO + -- ^ Will lift an IO action. Note that this can only happen with + -- 'ConcIO'. + | WillReturn + -- ^ Will execute a 'return' or 'pure' action. + | WillStop + -- ^ Will cease execution and terminate. + | WillSubconcurrency + -- ^ Will execute an action with @subconcurrency@. + | WillStopSubconcurrency + -- ^ Will stop executing an extion with @subconcurrency@. + deriving (Eq, Show) + +instance NFData Lookahead where + rnf (WillThreadDelay n) = rnf n + rnf (WillSetNumCapabilities c) = rnf c + rnf (WillPutMVar m) = rnf m + rnf (WillTryPutMVar m) = rnf m + rnf (WillReadMVar m) = rnf m + rnf (WillTryReadMVar m) = rnf m + rnf (WillTakeMVar m) = rnf m + rnf (WillTryTakeMVar m) = rnf m + rnf (WillReadCRef c) = rnf c + rnf (WillReadCRefCas c) = rnf c + rnf (WillModCRef c) = rnf c + rnf (WillModCRefCas c) = rnf c + rnf (WillWriteCRef c) = rnf c + rnf (WillCasCRef c) = rnf c + rnf (WillCommitCRef t c) = rnf (t, c) + rnf (WillThrowTo t) = rnf t + rnf (WillSetMasking b m) = b `seq` m `seq` () + rnf (WillResetMasking b m) = b `seq` m `seq` () + rnf l = l `seq` () + +-- | All the actions that an STM transaction can perform. +-- +-- @since 0.8.0.0 +data TAction = + TNew TVarId + -- ^ Create a new @TVar@ + | TRead TVarId + -- ^ Read from a @TVar@. + | TWrite TVarId + -- ^ Write to a @TVar@. + | TRetry + -- ^ Abort and discard effects. + | TOrElse [TAction] (Maybe [TAction]) + -- ^ Execute a transaction. If the transaction aborts by calling + -- @retry@, execute the other transaction. + | TThrow + -- ^ Throw an exception, abort, and discard effects. + | TCatch [TAction] (Maybe [TAction]) + -- ^ Execute a transaction. If the transaction aborts by throwing + -- an exception of the appropriate type, it is handled and execution + -- continues; otherwise aborts, propagating the exception upwards. + | TStop + -- ^ 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 + rnf (TOrElse tr mtr) = rnf (tr, mtr) + rnf (TCatch tr mtr) = rnf (tr, mtr) + rnf ta = ta `seq` () + +------------------------------------------------------------------------------- +-- * Traces + +-- | One of the outputs of the runner is a @Trace@, which is a log of +-- decisions made, all the alternative unblocked threads and what they +-- would do, and the action a thread took in its step. +-- +-- @since 0.8.0.0 +type Trace + = [(Decision, [(ThreadId, 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 + -- start of computation). + | Continue + -- ^ Continue running the last thread for another step. + | SwitchTo ThreadId + -- ^ 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 + rnf d = d `seq` () + +------------------------------------------------------------------------------- +-- * Failures + +-- | An indication of how a concurrent computation failed. +-- +-- The @Eq@, @Ord@, and @NFData@ instances compare/evaluate the +-- exception with @show@ in the @UncaughtException@ case. +-- +-- @since 0.9.0.0 +data Failure + = InternalError + -- ^ Will be raised if the scheduler does something bad. This should + -- never arise unless you write your own, faulty, scheduler! If it + -- does, please file a bug report. + | Abort + -- ^ The scheduler chose to abort execution. This will be produced + -- if, for example, all possible decisions exceed the specified + -- bounds (there have been too many pre-emptions, the computation + -- has executed for too long, or there have been too many yields). + | Deadlock + -- ^ Every thread is blocked, and the main thread is /not/ blocked + -- in an STM transaction. + | STMDeadlock + -- ^ Every thread is blocked, and the main thread is blocked in an + -- STM transaction. + | UncaughtException SomeException + -- ^ An uncaught exception bubbled to the top of the computation. + | IllegalSubconcurrency + -- ^ Calls to @subconcurrency@ were nested, or attempted when + -- multiple threads existed. + deriving Show + +instance Eq Failure where + InternalError == InternalError = True + Abort == Abort = True + Deadlock == Deadlock = True + STMDeadlock == STMDeadlock = True + (UncaughtException e1) == (UncaughtException e2) = show e1 == show e2 + IllegalSubconcurrency == IllegalSubconcurrency = True + _ == _ = False + +instance Ord Failure where + compare = compare `on` transform where + transform :: Failure -> (Int, Maybe String) + transform InternalError = (0, Nothing) + transform Abort = (1, Nothing) + transform Deadlock = (2, Nothing) + transform STMDeadlock = (3, Nothing) + transform (UncaughtException e) = (4, Just (show e)) + transform IllegalSubconcurrency = (5, Nothing) + +instance NFData Failure where + rnf (UncaughtException e) = rnf (show e) + rnf f = f `seq` () + +-- | Check if a failure is an @InternalError@. +-- +-- @since 0.9.0.0 +isInternalError :: Failure -> Bool +isInternalError InternalError = True +isInternalError _ = False + +-- | Check if a failure is an @Abort@. +-- +-- @since 0.9.0.0 +isAbort :: Failure -> Bool +isAbort Abort = True +isAbort _ = False + +-- | Check if a failure is a @Deadlock@ or an @STMDeadlock@. +-- +-- @since 0.9.0.0 +isDeadlock :: Failure -> Bool +isDeadlock Deadlock = True +isDeadlock STMDeadlock = True +isDeadlock _ = False + +-- | Check if a failure is an @UncaughtException@ +-- +-- @since 0.9.0.0 +isUncaughtException :: Failure -> Bool +isUncaughtException (UncaughtException _) = True +isUncaughtException _ = False + +-- | Check if a failure is an @IllegalSubconcurrency@ +-- +-- @since 0.9.0.0 +isIllegalSubconcurrency :: Failure -> Bool +isIllegalSubconcurrency IllegalSubconcurrency = True +isIllegalSubconcurrency _ = False + +------------------------------------------------------------------------------- +-- * Discarding results and traces + +-- | An @Either Failure a -> Maybe Discard@ value can be used to +-- selectively discard results. +-- +-- @since 0.7.1.0 +data Discard + = DiscardTrace + -- ^ Discard the trace but keep the result. The result will appear + -- to have an empty trace. + | DiscardResultAndTrace + -- ^ Discard the result and the trace. It will simply not be + -- reported as a possible behaviour of the program. + deriving (Eq, Show, Read, Ord, Enum, Bounded) + +instance NFData Discard where + rnf d = d `seq` () + +-- | Combine two discard values, keeping the weaker. +-- +-- @Nothing@ is weaker than @Just DiscardTrace@, which is weaker than +-- @Just DiscardResultAndTrace@. This forms a commutative monoid +-- where the unit is @const (Just DiscardResultAndTrace)@. +-- +-- @since 1.0.0.0 +weakenDiscard :: + (Either Failure a -> Maybe Discard) + -> (Either Failure a -> Maybe Discard) + -> Either Failure a -> Maybe Discard +weakenDiscard d1 d2 efa = case (d1 efa, d2 efa) of + (Nothing, _) -> Nothing + (_, Nothing) -> Nothing + (Just DiscardTrace, _) -> Just DiscardTrace + (_, Just DiscardTrace) -> Just DiscardTrace + _ -> Just DiscardResultAndTrace + +-- | Combine two discard functions, keeping the stronger. +-- +-- @Just DiscardResultAndTrace@ is stronger than @Just DiscardTrace@, +-- which is stronger than @Nothing@. This forms a commutative monoid +-- where the unit is @const Nothing@. +-- +-- @since 1.0.0.0 +strengthenDiscard :: + (Either Failure a -> Maybe Discard) + -> (Either Failure a -> Maybe Discard) + -> Either Failure a -> Maybe Discard +strengthenDiscard d1 d2 efa = case (d1 efa, d2 efa) of + (Just DiscardResultAndTrace, _) -> Just DiscardResultAndTrace + (_, Just DiscardResultAndTrace) -> Just DiscardResultAndTrace + (Just DiscardTrace, _) -> Just DiscardTrace + (_, Just DiscardTrace) -> Just DiscardTrace + _ -> Nothing + +------------------------------------------------------------------------------- +-- * 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 + -- interleaving of the actions in different threads. When a 'CRef' + -- is written to, that write is immediately visible to all threads. + | TotalStoreOrder + -- ^ 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. + | PartialStoreOrder + -- ^ 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 'CRef's + -- are not necessarily committed in the same order that they are + -- created. + deriving (Eq, Show, Read, Ord, Enum, Bounded) + +-- | @since 0.5.1.0 +instance NFData MemType where + rnf m = m `seq` () + +------------------------------------------------------------------------------- +-- * @MonadFail@ + +-- | An exception for errors in testing caused by use of 'fail'. +newtype MonadFailException = MonadFailException String + deriving Show + +instance Exception MonadFailException diff --git a/Test/DejaFu/Utils.hs b/Test/DejaFu/Utils.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Utils.hs @@ -0,0 +1,114 @@ +-- | +-- Module : Test.DejaFu.utils +-- Copyright : (c) 2017 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : portable +-- +-- Utility functions for users of dejafu. +module Test.DejaFu.Utils where + +import Control.Exception (Exception(..), displayException) +import Data.List (intercalate, minimumBy) +import Data.Maybe (mapMaybe) +import Data.Ord (comparing) + +import Test.DejaFu.Types + +------------------------------------------------------------------------------- +-- * Traces + +-- | 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 [] = "" +showTrace trc = intercalate "\n" $ go False trc : strkey where + go _ ((_,_,CommitCRef _ _):rest) = "C-" ++ go False rest + go _ ((Start (ThreadId (Id _ i)),_,a):rest) = "S" ++ show i ++ "-" ++ go (didYield a) rest + go y ((SwitchTo (ThreadId (Id _ i)),_,a):rest) = (if y then "p" else "P") ++ show i ++ "-" ++ go (didYield a) rest + go _ ((Continue,_,a):rest) = '-' : go (didYield a) rest + go _ _ = "" + + strkey = + [" " ++ show i ++ ": " ++ name | (i, name) <- threadNames trc] + + didYield Yield = True + didYield (ThreadDelay _) = True + didYield _ = False + +-- | Get all named threads in the trace. +-- +-- @since 0.7.3.0 +threadNames :: Trace -> [(Int, String)] +threadNames = mapMaybe go where + go (_, _, Fork (ThreadId (Id (Just name) i))) = Just (i, name) + go (_, _, ForkOS (ThreadId (Id (Just name) i))) = Just (i, name) + go _ = Nothing + +-- | Find the \"simplest\" trace leading to each result. +simplestsBy :: (x -> x -> Bool) -> [(x, Trace)] -> [(x, Trace)] +simplestsBy f = map choose . collect where + collect = groupBy' [] (\(a,_) (b,_) -> f a b) + choose = minimumBy . comparing $ \(_, trc) -> + let switchTos = length . filter (\(d,_,_) -> case d of SwitchTo _ -> True; _ -> False) + starts = length . filter (\(d,_,_) -> case d of Start _ -> True; _ -> False) + commits = length . filter (\(_,_,a) -> case a of CommitCRef _ _ -> True; _ -> False) + in (switchTos trc, commits trc, length trc, starts trc) + + groupBy' res _ [] = res + groupBy' res eq (y:ys) = groupBy' (insert' eq y res) eq ys + + insert' _ x [] = [[x]] + insert' eq x (ys@(y:_):yss) + | x `eq` y = (x:ys) : yss + | otherwise = ys : insert' eq x yss + insert' _ _ ([]:_) = undefined + +------------------------------------------------------------------------------- +-- * Failures + +-- | Pretty-print a failure +-- +-- @since 0.4.0.0 +showFail :: Failure -> String +showFail Abort = "[abort]" +showFail Deadlock = "[deadlock]" +showFail STMDeadlock = "[stm-deadlock]" +showFail InternalError = "[internal-error]" +showFail (UncaughtException exc) = "[" ++ displayException exc ++ "]" +showFail IllegalSubconcurrency = "[illegal-subconcurrency]" + +------------------------------------------------------------------------------- +-- * Scheduling + +-- | 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 +tidOf tid _ = tid + +-- | Get the 'Decision' that would have resulted in this thread +-- identifier, given a prior thread (if any) and collection of threads +-- which are unblocked at this point. +-- +-- @since 0.5.0.0 +decisionOf :: Foldable f + => Maybe ThreadId + -- ^ The prior thread. + -> f ThreadId + -- ^ The threads. + -> ThreadId + -- ^ The current thread. + -> Decision +decisionOf Nothing _ chosen = Start chosen +decisionOf (Just prior) runnable chosen + | prior == chosen = Continue + | prior `elem` runnable = SwitchTo chosen + | otherwise = Start chosen diff --git a/dejafu.cabal b/dejafu.cabal --- a/dejafu.cabal +++ b/dejafu.cabal @@ -2,29 +2,25 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: dejafu -version: 0.9.1.2 -synopsis: Systematic testing for Haskell concurrency. +version: 1.0.0.0 +synopsis: A library for unit-testing concurrent programs. description: /[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 - - provides deterministic parallelism, but sometimes we can tolerate a - bit of nondeterminism. - . This package builds on the - - package by enabling you to systematically and deterministically test - your concurrent programs. + [concurrency](https://hackage.haskell.org/package/concurrency) + package by enabling you to deterministically test your concurrent + programs. + . + See the [website](https://dejafu.readthedocs.io) or README for more. homepage: https://github.com/barrucadu/dejafu license: MIT license-file: LICENSE author: Michael Walker maintainer: mike@barrucadu.co.uk --- copyright: +copyright: (c) 2015--2017 Michael Walker category: Concurrency build-type: Simple extra-source-files: README.markdown CHANGELOG.markdown @@ -37,37 +33,39 @@ source-repository this type: git location: https://github.com/barrucadu/dejafu.git - tag: dejafu-0.9.1.2 + tag: dejafu-1.0.0.0 library exposed-modules: Test.DejaFu , Test.DejaFu.Conc - , Test.DejaFu.Common , Test.DejaFu.Defaults , Test.DejaFu.Refinement - , Test.DejaFu.Schedule , Test.DejaFu.SCT - , Test.DejaFu.STM + , Test.DejaFu.Schedule + , Test.DejaFu.Types + , Test.DejaFu.Utils , Test.DejaFu.Conc.Internal , Test.DejaFu.Conc.Internal.Common , Test.DejaFu.Conc.Internal.Memory + , Test.DejaFu.Conc.Internal.STM , Test.DejaFu.Conc.Internal.Threading - , Test.DejaFu.SCT.Internal - , Test.DejaFu.STM.Internal + , Test.DejaFu.Internal + , Test.DejaFu.SCT.Internal.DPOR + , Test.DejaFu.SCT.Internal.Weighted -- other-modules: -- other-extensions: build-depends: base >=4.8 && <5 - , concurrency >=1.1 && <1.3 + , concurrency >=1.3 && <1.4 , containers >=0.5 && <0.6 , deepseq >=1.1 && <2 , exceptions >=0.7 && <0.9 , leancheck >=0.6 && <0.8 + , profunctors >=4.0 && <6.0 , random >=1.0 && <1.2 , ref-fd >=0.4 && <0.5 - , transformers >=0.4 && <0.6 - , transformers-base >=0.4 && <0.5 + , transformers >=0.4 && <0.6 -- hs-source-dirs: default-language: Haskell2010 ghc-options: -Wall