diff --git a/Test/DejaFu/Deterministic.hs b/Test/DejaFu/Deterministic.hs index 06bde55..6290cda 100755 --- a/Test/DejaFu/Deterministic.hs +++ b/Test/DejaFu/Deterministic.hs @@ -47,6 +47,9 @@ module Test.DejaFu.Deterministic -- * Testing , _concNoTest + , _concKnowsAbout + , _concForgets + , _concAllKnown -- * Execution traces , Trace @@ -70,6 +73,7 @@ import Data.STRef (STRef, newSTRef) import Test.DejaFu.Deterministic.Internal import Test.DejaFu.Deterministic.Schedule import Test.DejaFu.STM (STMLike, runTransactionST) +import Test.DejaFu.STM.Internal (CTVar(..)) import qualified Control.Monad.Catch as Ca import qualified Control.Monad.Conc.Class as C @@ -117,6 +121,9 @@ instance C.MonadConc (Conc t) where modifyCRef = modifyCRef atomically = atomically _concNoTest = _concNoTest + _concKnowsAbout = _concKnowsAbout + _concForgets = _concForgets + _concAllKnown = _concAllKnown fixed :: Fixed (ST t) (STRef t) (STMLike t) fixed = Wrapper refST $ \ma -> cont (\c -> ALift $ c <$> ma) @@ -284,6 +291,22 @@ getNumCapabilities = return 1 _concNoTest :: Conc t a -> Conc t a _concNoTest ma = C $ cont $ \c -> ANoTest (unC ma) c +-- | Record that the referenced variable is known by the current thread. +_concKnowsAbout :: Either (CVar t a) (CTVar t (STRef t) a) -> Conc t () +_concKnowsAbout (Left (Var (cvarid, _))) = C $ cont $ \c -> AKnowsAbout (Left cvarid) (c ()) +_concKnowsAbout (Right (V (ctvarid, _))) = C $ cont $ \c -> AKnowsAbout (Right ctvarid) (c ()) + +-- | Record that the referenced variable will never be touched by the +-- current thread. +_concForgets :: Either (CVar t a) (CTVar t (STRef t) a) -> Conc t () +_concForgets (Left (Var (cvarid, _))) = C $ cont $ \c -> AForgets (Left cvarid) (c ()) +_concForgets (Right (V (ctvarid, _))) = C $ cont $ \c -> AForgets (Right ctvarid) (c ()) + +-- | Record that all 'CVar's and 'CTVar's known by the current thread +-- have been passed to '_concKnowsAbout'. +_concAllKnown :: Conc t () +_concAllKnown = C $ cont $ \c -> AAllKnown (c ()) + -- | Run a concurrent computation with a given 'Scheduler' and initial -- state, returning a failure reason on error. Also returned is the -- final state of the scheduler, and an execution trace. diff --git a/Test/DejaFu/Deterministic/IO.hs b/Test/DejaFu/Deterministic/IO.hs index ae3cca1..25b4058 100644 --- a/Test/DejaFu/Deterministic/IO.hs +++ b/Test/DejaFu/Deterministic/IO.hs @@ -51,6 +51,9 @@ module Test.DejaFu.Deterministic.IO -- * Testing , _concNoTest + , _concKnowsAbout + , _concForgets + , _concAllKnown -- * Execution traces , Trace @@ -72,6 +75,7 @@ import Data.IORef (IORef, newIORef) import Test.DejaFu.Deterministic.Internal import Test.DejaFu.Deterministic.Schedule import Test.DejaFu.STM (STMLike, runTransactionIO) +import Test.DejaFu.STM.Internal (CTVar(..)) import qualified Control.Monad.Catch as Ca import qualified Control.Monad.Conc.Class as C @@ -120,6 +124,9 @@ instance C.MonadConc (ConcIO t) where modifyCRef = modifyCRef atomically = atomically _concNoTest = _concNoTest + _concKnowsAbout = _concKnowsAbout + _concForgets = _concForgets + _concAllKnown = _concAllKnown fixed :: Fixed IO IORef (STMLike t) fixed = Wrapper refIO $ unC . liftIO @@ -285,6 +292,22 @@ getNumCapabilities = return 1 _concNoTest :: ConcIO t a -> ConcIO t a _concNoTest ma = C $ cont $ \c -> ANoTest (unC ma) c +-- | Record that the referenced variable is known by the current thread. +_concKnowsAbout :: Either (CVar t a) (CTVar t IORef a) -> ConcIO t () +_concKnowsAbout (Left (Var (cvarid, _))) = C $ cont $ \c -> AKnowsAbout (Left cvarid) (c ()) +_concKnowsAbout (Right (V (ctvarid, _))) = C $ cont $ \c -> AKnowsAbout (Right ctvarid) (c ()) + +-- | Record that the referenced variable will never be touched by the +-- current thread. +_concForgets :: Either (CVar t a) (CTVar t IORef a) -> ConcIO t () +_concForgets (Left (Var (cvarid, _))) = C $ cont $ \c -> AForgets (Left cvarid) (c ()) +_concForgets (Right (V (ctvarid, _))) = C $ cont $ \c -> AForgets (Right ctvarid) (c ()) + +-- | Record that all 'CVar's and 'CTVar's known by the current thread +-- have been passed to '_concKnowsAbout'. +_concAllKnown :: ConcIO t () +_concAllKnown = C $ cont $ \c -> AAllKnown (c ()) + -- | Run a concurrent computation with a given 'Scheduler' and initial -- state, returning an failure reason on error. Also returned is the -- final state of the scheduler, and an execution trace. diff --git a/Test/DejaFu/Deterministic/Internal.hs b/Test/DejaFu/Deterministic/Internal.hs index d0aaf01..9e2b559 100755 --- a/Test/DejaFu/Deterministic/Internal.hs +++ b/Test/DejaFu/Deterministic/Internal.hs @@ -173,6 +173,9 @@ stepThread fixed runconc runstm action idSource tid threads = case action of AMasking m ma c -> stepMasking m ma c AResetMask b1 b2 m c -> stepResetMask b1 b2 m c ANoTest ma a -> stepNoTest ma a + AKnowsAbout v c -> stepKnowsAbout v c + AForgets v c -> stepForgets v c + AAllKnown c -> stepAllKnown c AStop -> stepStop where @@ -320,5 +323,14 @@ stepThread fixed runconc runstm action idSource tid threads = case action of Right a' -> Right (goto (c a') tid threads, idSource', NoTest) _ -> Left FailureInNoTest + -- | Record that a variable is known about. + stepKnowsAbout v c = error "'stepKnowsAbout' not yet implemented." + + -- | Record that a variable will never be touched again. + stepForgets v c = error "'stepForgets' not yet implemented." + + -- | Record that all shared variables are known. + stepAllKnown c = error "'stepAllKnown' not yet implemented." + -- | Kill the current thread. stepStop = return $ Right (kill tid threads, idSource, Stop) diff --git a/Test/DejaFu/Deterministic/Internal/Common.hs b/Test/DejaFu/Deterministic/Internal/Common.hs index c883940..70dce4d 100644 --- a/Test/DejaFu/Deterministic/Internal/Common.hs +++ b/Test/DejaFu/Deterministic/Internal/Common.hs @@ -57,6 +57,9 @@ data Action n r s = | APopCatching (Action n r s) | forall a. AMasking MaskingState ((forall b. M n r s b -> M n r s b) -> M n r s a) (a -> Action n r s) | AResetMask Bool Bool MaskingState (Action n r s) + | AKnowsAbout (Either CVarId CTVarId) (Action n r s) + | AForgets (Either CVarId CTVarId) (Action n r s) + | AAllKnown (Action n r s) | AStop -------------------------------------------------------------------------------- diff --git a/Test/DejaFu/Deterministic/Internal/Threading.hs b/Test/DejaFu/Deterministic/Internal/Threading.hs index 119f8bf..945d2bc 100644 --- a/Test/DejaFu/Deterministic/Internal/Threading.hs +++ b/Test/DejaFu/Deterministic/Internal/Threading.hs @@ -31,6 +31,12 @@ data Thread n r s = Thread -- ^ Stack of exception handlers , _masking :: MaskingState -- ^ The exception masking state. + , _known :: [Either CVarId CTVarId] + -- ^ Shared variables the thread knows about. + , _fullknown :: Bool + -- ^ Whether the referenced variables of the thread are completely + -- known. If every thread has _fullknown == True, then turn on + -- detection of nonglobal deadlock. } -------------------------------------------------------------------------------- @@ -82,7 +88,7 @@ launch parent tid a threads = launch' mask tid a threads where -- | Start a thread with the given ID and masking state. This must not already be in use! launch' :: MaskingState -> ThreadId -> ((forall b. M n r s b -> M n r s b) -> Action n r s) -> Threads n r s -> Threads n r s launch' mask tid a = M.insert tid thread where - thread = Thread { _continuation = a umask, _blocking = Nothing, _handlers = [], _masking = mask } + thread = Thread { _continuation = a umask, _blocking = Nothing, _handlers = [], _masking = mask, _known = [], _fullknown = False } umask mb = resetMask True Unmasked >> mb >>= \b -> resetMask False mask >> return b resetMask typ m = cont $ \k -> AResetMask typ True m $ k () @@ -108,3 +114,18 @@ wake blockedOn threads = (M.map unblock threads, M.keys $ M.filter isBlocked thr isBlocked thread = case (_blocking thread, blockedOn) of (Just (OnCTVar ctvids), OnCTVar blockedOn') -> ctvids `intersect` blockedOn' /= [] (theblock, _) -> theblock == Just blockedOn + +-- | Record that a thread knows about a shared variable. +knows :: Either CVarId CTVarId -> ThreadId -> Threads n r s -> Threads n r s +knows theid = M.alter go where + go (Just thread) = Just $ thread { _known = if theid `elem` _known thread then _known thread else theid : _known thread } + +-- | Forget about a shared variable. +forgets :: Either CVarId CTVarId -> ThreadId -> Threads n r s -> Threads n r s +forgets theid = M.alter go where + go (Just thread) = Just $ thread { _known = filter (/=theid) $ _known thread } + +-- | Record that a thread's shared variable state is fully known. +fullknown :: ThreadId -> Threads n r s -> Threads n r s +fullknown = M.alter go where + go (Just thread) = Just $ thread { _fullknown = True }