Technical Report LPCR9309

TR#:LPCR9309
Class:LPCR
Title: SHARED MEMORY CONSISTENCY CONDITIONS FOR NON-SEQUENTIAL EXECUTION: DEFINITIONS AND PROGRAMMING STRATEGIES.
Authors: H. Attiya, S. Chaudhuri, R. Friedman and J.L. Welch
PDFLPCR9309.pdf
Abstract:

To enhance performance on shared memory multiprocessors, various techniques have been proposed to reduce the latency of memory accesses, including pipelining of accesses, out-of-order execution of accesses, and branch prediction with speculative execution. These optimizations however can complicate the users model of memory. This paper attacks the problem of simplifying programming on two fronts. First, a general framework is presented for defining shared memory consistency conditions that allows non-sequential execution of memory accesses. The interface at which conditions are defined is between the program and the system, and is architecture-independent. The framework is used to generalize four known consistency conditions - sequential consistency, hybrid consistency, weak consistency, and release consistency - for non-sequential execution. Thus familiar consistency conditions can be precisely specified even in optimized architectures. Second, several techniques are described for structuring programs so that a shared memory that provides the weaker (and more efficient) condition of hybrid consistency appears to guarantee the stronger (and more costly) condition of sequential consistency. The benefit is that sequentially consistent executions are easier to reason about. The first and second techniques statically classify accesses based on their type. This approach is extremely simply to use and leads to a general methodology for writing efficient synchronization code. The third technique is to avoid data races in the program. This technique also works on a simple variant of release consistent hardware, with an appropriate change to the definition of data race. Precise yet short and comprehensible proofs are provided for the correctness of the programming techniques. Such proofs shed light on the reasons these techniques work; we believe that the insight gained can lead to the development of other techniques.

CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/1993/LPCR/LPCR9309), rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the LPCR technical reports of 1993
To the main CS technical reports page

Computer science department, Technion
admin