diff --git a/io-sim/bench/Main.hs b/io-sim/bench/Main.hs index cd2670be..551083a6 100644 --- a/io-sim/bench/Main.hs +++ b/io-sim/bench/Main.hs @@ -4,7 +4,7 @@ module Main (main) where import Control.Concurrent.Class.MonadSTM -import Control.Monad (replicateM, forever) +import Control.Monad (forever, replicateM) import Control.Monad.Class.MonadAsync import Control.Monad.Class.MonadFork import Control.Monad.Class.MonadSay diff --git a/io-sim/io-sim.cabal b/io-sim/io-sim.cabal index be423b8b..84b69ab3 100644 --- a/io-sim/io-sim.cabal +++ b/io-sim/io-sim.cabal @@ -78,8 +78,9 @@ test-suite test type: exitcode-stdio-1.0 hs-source-dirs: test main-is: Main.hs - other-modules: Test.IOSim - Test.STM + other-modules: Test.Control.Monad.STM + Test.Control.Monad.Utils + Test.Control.Monad.IOSim Test.Control.Monad.IOSimPOR Test.Control.Monad.Class.MonadMVar default-language: Haskell2010 diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index 47a464d6..7da81100 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -1,14 +1,14 @@ -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE CPP #-} -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTSyntax #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTSyntax #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} {-# OPTIONS_GHC -Wno-orphans #-} -- incomplete uni patterns in 'schedule' (when interpreting 'StmTxCommitted') @@ -49,9 +49,7 @@ module Control.Monad.IOSim.Internal import Prelude hiding (read) import Data.Dynamic -import Data.Foldable (toList, traverse_, foldlM) -import Deque.Strict (Deque) -import qualified Deque.Strict as Deque +import Data.Foldable (foldlM, toList, traverse_) import qualified Data.List as List import qualified Data.List.Trace as Trace import Data.Map.Strict (Map) @@ -62,12 +60,14 @@ import qualified Data.OrdPSQ as PSQ import Data.Set (Set) import qualified Data.Set as Set import Data.Time (UTCTime (..), fromGregorian) +import Deque.Strict (Deque) +import qualified Deque.Strict as Deque import GHC.Exts (fromList) import GHC.Conc (ThreadStatus(..), BlockReason(..)) -import Control.Exception - (NonTermination (..), assert, throw, AsyncException (..)) +import Control.Exception (AsyncException (..), NonTermination (..), + assert, throw) import Control.Monad (join, when) import Control.Monad.ST.Lazy import Control.Monad.ST.Lazy.Unsafe (unsafeIOToST, unsafeInterleaveST) diff --git a/io-sim/src/Control/Monad/IOSim/InternalTypes.hs b/io-sim/src/Control/Monad/IOSim/InternalTypes.hs index 554ab2a9..16d7c90e 100644 --- a/io-sim/src/Control/Monad/IOSim/InternalTypes.hs +++ b/io-sim/src/Control/Monad/IOSim/InternalTypes.hs @@ -10,9 +10,9 @@ module Control.Monad.IOSim.InternalTypes , IsLocked (..) ) where -import Data.STRef.Lazy (STRef) import Control.Exception (Exception) import Control.Monad.Class.MonadThrow (MaskingState (..)) +import Data.STRef.Lazy (STRef) import Control.Monad.IOSim.Types (SimA, ThreadId, TimeoutId) diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index 9a214fd2..203b21ba 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -1,15 +1,15 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTSyntax #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE PatternSynonyms #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTSyntax #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} {-# OPTIONS_GHC -Wno-partial-fields #-} diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index 15ca22f8..f97a1cce 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -1,15 +1,15 @@ -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE CPP #-} -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTSyntax #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTSyntax #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} {-# OPTIONS_GHC -Wno-orphans #-} -- incomplete uni patterns in 'schedule' (when interpreting 'StmTxCommitted') @@ -50,7 +50,7 @@ module Control.Monad.IOSimPOR.Internal import Prelude hiding (read) import Data.Dynamic -import Data.Foldable (traverse_, foldlM) +import Data.Foldable (foldlM, traverse_) import qualified Data.List as List import qualified Data.List.Trace as Trace import Data.Map.Strict (Map) @@ -63,9 +63,9 @@ import Data.Set (Set) import qualified Data.Set as Set import Data.Time (UTCTime (..), fromGregorian) -import Control.Exception - (NonTermination (..), assert, throw, AsyncException (..)) -import Control.Monad ( join, when ) +import Control.Exception (AsyncException (..), NonTermination (..), + assert, throw) +import Control.Monad (join, when) import Control.Monad.ST.Lazy import Control.Monad.ST.Lazy.Unsafe (unsafeIOToST, unsafeInterleaveST) import Data.STRef.Lazy diff --git a/io-sim/test/Main.hs b/io-sim/test/Main.hs index 1a54c244..f20def74 100644 --- a/io-sim/test/Main.hs +++ b/io-sim/test/Main.hs @@ -3,7 +3,8 @@ module Main (main) where import Test.Tasty import qualified Test.Control.Monad.Class.MonadMVar (tests) -import qualified Test.IOSim (tests) +import qualified Test.Control.Monad.IOSim (tests) +import qualified Test.Control.Monad.IOSimPOR (tests) main :: IO () main = defaultMain tests @@ -11,6 +12,7 @@ main = defaultMain tests tests :: TestTree tests = testGroup "IO Sim" - [ Test.IOSim.tests - , Test.Control.Monad.Class.MonadMVar.tests + [ Test.Control.Monad.Class.MonadMVar.tests + , Test.Control.Monad.IOSim.tests + , Test.Control.Monad.IOSimPOR.tests ] diff --git a/io-sim/test/Test/IOSim.hs b/io-sim/test/Test/Control/Monad/IOSim.hs similarity index 68% rename from io-sim/test/Test/IOSim.hs rename to io-sim/test/Test/Control/Monad/IOSim.hs index ff204914..109e41c0 100644 --- a/io-sim/test/Test/IOSim.hs +++ b/io-sim/test/Test/Control/Monad/IOSim.hs @@ -3,20 +3,15 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} -module Test.IOSim +module Test.Control.Monad.IOSim ( tests , TestThreadGraph (..) - , arbitraryAcyclicGraph ) where -import Data.Array import Data.Either (isLeft) -import Data.Fixed (Fixed (..), Micro) +import Data.Fixed (Micro) import Data.Foldable (foldl') -import Data.Function (on) import Data.Functor (($>)) -import Data.Graph -import Data.List (sortBy) import Data.Time.Clock (picosecondsToDiffTime) import Control.Exception (ArithException (..)) @@ -33,7 +28,8 @@ import Control.Monad.Class.MonadTime import Control.Monad.Class.MonadTimer import Control.Monad.IOSim -import Test.STM +import Test.Control.Monad.Utils +import Test.Control.Monad.STM import Test.QuickCheck import Test.Tasty @@ -349,142 +345,6 @@ prop_stm_graph_sim g = -- that all other threads finished, but perhaps we should and structure -- the graph tests so that's the case. -prop_stm_graph :: (MonadFork m, MonadSTM m) => TestThreadGraph -> m () -prop_stm_graph (TestThreadGraph g) = do - vars <- listArray (bounds g) <$> - sequence [ newTVarIO False | _ <- vertices g ] - forM_ (vertices g) $ \v -> - void $ forkIO $ do - -- read all the inputs and wait for them to become true - -- then write to all the outputs - let incomming = g' ! v - atomically $ do - sequence_ [ readTVar (vars ! var) >>= check | var <- incomming ] - writeTVar (vars ! v) True - - let -- the vertices with incoming but no outgoing edges - outputs = [ v - | v <- vertices g - , not (null (g' ! v)) - , null (g ! v) ] - - -- Wait for the outputs - atomically $ sequence_ [ readTVar (vars ! var) >>= check | var <- outputs ] - where - g' = transposeG g -- for incoming edges - -newtype TestThreadGraph = TestThreadGraph Graph - deriving Show - -instance Arbitrary TestThreadGraph where - arbitrary = - sized $ \sz -> - TestThreadGraph <$> arbitraryAcyclicGraph - (choose (2, 8 `min` (sz `div` 3))) - (choose (1, 8 `min` (sz `div` 3))) - 0.3 - -arbitraryAcyclicGraph :: Gen Int -> Gen Int -> Float -> Gen Graph -arbitraryAcyclicGraph genNRanks genNPerRank edgeChance = do - nranks <- genNRanks - rankSizes <- replicateM nranks genNPerRank - let rankStarts = scanl (+) 0 rankSizes - rankRanges = drop 1 (zip rankStarts (tail rankStarts)) - totalRange = sum rankSizes - rankEdges <- mapM (uncurry genRank) rankRanges - return $ buildG (0, totalRange-1) (concat rankEdges) - where - genRank :: Vertex -> Vertex -> Gen [Edge] - genRank rankStart rankEnd = - filterM (const (pick edgeChance)) - [ (i,j) - | i <- [0..rankStart-1] - , j <- [rankStart..rankEnd-1] - ] - - pick :: Float -> Gen Bool - pick chance = (< chance) <$> choose (0,1) - - --- --- Timers --- - -newtype TestMicro = TestMicro [Micro] - deriving Show - --- | --- Arbitrary non negative micro numbers with a high probability of --- repetitions. -instance Arbitrary TestMicro where - arbitrary = sized $ \n -> TestMicro <$> genN n [] - where - genN :: Int -> [Micro] -> Gen [Micro] - genN 0 rs = return rs - genN n [] = do - r <- genMicro - genN (n - 1) [r] - genN n rs = do - r <- frequency - [ (2, elements rs) - , (1, genMicro) - ] - genN (n - 1) (r : rs) - - genMicro :: Gen Micro - genMicro = MkFixed <$> arbitrary - - shrink (TestMicro rs) = [ TestMicro rs' | rs' <- shrinkList (const []) rs ] - -test_timers :: forall m. - ( MonadFork m - , MonadSTM m - , MonadTimer m - ) - => [DiffTime] - -> m Property -test_timers xs = - label (lbl xs) . isValid <$> withProbe experiment - where - countUnique :: Eq a => [a] -> Int - countUnique [] = 0 - countUnique (a:as) = - let as' = filter (== a) as - in 1 + countUnique as' - - lbl :: Eq a => [a] -> String - lbl as = - let p = (if null as then 0 else (100 * countUnique as) `div` length as) - `mod` 10 * 10 - in show p ++ "% unique" - - experiment :: Probe m (DiffTime, Int) -> m () - experiment p = do - tvars <- forM (zip xs [0..]) $ \(t, idx) -> do - v <- newTVarIO False - void $ forkIO $ threadDelay t >> do - probeOutput p (t, idx) - atomically $ writeTVar v True - return v - - -- wait for all tvars - forM_ tvars $ \v -> atomically (readTVar v >>= check) - - isValid :: [(DiffTime, Int)] -> Property - isValid tr = - -- all timers should fire - (length tr === length xs) - -- timers should fire in the right order - .&&. (sortBy (on sortFn fst) tr === tr) - - -- timers with negative timeout never fired, so we treat them as they would - -- all fired at once at @-∞@. This is to say that the following function is - -- a well defined partial order. - sortFn :: DiffTime -> DiffTime -> Ordering - sortFn a b | a >= 0 && b >= 0 = a `compare` b - | a < 0 && b < 0 = EQ - | otherwise = a `compare` b - prop_timers_ST :: TestMicro -> Property prop_timers_ST (TestMicro xs) = let ds = map (realToFrac :: Micro -> DiffTime) xs @@ -501,97 +361,18 @@ prop_timers_IO = ioProperty . test_timers -- Forking -- -test_fork_order :: forall m. - ( MonadFork m - , MonadSTM m - , MonadTimer m - ) - => Positive Int - -> m Property -test_fork_order = \(Positive n) -> isValid n <$> withProbe (experiment n) - where - experiment :: Int -> Probe m Int -> m () - experiment 0 _ = return () - experiment n p = do - v <- newTVarIO False - - void $ forkIO $ do - probeOutput p n - atomically $ writeTVar v True - experiment (n - 1) p - - -- wait for the spawned thread to finish - atomically $ readTVar v >>= check - - isValid :: Int -> [Int] -> Property - isValid n tr = tr === [n,n-1..1] - prop_fork_order_ST :: Positive Int -> Property prop_fork_order_ST n = runSimOrThrow $ test_fork_order n prop_fork_order_IO :: Positive Int -> Property prop_fork_order_IO = ioProperty . test_fork_order - -test_threadId_order :: forall m. - ( MonadFork m - , MonadSTM m - , MonadTimer m - ) - => Positive Int - -> m Property -test_threadId_order = \(Positive n) -> do - isValid n <$> (forM [1..n] (const experiment)) - where - experiment :: m (ThreadId m) - experiment = do - v <- newTVarIO False - - tid <- forkIO $ atomically $ writeTVar v True - - -- wait for the spawned thread to finish - atomically $ readTVar v >>= check - return tid - - isValid :: Int -> [ThreadId m] -> Property - isValid n tr = map show tr === map (("ThreadId " ++ ) . show . (:[])) [1..n] - prop_threadId_order_order_Sim :: Positive Int -> Property prop_threadId_order_order_Sim n = runSimOrThrow $ test_threadId_order n - prop_wakeup_order_ST :: Property prop_wakeup_order_ST = runSimOrThrow $ test_wakeup_order --- This property is not actually deterministic in IO. Uncomment the following --- and try it! Arguably therefore, this property does not need to be true for --- the Sim either. Perhaps we should introduce random scheduling and abandon --- this property. In the meantime it's a helpful sanity check. - ---prop_wakeup_order_IO = ioProperty test_wakeup_order - -test_wakeup_order :: ( MonadFork m - , MonadSTM m - , MonadTimer m - ) - => m Property -test_wakeup_order = do - v <- newTVarIO False - wakupOrder <- - withProbe $ \p -> do - sequence_ - [ do _ <- forkIO $ do - atomically $ do - x <- readTVar v - check x - probeOutput p (n :: Int) - threadDelay 0.1 - | n <- [0..9] ] - atomically $ writeTVar v True - threadDelay 0.1 - return (wakupOrder === [0..9]) --FIFO order - - -- -- MonadFix properties -- @@ -762,27 +543,6 @@ prop_mfix_recdata = ioProperty $ do ) atomically (LazySTM.readTVar y) - --- --- Probe mini-abstraction --- - --- | Where returning results directly is not convenient, we can build up --- a trace of events we want to observe, and can do probe output from --- multiple threads. --- -type Probe m x = StrictTVar m [x] - -withProbe :: MonadSTM m => (Probe m x -> m ()) -> m [x] -withProbe action = do - probe <- newTVarIO [] - action probe - reverse <$> atomically (readTVar probe) - -probeOutput :: MonadSTM m => Probe m x -> x -> m () -probeOutput probe x = atomically (modifyTVar probe (x:)) - - -- -- Synchronous exceptions -- @@ -1242,51 +1002,6 @@ prop_stm_referenceSim :: SomeTerm -> Property prop_stm_referenceSim t = runSimOrThrow (prop_stm_referenceM t) ---TODO: would be nice to also have stronger tests here: --- * compare all the tvar values in the heap --- * compare the read and write sets - --- | Compare the behaviour of the STM reference operational semantics with --- the behaviour of any 'MonadSTM' STM implementation. --- -prop_stm_referenceM :: (MonadSTM m, MonadCatch (STM m), MonadCatch m) - => SomeTerm -> m Property -prop_stm_referenceM (SomeTerm _tyrep t) = do - let (r1, _heap) = evalAtomically t - r2 <- execAtomically t - return (r1 === r2) - - --- | Check that 'timeout' does not deadlock when executed with asynchronous --- exceptions uninterruptibly masked. --- -prop_timeout_no_deadlockM :: forall m. - ( MonadFork m - , MonadSTM m - , MonadTimer m - , MonadMask m - ) - => m Bool -prop_timeout_no_deadlockM = do - v <- registerDelay' 0.01 - r <- uninterruptibleMask_ $ timeout 0.02 $ do - atomically $ do - readTVar v >>= check - return True - case r of - Nothing -> return False - Just b -> return b - where - -- Like 'registerDelay', but does not require threaded RTS in the @m ~ IO@ - -- case. - registerDelay' :: DiffTime -> m (StrictTVar m Bool) - registerDelay' delta = do - v <- newTVarIO False - _ <- forkIO $ do - threadDelay delta - atomically (writeTVar v True) - return v - prop_timeout_no_deadlock_Sim :: Bool prop_timeout_no_deadlock_Sim = runSimOrThrow prop_timeout_no_deadlockM @@ -1298,44 +1013,6 @@ prop_timeout_no_deadlock_IO = ioProperty prop_timeout_no_deadlockM -- MonadMask properties -- -setMaskingState_ :: MonadMask m => MaskingState -> m a -> m a -setMaskingState_ Unmasked = id -setMaskingState_ MaskedInterruptible = mask_ -setMaskingState_ MaskedUninterruptible = uninterruptibleMask_ - -setMaskingState :: MonadMask m => MaskingState - -> ((forall x. m x -> m x) -> m a) -> m a -setMaskingState Unmasked = \f -> f id -setMaskingState MaskedInterruptible = mask -setMaskingState MaskedUninterruptible = uninterruptibleMask - -maxMS :: MaskingState -> MaskingState -> MaskingState -maxMS MaskedUninterruptible _ = MaskedUninterruptible -maxMS _ MaskedUninterruptible = MaskedUninterruptible -maxMS MaskedInterruptible _ = MaskedInterruptible -maxMS _ MaskedInterruptible = MaskedInterruptible -maxMS Unmasked Unmasked = Unmasked - - -forall_masking_states :: (MaskingState -> Property) - -> Property -forall_masking_states prop = - -- make sure that the property is executed once! - withMaxSuccess 1 $ - foldr (\ms p -> counterexample (show ms) (prop ms) .&&. p) - (property True) - [Unmasked, MaskedInterruptible, MaskedUninterruptible] - --- | Check that setting masking state is effective. --- -prop_set_masking_state :: MonadMaskingState m - => MaskingState - -> m Property -prop_set_masking_state ms = - setMaskingState_ ms $ do - ms' <- getMaskingState - return (ms === ms') - unit_set_masking_state_IO :: MaskingState -> Property unit_set_masking_state_IO = ioProperty . prop_set_masking_state @@ -1344,39 +1021,12 @@ unit_set_masking_state_ST :: MaskingState -> Property unit_set_masking_state_ST ms = runSimOrThrow (prop_set_masking_state ms) - --- | Check that 'unmask' restores the masking state. --- -prop_unmask :: MonadMaskingState m - => MaskingState - -> MaskingState - -> m Property -prop_unmask ms ms' = - setMaskingState_ ms $ - setMaskingState ms' $ \unmask -> do - ms'' <- unmask getMaskingState - return (ms'' === ms) - unit_unmask_IO :: MaskingState -> MaskingState -> Property unit_unmask_IO ms ms' = ioProperty $ prop_unmask ms ms' unit_unmask_ST :: MaskingState -> MaskingState -> Property unit_unmask_ST ms ms' = runSimOrThrow $ prop_unmask ms ms' - --- | Check that masking state is inherited by a forked thread. --- -prop_fork_masking_state :: ( MonadMaskingState m - , MonadFork m - , MonadSTM m - ) - => MaskingState -> m Property -prop_fork_masking_state ms = setMaskingState_ ms $ do - var <- newEmptyTMVarIO - _ <- forkIO $ getMaskingState >>= atomically . putTMVar var - ms' <- atomically $ takeTMVar var - return $ ms === ms' - unit_fork_masking_state_IO :: MaskingState -> Property unit_fork_masking_state_IO = ioProperty . prop_fork_masking_state @@ -1385,47 +1035,12 @@ unit_fork_masking_state_ST :: MaskingState -> Property unit_fork_masking_state_ST ms = runSimOrThrow (prop_fork_masking_state ms) - --- | Check that 'unmask' restores the masking state in a forked thread. --- --- Note: unlike 'prop_unmask', 'forkIOWithUnmask's 'unmask' function will --- restore 'Unmasked' state, not the encosing masking state. --- -prop_fork_unmask :: ( MonadMaskingState m - , MonadFork m - , MonadSTM m - ) - => MaskingState - -> MaskingState - -> m Property -prop_fork_unmask ms ms' = - setMaskingState_ ms $ - setMaskingState_ ms' $ do - var <- newEmptyTMVarIO - _ <- forkIOWithUnmask $ \unmask -> unmask getMaskingState - >>= atomically . putTMVar var - ms'' <- atomically $ takeTMVar var - return $ Unmasked === ms'' - unit_fork_unmask_IO :: MaskingState -> MaskingState -> Property unit_fork_unmask_IO ms ms' = ioProperty $ prop_fork_unmask ms ms' unit_fork_unmask_ST :: MaskingState -> MaskingState -> Property unit_fork_unmask_ST ms ms' = runSimOrThrow $ prop_fork_unmask ms ms' - --- | A unit test which checks the masking state in the context of a catch --- handler. --- -prop_catch_throwIO_masking_state :: forall m. MonadMaskingState m - => MaskingState -> m Property -prop_catch_throwIO_masking_state ms = - setMaskingState_ ms $ do - throwIO (userError "error") - `catch` \(_ :: IOError) -> do - ms' <- getMaskingState - return $ ms' === MaskedInterruptible `maxMS` ms - unit_catch_throwIO_masking_state_IO :: MaskingState -> Property unit_catch_throwIO_masking_state_IO ms = ioProperty $ prop_catch_throwIO_masking_state ms @@ -1434,22 +1049,6 @@ unit_catch_throwIO_masking_state_ST :: MaskingState -> Property unit_catch_throwIO_masking_state_ST ms = runSimOrThrow (prop_catch_throwIO_masking_state ms) - --- | Like 'prop_catch_masking_state' but using 'throwTo'. --- -prop_catch_throwTo_masking_state :: forall m. - ( MonadMaskingState m - , MonadFork m - ) - => MaskingState -> m Property -prop_catch_throwTo_masking_state ms = - setMaskingState_ ms $ do - tid <- myThreadId - (throwTo tid (userError "error") >> error "impossible") - `catch` \(_ :: IOError) -> do - ms' <- getMaskingState - return $ ms' === MaskedInterruptible `maxMS` ms - unit_catch_throwTo_masking_state_IO :: MaskingState -> Property unit_catch_throwTo_masking_state_IO = ioProperty . prop_catch_throwTo_masking_state @@ -1458,36 +1057,6 @@ unit_catch_throwTo_masking_state_ST :: MaskingState -> Property unit_catch_throwTo_masking_state_ST ms = runSimOrThrow $ prop_catch_throwTo_masking_state ms - --- | Like 'prop_catch_throwTo_masking_state' but using 'throwTo' to a different --- thread which is in a non-blocking mode. --- -prop_catch_throwTo_masking_state_async :: forall m. - ( MonadMaskingState m - , MonadFork m - , MonadSTM m - , MonadDelay m - ) - => MaskingState -> m Property -prop_catch_throwTo_masking_state_async ms = do - sgnl <- newEmptyTMVarIO - var <- newEmptyTMVarIO - tid <- forkIO $ - setMaskingState ms $ \unmask -> - (do atomically $ putTMVar sgnl () - unmask (threadDelay 1) - ) - `catch` \(_ :: IOError) -> do - ms' <- getMaskingState - atomically $ putTMVar var (ms' === ms `maxMS` MaskedInterruptible) - -- wait until the catch handler is installed - atomically $ takeTMVar sgnl - -- the forked thread is interruptibly blocked on `threadDelay`, - -- `throwTo` will not block - throwTo tid (userError "error") - atomically $ takeTMVar var - - unit_catch_throwTo_masking_state_async_IO :: MaskingState -> Property unit_catch_throwTo_masking_state_async_IO = ioProperty . prop_catch_throwTo_masking_state_async @@ -1496,42 +1065,6 @@ unit_catch_throwTo_masking_state_async_ST :: MaskingState -> Property unit_catch_throwTo_masking_state_async_ST ms = runSimOrThrow (prop_catch_throwTo_masking_state_async ms) - --- | Like 'prop_catch_throwTo_masking_state_async' but 'throwTo' will block if --- masking state is set to 'MaskedUninterruptible'. This makes sure that the --- 'willBlock' branch of 'ThrowTo' in 'schedule' is covered. --- -prop_catch_throwTo_masking_state_async_mayblock :: forall m. - ( MonadMaskingState m - , MonadFork m - , MonadSTM m - , MonadDelay m - ) - => MaskingState -> m Property -prop_catch_throwTo_masking_state_async_mayblock ms = do - sgnl <- newEmptyTMVarIO - var <- newEmptyTMVarIO - tid <- forkIO $ - setMaskingState ms $ \unmask -> - (do atomically $ putTMVar sgnl () - -- if 'ms' is 'MaskedUninterruptible' then the following - -- 'threadDelay' will block. - threadDelay 0.1 - -- make sure that even in 'MaskedUninterruptible' the thread - -- unblocks so async exceptions can be delivered. - unmask (threadDelay 1) - ) - `catch` \(_ :: IOError) -> do - ms' <- getMaskingState - atomically $ putTMVar var (ms' === ms `maxMS` MaskedInterruptible) - -- wait until the catch handler is installed - atomically $ takeTMVar sgnl - threadDelay 0.05 - -- we know the forked thread is interruptibly blocked on `threadDelay`, - -- `throwTo` will not be blocked. - throwTo tid (userError "error") - atomically $ takeTMVar var - unit_catch_throwTo_masking_state_async_mayblock_IO :: MaskingState -> Property unit_catch_throwTo_masking_state_async_mayblock_IO = ioProperty . prop_catch_throwTo_masking_state_async_mayblock @@ -1539,15 +1072,3 @@ unit_catch_throwTo_masking_state_async_mayblock_IO = unit_catch_throwTo_masking_state_async_mayblock_ST :: MaskingState -> Property unit_catch_throwTo_masking_state_async_mayblock_ST ms = runSimOrThrow (prop_catch_throwTo_masking_state_async_mayblock ms) - --- --- Utils --- - -runSimTraceSay :: (forall s. IOSim s a) -> [String] -runSimTraceSay action = selectTraceSay (runSimTrace action) - -selectTraceSay :: SimTrace a -> [String] -selectTraceSay (SimTrace _ _ _ (EventSay msg) trace) = msg : selectTraceSay trace -selectTraceSay (SimTrace _ _ _ _ trace) = selectTraceSay trace -selectTraceSay _ = [] diff --git a/io-sim/test/Test/Control/Monad/IOSimPOR.hs b/io-sim/test/Test/Control/Monad/IOSimPOR.hs index fb1272d2..08daab31 100644 --- a/io-sim/test/Test/Control/Monad/IOSimPOR.hs +++ b/io-sim/test/Test/Control/Monad/IOSimPOR.hs @@ -1,33 +1,123 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# OPTIONS_GHC -Wno-unused-top-binds #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} -module Test.Control.Monad.IOSimPOR where +module Test.Control.Monad.IOSimPOR (tests) where -import Control.Concurrent.Class.MonadSTM.TVar +import Data.Fixed (Micro) +import Data.Functor (($>)) +import Data.IORef +import Data.List +import Data.Map (Map) +import qualified Data.Map as Map + +import System.Exit +import System.IO.Error (ioeGetErrorString, isUserError) +import System.IO.Unsafe + +import Control.Exception (ArithException (..)) import Control.Monad +import Control.Monad.Fix +import Control.Parallel + import Control.Monad.Class.MonadFork -import Control.Monad.Class.MonadSTM +import Control.Concurrent.Class.MonadSTM +import Control.Monad.Class.MonadSay import Control.Monad.Class.MonadTest +import Control.Monad.Class.MonadThrow +import Control.Monad.Class.MonadTime import Control.Monad.Class.MonadTimer import Control.Monad.IOSim import GHC.Generics -import System.Exit -import System.IO.Unsafe +import Test.Control.Monad.Utils +import Test.Control.Monad.STM -import Control.Exception (SomeException, evaluate, try) -import Control.Parallel -import Data.IORef -import Data.List -import Data.Map (Map) -import qualified Data.Map as Map import Test.QuickCheck +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.QuickCheck + +tests :: TestTree +tests = + testGroup "IO simulator POR" + [ testProperty "propSimulates" propSimulates + , testProperty "propExploration" propExploration + -- , testProperty "propPermutations" propPermutations + , testGroup "IO simulator properties" + [ testProperty "read/write graph (IOSim)" (withMaxSuccess 1000 prop_stm_graph_sim) + , testProperty "timers (IOSim)" (withMaxSuccess 1000 prop_timers_ST) + , testProperty "timeout (IOSim): no deadlock" + prop_timeout_no_deadlock_Sim + , testProperty "threadId order (IOSim)" (withMaxSuccess 1000 prop_threadId_order_order_Sim) + , testProperty "forkIO order (IOSim)" (withMaxSuccess 1000 prop_fork_order_ST) + , testGroup "throw/catch unit tests" + [ testProperty "0" unit_catch_0 + , testProperty "1" unit_catch_1 + , testProperty "2" unit_catch_2 + , testProperty "3" unit_catch_3 + , testProperty "4" unit_catch_4 + , testProperty "5" unit_catch_5 + , testProperty "6" unit_catch_6 + ] + , testGroup "masking state" + [ testProperty "set (IOSim)" + $ forall_masking_states unit_set_masking_state_ST + + , testProperty "unmask (IOSim)" + $ forall_masking_states $ \ms -> + forall_masking_states $ \ms' -> unit_unmask_ST ms ms' + + , testProperty "fork (IOSim)" + $ forall_masking_states unit_fork_masking_state_ST + + , testProperty "fork unmask (IOSim)" + $ forall_masking_states $ \ms -> + forall_masking_states $ \ms' -> unit_fork_unmask_ST ms ms' + + , testProperty "catch (IOSim)" + $ forall_masking_states unit_catch_throwIO_masking_state_ST + + , testProperty "catch: throwTo (IOSim)" + $ forall_masking_states unit_catch_throwTo_masking_state_ST + + , testProperty "catch: throwTo async (IOSim)" + $ forall_masking_states unit_catch_throwTo_masking_state_async_ST + + , testProperty "catch: throwTo async blocking (IOSim)" + $ forall_masking_states unit_catch_throwTo_masking_state_async_mayblock_ST + ] + , testProperty "evaluate unit test" unit_evaluate_0 + , testGroup "forkIO unit tests" + [ testProperty "1" unit_fork_1 + ] + , testGroup "async exception unit tests" + [ testProperty "1" unit_async_1 + , testProperty "3" unit_async_3 + , testProperty "4" unit_async_4 + , testProperty "5" unit_async_5 + , testProperty "6" unit_async_6 + , testProperty "7" unit_async_7 + , testProperty "8" unit_async_8 + , testProperty "9" unit_async_9 + ] + , testGroup "STM reference semantics" + [ testProperty "Reference vs Sim" prop_stm_referenceSim + ] + , testGroup "MonadFix instance" + [ testProperty "purity" prop_mfix_purity + , testProperty "purity2" prop_mfix_purity_2 + , testProperty "tightening" prop_mfix_left_shrinking + , testProperty "lazy" prop_mfix_lazy + ] + ] + ] data Step = WhenSet Int Int @@ -279,3 +369,531 @@ traceNoDuplicates k = r `pseq` (k addTrace .&&. maximum (traceCounts ()) == 1) atomicModifyIORef r (\m->(Map.insertWith (+) (show t) 1 m,())) return x traceCounts () = unsafePerformIO $ Map.elems <$> readIORef r + +-- +-- IOSim reused properties +-- + + +-- +-- Read/Write graph +-- + +prop_stm_graph_sim :: TestThreadGraph -> Property +prop_stm_graph_sim g = + traceNoDuplicates $ \addTrace -> + exploreSimTrace id (prop_stm_graph g) $ \_ trace -> + addTrace trace $ + counterexample (splitTrace . noExceptions $ show trace) $ + case traceResult False trace of + Right () -> property True + Left e -> counterexample (show e) False + -- TODO: Note that we do not use runSimStrictShutdown here to check + -- that all other threads finished, but perhaps we should and structure + -- the graph tests so that's the case. + +prop_timers_ST :: TestMicro -> Property +prop_timers_ST (TestMicro xs) = + let ds = map (realToFrac :: Micro -> DiffTime) xs + in exploreSimTrace id (test_timers ds) $ \_ trace -> + case traceResult False trace of + Right a -> a + Left e -> counterexample (show e) False + +-- +-- Forking +-- + +prop_fork_order_ST :: Positive Int -> Property +prop_fork_order_ST n = + exploreSimTrace id (test_fork_order n) $ \_ trace -> + case traceResult False trace of + Right a -> a + Left e -> counterexample (show e) False + +prop_threadId_order_order_Sim :: Positive Int -> Property +prop_threadId_order_order_Sim n = + exploreSimTrace id (test_threadId_order n) $ \_ trace -> + case traceResult False trace of + Right a -> a + Left e -> counterexample (show e) False + +-- +-- MonadFix properties +-- + +-- | Purity demands that @mfix (return . f) = return (fix f)@. +-- +prop_mfix_purity :: Positive Int -> Property +prop_mfix_purity (Positive n) = + exploreSimTrace id (mfix (return . factorial)) $ \_ trace -> + case traceResult False trace of + Right f -> f n === fix factorial n + Left e -> counterexample (show e) False + where + factorial :: (Int -> Int) -> Int -> Int + factorial = \rec_ k -> if k <= 1 then 1 else k * rec_ (k - 1) + +prop_mfix_purity_2 :: [Positive Int] -> Property +prop_mfix_purity_2 as = + -- note: both 'IOSim' expressions are equivalent using 'Monad' and + -- 'Applicative' laws only. + exploreSimTrace id (join $ mfix (return . recDelay) + <*> return as') (\_ trace -> + case traceResult False trace of + Right a -> a === expected + Left e -> counterexample (show e) False) + .&&. + exploreSimTrace id (mfix (return . recDelay) >>= ($ as')) (\_ trace -> + case traceResult False trace of + Right a -> a === expected + Left e -> counterexample (show e) False) + where + as' :: [Int] + as' = getPositive `map` as + + -- recursive sum using 'threadDelay' + recDelay :: ( MonadMonotonicTime m + , MonadDelay m + ) + => ([Int] -> m Time) + -> [Int] -> m Time + recDelay = \rec_ bs -> + case bs of + [] -> getMonotonicTime + (b : bs') -> threadDelay (realToFrac b) + >> rec_ bs' + + expected :: Time + expected = foldl' (flip addTime) + (Time 0) + (realToFrac `map` as') + +prop_mfix_left_shrinking + :: Int + -> NonNegative Int + -> Positive Int + -> Property +prop_mfix_left_shrinking n (NonNegative d) (Positive i) = + let mn :: IOSim s Int + mn = do say "" + threadDelay (realToFrac d) + return n + in exploreSimTrace id (mfix (\rec_ -> mn >>= \a -> + threadDelay (realToFrac d) $> a : rec_)) + (\_ trace1 -> + exploreSimTrace id (mn >>= \a -> + mfix (\rec_ -> + threadDelay (realToFrac d) $> a : rec_)) + (\_ trace2 -> + case (traceResult False trace1, traceResult False trace2) of + (Right a , Right b) -> take i a === take i b + (Left e , Right _) -> counterexample (show e) False + (Right _ , Left e) -> counterexample (show e) False + (Left e , Left e') -> counterexample (show e ++ " " ++ show e') False)) + + +-- | 'Example 8.2.1' in 'Value Recursion in Monadic Computations' +-- +-- +prop_mfix_lazy :: NonEmptyList Char + -> Property +prop_mfix_lazy (NonEmpty env) = + exploreSimTrace id (withEnv (mfix . replicateHeadM)) (\_ trace -> + case traceResult False trace of + Right a -> take samples a === replicate samples (head env) + Left e -> counterexample (show e) False) + where + samples :: Int + samples = 10 + + replicateHeadM :: + ( + + MonadFail m, + MonadFail (STM m), + + MonadSTM m + ) + => m Char + -> String -> m String + replicateHeadM getChar_ as = do + -- Note: 'getChar' will be executed only once! This follows from 'fixIO` + -- semantics. + a <- getChar_ + return (a : as) + + -- construct 'getChar' using the simulated environment + withEnv :: ( + + MonadFail m, + + MonadSTM m + ) + => (m Char -> m a) -> m a + withEnv k = do + v <- newTVarIO env + let getChar_ = + atomically $ do + as <- readTVar v + case as of + [] -> error "withEnv: runtime error" + (a : as') -> writeTVar v as' + $> a + k getChar_ + +-- +-- Syncronous exceptions +-- + +unit_catch_0, unit_catch_1, unit_catch_2, unit_catch_3, unit_catch_4, + unit_catch_5, unit_catch_6, unit_fork_1 + :: Property + + +-- exploreSimTrace id (withEnv (mfix . replicateHeadM)) (\_ trace -> +-- case traceResult False trace of +-- Right a -> take samples a === replicate samples (head env) +-- Left e -> counterexample (show e) False) + +-- unhandled top level exception +unit_catch_0 = + exploreSimTrace id example $ \_ trace -> + counterexample (intercalate "\n" $ map show $ traceEvents trace) $ + counterexample (show $ selectTraceSay trace) $ + selectTraceSay trace === ["before"] + .&&. + case traceResult True trace of + Left (FailureException e) -> property ((Just DivideByZero ==) $ fromException e) + _ -> property False + where + example :: IOSim s () + example = do + say "before" + _ <- throwIO DivideByZero + say "after" + +-- normal execution of a catch frame +unit_catch_1 = + exploreSimTrace id (do catch (say "inner") + (\(_e :: IOError) -> say "handler") + say "after") + $ \_ trace -> + selectTraceSay trace === ["inner", "after"] + +-- catching an exception thrown in a catch frame +unit_catch_2 = + exploreSimTrace id + (do catch (do say "inner1" + _ <- throwIO DivideByZero + say "inner2") + (\(_e :: ArithException) -> say "handler") + say "after" + ) $ \_ trace -> + selectTraceSay trace === ["inner1", "handler", "after"] + +-- not catching an exception of the wrong type +unit_catch_3 = + exploreSimTrace id + (do catch (do say "inner" + throwIO DivideByZero) + (\(_e :: IOError) -> say "handler") + say "after" + ) $ \_ trace -> + selectTraceSay trace === ["inner"] + + +-- catching an exception in an outer handler +unit_catch_4 = + exploreSimTrace id + (do catch (catch (do say "inner" + throwIO DivideByZero) + (\(_e :: IOError) -> say "handler1")) + (\(_e :: ArithException) -> say "handler2") + say "after" + ) $ \_ trace -> + selectTraceSay trace === ["inner", "handler2", "after"] + + +-- catching an exception in the inner handler +unit_catch_5 = + exploreSimTrace id + (do catch (catch (do say "inner" + throwIO DivideByZero) + (\(_e :: ArithException) -> say "handler1")) + (\(_e :: ArithException) -> say "handler2") + say "after" + ) $ \_ trace -> + selectTraceSay trace === ["inner", "handler1", "after"] + +-- catching an exception in the inner handler, rethrowing and catching in outer +unit_catch_6 = + exploreSimTrace id + (do catch (catch (do say "inner" + throwIO DivideByZero) + (\(e :: ArithException) -> do + say "handler1" + throwIO e)) + (\(_e :: ArithException) -> say "handler2") + say "after" + ) $ \_ trace -> + selectTraceSay trace === ["inner", "handler1", "handler2", "after"] + +-- evaluate should catch pure errors +unit_evaluate_0 :: Property +unit_evaluate_0 = + -- This property also fails if the @error@ is not caught by the sim monad + -- and instead reaches the QuickCheck driver. + -- property $ isLeft $ runSim $ evaluate (error "boom" :: ()) + exploreSimTrace id (evaluate (error "boom" :: ())) $ \_ trace -> + case traceResult False trace of + Right _ -> counterexample "didn't fail" False + Left _ -> property True + + +-- Try works and we can pass exceptions back from threads. +-- And terminating with an exception is reported properly. +unit_fork_1 = + exploreSimTrace id example $ \_ trace -> + selectTraceSay trace === ["parent", "user error (oh noes!)"] + .&&. case traceResult True trace of + Left (FailureException e) + | Just ioe <- fromException e + , isUserError ioe + , ioeGetErrorString ioe == "oh noes!" -> property True + _ -> property False + where + example :: IOSim s () + example = do + resVar <- newEmptyTMVarIO + void $ forkIO $ do + res <- try (fail "oh noes!") + atomically (putTMVar resVar (res :: Either SomeException ())) + say "parent" + Left e <- atomically (takeTMVar resVar) + say (show e) + throwIO e + + +-- +-- Asyncronous exceptions +-- + +unit_async_1, unit_async_2, unit_async_3, unit_async_4, + unit_async_5, unit_async_6, unit_async_7, unit_async_8, + unit_async_9 + :: Property + + +unit_async_1 = + exploreSimTrace id + (do tid <- myThreadId + say "before" + throwTo tid DivideByZero + say "after" + ) $ \_ trace -> + selectTraceSay trace === ["before"] + + +unit_async_2 = + runSimTraceSay + (do tid <- myThreadId + catch (do say "before" + throwTo tid DivideByZero + say "never") + (\(_e :: ArithException) -> say "handler")) + === + ["before", "handler"] + + +unit_async_3 = + exploreSimTrace id + (do tid <- forkIO $ say "child" + threadDelay 1 + -- child has already terminated when we throw the async exception + throwTo tid DivideByZero + say "parent done" + ) $ \_ trace -> + selectTraceSay trace === ["child", "parent done"] + + +unit_async_4 = + exploreSimTrace id + (do tid <- forkIO $ do + say "child" + catch (atomically retry) + (\(_e :: ArithException) -> say "handler") + say "child done" + threadDelay 1 + throwTo tid DivideByZero + threadDelay 1 + say "parent done" + ) $ \_ trace -> + selectTraceSay trace === ["child", "handler", "child done", "parent done"] + + +unit_async_5 = + exploreSimTrace id + (do tid <- forkIO $ mask_ $ + do + say "child" + threadDelay 1 + say "child masked" + -- while masked, do a blocking (interruptible) operation + catch (atomically retry) + (\(_e :: ArithException) -> say "handler") + say "child done" + -- parent and child wake up on the runqueue at the same time + threadDelay 1 + throwTo tid DivideByZero + threadDelay 1 + say "parent done" + ) $ \_ trace -> + selectTraceSay trace === ["child", "child masked", "handler", "child done", "parent done"] + + +unit_async_6 = + exploreSimTrace id + (do tid <- forkIO $ + mask_ $ do + say "child" + threadDelay 1 + fail "oh noes!" + -- parent and child wake up on the runqueue at the same time + threadDelay 1 + throwTo tid DivideByZero + -- throwTo blocks but then unblocks because the child dies + say "parent done") $ \_ trace -> + selectTraceSay trace === ["child", "parent done"] + + +unit_async_7 = + exploreSimTrace id + (do tid <- forkIO $ do + uninterruptibleMask_ $ do + say "child" + threadDelay 1 + say "child masked" + -- while masked, do a blocking (interruptible) operation + catch (threadDelay 1) + (\(_e :: ArithException) -> say "handler") + say "child done" + say "never" + -- parent and child wake up on the runqueue at the same time + threadDelay 1 + throwTo tid DivideByZero + threadDelay 1 + say "parent done") $ \_ trace -> + selectTraceSay trace === ["child", "child masked", "child done", "parent done"] + + +unit_async_8 = + exploreSimTrace id + (uninterruptibleMask_ $ do + tid <- forkIO $ atomically retry + throwTo tid DivideByZero) $ \_ trace -> + case traceResult False trace of + Left FailureDeadlock {} -> property True + _ -> property False + + +unit_async_9 = + exploreSimTrace id + (do tid <- forkIO $ do + uninterruptibleMask_ $ do + say "child" + threadDelay 1 + say "child masked" + -- while masked do a blocking operation, but this is + -- an uninterruptible mask so nothing happens + catch (threadDelay 1) + (\(_e :: ArithException) -> say "handler") + say "child done" + say "never" + threadDelay 1 + throwTo tid DivideByZero + threadDelay 1 + say "parent done") $ \_ trace -> + selectTraceSay trace === ["child", "child masked", "child done", "parent done"] + + +-- +-- Tests vs STM operational semantics +-- + +-- | Compare the behaviour of the STM reference operational semantics with +-- the behaviour of the IO simulator's STM implementation. +-- +prop_stm_referenceSim :: SomeTerm -> Property +prop_stm_referenceSim t = + exploreSimTrace id (prop_stm_referenceM t) $ \_ trace -> + case traceResult False trace of + Right a -> a + Left e -> counterexample (show e) False + +prop_timeout_no_deadlock_Sim :: Property +prop_timeout_no_deadlock_Sim = -- runSimOrThrow prop_timeout_no_deadlockM + exploreSimTrace id prop_timeout_no_deadlockM $ \_ trace -> + case traceResult False trace of + Right a -> property a + Left e -> counterexample (show e) False + +-- +-- MonadMask properties +-- + +unit_set_masking_state_ST :: MaskingState -> Property +unit_set_masking_state_ST ms = + exploreSimTrace id (prop_set_masking_state ms) $ \_ trace -> + case traceResult False trace of + Right a -> a + Left e -> counterexample (show e) False + +unit_unmask_ST :: MaskingState -> MaskingState -> Property +unit_unmask_ST ms ms' = + exploreSimTrace id (prop_unmask ms ms') $ \_ trace -> + case traceResult False trace of + Right a -> a + Left e -> counterexample (show e) False + +unit_fork_masking_state_ST :: MaskingState -> Property +unit_fork_masking_state_ST ms = + exploreSimTrace id (prop_fork_masking_state ms) $ \_ trace -> + case traceResult False trace of + Right a -> a + Left e -> counterexample (show e) False + +unit_fork_unmask_ST :: MaskingState -> MaskingState -> Property +unit_fork_unmask_ST ms ms' = + exploreSimTrace id (prop_fork_unmask ms ms') $ \_ trace -> + case traceResult False trace of + Right a -> a + Left e -> counterexample (show e) False + +unit_catch_throwIO_masking_state_ST :: MaskingState -> Property +unit_catch_throwIO_masking_state_ST ms = + exploreSimTrace id (prop_catch_throwIO_masking_state ms) $ \_ trace -> + case traceResult False trace of + Right a -> a + Left e -> counterexample (show e) False + +unit_catch_throwTo_masking_state_ST :: MaskingState -> Property +unit_catch_throwTo_masking_state_ST ms = + exploreSimTrace id (prop_catch_throwTo_masking_state ms) $ \_ trace -> + case traceResult False trace of + Right a -> a + Left e -> counterexample (show e) False + +unit_catch_throwTo_masking_state_async_ST :: MaskingState -> Property +unit_catch_throwTo_masking_state_async_ST ms = + exploreSimTrace id (prop_catch_throwTo_masking_state_async ms) $ \_ trace -> + case traceResult False trace of + Right a -> a + Left e -> counterexample (show e) False + +unit_catch_throwTo_masking_state_async_mayblock_ST :: MaskingState -> Property +unit_catch_throwTo_masking_state_async_mayblock_ST ms = + exploreSimTrace id (prop_catch_throwTo_masking_state_async_mayblock ms) $ \_ trace -> + case traceResult False trace of + Right a -> a + Left e -> counterexample (show e) False diff --git a/io-sim/test/Test/STM.hs b/io-sim/test/Test/Control/Monad/STM.hs similarity index 99% rename from io-sim/test/Test/STM.hs rename to io-sim/test/Test/Control/Monad/STM.hs index f818b705..118f284b 100644 --- a/io-sim/test/Test/STM.hs +++ b/io-sim/test/Test/Control/Monad/STM.hs @@ -19,7 +19,7 @@ -- -- -- -module Test.STM where +module Test.Control.Monad.STM where import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map diff --git a/io-sim/test/Test/Control/Monad/Utils.hs b/io-sim/test/Test/Control/Monad/Utils.hs new file mode 100644 index 00000000..b92d9dac --- /dev/null +++ b/io-sim/test/Test/Control/Monad/Utils.hs @@ -0,0 +1,509 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Test.Control.Monad.Utils where + +import Data.Array +import Data.Fixed (Fixed (..), Micro) +import Data.Function (on) +import Data.Graph +import Data.List (sortBy) + +import Control.Monad + +import Control.Monad.Class.MonadFork +import Control.Concurrent.Class.MonadSTM.Strict +import Control.Monad.Class.MonadThrow +import Control.Monad.Class.MonadTime +import Control.Monad.Class.MonadTimer +import Control.Monad.IOSim + +import Test.Control.Monad.STM + +import Test.QuickCheck + +-- +-- Read/Write graph +-- + +prop_stm_graph :: (MonadFork m, MonadSTM m) => TestThreadGraph -> m () +prop_stm_graph (TestThreadGraph g) = do + vars <- listArray (bounds g) <$> + sequence [ newTVarIO False | _ <- vertices g ] + forM_ (vertices g) $ \v -> + void $ forkIO $ do + -- read all the inputs and wait for them to become true + -- then write to all the outputs + let incomming = g' ! v + outgoing = g ! v + atomically $ do + sequence_ [ readTVar (vars ! var) >>= check | var <- incomming ] + sequence_ [ writeTVar (vars ! var) True | var <- outgoing ] + + let -- the vertices with outgoing but no incoming edges + inputs = [ v + | v <- vertices g + , not (null (g ! v)) + , null (g' ! v) ] + -- the vertices with incoming but no outgoing edges + outputs = [ v + | v <- vertices g + , not (null (g' ! v)) + , null (g ! v) ] + + -- write to the inputs and wait for the outputs + void $ forkIO $ atomically $ sequence_ [ writeTVar (vars ! var) True | var <- inputs ] + atomically $ sequence_ [ readTVar (vars ! var) >>= check | var <- outputs ] + where + g' = transposeG g -- for incoming edges + +newtype TestThreadGraph = TestThreadGraph Graph + deriving Show + +instance Arbitrary TestThreadGraph where + arbitrary = + sized $ \sz -> + TestThreadGraph <$> arbitraryAcyclicGraph + (choose (2, 8 `min` (sz `div` 3))) + (choose (1, 8 `min` (sz `div` 3))) + 0.3 + +arbitraryAcyclicGraph :: Gen Int -> Gen Int -> Float -> Gen Graph +arbitraryAcyclicGraph genNRanks genNPerRank edgeChance = do + nranks <- genNRanks + rankSizes <- replicateM nranks genNPerRank + let rankStarts = scanl (+) 0 rankSizes + rankRanges = drop 1 (zip rankStarts (tail rankStarts)) + totalRange = sum rankSizes + rankEdges <- mapM (uncurry genRank) rankRanges + return $ buildG (0, totalRange-1) (concat rankEdges) + where + genRank :: Vertex -> Vertex -> Gen [Edge] + genRank rankStart rankEnd = + filterM (const (pick edgeChance)) + [ (i,j) + | i <- [0..rankStart-1] + , j <- [rankStart..rankEnd-1] + ] + + pick :: Float -> Gen Bool + pick chance = (< chance) <$> choose (0,1) + + +-- +-- Timers +-- + +newtype TestMicro = TestMicro [Micro] + deriving Show + +-- | +-- Arbitrary non negative micro numbers with a high probability of +-- repetitions. +instance Arbitrary TestMicro where + arbitrary = sized $ \n -> TestMicro <$> genN n [] + where + genN :: Int -> [Micro] -> Gen [Micro] + genN 0 rs = return rs + genN n [] = do + r <- genMicro + genN (n - 1) [r] + genN n rs = do + r <- frequency + [ (2, elements rs) + , (1, genMicro) + ] + genN (n - 1) (r : rs) + + genMicro :: Gen Micro + genMicro = MkFixed <$> arbitrary + + shrink (TestMicro rs) = [ TestMicro rs' | rs' <- shrinkList (const []) rs ] + +test_timers :: forall m. + ( MonadFork m + , MonadSTM m + , MonadTimer m + ) + => [DiffTime] + -> m Property +test_timers xs = + label (lbl xs) . isValid <$> withProbe experiment + where + countUnique :: Eq a => [a] -> Int + countUnique [] = 0 + countUnique (a:as) = + let as' = filter (== a) as + in 1 + countUnique as' + + lbl :: Eq a => [a] -> String + lbl as = + let p = (if null as then 0 else (100 * countUnique as) `div` length as) `mod` 10 * 10 + in show p ++ "% unique" + + experiment :: Probe m (DiffTime, Int) -> m () + experiment p = do + tvars <- forM (zip xs [0..]) $ \(t, idx) -> do + v <- newTVarIO False + void $ forkIO $ threadDelay t >> do + probeOutput p (t, idx) + atomically $ writeTVar v True + return v + + -- wait for all tvars + forM_ tvars $ \v -> atomically (readTVar v >>= check) + + isValid :: [(DiffTime, Int)] -> Property + isValid tr = + -- all timers should fire + (length tr === length xs) + -- timers should fire in the right order + .&&. (sortBy (on sortFn fst) tr === tr) + + -- timers with negative timeout never fired, so we treat them as they would + -- all fired at once at @-∞@. This is to say that the following function is + -- a well defined partial order. + sortFn :: DiffTime -> DiffTime -> Ordering + sortFn a b | a >= 0 && b >= 0 = a `compare` b + | a < 0 && b < 0 = EQ + | otherwise = a `compare` b + +-- +-- Forking +-- + +test_fork_order :: forall m. + ( MonadFork m + , MonadSTM m + , MonadTimer m + ) + => Positive Int + -> m Property +test_fork_order = \(Positive n) -> isValid n <$> withProbe (experiment n) + where + experiment :: Int -> Probe m Int -> m () + experiment 0 _ = return () + experiment n p = do + v <- newTVarIO False + + void $ forkIO $ do + probeOutput p n + atomically $ writeTVar v True + experiment (n - 1) p + + -- wait for the spawned thread to finish + atomically $ readTVar v >>= check + + isValid :: Int -> [Int] -> Property + isValid n tr = tr === [n,n-1..1] + +test_threadId_order :: forall m. + ( MonadFork m + , MonadSTM m + , MonadTimer m + ) + => Positive Int + -> m Property +test_threadId_order = \(Positive n) -> do + isValid n <$> (forM [1..n] (const experiment)) + where + experiment :: m (ThreadId m) + experiment = do + v <- newTVarIO False + + tid <- forkIO $ atomically $ writeTVar v True + + -- wait for the spawned thread to finish + atomically $ readTVar v >>= check + return tid + + isValid :: Int -> [ThreadId m] -> Property + isValid n tr = map show tr === map (("ThreadId " ++ ) . show . (:[])) [1..n] + +-- This property is not actually deterministic in IO. Uncomment the following +-- and try it! Arguably therefore, this property does not need to be true for +-- the Sim either. Perhaps we should introduce random scheduling and abandon +-- this property. In the meantime it's a helpful sanity check. + +--prop_wakeup_order_IO = ioProperty test_wakeup_order + +test_wakeup_order :: ( MonadFork m + , MonadSTM m + , MonadTimer m + ) + => m Property +test_wakeup_order = do + v <- newTVarIO False + wakupOrder <- + withProbe $ \p -> do + sequence_ + [ do _ <- forkIO $ do + atomically $ do + x <- readTVar v + check x + probeOutput p (n :: Int) + threadDelay 0.1 + | n <- [0..9] ] + atomically $ writeTVar v True + threadDelay 0.1 + return (wakupOrder === [0..9]) --FIFO order + +-- +-- Probe mini-abstraction +-- + +-- | Where returning results directly is not convenient, we can build up +-- a trace of events we want to observe, and can do probe output from +-- multiple threads. +-- +type Probe m x = StrictTVar m [x] + +withProbe :: MonadSTM m => (Probe m x -> m ()) -> m [x] +withProbe action = do + probe <- newTVarIO [] + action probe + reverse <$> atomically (readTVar probe) + +probeOutput :: MonadSTM m => Probe m x -> x -> m () +probeOutput probe x = atomically (modifyTVar probe (x:)) + +-- +-- Tests vs STM operational semantics +-- + +--TODO: would be nice to also have stronger tests here: +-- * compare all the tvar values in the heap +-- * compare the read and write sets + +-- | Compare the behaviour of the STM reference operational semantics with +-- the behaviour of any 'MonadSTM' STM implementation. +-- +prop_stm_referenceM :: (MonadSTM m, MonadThrow (STM m), MonadCatch (STM m), MonadCatch m) + => SomeTerm -> m Property +prop_stm_referenceM (SomeTerm _tyrep t) = do + let (r1, _heap) = evalAtomically t + r2 <- execAtomically t + return (r1 === r2) + +-- | Check that 'timeout' does not deadlock when executed with asynchronous +-- exceptions uninterruptibly masked. +-- +prop_timeout_no_deadlockM :: forall m. ( MonadFork m, MonadSTM m, MonadTimer m, MonadMask m ) + => m Bool +prop_timeout_no_deadlockM = do + v <- registerDelay' 0.01 + r <- uninterruptibleMask_ $ timeout 0.02 $ do + atomically $ do + readTVar v >>= check + return True + case r of + Nothing -> return False + Just b -> return b + where + -- Like 'registerDelay', but does not require threaded RTS in the @m ~ IO@ + -- case. + registerDelay' :: DiffTime -> m (StrictTVar m Bool) + registerDelay' delta = do + v <- newTVarIO False + _ <- forkIO $ do + threadDelay delta + atomically (writeTVar v True) + return v + +-- +-- MonadMask properties +-- + +setMaskingState_ :: MonadMask m => MaskingState -> m a -> m a +setMaskingState_ Unmasked = id +setMaskingState_ MaskedInterruptible = mask_ +setMaskingState_ MaskedUninterruptible = uninterruptibleMask_ + +setMaskingState :: MonadMask m => MaskingState + -> ((forall x. m x -> m x) -> m a) -> m a +setMaskingState Unmasked = \f -> f id +setMaskingState MaskedInterruptible = mask +setMaskingState MaskedUninterruptible = uninterruptibleMask + +maxMS :: MaskingState -> MaskingState -> MaskingState +maxMS MaskedUninterruptible _ = MaskedUninterruptible +maxMS _ MaskedUninterruptible = MaskedUninterruptible +maxMS MaskedInterruptible _ = MaskedInterruptible +maxMS _ MaskedInterruptible = MaskedInterruptible +maxMS Unmasked Unmasked = Unmasked + +-- | Check that setting masking state is effective. +-- +prop_set_masking_state :: MonadMaskingState m + => MaskingState + -> m Property +prop_set_masking_state ms = + setMaskingState_ ms $ do + ms' <- getMaskingState + return (ms === ms') + +-- | Check that 'unmask' restores the masking state. +-- +prop_unmask :: MonadMaskingState m + => MaskingState + -> MaskingState + -> m Property +prop_unmask ms ms' = + setMaskingState_ ms $ + setMaskingState ms' $ \unmask -> do + ms'' <- unmask getMaskingState + return (ms'' === ms) + +-- | Check that masking state is inherited by a forked thread. +-- +prop_fork_masking_state :: ( MonadMaskingState m + , MonadFork m + , MonadSTM m + ) + => MaskingState -> m Property +prop_fork_masking_state ms = setMaskingState_ ms $ do + var <- newEmptyTMVarIO + _ <- forkIO $ getMaskingState >>= atomically . putTMVar var + ms' <- atomically $ takeTMVar var + return $ ms === ms' + +-- | Check that 'unmask' restores the masking state in a forked thread. +-- +-- Note: unlike 'prop_unmask', 'forkIOWithUnmask's 'unmask' function will +-- restore 'Unmasked' state, not the encosing masking state. +-- +prop_fork_unmask :: ( MonadMaskingState m + , MonadFork m + , MonadSTM m + ) + => MaskingState + -> MaskingState + -> m Property +prop_fork_unmask ms ms' = + setMaskingState_ ms $ + setMaskingState_ ms' $ do + var <- newEmptyTMVarIO + _ <- forkIOWithUnmask $ \unmask -> unmask getMaskingState + >>= atomically . putTMVar var + ms'' <- atomically $ takeTMVar var + return $ Unmasked === ms'' + +-- | A unit test which checks the masking state in the context of a catch +-- handler. +-- +prop_catch_throwIO_masking_state :: forall m. MonadMaskingState m + => MaskingState -> m Property +prop_catch_throwIO_masking_state ms = + setMaskingState_ ms $ do + throwIO (userError "error") + `catch` \(_ :: IOError) -> do + ms' <- getMaskingState + return $ ms' === MaskedInterruptible `maxMS` ms + +-- | Like 'prop_catch_masking_state' but using 'throwTo'. +-- +prop_catch_throwTo_masking_state :: forall m. + ( MonadMaskingState m + , MonadFork m + ) + => MaskingState -> m Property +prop_catch_throwTo_masking_state ms = + setMaskingState_ ms $ do + tid <- myThreadId + (throwTo tid (userError "error") >> error "impossible") + `catch` \(_ :: IOError) -> do + ms' <- getMaskingState + return $ ms' === MaskedInterruptible `maxMS` ms + +-- | Like 'prop_catch_throwTo_masking_state' but using 'throwTo' to a different +-- thread which is in a non-blocking mode. +-- +prop_catch_throwTo_masking_state_async :: forall m. + ( MonadMaskingState m + , MonadFork m + , MonadSTM m + , MonadDelay m + ) + => MaskingState -> m Property +prop_catch_throwTo_masking_state_async ms = do + sgnl <- newEmptyTMVarIO + var <- newEmptyTMVarIO + tid <- forkIO $ + setMaskingState ms $ \unmask -> + (do atomically $ putTMVar sgnl () + unmask (threadDelay 1) + ) + `catch` \(_ :: IOError) -> do + ms' <- getMaskingState + atomically $ putTMVar var (ms' === ms `maxMS` MaskedInterruptible) + -- wait until the catch handler is installed + atomically $ takeTMVar sgnl + -- the forked thread is interruptibly blocked on `threadDelay`, + -- `throwTo` will not block + throwTo tid (userError "error") + atomically $ takeTMVar var + +-- | Like 'prop_catch_throwTo_masking_state_async' but 'throwTo' will block if +-- masking state is set to 'MaskedUninterruptible'. This makes sure that the +-- 'willBlock' branch of 'ThrowTo' in 'schedule' is covered. +-- +prop_catch_throwTo_masking_state_async_mayblock :: forall m. + ( MonadMaskingState m + , MonadFork m + , MonadSTM m + , MonadDelay m + ) + => MaskingState -> m Property +prop_catch_throwTo_masking_state_async_mayblock ms = do + sgnl <- newEmptyTMVarIO + var <- newEmptyTMVarIO + tid <- forkIO $ + setMaskingState ms $ \unmask -> + (do atomically $ putTMVar sgnl () + -- if 'ms' is 'MaskedUninterruptible' then the following + -- 'threadDelay' will block. + threadDelay 0.1 + -- make sure that even in 'MaskedUninterruptible' the thread + -- unblocks so async exceptions can be delivered. + unmask (threadDelay 1) + ) + `catch` \(_ :: IOError) -> do + ms' <- getMaskingState + atomically $ putTMVar var (ms' === ms `maxMS` MaskedInterruptible) + -- wait until the catch handler is installed + atomically $ takeTMVar sgnl + threadDelay 0.05 + -- we know the forked thread is interruptibly blocked on `threadDelay`, + -- `throwTo` will not be blocked. + throwTo tid (userError "error") + atomically $ takeTMVar var + +-- +-- MonadMask properties +-- + +forall_masking_states :: (MaskingState -> Property) + -> Property +forall_masking_states prop = + -- make sure that the property is executed once! + withMaxSuccess 1 $ + foldr (\ms p -> counterexample (show ms) (prop ms) .&&. p) + (property True) + [Unmasked, MaskedInterruptible, MaskedUninterruptible] + +-- +-- Utils +-- + +runSimTraceSay :: (forall s. IOSim s a) -> [String] +runSimTraceSay action = selectTraceSay (runSimTrace action) + +selectTraceSay :: SimTrace a -> [String] +selectTraceSay (SimTrace _ _ _ (EventSay msg) trace) = msg : selectTraceSay trace +selectTraceSay (SimTrace _ _ _ _ trace) = selectTraceSay trace +selectTraceSay (SimPORTrace _ _ _ _ (EventSay msg) trace) = msg : selectTraceSay trace +selectTraceSay (SimPORTrace _ _ _ _ _ trace) = selectTraceSay trace +selectTraceSay _ = [] +