Maximal Causality Reduction (MCR) algorithm

[barrucadu]

MCR is a concurrency testing algorithm by Jeff Huang which explores a provably minimal number of executions. In the first MCR paper, it vastly outperforms DPOR (which dejafu currently uses). It supports TSO and PSO. It has a Java implementation. It would be cool to have in dejafu.

Unfortunately, it has some constraints which don't work so well in Haskell:

1. It uses reference equality to cut down on the number of executions.
2. It assumes "local determinism": the next action of a thread is decided solely by the prior actions of the thread and values it has read.

For (1), we can use StableName. Haskell messes up (2) by having asynchronous exceptions.

I sent an email to Jeff, and he agreed that for (1) the algorithm can just assume that everything is unequal, which will degrade performance but it should still be better than DPOR; and for (2) every thread can be given an "exception variable", which is checked before every action. There are probably other topics to think about (eg, how to integrate masking states into this --- as they cause the throwing thread to block!).

This is definitely a project for the future, but it is something I would really like to have a go at some time.