NDLI: A calculus of atomic actions

Content Provider	ACM Digital Library
Author	Elmas, Tayfun Qadeer, Shaz Tasiran, Serdar
Abstract	We present a proof calculus and method for the static verification of assertions and procedure specifications in shared-memory concurrent programs. The key idea in our approach is to use atomicity as a proof tool and to simplify the verification of assertions by rewriting programs to consist of larger atomic actions. We propose a novel, iterative proof style in which alternating use of abstraction and reduction is exploited to compute larger atomic code blocks in a sound manner. This makes possible the verification of assertions in the transformed program by simple sequential reasoning within atomic blocks, or significantly simplified application of existing concurrent program verification techniques such as the Owicki-Gries or rely-guarantee methods. Our method facilitates a clean separation of concerns where at each phase of the proof, the user worries only about only either the sequential properties or the concurrency control mechanisms in the program. We implemented our method in a tool called QED. We demonstrate the simplicity and effectiveness of our approach on a number of benchmarks including ones with intricate concurrency protocols.
Starting Page	2
Ending Page	15
Page Count	14
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/1594834.1480885
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	44
Issue Number	1
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 Reduction Abstraction Concurrent programs
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 calculus of atomic actions

Atomizer:a dynamic atomicity checker for multithreaded programs

AtomCaml:first-class atomicity via rollback

Analyzing recursive programs using a fixed-point calculus

Stabilizers:a modular checkpointing abstraction for concurrent functional programs

Velodrome:a sound and complete dynamic atomicity checker for multithreaded programs

A generic approach to the static analysis of concurrent programs with procedures

Testing atomicity of composed concurrent operations

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

A calculus of atomic actions

Similar Documents

A calculus of atomic actions

Atomizer:a dynamic atomicity checker for multithreaded programs

AtomCaml:first-class atomicity via rollback

Analyzing recursive programs using a fixed-point calculus

Stabilizers:a modular checkpointing abstraction for concurrent functional programs

Velodrome:a sound and complete dynamic atomicity checker for multithreaded programs

A generic approach to the static analysis of concurrent programs with procedures

Testing atomicity of composed concurrent operations

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

A calculus of atomic actions