NDLI: Linearizable concurrent objects

Content Provider	ACM Digital Library
Author	Herlihy, M. P. Wing, J. M.
Abstract	Technological advances are making multiprocessors more readily available, but despite impressive progress at the hardware level, it is still difficult to realize these machines' potential for parallelism. In the sequential domain, “object-oriented” programming methodologies based on data abstraction are widely recognized as an effective means of enhancing modularity, expressibility, and correctness. Our paper describes the foundations for a new approach to extending object-oriented methodologies to highly-concurrent shared-memory multiprocessors.The basic idea is the following: rather than communicating through low-level machine constructs such as bytes, words, registers, etc., processes communicate through abstract data structures called concurrens objects. For example, in a real-time system consisting of a pool of sensor and actuator processes, the processes might communicate via a first-in-first-out (FIFO) queue object in shared memory. When a sensor process detects a condition requiring a response, it records the condition by enqueuing a record in the queue. Whenever an actuator process becomes idle, it dequeues the next item from the queue and takes appropriate action. While the correct behavior of objects such as FIFO queues is well-understood in the sequential domain, it is not so obvious how a FIFO queue should behave when manipulated by concurrent processes. We advocate a new correctness condition, linearizability, for implementing and reasoning about concurrent objects.We view a concurrent system as a collection of sequential processes that communicate through shared objects. Each object has a type, which defines a set of possible values and a set of primitive operations that provide the only means to create and manipulate that object. In the absence of concurrency, operations are executed one at a time, and their meanings can be captured by simple pre- and postconditions. In a concurrent program, however, operations can be executed concurrently, thus it is necessary to find a new meaning for operations that may overlap in time. Two requirements seem to make intuitive sense: First, each operation should appear to “take effect” instantaneously, and second, the order of non-concurrent operations should be preserved. We define a concurrent computation to be linearizable2 if it is “equivalent” to a legal sequential computation that satisfies these two requirements.Informally, linearizability provides the illusion that each operation applied by concurrent processes takes effect instantaneously at some point between its invocation and its response. This property implies that the effects of a concurrent object's operations can still be specified using pre- and post-conditions; however, we interpret a data type's sequential specification as permitting only linearizable interleavings. Thus, instead of treating data as a mass of hardware registers or single large database whose entities are uninterpreted, linearizability exploits the semantics of abstract data types. It permits a high degree of concurrency, yet it permits programmers to specify and reason about concurrent objects using known techniques from the sequential domain.Using axiomatic specifications and our notion of linearizability, we can reason about two kinds of problems: (1) the correctness of linearizable object implementations by using new techniques that generalize the sequential notions of representation invariant and abstraction function to the concurrent domain; and (2) the correctness of computations that use linearizable objects by transforming assertions about concurrent computations into simpler assertions about their sequential counterparts.
Starting Page	133
Ending Page	135
Page Count	3
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/67387.67423
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	24
Issue Number	4
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1983-05-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
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

Deriving linearizable fine-grained concurrent objects

Specifying concurrent objects

Two models of concurrent objects

A logical theory of concurrent objects

Hoare-style specifications as correctness conditions for non-linearizable concurrent objects

Concurrent objects in a logic programming framework

Objects in concurrent logic programming languages (abstract only)

Tractable Refinement Checking for Concurrent Objects

Position statement on concurrent objects for massively parallel architectures

Linearizable concurrent objects

Similar Documents

Deriving linearizable fine-grained concurrent objects

Specifying concurrent objects

Two models of concurrent objects

A logical theory of concurrent objects

Hoare-style specifications as correctness conditions for non-linearizable concurrent objects

Concurrent objects in a logic programming framework

Objects in concurrent logic programming languages (abstract only)

Tractable Refinement Checking for Concurrent Objects

Position statement on concurrent objects for massively parallel architectures

Linearizable concurrent objects