mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-11-29 22:22:54 +03:00
Simpler README more like the website
This commit is contained in:
parent
1da31432a8
commit
915233fec8
414
README.markdown
414
README.markdown
@ -10,44 +10,45 @@ dejafu [![Build Status][build-status]][build-log]
|
||||
>
|
||||
> -- Terry Pratchett, Thief of Time
|
||||
|
||||
Have you ever written a concurrent Haskell program and then, Heaven
|
||||
forbid, wanted to *test* it? Testing concurrency is normally a hard
|
||||
problem, because of the nondeterminism of scheduling: you can run your
|
||||
program ten times and get ten different results if you're unlucky.
|
||||
|
||||
There is a solution! Through these libraries, you can write concurrent
|
||||
programs and test them *deterministically*. By abstracting out the
|
||||
actual implementation of concurrency through a typeclass, an
|
||||
alternative implementation can be used for testing, allowing the
|
||||
*systematic* exploration of the possible results of your program.
|
||||
|
||||
|
||||
Table of Contents
|
||||
-----------------
|
||||
|
||||
- [Packages](#packages)
|
||||
- [Concurrent Programming](#getting-started)
|
||||
- [Asynchronous IO](#asynchronous-io)
|
||||
- [Threads and MVars](#threads-and-mvars)
|
||||
- [Software Transactional Memory](#software-transactional-memory)
|
||||
- [Relaxed Memory and IORefs](#relaxed-memory-and-iorefs)
|
||||
- [Program Testing](#program-testing)
|
||||
- [Porting](#porting)
|
||||
- [Test Performance](#test-performance)
|
||||
- [Installation](#installation)
|
||||
- [Quick start guide](#quick-start-guide)
|
||||
- [Why Déjà Fu?](#why-déjà-fu)
|
||||
- [Contributing](#contributing)
|
||||
- [Release Notes / Change Logs](#release-notes--change-logs)
|
||||
- [Release notes](#release-notes)
|
||||
- [Questions, feedback, discussion](#questions-feedback-discussion)
|
||||
- [Bibliography](#bibliography)
|
||||
- **[The website!](http://dejafu.readthedocs.io/)**
|
||||
|
||||
Déjà Fu is a unit-testing library for concurrent Haskell programs.
|
||||
Tests are deterministic and expressive, making it easy and convenient
|
||||
to test your threaded code. Available on [GitHub][], [Hackage][], and
|
||||
[Stackage][].
|
||||
|
||||
Packages
|
||||
--------
|
||||
[GitHub]: https://github.com/barrucadu/dejafu
|
||||
[Hackage]: https://hackage.haskell.org/package/dejafu
|
||||
[Stackage]: https://www.stackage.org/package/dejafu
|
||||
|
||||
| | Version | Intended Users | Summary |
|
||||
| --- | ------- | -------------- | ------- |
|
||||
| concurrency [[docs][d:conc]] [[hackage][h:conc]] | 1.1.2.1 | Authors | Typeclasses, functions, and data types for concurrency and STM. |
|
||||
| dejafu [[docs][d:dejafu]] [[hackage][h:dejafu]] | 0.7.1.2 | Testers | Systematic testing for Haskell concurrency. |
|
||||
| hunit-dejafu [[docs][d:hunit]] [[hackage][h:hunit]] | 0.7.0.0 | Testers | Deja Fu support for the HUnit test framework. |
|
||||
| tasty-dejafu [[docs][d:tasty]] [[hackage][h:tasty]] | 0.7.0.0 | Testers | Deja Fu support for the Tasty test framework. |
|
||||
Features:
|
||||
|
||||
- An abstraction over the concurrency functionality in `IO`
|
||||
- Deterministic testing of nondeterministic code
|
||||
- Both complete (slower) and incomplete (faster) modes
|
||||
- A unit-testing-like approach to writing test cases
|
||||
- A property-testing-like approach to comparing stateful operations
|
||||
- Testing of potentially nonterminating programs
|
||||
- Integration with [HUnit][] and [tasty][]
|
||||
|
||||
[HUnit]: https://hackage.haskell.org/package/HUnit
|
||||
[Tasty]: https://hackage.haskell.org/package/tasty
|
||||
|
||||
There are a few different packages under the Déjà Fu umbrella:
|
||||
|
||||
| | Version | Summary |
|
||||
| - | ------- | ------- |
|
||||
| [concurrency][h:conc] | 1.1.2.1 | Typeclasses, functions, and data types for concurrency and STM. |
|
||||
| [dejafu][h:dejafu] | 0.7.1.2 | Systematic testing for Haskell concurrency. |
|
||||
| [hunit-dejafu][h:hunit] | 0.7.0.0 | Deja Fu support for the HUnit test framework. |
|
||||
| [tasty-dejafu][h:tasty] | 0.7.0.0 | Deja Fu support for the Tasty test framework. |
|
||||
|
||||
Each package has its own README and CHANGELOG in its subdirectory.
|
||||
|
||||
@ -55,303 +56,113 @@ There is also dejafu-tests, the test suite for dejafu. This is in a
|
||||
separate package due to Cabal being bad with test suite transitive
|
||||
dependencies.
|
||||
|
||||
[d:conc]: https://docs.barrucadu.co.uk/concurrency/
|
||||
[d:dejafu]: https://docs.barrucadu.co.uk/dejafu/
|
||||
[d:hunit]: https://docs.barrucadu.co.uk/hunit-dejafu/
|
||||
[d:tasty]: https://docs.barrucadu.co.uk/tasty-dejafu/
|
||||
|
||||
[h:conc]: https://hackage.haskell.org/package/concurrency
|
||||
[h:dejafu]: https://hackage.haskell.org/package/dejafu
|
||||
[h:hunit]: https://hackage.haskell.org/package/hunit-dejafu
|
||||
[h:tasty]: https://hackage.haskell.org/package/tasty-dejafu
|
||||
|
||||
Everything is on Hackage and Stackage, and the last three major GHC
|
||||
versions (currently 8.2, 8.0, and 7.10) are supported.
|
||||
|
||||
Concurrent Programming
|
||||
----------------------
|
||||
|
||||
You should read [Parallel and Concurrent Programming in Haskell][parconc],
|
||||
by Simon Marlow. It's very good, and the API of the *concurrency*
|
||||
package is intentionally kept very similar to the *async*, *base*, and
|
||||
*stm* packages, so all the knowledge transfers.
|
||||
Installation
|
||||
------------
|
||||
|
||||
[parconc]: http://chimera.labs.oreilly.com/books/1230000000929/
|
||||
Install from Hackage globally:
|
||||
|
||||
### Asynchronous IO
|
||||
|
||||
The wonderful *[async][]* package by Simon Marlow greatly eases the
|
||||
difficulty of writing programs which merely need to perform some
|
||||
asynchronous IO. The *concurrency* package includes an almost-total
|
||||
reimplementation of *async*.
|
||||
|
||||
For example, assuming a suitable `getURL` function, to fetch the
|
||||
contents of two web pages at the same time:
|
||||
|
||||
```haskell
|
||||
withAsync (getURL url1) $ \a1 -> do
|
||||
withAsync (getURL url2) $ \a2 -> do
|
||||
page1 <- wait a1
|
||||
page2 <- wait a2
|
||||
-- ...
|
||||
```
|
||||
$ cabal-install dejafu
|
||||
```
|
||||
|
||||
The `withAsync` function starts an operation in a separate thread, and
|
||||
kills it if the inner action finishes before it completes.
|
||||
Or add it to your cabal file:
|
||||
|
||||
Another example, this time waiting for any of a number of web pages to
|
||||
download, and cancelling the others as soon as one completes:
|
||||
|
||||
```haskell
|
||||
let download url = do
|
||||
res <- getURL url
|
||||
pure (url, res)
|
||||
|
||||
downloads <- mapM (async . download) urls
|
||||
(url, res) <- waitAnyCancel downloads
|
||||
printf "%s was first (%d bytes)\n" url (B.length res)
|
||||
```
|
||||
build-depends: ...
|
||||
, dejafu
|
||||
```
|
||||
|
||||
The `async` function starts an operation in another thread but, unlike
|
||||
`withAsync` takes no inner action to execute: the programmer needs to
|
||||
make sure the computation is waited for or cancelled as appropriate.
|
||||
Or to your package.yaml:
|
||||
|
||||
[async]: http://hackage.haskell.org/package/async
|
||||
```
|
||||
dependencies:
|
||||
...
|
||||
- dejafu
|
||||
```
|
||||
|
||||
### Threads and MVars
|
||||
|
||||
The fundamental unit of concurrency is the thread, and the most basic
|
||||
communication mechanism is the `MVar`:
|
||||
Quick start guide
|
||||
-----------------
|
||||
|
||||
Déjà Fu supports unit testing, and comes with a helper function called
|
||||
`autocheck` to look for some common issues. Let's see it in action:
|
||||
|
||||
```haskell
|
||||
main = do
|
||||
import Control.Concurrent.Classy
|
||||
|
||||
myFunction :: MonadConc m => m String
|
||||
myFunction = do
|
||||
var <- newEmptyMVar
|
||||
fork $ putMVar var 'x'
|
||||
fork $ putMVar var 'y'
|
||||
r <- takeMVar m
|
||||
print r
|
||||
fork (putMVar var "hello")
|
||||
fork (putMVar var "world")
|
||||
readMVar var
|
||||
```
|
||||
|
||||
The `fork` function starts executing a `MonadConc` action in a
|
||||
separate thread, and `takeMVar`/`putMVar` are used to communicate
|
||||
values (`newEmptyMVar` just makes an `MVar` with nothing in it). This
|
||||
will either print `'x'` or `'y'`, depending on which of the two
|
||||
threads "wins".
|
||||
|
||||
On top of the simple `MVar`, we can build more complicated concurrent
|
||||
data structures, like channels. A collection of these are provided in
|
||||
the *concurrency* package.
|
||||
|
||||
If a thread attempts to read from an `MVar` which is never written to,
|
||||
or write to an `MVar` which is never read from, it blocks.
|
||||
|
||||
### Software Transactional Memory
|
||||
|
||||
Software transactional memory (STM) simplifies stateful concurrent
|
||||
programming by allowing complex atomic state operations. Whereas only
|
||||
one `MVar` can be modified atomically at a time, any number of `TVar`s
|
||||
can be. STM is normally provided by the *stm* package, but the
|
||||
*concurrency* package exposes it directly.
|
||||
|
||||
For example, we can swap the values of two variables, and read them in
|
||||
another thread:
|
||||
|
||||
```haskell
|
||||
main = do
|
||||
var1 <- newTVar 'x'
|
||||
var2 <- newTVar 'y'
|
||||
fork . atomically $ do
|
||||
a <- readTVar var1
|
||||
b <- readTVar var2
|
||||
writeTVar var2 a
|
||||
writeTVar var1 b
|
||||
a <- atomically $ readTVar var1
|
||||
b <- atomically $ readTVar var2
|
||||
print (a, b)
|
||||
```
|
||||
|
||||
Even though the reads and writes appear to be done in multiple steps
|
||||
inside the forked thread, the entire transaction is executed in a
|
||||
single step, by the `atomically` function. This means that the main
|
||||
thread will observe the values `('x', 'y')` or `('y', 'x')`, it can
|
||||
never get `('x', 'x')` as naive `MVar` implementation would.
|
||||
|
||||
### Relaxed Memory and CRefs
|
||||
|
||||
There is a third type of communication primitive, the `CRef` (known in
|
||||
normal Haskell as the `IORef`). These do not impose synchronisation,
|
||||
and so the behaviour of concurrent reads and writes depends on the
|
||||
memory model of the underlying processor.
|
||||
|
||||
```haskell
|
||||
crefs = 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
|
||||
```
|
||||
|
||||
Here `spawn` forks a thread and gives an `MVar` which can be read from
|
||||
to get the return value. Under a sequentially consistent memory model,
|
||||
there are three possible results: `(True, True)`, `(True, False)`, and
|
||||
`(False, True)`. Under the relaxed memory model of modern processors,
|
||||
the result `(False, False)` is also possible. Relaxed memory models
|
||||
allow for reads and writes to be re-ordered between threads.
|
||||
|
||||
For testing, three memory models are supported (with the default being
|
||||
TSO):
|
||||
|
||||
- **Sequential Consistency:** A program behaves as a simple
|
||||
interleaving of the actions in different threads. When a `CRef` is
|
||||
written to, that write is immediately visible to all threads.
|
||||
|
||||
- **Total Store Order (TSO):** Each thread has a write buffer. A
|
||||
thread sees its writes immediately, but other threads will only
|
||||
see writes when they are committed, which may happen later. Writes
|
||||
are committed in the same order that they are created.
|
||||
|
||||
- **Partial Store Order (PSO):** Each `CRef` has a write buffer. A
|
||||
thread sees its writes immediately, but other threads will only
|
||||
see writes when they are committed, which may happen later. Writes
|
||||
to different `CRefs` are not necessarily committed in the same
|
||||
order that they are created.
|
||||
|
||||
### Program Testing
|
||||
|
||||
If you just write your concurrent program using the `MonadConc` and
|
||||
`MonadSTM` typeclasses (maybe with `MonadIO` if you need `IO` as
|
||||
well), then it is testable with dejafu!
|
||||
|
||||
Testing is similar to unit testing, the programmer produces a
|
||||
self-contained monadic action to execute. It is run under many
|
||||
schedules, and the results gathered into a list. This is a little
|
||||
different from normal unit testing, where you just return "true" or
|
||||
"false", here you have *many* results, and need to decide if the
|
||||
collection is valid or not.
|
||||
|
||||
For the simple cases, where you just want to check something is
|
||||
deterministic and doesn't deadlock, there is a handy `autocheck`
|
||||
function. For example:
|
||||
|
||||
```haskell
|
||||
example = do
|
||||
a <- newEmptyMVar
|
||||
b <- newEmptyMVar
|
||||
|
||||
c <- newMVar 0
|
||||
|
||||
let lock m = putMVar m ()
|
||||
let unlock = takeMVar
|
||||
|
||||
j1 <- spawn $ lock a >> lock b >> modifyMVar_ c (return . succ) >> unlock b >> unlock a
|
||||
j2 <- spawn $ lock b >> lock a >> modifyMVar_ c (return . pred) >> unlock a >> unlock b
|
||||
|
||||
takeMVar j1
|
||||
takeMVar j2
|
||||
|
||||
takeMVar c
|
||||
```
|
||||
|
||||
The correct result is 0, as it starts out as 0 and is incremented and
|
||||
decremented by threads 1 and 2, respectively. However, note the order
|
||||
of acquisition of the locks in the two threads. If thread 2 pre-empts
|
||||
thread 1 between the acquisition of the locks (or if thread 1
|
||||
pre-empts thread 2), a deadlock situation will arise, as thread 1 will
|
||||
have lock a and be waiting on b, and thread 2 will have b and be
|
||||
waiting on a.
|
||||
|
||||
Here is what `autocheck` has to say about it:
|
||||
That `MonadConc` is a typeclass abstraction over concurrency, but
|
||||
we'll get onto that shortly. First, the result of testing:
|
||||
|
||||
```
|
||||
> autocheck example
|
||||
[fail] Never Deadlocks (checked: 5)
|
||||
[deadlock] S0------------S1-P2--S1-
|
||||
> autocheck myFunction
|
||||
[pass] Never Deadlocks (checked: 12)
|
||||
[pass] No Exceptions (checked: 12)
|
||||
[fail] Consistent Result (checked: 11)
|
||||
0 S0------------S2-----------------S1-----------------S0----
|
||||
"hello" S0----S1-P2-S0--
|
||||
|
||||
[deadlock] S0------------S1-P2--S1-
|
||||
"world" S0----S2--S0-P1-S0-
|
||||
False
|
||||
```
|
||||
|
||||
It identifies the deadlock, and also the possible results the
|
||||
computation can produce, and displays a simplified trace leading to
|
||||
each failing outcome. The traces contain thread numbers, which the
|
||||
programmer can give a thread a name when forking. It also returns
|
||||
false as there are test failures.
|
||||
There are no deadlocks or uncaught exceptions, which is good; but the
|
||||
program is (as you probably spotted) nondeterministic!
|
||||
|
||||
Note that if your test case does `IO`, the `IO` will be executed a lot
|
||||
of times. It needs to be deterministic enough to not invalidate the
|
||||
results of testing. That may seem a burden, but it's a requirement of
|
||||
any form of testing.
|
||||
|
||||
### Porting
|
||||
|
||||
As a general rule of thumb, to convert some existing code to work with
|
||||
dejafu:
|
||||
|
||||
- Depend on "concurrency".
|
||||
- Import `Control.Concurrent.Classy.*` instead of `Control.Concurrent.*`
|
||||
- Change `IO a` to `MonadConc m => m a`
|
||||
- Change `STM a` to `MonadSTM stm => stm a`
|
||||
- Parameterise all the types by the monad: `MVar` -> `MVar m`, `TVar`
|
||||
-> `TVar stm`, `IORef` -> `CRef m`, etc
|
||||
- Fix the type errors.
|
||||
Along with each result, Déjà Fu gives us a representative execution
|
||||
trace in an abbreviated form. `Sn` means that thread `n` started
|
||||
executing, and `Pn` means that thread `n` pre-empted the previously
|
||||
running thread.
|
||||
|
||||
|
||||
Test Performance
|
||||
----------------
|
||||
Why Déjà Fu?
|
||||
------------
|
||||
|
||||
dejafu (and the hunit/tasty bindings) leans more towards correctness
|
||||
than performance, by default. Your test cases will be executed using
|
||||
the `Test.DejaFu.SCT.sctBounded ` function, which is complete but can
|
||||
be slow; every result you get will have an associated trace, which can
|
||||
be useful for debugging, but takes up memory.
|
||||
Testing concurrent programs is difficult, because in general they are
|
||||
nondeterministic. This leads to people using work-arounds like
|
||||
running their testsuite many thousands of times; or running their
|
||||
testsuite while putting their machine under heavy load.
|
||||
|
||||
If testing it too slow, there are a few knobs you can tweak:
|
||||
These approaches are inadequate for a few reasons:
|
||||
|
||||
- Are you happy to trade space for time?
|
||||
- **How many runs is enough?** When you are just hopping to spot a bug
|
||||
by coincidence, how do you know to stop?
|
||||
- **How do you know if you've fixed a bug you saw previously?**
|
||||
Because the scheduler is a black box, you don't know if the
|
||||
previously buggy schedule has been re-run.
|
||||
- **You won't actually get that much scheduling variety!** Operating
|
||||
systems and language runtimes like to run threads for long periods
|
||||
of time, which reduces the variety you get (and so drives up the
|
||||
number of runs you need).
|
||||
|
||||
Consider computing the results once and running multiple
|
||||
predicates over the output: this is what `dejafus` / `testDejafus`
|
||||
/ etc does.
|
||||
Déjà Fu addresses these points by offering *complete* testing. You
|
||||
can run a test case and be guaranteed to find all results with some
|
||||
bounds. These bounds can be configured, or even disabled! The
|
||||
underlying approach used is smarter than merely trying all possible
|
||||
executions, and will in general explore the state-space quickly.
|
||||
|
||||
- Can you sacrifice completeness?
|
||||
|
||||
Consider using the random testing functionality. See the `*Way`
|
||||
functions and `Test.DejaFu.SCT.sct{Uniform,Weighted}Random`.
|
||||
|
||||
- Would strictness help?
|
||||
|
||||
Consider using the strict functions in `Test.DejaFu.SCT` (the ones
|
||||
ending with a `'`).
|
||||
|
||||
- Do you just want the set of results, and don't care about traces?
|
||||
|
||||
Consider using `Test.DejaFu.SCT.resultsSet`.
|
||||
|
||||
- Do you know something about the sort of results you care about?
|
||||
|
||||
Consider discarding results you *don't* care about. See the
|
||||
`*Discard` functions in `Test.DejaFu`, `Test.DejaFu.SCT`, and
|
||||
`Test.{HUnit,Tasty}.DejaFu`.
|
||||
|
||||
For example, let's say you want to know if your test case deadlocks,
|
||||
and are going to sacrifice completeness because your possible
|
||||
state-space is huge. You could do it like this:
|
||||
|
||||
```haskell
|
||||
dejafuDiscard
|
||||
-- "efa" == "either failure a", discard everything but deadlocks
|
||||
(\efa -> if efa == Left Deadlock then Nothing else Just DiscardResultAndTrace)
|
||||
-- try 1000 executions with random scheduling
|
||||
(randomly (mkStdGen 42) 1000)
|
||||
-- use the default memory model
|
||||
defaultMemType
|
||||
-- your test case
|
||||
testCase
|
||||
-- the predicate to check (which is a bit redundant in this case)
|
||||
("Never Deadlocks", deadlocksNever)
|
||||
```
|
||||
If your test case is just too big for complete testing, there is also
|
||||
a random scheduling mode, which is necessarily *incomplete*. However,
|
||||
Déjà Fu will tend to produce much more schedule variety than just
|
||||
running your test case in `IO` the same number of times, and so bugs
|
||||
will tend to crop up sooner. Furthermore, as you get execution traces
|
||||
out, you can be certain that a bug has been fixed by simply following
|
||||
the trace by eye.
|
||||
|
||||
|
||||
Contributing
|
||||
@ -359,13 +170,28 @@ Contributing
|
||||
|
||||
See the CONTRIBUTING.markdown file.
|
||||
|
||||
**If you'd like to get involved with Déjà Fu**, check out [the
|
||||
"beginner friendly" label on the issue tracke][beginners].
|
||||
|
||||
Release Notes / Change Logs
|
||||
---------------------------
|
||||
[beginners]: https://github.com/barrucadu/dejafu/issues?q=is%3Aissue+is%3Aopen+label%3A%22beginner+friendly%22
|
||||
|
||||
|
||||
Release notes
|
||||
-------------
|
||||
|
||||
See the CHANGELOG.markdown file.
|
||||
|
||||
|
||||
Questions, feedback, discussion
|
||||
-------------------------------
|
||||
|
||||
- For general help talk to me in IRC (barrucadu in #haskell) or shoot
|
||||
me an email (mike@barrucadu.co.uk)
|
||||
- For bugs, issues, or requests, please [file an issue][issues].
|
||||
|
||||
[issues]: https://github.com/barrucadu/dejafu/issues
|
||||
|
||||
|
||||
Bibliography
|
||||
------------
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user