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

Content Provider	ACM Digital Library
Author	Kincaid, Zachary Farzan, Azadeh
Abstract	In this paper, we consider the problem of verifying thread-state properties of multithreaded programs in which the number of active threads cannot be statically bounded. Our approach is based on decomposing the task into two modules, where one reasons about data and the other reasons about control. The data module computes thread-state invariants (e.g., linear constraints over global variables and local variables of one thread) using the thread interference information computed by the control module. The control module computes a representation of thread interference, as an incrementally constructed data flow graph, using the data invariants provided by the data module. These invariants are used to rule out patterns of thread interference that can not occur in a real program execution. The two modules are incorporated into a feedback loop, so that the abstractions of data and interference are iteratively coarsened as the algorithm progresses (that is, they become weaker) until a fixed point is reached. Our approach is sound and terminating, and applicable to programs with infinite state (e.g., unbounded integers) and unboundedly many threads. The verification method presented in this paper has been implemented into a tool, called Duet. We demonstrate the effectiveness of our technique by verifying properties of a selection of Linux device drivers using Duet, and also compare Duet with previous work on verification of parameterized Boolean program using the Boolean abstractions of these drivers.
Starting Page	297
Ending Page	308
Page Count	12
File Format	PDF MP4
ISSN	03621340 15581160
DOI	10.1145/2103621.2103693
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	47
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	Parameterized programs Concurrency Compositional reasoning Thread invariants Abstract interpretation Data flow graphs
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

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

Views:compositional reasoning for concurrent programs

Thread modularity at many levels: a pearl in compositional verification

Modular reasoning for deterministic parallelism

Modular reasoning about concurrent higher-order imperative programs

Inductive data flow graphs

Z.: Verification of parameterized concurrent programs by modular reasoning about data and control (2012)

Iris:Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning

Modular reasoning about invariants over shared state with interposed data members:(abstract only)

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

Similar Documents

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

Views:compositional reasoning for concurrent programs

Thread modularity at many levels: a pearl in compositional verification

Modular reasoning for deterministic parallelism

Modular reasoning about concurrent higher-order imperative programs

Inductive data flow graphs

Z.: Verification of parameterized concurrent programs by modular reasoning about data and control (2012)

Iris:Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning

Modular reasoning about invariants over shared state with interposed data members:(abstract only)

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