-
|
I found out about Unless I missed something, documentation is somewhat sparse, so I tried to get a small example up-and-running by looking at Haddocks and source-code. However, I'm unable to get it to work. Or maybe I have an incorrect understanding of what the tool is supposed to do... The testcase I wrote is quite simple: it create a I wrote two properties, one in plain If I'm not mistaken, the return value can be Any pointers?
{-# LANGUAGE TypeApplications #-}
module Main where
import Control.Applicative ((<|>))
import Control.Monad.Class.MonadAsync (MonadAsync, Concurrently(..), runConcurrently)
import Control.Monad.Class.MonadSTM.Internal (MonadSTM, atomically, check, newTVarIO, readTVar, writeTVar)
import Control.Monad.Class.MonadTest (MonadTest, exploreRaces)
import Control.Monad.Class.MonadTimer (MonadTimer)
import Test.Hspec (describe, hspec)
import Test.Hspec.QuickCheck (prop)
import Test.QuickCheck (Property, (===), counterexample)
import Test.QuickCheck.Monadic (monadicIO, run, stop)
import Control.Monad.IOSim (exploreSimTrace, traceResult)
main :: IO ()
main = hspec $ do
describe "Testcase" $ do
prop "in IO" propIO
prop "in IOSim" propIOSim
-- Run the testcase using 'real' STM in IO, and check whether the result
-- equals 4 (it could, but definitely shouldn't always).
propIO :: Property
propIO = monadicIO @() $ do
r <- run testCase
-- This is supposed to fail quite regularly
stop (r === 4)
-- Run the testcase using IOSim, and check whether the result equals 4.
-- It sometimes could, but shouldn't for every possible interleaving of
-- thread actions (as witnessd by the IO-based test).
propIOSim :: Property
propIOSim = exploreSimTrace id testCase $ \_ trace ->
case traceResult False trace of
Right result -> result === 4
Left e -> counterexample (show e) False
-- This test case is quite simple: it's based around a TVar whose initial
-- value is 0. Then, 4 threads are spawned: three of them will, atomically,
-- write some value (2, 3 or 4) in the TVar once they read the value 1 from
-- it. These three threads race: once one of them was able to write its value,
-- others will no longer read 1 from the TVar.
--
-- A fourth thread will write 1 into the TVar, and then (in another transaction)
-- wait for the value found in the TVar to be non-1 (at this point, this should
-- be one of 2, 3 or 4). It then returns this value.
testCase :: (MonadAsync m, MonadSTM m, MonadTest m, MonadTimer m) => m Int
testCase = do
v <- newTVarIO (0 :: Int)
runConcurrently $ (,) <$> ( Concurrently (exploreRaces >> writer v 2)
<|> Concurrently (exploreRaces >> writer v 3)
<|> Concurrently (exploreRaces >> writer v 4)
)
*> Concurrently (exploreRaces >> driver v)
where
writer v i = atomically $ do
-- Wait for driver to change value
v' <- readTVar v
check (v' == 1)
-- Write "our" value
writeTVar v i
driver v = do
-- Let (one of) the other threads continue
atomically $ writeTVar v 1
atomically $ do
-- Wait until some other thread wrote some other value
v' <- readTVar v
check (v' /= 1)
return v'
|
Beta Was this translation helpful? Give feedback.
Replies: 1 comment 2 replies
-
|
By default all the threads are not racy, you need to execute The default schedule of |
Beta Was this translation helpful? Give feedback.
-
|
Thanks for geting back! I had read the how-to, but misinterpreted it: I thought (as done in the original code above) I had to call Given this, also changing the property from checking equality to 4 to equality to 2, results in both the Not sure how to interpret the trace and other output, for now. Also it seems not all thread labels are displayed? Will look into that. For reference, changed testCase :: (MonadAsync m, MonadLabelledSTM m, MonadTest m, MonadTimer m) => m Int
testCase = do
flip withAsync wait $ do
exploreRaces
labelThisThread "main"
v <- newTVarIO (0 :: Int)
labelTVarIO v "cell"
runConcurrently $
(,)
<$> ( Concurrently (labelThisThread "writer2" >> writer v 2)
<|> Concurrently (labelThisThread "writer3" >> writer v 3)
<|> Concurrently (labelThisThread "writer4" >> writer v 4)
)
*> Concurrently (labelThisThread "driver" >> driver v) |
Beta Was this translation helpful? Give feedback.
-
|
My hypothesis why other threads are not labelled is because I only have an educated guess why my fix worked: probably the |
Beta Was this translation helpful? Give feedback.
By default all the threads are not racy, you need to execute
exploreRacesin the main thread (all threads forked from a racy thread will take part in the schedule exploration). I think this is explained here.The default schedule of
IOSimPORis a round-robin schedule, I guess the property is just true in that schedule.