From 30ab912210dfb926d2e743bedb8057d5a8acf30d Mon Sep 17 00:00:00 2001
From: Michael Walker <mike@barrucadu.co.uk>
Date: Wed, 1 Nov 2017 14:46:18 +0000
Subject: [PATCH] Don't consider TVar reads dependent

---
 dejafu/CHANGELOG.markdown          | 11 +++++++++++
 dejafu/Test/DejaFu/Common.hs       | 27 +++++++++++++++++++++++++--
 dejafu/Test/DejaFu/SCT/Internal.hs | 14 ++++++++++----
 3 files changed, 46 insertions(+), 6 deletions(-)

diff --git a/dejafu/CHANGELOG.markdown b/dejafu/CHANGELOG.markdown
index 4610301..da08638 100644
--- a/dejafu/CHANGELOG.markdown
+++ b/dejafu/CHANGELOG.markdown
@@ -7,6 +7,17 @@ This project is versioned according to the [Package Versioning Policy](https://p
 *de facto* standard Haskell versioning scheme.
 
 
+unreleased
+----------
+
+### Miscellaneous
+
+- Small improvement to dependency detection of STM transactions.
+
+
+---------------------------------------------------------------------------------------------------
+
+
 0.9.0.1
 -------
 
diff --git a/dejafu/Test/DejaFu/Common.hs b/dejafu/Test/DejaFu/Common.hs
index f4bd1bf..8f877ac 100644
--- a/dejafu/Test/DejaFu/Common.hs
+++ b/dejafu/Test/DejaFu/Common.hs
@@ -27,6 +27,8 @@ module Test.DejaFu.Common
   , ThreadAction(..)
   , isBlock
   , tvarsOf
+  , tvarsWritten
+  , tvarsRead
   -- ** Lookahead
   , Lookahead(..)
   , rewind
@@ -410,18 +412,39 @@ isBlock _ = False
 --
 -- @since 0.4.0.0
 tvarsOf :: ThreadAction -> Set TVarId
-tvarsOf act = S.fromList $ case act of
+tvarsOf act = tvarsRead act `S.union` tvarsWritten act
+
+-- | Get the @TVar@s a transaction wrote to (or would have, if it
+-- didn't @retry@).
+--
+-- @since unreleased
+tvarsWritten :: ThreadAction -> Set TVarId
+tvarsWritten act = S.fromList $ case act of
   STM trc _ -> concatMap tvarsOf' trc
   BlockedSTM trc -> concatMap tvarsOf' trc
   _ -> []
 
   where
-    tvarsOf' (TRead  tv) = [tv]
     tvarsOf' (TWrite tv) = [tv]
     tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)
     tvarsOf' (TCatch  ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)
     tvarsOf' _ = []
 
+-- | Get the @TVar@s a transaction read from.
+--
+-- @since unreleased
+tvarsRead :: ThreadAction -> Set TVarId
+tvarsRead act = S.fromList $ case act of
+  STM trc _ -> concatMap tvarsOf' trc
+  BlockedSTM trc -> concatMap tvarsOf' trc
+  _ -> []
+
+  where
+    tvarsOf' (TRead tv) = [tv]
+    tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)
+    tvarsOf' (TCatch  ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)
+    tvarsOf' _ = []
+
 ---------------------------------------
 -- Lookahead
 
diff --git a/dejafu/Test/DejaFu/SCT/Internal.hs b/dejafu/Test/DejaFu/SCT/Internal.hs
index f91e3e1..7451bcd 100644
--- a/dejafu/Test/DejaFu/SCT/Internal.hs
+++ b/dejafu/Test/DejaFu/SCT/Internal.hs
@@ -605,15 +605,21 @@ dependent memtype ds t1 a1 t2 a2 = case (a1, a2) of
   -- Dependency of STM transactions can be /greatly/ improved here, as
   -- the 'Lookahead' does not know which @TVar@s will be touched, and
   -- so has to assume all transactions are dependent.
-  (STM _ _, STM _ _)           -> not . S.null $ tvarsOf a1 `S.intersection` tvarsOf a2
-  (STM _ _, BlockedSTM _)      -> not . S.null $ tvarsOf a1 `S.intersection` tvarsOf a2
-  (BlockedSTM _, STM _ _)      -> not . S.null $ tvarsOf a1 `S.intersection` tvarsOf a2
-  (BlockedSTM _, BlockedSTM _) -> not . S.null $ tvarsOf a1 `S.intersection` tvarsOf a2
+  (STM _ _, STM _ _)           -> checkSTM
+  (STM _ _, BlockedSTM _)      -> checkSTM
+  (BlockedSTM _, STM _ _)      -> checkSTM
+  (BlockedSTM _, BlockedSTM _) -> checkSTM
 
   _ -> case (,) <$> rewind a1 <*> rewind a2 of
     Just (l1, l2) -> dependent' memtype ds t1 a1 t2 l2 && dependent' memtype ds t2 a2 t1 l1
     _ -> dependentActions memtype ds (simplifyAction a1) (simplifyAction a2)
 
+  where
+    -- STM actions A and B are dependent if A wrote to anything B
+    -- touched, or vice versa.
+    checkSTM = checkSTM' a1 a2 || checkSTM' a2 a1
+    checkSTM' a b = not . S.null $ tvarsWritten a `S.intersection` tvarsOf b
+
 -- | Variant of 'dependent' to handle 'Lookahead'.
 --
 -- Termination of the initial thread is handled specially in the DPOR