TSOTool 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 all top 5 Cited by 16 Authors 2 Alglave, Jade 1 Baswana, Surender 1 Dong, JinSong 1 Hoa, Koh Chuen 1 Hou, Zhe 1 Jagadeesan, Radha 1 Liu, Yang 1 Maranget, Luc 1 Mehta, Shashank K. 1 Pitcher, Corin 1 Powar, Vishal 1 Riely, James 1 Sanán, David 1 Sarkar, Susmit 1 Sewell, Peter 1 Tiu, Alwen Fernanto Cited in 2 Serials 2 Formal Methods in System Design 1 Journal of Automated Reasoning Cited in 2 Fields 5 Computer science (68-XX) 1 Combinatorics (05-XX) Citations by Year