[codex]

So far, nobody has mentioned the author's C++ based race detection tool. Conceptually it is similar to Corensic's commercial product, Jinx (http://www.corensic.com) but practically Jinx supports more languages, doesn't require recompilation, and is most likely much faster.

[dvyukov]

It's "similar" to a lot of software out there: Intel Thread Checker, Chord, Zing, Spin, RacerX, CheckFence, Sober, Coverity Thread Analyzer, CHESS, KISS, PreFast, Prefix, FxCop. However, what you are missing is that most of these tools (and Jinx as far as I see, can't find clear description on the site, mostly vague marketing stuff) are of help to you if you are an application developer who writes in term of mutexes. While RRD is of help to you if you are implementing mutexes itself. Can you verify involved mutex algorithm down to possible memory access reorderings? I doubt.

> and is most likely much faster. Or an order of magnitude slower.

[Kaya]

Jinx can help verify mutex implementations themselves, although the example code that ships with the product is a little more advanced (lock-free stack). Some of the underlying technology is described here: http://s3.amazonaws.com/corensic/whitepapers/DeterministicSh... and here: http://www.corensic.com/WhyYouNeedJinx/CorensicHasaUniqueTec.... Because it's a hypervisor, it can aid in verifying synchronization primitives that are a mix of userspace and kernel code.

[dvyukov]

I do not see anything about memory fences. If Jinx does not support them, then it's pretty much useless for verification of synchronization algorithms. I've implemented dozens of advanced synchronization algorithms, and I may say that it's crucial. Also, if it works on binary level (does not require re-compilation), then it also renders it useless, because on that level you lose information about order of memory accesses, memory fences, atomicity. For example, if you see plain x86 MOV instruction, what is it? non-atomic store? atomic relaxed store? atomic release store?