Automatically snapshot (when possible) in SCT

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

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
+      ]
     ]
   ]
 

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)

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)

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

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