Specifying non-blocking shared memories (extended abstract)
Phillip B. Gibbons, Michael Merritt · 1992
Specificationsof shared memories generally assume that processors block, awaiting the response to each memory request, e.g.awaiting the return value for a read operation.On the other hand, studies have shown that substantial performance gain can be obtained by permitting a processor to have multiple memory readslwrites in progress at a time, and indeed high-performance multiprocessors such as the Tera Computer permit such nonblocking memory accesses.Formalizing correctness conditions for nonblocking shared memories requires a generalization of the processorimemory interface to specify accesses to be done concurrently, indicate when an order must be preserved even among concurrently-requested accesses, and permit out-of-order responses to memory requests.This paper provides the first formal definition of such an interface.Sequential consistency and linearizability are defined with respect to this generaf interface, as natural correctness conditions for nonblocking shared memories.Sequential consistency in turn is used in the formal specification of relaxed consistency models on nonblocking shared memories, models that support sequential consistency only for a class of well-behaved (data-race-free or PL) programs.Finally, the framework is illustrated by studying a particular relaxed consistency model, release consistency.Extending the results of a previous paper, we give a formal specification and correctness proof of a release consistent nonblocking shared memory.This work provides new insights into memory systems and programs for nonblocking shared memories, areas that are not well-understood.techniques.We present a formal specification of a nonblockingshared memory, Mwb, and define correctness conditions based on this specification.This requires a generalization of the processor/memory interface in three respects: 1.A processor conveys to the memory which of its accesses can be processed concurrently, *The discussion in Section 5 mentions some alternative uses of the term '(nonblocking" in the literature.