a551893ccf
There should be one buffer for each (thread, ref) pair, not simply for each ref. The former is too strict as it enforces a total order on the commits to the same ref, yielding some bizarro memory model which is both stricter and more relaxed than TSO. This does add extra schedules when testing PSO. But that is to be expected, as this makes PSO executions less deterministic. Unfortunately this additional nondeterminism is required by the memory model. |
||
---|---|---|
async-dejafu | ||
dejafu | ||
dejafu-tests | ||
hunit-dejafu | ||
tasty-dejafu | ||
.gitignore | ||
README.markdown | ||
stack.yaml |
This repository contains dejafu, a concurrency testing library based on a typeclass abstraction of concurrency, and related libraries.
-
dejafu (hackage 0.2.0.0): Overloadable primitives for testable, potentially non-deterministic, concurrency.
-
async-dejafu (hackage 0.1.0.0): Run MonadConc operations asynchronously and wait for their results.
-
hunit-dejafu (hackage 0.2.0.0): Deja Fu support for the HUnit test framework.
-
tasty-dejafu (hackage 0.2.0.0): Deja Fu support for the Tasty test framework.
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.
Bibliography
Each paper has a short name in parentheses, which I use in non-haddock comments. Haddock comments get the full citation. PDF links are provided where non-paywalled ones are available.
-
[BPOR] Bounded partial-order reduction, K. Coons, M. Musuvathi, and K. McKinley (2013) http://research.microsoft.com/pubs/202164/bpor-oopsla-2013.pdf
-
[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
-
[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
-
[RMMVerification] On the Verification of Programs on Relaxed Memory Models, A. Linden (2014) https://orbi.ulg.ac.be/bitstream/2268/158670/1/thesis.pdf