基于Petri網(wǎng)的多線程死鎖檢測研究.pdf

1、隨著多核處理器的發(fā)展和多線程程序的普及，多線程技術(shù)的應(yīng)用越來越廣泛。但是在多線程程序中，當(dāng)多個線程之間運(yùn)行推進(jìn)順序不合適時，就可能造成死鎖。死鎖會導(dǎo)致多線程程序無法運(yùn)行，甚至軟件系統(tǒng)崩潰。因此如何有效地檢測多線程程序死鎖是軟件測試和開發(fā)領(lǐng)域的重要研究課題之一。目前主流的靜態(tài)死鎖檢測方法主要包括基于并發(fā)模型分析和基于數(shù)據(jù)流分析。基于數(shù)據(jù)流分析的死鎖檢測結(jié)果因為保守分析容易造成誤判，基于并發(fā)模型分析不能很好地支持多線程程序建模，并且大部分研

2、究主要針對Java程序的死鎖檢測，對使用Posix線程庫開發(fā)的C多線程程序研究不多。
　　針對這些問題，本文基于Posix線程庫開發(fā)的C多線程程序，在調(diào)研現(xiàn)有死鎖檢測技術(shù)的基礎(chǔ)上，結(jié)合程序靜態(tài)分析技術(shù)提出一種基于Petri網(wǎng)模型的多線程死鎖檢測方法，該方法適用于兩個或者多個線程的死鎖檢測。論文的主要工作如下:
　　1)對多線程程序進(jìn)行指針別名分析。在Linux平臺上使用GCC編譯器對程序預(yù)處理，得到控制流圖CFG、SSA形式

3、的中間代碼和函數(shù)依賴關(guān)系。然后基于SSA形式的中間代碼進(jìn)行指針別名分析，得到鎖、函數(shù)指針的可能值和所有線程的函數(shù)調(diào)用圖。
　　2)描述多線程程序轉(zhuǎn)換為Petri網(wǎng)模型的方法。在得到函數(shù)調(diào)用圖的基礎(chǔ)上對函數(shù)調(diào)用圖進(jìn)行優(yōu)化，目的是減少程序Petri網(wǎng)的規(guī)模。優(yōu)化過程包括刪除與鎖操作無關(guān)的函數(shù)、函數(shù)內(nèi)的優(yōu)化和使用lockset技術(shù)分析鎖相關(guān)函數(shù)等。然后對鎖操作函數(shù)和優(yōu)化后的函數(shù)調(diào)用圖進(jìn)行Petri網(wǎng)建模，這樣得到一個與源程序并發(fā)語義等價

4、的Petri網(wǎng)模型。
　　3)設(shè)計一種基于Petri網(wǎng)的死鎖檢測算法。首先根據(jù)多線程程序中鎖的使用特點(diǎn)，定義一個用來描述互斥鎖、自旋鎖和讀寫鎖操作的特殊Petri網(wǎng)。然后分析這個特殊Petri網(wǎng)的動態(tài)性質(zhì)，并提出基于混合整數(shù)規(guī)劃的死鎖檢測算法，通過求解該算法來檢測程序是否存在死鎖。最后從理論上證明算法是否有解與多線程程序是否死鎖之間的等價關(guān)系。
　　4)基于上述方法的實現(xiàn)，本文對Apache、OpenLDAP、FastDFS