TSOTool: a program for verifying memory systems using the memory consistency model. In this paper, we describe TSOtool, a program to check thebehavior of the memory subsystem in a shared memorymultiprocessor. TSOtool runs pseudo-randomly generatedprograms with data races on a system compliant with theTotal Store Order (TSO) memory consistency model; it thenchecks the results of the program against the formal TSOspecification. Such analysis can expose subtle memory errorslike data corruption, atomicity violation and illegalinstruction ordering.While verifying TSO compliance completely is an NP-completeproblem, we describe a new polynomial timealgorithm which is incorporated in TSOtool. In spite of beingincomplete, it has been successful in detecting several bugs inthe design of commercial microprocessors and systems,during both pre-silicon and post-silicon phases of validation.

This software is also peer reviewed by journal TOMS.