本篇論文提出一個切成小區塊的高效率平行性程式測試方法，以針對易出錯的區塊取代盲目地測試整個程式，並搭配一個簡化迴圈分析的策略，共同有效地避免狀態爆炸問題；緊接著為達最大驗證效率而設計一款優化方案，以期能減少因完整探索指定區塊所需驗證的可能執行路徑數量。此外，由於我們具備便捷地辨別出錯路徑的方法，因此大大地加快了偵錯效率。我們已實作出前述的區塊測試方法並成功地偵測到數個大型應用程式的錯誤案例。實驗結果顯示我們的方法能精確地辨認錯誤發生原因並且較傳統方法而言表現得更有效。

In this paper, we propose an effective concurrency bugs testing approach that focuses on suspicious bug-causing code regions instead of blindly testing the whole program. Additionally, with a simple loop heuristic, the region-based approach effectively avoids state explosion problem and is highly efficient while guarantee to find any existing concurrency bugs in the specified code regions. We also devise an optimization scheme to reduce the number of interleavings to be examined to achieve maximum efficiency. Our method can conveniently identify bug-causing interleavings and hence greatly improve debugging efficiency. We have implemented the proposed approach and successfully tested on a few large application cases. The experimental results show that the approach can precisely identify bug sources and perform much more effectively than traditional approaches.

ABSTRACT 3
Contents 4
List of Figures 5
List of Tables 7
I. INTRODUCTION 8
II. RELATED WORK 13
A. Non-systematic Methods 13
B. Active Methods 14
C. Systematic Methods 15
III. The Region-based Testing Approach 19
A. The Region-based Approach 19
B. Legalize Selected Regions 21
C. Make Regions Executable 27
D. Unroll Loops 27
IV. IMPLEMENTATION 29
A. Symbolic Path Analyzer 29
B. Simplify Interleaving Enumeration 30
C. Interleaving Filter 31
D. Bugs Verifier 32
E. The Workflow of Region-based Approach 33
V. EXPERIMENTAL RESULTS 34
A. Performance Analysis 35
B. Improved Verification Performance 35
VI. CONCLUSION 38
REFERENCES 39

[1] Hennessy, John L., and David A. Patterson. Computer architecture: a quantitative approach. Elsevier, 2011.
[2] Godefroid, Patrice. "Model checking for programming languages using VeriSoft." Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 1997.
[3] Godefroid, Patrice, et al. Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. Vol. 1032. Heidelberg: Springer, 1996.
[4] Flanagan, Cormac, and Patrice Godefroid. "Dynamic partial-order reduction for model checking software." ACM Sigplan Notices. Vol. 40. No. 1. ACM, 2005.
[5] Clarke, Edmund M., et al. "Symmetry reductions in model checking." International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg, 1998.
[6] Musuvathi, Madanlal, and Shaz Qadeer. "Iterative context bounding for systematic testing of multithreaded programs." ACM Sigplan Notices. Vol. 42. No. 6. ACM, 2007.
[7] Lu, Shan, et al. "Learning from mistakes: a comprehensive study on real world concurrency bug characteristics." ACM SIGARCH Computer Architecture News. Vol. 36. No. 1. ACM, 2008.
[8] King, James C. "Symbolic execution and program testing." Communications of the ACM 19.7 (1976): 385-394.
[9] Sivaraj, Hemanthkumar, and Ganesh Gopalakrishnan. "Random walk based heuristic algorithms for distributed memory model checking." Electronic Notes in Theoretical Computer Science89.1 (2003): 51-67.
[10] Carr, Steve, Jean Mayo, and Ching-Kuang Shene. "Race conditions: a case study." Journal of Computing Sciences in Colleges 17.1 (2001): 90-105.
[11] Zhang, Wei, et al. "ConSeq: detecting concurrency bugs through sequential errors." ACM SIGARCH Computer Architecture News. Vol. 39. No. 1. ACM, 2011.
[12] Russell, Stuart J., and Peter Norvig. Artificial intelligence: a modern approach. Malaysia; Pearson Education Limited,, 2016.
[13] Downey, Allen. The little book of semaphores. Green Tea Press, 2008.
[14] Lucia, Brandon, Benjamin P. Wood, and Luis Ceze. "Isolating and understanding concurrency errors using reconstructed execution fragments." ACM Sigplan Notices. Vol. 46. No. 6. ACM, 2011.
[15] Lucia, Brandon, and Luis Ceze. "Finding concurrency bugs with context-aware communication graphs." 2009 42nd Annual IEEE/ACM International Symposium on Microarchitecture (MICRO). IEEE, 2009.
[16] Musuvathi, Madanlal, et al. "Finding and Reproducing Heisenbugs in Concurrent Programs." OSDI. Vol. 8. 2008.
[17] Bron, Arkady, et al. "Applications of synchronization coverage." Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming. ACM, 2005.
[18] Novillo, Diego. "Tree SSA a new optimization infrastructure for GCC." Proceedings of the 2003 gCC developers’ summit. 2003.
[19] Sen, Koushik, Darko Marinov, and Gul Agha. "CUTE: a concolic unit testing engine for C." ACM SIGSOFT Software Engineering Notes. Vol. 30. No. 5. ACM, 2005.
[20] Gu, Rui, et al. "Understanding and Detecting Concurrency Attacks." (2016).
[21] Serebryany, Konstantin, and Timur Iskhodzhanov. "ThreadSanitizer: data race detection in practice." Proceedings of the workshop on binary instrumentation and applications. ACM, 2009.
[22] Liu, Bo, et al. "Pinso: Precise isolation of concurrency bugs via delta triaging." 2014 IEEE International Conference on Software Maintenance and Evolution. IEEE, 2014.
[23] Cadar, Cristian, Daniel Dunbar, and Dawson R. Engler. "KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs." OSDI. Vol. 8. 2008.
[24] Fonseca, Pedro, Rodrigo Rodrigues, and Björn B. Brandenburg. "{SKI}: Exposing Kernel Concurrency Bugs through Systematic Schedule Exploration." 11th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 14). 2014.
[25] Yu, Jie, et al. "Maple: a coverage-driven testing tool for multithreaded programs." Acm Sigplan Notices. Vol. 47. No. 10. ACM, 2012.
[26] Zhao, Shixiong, et al. "OWL: Understanding and Detecting Concurrency Attacks." 2018 48th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). IEEE, 2018.
[27] Bianchi, Francesco Adalberto, Alessandro Margara, and Mauro Pezzè. "A survey of recent trends in testing concurrent software systems." IEEE Transactions on Software Engineering 44.8 (2017): 747-783.
[28] Liu, Changming, et al. "A Heuristic Framework to Detect Concurrency Vulnerabilities." Proceedings of the 34th Annual Computer Security Applications Conference. ACM, 2018.
[29] Ramos, David A., and Dawson Engler. "Under-constrained symbolic execution: Correctness checking for real code." 24th {USENIX} Security Symposium ({USENIX} Security 15). 2015.
[30] Deng, Xianghua, and Jooyong Lee. "Bogor/kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems." 21st IEEE/ACM International Conference on Automated Software Engineering (ASE'06). IEEE, 2006.
[31] Norris, Brian, and Brian Demsky. "CDSchecker: checking concurrent data structures written with C/C++ atomics." ACM SIGPLAN Notices 48.10 (2013): 131-150.
[32] Batty, Mark, et al. "Mathematizing C++ concurrency." ACM SIGPLAN Notices. Vol. 46. No. 1. ACM, 2011.
[33] Joshi, Pallavi, et al. "CalFuzzer: An extensible active testing framework for concurrent programs." International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg, 2009.
[34] Abdulla, Parosh Aziz, et al. "Stateless model checking for TSO and PSO." Acta Informatica 54.8 (2017): 789-818.
[35] Khoshnood, Sepideh, Markus Kusano, and Chao Wang. "ConcBugAssist: constraint solving for diagnosis and repair of concurrency bugs." Proceedings of the 2015 international symposium on software testing and analysis. ACM, 2015.
[36] Parlato, Gennaro. "Finding rare concurrent programming bugs:: An automatic, symbolic, randomized, and parallelizable approach." (2018).
[37] Abdulla, Parosh Aziz, et al. "Optimal stateless model checking under the release-acquire semantics." Proceedings of the ACM on Programming Languages 2.OOPSLA (2018): 135.
[38] Hovemeyer, David, and William Pugh. "Finding bugs is easy." Acm sigplan notices 39.12 (2004): 92-106.
[39] Singh, Sanjana, Divyanjali Sharma, and Subodh Sharma. "Dynamic Verification with Observational Equivalence of C/C++ Concurrency." arXiv preprint arXiv:1905.03957 (2019).
[40] https://github.com/david128kim/region_based_project