-
Notifications
You must be signed in to change notification settings - Fork 19
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
readMVars are dependent! #169
Comments
The obvious solution to this made matters worse, somehow. Before
After
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Whoops!
As reads and takes both get turned into
SynchronisedRead
, they're not distinguished bydependentActions
. Need to either add a new constructor toActionType
, or add a flag toSynchronisedRead
indicating whether it is a take or not.The text was updated successfully, but these errors were encountered: