Add primitives for the new testing functions

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.

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.

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)

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

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 }