McPatom: A predictive analysis tool for atomicity violation using model checking Conference

Zeng, R, Sun, Z, Liu, S et al. (2012). McPatom: A predictive analysis tool for atomicity violation using model checking . Lecture Notes in Computer Science, 7385 LNCS 191-207. 10.1007/978-3-642-31759-0_14

cited authors

  • Zeng, R; Sun, Z; Liu, S; He, X

abstract

  • Multi-thread programs are prone to bugs due to concurrency. Concurrency bugs are hard to find and reproduce because of the large number of interleavings. Most non-deadlock concurrency bugs are atomicity violation bugs due to unprotected accesses of shared variables by multiple threads. This paper presents a dynamic prediction tool named McPatom for predicting atomicity violation bugs involving a pair of threads accessing a shared variable using model checking. McPatom uses model checking to ensure the completeness in predicting any possible atomicity violation captured in the abstract thread model extracted from an interleaved execution. McPatom can predict atomicity violations involving more than three accesses and multiple subroutines, and supports all synchronization primitives. We have applied McPatom in predicting several known bugs in real world systems including one that evades several other existing tools. We provide evaluations of McPatom in terms of atomicity violation predictability and performance with additional improvement strategies. © 2012 Springer-Verlag Berlin Heidelberg.

authors

publication date

  • August 15, 2012

published in

Digital Object Identifier (DOI)

start page

  • 191

end page

  • 207

volume

  • 7385 LNCS