Link to CALCM Home  

Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values

Monday September 26, 2005
Collaborative Innovation Center, 2nd Floor, Room 2101 (CR 2101)
10:30 am

Alan J. Hu
University of British Columbia

Shared memory multiprocessing is the dominant form of multiprocessing and will grow in importance as multi-core processors become commonplace. Multiprocessor memory system protocols are notoriously complex and have been a major application for formal verification, particularly finite-state model checking, which automatically finds bugs and provides counterexamples. Unfortunately, the computational complexity of model checking grows exponentially with system size, so in practice, when verifying realistically detailed protocol models, only tiny protocol configurations (a few processors, addresses, and distinguishable data values) can be handled. In this talk, I will present our recent, fully automatic method for proving sequential consistency of an entire parameterized family of protocols, with the number of processors fixed, but the number of addresses and data values being unbounded parameters. Under some practical, reasonable assumptions, the method automatically generates a finite-state abstract protocol from the parameterized protocol description; proving sequential consistency of the abstract model, via known methods, guarantees sequential consistency of the protocol for all possible address and data sizes. The method is sound, but incomplete, but is likely to apply to most real protocols. Our experimental results show the effectiveness of our method on parameterized versions of the Piranha shared memory protocol and an extended version of a directory protocol from the University of Wisconsin Multifacet Project.

Alan Hu received his BS and PhD degrees from Stanford University. He is an associate professor and associate head of the Department of Computer Science at the University of British Columbia. For the past 15 years, his main research focus has been automated, practical techniques for formal verification. He has served on the program committees of most major CAD and formal verification conferences, and chaired or co-chaired CAV (1998), HLDVT (2003), and FMCAD (2004). He was also a Technical Working Group Key Contributor on the 2001 International Technology Roadmap for Semiconductors, and is a member of the Technical Advisory Board of Jasper Design Automation.


Department of Electrical and Computer EngineeringCarnegie Mellon UniversitySchool of Computer Science