Shared-Memory Multiprocessors: Verifying Sequential Consistency

Title: Shared-Memory Multiprocessors: Verifying Sequential Consistency

Abstract: This research focuses on the verification of sequential consistency in shared-memory multiprocessors. The authors propose a model checking algorithm to verify sequential consistency for a finite number of processors and memory locations, and an arbitrary number of data values. The algorithm is based on the observation that, in practice, shared-memory systems satisfy the properties of causality and data independence. If a causal and data independent system also has the property that the logical order of write events to each location is identical to their temporal order, then sequential consistency can be verified algorithmically.

The research addresses the issue of verifying parameterized systems for arbitrary values of the parameters, which is undecidable for nontrivial systems. The authors propose an automatic method based on model checking to verify that a cache-coherence protocol with fixed parameter values is correct with respect to the sequential consistency memory model. This method is particularly useful for debugging and finding errors in the system before a more time-consuming effort of verification for arbitrary paramet

Link to Article: https://arxiv.org/abs/0108016v1 Authors: arXiv ID: 0108016v1