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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Poulsen, K.: Software bug contributed to blackout (2004), http://www.securityfocus.com/news/8016 (Online accessed July 16, 2011)
Lu, S., Tucek, J., Qin, F., Zhou, Y.: AVIO: detecting atomicity violations via access interleaving invariants. In: Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2006, San Jose, CA, USA, pp. 37–48 (2006)
Luk, C., Cohn, R., Muth, R., Patil, H., Klauser, A., Lowney, G., Wallace, S., Reddi, V.J., Hazelwood, K.: Pin: building customized program analysis tools with dynamic instrumentation. In: The 2005 ACM Conference on Programming Language Design and Implementation, PLDI 2005, Chicago, IL, USA, pp. 190–200 (2005)
Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley Professional (2003)
Lu, S., Park, S., Zhou, Y.: Finding Atomicity-Violation bugs through unserializable interleaving testing. IEEE Transactions on Software Engineering PP(99), 1 (2011)
Wang, C., Limaye, R., Ganai, M., Gupta, A.: Trace-Based Symbolic Analysis for Atomicity Violations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 328–342. Springer, Heidelberg (2010)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Communications of the ACM 21(7), 558–565 (1978)
Bernstein, P.A., Hadzilacos, V., Goodman, N.: Concurrency control and recovery in database systems, vol. 5. Addison-Wesley, New York (1987)
Yu, J., Narayanasamy, S.: A case for an interleaving constrained shared-memory multi-processor. In: Proceedings of the 36th International Symposium on Computer Architecture, ISCA 2009, Austin, TX, USA, pp. 325–336 (2009)
Woo, S.C., Ohara, M., Torrie, E., Singh, J.P., Gupta, A.: The SPLASH-2 programs: characterization and methodological considerations. In: Proceedings of the 22nd International Symposium on Computer Architecture, ISCA 1995, Madison, WI, USA, pp. 24–36 (1995)
Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI 2008, San Diego, CA, USA, pp. 267–280 (2008)
Flanagan, C., Freund, S.N., Yi, J.: Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008, Tucson, AZ, USA, pp. 293–303 (2008)
Wang, L., Stoller, S.D.: Runtime analysis of atomicity for multithreaded programs. IEEE Transactions on Software Engineering 32, 93–110 (2006)
Sorrentino, F., Farzan, A., Madhusudan, P.: Penelope: weaving threads to expose atomicity violations. In: Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2010, Santa Fe, NM, USA, pp. 37–46 (2010)
Farzan, A., Madhusudan, P.: The Complexity of Predicting Atomicity Violations. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 155–169. Springer, Heidelberg (2009)
Chen, F., Serbanuta, T.F., Rosu, G.: jPredictor: a predictive runtime analysis tool for java. In: Proceedings of the 30th International Conference on Software Engineering, ICSE 2008, Leipzig, Germany, pp. 221–230 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zeng, R., Sun, Z., Liu, S., He, X. (2012). McPatom: A Predictive Analysis Tool for Atomicity Violation Using Model Checking. In: Donaldson, A., Parker, D. (eds) Model Checking Software. SPIN 2012. Lecture Notes in Computer Science, vol 7385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31759-0_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-31759-0_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31758-3
Online ISBN: 978-3-642-31759-0
eBook Packages: Computer ScienceComputer Science (R0)