TSOtool
- 2 March 2004
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGARCH Computer Architecture News
- Vol. 32 (2)
- https://doi.org/10.1145/1028176.1006710
Abstract
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.Keywords
This publication has 8 references indexed in Scilit:
- The complexity of verifying memory coherencePublished by Association for Computing Machinery (ACM) ,2003
- Functional verification of the POWER4 microprocessor and POWER4 multiprocessor systemsIBM Journal of Research and Development, 2002
- Automatable verification of sequential consistencyPublished by Association for Computing Machinery (ACM) ,2001
- An executable specification and verifier for relaxed memory orderIEEE Transactions on Computers, 1999
- Multiprocessors should support simple memory consistency modelsComputer, 1998
- Functional verification of a multiple-issue, out-of-order, superscalar Alpha processor---the DEC Alpha 21264 microprocessorPublished by Association for Computing Machinery (ACM) ,1998
- Testing Shared MemoriesSIAM Journal on Computing, 1997
- Race-free interconnection networks and multiprocessor consistencyPublished by Association for Computing Machinery (ACM) ,1991