A Unified Formalization of Four Shared-Memory Models

Sarita V. Adve, Mark D. Hill

Research output: Contribution to journalArticlepeer-review

Abstract

This paper presents a shared-memory model, data- race-free-1, that unifies four earlier models: weak ordering, re-lease consistency (with sequentially consistent special operations), the VAX memory model, and data-race-free-O. The most intuitive and commonly assumed shared-memory model, sequential consistency, limits performance. The models of weak ordering, release consistency, the VAX, and data-race-free-0 are based on the common intuition that if programs synchronize explicitly and correctly, then sequential consistency can be guaranteed with high performance. However, each model formalizes this intuition differently and has different advantages and disadvantages with respect to the other models. Data-race-free-1 unifies the models of weak ordering, release consistency, the VAX, and data-race-free-0 by formalizing the above intuition in a manner that retains the advantages of each of the four models. A multiprocessor is data-race-free-1 if it guarantees sequential consistency to data-race-free programs. Data-race-free-1 unifies the four models by providing a programmer’s interface similar to the four models, and by allowing all implementations allowed by the four models. Additionally, data-race-free-1 expresses the programmer’s interface more explicitly and formally than weak ordering and the VAX, and allows an implementation not allowed by weak ordering, release consistency, or data-race-free-0, The new implementation proposal for data-race-free-1 differs from earlier implementations mainly by permitting the execution of all synchronization operations of a processor even while previous data operations of the processor are in progress. To ensure sequential consistency, two synchronizing processors exchange information to delay later operations of the second processor that conflict with an incomplete data operation of the first processor.

Original languageEnglish (US)
Pages (from-to)613-624
Number of pages12
JournalIEEE Transactions on Parallel and Distributed Systems
Volume4
Issue number6
DOIs
StatePublished - Jun 1993
Externally publishedYes

Keywords

  • Data-race-free-0
  • data-race-free-1
  • memory model
  • release consistency
  • sequential consistency
  • shared-memory multiprocessor
  • weak ordering

ASJC Scopus subject areas

  • Signal Processing
  • Hardware and Architecture
  • Computational Theory and Mathematics

Fingerprint Dive into the research topics of 'A Unified Formalization of Four Shared-Memory Models'. Together they form a unique fingerprint.

Cite this