mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-11-27 04:36:57 +03:00
Michael Walker
GitHub
commit
fb43e90097
@ -45,10 +45,10 @@ There are a few different packages under the Déjà Fu umbrella:
|
||||
|
||||
| | Version | Summary |
|
||||
| - | ------- | ------- |
|
||||
| [concurrency][h:conc] | 1.5.0.0 | Typeclasses, functions, and data types for concurrency and STM. |
|
||||
| [dejafu][h:dejafu] | 1.10.1.0 | Systematic testing for Haskell concurrency. |
|
||||
| [hunit-dejafu][h:hunit] | 1.2.0.5 | Deja Fu support for the HUnit test framework. |
|
||||
| [tasty-dejafu][h:tasty] | 1.2.0.6 | Deja Fu support for the Tasty test framework. |
|
||||
| [concurrency][h:conc] | 1.6.0.0 | Typeclasses, functions, and data types for concurrency and STM. |
|
||||
| [dejafu][h:dejafu] | 1.11.0.0 | Systematic testing for Haskell concurrency. |
|
||||
| [hunit-dejafu][h:hunit] | 1.2.0.6 | Deja Fu support for the HUnit test framework. |
|
||||
| [tasty-dejafu][h:tasty] | 1.2.0.7 | 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.6.0.0 - IORefs (2018-07-01)
|
||||
-----------------------------
|
||||
|
||||
* Git: :tag:`concurrency-1.6.0.0`
|
||||
* Hackage: :hackage:`concurrency-1.6.0.0`
|
||||
|
||||
Added
|
||||
~~~~~
|
||||
|
||||
* ``Control.Concurrent.Classy.CRef``, deprecated ``*CRef`` functions
|
||||
and a ``CRef`` alias.
|
||||
|
||||
Changed
|
||||
~~~~~~~
|
||||
|
||||
* (:issue:`274`) ``CRef`` is now ``IORef``: all functions, modules,
|
||||
and types have been renamed.
|
||||
|
||||
|
||||
1.5.0.0 - No More 7.10 (2018-03-28)
|
||||
-----------------------------------
|
||||
|
||||
|
||||
@ -1,3 +1,5 @@
|
||||
{-# OPTIONS_GHC -Wno-deprecations #-}
|
||||
|
||||
-- |
|
||||
-- Module : Control.Concurrent.Classy
|
||||
-- Copyright : (c) 2016 Michael Walker
|
||||
@ -23,6 +25,7 @@ module Control.Concurrent.Classy
|
||||
( module Control.Monad.Conc.Class
|
||||
, module Control.Concurrent.Classy.Chan
|
||||
, module Control.Concurrent.Classy.CRef
|
||||
, module Control.Concurrent.Classy.IORef
|
||||
, module Control.Concurrent.Classy.MVar
|
||||
, module Control.Concurrent.Classy.STM
|
||||
, module Control.Concurrent.Classy.QSem
|
||||
@ -31,6 +34,7 @@ module Control.Concurrent.Classy
|
||||
|
||||
import Control.Concurrent.Classy.Chan
|
||||
import Control.Concurrent.Classy.CRef
|
||||
import Control.Concurrent.Classy.IORef
|
||||
import Control.Concurrent.Classy.MVar
|
||||
import Control.Concurrent.Classy.QSem
|
||||
import Control.Concurrent.Classy.QSemN
|
||||
|
||||
@ -1,19 +1,18 @@
|
||||
-- |
|
||||
-- Module : Control.Concurrent.Classy.CRef
|
||||
-- Copyright : (c) 2016 Michael Walker
|
||||
-- Copyright : (c) 2016--2018 Michael Walker
|
||||
-- License : MIT
|
||||
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
|
||||
-- Stability : stable
|
||||
-- Stability : experimental
|
||||
-- Portability : portable
|
||||
--
|
||||
-- Mutable references in a concurrency monad.
|
||||
--
|
||||
-- __Deviations:__ There is no @Eq@ instance for @MonadConc@ the
|
||||
-- @CRef@ type. Furthermore, the @mkWeakIORef@ function is not
|
||||
-- provided.
|
||||
module Control.Concurrent.Classy.CRef
|
||||
-- Deprecated re-exports of @IORef@ functions under the old @CRef@
|
||||
-- names.
|
||||
module Control.Concurrent.Classy.CRef {-# DEPRECATED "Import Control.Concurrent.Classy.IORef instead" #-}
|
||||
( -- * CRefs
|
||||
newCRef
|
||||
CRef
|
||||
, newCRef
|
||||
, newCRefN
|
||||
, readCRef
|
||||
, writeCRef
|
||||
, modifyCRef
|
||||
@ -22,6 +21,11 @@ module Control.Concurrent.Classy.CRef
|
||||
, atomicModifyCRef'
|
||||
, atomicWriteCRef
|
||||
|
||||
-- ** Compare-and-swap
|
||||
, casCRef
|
||||
, modifyCRefCAS
|
||||
, modifyCRefCAS_
|
||||
|
||||
-- * Memory Model
|
||||
|
||||
-- | In a concurrent program, @CRef@ operations may appear
|
||||
@ -80,41 +84,85 @@ module Control.Concurrent.Classy.CRef
|
||||
-- memory barrier.
|
||||
) where
|
||||
|
||||
import Control.Monad.Conc.Class
|
||||
import qualified Control.Concurrent.Classy.IORef as IORef
|
||||
import Control.Monad.Conc.Class (IORef, MonadConc, Ticket)
|
||||
import qualified Control.Monad.Conc.Class as IORef
|
||||
|
||||
-- | Type alias for 'IORef'.
|
||||
type CRef m a = IORef m a
|
||||
{-# DEPRECATED CRef "Use IORef instead" #-}
|
||||
|
||||
-- | Create a new reference.
|
||||
newCRef :: MonadConc m => a -> m (CRef m a)
|
||||
newCRef = IORef.newIORef
|
||||
{-# DEPRECATED newCRef "Use newIORef instead" #-}
|
||||
|
||||
-- | Create a new reference, but it is given a name which may be used
|
||||
-- to present more useful debugging information.
|
||||
newCRefN :: MonadConc m => String -> a -> m (CRef m a)
|
||||
newCRefN = IORef.newIORefN
|
||||
{-# DEPRECATED newCRefN "Use newIORefN instead" #-}
|
||||
|
||||
-- | Read the current value stored in a reference.
|
||||
readCRef :: MonadConc m => CRef m a -> m a
|
||||
readCRef = IORef.readIORef
|
||||
{-# DEPRECATED readCRef "Use readIORef instead" #-}
|
||||
|
||||
-- | Write a new value into an @CRef@, without imposing a memory
|
||||
-- barrier. This means that relaxed memory effects can be observed.
|
||||
writeCRef :: MonadConc m => CRef m a -> a -> m ()
|
||||
writeCRef = IORef.writeIORef
|
||||
{-# DEPRECATED writeCRef "Use writeIORef instead" #-}
|
||||
|
||||
-- | Mutate the contents of a @CRef@.
|
||||
--
|
||||
-- Be warned that 'modifyCRef' does not apply the function strictly.
|
||||
-- This means if the program calls 'modifyCRef' many times, but
|
||||
-- seldomly uses the value, thunks will pile up in memory resulting in
|
||||
-- a space leak. This is a common mistake made when using a @CRef@ as
|
||||
-- a counter. For example, the following will likely produce a stack
|
||||
-- overflow:
|
||||
--
|
||||
-- >ref <- newCRef 0
|
||||
-- >replicateM_ 1000000 $ modifyCRef ref (+1)
|
||||
-- >readCRef ref >>= print
|
||||
--
|
||||
-- To avoid this problem, use 'modifyCRef'' instead.
|
||||
--
|
||||
-- @since 1.0.0.0
|
||||
-- a space leak.
|
||||
modifyCRef :: MonadConc m => CRef m a -> (a -> a) -> m ()
|
||||
modifyCRef ref f = readCRef ref >>= writeCRef ref . f
|
||||
modifyCRef = IORef.modifyIORef
|
||||
{-# DEPRECATED modifyCRef "Use modifyIORef instead" #-}
|
||||
|
||||
-- | Strict version of 'modifyCRef'
|
||||
--
|
||||
-- @since 1.0.0.0
|
||||
modifyCRef' :: MonadConc m => CRef m a -> (a -> a) -> m ()
|
||||
modifyCRef' ref f = do
|
||||
x <- readCRef ref
|
||||
writeCRef ref $! f x
|
||||
modifyCRef' = IORef.modifyIORef'
|
||||
{-# DEPRECATED modifyCRef' "Use modifyIORef' instead" #-}
|
||||
|
||||
-- | Atomically modify the value stored in a reference. This imposes
|
||||
-- a full memory barrier.
|
||||
atomicModifyCRef :: MonadConc m => CRef m a -> (a -> (a, b)) -> m b
|
||||
atomicModifyCRef = IORef.atomicModifyIORef
|
||||
{-# DEPRECATED atomicModifyCRef "Use atomicModifyIORef instead" #-}
|
||||
|
||||
-- | Strict version of 'atomicModifyCRef'. This forces both the value
|
||||
-- stored in the @CRef@ as well as the value returned.
|
||||
--
|
||||
-- @since 1.0.0.0
|
||||
atomicModifyCRef' :: MonadConc m => CRef m a -> (a -> (a,b)) -> m b
|
||||
atomicModifyCRef' ref f = do
|
||||
b <- atomicModifyCRef ref $ \a -> case f a of
|
||||
v@(a',_) -> a' `seq` v
|
||||
pure $! b
|
||||
atomicModifyCRef' = IORef.atomicModifyIORef'
|
||||
{-# DEPRECATED atomicModifyCRef' "Use atomicModifyIORef' instead" #-}
|
||||
|
||||
-- | Replace the value stored in a reference, with the
|
||||
-- barrier-to-reordering property that 'atomicModifyIORef' has.
|
||||
atomicWriteCRef :: MonadConc m => CRef m a -> a -> m ()
|
||||
atomicWriteCRef = IORef.atomicWriteIORef
|
||||
{-# DEPRECATED atomicWriteCRef "Use atomicWriteIORef instead" #-}
|
||||
|
||||
-- | Perform a machine-level compare-and-swap (CAS) operation on a
|
||||
-- @CRef@. Returns an indication of success and a @Ticket@ for the
|
||||
-- most current value in the @CRef@.
|
||||
-- This is strict in the \"new\" value argument.
|
||||
casCRef :: MonadConc m => CRef m a -> Ticket m a -> a -> m (Bool, Ticket m a)
|
||||
casCRef = IORef.casIORef
|
||||
{-# DEPRECATED casCRef "Use casIORef instead" #-}
|
||||
|
||||
-- | A replacement for 'atomicModifyCRef' using a compare-and-swap.
|
||||
--
|
||||
-- This is strict in the \"new\" value argument.
|
||||
modifyCRefCAS :: MonadConc m => CRef m a -> (a -> (a, b)) -> m b
|
||||
modifyCRefCAS = IORef.modifyIORefCAS
|
||||
{-# DEPRECATED modifyCRefCAS "Use modifyIORefCAS instead" #-}
|
||||
|
||||
-- | A variant of 'modifyCRefCAS' which doesn't return a result.
|
||||
modifyCRefCAS_ :: MonadConc m => CRef m a -> (a -> a) -> m ()
|
||||
modifyCRefCAS_ = IORef.modifyIORefCAS_
|
||||
{-# DEPRECATED modifyCRefCAS_ "Use modifyIORefCAS_ instead" #-}
|
||||
|
||||
120
concurrency/Control/Concurrent/Classy/IORef.hs
Normal file
120
concurrency/Control/Concurrent/Classy/IORef.hs
Normal file
@ -0,0 +1,120 @@
|
||||
-- |
|
||||
-- Module : Control.Concurrent.Classy.IORef
|
||||
-- Copyright : (c) 2018 Michael Walker
|
||||
-- License : MIT
|
||||
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
|
||||
-- Stability : stable
|
||||
-- Portability : portable
|
||||
--
|
||||
-- Mutable references in a concurrency monad.
|
||||
--
|
||||
-- __Deviations:__ There is no @Eq@ instance for @MonadConc@ the
|
||||
-- @IORef@ type. Furthermore, the @mkWeakIORef@ function is not
|
||||
-- provided.
|
||||
module Control.Concurrent.Classy.IORef
|
||||
( -- * IORefs
|
||||
newIORef
|
||||
, readIORef
|
||||
, writeIORef
|
||||
, modifyIORef
|
||||
, modifyIORef'
|
||||
, atomicModifyIORef
|
||||
, atomicModifyIORef'
|
||||
, atomicWriteIORef
|
||||
|
||||
-- * Memory Model
|
||||
|
||||
-- | In a concurrent program, @IORef@ operations may appear
|
||||
-- out-of-order to another thread, depending on the memory model of
|
||||
-- the underlying processor architecture. For example, on x86 (which
|
||||
-- uses total store order), loads can move ahead of stores. Consider
|
||||
-- this example:
|
||||
--
|
||||
-- > iorefs :: MonadConc m => m (Bool, Bool)
|
||||
-- > iorefs = 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
|
||||
--
|
||||
-- Under a sequentially consistent memory model the possible results
|
||||
-- are @(True, True)@, @(True, False)@, and @(False, True)@. Under
|
||||
-- total or partial store order, @(False, False)@ is also a possible
|
||||
-- result, even though there is no interleaving of the threads which
|
||||
-- can lead to this.
|
||||
--
|
||||
-- We can see this by testing with different memory models:
|
||||
--
|
||||
-- > > autocheckWay defaultWay SequentialConsistency relaxed
|
||||
-- > [pass] Never Deadlocks
|
||||
-- > [pass] No Exceptions
|
||||
-- > [fail] Consistent Result
|
||||
-- > (False,True) S0---------S1----S0--S2----S0--
|
||||
-- >
|
||||
-- > (True,True) S0---------S1-P2----S1---S0---
|
||||
-- >
|
||||
-- > (True,False) S0---------S2----S1----S0---
|
||||
-- > False
|
||||
--
|
||||
-- > > autocheckWay defaultWay TotalStoreOrder relaxed
|
||||
-- > [pass] Never Deadlocks
|
||||
-- > [pass] No Exceptions
|
||||
-- > [fail] Consistent Result
|
||||
-- > (False,True) S0---------S1----S0--S2----S0--
|
||||
-- >
|
||||
-- > (False,False) S0---------S1--P2----S1--S0---
|
||||
-- >
|
||||
-- > (True,False) S0---------S2----S1----S0---
|
||||
-- >
|
||||
-- > (True,True) S0---------S1-C-S2----S1---S0---
|
||||
-- > False
|
||||
--
|
||||
-- Traces for non-sequentially-consistent memory models show where
|
||||
-- writes to @IORef@s are /committed/, which makes a write visible to
|
||||
-- all threads rather than just the one which performed the
|
||||
-- write. Only 'writeIORef' is broken up into separate write and
|
||||
-- commit steps, 'atomicModifyIORef' is still atomic and imposes a
|
||||
-- memory barrier.
|
||||
) where
|
||||
|
||||
import Control.Monad.Conc.Class
|
||||
|
||||
-- | Mutate the contents of a @IORef@.
|
||||
--
|
||||
-- Be warned that 'modifyIORef' does not apply the function strictly.
|
||||
-- This means if the program calls 'modifyIORef' many times, but
|
||||
-- seldomly uses the value, thunks will pile up in memory resulting in
|
||||
-- a space leak. This is a common mistake made when using a @IORef@ as
|
||||
-- a counter. For example, the following will likely produce a stack
|
||||
-- overflow:
|
||||
--
|
||||
-- >ref <- newIORef 0
|
||||
-- >replicateM_ 1000000 $ modifyIORef ref (+1)
|
||||
-- >readIORef ref >>= print
|
||||
--
|
||||
-- To avoid this problem, use 'modifyIORef'' instead.
|
||||
--
|
||||
-- @since 1.6.0.0
|
||||
modifyIORef :: MonadConc m => IORef m a -> (a -> a) -> m ()
|
||||
modifyIORef ref f = readIORef ref >>= writeIORef ref . f
|
||||
|
||||
-- | Strict version of 'modifyIORef'
|
||||
--
|
||||
-- @since 1.6.0.0
|
||||
modifyIORef' :: MonadConc m => IORef m a -> (a -> a) -> m ()
|
||||
modifyIORef' ref f = do
|
||||
x <- readIORef ref
|
||||
writeIORef ref $! f x
|
||||
|
||||
-- | Strict version of 'atomicModifyIORef'. This forces both the value
|
||||
-- stored in the @IORef@ as well as the value returned.
|
||||
--
|
||||
-- @since 1.6.0.0
|
||||
atomicModifyIORef' :: MonadConc m => IORef m a -> (a -> (a,b)) -> m b
|
||||
atomicModifyIORef' ref f = do
|
||||
b <- atomicModifyIORef ref $ \a -> case f a of
|
||||
v@(a',_) -> a' `seq` v
|
||||
pure $! b
|
||||
@ -8,7 +8,7 @@
|
||||
|
||||
-- |
|
||||
-- Module : Control.Monad.Conc.Class
|
||||
-- Copyright : (c) 2016--2017 Michael Walker
|
||||
-- Copyright : (c) 2016--2018 Michael Walker
|
||||
-- License : MIT
|
||||
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
|
||||
-- Stability : experimental
|
||||
@ -18,7 +18,7 @@
|
||||
-- monads.
|
||||
--
|
||||
-- __Deviations:__ An instance of @MonadConc@ is not required to be an
|
||||
-- instance of @MonadFix@, unlike @IO@. The @CRef@, @MVar@, and
|
||||
-- instance of @MonadFix@, unlike @IO@. The @IORef@, @MVar@, and
|
||||
-- @Ticket@ types are not required to be instances of @Show@ or @Eq@,
|
||||
-- unlike their normal counterparts. The @threadCapability@,
|
||||
-- @threadWaitRead@, @threadWaitWrite@, @threadWaitReadSTM@,
|
||||
@ -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.5.0.0
|
||||
-- @since 1.6.0.0
|
||||
class ( Monad m
|
||||
, MonadCatch m, MonadThrow m, MonadMask m
|
||||
, MonadSTM (STM m)
|
||||
@ -172,13 +172,13 @@ class ( Monad m
|
||||
, tryReadMVar
|
||||
, takeMVar
|
||||
, tryTakeMVar
|
||||
, (newCRef | newCRefN)
|
||||
, atomicModifyCRef
|
||||
, writeCRef
|
||||
, (newIORef | newIORefN)
|
||||
, atomicModifyIORef
|
||||
, writeIORef
|
||||
, readForCAS
|
||||
, peekTicket'
|
||||
, casCRef
|
||||
, modifyCRefCAS
|
||||
, casIORef
|
||||
, modifyIORefCAS
|
||||
, atomically
|
||||
, throwTo
|
||||
#-}
|
||||
@ -197,13 +197,13 @@ class ( Monad m
|
||||
type MVar m :: * -> *
|
||||
|
||||
-- | The mutable non-blocking reference type. These may suffer from
|
||||
-- relaxed memory effects if functions outside the set @newCRef@,
|
||||
-- @readCRef@, @atomicModifyCRef@, and @atomicWriteCRef@ are used.
|
||||
-- relaxed memory effects if functions outside the set @newIORef@,
|
||||
-- @readIORef@, @atomicModifyIORef@, and @atomicWriteIORef@ are used.
|
||||
--
|
||||
-- @since 1.0.0.0
|
||||
type CRef m :: * -> *
|
||||
-- @since 1.6.0.0
|
||||
type IORef m :: * -> *
|
||||
|
||||
-- | When performing compare-and-swap operations on @CRef@s, a
|
||||
-- | When performing compare-and-swap operations on @IORef@s, a
|
||||
-- @Ticket@ is a proof that a thread observed a specific previous
|
||||
-- value.
|
||||
--
|
||||
@ -376,55 +376,55 @@ class ( Monad m
|
||||
|
||||
-- | Create a new reference.
|
||||
--
|
||||
-- > newCRef = newCRefN ""
|
||||
-- > newIORef = newIORefN ""
|
||||
--
|
||||
-- @since 1.0.0.0
|
||||
newCRef :: a -> m (CRef m a)
|
||||
newCRef = newCRefN ""
|
||||
-- @since 1.6.0.0
|
||||
newIORef :: a -> m (IORef m a)
|
||||
newIORef = newIORefN ""
|
||||
|
||||
-- | Create a new reference, but it is given a name which may be
|
||||
-- used to present more useful debugging information.
|
||||
--
|
||||
-- > newCRefN _ = newCRef
|
||||
-- > newIORefN _ = newIORef
|
||||
--
|
||||
-- @since 1.0.0.0
|
||||
newCRefN :: String -> a -> m (CRef m a)
|
||||
newCRefN _ = newCRef
|
||||
-- @since 1.6.0.0
|
||||
newIORefN :: String -> a -> m (IORef m a)
|
||||
newIORefN _ = newIORef
|
||||
|
||||
-- | Read the current value stored in a reference.
|
||||
--
|
||||
-- > readCRef cref = readForCAS cref >>= peekTicket
|
||||
-- > readIORef ioref = readForCAS ioref >>= peekTicket
|
||||
--
|
||||
-- @since 1.0.0.0
|
||||
readCRef :: CRef m a -> m a
|
||||
readCRef cref = readForCAS cref >>= peekTicket
|
||||
-- @since 1.6.0.0
|
||||
readIORef :: IORef m a -> m a
|
||||
readIORef ioref = readForCAS ioref >>= peekTicket
|
||||
|
||||
-- | Atomically modify the value stored in a reference. This imposes
|
||||
-- a full memory barrier.
|
||||
--
|
||||
-- @since 1.0.0.0
|
||||
atomicModifyCRef :: CRef m a -> (a -> (a, b)) -> m b
|
||||
-- @since 1.6.0.0
|
||||
atomicModifyIORef :: IORef m a -> (a -> (a, b)) -> m b
|
||||
|
||||
-- | Write a new value into an @CRef@, without imposing a memory
|
||||
-- | Write a new value into an @IORef@, without imposing a memory
|
||||
-- barrier. This means that relaxed memory effects can be observed.
|
||||
--
|
||||
-- @since 1.0.0.0
|
||||
writeCRef :: CRef m a -> a -> m ()
|
||||
-- @since 1.6.0.0
|
||||
writeIORef :: IORef m a -> a -> m ()
|
||||
|
||||
-- | Replace the value stored in a reference, with the
|
||||
-- barrier-to-reordering property that 'atomicModifyCRef' has.
|
||||
-- barrier-to-reordering property that 'atomicModifyIORef' has.
|
||||
--
|
||||
-- > atomicWriteCRef r a = atomicModifyCRef r $ const (a, ())
|
||||
-- > atomicWriteIORef r a = atomicModifyIORef r $ const (a, ())
|
||||
--
|
||||
-- @since 1.0.0.0
|
||||
atomicWriteCRef :: CRef m a -> a -> m ()
|
||||
atomicWriteCRef r a = atomicModifyCRef r $ const (a, ())
|
||||
-- @since 1.6.0.0
|
||||
atomicWriteIORef :: IORef m a -> a -> m ()
|
||||
atomicWriteIORef r a = atomicModifyIORef r $ const (a, ())
|
||||
|
||||
-- | Read the current value stored in a reference, returning a
|
||||
-- @Ticket@, for use in future compare-and-swap operations.
|
||||
--
|
||||
-- @since 1.0.0.0
|
||||
readForCAS :: CRef m a -> m (Ticket m a)
|
||||
-- @since 1.6.0.0
|
||||
readForCAS :: IORef m a -> m (Ticket m a)
|
||||
|
||||
-- | Extract the actual Haskell value from a @Ticket@.
|
||||
--
|
||||
@ -434,28 +434,28 @@ class ( Monad m
|
||||
peekTicket' :: Proxy m -> Ticket m a -> a
|
||||
|
||||
-- | Perform a machine-level compare-and-swap (CAS) operation on a
|
||||
-- @CRef@. Returns an indication of success and a @Ticket@ for the
|
||||
-- most current value in the @CRef@.
|
||||
-- @IORef@. Returns an indication of success and a @Ticket@ for the
|
||||
-- most current value in the @IORef@.
|
||||
--
|
||||
-- This is strict in the \"new\" value argument.
|
||||
--
|
||||
-- @since 1.0.0.0
|
||||
casCRef :: CRef m a -> Ticket m a -> a -> m (Bool, Ticket m a)
|
||||
-- @since 1.6.0.0
|
||||
casIORef :: IORef m a -> Ticket m a -> a -> m (Bool, Ticket m a)
|
||||
|
||||
-- | A replacement for 'atomicModifyCRef' using a compare-and-swap.
|
||||
-- | A replacement for 'atomicModifyIORef' using a compare-and-swap.
|
||||
--
|
||||
-- This is strict in the \"new\" value argument.
|
||||
--
|
||||
-- @since 1.0.0.0
|
||||
modifyCRefCAS :: CRef m a -> (a -> (a, b)) -> m b
|
||||
-- @since 1.6.0.0
|
||||
modifyIORefCAS :: IORef m a -> (a -> (a, b)) -> m b
|
||||
|
||||
-- | A variant of 'modifyCRefCAS' which doesn't return a result.
|
||||
-- | A variant of 'modifyIORefCAS' which doesn't return a result.
|
||||
--
|
||||
-- > modifyCRefCAS_ cref f = modifyCRefCAS cref (\a -> (f a, ()))
|
||||
-- > modifyIORefCAS_ ioref f = modifyIORefCAS ioref (\a -> (f a, ()))
|
||||
--
|
||||
-- @since 1.0.0.0
|
||||
modifyCRefCAS_ :: CRef m a -> (a -> a) -> m ()
|
||||
modifyCRefCAS_ cref f = modifyCRefCAS cref (\a -> (f a, ()))
|
||||
-- @since 1.6.0.0
|
||||
modifyIORefCAS_ :: IORef m a -> (a -> a) -> m ()
|
||||
modifyIORefCAS_ ioref f = modifyIORefCAS ioref (\a -> (f a, ()))
|
||||
|
||||
-- | Perform an STM transaction atomically.
|
||||
--
|
||||
@ -687,14 +687,14 @@ newMVarN n a = do
|
||||
peekTicket :: forall m a. MonadConc m => Ticket m a -> m a
|
||||
peekTicket t = pure $ peekTicket' (Proxy :: Proxy m) (t :: Ticket m a)
|
||||
|
||||
-- | Compare-and-swap a value in a @CRef@, returning an indication of
|
||||
-- | Compare-and-swap a value in a @IORef@, returning an indication of
|
||||
-- success and the new value.
|
||||
--
|
||||
-- @since 1.0.0.0
|
||||
cas :: MonadConc m => CRef m a -> a -> m (Bool, a)
|
||||
cas cref a = do
|
||||
tick <- readForCAS cref
|
||||
(suc, tick') <- casCRef cref tick a
|
||||
-- @since 1.6.0.0
|
||||
cas :: MonadConc m => IORef m a -> a -> m (Bool, a)
|
||||
cas ioref a = do
|
||||
tick <- readForCAS ioref
|
||||
(suc, tick') <- casIORef ioref tick a
|
||||
a' <- peekTicket tick'
|
||||
|
||||
pure (suc, a')
|
||||
@ -706,7 +706,7 @@ cas cref a = do
|
||||
instance MonadConc IO where
|
||||
type STM IO = IO.STM
|
||||
type MVar IO = IO.MVar
|
||||
type CRef IO = IO.IORef
|
||||
type IORef IO = IO.IORef
|
||||
type Ticket IO = IO.Ticket
|
||||
type ThreadId IO = IO.ThreadId
|
||||
|
||||
@ -741,15 +741,15 @@ instance MonadConc IO where
|
||||
tryPutMVar = IO.tryPutMVar
|
||||
takeMVar = IO.takeMVar
|
||||
tryTakeMVar = IO.tryTakeMVar
|
||||
newCRef = IO.newIORef
|
||||
readCRef = IO.readIORef
|
||||
atomicModifyCRef = IO.atomicModifyIORef
|
||||
writeCRef = IO.writeIORef
|
||||
atomicWriteCRef = IO.atomicWriteIORef
|
||||
newIORef = IO.newIORef
|
||||
readIORef = IO.readIORef
|
||||
atomicModifyIORef = IO.atomicModifyIORef
|
||||
writeIORef = IO.writeIORef
|
||||
atomicWriteIORef = IO.atomicWriteIORef
|
||||
readForCAS = IO.readForCAS
|
||||
peekTicket' _ = IO.peekTicket
|
||||
casCRef = IO.casIORef
|
||||
modifyCRefCAS = IO.atomicModifyIORefCAS
|
||||
casIORef = IO.casIORef
|
||||
modifyIORefCAS = IO.atomicModifyIORefCAS
|
||||
atomically = IO.atomically
|
||||
readTVarConc = IO.readTVarIO
|
||||
|
||||
@ -786,7 +786,7 @@ fromIsConc = unIsConc
|
||||
instance MonadConc m => MonadConc (IsConc m) where
|
||||
type STM (IsConc m) = IsSTM (STM m)
|
||||
type MVar (IsConc m) = MVar m
|
||||
type CRef (IsConc m) = CRef m
|
||||
type IORef (IsConc m) = IORef m
|
||||
type Ticket (IsConc m) = Ticket m
|
||||
type ThreadId (IsConc m) = ThreadId m
|
||||
|
||||
@ -813,17 +813,17 @@ instance MonadConc m => MonadConc (IsConc m) where
|
||||
tryPutMVar v = toIsConc . tryPutMVar v
|
||||
takeMVar = toIsConc . takeMVar
|
||||
tryTakeMVar = toIsConc . tryTakeMVar
|
||||
newCRef = toIsConc . newCRef
|
||||
newCRefN n = toIsConc . newCRefN n
|
||||
readCRef = toIsConc . readCRef
|
||||
atomicModifyCRef r = toIsConc . atomicModifyCRef r
|
||||
writeCRef r = toIsConc . writeCRef r
|
||||
atomicWriteCRef r = toIsConc . atomicWriteCRef r
|
||||
newIORef = toIsConc . newIORef
|
||||
newIORefN n = toIsConc . newIORefN n
|
||||
readIORef = toIsConc . readIORef
|
||||
atomicModifyIORef r = toIsConc . atomicModifyIORef r
|
||||
writeIORef r = toIsConc . writeIORef r
|
||||
atomicWriteIORef r = toIsConc . atomicWriteIORef r
|
||||
readForCAS = toIsConc . readForCAS
|
||||
peekTicket' _ = peekTicket' (Proxy :: Proxy m)
|
||||
casCRef r t = toIsConc . casCRef r t
|
||||
modifyCRefCAS r = toIsConc . modifyCRefCAS r
|
||||
modifyCRefCAS_ r = toIsConc . modifyCRefCAS_ r
|
||||
casIORef r t = toIsConc . casIORef r t
|
||||
modifyIORefCAS r = toIsConc . modifyIORefCAS r
|
||||
modifyIORefCAS_ r = toIsConc . modifyIORefCAS_ r
|
||||
atomically = toIsConc . atomically . fromIsSTM
|
||||
readTVarConc = toIsConc . readTVarConc
|
||||
|
||||
@ -834,7 +834,7 @@ instance MonadConc m => MonadConc (IsConc m) where
|
||||
instance C => MonadConc (T m) where { \
|
||||
type STM (T m) = STM m ; \
|
||||
type MVar (T m) = MVar m ; \
|
||||
type CRef (T m) = CRef m ; \
|
||||
type IORef (T m) = IORef m ; \
|
||||
type Ticket (T m) = Ticket m ; \
|
||||
type ThreadId (T m) = ThreadId m ; \
|
||||
\
|
||||
@ -861,17 +861,17 @@ instance C => MonadConc (T m) where { \
|
||||
tryPutMVar v = lift . tryPutMVar v ; \
|
||||
takeMVar = lift . takeMVar ; \
|
||||
tryTakeMVar = lift . tryTakeMVar ; \
|
||||
newCRef = lift . newCRef ; \
|
||||
newCRefN n = lift . newCRefN n ; \
|
||||
readCRef = lift . readCRef ; \
|
||||
atomicModifyCRef r = lift . atomicModifyCRef r ; \
|
||||
writeCRef r = lift . writeCRef r ; \
|
||||
atomicWriteCRef r = lift . atomicWriteCRef r ; \
|
||||
newIORef = lift . newIORef ; \
|
||||
newIORefN n = lift . newIORefN n ; \
|
||||
readIORef = lift . readIORef ; \
|
||||
atomicModifyIORef r = lift . atomicModifyIORef r ; \
|
||||
writeIORef r = lift . writeIORef r ; \
|
||||
atomicWriteIORef r = lift . atomicWriteIORef r ; \
|
||||
readForCAS = lift . readForCAS ; \
|
||||
peekTicket' _ = peekTicket' (Proxy :: Proxy m) ; \
|
||||
casCRef r t = lift . casCRef r t ; \
|
||||
modifyCRefCAS r = lift . modifyCRefCAS r ; \
|
||||
modifyCRefCAS_ r = lift . modifyCRefCAS_ r ; \
|
||||
casIORef r t = lift . casIORef r t ; \
|
||||
modifyIORefCAS r = lift . modifyIORefCAS r ; \
|
||||
modifyIORefCAS_ r = lift . modifyIORefCAS_ r ; \
|
||||
atomically = lift . atomically ; \
|
||||
readTVarConc = lift . readTVarConc }
|
||||
|
||||
|
||||
@ -2,7 +2,7 @@
|
||||
-- documentation, see http://haskell.org/cabal/users-guide/
|
||||
|
||||
name: concurrency
|
||||
version: 1.5.0.0
|
||||
version: 1.6.0.0
|
||||
synopsis: Typeclasses, functions, and data types for concurrency and STM.
|
||||
|
||||
description:
|
||||
@ -32,7 +32,7 @@ source-repository head
|
||||
source-repository this
|
||||
type: git
|
||||
location: https://github.com/barrucadu/dejafu.git
|
||||
tag: concurrency-1.5.0.0
|
||||
tag: concurrency-1.6.0.0
|
||||
|
||||
library
|
||||
exposed-modules: Control.Monad.Conc.Class
|
||||
@ -42,6 +42,7 @@ library
|
||||
, Control.Concurrent.Classy.Async
|
||||
, Control.Concurrent.Classy.Chan
|
||||
, Control.Concurrent.Classy.CRef
|
||||
, Control.Concurrent.Classy.IORef
|
||||
, Control.Concurrent.Classy.MVar
|
||||
, Control.Concurrent.Classy.QSem
|
||||
, Control.Concurrent.Classy.QSemN
|
||||
|
||||
@ -213,9 +213,9 @@ newEmptyMVarInt = newEmptyMVar
|
||||
newMVarInt :: MonadConc m => Int -> m (MVar m Int)
|
||||
newMVarInt = newMVar
|
||||
|
||||
-- | Create a monomorphic @CRef@.
|
||||
newCRefInt :: MonadConc m => Int -> m (CRef m Int)
|
||||
newCRefInt = newCRef
|
||||
-- | Create a monomorphic @IORef@.
|
||||
newIORefInt :: MonadConc m => Int -> m (IORef m Int)
|
||||
newIORefInt = newIORef
|
||||
|
||||
-- | Create a monomorphic @TVar@.
|
||||
newTVarInt :: MonadSTM stm => Int -> stm (TVar stm Int)
|
||||
|
||||
@ -60,9 +60,9 @@ deadlocks = join (mkAutoUpdate defaultUpdateSettings)
|
||||
-- the program explicitly yields, the bounds don't need changing.
|
||||
nondeterministic :: forall m. MonadConc m => m Int
|
||||
nondeterministic = do
|
||||
var <- newCRef 0
|
||||
var <- newIORef 0
|
||||
let settings = (defaultUpdateSettings :: UpdateSettings m ())
|
||||
{ updateAction = atomicModifyCRef var (\x -> (x+1, x)) }
|
||||
{ updateAction = atomicModifyIORef var (\x -> (x+1, x)) }
|
||||
auto <- mkAutoUpdate settings
|
||||
void auto
|
||||
auto
|
||||
@ -84,7 +84,7 @@ defaultUpdateSettings = UpdateSettings
|
||||
|
||||
mkAutoUpdate :: MonadConc m => UpdateSettings m a -> m (m a)
|
||||
mkAutoUpdate us = do
|
||||
currRef <- newCRef Nothing
|
||||
currRef <- newIORef Nothing
|
||||
needsRunning <- newEmptyMVar
|
||||
lastValue <- newEmptyMVar
|
||||
|
||||
@ -93,17 +93,17 @@ mkAutoUpdate us = do
|
||||
|
||||
a <- catchSome $ updateAction us
|
||||
|
||||
writeCRef currRef $ Just a
|
||||
writeIORef currRef $ Just a
|
||||
void $ tryTakeMVar lastValue
|
||||
putMVar lastValue a
|
||||
|
||||
threadDelay $ updateFreq us
|
||||
|
||||
writeCRef currRef Nothing
|
||||
writeIORef currRef Nothing
|
||||
void $ takeMVar lastValue
|
||||
|
||||
pure $ do
|
||||
mval <- readCRef currRef
|
||||
mval <- readIORef currRef
|
||||
case mval of
|
||||
Just val -> pure val
|
||||
Nothing -> do
|
||||
|
||||
@ -119,7 +119,7 @@ _IDLING_ON = True
|
||||
|
||||
type ROnly m = RD.ReaderT (Sched m) m
|
||||
|
||||
newtype IVar m a = IVar (CRef m (IVarContents m a))
|
||||
newtype IVar m a = IVar (IORef m (IVarContents m a))
|
||||
|
||||
data IVarContents m a = Full a | Empty | Blocked [a -> m ()]
|
||||
|
||||
@ -205,7 +205,7 @@ runNewSessionAndWait name sched userComp = do
|
||||
_ <- modifyHotVar (activeSessions sched) (\ set -> (S.insert sid set, ()))
|
||||
|
||||
-- Here we have an extra IORef... ugly.
|
||||
ref <- newCRef (error$ "Empty session-result ref ("++name++") should never be touched (sid "++ show sid++", "++show tid ++")")
|
||||
ref <- newIORef (error$ "Empty session-result ref ("++name++") should never be touched (sid "++ show sid++", "++show tid ++")")
|
||||
newFlag <- newHotVar False
|
||||
-- Push the new session:
|
||||
_ <- modifyHotVar (sessions sched) (\ ls -> (Session sid newFlag : ls, ()))
|
||||
@ -213,11 +213,11 @@ runNewSessionAndWait name sched userComp = do
|
||||
let userComp' = do ans <- userComp
|
||||
-- This add-on to userComp will run only after userComp has completed successfully,
|
||||
-- but that does NOT guarantee that userComp-forked computations have terminated:
|
||||
io$ do writeCRef ref ans
|
||||
io$ do writeIORef ref ans
|
||||
writeHotVarRaw newFlag True
|
||||
modifyHotVar (activeSessions sched) (\ set -> (S.delete sid set, ()))
|
||||
kont n = trivialCont$ "("++name++", sid "++show sid++", round "++show n++")"
|
||||
loop n = do flg <- readCRef newFlag
|
||||
loop n = do flg <- readIORef newFlag
|
||||
unless flg $ do
|
||||
rescheduleR 0 $ trivialCont$ "("++name++", sid "++show sid++")"
|
||||
loop (n+1)
|
||||
@ -238,7 +238,7 @@ runNewSessionAndWait name sched userComp = do
|
||||
-- By returning here we ARE implicitly reengaging the scheduler, since we
|
||||
-- are already inside the rescheduleR loop on this thread
|
||||
-- (before runParIO was called in a nested fashion).
|
||||
readCRef ref
|
||||
readIORef ref
|
||||
|
||||
|
||||
{-# NOINLINE runParIO #-}
|
||||
@ -285,7 +285,7 @@ runParIO userComp = do
|
||||
putMVar workerDone cpu
|
||||
else do x <- runNewSessionAndWait "top-lvl main worker" sched userComp
|
||||
-- When the main worker finishes we can tell the anonymous "system" workers:
|
||||
writeCRef topSessFlag True
|
||||
writeIORef topSessFlag True
|
||||
putMVar mfin x
|
||||
|
||||
unregisterWorker tid
|
||||
@ -333,7 +333,7 @@ baseSessionID = 1000
|
||||
{-# INLINE new #-}
|
||||
-- | Creates a new @IVar@
|
||||
new :: MonadConc m => Par m (IVar m a)
|
||||
new = io$ IVar <$> newCRef Empty
|
||||
new = io$ IVar <$> newIORef Empty
|
||||
|
||||
{-# INLINE get #-}
|
||||
-- | Read the value in an @IVar@. The 'get' operation can only return when the
|
||||
@ -342,7 +342,7 @@ new = io$ IVar <$> newCRef Empty
|
||||
get (IVar vr) =
|
||||
callCC $ \kont ->
|
||||
do
|
||||
e <- io$ readCRef vr
|
||||
e <- io$ readIORef vr
|
||||
case e of
|
||||
Full a -> pure a
|
||||
_ -> do
|
||||
@ -351,7 +351,7 @@ get (IVar vr) =
|
||||
let resched = longjmpSched -- Invariant: kont must not be lost.
|
||||
-- Because we continue on the same processor the Sched stays the same:
|
||||
-- TODO: Try NOT using monadic values as first class. Check for performance effect:
|
||||
join . io$ atomicModifyCRef vr $ \case
|
||||
join . io$ atomicModifyIORef vr $ \case
|
||||
Empty -> (Blocked [pushWork sch . kont], resched)
|
||||
Full a -> (Full a, pure a) -- kont is implicit here.
|
||||
Blocked ks -> (Blocked (pushWork sch . kont:ks), resched)
|
||||
@ -362,7 +362,7 @@ get (IVar vr) =
|
||||
-- In this scheduler, puts immediately execute woken work in the current thread.
|
||||
put_ (IVar vr) !content = do
|
||||
sched <- RD.ask
|
||||
ks <- io$ atomicModifyCRef vr $ \case
|
||||
ks <- io$ atomicModifyIORef vr $ \case
|
||||
Empty -> (Full content, [])
|
||||
Full _ -> error "multiple put"
|
||||
Blocked ks -> (Full content, ks)
|
||||
@ -445,8 +445,8 @@ rescheduleR cnt kont = do
|
||||
mtask <- lift $ popWork mysched
|
||||
case mtask of
|
||||
Nothing -> do
|
||||
Session _ finRef:_ <- lift $ readCRef $ sessions mysched
|
||||
fin <- lift $ readCRef finRef
|
||||
Session _ finRef:_ <- lift $ readIORef $ sessions mysched
|
||||
fin <- lift $ readIORef finRef
|
||||
if fin
|
||||
then kont (error "Direct.hs: The result value from rescheduleR should not be used.")
|
||||
else do
|
||||
|
||||
@ -132,12 +132,12 @@ writeHotVarRaw :: MonadConc m => HotVar m a -> a -> m ()
|
||||
{-# INLINE readHotVar #-}
|
||||
{-# INLINE writeHotVar #-}
|
||||
|
||||
type HotVar m a = CRef m a
|
||||
newHotVar = newCRef
|
||||
modifyHotVar = atomicModifyCRef
|
||||
modifyHotVar_ v fn = atomicModifyCRef v (\a -> (fn a, ()))
|
||||
readHotVar = readCRef
|
||||
writeHotVar = writeCRef
|
||||
type HotVar m a = IORef m a
|
||||
newHotVar = newIORef
|
||||
modifyHotVar = atomicModifyIORef
|
||||
modifyHotVar_ v fn = atomicModifyIORef v (\a -> (fn a, ()))
|
||||
readHotVar = readIORef
|
||||
writeHotVar = writeIORef
|
||||
|
||||
readHotVarRaw = readHotVar
|
||||
writeHotVarRaw = writeHotVar
|
||||
|
||||
@ -215,13 +215,13 @@ work shortcircuit workitems = do
|
||||
-- If there's only one capability don't bother with threads.
|
||||
driver 1 res kill = do
|
||||
atomically . putTMVar kill $ failit res
|
||||
remaining <- newCRef workitems
|
||||
remaining <- newIORef workitems
|
||||
process remaining res
|
||||
|
||||
-- Fork off as many threads as there are capabilities, and queue
|
||||
-- up the remaining work.
|
||||
driver caps res kill = do
|
||||
remaining <- newCRef workitems
|
||||
remaining <- newIORef workitems
|
||||
tids <- mapM (\cap -> forkOn cap $ process remaining res) [0..caps-1]
|
||||
|
||||
-- Construct an action to short-circuit the computation.
|
||||
@ -236,7 +236,7 @@ work shortcircuit workitems = do
|
||||
-- Process a work item and store the result if it is a success,
|
||||
-- otherwise continue.
|
||||
process remaining res = do
|
||||
mitem <- atomicModifyCRef remaining $ \rs -> if null rs then ([], Nothing) else (tail rs, Just $ head rs)
|
||||
mitem <- atomicModifyIORef remaining $ \rs -> if null rs then ([], Nothing) else (tail rs, Just $ head rs)
|
||||
case mitem of
|
||||
Just item -> do
|
||||
fwrap <- item
|
||||
|
||||
@ -4,7 +4,7 @@
|
||||
module Integration.Async where
|
||||
|
||||
import Control.Concurrent.Classy.Async
|
||||
import Control.Concurrent.Classy.CRef
|
||||
import Control.Concurrent.Classy.IORef
|
||||
import Control.Exception (AsyncException(..), Exception,
|
||||
SomeException, fromException)
|
||||
import Control.Monad (when)
|
||||
@ -132,28 +132,28 @@ async_poll2 = do
|
||||
|
||||
case_concurrently_ :: MonadConc m => m ()
|
||||
case_concurrently_ = do
|
||||
ref <- newCRefInt 0
|
||||
ref <- newIORefInt 0
|
||||
() <- concurrently_
|
||||
(atomicModifyCRef ref (\x -> (x + 1, True)))
|
||||
(atomicModifyCRef ref (\x -> (x + 2, 'x')))
|
||||
res <- readCRef ref
|
||||
(atomicModifyIORef ref (\x -> (x + 1, True)))
|
||||
(atomicModifyIORef ref (\x -> (x + 2, 'x')))
|
||||
res <- readIORef ref
|
||||
res @?= 3
|
||||
|
||||
case_replicateConcurrently :: MonadConc m => m ()
|
||||
case_replicateConcurrently = do
|
||||
ref <- newCRefInt 0
|
||||
let action = atomicModifyCRef ref (\x -> (x + 1, x + 1))
|
||||
ref <- newIORefInt 0
|
||||
let action = atomicModifyIORef ref (\x -> (x + 1, x + 1))
|
||||
resList <- replicateConcurrently 4 action
|
||||
resVal <- readCRef ref
|
||||
resVal <- readIORef ref
|
||||
resVal @?= 4
|
||||
sort resList @?= [1..4]
|
||||
|
||||
case_replicateConcurrently_ :: MonadConc m => m ()
|
||||
case_replicateConcurrently_ = do
|
||||
ref <- newCRefInt 0
|
||||
let action = atomicModifyCRef ref (\x -> (x + 1, x + 1))
|
||||
ref <- newIORefInt 0
|
||||
let action = atomicModifyIORef ref (\x -> (x + 1, x + 1))
|
||||
() <- replicateConcurrently_ 4 action
|
||||
resVal <- readCRef ref
|
||||
resVal <- readIORef ref
|
||||
resVal @?= 4
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
@ -81,51 +81,51 @@ compareTest act = do
|
||||
-- reordered with other stores.
|
||||
intelWP21 :: MonadConc m => m (Int, Int)
|
||||
intelWP21 = snd <$> litmus2
|
||||
(\x y -> writeCRef x 1 >> writeCRef y 1)
|
||||
(\x y -> (,) <$> readCRef y <*> readCRef x)
|
||||
(\x y -> writeIORef x 1 >> writeIORef y 1)
|
||||
(\x y -> (,) <$> readIORef y <*> readIORef x)
|
||||
|
||||
-- | Stores are not reordered with older loads.
|
||||
intelWP22 :: MonadConc m => m (Int, Int)
|
||||
intelWP22 = litmus2
|
||||
(\x y -> do r1 <- readCRef x; writeCRef y 1; pure r1)
|
||||
(\x y -> do r2 <- readCRef y; writeCRef x 1; pure r2)
|
||||
(\x y -> do r1 <- readIORef x; writeIORef y 1; pure r1)
|
||||
(\x y -> do r2 <- readIORef y; writeIORef x 1; pure r2)
|
||||
|
||||
-- | Loads may be reordered with older stores to different locations.
|
||||
intelWP23 :: MonadConc m => m (Int, Int)
|
||||
intelWP23 = litmus2
|
||||
(\x y -> writeCRef x 1 >> readCRef y)
|
||||
(\x y -> writeCRef y 1 >> readCRef x)
|
||||
(\x y -> writeIORef x 1 >> readIORef y)
|
||||
(\x y -> writeIORef y 1 >> readIORef x)
|
||||
|
||||
-- | Loads are not reordered with older stores to the same location.
|
||||
intelWP24 :: MonadConc m => m (Int, Int)
|
||||
intelWP24 = litmus2
|
||||
(\x _ -> writeCRef x 1 >> readCRef x)
|
||||
(\_ y -> writeCRef y 1 >> readCRef y)
|
||||
(\x _ -> writeIORef x 1 >> readIORef x)
|
||||
(\_ y -> writeIORef y 1 >> readIORef y)
|
||||
|
||||
-- | Intra-processor forwarding is allowed
|
||||
intelWP25 :: MonadConc m => m ((Int, Int), (Int, Int))
|
||||
intelWP25 = litmus2
|
||||
(\x y -> do writeCRef x 1; r1 <- readCRef x; r2 <- readCRef y; pure (r1, r2))
|
||||
(\x y -> do writeCRef y 1; r3 <- readCRef y; r4 <- readCRef x; pure (r3, r4))
|
||||
(\x y -> do writeIORef x 1; r1 <- readIORef x; r2 <- readIORef y; pure (r1, r2))
|
||||
(\x y -> do writeIORef y 1; r3 <- readIORef y; r4 <- readIORef x; pure (r3, r4))
|
||||
|
||||
-- | Stores are transitively visible.
|
||||
intelWP26 :: MonadConc m => m (Int, Int, Int)
|
||||
intelWP26 = do
|
||||
x <- newCRef 0
|
||||
y <- newCRef 0
|
||||
j1 <- spawn (writeCRef x 1)
|
||||
j2 <- spawn (do r1 <- readCRef x; writeCRef x 1; pure r1)
|
||||
j3 <- spawn (do r2 <- readCRef y; r3 <- readCRef x; pure (r2,r3))
|
||||
x <- newIORef 0
|
||||
y <- newIORef 0
|
||||
j1 <- spawn (writeIORef x 1)
|
||||
j2 <- spawn (do r1 <- readIORef x; writeIORef x 1; pure r1)
|
||||
j3 <- spawn (do r2 <- readIORef y; r3 <- readIORef x; pure (r2,r3))
|
||||
(\() r1 (r2,r3) -> (r1,r2,r3)) <$> readMVar j1 <*> readMVar j2 <*> readMVar j3
|
||||
|
||||
-- | Total order on stores to the same location.
|
||||
intelWP27 :: MonadConc m => m ((Int, Int), (Int, Int))
|
||||
intelWP27 = do
|
||||
x <- newCRef 0
|
||||
j1 <- spawn (writeCRef x 1)
|
||||
j2 <- spawn (writeCRef x 2)
|
||||
j3 <- spawn (do r1 <- readCRef x; r2 <- readCRef x; pure (r1, r2))
|
||||
j4 <- spawn (do r3 <- readCRef x; r4 <- readCRef x; pure (r3, r4))
|
||||
x <- newIORef 0
|
||||
j1 <- spawn (writeIORef x 1)
|
||||
j2 <- spawn (writeIORef x 2)
|
||||
j3 <- spawn (do r1 <- readIORef x; r2 <- readIORef x; pure (r1, r2))
|
||||
j4 <- spawn (do r3 <- readIORef x; r4 <- readIORef x; pure (r3, r4))
|
||||
(\() () r12 r23 -> (r12, r23)) <$> readMVar j1 <*> readMVar j2 <*> readMVar j3 <*> readMVar j4
|
||||
|
||||
-- | Independent Read Independent Write.
|
||||
@ -134,24 +134,24 @@ intelWP27 = do
|
||||
-- ((1,0),(1,0)). Intel (and TSO/PSO) forbid it.
|
||||
intelWP28 :: MonadConc m => m ((Int, Int), (Int, Int))
|
||||
intelWP28 = do
|
||||
x <- newCRef 0
|
||||
y <- newCRef 0
|
||||
j1 <- spawn (writeCRef x 1)
|
||||
j2 <- spawn (writeCRef y 1)
|
||||
j3 <- spawn (do r1 <- readCRef x; r2 <- readCRef y; pure (r1, r2))
|
||||
j4 <- spawn (do r3 <- readCRef y; r4 <- readCRef x; pure (r3, r4))
|
||||
x <- newIORef 0
|
||||
y <- newIORef 0
|
||||
j1 <- spawn (writeIORef x 1)
|
||||
j2 <- spawn (writeIORef y 1)
|
||||
j3 <- spawn (do r1 <- readIORef x; r2 <- readIORef y; pure (r1, r2))
|
||||
j4 <- spawn (do r3 <- readIORef y; r4 <- readIORef x; pure (r3, r4))
|
||||
(\() () r12 r23 -> (r12, r23)) <$> readMVar j1 <*> readMVar j2 <*> readMVar j3 <*> readMVar j4
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
-- | Create two @CRef@s, fork the two threads, and return the result.
|
||||
-- | Create two @IORef@s, fork the two threads, and return the result.
|
||||
litmus2 :: MonadConc m
|
||||
=> (CRef m Int -> CRef m Int -> m b)
|
||||
-> (CRef m Int -> CRef m Int -> m c)
|
||||
=> (IORef m Int -> IORef m Int -> m b)
|
||||
-> (IORef m Int -> IORef m Int -> m c)
|
||||
-> m (b, c)
|
||||
litmus2 thread1 thread2 = do
|
||||
x <- newCRef 0
|
||||
y <- newCRef 0
|
||||
x <- newIORef 0
|
||||
y <- newIORef 0
|
||||
j1 <- spawn (thread1 x y)
|
||||
j2 <- spawn (thread2 x y)
|
||||
(,) <$> readMVar j1 <*> readMVar j2
|
||||
|
||||
@ -18,7 +18,7 @@ tests :: [TestTree]
|
||||
tests =
|
||||
[ testGroup "Threading" threadingTests
|
||||
, testGroup "MVar" mvarTests
|
||||
, testGroup "CRef" crefTests
|
||||
, testGroup "IORef" iorefTests
|
||||
, testGroup "STM" stmTests
|
||||
, testGroup "Exceptions" exceptionTests
|
||||
, testGroup "Capabilities" capabilityTests
|
||||
@ -40,9 +40,9 @@ threadingTests = toTestList
|
||||
(/=) <$> myThreadId <*> readMVar tid
|
||||
|
||||
, djfuT "A thread doesn't wait for its children before terminating" (gives' [Nothing, Just ()]) $ do
|
||||
x <- newCRef Nothing
|
||||
_ <- fork . writeCRef x $ Just ()
|
||||
readCRef x
|
||||
x <- newIORef Nothing
|
||||
_ <- fork . writeIORef x $ Just ()
|
||||
readIORef x
|
||||
|
||||
, djfuT "The main thread is bound" (gives' [(True, True)]) $ do
|
||||
b1 <- isCurrentThreadBound
|
||||
@ -117,58 +117,58 @@ mvarTests = toTestList
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
crefTests :: [TestTree]
|
||||
crefTests = toTestList
|
||||
[ djfuT "Racey CRef computations are nondeterministic" (gives' [0,1]) $ do
|
||||
x <- newCRefInt 0
|
||||
j1 <- spawn $ writeCRef x 0
|
||||
j2 <- spawn $ writeCRef x 1
|
||||
iorefTests :: [TestTree]
|
||||
iorefTests = toTestList
|
||||
[ djfuT "Racey IORef computations are nondeterministic" (gives' [0,1]) $ do
|
||||
x <- newIORefInt 0
|
||||
j1 <- spawn $ writeIORef x 0
|
||||
j2 <- spawn $ writeIORef x 1
|
||||
takeMVar j1
|
||||
takeMVar j2
|
||||
readCRef x
|
||||
readIORef x
|
||||
|
||||
, djfuT "CASing CRef changes its value" (gives' [0,1]) $ do
|
||||
x <- newCRefInt 0
|
||||
_ <- fork $ modifyCRefCAS x (const (1, ()))
|
||||
readCRef x
|
||||
, djfuT "CASing IORef changes its value" (gives' [0,1]) $ do
|
||||
x <- newIORefInt 0
|
||||
_ <- fork $ modifyIORefCAS x (const (1, ()))
|
||||
readIORef x
|
||||
|
||||
, djfuT "Racey CAS computations are nondeterministic" (gives' [(True, 2), (False, 2)]) $ do
|
||||
x <- newCRefInt 0
|
||||
x <- newIORefInt 0
|
||||
t <- readForCAS x
|
||||
j <- spawn $ casCRef x t 1
|
||||
writeCRef x 2
|
||||
j <- spawn $ casIORef x t 1
|
||||
writeIORef x 2
|
||||
b <- fst <$> readMVar j
|
||||
v <- readCRef x
|
||||
v <- readIORef x
|
||||
pure (b, v)
|
||||
|
||||
, djfuT "A failed CAS gives an updated ticket" (gives' [(True, 1), (True, 2)]) $ do
|
||||
x <- newCRefInt 0
|
||||
x <- newIORefInt 0
|
||||
t <- readForCAS x
|
||||
v <- newEmptyMVar
|
||||
j <- spawn $ do
|
||||
o@(f, t') <- casCRef x t 1
|
||||
o@(f, t') <- casIORef x t 1
|
||||
takeMVar v
|
||||
if f then pure o else casCRef x t' 1
|
||||
writeCRef x 2
|
||||
if f then pure o else casIORef x t' 1
|
||||
writeIORef x 2
|
||||
putMVar v ()
|
||||
b <- fst <$> readMVar j
|
||||
o <- readCRef x
|
||||
o <- readIORef x
|
||||
pure (b, o)
|
||||
|
||||
, djfuT "A ticket is only good for one CAS" (gives' [(True, False, 1), (False, True, 2)]) $ do
|
||||
x <- newCRefInt 0
|
||||
x <- newIORefInt 0
|
||||
t <- readForCAS x
|
||||
j1 <- spawn $ casCRef x t 1
|
||||
j2 <- spawn $ casCRef x t 2
|
||||
j1 <- spawn $ casIORef x t 1
|
||||
j2 <- spawn $ casIORef x t 2
|
||||
b1 <- fst <$> readMVar j1
|
||||
b2 <- fst <$> readMVar j2
|
||||
v <- readCRef x
|
||||
v <- readIORef x
|
||||
pure (b1, b2, v)
|
||||
|
||||
, djfuT "CRef writes may be delayed" (gives' [0,1]) $ do
|
||||
x <- newCRefInt 0
|
||||
writeCRef x 1
|
||||
takeMVar =<< spawn (readCRef x)
|
||||
, djfuT "IORef writes may be delayed" (gives' [0,1]) $ do
|
||||
x <- newIORefInt 0
|
||||
writeIORef x 1
|
||||
takeMVar =<< spawn (readIORef x)
|
||||
]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
@ -312,18 +312,18 @@ hacksTests = toTestList
|
||||
, testGroup "DontCheck"
|
||||
[ djfuT "Inner action is run with a deterministic scheduler" (gives' [1]) $
|
||||
dontCheck Nothing $ do
|
||||
r <- newCRefInt 1
|
||||
_ <- fork (atomicWriteCRef r 2)
|
||||
readCRef r
|
||||
r <- newIORefInt 1
|
||||
_ <- fork (atomicWriteIORef r 2)
|
||||
readIORef r
|
||||
|
||||
, djfuT "Threads created by the inner action persist in the outside" (gives' [1,2]) $ do
|
||||
(ref, trigger) <- dontCheck Nothing $ do
|
||||
r <- newCRefInt 1
|
||||
r <- newIORefInt 1
|
||||
v <- newEmptyMVar
|
||||
_ <- fork (takeMVar v >> atomicWriteCRef r 2)
|
||||
_ <- fork (takeMVar v >> atomicWriteIORef r 2)
|
||||
pure (r, v)
|
||||
putMVar trigger ()
|
||||
readCRef ref
|
||||
readIORef ref
|
||||
|
||||
, djfuT "Bound threads created on the inside are bound on the outside" (gives' [True]) $ do
|
||||
(out, trigger) <- dontCheck Nothing $ do
|
||||
@ -344,10 +344,10 @@ hacksTests = toTestList
|
||||
|
||||
, djfuT "Inner action is run under sequential consistency" (gives' [1]) $ do
|
||||
x <- dontCheck Nothing $ do
|
||||
x <- newCRefInt 0
|
||||
writeCRef x 1
|
||||
x <- newIORefInt 0
|
||||
writeIORef x 1
|
||||
pure x
|
||||
takeMVar =<< spawn (readCRef x)
|
||||
takeMVar =<< spawn (readIORef x)
|
||||
]
|
||||
]
|
||||
|
||||
|
||||
@ -3,7 +3,7 @@ module Integration.Names where
|
||||
import Control.Concurrent.Classy hiding (check)
|
||||
import Data.Maybe (mapMaybe)
|
||||
import Test.DejaFu.Conc (ConcIO)
|
||||
import Test.DejaFu.Internal (crefOf, mvarOf, simplifyAction,
|
||||
import Test.DejaFu.Internal (iorefOf, mvarOf, simplifyAction,
|
||||
tidsOf, tvarsOf)
|
||||
import Test.DejaFu.SCT (runSCT)
|
||||
import Test.DejaFu.Types
|
||||
@ -15,7 +15,7 @@ tests :: [TestTree]
|
||||
tests =
|
||||
toTestList
|
||||
[ testCase "MVar names" testMVarNames
|
||||
, testCase "CRef names" testCRefNames
|
||||
, testCase "IORef names" testIORefNames
|
||||
, testCase "TVar names" testTVarNames
|
||||
, testCase "Thread names" testThreadNames
|
||||
]
|
||||
@ -52,24 +52,24 @@ testMVarNames =
|
||||
let validMVid = maybe False (`elem` [mvarName1, mvarName2]) . mvarName
|
||||
in all validMVid . mapMaybe mvar
|
||||
|
||||
testCRefNames :: Assertion
|
||||
testCRefNames =
|
||||
check "All traces should use only required CRef names" checkCRefs $ do
|
||||
x <- newCRefN crefName1 (0::Int)
|
||||
y <- newCRefN crefName2 (0::Int)
|
||||
_ <- fork $ modifyCRefCAS x (const (1, ()))
|
||||
_ <- fork $ writeCRef y 2
|
||||
(,) <$> readCRef x <*> readCRef y
|
||||
testIORefNames :: Assertion
|
||||
testIORefNames =
|
||||
check "All traces should use only required IORef names" checkIORefs $ do
|
||||
x <- newIORefN iorefName1 (0::Int)
|
||||
y <- newIORefN iorefName2 (0::Int)
|
||||
_ <- fork $ modifyIORefCAS x (const (1, ()))
|
||||
_ <- fork $ writeIORef y 2
|
||||
(,) <$> readIORef x <*> readIORef y
|
||||
where
|
||||
crefName1 = "cref-one"
|
||||
crefName2 = "cref-two"
|
||||
crefName (CRefId (Id (Just n) _)) = Just n
|
||||
crefName _ = Nothing
|
||||
cref (NewCRef ref) = Just ref
|
||||
cref a = crefOf (simplifyAction a)
|
||||
checkCRefs =
|
||||
let validCRef = maybe False (`elem` [crefName1, crefName2]) . crefName
|
||||
in all validCRef . mapMaybe cref
|
||||
iorefName1 = "ioref-one"
|
||||
iorefName2 = "ioref-two"
|
||||
iorefName (IORefId (Id (Just n) _)) = Just n
|
||||
iorefName _ = Nothing
|
||||
ioref (NewIORef ref) = Just ref
|
||||
ioref a = iorefOf (simplifyAction a)
|
||||
checkIORefs =
|
||||
let validIORef = maybe False (`elem` [iorefName1, iorefName2]) . iorefName
|
||||
in all validIORef . mapMaybe ioref
|
||||
|
||||
testTVarNames :: Assertion
|
||||
testTVarNames =
|
||||
|
||||
@ -16,9 +16,9 @@ import QSemN
|
||||
tests :: [TestTree]
|
||||
tests = toTestList
|
||||
[ djfu "https://github.com/barrucadu/dejafu/issues/40" (gives' [0,1]) $ do
|
||||
x <- newCRefInt 0
|
||||
_ <- fork $ myThreadId >> writeCRef x 1
|
||||
readCRef x
|
||||
x <- newIORefInt 0
|
||||
_ <- fork $ myThreadId >> writeIORef x 1
|
||||
readIORef x
|
||||
|
||||
, djfu "https://github.com/barrucadu/dejafu/issues/55" (gives' [True]) $ do
|
||||
a <- atomically newTQueue
|
||||
|
||||
@ -21,7 +21,7 @@ import Common
|
||||
tests :: [TestTree]
|
||||
tests =
|
||||
[ testGroup "MVar" mvarTests
|
||||
, testGroup "CRef" crefTests
|
||||
, testGroup "IORef" iorefTests
|
||||
, testGroup "STM" stmTests
|
||||
, testGroup "Exceptions" exceptionTests
|
||||
, testGroup "Capabilities" capabilityTests
|
||||
@ -86,47 +86,47 @@ mvarTests = toTestList
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
crefTests :: [TestTree]
|
||||
crefTests = toTestList
|
||||
[ djfu "Reading a non-updated CRef gives its initial value" (gives' [True]) $ do
|
||||
ref <- newCRefInt 5
|
||||
(5==) <$> readCRef ref
|
||||
iorefTests :: [TestTree]
|
||||
iorefTests = toTestList
|
||||
[ djfu "Reading a non-updated IORef gives its initial value" (gives' [True]) $ do
|
||||
ref <- newIORefInt 5
|
||||
(5==) <$> readIORef ref
|
||||
|
||||
, djfu "Reading an updated CRef gives its new value" (gives' [True]) $ do
|
||||
ref <- newCRefInt 5
|
||||
writeCRef ref 6
|
||||
(6==) <$> readCRef ref
|
||||
, djfu "Reading an updated IORef gives its new value" (gives' [True]) $ do
|
||||
ref <- newIORefInt 5
|
||||
writeIORef ref 6
|
||||
(6==) <$> readIORef ref
|
||||
|
||||
, djfu "Updating a CRef by a function changes its value" (gives' [True]) $ do
|
||||
ref <- newCRefInt 5
|
||||
atomicModifyCRef ref (\i -> (i+1, ()))
|
||||
(6==) <$> readCRef ref
|
||||
, djfu "Updating a IORef by a function changes its value" (gives' [True]) $ do
|
||||
ref <- newIORefInt 5
|
||||
atomicModifyIORef ref (\i -> (i+1, ()))
|
||||
(6==) <$> readIORef ref
|
||||
|
||||
, djfu "A ticket contains the value of the CRef at the time of its creation" (gives' [True]) $ do
|
||||
ref <- newCRefInt 5
|
||||
, djfu "A ticket contains the value of the IORef at the time of its creation" (gives' [True]) $ do
|
||||
ref <- newIORefInt 5
|
||||
tick <- readForCAS ref
|
||||
writeCRef ref 6
|
||||
writeIORef ref 6
|
||||
(5==) <$> peekTicket tick
|
||||
|
||||
, djfu "Compare-and-swap returns a ticket containing the new value" (gives' [True]) $ do
|
||||
ref <- newCRefInt 5
|
||||
ref <- newIORefInt 5
|
||||
tick <- readForCAS ref
|
||||
(_, tick') <- casCRef ref tick 6
|
||||
(_, tick') <- casIORef ref tick 6
|
||||
(6==) <$> peekTicket tick'
|
||||
|
||||
, djfu "Compare-and-swap on an unmodified CRef succeeds" (gives' [True]) $ do
|
||||
ref <- newCRefInt 5
|
||||
, djfu "Compare-and-swap on an unmodified IORef succeeds" (gives' [True]) $ do
|
||||
ref <- newIORefInt 5
|
||||
tick <- readForCAS ref
|
||||
(suc, _) <- casCRef ref tick 6
|
||||
val <- readCRef ref
|
||||
(suc, _) <- casIORef ref tick 6
|
||||
val <- readIORef ref
|
||||
pure (suc && (6 == val))
|
||||
|
||||
, djfu "Compare-and-swap on a modified CRef fails" (gives' [True]) $ do
|
||||
ref <- newCRefInt 5
|
||||
, djfu "Compare-and-swap on a modified IORef fails" (gives' [True]) $ do
|
||||
ref <- newIORefInt 5
|
||||
tick <- readForCAS ref
|
||||
writeCRef ref 6
|
||||
(suc, _) <- casCRef ref tick 7
|
||||
val <- readCRef ref
|
||||
writeIORef ref 6
|
||||
(suc, _) <- casIORef ref tick 7
|
||||
val <- readIORef ref
|
||||
pure (not suc && 7 /= val)
|
||||
]
|
||||
|
||||
@ -292,11 +292,11 @@ hacksTests = toTestList
|
||||
, toTestList . testGroup "Snapshotting" $ let snapshotTest n p conc = W n conc p ("randomly", randomly (mkStdGen 0) 150) in
|
||||
[ snapshotTest "State updates are applied correctly" (gives' [2]) $ do
|
||||
r <- dontCheck Nothing $ do
|
||||
r <- newCRefInt 0
|
||||
writeCRef r 1
|
||||
writeCRef r 2
|
||||
r <- newIORefInt 0
|
||||
writeIORef r 1
|
||||
writeIORef r 2
|
||||
pure r
|
||||
readCRef r
|
||||
readIORef r
|
||||
|
||||
, snapshotTest "Lifted IO is re-run (1)" (gives' [2..151]) $ do
|
||||
r <- dontCheck Nothing $ do
|
||||
|
||||
@ -162,12 +162,12 @@ commonProps = toTestList
|
||||
|
||||
, testProperty "isBarrier a ==> synchronises a r" $ do
|
||||
a <- H.forAll (HGen.filter D.isBarrier genActionType)
|
||||
r <- H.forAll genCRefId
|
||||
r <- H.forAll genIORefId
|
||||
H.assert (D.synchronises a r)
|
||||
|
||||
, testProperty "isCommit a r ==> synchronises a r" $ do
|
||||
a <- H.forAll genPartiallySynchronisedActionType
|
||||
case D.crefOf a of
|
||||
case D.iorefOf a of
|
||||
Just r -> H.assert (D.synchronises a r)
|
||||
_ -> H.discard
|
||||
]
|
||||
@ -179,8 +179,8 @@ memoryProps = toTestList
|
||||
[ testProperty "bufferWrite emptyBuffer k c a /= emptyBuffer" $ do
|
||||
k <- H.forAll genWBKey
|
||||
a <- H.forAll genInt
|
||||
res <- crefProp $ \cref -> do
|
||||
wb <- Mem.bufferWrite Mem.emptyBuffer k cref a
|
||||
res <- iorefProp $ \ioref -> do
|
||||
wb <- Mem.bufferWrite Mem.emptyBuffer k ioref a
|
||||
wb `eqWB` Mem.emptyBuffer
|
||||
H.assert (not res)
|
||||
|
||||
@ -194,8 +194,8 @@ memoryProps = toTestList
|
||||
, testProperty "commitWrite (bufferWrite emptyBuffer k a) k == emptyBuffer" $ do
|
||||
k <- H.forAll genWBKey
|
||||
a <- H.forAll genInt
|
||||
res <- crefProp $ \cref -> do
|
||||
wb1 <- Mem.bufferWrite Mem.emptyBuffer k cref a
|
||||
res <- iorefProp $ \ioref -> do
|
||||
wb1 <- Mem.bufferWrite Mem.emptyBuffer k ioref a
|
||||
wb2 <- Mem.commitWrite wb1 k
|
||||
wb2 `eqWB` Mem.emptyBuffer
|
||||
H.assert res
|
||||
@ -203,19 +203,19 @@ memoryProps = toTestList
|
||||
, testProperty "Single buffered write/read from same thread" $ do
|
||||
k@(tid, _) <- H.forAll genWBKey
|
||||
a <- H.forAll genInt
|
||||
res <- crefProp $ \cref -> do
|
||||
_ <- Mem.bufferWrite Mem.emptyBuffer k cref a
|
||||
Mem.readCRef cref tid
|
||||
res <- iorefProp $ \ioref -> do
|
||||
_ <- Mem.bufferWrite Mem.emptyBuffer k ioref a
|
||||
Mem.readIORef ioref tid
|
||||
a H.=== res
|
||||
|
||||
, testProperty "Overriding buffered write/read from same thread" $ do
|
||||
k@(tid, _) <- H.forAll genWBKey
|
||||
a1 <- H.forAll genInt
|
||||
a2 <- H.forAll genInt
|
||||
res <- crefProp $ \cref -> do
|
||||
_ <- Mem.bufferWrite Mem.emptyBuffer k cref a1
|
||||
_ <- Mem.bufferWrite Mem.emptyBuffer k cref a2
|
||||
Mem.readCRef cref tid
|
||||
res <- iorefProp $ \ioref -> do
|
||||
_ <- Mem.bufferWrite Mem.emptyBuffer k ioref a1
|
||||
_ <- Mem.bufferWrite Mem.emptyBuffer k ioref a2
|
||||
Mem.readIORef ioref tid
|
||||
a2 H.=== res
|
||||
|
||||
, testProperty "Buffered write/read from different thread" $ do
|
||||
@ -223,22 +223,22 @@ memoryProps = toTestList
|
||||
k2 <- H.forAll (HGen.filter ((/=tid) . fst) genWBKey)
|
||||
a1 <- H.forAll genInt
|
||||
a2 <- H.forAll genInt
|
||||
res <- crefProp $ \cref -> do
|
||||
_ <- Mem.bufferWrite Mem.emptyBuffer k1 cref a1
|
||||
_ <- Mem.bufferWrite Mem.emptyBuffer k2 cref a2
|
||||
Mem.readCRef cref tid
|
||||
res <- iorefProp $ \ioref -> do
|
||||
_ <- Mem.bufferWrite Mem.emptyBuffer k1 ioref a1
|
||||
_ <- Mem.bufferWrite Mem.emptyBuffer k2 ioref a2
|
||||
Mem.readIORef ioref tid
|
||||
a1 H.=== res
|
||||
]
|
||||
where
|
||||
crefProp
|
||||
iorefProp
|
||||
:: Show a
|
||||
=> (D.ModelCRef IO Int -> IO a)
|
||||
=> (D.ModelIORef IO Int -> IO a)
|
||||
-> H.PropertyT IO a
|
||||
crefProp p = do
|
||||
crefId <- H.forAll genCRefId
|
||||
iorefProp p = do
|
||||
iorefId <- H.forAll genIORefId
|
||||
liftIO $ do
|
||||
cref <- makeCRef crefId
|
||||
p cref
|
||||
ioref <- makeIORef iorefId
|
||||
p ioref
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
@ -278,8 +278,8 @@ sctProps = toTestList
|
||||
-------------------------------------------------------------------------------
|
||||
-- Utils
|
||||
|
||||
makeCRef :: D.CRefId -> IO (D.ModelCRef IO Int)
|
||||
makeCRef crid = D.ModelCRef crid <$> C.newCRef (M.empty, 0, 42)
|
||||
makeIORef :: D.IORefId -> IO (D.ModelIORef IO Int)
|
||||
makeIORef iorid = D.ModelIORef iorid <$> C.newIORef (M.empty, 0, 42)
|
||||
|
||||
-- equality for writebuffers is a little tricky as we can't directly
|
||||
-- compare the buffered values, so we compare everything else:
|
||||
@ -288,7 +288,7 @@ makeCRef crid = D.ModelCRef crid <$> C.newCRef (M.empty, 0, 42)
|
||||
-- - each pair of buffers for the same key must have an equal sequence of writes
|
||||
--
|
||||
-- individual writes are compared like so:
|
||||
-- - the threadid and crefid must be the same
|
||||
-- - the threadid and iorefid must be the same
|
||||
-- - the cache and number of writes inside the ref must be the same
|
||||
eqWB :: Mem.WriteBuffer IO -> Mem.WriteBuffer IO -> IO Bool
|
||||
eqWB (Mem.WriteBuffer wb1) (Mem.WriteBuffer wb2) = andM (pure (ks1 == ks2) :
|
||||
@ -301,10 +301,10 @@ eqWB (Mem.WriteBuffer wb1) (Mem.WriteBuffer wb2) = andM (pure (ks1 == ks2) :
|
||||
ks1 = M.keys $ M.filter (not . S.null) wb1
|
||||
ks2 = M.keys $ M.filter (not . S.null) wb2
|
||||
|
||||
eqBW (Mem.BufferedWrite t1 (D.ModelCRef crid1 ref1) _) (Mem.BufferedWrite t2 (D.ModelCRef crid2 ref2) _) = do
|
||||
d1 <- (\(m,i,_) -> (M.keys m, i)) <$> C.readCRef ref1
|
||||
d2 <- (\(m,i,_) -> (M.keys m, i)) <$> C.readCRef ref2
|
||||
pure (t1 == t2 && crid1 == crid2 && d1 == d2)
|
||||
eqBW (Mem.BufferedWrite t1 (D.ModelIORef iorid1 ref1) _) (Mem.BufferedWrite t2 (D.ModelIORef iorid2 ref2) _) = do
|
||||
d1 <- (\(m,i,_) -> (M.keys m, i)) <$> C.readIORef ref1
|
||||
d2 <- (\(m,i,_) -> (M.keys m, i)) <$> C.readIORef ref2
|
||||
pure (t1 == t2 && iorid1 == iorid2 && d1 == d2)
|
||||
|
||||
andM [] = pure True
|
||||
andM (p:ps) = do
|
||||
@ -322,8 +322,8 @@ infixr 0 ==>
|
||||
genThreadId :: H.Gen D.ThreadId
|
||||
genThreadId = D.ThreadId <$> genId
|
||||
|
||||
genCRefId :: H.Gen D.CRefId
|
||||
genCRefId = D.CRefId <$> genId
|
||||
genIORefId :: H.Gen D.IORefId
|
||||
genIORefId = D.IORefId <$> genId
|
||||
|
||||
genMVarId :: H.Gen D.MVarId
|
||||
genMVarId = D.MVarId <$> genId
|
||||
@ -347,8 +347,8 @@ genFailure = HGen.element $
|
||||
, E.toException E.NonTermination
|
||||
]
|
||||
|
||||
genWBKey :: H.Gen (D.ThreadId, Maybe D.CRefId)
|
||||
genWBKey = (,) <$> genThreadId <*> HGen.maybe genCRefId
|
||||
genWBKey :: H.Gen (D.ThreadId, Maybe D.IORefId)
|
||||
genWBKey = (,) <$> genThreadId <*> HGen.maybe genIORefId
|
||||
|
||||
genThreadAction :: H.Gen D.ThreadAction
|
||||
genThreadAction = HGen.choice
|
||||
@ -368,14 +368,14 @@ genThreadAction = HGen.choice
|
||||
, D.TakeMVar <$> genMVarId <*> genSmallList genThreadId
|
||||
, D.BlockedTakeMVar <$> genMVarId
|
||||
, D.TryTakeMVar <$> genMVarId <*> HGen.bool <*> genSmallList genThreadId
|
||||
, D.NewCRef <$> genCRefId
|
||||
, D.ReadCRef <$> genCRefId
|
||||
, D.ReadCRefCas <$> genCRefId
|
||||
, D.ModCRef <$> genCRefId
|
||||
, D.ModCRefCas <$> genCRefId
|
||||
, D.WriteCRef <$> genCRefId
|
||||
, D.CasCRef <$> genCRefId <*> HGen.bool
|
||||
, D.CommitCRef <$> genThreadId <*> genCRefId
|
||||
, D.NewIORef <$> genIORefId
|
||||
, D.ReadIORef <$> genIORefId
|
||||
, D.ReadIORefCas <$> genIORefId
|
||||
, D.ModIORef <$> genIORefId
|
||||
, D.ModIORefCas <$> genIORefId
|
||||
, D.WriteIORef <$> genIORefId
|
||||
, D.CasIORef <$> genIORefId <*> HGen.bool
|
||||
, D.CommitIORef <$> genThreadId <*> genIORefId
|
||||
, D.STM <$> genSmallList genTAction <*> genSmallList genThreadId
|
||||
, D.BlockedSTM <$> genSmallList genTAction
|
||||
, pure D.Catching
|
||||
@ -420,21 +420,21 @@ genActionType = HGen.choice
|
||||
|
||||
genUnsynchronisedActionType :: H.Gen D.ActionType
|
||||
genUnsynchronisedActionType = HGen.choice
|
||||
[ D.UnsynchronisedRead <$> genCRefId
|
||||
, D.UnsynchronisedWrite <$> genCRefId
|
||||
[ D.UnsynchronisedRead <$> genIORefId
|
||||
, D.UnsynchronisedWrite <$> genIORefId
|
||||
, pure D.UnsynchronisedOther
|
||||
]
|
||||
|
||||
genPartiallySynchronisedActionType :: H.Gen D.ActionType
|
||||
genPartiallySynchronisedActionType = HGen.choice
|
||||
[ D.PartiallySynchronisedCommit <$> genCRefId
|
||||
, D.PartiallySynchronisedWrite <$> genCRefId
|
||||
, D.PartiallySynchronisedModify <$> genCRefId
|
||||
[ D.PartiallySynchronisedCommit <$> genIORefId
|
||||
, D.PartiallySynchronisedWrite <$> genIORefId
|
||||
, D.PartiallySynchronisedModify <$> genIORefId
|
||||
]
|
||||
|
||||
genSynchronisedActionType :: H.Gen D.ActionType
|
||||
genSynchronisedActionType = HGen.choice
|
||||
[ D.SynchronisedModify <$> genCRefId
|
||||
[ D.SynchronisedModify <$> genIORefId
|
||||
, D.SynchronisedRead <$> genMVarId
|
||||
, D.SynchronisedWrite <$> genMVarId
|
||||
, pure D.SynchronisedOther
|
||||
@ -442,7 +442,7 @@ genSynchronisedActionType = HGen.choice
|
||||
|
||||
genDepState :: H.Gen SCT.DepState
|
||||
genDepState = SCT.DepState
|
||||
<$> genSmallMap genCRefId HGen.bool
|
||||
<$> genSmallMap genIORefId HGen.bool
|
||||
<*> genSmallSet genMVarId
|
||||
<*> genSmallMap genThreadId genMaskingState
|
||||
|
||||
|
||||
@ -7,6 +7,21 @@ standard Haskell versioning scheme.
|
||||
.. _PVP: https://pvp.haskell.org/
|
||||
|
||||
|
||||
1.11.0.0 - IORefs (2018-07-01)
|
||||
------------------------------
|
||||
|
||||
* Git: :tag:`dejafu-1.11.0.0`
|
||||
* Hackage: :hackage:`dejafu-1.11.0.0`
|
||||
|
||||
Changed
|
||||
~~~~~~~
|
||||
|
||||
* (:issue:`274`) ``CRef`` is now ``IORef``: all functions, data
|
||||
constructors, and types have been renamed.
|
||||
|
||||
* The lower bound on :hackage:`concurrency` is 1.6.
|
||||
|
||||
|
||||
1.10.1.0 (2018-06-17)
|
||||
---------------------
|
||||
|
||||
|
||||
@ -102,7 +102,7 @@ There are a few knobs to tweak to control the behaviour of dejafu.
|
||||
The defaults should generally be good enough, but if not you have a
|
||||
few tricks available. The main two are: the 'Way', which controls how
|
||||
schedules are explored; and the 'MemType', which controls how reads
|
||||
and writes to @CRef@s behave; see "Test.DejaFu.Settings" for a
|
||||
and writes to @IORef@s behave; see "Test.DejaFu.Settings" for a
|
||||
complete listing.
|
||||
|
||||
-}
|
||||
@ -301,10 +301,10 @@ let example = do
|
||||
|
||||
>>> :{
|
||||
let relaxed = do
|
||||
r1 <- newCRef False
|
||||
r2 <- newCRef False
|
||||
x <- spawn $ writeCRef r1 True >> readCRef r2
|
||||
y <- spawn $ writeCRef r2 True >> readCRef r1
|
||||
r1 <- newIORef False
|
||||
r2 <- newIORef False
|
||||
x <- spawn $ writeIORef r1 True >> readIORef r2
|
||||
y <- spawn $ writeIORef r2 True >> readIORef r1
|
||||
(,) <$> readMVar x <*> readMVar y
|
||||
:}
|
||||
|
||||
@ -363,7 +363,7 @@ 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 @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> ConcT n a
|
||||
-- ^ The computation to test.
|
||||
-> n Bool
|
||||
@ -454,7 +454,7 @@ dejafuWay :: (MonadConc n, MonadIO n, Show b)
|
||||
=> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> String
|
||||
-- ^ The name of the test.
|
||||
-> ProPredicate a b
|
||||
@ -505,7 +505,7 @@ dejafuDiscard :: (MonadConc n, MonadIO n, Show b)
|
||||
-> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> String
|
||||
-- ^ The name of the test.
|
||||
-> ProPredicate a b
|
||||
@ -555,7 +555,7 @@ dejafusWay :: (MonadConc n, MonadIO n, Show b)
|
||||
=> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ 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
|
||||
@ -672,7 +672,7 @@ runTestWay :: MonadConc n
|
||||
=> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> ProPredicate a b
|
||||
-- ^ The predicate to check
|
||||
-> ConcT n a
|
||||
|
||||
@ -46,7 +46,7 @@ module Test.DejaFu.Conc
|
||||
, ThreadAction(..)
|
||||
, Lookahead(..)
|
||||
, MVarId
|
||||
, CRefId
|
||||
, IORefId
|
||||
, MaskingState(..)
|
||||
, showTrace
|
||||
, showFail
|
||||
@ -124,7 +124,7 @@ instance Ca.MonadMask (ConcT n) where
|
||||
|
||||
instance Monad n => C.MonadConc (ConcT n) where
|
||||
type MVar (ConcT n) = ModelMVar n
|
||||
type CRef (ConcT n) = ModelCRef n
|
||||
type IORef (ConcT n) = ModelIORef n
|
||||
type Ticket (ConcT n) = ModelTicket
|
||||
type STM (ConcT n) = ModelSTM n
|
||||
type ThreadId (ConcT n) = ThreadId
|
||||
@ -153,18 +153,18 @@ instance Monad n => C.MonadConc (ConcT n) where
|
||||
|
||||
-- ----------
|
||||
|
||||
newCRefN n a = toConc (ANewCRef n a)
|
||||
newIORefN n a = toConc (ANewIORef n a)
|
||||
|
||||
readCRef ref = toConc (AReadCRef ref)
|
||||
readForCAS ref = toConc (AReadCRefCas ref)
|
||||
readIORef ref = toConc (AReadIORef ref)
|
||||
readForCAS ref = toConc (AReadIORefCas ref)
|
||||
|
||||
peekTicket' _ = ticketVal
|
||||
|
||||
writeCRef ref a = toConc (\c -> AWriteCRef ref a (c ()))
|
||||
casCRef ref tick a = toConc (ACasCRef ref tick a)
|
||||
writeIORef ref a = toConc (\c -> AWriteIORef ref a (c ()))
|
||||
casIORef ref tick a = toConc (ACasIORef ref tick a)
|
||||
|
||||
atomicModifyCRef ref f = toConc (AModCRef ref f)
|
||||
modifyCRefCAS ref f = toConc (AModCRefCas ref f)
|
||||
atomicModifyIORef ref f = toConc (AModIORef ref f)
|
||||
modifyIORefCAS ref f = toConc (AModIORefCas ref f)
|
||||
|
||||
-- ----------
|
||||
|
||||
@ -218,7 +218,7 @@ runConcurrent :: C.MonadConc n
|
||||
-> n (Either Failure a, s, Trace)
|
||||
runConcurrent sched memtype s ma = do
|
||||
res <- runConcurrency False sched memtype s initialIdSource 2 (unC ma)
|
||||
out <- efromJust <$> C.readCRef (finalRef res)
|
||||
out <- efromJust <$> C.readIORef (finalRef res)
|
||||
pure ( out
|
||||
, cSchedState (finalContext res)
|
||||
, F.toList (finalTrace res)
|
||||
@ -284,7 +284,7 @@ dontCheck lb ma = toConc (ADontCheck lb (unC ma))
|
||||
--
|
||||
-- __Snapshotting @IO@:__ A snapshot captures entire state of your
|
||||
-- concurrent program: the state of every thread, the number of
|
||||
-- capabilities, the values of any @CRef@s, @MVar@s, and @TVar@s, and
|
||||
-- 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
|
||||
@ -311,7 +311,7 @@ dontCheck lb ma = toConc (ADontCheck lb (unC ma))
|
||||
-- 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 . readCRef@ and @liftIO . writeIORef@ here), or reset
|
||||
-- of @liftIO . readIORef@ and @liftIO . writeIORef@ here), or reset
|
||||
-- the state to a known value. Both of these approaches will work:
|
||||
--
|
||||
-- @
|
||||
@ -349,7 +349,7 @@ runForDCSnapshot :: C.MonadConc n
|
||||
-> n (Maybe (Either Failure (DCSnapshot n a), Trace))
|
||||
runForDCSnapshot ma = do
|
||||
res <- runConcurrency True roundRobinSchedNP SequentialConsistency () initialIdSource 2 (unC ma)
|
||||
out <- C.readCRef (finalRef res)
|
||||
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))
|
||||
@ -374,7 +374,7 @@ runWithDCSnapshot sched memtype s snapshot = do
|
||||
let restore = dcsRestore snapshot
|
||||
let ref = dcsRef snapshot
|
||||
res <- runConcurrencyWithSnapshot sched memtype context restore ref
|
||||
out <- efromJust <$> C.readCRef (finalRef res)
|
||||
out <- efromJust <$> C.readIORef (finalRef res)
|
||||
pure ( out
|
||||
, cSchedState (finalContext res)
|
||||
, F.toList (finalTrace res)
|
||||
|
||||
@ -49,7 +49,7 @@ type SeqTrace
|
||||
-- | The result of running a concurrent program.
|
||||
data CResult n g a = CResult
|
||||
{ finalContext :: Context n g
|
||||
, finalRef :: C.CRef n (Maybe (Either Failure a))
|
||||
, finalRef :: C.IORef n (Maybe (Either Failure a))
|
||||
, finalRestore :: Maybe (Threads n -> n ())
|
||||
-- ^ Meaningless if this result doesn't come from a snapshotting
|
||||
-- execution.
|
||||
@ -66,8 +66,8 @@ data DCSnapshot n a = DCSnapshot
|
||||
-- ^ The execution context. The scheduler state is ignored when
|
||||
-- restoring.
|
||||
, dcsRestore :: Threads n -> n ()
|
||||
-- ^ Action to restore CRef, MVar, and TVar values.
|
||||
, dcsRef :: C.CRef n (Maybe (Either Failure a))
|
||||
-- ^ Action to restore IORef, MVar, and TVar values.
|
||||
, dcsRef :: C.IORef n (Maybe (Either Failure a))
|
||||
-- ^ Reference where the result will be written.
|
||||
}
|
||||
|
||||
@ -118,7 +118,7 @@ runConcurrencyWithSnapshot :: (C.MonadConc n, HasCallStack)
|
||||
-> MemType
|
||||
-> Context n g
|
||||
-> (Threads n -> n ())
|
||||
-> C.CRef n (Maybe (Either Failure a))
|
||||
-> C.IORef n (Maybe (Either Failure a))
|
||||
-> n (CResult n g a)
|
||||
runConcurrencyWithSnapshot sched memtype ctx restore ref = do
|
||||
let boundThreads = M.filter (isJust . _bound) (cThreads ctx)
|
||||
@ -151,13 +151,13 @@ runThreads :: (C.MonadConc n, HasCallStack)
|
||||
=> Bool
|
||||
-> Scheduler g
|
||||
-> MemType
|
||||
-> C.CRef n (Maybe (Either Failure a))
|
||||
-> C.IORef n (Maybe (Either Failure 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.writeCRef ref (Just $ Left reason)
|
||||
C.writeIORef ref (Just $ Left reason)
|
||||
stop finalR finalT finalD finalC
|
||||
|
||||
-- just terminate; 'ref' must have been written to before calling
|
||||
@ -367,11 +367,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.newCRef Nothing
|
||||
ref <- C.newIORef Nothing
|
||||
let mvar = ModelMVar newmvid ref
|
||||
pure ( Succeeded ctx { cThreads = goto (c mvar) tid cThreads, cIdSource = idSource' }
|
||||
, Single (NewMVar newmvid)
|
||||
, const (C.writeCRef ref Nothing)
|
||||
, const (C.writeIORef ref Nothing)
|
||||
)
|
||||
|
||||
-- put a value into a @MVar@, blocking the thread until it's empty.
|
||||
@ -424,85 +424,85 @@ stepThread _ _ _ _ tid (ATryTakeMVar mvar@ModelMVar{..} c) = synchronised $ \ctx
|
||||
, const effect
|
||||
)
|
||||
|
||||
-- create a new @CRef@, using the next 'CRefId'.
|
||||
stepThread _ _ _ _ tid (ANewCRef n a c) = \ctx@Context{..} -> do
|
||||
let (idSource', newcrid) = nextCRId n cIdSource
|
||||
-- create a new @IORef@, using the next 'IORefId'.
|
||||
stepThread _ _ _ _ tid (ANewIORef n a c) = \ctx@Context{..} -> do
|
||||
let (idSource', newiorid) = nextIORId n cIdSource
|
||||
let val = (M.empty, 0, a)
|
||||
ref <- C.newCRef val
|
||||
let cref = ModelCRef newcrid ref
|
||||
pure ( Succeeded ctx { cThreads = goto (c cref) tid cThreads, cIdSource = idSource' }
|
||||
, Single (NewCRef newcrid)
|
||||
, const (C.writeCRef ref val)
|
||||
ioref <- C.newIORef val
|
||||
let ref = ModelIORef newiorid ioref
|
||||
pure ( Succeeded ctx { cThreads = goto (c ref) tid cThreads, cIdSource = idSource' }
|
||||
, Single (NewIORef newiorid)
|
||||
, const (C.writeIORef ioref val)
|
||||
)
|
||||
|
||||
-- read from a @CRef@.
|
||||
stepThread _ _ _ _ tid (AReadCRef cref@ModelCRef{..} c) = \ctx@Context{..} -> do
|
||||
val <- readCRef cref tid
|
||||
-- read from a @IORef@.
|
||||
stepThread _ _ _ _ tid (AReadIORef ref@ModelIORef{..} c) = \ctx@Context{..} -> do
|
||||
val <- readIORef ref tid
|
||||
pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads }
|
||||
, Single (ReadCRef crefId)
|
||||
, Single (ReadIORef iorefId)
|
||||
, const (pure ())
|
||||
)
|
||||
|
||||
-- read from a @CRef@ for future compare-and-swap operations.
|
||||
stepThread _ _ _ _ tid (AReadCRefCas cref@ModelCRef{..} c) = \ctx@Context{..} -> do
|
||||
tick <- readForTicket cref tid
|
||||
-- read from a @IORef@ for future compare-and-swap operations.
|
||||
stepThread _ _ _ _ tid (AReadIORefCas ref@ModelIORef{..} c) = \ctx@Context{..} -> do
|
||||
tick <- readForTicket ref tid
|
||||
pure ( Succeeded ctx { cThreads = goto (c tick) tid cThreads }
|
||||
, Single (ReadCRefCas crefId)
|
||||
, Single (ReadIORefCas iorefId)
|
||||
, const (pure ())
|
||||
)
|
||||
|
||||
-- modify a @CRef@.
|
||||
stepThread _ _ _ _ tid (AModCRef cref@ModelCRef{..} f c) = synchronised $ \ctx@Context{..} -> do
|
||||
(new, val) <- f <$> readCRef cref tid
|
||||
effect <- writeImmediate cref new
|
||||
-- modify a @IORef@.
|
||||
stepThread _ _ _ _ tid (AModIORef ref@ModelIORef{..} f c) = synchronised $ \ctx@Context{..} -> do
|
||||
(new, val) <- f <$> readIORef ref tid
|
||||
effect <- writeImmediate ref new
|
||||
pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads }
|
||||
, Single (ModCRef crefId)
|
||||
, Single (ModIORef iorefId)
|
||||
, const effect
|
||||
)
|
||||
|
||||
-- modify a @CRef@ using a compare-and-swap.
|
||||
stepThread _ _ _ _ tid (AModCRefCas cref@ModelCRef{..} f c) = synchronised $ \ctx@Context{..} -> do
|
||||
tick@(ModelTicket _ _ old) <- readForTicket cref tid
|
||||
-- modify a @IORef@ using a compare-and-swap.
|
||||
stepThread _ _ _ _ tid (AModIORefCas ref@ModelIORef{..} f c) = synchronised $ \ctx@Context{..} -> do
|
||||
tick@(ModelTicket _ _ old) <- readForTicket ref tid
|
||||
let (new, val) = f old
|
||||
(_, _, effect) <- casCRef cref tid tick new
|
||||
(_, _, effect) <- casIORef ref tid tick new
|
||||
pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads }
|
||||
, Single (ModCRefCas crefId)
|
||||
, Single (ModIORefCas iorefId)
|
||||
, const effect
|
||||
)
|
||||
|
||||
-- write to a @CRef@ without synchronising.
|
||||
stepThread _ _ _ memtype tid (AWriteCRef cref@ModelCRef{..} a c) = \ctx@Context{..} -> case memtype of
|
||||
-- write to a @IORef@ without synchronising.
|
||||
stepThread _ _ _ memtype tid (AWriteIORef ref@ModelIORef{..} a c) = \ctx@Context{..} -> case memtype of
|
||||
-- write immediately.
|
||||
SequentialConsistency -> do
|
||||
effect <- writeImmediate cref a
|
||||
effect <- writeImmediate ref a
|
||||
pure ( Succeeded ctx { cThreads = goto c tid cThreads }
|
||||
, Single (WriteCRef crefId)
|
||||
, Single (WriteIORef iorefId)
|
||||
, const effect
|
||||
)
|
||||
-- add to buffer using thread id.
|
||||
TotalStoreOrder -> do
|
||||
wb' <- bufferWrite cWriteBuf (tid, Nothing) cref a
|
||||
wb' <- bufferWrite cWriteBuf (tid, Nothing) ref a
|
||||
pure ( Succeeded ctx { cThreads = goto c tid cThreads, cWriteBuf = wb' }
|
||||
, Single (WriteCRef crefId)
|
||||
, Single (WriteIORef iorefId)
|
||||
, const (pure ())
|
||||
)
|
||||
-- add to buffer using both thread id and cref id
|
||||
-- add to buffer using both thread id and IORef id
|
||||
PartialStoreOrder -> do
|
||||
wb' <- bufferWrite cWriteBuf (tid, Just crefId) cref a
|
||||
wb' <- bufferWrite cWriteBuf (tid, Just iorefId) ref a
|
||||
pure ( Succeeded ctx { cThreads = goto c tid cThreads, cWriteBuf = wb' }
|
||||
, Single (WriteCRef crefId)
|
||||
, Single (WriteIORef iorefId)
|
||||
, const (pure ())
|
||||
)
|
||||
|
||||
-- perform a compare-and-swap on a @CRef@.
|
||||
stepThread _ _ _ _ tid (ACasCRef cref@ModelCRef{..} tick a c) = synchronised $ \ctx@Context{..} -> do
|
||||
(suc, tick', effect) <- casCRef cref tid tick a
|
||||
-- perform a compare-and-swap on a @IORef@.
|
||||
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 (CasCRef crefId suc)
|
||||
, Single (CasIORef iorefId suc)
|
||||
, const effect
|
||||
)
|
||||
|
||||
-- commit a @CRef@ write
|
||||
-- commit a @IORef@ write
|
||||
stepThread _ _ _ memtype _ (ACommit t c) = \ctx@Context{..} -> do
|
||||
wb' <- case memtype of
|
||||
-- shouldn't ever get here
|
||||
@ -511,11 +511,11 @@ stepThread _ _ _ memtype _ (ACommit t c) = \ctx@Context{..} -> do
|
||||
-- commit using the thread id.
|
||||
TotalStoreOrder ->
|
||||
commitWrite cWriteBuf (t, Nothing)
|
||||
-- commit using the cref id.
|
||||
-- commit using the IORef id.
|
||||
PartialStoreOrder ->
|
||||
commitWrite cWriteBuf (t, Just c)
|
||||
pure ( Succeeded ctx { cWriteBuf = wb' }
|
||||
, Single (CommitCRef t c)
|
||||
, Single (CommitIORef t c)
|
||||
, const (pure ())
|
||||
)
|
||||
|
||||
@ -634,7 +634,7 @@ stepThread forSnapshot _ sched memtype tid (ASub ma c) = \ctx ->
|
||||
| M.size (cThreads ctx) > 1 -> pure (Failed IllegalSubconcurrency, Single Subconcurrency, const (pure ()))
|
||||
| otherwise -> do
|
||||
res <- runConcurrency False sched memtype (cSchedState ctx) (cIdSource ctx) (cCaps ctx) ma
|
||||
out <- efromJust <$> C.readCRef (finalRef res)
|
||||
out <- efromJust <$> C.readIORef (finalRef res)
|
||||
pure ( Succeeded ctx
|
||||
{ cThreads = goto (AStopSub (c out)) tid (cThreads ctx)
|
||||
, cIdSource = cIdSource (finalContext res)
|
||||
@ -662,7 +662,7 @@ stepThread forSnapshot isFirst _ _ tid (ADontCheck lb ma c) = \ctx ->
|
||||
threads' <- kill tid (cThreads ctx)
|
||||
let dcCtx = ctx { cThreads = threads', cSchedState = lb }
|
||||
res <- runConcurrency' forSnapshot dcSched SequentialConsistency dcCtx ma
|
||||
out <- efromJust <$> C.readCRef (finalRef res)
|
||||
out <- efromJust <$> C.readIORef (finalRef res)
|
||||
case out of
|
||||
Right a -> do
|
||||
let threads'' = launch' Unmasked tid (const (c a)) (cThreads (finalContext res))
|
||||
|
||||
@ -56,22 +56,22 @@ instance Fail.MonadFail (ModelConc n) where
|
||||
-- @Maybe@ value.
|
||||
data ModelMVar n a = ModelMVar
|
||||
{ mvarId :: MVarId
|
||||
, mvarRef :: C.CRef n (Maybe a)
|
||||
, mvarRef :: C.IORef n (Maybe a)
|
||||
}
|
||||
|
||||
-- | A @CRef@ is modelled as a unique ID and a reference holding
|
||||
-- | A @IORef@ is modelled as a unique ID and a reference holding
|
||||
-- thread-local values, the number of commits, and the most recent
|
||||
-- committed value.
|
||||
data ModelCRef n a = ModelCRef
|
||||
{ crefId :: CRefId
|
||||
, crefRef :: C.CRef n (Map ThreadId a, Integer, a)
|
||||
data ModelIORef n a = ModelIORef
|
||||
{ iorefId :: IORefId
|
||||
, iorefRef :: C.IORef n (Map ThreadId a, Integer, a)
|
||||
}
|
||||
|
||||
-- | A @Ticket@ is modelled as the ID of the @ModelCRef@ it came from,
|
||||
-- the commits to the @ModelCRef@ at the time it was produced, and the
|
||||
-- | A @Ticket@ is modelled as the ID of the @ModelIORef@ it came from,
|
||||
-- the commits to the @ModelIORef@ at the time it was produced, and the
|
||||
-- value observed.
|
||||
data ModelTicket a = ModelTicket
|
||||
{ ticketCRef :: CRefId
|
||||
{ ticketIORef :: IORefId
|
||||
, ticketWrites :: Integer
|
||||
, ticketVal :: a
|
||||
}
|
||||
@ -100,13 +100,13 @@ data Action n =
|
||||
| forall a. ATakeMVar (ModelMVar n a) (a -> Action n)
|
||||
| forall a. ATryTakeMVar (ModelMVar n a) (Maybe a -> Action n)
|
||||
|
||||
| forall a. ANewCRef String a (ModelCRef n a -> Action n)
|
||||
| forall a. AReadCRef (ModelCRef n a) (a -> Action n)
|
||||
| forall a. AReadCRefCas (ModelCRef n a) (ModelTicket a -> Action n)
|
||||
| forall a b. AModCRef (ModelCRef n a) (a -> (a, b)) (b -> Action n)
|
||||
| forall a b. AModCRefCas (ModelCRef n a) (a -> (a, b)) (b -> Action n)
|
||||
| forall a. AWriteCRef (ModelCRef n a) a (Action n)
|
||||
| forall a. ACasCRef (ModelCRef n a) (ModelTicket a) a ((Bool, ModelTicket a) -> Action n)
|
||||
| forall a. ANewIORef String a (ModelIORef n a -> Action n)
|
||||
| forall a. AReadIORef (ModelIORef n a) (a -> Action n)
|
||||
| forall a. AReadIORefCas (ModelIORef n a) (ModelTicket a -> Action n)
|
||||
| forall a b. AModIORef (ModelIORef n a) (a -> (a, b)) (b -> Action n)
|
||||
| forall a b. AModIORefCas (ModelIORef n a) (a -> (a, b)) (b -> Action n)
|
||||
| forall a. AWriteIORef (ModelIORef n a) a (Action n)
|
||||
| forall a. ACasIORef (ModelIORef n a) (ModelTicket a) a ((Bool, ModelTicket a) -> Action n)
|
||||
|
||||
| forall e. Exception e => AThrow e
|
||||
| forall e. Exception e => AThrowTo ThreadId e (Action n)
|
||||
@ -120,7 +120,7 @@ data Action n =
|
||||
| AYield (Action n)
|
||||
| ADelay Int (Action n)
|
||||
| AReturn (Action n)
|
||||
| ACommit ThreadId CRefId
|
||||
| ACommit ThreadId IORefId
|
||||
| AStop (n ())
|
||||
|
||||
| forall a. ASub (ModelConc n a) (Either Failure a -> Action n)
|
||||
@ -145,14 +145,14 @@ lookahead (AReadMVar (ModelMVar m _) _) = WillReadMVar m
|
||||
lookahead (ATryReadMVar (ModelMVar m _) _) = WillTryReadMVar m
|
||||
lookahead (ATakeMVar (ModelMVar m _) _) = WillTakeMVar m
|
||||
lookahead (ATryTakeMVar (ModelMVar m _) _) = WillTryTakeMVar m
|
||||
lookahead (ANewCRef _ _ _) = WillNewCRef
|
||||
lookahead (AReadCRef (ModelCRef r _) _) = WillReadCRef r
|
||||
lookahead (AReadCRefCas (ModelCRef r _) _) = WillReadCRefCas r
|
||||
lookahead (AModCRef (ModelCRef r _) _ _) = WillModCRef r
|
||||
lookahead (AModCRefCas (ModelCRef r _) _ _) = WillModCRefCas r
|
||||
lookahead (AWriteCRef (ModelCRef r _) _ _) = WillWriteCRef r
|
||||
lookahead (ACasCRef (ModelCRef r _) _ _ _) = WillCasCRef r
|
||||
lookahead (ACommit t c) = WillCommitCRef t c
|
||||
lookahead (ANewIORef _ _ _) = WillNewIORef
|
||||
lookahead (AReadIORef (ModelIORef r _) _) = WillReadIORef r
|
||||
lookahead (AReadIORefCas (ModelIORef r _) _) = WillReadIORefCas r
|
||||
lookahead (AModIORef (ModelIORef r _) _ _) = WillModIORef r
|
||||
lookahead (AModIORefCas (ModelIORef r _) _ _) = WillModIORefCas r
|
||||
lookahead (AWriteIORef (ModelIORef r _) _ _) = WillWriteIORef r
|
||||
lookahead (ACasIORef (ModelIORef r _) _ _ _) = WillCasIORef r
|
||||
lookahead (ACommit t c) = WillCommitIORef t c
|
||||
lookahead (AAtom _ _) = WillSTM
|
||||
lookahead (AThrow _) = WillThrow
|
||||
lookahead (AThrowTo tid _ _) = WillThrowTo tid
|
||||
|
||||
@ -12,14 +12,14 @@
|
||||
-- Stability : experimental
|
||||
-- Portability : BangPatterns, GADTs, FlexibleContexts, LambdaCase, RecordWildCards
|
||||
--
|
||||
-- Operations over @CRef@s and @MVar@s. This module is NOT considered
|
||||
-- Operations over @IORef@s and @MVar@s. This module is NOT considered
|
||||
-- to form part of the public interface of this library.
|
||||
--
|
||||
-- Relaxed memory operations over @CRef@s are implemented with an
|
||||
-- Relaxed memory operations over @IORef@s are implemented with an
|
||||
-- explicit write buffer: one per thread for TSO, and one per
|
||||
-- thread/variable combination for PSO. Unsynchronised writes append
|
||||
-- to this buffer, and periodically separate threads commit from these
|
||||
-- buffers to the \"actual\" @CRef@.
|
||||
-- buffers to the \"actual\" @IORef@.
|
||||
--
|
||||
-- This model comes from /Dynamic Partial Order Reduction for Relaxed
|
||||
-- Memory Models/, N. Zhang, M. Kusano, and C. Wang (2015).
|
||||
@ -40,93 +40,93 @@ import Test.DejaFu.Internal
|
||||
import Test.DejaFu.Types
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- * Manipulating @CRef@s
|
||||
-- * Manipulating @IORef@s
|
||||
|
||||
-- | In non-sequentially-consistent memory models, non-synchronised
|
||||
-- writes get buffered.
|
||||
--
|
||||
-- The @CRefId@ parameter is only used under PSO. Under TSO each
|
||||
-- The @IORefId@ parameter is only used under PSO. Under TSO each
|
||||
-- thread has a single buffer.
|
||||
newtype WriteBuffer n = WriteBuffer
|
||||
{ buffer :: Map (ThreadId, Maybe CRefId) (Seq (BufferedWrite n)) }
|
||||
{ buffer :: Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n)) }
|
||||
|
||||
-- | A buffered write is a reference to the variable, and the value to
|
||||
-- write. Universally quantified over the value type so that the only
|
||||
-- thing which can be done with it is to write it to the reference.
|
||||
data BufferedWrite n where
|
||||
BufferedWrite :: ThreadId -> ModelCRef n a -> a -> BufferedWrite n
|
||||
BufferedWrite :: ThreadId -> ModelIORef n a -> a -> BufferedWrite n
|
||||
|
||||
-- | An empty write buffer.
|
||||
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 CRefId) -> ModelCRef n a -> a -> n (WriteBuffer n)
|
||||
bufferWrite (WriteBuffer wb) k@(tid, _) cref@ModelCRef{..} new = do
|
||||
bufferWrite :: C.MonadConc 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 cref new
|
||||
let write = singleton $ BufferedWrite tid ref new
|
||||
let buffer' = M.insertWith (flip (><)) k write wb
|
||||
|
||||
-- Write the thread-local value to the @CRef@'s update map.
|
||||
(locals, count, def) <- C.readCRef crefRef
|
||||
C.writeCRef crefRef (M.insert tid new locals, count, def)
|
||||
-- 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)
|
||||
|
||||
pure (WriteBuffer buffer')
|
||||
|
||||
-- | Commit the write at the head of a buffer.
|
||||
commitWrite :: C.MonadConc n => WriteBuffer n -> (ThreadId, Maybe CRefId) -> n (WriteBuffer n)
|
||||
commitWrite :: C.MonadConc n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> n (WriteBuffer n)
|
||||
commitWrite w@(WriteBuffer wb) k = case maybe EmptyL viewl $ M.lookup k wb of
|
||||
BufferedWrite _ cref a :< rest -> do
|
||||
_ <- writeImmediate cref a
|
||||
BufferedWrite _ ref a :< rest -> do
|
||||
_ <- writeImmediate ref a
|
||||
pure . WriteBuffer $ M.insert k rest wb
|
||||
EmptyL -> pure w
|
||||
|
||||
-- | Read from a @CRef@, returning a newer thread-local non-committed
|
||||
-- | Read from a @IORef@, returning a newer thread-local non-committed
|
||||
-- write if there is one.
|
||||
readCRef :: C.MonadConc n => ModelCRef n a -> ThreadId -> n a
|
||||
readCRef cref tid = do
|
||||
(val, _) <- readCRefPrim cref tid
|
||||
readIORef :: C.MonadConc n => ModelIORef n a -> ThreadId -> n a
|
||||
readIORef ref tid = do
|
||||
(val, _) <- readIORefPrim ref tid
|
||||
pure val
|
||||
|
||||
-- | Read from a @CRef@, returning a @Ticket@ representing the current
|
||||
-- | Read from a @IORef@, returning a @Ticket@ representing the current
|
||||
-- view of the thread.
|
||||
readForTicket :: C.MonadConc n => ModelCRef n a -> ThreadId -> n (ModelTicket a)
|
||||
readForTicket cref@ModelCRef{..} tid = do
|
||||
(val, count) <- readCRefPrim cref tid
|
||||
pure (ModelTicket crefId count val)
|
||||
readForTicket :: C.MonadConc 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 @CRef@ if the ticket is still
|
||||
-- | Perform a compare-and-swap on a @IORef@ if the ticket is still
|
||||
-- valid. This is strict in the \"new\" value argument.
|
||||
casCRef :: C.MonadConc n => ModelCRef n a -> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ())
|
||||
casCRef cref tid (ModelTicket _ cc _) !new = do
|
||||
tick'@(ModelTicket _ cc' _) <- readForTicket cref tid
|
||||
casIORef :: C.MonadConc 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
|
||||
|
||||
if cc == cc'
|
||||
then do
|
||||
effect <- writeImmediate cref new
|
||||
tick'' <- readForTicket cref tid
|
||||
effect <- writeImmediate ref new
|
||||
tick'' <- readForTicket ref tid
|
||||
pure (True, tick'', effect)
|
||||
else pure (False, tick', pure ())
|
||||
|
||||
-- | Read the local state of a @CRef@.
|
||||
readCRefPrim :: C.MonadConc n => ModelCRef n a -> ThreadId -> n (a, Integer)
|
||||
readCRefPrim ModelCRef{..} tid = do
|
||||
(vals, count, def) <- C.readCRef crefRef
|
||||
-- | Read the local state of a @IORef@.
|
||||
readIORefPrim :: C.MonadConc n => ModelIORef n a -> ThreadId -> n (a, Integer)
|
||||
readIORefPrim ModelIORef{..} tid = do
|
||||
(vals, count, def) <- C.readIORef iorefRef
|
||||
pure (M.findWithDefault def tid vals, count)
|
||||
|
||||
-- | Write and commit to a @CRef@ immediately, clearing the update map
|
||||
-- | Write and commit to a @IORef@ immediately, clearing the update map
|
||||
-- and incrementing the write count.
|
||||
writeImmediate :: C.MonadConc n => ModelCRef n a -> a -> n (n ())
|
||||
writeImmediate ModelCRef{..} a = do
|
||||
(_, count, _) <- C.readCRef crefRef
|
||||
let effect = C.writeCRef crefRef (M.empty, count + 1, a)
|
||||
writeImmediate :: C.MonadConc 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)
|
||||
effect
|
||||
pure effect
|
||||
|
||||
-- | Flush all writes in the buffer.
|
||||
writeBarrier :: C.MonadConc n => WriteBuffer n -> n ()
|
||||
writeBarrier (WriteBuffer wb) = mapM_ flush $ M.elems wb where
|
||||
flush = mapM_ $ \(BufferedWrite _ cref a) -> writeImmediate cref a
|
||||
flush = mapM_ $ \(BufferedWrite _ ref a) -> writeImmediate ref a
|
||||
|
||||
-- | Add phantom threads to the thread list to commit pending writes.
|
||||
addCommitThreads :: WriteBuffer n -> Threads n -> Threads n
|
||||
@ -135,13 +135,13 @@ addCommitThreads (WriteBuffer wb) ts = ts <> M.fromList phantoms where
|
||||
| (k, b) <- M.toList wb
|
||||
, c <- maybeToList (go $ viewl b)
|
||||
]
|
||||
go (BufferedWrite tid ModelCRef{..} _ :< _) = Just $ ACommit tid crefId
|
||||
go (BufferedWrite tid ModelIORef{..} _ :< _) = Just $ ACommit tid iorefId
|
||||
go EmptyL = Nothing
|
||||
|
||||
-- | The ID of a commit thread.
|
||||
commitThreadId :: ThreadId -> Maybe CRefId -> ThreadId
|
||||
commitThreadId :: ThreadId -> Maybe IORefId -> ThreadId
|
||||
commitThreadId (ThreadId (Id _ t)) = ThreadId . Id Nothing . negate . go where
|
||||
go (Just (CRefId (Id _ c))) = t + 1 + c * 10000
|
||||
go (Just (IORefId (Id _ c))) = t + 1 + c * 10000
|
||||
go Nothing = t + 1
|
||||
|
||||
-- | Remove phantom threads.
|
||||
@ -220,7 +220,7 @@ mutMVar :: C.MonadConc n
|
||||
-> ThreadId
|
||||
-> Threads n
|
||||
-> n (Bool, Threads n, [ThreadId], n ())
|
||||
mutMVar blocking ModelMVar{..} a c threadid threads = C.readCRef mvarRef >>= \case
|
||||
mutMVar blocking ModelMVar{..} a c threadid threads = C.readIORef mvarRef >>= \case
|
||||
Just _ -> case blocking of
|
||||
Blocking ->
|
||||
let threads' = block (OnMVarEmpty mvarId) threadid threads
|
||||
@ -228,7 +228,7 @@ mutMVar blocking ModelMVar{..} a c threadid threads = C.readCRef mvarRef >>= \ca
|
||||
NonBlocking ->
|
||||
pure (False, goto (c False) threadid threads, [], pure ())
|
||||
Nothing -> do
|
||||
let effect = C.writeCRef mvarRef $ Just a
|
||||
let effect = C.writeIORef mvarRef $ Just a
|
||||
let (threads', woken) = wake (OnMVarFull mvarId) threads
|
||||
effect
|
||||
pure (True, goto (c True) threadid threads', woken, effect)
|
||||
@ -243,10 +243,10 @@ seeMVar :: C.MonadConc n
|
||||
-> ThreadId
|
||||
-> Threads n
|
||||
-> n (Bool, Threads n, [ThreadId], n ())
|
||||
seeMVar emptying blocking ModelMVar{..} c threadid threads = C.readCRef mvarRef >>= \case
|
||||
seeMVar emptying blocking ModelMVar{..} c threadid threads = C.readIORef mvarRef >>= \case
|
||||
val@(Just _) -> do
|
||||
let effect = case emptying of
|
||||
Emptying -> C.writeCRef mvarRef Nothing
|
||||
Emptying -> C.writeIORef mvarRef Nothing
|
||||
NonEmptying -> pure ()
|
||||
let (threads', woken) = wake (OnMVarEmpty mvarId) threads
|
||||
effect
|
||||
|
||||
@ -100,7 +100,7 @@ data STMAction n
|
||||
-- value.
|
||||
data ModelTVar n a = ModelTVar
|
||||
{ tvarId :: TVarId
|
||||
, tvarRef :: C.CRef n a
|
||||
, tvarRef :: C.IORef n a
|
||||
}
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
@ -145,7 +145,7 @@ doTransaction :: C.MonadConc n
|
||||
doTransaction ma idsource = do
|
||||
(c, ref) <- runRefCont SStop (Just . Right) (runModelSTM ma)
|
||||
(idsource', undo, readen, written, trace) <- go ref c (pure ()) idsource [] [] []
|
||||
res <- C.readCRef ref
|
||||
res <- C.readIORef ref
|
||||
|
||||
case res of
|
||||
Just (Right val) -> pure (Success (nub readen) (nub written) val, undo, idsource', reverse trace)
|
||||
@ -166,10 +166,10 @@ doTransaction ma idsource = do
|
||||
case tact of
|
||||
TStop -> pure (newIDSource, newUndo, newReaden, newWritten, TStop:newSofar)
|
||||
TRetry -> do
|
||||
C.writeCRef ref Nothing
|
||||
C.writeIORef ref Nothing
|
||||
pure (newIDSource, newUndo, newReaden, newWritten, TRetry:newSofar)
|
||||
TThrow -> do
|
||||
C.writeCRef ref (Just . Left $ case act of SThrow e -> toException e; _ -> undefined)
|
||||
C.writeIORef 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
|
||||
|
||||
@ -199,17 +199,17 @@ stepTrans act idsource = case act of
|
||||
Nothing -> pure (SThrow exc, nothing, idsource, [], [], TCatch trace Nothing))
|
||||
|
||||
stepRead ModelTVar{..} c = do
|
||||
val <- C.readCRef tvarRef
|
||||
val <- C.readIORef tvarRef
|
||||
pure (c val, nothing, idsource, [tvarId], [], TRead tvarId)
|
||||
|
||||
stepWrite ModelTVar{..} a c = do
|
||||
old <- C.readCRef tvarRef
|
||||
C.writeCRef tvarRef a
|
||||
pure (c, C.writeCRef tvarRef old, idsource, [], [tvarId], TWrite tvarId)
|
||||
old <- C.readIORef tvarRef
|
||||
C.writeIORef tvarRef a
|
||||
pure (c, C.writeIORef tvarRef old, idsource, [], [tvarId], TWrite tvarId)
|
||||
|
||||
stepNew n a c = do
|
||||
let (idsource', tvid) = nextTVId n idsource
|
||||
ref <- C.newCRef a
|
||||
ref <- C.newIORef a
|
||||
let tvar = ModelTVar tvid ref
|
||||
pure (c tvar, nothing, idsource', [], [tvid], TNew tvid)
|
||||
|
||||
|
||||
@ -65,17 +65,17 @@ instance Show Way where
|
||||
-- | The number of ID parameters was getting a bit unwieldy, so this
|
||||
-- hides them all away.
|
||||
data IdSource = IdSource
|
||||
{ _crids :: (Int, [String])
|
||||
{ _iorids :: (Int, [String])
|
||||
, _mvids :: (Int, [String])
|
||||
, _tvids :: (Int, [String])
|
||||
, _tids :: (Int, [String])
|
||||
} deriving (Eq, Ord, Show, Generic, NFData)
|
||||
|
||||
-- | Get the next free 'CRefId'.
|
||||
nextCRId :: String -> IdSource -> (IdSource, CRefId)
|
||||
nextCRId name idsource =
|
||||
let (crid, crids') = nextId name (_crids idsource)
|
||||
in (idsource { _crids = crids' }, CRefId crid)
|
||||
-- | Get the next free 'IORefId'.
|
||||
nextIORId :: String -> IdSource -> (IdSource, IORefId)
|
||||
nextIORId name idsource =
|
||||
let (iorid, iorids') = nextId name (_iorids idsource)
|
||||
in (idsource { _iorids = iorids' }, IORefId iorid)
|
||||
|
||||
-- | Get the next free 'MVarId'.
|
||||
nextMVId :: String -> IdSource -> (IdSource, MVarId)
|
||||
@ -176,14 +176,14 @@ rewind (TryReadMVar c _) = WillTryReadMVar c
|
||||
rewind (TakeMVar c _) = WillTakeMVar c
|
||||
rewind (BlockedTakeMVar c) = WillTakeMVar c
|
||||
rewind (TryTakeMVar c _ _) = WillTryTakeMVar c
|
||||
rewind (NewCRef _) = WillNewCRef
|
||||
rewind (ReadCRef c) = WillReadCRef c
|
||||
rewind (ReadCRefCas c) = WillReadCRefCas c
|
||||
rewind (ModCRef c) = WillModCRef c
|
||||
rewind (ModCRefCas c) = WillModCRefCas c
|
||||
rewind (WriteCRef c) = WillWriteCRef c
|
||||
rewind (CasCRef c _) = WillCasCRef c
|
||||
rewind (CommitCRef t c) = WillCommitCRef t c
|
||||
rewind (NewIORef _) = WillNewIORef
|
||||
rewind (ReadIORef c) = WillReadIORef c
|
||||
rewind (ReadIORefCas c) = WillReadIORefCas c
|
||||
rewind (ModIORef c) = WillModIORef c
|
||||
rewind (ModIORefCas c) = WillModIORefCas c
|
||||
rewind (WriteIORef c) = WillWriteIORef c
|
||||
rewind (CasIORef c _) = WillCasIORef c
|
||||
rewind (CommitIORef t c) = WillCommitIORef t c
|
||||
rewind (STM _ _) = WillSTM
|
||||
rewind (BlockedSTM _) = WillSTM
|
||||
rewind Catching = WillCatching
|
||||
@ -224,21 +224,21 @@ willRelease _ = False
|
||||
|
||||
-- | A simplified view of the possible actions a thread can perform.
|
||||
data ActionType =
|
||||
UnsynchronisedRead CRefId
|
||||
-- ^ A 'readCRef' or a 'readForCAS'.
|
||||
| UnsynchronisedWrite CRefId
|
||||
-- ^ A 'writeCRef'.
|
||||
UnsynchronisedRead IORefId
|
||||
-- ^ A 'readIORef' or a 'readForCAS'.
|
||||
| UnsynchronisedWrite IORefId
|
||||
-- ^ A 'writeIORef'.
|
||||
| UnsynchronisedOther
|
||||
-- ^ Some other action which doesn't require cross-thread
|
||||
-- communication.
|
||||
| PartiallySynchronisedCommit CRefId
|
||||
| PartiallySynchronisedCommit IORefId
|
||||
-- ^ A commit.
|
||||
| PartiallySynchronisedWrite CRefId
|
||||
-- ^ A 'casCRef'
|
||||
| PartiallySynchronisedModify CRefId
|
||||
-- ^ A 'modifyCRefCAS'
|
||||
| SynchronisedModify CRefId
|
||||
-- ^ An 'atomicModifyCRef'.
|
||||
| PartiallySynchronisedWrite IORefId
|
||||
-- ^ A 'casIORef'
|
||||
| PartiallySynchronisedModify IORefId
|
||||
-- ^ A 'modifyIORefCAS'
|
||||
| SynchronisedModify IORefId
|
||||
-- ^ An 'atomicModifyIORef'.
|
||||
| SynchronisedRead MVarId
|
||||
-- ^ A 'readMVar' or 'takeMVar' (or @try@/@blocked@ variants).
|
||||
| SynchronisedWrite MVarId
|
||||
@ -256,26 +256,26 @@ isBarrier (SynchronisedWrite _) = True
|
||||
isBarrier SynchronisedOther = True
|
||||
isBarrier _ = False
|
||||
|
||||
-- | Check if an action commits a given 'CRef'.
|
||||
isCommit :: ActionType -> CRefId -> Bool
|
||||
-- | Check if an action commits a given 'IORef'.
|
||||
isCommit :: ActionType -> IORefId -> Bool
|
||||
isCommit (PartiallySynchronisedCommit c) r = c == r
|
||||
isCommit (PartiallySynchronisedWrite c) r = c == r
|
||||
isCommit (PartiallySynchronisedModify c) r = c == r
|
||||
isCommit _ _ = False
|
||||
|
||||
-- | Check if an action synchronises a given 'CRef'.
|
||||
synchronises :: ActionType -> CRefId -> Bool
|
||||
-- | Check if an action synchronises a given 'IORef'.
|
||||
synchronises :: ActionType -> IORefId -> Bool
|
||||
synchronises a r = isCommit a r || isBarrier a
|
||||
|
||||
-- | Get the 'CRef' affected.
|
||||
crefOf :: ActionType -> Maybe CRefId
|
||||
crefOf (UnsynchronisedRead r) = Just r
|
||||
crefOf (UnsynchronisedWrite r) = Just r
|
||||
crefOf (SynchronisedModify r) = Just r
|
||||
crefOf (PartiallySynchronisedCommit r) = Just r
|
||||
crefOf (PartiallySynchronisedWrite r) = Just r
|
||||
crefOf (PartiallySynchronisedModify r) = Just r
|
||||
crefOf _ = Nothing
|
||||
-- | Get the 'IORef' affected.
|
||||
iorefOf :: ActionType -> Maybe IORefId
|
||||
iorefOf (UnsynchronisedRead r) = Just r
|
||||
iorefOf (UnsynchronisedWrite r) = Just r
|
||||
iorefOf (SynchronisedModify r) = Just r
|
||||
iorefOf (PartiallySynchronisedCommit r) = Just r
|
||||
iorefOf (PartiallySynchronisedWrite r) = Just r
|
||||
iorefOf (PartiallySynchronisedModify r) = Just r
|
||||
iorefOf _ = Nothing
|
||||
|
||||
-- | Get the 'MVar' affected.
|
||||
mvarOf :: ActionType -> Maybe MVarId
|
||||
@ -291,7 +291,7 @@ tidsOf (PutMVar _ tids) = S.fromList tids
|
||||
tidsOf (TryPutMVar _ _ tids) = S.fromList tids
|
||||
tidsOf (TakeMVar _ tids) = S.fromList tids
|
||||
tidsOf (TryTakeMVar _ _ tids) = S.fromList tids
|
||||
tidsOf (CommitCRef tid _) = S.singleton tid
|
||||
tidsOf (CommitIORef tid _) = S.singleton tid
|
||||
tidsOf (STM _ tids) = S.fromList tids
|
||||
tidsOf (ThrowTo tid _) = S.singleton tid
|
||||
tidsOf (BlockedThrowTo tid) = S.singleton tid
|
||||
@ -313,13 +313,13 @@ simplifyLookahead (WillReadMVar c) = SynchronisedRead c
|
||||
simplifyLookahead (WillTryReadMVar c) = SynchronisedRead c
|
||||
simplifyLookahead (WillTakeMVar c) = SynchronisedRead c
|
||||
simplifyLookahead (WillTryTakeMVar c) = SynchronisedRead c
|
||||
simplifyLookahead (WillReadCRef r) = UnsynchronisedRead r
|
||||
simplifyLookahead (WillReadCRefCas r) = UnsynchronisedRead r
|
||||
simplifyLookahead (WillModCRef r) = SynchronisedModify r
|
||||
simplifyLookahead (WillModCRefCas r) = PartiallySynchronisedModify r
|
||||
simplifyLookahead (WillWriteCRef r) = UnsynchronisedWrite r
|
||||
simplifyLookahead (WillCasCRef r) = PartiallySynchronisedWrite r
|
||||
simplifyLookahead (WillCommitCRef _ r) = PartiallySynchronisedCommit r
|
||||
simplifyLookahead (WillReadIORef r) = UnsynchronisedRead r
|
||||
simplifyLookahead (WillReadIORefCas r) = UnsynchronisedRead r
|
||||
simplifyLookahead (WillModIORef r) = SynchronisedModify r
|
||||
simplifyLookahead (WillModIORefCas r) = PartiallySynchronisedModify r
|
||||
simplifyLookahead (WillWriteIORef r) = UnsynchronisedWrite r
|
||||
simplifyLookahead (WillCasIORef r) = PartiallySynchronisedWrite r
|
||||
simplifyLookahead (WillCommitIORef _ r) = PartiallySynchronisedCommit r
|
||||
simplifyLookahead WillSTM = SynchronisedOther
|
||||
simplifyLookahead (WillThrowTo _) = SynchronisedOther
|
||||
simplifyLookahead _ = UnsynchronisedOther
|
||||
@ -393,8 +393,8 @@ runRefCont :: C.MonadConc n
|
||||
=> (n () -> x)
|
||||
-> (a -> Maybe b)
|
||||
-> ((a -> x) -> x)
|
||||
-> n (x, C.CRef n (Maybe b))
|
||||
-> n (x, C.IORef n (Maybe b))
|
||||
runRefCont act f k = do
|
||||
ref <- C.newCRef Nothing
|
||||
let c = k (act . C.writeCRef ref . f)
|
||||
ref <- C.newIORef Nothing
|
||||
let c = k (act . C.writeIORef ref . f)
|
||||
pure (c, ref)
|
||||
|
||||
@ -69,7 +69,7 @@ runSCT :: MonadConc n
|
||||
=> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> ConcT n a
|
||||
-- ^ The computation to run many times.
|
||||
-> n [(Either Failure a, Trace)]
|
||||
@ -82,7 +82,7 @@ resultsSet :: (MonadConc n, Ord a)
|
||||
=> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> ConcT n a
|
||||
-- ^ The computation to run many times.
|
||||
-> n (Set (Either Failure a))
|
||||
@ -100,7 +100,7 @@ runSCTDiscard :: MonadConc n
|
||||
-> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> ConcT n a
|
||||
-- ^ The computation to run many times.
|
||||
-> n [(Either Failure a, Trace)]
|
||||
@ -116,7 +116,7 @@ resultsSetDiscard :: (MonadConc n, Ord a)
|
||||
-> Way
|
||||
-- ^ How to run the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> ConcT n a
|
||||
-- ^ The computation to run many times.
|
||||
-> n (Set (Either Failure a))
|
||||
@ -373,7 +373,7 @@ lBacktrack = backtrackAt (\_ _ -> False)
|
||||
-- @since 1.0.0.0
|
||||
sctBound :: MonadConc n
|
||||
=> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> Bounds
|
||||
-- ^ The combined bounds.
|
||||
-> ConcT n a
|
||||
@ -392,7 +392,7 @@ sctBoundDiscard :: MonadConc n
|
||||
=> (Either Failure a -> Maybe Discard)
|
||||
-- ^ Selectively discard results.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> Bounds
|
||||
-- ^ The combined bounds.
|
||||
-> ConcT n a
|
||||
@ -412,7 +412,7 @@ sctBoundDiscard discard memtype cb = runSCTWithSettings $
|
||||
-- @since 1.0.0.0
|
||||
sctUniformRandom :: (MonadConc n, RandomGen g)
|
||||
=> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> g
|
||||
-- ^ The random number generator.
|
||||
-> Int
|
||||
@ -433,7 +433,7 @@ sctUniformRandomDiscard :: (MonadConc n, RandomGen g)
|
||||
=> (Either Failure a -> Maybe Discard)
|
||||
-- ^ Selectively discard results.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> g
|
||||
-- ^ The random number generator.
|
||||
-> Int
|
||||
@ -455,7 +455,7 @@ sctUniformRandomDiscard discard memtype g lim = runSCTWithSettings $
|
||||
-- @since 1.7.0.0
|
||||
sctWeightedRandom :: (MonadConc n, RandomGen g)
|
||||
=> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> g
|
||||
-- ^ The random number generator.
|
||||
-> Int
|
||||
@ -476,7 +476,7 @@ sctWeightedRandomDiscard :: (MonadConc n, RandomGen g)
|
||||
=> (Either Failure a -> Maybe Discard)
|
||||
-- ^ Selectively discard results.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> g
|
||||
-- ^ The random number generator.
|
||||
-> Int
|
||||
@ -533,7 +533,7 @@ yieldCountInc sofar prior (d, lnext) = case prior of
|
||||
|
||||
-- | Determine if an action is a commit or not.
|
||||
isCommitRef :: ThreadAction -> Bool
|
||||
isCommitRef (CommitCRef _ _) = True
|
||||
isCommitRef (CommitIORef _ _) = True
|
||||
isCommitRef _ = False
|
||||
|
||||
-- | Get the maximum difference between two ints in a list.
|
||||
|
||||
@ -71,7 +71,7 @@ sct settings s0 sfun srun conc
|
||||
(srun (runSnap snap))
|
||||
(runSnap snap)
|
||||
(toId $ 1 + fst (_tids idsrc))
|
||||
(toId $ 1 + fst (_crids 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
|
||||
@ -93,8 +93,8 @@ sct' :: (MonadConc n, HasCallStack)
|
||||
-- ^ Just run the computation
|
||||
-> ThreadId
|
||||
-- ^ The first available @ThreadId@
|
||||
-> CRefId
|
||||
-- ^ The first available @CRefId@
|
||||
-> IORefId
|
||||
-- ^ The first available @IORefId@
|
||||
-> n [(Either Failure a, Trace)]
|
||||
sct' settings s0 sfun srun run nTId nCRId = go Nothing [] s0 where
|
||||
go (Just res) _ _ | earlyExit res = pure []
|
||||
@ -154,8 +154,8 @@ simplifyExecution :: (MonadConc n, HasCallStack)
|
||||
-- ^ Just run the computation
|
||||
-> ThreadId
|
||||
-- ^ The first available @ThreadId@
|
||||
-> CRefId
|
||||
-- ^ The first available @CRefId@
|
||||
-> IORefId
|
||||
-- ^ The first available @IORefId@
|
||||
-> Either Failure a
|
||||
-- ^ The expected result
|
||||
-> Trace
|
||||
@ -244,7 +244,7 @@ permuteBy safeIO memtype = go initialDepState where
|
||||
dropCommits :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
|
||||
dropCommits _ SequentialConsistency = id
|
||||
dropCommits safeIO memtype = go initialDepState where
|
||||
go ds (t1@(tid1, ta1@(CommitCRef _ _)):t2@(tid2, ta2):trc)
|
||||
go ds (t1@(tid1, ta1@(CommitIORef _ _)):t2@(tid2, ta2):trc)
|
||||
| isBarrier (simplifyAction ta2) = 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
|
||||
@ -302,11 +302,11 @@ pushForward safeIO memtype = go initialDepState where
|
||||
| otherwise = Nothing
|
||||
fgo _ _ = Nothing
|
||||
|
||||
-- | Re-number threads and CRefs.
|
||||
-- | Re-number threads and IORefs.
|
||||
--
|
||||
-- Permuting forks or newCRefs makes the existing numbering invalid,
|
||||
-- Permuting forks or newIORefs makes the existing numbering invalid,
|
||||
-- which then causes problems for scheduling. Just re-numbering
|
||||
-- threads isn't enough, as CRef IDs are used to determine commit
|
||||
-- threads isn't enough, as IORef IDs are used to determine commit
|
||||
-- thread IDs.
|
||||
--
|
||||
-- Renumbered things will not fix their names, so don't rely on those
|
||||
@ -317,14 +317,14 @@ renumber
|
||||
-> Int
|
||||
-- ^ First free thread ID.
|
||||
-> Int
|
||||
-- ^ First free @CRef@ ID.
|
||||
-- ^ First free @IORef@ ID.
|
||||
-> [(ThreadId, ThreadAction)]
|
||||
-> [(ThreadId, ThreadAction)]
|
||||
renumber memtype tid0 crid0 = snd . mapAccumL go (I.empty, tid0, I.empty, crid0) where
|
||||
go s@(tidmap, _, cridmap, _) (_, CommitCRef tid crid) =
|
||||
go s@(tidmap, _, cridmap, _) (_, CommitIORef tid crid) =
|
||||
let tid' = renumbered tidmap tid
|
||||
crid' = renumbered cridmap crid
|
||||
act' = CommitCRef tid' crid'
|
||||
act' = CommitIORef tid' crid'
|
||||
in case memtype of
|
||||
PartialStoreOrder -> (s, (commitThreadId tid' (Just crid'), act'))
|
||||
_ -> (s, (commitThreadId tid' Nothing, act'))
|
||||
@ -351,22 +351,22 @@ renumber memtype tid0 crid0 = snd . mapAccumL go (I.empty, tid0, I.empty, crid0)
|
||||
(s, TakeMVar mvid (map (renumbered tidmap) olds))
|
||||
updateAction s@(tidmap, _, _, _) (TryTakeMVar mvid b olds) =
|
||||
(s, TryTakeMVar mvid b (map (renumbered tidmap) olds))
|
||||
updateAction (tidmap, nTId, cridmap, nCRId) (NewCRef old) =
|
||||
updateAction (tidmap, nTId, cridmap, nCRId) (NewIORef old) =
|
||||
let cridmap' = I.insert (fromId old) nCRId cridmap
|
||||
nCRId' = nCRId + 1
|
||||
in ((tidmap, nTId, cridmap', nCRId'), NewCRef (toId nCRId))
|
||||
updateAction s@(_, _, cridmap, _) (ReadCRef old) =
|
||||
(s, ReadCRef (renumbered cridmap old))
|
||||
updateAction s@(_, _, cridmap, _) (ReadCRefCas old) =
|
||||
(s, ReadCRefCas (renumbered cridmap old))
|
||||
updateAction s@(_, _, cridmap, _) (ModCRef old) =
|
||||
(s, ModCRef (renumbered cridmap old))
|
||||
updateAction s@(_, _, cridmap, _) (ModCRefCas old) =
|
||||
(s, ModCRefCas (renumbered cridmap old))
|
||||
updateAction s@(_, _, cridmap, _) (WriteCRef old) =
|
||||
(s, WriteCRef (renumbered cridmap old))
|
||||
updateAction s@(_, _, cridmap, _) (CasCRef old b) =
|
||||
(s, CasCRef (renumbered cridmap old) b)
|
||||
in ((tidmap, nTId, cridmap', nCRId'), NewIORef (toId nCRId))
|
||||
updateAction s@(_, _, cridmap, _) (ReadIORef old) =
|
||||
(s, ReadIORef (renumbered cridmap old))
|
||||
updateAction s@(_, _, cridmap, _) (ReadIORefCas old) =
|
||||
(s, ReadIORefCas (renumbered cridmap old))
|
||||
updateAction s@(_, _, cridmap, _) (ModIORef old) =
|
||||
(s, ModIORef (renumbered cridmap old))
|
||||
updateAction s@(_, _, cridmap, _) (ModIORefCas old) =
|
||||
(s, ModIORefCas (renumbered cridmap old))
|
||||
updateAction s@(_, _, cridmap, _) (WriteIORef old) =
|
||||
(s, WriteIORef (renumbered cridmap old))
|
||||
updateAction s@(_, _, cridmap, _) (CasIORef old b) =
|
||||
(s, CasIORef (renumbered cridmap old) b)
|
||||
updateAction s@(tidmap, _, _, _) (STM tas olds) =
|
||||
(s, STM tas (map (renumbered tidmap) olds))
|
||||
updateAction s@(tidmap, _, _, _) (ThrowTo old b) =
|
||||
|
||||
@ -572,7 +572,7 @@ independent safeIO ds t1 a1 t2 a2
|
||||
-- See #191 / #190
|
||||
check _ (ThrowTo t _) tid _ | t == tid = True
|
||||
check _ (BlockedThrowTo t) tid _ | t == tid = True
|
||||
-- can't re-order an unsynchronised write with something which synchronises that CRef.
|
||||
-- can't re-order an unsynchronised write with something which synchronises that IORef.
|
||||
check _ (simplifyAction -> UnsynchronisedWrite r) _ (simplifyAction -> a) | synchronises a r = True
|
||||
check _ _ _ _ = False
|
||||
|
||||
@ -674,14 +674,14 @@ dependentActions ds a1 a2 = case (a1, a2) of
|
||||
(SynchronisedWrite v1, SynchronisedRead v2) | v1 == v2 -> True
|
||||
(SynchronisedRead v1, SynchronisedWrite v2) | v1 == v2 -> True
|
||||
|
||||
(_, _) -> maybe False (\r -> Just r == crefOf a2) (crefOf a1)
|
||||
(_, _) -> maybe False (\r -> Just r == iorefOf a2) (iorefOf a1)
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
-- ** Dependency function state
|
||||
|
||||
data DepState = DepState
|
||||
{ depCRState :: Map CRefId Bool
|
||||
-- ^ Keep track of which @CRef@s have buffered writes.
|
||||
{ depIOState :: Map IORefId Bool
|
||||
-- ^ Keep track of which @IORef@s have buffered writes.
|
||||
, depMVState :: Set MVarId
|
||||
-- ^ Keep track of which @MVar@s are full.
|
||||
, depMaskState :: Map ThreadId MaskingState
|
||||
@ -692,7 +692,7 @@ data DepState = DepState
|
||||
} deriving (Eq, Show)
|
||||
|
||||
instance NFData DepState where
|
||||
rnf depstate = rnf ( depCRState depstate
|
||||
rnf depstate = rnf ( depIOState depstate
|
||||
, depMVState depstate
|
||||
, [(t, m `seq` ()) | (t, m) <- M.toList (depMaskState depstate)]
|
||||
)
|
||||
@ -705,17 +705,17 @@ initialDepState = DepState M.empty S.empty M.empty
|
||||
-- happened.
|
||||
updateDepState :: MemType -> DepState -> ThreadId -> ThreadAction -> DepState
|
||||
updateDepState memtype depstate tid act = DepState
|
||||
{ depCRState = updateCRState memtype act $ depCRState depstate
|
||||
{ depIOState = updateCRState memtype act $ depIOState depstate
|
||||
, depMVState = updateMVState act $ depMVState depstate
|
||||
, depMaskState = updateMaskState tid act $ depMaskState depstate
|
||||
}
|
||||
|
||||
-- | Update the @CRef@ buffer state with the action that has just
|
||||
-- | Update the @IORef@ buffer state with the action that has just
|
||||
-- happened.
|
||||
updateCRState :: MemType -> ThreadAction -> Map CRefId Bool -> Map CRefId Bool
|
||||
updateCRState :: MemType -> ThreadAction -> Map IORefId Bool -> Map IORefId Bool
|
||||
updateCRState SequentialConsistency _ = const M.empty
|
||||
updateCRState _ (CommitCRef _ r) = M.delete r
|
||||
updateCRState _ (WriteCRef r) = M.insert r True
|
||||
updateCRState _ (CommitIORef _ r) = M.delete r
|
||||
updateCRState _ (WriteIORef r) = M.insert r True
|
||||
updateCRState _ ta
|
||||
| isBarrier $ simplifyAction ta = const M.empty
|
||||
| otherwise = id
|
||||
@ -743,9 +743,9 @@ updateMaskState _ (ThrowTo tid True) = M.delete tid
|
||||
updateMaskState tid Stop = M.delete tid
|
||||
updateMaskState _ _ = id
|
||||
|
||||
-- | Check if a @CRef@ has a buffered write pending.
|
||||
isBuffered :: DepState -> CRefId -> Bool
|
||||
isBuffered depstate r = M.findWithDefault False r (depCRState depstate)
|
||||
-- | Check if a @IORef@ has a buffered write pending.
|
||||
isBuffered :: DepState -> IORefId -> Bool
|
||||
isBuffered depstate r = M.findWithDefault False r (depIOState depstate)
|
||||
|
||||
-- | Check if an @MVar@ is full.
|
||||
isFull :: DepState -> MVarId -> Bool
|
||||
|
||||
@ -59,22 +59,22 @@ module Test.DejaFu.Settings
|
||||
|
||||
-- ** The @MemType@
|
||||
|
||||
-- | When executed on a multi-core processor some @CRef@ / @IORef@
|
||||
-- | When executed on a multi-core processor some @IORef@ / @IORef@
|
||||
-- programs can exhibit \"relaxed memory\" behaviours, where the
|
||||
-- apparent behaviour of the program is not a simple interleaving of
|
||||
-- the actions of each thread.
|
||||
--
|
||||
-- __Example:__ This is a simple program which creates two @CRef@s
|
||||
-- __Example:__ This is a simple program which creates two @IORef@s
|
||||
-- containing @False@, and forks two threads. Each thread writes
|
||||
-- @True@ to one of the @CRef@s and reads the other. The value that
|
||||
-- @True@ to one of the @IORef@s and reads the other. The value that
|
||||
-- each thread reads is communicated back through an @MVar@:
|
||||
--
|
||||
-- > >>> :{
|
||||
-- > let relaxed = do
|
||||
-- > r1 <- newCRef False
|
||||
-- > r2 <- newCRef False
|
||||
-- > x <- spawn $ writeCRef r1 True >> readCRef r2
|
||||
-- > y <- spawn $ writeCRef r2 True >> readCRef r1
|
||||
-- > r1 <- newIORef False
|
||||
-- > r2 <- newIORef False
|
||||
-- > x <- spawn $ writeIORef r1 True >> readIORef r2
|
||||
-- > y <- spawn $ writeIORef r2 True >> readIORef r1
|
||||
-- > (,) <$> readMVar x <*> readMVar y
|
||||
-- > :}
|
||||
--
|
||||
@ -94,12 +94,12 @@ module Test.DejaFu.Settings
|
||||
-- > False
|
||||
--
|
||||
-- It's possible for both threads to read the value @False@, even
|
||||
-- though each writes @True@ to the other @CRef@ before reading.
|
||||
-- though each writes @True@ to the other @IORef@ before reading.
|
||||
-- This is because processors are free to re-order reads and writes
|
||||
-- to independent memory addresses in the name of performance.
|
||||
--
|
||||
-- Execution traces for relaxed memory computations can include
|
||||
-- \"C\" actions, as above, which show where @CRef@ writes were
|
||||
-- \"C\" actions, as above, which show where @IORef@ writes were
|
||||
-- explicitly /committed/, and made visible to other threads.
|
||||
--
|
||||
-- However, modelling this behaviour can require more executions.
|
||||
|
||||
@ -39,17 +39,14 @@ instance Show ThreadId where
|
||||
-- | @since 1.3.1.0
|
||||
deriving instance Generic ThreadId
|
||||
|
||||
-- | Every @CRef@ has a unique identifier.
|
||||
-- | Every @IORef@ has a unique identifier.
|
||||
--
|
||||
-- @since 1.0.0.0
|
||||
newtype CRefId = CRefId Id
|
||||
deriving (Eq, Ord, NFData)
|
||||
-- @since 1.11.0.0
|
||||
newtype IORefId = IORefId Id
|
||||
deriving (Eq, Ord, NFData, Generic)
|
||||
|
||||
instance Show CRefId where
|
||||
show (CRefId id_) = show id_
|
||||
|
||||
-- | @since 1.3.1.0
|
||||
deriving instance Generic CRefId
|
||||
instance Show IORefId where
|
||||
show (IORefId id_) = show id_
|
||||
|
||||
-- | Every @MVar@ has a unique identifier.
|
||||
--
|
||||
@ -75,7 +72,7 @@ instance Show TVarId where
|
||||
-- | @since 1.3.1.0
|
||||
deriving instance Generic TVarId
|
||||
|
||||
-- | An identifier for a thread, @MVar@, @CRef@, or @TVar@.
|
||||
-- | An identifier for a thread, @MVar@, @IORef@, or @TVar@.
|
||||
--
|
||||
-- The number is the important bit. The string is to make execution
|
||||
-- traces easier to read, but is meaningless.
|
||||
@ -109,7 +106,7 @@ initialThread = ThreadId (Id (Just "main") 0)
|
||||
|
||||
-- | All the actions that a thread can perform.
|
||||
--
|
||||
-- @since 1.9.0.0
|
||||
-- @since 1.11.0.0
|
||||
data ThreadAction =
|
||||
Fork ThreadId
|
||||
-- ^ Start a new thread.
|
||||
@ -147,23 +144,23 @@ data ThreadAction =
|
||||
-- ^ Get blocked on a take.
|
||||
| TryTakeMVar MVarId Bool [ThreadId]
|
||||
-- ^ Try to take from a 'MVar', possibly waking up some threads.
|
||||
| NewCRef CRefId
|
||||
-- ^ Create a new 'CRef'.
|
||||
| ReadCRef CRefId
|
||||
-- ^ Read from a 'CRef'.
|
||||
| ReadCRefCas CRefId
|
||||
-- ^ Read from a 'CRef' for a future compare-and-swap.
|
||||
| ModCRef CRefId
|
||||
-- ^ Modify a 'CRef'.
|
||||
| ModCRefCas CRefId
|
||||
-- ^ Modify a 'CRef' using a compare-and-swap.
|
||||
| WriteCRef CRefId
|
||||
-- ^ Write to a 'CRef' without synchronising.
|
||||
| CasCRef CRefId Bool
|
||||
-- ^ Attempt to to a 'CRef' using a compare-and-swap, synchronising
|
||||
| NewIORef IORefId
|
||||
-- ^ Create a new 'IORef'.
|
||||
| ReadIORef IORefId
|
||||
-- ^ Read from a 'IORef'.
|
||||
| ReadIORefCas IORefId
|
||||
-- ^ Read from a 'IORef' for a future compare-and-swap.
|
||||
| ModIORef IORefId
|
||||
-- ^ Modify a 'IORef'.
|
||||
| ModIORefCas IORefId
|
||||
-- ^ Modify a 'IORef' using a compare-and-swap.
|
||||
| WriteIORef IORefId
|
||||
-- ^ Write to a 'IORef' without synchronising.
|
||||
| CasIORef IORefId Bool
|
||||
-- ^ Attempt to to a 'IORef' using a compare-and-swap, synchronising
|
||||
-- it.
|
||||
| CommitCRef ThreadId CRefId
|
||||
-- ^ Commit the last write to the given 'CRef' by the given thread,
|
||||
| CommitIORef ThreadId IORefId
|
||||
-- ^ Commit the last write to the given 'IORef' by the given thread,
|
||||
-- so that all threads can see the updated value.
|
||||
| STM [TAction] [ThreadId]
|
||||
-- ^ An STM transaction was executed, possibly waking up some
|
||||
@ -203,10 +200,7 @@ data ThreadAction =
|
||||
-- ^ Stop executing an action with @subconcurrency@.
|
||||
| DontCheck Trace
|
||||
-- ^ Execute an action with @dontCheck@.
|
||||
deriving (Eq, Show)
|
||||
|
||||
-- | @since 1.3.1.0
|
||||
deriving instance Generic ThreadAction
|
||||
deriving (Eq, Generic, Show)
|
||||
|
||||
-- this makes me sad
|
||||
instance NFData ThreadAction where
|
||||
@ -228,14 +222,14 @@ instance NFData ThreadAction where
|
||||
rnf (TakeMVar m ts) = rnf (m, ts)
|
||||
rnf (BlockedTakeMVar m) = rnf m
|
||||
rnf (TryTakeMVar m b ts) = rnf (m, b, ts)
|
||||
rnf (NewCRef c) = rnf c
|
||||
rnf (ReadCRef c) = rnf c
|
||||
rnf (ReadCRefCas c) = rnf c
|
||||
rnf (ModCRef c) = rnf c
|
||||
rnf (ModCRefCas c) = rnf c
|
||||
rnf (WriteCRef c) = rnf c
|
||||
rnf (CasCRef c b) = rnf (c, b)
|
||||
rnf (CommitCRef t c) = rnf (t, c)
|
||||
rnf (NewIORef c) = rnf c
|
||||
rnf (ReadIORef c) = rnf c
|
||||
rnf (ReadIORefCas c) = rnf c
|
||||
rnf (ModIORef c) = rnf c
|
||||
rnf (ModIORefCas c) = rnf c
|
||||
rnf (WriteIORef c) = rnf c
|
||||
rnf (CasIORef c b) = rnf (c, b)
|
||||
rnf (CommitIORef t c) = rnf (t, c)
|
||||
rnf (STM as ts) = rnf (as, ts)
|
||||
rnf (BlockedSTM as) = rnf as
|
||||
rnf Catching = ()
|
||||
@ -254,7 +248,7 @@ instance NFData ThreadAction where
|
||||
|
||||
-- | A one-step look-ahead at what a thread will do next.
|
||||
--
|
||||
-- @since 1.1.0.0
|
||||
-- @since 1.11.0.0
|
||||
data Lookahead =
|
||||
WillFork
|
||||
-- ^ Will start a new thread.
|
||||
@ -288,23 +282,23 @@ data Lookahead =
|
||||
-- ^ Will take from a 'MVar', possibly waking up some threads.
|
||||
| WillTryTakeMVar MVarId
|
||||
-- ^ Will try to take from a 'MVar', possibly waking up some threads.
|
||||
| WillNewCRef
|
||||
-- ^ Will create a new 'CRef'.
|
||||
| WillReadCRef CRefId
|
||||
-- ^ Will read from a 'CRef'.
|
||||
| WillReadCRefCas CRefId
|
||||
-- ^ Will read from a 'CRef' for a future compare-and-swap.
|
||||
| WillModCRef CRefId
|
||||
-- ^ Will modify a 'CRef'.
|
||||
| WillModCRefCas CRefId
|
||||
-- ^ Will modify a 'CRef' using a compare-and-swap.
|
||||
| WillWriteCRef CRefId
|
||||
-- ^ Will write to a 'CRef' without synchronising.
|
||||
| WillCasCRef CRefId
|
||||
-- ^ Will attempt to to a 'CRef' using a compare-and-swap,
|
||||
| WillNewIORef
|
||||
-- ^ Will create a new 'IORef'.
|
||||
| WillReadIORef IORefId
|
||||
-- ^ Will read from a 'IORef'.
|
||||
| WillReadIORefCas IORefId
|
||||
-- ^ Will read from a 'IORef' for a future compare-and-swap.
|
||||
| WillModIORef IORefId
|
||||
-- ^ Will modify a 'IORef'.
|
||||
| WillModIORefCas IORefId
|
||||
-- ^ Will modify a 'IORef' using a compare-and-swap.
|
||||
| WillWriteIORef IORefId
|
||||
-- ^ Will write to a 'IORef' without synchronising.
|
||||
| WillCasIORef IORefId
|
||||
-- ^ Will attempt to to a 'IORef' using a compare-and-swap,
|
||||
-- synchronising it.
|
||||
| WillCommitCRef ThreadId CRefId
|
||||
-- ^ Will commit the last write by the given thread to the 'CRef'.
|
||||
| WillCommitIORef ThreadId IORefId
|
||||
-- ^ Will commit the last write by the given thread to the 'IORef'.
|
||||
| WillSTM
|
||||
-- ^ Will execute an STM transaction, possibly waking up some
|
||||
-- threads.
|
||||
@ -337,10 +331,7 @@ data Lookahead =
|
||||
-- ^ Will stop executing an extion with @subconcurrency@.
|
||||
| WillDontCheck
|
||||
-- ^ Will execute an action with @dontCheck@.
|
||||
deriving (Eq, Show)
|
||||
|
||||
-- | @since 1.3.1.0
|
||||
deriving instance Generic Lookahead
|
||||
deriving (Eq, Generic, Show)
|
||||
|
||||
-- this also makes me sad
|
||||
instance NFData Lookahead where
|
||||
@ -359,14 +350,14 @@ instance NFData Lookahead where
|
||||
rnf (WillTryReadMVar m) = rnf m
|
||||
rnf (WillTakeMVar m) = rnf m
|
||||
rnf (WillTryTakeMVar m) = rnf m
|
||||
rnf WillNewCRef = ()
|
||||
rnf (WillReadCRef c) = rnf c
|
||||
rnf (WillReadCRefCas c) = rnf c
|
||||
rnf (WillModCRef c) = rnf c
|
||||
rnf (WillModCRefCas c) = rnf c
|
||||
rnf (WillWriteCRef c) = rnf c
|
||||
rnf (WillCasCRef c) = rnf c
|
||||
rnf (WillCommitCRef t c) = rnf (t, c)
|
||||
rnf WillNewIORef = ()
|
||||
rnf (WillReadIORef c) = rnf c
|
||||
rnf (WillReadIORefCas c) = rnf c
|
||||
rnf (WillModIORef c) = rnf c
|
||||
rnf (WillModIORefCas c) = rnf c
|
||||
rnf (WillWriteIORef c) = rnf c
|
||||
rnf (WillCasIORef c) = rnf c
|
||||
rnf (WillCommitIORef t c) = rnf (t, c)
|
||||
rnf WillSTM = ()
|
||||
rnf WillCatching = ()
|
||||
rnf WillPopCatching = ()
|
||||
@ -715,13 +706,13 @@ strengthenDiscard d1 d2 =
|
||||
-------------------------------------------------------------------------------
|
||||
-- * Memory Models
|
||||
|
||||
-- | The memory model to use for non-synchronised 'CRef' operations.
|
||||
-- | The memory model to use for non-synchronised 'IORef' operations.
|
||||
--
|
||||
-- @since 0.4.0.0
|
||||
data MemType =
|
||||
SequentialConsistency
|
||||
-- ^ The most intuitive model: a program behaves as a simple
|
||||
-- interleaving of the actions in different threads. When a 'CRef'
|
||||
-- interleaving of the actions in different threads. When a 'IORef'
|
||||
-- is written to, that write is immediately visible to all threads.
|
||||
| TotalStoreOrder
|
||||
-- ^ Each thread has a write buffer. A thread sees its writes
|
||||
@ -729,9 +720,9 @@ data MemType =
|
||||
-- committed, which may happen later. Writes are committed in the
|
||||
-- same order that they are created.
|
||||
| PartialStoreOrder
|
||||
-- ^ Each 'CRef' has a write buffer. A thread sees its writes
|
||||
-- ^ 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 'CRef's
|
||||
-- committed, which may happen later. Writes to different 'IORef's
|
||||
-- are not necessarily committed in the same order that they are
|
||||
-- created.
|
||||
deriving (Eq, Show, Read, Ord, Enum, Bounded)
|
||||
|
||||
@ -34,7 +34,7 @@ toTIdTrace =
|
||||
showTrace :: Trace -> String
|
||||
showTrace [] = "<trace discarded>"
|
||||
showTrace trc = intercalate "\n" $ go False trc : strkey where
|
||||
go _ ((_,_,CommitCRef _ _):rest) = "C-" ++ go False rest
|
||||
go _ ((_,_,CommitIORef _ _):rest) = "C-" ++ go False rest
|
||||
go _ ((Start (ThreadId (Id _ i)),_,a):rest) = "S" ++ show i ++ "-" ++ go (didYield a) rest
|
||||
go y ((SwitchTo (ThreadId (Id _ i)),_,a):rest) = (if y then "p" else "P") ++ show i ++ "-" ++ go (didYield a) rest
|
||||
go _ ((Continue,_,a):rest) = '-' : go (didYield a) rest
|
||||
@ -63,7 +63,7 @@ simplestsBy f = map choose . collect where
|
||||
choose = minimumBy . comparing $ \(_, trc) ->
|
||||
let switchTos = length . filter (\(d,_,_) -> case d of SwitchTo _ -> True; _ -> False)
|
||||
starts = length . filter (\(d,_,_) -> case d of Start _ -> True; _ -> False)
|
||||
commits = length . filter (\(_,_,a) -> case a of CommitCRef _ _ -> True; _ -> False)
|
||||
commits = length . filter (\(_,_,a) -> case a of CommitIORef _ _ -> True; _ -> False)
|
||||
in (switchTos trc, commits trc, length trc, starts trc)
|
||||
|
||||
groupBy' res _ [] = res
|
||||
|
||||
@ -2,7 +2,7 @@
|
||||
-- documentation, see http://haskell.org/cabal/users-guide/
|
||||
|
||||
name: dejafu
|
||||
version: 1.10.1.0
|
||||
version: 1.11.0.0
|
||||
synopsis: A library for unit-testing concurrent programs.
|
||||
|
||||
description:
|
||||
@ -33,7 +33,7 @@ source-repository head
|
||||
source-repository this
|
||||
type: git
|
||||
location: https://github.com/barrucadu/dejafu.git
|
||||
tag: dejafu-1.10.1.0
|
||||
tag: dejafu-1.11.0.0
|
||||
|
||||
library
|
||||
exposed-modules: Test.DejaFu
|
||||
@ -58,7 +58,7 @@ library
|
||||
-- other-modules:
|
||||
-- other-extensions:
|
||||
build-depends: base >=4.9 && <5
|
||||
, concurrency >=1.5 && <1.6
|
||||
, concurrency >=1.6 && <1.7
|
||||
, containers >=0.5 && <0.6
|
||||
, contravariant >=1.2 && <1.5
|
||||
, deepseq >=1.1 && <2
|
||||
|
||||
@ -76,23 +76,23 @@ These types live in ``Test.DejaFu.Types``:
|
||||
-- ^ Get blocked on a take.
|
||||
| TryTakeMVar MVarId Bool [ThreadId]
|
||||
-- ^ Try to take from a 'MVar', possibly waking up some threads.
|
||||
| NewCRef CRefId
|
||||
-- ^ Create a new 'CRef'.
|
||||
| ReadCRef CRefId
|
||||
-- ^ Read from a 'CRef'.
|
||||
| ReadCRefCas CRefId
|
||||
-- ^ Read from a 'CRef' for a future compare-and-swap.
|
||||
| ModCRef CRefId
|
||||
-- ^ Modify a 'CRef'.
|
||||
| ModCRefCas CRefId
|
||||
-- ^ Modify a 'CRef' using a compare-and-swap.
|
||||
| WriteCRef CRefId
|
||||
-- ^ Write to a 'CRef' without synchronising.
|
||||
| CasCRef CRefId Bool
|
||||
-- ^ Attempt to to a 'CRef' using a compare-and-swap, synchronising
|
||||
| NewIORef IORefId
|
||||
-- ^ Create a new 'IORef'.
|
||||
| ReadIORef IORefId
|
||||
-- ^ Read from a 'IORef'.
|
||||
| ReadIORefCas IORefId
|
||||
-- ^ Read from a 'IORef' for a future compare-and-swap.
|
||||
| ModIORef IORefId
|
||||
-- ^ Modify a 'IORef'.
|
||||
| ModIORefCas IORefId
|
||||
-- ^ Modify a 'IORef' using a compare-and-swap.
|
||||
| WriteIORef IORefId
|
||||
-- ^ Write to a 'IORef' without synchronising.
|
||||
| CasIORef IORefId Bool
|
||||
-- ^ Attempt to to a 'IORef' using a compare-and-swap, synchronising
|
||||
-- it.
|
||||
| CommitCRef ThreadId CRefId
|
||||
-- ^ Commit the last write to the given 'CRef' by the given thread,
|
||||
| CommitIORef ThreadId IORefId
|
||||
-- ^ Commit the last write to the given 'IORef' by the given thread,
|
||||
-- so that all threads can see the updated value.
|
||||
| STM TTrace [ThreadId]
|
||||
-- ^ An STM transaction was executed, possibly waking up some
|
||||
@ -210,13 +210,13 @@ continuation to call when it is done:
|
||||
| forall a. ATakeMVar (MVar r a) (a -> Action n r)
|
||||
| forall a. ATryTakeMVar (MVar r a) (Maybe a -> Action n r)
|
||||
|
||||
| forall a. ANewCRef String a (CRef r a -> Action n r)
|
||||
| forall a. AReadCRef (CRef r a) (a -> Action n r)
|
||||
| forall a. AReadCRefCas (CRef r a) (Ticket a -> Action n r)
|
||||
| forall a b. AModCRef (CRef r a) (a -> (a, b)) (b -> Action n r)
|
||||
| forall a b. AModCRefCas (CRef r a) (a -> (a, b)) (b -> Action n r)
|
||||
| forall a. AWriteCRef (CRef r a) a (Action n r)
|
||||
| forall a. ACasCRef (CRef r a) (Ticket a) a ((Bool, Ticket a) -> Action n r)
|
||||
| forall a. ANewIORef String a (IORef r a -> Action n r)
|
||||
| forall a. AReadIORef (IORef r a) (a -> Action n r)
|
||||
| forall a. AReadIORefCas (IORef r a) (Ticket a -> Action n r)
|
||||
| forall a b. AModIORef (IORef r a) (a -> (a, b)) (b -> Action n r)
|
||||
| forall a b. AModIORefCas (IORef r a) (a -> (a, b)) (b -> Action n r)
|
||||
| forall a. AWriteIORef (IORef r a) a (Action n r)
|
||||
| forall a. ACasIORef (IORef r a) (Ticket a) a ((Bool, Ticket a) -> Action n r)
|
||||
|
||||
| forall e. Exception e => AThrow e
|
||||
| forall e. Exception e => AThrowTo ThreadId e (Action n r)
|
||||
@ -229,7 +229,7 @@ continuation to call when it is done:
|
||||
| ALift (n (Action n r))
|
||||
| AYield (Action n r)
|
||||
| AReturn (Action n r)
|
||||
| ACommit ThreadId CRefId
|
||||
| ACommit ThreadId IORefId
|
||||
| AStop (n ())
|
||||
|
||||
| forall a. ASub (M n r a) (Either Failure a -> Action n r)
|
||||
@ -293,9 +293,9 @@ variable ID", this is a naming convention from the past which I
|
||||
haven't updated yet.
|
||||
|
||||
The tricky bit here is ``synchronised``. It means that this action
|
||||
imposes a *memory barrier*: any uncommitted ``CRef`` writes get
|
||||
imposes a *memory barrier*: any uncommitted ``IORef`` writes get
|
||||
flushed when this action is performed. Pretty much everything other
|
||||
than a couple of ``CRef`` operations impose a memory barrier.
|
||||
than a couple of ``IORef`` operations impose a memory barrier.
|
||||
Incidentally, this is what the ``SynchronisedWrite`` we mentioned
|
||||
above refers to.
|
||||
|
||||
|
||||
@ -24,7 +24,7 @@ The available settings are:
|
||||
* **"Way"**, how to explore the behaviours of the program under test.
|
||||
|
||||
* **Memory model**, which affects how non-synchronised operations,
|
||||
such as ``readCRef`` and ``writeCRef`` behave.
|
||||
such as ``readIORef`` and ``writeIORef`` behave.
|
||||
|
||||
* **Discarding**, which allows throwing away uninteresting results,
|
||||
rather than keeping them around in memory.
|
||||
|
||||
@ -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.5.0.0", "Typeclasses, functions, and data types for concurrency and STM"
|
||||
":hackage:`dejafu`", "1.10.1.0", "Systematic testing for Haskell concurrency"
|
||||
":hackage:`hunit-dejafu`", "1.2.0.5", "Déjà Fu support for the HUnit test framework"
|
||||
":hackage:`tasty-dejafu`", "1.2.0.6", "Déjà Fu support for the tasty test framework"
|
||||
":hackage:`concurrency`", "1.6.0.0", "Typeclasses, functions, and data types for concurrency and STM"
|
||||
":hackage:`dejafu`", "1.11.0.0", "Systematic testing for Haskell concurrency"
|
||||
":hackage:`hunit-dejafu`", "1.2.0.6", "Déjà Fu support for the HUnit test framework"
|
||||
":hackage:`tasty-dejafu`", "1.2.0.7", "Déjà Fu support for the tasty test framework"
|
||||
|
||||
|
||||
Installation
|
||||
|
||||
@ -103,7 +103,7 @@ functions. These functions are:
|
||||
The signatures can have different state types, as long as the seed and
|
||||
observation types are the same. This lets you compare different
|
||||
implementations of the same idea: for example, comparing a concurrent
|
||||
stack implemented using ``MVar`` with one implemented using ``CRef``.
|
||||
stack implemented using ``MVar`` with one implemented using ``IORef``.
|
||||
|
||||
Properties can have parameters, given in the obvious way:
|
||||
|
||||
|
||||
@ -32,22 +32,18 @@ process:
|
||||
|
||||
* ``TVar`` becomes ``TVar stm``
|
||||
* ``MVar`` becomes ``MVar m``
|
||||
* ``IORef`` becomes ``CRef m`` [#]_
|
||||
* ``IORef`` becomes ``IORef m``
|
||||
|
||||
5. Some functions are renamed:
|
||||
|
||||
* ``*IORef*`` becomes ``*CRef*``
|
||||
* ``forkIO*`` becomes ``fork*``
|
||||
* ``atomicModifyIORefCAS*`` becomes ``modifyCRefCAS*``
|
||||
* ``atomicModifyIORefCAS*`` becomes ``modifyIORefCAS*``
|
||||
|
||||
6. Fix the type errors
|
||||
|
||||
If you're lucky enough to be starting a new concurrent Haskell
|
||||
project, you can just program against the ``MonadConc`` interface.
|
||||
|
||||
.. [#] I felt that calling it ``IORef`` when there was no I/O involved
|
||||
would be confusing, but this was perhaps a mistake.
|
||||
|
||||
|
||||
What if I really need I/O?
|
||||
--------------------------
|
||||
|
||||
@ -38,9 +38,9 @@ bugs. Here they are:
|
||||
|
||||
nondeterministic :: forall m. MonadConc m => m Int
|
||||
nondeterministic = do
|
||||
var <- newCRef 0
|
||||
var <- newIORef 0
|
||||
let settings = (defaultUpdateSettings :: UpdateSettings m ())
|
||||
{ updateAction = atomicModifyCRef var (\x -> (x+1, x)) }
|
||||
{ updateAction = atomicModifyIORef var (\x -> (x+1, x)) }
|
||||
auto <- mkAutoUpdate settings
|
||||
auto
|
||||
auto
|
||||
|
||||
@ -7,6 +7,18 @@ standard Haskell versioning scheme.
|
||||
.. _PVP: https://pvp.haskell.org/
|
||||
|
||||
|
||||
1.2.0.6 (2018-07-01)
|
||||
--------------------
|
||||
|
||||
* Git: :tag:`hunit-dejafu-1.2.0.6`
|
||||
* Hackage: :hackage:`hunit-dejafu-1.2.0.6`
|
||||
|
||||
Miscellaneous
|
||||
~~~~~~~~~~~~~
|
||||
|
||||
* The upper bound on :hackage:`dejafu` is <1.12.
|
||||
|
||||
|
||||
1.2.0.5 (2018-06-17)
|
||||
--------------------
|
||||
|
||||
|
||||
@ -115,7 +115,7 @@ testAutoWay :: (Eq a, Show a)
|
||||
=> Way
|
||||
-- ^ How to execute the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> Conc.ConcIO a
|
||||
-- ^ The computation to test.
|
||||
-> Test
|
||||
@ -157,7 +157,7 @@ testDejafuWay :: Show b
|
||||
=> Way
|
||||
-- ^ How to execute the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> String
|
||||
-- ^ The name of the test.
|
||||
-> ProPredicate a b
|
||||
@ -191,7 +191,7 @@ testDejafuDiscard :: Show b
|
||||
-> Way
|
||||
-- ^ How to execute the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> String
|
||||
-- ^ The name of the test.
|
||||
-> ProPredicate a b
|
||||
@ -224,7 +224,7 @@ testDejafusWay :: Show b
|
||||
=> Way
|
||||
-- ^ How to execute the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> [(String, ProPredicate a b)]
|
||||
-- ^ The list of predicates (with names) to check.
|
||||
-> Conc.ConcIO a
|
||||
@ -255,7 +255,7 @@ testDejafusDiscard :: Show b
|
||||
-> Way
|
||||
-- ^ How to execute the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> [(String, ProPredicate a b)]
|
||||
-- ^ The list of predicates (with names) to check.
|
||||
-> Conc.ConcIO a
|
||||
|
||||
@ -2,7 +2,7 @@
|
||||
-- documentation, see http://haskell.org/cabal/users-guide/
|
||||
|
||||
name: hunit-dejafu
|
||||
version: 1.2.0.5
|
||||
version: 1.2.0.6
|
||||
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-1.2.0.5
|
||||
tag: hunit-dejafu-1.2.0.6
|
||||
|
||||
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 >=1.5 && <1.11
|
||||
, dejafu >=1.5 && <1.12
|
||||
, 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/
|
||||
|
||||
|
||||
1.2.0.7 (2018-07-01)
|
||||
--------------------
|
||||
|
||||
* Git: :tag:`tasty-dejafu-1.2.0.7`
|
||||
* Hackage: :hackage:`tasty-dejafu-1.2.0.7`
|
||||
|
||||
Miscellaneous
|
||||
~~~~~~~~~~~~~
|
||||
|
||||
* The upper bound on :hackage:`dejafu` is <1.12.
|
||||
|
||||
|
||||
1.2.0.6 (2018-06-17)
|
||||
--------------------
|
||||
|
||||
|
||||
@ -148,7 +148,7 @@ testAutoWay :: (Eq a, Show a)
|
||||
=> Way
|
||||
-- ^ How to execute the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> Conc.ConcIO a
|
||||
-- ^ The computation to test.
|
||||
-> TestTree
|
||||
@ -190,7 +190,7 @@ testDejafuWay :: Show b
|
||||
=> Way
|
||||
-- ^ How to execute the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> TestName
|
||||
-- ^ The name of the test.
|
||||
-> ProPredicate a b
|
||||
@ -224,7 +224,7 @@ testDejafuDiscard :: Show b
|
||||
-> Way
|
||||
-- ^ How to execute the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> String
|
||||
-- ^ The name of the test.
|
||||
-> ProPredicate a b
|
||||
@ -257,7 +257,7 @@ testDejafusWay :: Show b
|
||||
=> Way
|
||||
-- ^ How to execute the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> [(TestName, ProPredicate a b)]
|
||||
-- ^ The list of predicates (with names) to check.
|
||||
-> Conc.ConcIO a
|
||||
@ -288,7 +288,7 @@ testDejafusDiscard :: Show b
|
||||
-> Way
|
||||
-- ^ How to execute the concurrent program.
|
||||
-> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
-- ^ The memory model to use for non-synchronised @IORef@ operations.
|
||||
-> [(TestName, ProPredicate a b)]
|
||||
-- ^ The list of predicates (with names) to check.
|
||||
-> Conc.ConcIO a
|
||||
|
||||
@ -2,7 +2,7 @@
|
||||
-- documentation, see http://haskell.org/cabal/users-guide/
|
||||
|
||||
name: tasty-dejafu
|
||||
version: 1.2.0.6
|
||||
version: 1.2.0.7
|
||||
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-1.2.0.6
|
||||
tag: tasty-dejafu-1.2.0.7
|
||||
|
||||
library
|
||||
exposed-modules: Test.Tasty.DejaFu
|
||||
-- other-modules:
|
||||
-- other-extensions:
|
||||
build-depends: base >=4.9 && <5
|
||||
, dejafu >=1.5 && <1.11
|
||||
, dejafu >=1.5 && <1.12
|
||||
, random >=1.0 && <1.2
|
||||
, tagged >=0.8 && <0.9
|
||||
, tasty >=0.10 && <1.2
|
||||
|
||||
Loading…
Reference in New Issue
Block a user