Thread sanitizer is a tool which can detect races. Spin is a tool which can prove an algorithm (or a simplified specification of it) is race-free. You start wi

Thread sanitizer is a tool which can detect races. Spin is a tool which can prove an algorithm (or a simplified specification of it) is race-free. You start with an algorithm involving concurrent operations. Spin searches across all possible interleavings of those operations -- basically like running your program while simulating every possible ordering of execution. Over all those simulations, it verify invariants (that you choose). So it's like a proof agent -- if your proof succeeds you get a much stronger guarantee that your algorithm behaves as you believe it does.