barrucadu/dejafu
1
1
Fork 0
mirror of https://github.com/barrucadu/dejafu.git synced 2024-11-22 12:15:39 +03:00
Code Issues Projects Releases Wiki Activity

Implement effect-free concurrency invariants

Browse Source
This commit is contained in:
Michael Walker 2019-02-01 14:44:59 +00:00
parent da474b5dcf
commit 129c21912e
13 changed files with 383 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
dejafu-tests/lib/Integration/MultiThreaded.hs
View File

@ -2,7 +2,7 @@ module Integration.MultiThreaded where
import qualified Control.Concurrent as C
import Control.Exception (ArithException(..))
import Control.Monad (replicateM, void)
import Control.Monad (replicateM, void, when)
import Control.Monad.IO.Class (liftIO)
import System.Random (mkStdGen)
import Test.DejaFu (Condition(..), gives, gives',
@ -11,6 +11,7 @@ import Test.DejaFu (Condition(..), gives, gives',
import Control.Concurrent.Classy hiding (newQSemN, signalQSemN,
waitQSemN)
import Control.Monad.Catch (throwM, toException)
import qualified Data.IORef as IORef
import Common
@ -364,6 +365,18 @@ programTests = toTestList
let interfere_ = waitQSemN s 0 >> signalQSemN s 0
in signalQSemN s 0 ||| waitQSemN s 0 ||| interfere_)
]
, testGroup "registerInvariant"
[ djfuT "Invariant failure is nondeterministic if there are races" (gives [Left (InvariantFailure (toException Overflow)), Right (Just 0), Right Nothing]) $
withSetup
(do v <- newEmptyMVarInt
registerInvariant (inspectMVar v >>= \x -> when (x == Just 1) (throwM Overflow))
pure v)
(\v -> do
_ <- fork $ putMVar v 0
_ <- fork $ putMVar v 1
tryReadMVar v)
]
]
-------------------------------------------------------------------------------

57
dejafu-tests/lib/Integration/SingleThreaded.hs
View File

@ -3,13 +3,18 @@ module Integration.SingleThreaded where
import Control.Exception (ArithException(..),
ArrayException(..))
import Test.DejaFu (Condition(..), gives, gives',
isDeadlock, isUncaughtException,
withSetup)
inspectIORef, inspectMVar,
inspectTVar, isDeadlock,
isInvariantFailure,
isUncaughtException,
registerInvariant, withSetup)
import Control.Concurrent.Classy
import Control.Monad (replicateM_)
import Control.Monad (replicateM_, when)
import Control.Monad.Catch (throwM)
import Control.Monad.IO.Class (liftIO)
import qualified Data.IORef as IORef
import Data.Maybe (isNothing)
import System.Random (mkStdGen)
import Common
@ -311,6 +316,52 @@ programTests = toTestList
(\_ x -> pure (either (const False) (==3) x))
takeMVar
]
, testGroup "registerInvariant"
[ djfuS "An uncaught exception fails an invariant" (alwaysFailsWith isInvariantFailure) $
withSetup (registerInvariant (throwM Overflow)) $
\() -> pure True
, djfuS "An invariant which never throws always passes" (gives' [True]) $
withSetup (registerInvariant (pure ())) $
\() -> pure True
, djfuS "An invariant can catch exceptions" (gives' [True]) $
withSetup (registerInvariant (throwM Overflow `catchArithException` \_ -> pure ())) $
\() -> pure True
, djfuS "Invariants can read MVars" (alwaysFailsWith isInvariantFailure) $
withSetup
(do v <- newMVarInt 10
registerInvariant (inspectMVar v >>= \x -> when (isNothing x) (throwM Overflow))
pure v)
takeMVar
, djfuS "Invariants can read TVars" (alwaysFailsWith isInvariantFailure) $
withSetup
(do v <- atomically (newTVar (10::Int))
registerInvariant (inspectTVar v >>= \x -> when (x < 5) (throwM Overflow))
pure v)
(\v -> atomically (writeTVar v 1))
, djfuS "Invariants aren't checked in the setup" (gives' [True]) $
withSetup
(do v <- newIORefInt 10
registerInvariant (inspectIORef v >>= \x -> when (x < 5) (throwM Overflow))
writeIORef v 1
writeIORef v 10)
(\_ -> pure True)
, djfuS "Invariants aren't checked in the teardown" (gives' [True]) $
withSetupAndTeardown
(do v <- newIORefInt 10
registerInvariant (inspectIORef v >>= \x -> when (x < 5) (throwM Overflow))
pure v)
(\v _ -> do
writeIORef v 1
writeIORef v 10
pure True)
(\_ -> pure ())
, djfuS "Invariants aren't checked if added in the main phase" (gives' [True]) $ do
v <- newIORefInt 10
registerInvariant (inspectIORef v >>= \x -> when (x < 5) (throwM Overflow))
writeIORef v 1
pure True
]
]
-------------------------------------------------------------------------------

13
dejafu/Test/DejaFu.hs
View File

@ -47,12 +47,15 @@ and, for each, a summarised execution trace leading to that result:
* Each \"-\" represents one \"step\" of the computation.
__Conditions:__ A program may fail to terminate in a way which
produces a value. dejafu can detect two such cases:
produces a value. There are three such cases:
* 'Deadlock', if every thread is blocked.
* 'UncaughtException', if the main thread is killed by an exception.
* 'InvariantFailure', if an invariant (created with
'registerInvariant') failed.
__Beware of 'liftIO':__ dejafu works by running your test case lots of
times with different schedules. If you use 'liftIO' at all, make sure
that any @IO@ you perform is deterministic when executed in the same
@ -76,6 +79,13 @@ module Test.DejaFu
, withTeardown
, withSetupAndTeardown
-- ** Invariants
, Invariant
, registerInvariant
, inspectIORef
, inspectMVar
, inspectTVar
-- * Unit testing
, autocheck
@ -182,6 +192,7 @@ Helper functions to identify conditions.
, isAbort
, isDeadlock
, isUncaughtException
, isInvariantFailure
-- * Property testing

49
dejafu/Test/DejaFu/Conc.hs
View File

@ -25,6 +25,13 @@ module Test.DejaFu.Conc
, withTeardown
, withSetupAndTeardown
-- ** Invariants
, Invariant
, registerInvariant
, inspectIORef
, inspectMVar
, inspectTVar
-- * Executing concurrent programs
, Snapshot
, MemType(..)
@ -53,6 +60,7 @@ import Control.Exception (MaskingState(..))
import Test.DejaFu.Conc.Internal.Common
import Test.DejaFu.Conc.Internal.Program
import Test.DejaFu.Conc.Internal.STM (ModelTVar)
import Test.DejaFu.Schedule
import Test.DejaFu.Types
import Test.DejaFu.Utils
@ -142,3 +150,44 @@ withSetupAndTeardown
-> Program (WithSetupAndTeardown x y) n a
withSetupAndTeardown setup teardown =
withTeardown teardown . withSetup setup
-------------------------------------------------------------------------------
-- Invariants
-- | Call this in the setup phase to register new invariant which will
-- be checked after every scheduling point in the main phase.
-- Invariants are atomic actions which can inspect the shared state of
-- your computation.
--
-- If the invariant throws an exception, the execution will be aborted
-- with n @InvariantFailure@. Any teardown action will still be run.
--
-- @since unreleased
registerInvariant :: Invariant n a -> Program Basic n ()
registerInvariant inv = ModelConc (\c -> ANewInvariant (() <$ inv) (c ()))
-- | Read the content of an @IORef@.
--
-- This returns the globally visible value, which may not be the same
-- as the value visible to any particular thread when using a memory
-- model other than 'SequentialConsistency'.
--
-- @since unreleased
inspectIORef :: ModelIORef n a -> Invariant n a
inspectIORef = Invariant . IInspectIORef
-- | Read the content of an @MVar@.
--
-- This is essentially @tryReadMVar@.
--
-- @since unreleased
inspectMVar :: ModelMVar n a -> Invariant n (Maybe a)
inspectMVar = Invariant . IInspectMVar
-- | Read the content of a @TVar@.
--
-- This is essentially @readTVar@.
--
-- @since unreleased
inspectTVar :: ModelTVar n a -> Invariant n a
inspectTVar = Invariant . IInspectTVar

166
dejafu/Test/DejaFu/Conc/Internal.hs
View File

@ -1,4 +1,5 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
@ -9,7 +10,7 @@
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : experimental
-- Portability : FlexibleContexts, MultiWayIf, RankNTypes, RecordWildCards
-- Portability : FlexibleContexts, LambdaCase, MultiWayIf, RankNTypes, RecordWildCards
--
-- Concurrent monads with a fixed scheduler: internal types and
-- functions. This module is NOT considered to form part of the public
@ -23,7 +24,7 @@ import qualified Control.Monad.Catch as E
import qualified Control.Monad.Conc.Class as C
import Data.Foldable (foldrM)
import Data.Functor (void)
import Data.List (sortOn)
import Data.List (nub, partition, sortOn)
import qualified Data.Map.Strict as M
import Data.Maybe (isJust, isNothing)
import Data.Monoid ((<>))
@ -61,7 +62,8 @@ data CResult n g a = CResult
-- state, returning a Condition reason on error. Also returned is the
-- final state of the scheduler, and an execution trace.
runConcurrency :: (C.MonadConc n, HasCallStack)
=> Bool
=> [Invariant n ()]
-> Bool
-> Scheduler g
-> MemType
-> g
@ -69,12 +71,14 @@ runConcurrency :: (C.MonadConc n, HasCallStack)
-> Int
-> ModelConc n a
-> n (CResult n g a)
runConcurrency forSnapshot sched memtype g idsrc caps ma = do
let ctx = Context { cSchedState = g
, cIdSource = idsrc
, cThreads = M.empty
, cWriteBuf = emptyBuffer
, cCaps = caps
runConcurrency invariants forSnapshot sched memtype g idsrc caps ma = do
let ctx = Context { cSchedState = g
, cIdSource = idsrc
, cThreads = M.empty
, cWriteBuf = emptyBuffer
, cCaps = caps
, cInvariants = InvariantContext { icActive = invariants, icBlocked = [] }
, cNewInvariants = []
}
(c, ref) <- runRefCont AStop (Just . Right) (runModelConc ma)
let threads0 = launch' Unmasked initialThread (const c) (cThreads ctx)
@ -114,11 +118,13 @@ killAllThreads ctx =
-- | The context a collection of threads are running in.
data Context n g = Context
{ cSchedState :: g
, cIdSource :: IdSource
, cThreads :: Threads n
, cWriteBuf :: WriteBuffer n
, cCaps :: Int
{ cSchedState :: g
, cIdSource :: IdSource
, cThreads :: Threads n
, cWriteBuf :: WriteBuffer n
, cCaps :: Int
, cInvariants :: InvariantContext n
, cNewInvariants :: [Invariant n ()]
}
-- | Run a collection of threads, until there are no threads left.
@ -191,10 +197,13 @@ runThreads forSnapshot sched memtype ref = schedule (const $ pure ()) Seq.empty
if forSnapshot
then restore threads' >> actionSnap threads'
else restore threads'
let ctx' = fixContext chosen res ctx
let ctx' = fixContext chosen actOrTrc res ctx
case res of
Succeeded _ ->
schedule restore' sofar' prior' ctx'
Succeeded _ -> checkInvariants (cInvariants ctx') >>= \case
Right ic ->
schedule restore' sofar' prior' ctx' { cInvariants = ic }
Left exc ->
die (InvariantFailure exc) restore' sofar' prior' ctx'
Failed failure ->
die failure restore' sofar' prior' ctx'
Snap _ ->
@ -205,17 +214,22 @@ runThreads forSnapshot sched memtype ref = schedule (const $ pure ()) Seq.empty
getPrior a = Just (chosen, a)
-- | Apply the context update from stepping an action.
fixContext :: ThreadId -> What n g -> Context n g -> Context n g
fixContext chosen (Succeeded ctx@Context{..}) _ =
fixContext :: ThreadId -> ThreadAction -> What n g -> Context n g -> Context n g
fixContext chosen act (Succeeded ctx@Context{..}) _ =
ctx { cThreads = delCommitThreads $
if (interruptible <$> M.lookup chosen cThreads) /= Just False
then unblockWaitingOn chosen cThreads
else cThreads
, cInvariants = unblockInvariants act cInvariants
}
fixContext _ act (Failed _) ctx@Context{..} =
ctx { cThreads = delCommitThreads cThreads
, cInvariants = unblockInvariants act cInvariants
}
fixContext _ act (Snap ctx@Context{..}) _ =
ctx { cThreads = delCommitThreads cThreads
, cInvariants = unblockInvariants act cInvariants
}
fixContext _ (Failed _) ctx@Context{..} =
ctx { cThreads = delCommitThreads cThreads }
fixContext _ (Snap ctx@Context{..}) _ =
ctx { cThreads = delCommitThreads cThreads }
-- | @unblockWaitingOn tid@ unblocks every thread blocked in a
-- @throwTo tid@.
@ -587,6 +601,16 @@ stepThread _ _ _ _ tid (AStop na) = \ctx@Context{..} -> do
, const (pure ())
)
-- register an invariant to be checked in the next execution
stepThread _ _ _ _ tid (ANewInvariant inv c) = \ctx@Context{..} ->
pure ( Succeeded ctx
{ cThreads = goto c tid cThreads
, cNewInvariants = inv : cNewInvariants
}
, RegisterInvariant
, const (pure ())
)
-- | Handle an exception being thrown from an @AAtom@, @AThrow@, or
-- @AThrowTo@.
stepThrow :: (C.MonadConc n, Exception e)
@ -630,3 +654,99 @@ synchronised :: C.MonadConc n
synchronised ma ctx@Context{..} = do
writeBarrier cWriteBuf
ma ctx { cWriteBuf = emptyBuffer }
--------------------------------------------------------------------------------
-- * Invariants
-- | The state of the invariants
data InvariantContext n = InvariantContext
{ icActive :: [Invariant n ()]
, icBlocked :: [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
}
-- | @unblockInvariants act@ unblocks every invariant which could have
-- its result changed by @act@.
unblockInvariants :: ThreadAction -> InvariantContext n -> InvariantContext n
unblockInvariants act ic = InvariantContext active blocked where
active = map fst unblocked ++ icActive ic
(unblocked, blocked) = (`partition` icBlocked ic) $
\(_, (ioridsB, mvidsB, tvidsB)) ->
maybe False (`elem` ioridsB) (iorefOf (simplifyAction act)) ||
maybe False (`elem` mvidsB) (mvarOf (simplifyAction act)) ||
any (`elem` tvidsB) (tvarsOf act)
-- | Check all active invariants, returning an arbitrary failure if
-- multiple ones fail.
checkInvariants :: C.MonadConc n
=> InvariantContext n
-> n (Either E.SomeException (InvariantContext n))
checkInvariants ic = go (icActive ic) >>= \case
Right blocked -> pure (Right (InvariantContext [] (blocked ++ icBlocked ic)))
Left exc -> pure (Left exc)
where
go (inv:is) = checkInvariant inv >>= \case
Right o -> fmap ((inv,o):) <$> go is
Left exc -> pure (Left exc)
go [] = pure (Right [])
-- | Check an invariant.
checkInvariant :: C.MonadConc n
=> Invariant n a
-> n (Either E.SomeException ([IORefId], [MVarId], [TVarId]))
checkInvariant inv = doInvariant inv >>= \case
(Right _, iorefs, mvars, tvars) -> pure (Right (iorefs, mvars, tvars))
(Left exc, _, _, _) -> pure (Left exc)
-- | Run an invariant (more primitive)
doInvariant :: C.MonadConc n
=> Invariant n a
-> n (Either E.SomeException a, [IORefId], [MVarId], [TVarId])
doInvariant inv = do
(c, ref) <- runRefCont IStop (Just . Right) (runInvariant inv)
(iorefs, mvars, tvars) <- go ref c [] [] []
val <- C.readIORef ref
pure (efromJust val, nub iorefs, nub mvars, nub tvars)
where
go ref act iorefs mvars tvars = do
(res, iorefs', mvars', tvars') <- stepInvariant act
let newIORefs = iorefs' ++ iorefs
let newMVars = mvars' ++ mvars
let newTVars = tvars' ++ tvars
case res of
Right (Just act') ->
go ref act' newIORefs newMVars newTVars
Right Nothing ->
pure (newIORefs, newMVars, newTVars)
Left exc -> do
C.writeIORef ref (Just (Left exc))
pure (newIORefs, newMVars, newTVars)
-- | Run an invariant for one step
stepInvariant :: C.MonadConc n
=> IAction n
-> n (Either E.SomeException (Maybe (IAction n)), [IORefId], [MVarId], [TVarId])
stepInvariant (IInspectIORef ioref@ModelIORef{..} k) = do
a <- readIORefGlobal ioref
pure (Right (Just (k a)), [iorefId], [], [])
stepInvariant (IInspectMVar ModelMVar{..} k) = do
a <- C.readIORef mvarRef
pure (Right (Just (k a)), [], [mvarId], [])
stepInvariant (IInspectTVar ModelTVar{..} k) = do
a <- C.readIORef tvarRef
pure (Right (Just (k a)), [], [], [tvarId])
stepInvariant (ICatch h nx k) = doInvariant nx >>= \case
(Right a, iorefs, mvars, tvars) ->
pure (Right (Just (k a)), iorefs, mvars, tvars)
(Left exc, iorefs, mvars, tvars) -> case E.fromException exc of
Just exc' -> doInvariant (h exc') >>= \case
(Right a, iorefs', mvars', tvars') ->
pure (Right (Just (k a)), iorefs' ++ iorefs, mvars' ++ mvars, tvars' ++ tvars)
(Left exc'', iorefs', mvars', tvars') ->
pure (Left exc'', iorefs' ++ iorefs, mvars' ++ mvars, tvars' ++ tvars)
Nothing -> pure (Left exc, iorefs, mvars, tvars)
stepInvariant (IThrow exc) =
pure (Left (toException exc), [], [], [])
stepInvariant (IStop finalise) = do
finalise
pure (Right Nothing, [], [], [])

58
dejafu/Test/DejaFu/Conc/Internal/Common.hs
View File

@ -16,10 +16,12 @@
module Test.DejaFu.Conc.Internal.Common where
import Control.Exception (Exception, MaskingState(..))
import Control.Monad.Catch (MonadCatch(..), MonadThrow(..))
import qualified Control.Monad.Conc.Class as C
import qualified Control.Monad.Fail as Fail
import Data.Map.Strict (Map)
import Test.DejaFu.Conc.Internal.STM (ModelSTM)
import Test.DejaFu.Conc.Internal.STM (ModelSTM, ModelTVar)
import Test.DejaFu.Types
--------------------------------------------------------------------------------
@ -125,7 +127,7 @@ data ModelTicket a = ModelTicket
}
--------------------------------------------------------------------------------
-- * Primitive Actions
-- ** Primitive Actions
-- | Scheduling is done in terms of a trace of 'Action's. Blocking can
-- only occur as a result of an action, and they cover (most of) the
@ -171,8 +173,10 @@ data Action n =
| ACommit ThreadId IORefId
| AStop (n ())
| ANewInvariant (Invariant n ()) (Action n)
--------------------------------------------------------------------------------
-- * Scheduling & Traces
-- ** Scheduling & Traces
-- | Look as far ahead in the given continuation as possible.
lookahead :: Action n -> Lookahead
@ -209,3 +213,51 @@ lookahead (AYield _) = WillYield
lookahead (ADelay n _) = WillThreadDelay n
lookahead (AReturn _) = WillReturn
lookahead (AStop _) = WillStop
lookahead (ANewInvariant _ _) = WillRegisterInvariant
-------------------------------------------------------------------------------
-- * Invariants
-- | Invariants are atomic actions which can inspect the shared state
-- of your computation, and terminate it on failure. Invariants have
-- no visible effects, and are checked after each scheduling point.
--
-- To be checked, an invariant must be created during the setup phase
-- of your 'Program', using 'Test.DejaFu.Conc.registerInvariant'. The
-- invariant will then be checked in the main phase (but not in the
-- setup or teardown phase). As a consequence of this, any shared
-- state you want your invariant to check must also be created in the
-- setup phase, and passed into the main phase as a parameter.
--
-- @since unreleased
newtype Invariant n a = Invariant { runInvariant :: (a -> IAction n) -> IAction n }
instance Functor (Invariant n) where
fmap f m = Invariant $ \c -> runInvariant m (c . f)
instance Applicative (Invariant n) where
pure x = Invariant $ \c -> c x
f <*> v = Invariant $ \c -> runInvariant f (\g -> runInvariant v (c . g))
instance Monad (Invariant n) where
return = pure
fail = Fail.fail
m >>= k = Invariant $ \c -> runInvariant m (\x -> runInvariant (k x) c)
instance Fail.MonadFail (Invariant n) where
fail e = Invariant $ \_ -> IThrow (MonadFailException e)
instance MonadThrow (Invariant n) where
throwM e = Invariant $ \_ -> IThrow e
instance MonadCatch (Invariant n) where
catch stm handler = Invariant $ ICatch handler stm
-- | Invariants are represented as a sequence of primitive actions.
data IAction n
= forall a. IInspectIORef (ModelIORef n a) (a -> IAction n)
| forall a. IInspectMVar (ModelMVar n a) (Maybe a -> IAction n)
| forall a. IInspectTVar (ModelTVar n a) (a -> IAction n)
| forall a e. Exception e => ICatch (e -> Invariant n a) (Invariant n a) (a -> IAction n)
| forall e. Exception e => IThrow e
| IStop (n ())

6
dejafu/Test/DejaFu/Conc/Internal/Memory.hs
View File

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

19
dejafu/Test/DejaFu/Conc/Internal/Program.hs
View File

@ -180,7 +180,7 @@ runConcurrent :: C.MonadConc n
-> Program pty n a
-> n (Either Condition a, s, Trace)
runConcurrent sched memtype s ma@(ModelConc _) = do
res <- runConcurrency False sched memtype s initialIdSource 2 ma
res <- runConcurrency [] False sched memtype s initialIdSource 2 ma
out <- efromJust <$> C.readIORef (finalRef res)
pure ( out
, cSchedState (finalContext res)
@ -276,7 +276,7 @@ runSnapshot
-> Snapshot pty n a
-> n (Either Condition a, s, Trace)
runSnapshot sched memtype s (WS SimpleSnapshot{..}) = do
let context = snapContext { cSchedState = s }
let context = fromSnapContext s snapContext
CResult{..} <- runConcurrencyWithSnapshot sched memtype context snapRestore snapNext
out <- efromJust <$> C.readIORef finalRef
pure ( out
@ -284,7 +284,7 @@ runSnapshot sched memtype s (WS SimpleSnapshot{..}) = do
, F.toList finalTrace
)
runSnapshot sched memtype s (WSAT SimpleSnapshot{..} teardown) = do
let context = snapContext { cSchedState = s }
let context = fromSnapContext s snapContext
intermediateResult <- runConcurrencyWithSnapshot sched memtype context snapRestore snapNext
let idsrc = cIdSource (finalContext intermediateResult)
out1 <- efromJust <$> C.readIORef (finalRef intermediateResult)
@ -357,7 +357,18 @@ simpleRunConcurrency ::(C.MonadConc n, HasCallStack)
-> ModelConc n a
-> n (CResult n () a)
simpleRunConcurrency forSnapshot idsrc =
runConcurrency forSnapshot roundRobinSchedNP SequentialConsistency () idsrc 2
runConcurrency [] forSnapshot roundRobinSchedNP SequentialConsistency () idsrc 2
-- | Make a new context from a snapshot context.
fromSnapContext :: g -> Context n s -> Context n g
fromSnapContext g ctx@Context{..} = ctx
{ cSchedState = g
, cInvariants = InvariantContext
{ icActive = cNewInvariants
, icBlocked = []
}
, cNewInvariants = []
}
wrap :: (((a -> Action n) -> Action n) -> ((a -> Action n) -> Action n)) -> ModelConc n a -> ModelConc n a
wrap f = ModelConc . f . runModelConc

1
dejafu/Test/DejaFu/Internal.hs
View File

@ -198,6 +198,7 @@ rewind (ResetMasking b m) = WillResetMasking b m
rewind LiftIO = WillLiftIO
rewind Return = WillReturn
rewind Stop = WillStop
rewind RegisterInvariant = WillRegisterInvariant
-- | Check if an operation could enable another thread.
willRelease :: Lookahead -> Bool

23
dejafu/Test/DejaFu/Types.hs
View File

@ -194,6 +194,8 @@ data ThreadAction =
-- ^ A 'return' or 'pure' action was executed.
| Stop
-- ^ Cease execution and terminate.
| RegisterInvariant
-- ^ Register an invariant.
deriving (Eq, Generic, Show)
-- this makes me sad
@ -236,6 +238,7 @@ instance NFData ThreadAction where
rnf LiftIO = ()
rnf Return = ()
rnf Stop = ()
rnf RegisterInvariant = ()
-- | A one-step look-ahead at what a thread will do next.
--
@ -316,6 +319,8 @@ data Lookahead =
-- ^ Will execute a 'return' or 'pure' action.
| WillStop
-- ^ Will cease execution and terminate.
| WillRegisterInvariant
-- ^ Will register an invariant
deriving (Eq, Generic, Show)
-- this also makes me sad
@ -353,6 +358,7 @@ instance NFData Lookahead where
rnf WillLiftIO = ()
rnf WillReturn = ()
rnf WillStop = ()
rnf WillRegisterInvariant = ()
-- | All the actions that an STM transaction can perform.
--
@ -424,7 +430,8 @@ instance NFData Decision
-- didn't produce a value.
--
-- The @Eq@, @Ord@, and @NFData@ instances compare/evaluate the
-- exception with @show@ in the @UncaughtException@ case.
-- exception with @show@ in the @UncaughtException@ and
-- @InvariantFailure@ cases.
--
-- @since unreleased
data Condition
@ -437,12 +444,15 @@ data Condition
-- ^ Every thread is blocked
| UncaughtException SomeException
-- ^ An uncaught exception bubbled to the top of the computation.
| InvariantFailure SomeException
-- ^ An uncaught exception caused an invariant to fail.
deriving (Show, Generic)
instance Eq Condition where
Abort == Abort = True
Deadlock == Deadlock = True
(UncaughtException e1) == (UncaughtException e2) = show e1 == show e2
(InvariantFailure e1) == (InvariantFailure e2) = show e1 == show e2
_ == _ = False
instance Ord Condition where
@ -450,10 +460,12 @@ instance Ord Condition where
transform :: Condition -> (Int, Maybe String)
transform Abort = (1, Nothing)
transform Deadlock = (2, Nothing)
transform (UncaughtException e) = (4, Just (show e))
transform (UncaughtException e) = (3, Just (show e))
transform (InvariantFailure e) = (4, Just (show e))
instance NFData Condition where
rnf (UncaughtException e) = rnf (show e)
rnf (InvariantFailure e) = rnf (show e)
rnf f = f `seq` ()
-- | Check if a condition is an @Abort@.
@ -477,6 +489,13 @@ isUncaughtException :: Condition -> Bool
isUncaughtException (UncaughtException _) = True
isUncaughtException _ = False
-- | Check if a condition is an @InvariantFailure@
--
-- @since unreleased
isInvariantFailure :: Condition -> Bool
isInvariantFailure (InvariantFailure _) = True
isInvariantFailure _ = False
-------------------------------------------------------------------------------
-- * Errors

1
dejafu/Test/DejaFu/Utils.hs
View File

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

6
hunit-dejafu/Test/HUnit/DejaFu.hs
View File

@ -53,6 +53,12 @@ module Test.HUnit.DejaFu
, withSetup
, withTeardown
, withSetupAndTeardown
-- *** Invariants
, Invariant
, registerInvariant
, inspectIORef
, inspectMVar
, inspectTVar
-- * Refinement property testing
, testProperty

6
tasty-dejafu/Test/Tasty/DejaFu.hs
View File

@ -53,6 +53,12 @@ module Test.Tasty.DejaFu
, withSetup
, withTeardown
, withSetupAndTeardown
-- *** Invariants
, Invariant
, registerInvariant
, inspectIORef
, inspectMVar
, inspectTVar
-- * Refinement property testing
, testProperty