swMATH ID: 10131
Software Authors: Hangal S, Vahia D, Manovit C, Lu J-YJ, Narayanan S
Description: 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.
Homepage: http://dl.acm.org/citation.cfm?id=1006710
Related Software: UMM; Coq; TSL; K Prover; CompCert; Lem; CoqJVM; Isabelle/HOL; ACL2; Scala
Cited in: 5 Publications

Citations by Year