WIP iosim stuff

Author: MaximilianAlgehed

quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs

@@ -1,18 +1,25 @@
 {-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE ImpredicativeTypes #-}
 
 -- | Define several variant models of /counters/ which are useful to
 -- test or use examples for various behaviours of the runtime.
 module Spec.DynamicLogic.Counters where
 
-import Control.Concurrent
 import Control.Monad.Reader
-import Data.IORef
-import Test.QuickCheck (frequency, Property)
+import Test.QuickCheck hiding (Some)
+import Test.QuickCheck.Gen.Unsafe
 import Test.QuickCheck.StateModel
 import Test.QuickCheck.ParallelActions
 import Test.QuickCheck.Extras
 import Test.QuickCheck.Monadic
 
+import Control.Concurrent.Class.MonadSTM
+import Control.Monad.Class.MonadFork
+import Control.Monad.Class.MonadThrow
+import Control.Monad.Class.MonadTimer
+import Control.Monad.Class.MonadTest
+import Control.Monad.IOSim
+
 -- A very simple model with a single action that always succeed in
 -- predictable way. This model is useful for testing the runtime.
 newtype SimpleCounter = SimpleCounter {count :: Int}
@@ -33,10 +40,13 @@ instance StateModel SimpleCounter where
 
   nextState SimpleCounter{count} IncSimple _ = SimpleCounter (count + 1)
 
-instance RunModel SimpleCounter (ReaderT (IORef Int) IO) where
+instance RunModel SimpleCounter (ReaderT (CounterState IO) IO) where
   perform _ IncSimple _ = do
-    ref <- ask
-    lift $ atomicModifyIORef' ref (\count -> (succ count, count))
+    ref <- asks counterState
+    lift $ atomically $ do
+      c <- readTVar ref
+      writeTVar ref (c + 1)
+      return c
 
 -- A very simple model with a single action whose postcondition fails in a
 -- predictable way. This model is useful for testing the runtime.
@@ -58,10 +68,13 @@ instance StateModel FailingCounter where
 
   nextState FailingCounter{failingCount} Inc' _ = FailingCounter (failingCount + 1)
 
-instance RunModel FailingCounter (ReaderT (IORef Int) IO) where
+instance RunModel FailingCounter (ReaderT (CounterState IO) IO) where
   perform _ Inc' _ = do
-    ref <- ask
-    lift $ atomicModifyIORef' ref (\count -> (succ count, count))
+    ref <- asks counterState
+    lift $ atomically $ do
+      c <- readTVar ref
+      writeTVar ref (c + 1)
+      return c
 
   postcondition (_, FailingCounter{failingCount}) _ _ _ = pure $ failingCount < 4
 
@@ -86,37 +99,74 @@ instance StateModel Counter where
   nextState (Counter n) Inc _ = Counter (n + 1)
   nextState _ Reset _ = Counter 0
 
-instance RunModel Counter (ReaderT (IORef Int) IO) where
+newtype CounterState m = CounterState { counterState :: TVar m Int }
+
+setupCounterState :: MonadSTM m => m (CounterState m)
+setupCounterState = CounterState <$> atomically (newTVar 0)
+
+instance (MonadSTM m) => RunModel Counter (ReaderT (CounterState m) m) where
   perform _ Inc _ = do
-    ref <- ask
+    ref <- asks counterState
     lift $ do
-      n <- readIORef ref
-      threadDelay 1000
-      writeIORef ref (n + 1)
+      n <- atomically $ readTVar ref
+      atomically $ writeTVar ref (n + 1)
   perform _ Reset _ = do
-    ref <- ask
+    ref <- asks counterState
     lift $ do
-      n <- readIORef ref
-      threadDelay 1000
-      writeIORef ref 0
+      n <- atomically $ readTVar ref
+      atomically $ writeTVar ref 0
       pure n
 
   postcondition (Counter n, _) Reset _ res = pure $ n == res
   postcondition _ _ _ _ = pure True
 
-instance RunModelPar Counter (ReaderT (IORef Int) IO) where
+instance MonadSTM m => RunModelPar Counter (ReaderT (CounterState m) m) where
   performPar Inc _ = do
-    ref <- ask
-    -- lift $ atomicModifyIORef ref (\ c -> (c+1, ()))
+    ref <- asks counterState
+    -- lift $ atomically $ modifyTVar ref (\ c -> (c+1, ()))
     lift $ do
-      n <- readIORef ref
-      threadDelay 5000
-      writeIORef ref (n + 1)
+      n <- atomically $ readTVar ref
+      atomically $ writeTVar ref (n + 1)
   performPar Reset _ = do
-    ref <- ask
-    lift $ atomicModifyIORef ref (\ c -> (0, c))
+    ref <- asks counterState
+    lift $ atomically $ do
+      c <- readTVar ref
+      writeTVar ref 0
+      return c
+
+prop_counter :: Actions Counter -> Property
+prop_counter as = monadicIO $ do
+  ref <- lift $ atomically $ newTVar (0 :: Int)
+  runPropertyReaderT (runActions as) (CounterState ref :: CounterState IO)
+  assert True
 
 prop_counter_par :: ParallelActions Counter -> Property
 prop_counter_par as = always 10 $ monadicIO $ do
-  ref <- lift $ newIORef (0 :: Int)
+  ref <- lift setupCounterState
   runPropertyReaderT (runParActions as) ref
+
+prop_counter_parIOSimPor :: ParallelActions Counter -> Property
+prop_counter_parIOSimPor as =
+  monadicIOSimPOR_ prop
+  where
+    prop :: forall s. PropertyM (IOSim s) ()
+    prop = do
+      ref <- lift $ atomically $ newTVar (0 :: Int)
+      lift $ exploreRaces
+      runPropertyReaderT (runParActions as) (CounterState ref :: CounterState (IOSim s))
+
+monadicIOSimPOR_ :: Testable a => (forall s. PropertyM (IOSim s) a) -> Property
+monadicIOSimPOR_ prop = forAllBlind prop' $ \ p -> exploreSimTrace id p $ \ _ tr ->
+    either (flip counterexample False . show) id $ traceResult False tr
+  where
+    prop' :: Gen (forall s. IOSim s Property)
+    prop' = do
+      Capture eval <- capture
+      pure $ eval $ monadic' prop
+
+instance Forking (IOSim s) where
+  forkThread io = do
+    t <- atomically newEmptyTMVar
+    forkIO $ io >>= atomically . putTMVar t
+    return $ atomically $ takeTMVar t
+

quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs

@@ -4,10 +4,9 @@
 module Test.QuickCheck.StateModelSpec where
 
 import Control.Monad.Reader (lift)
-import Data.IORef (newIORef)
 import Data.List (isInfixOf)
-import Spec.DynamicLogic.Counters (Counter (..), FailingCounter, SimpleCounter (..))
-import Test.QuickCheck (Property, Result (..), Testable, chatty, checkCoverage, choose, counterexample, cover, noShrinking, property, stdArgs)
+import Spec.DynamicLogic.Counters (FailingCounter, SimpleCounter (..), prop_counter, prop_counter_parIOSimPor, setupCounterState)
+import Test.QuickCheck
 import Test.QuickCheck.Extras (runPropertyReaderT)
 import Test.QuickCheck.Monadic (assert, monadicIO, monitor, pick)
 import Test.QuickCheck.StateModel (
@@ -43,30 +42,28 @@ tests =
     , testProperty
         "moreActions introduces long sequences of actions"
         prop_longSequences
+    , testProperty
+        "IOSimPor finds counterexample in parallel counters"
+        $ expectFailure prop_counter_parIOSimPor
+
     ]
 
 captureTerminal :: Testable p => p -> IO Result
 captureTerminal p =
   withState stdArgs{chatty = False} $ \st ->
     test st (property p)
 
-prop_counter :: Actions Counter -> Property
-prop_counter as = monadicIO $ do
-  ref <- lift $ newIORef (0 :: Int)
-  runPropertyReaderT (runActions as) ref
-  assert True
-
 prop_returnsFinalState :: Actions SimpleCounter -> Property
 prop_returnsFinalState actions@(Actions as) =
   monadicIO $ do
-    ref <- lift $ newIORef (0 :: Int)
+    ref <- lift $ setupCounterState
     (s, _) <- runPropertyReaderT (runActions actions) ref
     assert $ count (underlyingState s) == length as
 
 prop_variablesIndicesAre1Based :: Actions SimpleCounter -> Property
 prop_variablesIndicesAre1Based actions@(Actions as) =
   noShrinking $ monadicIO $ do
-    ref <- lift $ newIORef (0 :: Int)
+    ref <- lift setupCounterState
     (_, env) <- runPropertyReaderT (runActions actions) ref
     act <- pick $ choose (0, length as - 1)
     monitor $
@@ -81,7 +78,7 @@ prop_variablesIndicesAre1Based actions@(Actions as) =
 prop_failsOnPostcondition :: Actions FailingCounter -> Property
 prop_failsOnPostcondition actions =
   monadicIO $ do
-    ref <- lift $ newIORef (0 :: Int)
+    ref <- lift setupCounterState
     runPropertyReaderT (runActions actions) ref
     assert True