基于CSP的多線程自動(dòng)建模及死鎖檢測(cè)研究

高飛 武淑紅 王耀力

摘 ?要： 并發(fā)模型分析主要用于業(yè)務(wù)流程邏輯驗(yàn)證，并不能很好支持多線程程序建模。目前大部分研究主要針對(duì)Java程序的死鎖檢測(cè)，對(duì)于使用POSIX線程庫(kù)開(kāi)發(fā)的C語(yǔ)言程序研究并不多。為了檢測(cè)POSIX線程庫(kù)開(kāi)發(fā)的C語(yǔ)言程序是否存在死鎖問(wèn)題，提出一種對(duì)多線程程序進(jìn)行自動(dòng)建模與死鎖檢測(cè)的形式化驗(yàn)證方法。首先，根據(jù)C++CSP框架和源程序之間的聯(lián)系，實(shí)現(xiàn)源程序到C++CSP框架的語(yǔ)義轉(zhuǎn)換;然后，對(duì)C++CSP框架建立通信順序進(jìn)程（CSP）模型，并通過(guò)過(guò)程分析工具（PAT）對(duì)建立的模型進(jìn)行死鎖檢測(cè);最后，通過(guò)實(shí)例驗(yàn)證了本文中自動(dòng)建模與死鎖檢測(cè)方法的可行性與有效性。

關(guān)鍵詞： 多線程建模; 死鎖檢測(cè); 語(yǔ)義轉(zhuǎn)換; 形式化驗(yàn)證; 通信順序進(jìn)程; 過(guò)程分析

中圖分類(lèi)號(hào)： TN911.23?34; TP311.5 ? ? ? ? ? ? 文獻(xiàn)標(biāo)識(shí)碼： A ? ? ? ? ? ? ? ? ?文章編號(hào)： 1004?373X（2019）12?0057?05

Abstract： Concurrency model analysis is mainly used for logic verification of business process， but cannot support multithreaded program modeling well. Since most of current researches are mainly aiming at the deadlock detection of Java programs， researches on C language program developed with the POSIX thread library are still in small amount. Therefore， a formal verification method for automatic modeling and deadlock detection of multithreaded programs is proposed to detect whether there exists the deadlock phenomenon in the C language program developed with the POSIX thread library. The semantic transformation from the source program to the C++CSP framework is realized according to the relationship between the C++CSP framework and source program. The communication sequence process （CSP） model is established for the C++CSP framework. The deadlock detection for the established model is conducted by using the process analysis tool （PAT）. The feasibility and effectiveness of the automatic modeling and deadlock detection method proposed in this paper are verified by examples.

Keywords： multithreaded modeling; deadlock detection; semantic transformation; formal verification; communication sequence process; process analysis

0 ?引 ?言

隨著多核和異構(gòu)多處理器的廣泛應(yīng)用，計(jì)算機(jī)因有硬件的支持而能夠在同一時(shí)間執(zhí)行一個(gè)或多個(gè)線程，進(jìn)而提升了整體處理性能。如今，多線程已經(jīng)應(yīng)用于各類(lèi)復(fù)雜系統(tǒng)[1?2]，然而多線程也導(dǎo)致線程資源競(jìng)爭(zhēng)或線程推進(jìn)順序不合適而產(chǎn)生死鎖的問(wèn)題[3]。Lu S等人針對(duì)MySQL，F(xiàn)ireFox，Apache，OpenOffice這4款開(kāi)源軟件進(jìn)行了統(tǒng)計(jì)，發(fā)現(xiàn)接近30%的并行程序缺陷與死鎖有關(guān)[4]。死鎖造成了系統(tǒng)的不穩(wěn)定，對(duì)于安全性較高的行業(yè)，一旦軟件系統(tǒng)發(fā)生死鎖將會(huì)產(chǎn)生災(zāi)難性的后果。

國(guó)內(nèi)外針對(duì)并發(fā)模型分析大多用于業(yè)務(wù)流程系統(tǒng)，對(duì)于多線程程序形式化驗(yàn)證研究較少。馬莉等人針對(duì)物聯(lián)網(wǎng)系統(tǒng)進(jìn)行了形式化建模與驗(yàn)證[5];李凱寧等人基于模型驅(qū)動(dòng)框架（MDA）實(shí)現(xiàn)了業(yè)務(wù)流程（BPMN）面向?qū)ο蟮慕＃?duì)模型進(jìn)行了死鎖檢測(cè)分析[6];中國(guó)科技大學(xué)的黃理提出了一種基于Petri網(wǎng)的多線程死鎖檢測(cè)方法[7]。

現(xiàn)有方法針對(duì)業(yè)務(wù)流程和多線程死鎖形式化驗(yàn)證主要通過(guò)Petri網(wǎng)進(jìn)行建模，由于Petri網(wǎng)適用于表示過(guò)程關(guān)系，并不能很好地對(duì)數(shù)據(jù)的流向進(jìn)行描述，所以對(duì)于程序中的復(fù)雜過(guò)程并不適合。為了對(duì)源程序建立合適的模型，提高死鎖檢測(cè)精度，本文從肯特大學(xué)Neil BROWN和Peter WELCH等人開(kāi)發(fā)的C++CSP框架受到啟發(fā)[8?9]，使用C++CSP框架語(yǔ)言作為中介，提出一種多線程自動(dòng)建模及死鎖檢測(cè)方法，實(shí)現(xiàn)了多線程程序的形式化驗(yàn)證。多線程程序到CSP建模和檢測(cè)流程如圖1所示。

圖1 ?多線程程序建模和檢測(cè)流程

1 ?多線程程序到C++CSP框架轉(zhuǎn)換

C++CSP作為C++語(yǔ)言的一個(gè)多線程庫(kù)，符合編程語(yǔ)言的邏輯與語(yǔ)義，可以實(shí)現(xiàn)源程序到C++CSP框架的等價(jià)語(yǔ)義轉(zhuǎn)換。同時(shí)，該框架的通信方式是對(duì)CSP通道行為的模擬，為下一步C++CSP轉(zhuǎn)換為CSP模型奠定了基礎(chǔ)。因此，使用C++CSP作為中介可以精確地對(duì)源程序進(jìn)行CSP建模。

下面將針對(duì)圖2分析在POSIX多線程程序中，如何將通信結(jié)構(gòu)轉(zhuǎn)換為具有等效語(yǔ)義的消息傳遞結(jié)構(gòu)。

1.1 ?共享內(nèi)存通道轉(zhuǎn)換

在C語(yǔ)言中，共享內(nèi)存中數(shù)據(jù)的讀/寫(xiě)通過(guò)賦值運(yùn)算“=”，而在C++CSP中，則通過(guò)通道末端實(shí)現(xiàn)對(duì)共享內(nèi)存的讀寫(xiě)。C++CSP中存在兩種通道類(lèi)型：一個(gè)是允許正常寫(xiě)入數(shù)據(jù)的[chanout]通道;另一個(gè)是允許正常讀取數(shù)據(jù)的[chanin]通道。共享變量通道在C++CSP中的聲明如下：

1.2 ?互斥鎖通道轉(zhuǎn)換

對(duì)共享內(nèi)存并發(fā)讀/寫(xiě)時(shí)，互斥鎖保證了非原子操作可以不受干擾的發(fā)生。使用POSIX線程庫(kù)編寫(xiě)C語(yǔ)言程序中，通過(guò)對(duì)互斥量進(jìn)行加鎖和解鎖的操作保證并發(fā)系統(tǒng)發(fā)生。多個(gè)線程可能擁有一個(gè)共同的互斥量，但只存在一個(gè)線程可對(duì)互斥量進(jìn)行加鎖操作，并且只有該線程進(jìn)行互斥量解鎖操作。多線程程序示例如下：

互斥量加鎖和解鎖過(guò)程如圖2所示。在C++CSP中，互斥鎖是通過(guò)互斥鎖通道（[LockChannel]）進(jìn)行模擬的，[LockChannel]由輸入通道和輸出通道兩部分組成。聲明互斥量時(shí)，需要對(duì)互斥量通道初始化，向[Chanin]通道輸入一個(gè)互斥標(biāo)記值表明當(dāng)前為可加鎖狀態(tài)。當(dāng)加鎖時(shí)，從[Chanin]通道中讀出標(biāo)記值，互斥鎖通道中沒(méi)有標(biāo)記完成加鎖過(guò)程。同樣，在解鎖時(shí)向[Chanout]通道寫(xiě)入標(biāo)記，使互斥鎖通道中重新?lián)碛袠?biāo)記值完成了解鎖過(guò)程。互斥量加鎖與解鎖操作表示如下：

[Chanin mutex_in;Chanout mutex_out;mutex_out.read（lcl_mutex）;mutex_in.write（lcl_mutex）;]

圖2 ?互斥量加鎖和解鎖過(guò)程

1.3 ?等待條件與信號(hào)量通道轉(zhuǎn)換

POSIX線程庫(kù)中提供了一種使線程等待來(lái)自其他線程信號(hào)的方法。當(dāng)一個(gè)線程處于等待狀態(tài)時(shí)，直到收到另一個(gè)線程發(fā)來(lái)的喚醒信號(hào)時(shí)，等待線程中才會(huì)被喚醒。該線程庫(kù)中提供了[pthread_cond_wait（）]函數(shù)供用戶使用等待操作，而在C++CSP中將該操作分為解開(kāi)互斥鎖、等待信號(hào)量、鎖定互斥鎖3個(gè)過(guò)程進(jìn)行描述。信號(hào)量的產(chǎn)生與釋放在C++CSP中通過(guò)[flush（）]和[fallinto（）]方法描述，描述方法如下：

[csp：：Bucket cond;cond.flush（）;cond.fallinto（）;]

在多線程程序中，[pthread_cond_wait（）]函數(shù)在C++CSP中描述如下：

[mutex_out.write（lcl_mutex）cond.fallinto（）mutex_in.read（lcl_mutex）]

1.4 ?線程邏輯主體到C++CSP的轉(zhuǎn)換

[pthread_create（*thr，NULL，*start，*arg）]函數(shù)是POSIX線程庫(kù)供用戶進(jìn)行線程創(chuàng)建的方法，該方法的第3個(gè)參數(shù)是創(chuàng)建線程主體的入口。由于在C++CSP中，線程之間使用通道方式進(jìn)行通信，因此將線程主體中的邏輯關(guān)系轉(zhuǎn)換為C++CSP，需要把線程主體中對(duì)共享內(nèi)存的操作轉(zhuǎn)換為通道通信形式。多線程程序中，[thr1]，[thr2]線程主體在C++CSP中，通過(guò)創(chuàng)建[run（）]方法實(shí)現(xiàn)對(duì)共享內(nèi)存操作，對(duì)于每一個(gè)共享變量[X]，對(duì)應(yīng)的局部變量[lcl_X]都會(huì)在[run（）]方法中創(chuàng)建，同時(shí)[run（）]方法還包含了線程中邏輯主體的行為過(guò)程，該方法在執(zhí)行[delete ?thr]方法后線程將被終止。

2 ?面向C++CSP框架的抽象建模

C++CSP框架線程之間通信是以CSP為理論基礎(chǔ)進(jìn)行開(kāi)發(fā)的，所以C++CSP在通信行為上和CSP基本保持一致。而CSP作為一門(mén)可以有效描述并發(fā)結(jié)構(gòu)和進(jìn)程間交互的過(guò)程語(yǔ)言，CSP同樣具有其語(yǔ)法規(guī)則和邏輯。下面將分析如何對(duì)由源程序轉(zhuǎn)換而成的C++CSP框架語(yǔ)言進(jìn)行抽象建模。

2.1 ?進(jìn)程代數(shù)CSP

通信順序進(jìn)程（Communication Sequence Process，CSP）是描述并發(fā)系統(tǒng)中通信實(shí)體進(jìn)行消息交換而設(shè)計(jì)的一種進(jìn)程代數(shù)方法[10]。基于POSIX線程庫(kù)開(kāi)發(fā)的多線程程序是一種并發(fā)系統(tǒng)，本文采用CSP對(duì)多線程程序進(jìn)行形式化建模與分析。

針對(duì)CSP中的符號(hào)約定，設(shè)大寫(xiě)字母[P]，[Q]，[R]表示進(jìn)程，小寫(xiě)字母[x]，[y]表示事件。CSP中進(jìn)程由事件和算子構(gòu)成，它有順序算子“->”和非確定選擇算子“|”兩種基本算子運(yùn)算符。例如：進(jìn)程[P]可表示為[x->Q]，表示事件[x]發(fā)生后流向進(jìn)程[Q];進(jìn)程的選擇可表示為[（x->Q|x->R）]。此外，CSP中還定義了進(jìn)程的復(fù)合操作，例如確定性選擇進(jìn)程（[P[]Q]）、或進(jìn)程（[P?Q]）、并發(fā)進(jìn)程（[P||Q]）、穿插進(jìn)程（[P|||Q]）、順序進(jìn)程（[P;Q]）。