mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-11-29 11:23:43 +03:00
Merge pull request #299 from barrucadu/make-dejafu-pure-again
Make dejafu pure again
This commit is contained in:
commit
1a4f99de9c
@ -45,10 +45,10 @@ There are a few different packages under the Déjà Fu umbrella:
|
||||
|
||||
| | Version | Summary |
|
||||
| - | ------- | ------- |
|
||||
| [concurrency][h:conc] | 1.6.2.0 | Typeclasses, functions, and data types for concurrency and STM. |
|
||||
| [dejafu][h:dejafu] | 2.0.0.1 | Systematic testing for Haskell concurrency. |
|
||||
| [hunit-dejafu][h:hunit] | 2.0.0.0 | Deja Fu support for the HUnit test framework. |
|
||||
| [tasty-dejafu][h:tasty] | 2.0.0.0 | Deja Fu support for the Tasty test framework. |
|
||||
| [concurrency][h:conc] | 1.7.0.0 | Typeclasses, functions, and data types for concurrency and STM. |
|
||||
| [dejafu][h:dejafu] | 2.1.0.0 | Systematic testing for Haskell concurrency. |
|
||||
| [hunit-dejafu][h:hunit] | 2.0.0.1 | Deja Fu support for the HUnit test framework. |
|
||||
| [tasty-dejafu][h:tasty] | 2.0.0.1 | Deja Fu support for the Tasty test framework. |
|
||||
|
||||
Each package has its own README and CHANGELOG in its subdirectory.
|
||||
|
||||
|
@ -7,6 +7,25 @@ standard Haskell versioning scheme.
|
||||
.. _PVP: https://pvp.haskell.org/
|
||||
|
||||
|
||||
1.7.0.0 (2019-03-24)
|
||||
--------------------
|
||||
|
||||
* Git: :tag:`concurrency-1.7.0.0`
|
||||
* Hackage: :hackage:`concurrency-1.7.0.0`
|
||||
|
||||
Added
|
||||
~~~~~
|
||||
|
||||
* The ``Control.Monad.Conc.Class.supportsBoundThreads`` function, like
|
||||
``rtsSupportsBoundThreads`` but returns a monadic result.
|
||||
|
||||
Deprecated
|
||||
~~~~~~~~~~
|
||||
|
||||
* ``Control.Monad.Conc.Class.rtsSupportsBoundThreads``, in favour of
|
||||
``supportsBoundThreads``.
|
||||
|
||||
|
||||
1.6.2.0 (2018-11-28)
|
||||
--------------------
|
||||
|
||||
|
@ -55,7 +55,7 @@ module Control.Monad.Conc.Class
|
||||
-- To a foreign library, the bound thread will look exactly like an
|
||||
-- ordinary operating system thread created using OS functions like
|
||||
-- pthread_create or CreateThread.
|
||||
, IO.rtsSupportsBoundThreads
|
||||
, rtsSupportsBoundThreads
|
||||
, runInBoundThread
|
||||
, runInUnboundThread
|
||||
|
||||
@ -150,7 +150,7 @@ import qualified Control.Monad.Writer.Strict as WS
|
||||
-- Do not be put off by the use of @UndecidableInstances@, it is safe
|
||||
-- here.
|
||||
--
|
||||
-- @since 1.6.0.0
|
||||
-- @since 1.7.0.0
|
||||
class ( Monad m
|
||||
, MonadCatch m, MonadThrow m, MonadMask m
|
||||
, MonadSTM (STM m)
|
||||
@ -160,6 +160,7 @@ class ( Monad m
|
||||
(forkWithUnmask | forkWithUnmaskN)
|
||||
, (forkOnWithUnmask | forkOnWithUnmaskN)
|
||||
, (forkOSWithUnmask | forkOSWithUnmaskN)
|
||||
, supportsBoundThreads
|
||||
, isCurrentThreadBound
|
||||
, getNumCapabilities
|
||||
, setNumCapabilities
|
||||
@ -271,6 +272,13 @@ class ( Monad m
|
||||
forkOSWithUnmaskN :: String -> ((forall a. m a -> m a) -> m ()) -> m (ThreadId m)
|
||||
forkOSWithUnmaskN _ = forkOSWithUnmask
|
||||
|
||||
-- | Returns 'True' if bound threads can be forked. If 'False',
|
||||
-- 'isCurrentThreadBound' will always return 'False' and both
|
||||
-- 'forkOS' and 'runInBoundThread' will fail.
|
||||
--
|
||||
-- @since 1.7.0.0
|
||||
supportsBoundThreads :: m Bool
|
||||
|
||||
-- | Returns 'True' if the calling thread is bound, that is, if it
|
||||
-- is safe to use foreign libraries that rely on thread-local state
|
||||
-- from the calling thread.
|
||||
@ -560,6 +568,18 @@ forkOnN name i ma = forkOnWithUnmaskN name i (const ma)
|
||||
forkOSN :: MonadConc m => String -> m () -> m (ThreadId m)
|
||||
forkOSN name ma = forkOSWithUnmaskN name (const ma)
|
||||
|
||||
-- | 'True' if bound threads are supported. If
|
||||
-- 'rtsSupportsBoundThreads' is 'False', 'isCurrentThreadBound' will
|
||||
-- always return 'False' and both 'forkOS' and 'runInBoundThread' will
|
||||
-- fail.
|
||||
--
|
||||
-- Use 'supportsBoundThreads' in 'MonadConc' instead.
|
||||
--
|
||||
-- @since 1.3.0.0
|
||||
{-# DEPRECATED rtsSupportsBoundThreads "Use 'supportsBoundThreads' instead" #-}
|
||||
rtsSupportsBoundThreads :: Bool
|
||||
rtsSupportsBoundThreads = IO.rtsSupportsBoundThreads
|
||||
|
||||
-- | Run the computation passed as the first argument. If the calling
|
||||
-- thread is not /bound/, a bound thread is created temporarily.
|
||||
-- @runInBoundThread@ doesn't finish until the inner computation
|
||||
@ -726,6 +746,7 @@ instance MonadConc IO where
|
||||
labelMe n
|
||||
ma umask
|
||||
|
||||
supportsBoundThreads = pure IO.rtsSupportsBoundThreads
|
||||
isCurrentThreadBound = IO.isCurrentThreadBound
|
||||
|
||||
getNumCapabilities = IO.getNumCapabilities
|
||||
@ -797,6 +818,7 @@ instance MonadConc m => MonadConc (IsConc m) where
|
||||
forkOSWithUnmask ma = toIsConc (forkOSWithUnmask (\umask -> unIsConc $ ma (\mx -> toIsConc (umask $ unIsConc mx))))
|
||||
forkOSWithUnmaskN n ma = toIsConc (forkOSWithUnmaskN n (\umask -> unIsConc $ ma (\mx -> toIsConc (umask $ unIsConc mx))))
|
||||
|
||||
supportsBoundThreads = toIsConc supportsBoundThreads
|
||||
isCurrentThreadBound = toIsConc isCurrentThreadBound
|
||||
|
||||
getNumCapabilities = toIsConc getNumCapabilities
|
||||
@ -845,6 +867,7 @@ instance C => MonadConc (T m) where { \
|
||||
forkOSWithUnmask = liftedFork F forkOSWithUnmask ; \
|
||||
forkOSWithUnmaskN n = liftedFork F (forkOSWithUnmaskN n ) ; \
|
||||
\
|
||||
supportsBoundThreads = lift supportsBoundThreads ; \
|
||||
isCurrentThreadBound = lift isCurrentThreadBound ; \
|
||||
\
|
||||
getNumCapabilities = lift getNumCapabilities ; \
|
||||
|
@ -2,7 +2,7 @@
|
||||
-- documentation, see http://haskell.org/cabal/users-guide/
|
||||
|
||||
name: concurrency
|
||||
version: 1.6.2.0
|
||||
version: 1.7.0.0
|
||||
synopsis: Typeclasses, functions, and data types for concurrency and STM.
|
||||
|
||||
description:
|
||||
@ -19,7 +19,7 @@ license: MIT
|
||||
license-file: LICENSE
|
||||
author: Michael Walker
|
||||
maintainer: mike@barrucadu.co.uk
|
||||
copyright: (c) 2016--2017 Michael Walker
|
||||
copyright: (c) 2016--2019 Michael Walker
|
||||
category: Concurrency
|
||||
build-type: Simple
|
||||
extra-source-files: README.markdown CHANGELOG.rst
|
||||
@ -32,7 +32,7 @@ source-repository head
|
||||
source-repository this
|
||||
type: git
|
||||
location: https://github.com/barrucadu/dejafu.git
|
||||
tag: concurrency-1.6.2.0
|
||||
tag: concurrency-1.7.0.0
|
||||
|
||||
library
|
||||
exposed-modules: Control.Monad.Conc.Class
|
||||
|
@ -23,13 +23,14 @@ library
|
||||
|
||||
, Integration
|
||||
, Integration.Async
|
||||
, Integration.SingleThreaded
|
||||
, Integration.MultiThreaded
|
||||
, Integration.Refinement
|
||||
, Integration.Litmus
|
||||
, Integration.MonadDejaFu
|
||||
, Integration.MultiThreaded
|
||||
, Integration.Names
|
||||
, Integration.Refinement
|
||||
, Integration.Regressions
|
||||
, Integration.SCT
|
||||
, Integration.Names
|
||||
, Integration.SingleThreaded
|
||||
|
||||
, Examples
|
||||
, Examples.AutoUpdate
|
||||
|
@ -4,6 +4,7 @@ import Test.Tasty.Options (OptionDescription)
|
||||
|
||||
import qualified Integration.Async as A
|
||||
import qualified Integration.Litmus as L
|
||||
import qualified Integration.MonadDejaFu as MD
|
||||
import qualified Integration.MultiThreaded as M
|
||||
import qualified Integration.Names as N
|
||||
import qualified Integration.Refinement as R
|
||||
@ -19,6 +20,7 @@ tests =
|
||||
[ testGroup "Async" A.tests
|
||||
, testGroup "Litmus" L.tests
|
||||
, testGroup "MultiThreaded" M.tests
|
||||
, testGroup "MonadDejaFu" MD.tests
|
||||
, testGroup "Names" N.tests
|
||||
, testGroup "Refinement" R.tests
|
||||
, testGroup "Regressions" G.tests
|
||||
|
66
dejafu-tests/lib/Integration/MonadDejaFu.hs
Normal file
66
dejafu-tests/lib/Integration/MonadDejaFu.hs
Normal file
@ -0,0 +1,66 @@
|
||||
module Integration.MonadDejaFu where
|
||||
|
||||
import qualified Control.Concurrent.Classy as C
|
||||
|
||||
import Control.Monad.Catch.Pure (runCatchT)
|
||||
import Control.Monad.ST (runST)
|
||||
import Test.DejaFu.Conc (Condition(..), Program,
|
||||
roundRobinSched, runConcurrent)
|
||||
import Test.DejaFu.Settings (defaultMemType)
|
||||
import Test.DejaFu.Types (MonadDejaFu)
|
||||
import qualified Test.Tasty.HUnit as TH
|
||||
|
||||
import Common
|
||||
|
||||
tests :: [TestTree]
|
||||
tests =
|
||||
[ testGroup "IO" ioTests
|
||||
, testGroup "ST" stTests
|
||||
]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
ioTests :: [TestTree]
|
||||
ioTests = toTestList
|
||||
[ TH.testCase "Supports bound threads" $
|
||||
let res = single C.supportsBoundThreads
|
||||
in TH.assertEqual "" (Right True) =<< res
|
||||
|
||||
, TH.testCase "Main thread is bound" $
|
||||
let res = single C.isCurrentThreadBound
|
||||
in TH.assertEqual "" (Right True) =<< res
|
||||
|
||||
, TH.testCase "Can fork bound threads" $
|
||||
let res = single $ do
|
||||
_ <- C.forkOS (pure ())
|
||||
pure True
|
||||
in TH.assertEqual "" (Right True) =<< res
|
||||
]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
stTests :: [TestTree]
|
||||
stTests = toTestList
|
||||
[ TH.testCase "Doesn't support bound threads" $
|
||||
let res = runST $ runCatchT $ single C.supportsBoundThreads
|
||||
in TH.assertEqual "" (Right (Right False)) res
|
||||
|
||||
, TH.testCase "Main thread isn't bound" $
|
||||
let res = runST $ runCatchT $ single C.isCurrentThreadBound
|
||||
in TH.assertEqual "" (Right (Right False)) res
|
||||
|
||||
, TH.testCase "Can't fork bound threads" $
|
||||
let res = runST $ runCatchT $ single $ do
|
||||
_ <- C.forkOS (pure ())
|
||||
pure True
|
||||
in case res of
|
||||
Right (Left (UncaughtException _)) -> pure ()
|
||||
_ -> TH.assertFailure ("expected: Right (Left (UncaughtException _))\n but got: " ++ show res)
|
||||
]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
single :: MonadDejaFu n => Program pty n a -> n (Either Condition a)
|
||||
single program =
|
||||
let fst3 (a, _, _) = a
|
||||
in fst3 <$> runConcurrent roundRobinSched defaultMemType () program
|
@ -6,6 +6,67 @@ standard Haskell versioning scheme.
|
||||
|
||||
.. _PVP: https://pvp.haskell.org/
|
||||
|
||||
|
||||
2.1.0.0 (2019-03-24)
|
||||
--------------------
|
||||
|
||||
* Git: :tag:`dejafu-2.1.0.0`
|
||||
* Hackage: :hackage:`dejafu-2.1.0.0`
|
||||
|
||||
Added
|
||||
~~~~~
|
||||
|
||||
* The ``Test.DejaFu.Types.MonadDejaFu`` typeclass, containing the
|
||||
primitives needed to run a concurrent program. There are instances
|
||||
for:
|
||||
* ``IO``, which is probably the ``MonadConc`` instance people used
|
||||
previously, so there is no breaking change there.
|
||||
* ``CatchT (ST t)``, meaning that concurrent programs can be run
|
||||
without ``IO`` once more.
|
||||
|
||||
* Thread action constructors for ``MonadConc``
|
||||
``supportsBoundThreads`` function:
|
||||
* ``Test.DejaFu.Types.ThreadAction``, ``SupportsBoundThreads``
|
||||
* ``Test.DejaFu.Types.Lookahead``, ``WillSupportsBoundThreads``
|
||||
|
||||
Changed
|
||||
~~~~~~~
|
||||
|
||||
* Many functions which had a ``MonadConc`` constraint now have a
|
||||
``MonadDejaFu`` constraint:
|
||||
* In ``Test.DejaFu``
|
||||
* ``autocheck``
|
||||
* ``autocheckWay``
|
||||
* ``autocheckWithSettings``
|
||||
* ``dejafu``
|
||||
* ``dejafuWay``
|
||||
* ``dejafuWithSettings``
|
||||
* ``dejafus``
|
||||
* ``dejafusWay``
|
||||
* ``dejafusWithSettings``
|
||||
* ``runTest``
|
||||
* ``runTestWay``
|
||||
* ``runTestWithSettings``
|
||||
* In ``Test.DejaFu.Conc``
|
||||
* ``runConcurrent``
|
||||
* ``recordSnapshot``
|
||||
* ``runSnapshot``
|
||||
* In ``Test.DejaFu.SCT``
|
||||
* ``runSCT``
|
||||
* ``resultsSet``
|
||||
* ``runSCT'``
|
||||
* ``resultsSet'``
|
||||
* ``runSCTWithSettings``
|
||||
* ``resultsSetWithSettings``
|
||||
* ``runSCTWithSettings'``
|
||||
* ``resultsSetWithSettings'``
|
||||
|
||||
Miscellaneous
|
||||
~~~~~~~~~~~~~
|
||||
|
||||
* The version bound on :hackage:`concurrency` is >=1.7 and <1.8.
|
||||
|
||||
|
||||
2.0.0.1 (2019-03-14)
|
||||
--------------------
|
||||
|
||||
|
@ -313,18 +313,16 @@ interference we have provided: the left term never empties a full
|
||||
, inspectTVar
|
||||
) where
|
||||
|
||||
import Control.Arrow (first)
|
||||
import Control.DeepSeq (NFData(..))
|
||||
import Control.Monad (unless, when)
|
||||
import Control.Monad.Conc.Class (MonadConc)
|
||||
import Control.Monad.IO.Class (MonadIO(..))
|
||||
import Data.Either (isLeft)
|
||||
import Data.Function (on)
|
||||
import Data.List (intercalate, intersperse, partition)
|
||||
import Data.Maybe (catMaybes, isJust, isNothing,
|
||||
mapMaybe)
|
||||
import Data.Profunctor (Profunctor(..))
|
||||
import System.Environment (lookupEnv)
|
||||
import Control.Arrow (first)
|
||||
import Control.DeepSeq (NFData(..))
|
||||
import Control.Monad (unless, when)
|
||||
import Control.Monad.IO.Class (MonadIO(..))
|
||||
import Data.Either (isLeft)
|
||||
import Data.Function (on)
|
||||
import Data.List (intercalate, intersperse, partition)
|
||||
import Data.Maybe (catMaybes, isJust, isNothing, mapMaybe)
|
||||
import Data.Profunctor (Profunctor(..))
|
||||
import System.Environment (lookupEnv)
|
||||
|
||||
import Test.DejaFu.Conc
|
||||
import Test.DejaFu.Internal
|
||||
@ -373,8 +371,8 @@ let relaxed = do
|
||||
-- "world" S0----S2--S0--
|
||||
-- False
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
autocheck :: (MonadConc n, MonadIO n, Eq a, Show a)
|
||||
-- @since 2.1.0.0
|
||||
autocheck :: (MonadDejaFu n, MonadIO n, Eq a, Show a)
|
||||
=> Program pty n a
|
||||
-- ^ The computation to test.
|
||||
-> n Bool
|
||||
@ -405,8 +403,8 @@ autocheck = autocheckWithSettings defaultSettings
|
||||
-- (True,False) S0---------S2----S1----S0---
|
||||
-- False
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
autocheckWay :: (MonadConc n, MonadIO n, Eq a, Show a)
|
||||
-- @since 2.1.0.0
|
||||
autocheckWay :: (MonadDejaFu n, MonadIO n, Eq a, Show a)
|
||||
=> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
@ -440,8 +438,8 @@ autocheckWay way = autocheckWithSettings . fromWayAndMemType way
|
||||
-- (True,False) S0---------S2----S1----S0---
|
||||
-- False
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
autocheckWithSettings :: (MonadConc n, MonadIO n, Eq a, Show a)
|
||||
-- @since 2.1.0.0
|
||||
autocheckWithSettings :: (MonadDejaFu n, MonadIO n, Eq a, Show a)
|
||||
=> Settings n a
|
||||
-- ^ The SCT settings.
|
||||
-> Program pty n a
|
||||
@ -466,8 +464,8 @@ autocheckWithSettings settings = dejafusWithSettings settings
|
||||
-- "world" S0----S2--S0--
|
||||
-- False
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
dejafu :: (MonadConc n, MonadIO n, Show b)
|
||||
-- @since 2.1.0.0
|
||||
dejafu :: (MonadDejaFu n, MonadIO n, Show b)
|
||||
=> String
|
||||
-- ^ The name of the test.
|
||||
-> ProPredicate a b
|
||||
@ -496,8 +494,8 @@ dejafu = dejafuWithSettings defaultSettings
|
||||
-- "world" S0----S2--S1-S0--
|
||||
-- False
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
dejafuWay :: (MonadConc n, MonadIO n, Show b)
|
||||
-- @since 2.1.0.0
|
||||
dejafuWay :: (MonadDejaFu n, MonadIO n, Show b)
|
||||
=> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
@ -522,8 +520,8 @@ dejafuWay way = dejafuWithSettings . fromWayAndMemType way
|
||||
-- "world" S0----S2--S1-S0--
|
||||
-- False
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
dejafuWithSettings :: (MonadConc n, MonadIO n, Show b)
|
||||
-- @since 2.1.0.0
|
||||
dejafuWithSettings :: (MonadDejaFu n, MonadIO n, Show b)
|
||||
=> Settings n a
|
||||
-- ^ The SCT settings.
|
||||
-> String
|
||||
@ -547,8 +545,8 @@ dejafuWithSettings settings name test =
|
||||
-- [pass] B
|
||||
-- False
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
dejafus :: (MonadConc n, MonadIO n, Show b)
|
||||
-- @since 2.1.0.0
|
||||
dejafus :: (MonadDejaFu n, MonadIO n, Show b)
|
||||
=> [(String, ProPredicate a b)]
|
||||
-- ^ The list of predicates (with names) to check.
|
||||
-> Program pty n a
|
||||
@ -569,8 +567,8 @@ dejafus = dejafusWithSettings defaultSettings
|
||||
-- [pass] B
|
||||
-- False
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
dejafusWay :: (MonadConc n, MonadIO n, Show b)
|
||||
-- @since 2.1.0.0
|
||||
dejafusWay :: (MonadDejaFu n, MonadIO n, Show b)
|
||||
=> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
@ -594,8 +592,8 @@ dejafusWay way = dejafusWithSettings . fromWayAndMemType way
|
||||
-- [pass] B
|
||||
-- False
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
dejafusWithSettings :: (MonadConc n, MonadIO n, Show b)
|
||||
-- @since 2.1.0.0
|
||||
dejafusWithSettings :: (MonadDejaFu n, MonadIO n, Show b)
|
||||
=> Settings n a
|
||||
-- ^ The SCT settings.
|
||||
-> [(String, ProPredicate a b)]
|
||||
@ -670,8 +668,8 @@ instance Foldable Result where
|
||||
-- found, is unspecified and may change between releases. This may
|
||||
-- affect which failing traces are reported, when there is a failure.
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
runTest :: MonadConc n
|
||||
-- @since 2.1.0.0
|
||||
runTest :: MonadDejaFu n
|
||||
=> ProPredicate a b
|
||||
-- ^ The predicate to check
|
||||
-> Program pty n a
|
||||
@ -686,8 +684,8 @@ runTest = runTestWithSettings defaultSettings
|
||||
-- found, is unspecified and may change between releases. This may
|
||||
-- affect which failing traces are reported, when there is a failure.
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
runTestWay :: MonadConc n
|
||||
-- @since 2.1.0.0
|
||||
runTestWay :: MonadDejaFu n
|
||||
=> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
@ -705,8 +703,8 @@ runTestWay way = runTestWithSettings . fromWayAndMemType way
|
||||
-- found, is unspecified and may change between releases. This may
|
||||
-- affect which failing traces are reported, when there is a failure.
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
runTestWithSettings :: MonadConc n
|
||||
-- @since 2.1.0.0
|
||||
runTestWithSettings :: MonadDejaFu n
|
||||
=> Settings n a
|
||||
-- ^ The SCT settings.
|
||||
-> ProPredicate a b
|
||||
|
@ -3,14 +3,15 @@
|
||||
{-# LANGUAGE MultiWayIf #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
|
||||
-- |
|
||||
-- Module : Test.DejaFu.Conc.Internal
|
||||
-- Copyright : (c) 2016--2018 Michael Walker
|
||||
-- Copyright : (c) 2016--2019 Michael Walker
|
||||
-- License : MIT
|
||||
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
|
||||
-- Stability : experimental
|
||||
-- Portability : FlexibleContexts, LambdaCase, MultiWayIf, RankNTypes, RecordWildCards
|
||||
-- Portability : FlexibleContexts, LambdaCase, MultiWayIf, RankNTypes, RecordWildCards, ScopedTypeVariables
|
||||
--
|
||||
-- Concurrent monads with a fixed scheduler: internal types and
|
||||
-- functions. This module is NOT considered to form part of the public
|
||||
@ -21,7 +22,6 @@ import Control.Exception (Exception,
|
||||
MaskingState(..),
|
||||
toException)
|
||||
import qualified Control.Monad.Catch as E
|
||||
import qualified Control.Monad.Conc.Class as C
|
||||
import Data.Foldable (foldrM)
|
||||
import Data.Functor (void)
|
||||
import Data.List (nub, partition, sortOn)
|
||||
@ -50,7 +50,7 @@ type SeqTrace
|
||||
-- | The result of running a concurrent program.
|
||||
data CResult n g a = CResult
|
||||
{ finalContext :: Context n g
|
||||
, finalRef :: C.IORef n (Maybe (Either Condition a))
|
||||
, finalRef :: Ref n (Maybe (Either Condition a))
|
||||
, finalRestore :: Threads n -> n ()
|
||||
-- ^ Meaningless if this result doesn't come from a snapshotting
|
||||
-- execution.
|
||||
@ -61,7 +61,7 @@ data CResult n g a = CResult
|
||||
-- | 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)
|
||||
runConcurrency :: (MonadDejaFu n, HasCallStack)
|
||||
=> [Invariant n ()]
|
||||
-> Bool
|
||||
-> Scheduler g
|
||||
@ -83,13 +83,15 @@ runConcurrency invariants forSnapshot sched memtype g idsrc caps 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
|
||||
threads <- case forkBoundThread of
|
||||
Just fbt -> makeBound fbt initialThread threads0
|
||||
Nothing -> pure threads0
|
||||
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)
|
||||
runConcurrencyWithSnapshot :: (MonadDejaFu n, HasCallStack)
|
||||
=> Scheduler g
|
||||
-> MemType
|
||||
-> Context n g
|
||||
@ -100,16 +102,19 @@ 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 }
|
||||
threads <- case forkBoundThread of
|
||||
Just fbt -> do
|
||||
let boundThreads = M.filter (isJust . _bound) threads1
|
||||
threads' <- makeBound fbt initialThread threads1
|
||||
foldrM (makeBound fbt) threads' (M.keys boundThreads)
|
||||
Nothing -> pure threads1
|
||||
restore threads
|
||||
res <- runThreads False sched memtype ref ctx { cThreads = threads }
|
||||
killAllThreads (finalContext res)
|
||||
pure res
|
||||
|
||||
-- | Kill the remaining threads
|
||||
killAllThreads :: (C.MonadConc n, HasCallStack) => Context n g -> n ()
|
||||
killAllThreads :: (MonadDejaFu n, HasCallStack) => Context n g -> n ()
|
||||
killAllThreads ctx =
|
||||
let finalThreads = cThreads ctx
|
||||
in mapM_ (`kill` finalThreads) (M.keys finalThreads)
|
||||
@ -130,17 +135,17 @@ data Context n g = Context
|
||||
}
|
||||
|
||||
-- | Run a collection of threads, until there are no threads left.
|
||||
runThreads :: (C.MonadConc n, HasCallStack)
|
||||
runThreads :: (MonadDejaFu n, HasCallStack)
|
||||
=> Bool
|
||||
-> Scheduler g
|
||||
-> MemType
|
||||
-> C.IORef n (Maybe (Either Condition a))
|
||||
-> Ref n (Maybe (Either Condition a))
|
||||
-> Context n g
|
||||
-> n (CResult n g a)
|
||||
runThreads forSnapshot sched memtype ref = schedule (const $ pure ()) Seq.empty Nothing where
|
||||
-- signal failure & terminate
|
||||
die reason finalR finalT finalD finalC = do
|
||||
C.writeIORef ref (Just $ Left reason)
|
||||
writeRef ref (Just $ Left reason)
|
||||
stop finalR finalT finalD finalC
|
||||
|
||||
-- just terminate; 'ref' must have been written to before calling
|
||||
@ -256,7 +261,7 @@ data What n g
|
||||
--
|
||||
-- Note: the returned snapshot action will definitely not do the right
|
||||
-- thing with relaxed memory.
|
||||
stepThread :: (C.MonadConc n, HasCallStack)
|
||||
stepThread :: forall n g. (MonadDejaFu n, HasCallStack)
|
||||
=> Bool
|
||||
-- ^ Should we record a snapshot?
|
||||
-> Bool
|
||||
@ -282,12 +287,23 @@ stepThread _ _ _ _ tid (AFork n a b) = \ctx@Context{..} -> pure $
|
||||
)
|
||||
|
||||
-- start a new bound thread, assigning it the next 'ThreadId'
|
||||
stepThread _ _ _ _ tid (AForkOS n a b) = \ctx@Context{..} -> do
|
||||
let (idSource', newtid) = nextTId n cIdSource
|
||||
let threads' = launch tid newtid a cThreads
|
||||
threads'' <- makeBound newtid threads'
|
||||
pure ( Succeeded ctx { cThreads = goto (b newtid) tid threads'', cIdSource = idSource' }
|
||||
, ForkOS newtid
|
||||
stepThread _ _ _ _ tid (AForkOS n a b) = \ctx@Context{..} -> case forkBoundThread of
|
||||
Just fbt -> do
|
||||
let (idSource', newtid) = nextTId n cIdSource
|
||||
let threads' = launch tid newtid a cThreads
|
||||
threads'' <- makeBound fbt newtid threads'
|
||||
pure ( Succeeded ctx { cThreads = goto (b newtid) tid threads'', cIdSource = idSource' }
|
||||
, ForkOS newtid
|
||||
, const (pure ())
|
||||
)
|
||||
Nothing ->
|
||||
stepThrow Throw tid (MonadFailException "dejafu is running with bound threads disabled - do not use forkOS") ctx
|
||||
|
||||
-- check if we support bound threads
|
||||
stepThread _ _ _ _ tid (ASupportsBoundThreads c) = \ctx@Context{..} -> do
|
||||
let sbt = isJust (forkBoundThread :: Maybe (n (BoundThread n ())))
|
||||
pure ( Succeeded ctx { cThreads = goto (c sbt) tid cThreads }
|
||||
, SupportsBoundThreads sbt
|
||||
, const (pure ())
|
||||
)
|
||||
|
||||
@ -337,11 +353,11 @@ stepThread _ _ _ _ tid (ADelay n c) = \ctx@Context{..} ->
|
||||
-- create a new @MVar@, using the next 'MVarId'.
|
||||
stepThread _ _ _ _ tid (ANewMVar n c) = \ctx@Context{..} -> do
|
||||
let (idSource', newmvid) = nextMVId n cIdSource
|
||||
ref <- C.newIORef Nothing
|
||||
ref <- newRef Nothing
|
||||
let mvar = ModelMVar newmvid ref
|
||||
pure ( Succeeded ctx { cThreads = goto (c mvar) tid cThreads, cIdSource = idSource' }
|
||||
, NewMVar newmvid
|
||||
, const (C.writeIORef ref Nothing)
|
||||
, const (writeRef ref Nothing)
|
||||
)
|
||||
|
||||
-- put a value into a @MVar@, blocking the thread until it's empty.
|
||||
@ -398,11 +414,11 @@ stepThread _ _ _ _ tid (ATryTakeMVar mvar@ModelMVar{..} c) = synchronised $ \ctx
|
||||
stepThread _ _ _ _ tid (ANewIORef n a c) = \ctx@Context{..} -> do
|
||||
let (idSource', newiorid) = nextIORId n cIdSource
|
||||
let val = (M.empty, 0, a)
|
||||
ioref <- C.newIORef val
|
||||
ioref <- newRef val
|
||||
let ref = ModelIORef newiorid ioref
|
||||
pure ( Succeeded ctx { cThreads = goto (c ref) tid cThreads, cIdSource = idSource' }
|
||||
, NewIORef newiorid
|
||||
, const (C.writeIORef ioref val)
|
||||
, const (writeRef ioref val)
|
||||
)
|
||||
|
||||
-- read from a @IORef@.
|
||||
@ -609,7 +625,7 @@ stepThread _ _ _ _ tid (ANewInvariant inv c) = \ctx@Context{..} ->
|
||||
|
||||
-- | Handle an exception being thrown from an @AAtom@, @AThrow@, or
|
||||
-- @AThrowTo@.
|
||||
stepThrow :: (C.MonadConc n, Exception e)
|
||||
stepThrow :: (MonadDejaFu n, Exception e)
|
||||
=> (Bool -> ThreadAction)
|
||||
-- ^ Action to include in the trace.
|
||||
-> ThreadId
|
||||
@ -641,7 +657,7 @@ stepThrow act tid e ctx@Context{..} = case propagate some tid cThreads of
|
||||
some = toException e
|
||||
|
||||
-- | Helper for actions impose a write barrier.
|
||||
synchronised :: C.MonadConc n
|
||||
synchronised :: MonadDejaFu n
|
||||
=> (Context n g -> n x)
|
||||
-- ^ Action to run after the write barrier.
|
||||
-> Context n g
|
||||
@ -674,7 +690,7 @@ unblockInvariants act ic = InvariantContext active blocked where
|
||||
|
||||
-- | Check all active invariants, returning an arbitrary failure if
|
||||
-- multiple ones fail.
|
||||
checkInvariants :: C.MonadConc n
|
||||
checkInvariants :: MonadDejaFu n
|
||||
=> InvariantContext n
|
||||
-> n (Either E.SomeException (InvariantContext n))
|
||||
checkInvariants ic = go (icActive ic) >>= \case
|
||||
@ -687,7 +703,7 @@ checkInvariants ic = go (icActive ic) >>= \case
|
||||
go [] = pure (Right [])
|
||||
|
||||
-- | Check an invariant.
|
||||
checkInvariant :: C.MonadConc n
|
||||
checkInvariant :: MonadDejaFu n
|
||||
=> Invariant n a
|
||||
-> n (Either E.SomeException ([IORefId], [MVarId], [TVarId]))
|
||||
checkInvariant inv = doInvariant inv >>= \case
|
||||
@ -695,13 +711,13 @@ checkInvariant inv = doInvariant inv >>= \case
|
||||
(Left exc, _, _, _) -> pure (Left exc)
|
||||
|
||||
-- | Run an invariant (more primitive)
|
||||
doInvariant :: C.MonadConc n
|
||||
doInvariant :: MonadDejaFu 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
|
||||
val <- readRef ref
|
||||
pure (efromJust val, nub iorefs, nub mvars, nub tvars)
|
||||
where
|
||||
go ref act iorefs mvars tvars = do
|
||||
@ -715,21 +731,21 @@ doInvariant inv = do
|
||||
Right Nothing ->
|
||||
pure (newIORefs, newMVars, newTVars)
|
||||
Left exc -> do
|
||||
C.writeIORef ref (Just (Left exc))
|
||||
writeRef ref (Just (Left exc))
|
||||
pure (newIORefs, newMVars, newTVars)
|
||||
|
||||
-- | Run an invariant for one step
|
||||
stepInvariant :: C.MonadConc n
|
||||
stepInvariant :: MonadDejaFu 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
|
||||
a <- readRef mvarRef
|
||||
pure (Right (Just (k a)), [], [mvarId], [])
|
||||
stepInvariant (IInspectTVar ModelTVar{..} k) = do
|
||||
a <- C.readIORef tvarRef
|
||||
a <- readRef tvarRef
|
||||
pure (Right (Just (k a)), [], [], [tvarId])
|
||||
stepInvariant (ICatch h nx k) = doInvariant nx >>= \case
|
||||
(Right a, iorefs, mvars, tvars) ->
|
||||
|
@ -17,7 +17,6 @@ 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)
|
||||
|
||||
@ -106,7 +105,7 @@ instance (pty ~ Basic) => Fail.MonadFail (Program pty n) where
|
||||
-- @Maybe@ value.
|
||||
data ModelMVar n a = ModelMVar
|
||||
{ mvarId :: MVarId
|
||||
, mvarRef :: C.IORef n (Maybe a)
|
||||
, mvarRef :: Ref n (Maybe a)
|
||||
}
|
||||
|
||||
-- | A @IORef@ is modelled as a unique ID and a reference holding
|
||||
@ -114,7 +113,7 @@ data ModelMVar n a = ModelMVar
|
||||
-- committed value.
|
||||
data ModelIORef n a = ModelIORef
|
||||
{ iorefId :: IORefId
|
||||
, iorefRef :: C.IORef n (Map ThreadId a, Integer, a)
|
||||
, iorefRef :: Ref n (Map ThreadId a, Integer, a)
|
||||
}
|
||||
|
||||
-- | A @Ticket@ is modelled as the ID of the @ModelIORef@ it came from,
|
||||
@ -136,6 +135,8 @@ data ModelTicket a = ModelTicket
|
||||
data Action n =
|
||||
AFork String ((forall b. ModelConc n b -> ModelConc n b) -> Action n) (ThreadId -> Action n)
|
||||
| AForkOS String ((forall b. ModelConc n b -> ModelConc n b) -> Action n) (ThreadId -> Action n)
|
||||
|
||||
| ASupportsBoundThreads (Bool -> Action n)
|
||||
| AIsBound (Bool -> Action n)
|
||||
| AMyTId (ThreadId -> Action n)
|
||||
|
||||
@ -182,6 +183,7 @@ data Action n =
|
||||
lookahead :: Action n -> Lookahead
|
||||
lookahead (AFork _ _ _) = WillFork
|
||||
lookahead (AForkOS _ _ _) = WillForkOS
|
||||
lookahead (ASupportsBoundThreads _) = WillSupportsBoundThreads
|
||||
lookahead (AIsBound _) = WillIsCurrentThreadBound
|
||||
lookahead (AMyTId _) = WillMyThreadId
|
||||
lookahead (AGetNumCapabilities _) = WillGetNumCapabilities
|
||||
|
@ -6,7 +6,7 @@
|
||||
|
||||
-- |
|
||||
-- Module : Test.DejaFu.Conc.Internal.Memory
|
||||
-- Copyright : (c) 2016--2018 Michael Walker
|
||||
-- Copyright : (c) 2016--2019 Michael Walker
|
||||
-- License : MIT
|
||||
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
|
||||
-- Stability : experimental
|
||||
@ -25,7 +25,6 @@
|
||||
-- Memory Models/, N. Zhang, M. Kusano, and C. Wang (2015).
|
||||
module Test.DejaFu.Conc.Internal.Memory where
|
||||
|
||||
import qualified Control.Monad.Conc.Class as C
|
||||
import Data.Map.Strict (Map)
|
||||
import qualified Data.Map.Strict as M
|
||||
import Data.Maybe (maybeToList)
|
||||
@ -61,20 +60,20 @@ emptyBuffer :: WriteBuffer n
|
||||
emptyBuffer = WriteBuffer M.empty
|
||||
|
||||
-- | Add a new write to the end of a buffer.
|
||||
bufferWrite :: C.MonadConc n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> ModelIORef n a -> a -> n (WriteBuffer n)
|
||||
bufferWrite :: MonadDejaFu n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> ModelIORef n a -> a -> n (WriteBuffer n)
|
||||
bufferWrite (WriteBuffer wb) k@(tid, _) ref@ModelIORef{..} new = do
|
||||
-- Construct the new write buffer
|
||||
let write = singleton $ BufferedWrite tid ref new
|
||||
let buffer' = M.insertWith (flip (><)) k write wb
|
||||
|
||||
-- Write the thread-local value to the @IORef@'s update map.
|
||||
(locals, count, def) <- C.readIORef iorefRef
|
||||
C.writeIORef iorefRef (M.insert tid new locals, count, def)
|
||||
(locals, count, def) <- readRef iorefRef
|
||||
writeRef iorefRef (M.insert tid new locals, count, def)
|
||||
|
||||
pure (WriteBuffer buffer')
|
||||
|
||||
-- | Commit the write at the head of a buffer.
|
||||
commitWrite :: C.MonadConc n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> n (WriteBuffer n)
|
||||
commitWrite :: MonadDejaFu n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> n (WriteBuffer n)
|
||||
commitWrite w@(WriteBuffer wb) k = case maybe EmptyL viewl $ M.lookup k wb of
|
||||
BufferedWrite _ ref a :< rest -> do
|
||||
_ <- writeImmediate ref a
|
||||
@ -83,21 +82,21 @@ commitWrite w@(WriteBuffer wb) k = case maybe EmptyL viewl $ M.lookup k wb of
|
||||
|
||||
-- | Read from a @IORef@, returning a newer thread-local non-committed
|
||||
-- write if there is one.
|
||||
readIORef :: C.MonadConc n => ModelIORef n a -> ThreadId -> n a
|
||||
readIORef :: MonadDejaFu n => ModelIORef n a -> ThreadId -> n a
|
||||
readIORef ref tid = do
|
||||
(val, _) <- readIORefPrim ref tid
|
||||
pure val
|
||||
|
||||
-- | Read from a @IORef@, returning a @Ticket@ representing the current
|
||||
-- view of the thread.
|
||||
readForTicket :: C.MonadConc n => ModelIORef n a -> ThreadId -> n (ModelTicket a)
|
||||
readForTicket :: MonadDejaFu n => ModelIORef n a -> ThreadId -> n (ModelTicket a)
|
||||
readForTicket ref@ModelIORef{..} tid = do
|
||||
(val, count) <- readIORefPrim ref tid
|
||||
pure (ModelTicket iorefId count val)
|
||||
|
||||
-- | Perform a compare-and-swap on a @IORef@ if the ticket is still
|
||||
-- valid. This is strict in the \"new\" value argument.
|
||||
casIORef :: C.MonadConc n => ModelIORef n a -> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ())
|
||||
casIORef :: MonadDejaFu n => ModelIORef n a -> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ())
|
||||
casIORef ref tid (ModelTicket _ cc _) !new = do
|
||||
tick'@(ModelTicket _ cc' _) <- readForTicket ref tid
|
||||
|
||||
@ -109,28 +108,28 @@ casIORef ref tid (ModelTicket _ cc _) !new = do
|
||||
else pure (False, tick', pure ())
|
||||
|
||||
-- | Read the local state of a @IORef@.
|
||||
readIORefPrim :: C.MonadConc n => ModelIORef n a -> ThreadId -> n (a, Integer)
|
||||
readIORefPrim :: MonadDejaFu n => ModelIORef n a -> ThreadId -> n (a, Integer)
|
||||
readIORefPrim ModelIORef{..} tid = do
|
||||
(vals, count, def) <- C.readIORef iorefRef
|
||||
(vals, count, def) <- readRef 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 :: MonadDejaFu n => ModelIORef n a -> n a
|
||||
readIORefGlobal ModelIORef{..} = do
|
||||
(_, _, def) <- C.readIORef iorefRef
|
||||
(_, _, def) <- readRef 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 ())
|
||||
writeImmediate :: MonadDejaFu n => ModelIORef n a -> a -> n (n ())
|
||||
writeImmediate ModelIORef{..} a = do
|
||||
(_, count, _) <- C.readIORef iorefRef
|
||||
let effect = C.writeIORef iorefRef (M.empty, count + 1, a)
|
||||
(_, count, _) <- readRef iorefRef
|
||||
let effect = writeRef iorefRef (M.empty, count + 1, a)
|
||||
effect
|
||||
pure effect
|
||||
|
||||
-- | Flush all writes in the buffer.
|
||||
writeBarrier :: C.MonadConc n => WriteBuffer n -> n ()
|
||||
writeBarrier :: MonadDejaFu n => WriteBuffer n -> n ()
|
||||
writeBarrier (WriteBuffer wb) = mapM_ flush $ M.elems wb where
|
||||
flush = mapM_ $ \(BufferedWrite _ ref a) -> writeImmediate ref a
|
||||
|
||||
@ -162,7 +161,7 @@ data Blocking = Blocking | NonBlocking
|
||||
data Emptying = Emptying | NonEmptying
|
||||
|
||||
-- | Put into a @MVar@, blocking if full.
|
||||
putIntoMVar :: C.MonadConc n
|
||||
putIntoMVar :: MonadDejaFu n
|
||||
=> ModelMVar n a
|
||||
-> a
|
||||
-> Action n
|
||||
@ -172,7 +171,7 @@ putIntoMVar :: C.MonadConc n
|
||||
putIntoMVar cvar a c = mutMVar Blocking cvar a (const c)
|
||||
|
||||
-- | Try to put into a @MVar@, not blocking if full.
|
||||
tryPutIntoMVar :: C.MonadConc n
|
||||
tryPutIntoMVar :: MonadDejaFu n
|
||||
=> ModelMVar n a
|
||||
-> a
|
||||
-> (Bool -> Action n)
|
||||
@ -182,7 +181,7 @@ tryPutIntoMVar :: C.MonadConc n
|
||||
tryPutIntoMVar = mutMVar NonBlocking
|
||||
|
||||
-- | Read from a @MVar@, blocking if empty.
|
||||
readFromMVar :: (C.MonadConc n, HasCallStack)
|
||||
readFromMVar :: (MonadDejaFu n, HasCallStack)
|
||||
=> ModelMVar n a
|
||||
-> (a -> Action n)
|
||||
-> ThreadId
|
||||
@ -191,7 +190,7 @@ readFromMVar :: (C.MonadConc n, HasCallStack)
|
||||
readFromMVar cvar c = seeMVar NonEmptying Blocking cvar (c . efromJust)
|
||||
|
||||
-- | Try to read from a @MVar@, not blocking if empty.
|
||||
tryReadFromMVar :: C.MonadConc n
|
||||
tryReadFromMVar :: MonadDejaFu n
|
||||
=> ModelMVar n a
|
||||
-> (Maybe a -> Action n)
|
||||
-> ThreadId
|
||||
@ -200,7 +199,7 @@ tryReadFromMVar :: C.MonadConc n
|
||||
tryReadFromMVar = seeMVar NonEmptying NonBlocking
|
||||
|
||||
-- | Take from a @MVar@, blocking if empty.
|
||||
takeFromMVar :: (C.MonadConc n, HasCallStack)
|
||||
takeFromMVar :: (MonadDejaFu n, HasCallStack)
|
||||
=> ModelMVar n a
|
||||
-> (a -> Action n)
|
||||
-> ThreadId
|
||||
@ -209,7 +208,7 @@ takeFromMVar :: (C.MonadConc n, HasCallStack)
|
||||
takeFromMVar cvar c = seeMVar Emptying Blocking cvar (c . efromJust)
|
||||
|
||||
-- | Try to take from a @MVar@, not blocking if empty.
|
||||
tryTakeFromMVar :: C.MonadConc n
|
||||
tryTakeFromMVar :: MonadDejaFu n
|
||||
=> ModelMVar n a
|
||||
-> (Maybe a -> Action n)
|
||||
-> ThreadId
|
||||
@ -218,7 +217,7 @@ tryTakeFromMVar :: C.MonadConc n
|
||||
tryTakeFromMVar = seeMVar Emptying NonBlocking
|
||||
|
||||
-- | Mutate a @MVar@, in either a blocking or nonblocking way.
|
||||
mutMVar :: C.MonadConc n
|
||||
mutMVar :: MonadDejaFu n
|
||||
=> Blocking
|
||||
-> ModelMVar n a
|
||||
-> a
|
||||
@ -226,7 +225,7 @@ mutMVar :: C.MonadConc n
|
||||
-> ThreadId
|
||||
-> Threads n
|
||||
-> n (Bool, Threads n, [ThreadId], n ())
|
||||
mutMVar blocking ModelMVar{..} a c threadid threads = C.readIORef mvarRef >>= \case
|
||||
mutMVar blocking ModelMVar{..} a c threadid threads = readRef mvarRef >>= \case
|
||||
Just _ -> case blocking of
|
||||
Blocking ->
|
||||
let threads' = block (OnMVarEmpty mvarId) threadid threads
|
||||
@ -234,14 +233,14 @@ mutMVar blocking ModelMVar{..} a c threadid threads = C.readIORef mvarRef >>= \c
|
||||
NonBlocking ->
|
||||
pure (False, goto (c False) threadid threads, [], pure ())
|
||||
Nothing -> do
|
||||
let effect = C.writeIORef mvarRef $ Just a
|
||||
let effect = writeRef mvarRef $ Just a
|
||||
let (threads', woken) = wake (OnMVarFull mvarId) threads
|
||||
effect
|
||||
pure (True, goto (c True) threadid threads', woken, effect)
|
||||
|
||||
-- | Read a @MVar@, in either a blocking or nonblocking
|
||||
-- way.
|
||||
seeMVar :: C.MonadConc n
|
||||
seeMVar :: MonadDejaFu n
|
||||
=> Emptying
|
||||
-> Blocking
|
||||
-> ModelMVar n a
|
||||
@ -249,10 +248,10 @@ seeMVar :: C.MonadConc n
|
||||
-> ThreadId
|
||||
-> Threads n
|
||||
-> n (Bool, Threads n, [ThreadId], n ())
|
||||
seeMVar emptying blocking ModelMVar{..} c threadid threads = C.readIORef mvarRef >>= \case
|
||||
seeMVar emptying blocking ModelMVar{..} c threadid threads = readRef mvarRef >>= \case
|
||||
val@(Just _) -> do
|
||||
let effect = case emptying of
|
||||
Emptying -> C.writeIORef mvarRef Nothing
|
||||
Emptying -> writeRef mvarRef Nothing
|
||||
NonEmptying -> pure ()
|
||||
let (threads', woken) = wake (OnMVarEmpty mvarId) threads
|
||||
effect
|
||||
|
@ -92,11 +92,9 @@ instance (pty ~ Basic, Monad n) => C.MonadConc (Program pty n) where
|
||||
|
||||
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)"
|
||||
forkOSWithUnmaskN n ma = ModelConc (AForkOS n (\umask -> runModelConc (ma umask) (\_ -> AStop (pure ()))))
|
||||
|
||||
supportsBoundThreads = ModelConc ASupportsBoundThreads
|
||||
isCurrentThreadBound = ModelConc AIsBound
|
||||
|
||||
-- This implementation lies and returns 2 until a value is set. This
|
||||
@ -172,8 +170,8 @@ instance (pty ~ Basic, Monad n) => C.MonadConc (Program pty n) where
|
||||
-- nonexistent thread. In either of those cases, the computation will
|
||||
-- be halted.
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
runConcurrent :: C.MonadConc n
|
||||
-- @since 2.1.0.0
|
||||
runConcurrent :: MonadDejaFu n
|
||||
=> Scheduler s
|
||||
-> MemType
|
||||
-> s
|
||||
@ -181,7 +179,7 @@ runConcurrent :: C.MonadConc n
|
||||
-> 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)
|
||||
out <- efromJust <$> readRef (finalRef res)
|
||||
pure ( out
|
||||
, cSchedState (finalContext res)
|
||||
, F.toList (finalTrace res)
|
||||
@ -252,9 +250,9 @@ runConcurrent sched memtype s ma = recordSnapshot ma >>= \case
|
||||
-- (liftIO . readIORef)
|
||||
-- @
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
-- @since 2.1.0.0
|
||||
recordSnapshot
|
||||
:: C.MonadConc n
|
||||
:: MonadDejaFu n
|
||||
=> Program pty n a
|
||||
-> n (Maybe (Either Condition (Snapshot pty n a), Trace))
|
||||
recordSnapshot ModelConc{..} = pure Nothing
|
||||
@ -267,9 +265,9 @@ recordSnapshot WithSetupAndTeardown{..} =
|
||||
|
||||
-- | Runs a program with snapshotted setup to completion.
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
-- @since 2.1.0.0
|
||||
runSnapshot
|
||||
:: C.MonadConc n
|
||||
:: MonadDejaFu n
|
||||
=> Scheduler s
|
||||
-> MemType
|
||||
-> s
|
||||
@ -278,7 +276,7 @@ runSnapshot
|
||||
runSnapshot sched memtype s (WS SimpleSnapshot{..}) = do
|
||||
let context = fromSnapContext s snapContext
|
||||
CResult{..} <- runConcurrencyWithSnapshot sched memtype context snapRestore snapNext
|
||||
out <- efromJust <$> C.readIORef finalRef
|
||||
out <- efromJust <$> readRef finalRef
|
||||
pure ( out
|
||||
, cSchedState finalContext
|
||||
, F.toList finalTrace
|
||||
@ -287,9 +285,9 @@ 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)
|
||||
out1 <- efromJust <$> readRef (finalRef intermediateResult)
|
||||
teardownResult <- simpleRunConcurrency False idsrc (teardown out1)
|
||||
out2 <- efromJust <$> C.readIORef (finalRef teardownResult)
|
||||
out2 <- efromJust <$> readRef (finalRef teardownResult)
|
||||
pure ( out2
|
||||
, cSchedState (finalContext intermediateResult)
|
||||
, F.toList (finalTrace intermediateResult)
|
||||
@ -328,7 +326,7 @@ threadsFromSnapshot snap = (initialThread : runnable, blocked) where
|
||||
-- | 'recordSnapshot' implemented generically.
|
||||
--
|
||||
-- Throws an error if the snapshot could not be produced.
|
||||
defaultRecordSnapshot :: C.MonadConc n
|
||||
defaultRecordSnapshot :: MonadDejaFu n
|
||||
=> (SimpleSnapshot n a -> x -> snap)
|
||||
-> ModelConc n x
|
||||
-> (x -> ModelConc n a)
|
||||
@ -336,7 +334,7 @@ defaultRecordSnapshot :: C.MonadConc n
|
||||
defaultRecordSnapshot mkSnapshot setup program = do
|
||||
CResult{..} <- simpleRunConcurrency True initialIdSource setup
|
||||
let trc = F.toList finalTrace
|
||||
out <- C.readIORef finalRef
|
||||
out <- readRef finalRef
|
||||
pure . Just $ case out of
|
||||
Just (Right a) ->
|
||||
let snap = mkSnapshot (SimpleSnapshot finalContext finalRestore (program a)) a
|
||||
@ -351,7 +349,7 @@ defaultRecordSnapshot mkSnapshot setup program = do
|
||||
|
||||
-- | Run a concurrent program with a deterministic scheduler in
|
||||
-- snapshotting or non-snapshotting mode.
|
||||
simpleRunConcurrency ::(C.MonadConc n, HasCallStack)
|
||||
simpleRunConcurrency ::(MonadDejaFu n, HasCallStack)
|
||||
=> Bool
|
||||
-> IdSource
|
||||
-> ModelConc n a
|
||||
|
@ -7,7 +7,7 @@
|
||||
|
||||
-- |
|
||||
-- Module : Test.DejaFu.Conc.Internal.STM
|
||||
-- Copyright : (c) 2017--2018 Michael Walker
|
||||
-- Copyright : (c) 2017--2019 Michael Walker
|
||||
-- License : MIT
|
||||
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
|
||||
-- Stability : experimental
|
||||
@ -18,15 +18,14 @@
|
||||
-- of this library.
|
||||
module Test.DejaFu.Conc.Internal.STM where
|
||||
|
||||
import Control.Applicative (Alternative(..))
|
||||
import Control.Exception (Exception, SomeException,
|
||||
fromException, toException)
|
||||
import Control.Monad (MonadPlus(..))
|
||||
import Control.Monad.Catch (MonadCatch(..), MonadThrow(..))
|
||||
import qualified Control.Monad.Conc.Class as C
|
||||
import qualified Control.Monad.Fail as Fail
|
||||
import qualified Control.Monad.STM.Class as S
|
||||
import Data.List (nub)
|
||||
import Control.Applicative (Alternative(..))
|
||||
import Control.Exception (Exception, SomeException,
|
||||
fromException, toException)
|
||||
import Control.Monad (MonadPlus(..))
|
||||
import Control.Monad.Catch (MonadCatch(..), MonadThrow(..))
|
||||
import qualified Control.Monad.Fail as Fail
|
||||
import qualified Control.Monad.STM.Class as S
|
||||
import Data.List (nub)
|
||||
|
||||
import Test.DejaFu.Internal
|
||||
import Test.DejaFu.Types
|
||||
@ -100,7 +99,7 @@ data STMAction n
|
||||
-- value.
|
||||
data ModelTVar n a = ModelTVar
|
||||
{ tvarId :: TVarId
|
||||
, tvarRef :: C.IORef n a
|
||||
, tvarRef :: Ref n a
|
||||
}
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
@ -126,7 +125,7 @@ data Result a =
|
||||
|
||||
-- | Run a transaction, returning the result and new initial 'TVarId'.
|
||||
-- If the transaction failed, any effects are undone.
|
||||
runTransaction :: C.MonadConc n
|
||||
runTransaction :: MonadDejaFu n
|
||||
=> ModelSTM n a
|
||||
-> IdSource
|
||||
-> n (Result a, IdSource, [TAction])
|
||||
@ -138,14 +137,14 @@ runTransaction ma tvid = do
|
||||
--
|
||||
-- If the transaction fails, its effects will automatically be undone,
|
||||
-- so the undo action returned will be @pure ()@.
|
||||
doTransaction :: C.MonadConc n
|
||||
doTransaction :: MonadDejaFu n
|
||||
=> ModelSTM n a
|
||||
-> IdSource
|
||||
-> n (Result a, n (), IdSource, [TAction])
|
||||
doTransaction ma idsource = do
|
||||
(c, ref) <- runRefCont SStop (Just . Right) (runModelSTM ma)
|
||||
(idsource', undo, readen, written, trace) <- go ref c (pure ()) idsource [] [] []
|
||||
res <- C.readIORef ref
|
||||
res <- readRef ref
|
||||
|
||||
case res of
|
||||
Just (Right val) -> pure (Success (nub readen) (nub written) val, undo, idsource', reverse trace)
|
||||
@ -166,15 +165,15 @@ doTransaction ma idsource = do
|
||||
case tact of
|
||||
TStop -> pure (newIDSource, newUndo, newReaden, newWritten, TStop:newSofar)
|
||||
TRetry -> do
|
||||
C.writeIORef ref Nothing
|
||||
writeRef ref Nothing
|
||||
pure (newIDSource, newUndo, newReaden, newWritten, TRetry:newSofar)
|
||||
TThrow -> do
|
||||
C.writeIORef ref (Just . Left $ case act of SThrow e -> toException e; _ -> undefined)
|
||||
writeRef ref (Just . Left $ case act of SThrow e -> toException e; _ -> undefined)
|
||||
pure (newIDSource, newUndo, newReaden, newWritten, TThrow:newSofar)
|
||||
_ -> go ref newAct newUndo newIDSource newReaden newWritten newSofar
|
||||
|
||||
-- | Run a transaction for one step.
|
||||
stepTrans :: C.MonadConc n
|
||||
stepTrans :: MonadDejaFu n
|
||||
=> STMAction n
|
||||
-> IdSource
|
||||
-> n (STMAction n, n (), IdSource, [TVarId], [TVarId], TAction)
|
||||
@ -199,17 +198,17 @@ stepTrans act idsource = case act of
|
||||
Nothing -> pure (SThrow exc, nothing, idsource, [], [], TCatch trace Nothing))
|
||||
|
||||
stepRead ModelTVar{..} c = do
|
||||
val <- C.readIORef tvarRef
|
||||
val <- readRef tvarRef
|
||||
pure (c val, nothing, idsource, [tvarId], [], TRead tvarId)
|
||||
|
||||
stepWrite ModelTVar{..} a c = do
|
||||
old <- C.readIORef tvarRef
|
||||
C.writeIORef tvarRef a
|
||||
pure (c, C.writeIORef tvarRef old, idsource, [], [tvarId], TWrite tvarId)
|
||||
old <- readRef tvarRef
|
||||
writeRef tvarRef a
|
||||
pure (c, writeRef tvarRef old, idsource, [], [tvarId], TWrite tvarId)
|
||||
|
||||
stepNew n a c = do
|
||||
let (idsource', tvid) = nextTVId n idsource
|
||||
ref <- C.newIORef a
|
||||
ref <- newRef a
|
||||
let tvar = ModelTVar tvid ref
|
||||
pure (c tvar, nothing, idsource', [], [tvid], TNew tvid)
|
||||
|
||||
|
@ -4,7 +4,7 @@
|
||||
|
||||
-- |
|
||||
-- Module : Test.DejaFu.Conc.Internal.Threading
|
||||
-- Copyright : (c) 2016--2018 Michael Walker
|
||||
-- Copyright : (c) 2016--2019 Michael Walker
|
||||
-- License : MIT
|
||||
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
|
||||
-- Stability : experimental
|
||||
@ -16,8 +16,6 @@ module Test.DejaFu.Conc.Internal.Threading where
|
||||
|
||||
import Control.Exception (Exception, MaskingState(..),
|
||||
SomeException, fromException)
|
||||
import Control.Monad (forever)
|
||||
import qualified Control.Monad.Conc.Class as C
|
||||
import Data.List (intersect)
|
||||
import Data.Map.Strict (Map)
|
||||
import qualified Data.Map.Strict as M
|
||||
@ -44,20 +42,10 @@ data Thread n = Thread
|
||||
-- ^ Stack of exception handlers
|
||||
, _masking :: MaskingState
|
||||
-- ^ The exception masking state.
|
||||
, _bound :: Maybe (BoundThread n)
|
||||
, _bound :: Maybe (BoundThread n (Action n))
|
||||
-- ^ State for the associated bound thread, if it exists.
|
||||
}
|
||||
|
||||
-- | The state of a bound thread.
|
||||
data BoundThread n = BoundThread
|
||||
{ _runboundIO :: C.MVar n (n (Action n))
|
||||
-- ^ Run an @IO@ action in the bound thread by writing to this.
|
||||
, _getboundIO :: C.MVar n (Action n)
|
||||
-- ^ Get the result of the above by reading from this.
|
||||
, _boundTId :: C.ThreadId n
|
||||
-- ^ Thread ID
|
||||
}
|
||||
|
||||
-- | Construct a thread with just one action
|
||||
mkthread :: Action n -> Thread n
|
||||
mkthread c = Thread c Nothing [] Unmasked Nothing
|
||||
@ -167,33 +155,24 @@ wake blockedOn threads = (unblock <$> threads, M.keys $ M.filter isBlocked threa
|
||||
-- ** Bound threads
|
||||
|
||||
-- | Turn a thread into a bound thread.
|
||||
makeBound :: (C.MonadConc n, HasCallStack) => ThreadId -> Threads n -> n (Threads n)
|
||||
makeBound tid threads = do
|
||||
runboundIO <- C.newEmptyMVar
|
||||
getboundIO <- C.newEmptyMVar
|
||||
btid <- C.forkOSN ("bound worker for '" ++ show tid ++ "'") (go runboundIO getboundIO)
|
||||
let bt = BoundThread runboundIO getboundIO btid
|
||||
pure (eadjust (\t -> t { _bound = Just bt }) tid threads)
|
||||
where
|
||||
go runboundIO getboundIO = forever $ do
|
||||
na <- C.takeMVar runboundIO
|
||||
C.putMVar getboundIO =<< na
|
||||
makeBound :: (MonadDejaFu n, HasCallStack)
|
||||
=> n (BoundThread n (Action n)) -> ThreadId -> Threads n -> n (Threads n)
|
||||
makeBound fbt tid threads = do
|
||||
bt <- fbt
|
||||
pure (eadjust (\t -> t { _bound = Just bt }) tid threads)
|
||||
|
||||
-- | Kill a thread and remove it from the thread map.
|
||||
--
|
||||
-- If the thread is bound, the worker thread is cleaned up.
|
||||
kill :: (C.MonadConc n, HasCallStack) => ThreadId -> Threads n -> n (Threads n)
|
||||
kill :: (MonadDejaFu n, HasCallStack) => ThreadId -> Threads n -> n (Threads n)
|
||||
kill tid threads = do
|
||||
let thread = elookup tid threads
|
||||
maybe (pure ()) (C.killThread . _boundTId) (_bound thread)
|
||||
maybe (pure ()) killBoundThread (_bound thread)
|
||||
pure (M.delete tid threads)
|
||||
|
||||
-- | Run an action.
|
||||
--
|
||||
-- If the thread is bound, the action is run in the worker thread.
|
||||
runLiftedAct :: C.MonadConc n => ThreadId -> Threads n -> n (Action n) -> n (Action n)
|
||||
runLiftedAct :: MonadDejaFu n => ThreadId -> Threads n -> n (Action n) -> n (Action n)
|
||||
runLiftedAct tid threads ma = case _bound =<< M.lookup tid threads of
|
||||
Just bt -> do
|
||||
C.putMVar (_runboundIO bt) ma
|
||||
C.takeMVar (_getboundIO bt)
|
||||
Just bt -> runInBoundThread bt ma
|
||||
Nothing -> ma
|
||||
|
@ -17,18 +17,17 @@
|
||||
-- library.
|
||||
module Test.DejaFu.Internal where
|
||||
|
||||
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)
|
||||
import qualified Data.Set as S
|
||||
import GHC.Generics (Generic)
|
||||
import GHC.Stack (HasCallStack, withFrozenCallStack)
|
||||
import System.Random (RandomGen)
|
||||
import Control.DeepSeq (NFData(..))
|
||||
import Control.Exception (MaskingState(..))
|
||||
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)
|
||||
import qualified Data.Set as S
|
||||
import GHC.Generics (Generic)
|
||||
import GHC.Stack (HasCallStack, withFrozenCallStack)
|
||||
import System.Random (RandomGen)
|
||||
|
||||
import Test.DejaFu.Types
|
||||
|
||||
@ -165,6 +164,7 @@ tvarsRead act = S.fromList $ case act of
|
||||
rewind :: ThreadAction -> Lookahead
|
||||
rewind (Fork _) = WillFork
|
||||
rewind (ForkOS _) = WillForkOS
|
||||
rewind (SupportsBoundThreads _) = WillSupportsBoundThreads
|
||||
rewind (IsCurrentThreadBound _) = WillIsCurrentThreadBound
|
||||
rewind MyThreadId = WillMyThreadId
|
||||
rewind (GetNumCapabilities _) = WillGetNumCapabilities
|
||||
@ -449,12 +449,12 @@ fatal msg = withFrozenCallStack $ error ("(dejafu) " ++ msg)
|
||||
-- | Run with a continuation that writes its value into a reference,
|
||||
-- returning the computation and the reference. Using the reference
|
||||
-- is non-blocking, it is up to you to ensure you wait sufficiently.
|
||||
runRefCont :: C.MonadConc n
|
||||
runRefCont :: MonadDejaFu n
|
||||
=> (n () -> x)
|
||||
-> (a -> Maybe b)
|
||||
-> ((a -> x) -> x)
|
||||
-> n (x, C.IORef n (Maybe b))
|
||||
-> n (x, Ref n (Maybe b))
|
||||
runRefCont act f k = do
|
||||
ref <- C.newIORef Nothing
|
||||
let c = k (act . C.writeIORef ref . f)
|
||||
ref <- newRef Nothing
|
||||
let c = k (act . writeRef ref . f)
|
||||
pure (c, ref)
|
||||
|
@ -1,5 +1,3 @@
|
||||
{-# OPTIONS_GHC -Wno-deprecations #-}
|
||||
|
||||
-- |
|
||||
-- Module : Test.DejaFu.SCT
|
||||
-- Copyright : (c) 2015--2019 Michael Walker
|
||||
@ -26,7 +24,6 @@ module Test.DejaFu.SCT
|
||||
|
||||
import Control.Applicative ((<|>))
|
||||
import Control.DeepSeq (NFData(..), force)
|
||||
import Control.Monad.Conc.Class (MonadConc)
|
||||
import Data.List (foldl')
|
||||
import qualified Data.Map.Strict as M
|
||||
import Data.Maybe (fromMaybe)
|
||||
@ -51,8 +48,8 @@ import Test.DejaFu.Utils
|
||||
-- The exact executions tried, and the order in which results are
|
||||
-- found, is unspecified and may change between releases.
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
runSCT :: MonadConc n
|
||||
-- @since 2.1.0.0
|
||||
runSCT :: MonadDejaFu n
|
||||
=> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
@ -64,8 +61,8 @@ runSCT way = runSCTWithSettings . fromWayAndMemType way
|
||||
|
||||
-- | Return the set of results of a concurrent program.
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
resultsSet :: (MonadConc n, Ord a)
|
||||
-- @since 2.1.0.0
|
||||
resultsSet :: (MonadDejaFu n, Ord a)
|
||||
=> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
@ -83,8 +80,8 @@ resultsSet way = resultsSetWithSettings . fromWayAndMemType way
|
||||
-- The exact executions tried, and the order in which results are
|
||||
-- found, is unspecified and may change between releases.
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
runSCT' :: (MonadConc n, NFData a)
|
||||
-- @since 2.1.0.0
|
||||
runSCT' :: (MonadDejaFu n, NFData a)
|
||||
=> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
@ -99,8 +96,8 @@ runSCT' way = runSCTWithSettings' . fromWayAndMemType way
|
||||
-- Demanding the result of this will force it to normal form, which
|
||||
-- may be more efficient in some situations.
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
resultsSet' :: (MonadConc n, Ord a, NFData a)
|
||||
-- @since 2.1.0.0
|
||||
resultsSet' :: (MonadDejaFu n, Ord a, NFData a)
|
||||
=> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
@ -118,8 +115,8 @@ resultsSet' way = resultsSetWithSettings' . fromWayAndMemType way
|
||||
-- The exact executions tried, and the order in which results are
|
||||
-- found, is unspecified and may change between releases.
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
runSCTWithSettings :: MonadConc n
|
||||
-- @since 2.1.0.0
|
||||
runSCTWithSettings :: MonadDejaFu n
|
||||
=> Settings n a
|
||||
-- ^ The SCT settings.
|
||||
-> Program pty n a
|
||||
@ -159,8 +156,8 @@ runSCTWithSettings settings conc = case _way settings of
|
||||
|
||||
-- | A variant of 'resultsSet' which takes a 'Settings' record.
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
resultsSetWithSettings :: (MonadConc n, Ord a)
|
||||
-- @since 2.1.0.0
|
||||
resultsSetWithSettings :: (MonadDejaFu n, Ord a)
|
||||
=> Settings n a
|
||||
-- ^ The SCT settings.
|
||||
-> Program pty n a
|
||||
@ -178,8 +175,8 @@ resultsSetWithSettings settings conc =
|
||||
-- The exact executions tried, and the order in which results are
|
||||
-- found, is unspecified and may change between releases.
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
runSCTWithSettings' :: (MonadConc n, NFData a)
|
||||
-- @since 2.1.0.0
|
||||
runSCTWithSettings' :: (MonadDejaFu n, NFData a)
|
||||
=> Settings n a
|
||||
-- ^ The SCT settings.
|
||||
-> Program pty n a
|
||||
@ -194,8 +191,8 @@ runSCTWithSettings' settings conc = do
|
||||
-- Demanding the result of this will force it to normal form, which
|
||||
-- may be more efficient in some situations.
|
||||
--
|
||||
-- @since 2.0.0.0
|
||||
resultsSetWithSettings' :: (MonadConc n, Ord a, NFData a)
|
||||
-- @since 2.1.0.0
|
||||
resultsSetWithSettings' :: (MonadDejaFu n, Ord a, NFData a)
|
||||
=> Settings n a
|
||||
-- ^ The SCT settings.
|
||||
-> Program pty n a
|
||||
|
@ -5,7 +5,7 @@
|
||||
|
||||
-- |
|
||||
-- Module : Test.DejaFu.SCT.Internal
|
||||
-- Copyright : (c) 2018 Michael Walker
|
||||
-- Copyright : (c) 2018--2019 Michael Walker
|
||||
-- License : MIT
|
||||
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
|
||||
-- Stability : experimental
|
||||
@ -15,7 +15,6 @@
|
||||
-- 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)
|
||||
@ -36,7 +35,7 @@ import Test.DejaFu.Utils
|
||||
-- * Exploration
|
||||
|
||||
-- | General-purpose SCT function.
|
||||
sct :: (MonadConc n, HasCallStack)
|
||||
sct :: (MonadDejaFu n, HasCallStack)
|
||||
=> Settings n a
|
||||
-- ^ The SCT settings ('Way' is ignored)
|
||||
-> ([ThreadId] -> s)
|
||||
@ -79,7 +78,7 @@ sct settings s0 sfun srun conc = recordSnapshot conc >>= \case
|
||||
runSnap snap sched s = runSnapshot sched (_memtype settings) s snap
|
||||
|
||||
-- | Like 'sct' but given a function to run the computation.
|
||||
sct' :: (MonadConc n, HasCallStack)
|
||||
sct' :: (MonadDejaFu n, HasCallStack)
|
||||
=> Settings n a
|
||||
-- ^ The SCT settings ('Way' is ignored)
|
||||
-> ConcurrencyState
|
||||
@ -150,7 +149,7 @@ sct' settings cstate0 s0 sfun srun run nTId nCRId = go Nothing [] s0 where
|
||||
-- Unlike shrinking in randomised property-testing tools like
|
||||
-- QuickCheck or Hedgehog, we only run the test case /once/, at the
|
||||
-- end, rather than after every simplification step.
|
||||
simplifyExecution :: (MonadConc n, HasCallStack)
|
||||
simplifyExecution :: (MonadDejaFu n, HasCallStack)
|
||||
=> Settings n a
|
||||
-- ^ The SCT settings ('Way' is ignored)
|
||||
-> ConcurrencyState
|
||||
@ -190,7 +189,7 @@ simplifyExecution settings cstate0 run nTId nCRId res trace
|
||||
p = either show debugShow
|
||||
|
||||
-- | Replay an execution.
|
||||
replay :: MonadConc n
|
||||
replay :: MonadDejaFu n
|
||||
=> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
|
||||
-- ^ Run the computation
|
||||
-> [(ThreadId, ThreadAction)]
|
||||
|
@ -1,7 +1,10 @@
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
|
||||
-- |
|
||||
-- Module : Test.DejaFu.Types
|
||||
@ -9,24 +12,139 @@
|
||||
-- License : MIT
|
||||
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
|
||||
-- Stability : experimental
|
||||
-- Portability : DeriveGeneric, GeneralizedNewtypeDeriving, LambdaCase, StandaloneDeriving
|
||||
-- Portability : DeriveGeneric, FlexibleInstances, GeneralizedNewtypeDeriving, LambdaCase, RankNTypes, StandaloneDeriving, TypeFamilies
|
||||
--
|
||||
-- Common types and functions used throughout DejaFu.
|
||||
module Test.DejaFu.Types where
|
||||
|
||||
import qualified Control.Concurrent as IO
|
||||
import Control.DeepSeq (NFData(..))
|
||||
import Control.Exception (Exception(..),
|
||||
MaskingState(..),
|
||||
SomeException)
|
||||
import Control.Monad (forever)
|
||||
import Control.Monad.Catch (MonadThrow)
|
||||
import Control.Monad.Catch.Pure (CatchT)
|
||||
import qualified Control.Monad.ST as ST
|
||||
import Control.Monad.Trans.Class (lift)
|
||||
import Data.Function (on)
|
||||
import Data.Functor.Contravariant (Contravariant(..))
|
||||
import Data.Functor.Contravariant.Divisible (Divisible(..))
|
||||
import qualified Data.IORef as IO
|
||||
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)
|
||||
import qualified Data.STRef as ST
|
||||
import GHC.Generics (Generic, V1)
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
-- * The @MonadDejaFu@ typeclass
|
||||
|
||||
-- | The @MonadDejaFu@ class captures the two things needed to run a
|
||||
-- concurrent program which we can't implement in normal Haskell:
|
||||
-- mutable references, and the ability to create a bound thread in
|
||||
-- @IO@.
|
||||
--
|
||||
-- In addition to needing the operations in this class, dejafu also
|
||||
-- needs the ability to throw exceptions, as these are used to
|
||||
-- communicate 'Error's, so there is a 'MonadThrow' constraint.
|
||||
--
|
||||
-- @since 2.1.0.0
|
||||
class MonadThrow m => MonadDejaFu m where
|
||||
-- | The type of mutable references. These references will always
|
||||
-- contain a value, and so don't need to handle emptiness (like
|
||||
-- @MVar@ does).
|
||||
--
|
||||
-- These references are always used from the same Haskell thread, so
|
||||
-- it's safe to implement these using unsynchronised primitives with
|
||||
-- relaxed-memory behaviours (like @IORef@s).
|
||||
type Ref m :: * -> *
|
||||
|
||||
-- | Create a new reference holding a given initial value.
|
||||
newRef :: a -> m (Ref m a)
|
||||
|
||||
-- | Read the current value in the reference.
|
||||
readRef :: Ref m a -> m a
|
||||
|
||||
-- | Replace the value in the reference.
|
||||
writeRef :: Ref m a -> a -> m ()
|
||||
|
||||
-- | A handle to a bound thread. If the monad doesn't support bound
|
||||
-- threads (for example, if it's not based on @IO@), then this
|
||||
-- should be some type which can't be constructed, like 'V1'.
|
||||
type BoundThread m :: * -> *
|
||||
|
||||
-- | Fork a new bound thread, if the monad supports them.
|
||||
forkBoundThread :: Maybe (m (BoundThread m a))
|
||||
|
||||
-- | Run an action in a previously created bound thread.
|
||||
runInBoundThread :: BoundThread m a -> m a -> m a
|
||||
|
||||
-- | Terminate a previously created bound thread.
|
||||
--
|
||||
-- After termination, 'runInBoundThread' and 'killBoundThread' will
|
||||
-- never be called on this @BoundThread m a@ value again.
|
||||
killBoundThread :: BoundThread m a -> m ()
|
||||
|
||||
-- | A bound thread in @IO@.
|
||||
--
|
||||
-- @since 2.1.0.0
|
||||
data IOBoundThread a = IOBoundThread
|
||||
{ iobtRunInBoundThread :: IO a -> IO a
|
||||
-- ^ Pass an action to the bound thread, run it, and return the
|
||||
-- result to this thread.
|
||||
, iobtKillBoundThread :: IO ()
|
||||
-- ^ Terminate the bound thread.
|
||||
}
|
||||
|
||||
-- | @since 2.1.0.0
|
||||
instance MonadDejaFu IO where
|
||||
type Ref IO = IO.IORef
|
||||
|
||||
newRef = IO.newIORef
|
||||
readRef = IO.readIORef
|
||||
writeRef = IO.writeIORef
|
||||
|
||||
type BoundThread IO = IOBoundThread
|
||||
|
||||
forkBoundThread = Just $ do
|
||||
runboundIO <- IO.newEmptyMVar
|
||||
getboundIO <- IO.newEmptyMVar
|
||||
tid <- IO.forkOS (go runboundIO getboundIO)
|
||||
pure IOBoundThread
|
||||
{ iobtRunInBoundThread = run runboundIO getboundIO
|
||||
, iobtKillBoundThread = IO.killThread tid
|
||||
}
|
||||
where
|
||||
go runboundIO getboundIO = forever $ do
|
||||
na <- IO.takeMVar runboundIO
|
||||
IO.putMVar getboundIO =<< na
|
||||
|
||||
run runboundIO getboundIO ma = do
|
||||
IO.putMVar runboundIO ma
|
||||
IO.takeMVar getboundIO
|
||||
|
||||
runInBoundThread = iobtRunInBoundThread
|
||||
killBoundThread = iobtKillBoundThread
|
||||
|
||||
-- | This instance does not support bound threads.
|
||||
--
|
||||
-- @since 2.1.0.0
|
||||
instance MonadDejaFu (CatchT (ST.ST t)) where
|
||||
type Ref (CatchT (ST.ST t)) = ST.STRef t
|
||||
|
||||
newRef = lift . ST.newSTRef
|
||||
readRef = lift . ST.readSTRef
|
||||
writeRef r = lift . ST.writeSTRef r
|
||||
|
||||
-- V1 has no constructors
|
||||
type BoundThread (CatchT (ST.ST t)) = V1
|
||||
|
||||
forkBoundThread = Nothing
|
||||
runInBoundThread = undefined
|
||||
killBoundThread = undefined
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
-- * Identifiers
|
||||
@ -116,6 +234,8 @@ data ThreadAction =
|
||||
-- ^ Start a new thread.
|
||||
| ForkOS ThreadId
|
||||
-- ^ Start a new bound thread.
|
||||
| SupportsBoundThreads Bool
|
||||
-- ^ Check if bound threads are supported.
|
||||
| IsCurrentThreadBound Bool
|
||||
-- ^ Check if the current thread is bound.
|
||||
| MyThreadId
|
||||
@ -206,6 +326,7 @@ data ThreadAction =
|
||||
instance NFData ThreadAction where
|
||||
rnf (Fork t) = rnf t
|
||||
rnf (ForkOS t) = rnf t
|
||||
rnf (SupportsBoundThreads b) = rnf b
|
||||
rnf (IsCurrentThreadBound b) = rnf b
|
||||
rnf MyThreadId = ()
|
||||
rnf (GetNumCapabilities i) = rnf i
|
||||
@ -252,6 +373,8 @@ data Lookahead =
|
||||
-- ^ Will start a new thread.
|
||||
| WillForkOS
|
||||
-- ^ Will start a new bound thread.
|
||||
| WillSupportsBoundThreads
|
||||
-- ^ Will check if bound threads are supported.
|
||||
| WillIsCurrentThreadBound
|
||||
-- ^ Will check if the current thread is bound.
|
||||
| WillMyThreadId
|
||||
@ -331,6 +454,7 @@ data Lookahead =
|
||||
instance NFData Lookahead where
|
||||
rnf WillFork = ()
|
||||
rnf WillForkOS = ()
|
||||
rnf WillSupportsBoundThreads = ()
|
||||
rnf WillIsCurrentThreadBound = ()
|
||||
rnf WillMyThreadId = ()
|
||||
rnf WillGetNumCapabilities = ()
|
||||
|
@ -2,7 +2,7 @@
|
||||
-- documentation, see http://haskell.org/cabal/users-guide/
|
||||
|
||||
name: dejafu
|
||||
version: 2.0.0.1
|
||||
version: 2.1.0.0
|
||||
synopsis: A library for unit-testing concurrent programs.
|
||||
|
||||
description:
|
||||
@ -20,7 +20,7 @@ license: MIT
|
||||
license-file: LICENSE
|
||||
author: Michael Walker
|
||||
maintainer: mike@barrucadu.co.uk
|
||||
copyright: (c) 2015--2018 Michael Walker
|
||||
copyright: (c) 2015--2019 Michael Walker
|
||||
category: Concurrency
|
||||
build-type: Simple
|
||||
extra-source-files: README.markdown CHANGELOG.rst
|
||||
@ -33,7 +33,7 @@ source-repository head
|
||||
source-repository this
|
||||
type: git
|
||||
location: https://github.com/barrucadu/dejafu.git
|
||||
tag: dejafu-2.0.0.1
|
||||
tag: dejafu-2.1.0.0
|
||||
|
||||
library
|
||||
exposed-modules: Test.DejaFu
|
||||
@ -59,7 +59,7 @@ library
|
||||
-- other-modules:
|
||||
-- other-extensions:
|
||||
build-depends: base >=4.9 && <5
|
||||
, concurrency >=1.6 && <1.7
|
||||
, concurrency >=1.7 && <1.8
|
||||
, containers >=0.5 && <0.7
|
||||
, contravariant >=1.2 && <1.6
|
||||
, deepseq >=1.1 && <2
|
||||
|
@ -27,10 +27,10 @@ There are a few different packages under the Déjà Fu umbrella:
|
||||
.. csv-table::
|
||||
:header: "Package", "Version", "Summary"
|
||||
|
||||
":hackage:`concurrency`", "1.6.2.0", "Typeclasses, functions, and data types for concurrency and STM"
|
||||
":hackage:`dejafu`", "2.0.0.1", "Systematic testing for Haskell concurrency"
|
||||
":hackage:`hunit-dejafu`", "2.0.0.0", "Déjà Fu support for the HUnit test framework"
|
||||
":hackage:`tasty-dejafu`", "2.0.0.0", "Déjà Fu support for the tasty test framework"
|
||||
":hackage:`concurrency`", "1.7.0.0", "Typeclasses, functions, and data types for concurrency and STM"
|
||||
":hackage:`dejafu`", "2.1.0.0", "Systematic testing for Haskell concurrency"
|
||||
":hackage:`hunit-dejafu`", "2.0.0.1", "Déjà Fu support for the HUnit test framework"
|
||||
":hackage:`tasty-dejafu`", "2.0.0.1", "Déjà Fu support for the tasty test framework"
|
||||
|
||||
|
||||
Installation
|
||||
|
@ -7,6 +7,18 @@ standard Haskell versioning scheme.
|
||||
.. _PVP: https://pvp.haskell.org/
|
||||
|
||||
|
||||
2.0.0.1 (2019-03-24)
|
||||
--------------------
|
||||
|
||||
* Git: :tag:`hunit-dejafu-2.0.0.1`
|
||||
* Hackage: :hackage:`hunit-dejafu-2.0.0.1`
|
||||
|
||||
Miscellaneous
|
||||
~~~~~~~~~~~~~
|
||||
|
||||
* The upper bound on :hackage:`dejafu` is <2.2
|
||||
|
||||
|
||||
2.0.0.0 (2019-02-12)
|
||||
--------------------
|
||||
|
||||
|
@ -2,7 +2,7 @@
|
||||
-- documentation, see http://haskell.org/cabal/users-guide/
|
||||
|
||||
name: hunit-dejafu
|
||||
version: 2.0.0.0
|
||||
version: 2.0.0.1
|
||||
synopsis: Deja Fu support for the HUnit test framework.
|
||||
|
||||
description:
|
||||
@ -30,7 +30,7 @@ source-repository head
|
||||
source-repository this
|
||||
type: git
|
||||
location: https://github.com/barrucadu/dejafu.git
|
||||
tag: hunit-dejafu-2.0.0.0
|
||||
tag: hunit-dejafu-2.0.0.1
|
||||
|
||||
library
|
||||
exposed-modules: Test.HUnit.DejaFu
|
||||
@ -38,7 +38,7 @@ library
|
||||
-- other-extensions:
|
||||
build-depends: base >=4.9 && <5
|
||||
, exceptions >=0.7 && <0.11
|
||||
, dejafu >=2.0 && <2.1
|
||||
, dejafu >=2.0 && <2.2
|
||||
, HUnit >=1.3.1 && <1.7
|
||||
-- hs-source-dirs:
|
||||
default-language: Haskell2010
|
||||
|
@ -7,6 +7,18 @@ standard Haskell versioning scheme.
|
||||
.. _PVP: https://pvp.haskell.org/
|
||||
|
||||
|
||||
2.0.0.1 (2019-03-24)
|
||||
--------------------
|
||||
|
||||
* Git: :tag:`tasty-dejafu-2.0.0.1`
|
||||
* Hackage: :hackage:`tasty-dejafu-2.0.0.1`
|
||||
|
||||
Miscellaneous
|
||||
~~~~~~~~~~~~~
|
||||
|
||||
* The upper bound on :hackage:`dejafu` is <2.2
|
||||
|
||||
|
||||
2.0.0.0 (2019-02-12)
|
||||
--------------------
|
||||
|
||||
|
@ -2,7 +2,7 @@
|
||||
-- documentation, see http://haskell.org/cabal/users-guide/
|
||||
|
||||
name: tasty-dejafu
|
||||
version: 2.0.0.0
|
||||
version: 2.0.0.1
|
||||
synopsis: Deja Fu support for the Tasty test framework.
|
||||
|
||||
description:
|
||||
@ -30,14 +30,14 @@ source-repository head
|
||||
source-repository this
|
||||
type: git
|
||||
location: https://github.com/barrucadu/dejafu.git
|
||||
tag: tasty-dejafu-2.0.0.0
|
||||
tag: tasty-dejafu-2.0.0.1
|
||||
|
||||
library
|
||||
exposed-modules: Test.Tasty.DejaFu
|
||||
-- other-modules:
|
||||
-- other-extensions:
|
||||
build-depends: base >=4.9 && <5
|
||||
, dejafu >=2.0 && <2.1
|
||||
, dejafu >=2.0 && <2.2
|
||||
, random >=1.0 && <1.2
|
||||
, tagged >=0.8 && <0.9
|
||||
, tasty >=0.10 && <1.3
|
||||
|
Loading…
Reference in New Issue
Block a user