On interleaving space exploration of multi-threaded programs | Frontiers of Computer Science Skip to main content
Springer Nature Link
Log in

On interleaving space exploration of multi-threaded programs

  • Research Article
  • Published:
Frontiers of Computer Science Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

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 ACM SIGSOFT 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

    Article  Google Scholar 

  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

    Article  Google Scholar 

  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 M D, Coons K E, McKinley K S. PACER: proportional detection of data races. ACM SIGPLAN Notices, 2010, 45(6): 255–268

    Article  Google Scholar 

  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 ACM SIGPLAN Conference on Programming Language Design and Implementation. 2012, 251–262

  17. Raychev V, Vechev M, Sridharan M. Effective race detection for event-driven 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

    Article  Google Scholar 

  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

    Article  Google Scholar 

  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 SPIN Workshop on Model 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

    Article  Google Scholar 

  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

    Article  Google Scholar 

  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

    Article  Google Scholar 

  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

    Article  Google Scholar 

  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

    Article  Google Scholar 

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

    Article  Google Scholar 

  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

    Chapter  Google Scholar 

  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 thread-safety-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 Joint Meeting 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

    Book  Google Scholar 

  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

    Article  Google Scholar 

  66. Lu S, Jiang W, Zhou Y. A study of interleaving coverage criteria. In: Proceedings of Joint Meeting 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 shared-memory 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

    Article  Google Scholar 

  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

    Article  Google Scholar 

  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/ACM International 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

Download references

Acknowledgements

The authors would like to thank the anonymous reviewers for comments and suggestions. This work was supported in part by National Key R&D Program (2017YFB1001801) of China, the National Natural Science Foundation of China (Grant Nos. 61932021, 61690204, 61802165). The authors would like to thank the support from the Collaborative Innovation Center of Novel Software Technology and Industrialization, Jiangsu, China.

Author information

Authors and Affiliations

  1. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, 210023, China

    Dongjie Chen, Yanyan Jiang, Chang Xu & Xiaoxing Ma

  2. Department of Computer Science and Technology, Nanjing University, Nanjing, 210023, China

    Dongjie Chen, Yanyan Jiang, Chang Xu & Xiaoxing Ma

Authors
  1. Dongjie Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yanyan Jiang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Chang Xu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Xiaoxing Ma
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Yanyan Jiang or Chang Xu.

Additional information

Dongjie Chen is a second year PhD student in Department of Computer Science and Technology at Nanjing University, China. He received his bachelor degree in computer science and technology from Nanjing University, China. His research is mainly about multi-threaded programs anslysis.

Yanyan Jiang is an assistant researcher of Nanjing University, China. His research interests include software testing, analysis, and synthesis. He was a recipient of ACM SIGSOFT Distinguished Paper Award, CCF Outstanding Doctoral Dissertation Award, and Microsoft Research Asia Fellowship Award. He is also as a Scientific Committee member of provincial Computing Olympiad contests.

Chang Xu received his doctoral degree in computer science and engineering from The Hong Kong University of Science and Technology, China. He is a full professor with the State Key Laboratory for Novel Software Technology and Department of Computer Science and Technology at Nanjing University, China. He participates actively in program and organizing committees of major international software engineering conferences. His research interests include big data software engineering, intelligent software testing and analysis, and adaptive and autonomous software systems. He is a senior member of the CCF and IEEE, and a member of the ACM.

Xiaoxing Ma received his doctoral degree in computer science and technology from Nanjing University, China. He is a full professor with the State Key Laboratory for Novel Software Technology and Department of Computer Science and Technology at Nanjing University, China. His research interests include self-adaptive software systems, software architectures, and quality assurance for machine learning models used as software components. He co-authored more than 100 peer-reviewed conference and journal papers and has served as technical program committee members on various international conferences. He is a member of the IEEE and the ACM.

Electronic supplementary material

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Chen, D., Jiang, Y., Xu, C. et al. On interleaving space exploration of multi-threaded programs. Front. Comput. Sci. 15, 154206 (2021). https://doi.org/10.1007/s11704-020-9501-6

Download citation

  • Received:

  • Accepted:

  • Published:

  • DOI: https://doi.org/10.1007/s11704-020-9501-6

Keywords

Search

Navigation