NDLI: Specifying memory consistency of write buffer multiprocessors

Content Provider	ACM Digital Library
Author	Jackson, Lillanne Kawash, Jalal Higham, Lisa
Copyright Year	2007
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 article 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 simple specifications in terms of program-level instructions of the sparc total store order and partial store order memories.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 technique is used to show that Coherence does not correspond to a write-buffer architecture. A corollary, which follows from the relationship between Coherence and Alpha, 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.
File Format	PDF
ISSN	07342071
e-ISSN	15577333
DOI	10.1145/1189736.1189737
Volume Number	25
Issue Number	1
Journal	ACM Transactions on Computer Systems (TOCS)
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2007-02-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Memory consistency framework Alpha Coherence Partial store order Relaxed memory order Sequential consistency Sparc multiprocessors Total store order Write-buffer architectures
Content Type	Text
Resource Type	Article
Subject	Computer Science

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Specifying memory consistency of write buffer multiprocessors (2007)

Using Lamport Clocks to Reason About Relaxed Memory Models (1999)

Using Lamport Clocks to Reason About Relaxed Memory Models (1999)

Using lamport clocks to reason about relaxed memory models (1999)

Memory Consistency and Process Coordination for SPARC Multiprocessors

Mechanisms for store-wait-free multiprocessors

Shared memory computing on clusters with symmetric multiprocessors and system area networks

TSOtool:A Program for Verifying Memory Systems Using the Memory Consistency Model

Mechanisms for Store-wait-free Multiprocessors (2007)

Specifying memory consistency of write buffer multiprocessors

Similar Documents

Specifying memory consistency of write buffer multiprocessors (2007)

Using Lamport Clocks to Reason About Relaxed Memory Models (1999)

Using Lamport Clocks to Reason About Relaxed Memory Models (1999)

Using lamport clocks to reason about relaxed memory models (1999)

Memory Consistency and Process Coordination for SPARC Multiprocessors

Mechanisms for store-wait-free multiprocessors

Shared memory computing on clusters with symmetric multiprocessors and system area networks

TSOtool:A Program for Verifying Memory Systems Using the Memory Consistency Model

Mechanisms for Store-wait-free Multiprocessors (2007)

Specifying memory consistency of write buffer multiprocessors