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.
|