loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
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
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.