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.
Notes
We are currently acquiring citations for the work deposited into this collection. We recognize the distribution rights of this item may have been assigned to another entity, other than the author(s) of the work.If you can provide the citation for this work or you think you own the distribution rights to this work please contact the Institutional Repository Administrator at digitize@ucalgary.ca