From 6dd1060da7637d6ebbc0be341035a27612d51cea Mon Sep 17 00:00:00 2001
From: Joris Dral <joris@well-typed.com>
Date: Tue, 15 Oct 2024 00:38:10 +0200
Subject: [PATCH] WIP: find RWVar race condition using IOSimPOR

---
 .../Concurrent/Class/MonadSTM/RWVar.hs        | 101 +++++++++++-------
 1 file changed, 65 insertions(+), 36 deletions(-)

diff --git a/test-control/Test/Control/Concurrent/Class/MonadSTM/RWVar.hs b/test-control/Test/Control/Concurrent/Class/MonadSTM/RWVar.hs
index 2a2c92dbc..f812a22af 100644
--- a/test-control/Test/Control/Concurrent/Class/MonadSTM/RWVar.hs
+++ b/test-control/Test/Control/Concurrent/Class/MonadSTM/RWVar.hs
@@ -3,8 +3,10 @@ module Test.Control.Concurrent.Class.MonadSTM.RWVar (tests) where
 import qualified Control.Concurrent.Class.MonadSTM.RWVar as RW
 import           Control.Monad.Class.MonadAsync
 import           Control.Monad.Class.MonadSay (MonadSay (say))
-import           Control.Monad.Class.MonadTimer
+import           Control.Monad.Class.MonadTest (MonadTest (exploreRaces))
+import           Control.Monad.Class.MonadThrow
 import           Control.Monad.IOSim
+import           Data.Maybe (mapMaybe)
 import           Test.QuickCheck
 import           Test.Tasty
 import           Test.Tasty.QuickCheck
@@ -17,44 +19,71 @@ tests = testGroup "Test.Control.Concurrent.Class.MonadSTM.RWVar" [
 data Action a = Read a | Incr a
   deriving stock (Show, Eq, Read)
 
-instance Arbitrary (Action (Small Word, Small Word)) where
-  arbitrary = do
-    n <- oneof [ arbitrary, Small <$> choose (1, 5) ]
-    m <- oneof [ arbitrary, Small <$> choose (1, 5) ]
-    elements [ Read (n, m), Incr (n, m) ]
+instance Arbitrary a => Arbitrary (Action a) where
+  arbitrary = oneof [
+        Read <$> arbitrary
+      , Incr <$> arbitrary
+      ]
+  shrink (Read x) = [Read x' | x' <- shrink x]
+  shrink (Incr x) = [Incr x' | x' <- shrink x]
 
 -- | Performing reads and increments on an @'RWVar' Int@ in parallel should not
--- lead to races. We observe this by looking at the trace and seeing that the
--- value inside the 'RWVar' increases monotonically.
-prop_noRace :: [Action (Small Word, Small Word)] -> Property
-prop_noRace as = exploreSimTrace id prop (\_ st -> sayMonotonic 0 st)
+-- lead to races. We let IOSimPOR check that there are no deadlocks. We also
+-- look at the trace to see if the value inside the 'RWVar' increases
+-- monotonically.
+prop_noRace ::
+     Action ()
+  -> Action ()
+  -> Action ()
+  -> Property
+prop_noRace a1 a2 a3 = exploreSimTrace modifyOpts prop $ \_ tr ->
+    case traceResult False tr of
+      Left e -> counterexample (show e) (property False)
+      _      -> propSayMonotonic tr
   where
+    modifyOpts = id
+
     prop :: IOSim s ()
     prop = do
+      exploreRaces
       var <- RW.new (0 :: Int)
-      forConcurrently_ as $ \case
-        Read (Small n, Small m) -> do
-          threadDelay (fromIntegral n)
-          RW.withReadAccess var $ \x -> do
-            threadDelay (fromIntegral m)
-            say (show (Read x))
-        Incr (Small n, Small m) -> do
-          threadDelay (fromIntegral n)
-          RW.withWriteAccess_ var $ \x -> do
-            threadDelay (fromIntegral m)
-            let x' = x + 1
-            say (show (Incr x'))
-            pure x'
-
-    sayMonotonic ::  Int -> SimTrace () -> Property
-    sayMonotonic _ (Nil MainReturn{}) = property True
-    sayMonotonic prev (Cons se st') = (case se of
-        SimPOREvent{seType} -> case seType of
-          EventSay s -> case read s of
-            Read x -> counterexample "Unexpected Read result"
-                    $ prev     === x .&&. sayMonotonic x st'
-            Incr x -> counterexample "Unexpected Write result"
-                    $ prev + 1 === x .&&. sayMonotonic x st'
-          _ -> sayMonotonic prev st'
-        _ -> property False)
-    sayMonotonic _ _ = property False
+      let g = \case
+            Read () ->
+              RW.withReadAccess var $ \x -> do
+                say (show (Read x))
+            Incr () ->
+              RW.withWriteAccess_ var $ \x -> do
+                let x' = x + 1
+                say (show (Incr x'))
+                pure x'
+      t1 <- async (g a1)
+      t2 <- async (g a2)
+      t3 <- async (g a3)
+      async (cancel t1) >>= wait
+      (_ :: Either SomeException ()) <- try (wait t1)
+      (_ :: Either SomeException ()) <- try (wait t2)
+      (_ :: Either SomeException ()) <- try (wait t3)
+      pure ()
+
+propSayMonotonic :: SimTrace () -> Property
+propSayMonotonic simTrace = propResultsMonotonic (actionResults simTrace)
+
+propResultsMonotonic :: [Action Int] -> Property
+propResultsMonotonic as =
+    counterexample
+      ("Action results are not monotonic: " ++ show as)
+      (resultsMonotonic as)
+
+resultsMonotonic :: [Action Int] -> Bool
+resultsMonotonic = go 0
+  where
+    go _ []               = True
+    go prev (Read x : as) = prev == x     && go x as
+    go prev (Incr x : as) = prev + 1 == x && go x as
+
+actionResults :: SimTrace () -> [Action Int]
+actionResults simTrace = mapMaybe eventSayAction (traceEvents simTrace)
+  where
+    eventSayAction (_, _, _, eventType) = case eventType of
+        EventSay s -> Just (read s)
+        _          -> Nothing