本篇論文提出了一個實際並且有效率的區域符號測試和除錯的方法，用來給設計者保證一定的測試覆蓋率並且避免狀態爆炸問題。這篇研究主要的動機是來自於執行平行程式可以善用現今流行的多核心系統的運算能力，進而達到高性能和高產率。然而，平行程式最為人知的就是設計相當耗時和容易出錯的，主要是因為程式經常容易出現相當挑戰性的同步錯誤。傳統的測試方法不是嘗試不實際的列舉所有可能性而遇到狀態爆炸問題就是採取探索的方式只測試程式部分的狀態而只能得到有限的覆蓋率。為了要開發更為實際的解決方法，我們讓設計者自行選擇有問題的互動區域測試取代整份程式的測試，並且運用符號執行的技術來評估所有可能的執行結果。因為區域的大小正常都遠小於整份程式，所以我們的方法比過去更為有效率和實際。除此之外，我們將測試做在中介表示層而使得每次的測試程序可以涵蓋許多目標機器。這個方法已經實作出來並且測試了多個現實世界的例子，在每個例子中我們都能在可以被忽略的動態時間中準確地抓出錯誤。

We present in this thesis a practical and effective region-based symbolic testing and debugging method that guarantees desired coverage for designers while avoiding state explosion problem. This work is motivated by the growing demand of running parallel programs on the increasingly prevalent multi-core systems for higher performance and productivity. However, parallel programming is known to be error-prone and time-consuming as it often induces challenging concurrency bugs. Traditional testing approaches either are infeasible for trying to enumerate all possibilities and encountering state explosion issue or are heuristics that have only limited testing coverage as they explore only partial state space. To develop a practical solution, we have designers specify suspicious interacting regions, instead of blindly testing the whole program, and apply a symbolic execution technique to evaluate results of all execution possibility. Since the region size is normally much smaller than the whole program, our approach is much more efficient and effective in practice. Additionally, we conduct the testing in IR level and hence each testing process effectively covers many target machines. The approach has been implemented and tested on several real world examples and in each case the bug is precisely identified in negligible runtime.

[1]HENNESSY, John L.; PATTERSON, David A. Computer architecture: a quantitative approach. Elsevier, 2012.
[2]GODEFROID, Patrice. Model checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 1997. p. 174-186.
[3]GODEFROID, Patrice, et al. Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. Heidelberg: Springer, 1996.
[4]FLANAGAN, Cormac; GODEFROID, Patrice. Dynamic partial-order reduction for model checking software. In: ACM Sigplan Notices. ACM, 2005. p. 110-121.
[5]CLARKE, Edmund M., et al. Symmetry reductions in model checking. In: Computer Aided Verification. Springer Berlin Heidelberg, 1998. p. 147-158.
[6]MUSUVATHI, Madanlal; QADEER, Shaz. Iterative context bounding for systematic testing of multithreaded programs. In: ACM SIGPLAN Notices. ACM, 2007. p. 446-455.
[7]LU, Shan, et al. Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. ACM SIGARCH Computer Architecture News, 2008, 36.1: 329-339.
[8]KING, James C. Symbolic execution and program testing. Communications of the ACM, 1976, 19.7: 385-394.
[9]SIVARAJ, Hemanthkumar; GOPALAKRISHNAN, Ganesh. Random walk based heuristic algorithms for distributed memory model checking. Electronic Notes in Theoretical Computer Science, 2003, 89.1: 51-67.
[10]CARR, Steve; MAYO, Jean; SHENE, Ching-Kuang. Race conditions: a case study. Journal of Computing Sciences in Colleges, 2001, 17.1: 90-105.
[11]ZHANG, Wei, et al. ConSeq: detecting concurrency bugs through sequential errors. In: ACM SIGPLAN Notices. ACM, 2011. p. 251-264.
[12]RUSSELL, Stuart Jonathan, et al. Artificial intelligence: a modern approach. Englewood Cliffs: Prentice hall, 1995.
[13]DOWNEY, Allen B. The little book of semaphores. Green Tea Press, 2005.
[14]LUCIA, Brandon; WOOD, Benjamin P.; CEZE, Luis. Isolating and understanding concurrency errors using reconstructed execution fragments. ACM SIGPLAN Notices, 2011, 46.6: 378-388.
[15]LUCIA, Brandon; CEZE, Luis. Finding concurrency bugs with context-aware communication graphs. In: Microarchitecture, 2009. MICRO-42. 42nd Annual IEEE/ACM International Symposium on. IEEE, 2009. p. 553-563.
[16]MUSUVATHI, Madanlal, et al. Finding and reproducing heisenbugs in concurrent programs. In: Proceedings of the 8th USENIX conference on Operating systems design and implementation. USENIX Association, 2008. p. 267-280.
[17]BRON, Arkady, et al. Applications of synchronization coverage. In: Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming. ACM, 2005. p. 206-212.
[18]NOVILLO, Diego. Tree SSA A New Optimization Infrastructure for GCC. In: Proceedings of the 2003 GCC Developers’ Summit. 2003. p. 181-193.
[19]SEN, Koushik; MARINOV, Darko; AGHA, Gul. CUTE: a concolic unit testing engine for C. ACM, 2005.