Efficient predictive analysis for detecting nondeterminism in multi-threaded programs

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Scopus citations

Abstract

Determinism is often a desired property in multithreaded programs. A multi-threaded program is said to be deterministic if for a given input, different thread interleavings result in the same system state in the execution of the program. This, in turn, requires that different interleavings preserve the values read by each read operation. A related, but less strict condition is for the program to be race-free. A deterministic program is race-free but the converse may not be true. There is much work done in the static analysis of programs to detect races and nondeterminism. However, this can be expensive and may not complete for large programs in reasonable time. In contrast to static analysis, predictive analysis techniques take a given program trace and explore other possible interleavings that may violate a given property - in this case the property of interest is determinism. Predictive analysis can be sound, but is not complete as it is limited to a specific set of program runs. Nonetheless, it is of interest as it offers greater scalability than static analysis. This work presents a predictive analysis method for detecting nondeterminism in multi-threaded programs. Potential cases of nondeterminism are checked by constructing a causality graph from the thread events and confirming that it is acyclic. On average, the number of graphs analyzed per benchamrk is one per potential case of nondeterminism, thereby ensuring that it is efficient. We demonstrate its application on some benchmark Java and C/C++ programs.

Original languageEnglish (US)
Title of host publication2012 Formal Methods in Computer-Aided Design, FMCAD 2012
Pages6-15
Number of pages10
StatePublished - 2012
Event12th Conference on Formal Methods in Computer-Aided Design, FMCAD 2012 - Cambridge, United Kingdom
Duration: Oct 22 2012Oct 25 2012

Publication series

Name2012 Formal Methods in Computer-Aided Design, FMCAD 2012

Other

Other12th Conference on Formal Methods in Computer-Aided Design, FMCAD 2012
Country/TerritoryUnited Kingdom
CityCambridge
Period10/22/1210/25/12

All Science Journal Classification (ASJC) codes

  • Computer Graphics and Computer-Aided Design
  • Computer Vision and Pattern Recognition

Fingerprint

Dive into the research topics of 'Efficient predictive analysis for detecting nondeterminism in multi-threaded programs'. Together they form a unique fingerprint.

Cite this