Track full MVars in the dependency state

Before:

   105,910,870,840 bytes allocated in the heap
    24,834,921,776 bytes copied during GC
        17,775,024 bytes maximum residency (7973 sample(s))
           674,464 bytes maximum slop
                50 MB total memory in use (0 MB lost due to fragmentation)

                                       Tot time (elapsed)  Avg pause  Max pause
    Gen  0     196263 colls,     0 par   43.085s  43.734s     0.0002s    0.0225s
    Gen  1      7973 colls,     0 par   21.953s  22.359s     0.0028s    0.0778s

    TASKS: 204933 (204929 bound, 4 peak workers (4 total), using -N1)

    SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

    INIT    time    0.001s  (  0.001s elapsed)
    MUT     time  127.384s  (138.737s elapsed)
    GC      time   65.038s  ( 66.093s elapsed)
    EXIT    time    0.000s  (  0.000s elapsed)
    Total   time  192.517s  (204.831s elapsed)

After:

    89,073,483,552 bytes allocated in the heap
    20,134,704,256 bytes copied during GC
        13,426,968 bytes maximum residency (6623 sample(s))
           265,720 bytes maximum slop
                38 MB total memory in use (0 MB lost due to fragmentation)

                                       Tot time (elapsed)  Avg pause  Max pause
    Gen  0     165191 colls,     0 par   34.872s  35.319s     0.0002s    0.0111s
    Gen  1      6623 colls,     0 par   17.515s  17.831s     0.0027s    0.0509s

    TASKS: 173871 (173867 bound, 4 peak workers (4 total), using -N1)

    SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

    INIT    time    0.001s  (  0.001s elapsed)
    MUT     time  104.495s  (113.498s elapsed)
    GC      time   52.387s  ( 53.150s elapsed)
    EXIT    time    0.001s  (  0.001s elapsed)
    Total   time  156.991s  (166.650s elapsed)

Closes #168

dejafu-tests/Cases/Properties.hs

@@ -12,6 +12,8 @@ import qualified Data.Map as M
 import Data.Maybe (fromJust, isJust)
 import Data.Proxy (Proxy(..))
 import qualified Data.Sequence as S
+import Data.Set (Set)
+import qualified Data.Set as Set
 import Test.DejaFu.Types (ThreadAction, Lookahead)
 import qualified Test.DejaFu.Types as D
 import qualified Test.DejaFu.Internal as D
@@ -248,11 +250,14 @@ instance Listable D.ActionType where
     \/ cons0 D.SynchronisedOther
 
 instance Listable SCT.DepState where
-  tiers = mapT (uncurry SCT.DepState) (tiers >< tiers)
+  tiers = mapT (\(a,(b,c)) -> SCT.DepState a b c) (tiers >< tiers >< tiers)
 
 instance (Ord k, Listable k, Listable v) => Listable (Map k v) where
   tiers = mapT M.fromList tiers
 
+instance (Ord v, Listable v) => Listable (Set v) where
+  tiers = mapT Set.fromList tiers
+
 instance Listable D.Failure where
   list =
     [ D.InternalError

dejafu/CHANGELOG.markdown

@@ -104,6 +104,11 @@ This project is versioned according to the [Package Versioning Policy](https://p
 
 - This is now an internal module. (#155)
 
+### Performance
+
+- Significant resident memory reduction for most passing tests.
+- Improved dependency detection for `MVar` actions, leading to fewer executions.
+
 ### Miscellaneous
 
 - The minimum supported version of concurrency is now 1.3.0.0.

dejafu/Test/DejaFu/SCT/Internal/DPOR.hs

@@ -632,6 +632,12 @@ dependentActions ds a1 a2 = case (a1, a2) of
   (PartiallySynchronisedCommit _, _) | isBarrier a2 -> True
   (_, PartiallySynchronisedCommit _) | isBarrier a1 -> True
 
+  -- Two @MVar@ puts are dependent if they're to the same empty
+  -- @MVar@, and two takes are dependent if they're to the same full
+  -- @MVar@.
+  (SynchronisedWrite v1, SynchronisedWrite v2) -> v1 == v2 && not (isFull ds v1)
+  (SynchronisedRead  v1, SynchronisedRead  v2) -> v1 == v2 && isFull ds v1
+
   (_, _) -> case getSame crefOf of
     -- Two actions on the same CRef where at least one is synchronised
     Just r -> synchronises a1 r || synchronises a2 r
@@ -654,6 +660,8 @@ dependentActions ds a1 a2 = case (a1, a2) of
 data DepState = DepState
   { depCRState :: Map CRefId Bool
   -- ^ Keep track of which @CRef@s have buffered writes.
+  , depMVState :: Set MVarId
+  -- ^ Keep track of which @MVar@s are full.
   , depMaskState :: Map ThreadId MaskingState
   -- ^ Keep track of thread masking states. If a thread isn't present,
   -- the masking state is assumed to be @Unmasked@. This nicely
@@ -663,22 +671,24 @@ data DepState = DepState
 
 instance NFData DepState where
   rnf depstate = rnf ( depCRState depstate
+                     , depMVState depstate
                      , [(t, m `seq` ()) | (t, m) <- M.toList (depMaskState depstate)]
                      )
 
 -- | Initial dependency state.
 initialDepState :: DepState
-initialDepState = DepState M.empty M.empty
+initialDepState = DepState M.empty S.empty M.empty
 
--- | Update the 'CRef' buffer state with the action that has just
+-- | Update the dependency state with the action that has just
 -- happened.
 updateDepState :: DepState -> ThreadId -> ThreadAction -> DepState
 updateDepState depstate tid act = DepState
   { depCRState   = updateCRState       act $ depCRState   depstate
+  , depMVState   = updateMVState       act $ depMVState   depstate
   , depMaskState = updateMaskState tid act $ depMaskState depstate
   }
 
--- | Update the 'CRef' buffer state with the action that has just
+-- | Update the @CRef@ buffer state with the action that has just
 -- happened.
 updateCRState :: ThreadAction -> Map CRefId Bool -> Map CRefId Bool
 updateCRState (CommitCRef _ r) = M.delete r
@@ -687,6 +697,15 @@ updateCRState ta
   | isBarrier $ simplifyAction ta = const M.empty
   | otherwise = id
 
+-- | Update the @MVar@ full/empty state with the action that has just
+-- happened.
+updateMVState :: ThreadAction -> Set MVarId -> Set MVarId
+updateMVState (PutMVar mvid _) = S.insert mvid
+updateMVState (TryPutMVar mvid True _) = S.insert mvid
+updateMVState (TakeMVar mvid _) = S.delete mvid
+updateMVState (TryTakeMVar mvid True _) = S.delete mvid
+updateMVState _ = id
+
 -- | Update the thread masking state with the action that has just
 -- happened.
 updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState
@@ -698,10 +717,14 @@ updateMaskState tid (SetMasking   _ ms) = M.insert tid ms
 updateMaskState tid (ResetMasking _ ms) = M.insert tid ms
 updateMaskState _ _ = id
 
--- | Check if a 'CRef' has a buffered write pending.
+-- | Check if a @CRef@ has a buffered write pending.
 isBuffered :: DepState -> CRefId -> Bool
 isBuffered depstate r = M.findWithDefault False r (depCRState depstate)
 
+-- | Check if an @MVar@ is full.
+isFull :: DepState -> MVarId -> Bool
+isFull depstate v = S.member v (depMVState depstate)
+
 -- | Check if an exception can interrupt a thread (action).
 canInterrupt :: DepState -> ThreadId -> ThreadAction -> Bool
 canInterrupt depstate tid act