NDLI: Exploiting synchronization in the analysis of shared-memory asynchronous programs

Please wait, while we are loading the content...

Approximating happens-before order: interplay between static analysis and state space traversal

Automatic handling of native methods in Java PathFinder

Local state space construction for compositional verification of concurrent systems

CTL+FO verification as constraint solving

Exploiting synchronization in the analysis of shared-memory asynchronous programs

Quantifying information leaks using reliability analysis

Certification for configurable program analysis

Toward parameterized verification of synchronous distributed applications

Incremental bounded software model checking

Towards a test automation framework for alloy

An improvement of the piggyback algorithm for parallel model checking

SpinCause: a tool for causality checking

Satisfiability modulo abstraction for separation logic with linked lists

Verige: verification with invariant generation engine

Is there a best büchi automaton for explicit model checking?

SpinRCP: the eclipse rich client platform integrated development environment for the spin model checker

Generic and efficient attacker models in SPIN

TravMC2: higher-order model checking for alternating parity tree automata

Towards a GPGPU-parallel SPIN model checker

Unit testing for SPIN: runspin and parsepan

Exploiting synchronization in the analysis of shared-memory asynchronous programs

Content Provider	ACM Digital Library
Author	Tasiran, Serdar Emmi, Michael Ozkan, Burcu Kulahcioglu
Abstract	As asynchronous programming becomes more mainstream, program analyses capable of automatically uncovering programming errors are increasingly in demand. Since asynchronous program analysis is computationally costly, current approaches sacrifice completeness and focus on limited sets of asynchronous task schedules that are likely to expose programming errors. These approaches are based on parameterized task schedulers, each of which admits schedules which are variations of a default deterministic schedule. By increasing the parameter value, a larger variety of schedules is explored, at a higher cost. The efficacy of these approaches depends largely on the default deterministic scheduler on which varying schedules are fashioned. We find that the limited exploration of asynchronous program behaviors can be made more efficient by designing parameterized schedulers which better match the inherent ordering of program events, e.g., arising from waiting for an asynchronous task to complete. We follow a reduction-based "sequentialization" approach to analyzing asynchronous programs, which leverages existing (sequential) program analysis tools by encoding asynchronous program executions, according to a particular scheduler, as the executions of a sequential program. Analysis based on our new scheduler comes at no greater computational cost, and provides strictly greater behavioral coverage than analysis based on existing parameterized schedulers; we validate these claims both conceptually, with complexity and behavioral-inclusion arguments, and empirically, by discovering actual reported bugs faster with smaller parameter values. .
Starting Page	20
Ending Page	29
Page Count	10
File Format	PDF
ISBN	9781450324526
DOI	10.1145/2632362.2632370
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2014-07-21
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Sequentialization Concurrency Asynchronous programs
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

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