高飛 武淑紅 王耀力

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

關鍵詞： 多線程建模; 死鎖檢測; 語義轉換; 形式化驗證; 通信順序進程; 過程分析

中圖分類號： TN911.23?34; TP311.5 ? ? ? ? ? ? 文獻標識碼： A ? ? ? ? ? ? ? ? ?文章編號： 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 ?引 ?言

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

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

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

圖1 ?多線程程序建模和檢測流程

1 ?多線程程序到C++CSP框架轉換

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

下面將針對圖2分析在POSIX多線程程序中，如何將通信結構轉換為具有等效語義的消息傳遞結構。

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

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

1.2 ?互斥鎖通道轉換

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

互斥量加鎖和解鎖過程如圖2所示。在C++CSP中，互斥鎖是通過互斥鎖通道（[LockChannel]）進行模擬的，[LockChannel]由輸入通道和輸出通道兩部分組成。聲明互斥量時，需要對互斥量通道初始化，向[Chanin]通道輸入一個互斥標記值表明當前為可加鎖狀態(tài)。當加鎖時，從[Chanin]通道中讀出標記值，互斥鎖通道中沒有標記完成加鎖過程。同樣，在解鎖時向[Chanout]通道寫入標記，使互斥鎖通道中重新?lián)碛袠擞浿低瓿闪私怄i過程?；コ饬考渔i與解鎖操作表示如下：

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

圖2 ?互斥量加鎖和解鎖過程

1.3 ?等待條件與信號量通道轉換

POSIX線程庫中提供了一種使線程等待來自其他線程信號的方法。當一個線程處于等待狀態(tài)時，直到收到另一個線程發(fā)來的喚醒信號時，等待線程中才會被喚醒。該線程庫中提供了[pthread_cond_wait（）]函數(shù)供用戶使用等待操作，而在C++CSP中將該操作分為解開互斥鎖、等待信號量、鎖定互斥鎖3個過程進行描述。信號量的產(chǎn)生與釋放在C++CSP中通過[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的轉換

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

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

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

2.1 ?進程代數(shù)CSP

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

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