Published Articles >> Table of Contents >> Abstract

31st Annual International Symposium on Computer Architecture (ISCA'04)   p. 114
TSOtool: A Program for Verifying Memory Systems Using the Memory Consistency Model
Sudheendra Hangal, Sun Microsystems India Private Limited, Bangalore, India
Durgam Vahia, Sun Microsystems, Sunnyvale, CA
Chaiyasit Manovit, Sun Microsystems, Sunnyvale, CA
Juin-Yeu Joseph Lu, Sun Microsystems, Sunnyvale, CA
Sridhar, Sun Microsystems, Sunnyvale, CA

Full Article Text:

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ISCA.2004.1310768
Send link to a friend

Abstract
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.
Back to Top Additional Information
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, p. 114,  31st Annual International Symposium on Computer Architecture (ISCA'04),  2004