NDLI: Declarative fence insertion

Content Provider	ACM Digital Library
Author	Palsberg, Jens Bender, John Lesani, Mohsen
Abstract	Previous work has shown how to insert fences that enforce sequential consistency. However, for many concurrent algorithms, sequential consistency is unnecessarily strong and can lead to high execution overhead. The reason is that, often, correctness relies on the execution order of a few specific pairs of instructions. Algorithm designers can declare those execution orders and thereby enable memory-model-independent reasoning about correctness and also ease implementation of algorithms on multiple platforms. The literature has examples of such reasoning, while tool support for enforcing the orders has been lacking until now. In this paper we present a declarative approach to specify and enforce execution orders. Our fence insertion algorithm first identifies the execution orders that a given memory model enforces automatically, and then inserts fences that enforce the rest. Our benchmarks include three off-the-shelf transactional memory algorithms written in C/C++ for which we specify suitable execution orders. For those benchmarks, our experiments with the x86 and ARMv7 memory models show that our tool inserts fences that are competitive with those inserted by the original authors. Our tool is the first to insert fences into transactional memory algorithms and it solves the long-standing problem of how to easily port such algorithms to a novel memory model.
Starting Page	367
Ending Page	385
Page Count	19
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/2858965.2814318
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	50
Issue Number	10
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	Concurrency Static analysis Compilers Weak 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

Declarative fence insertion

Benchmarking weak memory models

Dynamic synthesis for relaxed memory models

Herding cats:modelling, simulation, testing, and data-mining for weak memory

Partial-coherence abstractions for relaxed memory models

A promising semantics for relaxed-memory concurrency

GPS:navigating weak memory with ghosts, protocols, and separation

The virtues of conflict:analysing modern concurrency

Automatically comparing memory consistency models

Declarative fence insertion

Similar Documents

Declarative fence insertion

Benchmarking weak memory models

Dynamic synthesis for relaxed memory models

Herding cats:modelling, simulation, testing, and data-mining for weak memory

Partial-coherence abstractions for relaxed memory models

A promising semantics for relaxed-memory concurrency

GPS:navigating weak memory with ghosts, protocols, and separation

The virtues of conflict:analysing modern concurrency

Automatically comparing memory consistency models

Declarative fence insertion