search

barrucadu / dejafu

Systematic concurrency testing meets Haskell.
https://dejafu.docs.barrucadu.co.uk/
191 stars 18 forks source link

readMVars are dependent! #169

Open barrucadu opened 6 years ago

barrucadu commented 6 years ago

Whoops!

As reads and takes both get turned into SynchronisedRead, they're not distinguished by dependentActions. Need to either add a new constructor to ActionType, or add a flag to SynchronisedRead indicating whether it is a take or not.

barrucadu commented 6 years ago

The obvious solution to this made matters worse, somehow.

Before

  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)

After

  89,071,723,912 bytes allocated in the heap
  20,120,870,472 bytes copied during GC
      13,571,040 bytes maximum residency (6650 sample(s))
         269,832 bytes maximum slop
              38 MB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0     165159 colls,     0 par   38.235s  38.741s     0.0002s    0.0200s
  Gen  1      6650 colls,     0 par   19.640s  19.978s     0.0030s    0.0654s

  TASKS: 173994 (173990 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  115.246s  (126.947s elapsed)
  GC      time   57.875s  ( 58.719s elapsed)
  EXIT    time    0.001s  (  0.001s elapsed)
  Total   time  173.225s  (185.667s elapsed)

Diff

diff --git a/dejafu-tests/Cases/Properties.hs b/dejafu-tests/Cases/Properties.hs
index 3988cff..2bad02d 100644
--- a/dejafu-tests/Cases/Properties.hs
+++ b/dejafu-tests/Cases/Properties.hs
@@ -246,6 +246,7 @@ instance Listable D.ActionType where
     \/ cons1 D.PartiallySynchronisedModify
     \/ cons1 D.SynchronisedModify
     \/ cons1 D.SynchronisedRead
+    \/ cons1 D.SynchronisedTake
     \/ cons1 D.SynchronisedWrite
     \/ cons0 D.SynchronisedOther

diff --git a/dejafu-tests/dejafu-tests.cabal b/dejafu-tests/dejafu-tests.cabal
index 4fbc6f6..1887264 100644
--- a/dejafu-tests/dejafu-tests.cabal
+++ b/dejafu-tests/dejafu-tests.cabal
@@ -59,4 +59,4 @@ executable dejafu-tests
     build-depends: transformers
   -- hs-source-dirs:      
   default-language:    Haskell2010
-  ghc-options: -threaded
+  ghc-options: -threaded -rtsopts
diff --git a/dejafu/Test/DejaFu/Internal.hs b/dejafu/Test/DejaFu/Internal.hs
index a9ed2bc..4fd27bb 100644
--- a/dejafu/Test/DejaFu/Internal.hs
+++ b/dejafu/Test/DejaFu/Internal.hs
@@ -206,7 +206,9 @@ data ActionType =
   | SynchronisedModify  CRefId
   -- ^ An 'atomicModifyCRef'.
   | SynchronisedRead    MVarId
-  -- ^ A 'readMVar' or 'takeMVar' (or @try@/@blocked@ variants).
+  -- ^ A 'readMVar' (or @try@/@blocked@ variants).
+  | SynchronisedTake    MVarId
+  -- ^ A 'takeMVar' (or @try@/@blocked@ variants).
   | SynchronisedWrite   MVarId
   -- ^ A 'putMVar' (or @try@/@blocked@ variant).
   | SynchronisedOther
@@ -222,6 +224,7 @@ instance NFData ActionType where
   rnf (PartiallySynchronisedModify c) = rnf c
   rnf (SynchronisedModify c) = rnf c
   rnf (SynchronisedRead m) = rnf m
+  rnf (SynchronisedTake m) = rnf m
   rnf (SynchronisedWrite m) = rnf m
   rnf a = a `seq` ()

@@ -229,6 +232,7 @@ instance NFData ActionType where
 isBarrier :: ActionType -> Bool
 isBarrier (SynchronisedModify _) = True
 isBarrier (SynchronisedRead   _) = True
+isBarrier (SynchronisedTake   _) = True
 isBarrier (SynchronisedWrite  _) = True
 isBarrier SynchronisedOther = True
 isBarrier _ = False
@@ -257,6 +261,7 @@ crefOf _ = Nothing
 -- | Get the 'MVar' affected.
 mvarOf :: ActionType -> Maybe MVarId
 mvarOf (SynchronisedRead  c) = Just c
+mvarOf (SynchronisedTake  c) = Just c
 mvarOf (SynchronisedWrite c) = Just c
 mvarOf _ = Nothing

@@ -274,8 +279,8 @@ simplifyLookahead (WillPutMVar c)     = SynchronisedWrite c
 simplifyLookahead (WillTryPutMVar c)  = SynchronisedWrite c
 simplifyLookahead (WillReadMVar c)    = SynchronisedRead c
 simplifyLookahead (WillTryReadMVar c) = SynchronisedRead c
-simplifyLookahead (WillTakeMVar c)    = SynchronisedRead c
-simplifyLookahead (WillTryTakeMVar c)  = SynchronisedRead c
+simplifyLookahead (WillTakeMVar c)    = SynchronisedTake c
+simplifyLookahead (WillTryTakeMVar c)  = SynchronisedTake c
 simplifyLookahead (WillReadCRef r)     = UnsynchronisedRead r
 simplifyLookahead (WillReadCRefCas r)  = UnsynchronisedRead r
 simplifyLookahead (WillModCRef r)      = SynchronisedModify r
diff --git a/dejafu/Test/DejaFu/SCT/Internal/DPOR.hs b/dejafu/Test/DejaFu/SCT/Internal/DPOR.hs
index b103bd0..779c641 100644
--- a/dejafu/Test/DejaFu/SCT/Internal/DPOR.hs
+++ b/dejafu/Test/DejaFu/SCT/Internal/DPOR.hs
@@ -636,7 +636,10 @@ dependentActions ds a1 a2 = case (a1, a2) of
   -- @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
+  (SynchronisedTake  v1, SynchronisedTake  v2) -> v1 == v2 && isFull ds v1
+
+  -- Two @MVar@ reads are never dependent
+  (SynchronisedRead _, SynchronisedRead _) -> False

   (_, _) -> case getSame crefOf of
     -- Two actions on the same CRef where at least one is synchronised