NDLI: DETERMIN: inferring likely deterministic specifications of multithreaded programs

Content Provider	IEEE Xplore Digital Library
Author	Burnim, J. Koushik Sen
Copyright Year	2010
Description	Author affiliation: UC Berkeley (Burnim, J.; Koushik Sen)
Abstract	The trend towards multicore processors and graphic processing units is increasing the need for software that can take advantage of parallelism. Writing correct parallel programs using threads, however, has proven to be quite challenging due to nondeterminism. The threads of a parallel application may be interleaved nondeterministically during execution, which can lead to nondeterministic results---some interleavings may produce the correct result while others may not. We have previously proposed an assertion framework for specifying that regions of a parallel program behave deterministically despite nondeterministic thread interleaving. The framework allows programmers to write assertions involving pairs of program states arising from different parallel schedules. We propose an algorithm to dynamically infer likely deterministic specifications for parallel programs given a set of inputs and schedules. We have implemented our specification inference algorithm for Java and have applied it to a number of previously examined Java benchmarks. We were able to automatically infer specifications largely equivalent to or stronger than our manual assertions from our previous work. We believe that the inference of deterministic specifications can aid in understanding and documenting the deterministic behavior of parallel programs. Moreover, an unexpected deterministic specification can indicate to a programmer the presence of erroneous or unintended behavior.
Starting Page	415
Ending Page	424
File Size	258077
Page Count	10
File Format	PDF
ISBN	9781605587196
ISSN	02705257
DOI	10.1145/1806799.1806860
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2010-05-02
Publisher Place	South Africa
Access Restriction	Subscribed
Rights Holder	Association for Computing Machinery, Inc. (ACM)
Subject Keyword	Bridges Schedules Vegetation Lattices Semantics Instruction sets Java specification inference determinism parallel programs
Content Type	Text
Resource Type	Article
Subject	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

DETERMIN: inferring likely deterministic specifications of multithreaded programs

Determin: Inferring likely deterministic specifications of multithreaded programs (2010)

Determin: inferring likely deterministic specifications of multithreaded programs.

An OpenMP library for Java

Dynamic Generation of Likely Invariants for Multithreaded Programs

Asserting and checking determinism for multithreaded programs (2009)

Asserting and checking determinism for multithreaded programs

Exploiting Task Order Information for Optimizing Sequentially Consistent Java Programs

Verifying OO Programs by Linking Algebraic and Abstract Specifications

DETERMIN: inferring likely deterministic specifications of multithreaded programs

Similar Documents

DETERMIN: inferring likely deterministic specifications of multithreaded programs

Determin: Inferring likely deterministic specifications of multithreaded programs (2010)

Determin: inferring likely deterministic specifications of multithreaded programs.

An OpenMP library for Java

Dynamic Generation of Likely Invariants for Multithreaded Programs

Asserting and checking determinism for multithreaded programs (2009)

Asserting and checking determinism for multithreaded programs

Exploiting Task Order Information for Optimizing Sequentially Consistent Java Programs

Verifying OO Programs by Linking Algebraic and Abstract Specifications

DETERMIN: inferring likely deterministic specifications of multithreaded programs