NDLI: CDSchecker:checking concurrent data structures written with C/C++ atomics

Content Provider	ACM Digital Library
Author	Norris, Brian Demsky, Brian
Abstract	Writing low-level concurrent software has traditionally required intimate knowledge of the entire toolchain and often has involved coding in assembly. New language standards have extended C and C++ with support for low-level atomic operations and a weak memory model, enabling developers to write portable and efficient multithreaded code. Developing correct low-level concurrent code is well-known to be especially difficult under a weak memory model, where code behavior can be surprising. Building reliable concurrent software using C/C++ low-level atomic operations will likely require tools that help developers discover unexpected program behaviors. In this paper we present CDSChecker, a tool for exhaustively exploring the behaviors of concurrent code under the C/C++ memory model. We develop several novel techniques for modeling the relaxed behaviors allowed by the memory model and for minimizing the number of execution behaviors that CDSChecker must explore. We have used CDSChecker to exhaustively unit test several concurrent data structure implementations on specific inputs and have discovered errors in both a recently published C11 implementation of a work-stealing queue and a single producer, single consumer queue implementation.
Starting Page	131
Ending Page	150
Page Count	20
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/2544173.2509514
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	48
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	Model checking Relaxed memory model
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

CDSchecker: checking concurrent data structures written with C/C++ atomics

CheckFence:checking consistency of concurrent data types on relaxed memory models

A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions

SATCheck: SAT-directed stateless model checking for SC and TSO

Quantitative relaxation of concurrent data structures

Deriving linearizable fine-grained concurrent objects

The SprayList: a scalable relaxed priority queue

Dynamic partial order reduction for relaxed memory models

B.: CDSchecker: checking concurrent data structures written with C/C++ atomics (2013)

CDSchecker:checking concurrent data structures written with C/C++ atomics

Similar Documents

CDSchecker: checking concurrent data structures written with C/C++ atomics

CheckFence:checking consistency of concurrent data types on relaxed memory models

A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions

SATCheck: SAT-directed stateless model checking for SC and TSO

Quantitative relaxation of concurrent data structures

Deriving linearizable fine-grained concurrent objects

The SprayList: a scalable relaxed priority queue

Dynamic partial order reduction for relaxed memory models

B.: CDSchecker: checking concurrent data structures written with C/C++ atomics (2013)

CDSchecker:checking concurrent data structures written with C/C++ atomics