NDLI: Memory, an elusive abstraction

Please wait, while we are loading the content...

Memory, an elusive abstraction

Content Provider	ACM Digital Library
Author	Sewell, Peter
Abstract	Multiprocessors are now ubiquitous. They provide an abstraction of shared memory, accessible by concurrently executing threads, which supports a wide range of software. However, exactly what this key abstraction is -- what the hardware designers implement, and what programmers can depend on -- is surprisingly elusive. In 1979, when articulating the notion of sequential consistency (SC), Lamport wrote "For some applications, achieving sequential consistency may not be worth the price of slowing down the processors." [7], and indeed most major multiprocessor families, including Alpha, ARM, Itanium, Power, Sparc, and x86, do not provide the abstraction of SC memory. Internally, they incorporate a range of sophisticated optimisations which have various programmer-visible effects. For some (such as Sparc) these effects are captured in a well-defined relaxed memory model, making it possible (if challenging) to reason with confidence about the behaviour of concurrent programs. For others, however, it has been very unclear what a reasonable model is, despite extensive research over the last three decades. In this talk, I will reflect on the experience of my colleagues and I in trying to establish usable models for x86 multiprocessors, where it appears that our x86-TSO model suffices for common-case code [1-4], and for Power and ARM multiprocessors, where we have models that capture some but not all aspects of their behaviour [5,6]. The underlying causes of these difficulties are complex, including: The programmer-observable relaxed-memory behaviour of a multiprocessor is a whole-system property that arises from the interaction between many complex aspects of the processor implementation: speculative execution, store buffering, cache protocol, and so forth. Programs are executed (and tested) on specific multiprocessor implementations, but processor vendors attempt to document loose specifications to cover a range of possible (past and future) implementations Multiprocessor implementation details are typically confidential and may change radically from one implementation to another Vendor specifications suffer from the tension between the need for loose specification, to preserve freedom for such changes, and the need for tight specification, to give strong properties to properties All too often, loose specification has been achieved by vague specification, using informal prose. When it comes to subtle concurrent properties this is almost inevitably ambiguous; it also makes it impossible (even in principle) to test conformance between a processor implementation and such a specification, let alone to verify such a correspondence or to reason about concurrent programs.
Starting Page	51
Ending Page	52
Page Count	2
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/1837855.1806660
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	45
Issue Number	8
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1983-05-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Semantics Relaxed memory models
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Software

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

Understanding POWER multiprocessors

Relaxed memory models:an operational approach

Relaxed-memory concurrency and verified compilation

Mathematizing C++ concurrency

Synchronising C/C++ and POWER

A promising semantics for relaxed-memory concurrency

The semantics of x86-CC multiprocessor machine code

Safe optimisations for shared-memory concurrent programs

Dynamic synthesis for relaxed memory models

Memory, an elusive abstraction

Similar Documents

Understanding POWER multiprocessors

Relaxed memory models:an operational approach

Relaxed-memory concurrency and verified compilation

Mathematizing C++ concurrency

Synchronising C/C++ and POWER

A promising semantics for relaxed-memory concurrency

The semantics of x86-CC multiprocessor machine code

Safe optimisations for shared-memory concurrent programs

Dynamic synthesis for relaxed memory models

Memory, an elusive abstraction