IEEE Int. Symp. on Computer Architecture (ISCA04), 2004.
In this paper, we describe TSOtool, a program to check the behavior of the memory subsystem in a shared memory multiprocessor. TSOtool runs pseudo-randomly generated programs with data races on a system compliant with the Total Store Order (TSO) memory consistency model; it then checks the results of the program against the formal TSO specification. Such analysis can expose subtle memory errors like data corruption, atomicity violation and illegal instruction ordering.

“TSOtool: A Program for Verifying Memory Systems Using the Memory Consistency Model”