From b9e1b110a9e1a25aceb7be163c24577b6d3b91d2 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        | 63 ++++++++++++-------
 1 file changed, 40 insertions(+), 23 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..b5a314bd6 100644
--- a/test-control/Test/Control/Concurrent/Class/MonadSTM/RWVar.hs
+++ b/test-control/Test/Control/Concurrent/Class/MonadSTM/RWVar.hs
@@ -3,7 +3,8 @@ 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           Test.QuickCheck
 import           Test.Tasty
@@ -11,7 +12,8 @@ import           Test.Tasty.QuickCheck
 
 tests :: TestTree
 tests = testGroup "Test.Control.Concurrent.Class.MonadSTM.RWVar" [
-      testProperty "prop_noRace" prop_noRace
+      testProperty "prop_noRace" $ \a1 a2 a3 ->
+        prop_noRace [a1, a2, a3]
     ]
 
 data Action a = Read a | Incr a
@@ -27,34 +29,49 @@ instance Arbitrary (Action (Small Word, Small Word)) where
 -- 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)
+prop_noRace [a1, a2, a3] = exploreSimTrace f prop $ \_ tr ->
+    case traceResult False tr of
+      Left e@(FailureDeadlock _) -> counterexample (show e) $ property False
+      _                          -> property True
   where
+    f = id
+    -- f opts = opts {
+    --     explorationScheduleBound = 300
+    --   , explorationBranching = 5
+    --   }
+
     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'
+      let g = \case
+            Read (Small _n, Small _m) ->
+              RW.withReadAccess var $ \x -> do
+                say (show (Read x))
+            Incr (Small _n, Small _m) ->
+              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 ()
 
-    sayMonotonic ::  Int -> SimTrace () -> Property
-    sayMonotonic _ (Nil MainReturn{}) = property True
-    sayMonotonic prev (Cons se st') = (case se of
+    _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'
+                    $ prev     === x .&&. _sayMonotonic x st'
             Incr x -> counterexample "Unexpected Write result"
-                    $ prev + 1 === x .&&. sayMonotonic x st'
-          _ -> sayMonotonic prev st'
+                    $ prev + 1 === x .&&. _sayMonotonic x st'
+          _ -> _sayMonotonic prev st'
         _ -> property False)
-    sayMonotonic _ _ = property False
+    _sayMonotonic _ _ = property False
+prop_noRace _ = property False