Sciweavers

CAV
2004
Springer

Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values

14 years 4 months ago
Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values
Sequential consistency is the archetypal correctness condition for the memory protocols of shared-memory multiprocessors. Typically, such protocols are parameterized by the number of processors, the number of addresses, and the number of distinguishable data values, and typically, automatic protocol verification analyzes only concrete instances of the protocol with small values (generally < 3) for the protocol parameters. This paper presents a fully automatic method for proving the 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. Using some practical, reasonable assumptions (data independence, processor symmetry, location symmetry, simple store ordering, some syntactic restrictions), the method automatically generates a finite-state protocol from the parameterized protocol description; proving sequential consistency of the abstract model, via known metho...
Jesse D. Bingham, Anne Condon, Alan J. Hu, Shaz Qa
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where CAV
Authors Jesse D. Bingham, Anne Condon, Alan J. Hu, Shaz Qadeer, Zhichuan Zhang
Comments (0)