Implement Source-Set DPOR #39
Description
Discussion
McMini currently uses DPOR with sleep sets and clock vectors. While this is a great improvement from where McMini started without sleep sets, there is still more room for improvement to reduce the number of Mazurkiewicz traces that McMini has to search.
Proposal
We should implement the source-set DPOR implementation described in the linked paper. I've read through it up to the source set implementation, and while there are still some kinks to work out, it seems that we can compute the operations described in the paper using the infrastructure we already have. For example, I think we can keep track of the first transition in the transition sequence (or stack). "Source-set DPOR" can perform quite a bit better than DPOR with only sleep sets.
Challenges
The biggest challenge here will be to figure out how to compute each of the operations efficiently. I've worked out a couple of ideas that seem like they'd work but there are more details we should work out