dejafu 0.9.1.2 → 1.0.0.0

raw patch · 24 files changed

+3554/−3305 lines, 24 filesdep +profunctorsdep −transformers-basedep ~concurrencyPVP ok

version bump matches the API change (PVP)

Dependencies added: profunctors

Dependencies removed: transformers-base

Dependency ranges changed: concurrency

API changes (from Hackage documentation)

Files

• CHANGELOG.markdown +112/−0
• LICENSE +1/−1
• README.markdown +105/−42
• Test/DejaFu.hs +939/−798
• Test/DejaFu/Common.hs +0/−1070
• Test/DejaFu/Conc.hs +28/−24
• Test/DejaFu/Conc/Internal.hs +48/−23
• Test/DejaFu/Conc/Internal/Common.hs +13/−8
• Test/DejaFu/Conc/Internal/Memory.hs +5/−5
• Test/DejaFu/Conc/Internal/STM.hs +239/−0
• Test/DejaFu/Conc/Internal/Threading.hs +59/−8
• Test/DejaFu/Defaults.hs +1/−1
• Test/DejaFu/Internal.hs +338/−0
• Test/DejaFu/Refinement.hs +4/−5
• Test/DejaFu/SCT.hs +92/−91
• Test/DejaFu/SCT/Internal.hs +0/−816
• Test/DejaFu/SCT/Internal/DPOR.hs +793/−0
• Test/DejaFu/SCT/Internal/Weighted.hs +66/−0
• Test/DejaFu/STM.hs +0/−122
• Test/DejaFu/STM/Internal.hs +0/−225
• Test/DejaFu/Schedule.hs +12/−45
• Test/DejaFu/Types.hs +566/−0
• Test/DejaFu/Utils.hs +114/−0
• dejafu.cabal +19/−21

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

@@ -1,4 +1,4 @@-Copyright (c) 2015, Michael Walker <mike@barrucadu.co.uk>+Copyright (c) 2015--2017, Michael Walker <mike@barrucadu.co.uk>  Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the

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

@@ -1,801 +1,942 @@-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE RankNTypes #-}---- |--- Module      : Test.DejaFu--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- 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 <mike@barrucadu.co.uk>+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" <trace discarded>+-- >+-- >         "world" <trace discarded>+--+-- @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

@@ -1,1070 +0,0 @@--- |--- Module      : Test.DejaFu.Common--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- 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 []  = "<trace discarded>"-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)

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

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

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

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

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

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

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

@@ -0,0 +1,338 @@+-- |+-- Module      : Test.DejaFu.Internal+-- Copyright   : (c) 2017 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- 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)

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

@@ -4,7 +4,7 @@  -- | -- Module      : Test.DejaFu.SCT--- Copyright   : (c) 2016 Michael Walker+-- Copyright   : (c) 2015--2017 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- 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

@@ -1,816 +0,0 @@-{-# LANGUAGE TupleSections #-}---- |--- Module      : Test.DejaFu.SCT.Internal--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- 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

@@ -0,0 +1,793 @@+-- |+-- Module      : Test.DejaFu.SCT.Internal.DPOR+-- Copyright   : (c) 2015--2017 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- 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

@@ -0,0 +1,66 @@+-- |+-- Module      : Test.DejaFu.SCT.Internal.Weighted+-- Copyright   : (c) 2015--2017 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- 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'')

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

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

@@ -1,6 +1,6 @@ -- | -- Module      : Test.DejaFu.Schedule--- Copyright   : (c) 2016 Michael Walker+-- Copyright   : (c) 2016--2017 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- 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 ()

@@ -0,0 +1,566 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++-- |+-- Module      : Test.DejaFu.Types+-- Copyright   : (c) 2017 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- 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