From 8636fe9708e0b87afc08d6a8714f10f3efa18259 Mon Sep 17 00:00:00 2001 From: Michael Walker Date: Wed, 20 Sep 2017 09:05:23 +0100 Subject: [PATCH] Remove top-level definitions of individual tests --- dejafu-tests/Cases/MultiThreaded.hs | 446 ++++++++++++--------------- dejafu-tests/Cases/Refinement.hs | 75 ++--- dejafu-tests/Cases/SingleThreaded.hs | 431 +++++++++++--------------- 3 files changed, 398 insertions(+), 554 deletions(-) diff --git a/dejafu-tests/Cases/MultiThreaded.hs b/dejafu-tests/Cases/MultiThreaded.hs index 0673487..2f4f25a 100644 --- a/dejafu-tests/Cases/MultiThreaded.hs +++ b/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" - [ threadId1 - , threadId2 - , threadNoWait - ] - , testGroup "MVar" - [ mvarLock - , 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 - ] + [ testGroup "Threading" threadingTests + , testGroup "MVar" mvarTests + , testGroup "CRef" crefTests + , testGroup "STM" stmTests + , testGroup "Exceptions" exceptionTests + , testGroup "Daemons" daemonTests + , testGroup "Subconcurrency" subconcurrencyTests ] -------------------------------------------------------------------------------- --- Threading -threadId1 :: [Test] -threadId1 = djfuT "Fork reports the thread ID of the child" (gives' [True]) $ do - var <- newEmptyMVar - tid <- fork $ myThreadId >>= putMVar var - (tid ==) <$> readMVar var +threadingTests :: [Test] +threadingTests = toTestList + [ djfuT "Fork reports the thread ID of the child" (gives' [True]) $ do + var <- newEmptyMVar + tid <- fork $ myThreadId >>= putMVar var + (tid ==) <$> readMVar var -threadId2 :: [Test] -threadId2 = djfuT "Different threads have different thread IDs" (gives' [True]) $ do - tid <- spawn myThreadId - (/=) <$> myThreadId <*> readMVar tid + , djfuT "Different threads have different thread IDs" (gives' [True]) $ do + tid <- spawn myThreadId + (/=) <$> myThreadId <*> readMVar tid -threadNoWait :: [Test] -threadNoWait = djfuT "A thread doesn't wait for its children before terminating" (gives' [Nothing, Just ()]) $ do - x <- newCRef Nothing - void . fork . writeCRef x $ Just () - readCRef x + , djfuT "A thread doesn't wait for its children before terminating" (gives' [Nothing, Just ()]) $ do + x <- newCRef Nothing + _ <- fork . writeCRef x $ Just () + readCRef x + ] -------------------------------------------------------------------------------- --- @MVar@s -mvarLock :: [Test] -mvarLock = djfuT "Racey MVar computations may deadlock" (gives [Left Deadlock, Right 0]) $ do - a <- newEmptyMVar - b <- newEmptyMVar +mvarTests :: [Test] +mvarTests = toTestList + [ djfuT "Racey MVar computations may deadlock" (gives [Left Deadlock, Right 0]) $ do + 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 - - 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 - -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 + , djfuT "Racey MVar computations are nondeterministic" (gives' [0,1]) $ do + x <- newEmptyMVarInt + _ <- fork $ putMVar x 0 + _ <- fork $ putMVar x 1 + readMVar x + ] -------------------------------------------------------------------------------- --- @CRef@s -crefRace :: [Test] -crefRace = djfuT "Racey CRef computations are nondeterministic" (gives' [0,1]) $ do - x <- newCRef (0::Int) +crefTests :: [Test] +crefTests = toTestList + [ 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 - j2 <- spawn $ writeCRef x 1 + , djfuT "CASing CRef changes its value" (gives' [0,1]) $ do + x <- newCRefInt 0 + _ <- fork $ modifyCRefCAS x (\_ -> (1, ())) + readCRef x - takeMVar j1 - takeMVar j2 + , djfuT "Racey CAS computations are nondeterministic" (gives' [(True, 2), (False, 2)]) $ do + 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] -crefCASModify = djfuT "CASing CRef changes its value" (gives' [0,1]) $ do - x <- newCRef (0::Int) - fork $ modifyCRefCAS x (\_ -> (1, ())) - readCRef x - -crefCASRace :: [Test] -crefCASRace = djfuT "Racey CAS computations are nondeterministic" (gives' [(True, 2), (False, 2)]) $ do - x <- newCRef (0::Int) - 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) + , djfuT "A ticket is only good for one CAS" (gives' [(True, False, 1), (False, True, 2)]) $ do + x <- newCRefInt 0 + 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] -stmAtomic = djfuT "Transactions are atomic" (gives' [0,2]) $ do - x <- atomically $ newTVar (0::Int) - void . fork . atomically $ writeTVar x 1 >> writeTVar x 2 - atomically $ readTVar x +stmTests :: [Test] +stmTests = toTestList + [ djfuT "Transactions are atomic" (gives' [0,2]) $ do + x <- atomically $ newTVarInt 0 + _ <- fork . atomically $ writeTVar x 1 >> writeTVar x 2 + atomically $ readTVar x -stmLeftRetry :: [Test] -stmLeftRetry = djfuT "'retry' is the left identity of 'orElse'" (gives' [()]) $ do - x <- atomically $ newTVar Nothing - let readJust var = maybe retry pure =<< readTVar var - fork . atomically . writeTVar x $ Just () - atomically $ retry `orElse` readJust x + , djfuT "'retry' is the left identity of 'orElse'" (gives' [()]) $ do + x <- atomically $ newTVar Nothing + let readJust var = maybe retry pure =<< readTVar var + _ <- fork . atomically . writeTVar x $ Just () + atomically $ retry `orElse` readJust x -stmRightRetry :: [Test] -stmRightRetry = djfuT "'retry' is the right identity of 'orElse'" (gives' [()]) $ do - x <- atomically $ newTVar Nothing - let readJust var = maybe retry pure =<< readTVar var - fork . atomically . writeTVar x $ Just () - atomically $ readJust x `orElse` retry + , djfuT "'retry' is the right identity of 'orElse'" (gives' [()]) $ do + x <- atomically $ newTVar Nothing + let readJust var = maybe retry pure =<< readTVar var + fork . atomically . writeTVar x $ Just () + atomically $ readJust x `orElse` retry -stmIssue55 :: [Test] -stmIssue55 = djfuT "https://github.com/barrucadu/dejafu/issues/55" (gives' [True]) $ do - a <- atomically $ newTQueue - b <- atomically $ newTQueue - fork . atomically $ writeTQueue b True - let both a b = readTQueue a `orElse` readTQueue b `orElse` retry - atomically $ both a b + , djfuT "https://github.com/barrucadu/dejafu/issues/55" (gives' [True]) $ do + a <- atomically $ newTQueue + b <- atomically $ newTQueue + _ <- fork . atomically $ writeTQueue b True + let both x y = readTQueue x `orElse` readTQueue y `orElse` retry + atomically $ both a b -stmIssue111 :: [Test] -stmIssue111 = djfuT "https://github.com/barrucadu/dejafu/issues/111" (gives' [1]) $ do - v <- atomically $ newTVar 1 - fork . atomically $ do - writeTVar v 2 - writeTVar v 3 - retry - atomically $ readTVar v + , djfuT "https://github.com/barrucadu/dejafu/issues/111" (gives' [1]) $ do + v <- atomically $ newTVarInt 1 + _ <- fork . atomically $ do + writeTVar v 2 + writeTVar v 3 + retry + atomically $ readTVar v + ] -------------------------------------------------------------------------------- --- Exceptions -threadKill :: [Test] -threadKill = djfuT "Exceptions can kill unmasked threads" (gives [Left Deadlock, Right ()]) $ do - x <- newEmptyMVar - tid <- fork $ putMVar x () - killThread tid - readMVar x +exceptionTests :: [Test] +exceptionTests = toTestList + [ djfuT "Exceptions can kill unmasked threads" (gives [Left Deadlock, Right ()]) $ do + x <- newEmptyMVar + tid <- fork $ putMVar x () + killThread tid + readMVar x -threadKillMask :: [Test] -threadKillMask = djfuT "Exceptions cannot kill nonblocking masked threads" (gives' [()]) $ do - x <- newEmptyMVar - y <- newEmptyMVar - tid <- fork $ mask $ \_ -> putMVar x () >> putMVar y () - readMVar x - killThread tid - readMVar y + , djfuT "Exceptions cannot kill nonblocking masked threads" (gives' [()]) $ do + x <- newEmptyMVar + y <- newEmptyMVar + tid <- fork $ mask $ \_ -> putMVar x () >> putMVar y () + readMVar x + killThread tid + readMVar y -threadKillUninterruptibleMask :: [Test] -threadKillUninterruptibleMask = djfuT "Throwing to an uninterruptible thread blocks" (gives [Left Deadlock]) $ do - x <- newEmptyMVar - y <- newEmptyMVar - tid <- fork $ uninterruptibleMask $ \_ -> putMVar x () >> takeMVar y - readMVar x - killThread tid + , djfuT "Throwing to an uninterruptible thread blocks" (gives [Left Deadlock]) $ do + x <- newEmptyMVar + y <- newEmptyMVar + tid <- fork $ uninterruptibleMask $ \_ -> putMVar x () >> takeMVar y + readMVar x + killThread tid -threadKillUmask :: [Test] -threadKillUmask = djfuT "Exceptions can kill nonblocking masked threads which have unmasked" (gives [Left Deadlock, Right ()]) $ do - x <- newEmptyMVar - y <- newEmptyMVar - tid <- fork $ mask $ \umask -> putMVar x () >> umask (putMVar y ()) - readMVar x - killThread tid - readMVar y + , djfuT "Exceptions can kill masked threads which have unmasked" (gives [Left Deadlock, Right ()]) $ do + x <- newEmptyMVar + y <- newEmptyMVar + tid <- fork $ mask $ \umask -> putMVar x () >> umask (putMVar y ()) + readMVar x + killThread tid + readMVar y -threadKillToMain1 :: [Test] -threadKillToMain1 = djfuT "Throwing to main kills the computation, if unhandled" (gives [Left UncaughtException]) $ do - tid <- myThreadId - j <- spawn $ throwTo tid Overflow - readMVar j + , djfuT "Throwing to main kills the computation, if unhandled" (gives [Left UncaughtException]) $ do + tid <- myThreadId + j <- spawn $ throwTo tid Overflow + readMVar j -threadKillToMain2 :: [Test] -threadKillToMain2 = djfuT "Throwing to main doesn't kill the computation, if handled" (gives' [()]) $ do - tid <- myThreadId - catchArithException (spawn (throwTo tid Overflow) >>= readMVar) - (\_ -> pure ()) + , djfuT "Throwing to main doesn't kill the computation, if handled" (gives' [()]) $ do + tid <- myThreadId + catchArithException + (spawn (throwTo tid Overflow) >>= readMVar) + (\_ -> pure ()) + ] ------------------------------------------------------------------------------- --- Daemon threads -schedDaemon :: [Test] -schedDaemon = djfuT "https://github.com/barrucadu/dejafu/issues/40" (gives' [0,1]) $ do - x <- newCRef 0 - _ <- fork $ myThreadId >> writeCRef x 1 - readCRef x +daemonTests :: [Test] +daemonTests = toTestList + [ djfuT "https://github.com/barrucadu/dejafu/issues/40" (gives' [0,1]) $ do + x <- newCRefInt 0 + _ <- fork $ myThreadId >> writeCRef x 1 + readCRef x + ] -------------------------------------------------------------------------------- --- Subconcurrency -scDeadlock1 :: [Test] -scDeadlock1 = djfuT "Failure is observable" (gives' [Left Deadlock, Right ()]) $ do - var <- newEmptyMVar - subconcurrency $ do - void . fork $ putMVar var () - putMVar var () +subconcurrencyTests :: [Test] +subconcurrencyTests = toTestList + [ djfuT "Failure is observable" (gives' [Left Deadlock, Right ()]) $ do + var <- newEmptyMVar + subconcurrency $ do + _ <- fork $ putMVar var () + putMVar var () -scDeadlock2 :: [Test] -scDeadlock2 = djfuT "Failure does not abort the outer computation" (gives' [(Left Deadlock, ()), (Right (), ())]) $ do - var <- newEmptyMVar - res <- subconcurrency $ do - void . fork $ putMVar var () - putMVar var () - (,) <$> pure res <*> readMVar var + , djfuT "Failure does not abort the outer computation" (gives' [(Left Deadlock, ()), (Right (), ())]) $ do + var <- newEmptyMVar + res <- subconcurrency $ do + _ <- fork $ putMVar var () + putMVar var () + (,) <$> pure res <*> readMVar var -scSuccess :: [Test] -scSuccess = djfuT "Success is observable" (gives' [Right ()]) $ do - var <- newMVar () - subconcurrency $ do - out <- newEmptyMVar - void . fork $ takeMVar var >>= putMVar out - takeMVar out + , djfuT "Success is observable" (gives' [Right ()]) $ do + var <- newMVar () + subconcurrency $ do + out <- newEmptyMVar + _ <- fork $ takeMVar var >>= putMVar out + takeMVar out -scIllegal :: [Test] -scIllegal = djfuT "It is illegal to start subconcurrency after forking" (gives [Left IllegalSubconcurrency]) $ do - var <- newEmptyMVar - void . fork $ readMVar var - void . subconcurrency $ pure () + , djfuT "It is illegal to start subconcurrency after forking" (gives [Left IllegalSubconcurrency]) $ do + var <- newEmptyMVar + _ <- fork $ readMVar var + _ <- subconcurrency $ pure () + pure () -scIssue71 :: [Test] -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 () } - s <- newEmptyMVar - _ <- subconcurrency (takeMVar s ||| pure ()) - pure () + , 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 () } + s <- newEmptyMVar + _ <- subconcurrency (takeMVar s ||| pure ()) + pure () -scIssue81 :: [Test] -scIssue81 = djfuT "https://github.com/barrucadu/dejafu/issues/81" (gives' [(Right (),0)]) $ do - s <- newQSemN 0 - let interfere = waitQSemN s 0 >> signalQSemN s 0 - x <- subconcurrency (signalQSemN s 0 ||| waitQSemN s 0 ||| interfere) - o <- remainingQSemN s - pure (x, o) + , djfuT "https://github.com/barrucadu/dejafu/issues/81" (gives' [(Right (),0)]) $ do + s <- newQSemN 0 + let interfere = waitQSemN s 0 >> signalQSemN s 0 + x <- subconcurrency (signalQSemN s 0 ||| waitQSemN s 0 ||| interfere) + o <- remainingQSemN s + pure (x, o) + ] diff --git a/dejafu-tests/Cases/Refinement.hs b/dejafu-tests/Cases/Refinement.hs index 485daf8..401a58e 100644 --- a/dejafu-tests/Cases/Refinement.hs +++ b/dejafu-tests/Cases/Refinement.hs @@ -9,24 +9,9 @@ import Test.HUnit.DejaFu (testProperty) import Common tests :: [Test] -tests = - [ 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 - ] - ] +tests = [ testGroup "MVar" mvarProps ] ------------------------------------------------------------------------------- --- 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. -prop_mvar_read_idempotent_s = - mvar readMVar === mvar (\v -> readMVar v >> readMVar v) +mvarProps :: [Test] +mvarProps = toTestList + [ testProperty "readMVar is idempotent when composed sequentially" $ + mvar readMVar === mvar (\v -> readMVar v >> readMVar v) --- | @readMVar@ is idempotent when composed concurrently. -prop_mvar_read_idempotent_c = - mvar readMVar === mvar (\v -> readMVar v ||| readMVar v) + , testProperty "readMVar is idempotent when composed concurrently" $ + mvar readMVar === mvar (\v -> readMVar v ||| readMVar v) --- | @readMVar@ is not equivalent to a take followed by a put. -prop_mvar_read_neq_take_put = expectFailure $ - mvar readMVar === mvar (\v -> takeMVar v >>= putMVar v) + , testProperty "readMVar is not equivalent to a take followed by a put" $ + expectFailure $ mvar readMVar === mvar (\v -> takeMVar v >>= putMVar v) --- | @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) + , testProperty "readMVar is a strict refinement of a take followed by a put" $ + mvar readMVar ->- mvar (\v -> takeMVar v >>= putMVar v) --- | @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) + , testProperty "takeMVar is equivalent to a read followed by a take" $ + mvar takeMVar === mvar (\v -> readMVar v >> takeMVar v) --- | @takeMVar@ is not equivalent to a read concurrently composed with a take. -prop_mvar_take_neq_read_take_c = expectFailure $ - mvar takeMVar === mvar (\v -> readMVar v ||| takeMVar v) + , testProperty "takeMVar is not equivalent to a read concurrently composed with a take" $ + expectFailure $ mvar takeMVar === mvar (\v -> readMVar v ||| takeMVar v) --- | @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) + , testProperty "takeMVar is a strict refinement of a read concurrently composed with a take" $ + mvar takeMVar ->- mvar (\v -> readMVar v ||| takeMVar v) --- | @putMVar@ is not equivalent to a put followed by a read. -prop_mvar_put_neq_put_read_s x = expectFailure $ - mvar (\v -> putMVar v x) === mvar (\v -> putMVar v x >> readMVar v) + , testProperty "putMVar is not equivalent to a put followed by a read" $ + \x -> expectFailure $ mvar (\v -> putMVar v x) === mvar (\v -> putMVar v x >> readMVar v) --- | @putMVar@ is a strict refinement of a put followed by a read. -prop_mvar_put_sr_put_read_s x = - mvar (\v -> putMVar v x) ->- mvar (\v -> putMVar v x >> readMVar v) + , testProperty "putMVar is a strict refinement of a put followed by a read" $ + \x -> mvar (\v -> putMVar v x) ->- mvar (\v -> putMVar v x >> readMVar v) --- | @putMVar@ is not equivalent to a put concurrently composed with a read. -prop_mvar_put_neq_put_read_c x = expectFailure $ - mvar (\v -> putMVar v x) === mvar (\v -> putMVar v x ||| readMVar v) + , testProperty "putMVar is not equivalent to a put concurrently composed with a read" $ + \x -> expectFailure $ 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. -prop_mvar_put_sr_put_read_c x = - mvar (\v -> putMVar v x) ->- mvar (\v -> putMVar v x ||| readMVar v) + , testProperty "putMVar is a strict refinement of a put concurrently composed with a read" $ + \x -> mvar (\v -> putMVar v x) ->- mvar (\v -> putMVar v x ||| readMVar v) + ] diff --git a/dejafu-tests/Cases/SingleThreaded.hs b/dejafu-tests/Cases/SingleThreaded.hs index 93d0738..decfebd 100644 --- a/dejafu-tests/Cases/SingleThreaded.hs +++ b/dejafu-tests/Cases/SingleThreaded.hs @@ -16,309 +16,232 @@ import Control.Applicative ((<$>), (<*>)) tests :: [Test] tests = - [ testGroup "MVar" - [ emptyMVarPut - , emptyMVarTryPut - , emptyMVarTake - , emptyMVarTryTake - , emptyMVarRead - , 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 - ] + [ testGroup "MVar" mvarTests + , testGroup "CRef" crefTests + , testGroup "STM" stmTests + , testGroup "Exceptions" exceptionTests + , testGroup "Capabilities" capabilityTests + , testGroup "Subconcurrency" subconcurrencyTests ] -------------------------------------------------------------------------------- --- @MVar@s -emptyMVarTake :: Test -emptyMVarTake = djfu "Taking from an empty MVar blocks" (gives [Left Deadlock]) $ do - var <- newEmptyMVarInt - takeMVar var +mvarTests :: [Test] +mvarTests = + [ djfu "Taking from an empty MVar blocks" (gives [Left Deadlock]) $ do + var <- newEmptyMVarInt + takeMVar var -emptyMVarTryTake :: Test -emptyMVarTryTake = djfu "Non-blockingly taking from an empty MVar gives nothing" (gives' [Nothing]) $ do - var <- newEmptyMVarInt - tryTakeMVar var + , djfu "Non-blockingly taking from an empty MVar gives nothing" (gives' [Nothing]) $ do + var <- newEmptyMVarInt + tryTakeMVar var -emptyMVarPut :: Test -emptyMVarPut = djfu "Putting into an empty MVar updates it" (gives' [True]) $ do - var <- newEmptyMVarInt - putMVar var 7 - (==7) <$> readMVar var + , djfu "Putting into an empty MVar updates it" (gives' [True]) $ do + var <- newEmptyMVarInt + putMVar var 7 + (==7) <$> readMVar var -emptyMVarTryPut :: Test -emptyMVarTryPut = djfu "Non-blockingly putting into an empty MVar updates it" (gives' [True]) $ do - var <- newEmptyMVarInt - _ <- tryPutMVar var 7 - (==7) <$> readMVar var + , djfu "Non-blockingly putting into an empty MVar updates it" (gives' [True]) $ do + var <- newEmptyMVarInt + _ <- tryPutMVar var 7 + (==7) <$> readMVar var -emptyMVarRead :: Test -emptyMVarRead = djfu "Reading an empty MVar blocks" (gives [Left Deadlock]) $ do - var <- newEmptyMVarInt - readMVar var + , djfu "Reading an empty MVar blocks" (gives [Left Deadlock]) $ do + var <- newEmptyMVarInt + readMVar var -emptyMVarTryRead :: Test -emptyMVarTryRead = djfu "Non-blockingly reading an empty MVar gives nothing" (gives' [Nothing]) $ do - var <- newEmptyMVarInt - tryReadMVar var + , djfu "Non-blockingly reading an empty MVar gives nothing" (gives' [Nothing]) $ do + var <- newEmptyMVarInt + tryReadMVar var -fullMVarPut :: Test -fullMVarPut = djfu "Putting into a full MVar blocks" (gives [Left Deadlock]) $ do - var <- newMVarInt 7 - putMVar var 10 + , djfu "Putting into a full MVar blocks" (gives [Left Deadlock]) $ do + var <- newMVarInt 7 + putMVar var 10 -fullMVarTryPut :: Test -fullMVarTryPut = djfu "Non-blockingly putting into a full MVar fails" (gives' [False]) $ do - var <- newMVarInt 7 - tryPutMVar var 10 + , djfu "Non-blockingly putting into a full MVar fails" (gives' [False]) $ do + var <- newMVarInt 7 + tryPutMVar var 10 -fullMVarTake :: Test -fullMVarTake = djfu "Taking from a full MVar works" (gives' [True]) $ do - var <- newMVarInt 7 - (==7) <$> takeMVar var + , djfu "Taking from a full MVar works" (gives' [True]) $ do + var <- newMVarInt 7 + (==7) <$> takeMVar var -fullMVarTryTake :: Test -fullMVarTryTake = djfu "Non-blockingly taking from a full MVar works" (gives' [True]) $ do - var <- newMVarInt 7 - (==Just 7) <$> tryTakeMVar var + , djfu "Non-blockingly taking from a full MVar works" (gives' [True]) $ do + var <- newMVarInt 7 + (==Just 7) <$> tryTakeMVar var -fullMVarRead :: Test -fullMVarRead = djfu "Reading a full MVar works" (gives' [True]) $ do - var <- newMVarInt 7 - (==7) <$> readMVar var + , djfu "Reading a full MVar works" (gives' [True]) $ do + var <- newMVarInt 7 + (==7) <$> readMVar var -fullMVarTryRead :: Test -fullMVarTryRead = djfu "Non-blockingly reading a full MVar works" (gives' [True]) $ do - var <- newMVarInt 7 - (==Just 7) <$> tryReadMVar var + , djfu "Non-blockingly reading a full MVar works" (gives' [True]) $ do + var <- newMVarInt 7 + (==Just 7) <$> tryReadMVar var + ] -------------------------------------------------------------------------------- --- @CRef@s -crefRead :: Test -crefRead = djfu "Reading a non-updated CRef gives its initial value" (gives' [True]) $ do - ref <- newCRefInt 5 - (5==) <$> readCRef ref +crefTests :: [Test] +crefTests = + [ djfu "Reading a non-updated CRef gives its initial value" (gives' [True]) $ do + ref <- newCRefInt 5 + (5==) <$> readCRef ref -crefWrite :: Test -crefWrite = djfu "Reading an updated CRef gives its new value" (gives' [True]) $ do - ref <- newCRefInt 5 - writeCRef ref 6 - (6==) <$> readCRef ref + , djfu "Reading an updated CRef gives its new value" (gives' [True]) $ do + ref <- newCRefInt 5 + writeCRef ref 6 + (6==) <$> readCRef ref -crefModify :: Test -crefModify = djfu "Updating a CRef by a function changes its value" (gives' [True]) $ do - ref <- newCRefInt 5 - atomicModifyCRef ref (\i -> (i+1, ())) - (6==) <$> readCRef ref + , djfu "Updating a CRef by a function changes its value" (gives' [True]) $ do + ref <- newCRefInt 5 + atomicModifyCRef ref (\i -> (i+1, ())) + (6==) <$> readCRef ref -crefTicketPeek :: Test -crefTicketPeek = djfu "A ticket contains the value of the CRef at the time of its creation" (gives' [True]) $ do - ref <- newCRefInt 5 - tick <- readForCAS ref - writeCRef ref 6 - (5==) <$> peekTicket tick + , djfu "A ticket contains the value of the CRef at the time of its creation" (gives' [True]) $ do + ref <- newCRefInt 5 + tick <- readForCAS ref + writeCRef ref 6 + (5==) <$> peekTicket tick -crefTicketPeek2 :: Test -crefTicketPeek2 = djfu "Compare-and-swap returns a ticket containing the new value" (gives' [True]) $ do - ref <- newCRefInt 5 - tick <- readForCAS ref - (_, tick') <- casCRef ref tick 6 - (6==) <$> peekTicket tick' + , djfu "Compare-and-swap returns a ticket containing the new value" (gives' [True]) $ do + ref <- newCRefInt 5 + tick <- readForCAS ref + (_, tick') <- casCRef ref tick 6 + (6==) <$> peekTicket tick' -crefCas1 :: Test -crefCas1 = djfu "Compare-and-swap on an unmodified CRef succeeds" (gives' [True]) $ do - ref <- newCRefInt 5 - tick <- readForCAS ref - (suc, _) <- casCRef ref tick 6 - val <- readCRef ref - return (suc && (6 == val)) + , djfu "Compare-and-swap on an unmodified CRef succeeds" (gives' [True]) $ do + ref <- newCRefInt 5 + tick <- readForCAS ref + (suc, _) <- casCRef ref tick 6 + val <- readCRef ref + return (suc && (6 == val)) -crefCas2 :: Test -crefCas2 = djfu "Compare-and-swap on a modified CRef fails" (gives' [True]) $ do - ref <- newCRefInt 5 - tick <- readForCAS ref - writeCRef ref 6 - (suc, _) <- casCRef ref tick 7 - val <- readCRef ref - return (not suc && not (7 == val)) + , djfu "Compare-and-swap on a modified CRef fails" (gives' [True]) $ do + ref <- newCRefInt 5 + tick <- readForCAS ref + writeCRef ref 6 + (suc, _) <- casCRef ref tick 7 + val <- readCRef ref + return (not suc && not (7 == val)) + ] -------------------------------------------------------------------------------- --- STM -stmWrite :: Test -stmWrite = djfu "When a TVar is updated in a transaction, its new value is visible later in the transaction" (gives' [True]) $ - (6==) <$> atomically (do { v <- newTVarInt 5; writeTVar v 6; readTVar v }) +stmTests :: [Test] +stmTests = + [ 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 -stmPreserve = djfu "When a TVar is updated, its new value is visible in a later transaction" (gives' [True]) $ do - ctv <- atomically $ newTVarInt 5 - (5==) <$> atomically (readTVar ctv) + , djfu "When a TVar is updated, its new value is visible in a later transaction" (gives' [True]) $ do + ctv <- atomically $ newTVarInt 5 + (5==) <$> atomically (readTVar ctv) -stmRetry :: Test -stmRetry = djfu "Aborting a transaction blocks the thread" (gives [Left STMDeadlock]) $ - (atomically retry :: MonadConc m => m ()) -- avoid an ambiguous type + , djfu "Aborting a transaction blocks the thread" (gives [Left STMDeadlock]) $ + (atomically retry :: MonadConc m => m ()) -- avoid an ambiguous type -stmOrElse :: Test -stmOrElse = djfu "Aborting a transaction can be caught and recovered from" (gives' [True]) $ do - ctv <- atomically $ newTVarInt 5 - atomically $ orElse retry (writeTVar ctv 6) - (6==) <$> atomically (readTVar ctv) + , djfu "Aborting a transaction can be caught and recovered from" (gives' [True]) $ do + ctv <- atomically $ newTVarInt 5 + atomically $ orElse retry (writeTVar ctv 6) + (6==) <$> atomically (readTVar ctv) -stmCatch1 :: Test -stmCatch1 = djfu "An exception thrown in a transaction can be caught" (gives' [True]) $ do - ctv <- atomically $ newTVarInt 5 - atomically $ catchArithException - (throwSTM Overflow) - (\_ -> writeTVar ctv 6) - (6==) <$> atomically (readTVar ctv) + , djfu "An exception thrown in a transaction can be caught" (gives' [True]) $ do + ctv <- atomically $ newTVarInt 5 + atomically $ catchArithException + (throwSTM Overflow) + (\_ -> writeTVar ctv 6) + (6==) <$> atomically (readTVar ctv) -stmCatch2 :: Test -stmCatch2 = djfu "Nested exception handlers in transactions work" (gives' [True]) $ do - ctv <- atomically $ newTVarInt 5 - atomically $ catchArithException - (catchArrayException - (throwSTM Overflow) - (\_ -> writeTVar ctv 0)) - (\_ -> writeTVar ctv 6) - (6==) <$> atomically (readTVar ctv) + , djfu "Nested exception handlers in transactions work" (gives' [True]) $ do + ctv <- atomically $ newTVarInt 5 + atomically $ catchArithException + (catchArrayException + (throwSTM Overflow) + (\_ -> writeTVar ctv 0)) + (\_ -> writeTVar ctv 6) + (6==) <$> atomically (readTVar ctv) -stmMFail :: Test -stmMFail = djfu "MonadSTM is a MonadFail" (gives [Left UncaughtException]) $ - (atomically $ fail "hello world" :: MonadConc m => m ()) + , djfu "MonadSTM is a MonadFail" (gives [Left UncaughtException]) $ + (atomically $ fail "hello world" :: MonadConc m => m ()) -- avoid an ambiguous type + ] -------------------------------------------------------------------------------- --- Exceptions -excCatch :: Test -excCatch = djfu "An exception thrown can be caught" (gives' [True]) $ - catchArithException - (throw Overflow) - (\_ -> 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 +exceptionTests :: [Test] +exceptionTests = + [ djfu "An exception thrown can be caught" (gives' [True]) $ + catchArithException (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 -excSTM = djfu "Exceptions thrown in a transaction can be caught outside it" (gives' [True]) $ - catchArithException - (atomically $ throwSTM Overflow) - (\_ -> return True) + , djfu "Uncaught exceptions kill the computation" (gives [Left UncaughtException]) $ + catchArithException + (throw $ IndexOutOfBounds "") + (\_ -> return False) -excToMain1 :: Test -excToMain1 = djfu "Throwing an unhandled exception to the main thread kills it" (gives [Left UncaughtException]) $ do - tid <- myThreadId - throwTo tid Overflow + , djfu "SomeException matches all exception types" (gives' [True]) $ do + a <- catchSomeException + (throw Overflow) + (\_ -> return True) + b <- catchSomeException + (throw $ IndexOutOfBounds "") + (\_ -> return True) + return (a && b) -excToMain2 :: Test -excToMain2 = 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 "Exceptions thrown in a transaction can be caught outside it" (gives' [True]) $ + catchArithException + (atomically $ throwSTM Overflow) + (\_ -> return True) -excMFail :: Test -excMFail = djfu "MonadConc is a MonadFail" (gives [Left UncaughtException]) $ - (fail "hello world" :: MonadConc m => m ()) + , djfu "Throwing an unhandled exception to the main thread kills it" (gives [Left UncaughtException]) $ do + tid <- myThreadId + 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 -capsGet = djfu "Reading the capabilities twice without update gives the same result" (gives' [True]) $ do - c1 <- getNumCapabilities - c2 <- getNumCapabilities - return (c1 == c2) +capabilityTests :: [Test] +capabilityTests = + [ djfu "Reading the capabilities twice without update gives the same result" (gives' [True]) $ do + c1 <- getNumCapabilities + c2 <- getNumCapabilities + return (c1 == c2) -capsSet :: Test -capsSet = djfu "Getting the updated capabilities gives the new value" (gives' [True]) $ do - caps <- getNumCapabilities - setNumCapabilities (caps + 1) - (== caps + 1) <$> getNumCapabilities + , djfu "Getting the updated capabilities gives the new value" (gives' [True]) $ do + caps <- getNumCapabilities + setNumCapabilities (caps + 1) + (== caps + 1) <$> getNumCapabilities + ] -------------------------------------------------------------------------------- --- Subconcurrency -scDeadlock1 :: Test -scDeadlock1 = djfu "Failures in subconcurrency can be observed" (gives' [True]) $ do - x <- subconcurrency (newEmptyMVar >>= readMVar) - pure (either (==Deadlock) (const False) x) +subconcurrencyTests :: [Test] +subconcurrencyTests = + [ djfu "Failures in subconcurrency can be observed" (gives' [True]) $ do + x <- subconcurrency (newEmptyMVar >>= readMVar) + pure (either (==Deadlock) (const False) x) -scDeadlock2 :: Test -scDeadlock2 = djfu "Actions after a failing subconcurrency still happen" (gives' [True]) $ do - var <- newMVarInt 0 - x <- subconcurrency (putMVar var 1) - y <- readMVar var - pure (either (==Deadlock) (const False) x && y == 0) + , djfu "Actions after a failing subconcurrency still happen" (gives' [True]) $ do + var <- newMVarInt 0 + x <- subconcurrency (putMVar var 1) + y <- readMVar var + pure (either (==Deadlock) (const False) x && y == 0) -scSuccess :: Test -scSuccess = djfu "Non-failing subconcurrency returns the final result" (gives' [True]) $ do - var <- newMVarInt 3 - x <- subconcurrency (takeMVar var) - pure (either (const False) (==3) x) + , djfu "Non-failing subconcurrency returns the final result" (gives' [True]) $ do + var <- newMVarInt 3 + x <- subconcurrency (takeMVar var) + pure (either (const False) (==3) x) + ]