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

• Type: Conference
• Year: 2004
• Where: CAV
• Authors: Jesse D. Bingham, Anne Condon, Alan J. Hu, Shaz Qadeer, Zhichuan Zhang
• Keywords: CAV 2004, Hardware, Memory Protocol, Parameterized Protocol Description, Sequential Consistency