Specifying Memory Consistency of Write Buffer Multiprocessors
Date
2004-08-17
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Write buffering is one of many successful mechanisms that improves
the performance and scalability of multiprocessors. However, it leads to more
complex memory system behavior, which cannot be described using intuitive
consistency models, such as sequential consistency. It is crucial to provide
programmers with a specification of the exact behavior of such complex
memories. This paper presents a uniform framework for describing systems at
different levels of abstraction and proving their equivalence. The framework
is used to derive and prove correct specification in terms of program-level
instruction of the SPARC total store order and partial store order memories.
<BR><BR>The framework is also used to examine the SPARC relaxed memory order. We show
that it is not a memory consistency model that corresponds to any
implementation on a multiprocessor that uses write-buffers, even though we
suspect that the SPARC Version 9 specification of relaxed memory order was
intended to capture a general write-buffer architecture. The same techniques
can be used to show that coherence does not correspond to a write-buffer
architecture. A corollary is that any implementation of Alpha consistency
using write-buffers cannot produce all possible Alpha computations. That is,
there are some computations that satisfy the Alpha specification but cannot
occur in the given write-buffer implementation.
Description
Keywords
Computer Science