NDLI: A type and effect system for atomicity

Content Provider	ACM Digital Library
Author	Qadeer, Shaz Flanagan, Cormac
Abstract	Ensuring the correctness of multithreaded programs is difficult, due to the potential for unexpected and nondeterministic interactions between threads. Previous work addressed this problem by devising tools for detecting race conditions, a situation where two threads simultaneously access the same data variable, and at least one of the accesses is a write. However, verifying the absence of such simultaneous-access race conditions is neither necessary nor sufficient to ensure the absence of errors due to unexpected thread interactions.We propose that a stronger non-interference property is required, namely atomicity. Atomic methods can be assumed to execute serially, without interleaved steps of other threads. Thus, atomic methods are amenable to sequential reasoning techniques, which significantly simplifies both formal and informal reasoning about program correctness.This paper presents a type system for specifying and verifying the atomicity of methods in multithreaded Java programs. The atomic type system is a synthesis of Lipton's theory of reduction and type systems for race detection.We have implemented this atomic type system for Java and used it to check a variety of standard Java library classes. The type checker uncovered subtle atomicity violations in classes such as `java.lang.String` and `java.lang.String-Buffer` that cause crashes under certain thread interleavings.This paper proposes that a stronger non-interference property is required, namely atomicity, and presents a type system for verifying the atomicity of methods in multithreaded Java programs. Methods in a class can be annotated with the keyword `atomic`. Clients of a well-typed class can then assume that each atomic method is executed in one step, thus significantly simplifying both formal and informal reasoning about the client's correctness.
Starting Page	338
Ending Page	349
Page Count	12
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/780822.781169
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	38
Issue Number	5
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	Atomicity Multithreading Static checking Race conditions
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

A type and effect system for atomicity

Race checking by context inference

DoubleChecker:efficient sound and precise atomicity checking

Hybrid type checking

A serializability violation detector for shared-memory server programs

Static type checking of multi-methods

Just-in-time static type checking for dynamic languages

Static contract checking for Haskell

Specifying and checking semantic atomicity for multithreaded programs (SIGP, Vol. 46, Issue. 3)

A type and effect system for atomicity

Similar Documents

A type and effect system for atomicity

Race checking by context inference

DoubleChecker:efficient sound and precise atomicity checking

Hybrid type checking

A serializability violation detector for shared-memory server programs

Static type checking of multi-methods

Just-in-time static type checking for dynamic languages

Static contract checking for Haskell

Specifying and checking semantic atomicity for multithreaded programs (SIGP, Vol. 46, Issue. 3)

A type and effect system for atomicity