31st Annual International Symposium on Computer Architecture (ISCA'04) TSOtool: A Program for Verifying Memory Systems Using the Memory Consistency Model M?nchen, Germany June 19-June 23 ISBN: 0-7695-2143-6
In this paper, we describe TSOtool, a program to check the behavior of the memory subsystem in a shared memory multiprocessor. TSOtool runs pseudo-randomly generated programs with data races on a system compliant with the Total Store Order (TSO) memory consistency model; it then checks the results of the program against the formal TSO specification. Such analysis can expose subtle memory errors like data corruption, atomicity violation and illegal instruction ordering.While verifying TSO compliance completely is an NP-complete problem, we describe a new polynomial time algorithm which is incorporated in TSOtool. In spite of being incomplete, it has been successful in detecting several bugs in the design of commercial microprocessors and systems, during both pre-silicon and post-silicon phases of validation.
Index Terms:
Memory consistency models, Multiprocessor verification, Sequential Consistency, Total Store Order
Citation:
Sudheendra Hangal, Durgam Vahia, Chaiyasit Manovit, Juin-Yeu Joseph Lu, Sridhar , "TSOtool: A Program for Verifying Memory Systems Using the Memory Consistency Model," isca, pp.114, 31st Annual International Symposium on Computer Architecture (ISCA'04), 2004 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||