I'm not sure that merely checking the result of some set of operations - whether a mutex is held by the expected process - tells you very much about the validit

I'm not sure that merely checking the result of some set of operations - whether a mutex is held by the expected process - tells you very much about the validity of how that mutex was obtained (assuming interleaving requests and such). This is where you need to explore the history, which is what the linearizability checker does and which is what Jepsen tests generally use. It is a bit of work and learning curve writing a Jepsen test suite, but it's not too bad, particularly with the excellent docs that Kyle has recently written: https://github.com/aphyr/jepsen/blob/master/doc/scaffolding.md https://github.com/aphyr/jepsen/blob/master/doc/scaffolding....