2016-05-03 21:17:06 +03:00
dejafu [![Build Status][build-status]][build-log]
2016-05-03 02:05:29 +03:00
======
2016-05-03 21:17:06 +03:00
[build-status]: https://travis-ci.org/barrucadu/dejafu.svg?branch=master
[build-log]: https://travis-ci.org/barrucadu/dejafu
2016-05-03 02:05:29 +03:00
> [Déjà Fu is] A martial art in which the user's limbs move in time as
> well as space, […] It is best described as "the feeling that you
> have been kicked in the head this way before"
>
> -- 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.
2016-08-25 19:24:00 +03:00
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.
2016-05-03 02:05:29 +03:00
2014-12-20 20:32:35 +03:00
2016-08-25 19:24:00 +03:00
Table of Contents
-----------------
2016-06-20 23:45:34 +03:00
2016-08-25 19:24:00 +03:00
- [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 )
2017-03-04 02:25:06 +03:00
- [Program Testing ](#program-testing )
2016-08-25 19:24:00 +03:00
- [Porting ](#porting )
- [Contributing ](#contributing )
2017-04-08 07:21:30 +03:00
- [Test Coverage ](#test-coverage )
2017-03-20 22:27:42 +03:00
- [Performance ](#performance )
2017-04-07 20:16:08 +03:00
- [Release Notes / Change Logs ](#release-notes--change-logs )
2016-08-25 19:24:00 +03:00
- [Bibliography ](#bibliography )
2015-08-27 15:33:48 +03:00
2016-04-03 16:26:31 +03:00
2016-08-25 19:24:00 +03:00
Packages
--------
2014-12-20 20:32:35 +03:00
2016-08-25 19:24:00 +03:00
| | Version | Intended Users | Summary |
| --- | ------- | -------------- | ------- |
2017-04-05 23:41:22 +03:00
| concurrency [[docs][d:conc]] [[hackage][h:conc]] | 1.1.2.0 | Authors | Typeclasses, functions, and data types for concurrency and STM. |
| dejafu [[docs][d:dejafu]] [[hackage][h:dejafu]] | 0.5.1.3 | Testers | Systematic testing for Haskell concurrency. |
2017-03-20 21:42:51 +03:00
| hunit-dejafu [[docs][d:hunit]] [[hackage][h:hunit]] | 0.4.0.1 | Testers | Deja Fu support for the HUnit test framework. |
2017-02-20 06:17:22 +03:00
| tasty-dejafu [[docs][d:tasty]] [[hackage][h:tasty]] | 0.4.0.0 | Testers | Deja Fu support for the Tasty test framework. |
2015-10-25 19:14:00 +03:00
2017-04-07 20:16:08 +03:00
Each package has its own README and CHANGELOG in its subdirectory.
2015-10-08 23:50:52 +03:00
2016-04-01 18:54:45 +03:00
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.
2016-08-25 19:24:00 +03:00
[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
Concurrent Programming
----------------------
You should read [Parallel and Concurrent Programming in Haskell][parconc],
2017-03-04 01:06:09 +03:00
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.
2016-08-25 19:24:00 +03:00
[parconc]: http://chimera.labs.oreilly.com/books/1230000000929/
### Asynchronous IO
The wonderful *[async][]* package by Simon Marlow greatly eases the
difficulty of writing programs which merely need to perform some
2017-03-04 01:06:09 +03:00
asynchronous IO. The *concurrency* package includes an almost-total
reimplementation of *async* .
2016-08-25 19:24:00 +03:00
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
-- ...
```
The `withAsync` function starts an operation in a separate thread, and
kills it if the inner action finishes before it completes.
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)
```
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.
[async]: http://hackage.haskell.org/package/async
### Threads and MVars
The fundamental unit of concurrency is the thread, and the most basic
communication mechanism is the `MVar` :
```haskell
main = do
var < - newEmptyMVar
fork $ putMVar var 'x'
fork $ putMVar var 'y'
r < - takeMVar m
print r
```
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:
2016-05-03 02:05:29 +03:00
2016-08-25 19:24:00 +03:00
```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)
```
2016-05-03 02:05:29 +03:00
2016-08-25 19:24:00 +03:00
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.
2016-05-03 02:05:29 +03:00
2016-08-25 19:24:00 +03:00
### Relaxed Memory and CRefs
2016-05-03 02:05:29 +03:00
2016-08-25 19:24:00 +03:00
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.
2016-05-03 02:05:29 +03:00
2016-08-25 19:24:00 +03:00
```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
```
2016-05-03 02:05:29 +03:00
2016-08-25 19:24:00 +03:00
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:
```
> autocheck example
[fail] Never Deadlocks (checked: 5)
[deadlock] S0------------S1-P2--S1-
[pass] No Exceptions (checked: 12)
[fail] Consistent Result (checked: 11)
0 S0------------S2-----------------S1-----------------S0----
[deadlock] S0------------S1-P2--S1-
False
```
It identifies the deadlock, and also the possible results the
computation can produce, and displays a simplified trace leading to
2016-08-29 20:34:27 +03:00
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.
2016-08-25 19:24:00 +03:00
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
2016-05-03 02:05:29 +03:00
As a general rule of thumb, to convert some existing code to work with
dejafu:
2016-08-25 19:24:00 +03:00
- Depend on "concurrency".
2016-05-03 02:05:29 +03:00
- 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.
Contributing
------------
Bug reports, pull requests, and comments are very welcome!
2017-02-26 06:16:52 +03:00
The general idea (which I'm trying out as of Feb 2017) is
that [master][] should always be at most a minor version ahead of what
is released on hackage, there shouldn't be any backwards-incompatible
changes. Backwards-incompatible changes go on the [next-major][]
branch. This is to make it feasible to fix bugs without also
introducing breaking changes, even if work on the next major version
has already begun.
2016-05-03 02:05:29 +03:00
Feel free to contact me on GitHub, through IRC (#haskell on freenode),
or email (mike@barrucadu.co.uk).
2016-04-01 18:54:45 +03:00
2017-02-26 06:16:52 +03:00
[master]: https://github.com/barrucadu/dejafu/tree/master
[next-major]: https://github.com/barrucadu/dejafu/tree/next-major
2017-04-08 07:21:30 +03:00
### Test Coverage
2017-03-04 02:25:06 +03:00
[`hpc`][hpc] can generate a coverage report from the execution of
dejafu-tests:
```
$ stack build --coverage
$ stack exec dejafu-tests
$ stack hpc report --all dejafu-tests.tix
```
This will print some stats and generate an HTML coverage report:
```
Generating combined report
52% expressions used (4052/7693)
48% boolean coverage (63/129)
43% guards (46/106), 31 always True, 9 always False, 20 unevaluated
68% 'if' conditions (11/16), 2 always True, 3 unevaluated
85% qualifiers (6/7), 1 unevaluated
61% alternatives used (392/635)
80% local declarations used (210/261)
26% top-level declarations used (280/1063)
The combined report is available at /home/barrucadu/projects/dejafu/.stack-work/install/x86_64-linux/nightly-2016-06-20/8.0.1/hpc/combined/custom/hpc_index.html
```
The highlighted code in the HTML report emphasises branch coverage:
- Red means a branch was evaluated as always false.
- Green means a branch was evaluated as always true.
- Yellow means an expression was never evaluated.
See also the [stack coverage documentation][hpc-stack].
[hpc]: https://wiki.haskell.org/Haskell_program_coverage
[hpc-stack]: https://docs.haskellstack.org/en/latest/coverage/
2017-03-20 22:27:42 +03:00
### Performance
GHC can generate performance statistics from the execution of
dejafu-tests:
```
$ stack build --profile
$ stack exec -- dejafu-tests +RTS -p
$ less dejafu-tests.prof
```
This prints a detailed breakdown of where memory and time are being
spent:
```
Mon Mar 20 19:26 2017 Time and Allocation Profiling Report (Final)
dejafu-tests +RTS -p -RTS
total time = 105.94 secs (105938 ticks @ 1000 us, 1 processor)
total alloc = 46,641,766,952 bytes (excludes profiling overheads)
COST CENTRE MODULE %time %alloc
findBacktrackSteps.doBacktrack.idxs' Test.DejaFu.SCT.Internal 21.9 12.0
== Test.DejaFu.Common 12.4 0.0
yieldCount.go Test.DejaFu.SCT 12.1 0.0
dependent' Test.DejaFu.SCT 5.1 0.0
runThreads.go Test.DejaFu.Conc.Internal 2.7 4.1
[...]
```
dejafu-tests is a good target for profiling, as it is a fairly
representative use: a testsuite where results will be quickly
summarised and printed. It may not be so useful for judging
performance of programs which keep the test results around for a long
time.
2016-08-25 19:24:00 +03:00
2017-04-07 20:16:08 +03:00
Release Notes / Change Logs
---------------------------
2017-04-07 22:22:22 +03:00
See the CHANGELOG.markdown file.
2017-04-07 20:16:08 +03:00
2016-04-01 18:54:45 +03:00
Bibliography
------------
2016-08-25 19:24:00 +03:00
These libraries wouldn't be possible without prior research, which I
mention in the documentation. Haddock comments get the full citation,
whereas in-line comments just get the shortened name:
2016-04-01 18:54:45 +03:00
2016-04-01 19:49:35 +03:00
- [BPOR] *Bounded partial-order reduction* , K. Coons, M. Musuvathi,
and K. McKinley (2013)
2016-04-01 18:54:45 +03:00
http://research.microsoft.com/pubs/202164/bpor-oopsla-2013.pdf
2016-04-01 19:49:35 +03:00
- [RDPOR] *Dynamic Partial Order Reduction for Relaxed Memory Models* ,
N. Zhang, M. Kusano, and C. Wang (2015)
http://www.faculty.ece.vt.edu/chaowang/pubDOC/ZhangKW15.pdf
2016-04-01 18:54:45 +03:00
- [Empirical] *Concurrency Testing Using Schedule Bounding: an
Empirical Study*, P. Thompson, A. Donaldson, and A. Betts (2014)
http://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2014/PPoPP.pdf
2016-04-01 18:56:17 +03:00
- [RMMVerification] *On the Verification of Programs on Relaxed Memory
Models*, A. Linden (2014)
https://orbi.ulg.ac.be/bitstream/2268/158670/1/thesis.pdf
2016-05-03 02:05:29 +03:00
There are also a couple of papers on dejafu itself:
- *Déjà Fu: A Concurrency Testing Library for Haskell*, M. Walker and
C. Runciman (2015)
https://www.barrucadu.co.uk/publications/dejafu-hs15.pdf
This details dejafu-0.1, and was presented at the 2015 Haskell
Symposium.
- *Déjà Fu: A Concurrency Testing Library for Haskell*, M. Walker and
C. Runciman (2016)
https://www.barrucadu.co.uk/publications/YCS-2016-503.pdf
This is a more in-depth technical report, written between the
dejafu-0.2 and dejafu-0.3 releases.