[Haskell-cafe] model checking for (subset of) concurrent Haskell?

[Michael Walker]

Hi Johannes,

I released an initial version of a tool for the systematic testing of
concurrent Haskell programs a couple of months ago[1]. I've never been
quite certain where the boundary between model checking and testing
is, but I think it's fair to say that what I've got is a bounded model
checker.

I presented a paper on it at the Haskell Symposium this year[2][3],
but since then it has been improved significantly, both in terms of
the concurrency features supported, and performance. The version on
Hackage is very outdated now, but I hope to get a new release out
reasonably soon.

> Is there something similar for Haskell models of concurrency?
> Ideally, some subset of Haskell (containing enough of
> Control.Concurrent.*) as an alternative for Promela.

I didn't go for LTL, rather a more unit test-like approach[4] where
you examine the final output of the program.

> It should even be possible to put the model checking
> in an alternative implementation of respective monad
> (STM, IO for MVars) so the whole thing is an embedded DSL.

My approach is based on a typeclass abstraction, with a class for
concurrency[5] and a class for STM[6]. Naturally, this means you can
just write some Haskell polymorphic in the monad but constrained by
the class, and then either run it "for real" using IO or STM, or test
it using the testing instances.

The current developmental version is on GitHub[7], and I'm writing up
a technical report on it (draft online[8]).

[1] https://hackage.haskell.org/package/dejafu
[2] http://www.barrucadu.co.uk/publications/dejafu-hs15.pdf
[3] https://youtu.be/jQCDa6WoFeY?list=PLnqUlCo055hV5dPC-4VWeXzhI8ooeTsVy
[4] http://barrucadu.github.io/dejafu/Test-DejaFu.html
[5] http://barrucadu.github.io/dejafu/Control-Monad-Conc-Class.html
[6] http://barrucadu.github.io/dejafu/Control-Monad-STM-Class.html
[7] https://github.com/barrucadu/dejafu
[8] http://misc.barrucadu.co.uk/pub/techreport.pdf

-- 
Michael Walker (http://www.barrucadu.co.uk)