TY - GEN
T1 - Efficient predictive analysis for detecting nondeterminism in multi-threaded programs
AU - Sinha, Arnab
AU - Malik, Sharad
AU - Gupta, Aarti
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84874612849&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84874612849&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:84874612849
SN - 9781467348324
T3 - 2012 Formal Methods in Computer-Aided Design, FMCAD 2012
SP - 6
EP - 15
BT - 2012 Formal Methods in Computer-Aided Design, FMCAD 2012
T2 - 12th Conference on Formal Methods in Computer-Aided Design, FMCAD 2012
Y2 - 22 October 2012 through 25 October 2012
ER -