Remove top-level definitions of individual tests

dejafu-tests/Cases/MultiThreaded.hs

@@ -1,307 +1,251 @@
 module Cases.MultiThreaded where
 
 import Control.Exception (ArithException(..))
-import Control.Monad (void, unless)
 import Test.DejaFu (Failure(..), gives, gives')
 import Test.Framework (Test)
 
 import Control.Concurrent.Classy hiding (newQSemN, signalQSemN, waitQSemN)
-import Test.DejaFu.Conc (ConcT, subconcurrency)
+import Test.DejaFu.Conc (subconcurrency)
 
 import Common
 import QSemN
 
 tests :: [Test]
 tests =
-    [ testGroup "Threading"
+    [ testGroup "Threading" threadingTests
-      [ threadId1
+    , testGroup "MVar" mvarTests
-      , threadId2
+    , testGroup "CRef" crefTests
-      , threadNoWait
+    , testGroup "STM" stmTests
-      ]
+    , testGroup "Exceptions" exceptionTests
-    , testGroup "MVar"
+    , testGroup "Daemons" daemonTests
-      [ mvarLock
+    , testGroup "Subconcurrency" subconcurrencyTests
-      , mvarRace
-      ]
-    , testGroup "CRef"
-      [ crefRace
-      , crefCASModify
-      , crefCASRace
-      , crefCASRaceRedo
-      , crefCASTickets
-      ]
-    , testGroup "STM"
-      [ stmAtomic
-      , stmLeftRetry
-      , stmRightRetry
-      , stmIssue55
-      , stmIssue111
-      ]
-    , testGroup "Killing Threads"
-      [ threadKill
-      , threadKillMask
-      , threadKillUninterruptibleMask
-      , threadKillUmask
-      , threadKillToMain1
-      , threadKillToMain2
-      ]
-    , testGroup "Daemons"
-      [ schedDaemon
-      ]
-    , testGroup "Subconcurrency"
-      [ scDeadlock1
-      , scDeadlock2
-      , scSuccess
-      , scIllegal
-      , scIssue71
-      , scIssue81
-      ]
     ]
 
 --------------------------------------------------------------------------------
--- Threading
 
-threadId1 :: [Test]
+threadingTests :: [Test]
-threadId1 = djfuT "Fork reports the thread ID of the child" (gives' [True]) $ do
+threadingTests = toTestList
-  var <- newEmptyMVar
+  [ djfuT "Fork reports the thread ID of the child" (gives' [True]) $ do
-  tid <- fork $ myThreadId >>= putMVar var
+      var <- newEmptyMVar
-  (tid ==) <$> readMVar var
+      tid <- fork $ myThreadId >>= putMVar var
+      (tid ==) <$> readMVar var
 
-threadId2 :: [Test]
+  , djfuT "Different threads have different thread IDs" (gives' [True]) $ do
-threadId2 = djfuT "Different threads have different thread IDs" (gives' [True]) $ do
+      tid <- spawn myThreadId
-  tid <- spawn myThreadId
+      (/=) <$> myThreadId <*> readMVar tid
-  (/=) <$> myThreadId <*> readMVar tid
 
-threadNoWait :: [Test]
+  , djfuT "A thread doesn't wait for its children before terminating" (gives' [Nothing, Just ()]) $ do
-threadNoWait = djfuT "A thread doesn't wait for its children before terminating" (gives' [Nothing, Just ()]) $ do
+      x <- newCRef Nothing
-  x <- newCRef Nothing
+      _ <- fork . writeCRef x $ Just ()
-  void . fork . writeCRef x $ Just ()
+      readCRef x
-  readCRef x
+  ]
 
 --------------------------------------------------------------------------------
--- @MVar@s
 
-mvarLock :: [Test]
+mvarTests :: [Test]
-mvarLock = djfuT "Racey MVar computations may deadlock" (gives [Left Deadlock, Right 0]) $ do
+mvarTests = toTestList
-  a <- newEmptyMVar
+  [ djfuT "Racey MVar computations may deadlock" (gives [Left Deadlock, Right 0]) $ do
-  b <- newEmptyMVar
+      a <- newEmptyMVar
+      b <- newEmptyMVar
+      c <- newMVarInt 0
+      let lock m = putMVar m ()
+      let unlock = takeMVar
+      j1 <- spawn $ lock a >> lock b >> modifyMVar_ c (return . succ) >> unlock b >> unlock a
+      j2 <- spawn $ lock b >> lock a >> modifyMVar_ c (return . pred) >> unlock a >> unlock b
+      takeMVar j1
+      takeMVar j2
+      takeMVar c
 
-  c <- newMVar 0
+  , djfuT "Racey MVar computations are nondeterministic" (gives' [0,1]) $ do
-
+      x <- newEmptyMVarInt
-  let lock m = putMVar m ()
+      _ <- fork $ putMVar x 0
-  let unlock = takeMVar
+      _ <- fork $ putMVar x 1
-
+      readMVar x
-  j1 <- spawn $ lock a >> lock b >> modifyMVar_ c (return . succ) >> unlock b >> unlock a
+  ]
-  j2 <- spawn $ lock b >> lock a >> modifyMVar_ c (return . pred) >> unlock a >> unlock b
-
-  takeMVar j1
-  takeMVar j2
-
-  takeMVar c
-
-mvarRace :: [Test]
-mvarRace = djfuT "Racey MVar computations are nondeterministic" (gives' [0,1]) $ do
-  x <- newEmptyMVar
-  _ <- fork $ putMVar x 0
-  _ <-  fork $ putMVar x 1
-  readMVar x
 
 --------------------------------------------------------------------------------
--- @CRef@s
 
-crefRace :: [Test]
+crefTests :: [Test]
-crefRace = djfuT "Racey CRef computations are nondeterministic" (gives' [0,1]) $ do
+crefTests = toTestList
-  x <- newCRef (0::Int)
+  [ djfuT "Racey CRef computations are nondeterministic" (gives' [0,1]) $ do
+      x  <- newCRefInt 0
+      j1 <- spawn $ writeCRef x 0
+      j2 <- spawn $ writeCRef x 1
+      takeMVar j1
+      takeMVar j2
+      readCRef x
 
-  j1 <- spawn $ writeCRef x 0
+  , djfuT "CASing CRef changes its value" (gives' [0,1]) $ do
-  j2 <- spawn $ writeCRef x 1
+      x <- newCRefInt 0
+      _ <- fork $ modifyCRefCAS x (\_ -> (1, ()))
+      readCRef x
 
-  takeMVar j1
+  , djfuT "Racey CAS computations are nondeterministic" (gives' [(True, 2), (False, 2)]) $ do
-  takeMVar j2
+      x <- newCRefInt 0
+      t <- readForCAS x
+      j <- spawn $ casCRef x t 1
+      writeCRef x 2
+      b <- fst <$> readMVar j
+      v <- readCRef x
+      pure (b, v)
 
-  readCRef x
+  , djfuT "A failed CAS gives an updated ticket" (gives' [(True, 1), (True, 2)]) $ do
+      x <- newCRefInt 0
+      t <- readForCAS x
+      v <- newEmptyMVar
+      j <- spawn $ do
+        o@(f, t') <- casCRef x t 1
+        takeMVar v
+        if f then pure o else casCRef x t' 1
+      writeCRef x 2
+      putMVar v ()
+      b <- fst <$> readMVar j
+      o <- readCRef x
+      pure (b, o)
 
-crefCASModify :: [Test]
+  , djfuT "A ticket is only good for one CAS" (gives' [(True, False, 1), (False, True, 2)]) $ do
-crefCASModify = djfuT "CASing CRef changes its value" (gives' [0,1]) $ do
+      x  <- newCRefInt 0
-  x <- newCRef (0::Int)
+      t  <- readForCAS x
-  fork $ modifyCRefCAS x (\_ -> (1, ()))
+      j1 <- spawn $ casCRef x t 1
-  readCRef x
+      j2 <- spawn $ casCRef x t 2
-
+      b1 <- fst <$> readMVar j1
-crefCASRace :: [Test]
+      b2 <- fst <$> readMVar j2
-crefCASRace = djfuT "Racey CAS computations are nondeterministic" (gives' [(True, 2), (False, 2)]) $ do
+      v  <- readCRef x
-  x <- newCRef (0::Int)
+      pure (b1, b2, v)
-  t <- readForCAS x
+  ]
-  j <- spawn $ casCRef x t 1
-  writeCRef x 2
-  b <- fst <$> readMVar j
-  v <- readCRef x
-  pure (b, v)
-
-crefCASRaceRedo :: [Test]
-crefCASRaceRedo = djfuT "A failed CAS gives an updated ticket" (gives' [(True, 1), (True, 2)]) $ do
-  x <- newCRef (0::Int)
-  t <- readForCAS x
-  v <- newEmptyMVar
-  j <- spawn $ do
-    o@(f, t') <- casCRef x t 1
-    takeMVar v
-    if f then pure o else casCRef x t' 1
-  writeCRef x 2
-  putMVar v ()
-  b <- fst <$> readMVar j
-  v <- readCRef x
-  pure (b, v)
-
-crefCASTickets :: [Test]
-crefCASTickets = djfuT "A ticket is only good for one CAS" (gives' [(True, False, 1), (False, True, 2)]) $ do
-  x  <- newCRef (0::Int)
-  t  <- readForCAS x
-  j1 <- spawn $ casCRef x t 1
-  j2 <- spawn $ casCRef x t 2
-  b1 <- fst <$> readMVar j1
-  b2 <- fst <$> readMVar j2
-  v  <- readCRef x
-  pure (b1, b2, v)
 
 --------------------------------------------------------------------------------
--- STM
 
-stmAtomic :: [Test]
+stmTests :: [Test]
-stmAtomic = djfuT "Transactions are atomic" (gives' [0,2]) $ do
+stmTests = toTestList
-  x <- atomically $ newTVar (0::Int)
+  [ djfuT "Transactions are atomic" (gives' [0,2]) $ do
-  void . fork . atomically $ writeTVar x 1 >> writeTVar x 2
+      x <- atomically $ newTVarInt 0
-  atomically $ readTVar x
+      _ <- fork . atomically $ writeTVar x 1 >> writeTVar x 2
+      atomically $ readTVar x
 
-stmLeftRetry :: [Test]
+  , djfuT "'retry' is the left identity of 'orElse'" (gives' [()]) $ do
-stmLeftRetry = djfuT "'retry' is the left identity of 'orElse'" (gives' [()]) $ do
+      x <- atomically $ newTVar Nothing
-  x <- atomically $ newTVar Nothing
+      let readJust var = maybe retry pure =<< readTVar var
-  let readJust var = maybe retry pure =<< readTVar var
+      _ <- fork . atomically . writeTVar x $ Just ()
-  fork . atomically . writeTVar x $ Just ()
+      atomically $ retry `orElse` readJust x
-  atomically $ retry `orElse` readJust x
 
-stmRightRetry :: [Test]
+  , djfuT "'retry' is the right identity of 'orElse'" (gives' [()]) $ do
-stmRightRetry = djfuT "'retry' is the right identity of 'orElse'" (gives' [()]) $ do
+      x <- atomically $ newTVar Nothing
-  x <- atomically $ newTVar Nothing
+      let readJust var = maybe retry pure =<< readTVar var
-  let readJust var = maybe retry pure =<< readTVar var
+      fork . atomically . writeTVar x $ Just ()
-  fork . atomically . writeTVar x $ Just ()
+      atomically $ readJust x `orElse` retry
-  atomically $ readJust x `orElse` retry
 
-stmIssue55 :: [Test]
+  , djfuT "https://github.com/barrucadu/dejafu/issues/55" (gives' [True]) $ do
-stmIssue55 = djfuT "https://github.com/barrucadu/dejafu/issues/55" (gives' [True]) $ do
+      a <- atomically $ newTQueue
-  a <- atomically $ newTQueue
+      b <- atomically $ newTQueue
-  b <- atomically $ newTQueue
+      _ <- fork . atomically $ writeTQueue b True
-  fork . atomically $ writeTQueue b True
+      let both x y = readTQueue x `orElse` readTQueue y `orElse` retry
-  let both a b = readTQueue a `orElse` readTQueue b `orElse` retry
+      atomically $ both a b
-  atomically $ both a b
 
-stmIssue111 :: [Test]
+  , djfuT "https://github.com/barrucadu/dejafu/issues/111" (gives' [1]) $ do
-stmIssue111 = djfuT "https://github.com/barrucadu/dejafu/issues/111" (gives' [1]) $ do
+      v <- atomically $ newTVarInt 1
-  v <- atomically $ newTVar 1
+      _ <- fork . atomically $ do
-  fork . atomically $ do
+        writeTVar v 2
-    writeTVar v 2
+        writeTVar v 3
-    writeTVar v 3
+        retry
-    retry
+      atomically $ readTVar v
-  atomically $ readTVar v
+  ]
 
 --------------------------------------------------------------------------------
--- Exceptions
 
-threadKill :: [Test]
+exceptionTests :: [Test]
-threadKill = djfuT "Exceptions can kill unmasked threads" (gives [Left Deadlock, Right ()]) $ do
+exceptionTests = toTestList
-  x <- newEmptyMVar
+  [ djfuT "Exceptions can kill unmasked threads" (gives [Left Deadlock, Right ()]) $ do
-  tid <- fork $ putMVar x ()
+      x <- newEmptyMVar
-  killThread tid
+      tid <- fork $ putMVar x ()
-  readMVar x
+      killThread tid
+      readMVar x
 
-threadKillMask :: [Test]
+  , djfuT "Exceptions cannot kill nonblocking masked threads" (gives' [()]) $ do
-threadKillMask = djfuT "Exceptions cannot kill nonblocking masked threads" (gives' [()]) $ do
+      x <- newEmptyMVar
-  x <- newEmptyMVar
+      y <- newEmptyMVar
-  y <- newEmptyMVar
+      tid <- fork $ mask $ \_ -> putMVar x () >> putMVar y ()
-  tid <- fork $ mask $ \_ -> putMVar x () >> putMVar y ()
+      readMVar x
-  readMVar x
+      killThread tid
-  killThread tid
+      readMVar y
-  readMVar y
 
-threadKillUninterruptibleMask :: [Test]
+  , djfuT "Throwing to an uninterruptible thread blocks" (gives [Left Deadlock]) $ do
-threadKillUninterruptibleMask = djfuT "Throwing to an uninterruptible thread blocks" (gives [Left Deadlock]) $ do
+      x <- newEmptyMVar
-  x <- newEmptyMVar
+      y <- newEmptyMVar
-  y <- newEmptyMVar
+      tid <- fork $ uninterruptibleMask $ \_ -> putMVar x () >> takeMVar y
-  tid <- fork $ uninterruptibleMask $ \_ -> putMVar x () >> takeMVar y
+      readMVar x
-  readMVar x
+      killThread tid
-  killThread tid
 
-threadKillUmask :: [Test]
+  , djfuT "Exceptions can kill masked threads which have unmasked" (gives [Left Deadlock, Right ()]) $ do
-threadKillUmask = djfuT "Exceptions can kill nonblocking masked threads which have unmasked" (gives [Left Deadlock, Right ()]) $ do
+      x <- newEmptyMVar
-  x <- newEmptyMVar
+      y <- newEmptyMVar
-  y <- newEmptyMVar
+      tid <- fork $ mask $ \umask -> putMVar x () >> umask (putMVar y ())
-  tid <- fork $ mask $ \umask -> putMVar x () >> umask (putMVar y ())
+      readMVar x
-  readMVar x
+      killThread tid
-  killThread tid
+      readMVar y
-  readMVar y
 
-threadKillToMain1 :: [Test]
+  , djfuT "Throwing to main kills the computation, if unhandled" (gives [Left UncaughtException]) $ do
-threadKillToMain1 = djfuT "Throwing to main kills the computation, if unhandled" (gives [Left UncaughtException]) $ do
+      tid <- myThreadId
-  tid <- myThreadId
+      j <- spawn $ throwTo tid Overflow
-  j <- spawn $ throwTo tid Overflow
+      readMVar j
-  readMVar j
 
-threadKillToMain2 :: [Test]
+  , djfuT "Throwing to main doesn't kill the computation, if handled" (gives' [()]) $ do
-threadKillToMain2 = djfuT "Throwing to main doesn't kill the computation, if handled" (gives' [()]) $ do
+      tid <- myThreadId
-  tid <- myThreadId
+      catchArithException
-  catchArithException (spawn (throwTo tid Overflow) >>= readMVar)
+        (spawn (throwTo tid Overflow) >>= readMVar)
-                      (\_ -> pure ())
+        (\_ -> pure ())
+  ]
 
 -------------------------------------------------------------------------------
--- Daemon threads
 
-schedDaemon :: [Test]
+daemonTests :: [Test]
-schedDaemon = djfuT "https://github.com/barrucadu/dejafu/issues/40" (gives' [0,1]) $ do
+daemonTests = toTestList
-  x <- newCRef 0
+  [ djfuT "https://github.com/barrucadu/dejafu/issues/40" (gives' [0,1]) $ do
-  _ <- fork $ myThreadId >> writeCRef x 1
+      x <- newCRefInt 0
-  readCRef x
+      _ <- fork $ myThreadId >> writeCRef x 1
+      readCRef x
+  ]
 
 --------------------------------------------------------------------------------
--- Subconcurrency
 
-scDeadlock1 :: [Test]
+subconcurrencyTests :: [Test]
-scDeadlock1 = djfuT "Failure is observable" (gives' [Left Deadlock, Right ()]) $ do
+subconcurrencyTests = toTestList
-  var <- newEmptyMVar
+  [ djfuT "Failure is observable" (gives' [Left Deadlock, Right ()]) $ do
-  subconcurrency $ do
+      var <- newEmptyMVar
-    void . fork $ putMVar var ()
+      subconcurrency $ do
-    putMVar var ()
+        _ <- fork $ putMVar var ()
+        putMVar var ()
 
-scDeadlock2 :: [Test]
+  , djfuT "Failure does not abort the outer computation" (gives' [(Left Deadlock, ()), (Right (), ())]) $ do
-scDeadlock2 = djfuT "Failure does not abort the outer computation" (gives' [(Left Deadlock, ()), (Right (), ())]) $ do
+      var <- newEmptyMVar
-  var <- newEmptyMVar
+      res <- subconcurrency $ do
-  res <- subconcurrency $ do
+        _ <- fork $ putMVar var ()
-    void . fork $ putMVar var ()
+        putMVar var ()
-    putMVar var ()
+      (,) <$> pure res <*> readMVar var
-  (,) <$> pure res <*> readMVar var
 
-scSuccess :: [Test]
+  , djfuT "Success is observable" (gives' [Right ()]) $ do
-scSuccess = djfuT "Success is observable" (gives' [Right ()]) $ do
+      var <- newMVar ()
-  var <- newMVar ()
+      subconcurrency $ do
-  subconcurrency $ do
+        out <- newEmptyMVar
-    out <- newEmptyMVar
+        _ <- fork $ takeMVar var >>= putMVar out
-    void . fork $ takeMVar var >>= putMVar out
+        takeMVar out
-    takeMVar out
 
-scIllegal :: [Test]
+  , djfuT "It is illegal to start subconcurrency after forking" (gives [Left IllegalSubconcurrency]) $ do
-scIllegal = djfuT "It is illegal to start subconcurrency after forking" (gives [Left IllegalSubconcurrency]) $ do
+      var <- newEmptyMVar
-  var <- newEmptyMVar
+      _ <- fork $ readMVar var
-  void . fork $ readMVar var
+      _ <- subconcurrency $ pure ()
-  void . subconcurrency $ pure ()
+      pure ()
 
-scIssue71 :: [Test]
+  , djfuT "https://github.com/barrucadu/dejafu/issues/71" (gives' [()]) $ do
-scIssue71 = djfuT "https://github.com/barrucadu/dejafu/issues/71" (gives' [()]) $ do
+      let ma ||| mb = do { j1 <- spawn ma; j2 <- spawn mb; takeMVar j1; takeMVar j2; pure () }
-  let ma ||| mb = do { j1 <- spawn ma; j2 <- spawn mb; takeMVar j1; takeMVar j2; pure () }
+      s <- newEmptyMVar
-  s <- newEmptyMVar
+      _ <- subconcurrency (takeMVar s ||| pure ())
-  _ <- subconcurrency (takeMVar s ||| pure ())
+      pure ()
-  pure ()
 
-scIssue81 :: [Test]
+  , djfuT "https://github.com/barrucadu/dejafu/issues/81" (gives' [(Right (),0)]) $ do
-scIssue81 = djfuT "https://github.com/barrucadu/dejafu/issues/81" (gives' [(Right (),0)]) $ do
+      s <- newQSemN 0
-  s <- newQSemN 0
+      let interfere = waitQSemN s 0 >> signalQSemN s 0
-  let interfere = waitQSemN s 0 >> signalQSemN s 0
+      x <- subconcurrency (signalQSemN s 0 ||| waitQSemN s 0 ||| interfere)
-  x <- subconcurrency (signalQSemN s 0 ||| waitQSemN s 0 ||| interfere)
+      o <- remainingQSemN s
-  o <- remainingQSemN s
+      pure (x, o)
-  pure (x, o)
+  ]

dejafu-tests/Cases/Refinement.hs

@@ -9,24 +9,9 @@ import Test.HUnit.DejaFu (testProperty)
 import Common
 
 tests :: [Test]
-tests =
+tests = [ testGroup "MVar" mvarProps ]
-  [ testGroup "MVar"
-    [ testProperty "read_idempotent_s"            prop_mvar_read_idempotent_s
-    , testProperty "read_idempotent_c"            prop_mvar_read_idempotent_c
-    , testProperty "read_neq_take_put"            prop_mvar_read_neq_take_put
-    , testProperty "read_sr_take_put"             prop_mvar_read_sr_take_put
-    , testProperty "take_eq_read_take_s"          prop_mvar_take_eq_read_take_s
-    , testProperty "take_neq_read_take_c"         prop_mvar_take_neq_read_take_c
-    , testProperty "take_sr_read_take_c"          prop_mvar_take_sr_read_take_c
-    , testProperty "prop_mvar_put_neq_put_read_s" prop_mvar_put_neq_put_read_s
-    , testProperty "prop_mvar_put_sr_put_read_s"  prop_mvar_put_sr_put_read_s
-    , testProperty "prop_mvar_put_neq_put_read_c" prop_mvar_put_neq_put_read_c
-    , testProperty "prop_mvar_put_sr_put_read_c"  prop_mvar_put_sr_put_read_c
-    ]
-  ]
 
 -------------------------------------------------------------------------------
--- MVars
 
 mvar :: (MVar ConcIO Int -> ConcIO a) ->  Sig (MVar ConcIO Int) (Maybe Int) (Maybe Int)
 mvar e = Sig
@@ -36,46 +21,38 @@ mvar e = Sig
   , expression = void . e
   }
 
--- | @readMVar@ is idempotent when composed sequentially.
+mvarProps :: [Test]
-prop_mvar_read_idempotent_s =
+mvarProps = toTestList
-  mvar readMVar === mvar (\v -> readMVar v >> readMVar v)
+  [ testProperty "readMVar is idempotent when composed sequentially" $
+      mvar readMVar === mvar (\v -> readMVar v >> readMVar v)
 
--- | @readMVar@ is idempotent when composed concurrently.
+  , testProperty "readMVar is idempotent when composed concurrently" $
-prop_mvar_read_idempotent_c =
+      mvar readMVar === mvar (\v -> readMVar v ||| readMVar v)
-  mvar readMVar === mvar (\v -> readMVar v ||| readMVar v)
 
--- | @readMVar@ is not equivalent to a take followed by a put.
+  , testProperty "readMVar is not equivalent to a take followed by a put" $
-prop_mvar_read_neq_take_put = expectFailure $
+      expectFailure $ mvar readMVar === mvar (\v -> takeMVar v >>= putMVar v)
-  mvar readMVar === mvar (\v -> takeMVar v >>= putMVar v)
 
--- | @readMVar@ is a strict refinement of a take followed by a put.
+  , testProperty "readMVar is a strict refinement of a take followed by a put" $
-prop_mvar_read_sr_take_put =
+      mvar readMVar ->- mvar (\v -> takeMVar v >>= putMVar v)
-  mvar readMVar ->- mvar (\v -> takeMVar v >>= putMVar v)
 
--- | @takeMVar@ is equivalent to a read followed by a take.
+  , testProperty "takeMVar is equivalent to a read followed by a take" $
-prop_mvar_take_eq_read_take_s =
+      mvar takeMVar === mvar (\v -> readMVar v >> takeMVar v)
-  mvar takeMVar === mvar (\v -> readMVar v >> takeMVar v)
 
--- | @takeMVar@ is not equivalent to a read concurrently composed with a take.
+  , testProperty "takeMVar is not equivalent to a read concurrently composed with a take" $
-prop_mvar_take_neq_read_take_c = expectFailure $
+      expectFailure $ mvar takeMVar === mvar (\v -> readMVar v ||| takeMVar v)
-  mvar takeMVar === mvar (\v -> readMVar v ||| takeMVar v)
 
--- | @takeMVar@ is a strict refinement of a read concurrently composed with a take.
+  , testProperty "takeMVar is a strict refinement of a read concurrently composed with a take" $
-prop_mvar_take_sr_read_take_c =
+      mvar takeMVar ->- mvar (\v -> readMVar v ||| takeMVar v)
-  mvar takeMVar ->- mvar (\v -> readMVar v ||| takeMVar v)
 
--- | @putMVar@ is not equivalent to a put followed by a read.
+  , testProperty "putMVar is not equivalent to a put followed by a read" $
-prop_mvar_put_neq_put_read_s x = expectFailure $
+      \x -> expectFailure $ mvar (\v -> putMVar v x) === mvar (\v -> putMVar v x >> readMVar v)
-  mvar (\v -> putMVar v x) === mvar (\v -> putMVar v x >> readMVar v)
 
--- | @putMVar@ is a strict refinement of a put followed by a read.
+  , testProperty "putMVar is a strict refinement of a put followed by a read" $
-prop_mvar_put_sr_put_read_s x =
+      \x -> mvar (\v -> putMVar v x) ->- mvar (\v -> putMVar v x >> readMVar v)
-  mvar (\v -> putMVar v x) ->- mvar (\v -> putMVar v x >> readMVar v)
 
--- | @putMVar@ is not equivalent to a put concurrently composed with a read.
+  , testProperty "putMVar is not equivalent to a put concurrently composed with a read" $
-prop_mvar_put_neq_put_read_c x = expectFailure $
+      \x -> expectFailure $ mvar (\v -> putMVar v x) === mvar (\v -> putMVar v x ||| readMVar v)
-  mvar (\v -> putMVar v x) === mvar (\v -> putMVar v x ||| readMVar v)
 
--- | @putMVar@ is a strict refinement of a put concurrently composed with a read.
+  , testProperty "putMVar is a strict refinement of a put concurrently composed with a read" $
-prop_mvar_put_sr_put_read_c x =
+      \x -> mvar (\v -> putMVar v x) ->- mvar (\v -> putMVar v x ||| readMVar v)
-  mvar (\v -> putMVar v x) ->- mvar (\v -> putMVar v x ||| readMVar v)
+  ]

dejafu-tests/Cases/SingleThreaded.hs

@@ -16,309 +16,232 @@ import Control.Applicative ((<$>), (<*>))
 
 tests :: [Test]
 tests =
-  [ testGroup "MVar"
+  [ testGroup "MVar" mvarTests
-    [ emptyMVarPut
+  , testGroup "CRef" crefTests
-    , emptyMVarTryPut
+  , testGroup "STM" stmTests
-    , emptyMVarTake
+  , testGroup "Exceptions" exceptionTests
-    , emptyMVarTryTake
+  , testGroup "Capabilities" capabilityTests
-    , emptyMVarRead
+  , testGroup "Subconcurrency" subconcurrencyTests
-    , emptyMVarTryRead
-    , fullMVarPut
-    , fullMVarTryPut
-    , fullMVarTake
-    , fullMVarTryTake
-    , fullMVarRead
-    , fullMVarTryRead
-    ]
-
-  , testGroup "CRef"
-    [ crefRead
-    , crefWrite
-    , crefModify
-    , crefTicketPeek
-    , crefTicketPeek2
-    , crefCas1
-    , crefCas2
-    ]
-
-  , testGroup "STM"
-    [ stmWrite
-    , stmPreserve
-    , stmRetry
-    , stmOrElse
-    , stmCatch1
-    , stmCatch2
-    , stmMFail
-    ]
-
-  , testGroup "Exceptions"
-    [ excCatch
-    , excNest
-    , excEscape
-    , excCatchAll
-    , excSTM
-    , excToMain1
-    , excToMain2
-    , excMFail
-    ]
-
-  , testGroup "Capabilities"
-    [ capsGet
-    , capsSet
-    ]
-
-  , testGroup "Subconcurrency"
-    [ scDeadlock1
-    , scDeadlock2
-    , scSuccess
-    ]
   ]
 
 --------------------------------------------------------------------------------
--- @MVar@s
 
-emptyMVarTake :: Test
+mvarTests :: [Test]
-emptyMVarTake = djfu "Taking from an empty MVar blocks" (gives [Left Deadlock]) $ do
+mvarTests =
-  var <- newEmptyMVarInt
+  [ djfu "Taking from an empty MVar blocks" (gives [Left Deadlock]) $ do
-  takeMVar var
+      var <- newEmptyMVarInt
+      takeMVar var
 
-emptyMVarTryTake :: Test
+  , djfu "Non-blockingly taking from an empty MVar gives nothing" (gives' [Nothing]) $ do
-emptyMVarTryTake = djfu "Non-blockingly taking from an empty MVar gives nothing" (gives' [Nothing]) $ do
+      var <- newEmptyMVarInt
-  var <- newEmptyMVarInt
+      tryTakeMVar var
-  tryTakeMVar var
 
-emptyMVarPut :: Test
+  , djfu "Putting into an empty MVar updates it" (gives' [True]) $ do
-emptyMVarPut = djfu "Putting into an empty MVar updates it" (gives' [True]) $ do
+      var <- newEmptyMVarInt
-  var <- newEmptyMVarInt
+      putMVar var 7
-  putMVar var 7
+      (==7) <$> readMVar var
-  (==7) <$> readMVar var
 
-emptyMVarTryPut :: Test
+  , djfu "Non-blockingly putting into an empty MVar updates it" (gives' [True]) $ do
-emptyMVarTryPut = djfu "Non-blockingly putting into an empty MVar updates it" (gives' [True]) $ do
+      var <- newEmptyMVarInt
-  var <- newEmptyMVarInt
+      _   <- tryPutMVar var 7
-  _   <- tryPutMVar var 7
+      (==7) <$> readMVar var
-  (==7) <$> readMVar var
 
-emptyMVarRead :: Test
+  , djfu "Reading an empty MVar blocks" (gives [Left Deadlock]) $ do
-emptyMVarRead = djfu "Reading an empty MVar blocks" (gives [Left Deadlock]) $ do
+      var <- newEmptyMVarInt
-  var <- newEmptyMVarInt
+      readMVar var
-  readMVar var
 
-emptyMVarTryRead :: Test
+  , djfu "Non-blockingly reading an empty MVar gives nothing" (gives' [Nothing]) $ do
-emptyMVarTryRead = djfu "Non-blockingly reading an empty MVar gives nothing" (gives' [Nothing]) $ do
+      var <- newEmptyMVarInt
-  var <- newEmptyMVarInt
+      tryReadMVar var
-  tryReadMVar var
 
-fullMVarPut :: Test
+  , djfu "Putting into a full MVar blocks" (gives [Left Deadlock]) $ do
-fullMVarPut = djfu "Putting into a full MVar blocks" (gives [Left Deadlock]) $ do
+      var <- newMVarInt 7
-  var <- newMVarInt 7
+      putMVar var 10
-  putMVar var 10
 
-fullMVarTryPut :: Test
+  , djfu "Non-blockingly putting into a full MVar fails" (gives' [False]) $ do
-fullMVarTryPut = djfu "Non-blockingly putting into a full MVar fails" (gives' [False]) $ do
+      var <- newMVarInt 7
-  var <- newMVarInt 7
+      tryPutMVar var 10
-  tryPutMVar var 10
 
-fullMVarTake :: Test
+  , djfu "Taking from a full MVar works" (gives' [True]) $ do
-fullMVarTake = djfu "Taking from a full MVar works" (gives' [True]) $ do
+      var <- newMVarInt 7
-  var <- newMVarInt 7
+      (==7) <$> takeMVar var
-  (==7) <$> takeMVar var
 
-fullMVarTryTake :: Test
+  , djfu "Non-blockingly taking from a full MVar works" (gives' [True]) $ do
-fullMVarTryTake = djfu "Non-blockingly taking from a full MVar works" (gives' [True]) $ do
+      var <- newMVarInt 7
-  var <- newMVarInt 7
+      (==Just 7) <$> tryTakeMVar var
-  (==Just 7) <$> tryTakeMVar var
 
-fullMVarRead :: Test
+  , djfu "Reading a full MVar works" (gives' [True]) $ do
-fullMVarRead = djfu "Reading a full MVar works" (gives' [True]) $ do
+      var <- newMVarInt 7
-  var <- newMVarInt 7
+      (==7) <$> readMVar var
-  (==7) <$> readMVar var
 
-fullMVarTryRead :: Test
+  , djfu "Non-blockingly reading a full MVar works" (gives' [True]) $ do
-fullMVarTryRead = djfu "Non-blockingly reading a full MVar works" (gives' [True]) $ do
+      var <- newMVarInt 7
-  var <- newMVarInt 7
+      (==Just 7) <$> tryReadMVar var
-  (==Just 7) <$> tryReadMVar var
+  ]
 
 --------------------------------------------------------------------------------
--- @CRef@s
 
-crefRead :: Test
+crefTests :: [Test]
-crefRead = djfu "Reading a non-updated CRef gives its initial value" (gives' [True]) $ do
+crefTests =
-  ref <- newCRefInt 5
+  [ djfu "Reading a non-updated CRef gives its initial value" (gives' [True]) $ do
-  (5==) <$> readCRef ref
+      ref <- newCRefInt 5
+      (5==) <$> readCRef ref
 
-crefWrite :: Test
+  , djfu "Reading an updated CRef gives its new value" (gives' [True]) $ do
-crefWrite = djfu "Reading an updated CRef gives its new value" (gives' [True]) $ do
+      ref <- newCRefInt 5
-  ref <- newCRefInt 5
+      writeCRef ref 6
-  writeCRef ref 6
+      (6==) <$> readCRef ref
-  (6==) <$> readCRef ref
 
-crefModify :: Test
+  , djfu "Updating a CRef by a function changes its value" (gives' [True]) $ do
-crefModify = djfu "Updating a CRef by a function changes its value" (gives' [True]) $ do
+      ref <- newCRefInt 5
-  ref <- newCRefInt 5
+      atomicModifyCRef ref (\i -> (i+1, ()))
-  atomicModifyCRef ref (\i -> (i+1, ()))
+      (6==) <$> readCRef ref
-  (6==) <$> readCRef ref
 
-crefTicketPeek :: Test
+  , djfu "A ticket contains the value of the CRef at the time of its creation" (gives' [True]) $ do
-crefTicketPeek = djfu "A ticket contains the value of the CRef at the time of its creation" (gives' [True]) $ do
+      ref  <- newCRefInt 5
-  ref  <- newCRefInt 5
+      tick <- readForCAS ref
-  tick <- readForCAS ref
+      writeCRef ref 6
-  writeCRef ref 6
+      (5==) <$> peekTicket tick
-  (5==) <$> peekTicket tick
 
-crefTicketPeek2 :: Test
+  , djfu "Compare-and-swap returns a ticket containing the new value" (gives' [True]) $ do
-crefTicketPeek2 = djfu "Compare-and-swap returns a ticket containing the new value" (gives' [True]) $ do
+      ref  <- newCRefInt 5
-  ref  <- newCRefInt 5
+      tick <- readForCAS ref
-  tick <- readForCAS ref
+      (_, tick') <- casCRef ref tick 6
-  (_, tick') <- casCRef ref tick 6
+      (6==) <$> peekTicket tick'
-  (6==) <$> peekTicket tick'
 
-crefCas1 :: Test
+  , djfu "Compare-and-swap on an unmodified CRef succeeds" (gives' [True]) $ do
-crefCas1 = djfu "Compare-and-swap on an unmodified CRef succeeds" (gives' [True]) $ do
+      ref  <- newCRefInt 5
-  ref  <- newCRefInt 5
+      tick <- readForCAS ref
-  tick <- readForCAS ref
+      (suc, _) <- casCRef ref tick 6
-  (suc, _) <- casCRef ref tick 6
+      val <- readCRef ref
-  val <- readCRef ref
+      return (suc && (6 == val))
-  return (suc && (6 == val))
 
-crefCas2 :: Test
+  , djfu "Compare-and-swap on a modified CRef fails" (gives' [True]) $ do
-crefCas2 = djfu "Compare-and-swap on a modified CRef fails" (gives' [True]) $ do
+      ref  <- newCRefInt 5
-  ref  <- newCRefInt 5
+      tick <- readForCAS ref
-  tick <- readForCAS ref
+      writeCRef ref 6
-  writeCRef ref 6
+      (suc, _) <- casCRef ref tick 7
-  (suc, _) <- casCRef ref tick 7
+      val <- readCRef ref
-  val <- readCRef ref
+      return (not suc && not (7 == val))
-  return (not suc && not (7 == val))
+  ]
 
 --------------------------------------------------------------------------------
--- STM
 
-stmWrite :: Test
+stmTests :: [Test]
-stmWrite = djfu "When a TVar is updated in a transaction, its new value is visible later in the transaction" (gives' [True]) $
+stmTests =
-  (6==) <$> atomically (do { v <- newTVarInt 5; writeTVar v 6; readTVar v })
+  [ djfu "When a TVar is updated, its new value is visible later in same transaction" (gives' [True]) $
+      (6==) <$> atomically (do { v <- newTVarInt 5; writeTVar v 6; readTVar v })
 
-stmPreserve :: Test
+  , djfu "When a TVar is updated, its new value is visible in a later transaction" (gives' [True]) $ do
-stmPreserve = djfu "When a TVar is updated, its new value is visible in a later transaction" (gives' [True]) $ do
+      ctv <- atomically $ newTVarInt 5
-  ctv <- atomically $ newTVarInt 5
+      (5==) <$> atomically (readTVar ctv)
-  (5==) <$> atomically (readTVar ctv)
 
-stmRetry :: Test
+  , djfu "Aborting a transaction blocks the thread" (gives [Left STMDeadlock]) $
-stmRetry = djfu "Aborting a transaction blocks the thread" (gives [Left STMDeadlock]) $
+      (atomically retry :: MonadConc m => m ()) -- avoid an ambiguous type
-  (atomically retry :: MonadConc m => m ()) -- avoid an ambiguous type
 
-stmOrElse :: Test
+  , djfu "Aborting a transaction can be caught and recovered from" (gives' [True]) $ do
-stmOrElse = djfu "Aborting a transaction can be caught and recovered from" (gives' [True]) $ do
+      ctv <- atomically $ newTVarInt 5
-  ctv <- atomically $ newTVarInt 5
+      atomically $ orElse retry (writeTVar ctv 6)
-  atomically $ orElse retry (writeTVar ctv 6)
+      (6==) <$> atomically (readTVar ctv)
-  (6==) <$> atomically (readTVar ctv)
 
-stmCatch1 :: Test
+  , djfu "An exception thrown in a transaction can be caught" (gives' [True]) $ do
-stmCatch1 = djfu "An exception thrown in a transaction can be caught" (gives' [True]) $ do
+      ctv <- atomically $ newTVarInt 5
-  ctv <- atomically $ newTVarInt 5
+      atomically $ catchArithException
-  atomically $ catchArithException
+        (throwSTM Overflow)
-                 (throwSTM Overflow)
+        (\_ -> writeTVar ctv 6)
-                 (\_ -> writeTVar ctv 6)
+      (6==) <$> atomically (readTVar ctv)
-  (6==) <$> atomically (readTVar ctv)
 
-stmCatch2 :: Test
+  , djfu "Nested exception handlers in transactions work" (gives' [True]) $ do
-stmCatch2 = djfu "Nested exception handlers in transactions work" (gives' [True]) $ do
+      ctv <- atomically $ newTVarInt 5
-  ctv <- atomically $ newTVarInt 5
+      atomically $ catchArithException
-  atomically $ catchArithException
+        (catchArrayException
-                 (catchArrayException
+          (throwSTM Overflow)
-                   (throwSTM Overflow)
+          (\_ -> writeTVar ctv 0))
-                   (\_ -> writeTVar ctv 0))
+        (\_ -> writeTVar ctv 6)
-                 (\_ -> writeTVar ctv 6)
+      (6==) <$> atomically (readTVar ctv)
-  (6==) <$> atomically (readTVar ctv)
 
-stmMFail :: Test
+  , djfu "MonadSTM is a MonadFail" (gives [Left UncaughtException]) $
-stmMFail = djfu "MonadSTM is a MonadFail" (gives [Left UncaughtException]) $
+      (atomically $ fail "hello world" :: MonadConc m => m ())  -- avoid an ambiguous type
-  (atomically $ fail "hello world" :: MonadConc m => m ())
+  ]
 
 --------------------------------------------------------------------------------
--- Exceptions
 
-excCatch :: Test
+exceptionTests :: [Test]
-excCatch = djfu "An exception thrown can be caught" (gives' [True]) $
+exceptionTests =
-  catchArithException
+  [ djfu "An exception thrown can be caught" (gives' [True]) $
-    (throw Overflow)
+      catchArithException
-    (\_ -> return True)
-
-excNest :: Test
-excNest = djfu "Nested exception handlers work" (gives' [True]) $
-  catchArithException
-    (catchArrayException
-      (throw Overflow)
-      (\_ -> return False))
-    (\_ -> return True)
-
-excEscape :: Test
-excEscape = djfu "Uncaught exceptions kill the computation" (gives [Left UncaughtException]) $
-  catchArithException
-    (throw $ IndexOutOfBounds "")
-    (\_ -> return False)
-
-excCatchAll :: Test
-excCatchAll = djfu "SomeException matches all exception types" (gives' [True]) $ do
-  a <- catchSomeException
         (throw Overflow)
         (\_ -> return True)
-  b <- catchSomeException
+
-        (throw $ IndexOutOfBounds "")
+  , djfu "Nested exception handlers work" (gives' [True]) $
+      catchArithException
+        (catchArrayException
+          (throw Overflow)
+          (\_ -> return False))
         (\_ -> return True)
-  return (a && b)
 
-excSTM :: Test
+  , djfu "Uncaught exceptions kill the computation" (gives [Left UncaughtException]) $
-excSTM = djfu "Exceptions thrown in a transaction can be caught outside it" (gives' [True]) $
+      catchArithException
-  catchArithException
+        (throw $ IndexOutOfBounds "")
-    (atomically $ throwSTM Overflow)
+        (\_ -> return False)
-    (\_ -> return True)
 
-excToMain1 :: Test
+  , djfu "SomeException matches all exception types" (gives' [True]) $ do
-excToMain1 = djfu "Throwing an unhandled exception to the main thread kills it" (gives [Left UncaughtException]) $ do
+      a <- catchSomeException
-  tid <- myThreadId
+           (throw Overflow)
-  throwTo tid Overflow
+           (\_ -> return True)
+      b <- catchSomeException
+           (throw $ IndexOutOfBounds "")
+           (\_ -> return True)
+      return (a && b)
 
-excToMain2 :: Test
+  , djfu "Exceptions thrown in a transaction can be caught outside it" (gives' [True]) $
-excToMain2 = djfu "Throwing a handled exception to the main thread does not kill it" (gives' [True]) $ do
+      catchArithException
-  tid <- myThreadId
+        (atomically $ throwSTM Overflow)
-  catchArithException (throwTo tid Overflow >> pure False) (\_ -> pure True)
+        (\_ -> return True)
 
-excMFail :: Test
+  , djfu "Throwing an unhandled exception to the main thread kills it" (gives [Left UncaughtException]) $ do
-excMFail = djfu "MonadConc is a MonadFail" (gives [Left UncaughtException]) $
+      tid <- myThreadId
-  (fail "hello world" :: MonadConc m => m ())
+      throwTo tid Overflow
+
+  , djfu "Throwing a handled exception to the main thread does not kill it" (gives' [True]) $ do
+      tid <- myThreadId
+      catchArithException (throwTo tid Overflow >> pure False) (\_ -> pure True)
+
+  , djfu "MonadConc is a MonadFail" (gives [Left UncaughtException]) $
+      (fail "hello world" :: MonadConc m => m ())  -- avoid an ambiguous type
+  ]
 
 --------------------------------------------------------------------------------
--- Capabilities
 
-capsGet :: Test
+capabilityTests :: [Test]
-capsGet = djfu "Reading the capabilities twice without update gives the same result" (gives' [True]) $ do
+capabilityTests =
-  c1 <- getNumCapabilities
+  [ djfu "Reading the capabilities twice without update gives the same result" (gives' [True]) $ do
-  c2 <- getNumCapabilities
+      c1 <- getNumCapabilities
-  return (c1 == c2)
+      c2 <- getNumCapabilities
+      return (c1 == c2)
 
-capsSet :: Test
+  , djfu "Getting the updated capabilities gives the new value" (gives' [True]) $ do
-capsSet = djfu "Getting the updated capabilities gives the new value" (gives' [True]) $ do
+      caps <- getNumCapabilities
-  caps <- getNumCapabilities
+      setNumCapabilities (caps + 1)
-  setNumCapabilities (caps + 1)
+      (== caps + 1) <$> getNumCapabilities
-  (== caps + 1) <$> getNumCapabilities
+  ]
 
 --------------------------------------------------------------------------------
--- Subconcurrency
 
-scDeadlock1 :: Test
+subconcurrencyTests :: [Test]
-scDeadlock1 = djfu "Failures in subconcurrency can be observed" (gives' [True]) $ do
+subconcurrencyTests =
-  x <- subconcurrency (newEmptyMVar >>= readMVar)
+  [ djfu "Failures in subconcurrency can be observed" (gives' [True]) $ do
-  pure (either (==Deadlock) (const False) x)
+      x <- subconcurrency (newEmptyMVar >>= readMVar)
+      pure (either (==Deadlock) (const False) x)
 
-scDeadlock2 :: Test
+  , djfu "Actions after a failing subconcurrency still happen" (gives' [True]) $ do
-scDeadlock2 = djfu "Actions after a failing subconcurrency still happen" (gives' [True]) $ do
+      var <- newMVarInt 0
-  var <- newMVarInt 0
+      x <- subconcurrency (putMVar var 1)
-  x <- subconcurrency (putMVar var 1)
+      y <- readMVar var
-  y <- readMVar var
+      pure (either (==Deadlock) (const False) x && y == 0)
-  pure (either (==Deadlock) (const False) x && y == 0)
 
-scSuccess :: Test
+  , djfu "Non-failing subconcurrency returns the final result" (gives' [True]) $ do
-scSuccess = djfu "Non-failing subconcurrency returns the final result" (gives' [True]) $ do
+      var <- newMVarInt 3
-  var <- newMVarInt 3
+      x <- subconcurrency (takeMVar var)
-  x <- subconcurrency (takeMVar var)
+      pure (either (const False) (==3) x)
-  pure (either (const False) (==3) x)
+  ]