dejafu 1.0.0.1 → 1.0.0.2
raw patch · 10 files changed
+1240/−1134 lines, 10 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Test.DejaFu.Internal: ehead :: String -> [a] -> a
+ Test.DejaFu.Internal: eadjust :: (Ord k, Show k) => String -> (v -> v) -> k -> Map k v -> Map k v
+ Test.DejaFu.Internal: einsert :: (Ord k, Show k) => String -> k -> v -> Map k v -> Map k v
+ Test.DejaFu.Internal: elookup :: (Ord k, Show k) => String -> k -> Map k v -> v
+ Test.DejaFu.SCT.Internal.DPOR: independent :: DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool
+ Test.DejaFu.SCT.Internal.DPOR: validateDPOR :: String -> DPOR -> DPOR
Files
- CHANGELOG.markdown +0/−934
- CHANGELOG.rst +925/−0
- Test/DejaFu.hs +169/−121
- Test/DejaFu/Conc/Internal.hs +3/−3
- Test/DejaFu/Conc/Internal/Memory.hs +5/−2
- Test/DejaFu/Conc/Internal/Threading.hs +25/−30
- Test/DejaFu/Internal.hs +22/−6
- Test/DejaFu/Refinement.hs +17/−12
- Test/DejaFu/SCT/Internal/DPOR.hs +71/−23
- dejafu.cabal +3/−3
− CHANGELOG.markdown
@@ -1,934 +0,0 @@-Release Notes-=============--All notable changes to this project will be documented in this file.--This project is versioned according to the [Package Versioning Policy](https://pvp.haskell.org), the-*de facto* standard Haskell versioning scheme.---1.0.0.1----------- **Date** 2017-01-19-- **Git tag** [dejafu-1.0.0.1][]-- **Hackage** https://hackage.haskell.org/package/dejafu-1.0.0.1--### Miscellaneous--- The upper bound on concurrency was bumped to <1.5.--[dejafu-1.0.0.1]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-1.0.0.1---------------------------------------------------------------------------------------------------------1.0.0.0----------- **Date** 2017-12-23-- **Git tag** [dejafu-1.0.0.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-1.0.0.0--### Test.DejaFu--- All testing functions now require a `MonadConc`, `MonadRef`, and `MonadIO` constraint:-- It is no longer possible to test things in `ST`.--- All testing functions now take the action to test as the last parameter.--- The `autocheckIO`, `dejafuIO`, `dejafusIO`, `autocheckWayIO`, `dejafuWayIO`, `dejafusWayIO`,- `dejafuDiscardIO`, `runTestM`, and `runTestWayM` functions are now gone.--- The `Predicate` type has been replaced with a more general `ProPredicate` type which is a- profunctor and (b) can discard results not needed to determine if the predicate passes. (#124)-- All testing functions have been generalised to take a `ProPredicate` instead. The `Predicate a`- type remains as an alias for `ProPredicate a a`. Passing tests have their resident memory usage- significantly decreased.--- The `Result` type no longer includes a number of cases checked, as this is not meaningful with- predicates including discard functions.--- New `alwaysNothing` and `somewhereNothing` functions, like `alwaysTrue` and `somewhereTrue`, to- lift functions to `ProPredicate`s.--- The `alwaysTrue2` function is gone, as its behaviour was unintuitive and easy to get wrong, and- has been replaced with new `alwaysSameOn` and `alwaysSameBy` predicates, which generalise- `alwaysSame`.--- The `alwaysSame`, `alwaysSameOn`, and `alwaysSameBy` predicates now gives the simplest execution- trace leading to each distinct result.--### Test.DejaFu.Common--- This module has been split up into new Test.DejaFu.Internal, Types, and Utils modules. (#155)--- New `ForkOS` and `IsCurrentThreadBound` thread actions. (#126)--- New `WillForkOS` and `WillIsCurrentThreadBound` lookaheads. (#126)--- The `TTrace` type synonym for `[TAction]` has been removed.--- The `preEmpCount` function has been removed.--- New functions `strengthenDiscard` and `weakenDiscard` to combine discard functions.--- The `Discard` type is now defined here and re-exported from Test.DejaFu.SCT.--- The `ThreadId`, `CRefId`, `MVarId`, and `TVarId` types are now newtypes over a common `Id`- type. (#137)--### Test.DejaFu.Conc--- The `ConcST` type alias is gone.--- The `MonadBase IO ConcIO` instance is gone.--- The `MonadIO ConcIO` instance is replaces with a more general `MonadIO n => MonadIO (ConcT r n)`- instance.--- The `runConcurrent` function now has a `MonadConc` constraint.--- If bound threads are supported, the main thread when testing is bound. (#126)--- Each entry in an execution trace is now in the form `(decision, alternatives, action)`. The- chosen thread is no longer in the list of alternatives, which makes raw traces easier to- read. (#121)--- Due to changes in Test.DejaFu.Schedule, no longer re-exports `Decision`, `NonEmpty`, `tidOf`, or- `decisionOf`.--### Test.DejaFu.Refinement--- A blocking interference function is no longer reported as a deadlocking execution.--### Test.DejaFu.Schedule--- No longer re-exports `Decision` or `NonEmpty`.--- The `tidOf` and `decisionOf` functions have moved to Test.DejaFu.Utils.--### Test.DejaFu.SCT--- All testing functions now require a `MonadConc` constraint:-- It is no longer possible to test things in `ST`.--### Test.DejaFu.STM--- 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-1.0.0.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-1.0.0.0---------------------------------------------------------------------------------------------------------0.9.1.2----------- **Date** 2017-12-12-- **Git tag** [dejafu-0.9.1.2][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.9.1.2--### Miscellaneous--- The upper bound on leancheck was bumped to <0.8.--[dejafu-0.9.1.2]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.9.1.2---------------------------------------------------------------------------------------------------------0.9.1.1----------- **Date** 2017-12-08-- **Git tag** [dejafu-0.9.1.1][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.9.1.1--### Miscellaneous--- Fix an issue where nested masks nested inside unmasks would sometimes not be pre-empted in- systematic testing.--[dejafu-0.9.1.1]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.9.1.1---------------------------------------------------------------------------------------------------------0.9.1.0----------- **Date** 2017-11-26-- **Git tag** [dejafu-0.9.1.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.9.1.0--### Test.DejaFu.Common--- Fix some incorrect "@since" haddock comments.-- Pretty-printed traces now display a pre-emption following a yield with a little "p".--### Test.DejaFu.Conc--- Add a missing `MonadFail` instance.--### Test.DejaFu.STM--- Add a missing `MonadFail` instance.--[dejafu-0.9.1.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.9.1.0---------------------------------------------------------------------------------------------------------0.9.0.3----------- **Date** 2017-11-06-- **Git tag** [dejafu-0.9.0.3][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.9.0.3--### Miscellaneous--- Impose a dependency between commits and memory barriers, to make barriers sound (#138).--[dejafu-0.9.0.3]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.9.0.3---------------------------------------------------------------------------------------------------------0.9.0.2----------- **Date** 2017-11-02-- **Git tag** [dejafu-0.9.0.2][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.9.0.2--### Miscellaneous--- Small improvement to dependency detection of STM transactions.-- A fair bound of 0 will now prevent all yields.--[dejafu-0.9.0.2]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.9.0.2---------------------------------------------------------------------------------------------------------0.9.0.1----------- **Date** 2017-10-28-- **Git tag** [dejafu-0.9.0.1][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.9.0.1--### Miscellaneous--- Fixed an issue where tests with exception handlers would sometimes skip over nested handlers or- try to take the tail of an empty list (#139 and #141).--[dejafu-0.9.0.1]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.9.0.1---------------------------------------------------------------------------------------------------------0.9.0.0----------- **Date** 2017-10-11-- **Git tag** [dejafu-0.9.0.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.9.0.0--### Test.DejaFu.Common--- New `isInternalError`, `isAbort`, `isDeadlock`, `isUncaughtException`, and- `isIllegalSubconcurrency` functions for matching failure types. Also exported from Test.DejaFu.--- The `UncaughtException` `Failure` constructor now includes the exception.-- The `Read`, `Enum`, and `Bounded` instances are gone. The `Eq`, `Ord`, and `NFData` instances- use the `show` of the exception. Pretty-printed failures include the exception text.--- New `ThreadDelay` and `WillThreadDelay` constructors in `ThreadAction` and `Lookahead`. Uses of- `threadDelay` are no longer reported as a use of `yield`.--[dejafu-0.9.0.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.9.0.0---------------------------------------------------------------------------------------------------------0.8.0.0----------- **Date** 2017-09-26-- **Git tag** [dejafu-0.8.0.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.8.0.0--### Test.DejaFu.Common--- Execution traces now only include a single item of lookahead (#120).-- STM traces now include IDs of created `TVar`s (#80).--### Test.DejaFu.Schedule--- Schedulers no longer take the execution trace so far (#106).-- The `Scheduler` type is now a newtype (#122).--[dejafu-0.8.0.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.8.0.0---------------------------------------------------------------------------------------------------------0.7.3.0----------- **Date** 2017-09-26-- **Git tag** [dejafu-0.7.3.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.7.3.0--### Test.DejaFu.Common--- A new function `threadNames`, to get all named threads from a trace.--### Miscellaneous--- Escaping a mask by raising an exception now correctly restores the masking state (#118).-- Named threads which are only started by a pre-emption now show up in the trace (#101).--[dejafu-0.7.3.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.7.3.0---------------------------------------------------------------------------------------------------------0.7.2.0----------- **Date** 2017-09-16-- **Git tag** [dejafu-0.7.2.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.7.2.0--### Test.DejaFu.STM--- The `STM n r` monad now has `Alternative` and `MonadPlus` instances, using `orElse` for the binary- operation and `retry` for the unit.--### Miscellaneous--- The `Eq` instance for `ThreadId`, `CRefId`, `MVarId`, and `TVarId` now only compares the numbers,- not the names.-- This makes it consistent with the `Ord` instances, and is also a small performance gain.--- Now compatible with concurrency-1.2.0.0.--[dejafu-0.7.2.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.7.2.0---------------------------------------------------------------------------------------------------------0.7.1.3----------- **Date** 2017-09-08-- **Git tag** [dejafu-0.7.1.3][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.7.1.3--### Miscellaneous--- Aborted STM transactions are now rolled back correctly (issue #111).-- Slightly improved run-time of systematic testing.--[dejafu-0.7.1.3]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.7.1.3---------------------------------------------------------------------------------------------------------0.7.1.2----------- **Date** 2017-08-21-- **Git tag** [dejafu-0.7.1.2][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.7.1.2--### Miscellaneous--- Errors thrown with `Control.Monad.fail` no longer terminate testing, and are now correctly treated- as asynchronous exceptions.--[dejafu-0.7.1.2]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.7.1.2---------------------------------------------------------------------------------------------------------0.7.1.1----------- **Date** 2017-08-16-- **Git tag** [dejafu-0.7.1.1][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.7.1.1--### Miscellaneous--- Significantly reduced memory usage in systematic testing when discarding traces.-- Previously this was `O(max trace length * number of executions)`-- Now it's `O(max trace length + total size of traces kept)`--[dejafu-0.7.1.1]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.7.1.1---------------------------------------------------------------------------------------------------------0.7.1.0----------- **Date** 2017-08-10-- **Git tag** [dejafu-0.7.1.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.7.1.0--### Test.DejaFu--- Exposed the new SCT discard functions through `dejafuDiscard` and `dejafuDiscardIO`.-- There are no `dejafusDiscard` and `dejafusDiscardIO` functions because this would probably be- confusing, as the traces are shared.--- The `Discard` type and `defaultDiscard` function are also exposed.--### Test.DejaFu.Defaults--- Added a new `defaultDiscarder` function, which discards nothing.--### Test.DejaFu.SCT--- Added new SCT functions to selectively discard results or traces, which can be a significant- memory saving if you know what sorts of results you are interested in:- - New type: `Discard`.- - New functions: `runSCTDiscard`, `resultsSetDiscard`, `sctBoundDiscard`,- `sctUniformRandomDiscard`, and `sctWeightedRandomDiscard`.- - `resultsSet` and `resultsSet'` now discard traces as they are produced, rather than all at the- end, greatly improving performance when traces are large.--[dejafu-0.7.1.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.7.1.0---------------------------------------------------------------------------------------------------------0.7.0.2----------- **Date** 2017-06-12-- **Git tag** [dejafu-0.7.0.2][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.7.0.2--### Test.DejaFu.Refinement--- Removed unnecessary typeclass constraints from `check`, `check'`, `checkFor`, and- `counterExamples`.--### Miscellaneous--- Removed an unnecessary dependency on [monad-loops][].--[monad-loops]: https://hackage.haskell.org/package/monad-loops-[dejafu-0.7.0.2]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.7.0.2---------------------------------------------------------------------------------------------------------0.7.0.1----------- **Date** 2017-06-09-- **Git tag** [dejafu-0.7.0.1][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.7.0.1--### Test.DejaFu.Refinement--- `check`, `check'`, and `checkFor` are now faster if there are multiple counterexamples.-- The above and `counterExamples` are now faster even if there is only a single counterexample in- some cases.--[dejafu-0.7.0.1]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.7.0.1---------------------------------------------------------------------------------------------------------0.7.0.0----------- **Date** 2017-06-07-- **Git tag** [dejafu-0.7.0.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.7.0.0--### Test.DejaFu--- The new Test.DejaFu.Defaults and Test.DejaFu.Refinement modules are re-exported.-- The new smart constructors from Test.DejaFu.SCT are exported.--### Test.DejaFu.Defaults--- The `default*` values are now defined in the new Test.DejaFu.Defaults module. There is no breaking- API change as they are re-exported from Test.DejaFu.--### Test.DejaFu.Refinement--- A new module for checking observational properties of the side-effects of stateful, concurrent- functions.-- This is related to my work on [CoCo][], allowing dejafu to test what CoCo discovers.--### Test.DejaFu.SCT--- The `Way` type is now abstract and exposes smart constructor functions:- - `systematically`, corresponding to the old `Systematically`.- - `randomly`, corresponding to the old `Randomly`,- - `uniformly`, a new uniform random (as opposed to weighted random) scheduler.- - `swarmy`, corresponding to the old `Randomly` and specifying how many executions to use the- same weights for.-- A new `sctUniformRandom` function to do uniform (non-weighted) scheduling.-- The `sctRandom` function is now called `sctWeightedRandom` and can now re-use the same weights for- multiple executions.-- The `sctPreBound`, `sctFairBound`, and `sctLengthBound` functions have been removed.--### Fixed--- An issue where `subconcurrency` would re-use `MVar` IDs, leading to false reports of deadlock on- occasion (issue #81).--[CoCo]: https://github.com/barrucadu/coco-[dejafu-0.7.0.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.7.0.0---------------------------------------------------------------------------------------------------------0.6.0.0----------- **Date** 2017-04-08-- **Git tag** [dejafu-0.6.0.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.6.0.0--### Test.DejaFu.Conc--- The `Conc n r a` type is now `ConcT r n a`, and has been given a `MonadTrans` instance. Uses of- `lift` appear in the execution trace in the same way as `liftBase` and `liftIO`.- - The `ConcIO` and `ConcST` aliases have been updated, so this should be an invisible change to- most users.--### Test.DejaFu.SCT--- `Way` is now a GADT, no longer taking a type parameter. This greatly improves type inference when- the `Systematically` constructor is used.- - The `NFData` instance for `Way` is now gone. The alternative was requiring that any- `RandomGen` used also implement `NFData`, which is *very* restrictive--### Miscellaneous--- There is now a changelog.-- Test.DejaFu.Common is now considered to form part of the public API of the library.-- Every definition and instance now has a Haddock "@since" annotation.--[dejafu-0.6.0.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.6.0.0---------------------------------------------------------------------------------------------------------0.5.1.3----------- **Date** 2017-04-05-- **Git tag** [dejafu-0.5.1.3][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.5.1.3--### Miscellaneous--- The version range on the concurrency package has been changed to 1.1.*.--[dejafu-0.5.1.3]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.5.1.3---------------------------------------------------------------------------------------------------------0.5.1.2----------- **Date** 2017-03-04-- **Git tag** [dejafu-0.5.1.2][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.5.1.2--**This version was misnumbered! It should have caused a minor version bump!**--### Test.DejaFu.Conc--- New `MonadRef` and `MonadAtomicRef` instances for the `Conc` type using `CRef`.--### Fixed--- A long-standing bug where if the main thread is killed with a `throwTo`, the throwing neither- appears in the trace nor correctly terminates the execution.--### Miscellaneous--- The maximum supported version of the concurrency package has been changed to 1.1.1.*.--[dejafu-0.5.1.2]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.5.1.2---------------------------------------------------------------------------------------------------------0.5.1.1----------- **Date** 2017-02-25-- **Git tag** [dejafu-0.5.1.1][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.5.1.1--### Fixed--- The correct scheduler state is now passed to the scheduler immediately after the termination of a- `subconcurrency` action.-- SCT of subconcurrency no longer loops infinitely.--[dejafu-0.5.1.1]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.5.1.1---------------------------------------------------------------------------------------------------------0.5.1.0----------- **Date** 2017-02-25-- **Git tag** [dejafu-0.5.1.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.5.1.0--### Test.DejaFu--- A new `NFData` instance for `Result`.--### Test.DejaFu.Common--- New instances:- - `NFData` for `ThreadId`, `CRefId`, `MVarId`, `TVarId`, `IdSource`, `ThreadAction`,- `Lookahead`, `ActionType`, `TAction`, `Decision`, `Failure`, and `MemType`.- - `Eq`, `Ord`, and `Show` instances for `IdSource`.--### Test.DejaFu.SCT--- New `NFData` instances for `Way`, `Bounds`, `PreemptionBound`, `FairBound`, and `LengthBound`.-- New strict variants of `runSCT` and `resultsSet`: `runSCT'` and `resultsSet'`.--### Test.DejaFu.STM--- A new `NFData` instance for `Result`.--[dejafu-0.5.1.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.5.1.0---------------------------------------------------------------------------------------------------------0.5.0.2----------- **Date** 2017-02-22-- **Git tag** [dejafu-0.5.0.2][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.5.0.2--**This version was misnumbered! It should have caused a major version bump!**--### Test.DejaFu.Common--- A new `StopSubconcurrency` constructor of `ThreadAction`.--### Changed--- A `StopConcurrency` action appears in the execution trace immediately after the end of a- `subconcurrency` action (much like the `PopCatching` and `ResetMasking` actions which appear after- a catch and mask).-- A `subconcurrency` action now inherits the number of capabilities from the outer computation,- rather than being reset to 2 as before.--### Miscellaneous--- Test.DejaFu.SCT now compiles with MonoLocalBinds enabled (implied by GADTs and TypeFamilies),- which may be relevant to hackers.--[dejafu-0.5.0.2]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.5.0.2---------------------------------------------------------------------------------------------------------0.5.0.1----------- **Date** 2017-02-21-- **Git tag** [dejafu-0.5.0.1][]-- **This version was never pushed to hackage, whoops!**--### Fixed--- `readMVar` is once again considered a "release action" for the purposes of fair-bounding.--[dejafu-0.5.0.1]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.5.0.1---------------------------------------------------------------------------------------------------------0.5.0.0----------- **Date** 2017-02-21-- **Git tag** [dejafu-0.5.0.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.5.0.0--### Test.DejaFu--- All the functions which did take a `Bounds` now take a `Way` instead and support random scheduling- as well.--### Test.DejaFu.Common--- New `Eq` instances for `ThreadAction` and `Lookahead`.-- A `TryReadMVar` constructor for `ThreadAction` and a corresponding `WillTryReadMVar` constructor- for `Lookahead`.--### Test.DejaFu.Conc--- A new testing-only `subconcurrency` function, to run a concurrent action and do something with its- result in the same concurrent context, even if it fails.--### Test.DejaFu.SCT--- An `sctRandom` function to run a fixed number of randomly-scheduled executions of a program.-- The `Way` type, to abstract over how to run a concurrent program, used by new functions `runSCT`- and `resultsSet`.--### Fixed--- Some previously-missed `CRef` action dependencies are no longer missed.--### Miscellaneous--- The supported version of the concurrency package was bumped to 1.1.0.0, introducing `tryReadMVar`.-- A bunch of things were called "Var" or "Ref", these are now consistently "MVar" and "CRef".-- Significant performance improvements in both time and space.-- The dpor package has been merged back into this, as it turned out not to be very generally- useful. There is no direct replacement, but I have no intent to update it, so the dpor package is- now __deprecated__.--[dejafu-0.5.0.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.5.0.0---------------------------------------------------------------------------------------------------------0.4.0.0----------- **Date** 2016-09-10-- **Git tag** [dejafu-0.4.0.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.4.0.0--### Test.DejaFu--- The `autocheck'` function now takes the schedule bounds as a parameter.-- New `runTestM` and `runTestM'` functions, monad-polymorphic variants of the now-removed- `runTestIO` and `runTestIO'` functions.--### Test.DejaFu.Conc--- The `Conc` type no longer has the STM type as a parameter.-- A new `runConcurrent` function, a monad-polymorphic version of the now-removed `runConcST` and- `runConcIO` functions.--### Test.DejaFu.SCT--- The `ST`-specific functions are now monad-polymorphic.-- The `IO` function variants have been removed.--### Test.DejaFu.STM--- A new `runTransaction` function, a monad-polymorphic version of the now-removed `runTransactionST`- and `runTransactionIO` functions.--### Changed--- The termination of the main thread in execution traces now appears as a single `Stop`, rather than- the sequence `Lift, Stop`.-- Execution traces printed by the helpful functions in Test.DejaFu now include a key of thread- names.--### Miscellaneous--- Remodularisation:- - The Control.* modules have all been split out into a separate "concurrency" package.- - Many definitions from other modules have been moved to the new Test.DejaFu.Common module.- - The Test.DejaFu.Deterministic module has been renamed to Test.DejaFu.Conc--[dejafu-0.4.0.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.4.0.0---------------------------------------------------------------------------------------------------------0.3.2.1----------- **Date** 2016-07-21-- **Git tag** [dejafu-0.3.2.1][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.3.2.1--### Fixed--- The implementation of the STM `orElse` for `STMLike` incorrectly handled some state- non-associatively, leading to false deadlocks being reported in some cases.--[dejafu-0.3.2.1]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.3.2.1---------------------------------------------------------------------------------------------------------0.3.2.0----------- **Date** 2016-06-06-- **Git tag** [dejafu-0.3.2.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.3.2.0--**Builds with both dpor-0.1 and dpor-0.2, however some improvements require dpor-0.2.**--### Fixed--- (faster with dpor-0.2) Executions missed due to daemon threads with uninteresting first actions- are no longer missed.--### Changed--- (requires dpor-0.2) Significantly improved dependency inference of exceptions, greatly improving- performance of testcases using exceptions.-- Significantly improved dependency inference of STM transactions, greatly improving performance of- testcases using STM.--[dejafu-0.3.2.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.3.2.0---------------------------------------------------------------------------------------------------------0.3.1.1----------- **Date** 2016-05-26-- **Git tag** [dejafu-0.3.1.1][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.3.1.1--### Miscellaneous--- Now supports GHC 8.--[dejafu-0.3.1.1]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.3.1.1---------------------------------------------------------------------------------------------------------0.3.1.0----------- **Date** 2016-05-02-- **Git tag** [dejafu-0.3.1.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.3.1.0--### Fixed--- Context switches around relaxed memory commit actions could cause the number of pre-emptions in an- execution to be miscounted, leading to the pre-emption bounding being too lenient.--[dejafu-0.3.1.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.3.1.0---------------------------------------------------------------------------------------------------------0.3.0.0----------- **Date** 2016-04-03-- **Git tag** [dejafu-0.3.0.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.3.0.0--**The minimum supported version of GHC is now 7.10.**--I didn't write proper release notes, and this is so far back I don't really care to dig through the-logs.--[dejafu-0.3.0.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.3.0.0---------------------------------------------------------------------------------------------------------0.2.0.0----------- **Date** 2015-12-01-- **Git tag** [0.2.0.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.2.0.0--I didn't write proper release notes, and this is so far back I don't really care to dig through the-logs.--[0.2.0.0]: https://github.com/barrucadu/dejafu/releases/tag/0.2.0.0---------------------------------------------------------------------------------------------------------0.1.0.0----------- **Date** 2015-08-27-- **Git tag** [0.1.0.0][]-- **Hackage** https://hackage.haskell.org/package/dejafu-0.1.0.0--Initial release. Go read the API docs.--[0.1.0.0]: https://github.com/barrucadu/dejafu/releases/tag/0.1.0.0
+ CHANGELOG.rst view
@@ -0,0 +1,925 @@+Release Notes+=============++This project is versioned according to the PVP_, the *de facto*+standard Haskell versioning scheme.++.. _PVP: https://pvp.haskell.org/+++1.0.0.2 (2017-02-18)+--------------------++* Git: :tag:`dejafu-1.0.0.2`+* Hackage: :hackage:`dejafu-1.0.0.2`++**Contributors:** :u:`qrilka` (:pull:`214`).++Changed+~~~~~~~++* (:issue:`193`) Deterministically assign commit thread IDs.++Fixed+~~~~~++* (:issue:`189`) Remove an incorrect optimisation in systematic+ testing for ``getNumCapabilities`` and ``setNumCapabilities``.++* (:issue:`204`) Fix missed interleavings in systematic testing with+ some uses of STM.++* (:issue:`205`) Fix ``forkOS`` being recorded in an execution trace+ as if it were a ``fork``.++Miscellaneous+~~~~~~~~~~~~~++* (:pull:`180`) Doctest Haddock examples in ``Test.DejaFu`` and+ ``Test.DejaFu.Refinement``.++* (:pull:`185`, :pull:`215`) Check some more internal invariants and+ throw on error.++* (:pull:`214`) Remove unnecessary use of ``head``.+++1.0.0.1 (2018-01-19)+--------------------++* Git: :tag:`dejafu-1.0.0.1`+* Hackage: :hackage:`dejafu-1.0.0.1`++Miscellaneous+~~~~~~~~~~~~~++* The upper bound on :hackage:`concurrency` is <1.5.+++1.0.0.0 - The API Friendliness Release (2017-12-23)+---------------------------------------------------++* Git: :tag:`dejafu-1.0.0.0`+* Hackage: :hackage:`dejafu-1.0.0.0`++Added+~~~~~++* ``Test.DejaFu.alwaysSameOn`` and ``alwaysSameBy`` predicate helpers.++* ``Test.DejaFu.SCT.strengthenDiscard`` and ``weakenDiscard``+ functions to combine discard functions.++* (:issue:`124`) The ``Test.DejaFu.ProPredicate`` type, which contains+ both an old-style ``Predicate`` and a discard function. It is also+ a ``Profunctor``, parameterised by the input and output types.++* (:issue:`124`) ``Test.DejaFu.alwaysNothing`` and+ ``somewhereNothing`` predicate helpers, like ``alwaysTrue`` and+ ``somewhereTrue``, to lift regular functions into a+ ``ProPredicate``.++* (:issue:`137`) The ``Test.DejaFu.Types.Id`` type.++* (:pull:`145`) Thread action and lookahead values for bound threads:++ * ``Test.DejaFu.Types.ForkOS``+ * ``Test.DejaFu.Types.IsCurrentThreadBound``+ * ``Test.DejaFu.Types.WillForkOS``+ * ``Test.DejaFu.Types.WillIsCurrentThreadBound``++* (:issue:`155`) ``Test.DejaFu.Types`` and ``Test.DejaFu.Utils``+ modules, each containing some of what was in ``Test.DejaFu.Common``.++Changed+~~~~~~~++* All testing functions require ``MonadConc``, ``MonadRef``, and+ ``MonadIO`` constraints. Testing with ``ST`` is no longer possible.++* The ``Test.DejaFu.alwaysSame`` predicate helper gives the simplest+ trace leading to each distinct result.++* The ``MonadIO Test.DejaFu.Conc.ConcIO`` instance is now the more+ general ``MonadIO n => MonadIO (ConcT r n)``.++* (:issue:`121`) The chosen thread is no longer redundantly included+ in trace lookahead.++* (:issue:`123`) All testing functions in ``Test.DejaFu`` take the+ action to run as the final parameter.++* (:issue:`124`) All testing functions in ``Test.DejaFu`` have been+ generalised to take a ``ProPredicate`` instead of a ``Predicate``.++* (:issue:`124`) The ``Test.DejaFu.Predicate`` type is an alias for+ ``ProPredicate a a``.++* (:issue:`124`) The ``Test.DejaFu.Result`` type no longer includes a+ number of cases checked.++* (:issue:`137`) The ``Test.DejaFu.Types.ThreadId``, ``CRefId``,+ ``MVarId``, and ``TVarId`` types are now wrappers for an ``Id``.++* (:pull:`145`) If built with the threaded runtime, the main thread in+ a test is executed as a bound thread.++* (:issue:`155`) The ``Test.DejaFu.SCT.Discard`` type is defined in+ ``Test.DejaFu.Types``, and re-exported from ``Test.DejaFu.SCT``.++* (:issue:`155`) The ``Test.DejaFu.Schedule.tidOf`` and ``decisionOf``+ functions are defined in ``Test.DejaFu.Utils``, but not re-exported+ from ``Test.DejaFu.Schedule``.++Removed+~~~~~~~++* The ``IO`` specific testing functions:++ * ``Test.DejaFu.autocheckIO``+ * ``Test.DejaFu.dejafuIO``+ * ``Test.DejaFu.dejafusIO``+ * ``Test.DejaFu.autocheckWayIO``+ * ``Test.DejaFu.dejafuWayIO``+ * ``Test.DejaFu.dejafusWayIO``+ * ``Test.DejaFu.dejafuDiscardIO``+ * ``Test.DejaFu.runTestM``+ * ``Test.DejaFu.runTestWayM``++* The ``Test.DejaFu.Conc.ConcST`` type alias.++* The ``MonadBaseControl IO Test.DejaFu.Conc.ConcIO`` typeclass instance.++* The ``Test.DejaFu.alwaysTrue2`` function, which had confusing+ behaviour.++* The ``Test.DejaFu.Common.TTrace`` type synonym for ``[TAction]``.++* The ``Test.DejaFu.Common.preEmpCount`` function.++* Re-exports of ``Decision`` and ``NonEmpty`` from+ ``Test.DejaFu.Schedule``.++* (:issue:`155`) The ``Test.DejaFu.Common`` and ``Test.DejaFu.STM``+ modules.++Fixed+~~~~~++* In refinement property testing, a blocking interference function is+ not reported as a deadlocking execution.++Performance+~~~~~~~~~~~++* (:issue:`124`) Passing tests should use substantially less memory.++* (:issue:`168`) Prune some unnecessary interleavings of ``MVar``+ actions in systematic testing.++Miscellaneous+~~~~~~~~~~~~~++* The lower bound on :hackage:`concurrency` is >=1.3.+++0.9.1.2 (2017-12-12)+--------------------++* Git: :tag:`dejafu-0.9.1.2`+* Hackage: :hackage:`dejafu-0.9.1.2`++Miscellaneous+~~~~~~~~~~~~~++* The upper bound on :hackage:`leancheck` is <0.8.+++0.9.1.1 (2017-12-08)+--------------------++* Git: :tag:`dejafu-0.9.1.1`+* Hackage: :hackage:`dejafu-0.9.1.1`++Fixed+~~~~~++* (:issue:`160`) Fix an off-by-one issue with nested masks during+ systematic testing.+++0.9.1.0 (2017-11-26)+--------------------++* Git: :tag:`dejafu-0.9.1.0`+* Hackage: :hackage:`dejafu-0.9.1.0`++Added+~~~~~++* ``MonadFail`` instance for ``Test.DejaFu.Conc.ConcT``.+* ``MonadFail`` instance for ``Test.DejaFu.STM.STMLike``.++Changed+~~~~~~~++* Pretty-printed traces display a pre-emption following a yield with a+ little "p".++Fixed+~~~~~++* Some incorrect Haddock ``@since`` comments.+++0.9.0.3 (2017-11-06)+--------------------++* Git: :tag:`dejafu-0.9.0.3`+* Hackage: :hackage:`dejafu-0.9.0.3`++Fixed+~~~~~++* (:issue:`138`) Fix missed interleavings in systematic testing with+ some relaxed memory programs.+++0.9.0.2 (2017-11-02)+--------------------++* Git: :tag:`dejafu-0.9.0.2`+* Hackage: :hackage:`dejafu-0.9.0.2`++Changed+~~~~~~~++* A fair bound of 0 prevents yielding or delaying.++Performance+~~~~~~~~~~~++* Prune some unnecessary interleavings of STM transactions in+ systematic testing.+++0.9.0.1 (2017-10-28)+--------------------++* Git: :tag:`dejafu-0.9.0.1`+* Hackage: :hackage:`dejafu-0.9.0.1`++Fixed+~~~~~++* (:issue:`139`) Fix double pop of exception handler stack.+++0.9.0.0 (2017-10-11)+--------------------++* Git: :tag:`dejafu-0.9.0.0`+* Hackage: :hackage:`dejafu-0.9.0.0`++Added+~~~~~++* Failure predicates (also exported from ``Test.DejaFu``):++ * ``Test.DejaFu.Common.isAbort``+ * ``Test.DejaFu.Common.isDeadlock``+ * ``Test.DejaFu.Common.isIllegalSubconcurrency``+ * ``Test.DejaFu.Common.isInternalError``+ * ``Test.DejaFu.Common.isUncaughtException``++* Thread action and lookahead values for ``threadDelay``:++ * ``Test.DejaFu.Common.ThreadDelay``+ * ``Test.DejaFu.Common.WillThreadDelay``++Changed+~~~~~~~++* The ``UncaughtException`` constructor for+ ``Test.DejaFu.Common.Failure`` now includes the exception value.++* Uses of ``threadDelay`` are no longer reported in the trace as a use+ of ``yield``.++Removed+~~~~~~~++* The ``Bounded``, ``Enum``, and ``Read`` instances for+ ``Test.DejaFu.Common.Failure``.+++0.8.0.0 (2017-09-26)+--------------------++* Git: :tag:`dejafu-0.8.0.0`+* Hackage: :hackage:`dejafu-0.8.0.0`++Changed+~~~~~~~++* (:issue:`80`) STM traces now include the ID of a newly-created+ ``TVar``.++* (:issue:`106`) Schedulers are not given the execution trace so far.++* (:issue:`120`) Traces only include a single action of lookahead.++* (:issue:`122`) The ``Test.DejaFu.Scheduler.Scheduler`` type is now a+ newtype, rather than a type synonym.+++0.7.3.0 (2017-09-26)+--------------------++* Git: :tag:`dejafu-0.7.3.0`+* Hackage: :hackage:`dejafu-0.7.3.0`++Added+~~~~~++* The ``Test.DejaFu.Common.threadNames`` function.++Fixed+~~~~~++* (:issue:`101`) Named threads which are only started by a pre-emption+ are shown in the pretty-printed trace key.++* (:issue:`118`) Escaping a mask by raising an exception correctly+ restores the masking state (#118).+++0.7.2.0 (2017-09-16)+--------------------++* Git: :tag:`dejafu-0.7.2.0`+* Hackage: :hackage:`dejafu-0.7.2.0`++Added+~~~~~++* ``Alternative`` and ``MonadPlus`` instances for+ ``Test.DejaFu.STM.STM``.++Fixed+~~~~~++* The ``Eq`` and ``Ord`` instances for+ ``Test.DejaFu.Common.ThreadId``, ``CRefId``, ``MVarId``, and+ ``TVarId`` are consistent.++Miscellaneous+~~~~~~~~~~~~~++* The upper bound on :hackage:`concurrency` is <1.2.+++0.7.1.3 (2017-09-08)+--------------------++* Git: :tag:`dejafu-0.7.1.3`+* Hackage: :hackage:`dejafu-0.7.1.3`++Fixed+~~~~~++* (:issue:`111`) Aborted STM transactions are correctly rolled back.++Performance+~~~~~~~~~~~++* (:issue:`105`) Use a more efficient approach for an internal+ component of the systematic testing.+++0.7.1.2 (2017-08-21)+--------------------++* Git: :tag:`dejafu-0.7.1.2`+* Hackage: :hackage:`dejafu-0.7.1.2`++Fixed+~~~~~++* (:issue:`110`) Errors thrown with ``Control.Monad.fail`` are+ correctly treated as asynchronous exceptions.+++0.7.1.1 (2017-08-16)+--------------------++* Git: :tag:`dejafu-0.7.1.1`+* Hackage: :hackage:`dejafu-0.7.1.1`++Performance+~~~~~~~~~~~++* (:issue:`64`) Greatly reduce memory usage in systematic testing when+ discarding traces by using an alternative data structure.++ * Old: ``O(max trace length * number of executions)``+ * New: ``O(max trace length * number of traces kept)``+++0.7.1.0 - The Discard Release (2017-08-10)+------------------------------------------++* Git: :tag:`dejafu-0.7.1.0`+* Hackage: :hackage:`dejafu-0.7.1.0`++Added+~~~~~++* (:issue:`90`) A way to selectively discard results or traces:++ * Type: ``Test.DejaFu.SCT.Discard``+ * Functions: ``Test.DejaFu.SCT.runSCTDiscard``,+ ``resultsSetDiscard``, ``sctBoundDiscard``,+ ``sctUniformRandomDiscard``, and ``sctWeightedRandomDiscard``.++* (:issue:`90`) Discarding variants of the testing functions:++ * ``Test.DejaFu.dejafuDiscard``+ * ``Test.DejaFu.dejafuDiscardIO``++* (:issue:`90`) ``Test.DejaFu.Defaults.defaultDiscarder``.++Performance+~~~~~~~~~~~++* (:issue:`90`) The ``Test.DejaFu.SCT.resultsSet`` and ``resultsSet'``+ functions discard traces as they are produced, rather than all at+ the end.+++0.7.0.2 (2017-06-12)+--------------------++* Git: :tag:`dejafu-0.7.0.2`+* Hackage: :hackage:`dejafu-0.7.0.2`++Changed+~~~~~~~++* Remove unnecessary typeclass constraints from+ ``Test.DejaFu.Refinement.check``, ``check'``, ``checkFor``, and+ ``counterExamples``.++Miscellaneous+~~~~~~~~~~~~~++* Remove an unnecessary dependency on :hackage:`monad-loops`.+++0.7.0.1 (2017-06-09)+--------------------++* Git: :tag:`dejafu-0.7.0.1`+* Hackage: :hackage:`dejafu-0.7.0.1`++Performance+~~~~~~~~~~~++* The ``Test.DejaFu.Refinement.check``, ``check'``, and ``checkFor``+ functions no longer need to compute all counterexamples before+ showing only one.++* The above and ``counterExamples`` are now faster even if there is+ only a single counterexample in some cases.+++0.7.0.0 - The Refinement Release (2017-06-07)+---------------------------------------------++* Git: :tag:`dejafu-0.7.0.0`+* Hackage: :hackage:`dejafu-0.7.0.0`++Added+~~~~~++* The ``Test.DejaFu.Refinement`` module, re-exported from+ ``Test.DejaFu``.++* The ``Test.DejaFu.SCT.sctUniformRandom`` function for SCT via random+ scheduling.++* Smart constructors for ``Test.DejaFu.SCT.Way`` (also re-exported+ from ``Test.DejaFu``):++ * ``Test.DejaFu.SCT.systematically``, like the old+ ``Systematically``.+ * ``Test.DejaFu.SCT.randomly``, like the old ``Randomly``.+ * ``Test.DejaFu.SCT.uniformly``, a new uniform (as opposed to+ weighted) random scheduler.+ * ``Test.DejaFu.SCT.swarmy``, like the old ``Randomly`` but which+ can use the same weights for multiple executions.++Changed+~~~~~~~++* The ``default*`` values are defined in ``Test.DejaFu.Defaults`` and+ re-exported from ``Test.DejaFu``.++* The ``Test.DejaFu.SCT.sctRandom`` function is now called+ ``sctWeightedRandom`` and can re-use the same weights for multiple+ executions.++Removed+~~~~~~~++* The ``Test.DejaFu.SCT.Way`` type is now abstract, so its+ constructors are no longer exported:++ * ``Test.DejaFu.SCT.Systematically``+ * ``Test.DejaFu.SCT.Randomly``++* The ``Test.DejaFu.SCT.sctPreBound``, ``sctFairBound``, and+ ``sctLengthBound`` functions.++Fixed+~~~~~++* (:issue:`81`) ``Test.DejaFu.Conc.subconcurrency`` no longer re-uses+ IDs.+++0.6.0.0 (2017-04-08)+--------------------++* Git: :tag:`dejafu-0.6.0.0`+* Hackage: :hackage:`dejafu-0.6.0.0`++Changed+~~~~~~~++* The ``Test.DejaFu.Conc.Conc n r a`` type is ``ConcT r n a``, and has+ a ``MonadTrans`` instance.++* The ``Test.DejaFu.SCT.Way`` type is a GADT, and does not expose the+ type parameter of the random generator.++Removed+~~~~~~~++* The ``NFData`` instance for ``Test.DejaFu.SCT.Way``.++Miscellaneous+~~~~~~~~~~~~~++* ``Test.DejaFu.Common`` forms part of the public API.++* Every definition, class, and instance now has a Haddock ``@since``+ annotation.+++0.5.1.3 (2017-04-05)+--------------------++* Git: :tag:`dejafu-0.5.1.3`+* Hackage: :hackage:`dejafu-0.5.1.3`++Miscellaneous+~~~~~~~~~~~~~++* The version bounds on :hackage:`concurrency` are 1.1.*.+++0.5.1.2 (2017-03-04)+--------------------++* Git: :tag:`dejafu-0.5.1.2`+* Hackage: :hackage:`dejafu-0.5.1.2`++**Note:** this version was misnumbered! It should have caused a minor+ version bump!++Added+~~~~~++* ``MonadRef`` and ``MonadAtomicRef`` instances for+ ``Test.DejaFu.Conc.Conc`` using ``CRef``.++Fixed+~~~~~++* A long-standing bug where if the main thread is killed with a+ ``throwTo``, the throwing neither appears in the trace nor correctly+ terminates the execution.++Miscellaneous+~~~~~~~~~~~~~++* The upper bound on :hackage:`concurrency` is <1.1.1.+++0.5.1.1 (2017-02-25)+--------------------++* Git: :tag:`dejafu-0.5.1.1`+* Hackage: :hackage:`dejafu-0.5.1.1`++Fixed+~~~~~++* Fix using incorrect correct scheduler state after a `subconcurrency`+ action.++* Fix infinite loop in SCT of subconcurrency.+++0.5.1.0 (2017-02-25)+--------------------++* Git: :tag:`dejafu-0.5.1.0`+* Hackage: :hackage:`dejafu-0.5.1.0`++Added+~~~~~++* ``NFData`` instances for:++ * ``Test.DejaFu.Result``+ * ``Test.DejaFu.Common.ThreadId``+ * ``Test.DejaFu.Common.CRefId``+ * ``Test.DejaFu.Common.MVarId``+ * ``Test.DejaFu.Common.TVarId``+ * ``Test.DejaFu.Common.IdSource``+ * ``Test.DejaFu.Common.ThreadAction``+ * ``Test.DejaFu.Common.Lookahead``+ * ``Test.DejaFu.Common.ActionType``+ * ``Test.DejaFu.Common.TAction``+ * ``Test.DejaFu.Common.Decision``+ * ``Test.DejaFu.Common.Failure``+ * ``Test.DejaFu.Common.MemType``+ * ``Test.DejaFu.SCT.Bounds``+ * ``Test.DejaFu.SCT.PreemptionBound``+ * ``Test.DejaFu.SCT.FairBound``+ * ``Test.DejaFu.SCT.LengthBound``+ * ``Test.DejaFu.SCT.Way``+ * ``Test.DejaFu.STM.Result``++* ``Eq``, ``Ord``, and ``Show`` instances for+ ``Test.DejaFu.Common.IdSource``.++* Strict variants of ``Test.DejaFu.SCT.runSCT`` and ``resultsSet``:+ ``runSCT'`` and ``resultsSet'``.+++0.5.0.2 (2017-02-22)+--------------------++* Git: :tag:`dejafu-0.5.0.2`+* Hackage: :hackage:`dejafu-0.5.0.2`++**Note:** this version was misnumbered! It should have caused a major+ version bump!++Added+~~~~~++* ``StopSubconcurrency`` constructor for+ ``Test.DejaFu.Common.ThreadAction``.++Changed+~~~~~~~++* A ``Test.DejaFu.Common.StopConcurrency`` action appears in the+ execution trace immediately after the end of a+ ``Test.DejaFu.Conc.subconcurrency`` action.++Fixed+~~~~~++* A ``Test.DejaFu.Conc.subconcurrency`` action inherits the number of+ capabilities from the outer computation.++Miscellaneous+~~~~~~~~~~~~~++- ``Test.DejaFu.SCT`` compiles with ``MonoLocalBinds`` enabled+ (implied by ``GADTs`` and ``TypeFamilies``), which may be relevant+ to hackers.+++0.5.0.1 (2017-02-21)+--------------------++* Git: :tag:`dejafu-0.5.0.1`+* Hackage: :hackage:`ps!**`++Fixed+~~~~~++* ``readMVar`` is considered a "release action" for the purposes of+ fair-bounding.+++0.5.0.0 - The Way Release (2017-02-21)+--------------------------------------++* Git: :tag:`dejafu-0.5.0.0`+* Hackage: :hackage:`dejafu-0.5.0.0`++Added+~~~~~++* ``Eq`` instances for ``Test.DejaFu.Common.ThreadAction`` and+ ``Lookahead``.++* Thread action and lookahead values for ``tryReadMVar``:++ * ``Test.DejaFu.Common.TryReadMVar``+ * ``Test.DejaFu.Common.WillTryReadMVar``++* The testing-only ``Test.DejaFu.Conc.subconcurrency`` function.++* SCT through weighted random scheduling:+ ``Test.DejaFu.SCT.sctRandom``.++* The ``Test.DejaFu.SCT.Way`` type, used by the new functions+ ``runSCT`` and ``resultsSet``.++Changed+~~~~~~~++* All the functions which took a ``Test.DejaFu.SCT.Bounds`` now take a+ ``Way`` instead.++Fixed+~~~~~++* Some previously-missed ``CRef`` action dependencies are no longer+ missed.++Miscellaneous+~~~~~~~~~~~~~++* The version bounds on :hackage:`concurrency` are 1.1.0.*.++* A bunch of things were called "Var" or "Ref", these are now+ consistently "MVar" and "CRef".++* Significant performance improvements in both time and space.++* The :hackage:`dpor` package has been merged back into this, as it+ turned out not to be very generally useful.+++0.4.0.0 - The Packaging Release (2016-09-10)+--------------------------------------------++* Git: :tag:`dejafu-0.4.0.0`+* Hackage: :hackage:`dejafu-0.4.0.0`++Added+~~~~~++* The ``Test.DejaFu.runTestM`` and ``runTestM'`` functions.++* The ``Test.DejaFu.Conc.runConcurrent`` function.++* The ``Test.DejaFu.STM.runTransaction`` function.++* The ``Test.DejaFu.Common`` module.++Changed+~~~~~~~++* The ``Control.*`` modules have all been split out into a separate+ :hackage:`concurrency` package.++* The ``Test.DejaFu.Deterministic`` module has been renamed to+ ``Test.DejaFu.Conc``.++* Many definitions from other modules have been moved to the+ ``Test.DejaFu.Common`` module.++* The ``Test.DejaFu.autocheck'`` function takes the schedule bounds as+ a parameter.++* The ``Test.DejaFu.Conc.Conc`` type no longer has the STM type as a+ parameter.++* The ``ST`` specific functions in ``Test.DejaFu.SCT`` are polymorphic+ in the monad.++* The termination of the main thread in execution traces appears as a+ single ``Stop``, rather than the previous ``Lift, Stop``.++* Execution traces printed by the helpful functions in ``Test.DejaFu``+ include a key of thread names.++Removed+~~~~~~~++* The ``Test.DejaFu.runTestIO`` and ``runTestIO'`` functions: use+ ``runTestM`` and ``runTestM'`` instead.++* The ``Test.DejaFu.Conc.runConcST`` and ``runConcIO`` functions: use+ ``runConcurrent`` instead.++* The ``Test.DejaFu.STM.runTransactionST`` and ``runTransactionIO``+ functions: use ``runTransaction`` instead.++* The ``IO`` specific functions in ``Test.DejaFu.SCT``.++++0.3.2.1 (2016-07-21)+--------------------++* Git: :tag:`dejafu-0.3.2.1`+* Hackage: :hackage:`dejafu-0.3.2.1`++Fixed+~~~~~++* (:issue:`55`) Fix incorrect detection of deadlocks with some nested+ STM transactions.+++0.3.2.0 (2016-06-06)+--------------------++* Git: :tag:`dejafu-0.3.2.0`+* Hackage: :hackage:`dejafu-0.3.2.0`++Fixed+~~~~~++* (:issue:`40`) Fix missing executions with daemon threads with+ uninteresting first actions. This is significantly faster with+ :hackage:`dpor-0.2.0.0`.++Performance+~~~~~~~~~~~++* When using :hackage:`dpor-0.2.0.0`, greatly improve dependency+ inference of exceptions during systematic testing.++* Improve dependency inference of STM transactions during systematic+ testing.+++0.3.1.1 (2016-05-26)+--------------------++* Git: :tag:`dejafu-0.3.1.1`+* Hackage: :hackage:`dejafu-0.3.1.1`++Miscellaneous+~~~~~~~~~~~~~++* Now supports GHC 8.+++0.3.1.0 (2016-05-02)+--------------------++* Git: :tag:`dejafu-0.3.1.0`+* Hackage: :hackage:`dejafu-0.3.1.0`++Fixed+~~~~~++* Fix inaccurate counting of pre-emptions in an execution trace when+ relaxed memory commit actions are present.+++0.3.0.0 (2016-04-03)+--------------------++* Git: :tag:`dejafu-0.3.0.0`+* Hackage: :hackage:`dejafu-0.3.0.0`++**The minimum supported version of GHC is now 7.10.**++I didn't write proper release notes, and this is so far back I don't+really care to dig through the logs.+++0.2.0.0 (2015-12-01)+--------------------++* Git: :tag:`0.2.0.0`+* Hackage: :hackage:`dejafu-0.2.0.0`++I didn't write proper release notes, and this is so far back I don't+really care to dig through the logs.+++0.1.0.0 - The Initial Release (2015-08-27)+------------------------------------------++* Git: :tag:`0.1.0.0`+* Hackage: :hackage:`dejafu-0.1.0.0`++Added+~~~~~++* Everything.
Test/DejaFu.hs view
@@ -17,21 +17,24 @@ __A first test:__ This is a simple concurrent program which forks two threads and each races to write to the same @MVar@: -> example = do-> var <- newEmptyMVar-> fork (putMVar var "hello")-> fork (putMVar var "world")-> readMVar var+>>> :{+let example = do+ var <- newEmptyMVar+ fork (putMVar var "hello")+ fork (putMVar var "world")+ readMVar var+:} We can test it with dejafu like so: -> > autocheck example-> [pass] Never Deadlocks-> [pass] No Exceptions-> [fail] Consistent Result-> "hello" S0----S1--S0--->-> "world" S0----S2--S0--+>>> autocheck example+[pass] Never Deadlocks+[pass] No Exceptions+[fail] Consistent Result+ "hello" S0----S1--S0--+<BLANKLINE>+ "world" S0----S2--S0--+False The 'autocheck' function takes a concurrent program to test and looks for some common unwanted behaviours: deadlocks, uncaught exceptions in@@ -180,26 +183,29 @@ to one of the @CRef@s and reads the other. The value that each thread reads is communicated back through an @MVar@: -> relaxed = do-> r1 <- newCRef False-> r2 <- newCRef False-> x <- spawn $ writeCRef r1 True >> readCRef r2-> y <- spawn $ writeCRef r2 True >> readCRef r1-> (,) <$> readMVar x <*> readMVar y+>>> :{+let relaxed = do+ r1 <- newCRef False+ r2 <- newCRef False+ x <- spawn $ writeCRef r1 True >> readCRef r2+ y <- spawn $ writeCRef r2 True >> readCRef r1+ (,) <$> readMVar x <*> readMVar y+:} We see something surprising if we ask for the results: -> > autocheck relaxed-> [pass] Never Deadlocks-> [pass] No Exceptions-> [fail] Consistent Result-> (False,True) S0---------S1----S0--S2----S0--->-> (False,False) S0---------S1--P2----S1--S0---->-> (True,False) S0---------S2----S1----S0---->-> (True,True) S0---------S1-C-S2----S1---S0---+>>> autocheck relaxed+[pass] Never Deadlocks+[pass] No Exceptions+[fail] Consistent Result+ (False,True) S0---------S1----S0--S2----S0--+<BLANKLINE>+ (False,False) S0---------S1--P2----S1--S0---+<BLANKLINE>+ (True,False) S0---------S2----S1----S0---+<BLANKLINE>+ (True,True) S0---------S1-C-S2----S1---S0---+False It's possible for both threads to read the value @False@, even though each writes @True@ to the other @CRef@ before reading. This is@@ -346,12 +352,15 @@ * The expression to evaluate, as a function over the state. -> sig e = Sig-> { initialise = maybe newEmptyMVar newMVar-> , observe = \v _ -> tryReadMVar v-> , interfere = \v _ -> putMVar v 42-> , expression = void . e-> }+>>> import Control.Monad (void)+>>> :{+let sig e = Sig+ { initialise = maybe newEmptyMVar newMVar+ , observe = \v _ -> tryReadMVar v+ , interfere = \v _ -> putMVar v 42+ , expression = void . e+ }+:} This is a signature for operations over @Num n => MVar n@ values where there are multiple producers. The initialisation function takes a@@ -362,10 +371,11 @@ Given this signature, we can check if @readMVar@ is the same as a @takeMVar@ followed by a @putMVar@: -> > check $ sig readMVar === sig (\v -> takeMVar v >>= putMVar v)-> *** Failure: (seed Just 0)-> left: [(Nothing,Just 0)]-> right: [(Nothing,Just 0),(Just Deadlock,Just 42)]+>>> check $ sig readMVar === sig (\v -> takeMVar v >>= putMVar v)+*** Failure: (seed Just 0)+ left: [(Nothing,Just 0)]+ right: [(Nothing,Just 0),(Just Deadlock,Just 42)]+False The two expressions are not equivalent, and we get a counterexample: if the @MVar@ is nonempty, then the left expression (@readMVar@) will@@ -387,8 +397,10 @@ import Control.Monad.Ref (MonadRef) import Data.Function (on) import Data.List (intercalate, intersperse)-import Data.Maybe (catMaybes, isNothing, mapMaybe)+import Data.Maybe (catMaybes, isJust, isNothing,+ mapMaybe) import Data.Profunctor (Profunctor(..))+import System.Environment (lookupEnv) import Test.DejaFu.Conc import Test.DejaFu.Defaults@@ -397,7 +409,29 @@ import Test.DejaFu.Types import Test.DejaFu.Utils +{- $setup +>>> import Control.Concurrent.Classy hiding (check)++>>> :{+let example = do+ var <- newEmptyMVar+ fork (putMVar var "hello")+ fork (putMVar var "world")+ readMVar var+:}++>>> :{+let relaxed = do+ r1 <- newCRef False+ r2 <- newCRef False+ x <- spawn $ writeCRef r1 True >> readCRef r2+ y <- spawn $ writeCRef r2 True >> readCRef r1+ (,) <$> readMVar x <*> readMVar y+:}++-}+ ------------------------------------------------------------------------------- -- DejaFu @@ -406,13 +440,14 @@ -- In particular, look for deadlocks, uncaught exceptions, and -- multiple return values. Returns @True@ if all tests pass ----- > > autocheck example--- > [pass] Never Deadlocks--- > [pass] No Exceptions--- > [fail] Consistent Result--- > "hello" S0----S1--S0----- >--- > "world" S0----S2--S0--+-- >>> autocheck example+-- [pass] Never Deadlocks+-- [pass] No Exceptions+-- [fail] Consistent Result+-- "hello" S0----S1--S0--+-- <BLANKLINE>+-- "world" S0----S2--S0--+-- False -- -- @since 1.0.0.0 autocheck :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a)@@ -424,28 +459,30 @@ -- | Variant of 'autocheck' which takes a way to run the program and a -- memory model. ----- > > autocheckWay defaultWay defaultMemType relaxed--- > [pass] Never Deadlocks--- > [pass] No Exceptions--- > [fail] Consistent Result--- > (False,True) S0---------S1----S0--S2----S0----- >--- > (False,False) S0---------S1--P2----S1--S0------ >--- > (True,False) S0---------S2----S1----S0------ >--- > (True,True) S0---------S1-C-S2----S1---S0------ >--- > > autocheckWay defaultWay SequentialConsistency relaxed--- > [pass] Never Deadlocks--- > [pass] No Exceptions--- > [fail] Consistent Result--- > (False,True) S0---------S1----S0--S2----S0----- >--- > (True,True) S0---------S1-P2----S1---S0------ >--- > (True,False) S0---------S2----S1----S0---+-- >>> autocheckWay defaultWay defaultMemType relaxed+-- [pass] Never Deadlocks+-- [pass] No Exceptions+-- [fail] Consistent Result+-- (False,True) S0---------S1----S0--S2----S0--+-- <BLANKLINE>+-- (False,False) S0---------S1--P2----S1--S0---+-- <BLANKLINE>+-- (True,False) S0---------S2----S1----S0---+-- <BLANKLINE>+-- (True,True) S0---------S1-C-S2----S1---S0---+-- False --+-- >>> autocheckWay defaultWay SequentialConsistency relaxed+-- [pass] Never Deadlocks+-- [pass] No Exceptions+-- [fail] Consistent Result+-- (False,True) S0---------S1----S0--S2----S0--+-- <BLANKLINE>+-- (True,True) S0---------S1-P2----S1---S0---+-- <BLANKLINE>+-- (True,False) S0---------S2----S1----S0---+-- False+-- -- @since 1.0.0.0 autocheckWay :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a) => Way@@ -472,11 +509,12 @@ -- predicate to determine if the test passes. Predicates can look for -- anything, including checking for some expected nondeterminism. ----- > > dejafu "Test Name" alwaysSame example--- > [fail] Test Name--- > "hello" S0----S1--S0----- >--- > "world" S0----S2--S0--+-- >>> dejafu "Test Name" alwaysSame example+-- [fail] Test Name+-- "hello" S0----S1--S0--+-- <BLANKLINE>+-- "world" S0----S2--S0--+-- False -- -- @since 1.0.0.0 dejafu :: (MonadConc n, MonadIO n, MonadRef r n, Show b)@@ -492,20 +530,22 @@ -- | Variant of 'dejafu' which takes a way to run the program and a -- memory model. ----- > > import System.Random--- >--- > > dejafuWay (randomly (mkStdGen 0) 100) defaultMemType "Randomly!" alwaysSame example--- > [fail] Randomly!--- > "hello" S0----S1--S0----- >--- > "world" S0----S2--S0----- >--- > > dejafuWay (randomly (mkStdGen 1) 100) defaultMemType "Randomly!" alwaysSame example--- > [fail] Randomly!--- > "hello" S0----S1--S0----- >--- > "world" S0----S2--S1-S0--+-- >>> import System.Random --+-- >>> dejafuWay (randomly (mkStdGen 0) 100) defaultMemType "Randomly!" alwaysSame example+-- [fail] Randomly!+-- "hello" S0----S1--S0--+-- <BLANKLINE>+-- "world" S0----S2--S0--+-- False+--+-- >>> dejafuWay (randomly (mkStdGen 1) 100) defaultMemType "Randomly!" alwaysSame example+-- [fail] Randomly!+-- "hello" S0----S1--S0--+-- <BLANKLINE>+-- "world" S0----S2--S1-S0--+-- False+-- -- @since 1.0.0.0 dejafuWay :: (MonadConc n, MonadIO n, MonadRef r n, Show b) => Way@@ -523,11 +563,12 @@ -- | Variant of 'dejafuWay' which can selectively discard results. ----- > > dejafuDiscard (\_ -> Just DiscardTrace) defaultWay defaultMemType "Discarding" alwaysSame example--- > [fail] Discarding--- > "hello" <trace discarded>--- >--- > "world" <trace discarded>+-- >>> dejafuDiscard (\_ -> Just DiscardTrace) defaultWay defaultMemType "Discarding" alwaysSame example+-- [fail] Discarding+-- "hello" <trace discarded>+-- <BLANKLINE>+-- "world" <trace discarded>+-- False -- -- @since 1.0.0.0 dejafuDiscard :: (MonadConc n, MonadIO n, MonadRef r n, Show b)@@ -552,12 +593,13 @@ -- | Variant of 'dejafu' which takes a collection of predicates to -- test, returning 'True' if all pass. ----- > > dejafus [("A", alwaysSame), ("B", deadlocksNever)] example--- > [fail] A--- > "hello" S0----S1--S0----- >--- > "world" S0----S2--S0----- > [pass] B+-- >>> dejafus [("A", alwaysSame), ("B", deadlocksNever)] example+-- [fail] A+-- "hello" S0----S1--S0--+-- <BLANKLINE>+-- "world" S0----S2--S0--+-- [pass] B+-- False -- -- @since 1.0.0.0 dejafus :: (MonadConc n, MonadIO n, MonadRef r n, Show b)@@ -571,14 +613,15 @@ -- | Variant of 'dejafus' which takes a way to run the program and a -- memory model. ----- > > dejafusWay defaultWay SequentialConsistency [("A", alwaysSame), ("B", exceptionsNever)] relaxed--- > [fail] A--- > (False,True) S0---------S1----S0--S2----S0----- >--- > (True,True) S0---------S1-P2----S1---S0------ >--- > (True,False) S0---------S2----S1----S0------ > [pass] B+-- >>> dejafusWay defaultWay SequentialConsistency [("A", alwaysSame), ("B", exceptionsNever)] relaxed+-- [fail] A+-- (False,True) S0---------S1----S0--S2----S0--+-- <BLANKLINE>+-- (True,True) S0---------S1-P2----S1---S0---+-- <BLANKLINE>+-- (True,False) S0---------S2----S1----S0---+-- [pass] B+-- False -- -- @since 1.0.0.0 dejafusWay :: (MonadConc n, MonadIO n, MonadRef r n, Show b)@@ -912,25 +955,30 @@ -- | Run a test and print to stdout doTest :: Show a => String -> Result a -> IO Bool doTest name result = do- if _pass result- then- -- Display a pass message.- putStrLn ("\27[32m[pass]\27[0m " ++ name)- else do- -- Display a failure message, and the first 5 (simplified) failed traces- putStrLn ("\27[31m[fail]\27[0m " ++ name)+ doctest <- isJust <$> lookupEnv "DEJAFU_DOCTEST"+ if _pass result+ then putStrLn (passmsg doctest)+ else do+ -- Display a failure message, and the first 5 (simplified) failed traces+ putStrLn (failmsg doctest) - unless (null $ _failureMsg result) $- putStrLn $ _failureMsg result+ unless (null $ _failureMsg result) $+ putStrLn $ _failureMsg result - let failures = _failures result- let output = map (\(r, t) -> putStrLn . indent $ either showFail show r ++ " " ++ showTrace t) $ take 5 failures- sequence_ $ intersperse (putStrLn "") output- when (moreThan 5 failures) $- putStrLn (indent "...")+ let failures = _failures result+ let output = map (\(r, t) -> putStrLn . indent $ either showFail show r ++ " " ++ showTrace t) $ take 5 failures+ sequence_ $ intersperse (putStrLn "") output+ when (moreThan 5 failures) $+ putStrLn (indent "...") - pure (_pass result)+ pure (_pass result)+ where+ passmsg True = "[pass] " ++ name+ passmsg False = "\27[32m[pass]\27[0m " ++ name + failmsg True = "[fail] " ++ name+ failmsg False = "\27[31m[fail]\27[0m " ++ name+ -- | Check if a list is longer than some value, without needing to -- compute the entire length. moreThan :: Int -> [a] -> Bool@@ -940,4 +988,4 @@ -- | Indent every line of a string. indent :: String -> String-indent = intercalate "\n" . map ('\t':) . lines+indent = intercalate "\n" . map (" "++) . lines
Test/DejaFu/Conc/Internal.hs view
@@ -191,11 +191,11 @@ let (idSource', newtid) = nextTId n (cIdSource ctx) let threads' = launch tid newtid a (cThreads ctx) threads'' <- makeBound newtid threads'- pure (Right ctx { cThreads = goto (b newtid) tid threads'', cIdSource = idSource' }, Single (Fork newtid))+ pure (Right ctx { cThreads = goto (b newtid) tid threads'', cIdSource = idSource' }, Single (ForkOS newtid)) -- check if the current thread is bound AIsBound c ->- let isBound = isJust (_bound =<< M.lookup tid (cThreads ctx))+ let isBound = isJust . _bound $ elookup "stepThread.AIsBound" tid (cThreads ctx) in simple (goto (c isBound) tid (cThreads ctx)) (IsCurrentThreadBound isBound) -- get the 'ThreadId' of the current thread@@ -370,7 +370,7 @@ -- a function to run a computation with the current masking state. AMasking m ma c -> let a = runCont (ma umask) (AResetMask False False m' . c)- m' = _masking . efromJust "stepThread.AMasking" $ M.lookup tid (cThreads ctx)+ m' = _masking $ elookup "stepThread.AMasking" tid (cThreads ctx) umask mb = resetMask True m' >> mb >>= \b -> resetMask False m >> pure b resetMask typ ms = cont $ \k -> AResetMask typ True ms $ k () threads' = goto a tid (mask m tid (cThreads ctx))
Test/DejaFu/Conc/Internal/Memory.hs view
@@ -129,12 +129,15 @@ -- | Add phantom threads to the thread list to commit pending writes. addCommitThreads :: WriteBuffer r -> Threads n r -> Threads n r addCommitThreads (WriteBuffer wb) ts = ts <> M.fromList phantoms where- phantoms = [ (ThreadId (Id Nothing $ negate tid), mkthread c)- | ((_, b), tid) <- zip (M.toList wb) [1..]+ phantoms = [ (ThreadId (Id Nothing . negate $ commitTidOf k), mkthread c)+ | (k, b) <- M.toList wb , c <- maybeToList (go $ viewl b) ] go (BufferedWrite tid (CRef crid _) _ :< _) = Just $ ACommit tid crid go EmptyL = Nothing++ commitTidOf (ThreadId (Id _ t), Nothing) = t + 1+ commitTidOf (ThreadId (Id _ t), Just (CRefId (Id _ c))) = t + 1 + c * 10000 -- | Remove phantom threads. delCommitThreads :: Threads n r -> Threads n r
Test/DejaFu/Conc/Internal/Threading.hs view
@@ -16,16 +16,16 @@ import qualified Control.Concurrent.Classy as C import Control.Exception (Exception, MaskingState(..), SomeException, fromException)+import Control.Monad (forever) import Data.List (intersect) import Data.Map.Strict (Map)+import qualified Data.Map.Strict as M import Data.Maybe (isJust) import Test.DejaFu.Conc.Internal.Common import Test.DejaFu.Internal import Test.DejaFu.Types -import qualified Data.Map.Strict as M- -------------------------------------------------------------------------------- -- * Threads @@ -85,32 +85,33 @@ -- | Propagate an exception upwards, finding the closest handler -- which can deal with it. propagate :: SomeException -> ThreadId -> Threads n r -> Maybe (Threads n r)-propagate e tid threads = case M.lookup tid threads >>= go . _handlers of- Just (act, hs) -> Just $ except act hs tid threads- Nothing -> Nothing+propagate e tid threads = raise <$> propagate' handlers where+ handlers = _handlers (elookup "propagate" tid threads) - where- go [] = Nothing- go (Handler h:hs) = maybe (go hs) (\act -> Just (act, hs)) $ h <$> fromException e+ raise (act, hs) = except act hs tid threads + propagate' [] = Nothing+ propagate' (Handler h:hs) = maybe (propagate' hs) (\act -> Just (act, hs)) $ h <$> fromException e+ -- | Check if a thread can be interrupted by an exception. interruptible :: Thread n r -> Bool interruptible thread = _masking thread == Unmasked || (_masking thread == MaskedInterruptible && isJust (_blocking thread)) -- | Register a new exception handler. catching :: Exception e => (e -> Action n r) -> ThreadId -> Threads n r -> Threads n r-catching h = M.adjust $ \thread ->+catching h = eadjust "catching" $ \thread -> let ms0 = _masking thread h' = Handler $ \e ms -> (if ms /= ms0 then AResetMask False False ms0 else id) (h e) in thread { _handlers = h' : _handlers thread } -- | Remove the most recent exception handler. uncatching :: ThreadId -> Threads n r -> Threads n r-uncatching = M.adjust $ \thread -> thread { _handlers = etail "uncatching" (_handlers thread) }+uncatching = eadjust "uncatching" $ \thread ->+ thread { _handlers = etail "uncatching" (_handlers thread) } -- | Raise an exception in a thread. except :: (MaskingState -> Action n r) -> [Handler n r] -> ThreadId -> Threads n r -> Threads n r-except actf hs = M.adjust $ \thread -> thread+except actf hs = eadjust "except" $ \thread -> thread { _continuation = actf (_masking thread) , _handlers = hs , _blocking = Nothing@@ -118,24 +119,24 @@ -- | Set the masking state of a thread. mask :: MaskingState -> ThreadId -> Threads n r -> Threads n r-mask ms = M.adjust $ \thread -> thread { _masking = ms }+mask ms = eadjust "mask" $ \thread -> thread { _masking = ms } -------------------------------------------------------------------------------- -- * Manipulating threads -- | Replace the @Action@ of a thread. goto :: Action n r -> ThreadId -> Threads n r -> Threads n r-goto a = M.adjust $ \thread -> thread { _continuation = a }+goto a = eadjust "goto" $ \thread -> thread { _continuation = a } -- | Start a thread with the given ID, inheriting the masking state -- from the parent thread. This ID must not already be in use! launch :: ThreadId -> ThreadId -> ((forall b. M n r b -> M n r b) -> Action n r) -> Threads n r -> Threads n r launch parent tid a threads = launch' ms tid a threads where- ms = maybe Unmasked _masking (M.lookup parent threads)+ ms = _masking (elookup "launch" parent threads) -- | Start a thread with the given ID and masking state. This must not already be in use! launch' :: MaskingState -> ThreadId -> ((forall b. M n r b -> M n r b) -> Action n r) -> Threads n r -> Threads n r-launch' ms tid a = M.insert tid thread where+launch' ms tid a = einsert "launch'" tid thread where thread = Thread (a umask) Nothing [] ms Nothing umask mb = resetMask True Unmasked >> mb >>= \b -> resetMask False ms >> pure b@@ -143,7 +144,7 @@ -- | Block a thread. block :: BlockedOn -> ThreadId -> Threads n r -> Threads n r-block blockedOn = M.adjust $ \thread -> thread { _blocking = Just blockedOn }+block blockedOn = eadjust "block" $ \thread -> thread { _blocking = Just blockedOn } -- | Unblock all threads waiting on the appropriate block. For 'TVar' -- blocks, this will wake all threads waiting on at least one of the@@ -168,26 +169,20 @@ getboundIO <- C.newEmptyMVar btid <- C.forkOSN ("bound worker for '" ++ show tid ++ "'") (go runboundIO getboundIO) let bt = BoundThread runboundIO getboundIO btid- pure (M.adjust (\t -> t { _bound = Just bt }) tid threads)+ pure (eadjust "makeBound" (\t -> t { _bound = Just bt }) tid threads) where- go runboundIO getboundIO =- let loop = do- na <- C.takeMVar runboundIO- C.putMVar getboundIO =<< na- loop- in loop+ go runboundIO getboundIO = forever $ do+ na <- C.takeMVar runboundIO+ C.putMVar getboundIO =<< na -- | Kill a thread and remove it from the thread map. -- -- If the thread is bound, the worker thread is cleaned up. kill :: C.MonadConc n => ThreadId -> Threads n r -> n (Threads n r)-kill tid threads = case M.lookup tid threads of- Just thread -> case _bound thread of- Just bt -> do- C.killThread (_boundTId bt)- pure (M.delete tid threads)- Nothing -> pure (M.delete tid threads)- Nothing -> pure threads+kill tid threads = do+ let thread = elookup "kill" tid threads+ maybe (pure ()) (C.killThread . _boundTId) (_bound thread)+ pure (M.delete tid threads) -- | Run an action. --
Test/DejaFu/Internal.hs view
@@ -14,6 +14,7 @@ import Control.DeepSeq (NFData(..)) import Control.Monad.Ref (MonadRef(..)) import Data.List.NonEmpty (NonEmpty(..))+import qualified Data.Map.Strict as M import Data.Maybe (fromMaybe) import Data.Set (Set) import qualified Data.Set as S@@ -290,12 +291,6 @@ ------------------------------------------------------------------------------- -- * Error reporting --- | 'head' but with a better error message if it fails. Use this--- only where it shouldn't fail!-ehead :: String -> [a] -> a-ehead _ (x:_) = x-ehead src _ = fatal src "head: empty list"- -- | 'tail' but with a better error message if it fails. Use this -- only where it shouldn't fail! etail :: String -> [a] -> [a]@@ -320,6 +315,27 @@ efromList :: String -> [a] -> NonEmpty a efromList _ (x:xs) = x:|xs efromList src _ = fatal src "fromList: empty list"++-- | 'M.adjust' but which errors if the key is not present. Use this+-- only where it shouldn't fail!+eadjust :: (Ord k, Show k) => String -> (v -> v) -> k -> M.Map k v -> M.Map k v+eadjust src f k m = case M.lookup k m of+ Just v -> M.insert k (f v) m+ Nothing -> fatal src ("adjust: key '" ++ show k ++ "' not found")++-- | 'M.insert' but which errors if the key is already present. Use+-- this only where it shouldn't fail!+einsert :: (Ord k, Show k) => String -> k -> v -> M.Map k v -> M.Map k v+einsert src k v m+ | M.member k m = fatal src ("insert: key '" ++ show k ++ "' already present")+ | otherwise = M.insert k v m++-- | 'M.lookup' but which errors if the key is not present. Use this+-- only where it shouldn't fail!+elookup :: (Ord k, Show k) => String -> k -> M.Map k v -> v+elookup src k =+ fromMaybe (fatal src ("lookup: key '" ++ show k ++ "' not found")) .+ M.lookup k -- | 'error' but saying where it came from fatal :: String -> String -> a
Test/DejaFu/Refinement.hs view
@@ -22,19 +22,21 @@ -- -- This module can test properties like that: ----- @--- sig e = Sig--- { initialise = maybe newEmptyMVar newMVar--- , observe = \\v _ -> tryReadMVar v--- , interfere = \\v s -> tryTakeMVar v >> maybe (pure ()) (void . tryPutMVar v) s--- , expression = e--- }+-- >>> import Control.Monad (void)+-- >>> :{+-- let sig e = Sig+-- { initialise = maybe newEmptyMVar newMVar+-- , observe = \v _ -> tryReadMVar v+-- , interfere = \v _ -> putMVar v 42+-- , expression = void . e+-- }+-- :} ----- > check $ sig (void . readMVar) \`equivalentTo\` sig (\\v -> takeMVar v >>= putMVar v)--- *** Failure: (seed Just ())--- left: [(Nothing,Just ())]--- right: [(Nothing,Just ()),(Just Deadlock,Just ())]--- @+-- >>> check $ sig readMVar === sig (\v -> takeMVar v >>= putMVar v)+-- *** Failure: (seed Just 0)+-- left: [(Nothing,Just 0)]+-- right: [(Nothing,Just 0),(Just Deadlock,Just 42)]+-- False -- -- The two expressions are not equivalent, and we get given the -- counterexample!@@ -115,6 +117,9 @@ import Test.DejaFu.Conc (ConcIO, Failure, subconcurrency) import Test.DejaFu.Defaults (defaultMemType, defaultWay) import Test.DejaFu.SCT (runSCT)++-- $setup+-- >>> import Control.Concurrent.Classy hiding (check) ------------------------------------------------------------------------------- -- Specifying properties
Test/DejaFu/SCT/Internal/DPOR.hs view
@@ -1,10 +1,12 @@+{-# LANGUAGE ViewPatterns #-}+ -- | -- Module : Test.DejaFu.SCT.Internal.DPOR -- Copyright : (c) 2015--2017 Michael Walker -- License : MIT -- Maintainer : Michael Walker <mike@barrucadu.co.uk> -- Stability : experimental--- Portability : portable+-- Portability : ViewPatterns -- -- Internal types and functions for SCT via dynamic partial-order -- reduction. This module is NOT considered to form part of the@@ -20,7 +22,8 @@ import Data.List.NonEmpty (toList) import Data.Map.Strict (Map) import qualified Data.Map.Strict as M-import Data.Maybe (isJust, isNothing, listToMaybe)+import Data.Maybe (isJust, isNothing, listToMaybe,+ maybeToList) import Data.Sequence (Seq, (|>)) import qualified Data.Sequence as Sq import Data.Set (Set)@@ -67,6 +70,28 @@ , dporTaken dpor ) +-- | Check the DPOR data invariants and raise an error if any are+-- broken.+--+-- This is a reasonable thing to do, because if the state is corrupted+-- then nothing sensible can happen anyway.+validateDPOR :: String -> DPOR -> DPOR+validateDPOR src dpor+ | not (todo `S.isSubsetOf` runnable) = fatal src "thread exists in todo set but not runnable set"+ | not (done `S.isSubsetOf` runnable) = fatal src "thread exists in done set but not runnable set"+ | not (taken `S.isSubsetOf` done) = fatal src "thread exists in taken set but not done set"+ | not (todo `disjoint` done) = fatal src "thread exists in both taken set and done set"+ | not (maybe True (`S.member` done) next) = fatal src "taken thread does not exist in done set"+ | otherwise = dpor+ where+ done = dporDone dpor+ next = fst <$> dporNext dpor+ runnable = dporRunnable dpor+ taken = S.fromList (M.keys (dporTaken dpor))+ todo = S.fromList (M.keys (dporTodo dpor))++ disjoint s1 s2 = S.null (S.intersection s1 s2)+ -- | One step of the execution, including information for backtracking -- purposes. This backtracking information is used to generate new -- schedules.@@ -152,9 +177,10 @@ state' = updateDepState state tid' a in case dporNext dpor of Just (t, child)- | t == tid' -> dpor { dporNext = Just (tid', grow state' tid' rest child) }+ | t == tid' ->+ validateDPOR "incorporateTrace (grow / Just)" $ dpor { dporNext = Just (tid', grow state' tid' rest child) } | hasTodos child -> fatal "incorporateTrace" "replacing child with todos!"- _ ->+ _ -> validateDPOR "incorporateTrace (grow / Nothing)" $ let taken = M.insert tid' a (dporTaken dpor) sleep = dporSleep dpor `M.union` dporTaken dpor in dpor { dporTaken = if conservative then dporTaken dpor else taken@@ -168,12 +194,12 @@ hasTodos dpor = not (M.null (dporTodo dpor)) || (case dporNext dpor of Just (_, dpor') -> hasTodos dpor'; _ -> False) -- Construct a new subtree corresponding to a trace suffix.- subtree state tid sleep ((_, _, a):rest) =+ subtree state tid sleep ((_, _, a):rest) = validateDPOR "incorporateTrace (subtree)" $ let state' = updateDepState state tid a sleep' = M.filterWithKey (\t a' -> not $ dependent state' tid a t a') sleep in DPOR { dporRunnable = S.fromList $ case rest of- ((_, runnable, _):_) -> map fst runnable+ ((d', runnable, _):_) -> tidOf tid d' : map fst runnable [] -> [] , dporTodo = M.empty , dporNext = case rest of@@ -245,24 +271,23 @@ -- backtracking points. doBacktrack killsEarly allThreads enabledThreads bs = let tagged = reverse $ zip [0..] bs- idxs = [ (ehead "doBacktrack.idxs" is, False, u)+ idxs = [ (i, False, u) | (u, n) <- enabledThreads , v <- S.toList allThreads , u /= v- , let is = idxs' u n v tagged- , not $ null is]+ , i <- maybeToList (findIndex u n v tagged)] - idxs' u n v = go' True where+ findIndex u n v = go' True where {-# INLINE go' #-} go' final ((i,b):rest) -- Don't cross subconcurrency boundaries- | isSubC final b = []+ | isSubC final b = Nothing -- If this is the final action in the trace and the -- execution was killed due to nothing being within bounds -- (@killsEarly == True@) assume worst-case dependency.- | bcktThreadid b == v && (killsEarly || isDependent b) = i : go' False rest+ | bcktThreadid b == v && (killsEarly || isDependent b) = Just i | otherwise = go' False rest- go' _ [] = []+ go' _ [] = Nothing {-# INLINE isSubC #-} isSubC final b = case bcktAction b of@@ -284,7 +309,7 @@ -- | Add new backtracking points, if they have not already been -- visited and aren't in the sleep set. incorporateBacktrackSteps :: [BacktrackStep] -> DPOR -> DPOR-incorporateBacktrackSteps (b:bs) dpor = dpor' where+incorporateBacktrackSteps (b:bs) dpor = validateDPOR "incorporateBacktrackSteps" dpor' where tid = bcktThreadid b dpor' = dpor@@ -529,6 +554,35 @@ ------------------------------------------------------------------------------- -- * Dependency function +-- | Check if two actions commute.+--+-- This implements a stronger check that @not (dependent ...)@, as it+-- handles some cases which 'dependent' doesn't need to care about.+--+-- This should not be used to re-order traces which contain+-- subconcurrency.+independent :: DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool+independent ds t1 a1 t2 a2+ | t1 == t2 = False+ | check t1 a1 t2 a2 = False+ | check t2 a2 t1 a1 = False+ | otherwise = not (dependent ds t1 a1 t2 a2)+ where+ -- can't re-order any action of a thread with the fork which+ -- created it.+ check _ (Fork t) tid _ | t == tid = True+ check _ (ForkOS t) tid _ | t == tid = True+ -- because we can't easily tell if this will terminate the other+ -- thread, we just can't re-order asynchronous exceptions at all+ -- :(+ --+ -- See #191 / #190+ check _ (ThrowTo t) tid _ | t == tid = True+ check _ (BlockedThrowTo t) tid _ | t == tid = True+ -- can't re-order an unsynchronised write with something which synchronises that CRef.+ check _ (simplifyAction -> UnsynchronisedWrite r) _ (simplifyAction -> a) | synchronises a r = True+ check _ _ _ _ = False+ -- | Check if an action is dependent on another. -- -- This is basically the same as 'dependent'', but can make use of the@@ -536,13 +590,6 @@ -- in a few cases. dependent :: DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool dependent ds t1 a1 t2 a2 = case (a1, a2) of- -- @SetNumCapabilities@ and @GetNumCapabilities@ are NOT dependent- -- IF the value read is the same as the value written. 'dependent''- -- can not see the value read (as it hasn't happened yet!), and so- -- is more pessimistic here.- (SetNumCapabilities a, GetNumCapabilities b) | a == b -> False- (GetNumCapabilities a, SetNumCapabilities b) | a == b -> False- -- When masked interruptible, a thread can only be interrupted when -- actually blocked. 'dependent'' has to assume that all -- potentially-blocking operations can block, and so is more@@ -588,13 +635,13 @@ -- 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.- (GetNumCapabilities a, WillSetNumCapabilities b) -> a /= b+ (GetNumCapabilities _, WillSetNumCapabilities _) -> True (SetNumCapabilities _, WillGetNumCapabilities) -> True- (SetNumCapabilities a, WillSetNumCapabilities b) -> a /= b _ -> dependentActions ds (simplifyAction a1) (simplifyLookahead l2) @@ -715,6 +762,7 @@ Nothing -> masks updateMaskState tid (SetMasking _ ms) = M.insert tid ms updateMaskState tid (ResetMasking _ ms) = M.insert tid ms+updateMaskState tid Stop = M.delete tid updateMaskState _ _ = id -- | Check if a @CRef@ has a buffered write pending.
dejafu.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: dejafu-version: 1.0.0.1+version: 1.0.0.2 synopsis: A library for unit-testing concurrent programs. description:@@ -23,7 +23,7 @@ copyright: (c) 2015--2017 Michael Walker category: Concurrency build-type: Simple-extra-source-files: README.markdown CHANGELOG.markdown+extra-source-files: README.markdown CHANGELOG.rst cabal-version: >=1.10 source-repository head@@ -33,7 +33,7 @@ source-repository this type: git location: https://github.com/barrucadu/dejafu.git- tag: dejafu-1.0.0.1+ tag: dejafu-1.0.0.2 library exposed-modules: Test.DejaFu