Meta-analysis for Atomicity Violations under Nested Locking

Abstract. We study the problem of determining, given a run of a concurrent program, whether there is any alternate execution of it that violates atomicity, where atomicity is defined using marked blocks of local runs. We show that if a concurrent program adopts nested locking, the problem of predicting atomicity violations is efficiently solvable, without exploring all interleavings. In particular, for the case of atomicity violations involving only two threads and a single variable, which covers many of the atomicity errors reported in bug databases, we exhibit efficient algorithms that work in time that is linear in the length of the runs, and quadratic in the number of threads. Moreover, we report on an implementation of this algorithm, and show experimentally that it scales well for benchmark concurrent programs and is effective in predicting a large number of atomicity violations even from a single run.

• Type: Conference
• Year: 2009
• Where: CAV
• Authors: Azadeh Farzan, P. Madhusudan, Francesco Sorrentino
• Keywords: Atomicity Errors, Atomicity Violations, CAV 2009, Concurrent Program Adopts, Formal Methods