mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-18 02:51:42 +03:00
Give test cases more descriptive names
This commit is contained in:
Michael Walker
parent
58ab0e2c2f
commit
fb13d62218
@ -2,16 +2,18 @@ module Cases.Discard where
|
||||
|
||||
import Control.Concurrent.Classy
|
||||
import Test.DejaFu (gives')
|
||||
import Test.Framework (Test)
|
||||
import Test.Framework.Providers.HUnit (hUnitTestToTests)
|
||||
import Test.HUnit (test)
|
||||
import Test.HUnit.DejaFu (Discard(..), defaultMemType, defaultWay, testDejafuDiscard)
|
||||
|
||||
import Common
|
||||
|
||||
tests :: [Test]
|
||||
tests = hUnitTestToTests $ test
|
||||
[ check "all results" [1, 2, 3] (const Nothing)
|
||||
, check "no results" [] (const $ Just DiscardResultAndTrace)
|
||||
, check "some results" [1, 2] (\x -> if x == Right 3 then Just DiscardResultAndTrace else Nothing)
|
||||
tests = toTestList
|
||||
[ check "All results are kept when none are discarded" [1, 2, 3] $
|
||||
const Nothing
|
||||
, check "No results are kept when all are discarded" [] $
|
||||
const (Just DiscardResultAndTrace)
|
||||
, check "Results failing the test are not present" [1, 2] $
|
||||
\x -> if x == Right 3 then Just DiscardResultAndTrace else Nothing
|
||||
]
|
||||
where
|
||||
check name xs f = testDejafuDiscard f defaultWay defaultMemType nondet name (gives' xs)
|
||||
@ -19,7 +21,7 @@ tests = hUnitTestToTests $ test
|
||||
nondet :: MonadConc m => m Int
|
||||
nondet = do
|
||||
mvar <- newEmptyMVar
|
||||
fork $ putMVar mvar 1
|
||||
fork $ putMVar mvar 2
|
||||
fork $ putMVar mvar 3
|
||||
_ <- fork $ putMVar mvar 1
|
||||
_ <- fork $ putMVar mvar 2
|
||||
_ <- fork $ putMVar mvar 3
|
||||
readMVar mvar
|
||||
|
||||
@ -17,45 +17,31 @@ import Control.Monad.Conc.Class
|
||||
|
||||
tests :: [Test]
|
||||
tests =
|
||||
[ litmusTest "intelWP21" intelWP21
|
||||
[(0,0),(0,1),(1,1)]
|
||||
[(0,0),(0,1),(1,1)]
|
||||
[(0,0),(0,1),(1,1)]
|
||||
[ let out = [(a,b) | a <- [0..1], b <- [0..1], (a,b) /= (1,0)]
|
||||
in litmusTest "Loads are not reordered with other loads and stores are not reordered with other stores" intelWP21 out out out
|
||||
|
||||
, litmusTest "intelWP22" intelWP22
|
||||
[(0,0),(0,1),(1,0)]
|
||||
[(0,0),(0,1),(1,0)]
|
||||
[(0,0),(0,1),(1,0)]
|
||||
, let out = [(a,b) | a <- [0..1], b <- [0..1], (a,b) /= (1,1)]
|
||||
in litmusTest "Stores are not reordered with older loads" intelWP22 out out out
|
||||
|
||||
, litmusTest "intelWP23" intelWP23
|
||||
[(0,1),(1,0),(1,1)]
|
||||
[(0,0),(0,1),(1,0),(1,1)]
|
||||
[(0,0),(0,1),(1,0),(1,1)]
|
||||
, let sq = [(a,b) | a <- [0..1], b <- [0..1], (a,b) /= (0,0)]
|
||||
rel = [(a,b) | a <- [0..1], b <- [0..1]]
|
||||
in litmusTest "Loads may be reordered with older stores to different locations" intelWP23 sq rel rel
|
||||
|
||||
, litmusTest "intelWP24" intelWP24
|
||||
[(1,1)]
|
||||
[(1,1)]
|
||||
[(1,1)]
|
||||
, let out = [(1,1)]
|
||||
in litmusTest "Loads are not reordered with older stores to the same location" intelWP24 out out out
|
||||
|
||||
, litmusTest "intelWP25" intelWP25
|
||||
[((1,0),(1,1)),((1,1),(1,0)),((1,1),(1,1))]
|
||||
[((1,0),(1,0)),((1,0),(1,1)),((1,1),(1,0)),((1,1),(1,1))]
|
||||
[((1,0),(1,0)),((1,0),(1,1)),((1,1),(1,0)),((1,1),(1,1))]
|
||||
, let sq = [((1,0),(1,1)),((1,1),(1,0)),((1,1),(1,1))]
|
||||
rel = [((1,0),(1,0)),((1,0),(1,1)),((1,1),(1,0)),((1,1),(1,1))]
|
||||
in litmusTest "Intra-processor forwarding is allowed" intelWP25 sq rel rel
|
||||
|
||||
, litmusTest "intelWP26" intelWP26
|
||||
[(0,0,0),(0,0,1),(1,0,0),(1,0,1)]
|
||||
[(0,0,0),(0,0,1),(1,0,0),(1,0,1)]
|
||||
[(0,0,0),(0,0,1),(1,0,0),(1,0,1)]
|
||||
, let out = [(0,0,0),(0,0,1),(1,0,0),(1,0,1)]
|
||||
in litmusTest "Stores are transitively visible" intelWP26 out out out
|
||||
|
||||
, litmusTest "intelWP27" intelWP27
|
||||
[((0,0),(0,0)),((0,0),(0,1)),((0,0),(0,2)),((0,0),(1,1)),((0,0),(1,2)),((0,0),(2,1)),((0,0),(2,2)),((0,1),(0,0)),((0,1),(0,1)),((0,1),(0,2)),((0,1),(1,1)),((0,1),(1,2)),((0,1),(2,1)),((0,1),(2,2)),((0,2),(0,0)),((0,2),(0,1)),((0,2),(0,2)),((0,2),(1,1)),((0,2),(1,2)),((0,2),(2,1)),((0,2),(2,2)),((1,1),(0,0)),((1,1),(0,1)),((1,1),(0,2)),((1,1),(1,1)),((1,1),(1,2)),((1,1),(2,1)),((1,1),(2,2)),((1,2),(0,0)),((1,2),(0,1)),((1,2),(0,2)),((1,2),(1,1)),((1,2),(1,2)),((1,2),(2,2)),((2,1),(0,0)),((2,1),(0,1)),((2,1),(0,2)),((2,1),(1,1)),((2,1),(2,1)),((2,1),(2,2)),((2,2),(0,0)),((2,2),(0,1)),((2,2),(0,2)),((2,2),(1,1)),((2,2),(1,2)),((2,2),(2,1)),((2,2),(2,2))]
|
||||
[((0,0),(0,0)),((0,0),(0,1)),((0,0),(0,2)),((0,0),(1,1)),((0,0),(1,2)),((0,0),(2,1)),((0,0),(2,2)),((0,1),(0,0)),((0,1),(0,1)),((0,1),(0,2)),((0,1),(1,1)),((0,1),(1,2)),((0,1),(2,1)),((0,1),(2,2)),((0,2),(0,0)),((0,2),(0,1)),((0,2),(0,2)),((0,2),(1,1)),((0,2),(1,2)),((0,2),(2,1)),((0,2),(2,2)),((1,1),(0,0)),((1,1),(0,1)),((1,1),(0,2)),((1,1),(1,1)),((1,1),(1,2)),((1,1),(2,1)),((1,1),(2,2)),((1,2),(0,0)),((1,2),(0,1)),((1,2),(0,2)),((1,2),(1,1)),((1,2),(1,2)),((1,2),(2,2)),((2,1),(0,0)),((2,1),(0,1)),((2,1),(0,2)),((2,1),(1,1)),((2,1),(2,1)),((2,1),(2,2)),((2,2),(0,0)),((2,2),(0,1)),((2,2),(0,2)),((2,2),(1,1)),((2,2),(1,2)),((2,2),(2,1)),((2,2),(2,2))]
|
||||
[((0,0),(0,0)),((0,0),(0,1)),((0,0),(0,2)),((0,0),(1,1)),((0,0),(1,2)),((0,0),(2,1)),((0,0),(2,2)),((0,1),(0,0)),((0,1),(0,1)),((0,1),(0,2)),((0,1),(1,1)),((0,1),(1,2)),((0,1),(2,1)),((0,1),(2,2)),((0,2),(0,0)),((0,2),(0,1)),((0,2),(0,2)),((0,2),(1,1)),((0,2),(1,2)),((0,2),(2,1)),((0,2),(2,2)),((1,1),(0,0)),((1,1),(0,1)),((1,1),(0,2)),((1,1),(1,1)),((1,1),(1,2)),((1,1),(2,1)),((1,1),(2,2)),((1,2),(0,0)),((1,2),(0,1)),((1,2),(0,2)),((1,2),(1,1)),((1,2),(1,2)),((1,2),(2,2)),((2,1),(0,0)),((2,1),(0,1)),((2,1),(0,2)),((2,1),(1,1)),((2,1),(2,1)),((2,1),(2,2)),((2,2),(0,0)),((2,2),(0,1)),((2,2),(0,2)),((2,2),(1,1)),((2,2),(1,2)),((2,2),(2,1)),((2,2),(2,2))]
|
||||
, let out = [((0,0),(0,0)),((0,0),(0,1)),((0,0),(0,2)),((0,0),(1,1)),((0,0),(1,2)),((0,0),(2,1)),((0,0),(2,2)),((0,1),(0,0)),((0,1),(0,1)),((0,1),(0,2)),((0,1),(1,1)),((0,1),(1,2)),((0,1),(2,1)),((0,1),(2,2)),((0,2),(0,0)),((0,2),(0,1)),((0,2),(0,2)),((0,2),(1,1)),((0,2),(1,2)),((0,2),(2,1)),((0,2),(2,2)),((1,1),(0,0)),((1,1),(0,1)),((1,1),(0,2)),((1,1),(1,1)),((1,1),(1,2)),((1,1),(2,1)),((1,1),(2,2)),((1,2),(0,0)),((1,2),(0,1)),((1,2),(0,2)),((1,2),(1,1)),((1,2),(1,2)),((1,2),(2,2)),((2,1),(0,0)),((2,1),(0,1)),((2,1),(0,2)),((2,1),(1,1)),((2,1),(2,1)),((2,1),(2,2)),((2,2),(0,0)),((2,2),(0,1)),((2,2),(0,2)),((2,2),(1,1)),((2,2),(1,2)),((2,2),(2,1)),((2,2),(2,2))]
|
||||
in litmusTest "Total order on stores to the same location" intelWP27 out out out
|
||||
|
||||
, litmusTest "intelWP28" intelWP28
|
||||
[((0,0),(0,0)),((0,0),(0,1)),((0,0),(1,0)),((0,0),(1,1)),((0,1),(0,0)),((0,1),(0,1)),((0,1),(1,0)),((0,1),(1,1)),((1,0),(0,0)),((1,0),(0,1)),((1,0),(1,1)),((1,1),(0,0)),((1,1),(0,1)),((1,1),(1,0)),((1,1),(1,1))]
|
||||
[((0,0),(0,0)),((0,0),(0,1)),((0,0),(1,0)),((0,0),(1,1)),((0,1),(0,0)),((0,1),(0,1)),((0,1),(1,0)),((0,1),(1,1)),((1,0),(0,0)),((1,0),(0,1)),((1,0),(1,1)),((1,1),(0,0)),((1,1),(0,1)),((1,1),(1,0)),((1,1),(1,1))]
|
||||
[((0,0),(0,0)),((0,0),(0,1)),((0,0),(1,0)),((0,0),(1,1)),((0,1),(0,0)),((0,1),(0,1)),((0,1),(1,0)),((0,1),(1,1)),((1,0),(0,0)),((1,0),(0,1)),((1,0),(1,1)),((1,1),(0,0)),((1,1),(0,1)),((1,1),(1,0)),((1,1),(1,1))]
|
||||
, let out = [((a,b),(c,d)) | a <- [0..1], b <- [0..1], c <- [0..1], d <- [0..1], ((a,b),(c,d)) /= ((1,0),(1,0))]
|
||||
in litmusTest "Independent Read Independent Write" intelWP28 out out out
|
||||
]
|
||||
|
||||
litmusTest :: (Eq a, Show a) => String -> (forall t. ConcST t a) -> [a] -> [a] -> [a] -> Test
|
||||
|
||||
@ -14,84 +14,74 @@ import QSemN
|
||||
tests :: [Test]
|
||||
tests =
|
||||
[ testGroup "Threading"
|
||||
[ T "child thread ID" threadId1 $ gives' [True]
|
||||
, T "parent thread ID" threadId2 $ gives' [True]
|
||||
, T "no wait" threadNoWait $ gives' [Nothing, Just ()]
|
||||
[ threadId1
|
||||
, threadId2
|
||||
, threadNoWait
|
||||
]
|
||||
, testGroup "MVar"
|
||||
[ T "deadlock" cvarLock $ gives [Left Deadlock, Right 0]
|
||||
, T "race" cvarRace $ gives' [0,1]
|
||||
[ mvarLock
|
||||
, mvarRace
|
||||
]
|
||||
, testGroup "CRef"
|
||||
[ T "race" crefRace $ gives' [0,1]
|
||||
, T "cas modify" crefCASModify $ gives' [0,1]
|
||||
, T "cas race" crefCASRace $ gives' [(True, 2), (False, 2)]
|
||||
, T "cas race (redo)" crefCASRaceRedo $ gives' [(True, 1), (True, 2)]
|
||||
, T "cas tickets" crefCASTickets $ gives' [(True, False, 1), (False, True, 2)]
|
||||
[ crefRace
|
||||
, crefCASModify
|
||||
, crefCASRace
|
||||
, crefCASRaceRedo
|
||||
, crefCASTickets
|
||||
]
|
||||
, testGroup "STM"
|
||||
[ T "atomicity" stmAtomic $ gives' [0,2]
|
||||
, T "left retry" stmLeftRetry $ gives' [()]
|
||||
, T "right retry" stmRightRetry $ gives' [()]
|
||||
, T "issue 55" stmIssue55 $ gives' [True]
|
||||
, T "issue 111" stmIssue111 $ gives' [1]
|
||||
[ stmAtomic
|
||||
, stmLeftRetry
|
||||
, stmRightRetry
|
||||
, stmIssue55
|
||||
, stmIssue111
|
||||
]
|
||||
, testGroup "Killing Threads"
|
||||
[ T "no masking" threadKill $ gives [Left Deadlock, Right ()]
|
||||
, T "masked" threadKillMask $ gives' [()]
|
||||
, T "masked (uninterruptible)" threadKillUninterruptibleMask $ gives [Left Deadlock]
|
||||
, T "unmasked" threadKillUmask $ gives [Left Deadlock, Right ()]
|
||||
, T "throw to main (uncaught)" threadKillToMain1 $ gives [Left UncaughtException]
|
||||
, T "throw to main (caught)" threadKillToMain2 $ gives' [()]
|
||||
[ threadKill
|
||||
, threadKillMask
|
||||
, threadKillUninterruptibleMask
|
||||
, threadKillUmask
|
||||
, threadKillToMain1
|
||||
, threadKillToMain2
|
||||
]
|
||||
, testGroup "Daemons"
|
||||
[ T "schedule daemon" schedDaemon $ gives' [0,1]
|
||||
[ schedDaemon
|
||||
]
|
||||
, testGroup "Subconcurrency"
|
||||
[ T "deadlock1" scDeadlock1 $ gives' [Left Deadlock, Right ()]
|
||||
, T "deadlock2" scDeadlock2 $ gives' [(Left Deadlock, ()), (Right (), ())]
|
||||
, T "success" scSuccess $ gives' [Right ()]
|
||||
, T "illegal" scIllegal $ gives [Left IllegalSubconcurrency]
|
||||
, T "issue 71" scIssue71 $ gives' [()]
|
||||
, T "issue 81" scIssue81 $ gives' [(Right (),0)]
|
||||
[ scDeadlock1
|
||||
, scDeadlock2
|
||||
, scSuccess
|
||||
, scIllegal
|
||||
, scIssue71
|
||||
, scIssue81
|
||||
]
|
||||
]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Threading
|
||||
|
||||
-- | Fork reports the good @ThreadId@.
|
||||
threadId1 :: MonadConc m => m Bool
|
||||
threadId1 = do
|
||||
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
|
||||
|
||||
-- | A child and parent thread have different @ThreadId@s.
|
||||
threadId2 :: MonadConc m => m Bool
|
||||
threadId2 = do
|
||||
threadId2 :: [Test]
|
||||
threadId2 = djfuT "Different threads have different thread IDs" (gives' [True]) $ do
|
||||
tid <- spawn myThreadId
|
||||
|
||||
(/=) <$> myThreadId <*> readMVar tid
|
||||
|
||||
-- | A parent thread doesn't wait for child threads before
|
||||
-- terminating.
|
||||
threadNoWait :: MonadConc m => m (Maybe ())
|
||||
threadNoWait = do
|
||||
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
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- @MVar@s
|
||||
|
||||
-- | Deadlocks sometimes due to order of acquision of locks.
|
||||
cvarLock :: MonadConc m => m Int
|
||||
cvarLock = do
|
||||
mvarLock :: [Test]
|
||||
mvarLock = djfuT "Racey MVar computations may deadlock" (gives [Left Deadlock, Right 0]) $ do
|
||||
a <- newEmptyMVar
|
||||
b <- newEmptyMVar
|
||||
|
||||
@ -108,22 +98,18 @@ cvarLock = do
|
||||
|
||||
takeMVar c
|
||||
|
||||
-- | When racing two @putMVar@s, one of them will win.
|
||||
cvarRace :: MonadConc m => m Int
|
||||
cvarRace = do
|
||||
mvarRace :: [Test]
|
||||
mvarRace = djfuT "Racey MVar computations are nondeterministic" (gives' [0,1]) $ do
|
||||
x <- newEmptyMVar
|
||||
|
||||
void . fork $ putMVar x 0
|
||||
void . fork $ putMVar x 1
|
||||
|
||||
_ <- fork $ putMVar x 0
|
||||
_ <- fork $ putMVar x 1
|
||||
readMVar x
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- @CRef@s
|
||||
|
||||
-- | When racing two @writeCRef@s, one of them will win.
|
||||
crefRace :: MonadConc m => m Int
|
||||
crefRace = do
|
||||
crefRace :: [Test]
|
||||
crefRace = djfuT "Racey CRef computations are nondeterministic" (gives' [0,1]) $ do
|
||||
x <- newCRef (0::Int)
|
||||
|
||||
j1 <- spawn $ writeCRef x 0
|
||||
@ -134,16 +120,14 @@ crefRace = do
|
||||
|
||||
readCRef x
|
||||
|
||||
-- | Modify CAS works.
|
||||
crefCASModify :: MonadConc m => m Int
|
||||
crefCASModify = do
|
||||
crefCASModify :: [Test]
|
||||
crefCASModify = djfuT "CASing CRef changes its value" (gives' [0,1]) $ do
|
||||
x <- newCRef (0::Int)
|
||||
fork $ modifyCRefCAS x (\_ -> (1, ()))
|
||||
readCRef x
|
||||
|
||||
-- | CAS with two threads is racey.
|
||||
crefCASRace :: MonadConc m => m (Bool, Int)
|
||||
crefCASRace = do
|
||||
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
|
||||
@ -152,9 +136,8 @@ crefCASRace = do
|
||||
v <- readCRef x
|
||||
pure (b, v)
|
||||
|
||||
-- | Failed CAS can use the new ticket to succeed.
|
||||
crefCASRaceRedo :: MonadConc m => m (Bool, Int)
|
||||
crefCASRaceRedo = do
|
||||
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
|
||||
@ -168,9 +151,8 @@ crefCASRaceRedo = do
|
||||
v <- readCRef x
|
||||
pure (b, v)
|
||||
|
||||
-- | A ticket is only good for one CAS.
|
||||
crefCASTickets :: MonadConc m => m (Bool, Bool, Int)
|
||||
crefCASTickets = do
|
||||
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
|
||||
@ -183,41 +165,36 @@ crefCASTickets = do
|
||||
--------------------------------------------------------------------------------
|
||||
-- STM
|
||||
|
||||
-- | Transactions are atomic.
|
||||
stmAtomic :: MonadConc m => m Int
|
||||
stmAtomic = do
|
||||
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
|
||||
|
||||
-- | 'retry' is the left identity of 'orElse'.
|
||||
stmLeftRetry :: MonadConc m => m ()
|
||||
stmLeftRetry = do
|
||||
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
|
||||
|
||||
-- | 'retry' is the right identity of 'orElse'.
|
||||
stmRightRetry :: MonadConc m => m ()
|
||||
stmRightRetry = do
|
||||
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
|
||||
|
||||
-- | Test case from issue #55.
|
||||
stmIssue55 :: MonadConc m => m Bool
|
||||
stmIssue55 = do
|
||||
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
|
||||
|
||||
-- | Test case from issue #111
|
||||
stmIssue111 :: MonadConc m => m Int
|
||||
stmIssue111 = do
|
||||
stmIssue111 :: [Test]
|
||||
stmIssue111 = djfuT "https://github.com/barrucadu/dejafu/issues/111" (gives' [1]) $ do
|
||||
v <- atomically $ newTVar 1
|
||||
fork . atomically $ do
|
||||
writeTVar v 2
|
||||
@ -228,17 +205,15 @@ stmIssue111 = do
|
||||
--------------------------------------------------------------------------------
|
||||
-- Exceptions
|
||||
|
||||
-- | Cause a deadlock sometimes by killing a thread.
|
||||
threadKill :: MonadConc m => m ()
|
||||
threadKill = do
|
||||
threadKill :: [Test]
|
||||
threadKill = djfuT "Exceptions can kill unmasked threads" (gives [Left Deadlock, Right ()]) $ do
|
||||
x <- newEmptyMVar
|
||||
tid <- fork $ putMVar x ()
|
||||
killThread tid
|
||||
readMVar x
|
||||
|
||||
-- | Never deadlock by masking a thread.
|
||||
threadKillMask :: MonadConc m => m ()
|
||||
threadKillMask = do
|
||||
threadKillMask :: [Test]
|
||||
threadKillMask = djfuT "Exceptions cannot kill nonblocking masked threads" (gives' [()]) $ do
|
||||
x <- newEmptyMVar
|
||||
y <- newEmptyMVar
|
||||
tid <- fork $ mask $ \_ -> putMVar x () >> putMVar y ()
|
||||
@ -246,19 +221,16 @@ threadKillMask = do
|
||||
killThread tid
|
||||
readMVar y
|
||||
|
||||
-- | Deadlock trying to throw an exception to an
|
||||
-- uninterruptibly-masked thread.
|
||||
threadKillUninterruptibleMask :: MonadConc m => m ()
|
||||
threadKillUninterruptibleMask = do
|
||||
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
|
||||
|
||||
-- | Sometimes deadlock by killing a thread.
|
||||
threadKillUmask :: MonadConc m => m ()
|
||||
threadKillUmask = do
|
||||
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 ())
|
||||
@ -266,18 +238,14 @@ threadKillUmask = do
|
||||
killThread tid
|
||||
readMVar y
|
||||
|
||||
-- | Throw an exception to the main thread with 'throwTo', without a
|
||||
-- handler.
|
||||
threadKillToMain1 :: MonadConc m => m ()
|
||||
threadKillToMain1 = do
|
||||
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
|
||||
|
||||
-- | Throw an exception to the main thread with 'throwTo', with a
|
||||
-- handler.
|
||||
threadKillToMain2 :: MonadConc m => m ()
|
||||
threadKillToMain2 = do
|
||||
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 ())
|
||||
@ -285,11 +253,8 @@ threadKillToMain2 = do
|
||||
-------------------------------------------------------------------------------
|
||||
-- Daemon threads
|
||||
|
||||
-- | Fork off a thread where the first action has no dependency with
|
||||
-- anything the initial thread does, but which has a later action
|
||||
-- which does. This exhibits issue #40.
|
||||
schedDaemon :: MonadConc m => m Int
|
||||
schedDaemon = do
|
||||
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
|
||||
@ -297,52 +262,44 @@ schedDaemon = do
|
||||
--------------------------------------------------------------------------------
|
||||
-- Subconcurrency
|
||||
|
||||
-- | Subcomputation deadlocks sometimes.
|
||||
scDeadlock1 :: Monad n => ConcT r n (Either Failure ())
|
||||
scDeadlock1 = do
|
||||
scDeadlock1 :: [Test]
|
||||
scDeadlock1 = djfuT "Failure is observable" (gives' [Left Deadlock, Right ()]) $ do
|
||||
var <- newEmptyMVar
|
||||
subconcurrency $ do
|
||||
void . fork $ putMVar var ()
|
||||
putMVar var ()
|
||||
|
||||
-- | Subcomputation deadlocks sometimes, and action after it still
|
||||
-- happens.
|
||||
scDeadlock2 :: Monad n => ConcT r n (Either Failure (), ())
|
||||
scDeadlock2 = do
|
||||
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
|
||||
|
||||
-- | Subcomputation successfully completes.
|
||||
scSuccess :: Monad n => ConcT r n (Either Failure ())
|
||||
scSuccess = do
|
||||
scSuccess :: [Test]
|
||||
scSuccess = djfuT "Success is observable" (gives' [Right ()]) $ do
|
||||
var <- newMVar ()
|
||||
subconcurrency $ do
|
||||
out <- newEmptyMVar
|
||||
void . fork $ takeMVar var >>= putMVar out
|
||||
takeMVar out
|
||||
|
||||
-- | Illegal usage
|
||||
scIllegal :: Monad n => ConcT r n ()
|
||||
scIllegal = do
|
||||
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 ()
|
||||
|
||||
-- | Test case from issue 71. This won't fail if the bug is
|
||||
-- reintroduced, it will just hang.
|
||||
scIssue71 :: Monad n => ConcT r n ()
|
||||
scIssue71 = do
|
||||
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 ()
|
||||
|
||||
-- | Test case from issue 81.
|
||||
scIssue81 :: Monad n => ConcT r n (Either Failure (), Int)
|
||||
scIssue81 = do
|
||||
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)
|
||||
|
||||
@ -3,12 +3,10 @@
|
||||
module Cases.SingleThreaded where
|
||||
|
||||
import Control.Exception (ArithException(..), ArrayException(..))
|
||||
import Data.Maybe (isNothing)
|
||||
import Test.DejaFu (Failure(..), gives, gives')
|
||||
import Test.HUnit.DejaFu (testDejafu)
|
||||
|
||||
import Control.Concurrent.Classy
|
||||
import Test.DejaFu.Conc (ConcT, subconcurrency)
|
||||
import Test.DejaFu.Conc (subconcurrency)
|
||||
|
||||
import Common
|
||||
|
||||
@ -19,348 +17,308 @@ import Control.Applicative ((<$>), (<*>))
|
||||
tests :: [Test]
|
||||
tests =
|
||||
[ testGroup "MVar"
|
||||
[ testDejafu emptyMVarTake "empty take" $ gives [Left Deadlock]
|
||||
, testDejafu emptyMVarTryTake "empty take (try)" $ gives' [True]
|
||||
, testDejafu emptyMVarPut "empty put" $ gives' [True]
|
||||
, testDejafu emptyMVarTryPut "empty put (try)" $ gives' [True]
|
||||
, testDejafu emptyMVarRead "empty read" $ gives [Left Deadlock]
|
||||
, testDejafu emptyMVarTryRead "empty read (try)" $ gives' [True]
|
||||
, testDejafu fullMVarPut "full put" $ gives [Left Deadlock]
|
||||
, testDejafu fullMVarTryPut "full put (try)" $ gives' [True]
|
||||
, testDejafu fullMVarTake "full take" $ gives' [True]
|
||||
, testDejafu fullMVarTryTake "full take (try)" $ gives' [True]
|
||||
, testDejafu fullMVarRead "full read" $ gives' [True]
|
||||
, testDejafu fullMVarTryRead "full read (try)" $ gives' [True]
|
||||
[ emptyMVarPut
|
||||
, emptyMVarTryPut
|
||||
, emptyMVarTake
|
||||
, emptyMVarTryTake
|
||||
, emptyMVarRead
|
||||
, emptyMVarTryRead
|
||||
, fullMVarPut
|
||||
, fullMVarTryPut
|
||||
, fullMVarTake
|
||||
, fullMVarTryTake
|
||||
, fullMVarRead
|
||||
, fullMVarTryRead
|
||||
]
|
||||
|
||||
, testGroup "CRef"
|
||||
[ testDejafu crefRead "read" $ gives' [True]
|
||||
, testDejafu crefWrite "write" $ gives' [True]
|
||||
, testDejafu crefModify "modify" $ gives' [True]
|
||||
, testDejafu crefTicketPeek "ticket peek" $ gives' [True]
|
||||
, testDejafu crefTicketPeek2 "ticket peek (2)" $ gives' [True]
|
||||
, testDejafu crefCas1 "cas" $ gives' [(True, True)]
|
||||
, testDejafu crefCas2 "cas (modified)" $ gives' [(False, False)]
|
||||
[ crefRead
|
||||
, crefWrite
|
||||
, crefModify
|
||||
, crefTicketPeek
|
||||
, crefTicketPeek2
|
||||
, crefCas1
|
||||
, crefCas2
|
||||
]
|
||||
|
||||
, testGroup "STM"
|
||||
[ testDejafu stmWrite "write" $ gives' [True]
|
||||
, testDejafu stmPreserve "write (across transactions)" $ gives' [True]
|
||||
, testDejafu stmRetry "retry" $ gives [Left STMDeadlock]
|
||||
, testDejafu stmOrElse "or else" $ gives' [True]
|
||||
, testDejafu stmCatch1 "single catch" $ gives' [True]
|
||||
, testDejafu stmCatch2 "nested catch" $ gives' [True]
|
||||
[ stmWrite
|
||||
, stmPreserve
|
||||
, stmRetry
|
||||
, stmOrElse
|
||||
, stmCatch1
|
||||
, stmCatch2
|
||||
, stmMFail
|
||||
]
|
||||
|
||||
, testGroup "Exceptions"
|
||||
[ testDejafu excCatch "single catch" $ gives' [True]
|
||||
, testDejafu excNest "nested catch" $ gives' [True]
|
||||
, testDejafu excEscape "uncaught" $ gives [Left UncaughtException]
|
||||
, testDejafu excCatchAll "catch all" $ gives' [(True, True)]
|
||||
, testDejafu excSTM "from stm" $ gives' [True]
|
||||
, testDejafu excToMain1 "throw to main (uncaught)" $ gives [Left UncaughtException]
|
||||
, testDejafu excToMain2 "throw to main (caught)" $ gives' [()]
|
||||
, testDejafu excMFail "monadfail" $ gives [Left UncaughtException]
|
||||
, testDejafu excMFailSTM "monadfail (stm)" $ gives [Left UncaughtException]
|
||||
[ excCatch
|
||||
, excNest
|
||||
, excEscape
|
||||
, excCatchAll
|
||||
, excSTM
|
||||
, excToMain1
|
||||
, excToMain2
|
||||
, excMFail
|
||||
]
|
||||
|
||||
, testGroup "Capabilities"
|
||||
[ testDejafu capsGet "get" $ gives' [True]
|
||||
, testDejafu capsSet "set" $ gives' [True]
|
||||
[ capsGet
|
||||
, capsSet
|
||||
]
|
||||
|
||||
, testGroup "Subconcurrency"
|
||||
[ testDejafu scDeadlock1 "deadlock1" $ gives' [Left Deadlock]
|
||||
, testDejafu scDeadlock2 "deadlock2" $ gives' [(Left Deadlock, ())]
|
||||
, testDejafu scSuccess "success" $ gives' [Right ()]
|
||||
[ scDeadlock1
|
||||
, scDeadlock2
|
||||
, scSuccess
|
||||
]
|
||||
]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- @MVar@s
|
||||
|
||||
-- | An empty @MVar@ cannot be taken from.
|
||||
emptyMVarTake :: MonadConc m => m ()
|
||||
emptyMVarTake = do
|
||||
var <- newEmptyMVar
|
||||
emptyMVarTake :: Test
|
||||
emptyMVarTake = djfu "Taking from an empty MVar blocks" (gives [Left Deadlock]) $ do
|
||||
var <- newEmptyMVarInt
|
||||
takeMVar var
|
||||
|
||||
-- | An empty @MVar@ cannot be taken from.
|
||||
emptyMVarTryTake :: MonadConc m => m Bool
|
||||
emptyMVarTryTake = do
|
||||
var <- newEmptyMVar
|
||||
res <- tryTakeMVar var
|
||||
emptyMVarTryTake :: Test
|
||||
emptyMVarTryTake = djfu "Non-blockingly taking from an empty MVar gives nothing" (gives' [Nothing]) $ do
|
||||
var <- newEmptyMVarInt
|
||||
tryTakeMVar var
|
||||
|
||||
return $ (res :: Maybe ()) == Nothing
|
||||
|
||||
-- | An empty @MVar@ can be put into.
|
||||
emptyMVarPut :: MonadConc m => m Bool
|
||||
emptyMVarPut = do
|
||||
var <- newEmptyMVar
|
||||
emptyMVarPut :: Test
|
||||
emptyMVarPut = djfu "Putting into an empty MVar updates it" (gives' [True]) $ do
|
||||
var <- newEmptyMVarInt
|
||||
putMVar var 7
|
||||
(==7) <$> readMVar var
|
||||
|
||||
-- | An empty @MVar@ can be put into.
|
||||
emptyMVarTryPut :: MonadConc m => m Bool
|
||||
emptyMVarTryPut = do
|
||||
var <- newEmptyMVar
|
||||
tryPutMVar var 7
|
||||
emptyMVarTryPut :: Test
|
||||
emptyMVarTryPut = djfu "Non-blockingly putting into an empty MVar updates it" (gives' [True]) $ do
|
||||
var <- newEmptyMVarInt
|
||||
_ <- tryPutMVar var 7
|
||||
(==7) <$> readMVar var
|
||||
|
||||
-- | An empty @MVar@ cannot be read from.
|
||||
emptyMVarRead :: MonadConc m => m ()
|
||||
emptyMVarRead = do
|
||||
var <- newEmptyMVar
|
||||
emptyMVarRead :: Test
|
||||
emptyMVarRead = djfu "Reading an empty MVar blocks" (gives [Left Deadlock]) $ do
|
||||
var <- newEmptyMVarInt
|
||||
readMVar var
|
||||
|
||||
-- | An empty @MVar@ cannot be read from.
|
||||
emptyMVarTryRead :: MonadConc m => m Bool
|
||||
emptyMVarTryRead = do
|
||||
var <- newEmptyMVar
|
||||
isNothing <$> tryReadMVar var
|
||||
emptyMVarTryRead :: Test
|
||||
emptyMVarTryRead = djfu "Non-blockingly reading an empty MVar gives nothing" (gives' [Nothing]) $ do
|
||||
var <- newEmptyMVarInt
|
||||
tryReadMVar var
|
||||
|
||||
-- | A full @MVar@ cannot be put into.
|
||||
fullMVarPut :: MonadConc m => m ()
|
||||
fullMVarPut = do
|
||||
var <- newMVar ()
|
||||
putMVar var ()
|
||||
fullMVarPut :: Test
|
||||
fullMVarPut = djfu "Putting into a full MVar blocks" (gives [Left Deadlock]) $ do
|
||||
var <- newMVarInt 7
|
||||
putMVar var 10
|
||||
|
||||
-- | A full @MVar@ cannot be put into.
|
||||
fullMVarTryPut :: MonadConc m => m Bool
|
||||
fullMVarTryPut = do
|
||||
var <- newMVar ()
|
||||
not <$> tryPutMVar var ()
|
||||
fullMVarTryPut :: Test
|
||||
fullMVarTryPut = djfu "Non-blockingly putting into a full MVar fails" (gives' [False]) $ do
|
||||
var <- newMVarInt 7
|
||||
tryPutMVar var 10
|
||||
|
||||
-- | A full @MVar@ can be taken from.
|
||||
fullMVarTake :: MonadConc m => m Bool
|
||||
fullMVarTake = do
|
||||
var <- newMVar ()
|
||||
(() ==) <$> takeMVar var
|
||||
fullMVarTake :: Test
|
||||
fullMVarTake = djfu "Taking from a full MVar works" (gives' [True]) $ do
|
||||
var <- newMVarInt 7
|
||||
(==7) <$> takeMVar var
|
||||
|
||||
-- | A full @MVar@ can be taken from.
|
||||
fullMVarTryTake :: MonadConc m => m Bool
|
||||
fullMVarTryTake = do
|
||||
var <- newMVar ()
|
||||
(Just () ==) <$> tryTakeMVar var
|
||||
fullMVarTryTake :: Test
|
||||
fullMVarTryTake = djfu "Non-blockingly taking from a full MVar works" (gives' [True]) $ do
|
||||
var <- newMVarInt 7
|
||||
(==Just 7) <$> tryTakeMVar var
|
||||
|
||||
-- | A full @MVar@ can be read from.
|
||||
fullMVarRead :: MonadConc m => m Bool
|
||||
fullMVarRead = do
|
||||
var <- newMVar ()
|
||||
(() ==) <$> readMVar var
|
||||
fullMVarRead :: Test
|
||||
fullMVarRead = djfu "Reading a full MVar works" (gives' [True]) $ do
|
||||
var <- newMVarInt 7
|
||||
(==7) <$> readMVar var
|
||||
|
||||
-- | A full @MVar@ can be read from.
|
||||
fullMVarTryRead :: MonadConc m => m Bool
|
||||
fullMVarTryRead = do
|
||||
var <- newMVar ()
|
||||
(Just () ==) <$> tryReadMVar var
|
||||
fullMVarTryRead :: Test
|
||||
fullMVarTryRead = djfu "Non-blockingly reading a full MVar works" (gives' [True]) $ do
|
||||
var <- newMVarInt 7
|
||||
(==Just 7) <$> tryReadMVar var
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- @CRef@s
|
||||
|
||||
-- | A @CRef@ can be read from.
|
||||
crefRead :: MonadConc m => m Bool
|
||||
crefRead = do
|
||||
ref <- newCRef (5::Int)
|
||||
crefRead :: Test
|
||||
crefRead = djfu "Reading a non-updated CRef gives its initial value" (gives' [True]) $ do
|
||||
ref <- newCRefInt 5
|
||||
(5==) <$> readCRef ref
|
||||
|
||||
-- | A @CRef@ can be written to.
|
||||
crefWrite :: MonadConc m => m Bool
|
||||
crefWrite = do
|
||||
ref <- newCRef (5::Int)
|
||||
crefWrite :: Test
|
||||
crefWrite = djfu "Reading an updated CRef gives its new value" (gives' [True]) $ do
|
||||
ref <- newCRefInt 5
|
||||
writeCRef ref 6
|
||||
(6==) <$> readCRef ref
|
||||
|
||||
-- | A @CRef@ can be modified.
|
||||
crefModify :: MonadConc m => m Bool
|
||||
crefModify = do
|
||||
ref <- newCRef (5::Int)
|
||||
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
|
||||
|
||||
-- | A @Ticket@ contains the value as of when it was created.
|
||||
crefTicketPeek :: MonadConc m => m Bool
|
||||
crefTicketPeek = do
|
||||
ref <- newCRef (5::Int)
|
||||
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
|
||||
|
||||
-- | A @Ticket@ contains the value as of when it was created (and
|
||||
-- casCRef returns a correct new ticket).
|
||||
crefTicketPeek2 :: MonadConc m => m Bool
|
||||
crefTicketPeek2 = do
|
||||
ref <- newCRef (5::Int)
|
||||
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'
|
||||
|
||||
-- | A compare-and-swap can be done on a @CRef@ which hasn't been
|
||||
-- modified.
|
||||
crefCas1 :: MonadConc m => m (Bool, Bool)
|
||||
crefCas1 = do
|
||||
ref <- newCRef (5::Int)
|
||||
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)
|
||||
return (suc && (6 == val))
|
||||
|
||||
-- | A compare-and-swap cannot be done on a @CRef@ which has been
|
||||
-- modified.
|
||||
crefCas2 :: MonadConc m => m (Bool, Bool)
|
||||
crefCas2 = do
|
||||
ref <- newCRef (5::Int)
|
||||
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 (suc, 7 == val)
|
||||
return (not suc && not (7 == val))
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- STM
|
||||
|
||||
-- | A @TVar@ can be written to.
|
||||
stmWrite :: MonadConc m => m Bool
|
||||
stmWrite =
|
||||
(6==) <$> atomically (do { v <- newTVar (5::Int); writeTVar v 6; readTVar v })
|
||||
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 })
|
||||
|
||||
-- | A @TVar@ preserves its value between transactions.
|
||||
stmPreserve :: MonadConc m => m Bool
|
||||
stmPreserve = do
|
||||
ctv <- atomically $ newTVar (5::Int)
|
||||
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)
|
||||
|
||||
-- | A transaction can be aborted, which blocks the thread.
|
||||
stmRetry :: MonadConc m => m ()
|
||||
stmRetry = atomically retry
|
||||
stmRetry :: Test
|
||||
stmRetry = djfu "Aborting a transaction blocks the thread" (gives [Left STMDeadlock]) $
|
||||
(atomically retry :: MonadConc m => m ()) -- avoid an ambiguous type
|
||||
|
||||
-- | An abort can be caught by an @orElse@.
|
||||
stmOrElse :: MonadConc m => m Bool
|
||||
stmOrElse = do
|
||||
ctv <- atomically $ newTVar (5::Int)
|
||||
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)
|
||||
|
||||
-- | An exception can be caught by an appropriate handler.
|
||||
stmCatch1 :: MonadConc m => m Bool
|
||||
stmCatch1 = do
|
||||
ctv <- atomically $ newTVar (5::Int)
|
||||
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)
|
||||
|
||||
-- | Nested exception handlers can catch different types of exception.
|
||||
stmCatch2 :: MonadConc m => m Bool
|
||||
stmCatch2 = do
|
||||
ctv <- atomically $ newTVar (5::Int)
|
||||
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)
|
||||
|
||||
stmMFail :: Test
|
||||
stmMFail = djfu "MonadSTM is a MonadFail" (gives [Left UncaughtException]) $
|
||||
(atomically $ fail "hello world" :: MonadConc m => m ())
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Exceptions
|
||||
|
||||
-- | An exception can be caught by an appropriate handler.
|
||||
excCatch :: MonadConc m => m Bool
|
||||
excCatch = catchArithException
|
||||
(throw Overflow)
|
||||
(\_ -> return True)
|
||||
|
||||
-- | Nested exception handlers can catch different types of exception.
|
||||
excNest :: MonadConc m => m Bool
|
||||
excNest = catchArithException
|
||||
(catchArrayException
|
||||
excCatch :: Test
|
||||
excCatch = djfu "An exception thrown can be caught" (gives' [True]) $
|
||||
catchArithException
|
||||
(throw Overflow)
|
||||
(\_ -> return False))
|
||||
(\_ -> return True)
|
||||
(\_ -> return True)
|
||||
|
||||
-- | Exceptions of the wrong type kill the computation
|
||||
excEscape :: MonadConc m => m ()
|
||||
excEscape = catchArithException
|
||||
(throw $ IndexOutOfBounds "")
|
||||
(\_ -> return undefined)
|
||||
excNest :: Test
|
||||
excNest = djfu "Nested exception handlers work" (gives' [True]) $
|
||||
catchArithException
|
||||
(catchArrayException
|
||||
(throw Overflow)
|
||||
(\_ -> return False))
|
||||
(\_ -> return True)
|
||||
|
||||
-- | @SomeException@ matches all exception types.
|
||||
excCatchAll :: MonadConc m => m (Bool, Bool)
|
||||
excCatchAll = do
|
||||
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 "")
|
||||
(\_ -> return True)
|
||||
return (a && b)
|
||||
|
||||
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)
|
||||
|
||||
-- | Exceptions thrown from STM can be caught.
|
||||
excSTM :: MonadConc m => m Bool
|
||||
excSTM = catchArithException
|
||||
(atomically $ throwSTM Overflow)
|
||||
(\_ -> return True)
|
||||
|
||||
-- | Throw an exception to the main thread with 'throwTo', without a
|
||||
-- handler.
|
||||
excToMain1 :: MonadConc m => m ()
|
||||
excToMain1 = do
|
||||
excToMain1 :: Test
|
||||
excToMain1 = djfu "Throwing an unhandled exception to the main thread kills it" (gives [Left UncaughtException]) $ do
|
||||
tid <- myThreadId
|
||||
throwTo tid Overflow
|
||||
|
||||
-- | Throw an exception to the main thread with 'throwTo', with a
|
||||
-- handler.
|
||||
excToMain2 :: MonadConc m => m ()
|
||||
excToMain2 = do
|
||||
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 ())
|
||||
catchArithException (throwTo tid Overflow >> pure False) (\_ -> pure True)
|
||||
|
||||
-- | Throw an exception using 'fail'. Using 'ConcT' directly to avoid
|
||||
-- a 'MonadFail' constraint, which won't work with base < 4.9.
|
||||
excMFail :: Monad n => ConcT r n (Either Failure ())
|
||||
excMFail = fail "hello world"
|
||||
|
||||
-- | Throw an exception in an STM transaction using 'fail'.
|
||||
excMFailSTM :: Monad n => ConcT r n (Either Failure ())
|
||||
excMFailSTM = atomically $ fail "hello world"
|
||||
excMFail :: Test
|
||||
excMFail = djfu "MonadConc is a MonadFail" (gives [Left UncaughtException]) $
|
||||
(fail "hello world" :: MonadConc m => m ())
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Capabilities
|
||||
|
||||
-- | Check that the capabilities are consistent when retrieved.
|
||||
capsGet :: MonadConc m => m Bool
|
||||
capsGet = (==) <$> getNumCapabilities <*> getNumCapabilities
|
||||
capsGet :: Test
|
||||
capsGet = djfu "Reading the capabilities twice without update gives the same result" (gives' [True]) $ do
|
||||
c1 <- getNumCapabilities
|
||||
c2 <- getNumCapabilities
|
||||
return (c1 == c2)
|
||||
|
||||
-- | Check that the capabilities can be set.
|
||||
capsSet :: MonadConc m => m Bool
|
||||
capsSet = do
|
||||
capsSet :: Test
|
||||
capsSet = djfu "Getting the updated capabilities gives the new value" (gives' [True]) $ do
|
||||
caps <- getNumCapabilities
|
||||
setNumCapabilities $ caps + 1
|
||||
setNumCapabilities (caps + 1)
|
||||
(== caps + 1) <$> getNumCapabilities
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Subconcurrency
|
||||
|
||||
-- | Subcomputation deadlocks.
|
||||
scDeadlock1 :: Monad n => ConcT r n (Either Failure ())
|
||||
scDeadlock1 = subconcurrency (newEmptyMVar >>= readMVar)
|
||||
scDeadlock1 :: Test
|
||||
scDeadlock1 = djfu "Failures in subconcurrency can be observed" (gives' [True]) $ do
|
||||
x <- subconcurrency (newEmptyMVar >>= readMVar)
|
||||
pure (either (==Deadlock) (const False) x)
|
||||
|
||||
-- | Subcomputation deadlocks, and action after it still happens.
|
||||
scDeadlock2 :: Monad n => ConcT r n (Either Failure (), ())
|
||||
scDeadlock2 = do
|
||||
var <- newMVar ()
|
||||
(,) <$> subconcurrency (putMVar var ()) <*> readMVar var
|
||||
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)
|
||||
|
||||
-- | Subcomputation successfully completes.
|
||||
scSuccess :: Monad n => ConcT r n (Either Failure ())
|
||||
scSuccess = do
|
||||
var <- newMVar ()
|
||||
subconcurrency (takeMVar var)
|
||||
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)
|
||||
|
||||
@ -9,14 +9,15 @@ module Common
|
||||
import Control.Exception (ArithException, ArrayException, SomeException)
|
||||
import Control.Monad (void)
|
||||
import qualified Control.Monad.Catch as C
|
||||
import Control.Monad.Conc.Class (MonadConc, readMVar, spawn)
|
||||
import Control.Monad.Conc.Class
|
||||
import Control.Monad.STM.Class
|
||||
import System.Random (mkStdGen)
|
||||
import Test.DejaFu (Predicate)
|
||||
import Test.DejaFu.Conc (ConcST)
|
||||
import qualified Test.Framework as TF
|
||||
import Test.Framework.Providers.HUnit (hUnitTestToTests)
|
||||
import qualified Test.HUnit as TH
|
||||
import Test.HUnit.DejaFu (Bounds, defaultBounds, defaultMemType, uniformly, randomly, swarmy, systematically, testDejafuWay)
|
||||
import Test.HUnit.DejaFu (Bounds, defaultBounds, defaultMemType, uniformly, randomly, swarmy, systematically, testDejafu, testDejafuWay)
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
-- Tests
|
||||
@ -51,6 +52,12 @@ data T where
|
||||
testGroup :: IsTest t => String -> t -> TF.Test
|
||||
testGroup name = TF.testGroup name . toTestList
|
||||
|
||||
djfu :: Show a => String -> Predicate a -> (forall t. ConcST t a) -> TF.Test
|
||||
djfu name p c = head . toTestList $ testDejafu c name p
|
||||
|
||||
djfuT :: Show a => String -> Predicate a -> (forall t. ConcST t a) -> [TF.Test]
|
||||
djfuT name p c = toTestList $ T name c p
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
-- Exceptions
|
||||
|
||||
@ -71,3 +78,19 @@ a ||| b = do
|
||||
j <- spawn a
|
||||
void b
|
||||
void (readMVar j)
|
||||
|
||||
-- | Create an empty monomorphic @MVar@.
|
||||
newEmptyMVarInt :: MonadConc m => m (MVar m Int)
|
||||
newEmptyMVarInt = newEmptyMVar
|
||||
|
||||
-- | Create a full monomorphic @MVar@.
|
||||
newMVarInt :: MonadConc m => Int -> m (MVar m Int)
|
||||
newMVarInt = newMVar
|
||||
|
||||
-- | Create a monomorphic @CRef@.
|
||||
newCRefInt :: MonadConc m => Int -> m (CRef m Int)
|
||||
newCRefInt = newCRef
|
||||
|
||||
-- | Create a monomorphic @TVar@.
|
||||
newTVarInt :: MonadSTM stm => Int -> stm (TVar stm Int)
|
||||
newTVarInt = newTVar
|
||||
|
||||
Loading…
Reference in New Issue
Block a user