diff --git a/README.markdown b/README.markdown index 02d2430..df29801 100644 --- a/README.markdown +++ b/README.markdown @@ -46,7 +46,7 @@ There are a few different packages under the Déjà Fu umbrella: | | Version | Summary | | - | ------- | ------- | | [concurrency][h:conc] | 1.4.0.1 | Typeclasses, functions, and data types for concurrency and STM. | -| [dejafu][h:dejafu] | 1.3.0.1 | Systematic testing for Haskell concurrency. | +| [dejafu][h:dejafu] | 1.3.0.2 | Systematic testing for Haskell concurrency. | | [hunit-dejafu][h:hunit] | 1.1.0.1 | Deja Fu support for the HUnit test framework. | | [tasty-dejafu][h:tasty] | 1.1.0.1 | Deja Fu support for the Tasty test framework. | diff --git a/dejafu-tests/lib/Integration/Regressions.hs b/dejafu-tests/lib/Integration/Regressions.hs index 96a2a8c..d6886fd 100644 --- a/dejafu-tests/lib/Integration/Regressions.hs +++ b/dejafu-tests/lib/Integration/Regressions.hs @@ -65,4 +65,10 @@ tests = toTestList t <- mask $ \restore -> fork (try (restore (act s)) >> pure ()) killThread t tryReadMVar s + + , djfu "https://github.com/barrucadu/dejafu/issues/243" (gives' [1,2,3]) $ do + setNumCapabilities 1 + _ <- fork (setNumCapabilities 2) + _ <- fork (setNumCapabilities 3) + getNumCapabilities ] diff --git a/dejafu/CHANGELOG.rst b/dejafu/CHANGELOG.rst index a631723..5830e5d 100644 --- a/dejafu/CHANGELOG.rst +++ b/dejafu/CHANGELOG.rst @@ -6,6 +6,19 @@ standard Haskell versioning scheme. .. _PVP: https://pvp.haskell.org/ +1.3.0.2 (2018-03-11) +-------------------- + +* Git: :tag:`dejafu-1.3.0.2` +* Hackage: :hackage:`dejafu-1.3.0.2` + +Fixed +~~~~~ + +* (:pull:`244`) Add missing dependency for ``setNumCapabilities`` + actions. + + 1.3.0.1 (2018-03-08) -------------------- diff --git a/dejafu/Test/DejaFu/SCT/Internal/DPOR.hs b/dejafu/Test/DejaFu/SCT/Internal/DPOR.hs index 8f648a5..03aa851 100644 --- a/dejafu/Test/DejaFu/SCT/Internal/DPOR.hs +++ b/dejafu/Test/DejaFu/SCT/Internal/DPOR.hs @@ -634,20 +634,18 @@ dependent' ds t1 a1 t2 l2 = case (a1, l2) of -- thread and if the actions can be interrupted. We can also -- slightly improve on that by not considering interrupting the -- normal termination of a thread: it doesn't make a difference. - (ThrowTo t, WillStop) | t == t2 -> False - (Stop, WillThrowTo t) | t == t1 -> False - (ThrowTo t, _) | t == t2 -> canInterruptL ds t2 l2 - (_, WillThrowTo t) | t == t1 -> canInterrupt ds t1 a1 + (ThrowTo t, _) | t == t2 -> canInterruptL ds t2 l2 && l2 /= WillStop + (_, WillThrowTo t) | t == t1 -> canInterrupt ds t1 a1 && a1 /= Stop -- Another worst-case: assume all STM is dependent. (STM _ _, WillSTM) -> True (BlockedSTM _, WillSTM) -> True - -- This is a bit pessimistic: Set/Get are only dependent if the - -- value set is not the same as the value that will be got, but we - -- can't know that here. 'dependent' optimises this case. + -- the number of capabilities is essentially a global shared + -- variable (GetNumCapabilities _, WillSetNumCapabilities _) -> True (SetNumCapabilities _, WillGetNumCapabilities) -> True + (SetNumCapabilities _, WillSetNumCapabilities _) -> True _ -> dependentActions ds (simplifyAction a1) (simplifyLookahead l2) @@ -656,56 +654,37 @@ dependent' ds t1 a1 t2 l2 = case (a1, l2) of -- being so great an over-approximation as to be useless! dependentActions :: DepState -> ActionType -> ActionType -> Bool dependentActions ds a1 a2 = case (a1, a2) of - -- Unsynchronised reads and writes are always dependent, even under - -- a relaxed memory model, as an unsynchronised write gives rise to - -- a commit, which synchronises. - (UnsynchronisedRead r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> a2 /= UnsynchronisedRead r1 - (UnsynchronisedWrite r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True - (PartiallySynchronisedWrite r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True - (PartiallySynchronisedModify r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True - (SynchronisedModify r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True + (UnsynchronisedRead _, UnsynchronisedRead _) -> False -- Unsynchronised writes and synchronisation where the buffer is not -- empty. -- -- See [RMMVerification], lemma 5.25. - (UnsynchronisedWrite r1, PartiallySynchronisedCommit _) | same crefOf && isBuffered ds r1 -> False - (PartiallySynchronisedCommit _, UnsynchronisedWrite r2) | same crefOf && isBuffered ds r2 -> False + (UnsynchronisedWrite r1, PartiallySynchronisedCommit r2) | r1 == r2 && isBuffered ds r1 -> False + (PartiallySynchronisedCommit r1, UnsynchronisedWrite r2) | r1 == r2 && isBuffered ds r1 -> False -- Unsynchronised reads where a memory barrier would flush a -- buffered write - (UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered ds r1 - (_, UnsynchronisedRead r2) | isBarrier a1 -> isBuffered ds r2 + (UnsynchronisedRead r1, _) | isBarrier a2 && isBuffered ds r1 -> True + (_, UnsynchronisedRead r2) | isBarrier a1 && isBuffered ds r2 -> True -- Commits and memory barriers must be dependent, as memory barriers -- (currently) flush in a consistent order. Alternative orders need -- to be explored as well. Perhaps a better implementation of -- memory barriers would just block every non-commit thread while -- any buffer is nonempty. - (PartiallySynchronisedCommit _, _) | isBarrier a2 -> True - (_, PartiallySynchronisedCommit _) | isBarrier a1 -> True + (PartiallySynchronisedCommit r1, _) | synchronises a2 r1 -> True + (_, PartiallySynchronisedCommit r2) | synchronises a1 r2 -> 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 + (SynchronisedWrite v1, SynchronisedWrite v2) | v1 == v2 -> not (isFull ds v1) + (SynchronisedRead v1, SynchronisedRead v2) | v1 == v2 -> isFull ds v1 + (SynchronisedWrite v1, SynchronisedRead v2) | v1 == v2 -> True + (SynchronisedRead v1, SynchronisedWrite v2) | v1 == v2 -> True - (_, _) -> case getSame crefOf of - -- Two actions on the same CRef where at least one is synchronised - Just r -> synchronises a1 r || synchronises a2 r - -- Two actions on the same MVar - _ -> same mvarOf - - where - same :: Eq a => (ActionType -> Maybe a) -> Bool - same = isJust . getSame - - getSame :: Eq a => (ActionType -> Maybe a) -> Maybe a - getSame f = - let f1 = f a1 - f2 = f a2 - in if f1 == f2 then f1 else Nothing + (_, _) -> maybe False (\r -> Just r == crefOf a2) (crefOf a1) ------------------------------------------------------------------------------- -- ** Dependency function state diff --git a/dejafu/dejafu.cabal b/dejafu/dejafu.cabal index bce590f..f2fee9c 100755 --- a/dejafu/dejafu.cabal +++ b/dejafu/dejafu.cabal @@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: dejafu -version: 1.3.0.1 +version: 1.3.0.2 synopsis: A library for unit-testing concurrent programs. description: @@ -33,7 +33,7 @@ source-repository head source-repository this type: git location: https://github.com/barrucadu/dejafu.git - tag: dejafu-1.3.0.1 + tag: dejafu-1.3.0.2 library exposed-modules: Test.DejaFu diff --git a/doc/getting_started.rst b/doc/getting_started.rst index ccb55f5..0f23022 100644 --- a/doc/getting_started.rst +++ b/doc/getting_started.rst @@ -28,7 +28,7 @@ There are a few different packages under the Déjà Fu umbrella: :header: "Package", "Version", "Summary" ":hackage:`concurrency`", "1.4.0.1", "Typeclasses, functions, and data types for concurrency and STM" - ":hackage:`dejafu`", "1.3.0.1", "Systematic testing for Haskell concurrency" + ":hackage:`dejafu`", "1.3.0.2", "Systematic testing for Haskell concurrency" ":hackage:`hunit-dejafu`", "1.1.0.1", "Déjà Fu support for the HUnit test framework" ":hackage:`tasty-dejafu`", "1.1.0.1", "Déjà Fu support for the tasty test framework"