Add tests for named threads, vars, and refs

dejafu-tests/dejafu-tests.cabal

@@ -29,6 +29,7 @@ library
                      , Integration.Discard
                      , Integration.Regressions
                      , Integration.SCT
+                     , Integration.Names
 
                      , Examples
                      , Examples.AutoUpdate

dejafu-tests/lib/Integration.hs

@@ -6,6 +6,7 @@ import qualified Integration.Async          as A
 import qualified Integration.Discard        as D
 import qualified Integration.Litmus         as L
 import qualified Integration.MultiThreaded  as M
+import qualified Integration.Names          as N
 import qualified Integration.Refinement     as R
 import qualified Integration.Regressions    as G
 import qualified Integration.SCT            as SC
@@ -20,6 +21,7 @@ tests =
   , testGroup "Discard"        D.tests
   , testGroup "Litmus"         L.tests
   , testGroup "MultiThreaded"  M.tests
+  , testGroup "Names"          N.tests
   , testGroup "Refinement"     R.tests
   , testGroup "Regressions"    G.tests
   , testGroup "SingleThreaded" S.tests

dejafu-tests/lib/Integration/Names.hs

@@ -0,0 +1,116 @@
+module Integration.Names where
+
+import           Control.Concurrent.Classy hiding (check)
+import           Data.Maybe                (mapMaybe)
+import           Test.DejaFu.Conc          (ConcIO)
+import           Test.DejaFu.Internal      (crefOf, mvarOf, simplifyAction,
+                                            tidsOf, tvarsOf)
+import           Test.DejaFu.SCT           (runSCT)
+import           Test.DejaFu.Types
+import           Test.Tasty.HUnit
+
+import           Common
+
+tests :: [TestTree]
+tests =
+  toTestList
+    [ testCase "MVar names" testMVarNames
+    , testCase "CRef names" testCRefNames
+    , testCase "TVar names" testTVarNames
+    , testCase "Thread names" testThreadNames
+    ]
+
+check ::
+     String
+  -> ([ThreadAction] -> Bool)
+  -> ConcIO a
+  -> Assertion
+check msg validActions testAction = do
+  outcomes <- runSCT defaultWay defaultMemType testAction
+  let extractActions = map $ \(_, _, action) -> action
+      actions = [extractActions trace | (_, trace) <- outcomes]
+  assertBool msg $ any validActions actions
+
+testMVarNames :: Assertion
+testMVarNames =
+  check "All traces should use only required MVar names" checkMVars $ do
+    mvar1 <- newEmptyMVarN mvarName1
+    mvar2 <- newEmptyMVarN mvarName2
+    _ <- takeMVar mvar1
+    _ <- fork $ putMVar mvar1 (1 :: Int)
+    _ <- fork $ putMVar mvar2 (2 :: Int)
+    _ <- fork $ putMVar mvar1 3
+    (,) <$> readMVar mvar1 <*> readMVar mvar2
+  where
+    mvarName1 = "first-mvar"
+    mvarName2 = "second-mvar"
+    mvarName (MVarId (Id (Just n) _)) = Just n
+    mvarName _ = Nothing
+    mvar (NewMVar mvid) = Just mvid
+    mvar a = mvarOf (simplifyAction a)
+    checkMVars =
+      let validMVid = maybe False (`elem` [mvarName1, mvarName2]) . mvarName
+      in all validMVid . mapMaybe mvar
+
+testCRefNames :: Assertion
+testCRefNames =
+  check "All traces should use only required CRef names" checkCRefs $ do
+    x <- newCRefN crefName1 (0::Int)
+    y <- newCRefN crefName2 (0::Int)
+    _ <- fork $ modifyCRefCAS x (const (1, ()))
+    _ <- fork $ writeCRef y 2
+    (,) <$> readCRef x <*> readCRef y
+  where
+    crefName1 = "cref-one"
+    crefName2 = "cref-two"
+    crefName (CRefId (Id (Just n) _)) = Just n
+    crefName _ = Nothing
+    cref (NewCRef ref) = Just ref
+    cref a = crefOf (simplifyAction a)
+    checkCRefs =
+      let validCRef = maybe False (`elem` [crefName1, crefName2]) . crefName
+      in all validCRef . mapMaybe cref
+
+testTVarNames :: Assertion
+testTVarNames =
+  check "All traces should use only required TVar names" checkTVars $ do
+    v1 <- atomically $ newTVarN tvarName1 (0::Int)
+    v2 <- atomically $ newTVarN  tvarName2 (0::Int)
+    _ <-
+      fork . atomically $ do
+        writeTVar v1 1
+        modifyTVar v2 (+ 100)
+    _ <-
+      fork . atomically $ do
+        modifyTVar v1 (* 100)
+        writeTVar v2 42
+    pure ()
+  where
+    tvarName1 = "tvar-one"
+    tvarName2 = "tvar-two"
+    tvarName (TVarId (Id (Just n) _)) = Just n
+    tvarName _ = Nothing
+    checkTVars =
+      let validTVar =
+            maybe False (`elem` [tvarName1, tvarName2]) . tvarName
+      in all (all validTVar) . map tvarsOf
+
+testThreadNames :: Assertion
+testThreadNames =
+  check "All traces should use only required thread names" checkThreads $ do
+      x <- newEmptyMVar
+      tid <- forkN threadName2 $ putMVar x ()
+      _ <- forkN threadName1 $ readMVar x
+      _ <- forkN threadName3 $ pure ()
+      killThread tid
+  where
+    threadName1 = "thread-one"
+    threadName2 = "thread-two"
+    threadName3 = "thread-three"
+    threadName (ThreadId (Id (Just n) _)) = Just n
+    threadName _ = Nothing
+    checkThreads =
+      let validTid =
+            maybe False (`elem` [threadName1, threadName2, threadName3]) .
+            threadName
+      in all (all validTid) . map tidsOf

dejafu/Test/DejaFu/Internal.hs

@@ -105,6 +105,7 @@ tvarsWritten act = S.fromList $ case act of
   _ -> []
 
   where
+    tvarsOf' (TNew tv) = [tv]
     tvarsOf' (TWrite tv) = [tv]
     tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)
     tvarsOf' (TCatch  ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)
@@ -263,6 +264,20 @@ mvarOf (SynchronisedRead  c) = Just c
 mvarOf (SynchronisedWrite c) = Just c
 mvarOf _ = Nothing
 
+-- | Get the @ThreadId@s involved in a @ThreadAction@.
+tidsOf :: ThreadAction -> Set ThreadId
+tidsOf (Fork tid) = S.singleton tid
+tidsOf (ForkOS tid) = S.singleton tid
+tidsOf (PutMVar _ tids) = S.fromList tids
+tidsOf (TryPutMVar _ _ tids) = S.fromList tids
+tidsOf (TakeMVar _ tids) = S.fromList tids
+tidsOf (TryTakeMVar _ _ tids) = S.fromList tids
+tidsOf (CommitCRef tid _) = S.singleton tid
+tidsOf (STM _ tids) = S.fromList tids
+tidsOf (ThrowTo tid) = S.singleton tid
+tidsOf (BlockedThrowTo tid) = S.singleton tid
+tidsOf _ = S.empty
+
 -- | Throw away information from a 'ThreadAction' and give a
 -- simplified view of what is happening.
 --