|
|
On interleaving space exploration of multi-threaded programs |
Dongjie CHEN1,2, Yanyan JIANG1,2( ), Chang XU1,2( ), Xiaoxing MA1,2 |
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 |
|
|
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
|
Corresponding Author(s):
Yanyan JIANG,Chang XU
|
Just Accepted Date: 27 April 2020
Issue Date: 11 March 2021
|
|
1 |
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
|
8 |
R O’Callahan, J D Choi. Hybrid dynamic data race detection. ACM SIGPLAN Notices, 2003, 38(10): 167–178
https://doi.org/10.1145/966049.781528
|
9 |
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
|
46 |
M Emmi, S Qadeer, Z Rakamarić. Delay-bounded scheduling. ACMSIGPLAN Notices, 2011, 46(1): 411–422
https://doi.org/10.1145/1925844.1926432
|
47 |
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
|
48 |
P Godefroid, K Sen. Combining Model Checking and Testing. In: Handbook of Model Checking. Springer, Cham, 2018, 613–649
https://doi.org/10.1007/978-3-319-10575-8_19
|
49 |
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
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
|
Shared |
|
|
|
|
|
Discussed |
|
|
|
|