Dimensions of Verifying the HardwareSoftware Interface in a Shared-Memory Multiprocessor

Scalable shared-memory multiprocessors provide a flexible programming model with good performance scaling. These features, however, come at the expense of additional hardware complexity to provide a consistent view of the memory hierarchy. Verifying this aspect of a multiprocessor system is nontrivial, often requiring far more time than the actual implementation. We investigate the various approaches for verifying coherent memory systems in large-scale multiprocessors. In the process, we define a set of sufficient conditions for correctness and establish a taxonomy of known verification methods. We analyze the strengths and limitations of each approach, and discuss where each fits in the context of a large design project. 1 Memory Consistency and Coherence The design of large-scale multiprocessors poses many challenges. A critical challenge is the design and verification of a memory system that provides scalability in addition to a flexible programming model. A Distributed Shared Memory (DSM) architecture provides a logically shared address space that is physically distributed among the computing nodes in the system. DSM architectures use an interconnection network to communicate between multiple processors, and rely on an efficient memory hierarchy to hide the memory access latency. Unfortunately, this hierarchy introduces additional complexity to ensure that various levels remain consistent. The hardware-software interface When executing a parallel application, multiple processors must coordinate their actions using an appropriate programming model. This model defines the programmer’s view of the machine and dictates when explicit synchronization and communication is required This work was supported in part by National Science Foundatio