From 0ce6d541e9397d91c7598247209d2e58df8e490a Mon Sep 17 00:00:00 2001 From: Michael Walker Date: Thu, 22 Feb 2018 00:22:15 +0000 Subject: [PATCH] Automatically snapshot (when possible) in SCT --- dejafu-tests/lib/Integration/MultiThreaded.hs | 9 +++++ .../lib/Integration/SingleThreaded.hs | 13 +++++++ dejafu/CHANGELOG.rst | 9 ++++- dejafu/Test/DejaFu/Conc.hs | 31 ++++++++++++++++- dejafu/Test/DejaFu/SCT.hs | 34 ++++++++++++------- dejafu/Test/DejaFu/SCT/Internal/DPOR.hs | 22 +++++++----- 6 files changed, 94 insertions(+), 24 deletions(-) diff --git a/dejafu-tests/lib/Integration/MultiThreaded.hs b/dejafu-tests/lib/Integration/MultiThreaded.hs index 50fa53e..a85a692 100644 --- a/dejafu-tests/lib/Integration/MultiThreaded.hs +++ b/dejafu-tests/lib/Integration/MultiThreaded.hs @@ -282,6 +282,15 @@ hacksTests = toTestList putMVar trigger () readCRef ref + , djfuT "Bound threads created on the inside are bound on the outside" (gives' [True]) $ do + (out, trigger) <- dontCheck Nothing $ do + v <- newEmptyMVar + o <- newEmptyMVar + _ <- forkOS (takeMVar v >> isCurrentThreadBound >>= putMVar o) + pure (o, v) + putMVar trigger () + takeMVar out + , djfuT "Thread IDs are consistent between the inner action and the outside" (sometimesFailsWith isUncaughtException) $ do (tid, trigger) <- dontCheck Nothing $ do me <- myThreadId diff --git a/dejafu-tests/lib/Integration/SingleThreaded.hs b/dejafu-tests/lib/Integration/SingleThreaded.hs index 040aadd..630c184 100644 --- a/dejafu-tests/lib/Integration/SingleThreaded.hs +++ b/dejafu-tests/lib/Integration/SingleThreaded.hs @@ -13,6 +13,7 @@ import Control.Concurrent.Classy import Control.Monad (replicateM_) import Control.Monad.IO.Class (liftIO) import qualified Data.IORef as IORef +import System.Random (mkStdGen) import Test.DejaFu.Conc (dontCheck, subconcurrency) import Common @@ -273,6 +274,18 @@ hacksTests = toTestList let ntimes = fromIntegral defaultLengthBound * 5 dontCheck Nothing $ replicateM_ ntimes (pure ()) pure True + + -- we use 'randomly' here because we specifically want to compare + -- multiple executions with snapshotting + , 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 + pure r + readCRef r + ] ] ] diff --git a/dejafu/CHANGELOG.rst b/dejafu/CHANGELOG.rst index c396d51..c9b5af9 100644 --- a/dejafu/CHANGELOG.rst +++ b/dejafu/CHANGELOG.rst @@ -24,9 +24,16 @@ Added * (:pull:`219`) A snapshotting approach based on ``Test.DejaFu.Conc.dontCheck``: - * ``Test.DejaFu.Conc.canDCSnapshot`` * ``Test.DejaFu.Conc.runForDCSnapshot`` * ``Test.DejaFu.Conc.runWithDCSnapshot`` + * ``Test.DejaFu.Conc.canDCSnapshot`` + * ``Test.DejaFu.Conc.threadsFromDCSnapshot`` + +Changed +~~~~~~~ + +* (:pull:`219`) SCT functions automatically use the snapshotting + mechanism when possible. 1.0.0.2 (2018-02-18) diff --git a/dejafu/Test/DejaFu/Conc.hs b/dejafu/Test/DejaFu/Conc.hs index b626234..cc8c8be 100755 --- a/dejafu/Test/DejaFu/Conc.hs +++ b/dejafu/Test/DejaFu/Conc.hs @@ -34,6 +34,8 @@ module Test.DejaFu.Conc , DCSnapshot , runForDCSnapshot , runWithDCSnapshot + , canDCSnapshot + , threadsFromDCSnapshot -- * Execution traces , Trace @@ -59,13 +61,17 @@ import qualified Control.Monad.Ref as Re import Control.Monad.Trans.Class (MonadTrans(..)) import qualified Data.Foldable as F import Data.IORef (IORef) +import Data.List (partition) +import qualified Data.Map.Strict as M +import Data.Maybe (isNothing) import Test.DejaFu.Schedule import qualified Control.Monad.Conc.Class as C import Test.DejaFu.Conc.Internal import Test.DejaFu.Conc.Internal.Common import Test.DejaFu.Conc.Internal.STM -import Test.DejaFu.Conc.Internal.Threading (Threads) +import Test.DejaFu.Conc.Internal.Threading (Thread(_blocking), + Threads) import Test.DejaFu.Internal import Test.DejaFu.Types import Test.DejaFu.Utils @@ -299,6 +305,10 @@ data DCSnapshot r n a = DCSnapshot -- If this program does not contain a legal use of 'dontCheck', then -- the result will be @Nothing@. -- +-- If you are using the SCT functions on an action which contains a +-- 'dontCheck', snapshotting will be handled for you, without you +-- needing to call this function yourself. +-- -- @since unreleased runForDCSnapshot :: (C.MonadConc n, MonadRef r n) => ConcT r n a @@ -314,6 +324,10 @@ runForDCSnapshot ma = do -- | Like 'runConcurrent', but uses a 'DCSnapshot' produced by -- 'runForDCSnapshot' to skip the 'dontCheck' work. -- +-- If you are using the SCT functions on an action which contains a +-- 'dontCheck', snapshotting will be handled for you, without you +-- needing to call this function yourself. +-- -- @since unreleased runWithDCSnapshot :: (C.MonadConc n, MonadRef r n) => Scheduler s @@ -331,3 +345,18 @@ runWithDCSnapshot sched memtype s snapshot = do , cSchedState (finalContext res) , F.toList (finalTrace res) ) + +-- | Check if a 'DCSnapshot' can be taken from this computation. +-- +-- @since unreleased +canDCSnapshot :: ConcT r n a -> Bool +canDCSnapshot (C (M k)) = lookahead (k undefined) == WillDontCheck + +-- | Get the threads which exist in a snapshot, partitioned into +-- runnable and not runnable. +-- +-- @since unreleased +threadsFromDCSnapshot :: DCSnapshot r n a -> ([ThreadId], [ThreadId]) +threadsFromDCSnapshot snapshot = partition isRunnable (M.keys threads) where + threads = cThreads (dcsContext snapshot) + isRunnable tid = isNothing (_blocking =<< M.lookup tid threads) diff --git a/dejafu/Test/DejaFu/SCT.hs b/dejafu/Test/DejaFu/SCT.hs index e759ba4..40a82d1 100755 --- a/dejafu/Test/DejaFu/SCT.hs +++ b/dejafu/Test/DejaFu/SCT.hs @@ -550,7 +550,7 @@ sctUniformRandomDiscard :: (MonadConc n, MonadRef r n, RandomGen g) -> ConcT r n a -- ^ The computation to run many times. -> n [(Either Failure a, Trace)] -sctUniformRandomDiscard discard0 memtype0 g0 lim0 = sct (g0, max 0 lim0) check step discard0 memtype0 where +sctUniformRandomDiscard discard0 memtype0 g0 lim0 = sct (const (g0, max 0 lim0)) check step discard0 memtype0 where check (_, 0) = Nothing check s = Just s @@ -602,7 +602,7 @@ sctWeightedRandomDiscard :: (MonadConc n, MonadRef r n, RandomGen g) -> ConcT r n a -- ^ The computation to run many times. -> n [(Either Failure a, Trace)] -sctWeightedRandomDiscard discard0 memtype0 g0 lim0 use0 = sct (g0, max 0 lim0, max 1 use0, M.empty) check step discard0 memtype0 where +sctWeightedRandomDiscard discard0 memtype0 g0 lim0 use0 = sct (const (g0, max 0 lim0, max 1 use0, M.empty)) check step discard0 memtype0 where check (_, 0, _, _) = Nothing check s = Just s @@ -615,7 +615,7 @@ sctWeightedRandomDiscard discard0 memtype0 g0 lim0 use0 = sct (g0, max 0 lim0, m -- | General-purpose SCT function. sct :: (MonadConc n, MonadRef r n) - => s + => ([ThreadId] -> s) -- ^ Initial state -> (s -> Maybe t) -- ^ State predicate @@ -625,17 +625,25 @@ sct :: (MonadConc n, MonadRef r n) -> MemType -> ConcT r n a -> n [(Either Failure a, Trace)] -sct s0 sfun srun discard memtype conc = go s0 where - go !s = case sfun s of - Just t -> srun s t run >>= \case - (s', Just (res, trace)) -> case discard res of - Just DiscardResultAndTrace -> go s' - Just DiscardTrace -> ((res, []):) <$> go s' - Nothing -> ((res, trace):) <$> go s' - (s', Nothing) -> go s' - Nothing -> pure [] +sct s0 sfun srun discard memtype conc + | canDCSnapshot conc = runForDCSnapshot conc >>= \case + Just (Right snap, _) -> go (runSnap snap) (fst (threadsFromDCSnapshot snap)) + Just (Left f, trace) -> pure [(Left f, trace)] + _ -> fatal "sct" "Failed to construct snapshot" + | otherwise = go runFull [initialThread] + where + go run = go' . s0 where + go' !s = case sfun s of + Just t -> srun s t run >>= \case + (s', Just (res, trace)) -> case discard res of + Just DiscardResultAndTrace -> go' s' + Just DiscardTrace -> ((res, []):) <$> go' s' + Nothing -> ((res, trace):) <$> go' s' + (s', Nothing) -> go' s' + Nothing -> pure [] - run sched s = runConcurrent sched memtype s conc + runFull sched s = runConcurrent sched memtype s conc + runSnap snap sched s = runWithDCSnapshot sched memtype s snap ------------------------------------------------------------------------------- -- Utilities diff --git a/dejafu/Test/DejaFu/SCT/Internal/DPOR.hs b/dejafu/Test/DejaFu/SCT/Internal/DPOR.hs index 0905d6f..8f648a5 100644 --- a/dejafu/Test/DejaFu/SCT/Internal/DPOR.hs +++ b/dejafu/Test/DejaFu/SCT/Internal/DPOR.hs @@ -122,15 +122,19 @@ instance NFData BacktrackStep where -- | Initial DPOR state, given an initial thread ID. This initial -- thread should exist and be runnable at the start of execution. -initialState :: DPOR -initialState = DPOR - { dporRunnable = S.singleton initialThread - , dporTodo = M.singleton initialThread False - , dporNext = Nothing - , dporDone = S.empty - , dporSleep = M.empty - , dporTaken = M.empty - } +-- +-- The main thread must be in the list of initially runnable threads. +initialState :: [ThreadId] -> DPOR +initialState threads + | initialThread `elem` threads = DPOR + { dporRunnable = S.fromList threads + , dporTodo = M.singleton initialThread False + , dporNext = Nothing + , dporDone = S.empty + , dporSleep = M.empty + , dporTaken = M.empty + } + | otherwise = fatal "initialState" "Initial thread is not in initially runnable set" -- | Produce a new schedule prefix from a @DPOR@ tree. If there are no new -- prefixes remaining, return 'Nothing'. Also returns whether the