×

Abstraction and mining of traces to explain concurrency bugs. (English) Zbl 1380.68107

Summary: We propose an automated mining-based method for explaining concurrency bugs. We use a data mining technique called sequential pattern mining to identify problematic sequences of concurrent read and write accesses to the shared memory of a multithreaded program. Our technique does not rely on any characteristics specific to one type of concurrency bug, thus providing a general framework for concurrency bug explanation. In our method, given a set of concurrent execution traces, we first mine sequences that frequently occur in failing traces and then rank them based on the number of their occurrences in passing traces. We consider the highly ranked sequences of events that occur frequently only in failing traces an explanation of the system failure, as they can reveal its causes in the execution traces. Since the scalability of sequential pattern mining is limited by the length of the traces, we present an abstraction technique which shortens the traces at the cost of introducing spurious explanations. Spurious as well as misleading explanations are then eliminated by a subsequent filtering step, helping the programmer to focus on likely causes of the failure. We validate our approach using a number of case studies, including synthetic as well as real-world bugs.

MSC:

68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68T05 Learning and adaptive systems in artificial intelligence
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] http://bzip2smp.sourceforge.net/, (bzip2smp 1.0). Accessed in Sept 2015
[2] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. CAV, LNCS 1855:154-169 · Zbl 0974.68517
[3] Delgado N, Gates AQ, Roach S (2004) A taxonomy and catalog of runtime software-fault monitoring tools. IEEE Trans Softw Eng (TSE) 30(12):859-872 · doi:10.1109/TSE.2004.91
[4] Elmas T, Qadeer S, Tasiran S (2010) Goldilocks: a race-aware Java runtime. Commun ACM 53(11):85-92 · doi:10.1145/1839676.1839698
[5] Engler DR, Ashcraft K (2003) RacerX: effective, static detection of race conditions and deadlocks. In: Symposium on operating systems principles (SOSP), ACM 2003, pp 237-252
[6] Erickson J, Musuvathi M, Burckhardt S, Olynyk K. (2010) Effective data-race detection for the kernel. In: USENIX symposium on operating systems design and implementation (OSDI), USENIX Association 2010, pp 151-162
[7] Flanagan C, Freund SN (2010) FastTrack: efficient and precise dynamic race detection. Commun ACM 53(11):93-101 · doi:10.1145/1839676.1839699
[8] Flanagan C, Qadeer S (2003) A type and effect system for atomicity. In: PLDI, ACM 2003, pp 338-349
[9] Fleming SD, Kraemer E, Stirewalt REK, Xie S, Dillon LK (2008) A study of student strategies for the corrective maintenance of concurrent software. In: International conference on software engineering (ICSE), ACM 2008, pp 759-768
[10] Hammer C, Dolby J, Vaziri M, Tip F (2008) Dynamic detection of atomic-set-serializability violations. In: International conference on software engineering (ICSE), ACM 2008, pp 231-240
[11] Herlihy M, Shavit N (2008) The art of multiprocessor programming. Morgan Kaufmann, Burlington
[12] LeBlanc TJ, Mellor-Crummey JM (1987) Debugging parallel programs with instant replay. IEEE Trans Comput 36(4):471-482 · doi:10.1109/TC.1987.1676929
[13] Leue S, Tabaei-Befrouei M (2012) Counterexample explanation by anomaly detection. In: Model checking and software verification (SPIN), 2012
[14] Leue S, Tabaei-Befrouei M (2013) Mining sequential patterns to explain concurrent counterexamples. In: Model checking and software verification (SPIN), 2013
[15] Lewis D (2001) Counterfactuals. Wiley-Blackwell, New York · Zbl 0989.03003
[16] Lu S, Jiang W, Zhou Y (2007) A study of interleaving coverage criteria. In: Foundations of software engineering (FSE), ESEC-FSE Companion, ACM 2007, pp 533-536
[17] Lu S, Park S, Seo E, Zhou Y (2008) Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: ACM Sigplan Notices, ACM 2008, vol 43, pp 329-339 · Zbl 0974.68517
[18] Lu S, Tucek J, Qin F, Zhou Y (2006) AVIO: detecting atomicity violations via access interleaving invariants. In: Architectural support for programming languages and operating systems (ASPLOS), 2006
[19] Lucia B, Ceze L (2009) Finding concurrency bugs with context-aware communication graphs. In: Symposium on microarchitecture (MICRO), ACM 2009, pp 553-563
[20] Mabroukeh NR, Ezeife CI (2010) A taxonomy of sequential pattern mining algorithms. ACM Comput Surv 43(1):3:1-3:41. doi:10.1145/1824795.1824798 · doi:10.1145/1824795.1824798
[21] Mazurkiewicz AW (1986) Trace theory. In: Petri nets: central models and their properties, advances in petri nets, LNCS, Springer, vol 255, pp 279-324
[22] Musuvathi M, Qadeer S (2006) CHESS: systematic stress testing of concurrent software. In: Logic-based program synthesis and transformation (LOPSTR), LNCS, Springer, vol 4407, pp 15-16
[23] Musuvathi M, Qadeer S (2007) Iterative context bounding for systematic testing of multithreaded programs. In: PLDI, ACM 2007, pp 446-455. doi:10.1145/1250734.1250785
[24] Musuvathi M, Qadeer S, Ball T (2007) CHESS: a systematic testing tool for concurrent software. Tech Rep MSR-TR-2007-149, Microsoft Research, 2007
[25] Netzer RHB, Miller BP (1991) Improving the accuracy of data race detection. SIGPLAN Notices 26(7):133-144. doi:10.1145/109626.109640 · doi:10.1145/109626.109640
[26] Papadimitriou CH (1979) The serializability of concurrent database updates. J ACM 26(4):631-653 · Zbl 0419.68036 · doi:10.1145/322154.322158
[27] Park S, Lu S, Zhou Y (2009) CTrigger: exposing atomicity violation bugs from their hiding places. In: Architectural support for programming languages and operating systems (ASPLOS), ACM, 2009, pp 25-36
[28] Park S, Vuduc R, Harrold MJ (2012) A unified approach for localizing non-deadlock concurrency bugs. In: Software testing, verification and validation (ICST), IEEE 2012, pp 51-60
[29] Park S, Vuduc RW, Harrold MJ (2010) Falcon: fault localization in concurrent programs. In: International conference on software engineering (ICSE), ACM 2010, pp 245-254
[30] Pei J, Han J, Mortazavi-Asl B, Pinto H, Chen Q, Dayal U, Hsu M (2001) PrefixSpan: Mining sequential patterns efficiently by prefix-projected pattern growth. In: 17th international conference on data engineering (ICDE’01), 2001
[31] Rößler J, Fraser G, Zeller A, Orso A (2012) Isolating failure causes through test case generation. In: International symposium on software testing and analysis, ACM 2012, pp 309-319
[32] Savage S, Burrows M, Nelson G, Sobalvarro P, Anderson T (1997) Eraser: a dynamic data race detector for multithreaded programs. Trans Comput Syst (TOCS) 15(4):391-411. doi:10.1145/265924.265927 · doi:10.1145/265924.265927
[33] Tabaei-Befrouei M, Wang C, Weissenbacher G (2014) Abstraction and mining of traces to explain concurrency bugs. In: Proceedings of the 14th international conference on runtime verification (RV), 2014 · Zbl 1380.68107
[34] Wang J, Han J (2004) Bide: efficient mining of frequent closed sequences. In: ICDE, 2004
[35] Wang L, Stoller SD (2006) Runtime analysis of atomicity for multithreaded programs. TSE 32(2):93-110
[36] Xu M, Bodík R, Hill MD (2005) A serializability violation detector for shared-memory server programs. In: PLDI, ACM 2005, pp 1-14
[37] Yan X, Han J, Afshar R (2003) CloSpan: mining closed sequential patterns in large datasets. In: Proceedings of 2003 SIAM international conference on data mining (SDM’03), 2003
[38] Yang Y, Chen X, Gopalakrishnan G, Kirby RM (2007) Distributed dynamic partial order reduction based verification of threaded software. In: Model checking and software verification (SPIN), LNCS 2007, pp 58-75
[39] Zeller A (2009) Why Programs Fail: A Guide to Systematic Debugging. Morgan Kaufmann, Burlington
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.