dejafu 1.12.0.0 → 2.0.0.0

raw patch · 18 files changed

+1556/−1262 lines, 18 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.rst +139/−0
• Test/DejaFu.hs +133/−87
• Test/DejaFu/Conc.hs +125/−330
• Test/DejaFu/Conc/Internal.hs +211/−196
• Test/DejaFu/Conc/Internal/Common.hs +119/−26
• Test/DejaFu/Conc/Internal/Memory.hs +6/−0
• Test/DejaFu/Conc/Internal/Program.hs +374/−0
• Test/DejaFu/Internal.hs +66/−7
• Test/DejaFu/Refinement.hs +12/−9
• Test/DejaFu/SCT.hs +66/−281
• Test/DejaFu/SCT/Internal.hs +91/−62
• Test/DejaFu/SCT/Internal/DPOR.hs +33/−164
• Test/DejaFu/SCT/Internal/Weighted.hs +11/−6
• Test/DejaFu/Schedule.hs +11/−8
• Test/DejaFu/Settings.hs +24/−14
• Test/DejaFu/Types.hs +129/−67
• Test/DejaFu/Utils.hs +1/−1
• dejafu.cabal +5/−4

@@ -7,6 +7,145 @@ .. _PVP: https://pvp.haskell.org/  +2.0.0.0 (2019-02-12)+--------------------++* Git: :tag:`dejafu-2.0.0.0`+* Hackage: :hackage:`dejafu-2.0.0.0`++Added+~~~~~++* The ``Program`` types and their constructors (re-exported from+  ``Test.DejaFu``):+    * ``Test.DejaFu.Conc.Program``+    * ``Test.DejaFu.Conc.Basic``+    * ``Test.DejaFu.Conc.WithSetup``+    * ``Test.DejaFu.Conc.WithSetupAndTeardown``+    * ``Test.DejaFu.Conc.withSetup``+    * ``Test.DejaFu.Conc.withTeardown``+    * ``Test.DejaFu.Conc.withSetupAndTeardown``++* The ``Invariant`` type and associated functions (re-exported from+  ``Test.DejaFu``):+    * ``Test.DejaFu.Conc.Invariant``+    * ``Test.DejaFu.Conc.registerInvariant``+    * ``Test.DejaFu.Conc.inspectIORef``+    * ``Test.DejaFu.Conc.inspectMVar``+    * ``Test.DejaFu.Conc.inspectTVar``++* New snapshotting functions:+    * ``Test.DejaFu.Conc.Snapshot``+    * ``Test.DejaFu.Conc.recordSnapshot``+    * ``Test.DejaFu.Conc.runSnapshot``++* ``Test.DejaFu.Settings.llengthBound``, which now applies to all ways+  of testing.++* ``Test.DejaFu.Types.isInvariantFailure`` (re-exported from+  ``Test.DejaFu``).++* ``Test.DejaFu.runTestWithSettings`` function.++* A simplified form of the concurrency state:+    * ``Test.DejaFu.Types.ConcurrencyState``+    * ``Test.DejaFu.Types.isBuffered``+    * ``Test.DejaFu.Types.numBuffered``+    * ``Test.DejaFu.Types.isFull``+    * ``Test.DejaFu.Types.canInterrupt``+    * ``Test.DejaFu.Types.canInterruptL``+    * ``Test.DejaFu.Types.isMaskedInterruptible``+    * ``Test.DejaFu.Types.isMaskedUninterruptible``++Changed+~~~~~~~++* ``Test.DejaFu.Schedule.Scheduler`` has a ``ConcurrencyState``+  parameter.++* ``Test.DejaFu.alwaysSameBy`` and ``Test.DejaFu.notAlwaysSameBy``+  return a representative trace for each unique condition.++* Functions which took a ``ConcT`` now take a ``Program pty``:+    * ``Test.DejaFu.autocheck``+    * ``Test.DejaFu.autocheckWay``+    * ``Test.DejaFu.autocheckWithSettings``+    * ``Test.DejaFu.dejafu``+    * ``Test.DejaFu.dejafuWay``+    * ``Test.DejaFu.dejafuWithSettings``+    * ``Test.DejaFu.dejafus``+    * ``Test.DejaFu.dejafusWay``+    * ``Test.DejaFu.dejafusWithSettings``+    * ``Test.DejaFu.runTest``+    * ``Test.DejaFu.runTestWay``+    * ``Test.DejaFu.runTestWithSettings``+    * ``Test.DejaFu.Conc.runConcurrent``+    * ``Test.DejaFu.SCT.runSCT``+    * ``Test.DejaFu.SCT.resultsSet``+    * ``Test.DejaFu.SCT.runSCT'``+    * ``Test.DejaFu.SCT.resultsSet'``+    * ``Test.DejaFu.SCT.runSCTWithSettings``+    * ``Test.DejaFu.SCT.resultsSetWithSettings``+    * ``Test.DejaFu.SCT.runSCTWithSettings'``+    * ``Test.DejaFu.SCT.resultsSetWithSettings'``++* ``Test.DejaFu.Conc.ConcT`` is an alias for ``Program Basic``.++* ``Test.DejaFu.Types.Bounds``:+    * Removed ``boundLength`` field.++* ``Test.DejaFu.Types.Condition``:+    * Added ``InvariantFailure`` constructor+    * Removed ``STMDeadlock`` constructor++* ``Test.DejaFu.Types.Error``:+    * Removed ``NestedSubconcurrency``, ``MultithreadedSubconcurrency``,+      and ``LateDontCheck`` constructors.++* ``Test.DejaFu.Types.Lookahead``:+    * Added ``WillRegisterInvariant`` constructor+    * Removed ``WillSubconcurrency``, ``WillStopSubconcurrency``, and+      ``WillDontCheck`` constructors++* ``Test.DejaFu.Types.ThreadAction``:+    * Added ``RegisterInvariant`` constructor+    * Removed ``Subconcurrency``, ``StopSubconcurrency``, and+      ``DontCheck`` constructors++Removed+~~~~~~~++* The deprecated functions:+    * ``Test.DejaFu.dejafuDiscard``+    * ``Test.DejaFu.SCT.runSCTDiscard``+    * ``Test.DejaFu.SCT.runSCTDiscard'``+    * ``Test.DejaFu.SCT.resultsSetDiscard``+    * ``Test.DejaFu.SCT.resultsSetDiscard'``+    * ``Test.DejaFu.SCT.sctBound``+    * ``Test.DejaFu.SCT.sctBoundDiscard``+    * ``Test.DejaFu.SCT.sctUniformRandom``+    * ``Test.DejaFu.SCT.sctUniformRandomDiscard``+    * ``Test.DejaFu.SCT.sctWeightedRandom``+    * ``Test.DejaFu.SCT.sctWeightedRandomDiscard``++* The deprecated type ``Test.DejaFu.Types.Failure``++* Old snapshotting functions:+    * ``Test.DejaFu.Conc.DCSnapshot``+    * ``Test.DejaFu.Conc.runForDCSnapshot``+    * ``Test.DejaFu.Conc.runWithDCSnapshot``+    * ``Test.DejaFu.Conc.canDCSnapshot``+    * ``Test.DejaFu.Conc.threadsFromDCSnapshot``++* ``Test.DejaFu.Conc.dontCheck``++* ``Test.DejaFu.Conc.subconcurrency``++* ``Test.DejaFu.Settings.defaultLengthBound``++* ``Test.DejaFu.Types.isIncorrectUsage``++ 1.12.0.0 (2019-01-20) --------------------- 

@@ -2,16 +2,20 @@  {- | Module      : Test.DejaFu-Copyright   : (c) 2015--2018 Michael Walker+Copyright   : (c) 2015--2019 Michael Walker License     : MIT Maintainer  : Michael Walker <mike@barrucadu.co.uk> Stability   : experimental Portability : 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.+dejafu is a library for unit-testing concurrent Haskell programs which+are written using the <https://hackage.haskell.org/package/concurrency+concurrency> package's 'MonadConc' typeclass. +For more in-depth documentation, including migration guides from+earlier versions of dejafu, see the <https://dejafu.readthedocs.io+website>.+ __A first test:__ This is a simple concurrent program which forks two threads and each races to write to the same @MVar@: @@ -46,16 +50,66 @@   * Each \"-\" represents one \"step\" of the computation. -__Conditions:__ A program may fail to terminate in a way which-produces a value. dejafu can detect a few such cases:+__Memory models:__ dejafu supports three different memory models,+which affect how one thread's 'IORef' updates become visible to other+threads. - * 'Deadlock', if every thread is blocked.+ * Sequential consistency: a program behaves as a simple interleaving+   of the actions in different threads. When an 'IORef' is written to,+   that write is immediately visible to all threads. - * 'STMDeadlock', if every thread is blocked /and/ the main thread is-   blocked in an STM transaction.+  * 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. - * 'UncaughtException', if the main thread is killed by an exception.+  * Partial store order (PSO): each 'IORef' 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 'IORef's are not necessarily committed in the+    same order that they are created. +This small example shows the difference between sequential consistency+and TSO:++>>> :{+let relaxed = do+      r1 <- newIORef False+      r2 <- newIORef False+      x <- spawn $ writeIORef r1 True >> readIORef r2+      y <- spawn $ writeIORef r2 True >> readIORef r1+      (,) <$> readMVar x <*> readMVar y+:}++The 'autocheckWay' function will let us specify the memory model:++>>> autocheckWay defaultWay SequentialConsistency relaxed+[pass] Successful+[fail] Deterministic+    (False,True) S0---------S1----S0--S2----S0--+<BLANKLINE>+    (True,True) S0---------S1-P2----S1---S0---+<BLANKLINE>+    (True,False) S0---------S2----S1----S0---+False++>>> autocheckWay defaultWay TotalStoreOrder relaxed+[pass] Successful+[fail] Deterministic+    (False,True) S0---------S1----S0--S2----S0--+<BLANKLINE>+    (False,False) S0---------S1--P2----S1--S0---+<BLANKLINE>+    (True,False) S0---------S2----S1----S0---+<BLANKLINE>+    (True,True) S0---------S1-C-S2----S1---S0---+False++The result @(False,False)@ is possible using TSO and PSO, but not+sequential consistency.  The \"C\" in the trace shows where a /commit/+action occurred, which makes a write to an 'IORef' visible to all+threads.+ __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@@ -107,9 +161,9 @@ -}    , Result(..)-  , Condition(..)   , runTest   , runTestWay+  , runTestWithSettings    -- ** Predicates @@ -169,23 +223,24 @@  -} +  , Condition(..)   , isAbort   , isDeadlock   , isUncaughtException+  , isInvariantFailure -  -- * Property testing+  -- * Property-based testing    {- | -dejafu can also use a property-testing style to test stateful+dejafu can also use a property-based 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+<https://hackage.haskell.org/package/leancheck 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+__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. @@ -237,11 +292,27 @@    , module Test.DejaFu.Refinement -  -- * Deprecated-  , Failure-  , dejafuDiscard-  ) where+  -- * Expressing concurrent programs+  , Program+  , Basic+  , ConcT+  , ConcIO +  -- ** Setup and teardown+  , WithSetup+  , WithSetupAndTeardown+  , withSetup+  , withTeardown+  , withSetupAndTeardown++  -- ** Invariants+  , Invariant+  , registerInvariant+  , inspectIORef+  , inspectMVar+  , inspectTVar+) where+ import           Control.Arrow            (first) import           Control.DeepSeq          (NFData(..)) import           Control.Monad            (unless, when)@@ -302,9 +373,9 @@ --     "world" S0----S2--S0-- -- False ----- @since 1.0.0.0+-- @since 2.0.0.0 autocheck :: (MonadConc n, MonadIO n, Eq a, Show a)-  => ConcT n a+  => Program pty n a   -- ^ The computation to test.   -> n Bool autocheck = autocheckWithSettings defaultSettings@@ -334,13 +405,13 @@ --     (True,False) S0---------S2----S1----S0--- -- False ----- @since 1.0.0.0+-- @since 2.0.0.0 autocheckWay :: (MonadConc n, MonadIO n, Eq a, Show a)   => Way   -- ^ How to run the concurrent program.   -> MemType   -- ^ The memory model to use for non-synchronised @IORef@ operations.-  -> ConcT n a+  -> Program pty n a   -- ^ The computation to test.   -> n Bool autocheckWay way = autocheckWithSettings . fromWayAndMemType way@@ -369,16 +440,16 @@ --     (True,False) S0---------S2----S1----S0--- -- False ----- @since 1.2.0.0+-- @since 2.0.0.0 autocheckWithSettings :: (MonadConc n, MonadIO n, Eq a, Show a)   => Settings n a   -- ^ The SCT settings.-  -> ConcT n a+  -> Program pty n a   -- ^ The computation to test.   -> n Bool autocheckWithSettings settings = dejafusWithSettings settings   [ ("Successful", representative successful)-  , ("Deterministic", alwaysSame) -- already representative+  , ("Deterministic", representative alwaysSame)   ]  -- | Check a predicate and print the result to stdout, return 'True'@@ -395,13 +466,13 @@ --     "world" S0----S2--S0-- -- False ----- @since 1.0.0.0+-- @since 2.0.0.0 dejafu :: (MonadConc n, MonadIO n, Show b)   => String   -- ^ The name of the test.   -> ProPredicate a b   -- ^ The predicate to check.-  -> ConcT n a+  -> Program pty n a   -- ^ The computation to test.   -> n Bool dejafu = dejafuWithSettings defaultSettings@@ -425,7 +496,7 @@ --     "world" S0----S2--S1-S0-- -- False ----- @since 1.0.0.0+-- @since 2.0.0.0 dejafuWay :: (MonadConc n, MonadIO n, Show b)   => Way   -- ^ How to run the concurrent program.@@ -435,7 +506,7 @@   -- ^ The name of the test.   -> ProPredicate a b   -- ^ The predicate to check.-  -> ConcT n a+  -> Program pty n a   -- ^ The computation to test.   -> n Bool dejafuWay way = dejafuWithSettings . fromWayAndMemType way@@ -451,7 +522,7 @@ --     "world" S0----S2--S1-S0-- -- False ----- @since 1.2.0.0+-- @since 2.0.0.0 dejafuWithSettings :: (MonadConc n, MonadIO n, Show b)   => Settings n a   -- ^ The SCT settings.@@ -459,40 +530,12 @@   -- ^ The name of the test.   -> ProPredicate a b   -- ^ The predicate to check.-  -> ConcT n a+  -> Program pty n a   -- ^ The computation to test.   -> n Bool dejafuWithSettings settings name test =   dejafusWithSettings settings [(name, test)] --- | Variant of 'dejafuWay' which can selectively discard results.------ >>> dejafuDiscard (\_ -> Just DiscardTrace) defaultWay defaultMemType "Discarding" alwaysSame example--- [fail] Discarding---     "hello" <trace discarded>--- <BLANKLINE>---     "world" <trace discarded>--- False------ @since 1.0.0.0-dejafuDiscard :: (MonadConc n, MonadIO n, Show b)-  => (Either Condition a -> Maybe Discard)-  -- ^ Selectively discard results.-  -> Way-  -- ^ How to run the concurrent program.-  -> MemType-  -- ^ The memory model to use for non-synchronised @IORef@ operations.-  -> String-  -- ^ The name of the test.-  -> ProPredicate a b-  -- ^ The predicate to check.-  -> ConcT n a-  -- ^ The computation to test.-  -> n Bool-dejafuDiscard discard way =-  dejafuWithSettings . set ldiscard (Just discard) . fromWayAndMemType way-{-# DEPRECATED dejafuDiscard "Use dejafuWithSettings instead" #-}- -- | Variant of 'dejafu' which takes a collection of predicates to -- test, returning 'True' if all pass. --@@ -504,11 +547,11 @@ -- [pass] B -- False ----- @since 1.0.0.0+-- @since 2.0.0.0 dejafus :: (MonadConc n, MonadIO n, Show b)   => [(String, ProPredicate a b)]   -- ^ The list of predicates (with names) to check.-  -> ConcT n a+  -> Program pty n a   -- ^ The computation to test.   -> n Bool dejafus = dejafusWithSettings defaultSettings@@ -526,7 +569,7 @@ -- [pass] B -- False ----- @since 1.0.0.0+-- @since 2.0.0.0 dejafusWay :: (MonadConc n, MonadIO n, Show b)   => Way   -- ^ How to run the concurrent program.@@ -534,7 +577,7 @@   -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> [(String, ProPredicate a b)]   -- ^ The list of predicates (with names) to check.-  -> ConcT n a+  -> Program pty n a   -- ^ The computation to test.   -> n Bool dejafusWay way = dejafusWithSettings . fromWayAndMemType way@@ -551,13 +594,13 @@ -- [pass] B -- False ----- @since 1.2.0.0+-- @since 2.0.0.0 dejafusWithSettings :: (MonadConc n, MonadIO n, Show b)   => Settings n a   -- ^ The SCT settings.   -> [(String, ProPredicate a b)]   -- ^ The list of predicates (with names) to check.-  -> ConcT n a+  -> Program pty n a   -- ^ The computation to test.   -> n Bool dejafusWithSettings settings tests conc = do@@ -627,11 +670,11 @@ -- 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+-- @since 2.0.0.0 runTest :: MonadConc n   => ProPredicate a b   -- ^ The predicate to check-  -> ConcT n a+  -> Program pty n a   -- ^ The computation to test   -> n (Result b) runTest = runTestWithSettings defaultSettings@@ -643,7 +686,7 @@ -- 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+-- @since 2.0.0.0 runTestWay :: MonadConc n   => Way   -- ^ How to run the concurrent program.@@ -651,7 +694,7 @@   -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> ProPredicate a b   -- ^ The predicate to check-  -> ConcT n a+  -> Program pty n a   -- ^ The computation to test   -> n (Result b) runTestWay way = runTestWithSettings . fromWayAndMemType way@@ -662,13 +705,13 @@ -- found, is unspecified and may change between releases.  This may -- affect which failing traces are reported, when there is a failure. ----- @since 1.2.0.0+-- @since 2.0.0.0 runTestWithSettings :: MonadConc n   => Settings n a   -- ^ The SCT settings.   -> ProPredicate a b   -- ^ The predicate to check-  -> ConcT n a+  -> Program pty n a   -- ^ The computation to test   -> n (Result b) runTestWithSettings settings p conc =@@ -723,7 +766,7 @@       in result { _failures = simplestsBy (==) (_failures result) }   } --- | Check that a computation never fails.+-- | Check that a computation never produces a @Left@ value. -- -- @since 1.9.1.0 successful :: Predicate a@@ -801,8 +844,7 @@ exceptionsSometimes :: Predicate a exceptionsSometimes = somewhereTrue $ either isUncaughtException (const False) --- | Check that a computation always gives the same, successful,--- result.+-- | Check that a computation always gives the same, @Right@, result. -- -- > alwaysSame = alwaysSameBy (==) --@@ -811,7 +853,7 @@ alwaysSame = alwaysSameBy (==)  -- | Check that a computation always gives the same (according to the--- provided function), successful, result.+-- provided function), @Right@, result. -- -- > alwaysSameOn = alwaysSameBy ((==) `on` f) --@@ -829,14 +871,15 @@   , peval = \xs ->       let (failures, successes) = partition (isLeft . fst) xs           simpleSuccesses = simplestsBy (f `on` efromRight) successes-      in case (failures, simpleSuccesses) of+          simpleFailures  = simplestsBy ((==) `on` efromLeft) failures+      in case (simpleFailures, simpleSuccesses) of         ([], []) -> defaultPass         ([], [_]) -> defaultPass-        (_, _) -> defaultFail (failures ++ simpleSuccesses)+        (_, _) -> defaultFail (simpleFailures ++ simpleSuccesses)   }  -- | Check that a computation never fails, and gives multiple distinct--- successful results.+-- @Right@ results. -- -- > notAlwaysSame = notAlwaysSameBy (==) --@@ -845,7 +888,7 @@ notAlwaysSame = notAlwaysSameBy (==)  -- | Check that a computation never fails, and gives multiple distinct--- (according to the provided function) successful results.+-- (according to the provided function) @Right@ results. -- -- > notAlwaysSameOn = notAlwaysSameBy ((==) `on` f) --@@ -854,7 +897,7 @@ notAlwaysSameOn f = notAlwaysSameBy ((==) `on` f)  -- | Check that a computation never fails, and gives multiple distinct--- successful results, by applying a transformation on results.+-- @Right@ results, by applying a transformation on results. -- -- This inverts the condition, so (eg) @notAlwaysSameBy (==)@ will -- pass if there are unequal results.@@ -865,13 +908,14 @@     { pdiscard = const Nothing     , peval = \xs ->         let (failures, successes) = partition (isLeft . fst) xs+            simpleFailures = simplestsBy ((==) `on` efromLeft) failures         in case successes of-          [x] -> defaultFail (x : failures)+          [x] -> defaultFail (x : simpleFailures)           _  ->             let res = go successes (defaultFail [])             in case failures of               [] -> res-              _ -> res { _failures = failures ++ _failures res, _pass = False }+              _ -> res { _failures = simpleFailures ++ _failures res, _pass = False }     }   where     y1 .*. y2 = not (on f (efromRight . fst) y1 y2)@@ -945,7 +989,9 @@      failures = filter (\(r, _) -> r `notElem` expected) --- | Variant of 'gives' that doesn't allow for non-success conditions.+-- | Variant of 'gives' that doesn't allow for @Left@ results.+--+-- > gives' = gives . map Right -- -- @since 1.0.0.0 gives' :: (Eq a, Show a) => [a] -> Predicate a

@@ -1,16 +1,10 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE TypeFamilies #-}- -- | -- Module      : Test.DejaFu.Conc--- Copyright   : (c) 2016--2018 Michael Walker+-- Copyright   : (c) 2016--2019 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : CPP, FlexibleInstances, GeneralizedNewtypeDeriving, TypeFamilies+-- Portability : portable -- -- Deterministic traced execution of concurrent computations. --@@ -18,28 +12,38 @@ -- out to the supplied scheduler after each step to determine which -- thread runs next. module Test.DejaFu.Conc-  ( -- * The @ConcT@ monad transformer-    ConcT+  ( -- * Expressing concurrent programs+    Program+  , Basic+  , ConcT   , ConcIO -  -- * Executing computations-  , Condition(..)-  , MemType(..)-  , runConcurrent-  , subconcurrency-  , dontCheck+  -- ** Setup and teardown+  , WithSetup+  , WithSetupAndTeardown+  , withSetup+  , withTeardown+  , withSetupAndTeardown -  -- ** Snapshotting+  -- ** Invariants+  , Invariant+  , registerInvariant+  , inspectIORef+  , inspectMVar+  , inspectTVar -  -- $snapshotting_io+  -- * Executing concurrent programs+  , Snapshot+  , MemType(..)+  , runConcurrent+  , recordSnapshot+  , runSnapshot -  , DCSnapshot-  , runForDCSnapshot-  , runWithDCSnapshot-  , canDCSnapshot-  , threadsFromDCSnapshot+  -- ** Scheduling+  , module Test.DejaFu.Schedule -  -- * Execution traces+  -- * Results+  , Condition(..)   , Trace   , Decision(..)   , ThreadId(..)@@ -50,349 +54,140 @@   , MaskingState(..)   , showTrace   , showCondition--  -- * Scheduling-  , module Test.DejaFu.Schedule--  -- * Deprecated-  , Failure   ) where -import           Control.Exception                   (MaskingState(..))-import qualified Control.Monad.Catch                 as Ca-import           Control.Monad.Fail                  (MonadFail)-import qualified Control.Monad.IO.Class              as IO-import           Control.Monad.Trans.Class           (MonadTrans(..))-import qualified Data.Foldable                       as F-import           Data.List                           (partition)-import qualified Data.Map.Strict                     as M-import           Data.Maybe                          (isNothing)-import           Test.DejaFu.Schedule+import           Control.Exception                 (MaskingState(..)) -import qualified Control.Monad.Conc.Class            as C-import           Test.DejaFu.Conc.Internal import           Test.DejaFu.Conc.Internal.Common-import           Test.DejaFu.Conc.Internal.STM       (ModelSTM)-import           Test.DejaFu.Conc.Internal.Threading (_blocking)-import           Test.DejaFu.Internal+import           Test.DejaFu.Conc.Internal.Program+import           Test.DejaFu.Conc.Internal.STM     (ModelTVar)+import           Test.DejaFu.Schedule import           Test.DejaFu.Types import           Test.DejaFu.Utils +-------------------------------------------------------------------------------+-- Expressing concurrent programs+ -- | @since 1.4.0.0-newtype ConcT n a = C { unC :: ModelConc n a }-  deriving (Functor, Applicative, Monad, MonadFail)+type ConcT = Program Basic  -- | A 'MonadConc' implementation using @IO@. -- -- @since 0.4.0.0 type ConcIO = ConcT IO -toConc :: ((a -> Action n) -> Action n) -> ConcT n a-toConc = C . ModelConc--wrap :: (ModelConc n a -> ModelConc n a) -> ConcT n a -> ConcT n a-wrap f = C . f . unC---- | @since 1.0.0.0-instance IO.MonadIO n => IO.MonadIO (ConcT n) where-  liftIO ma = toConc (\c -> ALift (fmap c (IO.liftIO ma)))--instance MonadTrans ConcT where-  lift ma = toConc (\c -> ALift (fmap c ma))--instance Ca.MonadCatch (ConcT n) where-  catch ma h = toConc (ACatching (unC . h) (unC ma))--instance Ca.MonadThrow (ConcT n) where-  throwM e = toConc (\_ -> AThrow e)--instance Ca.MonadMask (ConcT n) where-  mask                mb = toConc (AMasking MaskedInterruptible   (\f -> unC $ mb $ wrap f))-  uninterruptibleMask mb = toConc (AMasking MaskedUninterruptible (\f -> unC $ mb $ wrap f))--#if MIN_VERSION_exceptions(0,10,0)-  generalBracket acquire release use = Ca.mask $ \unmasked -> do-    resource <- acquire-    b <- unmasked (use resource) `Ca.catch` (\e -> release resource (Ca.ExitCaseException e) >> Ca.throwM e)-    c <- release resource (Ca.ExitCaseSuccess b)-    pure (b, c)-#elif MIN_VERSION_exceptions(0,9,0)-  -- from https://github.com/fpco/stackage/issues/3315#issuecomment-368583481-  generalBracket acquire release cleanup use = Ca.mask $ \unmasked -> do-    resource <- acquire-    result <- unmasked (use resource) `Ca.catch` (\e -> cleanup resource e >> Ca.throwM e)-    _ <- release resource-    pure result-#endif--instance Monad n => C.MonadConc (ConcT n) where-  type MVar     (ConcT n) = ModelMVar n-  type IORef    (ConcT n) = ModelIORef n-  type Ticket   (ConcT n) = ModelTicket-  type STM      (ConcT n) = ModelSTM n-  type ThreadId (ConcT n) = ThreadId--  -- ------------  forkWithUnmaskN   n ma = toConc (AFork n (\umask -> runModelConc (unC $ ma $ wrap umask) (\_ -> AStop (pure ()))))-  forkOnWithUnmaskN n _  = C.forkWithUnmaskN n-  forkOSWithUnmaskN n ma-    | C.rtsSupportsBoundThreads =-      toConc (AForkOS n (\umask -> runModelConc (unC $ ma $ wrap umask) (\_ -> AStop (pure ()))))-    | otherwise = fail "RTS doesn't support multiple OS threads (use ghc -threaded when linking)"--  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.-  getNumCapabilities      = toConc AGetNumCapabilities-  setNumCapabilities caps = toConc (\c -> ASetNumCapabilities caps (c ()))--  myThreadId = toConc AMyTId--  yield = toConc (\c -> AYield (c ()))-  threadDelay n = toConc (\c -> ADelay n (c ()))--  -- ------------  newIORefN n a = toConc (ANewIORef n a)--  readIORef   ref = toConc (AReadIORef    ref)-  readForCAS ref = toConc (AReadIORefCas ref)--  peekTicket' _ = ticketVal--  writeIORef ref      a = toConc (\c -> AWriteIORef ref a (c ()))-  casIORef   ref tick a = toConc (ACasIORef ref tick a)--  atomicModifyIORef ref f = toConc (AModIORef    ref f)-  modifyIORefCAS    ref f = toConc (AModIORefCas ref f)--  -- ------------  newEmptyMVarN n = toConc (ANewMVar n)--  putMVar  var a = toConc (\c -> APutMVar var a (c ()))-  readMVar var   = toConc (AReadMVar var)-  takeMVar var   = toConc (ATakeMVar var)--  tryPutMVar  var a = toConc (ATryPutMVar  var a)-  tryReadMVar var   = toConc (ATryReadMVar var)-  tryTakeMVar var   = toConc (ATryTakeMVar var)--  -- ------------  throwTo tid e = toConc (\c -> AThrowTo tid e (c ()))--  -- ------------  atomically = toConc . AAtom---- | Run a concurrent computation with a given 'Scheduler' and initial--- state, returning either the final result or the condition which--- prevented that. 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!--- You should therefore keep @IO@ blocks small, and only perform--- blocking operations with the supplied primitives, insofar as--- possible.------ __Note:__ In order to prevent computation from hanging, the runtime--- will assume that a deadlock situation has arisen if the scheduler--- attempts to (a) schedule a blocked thread, or (b) schedule a--- nonexistent thread. In either of those cases, the computation will--- be halted.------ @since 1.0.0.0-runConcurrent :: C.MonadConc n-  => Scheduler s-  -> MemType-  -> s-  -> ConcT n a-  -> n (Either Condition a, s, Trace)-runConcurrent sched memtype s ma = do-  res <- runConcurrency False sched memtype s initialIdSource 2 (unC ma)-  out <- efromJust <$> C.readIORef (finalRef res)-  pure ( out-       , cSchedState (finalContext res)-       , F.toList (finalTrace res)-       )+-------------------------------------------------------------------------------+-- Setup & teardown --- | Run a concurrent computation and return its result.+-- | A concurrent program with some set-up action. ----- This can only be called in the main thread, when no other threads--- exist. Calls to 'subconcurrency' cannot be nested, or placed inside--- a call to 'dontCheck'. Violating either of these conditions will--- result in the computation throwing a @NestedSubconcurrency@ or--- @MultithreadedSubconcurrency@ error.+-- In terms of results, this is the same as @setup >>= program@.+-- However, the setup action will be __snapshotted__ (see+-- 'recordSnapshot' and 'runSnapshot') by the testing functions.  This+-- means that even if dejafu runs this program many many times, the+-- setup action will only be run the first time, and its effects+-- remembered for subsequent executions. ----- @since 0.6.0.0-subconcurrency :: ConcT n a -> ConcT n (Either Condition a)-subconcurrency ma = toConc (ASub (unC ma))+-- @since 2.0.0.0+withSetup+  :: Program Basic n x+  -- ^ Setup action+  -> (x -> Program Basic n a)+  -- ^ Main program+  -> Program (WithSetup x) n a+withSetup setup p = WithSetup+  { wsSetup   = setup+  , wsProgram = p+  } --- | Run an arbitrary action which gets some special treatment:------  * For systematic testing, 'dontCheck' is not dependent with---    anything, even if the action has dependencies.------  * For pre-emption bounding, 'dontCheck' counts for zero---    pre-emptions, even if the action performs pre-emptive context---    switches.------  * For fair bounding, 'dontCheck' counts for zero yields/delays,---    even if the action performs yields or delays.+-- | A concurrent program with some set-up and teardown actions. -----  * For length bounding, 'dontCheck' counts for one step, even if---    the action has many.+-- This is similar to -----   * All SCT functions use 'runForDCSnapshot' / 'runWithDCSnapshot'---     to ensure that the action is only executed once, although you---     should be careful with @IO@ (see note on snapshotting @IO@).+-- @+-- do+--   x <- setup+--   y <- program x+--   teardown x y+-- @ ----- The action is executed atomically with a deterministic scheduler--- under sequential consistency.  Any threads created inside the--- action continue to exist in the main computation.+-- But with two differences: ----- This must be the first thing done in the main thread.  Violating--- this condition will result in the computation throwing a--- @LateDontCheck@ exception.+--   * The setup action can be __snapshotted__, as described for+--     'withSetup' ----- If the action does not successfully produce a value (deadlock,--- length bound exceeded, etc), the whole computation is terminated.+--   * The teardown action will be executed even if the main action+--     fails to produce a value. ----- @since 1.1.0.0-dontCheck-  :: Maybe Int-  -- ^ An optional length bound.-  -> ConcT n a-  -- ^ The action to execute.-  -> ConcT n a-dontCheck lb ma = toConc (ADontCheck lb (unC ma))------------------------------------------------------------------------------------ Snapshotting+-- @since 2.0.0.0+withTeardown+  :: (x -> Either Condition y -> Program Basic n a)+  -- ^ Teardown action+  -> Program (WithSetup x) n y+  -- ^ Main program+  -> Program (WithSetupAndTeardown x y) n a+withTeardown teardown ws = WithSetupAndTeardown+  { wstSetup    = wsSetup ws+  , wstProgram  = wsProgram ws+  , wstTeardown = teardown+  } --- $snapshotting_io------ __Snapshotting @IO@:__ A snapshot captures entire state of your--- concurrent program: the state of every thread, the number of--- capabilities, the values of any @IORef@s, @MVar@s, and @TVar@s, and--- records any @IO@ that you performed.------ When restoring a snapshot this @IO@ is replayed, in order.  But the--- whole snapshotted computation is not.  So the effects of the @IO@--- take place again, but any return values are ignored.  For example,--- this program will not do what you want:+-- | A combination of 'withSetup' and 'withTeardown' for convenience. -- -- @--- bad_snapshot = do---   r <- dontCheck Nothing $ do---     r <- liftIO (newIORef 0)---     liftIO (modifyIORef r (+1))---     pure r---   liftIO (readIORef r)+-- withSetupAndTeardown setup teardown =+--   withTeardown teardown . withSetup setup -- @ ----- When the snapshot is taken, the value in the @IORef@ will be 1.--- When the snapshot is restored for the first time, those @IO@--- actions will be run again, /but their return values will be discarded/.--- The value in the @IORef@ will be 2.  When the snapshot--- is restored for the second time, the value in the @IORef@ will be--- 3.  And so on.------ To safely use @IO@ in a snapshotted computation, __the combined effect must be idempotent__.--- You should either use actions which set the state to the final--- value directly, rather than modifying it (eg, using a combination--- of @liftIO . readIORef@ and @liftIO . writeIORef@ here), or reset--- the state to a known value.  Both of these approaches will work:+-- @since 2.0.0.0+withSetupAndTeardown+  :: Program Basic n x+  -- ^ Setup action+  -> (x -> Either Condition y -> Program Basic n a)+  -- ^ Teardown action+  -> (x -> Program Basic n y)+  -- ^ Main program+  -> Program (WithSetupAndTeardown x y) n a+withSetupAndTeardown setup teardown =+  withTeardown teardown . withSetup setup++-------------------------------------------------------------------------------+-- Invariants++-- | Call this in the setup phase to register new invariant which will+-- be checked after every scheduling point in the main phase.+-- Invariants are atomic actions which can inspect the shared state of+-- your computation. ----- @--- good_snapshot1 = do---   r <- dontCheck Nothing $ do---     let modify r f = liftIO (readIORef r) >>= liftIO . writeIORef r . f---     r <- liftIO (newIORef 0)---     modify r (+1)---     pure r---   liftIO (readIORef r)+-- If the invariant throws an exception, the execution will be aborted+-- with n @InvariantFailure@.  Any teardown action will still be run. ----- good_snapshot2 = do---   r <- dontCheck Nothing $ do---     r <- liftIO (newIORef 0)---     liftIO (writeIORef r 0)---     liftIO (modifyIORef r (+1))---     pure r---   liftIO (readIORef r)--- @+-- @since 2.0.0.0+registerInvariant :: Invariant n a -> Program Basic n ()+registerInvariant inv = ModelConc (\c -> ANewInvariant (() <$ inv) (c ())) --- | Like 'runConcurrent', but terminates immediately after running--- the 'dontCheck' action with a 'DCSnapshot' which can be used in--- 'runWithDCSnapshot' to avoid doing that work again.------ If this program does not contain a legal use of 'dontCheck', then--- the result will be @Nothing@.+-- | Read the content of an @IORef@. ----- If you are using the SCT functions on an action which contains a--- 'dontCheck', snapshotting will be handled for you, without you--- needing to call this function yourself.+-- This returns the globally visible value, which may not be the same+-- as the value visible to any particular thread when using a memory+-- model other than 'SequentialConsistency'. ----- @since 1.1.0.0-runForDCSnapshot :: C.MonadConc n-  => ConcT n a-  -> n (Maybe (Either Condition (DCSnapshot n a), Trace))-runForDCSnapshot ma = do-  res <- runConcurrency True roundRobinSchedNP SequentialConsistency () initialIdSource 2 (unC ma)-  out <- C.readIORef (finalRef res)-  pure $ case (finalRestore res, out) of-    (Just _, Just (Left f)) -> Just (Left f, F.toList (finalTrace res))-    (Just restore, _) -> Just (Right (DCSnapshot (finalContext res) restore (finalRef res)), F.toList (finalTrace res))-    (_, _) -> Nothing+-- @since 2.0.0.0+inspectIORef :: ModelIORef n a -> Invariant n a+inspectIORef = Invariant . IInspectIORef --- | Like 'runConcurrent', but uses a 'DCSnapshot' produced by--- 'runForDCSnapshot' to skip the 'dontCheck' work.+-- | Read the content of an @MVar@. ----- If you are using the SCT functions on an action which contains a--- 'dontCheck', snapshotting will be handled for you, without you--- needing to call this function yourself.+-- This is essentially @tryReadMVar@. ----- @since 1.1.0.0-runWithDCSnapshot :: C.MonadConc n-  => Scheduler s-  -> MemType-  -> s-  -> DCSnapshot n a-  -> n (Either Condition a, s, Trace)-runWithDCSnapshot sched memtype s snapshot = do-  let context = (dcsContext snapshot) { cSchedState = s }-  let restore = dcsRestore snapshot-  let ref = dcsRef snapshot-  res <- runConcurrencyWithSnapshot sched memtype context restore ref-  out <- efromJust <$> C.readIORef (finalRef res)-  pure ( out-       , cSchedState (finalContext res)-       , F.toList (finalTrace res)-       )+-- @since 2.0.0.0+inspectMVar :: ModelMVar n a -> Invariant n (Maybe a)+inspectMVar = Invariant . IInspectMVar --- | Check if a 'DCSnapshot' can be taken from this computation.+-- | Read the content of a @TVar@. ----- @since 1.1.0.0-canDCSnapshot :: ConcT n a -> Bool-canDCSnapshot (C (ModelConc k)) = lookahead (k undefined) == WillDontCheck---- | Get the threads which exist in a snapshot, partitioned into--- runnable and not runnable.+-- This is essentially @readTVar@. ----- @since 1.1.0.0-threadsFromDCSnapshot :: DCSnapshot n a -> ([ThreadId], [ThreadId])-threadsFromDCSnapshot snapshot = partition isRunnable (M.keys threads) where-  threads = cThreads (dcsContext snapshot)-  isRunnable tid = isNothing (_blocking =<< M.lookup tid threads)+-- @since 2.0.0.0+inspectTVar :: ModelTVar n a -> Invariant n a+inspectTVar = Invariant . IInspectTVar

@@ -1,4 +1,5 @@ {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-}@@ -9,7 +10,7 @@ -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : FlexibleContexts, MultiWayIf, RankNTypes, RecordWildCards+-- Portability : FlexibleContexts, LambdaCase, MultiWayIf, RankNTypes, RecordWildCards -- -- Concurrent monads with a fixed scheduler: internal types and -- functions. This module is NOT considered to form part of the public@@ -21,14 +22,13 @@                                                       toException) import qualified Control.Monad.Catch                 as E import qualified Control.Monad.Conc.Class            as C-import           Data.Foldable                       (foldrM, toList)+import           Data.Foldable                       (foldrM) import           Data.Functor                        (void)-import           Data.List                           (sortOn)+import           Data.List                           (nub, partition, sortOn) import qualified Data.Map.Strict                     as M-import           Data.Maybe                          (fromMaybe, isJust,-                                                      isNothing)+import           Data.Maybe                          (isJust, isNothing) import           Data.Monoid                         ((<>))-import           Data.Sequence                       (Seq, (<|))+import           Data.Sequence                       (Seq) import qualified Data.Sequence                       as Seq import           GHC.Stack                           (HasCallStack) @@ -51,32 +51,19 @@ data CResult n g a = CResult   { finalContext :: Context n g   , finalRef :: C.IORef n (Maybe (Either Condition a))-  , finalRestore :: Maybe (Threads n -> n ())+  , finalRestore :: Threads n -> n ()   -- ^ Meaningless if this result doesn't come from a snapshotting   -- execution.   , finalTrace :: SeqTrace   , finalDecision :: Maybe (ThreadId, ThreadAction)   } --- | A snapshot of the concurrency state immediately after 'dontCheck'--- finishes.------ @since 1.4.0.0-data DCSnapshot n a = DCSnapshot-  { dcsContext :: Context n ()-  -- ^ The execution context.  The scheduler state is ignored when-  -- restoring.-  , dcsRestore :: Threads n -> n ()-  -- ^ Action to restore IORef, MVar, and TVar values.-  , dcsRef :: C.IORef n (Maybe (Either Condition a))-  -- ^ Reference where the result will be written.-  }- -- | Run a concurrent computation with a given 'Scheduler' and initial -- state, returning a Condition reason on error. Also returned is the -- final state of the scheduler, and an execution trace. runConcurrency :: (C.MonadConc n, HasCallStack)-  => Bool+  => [Invariant n ()]+  -> Bool   -> Scheduler g   -> MemType   -> g@@ -84,34 +71,22 @@   -> Int   -> ModelConc n a   -> n (CResult n g a)-runConcurrency forSnapshot sched memtype g idsrc caps ma = do-  let ctx = Context { cSchedState = g-                    , cIdSource   = idsrc-                    , cThreads    = M.empty-                    , cWriteBuf   = emptyBuffer-                    , cCaps       = caps+runConcurrency invariants forSnapshot sched memtype g idsrc caps ma = do+  let ctx = Context { cSchedState    = g+                    , cIdSource      = idsrc+                    , cThreads       = M.empty+                    , cWriteBuf      = emptyBuffer+                    , cCaps          = caps+                    , cInvariants    = InvariantContext { icActive = invariants, icBlocked = [] }+                    , cNewInvariants = []+                    , cCState        = initialCState                     }-  res <- runConcurrency' forSnapshot sched memtype ctx ma-  killAllThreads (finalContext res)-  pure res---- | Run a concurrent program using the given context, and without--- killing threads which remain at the end.  The context must have no--- main thread.------ Only a separate function because @ADontCheck@ needs it.-runConcurrency' :: (C.MonadConc n, HasCallStack)-  => Bool-  -> Scheduler g-  -> MemType-  -> Context n g-  -> ModelConc n a-  -> n (CResult n g a)-runConcurrency' forSnapshot sched memtype ctx ma = do   (c, ref) <- runRefCont AStop (Just . Right) (runModelConc ma)   let threads0 = launch' Unmasked initialThread (const c) (cThreads ctx)   threads <- (if C.rtsSupportsBoundThreads then makeBound initialThread else pure) threads0-  runThreads forSnapshot sched memtype ref ctx { cThreads = threads }+  res <- runThreads forSnapshot sched memtype ref ctx { cThreads = threads }+  killAllThreads (finalContext res)+  pure res  -- | Like 'runConcurrency' but starts from a snapshot. runConcurrencyWithSnapshot :: (C.MonadConc n, HasCallStack)@@ -119,13 +94,17 @@   -> MemType   -> Context n g   -> (Threads n -> n ())-  -> C.IORef n (Maybe (Either Condition a))+  -> ModelConc n a   -> n (CResult n g a)-runConcurrencyWithSnapshot sched memtype ctx restore ref = do-  let boundThreads = M.filter (isJust . _bound) (cThreads ctx)-  threads <- foldrM makeBound (cThreads ctx) (M.keys boundThreads)-  restore threads-  res <- runThreads False sched memtype ref ctx { cThreads = threads }+runConcurrencyWithSnapshot sched memtype ctx restore ma = do+  (c, ref) <- runRefCont AStop (Just . Right) (runModelConc ma)+  let threads0 = M.delete initialThread (cThreads ctx)+  let threads1 = launch' Unmasked initialThread (const c) threads0+  let boundThreads = M.filter (isJust . _bound) threads1+  threads2 <- (if C.rtsSupportsBoundThreads then makeBound initialThread else pure) threads1+  threads3 <- foldrM makeBound threads2 (M.keys boundThreads)+  restore threads3+  res <- runThreads False sched memtype ref ctx { cThreads = threads3 }   killAllThreads (finalContext res)   pure res @@ -140,11 +119,14 @@  -- | The context a collection of threads are running in. data Context n g = Context-  { cSchedState :: g-  , cIdSource   :: IdSource-  , cThreads    :: Threads n-  , cWriteBuf   :: WriteBuffer n-  , cCaps       :: Int+  { cSchedState    :: g+  , cIdSource      :: IdSource+  , cThreads       :: Threads n+  , cWriteBuf      :: WriteBuffer n+  , cCaps          :: Int+  , cInvariants    :: InvariantContext n+  , cNewInvariants :: [Invariant n ()]+  , cCState        :: ConcurrencyState   }  -- | Run a collection of threads, until there are no threads left.@@ -166,7 +148,7 @@   stop finalR finalT finalD finalC = pure CResult     { finalContext  = finalC     , finalRef      = ref-    , finalRestore  = if forSnapshot then Just finalR else Nothing+    , finalRestore  = finalR     , finalTrace    = finalT     , finalDecision = finalD     }@@ -175,7 +157,6 @@   schedule restore sofar prior ctx     | isTerminated  = stop restore sofar prior ctx     | isDeadlocked  = die Deadlock restore sofar prior ctx-    | isSTMLocked   = die STMDeadlock restore sofar prior ctx     | otherwise =       let ctx' = ctx { cSchedState = g' }       in case choice of@@ -192,19 +173,14 @@              Nothing -> E.throwM ScheduledMissingThread            Nothing -> die Abort restore sofar prior ctx'     where-      (choice, g')  = scheduleThread sched prior (efromList runnable') (cSchedState ctx)+      (choice, g')  = scheduleThread sched prior (efromList runnable') (cCState ctx) (cSchedState ctx)       runnable'     = [(t, lookahead (_continuation a)) | (t, a) <- sortOn fst $ M.assocs runnable]       runnable      = M.filter (not . isBlocked) threadsc       threadsc      = addCommitThreads (cWriteBuf ctx) threads       threads       = cThreads ctx       isBlocked     = isJust . _blocking       isTerminated  = initialThread `notElem` M.keys threads-      isDeadlocked  = M.null (M.filter (not . isBlocked) threads) &&-        (((~=  OnMVarFull  undefined) <$> M.lookup initialThread threads) == Just True ||-         ((~=  OnMVarEmpty undefined) <$> M.lookup initialThread threads) == Just True ||-         ((~=  OnMask      undefined) <$> M.lookup initialThread threads) == Just True)-      isSTMLocked = M.null (M.filter (not . isBlocked) threads) &&-        ((~=  OnTVar []) <$> M.lookup initialThread threads) == Just True+      isDeadlocked  = M.null (M.filter (not . isBlocked) threads)    -- run the chosen thread for one step and then pass control back to   -- 'schedule'@@ -223,33 +199,36 @@             if forSnapshot             then restore threads' >> actionSnap threads'             else restore threads'-      let ctx' = fixContext chosen res ctx+      let ctx' = fixContext memtype chosen actOrTrc res ctx       case res of-        Succeeded _ ->-          schedule restore' sofar' prior' ctx'+        Succeeded _ -> checkInvariants (cInvariants ctx') >>= \case+          Right ic ->+            schedule restore' sofar' prior' ctx' { cInvariants = ic }+          Left exc ->+            die (InvariantFailure exc) restore' sofar' prior' ctx'         Failed failure ->           die failure restore' sofar' prior' ctx'-        Snap _ ->-          stop actionSnap sofar' prior' ctx'     where-      getTrc (Single a) = Seq.singleton (decision, alternatives, a)-      getTrc (SubC as _) = (decision, alternatives, Subconcurrency) <| as+      getTrc a = Seq.singleton (decision, alternatives, a) -      getPrior (Single a) = Just (chosen, a)-      getPrior (SubC _ finalD) = finalD+      getPrior a = Just (chosen, a)  -- | Apply the context update from stepping an action.-fixContext :: ThreadId -> What n g -> Context n g -> Context n g-fixContext chosen (Succeeded ctx@Context{..}) _ =-  ctx { cThreads = delCommitThreads $-        if (interruptible <$> M.lookup chosen cThreads) /= Just False-        then unblockWaitingOn chosen cThreads-        else cThreads+fixContext :: MemType -> ThreadId -> ThreadAction -> What n g -> Context n g -> Context n g+fixContext memtype tid act what ctx0 = fixContextCommon $ case what of+    Succeeded ctx@Context{..} -> ctx+      { cThreads =+          if (interruptible <$> M.lookup tid cThreads) /= Just False+          then unblockWaitingOn tid cThreads+          else cThreads       }-fixContext _ (Failed _) ctx@Context{..} =-  ctx { cThreads = delCommitThreads cThreads }-fixContext _ (Snap ctx@Context{..}) _ =-  ctx { cThreads = delCommitThreads cThreads }+    _ -> ctx0+  where+  fixContextCommon ctx@Context{..} = ctx+    { cThreads    = delCommitThreads cThreads+    , cInvariants = unblockInvariants act cInvariants+    , cCState     = updateCState memtype cCState tid act+    }  -- | @unblockWaitingOn tid@ unblocks every thread blocked in a -- @throwTo tid@.@@ -261,22 +240,12 @@ -------------------------------------------------------------------------------- -- * Single-step execution --- | What a thread did, for trace purposes.-data Act-  = Single ThreadAction-  -- ^ Just one action.-  | SubC SeqTrace (Maybe (ThreadId, ThreadAction))-  -- ^ @subconcurrency@, with the given trace and final action.-  deriving (Eq, Show)- -- | What a thread did, for execution purposes. data What n g   = Succeeded (Context n g)   -- ^ Action succeeded: continue execution.   | Failed Condition   -- ^ Action caused computation to fail: stop.-  | Snap (Context n g)-  -- ^ Action was a snapshot point and we're in snapshot mode: stop.  -- | Run a single thread one step, by dispatching on the type of -- 'Action'.@@ -302,13 +271,13 @@   -- ^ Action to step   -> Context n g   -- ^ The execution context.-  -> n (What n g, Act, Threads n -> n ())+  -> n (What n g, ThreadAction, Threads n -> n ()) -- start a new thread, assigning it the next 'ThreadId' stepThread _ _ _ _ tid (AFork n a b) = \ctx@Context{..} -> pure $   let (idSource', newtid) = nextTId n cIdSource       threads' = launch tid newtid a cThreads   in ( Succeeded ctx { cThreads = goto (b newtid) tid threads', cIdSource = idSource' }-     , Single (Fork newtid)+     , Fork newtid      , const (pure ())      ) @@ -318,7 +287,7 @@   let threads' = launch tid newtid a cThreads   threads'' <- makeBound newtid threads'   pure ( Succeeded ctx { cThreads = goto (b newtid) tid threads'', cIdSource = idSource' }-       , Single (ForkOS newtid)+       , ForkOS newtid        , const (pure ())        ) @@ -326,42 +295,42 @@ stepThread _ _ _ _ tid (AIsBound c) = \ctx@Context{..} -> do   let isBound = isJust . _bound $ elookup tid cThreads   pure ( Succeeded ctx { cThreads = goto (c isBound) tid cThreads }-       , Single (IsCurrentThreadBound isBound)+       , IsCurrentThreadBound isBound        , const (pure ())        )  -- get the 'ThreadId' of the current thread stepThread _ _ _ _ tid (AMyTId c) = \ctx@Context{..} ->   pure ( Succeeded ctx { cThreads = goto (c tid) tid cThreads }-       , Single MyThreadId+       , MyThreadId        , const (pure ())        )  -- get the number of capabilities stepThread _ _ _ _ tid (AGetNumCapabilities c) = \ctx@Context{..} ->   pure ( Succeeded ctx { cThreads = goto (c cCaps) tid cThreads }-       , Single (GetNumCapabilities cCaps)+       , GetNumCapabilities cCaps        , const (pure ())        )  -- set the number of capabilities stepThread _ _ _ _ tid (ASetNumCapabilities i c) = \ctx@Context{..} ->   pure ( Succeeded ctx { cThreads = goto c tid cThreads, cCaps = i }-       , Single (SetNumCapabilities i)+       , SetNumCapabilities i        , const (pure ())        )  -- yield the current thread stepThread _ _ _ _ tid (AYield c) = \ctx@Context{..} ->   pure ( Succeeded ctx { cThreads = goto c tid cThreads }-       , Single Yield+       , Yield        , const (pure ())        )  -- yield the current thread (delay is ignored) stepThread _ _ _ _ tid (ADelay n c) = \ctx@Context{..} ->   pure ( Succeeded ctx { cThreads = goto c tid cThreads }-       , Single (ThreadDelay n)+       , ThreadDelay n        , const (pure ())        ) @@ -371,7 +340,7 @@   ref <- C.newIORef Nothing   let mvar = ModelMVar newmvid ref   pure ( Succeeded ctx { cThreads = goto (c mvar) tid cThreads, cIdSource = idSource' }-       , Single (NewMVar newmvid)+       , NewMVar newmvid        , const (C.writeIORef ref Nothing)        ) @@ -379,7 +348,7 @@ stepThread _ _ _ _ tid (APutMVar mvar@ModelMVar{..} a c) = synchronised $ \ctx@Context{..} -> do   (success, threads', woken, effect) <- putIntoMVar mvar a c tid cThreads   pure ( Succeeded ctx { cThreads = threads' }-       , Single (if success then PutMVar mvarId woken else BlockedPutMVar mvarId)+       , if success then PutMVar mvarId woken else BlockedPutMVar mvarId        , const effect        ) @@ -387,7 +356,7 @@ stepThread _ _ _ _ tid (ATryPutMVar mvar@ModelMVar{..} a c) = synchronised $ \ctx@Context{..} -> do   (success, threads', woken, effect) <- tryPutIntoMVar mvar a c tid cThreads   pure ( Succeeded ctx { cThreads = threads' }-       , Single (TryPutMVar mvarId success woken)+       , TryPutMVar mvarId success woken        , const effect        ) @@ -396,7 +365,7 @@ stepThread _ _ _ _ tid (AReadMVar mvar@ModelMVar{..} c) = synchronised $ \ctx@Context{..} -> do   (success, threads', _, _) <- readFromMVar mvar c tid cThreads   pure ( Succeeded ctx { cThreads = threads' }-       , Single (if success then ReadMVar mvarId else BlockedReadMVar mvarId)+       , if success then ReadMVar mvarId else BlockedReadMVar mvarId        , const (pure ())        ) @@ -405,7 +374,7 @@ stepThread _ _ _ _ tid (ATryReadMVar mvar@ModelMVar{..} c) = synchronised $ \ctx@Context{..} -> do   (success, threads', _, _) <- tryReadFromMVar mvar c tid cThreads   pure ( Succeeded ctx { cThreads = threads' }-       , Single (TryReadMVar mvarId success)+       , TryReadMVar mvarId success        , const (pure ())        ) @@ -413,7 +382,7 @@ stepThread _ _ _ _ tid (ATakeMVar mvar@ModelMVar{..} c) = synchronised $ \ctx@Context{..} -> do   (success, threads', woken, effect) <- takeFromMVar mvar c tid cThreads   pure ( Succeeded ctx { cThreads = threads' }-       , Single (if success then TakeMVar mvarId woken else BlockedTakeMVar mvarId)+       , if success then TakeMVar mvarId woken else BlockedTakeMVar mvarId        , const effect        ) @@ -421,7 +390,7 @@ stepThread _ _ _ _ tid (ATryTakeMVar mvar@ModelMVar{..} c) = synchronised $ \ctx@Context{..} -> do   (success, threads', woken, effect) <- tryTakeFromMVar mvar c tid cThreads   pure ( Succeeded ctx { cThreads = threads' }-       , Single (TryTakeMVar mvarId success woken)+       , TryTakeMVar mvarId success woken        , const effect        ) @@ -432,7 +401,7 @@   ioref <- C.newIORef val   let ref = ModelIORef newiorid ioref   pure ( Succeeded ctx { cThreads = goto (c ref) tid cThreads, cIdSource = idSource' }-       , Single (NewIORef newiorid)+       , NewIORef newiorid        , const (C.writeIORef ioref val)        ) @@ -440,7 +409,7 @@ stepThread _ _ _ _  tid (AReadIORef ref@ModelIORef{..} c) = \ctx@Context{..} -> do   val <- readIORef ref tid   pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads }-       , Single (ReadIORef iorefId)+       , ReadIORef iorefId        , const (pure ())        ) @@ -448,7 +417,7 @@ stepThread _ _ _ _ tid (AReadIORefCas ref@ModelIORef{..} c) = \ctx@Context{..} -> do   tick <- readForTicket ref tid   pure ( Succeeded ctx { cThreads = goto (c tick) tid cThreads }-       , Single (ReadIORefCas iorefId)+       , ReadIORefCas iorefId        , const (pure ())        ) @@ -457,7 +426,7 @@   (new, val) <- f <$> readIORef ref tid   effect <- writeImmediate ref new   pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads }-       , Single (ModIORef iorefId)+       , ModIORef iorefId        , const effect        ) @@ -467,7 +436,7 @@   let (new, val) = f old   (_, _, effect) <- casIORef ref tid tick new   pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads }-       , Single (ModIORefCas iorefId)+       , ModIORefCas iorefId        , const effect        ) @@ -477,21 +446,21 @@   SequentialConsistency -> do     effect <- writeImmediate ref a     pure ( Succeeded ctx { cThreads = goto c tid cThreads }-         , Single (WriteIORef iorefId)+         , WriteIORef iorefId          , const effect          )   -- add to buffer using thread id.   TotalStoreOrder -> do     wb' <- bufferWrite cWriteBuf (tid, Nothing) ref a     pure ( Succeeded ctx { cThreads = goto c tid cThreads, cWriteBuf = wb' }-         , Single (WriteIORef iorefId)+         , WriteIORef iorefId          , const (pure ())          )   -- add to buffer using both thread id and IORef id   PartialStoreOrder -> do     wb' <- bufferWrite cWriteBuf (tid, Just iorefId) ref a     pure ( Succeeded ctx { cThreads = goto c tid cThreads, cWriteBuf = wb' }-         , Single (WriteIORef iorefId)+         , WriteIORef iorefId          , const (pure ())          ) @@ -499,7 +468,7 @@ stepThread _ _ _ _ tid (ACasIORef ref@ModelIORef{..} tick a c) = synchronised $ \ctx@Context{..} -> do   (suc, tick', effect) <- casIORef ref tid tick a   pure ( Succeeded ctx { cThreads = goto (c (suc, tick')) tid cThreads }-       , Single (CasIORef iorefId suc)+       , CasIORef iorefId suc        , const effect        ) @@ -516,7 +485,7 @@     PartialStoreOrder ->       commitWrite cWriteBuf (t, Just c)   pure ( Succeeded ctx { cWriteBuf = wb' }-       , Single (CommitIORef t c)+       , CommitIORef t c        , const (pure ())        ) @@ -529,22 +498,21 @@     Success _ written val -> do       let (threads', woken) = wake (OnTVar written) cThreads       pure ( Succeeded ctx { cThreads = goto (c val) tid threads', cIdSource = idSource' }-           , Single (STM trace woken)+           , STM trace woken            , effect            )     Retry touched -> do       let threads' = block (OnTVar touched) tid cThreads       pure ( Succeeded ctx { cThreads = threads', cIdSource = idSource'}-           , Single (BlockedSTM trace)+           , BlockedSTM trace            , effect            )     Exception e -> do       let act = STM trace []       res' <- stepThrow (const act) tid e ctx       pure $ case res' of-        (Succeeded ctx', _, effect') -> (Succeeded ctx' { cIdSource = idSource' }, Single act, effect')-        (Failed err, _, effect') -> (Failed err, Single act, effect')-        (Snap _, _, _) -> fatal "stepThread.AAtom" "Unexpected snapshot while propagating STM exception"+        (Succeeded ctx', _, effect') -> (Succeeded ctx' { cIdSource = idSource' }, act, effect')+        (Failed err, _, effect') -> (Failed err, act, effect')  -- lift an action from the underlying monad into the @Conc@ -- computation.@@ -552,7 +520,7 @@   let effect threads = runLiftedAct tid threads na   a <- effect cThreads   pure (Succeeded ctx { cThreads = goto a tid cThreads }-       , Single LiftIO+       , LiftIO        , void <$> effect        ) @@ -569,12 +537,12 @@          | interruptible thread -> stepThrow (ThrowTo t) t e ctx { cThreads = threads' }          | otherwise -> pure            ( Succeeded ctx { cThreads = blocked }-           , Single (BlockedThrowTo t)+           , BlockedThrowTo t            , const (pure ())            )        Nothing -> pure          (Succeeded ctx { cThreads = threads' }-         , Single (ThrowTo t False)+         , ThrowTo t False          , const (pure ())          ) @@ -583,14 +551,14 @@   let a     = runModelConc ma (APopCatching . c)       e exc = runModelConc (h exc) c   in ( Succeeded ctx { cThreads = goto a tid (catching e tid cThreads) }-     , Single Catching+     , Catching      , const (pure ())      )  -- pop the top exception handler from the thread's stack. stepThread _ _ _ _ tid (APopCatching a) = \ctx@Context{..} ->   pure ( Succeeded ctx { cThreads = goto a tid (uncatching tid cThreads) }-       , Single PopCatching+       , PopCatching        , const (pure ())        ) @@ -602,21 +570,21 @@       m' = _masking $ elookup tid cThreads       a  = runModelConc (ma umask) (AResetMask False False m' . c)   in ( Succeeded ctx { cThreads = goto a tid (mask m tid cThreads) }-     , Single (SetMasking False m)+     , SetMasking False m      , const (pure ())      )  -- reset the masking thread of the state. stepThread _ _ _ _ tid (AResetMask b1 b2 m c) = \ctx@Context{..} ->   pure ( Succeeded ctx { cThreads = goto c tid (mask m tid cThreads) }-       , Single ((if b1 then SetMasking else ResetMasking) b2 m)+       , (if b1 then SetMasking else ResetMasking) b2 m        , const (pure ())        )  -- execute a 'return' or 'pure'. stepThread _ _ _ _ tid (AReturn c) = \ctx@Context{..} ->   pure ( Succeeded ctx { cThreads = goto c tid cThreads }-       , Single Return+       , Return        , const (pure ())        ) @@ -625,61 +593,20 @@   na   threads' <- kill tid cThreads   pure ( Succeeded ctx { cThreads = threads' }-       , Single Stop+       , Stop        , const (pure ())        ) --- run a subconcurrent computation.-stepThread forSnapshot _ sched memtype tid (ASub ma c) = \ctx ->-  if | forSnapshot -> E.throwM NestedSubconcurrency-     | M.size (cThreads ctx) > 1 -> E.throwM MultithreadedSubconcurrency-     | otherwise -> do-         res <- runConcurrency False sched memtype (cSchedState ctx) (cIdSource ctx) (cCaps ctx) ma-         out <- efromJust <$> C.readIORef (finalRef res)-         pure ( Succeeded ctx-                { cThreads    = goto (AStopSub (c out)) tid (cThreads ctx)-                , cIdSource   = cIdSource (finalContext res)-                , cSchedState = cSchedState (finalContext res)-                }-              , SubC (finalTrace res) (finalDecision res)-              , const (pure ())-              )---- after the end of a subconcurrent computation. does nothing, only--- exists so that: there is an entry in the trace for returning to--- normal computation; and every item in the trace corresponds to a--- scheduling point.-stepThread _ _ _ _ tid (AStopSub c) = \ctx@Context{..} ->-  pure ( Succeeded ctx { cThreads = goto c tid cThreads }-       , Single StopSubconcurrency+-- register an invariant to be checked in the next execution+stepThread _ _ _ _ tid (ANewInvariant inv c) = \ctx@Context{..} ->+  pure ( Succeeded ctx+         { cThreads = goto c tid cThreads+         , cNewInvariants = inv : cNewInvariants+         }+       , RegisterInvariant        , const (pure ())        ) --- run an action atomically, with a non-preemptive length bounded--- round robin scheduler, under sequential consistency.-stepThread forSnapshot isFirst _ _ tid (ADontCheck lb ma c) = \ctx ->-  if | isFirst -> do-         -- create a restricted context-         threads' <- kill tid (cThreads ctx)-         let dcCtx = ctx { cThreads = threads', cSchedState = lb }-         res <- runConcurrency' forSnapshot dcSched SequentialConsistency dcCtx ma-         out <- efromJust <$> C.readIORef (finalRef res)-         case out of-           Right a -> do-             let threads'' = launch' Unmasked tid (const (c a)) (cThreads (finalContext res))-             threads''' <- (if C.rtsSupportsBoundThreads then makeBound tid else pure) threads''-             pure ( (if forSnapshot then Snap else Succeeded) (finalContext res)-                    { cThreads = threads''', cSchedState = cSchedState ctx }-                  , Single (DontCheck (toList (finalTrace res)))-                  , fromMaybe (const (pure ())) (finalRestore res)-                  )-           Left f -> pure-             ( Failed f-             , Single (DontCheck (toList (finalTrace res)))-             , const (pure ())-             )-     | otherwise -> E.throwM LateDontCheck- -- | Handle an exception being thrown from an @AAtom@, @AThrow@, or -- @AThrowTo@. stepThrow :: (C.MonadConc n, Exception e)@@ -691,23 +618,23 @@   -- ^ Exception to raise.   -> Context n g   -- ^ The execution context.-  -> n (What n g, Act, Threads n -> n ())+  -> n (What n g, ThreadAction, Threads n -> n ()) stepThrow act tid e ctx@Context{..} = case propagate some tid cThreads of     Just ts' -> pure       ( Succeeded ctx { cThreads = ts' }-      , Single (act False)+      , act False       , const (pure ())       )     Nothing       | tid == initialThread -> pure         ( Failed (UncaughtException some)-        , Single (act True)+        , act True         , const (pure ())         )       | otherwise -> do           ts' <- kill tid cThreads           pure ( Succeeded ctx { cThreads = ts' }-               , Single (act True)+               , act True                , const (pure ())                )   where@@ -715,19 +642,107 @@  -- | Helper for actions impose a write barrier. synchronised :: C.MonadConc n-  => (Context n g -> n (What n g, Act, Threads n -> n ()))+  => (Context n g -> n x)   -- ^ Action to run after the write barrier.   -> Context n g   -- ^ The original execution context.-  -> n (What n g, Act, Threads n -> n ())+  -> n x synchronised ma ctx@Context{..} = do   writeBarrier cWriteBuf   ma ctx { cWriteBuf = emptyBuffer } --- | scheduler for @ADontCheck@-dcSched :: Scheduler (Maybe Int)-dcSched = Scheduler go where-  go _ _ (Just 0) = (Nothing, Just 0)-  go prior threads s =-    let (t, _) = scheduleThread roundRobinSchedNP prior threads ()-    in (t, fmap (\lb -> lb - 1) s)+--------------------------------------------------------------------------------+-- * Invariants++-- | The state of the invariants+data InvariantContext n = InvariantContext+  { icActive  :: [Invariant n ()]+  , icBlocked :: [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]+  }++-- | @unblockInvariants act@ unblocks every invariant which could have+-- its result changed by @act@.+unblockInvariants ::  ThreadAction -> InvariantContext n -> InvariantContext n+unblockInvariants act ic = InvariantContext active blocked where+  active = map fst unblocked ++ icActive ic++  (unblocked, blocked) = (`partition` icBlocked ic) $+    \(_, (ioridsB, mvidsB, tvidsB)) ->+      maybe False (`elem` ioridsB) (iorefOf (simplifyAction act)) ||+      maybe False (`elem` mvidsB)  (mvarOf (simplifyAction act))  ||+      any (`elem` tvidsB) (tvarsOf act)++-- | Check all active invariants, returning an arbitrary failure if+-- multiple ones fail.+checkInvariants :: C.MonadConc n+  => InvariantContext n+  -> n (Either E.SomeException (InvariantContext n))+checkInvariants ic = go (icActive ic) >>= \case+    Right blocked -> pure (Right (InvariantContext [] (blocked ++ icBlocked ic)))+    Left exc -> pure (Left exc)+  where+    go (inv:is) = checkInvariant inv >>= \case+      Right o -> fmap ((inv,o):) <$> go is+      Left exc -> pure (Left exc)+    go [] = pure (Right [])++-- | Check an invariant.+checkInvariant :: C.MonadConc n+  => Invariant n a+  -> n (Either E.SomeException ([IORefId], [MVarId], [TVarId]))+checkInvariant inv = doInvariant inv >>= \case+  (Right _, iorefs, mvars, tvars) -> pure (Right (iorefs, mvars, tvars))+  (Left exc, _, _, _) -> pure (Left exc)++-- | Run an invariant (more primitive)+doInvariant :: C.MonadConc n+  => Invariant n a+  -> n (Either E.SomeException a, [IORefId], [MVarId], [TVarId])+doInvariant inv = do+    (c, ref) <- runRefCont IStop (Just . Right) (runInvariant inv)+    (iorefs, mvars, tvars) <- go ref c [] [] []+    val <- C.readIORef ref+    pure (efromJust val, nub iorefs, nub mvars, nub tvars)+  where+    go ref act iorefs mvars tvars = do+      (res, iorefs', mvars', tvars') <- stepInvariant act+      let newIORefs = iorefs' ++ iorefs+      let newMVars  = mvars'  ++ mvars+      let newTVars  = tvars'  ++ tvars+      case res of+        Right (Just act') ->+          go ref act' newIORefs newMVars newTVars+        Right Nothing ->+          pure (newIORefs, newMVars, newTVars)+        Left exc -> do+          C.writeIORef ref (Just (Left exc))+          pure (newIORefs, newMVars, newTVars)++-- | Run an invariant for one step+stepInvariant :: C.MonadConc n+  => IAction n+  -> n (Either E.SomeException (Maybe (IAction n)), [IORefId], [MVarId], [TVarId])+stepInvariant (IInspectIORef ioref@ModelIORef{..} k) = do+  a <- readIORefGlobal ioref+  pure (Right (Just (k a)), [iorefId], [], [])+stepInvariant (IInspectMVar ModelMVar{..} k) = do+  a <- C.readIORef mvarRef+  pure (Right (Just (k a)), [], [mvarId], [])+stepInvariant (IInspectTVar ModelTVar{..} k) = do+  a <- C.readIORef tvarRef+  pure (Right (Just (k a)), [], [], [tvarId])+stepInvariant (ICatch h nx k) = doInvariant nx >>= \case+  (Right a, iorefs, mvars, tvars) ->+    pure (Right (Just (k a)), iorefs, mvars, tvars)+  (Left exc, iorefs, mvars, tvars) -> case E.fromException exc of+    Just exc' -> doInvariant (h exc') >>= \case+      (Right a, iorefs', mvars', tvars') ->+        pure (Right (Just (k a)), iorefs' ++ iorefs, mvars' ++ mvars, tvars' ++ tvars)+      (Left exc'', iorefs', mvars', tvars') ->+        pure (Left exc'', iorefs' ++ iorefs, mvars' ++ mvars, tvars' ++ tvars)+    Nothing -> pure (Left exc, iorefs, mvars, tvars)+stepInvariant (IThrow exc) =+  pure (Left (toException exc), [], [], [])+stepInvariant (IStop finalise) = do+  finalise+  pure (Right Nothing, [], [], [])

@@ -1,13 +1,14 @@ {-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-}  -- | -- Module      : Test.DejaFu.Conc.Internal.Common--- Copyright   : (c) 2016--2018 Michael Walker+-- Copyright   : (c) 2016--2019 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : ExistentialQuantification, RankNTypes+-- Portability : ExistentialQuantification, GADTs, RankNTypes -- -- Common types and utility functions for deterministic execution of -- 'MonadConc' implementations. This module is NOT considered to form@@ -15,14 +16,16 @@ module Test.DejaFu.Conc.Internal.Common where  import           Control.Exception             (Exception, MaskingState(..))+import           Control.Monad.Catch           (MonadCatch(..), MonadThrow(..)) import qualified Control.Monad.Conc.Class      as C import qualified Control.Monad.Fail            as Fail import           Data.Map.Strict               (Map)-import           Test.DejaFu.Conc.Internal.STM (ModelSTM)++import           Test.DejaFu.Conc.Internal.STM (ModelSTM, ModelTVar) import           Test.DejaFu.Types  ----------------------------------------------------------------------------------- * The @ModelConc@ Monad+-- * Types for Modelling Concurrency  -- | The underlying monad is based on continuations over 'Action's. --@@ -32,26 +35,73 @@ -- current expression of threads and exception handlers very difficult -- (perhaps even not possible without significant reworking), so I -- abandoned the attempt.-newtype ModelConc n a = ModelConc { runModelConc :: (a -> Action n) -> Action n }+type ModelConc = Program Basic -instance Functor (ModelConc n) where-    fmap f m = ModelConc $ \c -> runModelConc m (c . f)+-- | A representation of a concurrent program for testing.+--+-- To construct these, use the 'C.MonadConc' instance, or see+-- 'Test.DejaFu.Conc.withSetup', 'Test.DejaFu.Conc.withTeardown', and+-- 'Test.DejaFu.Conc.withSetupAndTeardown'.+--+-- @since 2.0.0.0+data Program pty n a where+  ModelConc ::+    { runModelConc :: (a -> Action n) -> Action n+    } -> Program Basic n a+  WithSetup ::+    { wsSetup   :: ModelConc n x+    , wsProgram :: x -> ModelConc n a+    } -> Program (WithSetup x) n a+  WithSetupAndTeardown ::+    { wstSetup    :: ModelConc n x+    , wstProgram  :: x -> ModelConc n y+    , wstTeardown :: x -> Either Condition y -> ModelConc n a+    } -> Program (WithSetupAndTeardown x y) n a -instance Applicative (ModelConc n) where-    -- without the @AReturn@, a thread could lock up testing by-    -- entering an infinite loop (eg: @forever (return ())@)-    pure x  = ModelConc $ \c -> AReturn $ c x-    f <*> v = ModelConc $ \c -> runModelConc f (\g -> runModelConc v (c . g))+-- | A type used to constrain 'Program': a @Program Basic@ is a+-- \"basic\" program with no set-up or teardown.+--+-- Construct with the 'MonadConc' instance.+--+-- @since 2.0.0.0+data Basic -instance Monad (ModelConc n) where-    return  = pure-    m >>= k = ModelConc $ \c -> runModelConc m (\x -> runModelConc (k x) c)+-- | A type used to constrain 'Program': a @Program (WithSetup x)@ is+-- a program with some set-up action producing a value of type @x@.+--+-- Construct with 'Test.DejaFu.Conc.withSetup'.+--+-- @since 2.0.0.0+data WithSetup x -    fail = Fail.fail+-- | A type used to constrain 'Program': a @Program+-- (WithSetupAndTeardown x y)@ is a program producing a value of type+-- @y@ with some set-up action producing a value of type @x@ and a+-- teardown action producing the final result.+--+-- Construct with 'Test.DejaFu.Conc.withTeardown' or+-- 'Test.DejaFu.Conc.withSetupAndTeardown'.+--+-- @since 2.0.0.0+data WithSetupAndTeardown x y -instance Fail.MonadFail (ModelConc n) where-    fail e = ModelConc $ \_ -> AThrow (MonadFailException e)+instance (pty ~ Basic) => Functor (Program pty n) where+  fmap f m = ModelConc $ \c -> runModelConc m (c . f) +instance (pty ~ Basic) => Applicative (Program pty n) where+  -- without the @AReturn@, a thread could lock up testing by entering+  -- an infinite loop (eg: @forever (return ())@)+  pure x  = ModelConc $ \c -> AReturn $ c x+  f <*> v = ModelConc $ \c -> runModelConc f (\g -> runModelConc v (c . g))++instance (pty ~ Basic) => Monad (Program pty n) where+  return  = pure+  fail    = Fail.fail+  m >>= k = ModelConc $ \c -> runModelConc m (\x -> runModelConc (k x) c)++instance (pty ~ Basic) => Fail.MonadFail (Program pty n) where+  fail e = ModelConc $ \_ -> AThrow (MonadFailException e)+ -- | An @MVar@ is modelled as a unique ID and a reference holding a -- @Maybe@ value. data ModelMVar n a = ModelMVar@@ -77,7 +127,7 @@   }  ----------------------------------------------------------------------------------- * Primitive Actions+-- ** Primitive Actions  -- | Scheduling is done in terms of a trace of 'Action's. Blocking can -- only occur as a result of an action, and they cover (most of) the@@ -123,12 +173,10 @@   | ACommit ThreadId IORefId   | AStop (n ()) -  | forall a. ASub (ModelConc n a) (Either Condition a -> Action n)-  | AStopSub (Action n)-  | forall a. ADontCheck (Maybe Int) (ModelConc n a) (a -> Action n)+  | ANewInvariant (Invariant n ()) (Action n)  ----------------------------------------------------------------------------------- * Scheduling & Traces+-- ** Scheduling & Traces  -- | Look as far ahead in the given continuation as possible. lookahead :: Action n -> Lookahead@@ -165,6 +213,51 @@ lookahead (ADelay n _) = WillThreadDelay n lookahead (AReturn _) = WillReturn lookahead (AStop _) = WillStop-lookahead (ASub _ _) = WillSubconcurrency-lookahead (AStopSub _) = WillStopSubconcurrency-lookahead (ADontCheck _ _ _) = WillDontCheck+lookahead (ANewInvariant _ _) = WillRegisterInvariant++-------------------------------------------------------------------------------+-- * Invariants++-- | Invariants are atomic actions which can inspect the shared state+-- of your computation, and terminate it on failure.  Invariants have+-- no visible effects, and are checked after each scheduling point.+--+-- To be checked, an invariant must be created during the setup phase+-- of your 'Program', using 'Test.DejaFu.Conc.registerInvariant'.  The+-- invariant will then be checked in the main phase (but not in the+-- setup or teardown phase).  As a consequence of this, any shared+-- state you want your invariant to check must also be created in the+-- setup phase, and passed into the main phase as a parameter.+--+-- @since 2.0.0.0+newtype Invariant n a = Invariant { runInvariant :: (a -> IAction n) -> IAction n }++instance Functor (Invariant n) where+  fmap f m = Invariant $ \c -> runInvariant m (c . f)++instance Applicative (Invariant n) where+  pure x  = Invariant $ \c -> c x+  f <*> v = Invariant $ \c -> runInvariant f (\g -> runInvariant v (c . g))++instance Monad (Invariant n) where+  return  = pure+  fail    = Fail.fail+  m >>= k = Invariant $ \c -> runInvariant m (\x -> runInvariant (k x) c)++instance Fail.MonadFail (Invariant n) where+  fail e = Invariant $ \_ -> IThrow (MonadFailException e)++instance MonadThrow (Invariant n) where+  throwM e = Invariant $ \_ -> IThrow e++instance MonadCatch (Invariant n) where+  catch stm handler = Invariant $ ICatch handler stm++-- | Invariants are represented as a sequence of primitive actions.+data IAction n+  = forall a. IInspectIORef (ModelIORef n a) (a -> IAction n)+  | forall a. IInspectMVar  (ModelMVar  n a) (Maybe a -> IAction n)+  | forall a. IInspectTVar  (ModelTVar  n a) (a -> IAction n)+  | forall a e. Exception e => ICatch (e -> Invariant n a) (Invariant n a) (a -> IAction n)+  | forall e. Exception e => IThrow e+  | IStop (n ())

@@ -114,6 +114,12 @@   (vals, count, def) <- C.readIORef iorefRef   pure (M.findWithDefault def tid vals, count) +-- | Read the global state of a @IORef@.+readIORefGlobal :: C.MonadConc n => ModelIORef n a -> n a+readIORefGlobal ModelIORef{..} = do+  (_, _, def) <- C.readIORef iorefRef+  pure def+ -- | Write and commit to a @IORef@ immediately, clearing the update map -- and incrementing the write count. writeImmediate :: C.MonadConc n => ModelIORef n a -> a -> n (n ())

@@ -0,0 +1,374 @@+{-# OPTIONS_GHC -Wno-orphans #-}++{-# LANGUAGE CPP #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TypeFamilies #-}++-- GHC doesn't need this to compile the module, but stylish-haskell+-- does to format it.+{-# LANGUAGE FlexibleContexts #-}++-- |+-- Module      : Test.DejaFu.Conc.Internal.Program+-- Copyright   : (c) 2019 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- Stability   : experimental+-- Portability : CPP, FlexibleContexts, FlexibleInstances, GADTs, LambdaCase, RecordWildCards, TypeFamilies+--+-- Representations of concurrent programs with setup, teardown, and+-- snapshotting.  This module is NOT considered to form part of the+-- public interface of this library.+--+-- This module defines orphan instances for the 'Program' type which+-- lives in "Test.DejaFu.Conc.Internal.Common", to avoid needing to+-- pull a bunch more stuff into that module.+module Test.DejaFu.Conc.Internal.Program where++import           Control.Applicative                 (Applicative(..))+import           Control.Exception                   (MaskingState(..))+import qualified Control.Monad.Catch                 as Ca+import qualified Control.Monad.IO.Class              as IO+import           Control.Monad.Trans.Class           (MonadTrans(..))+import qualified Data.Foldable                       as F+import           Data.List                           (partition)+import qualified Data.Map.Strict                     as M+import           Data.Maybe                          (isNothing)+import           GHC.Stack                           (HasCallStack)++import qualified Control.Monad.Conc.Class            as C+import           Test.DejaFu.Conc.Internal+import           Test.DejaFu.Conc.Internal.Common+import           Test.DejaFu.Conc.Internal.STM       (ModelSTM)+import           Test.DejaFu.Conc.Internal.Threading (Threads, _blocking)+import           Test.DejaFu.Internal+import           Test.DejaFu.Schedule+import           Test.DejaFu.Types++-------------------------------------------------------------------------------+-- Expressing concurrent programs++instance (pty ~ Basic, IO.MonadIO n) => IO.MonadIO (Program pty n) where+  liftIO ma = ModelConc (\c -> ALift (fmap c (IO.liftIO ma)))++instance (pty ~ Basic) => MonadTrans (Program pty) where+  lift ma = ModelConc (\c -> ALift (fmap c ma))++instance (pty ~ Basic) =>  Ca.MonadCatch (Program pty n) where+  catch ma h = ModelConc (ACatching h ma)++instance (pty ~ Basic) => Ca.MonadThrow (Program pty n) where+  throwM e = ModelConc (\_ -> AThrow e)++instance (pty ~ Basic) => Ca.MonadMask (Program pty n) where+  mask                mb = ModelConc (AMasking MaskedInterruptible   (\f -> mb f))+  uninterruptibleMask mb = ModelConc (AMasking MaskedUninterruptible (\f -> mb f))++#if MIN_VERSION_exceptions(0,10,0)+  generalBracket acquire release use = Ca.mask $ \unmasked -> do+    resource <- acquire+    b <- unmasked (use resource) `Ca.catch` (\e -> release resource (Ca.ExitCaseException e) >> Ca.throwM e)+    c <- release resource (Ca.ExitCaseSuccess b)+    pure (b, c)+#elif MIN_VERSION_exceptions(0,9,0)+  -- from https://github.com/fpco/stackage/issues/3315#issuecomment-368583481+  generalBracket acquire release cleanup use = Ca.mask $ \unmasked -> do+    resource <- acquire+    result <- unmasked (use resource) `Ca.catch` (\e -> cleanup resource e >> Ca.throwM e)+    _ <- release resource+    pure result+#endif++instance (pty ~ Basic, Monad n) => C.MonadConc (Program pty n) where+  type MVar     (Program pty n) = ModelMVar n+  type IORef    (Program pty n) = ModelIORef n+  type Ticket   (Program pty n) = ModelTicket+  type STM      (Program pty n) = ModelSTM n+  type ThreadId (Program pty n) = ThreadId++  -- ----------++  forkWithUnmaskN   n ma = ModelConc (AFork n (\umask -> runModelConc (ma umask) (\_ -> AStop (pure ()))))+  forkOnWithUnmaskN n _  = C.forkWithUnmaskN n+  forkOSWithUnmaskN n ma+    | C.rtsSupportsBoundThreads =+      ModelConc (AForkOS n (\umask -> runModelConc (ma umask) (\_ -> AStop (pure ()))))+    | otherwise = fail "RTS doesn't support multiple OS threads (use ghc -threaded when linking)"++  isCurrentThreadBound = ModelConc 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.+  getNumCapabilities      = ModelConc AGetNumCapabilities+  setNumCapabilities caps = ModelConc (\c -> ASetNumCapabilities caps (c ()))++  myThreadId = ModelConc AMyTId++  yield = ModelConc (\c -> AYield (c ()))+  threadDelay n = ModelConc (\c -> ADelay n (c ()))++  -- ----------++  newIORefN n a = ModelConc (ANewIORef n a)++  readIORef   ref = ModelConc (AReadIORef    ref)+  readForCAS ref = ModelConc (AReadIORefCas ref)++  peekTicket' _ = ticketVal++  writeIORef ref      a = ModelConc (\c -> AWriteIORef ref a (c ()))+  casIORef   ref tick a = ModelConc (ACasIORef ref tick a)++  atomicModifyIORef ref f = ModelConc (AModIORef    ref f)+  modifyIORefCAS    ref f = ModelConc (AModIORefCas ref f)++  -- ----------++  newEmptyMVarN n = ModelConc (ANewMVar n)++  putMVar  var a = ModelConc (\c -> APutMVar var a (c ()))+  readMVar var   = ModelConc (AReadMVar var)+  takeMVar var   = ModelConc (ATakeMVar var)++  tryPutMVar  var a = ModelConc (ATryPutMVar  var a)+  tryReadMVar var   = ModelConc (ATryReadMVar var)+  tryTakeMVar var   = ModelConc (ATryTakeMVar var)++  -- ----------++  throwTo tid e = ModelConc (\c -> AThrowTo tid e (c ()))++  -- ----------++  atomically = ModelConc . AAtom++-------------------------------------------------------------------------------+-- Executing concurrent programs++-- | Run a concurrent computation with a given 'Scheduler' and initial+-- state, returning either the final result or the condition which+-- prevented that. 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!+-- You should therefore keep @IO@ blocks small, and only perform+-- blocking operations with the supplied primitives, insofar as+-- possible.+--+-- __Note:__ In order to prevent computation from hanging, the runtime+-- will assume that a deadlock situation has arisen if the scheduler+-- attempts to (a) schedule a blocked thread, or (b) schedule a+-- nonexistent thread. In either of those cases, the computation will+-- be halted.+--+-- @since 2.0.0.0+runConcurrent :: C.MonadConc n+  => Scheduler s+  -> MemType+  -> s+  -> Program pty n a+  -> n (Either Condition a, s, Trace)+runConcurrent sched memtype s ma@(ModelConc _) = do+  res <- runConcurrency [] False sched memtype s initialIdSource 2 ma+  out <- efromJust <$> C.readIORef (finalRef res)+  pure ( out+       , cSchedState (finalContext res)+       , F.toList (finalTrace res)+       )+runConcurrent sched memtype s ma = recordSnapshot ma >>= \case+  Just (Left cond, trc) -> pure (Left cond, s, trc)+  Just (Right snap, _)  -> runSnapshot sched memtype s snap+  Nothing -> fatal "failed to record snapshot!"++-- | Runs any setup action and returns a 'Snapshot' which can be+-- passed to 'runSnapshot'.  If there is no setup action (this is a+-- @Program Basic@, then @Nothing@ is returned.  The snapshot captures+-- the state at the end of the setup, so the full program can be run+-- multiple times without repeating the setup.+--+-- The setup action is executed atomically with a deterministic+-- scheduler under sequential consistency.  Any forked threads+-- continue to exist in the main program.+--+-- If the setup action does not successfully produce a value+-- (deadlock, uncaught exception, etc), no snapshot is produced.+--+-- __Snapshotting @IO@:__ A snapshot captures entire state of your+-- concurrent program: the state of every thread, the number of+-- capabilities, the values of any @IORef@s, @MVar@s, and @TVar@s, and+-- records any @IO@ that you performed.+--+-- When restoring a snapshot this @IO@ is replayed, in order.  But the+-- whole snapshotted computation is not.  So the effects of the @IO@+-- take place again, but any return values are ignored.  For example,+-- this program will not do what you want:+--+-- @+-- bad_snapshot = withSetup+--   (do r <- liftIO (newIORef 0)+--       liftIO (modifyIORef r (+1))+--       pure r)+--   (liftIO . readIORef)+-- @+--+-- When the snapshot is taken, the value in the @IORef@ will be 1.+-- When the snapshot is restored for the first time, those @IO@+-- actions will be run again, /but their return values will be+-- discarded/.  The value in the @IORef@ will be 2.  When the snapshot+-- is restored for the second time, the value in the @IORef@ will be+-- 3.  And so on.+--+-- To safely use @IO@ in a snapshotted computation, __the combined+-- effect must be idempotent__.  You should either use actions which+-- set the state to the final value directly, rather than modifying it+-- (eg, using a combination of @liftIO . readIORef@ and @liftIO+-- . writeIORef@ here), or reset the state to a known value.  Both of+-- these approaches will work:+--+-- @+-- good_snapshot1 = withSetup+--   (do let modify r f = liftIO (readIORef r) >>= liftIO . writeIORef r . f+--        r <- liftIO (newIORef 0)+--        modify r (+1)+--        pure r)+--   (liftIO . readIORef)+--+-- good_snapshot2 = withSetup+--   (do r <- liftIO (newIORef 0)+--       liftIO (writeIORef r 0)+--       liftIO (modifyIORef r (+1))+--       pure r)+--   (liftIO . readIORef)+-- @+--+-- @since 2.0.0.0+recordSnapshot+  :: C.MonadConc n+  => Program pty n a+  -> n (Maybe (Either Condition (Snapshot pty n a), Trace))+recordSnapshot ModelConc{..} = pure Nothing+recordSnapshot WithSetup{..} =+  let mkSnapshot snap _ = WS snap+  in defaultRecordSnapshot mkSnapshot wsSetup wsProgram+recordSnapshot WithSetupAndTeardown{..} =+  let mkSnapshot snap = WSAT snap . wstTeardown+  in defaultRecordSnapshot mkSnapshot wstSetup wstProgram++-- | Runs a program with snapshotted setup to completion.+--+-- @since 2.0.0.0+runSnapshot+  :: C.MonadConc n+  => Scheduler s+  -> MemType+  -> s+  -> Snapshot pty n a+  -> n (Either Condition a, s, Trace)+runSnapshot sched memtype s (WS SimpleSnapshot{..}) = do+  let context = fromSnapContext s snapContext+  CResult{..} <- runConcurrencyWithSnapshot sched memtype context snapRestore snapNext+  out <- efromJust <$> C.readIORef finalRef+  pure ( out+       , cSchedState finalContext+       , F.toList finalTrace+       )+runSnapshot sched memtype s (WSAT SimpleSnapshot{..} teardown) = do+  let context = fromSnapContext s snapContext+  intermediateResult <- runConcurrencyWithSnapshot sched memtype context snapRestore snapNext+  let idsrc = cIdSource (finalContext intermediateResult)+  out1 <- efromJust <$> C.readIORef (finalRef intermediateResult)+  teardownResult <- simpleRunConcurrency False idsrc (teardown out1)+  out2 <- efromJust <$> C.readIORef (finalRef teardownResult)+  pure ( out2+       , cSchedState (finalContext intermediateResult)+       , F.toList (finalTrace intermediateResult)+       )++-------------------------------------------------------------------------------+-- Snapshotting++-- | A record of the state of a concurrent program immediately after+-- completing the setup action.+--+-- @since 2.0.0.0+data Snapshot pty n a where+  WS   :: SimpleSnapshot n a -> Snapshot (WithSetup x) n a+  WSAT :: SimpleSnapshot n a -> (Either Condition a -> ModelConc n y) -> Snapshot (WithSetupAndTeardown x a) n y++data SimpleSnapshot n a = SimpleSnapshot+  { snapContext :: Context n ()+  , snapRestore :: Threads n -> n ()+  , snapNext    :: ModelConc n a+  }++-- | Get the 'Context' from a 'Snapshot'.+contextFromSnapshot :: Snapshot p n a -> Context n ()+contextFromSnapshot (WS SimpleSnapshot{..})     = snapContext+contextFromSnapshot (WSAT SimpleSnapshot{..} _) = snapContext++-- | Get the threads which exist in a snapshot, partitioned into+-- runnable and not runnable.+threadsFromSnapshot :: Snapshot p n a -> ([ThreadId], [ThreadId])+threadsFromSnapshot snap = (initialThread : runnable, blocked) where+  (runnable, blocked) = partition isRunnable (M.keys threads)+  threads = cThreads (contextFromSnapshot snap)+  isRunnable tid = isNothing (_blocking =<< M.lookup tid threads)++-- | 'recordSnapshot' implemented generically.+--+-- Throws an error if the snapshot could not be produced.+defaultRecordSnapshot :: C.MonadConc n+  => (SimpleSnapshot n a -> x -> snap)+  -> ModelConc n x+  -> (x -> ModelConc n a)+  -> n (Maybe (Either Condition snap, Trace))+defaultRecordSnapshot mkSnapshot setup program = do+  CResult{..} <- simpleRunConcurrency True initialIdSource setup+  let trc = F.toList finalTrace+  out <- C.readIORef finalRef+  pure . Just $ case out of+    Just (Right a) ->+      let snap = mkSnapshot (SimpleSnapshot finalContext finalRestore (program a)) a+      in (Right snap, trc)+    Just (Left f) -> (Left f, trc)+    -- alternative behaviour: return @Nothing@ here.  but this should+    -- never fail, so it should be an error if it does.+    Nothing -> fatal "failed to produce snapshot"++-------------------------------------------------------------------------------+-- Utilities++-- | Run a concurrent program with a deterministic scheduler in+-- snapshotting or non-snapshotting mode.+simpleRunConcurrency ::(C.MonadConc n, HasCallStack)+  => Bool+  -> IdSource+  -> ModelConc n a+  -> n (CResult n () a)+simpleRunConcurrency forSnapshot idsrc =+  runConcurrency [] forSnapshot roundRobinSchedNP SequentialConsistency () idsrc 2++-- | Make a new context from a snapshot context.+fromSnapContext :: g -> Context n s -> Context n g+fromSnapContext g ctx@Context{..} = ctx+  { cSchedState = g+  , cInvariants = InvariantContext+    { icActive  = cNewInvariants+    , icBlocked = []+    }+  , cNewInvariants = []+  }++wrap :: (((a -> Action n) -> Action n) -> ((a -> Action n) -> Action n)) -> ModelConc n a -> ModelConc n a+wrap f = ModelConc . f . runModelConc

@@ -2,23 +2,26 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}  -- | -- Module      : Test.DejaFu.Internal--- Copyright   : (c) 2017--2018 Michael Walker+-- Copyright   : (c) 2017--2019 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : DeriveAnyClass, DeriveGeneric, FlexibleContexts, GADTs+-- Portability : DeriveAnyClass, DeriveGeneric, FlexibleContexts, GADTs, LambdaCase -- -- 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.DeepSeq          (NFData(..))+import           Control.Exception        (MaskingState(..)) import qualified Control.Monad.Conc.Class as C import           Data.List.NonEmpty       (NonEmpty(..))+import           Data.Map.Strict          (Map) import qualified Data.Map.Strict          as M import           Data.Maybe               (fromMaybe) import           Data.Set                 (Set)@@ -37,6 +40,7 @@ -- @since 1.2.0.0 data Settings n a = Settings   { _way :: Way+  , _lengthBound :: Maybe LengthBound   , _memtype :: MemType   , _discard :: Maybe (Either Condition a -> Maybe Discard)   , _debugShow :: Maybe (a -> String)@@ -197,9 +201,7 @@ rewind LiftIO = WillLiftIO rewind Return = WillReturn rewind Stop = WillStop-rewind Subconcurrency = WillSubconcurrency-rewind StopSubconcurrency = WillStopSubconcurrency-rewind (DontCheck _) = WillDontCheck+rewind RegisterInvariant = WillRegisterInvariant  -- | Check if an operation could enable another thread. willRelease :: Lookahead -> Bool@@ -217,7 +219,6 @@ willRelease (WillSetMasking _ _) = True willRelease (WillResetMasking _ _) = True willRelease WillStop = True-willRelease WillDontCheck = True willRelease _ = False  -------------------------------------------------------------------------------@@ -326,6 +327,58 @@ simplifyLookahead _ = UnsynchronisedOther  -------------------------------------------------------------------------------+-- * Concurrency state++-- | Initial concurrency state.+initialCState :: ConcurrencyState+initialCState = ConcurrencyState M.empty S.empty M.empty++-- | Update the concurrency state with the action that has just+-- happened.+updateCState :: MemType -> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState+updateCState memtype cstate tid act = ConcurrencyState+  { concIOState   = updateIOState memtype act $ concIOState   cstate+  , concMVState   = updateMVState         act $ concMVState   cstate+  , concMaskState = updateMaskState tid   act $ concMaskState cstate+  }++-- | Update the @IORef@ buffer state with the action that has just+-- happened.+updateIOState :: MemType -> ThreadAction -> Map IORefId Int -> Map IORefId Int+updateIOState SequentialConsistency _ = const M.empty+updateIOState _ (CommitIORef _ r) = (`M.alter` r) $ \case+  Just 1  -> Nothing+  Just n  -> Just (n-1)+  Nothing -> Nothing+updateIOState _ (WriteIORef    r) = M.insertWith (+) r 1+updateIOState _ 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 tid (Throw True) = M.delete tid+updateMaskState _ (ThrowTo tid True) = M.delete tid+updateMaskState tid Stop = M.delete tid+updateMaskState _ _ = id++------------------------------------------------------------------------------- -- * Error reporting  -- | 'tail' but with a better error message if it fails.  Use this@@ -358,6 +411,12 @@ efromRight :: HasCallStack => Either a b -> b efromRight (Right b) = b efromRight _ = withFrozenCallStack $ fatal "fromRight: Left"++-- | 'fromLeft' but with a better error message if it fails.  Use+-- this only where it shouldn't fail!+efromLeft :: HasCallStack => Either a b -> a+efromLeft (Left a) = a+efromLeft _ = withFrozenCallStack $ fatal "fromLeft: Right"  -- | 'M.adjust' but which errors if the key is not present.  Use this -- only where it shouldn't fail!

@@ -114,7 +114,8 @@ import qualified Data.Set                 as S import           Test.LeanCheck           (Listable(..), concatMapT, mapT) -import           Test.DejaFu.Conc         (ConcIO, Condition, subconcurrency)+import           Test.DejaFu.Conc         (ConcIO, Condition,+                                           withSetupAndTeardown) import           Test.DejaFu.SCT          (runSCT) import           Test.DejaFu.Settings     (defaultMemType, defaultWay) @@ -411,12 +412,14 @@   -> x   -> IO (Set (Maybe Condition, o)) evalSigWithSeed sig x = do-  results <- runSCT defaultWay defaultMemType $ do-    s <- initialise sig x-    r <- subconcurrency $ do-      _ <- fork (interfere sig s x)-      _ <- expression sig s-      pure ()-    o <- observe sig s x-    pure (either Just (const Nothing) r, o)+  results <- runSCT defaultWay defaultMemType $+    withSetupAndTeardown+      (initialise sig x)+      (\s r -> do+          o <- observe sig s x+          pure (either Just (const Nothing) r, o))+      (\s -> do+          _ <- fork (interfere sig s x)+          _ <- expression sig s+          pure ())   pure . S.fromList $ map (\(Right a, _) -> a) results

@@ -2,7 +2,7 @@  -- | -- Module      : Test.DejaFu.SCT--- Copyright   : (c) 2015--2018 Michael Walker+-- Copyright   : (c) 2015--2019 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental@@ -22,18 +22,6 @@   , resultsSetWithSettings   , resultsSetWithSettings'   , module Test.DejaFu.Settings--  -- * Deprecated-  , runSCTDiscard-  , runSCTDiscard'-  , resultsSetDiscard-  , resultsSetDiscard'-  , sctBound-  , sctBoundDiscard-  , sctUniformRandom-  , sctUniformRandomDiscard-  , sctWeightedRandom-  , sctWeightedRandomDiscard   ) where  import           Control.Applicative               ((<|>))@@ -44,7 +32,6 @@ import           Data.Maybe                        (fromMaybe) import           Data.Set                          (Set) import qualified Data.Set                          as S-import           System.Random                     (RandomGen)  import           Test.DejaFu.Conc import           Test.DejaFu.Internal@@ -64,67 +51,30 @@ -- The exact executions tried, and the order in which results are -- found, is unspecified and may change between releases. ----- @since 1.0.0.0+-- @since 2.0.0.0 runSCT :: MonadConc n   => Way   -- ^ How to run the concurrent program.   -> MemType   -- ^ The memory model to use for non-synchronised @IORef@ operations.-  -> ConcT n a+  -> Program pty n a   -- ^ The computation to run many times.   -> n [(Either Condition a, Trace)] runSCT way = runSCTWithSettings . fromWayAndMemType way  -- | Return the set of results of a concurrent program. ----- @since 1.0.0.0+-- @since 2.0.0.0 resultsSet :: (MonadConc n, Ord a)   => Way   -- ^ How to run the concurrent program.   -> MemType   -- ^ The memory model to use for non-synchronised @IORef@ operations.-  -> ConcT n a+  -> Program pty n a   -- ^ The computation to run many times.   -> n (Set (Either Condition a)) resultsSet way = resultsSetWithSettings . fromWayAndMemType way --- | A variant of 'runSCT' which can selectively discard results.------ 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-  => (Either Condition a -> Maybe Discard)-  -- ^ Selectively discard results.-  -> Way-  -- ^ How to run the concurrent program.-  -> MemType-  -- ^ The memory model to use for non-synchronised @IORef@ operations.-  -> ConcT n a-  -- ^ The computation to run many times.-  -> n [(Either Condition a, Trace)]-runSCTDiscard discard way = runSCTWithSettings . set ldiscard (Just discard) . fromWayAndMemType way-{-# DEPRECATED runSCTDiscard "Use runSCTWithSettings instead" #-}---- | A variant of 'resultsSet' which can selectively discard results.------ @since 1.0.0.0-resultsSetDiscard :: (MonadConc n, Ord a)-  => (Either Condition a -> Maybe Discard)-  -- ^ Selectively discard results.  Traces are always discarded.-  -> Way-  -- ^ How to run the concurrent program.-  -> MemType-  -- ^ The memory model to use for non-synchronised @IORef@ operations.-  -> ConcT n a-  -- ^ The computation to run many times.-  -> n (Set (Either Condition a))-resultsSetDiscard discard way memtype conc =-  let discard' efa = discard efa <|> Just DiscardTrace-  in S.fromList . map fst <$> runSCTDiscard discard' way memtype conc-{-# DEPRECATED resultsSetDiscard "Use resultsSetWithSettings instead" #-}- -- | A strict variant of 'runSCT'. -- -- Demanding the result of this will force it to normal form, which@@ -133,9 +83,15 @@ -- The exact executions tried, and the order in which results are -- found, is unspecified and may change between releases. ----- @since 1.0.0.0+-- @since 2.0.0.0 runSCT' :: (MonadConc n, NFData a)-  => Way -> MemType -> ConcT n a -> n [(Either Condition a, Trace)]+  => Way+  -- ^ How to run the concurrent program.+  -> MemType+  -- ^ The memory model to use for non-synchronised @IORef@ operations.+  -> Program pty n a+  -- ^ The computation to run many times.+  -> n [(Either Condition a, Trace)] runSCT' way = runSCTWithSettings' . fromWayAndMemType way  -- | A strict variant of 'resultsSet'.@@ -143,40 +99,17 @@ -- Demanding the result of this will force it to normal form, which -- may be more efficient in some situations. ----- @since 1.0.0.0+-- @since 2.0.0.0 resultsSet' :: (MonadConc n, Ord a, NFData a)-  => Way -> MemType -> ConcT n a -> n (Set (Either Condition a))+  => Way+  -- ^ How to run the concurrent program.+  -> MemType+  -- ^ The memory model to use for non-synchronised @IORef@ operations.+  -> Program pty n a+  -- ^ The computation to run many times.+  -> n (Set (Either Condition a)) resultsSet' way = resultsSetWithSettings' . fromWayAndMemType way --- | A strict variant of 'runSCTDiscard'.------ Demanding the result of this will force it to normal form, which--- may be more efficient in some situations.------ 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, NFData a)-  => (Either Condition a -> Maybe Discard) -> Way -> MemType -> ConcT n a -> n [(Either Condition a, Trace)]-runSCTDiscard' discard way memtype conc = do-  res <- runSCTDiscard discard way memtype conc-  rnf res `seq` pure res-{-# DEPRECATED runSCTDiscard' "Use runSCTWithSettings' instead" #-}---- | A strict variant of 'resultsSetDiscard'.------ Demanding the result of this will force it to normal form, which--- may be more efficient in some situations.------ @since 1.0.0.0-resultsSetDiscard' :: (MonadConc n, Ord a, NFData a)-  => (Either Condition a -> Maybe Discard) -> Way -> MemType -> ConcT n a -> n (Set (Either Condition a))-resultsSetDiscard' discard way memtype conc = do-  res <- resultsSetDiscard discard way memtype conc-  rnf res `seq` pure res-{-# DEPRECATED resultsSetDiscard' "Use resultsSetWithSettings' instead" #-}- ------------------------------------------------------------------------------- -- Configuration @@ -185,11 +118,11 @@ -- The exact executions tried, and the order in which results are -- found, is unspecified and may change between releases. ----- @since 1.2.0.0+-- @since 2.0.0.0 runSCTWithSettings :: MonadConc n   => Settings n a   -- ^ The SCT settings.-  -> ConcT n a+  -> Program pty n a   -- ^ The computation to run many times.   -> n [(Either Condition a, Trace)] runSCTWithSettings settings conc = case _way settings of@@ -198,13 +131,13 @@          check = findSchedulePrefix -        step run dp (prefix, conservative, sleep) = do+        step cstate0 run dp (prefix, conservative, sleep) = do           (res, s, trace) <- run-            (dporSched (_safeIO settings) (_memtype settings) (cBound cb0))-            (initialDPORSchedState sleep prefix)+            (dporSched (_safeIO settings) (cBound (_lengthBound settings) cb0))+            (initialDPORSchedState sleep prefix cstate0) -          let bpoints = findBacktrackSteps (_safeIO settings) (_memtype settings) (cBacktrack cb0) (schedBoundKill s) (schedBPoints s) trace-          let newDPOR = incorporateTrace (_safeIO settings) (_memtype settings) conservative trace dp+          let bpoints = findBacktrackSteps (_safeIO settings) (_memtype settings) (cBacktrack cb0) (schedBoundKill s) cstate0 (schedBPoints s) trace+          let newDPOR = incorporateTrace (_safeIO settings) (_memtype settings) conservative trace cstate0 dp            pure $ if schedIgnore s                  then (force newDPOR, Nothing)@@ -217,20 +150,20 @@         check (_, 0) = Nothing         check s = Just s -        step run _ (g, n) = do+        step _ run _ (g, n) = do           (res, s, trace) <- run             (randSched gen)-            (initialRandSchedState g)+            (initialRandSchedState (_lengthBound settings) g)           pure ((schedGen s, n-1), Just (res, trace))     in sct settings initial check step conc  -- | A variant of 'resultsSet' which takes a 'Settings' record. ----- @since 1.2.0.0+-- @since 2.0.0.0 resultsSetWithSettings :: (MonadConc n, Ord a)   => Settings n a   -- ^ The SCT settings.-  -> ConcT n a+  -> Program pty n a   -- ^ The computation to run many times.   -> n (Set (Either Condition a)) resultsSetWithSettings settings conc =@@ -245,10 +178,12 @@ -- The exact executions tried, and the order in which results are -- found, is unspecified and may change between releases. ----- @since 1.2.0.0+-- @since 2.0.0.0 runSCTWithSettings' :: (MonadConc n, NFData a)   => Settings n a-  -> ConcT n a+  -- ^ The SCT settings.+  -> Program pty n a+  -- ^ The computation to run many times.   -> n [(Either Condition a, Trace)] runSCTWithSettings' settings conc = do   res <- runSCTWithSettings settings conc@@ -259,10 +194,12 @@ -- Demanding the result of this will force it to normal form, which -- may be more efficient in some situations. ----- @since 1.2.0.0+-- @since 2.0.0.0 resultsSetWithSettings' :: (MonadConc n, Ord a, NFData a)   => Settings n a-  -> ConcT n a+  -- ^ The SCT settings.+  -> Program pty n a+  -- ^ The computation to run many times.   -> n (Set (Either Condition a)) resultsSetWithSettings' settings conc = do   res <- resultsSetWithSettings settings conc@@ -272,24 +209,40 @@ -- Combined Bounds  -- | Combination bound function-cBound :: Bounds -> IncrementalBoundFunc ((Int, Maybe ThreadId), M.Map ThreadId Int, Int)-cBound (Bounds pb fb lb) (Just (k1, k2, k3)) prior lh =+cBound :: Maybe LengthBound -> Bounds -> IncrementalBoundFunc ((Int, Maybe ThreadId), M.Map ThreadId Int, Int)+cBound lb (Bounds pb fb) (Just (k1, k2, k3)) prior lh =   let k1' = maybe (\k _ _ -> k) pBound pb (Just k1) prior lh       k2' = maybe (\k _ _ -> k) fBound fb (Just k2) prior lh       k3' = maybe (\k _ _ -> k) lBound lb (Just k3) prior lh   in (,,) <$> k1' <*> k2' <*> k3'-cBound _ Nothing _ _ = Just ((0, Nothing), M.empty, 1)+cBound _ _ Nothing _ _ = Just ((0, Nothing), M.empty, 1) --- | Combination backtracking function. Add all backtracking points--- corresponding to enabled bound functions.+-- | Backtracks to the given point. ----- If no bounds are enabled, just backtrack to the given point.+-- If pre-emption bounding is enabled, also conservatively adds a+-- backtracking point prior to the most recent transition before that+-- point.  This may result in the same state being reached multiple+-- times, but is needed because of the artificial dependency imposed+-- by the bound. cBacktrack :: Bounds -> BacktrackFunc-cBacktrack (Bounds (Just _) _ _) = pBacktrack-cBacktrack (Bounds _ (Just _) _) = fBacktrack-cBacktrack (Bounds _ _ (Just _)) = lBacktrack-cBacktrack _ = backtrackAt (\_ _ -> False)+cBacktrack (Bounds (Just _) _) bs =+    backtrackAt (\_ _ -> False) bs . concatMap addConservative+  where+    addConservative o@(i, _, tid) = o : case conservative i of+      Just j  -> [(j, True, tid)]+      Nothing -> [] +    -- index of conservative point+    conservative i = go (reverse (take (i-1) bs)) (i-1) where+      go _ (-1) = Nothing+      go (b1:rest@(b2:_)) j+        | bcktThreadid b1 /= bcktThreadid b2+          && not (isCommitRef $ bcktAction b1)+          && not (isCommitRef $ bcktAction b2) = Just j+        | otherwise = go rest (j-1)+      go _ _ = Nothing+cBacktrack _ bs = backtrackAt (\_ _ -> False) bs+ ------------------------------------------------------------------------------- -- Pre-emption bounding @@ -300,26 +253,6 @@   let k'@(pcount, _) = preEmpCountInc (fromMaybe (0, Nothing) k) prior lhead   in if pcount <= pb then Just k' else Nothing --- | Add a backtrack point, and also conservatively add one prior to--- the most recent transition before that point. This may result in--- the same state being reached multiple times, but is needed because--- of the artificial dependency imposed by the bound.-pBacktrack :: BacktrackFunc-pBacktrack bs = backtrackAt (\_ _ -> False) bs . concatMap addConservative where-  addConservative o@(i, _, tid) = o : case conservative i of-    Just j  -> [(j, True, tid)]-    Nothing -> []--  -- index of conservative point-  conservative i = go (reverse (take (i-1) bs)) (i-1) where-    go _ (-1) = Nothing-    go (b1:rest@(b2:_)) j-      | bcktThreadid b1 /= bcktThreadid b2-        && not (isCommitRef $ bcktAction b1)-        && not (isCommitRef $ bcktAction b2) = Just j-      | otherwise = go rest (j-1)-    go _ _ = Nothing- ------------------------------------------------------------------------------- -- Fair bounding @@ -331,13 +264,6 @@      then Just k'      else Nothing --- | 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.-  check t b = Just True == (willRelease <$> M.lookup t (bcktRunnable b))- ------------------------------------------------------------------------------- -- Length bounding @@ -346,147 +272,6 @@ lBound (LengthBound lb) len _ _ =   let len' = maybe 1 (+1) len   in if len' < lb then Just len' else Nothing---- | Add a backtrack point. If the thread doesn't exist or is blocked,--- add all unblocked threads.-lBacktrack :: BacktrackFunc-lBacktrack = backtrackAt (\_ _ -> False)------------------------------------------------------------------------------------ Systematic concurrency testing---- | SCT via BPOR.------ Schedules are generated by running the computation with a--- deterministic scheduler with some initial list of decisions. At--- each step of execution, possible-conflicting actions are looked--- for, if any are found, \"backtracking points\" are added, to cause--- the events to happen in a different order in a future execution.------ Note that unlike with non-bounded partial-order reduction, this may--- do some redundant work as the introduction of a bound can make--- previously non-interfering events interfere with each other.------ 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-  => MemType-  -- ^ The memory model to use for non-synchronised @IORef@ operations.-  -> Bounds-  -- ^ The combined bounds.-  -> ConcT n a-  -- ^ The computation to run many times-  -> n [(Either Condition a, Trace)]-sctBound = sctBoundDiscard (const Nothing)-{-# DEPRECATED sctBound "Use runSCT instead" #-}---- | A variant of 'sctBound' which can selectively discard results.------ 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-  => (Either Condition a -> Maybe Discard)-  -- ^ Selectively discard results.-  -> MemType-  -- ^ The memory model to use for non-synchronised @IORef@ operations.-  -> Bounds-  -- ^ The combined bounds.-  -> ConcT n a-  -- ^ The computation to run many times-  -> n [(Either Condition a, Trace)]-sctBoundDiscard discard memtype cb = runSCTWithSettings $-  set ldiscard (Just discard) (fromWayAndMemType (systematically cb) memtype)-{-# DEPRECATED sctBoundDiscard "Use runSCTWithSettings instead" #-}---- | SCT via uniform random scheduling.------ Schedules are generated by assigning to each new thread a random--- weight. Threads are then scheduled by a weighted random selection.------ This is not guaranteed to find all distinct results.------ @since 1.0.0.0-sctUniformRandom :: (MonadConc n, RandomGen g)-  => MemType-  -- ^ The memory model to use for non-synchronised @IORef@ operations.-  -> g-  -- ^ The random number generator.-  -> Int-  -- ^ The number of executions to perform.-  -> ConcT n a-  -- ^ The computation to run many times.-  -> n [(Either Condition a, Trace)]-sctUniformRandom = sctUniformRandomDiscard (const Nothing)-{-# DEPRECATED sctUniformRandom "Use runSCT instead" #-}---- | A variant of 'sctUniformRandom' which can selectively discard--- results.------ This is not guaranteed to find all distinct results.------ @since 1.0.0.0-sctUniformRandomDiscard :: (MonadConc n, RandomGen g)-  => (Either Condition a -> Maybe Discard)-  -- ^ Selectively discard results.-  -> MemType-  -- ^ The memory model to use for non-synchronised @IORef@ operations.-  -> g-  -- ^ The random number generator.-  -> Int-  -- ^ The number of executions to perform.-  -> ConcT n a-  -- ^ The computation to run many times.-  -> n [(Either Condition a, Trace)]-sctUniformRandomDiscard discard memtype g lim = runSCTWithSettings $-  set ldiscard (Just discard) (fromWayAndMemType (uniformly g lim) memtype)-{-# DEPRECATED sctUniformRandomDiscard "Use runSCTWithSettings instead" #-}---- | SCT via weighted random scheduling.------ Schedules are generated by assigning to each new thread a random--- weight. Threads are then scheduled by a weighted random selection.------ This is not guaranteed to find all distinct results.------ @since 1.7.0.0-sctWeightedRandom :: (MonadConc n, RandomGen g)-  => MemType-  -- ^ The memory model to use for non-synchronised @IORef@ operations.-  -> g-  -- ^ The random number generator.-  -> Int-  -- ^ The number of executions to perform.-  -> ConcT n a-  -- ^ The computation to run many times.-  -> n [(Either Condition a, Trace)]-sctWeightedRandom = sctWeightedRandomDiscard (const Nothing)-{-# DEPRECATED sctWeightedRandom "Use runSCT instead" #-}---- | A variant of 'sctWeightedRandom' which can selectively discard--- results.------ This is not guaranteed to find all distinct results.------ @since 1.7.0.0-sctWeightedRandomDiscard :: (MonadConc n, RandomGen g)-  => (Either Condition a -> Maybe Discard)-  -- ^ Selectively discard results.-  -> MemType-  -- ^ The memory model to use for non-synchronised @IORef@ operations.-  -> g-  -- ^ The random number generator.-  -> Int-  -- ^ The number of executions to perform.-  -> ConcT n a-  -- ^ The computation to run many times.-  -> n [(Either Condition a, Trace)]-sctWeightedRandomDiscard discard memtype g lim = runSCTWithSettings $-  set ldiscard (Just discard) (fromWayAndMemType (randomly g lim) memtype)-{-# DEPRECATED sctWeightedRandomDiscard "Use runSCTWithSettings instead" #-}  ------------------------------------------------------------------------------- -- Utilities

@@ -15,18 +15,19 @@ -- considered to form part of the public interface of this library. module Test.DejaFu.SCT.Internal where -import           Control.Monad.Conc.Class         (MonadConc)-import           Data.Coerce                      (Coercible, coerce)-import qualified Data.IntMap.Strict               as I-import           Data.List                        (find, mapAccumL)-import           Data.Maybe                       (fromMaybe)-import           GHC.Stack                        (HasCallStack)+import           Control.Monad.Conc.Class          (MonadConc)+import           Data.Coerce                       (Coercible, coerce)+import qualified Data.IntMap.Strict                as I+import           Data.List                         (find, mapAccumL)+import           Data.Maybe                        (fromMaybe)+import           GHC.Stack                         (HasCallStack)  import           Test.DejaFu.Conc-import           Test.DejaFu.Conc.Internal        (Context(..), DCSnapshot(..))-import           Test.DejaFu.Conc.Internal.Memory (commitThreadId)+import           Test.DejaFu.Conc.Internal         (Context(..))+import           Test.DejaFu.Conc.Internal.Memory  (commitThreadId)+import           Test.DejaFu.Conc.Internal.Program import           Test.DejaFu.Internal-import           Test.DejaFu.Schedule             (Scheduler(..))+import           Test.DejaFu.Schedule              (Scheduler(..)) import           Test.DejaFu.SCT.Internal.DPOR import           Test.DejaFu.Types import           Test.DejaFu.Utils@@ -42,47 +43,47 @@   -- ^ Initial state   -> (s -> Maybe t)   -- ^ State predicate-  -> ((Scheduler g -> g -> n (Either Condition a, g, Trace)) -> s -> t -> n (s, Maybe (Either Condition a, Trace)))+  -> (ConcurrencyState -> (Scheduler g -> g -> n (Either Condition a, g, Trace)) -> s -> t -> n (s, Maybe (Either Condition a, Trace)))   -- ^ Run the computation and update the state-  -> ConcT n a+  -> Program pty n a   -> n [(Either Condition a, Trace)]-sct settings s0 sfun srun conc-    | canDCSnapshot conc = runForDCSnapshot conc >>= \case-        Just (Right snap, _) -> sct'Snap snap-        Just (Left f, trace) -> pure [(Left f, trace)]-        _ -> do-          debugFatal "Failed to construct snapshot, continuing without."-          sct'Full-    | otherwise = sct'Full+sct settings s0 sfun srun conc = recordSnapshot conc >>= \case+    Just (Right snap, _) -> sct'Snap snap+    Just (Left f, trace) -> pure [(Left f, trace)]+    Nothing -> sct'Full   where     sct'Full = sct'       settings+      initialCState       (s0 [initialThread])       sfun-      (srun runFull)+      (srun initialCState runFull)       runFull       (toId 1)       (toId 1) -    sct'Snap snap = let idsrc = cIdSource (dcsContext snap) in sct'-      settings-      (s0 (fst (threadsFromDCSnapshot snap)))-      sfun-      (srun (runSnap snap))-      (runSnap snap)-      (toId $ 1 + fst (_tids idsrc))-      (toId $ 1 + fst (_iorids idsrc))+    sct'Snap snap =+      let idsrc = cIdSource (contextFromSnapshot snap)+          cstate = cCState (contextFromSnapshot snap)+      in sct'+         settings+         cstate+         (s0 (fst (threadsFromSnapshot snap)))+         sfun+         (srun cstate (runSnap snap))+         (runSnap snap)+         (toId $ 1 + fst (_tids idsrc))+         (toId $ 1 + fst (_iorids idsrc))      runFull sched s = runConcurrent sched (_memtype settings) s conc-    runSnap snap sched s = runWithDCSnapshot sched (_memtype settings) s snap--    debugFatal = if _debugFatal settings then fatal else debugPrint-    debugPrint = fromMaybe (const (pure ())) (_debugPrint settings)+    runSnap snap sched s = runSnapshot sched (_memtype settings) s snap  -- | Like 'sct' but given a function to run the computation. sct' :: (MonadConc n, HasCallStack)   => Settings n a   -- ^ The SCT settings ('Way' is ignored)+  -> ConcurrencyState+  -- ^ The initial concurrency state   -> s   -- ^ Initial state   -> (s -> Maybe t)@@ -96,7 +97,7 @@   -> IORefId   -- ^ The first available @IORefId@   -> n [(Either Condition a, Trace)]-sct' settings s0 sfun srun run nTId nCRId = go Nothing [] s0 where+sct' settings cstate0 s0 sfun srun run nTId nCRId = go Nothing [] s0 where   go (Just res) _ _ | earlyExit res = pure []   go res0 seen !s = case sfun s of     Just t -> srun s t >>= \case@@ -128,7 +129,7 @@   dosimplify res trace seen s     | not (_simplify settings) = ((res, trace) :) <$> go (Just res) seen s     | otherwise = do-        shrunk <- simplifyExecution settings run nTId nCRId res trace+        shrunk <- simplifyExecution settings cstate0 run nTId nCRId res trace         (shrunk :) <$> go (Just res) seen s    earlyExit = fromMaybe (const False) (_earlyExit settings)@@ -152,6 +153,8 @@ simplifyExecution :: (MonadConc n, HasCallStack)   => Settings n a   -- ^ The SCT settings ('Way' is ignored)+  -> ConcurrencyState+  -- ^ The initial concurrency state   -> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))   -- ^ Just run the computation   -> ThreadId@@ -162,7 +165,7 @@   -- ^ The expected result   -> Trace   -> n (Either Condition a, Trace)-simplifyExecution settings run nTId nCRId res trace+simplifyExecution settings cstate0 run nTId nCRId res trace     | tidTrace == simplifiedTrace = do         debugPrint ("Simplifying new result '" ++ p res ++ "': no simplification possible!")         pure (res, trace)@@ -178,7 +181,7 @@             pure (res, trace)   where     tidTrace = toTIdTrace trace-    simplifiedTrace = simplify (_safeIO settings) (_memtype settings) tidTrace+    simplifiedTrace = simplify (_safeIO settings) (_memtype settings) cstate0 tidTrace     fixup = renumber (_memtype settings) (fromId nTId) (fromId nCRId)      debugFatal = if _debugFatal settings then fatal else debugPrint@@ -194,11 +197,11 @@   -- ^ The reduced sequence of scheduling decisions   -> n (Either Condition a, [(ThreadId, ThreadAction)], Trace) replay run = run (Scheduler (const sched)) where-    sched runnable ((t, Stop):ts) = case findThread t runnable of+    sched runnable cs ((t, Stop):ts) = case findThread t runnable of       Just t' -> (Just t', ts)-      Nothing -> sched runnable ts-    sched runnable ((t, _):ts) = (findThread t runnable, ts)-    sched _ _ = (Nothing, [])+      Nothing -> sched runnable cs ts+    sched runnable _ ((t, _):ts) = (findThread t runnable, ts)+    sched _ _ _ = (Nothing, [])      -- find a thread ignoring names     findThread tid0 =@@ -209,10 +212,15 @@  -- | Simplify a trace by permuting adjacent independent actions to -- reduce context switching.-simplify :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]-simplify safeIO memtype trc0 = loop (length trc0) (prepare trc0) where-  prepare = dropCommits safeIO memtype . lexicoNormalForm safeIO memtype-  step = pushForward safeIO memtype . pullBack safeIO memtype+simplify+  :: Bool+  -> MemType+  -> ConcurrencyState+  -> [(ThreadId, ThreadAction)]+  -> [(ThreadId, ThreadAction)]+simplify safeIO memtype cstate0 trc0 = loop (length trc0) (prepare trc0) where+  prepare = dropCommits safeIO memtype cstate0 . lexicoNormalForm safeIO memtype cstate0+  step = pushForward safeIO memtype cstate0 . pullBack safeIO memtype cstate0    loop 0 trc = trc   loop n trc =@@ -220,10 +228,15 @@     in if trc' /= trc then loop (n-1) trc' else trc  -- | Put a trace into lexicographic (by thread ID) normal form.-lexicoNormalForm :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]-lexicoNormalForm safeIO memtype = go where+lexicoNormalForm+  :: Bool+  -> MemType+  -> ConcurrencyState+  -> [(ThreadId, ThreadAction)]+  -> [(ThreadId, ThreadAction)]+lexicoNormalForm safeIO memtype cstate0 = go where   go trc =-    let trc' = permuteBy safeIO memtype (repeat (>)) trc+    let trc' = permuteBy safeIO memtype cstate0 (repeat (>)) trc     in if trc == trc' then trc else go trc'  -- | Swap adjacent independent actions in the trace if a predicate@@ -231,25 +244,31 @@ permuteBy   :: Bool   -> MemType+  -> ConcurrencyState   -> [ThreadId -> ThreadId -> Bool]   -> [(ThreadId, ThreadAction)]   -> [(ThreadId, ThreadAction)]-permuteBy safeIO memtype = go initialDepState where+permuteBy safeIO memtype = go where   go ds (p:ps) (t1@(tid1, ta1):t2@(tid2, ta2):trc)     | independent safeIO ds tid1 ta1 tid2 ta2 && p tid1 tid2 = go' ds ps t2 (t1 : trc)     | otherwise = go' ds ps t1 (t2 : trc)   go _ _ trc = trc -  go' ds ps t@(tid, ta) trc = t : go (updateDepState memtype ds tid ta) ps trc+  go' ds ps t@(tid, ta) trc = t : go (updateCState memtype ds tid ta) ps trc  -- | Throw away commit actions which are followed by a memory barrier.-dropCommits :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]-dropCommits _ SequentialConsistency = id-dropCommits safeIO memtype = go initialDepState where+dropCommits+  :: Bool+  -> MemType+  -> ConcurrencyState+  -> [(ThreadId, ThreadAction)]+  -> [(ThreadId, ThreadAction)]+dropCommits _ SequentialConsistency = const id+dropCommits safeIO memtype = go where   go ds (t1@(tid1, ta1@(CommitIORef _ iorefid)):t2@(tid2, ta2):trc)     | isBarrier (simplifyAction ta2) && numBuffered ds iorefid == 1 = go ds (t2:trc)-    | independent safeIO ds tid1 ta1 tid2 ta2 = t2 : go (updateDepState memtype ds tid2 ta2) (t1:trc)-  go ds (t@(tid,ta):trc) = t : go (updateDepState memtype ds tid ta) trc+    | independent safeIO ds tid1 ta1 tid2 ta2 = t2 : go (updateCState memtype ds tid2 ta2) (t1:trc)+  go ds (t@(tid,ta):trc) = t : go (updateCState memtype ds tid ta) trc   go _ [] = []  -- | Attempt to reduce context switches by \"pulling\" thread actions@@ -259,10 +278,15 @@ -- act3)]@, where @act2@ and @act3@ are independent.  In this case -- 'pullBack' will swap them, giving the sequence @[(tidA, act1), -- (tidA, act3), (tidB, act2)]@.  It works for arbitrary separations.-pullBack :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]-pullBack safeIO memtype = go initialDepState where+pullBack+  :: Bool+  -> MemType+  -> ConcurrencyState+  -> [(ThreadId, ThreadAction)]+  -> [(ThreadId, ThreadAction)]+pullBack safeIO memtype = go where   go ds (t1@(tid1, ta1):trc@((tid2, _):_)) =-    let ds' = updateDepState memtype ds tid1 ta1+    let ds' = updateCState memtype ds tid1 ta1         trc' = if tid1 /= tid2                then maybe trc (uncurry (:)) (findAction tid1 ds' trc)                else trc@@ -272,7 +296,7 @@   findAction tid0 = fgo where     fgo ds (t@(tid, ta):trc)       | tid == tid0 = Just (t, trc)-      | otherwise = case fgo (updateDepState memtype ds tid ta) trc of+      | otherwise = case fgo (updateCState memtype ds tid ta) trc of           Just (ft@(ftid, fa), trc')             | independent safeIO ds tid ta ftid fa -> Just (ft, t:trc')           _ -> Nothing@@ -288,10 +312,15 @@ -- act3)]@, where @act1@ and @act2@ are independent.  In this case -- 'pushForward' will swap them, giving the sequence @[(tidB, act2), -- (tidA, act1), (tidA, act3)]@.  It works for arbitrary separations.-pushForward :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]-pushForward safeIO memtype = go initialDepState where+pushForward+  :: Bool+  -> MemType+  -> ConcurrencyState+  -> [(ThreadId, ThreadAction)]+  -> [(ThreadId, ThreadAction)]+pushForward safeIO memtype = go where   go ds (t1@(tid1, ta1):trc@((tid2, _):_)) =-    let ds' = updateDepState memtype ds tid1 ta1+    let ds' = updateCState memtype ds tid1 ta1     in if tid1 /= tid2        then maybe (t1 : go ds' trc) (go ds) (findAction tid1 ta1 ds trc)        else t1 : go ds' trc@@ -300,7 +329,7 @@   findAction tid0 ta0 = fgo where     fgo ds (t@(tid, ta):trc)       | tid == tid0 = Just ((tid0, ta0) : t : trc)-      | independent safeIO ds tid0 ta0 tid ta = (t:) <$> fgo (updateDepState memtype ds tid ta) trc+      | independent safeIO ds tid0 ta0 tid ta = (t:) <$> fgo (updateCState memtype ds tid ta) trc       | otherwise = Nothing     fgo _ _ = Nothing 

@@ -1,7 +1,6 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE LambdaCase #-} {-# LANGUAGE ViewPatterns #-}  -- |@@ -10,7 +9,7 @@ -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : DeriveAnyClass, DeriveGeneric, FlexibleContexts, LambdaCase, ViewPatterns+-- Portability : DeriveAnyClass, DeriveGeneric, FlexibleContexts, ViewPatterns -- -- Internal types and functions for SCT via dynamic partial-order -- reduction.  This module is NOT considered to form part of the@@ -18,8 +17,7 @@ module Test.DejaFu.SCT.Internal.DPOR where  import           Control.Applicative  ((<|>))-import           Control.DeepSeq      (NFData(..))-import           Control.Exception    (MaskingState(..))+import           Control.DeepSeq      (NFData) import qualified Data.Foldable        as F import           Data.Function        (on) import           Data.List            (nubBy, partition, sortOn)@@ -104,7 +102,7 @@   , bcktBacktracks :: Map ThreadId Bool   -- ^ The list of alternative threads to run, and whether those   -- alternatives were added conservatively due to the bound.-  , bcktState      :: DepState+  , bcktState      :: ConcurrencyState   -- ^ Some domain-specific state at this point.   } deriving (Eq, Show, Generic, NFData) @@ -164,12 +162,14 @@   -> Trace   -- ^ The execution trace: the decision made, the runnable threads,   -- and the action performed.+  -> ConcurrencyState+  -- ^ The initial concurrency state   -> DPOR   -> DPOR-incorporateTrace safeIO memtype conservative trace dpor0 = grow initialDepState (initialDPORThread dpor0) trace dpor0 where+incorporateTrace safeIO memtype conservative trace state0 dpor0 = grow state0 (initialDPORThread dpor0) trace dpor0 where   grow state tid trc@((d, _, a):rest) dpor =     let tid'   = tidOf tid d-        state' = updateDepState memtype state tid' a+        state' = updateCState memtype state tid' a     in case dporNext dpor of          Just (t, child)            | t == tid' ->@@ -190,7 +190,7 @@    -- Construct a new subtree corresponding to a trace suffix.   subtree state tid sleep ((_, _, a):rest) = validateDPOR $-    let state' = updateDepState memtype state tid a+    let state' = updateCState memtype state tid a         sleep' = M.filterWithKey (\t a' -> not $ dependent safeIO state' tid a t a') sleep     in DPOR         { dporRunnable = S.fromList $ case rest of@@ -235,6 +235,8 @@   -> Bool   -- ^ Whether the computation was aborted due to no decisions being   -- in-bounds.+  -> ConcurrencyState+  -- ^ The initial concurrency state.   -> 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@@ -244,12 +246,12 @@   -> Trace   -- ^ The execution trace.   -> [BacktrackStep]-findBacktrackSteps safeIO memtype backtrack boundKill = go initialDepState S.empty initialThread [] . F.toList where+findBacktrackSteps safeIO memtype backtrack boundKill state0 = go state0 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 memtype state tid' a+        state' = updateCState memtype state tid' a         this = BacktrackStep           { bcktThreadid   = tid'           , bcktDecision   = d@@ -275,23 +277,15 @@                  , u /= v                  , i <- maybeToList (findIndex u n v tagged)] -        findIndex u n v = go' True where+        findIndex u n v = go' where           {-# INLINE go' #-}-          go' final ((i,b):rest)-            -- Don't cross subconcurrency boundaries-            | isSubC final b = Nothing+          go' ((i,b):rest)             -- 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) = Just i-            | otherwise = go' False rest-          go' _ [] = Nothing--          {-# INLINE isSubC #-}-          isSubC final b = case bcktAction b of-            Stop -> not final && bcktThreadid b == initialThread-            Subconcurrency -> bcktThreadid b == initialThread-            _ -> False+            | otherwise = go' rest+          go' [] = Nothing            {-# INLINE isDependent #-}           isDependent b@@ -352,7 +346,7 @@   , schedBoundKill :: Bool   -- ^ Whether the execution was terminated due to all decisions being   -- out of bounds.-  , schedDepState  :: DepState+  , schedCState    :: ConcurrencyState   -- ^ State used by the dependency function to determine when to   -- remove decisions from the sleep set.   , schedBState    :: Maybe k@@ -364,14 +358,16 @@   -- ^ The initial sleep set.   -> [ThreadId]   -- ^ The schedule prefix.+  -> ConcurrencyState+  -- ^ The initial concurrency state.   -> DPORSchedState k-initialDPORSchedState sleep prefix = DPORSchedState+initialDPORSchedState sleep prefix state0 = DPORSchedState   { schedSleep     = sleep   , schedPrefix    = prefix   , schedBPoints   = Sq.empty   , schedIgnore    = False   , schedBoundKill = False-  , schedDepState  = initialDepState+  , schedCState    = state0   , schedBState    = Nothing   } @@ -450,19 +446,22 @@ dporSched :: HasCallStack   => Bool   -- ^ True if all IO is thread safe.-  -> MemType   -> IncrementalBoundFunc k   -- ^ Bound function: returns true if that schedule prefix terminated   -- with the lookahead decision fits within the bound.   -> Scheduler (DPORSchedState k)-dporSched safeIO memtype boundf = Scheduler $ \prior threads s ->+dporSched safeIO boundf = Scheduler $ \prior threads cstate s ->   let     -- The next scheduler state     nextState rest = s       { schedBPoints  = schedBPoints s |> (restrictToBound fst threads', rest)-      , schedDepState = nextDepState+      -- we only update this after using the current value; so in+      -- effect this field is the depstate *before* the action which+      -- just happened, we need this because we need to know if the+      -- prior action (in the state we did it from) is dependent with+      -- anything in the sleep set.+      , schedCState = cstate       }-    nextDepState = let ds = schedDepState s in maybe ds (uncurry $ updateDepState memtype ds) prior      -- Pick a new thread to run, not considering bounds. Choose the     -- current thread if available and it hasn't just yielded,@@ -530,7 +529,7 @@     [] ->       let choices  = restrictToBound id initialise           checkDep t a = case prior of-            Just (tid, act) -> dependent safeIO (schedDepState s) tid act t a+            Just (tid, act) -> dependent safeIO (schedCState 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@@ -550,18 +549,13 @@ -- -- This implements a stronger check that @not (dependent ...)@, as it -- handles some cases which 'dependent' doesn't need to care about.------ This should not be used to re-order traces which contain--- subconcurrency.-independent :: Bool -> DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool+independent :: Bool -> ConcurrencyState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool independent safeIO ds t1 a1 t2 a2     | t1 == t2 = False     | check t1 a1 t2 a2 = False     | check t2 a2 t1 a1 = False     | otherwise = not (dependent safeIO ds t1 a1 t2 a2)   where-    -- @dontCheck@ must be the first thing in the computation.-    check _ (DontCheck _) _ _ = True     -- can't re-order any action of a thread with the fork which     -- created it.     check _ (Fork t) tid _ | t == tid = True@@ -582,7 +576,7 @@ -- 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 :: Bool -> DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool+dependent :: Bool -> ConcurrencyState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool dependent safeIO ds t1 a1 t2 a2 = case (a1, a2) of   -- When masked interruptible, a thread can only be interrupted when   -- actually blocked. 'dependent'' has to assume that all@@ -614,7 +608,7 @@ -- -- Termination of the initial thread is handled specially in the DPOR -- implementation.-dependent' :: Bool -> DepState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool+dependent' :: Bool -> ConcurrencyState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool dependent' safeIO ds t1 a1 t2 l2 = case (a1, l2) of   -- Worst-case assumption: all IO is dependent.   (LiftIO, WillLiftIO) -> not safeIO@@ -643,7 +637,7 @@ -- | 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 :: ConcurrencyState -> ActionType -> ActionType -> Bool dependentActions ds a1 a2 = case (a1, a2) of   (UnsynchronisedRead _, UnsynchronisedRead _) -> False @@ -676,131 +670,6 @@   (SynchronisedRead  v1, SynchronisedWrite v2) | v1 == v2 -> True    (_, _) -> maybe False (\r -> Just r == iorefOf a2) (iorefOf a1)------------------------------------------------------------------------------------ ** Dependency function state--data DepState = DepState-  { depIOState :: Map IORefId Int-  -- ^ Keep track of which @IORef@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 ( depIOState 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 :: MemType -> DepState -> ThreadId -> ThreadAction -> DepState-updateDepState memtype depstate tid act = DepState-  { depIOState   = updateIOState memtype act $ depIOState   depstate-  , depMVState   = updateMVState         act $ depMVState   depstate-  , depMaskState = updateMaskState tid   act $ depMaskState depstate-  }---- | Update the @IORef@ buffer state with the action that has just--- happened.-updateIOState :: MemType -> ThreadAction -> Map IORefId Int -> Map IORefId Int-updateIOState SequentialConsistency _ = const M.empty-updateIOState _ (CommitIORef _ r) = (`M.alter` r) $ \case-  Just 1  -> Nothing-  Just n  -> Just (n-1)-  Nothing -> Nothing-updateIOState _ (WriteIORef    r) = M.insertWith (+) r 1-updateIOState _ 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 tid (Throw True) = M.delete tid-updateMaskState _ (ThrowTo tid True) = M.delete tid-updateMaskState tid Stop = M.delete tid-updateMaskState _ _ = id---- | Check if a @IORef@ has a buffered write pending.-isBuffered :: DepState -> IORefId -> Bool-isBuffered depstate r = numBuffered depstate r /= 0---- | Check how many buffered writes an @IORef@ has.-numBuffered :: DepState -> IORefId -> Int-numBuffered depstate r = M.findWithDefault 0 r (depIOState 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

@@ -3,11 +3,11 @@  -- | -- Module      : Test.DejaFu.SCT.Internal.Weighted--- Copyright   : (c) 2015--2018 Michael Walker+-- Copyright   : (c) 2015--2019 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : portable+-- Portability : DeriveAnyClass, DeriveGeneric -- -- Internal types and functions for SCT via weighted random -- scheduling.  This module is NOT considered to form part of the@@ -31,19 +31,21 @@ data RandSchedState g = RandSchedState   { schedWeights :: Map ThreadId Int   -- ^ The thread weights: used in determining which to run.-  , schedGen     :: g+  , schedLengthBound :: Maybe LengthBound+  -- ^ The optional length bound.+  , schedGen :: g   -- ^ The random number generator.   } deriving (Eq, Show, Generic, NFData)  -- | Initial weighted random scheduler state.-initialRandSchedState :: g -> RandSchedState g+initialRandSchedState :: Maybe LengthBound -> g -> RandSchedState g initialRandSchedState = RandSchedState 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 ->+randSched weightf = Scheduler $ \_ threads _ s ->   let     -- Select a thread     pick idx ((x, f):xs)@@ -61,4 +63,7 @@      -- The runnable threads.     tids = map fst (toList threads)-  in (pick choice enabled, RandSchedState weights' g'')+  in case schedLengthBound s of+    Just 0 -> (Nothing, s)+    Just n -> (pick choice enabled, RandSchedState weights' (Just (n - 1)) g'')+    Nothing -> (pick choice enabled, RandSchedState weights' Nothing g'')

@@ -37,16 +37,19 @@ -- -- 2. The unblocked threads. ----- 3. The state.+-- 3. The concurrency state. --+-- 4. The scheduler state.+-- -- It returns a thread to execute, or @Nothing@ if execution should -- abort here, and also a new state. ----- @since 0.8.0.0+-- @since 2.0.0.0 newtype Scheduler state = Scheduler   { scheduleThread     :: Maybe (ThreadId, ThreadAction)     -> NonEmpty (ThreadId, Lookahead)+    -> ConcurrencyState     -> state     -> (Maybe ThreadId, state)   }@@ -60,7 +63,7 @@ -- @since 0.8.0.0 randomSched :: RandomGen g => Scheduler g randomSched = Scheduler go where-  go _ threads g =+  go _ threads _ g =     let threads' = map fst (toList threads)         (choice, g') = randomR (0, length threads' - 1) g     in (Just $ eidx threads' choice, g')@@ -71,8 +74,8 @@ -- @since 0.8.0.0 roundRobinSched :: Scheduler () roundRobinSched = Scheduler go where-  go Nothing ((tid,_):|_) _ = (Just tid, ())-  go (Just (prior, _)) threads _ =+  go Nothing ((tid,_):|_) _ _ = (Just tid, ())+  go (Just (prior, _)) threads _ _ =     let threads' = map fst (toList threads)         candidates =           if prior >= maximum threads'@@ -109,7 +112,7 @@ -- @since 0.8.0.0 makeNonPreemptive :: Scheduler s -> Scheduler s makeNonPreemptive sched = Scheduler newsched where-  newsched p@(Just (prior, _)) threads s+  newsched p@(Just (prior, _)) threads cs s     | prior `elem` map fst (toList threads) = (Just prior, s)-    | otherwise = scheduleThread sched p threads s-  newsched Nothing threads s = scheduleThread sched Nothing threads s+    | otherwise = scheduleThread sched p threads cs s+  newsched Nothing threads cs s = scheduleThread sched Nothing threads cs s

@@ -23,7 +23,7 @@   , randomly   , uniformly -  -- *** Schedule bounds+  -- *** Schedule bounding    -- | Schedule bounding is used by the 'systematically' approach to   -- limit the search-space, which in general will be huge.@@ -50,13 +50,23 @@   , Bounds(..)   , PreemptionBound(..)   , FairBound(..)-  , LengthBound(..)   , defaultBounds   , defaultPreemptionBound   , defaultFairBound-  , defaultLengthBound   , noBounds +  -- *** Length bounding++  -- | Length bounding can be used to test potentially nonterminating+  -- computations.  Any execution exceeding the length bound gets+  -- discarded.+  --+  -- While 'PreemptionBound' and 'FairBound' are only used by+  -- 'systematically', all 'Way's use the length bound.++  , LengthBound(..)+  , llengthBound+   -- ** The @MemType@    -- | When executed on a multi-core processor some @IORef@ / @IORef@@@ -258,6 +268,7 @@ fromWayAndMemType :: Applicative n => Way -> MemType -> Settings n a fromWayAndMemType way memtype = Settings   { _way = way+  , _lengthBound = Nothing   , _memtype = memtype   , _discard = Nothing   , _debugShow = Nothing@@ -332,7 +343,7 @@ uniformly = Randomly $ \g -> (1, g)  ---------------------------------------------------------------------------------- Schedule bounds+-- Schedule bounding  -- | All bounds enabled, using their default values. --@@ -344,7 +355,6 @@ defaultBounds = Bounds   { boundPreemp = Just defaultPreemptionBound   , boundFair   = Just defaultFairBound-  , boundLength = Nothing   }  -- | A sensible default preemption bound: 2.@@ -365,14 +375,6 @@ defaultFairBound :: FairBound defaultFairBound = 5 --- | There is no default length bound.------ This is only suitable if your computation will always terminate!------ @since 1.8.0.0-defaultLengthBound :: LengthBound-defaultLengthBound = 250- -- | No bounds enabled. This forces the scheduler to just use -- partial-order reduction and sleep sets to prune the search -- space. This will /ONLY/ work if your computation always terminates!@@ -382,8 +384,16 @@ noBounds = Bounds   { boundPreemp = Nothing   , boundFair   = Nothing-  , boundLength = Nothing   }++-------------------------------------------------------------------------------+-- Length bounding++-- | A lens into the length bound.+--+-- @since 2.0.0.0+llengthBound :: Lens' (Settings n a) (Maybe LengthBound)+llengthBound afb s = (\b -> s {_lengthBound = b}) <$> afb (_lengthBound s)  ------------------------------------------------------------------------------- -- The @MemType@

@@ -5,7 +5,7 @@  -- | -- Module      : Test.DejaFu.Types--- Copyright   : (c) 2017--2018 Michael Walker+-- Copyright   : (c) 2017--2019 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental@@ -21,7 +21,11 @@ import           Data.Function                        (on) import           Data.Functor.Contravariant           (Contravariant(..)) import           Data.Functor.Contravariant.Divisible (Divisible(..))+import           Data.Map.Strict                      (Map)+import qualified Data.Map.Strict                      as M import           Data.Semigroup                       (Semigroup(..))+import           Data.Set                             (Set)+import qualified Data.Set                             as S import           GHC.Generics                         (Generic)  -------------------------------------------------------------------------------@@ -106,7 +110,7 @@  -- | All the actions that a thread can perform. ----- @since 1.11.0.0+-- @since 2.0.0.0 data ThreadAction =     Fork ThreadId   -- ^ Start a new thread.@@ -194,12 +198,8 @@   -- ^ 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@.-  | DontCheck Trace-  -- ^ Execute an action with @dontCheck@.+  | RegisterInvariant+  -- ^ Register an invariant.   deriving (Eq, Generic, Show)  -- this makes me sad@@ -242,13 +242,11 @@   rnf LiftIO = ()   rnf Return = ()   rnf Stop = ()-  rnf Subconcurrency = ()-  rnf StopSubconcurrency = ()-  rnf (DontCheck as) = rnf as+  rnf RegisterInvariant = ()  -- | A one-step look-ahead at what a thread will do next. ----- @since 1.11.0.0+-- @since 2.0.0.0 data Lookahead =     WillFork   -- ^ Will start a new thread.@@ -325,12 +323,8 @@   -- ^ 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@.-  | WillDontCheck-  -- ^ Will execute an action with @dontCheck@.+  | WillRegisterInvariant+  -- ^ Will register an invariant   deriving (Eq, Generic, Show)  -- this also makes me sad@@ -368,9 +362,7 @@   rnf WillLiftIO = ()   rnf WillReturn = ()   rnf WillStop = ()-  rnf WillSubconcurrency = ()-  rnf WillStopSubconcurrency = ()-  rnf WillDontCheck = ()+  rnf WillRegisterInvariant = ()  -- | All the actions that an STM transaction can perform. --@@ -438,19 +430,14 @@ ------------------------------------------------------------------------------- -- * Conditions --- | A type synonym for 'Condition', use that instead.------ @since 1.12.0.0-{-# DEPRECATED Failure "The 'Failure' type has been split up into 'Condition' and 'Error', with different semantics." #-}-type Failure = Condition- -- | An indication of how a concurrent computation terminated, if it -- didn't produce a value. -- -- The @Eq@, @Ord@, and @NFData@ instances compare/evaluate the--- exception with @show@ in the @UncaughtException@ case.+-- exception with @show@ in the @UncaughtException@ and+-- @InvariantFailure@ cases. ----- @since 1.12.0.0+-- @since 2.0.0.0 data Condition   = Abort   -- ^ The scheduler chose to abort execution. This will be produced@@ -458,20 +445,18 @@   -- 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.+  -- ^ Every thread is blocked   | UncaughtException SomeException   -- ^ An uncaught exception bubbled to the top of the computation.+  | InvariantFailure SomeException+  -- ^ An uncaught exception caused an invariant to fail.   deriving (Show, Generic)  instance Eq Condition where   Abort                  == Abort                  = True   Deadlock               == Deadlock               = True-  STMDeadlock            == STMDeadlock            = True   (UncaughtException e1) == (UncaughtException e2) = show e1 == show e2+  (InvariantFailure  e1) == (InvariantFailure  e2) = show e1 == show e2   _ == _ = False  instance Ord Condition where@@ -479,11 +464,12 @@     transform :: Condition -> (Int, Maybe String)     transform Abort = (1, Nothing)     transform Deadlock = (2, Nothing)-    transform STMDeadlock = (3, Nothing)-    transform (UncaughtException e) = (4, Just (show e))+    transform (UncaughtException e) = (3, Just (show e))+    transform (InvariantFailure  e) = (4, Just (show e))  instance NFData Condition where   rnf (UncaughtException e) = rnf (show e)+  rnf (InvariantFailure  e) = rnf (show e)   rnf f = f `seq` ()  -- | Check if a condition is an @Abort@.@@ -493,12 +479,11 @@ isAbort Abort = True isAbort _ = False --- | Check if a condition is a @Deadlock@ or an @STMDeadlock@.+-- | Check if a condition is a @Deadlock@. -- -- @since 0.9.0.0 isDeadlock :: Condition -> Bool isDeadlock Deadlock = True-isDeadlock STMDeadlock = True isDeadlock _ = False  -- | Check if a condition is an @UncaughtException@@@ -508,13 +493,20 @@ isUncaughtException (UncaughtException _) = True isUncaughtException _ = False +-- | Check if a condition is an @InvariantFailure@+--+-- @since 2.0.0.0+isInvariantFailure :: Condition -> Bool+isInvariantFailure (InvariantFailure _) = True+isInvariantFailure _ = False+ ------------------------------------------------------------------------------- -- * Errors  -- | An indication that there is a bug in dejafu or you are using it -- incorrectly. ----- @since 1.12.0.0+-- @since 2.0.0.0 data Error   = ScheduledBlockedThread   -- ^ Raised as an exception if the scheduler attempts to schedule a@@ -522,14 +514,6 @@   | ScheduledMissingThread   -- ^ Raised as an exception if the scheduler attempts to schedule a   -- nonexistent thread.-  | NestedSubconcurrency-  -- ^ Raised as an exception if a @subconcurrency@ is nested inside-  -- another @subconcurrency@ or a @dontCheck@.-  | MultithreadedSubconcurrency-  -- ^ Raised as an exception if @subconcurrency@ is called after-  -- forking threads.-  | LateDontCheck-  -- ^ Raised as an exception if @dontCheck@ is called after the first action.   deriving (Show, Eq, Ord, Bounded, Enum, Generic)  instance Exception Error@@ -538,33 +522,17 @@ -- -- @since 1.12.0.0 isSchedulerError :: Error -> Bool-isSchedulerError ScheduledBlockedThread = True-isSchedulerError ScheduledMissingThread = True-isSchedulerError _ = False---- | Check if an error is an incorrect usage of dejafu.------ @since 1.12.0.0-isIncorrectUsage :: Error -> Bool-isIncorrectUsage NestedSubconcurrency = True-isIncorrectUsage MultithreadedSubconcurrency = True-isIncorrectUsage LateDontCheck = True-isIncorrectUsage _ = False+isSchedulerError _ = True  ------------------------------------------------------------------------------- -- * Schedule bounding --- | @since 0.2.0.0+-- | @since 2.0.0.0 data Bounds = Bounds   { boundPreemp :: Maybe PreemptionBound   , boundFair   :: Maybe FairBound-  , boundLength :: Maybe LengthBound-  } deriving (Eq, Ord, Read, Show)---- | @since 1.3.1.0-deriving instance Generic Bounds+  } deriving (Eq, Ord, Read, Show, Generic) --- | @since 0.5.1.0 instance NFData Bounds  -- | Restrict the number of pre-emptive context switches allowed in an@@ -757,3 +725,97 @@  -- | @since 1.3.1.0 instance NFData MonadFailException++-------------------------------------------------------------------------------+-- ** Concurrency state++-- | A summary of the concurrency state of the program.+--+-- @since 2.0.0.0+data ConcurrencyState = ConcurrencyState+  { concIOState :: Map IORefId Int+  -- ^ Keep track of which @IORef@s have buffered writes.+  , concMVState :: Set MVarId+  -- ^ Keep track of which @MVar@s are full.+  , concMaskState :: 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 ConcurrencyState where+  rnf cstate = rnf+    ( concIOState cstate+    , concMVState cstate+    , [(t, show m) | (t, m) <- M.toList (concMaskState cstate)]+    )++-- | Check if a @IORef@ has a buffered write pending.+--+-- @since 2.0.0.0+isBuffered :: ConcurrencyState -> IORefId -> Bool+isBuffered cstate r = numBuffered cstate r /= 0++-- | Check how many buffered writes an @IORef@ has.+--+-- @since 2.0.0.0+numBuffered :: ConcurrencyState -> IORefId -> Int+numBuffered cstate r = M.findWithDefault 0 r (concIOState cstate)++-- | Check if an @MVar@ is full.+--+-- @since 2.0.0.0+isFull :: ConcurrencyState -> MVarId -> Bool+isFull cstate v = S.member v (concMVState cstate)++-- | Check if an exception can interrupt a thread (action).+--+-- @since 2.0.0.0+canInterrupt :: ConcurrencyState -> ThreadId -> ThreadAction -> Bool+canInterrupt cstate tid act+  -- If masked interruptible, blocked actions can be interrupted.+  | isMaskedInterruptible cstate tid = case act of+    BlockedPutMVar  _ -> True+    BlockedReadMVar _ -> True+    BlockedTakeMVar _ -> True+    BlockedSTM      _ -> True+    BlockedThrowTo  _ -> True+    _ -> False+  -- If masked uninterruptible, nothing can be.+  | isMaskedUninterruptible cstate tid = False+  -- If no mask, anything can be.+  | otherwise = True++-- | Check if an exception can interrupt a thread (lookahead).+--+-- @since 2.0.0.0+canInterruptL :: ConcurrencyState -> ThreadId -> Lookahead -> Bool+canInterruptL cstate tid lh+  -- If masked interruptible, actions which can block may be+  -- interrupted.+  | isMaskedInterruptible cstate tid = case lh of+    WillPutMVar  _ -> True+    WillReadMVar _ -> True+    WillTakeMVar _ -> True+    WillSTM        -> True+    WillThrowTo  _ -> True+    _ -> False+  -- If masked uninterruptible, nothing can be.+  | isMaskedUninterruptible cstate tid = False+  -- If no mask, anything can be.+  | otherwise = True++-- | Check if a thread is masked interruptible.+--+-- @since 2.0.0.0+isMaskedInterruptible :: ConcurrencyState -> ThreadId -> Bool+isMaskedInterruptible cstate tid =+  M.lookup tid (concMaskState cstate) == Just MaskedInterruptible++-- | Check if a thread is masked uninterruptible.+--+-- @since 2.0.0.0+isMaskedUninterruptible :: ConcurrencyState -> ThreadId -> Bool+isMaskedUninterruptible cstate tid =+  M.lookup tid (concMaskState cstate) == Just MaskedUninterruptible

@@ -84,8 +84,8 @@ showCondition :: Condition -> String showCondition Abort = "[abort]" showCondition Deadlock = "[deadlock]"-showCondition STMDeadlock = "[stm-deadlock]" showCondition (UncaughtException exc) = "[" ++ displayException exc ++ "]"+showCondition (InvariantFailure _) = "[invariant failure]"  ------------------------------------------------------------------------------- -- * Scheduling

@@ -2,18 +2,18 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                dejafu-version:             1.12.0.0+version:             2.0.0.0 synopsis:            A library for unit-testing concurrent programs.  description:   /[Déjà Fu is] A martial art in which the user's limbs move in time as well as space, […] It is best described as "the feeling that you have been kicked in the head this way before"/ -- Terry Pratchett, Thief of Time   .   This package builds on the-  [concurrency](https://hackage.haskell.org/package/concurrency)+  <https://hackage.haskell.org/package/concurrency concurrency>   package by enabling you to deterministically test your concurrent   programs.   .-  See the [website](https://dejafu.readthedocs.io) or README for more.+  See the <https://dejafu.readthedocs.io website> or README for more.  homepage:            https://github.com/barrucadu/dejafu license:             MIT@@ -33,7 +33,7 @@ source-repository this   type:     git   location: https://github.com/barrucadu/dejafu.git-  tag:      dejafu-1.12.0.0+  tag:      dejafu-2.0.0.0  library   exposed-modules:     Test.DejaFu@@ -48,6 +48,7 @@                      , Test.DejaFu.Conc.Internal                      , Test.DejaFu.Conc.Internal.Common                      , Test.DejaFu.Conc.Internal.Memory+                     , Test.DejaFu.Conc.Internal.Program                      , Test.DejaFu.Conc.Internal.STM                      , Test.DejaFu.Conc.Internal.Threading                      , Test.DejaFu.Internal