Scenario driven concurrency bugs: model and check
View Patent ↗A computer implemented testing methodology employing a scenario-driven modeling of specific instances of bug patterns that commonly occur in concurrent programs which encodes these instances in an SMT-based symbolic analysis. Such modeling and encoding advantageously allow the symbolic analysis framework to focus on real bugs, thereby allowing effective utilization of resources. Experimentation determined a number of previously unknown bugs in public benchmarks and advantageously scenario-specific modeling and encoding improves the scalability of symbolic technique and, therefore, improves overall quality of concurrency testing.
1. A computer implemented method for identifying concurrency errors in a concurrent software program comprising the steps of:
constructing an initial concurrent trace model (CTM) from an observed concurrent event trace of the concurrent software program;
obtaining a set of independent transactions and a set of ordered pairs between the independent transactions by performing a mutually atomic transaction (MAT) analysis on the CTM;
identifying specific scenarios of errors that may correspond to concurrency errors;
generating a transaction interaction model for each of the scenarios identified;
encoding violation conditions for each of the scenarios and generating a quantifier-free satisfiability modulo theory (SMT) formula including the encoded violation conditions;
determining any feasible interleaving meeting one or more violation conditions through the effect of a SMT solver on the SMT formula; and
outputting any indicia of the interleaving.
2. A computer implemented method according to claim 1 , wherein the scenario specific errors include mismatch communication, improper resource utilization, and atomicity violation.
3. The computer implemented method according to claim 2 wherein the mismatch communication scenario generates specific instances corresponding to mismatched wait/notify, and send/receive synchronization pairs.
4. The computer implemented method according to claim 2 wherein the improper resource utilization scenario generates specific instances corresponding to various shared heap memory access errors.
5. The computer implemented method according to claim 2 wherein the atomicity violation scenario generates specific instances of non-atomic updates of inferred atomic regions comprising multiple shared accesses.
6. The computer implemented method according to claim 5 wherein the inferred atomic region is obtained from a code layout and a correlation of shared variables.