NDLI: Views:compositional reasoning for concurrent programs

Content Provider	ACM Digital Library
Author	Gardner, Philippa Parkinson, Matthew Birkedal, Lars Yang, Hongseok Dinsdale-Young, Thomas
Abstract	Compositional abstractions underly many reasoning principles for concurrent programs: the concurrent environment is abstracted in order to reason about a thread in isolation; and these abstractions are composed to reason about a program consisting of many threads. For instance, separation logic uses formulae that describe part of the state, abstracting the rest; when two threads use disjoint state, their specifications can be composed with the separating conjunction. Type systems abstract the state to the types of variables; threads may be composed when they agree on the types of shared variables. In this paper, we present the "Concurrent Views Framework", a metatheory of concurrent reasoning principles. The theory is parameterised by an abstraction of state with a notion of composition, which we call views. The metatheory is remarkably simple, but highly applicable: the rely-guarantee method, concurrent separation logic, concurrent abstract predicates, type systems for recursive references and for unique pointers, and even an adaptation of the Owicki-Gries method can all be seen as instances of the Concurrent Views Framework. Moreover, our metatheory proves each of these systems is sound without requiring induction on the operational semantics.
Starting Page	287
Ending Page	300
Page Count	14
File Format	PDF MP4
ISSN	03621340 15581160
DOI	10.1145/2480359.2429104
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	48
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	Concurrency Compositional reasoning Axiomatic semantics
Content Type	Audio 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

Views: compositional reasoning for concurrent programs

Verification of parameterized concurrent programs by modular reasoning about data and control

Modular reasoning for deterministic parallelism

Parallel concurrent ML

Mathematizing C++ concurrency

A rely-guarantee-based simulation for verifying concurrent program transformations

Mechanized verification of fine-grained concurrent programs

Execution privatization for scheduler-oblivious concurrent programs

Race directed scheduling of concurrent programs

Views:compositional reasoning for concurrent programs

Similar Documents

Views: compositional reasoning for concurrent programs

Verification of parameterized concurrent programs by modular reasoning about data and control

Modular reasoning for deterministic parallelism

Parallel concurrent ML

Mathematizing C++ concurrency

A rely-guarantee-based simulation for verifying concurrent program transformations

Mechanized verification of fine-grained concurrent programs

Execution privatization for scheduler-oblivious concurrent programs

Race directed scheduling of concurrent programs

Views:compositional reasoning for concurrent programs