mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-10-05 18:28:30 +03:00
Add new mdbook / GitHub Pages based website
This commit is contained in:
Michael Walker
parent
ee99cbb975
commit
a4d31bdaaa
92
.github/scripts/build-documentation.sh
vendored
Executable file
92
.github/scripts/build-documentation.sh
vendored
Executable file
@ -0,0 +1,92 @@
|
||||
#! /usr/bin/env nix-shell
|
||||
#! nix-shell -I nixpkgs=channel:nixos-23.05 -i bash --packages coreutils mdbook mdbook-admonish python3 virtualenv ghc stack
|
||||
|
||||
set -ex
|
||||
|
||||
OUTPUT_DIR="_site"
|
||||
|
||||
pushd docs
|
||||
mdbook-admonish install
|
||||
popd
|
||||
|
||||
python3 <<'EOF' > docs/src/index.md
|
||||
import sys
|
||||
|
||||
with open("README.markdown") as f:
|
||||
mode = "title"
|
||||
for line in f:
|
||||
line = line.rstrip()
|
||||
if mode == "title":
|
||||
print("Getting Started")
|
||||
mode = "after-title"
|
||||
elif mode == "after-title":
|
||||
if line.startswith("- "):
|
||||
mode = "skip-links"
|
||||
else:
|
||||
print(line)
|
||||
elif mode == "skip-links":
|
||||
if line.startswith("- "):
|
||||
continue
|
||||
else:
|
||||
mode = "pre-version-table"
|
||||
print(line)
|
||||
elif mode == "pre-version-table":
|
||||
print(line)
|
||||
if line.startswith("|"):
|
||||
mode = "version-table"
|
||||
elif mode == "version-table":
|
||||
print(line)
|
||||
if line.startswith("See [the latest package documentation]"):
|
||||
mode = "after-version-table"
|
||||
elif mode == "after-version-table":
|
||||
if line.startswith("["):
|
||||
mode = "pre-contributing"
|
||||
print("")
|
||||
print(line)
|
||||
elif mode == "pre-contributing":
|
||||
if line == "Contributing":
|
||||
mode = "skip-to-bibliography"
|
||||
continue
|
||||
print(line)
|
||||
elif mode == "skip-to-bibliography":
|
||||
if line == "Bibliography":
|
||||
mode = "rest"
|
||||
print(line)
|
||||
else:
|
||||
print(line)
|
||||
|
||||
if mode != "rest":
|
||||
print(f"unexpected mode: {mode}", file=sys.stderr)
|
||||
sys.exit(1)
|
||||
EOF
|
||||
|
||||
bash <<'EOF'
|
||||
virtualenv venv
|
||||
source venv/bin/activate
|
||||
pip install "rst-to-myst"
|
||||
|
||||
mkdir -p docs/src/release-notes
|
||||
for package in concurrency dejafu hunit-dejafu tasty-dejafu; do
|
||||
rst2myst convert --no-sphinx "${package}/CHANGELOG.rst"
|
||||
cat "${package}/CHANGELOG.md" | \
|
||||
sed 'sZ{issue}`\([^`]*\)`Z[issue #\1](https://github.com/barrucadu/dejafu/issues/\1)Zg' | \
|
||||
sed 'sZ{pull}`\([^`]*\)`Z[pull request #\1](https://github.com/barrucadu/dejafu/pull/\1)Zg' | \
|
||||
sed 'sZ{tag}`\([^`]*\)`Z[\1](https://github.com/barrucadu/dejafu/releases/tag/\1)Zg' | \
|
||||
sed 'sZ{u}`\([^`]*\)`Z[\1](https://github.com/\1)Zg' | \
|
||||
sed 'sZ{hackage}`\([^`]*\)`Z[\1](https://hackage.haskell.org/package/\1)Zg' > "docs/src/release-notes/${package}.md"
|
||||
rm "${package}/CHANGELOG.md"
|
||||
done
|
||||
|
||||
rm -rf venv
|
||||
EOF
|
||||
|
||||
mdbook build docs
|
||||
mv docs/book "$OUTPUT_DIR"
|
||||
|
||||
stack --no-install-ghc --no-nix --skip-ghc-check --system-ghc haddock concurrency dejafu hunit-dejafu tasty-dejafu
|
||||
rm -rf .stack-work/install/*/*/*/doc/all/
|
||||
mv .stack-work/install/*/*/*/doc/ "$OUTPUT_DIR/packages"
|
||||
|
||||
chmod -c -R +rX "$OUTPUT_DIR" | while read -r line; do
|
||||
echo "::warning title=Invalid file permissions automatically fixed::$line"
|
||||
done
|
||||
17
.github/workflows/ci.yaml
vendored
17
.github/workflows/ci.yaml
vendored
@ -3,6 +3,23 @@ name: Run tests
|
||||
on: pull_request
|
||||
|
||||
jobs:
|
||||
check-docs-site:
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
- uses: actions/checkout@v4
|
||||
- name: Check mdbook-admonish changes are not committed
|
||||
run: |
|
||||
if grep -q "do not edit: managed by \`mdbook-admonish install\`" docs/book.toml; then
|
||||
echo "remove generated mdbook-admonish lines from docs/books.toml" >&2
|
||||
exit 1
|
||||
fi
|
||||
- name: Install nix
|
||||
uses: cachix/install-nix-action@v23
|
||||
with:
|
||||
nix_path: nixpkgs=channel:nixos-23.05
|
||||
- name: Check documentation site builds
|
||||
run: nix-shell ./.github/scripts/build-documentation.sh
|
||||
|
||||
lint:
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
|
||||
51
.github/workflows/deploy-documentation.yml
vendored
Normal file
51
.github/workflows/deploy-documentation.yml
vendored
Normal file
@ -0,0 +1,51 @@
|
||||
name: Deploy documentation site
|
||||
|
||||
on:
|
||||
# Runs on pushes targeting the default branch
|
||||
push:
|
||||
branches: ["master"]
|
||||
|
||||
# Allows you to run this workflow manually from the Actions tab
|
||||
workflow_dispatch:
|
||||
|
||||
# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
|
||||
permissions:
|
||||
contents: read
|
||||
pages: write
|
||||
id-token: write
|
||||
|
||||
# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued.
|
||||
# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete.
|
||||
concurrency:
|
||||
group: "pages"
|
||||
cancel-in-progress: false
|
||||
|
||||
jobs:
|
||||
# Build job
|
||||
build:
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
- name: Checkout
|
||||
uses: actions/checkout@v4
|
||||
- name: Setup Pages
|
||||
uses: actions/configure-pages@v3
|
||||
- name: Install nix
|
||||
uses: cachix/install-nix-action@v23
|
||||
with:
|
||||
nix_path: nixpkgs=channel:nixos-23.05
|
||||
- name: Build
|
||||
run: nix-shell ./.github/scripts/build-documentation.sh
|
||||
- name: Upload artifact
|
||||
uses: actions/upload-pages-artifact@v2
|
||||
|
||||
# Deployment job
|
||||
deploy:
|
||||
environment:
|
||||
name: github-pages
|
||||
url: ${{ steps.deployment.outputs.page_url }}
|
||||
runs-on: ubuntu-latest
|
||||
needs: build
|
||||
steps:
|
||||
- name: Deploy to GitHub Pages
|
||||
id: deployment
|
||||
uses: actions/deploy-pages@v2
|
||||
1
.gitignore
vendored
1
.gitignore
vendored
@ -4,3 +4,4 @@ dist
|
||||
.stack-work
|
||||
*.tix
|
||||
*.prof
|
||||
_site
|
||||
|
||||
@ -14,12 +14,13 @@ dejafu
|
||||
- [Release notes](#release-notes)
|
||||
- [Questions, feedback, discussion](#questions-feedback-discussion)
|
||||
- [Bibliography](#bibliography)
|
||||
- **[The website!](http://dejafu.readthedocs.io/)**
|
||||
- **[The website!](https://dejafu.docs.barrucadu.co.uk/)**
|
||||
|
||||
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][].
|
||||
to test your threaded code.
|
||||
|
||||
Available on [GitHub][], [Hackage][], and [Stackage][].
|
||||
|
||||
[GitHub]: https://github.com/barrucadu/dejafu
|
||||
[Hackage]: https://hackage.haskell.org/package/dejafu
|
||||
@ -47,6 +48,8 @@ There are a few different packages under the Déjà Fu umbrella:
|
||||
| [hunit-dejafu][h:hunit] | 2.0.0.6 | Deja Fu support for the HUnit test framework. |
|
||||
| [tasty-dejafu][h:tasty] | 2.1.0.1 | Deja Fu support for the Tasty test framework. |
|
||||
|
||||
See [the latest package documentation](https://dejafu.docs.barrucadu.co.uk/packages/).
|
||||
|
||||
Each package has its own README and CHANGELOG in its subdirectory.
|
||||
|
||||
There is also dejafu-tests, the test suite for dejafu. This is in a
|
||||
@ -162,7 +165,7 @@ the trace by eye.
|
||||
Contributing
|
||||
------------
|
||||
|
||||
See the "contributing" page on [the website](http://dejafu.readthedocs.io/en/latest/contributing.html).
|
||||
See the "contributing" page on [the website](https://dejafu.docs.barrucadu.co.uk/dev-docs/contributing.html).
|
||||
|
||||
**If you'd like to get involved with Déjà Fu**, check out [the
|
||||
"good first issue" label on the issue tracker][beginners].
|
||||
@ -193,34 +196,33 @@ 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:
|
||||
|
||||
- [BPOR] *Bounded partial-order reduction*, K. Coons, M. Musuvathi,
|
||||
and K. McKinley (2013)
|
||||
http://research.microsoft.com/pubs/202164/bpor-oopsla-2013.pdf
|
||||
- [BPOR] [Bounded partial-order reduction](http://research.microsoft.com/pubs/202164/bpor-oopsla-2013.pdf),
|
||||
K. Coons, M. Musuvathi, and K. McKinley (2013)
|
||||
|
||||
- [RDPOR] *Dynamic Partial Order Reduction for Relaxed Memory Models*,
|
||||
- [RDPOR] [Dynamic Partial Order Reduction for Relaxed Memory Models](http://www.faculty.ece.vt.edu/chaowang/pubDOC/ZhangKW15.pdf),
|
||||
N. Zhang, M. Kusano, and C. Wang (2015)
|
||||
http://www.faculty.ece.vt.edu/chaowang/pubDOC/ZhangKW15.pdf
|
||||
|
||||
- [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
|
||||
- [Empirical] [Concurrency Testing Using Schedule Bounding: an Empirical Study](http://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2014/PPoPP.pdf),
|
||||
P. Thompson, A. Donaldson, and A. Betts (2014)
|
||||
|
||||
- [RMMVerification] *On the Verification of Programs on Relaxed Memory
|
||||
Models*, A. Linden (2014)
|
||||
https://orbi.ulg.ac.be/bitstream/2268/158670/1/thesis.pdf
|
||||
- [RMMVerification] [On the Verification of Programs on Relaxed Memory Models](https://orbi.ulg.ac.be/bitstream/2268/158670/1/thesis.pdf),
|
||||
A. Linden (2014)
|
||||
|
||||
There are also a couple of papers on dejafu itself:
|
||||
There are also a few 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
|
||||
- [Déjà Fu: A Concurrency Testing Library for Haskell](https://www.barrucadu.co.uk/publications/dejafu-hs15.pdf),
|
||||
M. Walker and C. Runciman (2015)
|
||||
|
||||
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
|
||||
- [Déjà Fu: A Concurrency Testing Library for Haskell](https://www.barrucadu.co.uk/publications/YCS-2016-503.pdf),
|
||||
M. Walker and C. Runciman (2016)
|
||||
|
||||
This is a more in-depth technical report, written between the
|
||||
dejafu-0.2 and dejafu-0.3 releases.
|
||||
|
||||
- [Revealing Behaviours of Concurrent Functional Programs by Systematic Testing](https://www.barrucadu.co.uk/publications/thesis.pdf),
|
||||
M. Walker (2018)
|
||||
|
||||
This is my Ph.D thesis, which discusses dejafu and my other research projects.
|
||||
|
||||
@ -13,6 +13,7 @@ unreleased
|
||||
Miscellaneous
|
||||
~~~~~~~~~~~~~
|
||||
|
||||
* Update documentation link in ``Test.DejaFu``.
|
||||
* Fix GHC compatibility warning.
|
||||
|
||||
|
||||
|
||||
@ -14,7 +14,7 @@ dejafu
|
||||
- [Release notes](#release-notes)
|
||||
- [Questions, feedback, discussion](#questions-feedback-discussion)
|
||||
- [Bibliography](#bibliography)
|
||||
- **[The website!](http://dejafu.readthedocs.io/)**
|
||||
- **[The website!](https://dejafu.docs.barrucadu.co.uk/)**
|
||||
|
||||
Déjà Fu is a unit-testing library for concurrent Haskell programs.
|
||||
Tests are deterministic and expressive, making it easy and convenient
|
||||
|
||||
@ -13,7 +13,7 @@ are written using the <https://hackage.haskell.org/package/concurrency
|
||||
concurrency> package's 'MonadConc' typeclass.
|
||||
|
||||
For more in-depth documentation, including migration guides from
|
||||
earlier versions of dejafu, see the <https://dejafu.readthedocs.io
|
||||
earlier versions of dejafu, see the <https://dejafu.docs.barrucadu.co.uk/
|
||||
website>.
|
||||
|
||||
__A first test:__ This is a simple concurrent program which forks two
|
||||
|
||||
@ -13,7 +13,7 @@ description:
|
||||
package by enabling you to deterministically test your concurrent
|
||||
programs.
|
||||
.
|
||||
See the <https://dejafu.readthedocs.io website> or README for more.
|
||||
See the <https://dejafu.docs.barrucadu.co.uk/ website> or README for more.
|
||||
|
||||
homepage: https://github.com/barrucadu/dejafu
|
||||
license: MIT
|
||||
|
||||
9
docs/.gitignore
vendored
Normal file
9
docs/.gitignore
vendored
Normal file
@ -0,0 +1,9 @@
|
||||
book
|
||||
|
||||
# generated by the build script
|
||||
src/index.md
|
||||
src/release-notes/concurrency.md
|
||||
src/release-notes/dejafu.md
|
||||
src/release-notes/hunit-dejafu.md
|
||||
src/release-notes/tasty-dejafu.md
|
||||
mdbook-admonish.css
|
||||
17
docs/book.toml
Normal file
17
docs/book.toml
Normal file
@ -0,0 +1,17 @@
|
||||
[book]
|
||||
title = "Déjà Fu"
|
||||
authors = ["Michael Walker (barrucadu)"]
|
||||
description = "Systematic concurrency testing meets Haskell."
|
||||
language = "en"
|
||||
multilingual = false
|
||||
|
||||
[build]
|
||||
create-missing = false
|
||||
|
||||
[output.html]
|
||||
git-repository-url = "https://github.com/barrucadu/dejafu"
|
||||
cname = "dejafu.docs.barrucadu.co.uk"
|
||||
|
||||
[preprocessor.admonish]
|
||||
on_failure = "bail"
|
||||
command = "mdbook-admonish"
|
||||
25
docs/src/SUMMARY.md
Normal file
25
docs/src/SUMMARY.md
Normal file
@ -0,0 +1,25 @@
|
||||
# Summary
|
||||
|
||||
- [Getting Started](./index.md)
|
||||
- [Typeclasses](./typeclasses.md)
|
||||
- [Unit Testing](./unit-testing.md)
|
||||
- [Refinement Testing](./refinement-testing.md)
|
||||
- [Advanced Usage](./advanced-usage.md)
|
||||
|
||||
# Migration Guides
|
||||
|
||||
- [1.x to 2.x](./migration-guides/1x-2x.md)
|
||||
- [0.x to 1.x](./migration-guides/0x-1x.md)
|
||||
|
||||
# Developer Documentation
|
||||
|
||||
- [Contributing](./dev-docs/contributing.md)
|
||||
- [Supported GHC Versions](./dev-docs/supported-ghc-versions.md)
|
||||
- [Release Process](./dev-docs/release-process.md)
|
||||
|
||||
# Release Notes
|
||||
|
||||
- [concurrency](./release-notes/concurrency.md)
|
||||
- [dejafu](./release-notes/dejafu.md)
|
||||
- [hunit-dejafu](./release-notes/hunit-dejafu.md)
|
||||
- [tasty-dejafu](./release-notes/tasty-dejafu.md)
|
||||
96
docs/src/advanced-usage.md
Normal file
96
docs/src/advanced-usage.md
Normal file
@ -0,0 +1,96 @@
|
||||
Advanced Usage
|
||||
==============
|
||||
|
||||
Déjà Fu tries to have a sensible set of defaults, but there are some
|
||||
times when the defaults are not suitable. There are a lot of knobs
|
||||
provided to tweak how things work.
|
||||
|
||||
|
||||
Execution settings
|
||||
------------------
|
||||
|
||||
The `autocheckWithSettings`, `dejafuWithSettings`, and `dejafusWithSettings` let
|
||||
you provide a `Settings` value, which controls some of Déjà Fu's behaviour:
|
||||
|
||||
```haskell
|
||||
dejafuWithSettings mySettings "Assert the thing holds" myPredicate myAction
|
||||
```
|
||||
|
||||
The available settings are:
|
||||
|
||||
- **"Way"**, how to explore the behaviours of the program under test.
|
||||
|
||||
- **Length bound**, a cut-off point to terminate an execution even if it's not
|
||||
done yet.
|
||||
|
||||
- **Memory model**, which affects how non-synchronised operations, such as
|
||||
`readIORef` and `writeIORef` behave.
|
||||
|
||||
- **Discarding**, which allows throwing away uninteresting results, rather than
|
||||
keeping them around in memory.
|
||||
|
||||
- **Early exit**, which allows exiting as soon as a result matching a predicate
|
||||
is found.
|
||||
|
||||
- **Representative traces**, keeping only one execution trace for each distinct
|
||||
result.
|
||||
|
||||
- **Trace simplification**, rewriting execution traces into a simpler form
|
||||
(particularly effective with the random testing).
|
||||
|
||||
- **Safe IO**, pruning needless schedules when your IO is only used to manage
|
||||
thread-local state.
|
||||
|
||||
See the `Test.DejaFu.Settings` module for more information.
|
||||
|
||||
|
||||
Performance tuning
|
||||
------------------
|
||||
|
||||
- Are you happy to trade space for time?
|
||||
|
||||
Consider computing the results once and running multiple predicates over the
|
||||
output: this is what `dejafus` / `testDejafus` / etc does.
|
||||
|
||||
- Can you sacrifice completeness?
|
||||
|
||||
Consider using the random testing functionality. See the `*WithSettings`
|
||||
functions.
|
||||
|
||||
- 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 `*WithSettings`
|
||||
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, but you
|
||||
don't care about the execution trace, and you are going to sacrifice
|
||||
completeness because your possible state-space is huge. You could do it like
|
||||
this:
|
||||
|
||||
```haskell
|
||||
dejafuWithSettings
|
||||
( set ldiscard
|
||||
-- "efa" == "either failure a", discard everything but deadlocks
|
||||
(Just $ \efa -> Just (if either isDeadlock (const False) efa then DiscardTrace else DiscardResultAndTrace))
|
||||
. set lway
|
||||
-- try 10000 executions with random scheduling
|
||||
(randomly (mkStdGen 42) 10000)
|
||||
$ defaultSettings
|
||||
)
|
||||
-- the name of the test
|
||||
"Never Deadlocks"
|
||||
-- the predicate to check
|
||||
deadlocksNever
|
||||
-- your test case
|
||||
testCase
|
||||
```
|
||||
221
docs/src/dev-docs/contributing.md
Normal file
221
docs/src/dev-docs/contributing.md
Normal file
@ -0,0 +1,221 @@
|
||||
Contributing
|
||||
============
|
||||
|
||||
Thanks for caring about Déjà Fu!
|
||||
|
||||
|
||||
Ways to contribute
|
||||
------------------
|
||||
|
||||
Déjà Fu is a project under active development, there's always something to do.
|
||||
Here's a list of ideas to get you started:
|
||||
|
||||
- Submit bug reports.
|
||||
- Submit feature requests.
|
||||
- Got a particularly slow test case which you think should be faster? Open an
|
||||
issue for that too.
|
||||
- Blog about how and why you use Déjà Fu.
|
||||
- Check if any bugs which have been open for a while are still bugs.
|
||||
|
||||
If you want to contribute code, you could:
|
||||
|
||||
- Tackle one of the issues tagged ["good first issue"][good-first-issue].
|
||||
- Tackle a bigger issue, perhaps one of the [roadmap issues][roadmap]!
|
||||
- Run code coverage and try to fix a gap in the tests.
|
||||
- Profile the test suite and try to improve a slow function.
|
||||
|
||||
[Roadmap issues][roadmap] are priority issues (in my opinion), so help with
|
||||
those is especially appreciated.
|
||||
|
||||
If you have a support question, you can talk to me on IRC (#haskell on freenode)
|
||||
or send an email (mike@barrucadu.co.uk) rather than opening an issue. But maybe
|
||||
your question is a bug report about poor documentation in disguise!
|
||||
|
||||
[good-first-issue]: https://github.com/barrucadu/dejafu/labels/good%20first%20issue
|
||||
[roadmap]: https://github.com/barrucadu/dejafu/labels/roadmap
|
||||
|
||||
|
||||
Making the change
|
||||
-----------------
|
||||
|
||||
1. Talk to me!
|
||||
|
||||
I don't bite, and chances are I can quickly tell you where you should start.
|
||||
It's better to ask what seems like a stupid question than to waste a lot of
|
||||
time on the wrong approach.
|
||||
|
||||
2. Make the change.
|
||||
|
||||
Figure out what needs to be changed, how to change it, and do it. If you're
|
||||
fixing a bug, make sure to add a minimal reproduction to Cases.Regressions in
|
||||
dejafu-tests.
|
||||
|
||||
3. Document the change.
|
||||
|
||||
All top-level definitions should have a [Haddock][] comment explaining what
|
||||
it does. If you've added or changed a top-level function, consider
|
||||
commenting its arguments too.
|
||||
|
||||
If you've added a top-level definition, or changed one in a
|
||||
backwards-incompatible way, add an `@since unreleased` Haddock comment to it.
|
||||
This is to help prevent me from missing things when I update the changelog
|
||||
ahead of a release.
|
||||
|
||||
4. Submit a PR.
|
||||
|
||||
GitHub Actions will run some checks, which might prompt further action. You
|
||||
should expect a response from me in a day or two.
|
||||
|
||||
Don't worry about your PR being perfect the first time. We'll work through any
|
||||
issues together, to ensure that Déjà Fu gets the best code it can.
|
||||
|
||||
[Haddock]: https://hackage.haskell.org/package/haddock
|
||||
|
||||
|
||||
Coding style
|
||||
------------
|
||||
|
||||
There isn't really a prescribed style. It's not quite the wild west though;
|
||||
keep these three rules in mind:
|
||||
|
||||
1. Be consistent.
|
||||
2. Run [stylish-haskell][] to format import lists.
|
||||
3. Use [hlint][] and [weeder][] and fix lints unless you
|
||||
have a good reason not to.
|
||||
|
||||
GitHub Actions runs stylish-haskell and hlint on all PRs.
|
||||
|
||||
[stylish-haskell]: https://hackage.haskell.org/package/stylish-haskell
|
||||
[hlint]: https://hackage.haskell.org/package/hlint
|
||||
[weeder]: https://hackage.haskell.org/package/weeder
|
||||
|
||||
|
||||
Coverage
|
||||
--------
|
||||
|
||||
[hpc][] can generate a coverage report from the execution of dejafu-tests:
|
||||
|
||||
```text
|
||||
$ 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:
|
||||
|
||||
```text
|
||||
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][cov].
|
||||
|
||||
[hpc]: https://wiki.haskell.org/Haskell_program_coverage
|
||||
[cov]: https://docs.haskellstack.org/en/latest/coverage/
|
||||
|
||||
|
||||
Performance
|
||||
-----------
|
||||
|
||||
GHC can generate performance statistics from the execution of dejafu-tests:
|
||||
|
||||
```text
|
||||
$ 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:
|
||||
|
||||
```text
|
||||
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
|
||||
[...]
|
||||
```
|
||||
|
||||
Be careful, however! Compiling with profiling can significantly affect the
|
||||
behaviour of a program! Use profiling to get an idea of where the hot spots
|
||||
are, but make sure to confirm with a non-profiled build that things are actually
|
||||
getting faster.
|
||||
|
||||
If you compile with `-rtsopts` you can get some basic stats from a non-profiled
|
||||
build:
|
||||
|
||||
```text
|
||||
$ stack exec -- dejafu-tests +RTS -s
|
||||
|
||||
[...]
|
||||
86,659,658,504 bytes allocated in the heap
|
||||
13,057,037,448 bytes copied during GC
|
||||
13,346,952 bytes maximum residency (4743 sample(s))
|
||||
127,824 bytes maximum slop
|
||||
37 MB total memory in use (0 MB lost due to fragmentation)
|
||||
|
||||
Tot time (elapsed) Avg pause Max pause
|
||||
Gen 0 78860 colls, 0 par 32.659s 32.970s 0.0004s 0.0669s
|
||||
Gen 1 4743 colls, 0 par 3.043s 3.052s 0.0006s 0.0086s
|
||||
|
||||
TASKS: 174069 (174065 bound, 4 peak workers (4 total), using -N1)
|
||||
|
||||
SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)
|
||||
|
||||
INIT time 0.001s ( 0.001s elapsed)
|
||||
MUT time 98.685s (101.611s elapsed)
|
||||
GC time 35.702s ( 36.022s elapsed)
|
||||
EXIT time 0.001s ( 0.007s elapsed)
|
||||
Total time 134.388s (137.640s elapsed)
|
||||
|
||||
Alloc rate 878,145,635 bytes per MUT second
|
||||
|
||||
Productivity 73.4% of total user, 73.8% of total elapsed
|
||||
```
|
||||
|
||||
|
||||
Heap profiling
|
||||
--------------
|
||||
|
||||
GHC can tell you where the memory is going:
|
||||
|
||||
```text
|
||||
$ stack build --profile
|
||||
$ stack exec -- dejafu-tests +RTS -hc
|
||||
$ hp2ps -c dejafu-tests.hp
|
||||
```
|
||||
|
||||
This will produce a graph of memory usage over time, as a postscript file,
|
||||
broken down by cost-centre which produced the data. There are a few different
|
||||
views:
|
||||
|
||||
- `-hm` breaks down the graph by module
|
||||
- `-hd` breaks down the graph by closure description
|
||||
- `-hy` breaks down the graph by type
|
||||
|
||||
I typically find `-hd` and `-hy` most useful. If you're feeling particularly
|
||||
brave, you can try `-hr`, which is intended to help track down memory leaks
|
||||
caused by unevaluated thunks.
|
||||
61
docs/src/dev-docs/release-process.md
Normal file
61
docs/src/dev-docs/release-process.md
Normal file
@ -0,0 +1,61 @@
|
||||
Release Process
|
||||
===============
|
||||
|
||||
```admonish warning
|
||||
If it's early in the year, make sure you put down the right year in the CHANGELOG!
|
||||
```
|
||||
|
||||
1. Figure out what the next version number is. See the PVP_ page if unsure.
|
||||
|
||||
2. Update version numbers in the relevant cabal files:
|
||||
|
||||
* Update the `version` field
|
||||
* Update the `tag` in the `source-repository` block
|
||||
|
||||
3. Fill in all `@since unreleased` Haddock comments with the relevant version
|
||||
number.
|
||||
|
||||
4. Update version numbers in the tables in the README page.
|
||||
|
||||
5. Ensure the relevant CHANGELOG files have all the entries they should.
|
||||
|
||||
6. Add the release information to the relevant CHANGELOG files:
|
||||
|
||||
* Change the `unreleased` title to the version number
|
||||
* Add the current date
|
||||
* Add the git tag name
|
||||
* Add the Hackage URL
|
||||
* Add the contributors list
|
||||
|
||||
7. Commit.
|
||||
|
||||
8. Push to GitHub and wait for GitHub Actions to confirm everything is
|
||||
OK. If it's not OK, fix what is broken before continuing.
|
||||
|
||||
9. Merge the PR.
|
||||
|
||||
10. Tag the merge commit. Tags are in the form `<package>-<version>`, and the
|
||||
message is the changelog entry.
|
||||
|
||||
11. Push tags to GitHub.
|
||||
|
||||
When the merge commit successfully builds on `master` the updated packages will
|
||||
be pushed to Hackage by Concourse.
|
||||
|
||||
|
||||
Pro tips
|
||||
--------
|
||||
|
||||
* If a release would have a combination of breaking and non-breaking changes, if
|
||||
possible make two releases: the non-breaking ones first, and then a major
|
||||
release with the breaking ones.
|
||||
|
||||
This makes it possible for users who don't want the breaking changes to still
|
||||
benefit from the non-breaking improvements.
|
||||
|
||||
* Before uploading to Hackage, check you have no changes to the files (for
|
||||
example, temporarily changing the GHC options, or adding `trace` calls, for
|
||||
debugging reasons).
|
||||
|
||||
`stack upload` will upload the files on the disk, not the files in version
|
||||
control, so your unwanted changes will be published!
|
||||
70
docs/src/dev-docs/supported-ghc-versions.md
Normal file
70
docs/src/dev-docs/supported-ghc-versions.md
Normal file
@ -0,0 +1,70 @@
|
||||
Supported GHC Versions
|
||||
======================
|
||||
|
||||
Déjà Fu supports the latest four GHC releases, at least. For testing purposes,
|
||||
we use Stackage snapshots as a proxy for GHC versions. The currently supported
|
||||
versions are:
|
||||
|
||||
| GHC | Stackage | base |
|
||||
| --- | -------- | ---- |
|
||||
| 9.6 | Nightly 2021-07-01 | 4.18.0.0 |
|
||||
| 9.4 | LTS 21.0 | 4.17.0.0 |
|
||||
| 9.2 | LTS 20.0 | 4.16.0.0 |
|
||||
| 9.0 | LTS 19.0 | 4.15.0.0 |
|
||||
| 8.1 |,LTS 17.0 | 4.14.1.0 |
|
||||
| 8.8 | LTS 15.0 | 4.13.0.0 |
|
||||
| 8.6 | LTS 14.0 | 4.12.0.0 |
|
||||
| 8.4 | LTS 12.0 | 4.11.0.0 |
|
||||
| 8.2 | LTS 10.0 | 4.10.1.0 |
|
||||
|
||||
In practice, we may *compile with* older versions of GHC, but keeping them
|
||||
working is not a priority.
|
||||
|
||||
|
||||
Adding new GHC releases
|
||||
-----------------------
|
||||
|
||||
When a new version of GHC is released, we need to make some changes for
|
||||
everything to go smoothly. In general, these changes should only cause a
|
||||
**patch level version bump**.
|
||||
|
||||
1. Bump the upper bound of [base][] and set up any needed conditional
|
||||
compilation
|
||||
2. Add the GHC and base versions to the table.
|
||||
3. Remove any unsupported versions from the table.
|
||||
4. Make a patch release.
|
||||
|
||||
A new GHC release won't get a Stackage snapshot for little while. When it
|
||||
does:
|
||||
|
||||
1. Add the snapshot to the GitHub Actions configuration.
|
||||
2. Update the resolver in the stack.yaml.
|
||||
3. Put the snapshot in the table.
|
||||
|
||||
|
||||
Dropping old GHC releases
|
||||
-------------------------
|
||||
|
||||
When we want to drop an unsupported version of GHC, we need to bump the version
|
||||
bound on [base][] to preclude it. This is a backwards-incompatible change which
|
||||
causes a **major version bump**.
|
||||
|
||||
1. Remove the dropped GHC version from the GitHub Actions configuration.
|
||||
2. Bump the lower bound of [base][].
|
||||
3. Look through the other dependencies. Some may not work with our new lower
|
||||
bound on [base][], so we should bump those too.
|
||||
4. Remove any now-irrelevant conditional compilation (mostly CPP, but there may
|
||||
also be some cabal file bits).
|
||||
5. Make whatever change required the bump.
|
||||
6. Make a major release.
|
||||
|
||||
GHC versions shouldn't be dropped just because we can, but here are some good
|
||||
reasons to do it:
|
||||
|
||||
- We want to bump the lower bounds of a dependency to a version which doesn't
|
||||
support that GHC.
|
||||
- We want to add a new dependency which doesn't support that GHC.
|
||||
- The conditional compilation needed to keep that GHC working is getting
|
||||
confusing.
|
||||
|
||||
[base]: https://hackage.haskell.org/package/base
|
||||
122
docs/src/migration-guides/0x-1x.md
Normal file
122
docs/src/migration-guides/0x-1x.md
Normal file
@ -0,0 +1,122 @@
|
||||
0.x to 1.x
|
||||
==========
|
||||
|
||||
[dejafu-1.0.0.0][] is a super-major release which breaks compatibility with
|
||||
[dejafu-0.x][] quite significantly, but brings with it support for bound
|
||||
threads, and significantly improves memory usage in the general case.
|
||||
|
||||
Highlights reel:
|
||||
|
||||
- Most predicates now only need to keep around the failures, rather than all
|
||||
results.
|
||||
- Support for bound threads (with [concurrency-1.3.0.0][]).
|
||||
- The `ST` / `IO` interface duplication is gone, everything is now monadic.
|
||||
- Function parameter order is closer to other testing libraries.
|
||||
- Much improved API documentation.
|
||||
|
||||
See the changelogs for the full details.
|
||||
|
||||
|
||||
`ST` and `IO` functions
|
||||
-----------------------
|
||||
|
||||
There is only one set of functions now. Testing bound threads requires being
|
||||
able to fork actual threads, so testing with `ST` is no longer possible. The
|
||||
`ConcST` type is gone, there is only `ConcIO`.
|
||||
|
||||
For [dejafu][] change:
|
||||
|
||||
- `autocheckIO` to `autocheck`
|
||||
- `dejafuIO` to `dejafu`
|
||||
- `dejafusIO` to `dejafus`
|
||||
- `autocheckWayIO` to `autocheckWay`
|
||||
- `dejafuWayIO` to `dejafuWay`
|
||||
- `dejafusWayIO` to `dejafusWay`
|
||||
- `dejafuDiscardIO` to `dejafuDiscard`
|
||||
- `runTestM` to `runTest`
|
||||
- `runTestWayM` to `runTestWay`
|
||||
|
||||
If you relied on being able to get a pure result from the `ConcST` functions,
|
||||
you can no longer do this.
|
||||
|
||||
For [hunit-dejafu][] and [tasty-dejafu][] change:
|
||||
|
||||
- `testAutoIO` to `testAuto`
|
||||
- `testDejafuIO` to `testDejafu`
|
||||
- `testDejafusIO` to `testDejafus`
|
||||
- `testAutoWayIO` to `testAutoWay`
|
||||
- `testDejafuWayIO` to `testDejafuWay`
|
||||
- `testDejafusWayIO` to `testDejafusWay`
|
||||
- `testDejafuDiscardIO` to `testDejafuDiscard`
|
||||
|
||||
|
||||
Function parameter order
|
||||
------------------------
|
||||
|
||||
Like [HUnit][], the monadic action to test is now the last parameter of the
|
||||
testing functions. This makes it convenient to write tests without needing to
|
||||
define the action elsewhere.
|
||||
|
||||
For [dejafu][] change:
|
||||
|
||||
- `dejafu ma (s, p)` to `dejafu s p ma`
|
||||
- `dejafus ma ps` to `dejafus ps ma`
|
||||
- `dejafuWay way mem ma (s, p)` to `dejafuWay way mem s p ma`
|
||||
- `dejafusWay way mem ma ps` to `dejafuWay way mem ps ma`
|
||||
- `dejafuDiscard d way mem ma (s, p)` to `dejafuDiscard d way mem s p ma`
|
||||
|
||||
For [hunit-dejafu][] and [tasty-dejafu][] change:
|
||||
|
||||
- `testDejafu ma s p` to `testDejafu s p ma`
|
||||
- `testDejafus ma ps` to `testDejafus ps ma`
|
||||
- `testDejafuWay way mem ma s p` to `testDejafuWay way mem s p ma`
|
||||
- `testDejafusWay way mem ma ps` to `testDejafusWay way mem ps ma`
|
||||
- `testDejafuDiscard d way mem ma s p` to `testDejafuDiscard d way mem s p ma`
|
||||
|
||||
|
||||
Predicates
|
||||
----------
|
||||
|
||||
The `Predicate a` type is now an alias for `ProPredicate a a`, defined like so:
|
||||
|
||||
```haskell
|
||||
data ProPredicate a b = ProPredicate
|
||||
{ pdiscard :: Either Failure a -> Maybe Discard
|
||||
-- ^ Selectively discard results before computing the result.
|
||||
, peval :: [(Either Failure a, Trace)] -> Result b
|
||||
-- ^ Compute the result with the un-discarded results.
|
||||
}
|
||||
```
|
||||
|
||||
If you use the predicate helper functions to construct a predicate, you do not
|
||||
need to change anything (and should get a nice reduction in your resident memory
|
||||
usage). If you supply a function directly, you can recover the old behaviour
|
||||
like so:
|
||||
|
||||
```haskell
|
||||
old :: ([(Either Failure a, Trace)] -> Result a) -> ProPredicate a a
|
||||
old p = ProPredicate
|
||||
{ pdiscard = const Nothing
|
||||
, peval = p
|
||||
}
|
||||
```
|
||||
|
||||
The `alwaysTrue2` helper function is gone. If you use it, use `alwaysSameOn` or
|
||||
`alwaysSameBy` instead.
|
||||
|
||||
|
||||
Need help?
|
||||
----------
|
||||
|
||||
- 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][].
|
||||
|
||||
[dejafu-1.0.0.0]: https://hackage.haskell.org/package/dejafu-1.0.0.0
|
||||
[dejafu-0.x]: https://hackage.haskell.org/package/dejafu-0.9.1.1
|
||||
[concurrency-1.3.0.0]: https://hackage.haskell.org/package/concurrency-1.3.0.0
|
||||
[dejafu]: https://hackage.haskell.org/package/dejafu
|
||||
[hunit-dejafu]: https://hackage.haskell.org/package/hunit-dejafu
|
||||
[tasty-dejafu]: https://hackage.haskell.org/package/tasty-dejafu
|
||||
[HUnit]: https://hackage.haskell.org/package/HUnit
|
||||
[file an issue]: https://github.com/barrucadu/dejafu/issues/
|
||||
117
docs/src/migration-guides/1x-2x.md
Normal file
117
docs/src/migration-guides/1x-2x.md
Normal file
@ -0,0 +1,117 @@
|
||||
1.x to 2.x
|
||||
==========
|
||||
|
||||
[dejafu-2.0.0.0][] is a super-major release which breaks compatibility with
|
||||
[dejafu-1.x][].
|
||||
|
||||
Highlights reel:
|
||||
|
||||
- Test cases are written in terms of a new `Program` type.
|
||||
- The `Failure` type has been replaced with a `Condition` type (actually in
|
||||
1.12).
|
||||
- Random testing takes an optional length bound.
|
||||
- Atomically-checked invariants over shared mutable state.
|
||||
|
||||
See the changelogs for the full details.
|
||||
|
||||
|
||||
The `Program` type
|
||||
------------------
|
||||
|
||||
The `ConcT` type is now an alias for `Program Basic`.
|
||||
|
||||
A `Program Basic` has all the instances `ConcT` did, defined using the `~`
|
||||
instance trick, so this shouldn't be a breaking change:
|
||||
|
||||
```haskell
|
||||
instance (pty ~ Basic) => MonadTrans (Program pty)
|
||||
instance (pty ~ Basic) => MonadCatch (Program pty n)
|
||||
instance (pty ~ Basic) => MonadThrow (Program pty n)
|
||||
instance (pty ~ Basic) => MonadMask (Program pty n)
|
||||
instance (pty ~ Basic, Monad n) => MonadConc (Program pty n)
|
||||
instance (pty ~ Basic, MonadIO n) => MonadIO (Program pty n)
|
||||
```
|
||||
|
||||
The `dontCheck` function has been removed in favour of `withSetup`:
|
||||
|
||||
```haskell
|
||||
do x <- dontCheck setup
|
||||
action x
|
||||
|
||||
-- becomes
|
||||
|
||||
withSetup setup action
|
||||
```
|
||||
|
||||
The `subconcurrency` function has been removed in favour of
|
||||
`withSetupAndTeardown`:
|
||||
|
||||
```haskell
|
||||
do x <- setup
|
||||
y <- subconcurrency (action x)
|
||||
teardown x y
|
||||
|
||||
-- becomes
|
||||
|
||||
withSetupAndTeardown setup teardown action
|
||||
```
|
||||
|
||||
The `dontCheck` and `subconcurrency` functions used to throw runtime errors if
|
||||
nested. This is not possible with `withSetup` and `withSetupAndTeardown` due to
|
||||
their types:
|
||||
|
||||
```haskell
|
||||
withSetup
|
||||
:: Program Basic n x
|
||||
-- ^ Setup action
|
||||
-> (x -> Program Basic n a)
|
||||
-- ^ Main program
|
||||
-> Program (WithSetup x) n a
|
||||
|
||||
withSetupAndTeardown
|
||||
:: Program Basic n x
|
||||
-- ^ Setup action
|
||||
-> (x -> Either Condition y -> Program Basic n a)
|
||||
-- ^ Teardown action
|
||||
-> (x -> Program Basic n y)
|
||||
-- ^ Main program
|
||||
-> Program (WithSetupAndTeardown x y) n a
|
||||
```
|
||||
|
||||
Previously, multiple calls to `subconcurrency` could be sequenced in the same
|
||||
test case. This is not possible using `withSetupAndTeardown`. If you rely on
|
||||
this behaviour, please [file an issue][].
|
||||
|
||||
|
||||
The `Condition` type
|
||||
--------------------
|
||||
|
||||
This is a change in [dejafu-1.12.0.0][dejafu-1.x], but the alias `Failure =
|
||||
Condition` is removed in [dejafu-2.0.0.0][].
|
||||
|
||||
- The `STMDeadlock` and `Deadlock` constructors have been merged.
|
||||
- Internal errors have been split into the `Error` type and are raised as
|
||||
exceptions, instead of being returned as conditions.
|
||||
|
||||
The name "failure" has been a recurring source of confusion, because an
|
||||
individual execution can "fail" without the predicate as a whole failing. My
|
||||
hope is that the more neutral "condition" will prevent this confusion.
|
||||
|
||||
|
||||
Deprecated functions
|
||||
--------------------
|
||||
|
||||
All the deprecated special-purpose functions have been removed. Use more
|
||||
general `*WithSettings` functions instead.
|
||||
|
||||
|
||||
Need help?
|
||||
----------
|
||||
|
||||
- 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][].
|
||||
|
||||
[dejafu-2.0.0.0]: https://hackage.haskell.org/package/dejafu-2.0.0.0
|
||||
[dejafu-1.x]: https://hackage.haskell.org/package/dejafu-1.12.0.0
|
||||
[file an issue]: https://github.com/barrucadu/dejafu/issues/
|
||||
148
docs/src/refinement-testing.md
Normal file
148
docs/src/refinement-testing.md
Normal file
@ -0,0 +1,148 @@
|
||||
Refinement Testing
|
||||
==================
|
||||
|
||||
Déjà Fu also supports a form of property-testing where you can check things
|
||||
about the side-effects of stateful operations. For example, we can assert that
|
||||
`readMVar` is equivalent to sequencing `takeMVar` and `putMVar` like so:
|
||||
|
||||
```haskell
|
||||
prop_mvar_read_take_put =
|
||||
sig readMVar `equivalentTo` sig (\v -> takeMVar v >>= putMVar v)
|
||||
```
|
||||
|
||||
Given the signature function, `sig`, defined in the next section. If we check
|
||||
this, our property fails!
|
||||
|
||||
```text
|
||||
> check prop_mvar_read_take_put
|
||||
*** Failure: (seed Just 0)
|
||||
left: [(Nothing,Just 0)]
|
||||
right: [(Nothing,Just 0),(Just Deadlock,Just 0)]
|
||||
False
|
||||
```
|
||||
|
||||
This is because `readMVar` is atomic, whereas sequencing `takeMVar` with
|
||||
`putMVar` is not, and so another thread can interfere with the `MVar` in the
|
||||
middle. The `check` and `equivalentTo` functions come from
|
||||
`Test.DejaFu.Refinement` (also re-exported from `Test.DejaFu`).
|
||||
|
||||
|
||||
Signatures
|
||||
----------
|
||||
|
||||
A signature tells the property-tester something about the state your operation
|
||||
acts upon, it has a few components:
|
||||
|
||||
```haskell
|
||||
data Sig s o x = Sig
|
||||
{ initialise :: x -> ConcIO s
|
||||
, observe :: s -> x -> ConcIO o
|
||||
, interfere :: s -> x -> ConcIO ()
|
||||
, expression :: s -> ConcIO ()
|
||||
}
|
||||
```
|
||||
|
||||
- `s` is the **state type**, it's the thing which your operations mutate. For
|
||||
`readMVar`, the state is some `MVar a`.
|
||||
|
||||
- `o` is the **observation type**, it's some pure (and comparable) proxy for a
|
||||
snapshot of your mutable state. For `MVar a`, the observation is probably a
|
||||
`Maybe a`.
|
||||
|
||||
- `x` is the **seed type**, it's some pure value used to construct the initial
|
||||
mutable state. For `MVar a`, the seed is probably a `Maybe a`.
|
||||
|
||||
- `ConcIO` is just one of the instances of `MonadConc` that Déjà Fu defines for
|
||||
testing purposes. Just write code polymorphic in the monad as usual, and all
|
||||
will work.
|
||||
|
||||
The `initialise`, `observe`, and `expression` functions should be
|
||||
self-explanatory, but the `interfere` one may not be. It's the job of the
|
||||
`interfere` function to change the state in some way; it's run concurrently with
|
||||
the expression, to simulate the nondeterministic action of other threads.
|
||||
|
||||
Here's a concrete example for our `MVar` example:
|
||||
|
||||
```haskell
|
||||
sig :: (MVar ConcIO Int -> ConcIO a) -> Sig (MVar ConcIO Int) (Maybe Int) (Maybe Int)
|
||||
sig e = Sig
|
||||
{ initialise = maybe newEmptyMVar newMVar
|
||||
, observe = \v _ -> tryTakeMVar v
|
||||
, interfere = \v s -> tryTakeMVar v >> maybe (pure ()) (\x -> void $ tryPutMVar v (x * 1000)) s
|
||||
, expression = void . e
|
||||
}
|
||||
```
|
||||
|
||||
The `observe` function should be deterministic, but as it is run after the
|
||||
normal execution ends, it may have side-effects on the state. The `interfere`
|
||||
function can do just about anything (there are probably some concrete rules for
|
||||
a good function, but I haven't figured them out yet), but a poor one may result
|
||||
in the property-checker being unable to distinguish between atomic and nonatomic
|
||||
expressions.
|
||||
|
||||
|
||||
Properties
|
||||
----------
|
||||
|
||||
A property is a pair of signatures linked by one of three provided
|
||||
functions. These functions are:
|
||||
|
||||
| Function | Operator | Checks that... |
|
||||
| - | - | - |
|
||||
| `equivalentTo` | `===` | ... the left and right have exactly the same behaviours |
|
||||
| `refines` | `=>=` | ... every behaviour of the left is also a behaviour of the right |
|
||||
| `strictlyRefines` | `->-` | ... `left =>= right` holds but `left === right` does not |
|
||||
|
||||
The signatures can have different state types, as long as the seed and
|
||||
observation types are the same. This lets you compare different implementations
|
||||
of the same idea: for example, comparing a concurrent stack implemented using
|
||||
`MVar` with one implemented using `IORef`.
|
||||
|
||||
Properties can have parameters, given in the obvious way:
|
||||
|
||||
```haskell
|
||||
check $ \a b c -> sig1 ... `op` sig2 ...
|
||||
```
|
||||
|
||||
Under the hood, seed and parameter values are generated using the [leancheck][]
|
||||
package, an enumerative property-based testing library. This means that any
|
||||
types you use will need to have a `Listable` instance.
|
||||
|
||||
You can also think about the three functions in terms of sets of results, where
|
||||
a result is a `(Maybe Failure, o)` value. A `Failure` is something like
|
||||
deadlocking, or being killed by an exception; `o` is the observation type. An
|
||||
observation is always made, even if execution of the expression fails.
|
||||
|
||||
| Function | Result-set operation |
|
||||
| - | - |
|
||||
| `refines` | For all seed and parameter assignments, subset-or-equal |
|
||||
| `strictlyRefines` | For at least one seed and parameter assignment, proper subset; for all others, subset-or-equal |
|
||||
| `equivalentTo` | For all seed and parameter assignments, equality |
|
||||
|
||||
Finally, there is an `expectFailure` function, which inverts the expected result
|
||||
of a property.
|
||||
|
||||
The Déjà Fu testsuite has [a collection of refinement properties][], which may
|
||||
help you get a feel for this sort of testing.
|
||||
|
||||
[leancheck]: https://hackage.haskell.org/package/leancheck
|
||||
[a collection of refinement properties]: https://github.com/barrucadu/dejafu/blob/2a15549d97c2fa12f5e8b92ab918fdb34da78281/dejafu-tests/Cases/Refinement.hs
|
||||
|
||||
|
||||
Using HUnit and Tasty
|
||||
---------------------
|
||||
|
||||
As for unit testing, [HUnit][] and [tasty][] integration is provided for
|
||||
refinement testing in the [hunit-dejafu][] and [tasty-dejafu][] packages.
|
||||
|
||||
The `testProperty` function is used to check properties. Our example from the
|
||||
start becomes:
|
||||
|
||||
```haskell
|
||||
testProperty "Read is equivalent to Take then Put" prop_mvar_read_take_put
|
||||
```
|
||||
|
||||
[HUnit]: https://hackage.haskell.org/package/HUnit
|
||||
[tasty]: https://hackage.haskell.org/package/tasty
|
||||
[hunit-dejafu]: https://hackage.haskell.org/package/hunit-dejafu
|
||||
[tasty-dejafu]: https://hackage.haskell.org/package/tasty-dejafu
|
||||
115
docs/src/typeclasses.md
Normal file
115
docs/src/typeclasses.md
Normal file
@ -0,0 +1,115 @@
|
||||
Typeclasses
|
||||
===========
|
||||
|
||||
We don't use the regular `Control.Concurrent` and `Control.Exception` modules,
|
||||
we use typeclass-generalised ones instead from the [concurrency][h:conc] and
|
||||
[exceptions][h:exc] packages.
|
||||
|
||||
[h:conc]: https://hackage.haskell.org/package/concurrency
|
||||
[h:exc]: https://hackage.haskell.org/package/exceptions
|
||||
|
||||
|
||||
Porting guide
|
||||
-------------
|
||||
|
||||
If you want to test some existing code, you'll need to port it to the
|
||||
appropriate typeclass. The typeclass is necessary, because we can't peek inside
|
||||
`IO` and `STM` values, so we need to able to plug in an alternative
|
||||
implementation when testing.
|
||||
|
||||
Fortunately, this tends to be a fairly mechanical and type-driven process:
|
||||
|
||||
1. Import `Control.Concurrent.Classy.*` instead of `Control.Concurrent.*`
|
||||
|
||||
2. Import `Control.Monad.Catch` instead of `Control.Exception`
|
||||
|
||||
3. Change your monad type:
|
||||
|
||||
- `IO a` becomes `MonadConc m => m a`
|
||||
- `STM a` becomes `MonadSTM stm => stm a`
|
||||
|
||||
4. Parameterise your state types by the monad:
|
||||
|
||||
- `TVar` becomes `TVar stm`
|
||||
- `MVar` becomes `MVar m`
|
||||
- `IORef` becomes `IORef m`
|
||||
|
||||
5. Some functions are renamed:
|
||||
|
||||
- `forkIO*` becomes `fork*`
|
||||
- `atomicModifyIORefCAS` becomes `modifyIORefCAS*`
|
||||
|
||||
6. Fix the type errors
|
||||
|
||||
If you're lucky enough to be starting a new concurrent Haskell project, you can
|
||||
just program against the `MonadConc` interface.
|
||||
|
||||
|
||||
What if I really need I/O?
|
||||
--------------------------
|
||||
|
||||
You can use `MonadIO` and `liftIO` with `MonadConc`, for instance if you need to
|
||||
talk to a database (or just use some existing library which needs real I/O).
|
||||
|
||||
To test `IO`-using code, there are some rules you need to follow:
|
||||
|
||||
1. Given the same set of scheduling decisions, your `IO` code must be
|
||||
deterministic (see below).
|
||||
|
||||
2. As dejafu can't inspect `IO` values, they should be kept small; otherwise
|
||||
dejafu may miss buggy interleavings.
|
||||
|
||||
3. You absolutely cannot block on the action of another thread inside `IO`, or
|
||||
the test execution will just deadlock.
|
||||
|
||||
```admonish tip
|
||||
Deterministic `IO` is only essential if you're using the systematic testing (the
|
||||
default). Nondeterministic `IO` won't break the random testing, it'll just make
|
||||
things more confusing.
|
||||
```
|
||||
|
||||
|
||||
Deriving your own instances
|
||||
---------------------------
|
||||
|
||||
There are `MonadConc` and `MonadSTM` instances for many common monad
|
||||
transformers. In the simple case, where you want an instance for a newtype
|
||||
wrapper around a type that has an instance, you may be able to derive it. For
|
||||
example:
|
||||
|
||||
```haskell
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
data Env = Env
|
||||
|
||||
newtype MyMonad m a = MyMonad { runMyMonad :: ReaderT Env m a }
|
||||
deriving (Functor, Applicative, Monad)
|
||||
|
||||
deriving instance MonadThrow m => MonadThrow (MyMonad m)
|
||||
deriving instance MonadCatch m => MonadCatch (MyMonad m)
|
||||
deriving instance MonadMask m => MonadMask (MyMonad m)
|
||||
|
||||
deriving instance MonadConc m => MonadConc (MyMonad m)
|
||||
```
|
||||
|
||||
`MonadSTM` needs a slightly different set of classes:
|
||||
|
||||
```haskell
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
data Env = Env
|
||||
|
||||
newtype MyMonad m a = MyMonad { runMyMonad :: ReaderT Env m a }
|
||||
deriving (Functor, Applicative, Monad, Alternative, MonadPlus)
|
||||
|
||||
deriving instance MonadThrow m => MonadThrow (MyMonad m)
|
||||
deriving instance MonadCatch m => MonadCatch (MyMonad m)
|
||||
|
||||
deriving instance MonadSTM m => MonadSTM (MyMonad m)
|
||||
```
|
||||
|
||||
Don't be put off by the use of `UndecidableInstances`, it's safe here.
|
||||
240
docs/src/unit-testing.md
Normal file
240
docs/src/unit-testing.md
Normal file
@ -0,0 +1,240 @@
|
||||
Unit Testing
|
||||
============
|
||||
|
||||
Writing tests with Déjà Fu is a little different to traditional unit testing, as
|
||||
your test case may have multiple results. A "test" is a combination of your
|
||||
code, and a predicate which says something about the set of allowed results.
|
||||
|
||||
Most tests will look something like this:
|
||||
|
||||
```haskell
|
||||
dejafu "Assert the thing holds" myPredicate myAction
|
||||
```
|
||||
|
||||
The `dejafu` function comes from `Test.DejaFu`. Another useful function is
|
||||
`dejafuWithSettings` (see [Advanced Usage](./advanced-usage.md)).
|
||||
|
||||
|
||||
Actions
|
||||
-------
|
||||
|
||||
An action is just something with the type `MonadConc m => m a`, or `(MonadConc
|
||||
m, MonadIO m) => m a` for some `a` that your chosen predicate can deal with.
|
||||
|
||||
For example, some users on Reddit found a couple of apparent bugs in the
|
||||
[auto-update][h:auto] package a while ago ([thread here][auto-thread]). As the
|
||||
package is simple and self-contained, I translated it to the `MonadConc`
|
||||
abstraction and wrote a couple of tests to replicate the bugs. Here they are:
|
||||
|
||||
```haskell
|
||||
deadlocks :: MonadConc m => m ()
|
||||
deadlocks = do
|
||||
auto <- mkAutoUpdate defaultUpdateSettings
|
||||
auto
|
||||
|
||||
nondeterministic :: forall m. MonadConc m => m Int
|
||||
nondeterministic = do
|
||||
var <- newIORef 0
|
||||
let settings = (defaultUpdateSettings :: UpdateSettings m ())
|
||||
{ updateAction = atomicModifyIORef var (\x -> (x+1, x)) }
|
||||
auto <- mkAutoUpdate settings
|
||||
auto
|
||||
auto
|
||||
```
|
||||
|
||||
These actions action could be tested with `autocheck`, and the issues would be
|
||||
revealed. The use of `ScopedTypeVariables` in the second is an unfortunate
|
||||
example of what can happen when everything becomes more polymorphic. But other
|
||||
than that, note how there is no special mention of Déjà Fu in the actions: it's
|
||||
just normal concurrent Haskell, simply written against a different interface.
|
||||
|
||||
The modified package is included [in the test suite][], if you want to see the
|
||||
full code.
|
||||
|
||||
```admonish note
|
||||
The predicates in dejafu-tests are a little confusing, as they're the opposite
|
||||
of what you would normally write! These predicates are checking that the bug is
|
||||
found, not that the code is correct.
|
||||
```
|
||||
|
||||
If the RTS supports bound threads (the `-threaded` flag was passed to GHC when
|
||||
linking), then the main thread of an action given to Déjà Fu will be bound, and
|
||||
further bound threads can be forked with the `forkOS` functions. If not, then
|
||||
attempting to fork a bound thread will raise an error.
|
||||
|
||||
[h:auto]: https://hackage.haskell.org/package/auto-update
|
||||
[auto-thread]: https://www.reddit.com/r/haskell/comments/2i5d7m/updating_autoupdate/
|
||||
[in the test suite]: https://github.com/barrucadu/dejafu/blob/2a15549d97c2fa12f5e8b92ab918fdb34da78281/dejafu-tests/Examples/AutoUpdate.hs
|
||||
|
||||
|
||||
Conditions
|
||||
----------
|
||||
|
||||
When a concurrent program of type `MonadConc m => m a` is executed, it may
|
||||
produce a value of type `a`, or it may experience a **condition** such as
|
||||
deadlock.
|
||||
|
||||
A condition does not necessarily cause your test to fail. It's important to be
|
||||
aware of what exactly your test is testing, to avoid drawing the wrong
|
||||
conclusions from a passing (or failing) test.
|
||||
|
||||
|
||||
Setup and Teardown
|
||||
------------------
|
||||
|
||||
Because dejafu drives the execution of the program under test, there are some
|
||||
tricks available to you which are not possible using normal concurrent Haskell.
|
||||
|
||||
If your test does some set-up work which is required for your test to work, but
|
||||
which is not the actual thing you are testing, you can define that as a **setup
|
||||
action**:
|
||||
|
||||
```haskell
|
||||
withSetup
|
||||
:: Program Basic n x
|
||||
-- ^ Setup action
|
||||
-> (x -> Program Basic n a)
|
||||
-- ^ Main program
|
||||
-> Program (WithSetup x) n a
|
||||
```
|
||||
|
||||
dejafu will save the state at the end of the setup action, and efficiently
|
||||
restore that state in subsequent runs of the same test with a different
|
||||
schedule. This can be much more efficient than dejafu running the setup action
|
||||
normally every single time.
|
||||
|
||||
If you want to examine some state you created in your setup action even if your
|
||||
actual test case deadlocks or something, you can define a **teardown action**:
|
||||
|
||||
```haskell
|
||||
withSetupAndTeardown
|
||||
:: Program Basic n x
|
||||
-- ^ Setup action
|
||||
-> (x -> Either Condition y -> Program Basic n a)
|
||||
-- ^ Teardown action
|
||||
-> (x -> Program Basic n y)
|
||||
-- ^ Main program
|
||||
-> Program (WithSetupAndTeardown x y) n a
|
||||
```
|
||||
|
||||
The teardown action is always executed.
|
||||
|
||||
Finally, if you want to ensure that some invariant holds over some shared state,
|
||||
you can define invariants in the setup action, which are checked atomically
|
||||
during the main action:
|
||||
|
||||
```haskell
|
||||
-- slightly contrived example
|
||||
let setup = do
|
||||
var <- newEmptyMVar
|
||||
registerInvariant $ do
|
||||
value <- inspectMVar var
|
||||
when (x == Just 1) (throwM Overflow)
|
||||
pure var
|
||||
in withSetup setup $ \var -> do
|
||||
fork $ putMVar var 0
|
||||
fork $ putMVar var 1
|
||||
tryReadMVar var
|
||||
```
|
||||
|
||||
If the main action violates the invariant, it is terminated with an
|
||||
`InvariantFailure` condition, and any teardown action is run.
|
||||
|
||||
|
||||
Predicates
|
||||
----------
|
||||
|
||||
There are a few predicates built in, and some helpers to define your own.
|
||||
|
||||
|
||||
| | |
|
||||
| - | - |
|
||||
| `abortsNever` | checks that the computation never aborts |
|
||||
| `abortsAlways` | checks that the computation always aborts |
|
||||
| `abortsSometimes` | checks that the computation aborts at least once |
|
||||
|
||||
An **abort** is where the scheduler chooses to terminate execution early. If
|
||||
you see it, it probably means that a test didn't terminate before it hit the
|
||||
execution length limit. Aborts are hidden unless you use explicitly enable
|
||||
them, see (see [Advanced Usage](./advanced-usage.md)).
|
||||
|
||||
| | |
|
||||
| - | - |
|
||||
| `deadlocksNever` | checks that the computation never deadlocks |
|
||||
| `deadlocksAlways` | checks that the computation always deadlocks |
|
||||
| `deadlocksSometimes` | checks that the computation deadlocks at least once |
|
||||
|
||||
**Deadlocking** is where every thread becomes blocked. This can be, for
|
||||
example, if every thread is trying to read from an `MVar` that has been emptied.
|
||||
|
||||
| | |
|
||||
| - | - |
|
||||
| `exceptionsNever` | checks that the main thread is never killed by an exception |
|
||||
| `exceptionsAlways` | checks that the main thread is always killed by an exception |
|
||||
| `exceptionsSometimes` | checks that the main thread is killed by an exception at least once |
|
||||
|
||||
An uncaught **exception** in the main thread kills the process. These can be
|
||||
synchronous (thrown in the main thread) or asynchronous (thrown to it from a
|
||||
different thread).
|
||||
|
||||
| | |
|
||||
| - | - |
|
||||
| `alwaysSame` | checks that the computation is deterministic and always produces a value |
|
||||
| `alwaysSameOn f` | is like `alwaysSame`, but transforms the results with `f` first |
|
||||
| `alwaysSameBy f` | is like `alwaysSame`, but uses `f` instead of `(==)` to compare |
|
||||
| `notAlwaysSame` | checks that the computation is nondeterministic |
|
||||
| `notAlwaysSameOn f` | is like `notAlwaysSame`, but transforms the results with `f` first |
|
||||
| `notAlwaysSameBy f` | is like `notAlwaysSame`, but uses `f` instead of `(==)` to compare |
|
||||
|
||||
Checking for **determinism** will also find nondeterministic failures:
|
||||
deadlocking (for instance) is still a result of a test!
|
||||
|
||||
| | |
|
||||
| - | - |
|
||||
| `alwaysTrue p` | checks that `p` is true for every result |
|
||||
| `somewhereTrue p` | checks that `p` is true for at least one result |
|
||||
|
||||
These can be used to check custom predicates. For example, you might want all
|
||||
your results to be less than five.
|
||||
|
||||
| | |
|
||||
| - | - |
|
||||
| `gives xs` |checks that the set of results is exactly `xs` (which may include conditions) |
|
||||
| `gives' xs` |checks that the set of results is exactly `xs` (which may not include conditions) |
|
||||
|
||||
These let you say exactly what you want the results to be. Your test will fail
|
||||
if it has any extra results, or misses a result.
|
||||
|
||||
You can check multiple predicates against the same collection of results using
|
||||
the `dejafus` and `dejafusWithSettings` functions. These avoid recomputing the
|
||||
results, and so may be faster than multiple `dejafu` / `dejafuWithSettings`
|
||||
calls.
|
||||
|
||||
|
||||
Using HUnit and Tasty
|
||||
---------------------
|
||||
|
||||
By itself, Déjà Fu has no framework in place for named test groups and parallel
|
||||
execution or anything like that. It does one thing and does it well, which is
|
||||
running test cases for concurrent programs. [HUnit][] and [tasty][] integration
|
||||
is provided to get more of the features you'd expect from a testing framework.
|
||||
|
||||
The integration is provided by the [hunit-dejafu][] and [tasty-dejafu][]
|
||||
packages.
|
||||
|
||||
There's a simple naming convention used: the `Test.DejaFu` function `dejafuFoo`
|
||||
is wrapped in the appropriate way and exposed as `testDejafuFoo` from
|
||||
`Test.HUnit.DejaFu` and `Test.Tasty.DejaFu`.
|
||||
|
||||
Our example from the start becomes:
|
||||
|
||||
```haskell
|
||||
testDejafu "Assert the thing holds" myPredicate myAction
|
||||
```
|
||||
|
||||
The `autocheck` function is exposed as `testAuto`.
|
||||
|
||||
[HUnit]: https://hackage.haskell.org/package/HUnit
|
||||
[tasty]: https://hackage.haskell.org/package/tasty
|
||||
[hunit-dejafu]: https://hackage.haskell.org/package/hunit-dejafu
|
||||
[tasty-dejafu]: https://hackage.haskell.org/package/tasty-dejafu
|
||||
Loading…
Reference in New Issue
Block a user