On interleaving space exploration of multi-threaded programs

Abstract

Exploring the interleaving space of a multithreaded program to efficiently detect concurrency bugs is important but also difficult because of the astronomically many thread schedules. This paper presents a novel framework to decompose a thread schedule generator that explores the interleaving space into the composition of a basic generator and its extension under the “small interleaving hypothesis”. Under this framework, we in-depth analyzed research work on interleaving space exploration, illustrated how to design an effective schedule generator, and shed light on future research opportunities.

Keywords

survey / testing / concurrency bugs / interleaving space

References

[1] Voung J W, Jhala R, Lerner S. RELAY: static race detection on millions of lines of code. In: Proceedings of Joint Meeting of the European Software Engineering Conference and the ACMSIGSOFT Symposium on the Foundations of Software Engineering. 2007, 205–214

[2] Naik M, Aiken A, Whaley J. Effective static race detection for java. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2006, 308–319

[3] Blackshear S, Gorogiannis N, O’Hearn P W, Sergey I. RacerD: compositional static race detection. In: Proceedings of ACM International Conference on Object Oriented Programming, Systems, Languages, and Applications. 2018, 1–28

[4] Gorogiannis N, O’Hearn P W, Sergey I. A true positives theorem for a static race detector. In: Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2019, 1–29

[5] Savage S, Burrows M, Nelson G, Sobalvarro P, Anderson T. Eraser: a dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems, 1997, 15(4): 391–411

[6] Netzer R. Race Condition Detection for Debugging Shared-memory Parallel Programs. University of Wisconsin-Madison, 1991

[7] Smaragdakis Y, Evans J, Sadowski C, Yi J, Flanagan C. Sound predictive race detection in polynomial time. In: Proceedings of Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2012, 387–400

[8] O’Callahan R, Choi J D. Hybrid dynamic data race detection. ACM SIGPLAN Notices, 2003, 38(10): 167–178

[9] Sheng T, Vachharajani N, Eranian S, Hundt R, Chen W, Zheng W. RACEZ: a lightweight and non-invasive race detection tool for production applications. In: Proceedings of International Conference on Software Engineering. 2011, 401–410

[10] Flanagan C, Freund S N. FastTrack: efficient and precise dynamic race detection. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2009, 121–133

[11] Marino D, Musuvathi M, Narayanasamy S. LiteRace: effective sampling for lightweight data-race detection. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2009, 134–143

[12] Bond MD, Coons K E, McKinley K S. PACER: proportional detection of data races. ACM SIGPLAN Notices, 2010, 45(6): 255–268

[13] Prvulovic M, Torrellas J. ReEnact: using thread-level speculation mechanisms to debug data races in multithreaded codes. In: Proceedings of Annual International Symposium on Computer Architecture. 2003, 110–121

[14] Rajagopalan A K, Huang J. RDIT: race detection from incomplete traces. In: Proceedings of Joint Meeting on Foundations of Software Engineering. 2015, 914–917

[15] Cai Y, Cao L. Effective and precise dynamic detection of hidden races for java programs. In: Proceedings of Joint Meeting on Foundations of Software Engineering. 2015, 450–461

[16] Petrov B, Vechev M, Sridharan M, Dolby J. Race detection for web applications. In: Proceedings of ACMSIGPLAN Conference on Programming Language Design and Implementation. 2012, 251–262

[17] Raychev V, Vechev M, Sridharan M. Effective race detection for eventdriven programs. In: Proceedings of ACM SIGPLAN International Conference on Object Oriented Programming, Systems, Languages, and Applications. 2013, 151–166

[18] Maiya P, Kanade A, Majumdar R. Race detection for android applications. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2014, 316–325

[19] Yu Y, Rodeheffer T, Chen W. RaceTrack: efficient detection of data race conditions via adaptive tracking. In: Proceedings of ACM Symposium on Operating Systems Principles. 2005, 221–234

[20] Kasikci B, Zamfir C, Candea G. RaceMob: crowdsourced data race detection. In: Proceedings of ACM Symposium on Operating Systems Principles. 2013, 406–422

[21] Choi J D, Lee K, Loginov A, O’Callahan R, Sarkar V, Sarkar V, Sridharan M. Efficient and precise datarace detection for multithreaded object oriented programs. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2002, 258–269

[22] Narayanasamy S, Wang Z, Tigani J, Edwards A, Calder B. Automatically classifying benign and harmful data races using replay analysis. ACM SIGPLAN Notices, 2007, 42(6): 22–31

[23] Kasikci B, Zamfir C, Candea G. Data races vs. data race bugs: telling the difference with portend. ACM SIGPLAN Notices, 2012, 47(4): 185–198

[24] Lu S, Tucek J, Qin F, Zhou Y. AVIO: detecting atomicity violations via access interleaving invariants. In: Proceedings of International Conference on Architectural Support for Programming Languages and Operating Systems. 2006, 37–48

[25] Flanagan C, Freund S N, Yi J. Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2008, 293–303

[26] Park C S, Sen K. Randomized active atomicity violation detection in concurrent programs. In: Proceedings of ACM SIGSOFT International Symposium on Foundations of Software Engineering. 2008, 135–145

[27] Park S, Lu S, Zhou Y. CTrigger: exposing atomicity violation bugs from their hiding places. In: Proceedings of International Conference on Architectural Support for Programming Languages and Operating Systems. 2009, 25–36

[28] Park S, Vuduc R W, Harrold M J. Falcon: fault localization in concurrent programs. In: Proceedings of ACM/IEEE International Conference on Software Engineering. 2010, 245–254

[29] Biswas S, Huang J, Sengupta A, Bond M D. DoubleChecker: efficient sound and precise atomicity checking. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2014, 28–39

[30] Flanagan C, Freund S N. Atomizer: a dynamic atomicity checker for multithreaded programs. In: Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2004, 256–267

[31] Lu S, Park S, Hu C, Ma X, Jiang W, Li Z, Popa R A, Zhou Y. MUVI: automatically inferring multi-variable access correlations and detecting related semantic and concurrency bugs. In: Proceedings of ACM SIGOPS Symposium on Operating Systems Principles. 2007, 103–116

[32] Havelund K. Using runtime analysis to guide model checking of java programs. In: Proceedings of International SPINWorkshop onModel Checking of Software. 2000, 245–264

[33] Cai Y, Wu S, Chan W K. ConLock: a constraint-based approach to dynamic checking on deadlocks in multithreaded programs. In: Proceedings of International Conference on Software Engineering. 2014, 491–502

[34] Eslamimehr M, Palsberg J. Sherlock: scalable deadlock detection for concurrent programs. In: Proceedings of ACM SIGSOFT International Symposium on Foundations of Software Engineering. 2014, 353–365

[35] Sen K. Effective random testing of concurrent programs. In: Proceedings of IEEE/ACM International Conference on Automated Software Engineering. 2007, 323–332

[36] Bianchi F A, Margara A, Pezzè M. A survey of recent trends in testing concurrent software systems. IEEE Transactions on Software Engineering, 2018, 44(8): 747–783

[37] Thomson P, Donaldson A F, Betts A. Concurrency testing using schedule bounding: an empirical study. In: Proceedings of ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. 2014, 15–28

[38] Desai A, Qadeer S, Seshia S A. Systematic testing of asynchronous reactive systems. In: Proceedings of Joint Meeting on Foundations of Software Engineering. 2015, 73–83

[39] Fu H, Wang Z, Chen X, Fan X. A systematic survey on automated concurrency bug detection, exposing, avoidance, and fixing techniques. Software Quality Journal, 2018, 26(3): 855–889

[40] Arora V, Bhatia R, Singh M. A systematic review of approaches for testing concurrent programs. Concurrency and Computation: Practice and Experience, 2016, 28(5): 1572–1611

[41] Souza S R S, Brito M A S, Silva R A, Souza P S L, Zaluska E. Research in concurrent software testing: a systematic review. In: Proceedings of Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging. 2011, 1–5

[42] Sewell P, Sarkar S, Owens S, Nardelli F Z, Myreen M O. X86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Communications of the ACM, 2010, 53(7): 89–97

[43] Manson J, Pugh W, Adve S V. The java memory model. In: Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2005, 378–391

[44] Godefroid P. Model checking for programming languages using veriSoft. In: Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 1997, 174–186

[45] Musuvathi M, Qadeer S. Iterative context bounding for systematic testing of multithreaded programs. ACM SIGPLAN Notices, 2007, 42(6): 446–455

[46] Emmi M, Qadeer S, Rakamarić Z. Delay-bounded scheduling. ACMSIGPLAN Notices, 2011, 46(1): 411–422

[47] Burckhardt S, Kothari P, Musuvathi M, Nagarakatte S. A randomized scheduler with probabilistic guarantees of finding bugs. In: Proceedings of International Conference on Architectural Support for Programming Languages and Operating Systems. 2010, 167–178

[48] Godefroid P, Sen K. Combining Model Checking and Testing. In: Handbook of Model Checking. Springer, Cham, 2018, 613–649

[49] Andoni A, Daniliuc D, Khurshid S. Evaluating the “Small Scope Hypothesis”. 2003

[50] Lu S, Park S, Seo E, Zhou Y. Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: Proceedings of International Conference on Architectural Support for Programming Languages and Operating Systems. 2008, 329–339

[51] Qadeer S, Rehof J. Context-bounded model checking of concurrent software. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2005, 93–107

[52] Nagarakatte S, Burckhardt S, Martin M M, Musuvathi M. Multicore acceleration of priority-based schedulers for concurrency bug detection. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2012, 543–554

[53] Nistor A, Luo Q, Pradel M, Gross T R, Marinov D. BALLERINA: automatic generation and clustering of efficient random unit tests for multithreaded code. In: Proceedings of International Conference on Software Engineering. 2012, 727–737

[54] Li G, Lu S, Musuvathi M, Nath S, Padhye R. Efficient scalable threadsafety- violation detection: finding thousands of concurrency bugs during testing. In: Proceedings of ACM Symposium on Operating Systems Principles. 2019, 162–180

[55] Sen K. Race directed random testing of concurrent programs. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2008, 11–21

[56] Joshi P, Park C S, Sen K, Naik M. A randomized dynamic program analysis technique for detecting real deadlocks. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2009, 110–120

[57] Yuan X, Yang J, Gu R. Partial order aware concurrency sampling. In: Proceedings of International Conference on Computer Aided Verification. 2018, 317–335

[58] Arpaci-Dusseau R H, Arpaci-Dusseau A C. Operating Systems: Three Easy Pieces. Arpaci-Dusseau Books, LLC, 2018

[59] Davis R I, Cucu-Grosjean L, Bertogna M, Burns A. A review of priority assignment in real-time systems. Journal of Systems Architecture, 2016, 65: 64–82

[60] Chen D, Jiang Y, Xu C, Ma X, Lu J. Testing multithreaded programs via thread speed control. In: Proceedings of ACM JointMeeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 2018, 15–25

[61] Musuvathi M, Qadeer S, Ball T, Basler G, Nainar P A, Neamtiu I. Finding and reproducing heisenbugs in concurrent programs. In: Proceedings of USENIX Conference on Operating Systems Design and Implementation. 2008, 267–280

[62] Godefroid P. Partial-order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Heidelberg: Springer, 1996

[63] Flanagan C, Godefroid P. Dynamic partial-order reduction for model checking software. In: Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2005, 110–121

[64] Yang Y, Chen X, Gopalakrishnan G. Inspect: a runtime model checker for multithreaded C programs. Technical Report, 2008

[65] Kokologiannakis M, Raad A, Vafeiadis V. Effective lock handling in stateless model checking. Proceedings of the ACM on Programming Languages. 2019, 3(OOPSLA): 1–26

[66] Lu S, Jiang W, Zhou Y. A study of interleaving coverage criteria. In: Proceedings of JointMeeting on European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering: Companion Papers. 2007, 533–536

[67] Bron A, Farchi E, Magid Y, Nir Y, Ur S. Applications of synchronization coverage. In: Proceedings of ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. 2005, 206–212

[68] Hong S, Ahn J, Park S, Kim M, Harrold M J. Testing concurrent programs to achieve high synchronization coverage. In: Proceedings of International Symposium on Software Testing and Analysis. 2012, 210–220

[69] Yu J, Narayanasamy S. A case for an interleaving constrained sharedmemory multi-processor. In: Proceedings of Annual International Symposium on Computer Architecture. 2009, 325–336

[70] Wang C, Said M, Gupta A. Coverage guided systematic concurrency testing. In: Proceedings of International Conference on Software Engineering. 2011, 221–230

[71] Burnim J, Elmas T, Necula G, Sen K. CONCURRIT: testing concurrent programs with programmable state-space exploration. In: Proceedings of the 4th USENIX Workshop on Hot Topics in Parallelism. 2012

[72] Huang J, Meredith P O, Rosu G. Maximal sound predictive race detection with control flow abstraction. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2014, 337–348

[73] Huang S, Huang J. Maximal causality reduction for TSO and PSO. In: Proceedings of ACM SIGPLAN International Conference on Object- Oriented Programming, Systems, Languages, and Applications. 2016, 447–461

[74] Huang J, Luo Q, Rosu G. GPredict: generic predictive concurrency analysis. In: Proceedings of International Conference on Software Engineering. 2015, 847–857

[75] Eslamimehr M, Palsberg J. Race directed scheduling of concurrent programs. In: Proceedings of ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. 2014, 301–314

[76] Godefroid P, Klarlund N, Sen K. DART: directed automated random testing. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2005, 213–223

[77] Sen K. Concolic testing. In: Proceedings of IEEE/ACM International Conference on Automated Software Engineering. 2007, 571–572

[78] Sorrentino F, Farzan A, Madhusudan P. PENELOPE: weaving threads to expose atomicity violations. In: Proceedings of ACM SIGSOFT International Symposium on Foundations of Software Engineering. 2010, 37–46

[79] Lu G, Xu L, Yang Y, Xu B. Predictive analysis for race detection in software-defined networ. Sciece China Information Sciences, 2019, 62(6): 62101

[80] De Moura L, Bjørner N. Z3: an efficient SMT solver. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2008, 337–340

[81] Joshi P, Naik M, Sen K, Gay D. An effective dynamic analysis for detecting generalized deadlocks. In: Proceedings of ACM SIGSOFT International Symposium on Foundations of Software Engineering. 2010, 327–336

[82] Musuvathi M, Qadeer S. Fair stateless model checking. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2008, 362–371

[83] Batty M, Owens S, Sarkar S, Sewell P, Weber T. Mathematizing C++ concurrency. In: Proceedings of Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2011, 55–66

[84] Norris B, Demsky B. CDSchecker: checking concurrent data structures written with C/C++ atomics. ACM SIGPLAN Notices, 2013, 48(10): 131–150

[85] Kasikci B, Cui W, Ge X, Niu B. Lazy diagnosis of in-production concurrency bugs. In: Proceedings of the 26th Symposium on Operating Systems Principles. 2017, 582–598

[86] Guo S, Kusano M, Wang C, Yang Z, Gupta A. Assertion guided symbolic execution of multithreaded programs. In: Proceedings of Joint Meeting on Foundations of Software Engineering. 2015, 854–865

[87] Bergan T, Grossman D, Ceze L. Symbolic execution of multithreaded programs from arbitrary program contexts. In: Proceedings of ACM International Conference on Object Oriented Programming, Systems, Languages, and Applications. 2014, 491–506

[88] Guo S, Kusano M, Wang C. Conc-ISE: incremental symbolic execution of concurrent software. In: Proceedings of IEEE/ACMInternational Conference on Automated Software Engineering. 2016, 531–542

[89] Farzan A, Holzer A, Razavi N, Veith H. Con2colic testing. In: Proceedings of Joint Meeting on Foundations of Software Engineering. 2013, 37–47

RIGHTS & PERMISSIONS

2020 Higher Education Press