程序中死鎖檢測的方法和工具

翟宇鵬，程雪梅

（四川大學計算機學院，成都610065）

程序中死鎖檢測的方法和工具

翟宇鵬，程雪梅

（四川大學計算機學院，成都610065）

死鎖一直都是并發系統中最重要的問題之一，對死鎖檢測的研究一直都在不斷地進行著。模型檢測方法是一種重要的自動驗證技術，越來越多地被用在驗證軟硬件設計是否規范的工作中。針對死鎖檢測的問題進行綜述，統計已有的死鎖檢測方法的文獻資料并給出統計結果。然后對搜集出來的文獻進行分析，介紹許多動態以及靜態的死鎖檢測方法。最后介紹兩種常用的模型檢測工具，提出使用模型檢測工具進行死鎖檢測的思路與方法，并證實這種方法的可行性。

死鎖檢測；模型檢測；文獻計量分析

0 引言

隨著計算機行業的不斷發展，軟件規模和復雜度也在不斷擴大，軟件故障已成為計算機系統出錯和崩潰的主要因素。死鎖[1]是分布式系統以及集成式系統中的最重要的問題之一，也是影響軟件安全的主要因素。死鎖會導致程序無法正常運行或終止，甚至導致系統崩潰，帶來不必要的損失。同時，死鎖的運行狀態空間過大，難于重現和修正等問題使其成為軟件領域的難題之一，因此，如何有效地檢測死鎖,提高軟件的可靠性和安全性，成為急需解決的問題。

本文針對10年內國內外各知名數據庫中與死鎖檢測以及模型檢測相關的論文進行查詢、篩選、分類、比較、整理等，然后對整理好的論文進行總結，分析出死鎖檢測的方法并進行羅列比較，以及模型檢測的工具以及方法，從而再將二者結合，找出模型檢測工具在死鎖檢測里的應用。

1 文獻計量分析

對搜索出來的412篇論文的不同方向進行了計量分析，并對統計的數據進行了描述，以及通過計量分析來找出這方面研究領域的熱點。。

因為近10年的論文更能體現出研究的正確方向，所以對于論文時間進行分析，得知最近10年每年論文發表量隨著時間在平緩地增多，可知對于這方面問題的研究總體保持在增長的狀態。

對作者進行統計，分析得知高產的作者只占少數，只有少數的作者對這方面領域的研究比較深入，提出的觀點也具有指導的意義。

對論文的引文類型的進行分析，得知絕大多數來自會議論文或者期刊論文。這也屬于一般的論文來源規律，指導研究者應該在什么地方查閱文獻或者將文獻發布在什么地方。

對論文中關鍵詞進行了統計，其中系統恢復最多出現，因為死鎖是系統中常出現的一類漏洞，系統恢復的過程也就包含了對死鎖進行檢測并處理的過程。關鍵詞中常出現的也包括算法一詞，這也表示對于死鎖的檢測，很多人都提出了相應的算法。除了算法，另一個常出現的詞則是分布式，這也是因為在分布式系統中死鎖檢測越來越多，也越來越被研究者們關注。

圖1 Refviz分析結果（matrix圖）

通過使用Refviz工具，對關鍵詞共現頻率進行了分析，如圖1，發現distribute，deadlocks，algorithm共現的頻率最高，這也表面死鎖檢測方面的研究熱點主要為分布式系統中死鎖檢測的算法一塊。另外，model與deadlock也有著較高的共現頻率，表明有作者也在提出將模型應用在死鎖檢測中，為文章后面提出的使用模型檢測方法進行死鎖檢測提供了一些理論的依據。

2 死鎖檢測方法

針對死鎖產生的必要條件，以及不同系統不同程序中的死鎖，許多學者都提出了新的進行死鎖檢測的方法，或是對常用方法的改良補充。這篇文章收集了許多不同的死鎖檢測方法，并簡單的將它們分為2類，即靜態方法與動態方法。這一章節對其中的一些方法進行了闡述，并做了簡單的分類比較。

2.1 靜態死鎖檢測方法

（1）SystemC中的靜態死鎖檢測分析方法

SystemC是一種基于C++語言的用于系統設計的計算機語言。Mikhail Moiseev對此提出了一個基于對靜態代碼的分析的方法來解決死鎖的檢測問題[2]。

此方法運用了正式的程序模型，為了對算法進行有效的分析，由原理可知唯一的死鎖狀態是在一個事件中無窮的wait都不會被notify。死鎖會導致所有程序執行的阻塞或者某一部分程序執行的阻塞，針對這兩種情況需要不同的死鎖檢測規則。

（2）SHIM并發語言中的靜態死鎖檢測算法

隨著多核處理器的出現，并發程序也就自然而然的出現，在并發程序中，兩個最被關注的方面就是數據爭用（data race）以及死鎖。對于SHIM語言，它通過避免共享內存從而避免了數據爭用的出現，但是卻不能避免死鎖。

Nalini Vasudevan針對這一問題提出了一個基于模型檢測的死鎖檢測技術，在這個方法中，建立了SHIM程序的異步抽象模型，并用NuSMV符號模型檢測器來檢測模型中是否存在死鎖，這個方法能在系統運行前找到系統中存在的潛在的死鎖。

2.2 動態死鎖檢測

（1）分布式系統中的死鎖檢測算法

死鎖檢測是分布式系統中最重要的問題之一，Mehdi Hashemzadeh以及他的團隊基于此提出了一個分布式的死鎖檢測算法[3]：該算法通過探針進行標記，對每個節點進行進行檢測，通過層層條件來找出死鎖。該算法能通過死鎖中包含的節點來管理算法同時運行于幾處，可以防止對同一處死鎖進行多次檢測，可以通過對進程進行優先級劃分來來最小化算法同時運行于幾處時產生的無用的信息。同時這個算法通過其獨特的特性，能在死鎖被檢測出來的同時進行解決。

除了Mehdi Hashemzadeh提出的算法，對于分布式系統中的死鎖檢測問題，還有幾位其他作者也提出了不同的方法。

（2）并發的消息傳遞程序中的死鎖檢測算法

針對于并發消息傳遞程序中的死鎖問題，Sagar Chaki以及他的團隊提出了一種算法，并且此算法采用了包括抽象型以及組合型的論證的框架，有效的解決了因死鎖引起的狀態空間爆炸的問題[4]。此算法使用了抽象、驗證、精確的三步迭代過程來檢測系統中是否存在死鎖。Chaki指出此算法在將來還能用假設-證明式（assume-guarantee style）的推論來進行提升，同時他的團隊也將在未來做這方面的研究。

（3）Java多線程程序中的死鎖檢測方法

Java語言由于其被用戶越來越廣泛的使用，它里面的死鎖檢測也就變得重要。

Takao Shimomura[5]提出了對Java多線程程序中的死鎖的檢測方法，提出了3種死鎖的狀態：鎖阻塞（lock-blocked）、等待阻塞（wait-blocked）、加入阻塞（join-blocked），在這3個死鎖狀態的基礎上將死鎖分為了2種類型：環型以及非環型。Takao還對他提出的3種死鎖狀態進行了實驗，較好地檢測出了他提出的死鎖。

對于Java中的死鎖檢測問題，Yan Wen[6]也提出了名為JDeadlockDetector的新的Java線程死鎖檢測的方法。

（4）過程網絡（Process Network）中的死鎖檢測算法

過程網絡模型用于為并行程序設計設計語言，因為其支持無限通道的能力而成為了基于流的多媒體應用以及信號處理應用的理想模型[7]，然而在實現它的過程中卻出現了死鎖的問題。Mar'ia Castillo在論文中介紹了一種復雜度為O（n）的算法去解決死鎖，為了減少信息的數量，該算法從系統轉變成死鎖狀態的過程中提取信息，并能保證檢測出死鎖所在的節點。

（5）運用幾何學進行死鎖檢測

David A.Cape[8]提出了一種運用包含拓撲概念的幾何學知識將狀態空間分成幾個部分，并通過對狀態空間的減少進行研究，從而對死鎖問題進行解決。以前對狀態空間都是進行歸納性的劃分，而他則展示了一種由遞歸方法促進的分解方法，這種方法能有效的減少狀態轉換的規模，從而能整體提升驗證的運行效率。

3 基于模型檢測工具的死鎖檢測方法

模型檢測是一種很重要的自動驗證技術，一般應用于驗證系統設計是否滿足設計規范。模型檢測方法最早由Allen Emerson[9]等人分別獨立提出，其基本思想是先建立待驗證系統的有限狀態模型，然后使用算法對模型中的所有可能執行組合狀態進行窮盡搜索，通過利用驗證表達式判斷這些組合路徑是否符合設計規范，如果某條執行路徑不滿足設計規范，模型檢測工具會給出不滿足該設計規范的執行路徑[10]。雖然模型檢測在現階段起著越來越重要的作用，但它也有著它的弊端，當系統或者軟件的模塊很多時，所能產生的狀態組合也會以指數倍數增長，導致檢測的難度會大大的增加。

模型檢測是一種很重要的自動驗證技術，而死鎖檢測是一種在如今的軟件系統中很重要的問題，本章節將討論到將這二者結合起來，使用模型檢測的工具來對死鎖進行檢測，從中發現對死鎖這一問題的另一種方面的解決辦法。

3.1 模型檢測工具介紹

模型檢測有許許多多的方法與工具，而這其中最被人們熟知的工具之一是NuSMV[11]。它是一款模型檢測工具，它在SMV（Symbolic Model Checker）工具的基礎上進行改進后產生，具有了一般的模型檢測工具有的所有功能，功能較SMV更為強大。NuSMV是由多個模塊構建組成，模塊與模塊之間相互獨立，它們通過模塊的內部接口來進行通信。同時NuSMV是一個開源的工具，它允許使用者對其進行擴展修改，這就使得NuSMV被廣泛的應用在了許多研究的領域。NuSMV高效的實現了符號模型檢測技術[12]，它是第一款基于CUDD包中的[13]BBDs（Binary Decision Diagrams）操作的模型檢測工具。NuSMV在模型檢測中是一個比較經典的工具，對符號化模型檢測算法進行了優化，達到了高效驗證的目標，并且NuSMV的軟件體系結構設計的比較靈活，容易對功能進行擴展。

NuSMV的前身是SMV，它對后者在不同程度上進行了優化，包括功能的擴展、系統架構的優化以及易用性的優化。

3.2 模型檢測工具在死鎖檢測中的應用

這一節提出了一種模型檢測工具在死鎖檢測中的應用方法，此方法主要用在系統設計階段對設計方案進行死鎖檢測，并選擇NuSMV來進行操作。

因為死鎖的發生具有偶發性，在系統運行時某一些執行路徑在特定條件下才會出現，這樣模型檢測可以對所有可能的執行路徑進行模擬運行，將模型檢測應用到死鎖檢測，對并發系統進程之間資源使用進行執行路徑搜索，設計合理的時序邏輯表達式，可以達到死鎖檢測的目的。由于并發系統在調用資源時，調用的進程順序具有不確定性，而狀態組合又是有限狀態，因此可以對系統進行建模，通過NuSMV工具驗證時序邏輯表達式的正確性來判斷是否發生死鎖。

針對并發同步和異步以及這兩種模式下的信號量、互斥鎖、條件變量機制設計出了8個基于NuSMV的死鎖檢測模型驗證模板，通過對被測系統的設計文檔分析獲得并發進程對臨界區的訪問信息，使用算法自動對這些信息判斷處理并創建用于驗證是否發生死鎖的時序邏輯表達式，然后根據獲得的信息選擇相應模板轉換為NuSMV可以運行的SMV程序，之后利用NuSMV對時序邏輯表達式進行驗證，通過時序邏輯表達式真值判斷是否產生死鎖，并給出真值為假的執行路徑，該路徑就是產生死鎖時的進程執行路徑。最終通過基于NuSMV死鎖檢測模型驗證模板和算法實現并發同步和異步以及這兩種模式下的信號量、互斥鎖、條件變量機制的死鎖檢測。

4 結語

本文對死鎖檢測的問題以及模型檢測方法進行了綜述，羅列出了現有的比較常見比較被人們熟知的方法，并對它們的特性等進行了描述。文章能夠給未來進行這方面研究的研究人員帶來幫助，讓他們能夠減少自己重新查閱這方面文獻資料并搜集需要信息的工作，將重點放在進行新的死鎖檢測方法的研究以及對已有方法進行完善的工作上面。同時這篇文章也提出了一種新的進行死鎖檢測的思路，這一思路也得到了實驗結果的支持，表明這個方法確實是有效的，但卻還需要更進一步的深入實驗。

死鎖是很難避免發生的缺陷，隨著科技的發展，越來越多新穎卻讓人眼前一亮的方法出現，這些方法或者從整體提升了整個死鎖檢測的效率，或者對某一方面的死鎖檢測進行了很好的優化。雖然死鎖不會因為這些方法得到徹底的解決，但這些不同研究者的不同的思路卻讓人相信死鎖的問題會得到很好的處理。

[1]A.O.Abd El-Gwad,A.I.Saleh,M.M.Abd-ElRazik.A Novel Scheduling Strategy for an Efficient Deadlock Detection.In Computer Engineering&Systems,2009.ICCES 2009.International Conference on,2009,pp.579-583.

[2]M.Moiseev,A.Zakharov,I.Klotchkov,S.Salishev.Static Analysis Method for Deadlock Detection in SystemC Designs.In System on Chip（SoC）,2011 International Symposium on,2011,pp.42-47.

[3]M.Hashemzadeh,N.Farajzadeh,A.T.Haghighat.Optimal Detection and Resolution of Distributed Deadlocks in the Generalized Model.in Parallel,Distributed,and Network-Based Processing,2006.PDP 2006.14th Eurom icro International Conference on,2006, p.4 pp.

[4]S.Chaki,E.Clarke,J.Ouaknine,N.Sharygina.Automated,Compositional and Iterative Deadlock Detection.in Formal Methods and Models for Co-Design,2004.MEMOCODE'04.Proceedings.Second ACM and IEEE International Conference on,2004,pp.201-210.

[5]T.Shimomura，K.Ikeda.Waiting Blocked-Tree Type Deadlock Detection.in Science and Information Conference（SAI）,2013,2013, pp.45-50.

[6]W.Yan,Z.Jinjing,H.Minhuan,C.Hua.Towards Detecting Thread Deadlock in Java Programswith JVM Introspection.in Trust,Security and Privacy in Computing and Communications（TrustCom）,2011 IEEE 10th International Conference on,2011,pp.1600-1607.

[7]M.Castillo,F.Farina,A.Cordoba.Deadlock in Process Networks:A Dynamic Detection and Resolution.in Signal Processing and Communication Systems（ICSPCS）,2011 5th International Conference on,2011,pp.1-9.

[8]D.A.Cape,S.C.Jackson,B.M.McMillin.Dihomotopic Deadlock Detection via Progress Shell Decomposition.in Advances in System Testing and Validation Lifecycle（VALID）,2010 Second International Conference on,2010,pp.20-25.

[9]C.E，E.E.Design and Synthesis of Synchronization Skeletons Using Braching Time Temporal Locic.LNUS 137,pp.337-351,1982.

[10]E.M.Clarke，O.Grumberg.Counterexample Guided Abstraction Refinement for Symbolic Model Checking.Journal of the ACM,vol.50（5）,pp.752-794,2003.

[11]K.L.，McMillall.Symbolic Model Checking.Kluwer Academ ic Publ,1993.

[12]R.Cavada.,A.Cimatti.,C.A.Jochim.,G.Keighren.,E.Olivetti.,M.Pistore.,etal..NuSMV2.5.4-User Mannual,"IRST,2005.

[13]顧濱兵.基于模型檢測的軟件驗證技術研究[D].吉林大學學報,2007.

Methods and Tools of Program Dead lock Detection

ZHAIYu-peng，CHENG Xue-mei

（College of Computer Science,Sichuan University,Chengdu 610065）

Deadlock is always one of themost important problems in concurrent system,and the study of deadlock detection has never been stopped. Model checking is an important technology of automatic verification,is increasingly being used in the verification of software and hardware design of whether the specification.Reviews on the problems aiming at deadlock detection,first reviews the deadlock detection method of statisticalwork,the existing literature and gives the statistical results.Then analyzes the collection of literature,proposes the dynamic as well as static dead lock detection method.Finally,introduces two kinds of common model checking tools,and then describes the use ofmodel checking tool of thoughts andmethods for the detection of deadlocks,and confirms the feasibility of thismethod.

Dead lock Detection;Model Checking;Literature Measurement Analysis

1007-1423（2017）03-0041-04

10.3969/j.issn.1007-1423.2017.03.011

翟宇鵬（1992-），男，江蘇興化人，碩士研究生，研究方向為嵌入式軟件開發與測試

2016-11-22

2017-01-15

四川省應用基礎研究項目（No.2014JY0112）

程雪梅（1991-），女，重慶萬州人，碩士，研究方向為軟件工程與軟件測試