基於使用信號機及共享記憶體的並行軟體測試

Abstract

並行程式在現代的計算中已經變得非常地普遍。然而，因為並行程式的非確定性行為，在並行程式中的錯誤通常都很難被偵測到。在電腦科學中信號機是其中一個主要的同步機制，在多元程式規劃中，它通常被用來控制共享資料的存取。對信號機的誤用是一個非常嚴重的問題，因為這可能導致程式發生死結或是造成一些對共享資料的違規存取。 在這篇論文中，我們會描述如何將動態敏捷測試應用到測試使用信號機的並行程式。我們提出了一些可以對信號機的運算做前綴重播(prefix-based replay)和當死結發生時能夠記錄下程式狀態的協定。我們也針對使用信號機的程式定義了新的同步序列格式。然後，我們提出了一個演算法用來過濾掉被競爭分析(race analyzer)產生的不可行的競爭變異(race variant)。最後，我們發展了一個壓縮的功能來解決被重複的事件所引起的狀態空間爆炸(state space explosion)問題。如此一來，我們可以成功地針對使用信號機和共享記憶體的並行程式做狀態全覆(state-cover)的動態測試，並且可以產生使用信號機以及共享記憶體的並行程式的所有狀態以及所有在程式中的死結。Concurrent program is becoming commonplace in modern computing. However, the bugs in concurrent program are usually difficult to be detected because of the non-deterministic behavior of concurrent programs. Semaphore is one of the major synchronization mechanisms in computer science. It often used to control the access of shared data in a multiprogramming environment. The misuse of semaphore is a very serious problem, because this may cause the program deadlock or make some inappropriate access of shared data. In this thesis, we describe how to apply dynamic effective testing to semaphore-based concurrent programs. We propose some protocols that can perform prefix-based replay on semaphore operations and record the program status when the deadlock happened. We also define a novel format for the SYN-sequence of semaphore-based program. Then, we have an algorithm to filter out the infeasible race variants generated by race analyzer in reachability testing. Last, we develop a compression function to deal with the state space explosion problem induced by the reiterative events. Thus, we can successfully perform state-cover testing for semaphore-based and shared memory concurrent programs and find out all the states of the concurrent programs which contain shared semaphores and shared memories and all the deadlocks in the programs.