Paper Info
Title
TSOtool: A Program for Verifying Memory Systems Using the Memory Consistency Model
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.
Year
DOI
Venue
2004
http://doi.acm.org/10.1145/1028176.1006710
Proceedings of the 31st annual international symposium on Computer architecture
Keywords
Field
DocType
Memory consistency models,Multiprocessor verification,Sequential Consistency,Total Store Order
Atomicity,Programming language,Sequential consistency,Computer science,Software bug,Real-time computing,Consistency model,Overlay,Memory errors,Parallel computing,Data integrity,Operating system,Formal verification
Conference
Volume
Issue
ISSN
32
2
0163-5964
ISBN
Citations 
PageRank 
0-7695-2143-6
56
2.92
References 
Authors
14
4
Name
Order
Citations
PageRank
Sudheendra Hangal153635.73
Durgam Vahia2623.46
Chaiyasit Manovit31146.48
Juin-Yeu Joseph Lu4724.21