1. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210023, China 2. Department of Computer Science and Technology, Nanjing University, Nanjing 210023, China
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.
J W Voung, R Jhala, S Lerner. 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 https://doi.org/10.1145/1287624.1287654
2
M Naik, A Aiken, J Whaley. Effective static race detection for java. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2006, 308–319 https://doi.org/10.1145/1133255.1134018
3
S Blackshear, N Gorogiannis, P W O’Hearn, I Sergey. RacerD: compositional static race detection. In: Proceedings of ACM International Conference on Object Oriented Programming, Systems, Languages, and Applications. 2018, 1–28 https://doi.org/10.1145/3276514
4
N Gorogiannis, P W O’Hearn, I Sergey. A true positives theorem for a static race detector. In: Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2019, 1–29 https://doi.org/10.1145/3290370
5
S Savage, M Burrows, G Nelson, P Sobalvarro, T Anderson. Eraser: a dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems, 1997, 15(4): 391–411 https://doi.org/10.1145/265924.265927
6
R Netzer. Race Condition Detection for Debugging Shared-memory Parallel Programs. University of Wisconsin-Madison, 1991
7
Y Smaragdakis, J Evans, C Sadowski, J Yi, C Flanagan. Sound predictive race detection in polynomial time. In: Proceedings of Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2012, 387–400 https://doi.org/10.1145/2103621.2103702
T Sheng, N Vachharajani, S Eranian, R Hundt, W Chen, W Zheng. RACEZ: a lightweight and non-invasive race detection tool for production applications. In: Proceedings of International Conference on Software Engineering. 2011, 401–410
10
C Flanagan, S N Freund. FastTrack: efficient and precise dynamic race detection. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2009, 121–133 https://doi.org/10.1145/1543135.1542490
11
D Marino, M Musuvathi, S Narayanasamy. LiteRace: effective sampling for lightweight data-race detection. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2009, 134–143 https://doi.org/10.1145/1543135.1542491
12
MD Bond, K E Coons, K S McKinley. PACER: proportional detection of data races. ACM SIGPLAN Notices, 2010, 45(6): 255–268 https://doi.org/10.1145/1809028.1806626
13
M Prvulovic, J Torrellas. 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 https://doi.org/10.1145/871656.859632
14
A K Rajagopalan, J Huang. RDIT: race detection from incomplete traces. In: Proceedings of Joint Meeting on Foundations of Software Engineering. 2015, 914–917 https://doi.org/10.1145/2786805.2803209
15
Y Cai, L Cao. Effective and precise dynamic detection of hidden races for java programs. In: Proceedings of Joint Meeting on Foundations of Software Engineering. 2015, 450–461 https://doi.org/10.1145/2786805.2786839
16
B Petrov, M Vechev, M Sridharan, J Dolby. Race detection for web applications. In: Proceedings of ACMSIGPLAN Conference on Programming Language Design and Implementation. 2012, 251–262 https://doi.org/10.1145/2345156.2254095
17
V Raychev, M Vechev, M Sridharan. Effective race detection for eventdriven programs. In: Proceedings of ACM SIGPLAN International Conference on Object Oriented Programming, Systems, Languages, and Applications. 2013, 151–166 https://doi.org/10.1145/2544173.2509538
18
P Maiya, A Kanade, R Majumdar. Race detection for android applications. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2014, 316–325 https://doi.org/10.1145/2666356.2594311
19
Y Yu, T Rodeheffer, W Chen. RaceTrack: efficient detection of data race conditions via adaptive tracking. In: Proceedings of ACM Symposium on Operating Systems Principles. 2005, 221–234 https://doi.org/10.1145/1095809.1095832
20
B Kasikci, C Zamfir, G Candea. RaceMob: crowdsourced data race detection. In: Proceedings of ACM Symposium on Operating Systems Principles. 2013, 406–422 https://doi.org/10.1145/2517349.2522736
21
J D Choi, K Lee, A Loginov, R O’Callahan, V Sarkar, V Sarkar, M Sridharan. 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 https://doi.org/10.1145/543552.512560
22
S Narayanasamy, Z Wang, J Tigani, A Edwards, B Calder. Automatically classifying benign and harmful data races using replay analysis. ACM SIGPLAN Notices, 2007, 42(6): 22–31 https://doi.org/10.1145/1273442.1250738
23
B Kasikci, C Zamfir, G Candea. Data races vs. data race bugs: telling the difference with portend. ACM SIGPLAN Notices, 2012, 47(4): 185–198 https://doi.org/10.1145/2248487.2150997
24
S Lu, J Tucek, F Qin, Y Zhou. 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 https://doi.org/10.1145/1168917.1168864
25
C Flanagan, S N Freund, J Yi. 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 https://doi.org/10.1145/1379022.1375618
26
C S Park, K Sen. Randomized active atomicity violation detection in concurrent programs. In: Proceedings of ACM SIGSOFT International Symposium on Foundations of Software Engineering. 2008, 135–145 https://doi.org/10.1145/1453101.1453121
27
S Park, S Lu, Y Zhou. 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 https://doi.org/10.1145/1508284.1508249
28
S Park, R W Vuduc, M J Harrold. Falcon: fault localization in concurrent programs. In: Proceedings of ACM/IEEE International Conference on Software Engineering. 2010, 245–254 https://doi.org/10.1145/1806799.1806838
29
S Biswas, J Huang, A Sengupta, M D Bond. DoubleChecker: efficient sound and precise atomicity checking. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2014, 28–39 https://doi.org/10.1145/2666356.2594323
30
C Flanagan, S N Freund. Atomizer: a dynamic atomicity checker for multithreaded programs. In: Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2004, 256–267 https://doi.org/10.1145/982962.964023
31
S Lu, S Park, C Hu, X Ma, W Jiang, Z Li, R A Popa, Y Zhou. 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 https://doi.org/10.1145/1323293.1294272
32
K Havelund. Using runtime analysis to guide model checking of java programs. In: Proceedings of International SPINWorkshop onModel Checking of Software. 2000, 245–264 https://doi.org/10.1007/10722468_15
33
Y Cai, S Wu, W K Chan. ConLock: a constraint-based approach to dynamic checking on deadlocks in multithreaded programs. In: Proceedings of International Conference on Software Engineering. 2014, 491–502 https://doi.org/10.1145/2568225.2568312
34
M Eslamimehr, J Palsberg. Sherlock: scalable deadlock detection for concurrent programs. In: Proceedings of ACM SIGSOFT International Symposium on Foundations of Software Engineering. 2014, 353–365 https://doi.org/10.1145/2635868.2635918
35
K Sen. Effective random testing of concurrent programs. In: Proceedings of IEEE/ACM International Conference on Automated Software Engineering. 2007, 323–332 https://doi.org/10.1145/1321631.1321679
36
F A Bianchi, A Margara, M Pezzè. A survey of recent trends in testing concurrent software systems. IEEE Transactions on Software Engineering, 2018, 44(8): 747–783 https://doi.org/10.1109/TSE.2017.2707089
37
P Thomson, A F Donaldson, A Betts. Concurrency testing using schedule bounding: an empirical study. In: Proceedings of ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. 2014, 15–28 https://doi.org/10.1145/2692916.2555260
38
A Desai, S Qadeer, S A Seshia. Systematic testing of asynchronous reactive systems. In: Proceedings of Joint Meeting on Foundations of Software Engineering. 2015, 73–83 https://doi.org/10.1145/2786805.2786861
39
H Fu, Z Wang, X Chen, X Fan. A systematic survey on automated concurrency bug detection, exposing, avoidance, and fixing techniques. Software Quality Journal, 2018, 26(3): 855–889 https://doi.org/10.1007/s11219-017-9385-3
40
V Arora, R Bhatia, M Singh. A systematic review of approaches for testing concurrent programs. Concurrency and Computation: Practice and Experience, 2016, 28(5): 1572–1611 https://doi.org/10.1002/cpe.3711
41
S R S Souza, M A S Brito, R A Silva, P S L Souza, E Zaluska. Research in concurrent software testing: a systematic review. In: Proceedings of Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging. 2011, 1–5 https://doi.org/10.1145/2002962.2002964
42
P Sewell, S Sarkar, S Owens, F Z Nardelli, M O Myreen. X86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Communications of the ACM, 2010, 53(7): 89–97 https://doi.org/10.1145/1785414.1785443
43
J Manson, W Pugh, S V Adve. The java memory model. In: Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2005, 378–391 https://doi.org/10.1145/1047659.1040336
44
P Godefroid. Model checking for programming languages using veriSoft. In: Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 1997, 174–186 https://doi.org/10.1145/263699.263717
45
M Musuvathi, S Qadeer. Iterative context bounding for systematic testing of multithreaded programs. ACM SIGPLAN Notices, 2007, 42(6): 446–455 https://doi.org/10.1145/1273442.1250785
S Burckhardt, P Kothari, M Musuvathi, S Nagarakatte. 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 https://doi.org/10.1145/1735970.1736040
A Andoni, D Daniliuc, S Khurshid. Evaluating the “Small Scope Hypothesis”. 2003
50
S Lu, S Park, E Seo, Y Zhou. 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 https://doi.org/10.1145/1353535.1346323
51
S Qadeer, J Rehof. 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 https://doi.org/10.1007/978-3-540-31980-1_7
52
S Nagarakatte, S Burckhardt, M M Martin, M Musuvathi. 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 https://doi.org/10.1145/2345156.2254128
53
A Nistor, Q Luo, M Pradel, T R Gross, D Marinov. BALLERINA: automatic generation and clustering of efficient random unit tests for multithreaded code. In: Proceedings of International Conference on Software Engineering. 2012, 727–737 https://doi.org/10.1109/ICSE.2012.6227145
54
G Li, S Lu, M Musuvathi, S Nath, R Padhye. Efficient scalable threadsafety- violation detection: finding thousands of concurrency bugs during testing. In: Proceedings of ACM Symposium on Operating Systems Principles. 2019, 162–180 https://doi.org/10.1145/3341301.3359638
55
K Sen. Race directed random testing of concurrent programs. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2008, 11–21 https://doi.org/10.1145/1379022.1375584
56
P Joshi, C S Park, K Sen, M Naik. 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 https://doi.org/10.1145/1543135.1542489
57
X Yuan, J Yang, R Gu. Partial order aware concurrency sampling. In: Proceedings of International Conference on Computer Aided Verification. 2018, 317–335 https://doi.org/10.1007/978-3-319-96142-2_20
58
R H Arpaci-Dusseau, A C Arpaci-Dusseau. Operating Systems: Three Easy Pieces. Arpaci-Dusseau Books, LLC, 2018
59
R I Davis, L Cucu-Grosjean, M Bertogna, A Burns. A review of priority assignment in real-time systems. Journal of Systems Architecture, 2016, 65: 64–82 https://doi.org/10.1016/j.sysarc.2016.04.002
60
D Chen, Y Jiang, C Xu, X Ma, J Lu. 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 https://doi.org/10.1145/3236024.3236077
61
M Musuvathi, S Qadeer, T Ball, G Basler, P A Nainar, I Neamtiu. Finding and reproducing heisenbugs in concurrent programs. In: Proceedings of USENIX Conference on Operating Systems Design and Implementation. 2008, 267–280
62
P Godefroid. Partial-order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Heidelberg: Springer, 1996 https://doi.org/10.1007/3-540-60761-7
63
C Flanagan, P Godefroid. Dynamic partial-order reduction for model checking software. In: Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2005, 110–121 https://doi.org/10.1145/1047659.1040315
64
Y Yang, X Chen, G Gopalakrishnan. Inspect: a runtime model checker for multithreaded C programs. Technical Report, 2008
65
M Kokologiannakis, A Raad, V Vafeiadis. Effective lock handling in stateless model checking. Proceedings of the ACM on Programming Languages. 2019, 3(OOPSLA): 1–26 https://doi.org/10.1145/3360599
66
S Lu, W Jiang, Y Zhou. 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 https://doi.org/10.1145/1295014.1295034
67
A Bron, E Farchi, Y Magid, Y Nir, S Ur. Applications of synchronization coverage. In: Proceedings of ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. 2005, 206–212 https://doi.org/10.1145/1065944.1065972
68
S Hong, J Ahn, S Park, M Kim, M J Harrold. Testing concurrent programs to achieve high synchronization coverage. In: Proceedings of International Symposium on Software Testing and Analysis. 2012, 210–220 https://doi.org/10.1145/2338965.2336779
69
J Yu, S Narayanasamy. A case for an interleaving constrained sharedmemory multi-processor. In: Proceedings of Annual International Symposium on Computer Architecture. 2009, 325–336 https://doi.org/10.1145/1555815.1555796
70
C Wang, M Said, A Gupta. Coverage guided systematic concurrency testing. In: Proceedings of International Conference on Software Engineering. 2011, 221–230 https://doi.org/10.1145/1985793.1985824
71
J Burnim, T Elmas, G Necula, K Sen. CONCURRIT: testing concurrent programs with programmable state-space exploration. In: Proceedings of the 4th USENIX Workshop on Hot Topics in Parallelism. 2012
72
J Huang, P O Meredith, G Rosu. Maximal sound predictive race detection with control flow abstraction. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2014, 337–348 https://doi.org/10.1145/2666356.2594315
73
S Huang, J Huang. 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 https://doi.org/10.1145/3022671.2984025
74
J Huang, Q Luo, G Rosu. GPredict: generic predictive concurrency analysis. In: Proceedings of International Conference on Software Engineering. 2015, 847–857 https://doi.org/10.1109/ICSE.2015.96
75
M Eslamimehr, J Palsberg. Race directed scheduling of concurrent programs. In: Proceedings of ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. 2014, 301–314 https://doi.org/10.1145/2692916.2555263
76
P Godefroid, N Klarlund, K Sen. DART: directed automated random testing. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2005, 213–223 https://doi.org/10.1145/1064978.1065036
77
K Sen. Concolic testing. In: Proceedings of IEEE/ACM International Conference on Automated Software Engineering. 2007, 571–572 https://doi.org/10.1145/1321631.1321746
78
F Sorrentino, A Farzan, P Madhusudan. PENELOPE: weaving threads to expose atomicity violations. In: Proceedings of ACM SIGSOFT International Symposium on Foundations of Software Engineering. 2010, 37–46 https://doi.org/10.1145/1882291.1882300
79
G Lu, L Xu, Y Yang, B Xu. Predictive analysis for race detection in software-defined networ. Sciece China Information Sciences, 2019, 62(6): 62101 https://doi.org/10.1007/s11432-018-9826-x
80
L De Moura, N Bjørner. Z3: an efficient SMT solver. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2008, 337–340 https://doi.org/10.1007/978-3-540-78800-3_24
81
P Joshi, M Naik, K Sen, D Gay. An effective dynamic analysis for detecting generalized deadlocks. In: Proceedings of ACM SIGSOFT International Symposium on Foundations of Software Engineering. 2010, 327–336 https://doi.org/10.1145/1882291.1882339
82
M Musuvathi, S Qadeer. Fair stateless model checking. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. 2008, 362–371 https://doi.org/10.1145/1379022.1375625
83
M Batty, S Owens, S Sarkar, P Sewell, T Weber. Mathematizing C++ concurrency. In: Proceedings of Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2011, 55–66 https://doi.org/10.1145/1925844.1926394
84
B Norris, B Demsky. CDSchecker: checking concurrent data structures written with C/C++ atomics. ACM SIGPLAN Notices, 2013, 48(10): 131–150 https://doi.org/10.1145/2544173.2509514
85
B Kasikci, W Cui, X Ge, B Niu. Lazy diagnosis of in-production concurrency bugs. In: Proceedings of the 26th Symposium on Operating Systems Principles. 2017, 582–598 https://doi.org/10.1145/3132747.3132767
86
S Guo, M Kusano, C Wang, Z Yang, A Gupta. Assertion guided symbolic execution of multithreaded programs. In: Proceedings of Joint Meeting on Foundations of Software Engineering. 2015, 854–865 https://doi.org/10.1145/2786805.2786841
87
T Bergan, D Grossman, L Ceze. 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 https://doi.org/10.1145/2714064.2660200
88
S Guo, M Kusano, C Wang. Conc-ISE: incremental symbolic execution of concurrent software. In: Proceedings of IEEE/ACMInternational Conference on Automated Software Engineering. 2016, 531–542 https://doi.org/10.1145/2970276.2970332
89
A Farzan, A Holzer, N Razavi, H Veith. Con2colic testing. In: Proceedings of Joint Meeting on Foundations of Software Engineering. 2013, 37–47 https://doi.org/10.1145/2491411.2491453
