基于SM T求解器的嵌入式多線程程序數(shù)據(jù)競態(tài)條件分析?

容　會　潘有順　王艷玲　周祖坤　王曉亮

（1.昆明冶金高等?？茖W(xué)校藝術(shù)設(shè)計學(xué)院　昆明　650033）（2.昆明理工大學(xué)云南省計算機技術(shù)應(yīng)用重點實驗室　昆明　650500）（3.昆明理工大學(xué)信息工程與自動化學(xué)院　昆明　650500）（4.昆明冶金高等?？茖W(xué)校外語學(xué)院　昆明　650033）（5.昆明冶金高等?？茖W(xué)校招生就業(yè)處　昆明　650033）（6.昆明冶金高等?？茖W(xué)校商學(xué)院　昆明　650033）

1　引言

近年來，在嵌入式硬件領(lǐng)域中，一個芯片上具有多核處理器（CMP）已經(jīng)開始占據(jù)市場并成為主流趨勢，再加上對嵌入式軟件功能的需求日益增加且趨向復(fù)雜，因而在嵌入式軟件設(shè)計中多線程技術(shù)已逐步廣泛應(yīng)用起來。利用多線程編程技術(shù)設(shè)計的嵌入式軟件在其運行過程中能夠?qū)崿F(xiàn)并發(fā)運行，最終達(dá)到了提高軟件性能的目的。跟普通PC系統(tǒng)相比，因共享嵌入式系統(tǒng)中資源為公共資源，多個線程編程技術(shù)會出現(xiàn)較高的復(fù)雜性與不確定性，從而導(dǎo)致嵌入式軟件系統(tǒng)的故障，而最為嚴(yán)重的問題是數(shù)據(jù)競態(tài)條件故障。所以，如何減少多線程軟件的故障發(fā)生，提高程序的運行質(zhì)量，剖析多線程程序中所出現(xiàn)的數(shù)據(jù)競態(tài)條件成為嵌入式系統(tǒng)需要解決的重要問題［1～3］。

數(shù)據(jù)競態(tài)條件的分析根據(jù)檢測分析的依據(jù)不同主要分為基于鎖集的競態(tài)條件檢測分析、基于發(fā)生序（happens-before）的競態(tài)條件檢測分析和基于鎖集和發(fā)生序相結(jié)合的競態(tài)條件檢測分析三種方法。前兩種方法又各自存在不足，基于鎖集分析方法經(jīng)常會有誤報現(xiàn)象發(fā)生，基于發(fā)生序分析方法容易受到線程調(diào)度與交錯的影響會產(chǎn)生漏報現(xiàn)象［4～5］。

本文提出一種基于SMT求解器的嵌入式多線程程序數(shù)據(jù)競態(tài)條件檢測分析方法，它是在獲得并行程序一次執(zhí)行路徑信息記錄的基礎(chǔ)上運用靜態(tài)分析（事后分析）方法，也就是將分析檢測數(shù)據(jù)競態(tài)條件過程轉(zhuǎn)變?yōu)镾MT（可滿足性模理論）求解過程。具體是由嵌入式多線程程序一次執(zhí)行路徑信息所構(gòu)建的各種約束表達(dá)式組成的一個路徑模型F和一個數(shù)據(jù)競態(tài)發(fā)生條件T，然后利用SMT求解器去求解，再根據(jù)求解結(jié)果來判斷程序在這一次執(zhí)行過程中是否存在著數(shù)據(jù)競態(tài)條件，若有就用數(shù)據(jù)競態(tài)繪圖模塊輸出競態(tài)條件圖（RG）和用證據(jù)數(shù)組（WA）來記錄相應(yīng)解釋路徑序列。這樣程序設(shè)計人員就可以快速查看到引發(fā)數(shù)據(jù)競態(tài)條件的原因及關(guān)鍵節(jié)點，從而便于對源程序進行修改和完善［6～9］。

2　嵌入式多線程程序數(shù)據(jù)競態(tài)條件描述

在嵌入式編程中，多線程數(shù)據(jù)競態(tài)條件定義為兩個或兩個以上的線程事件（屬于不同線程）在對沒有同步機制保護的共享資源進行訪問時，它們中至少有一個為寫訪問，最終由這些線程事件的執(zhí)行順序決定結(jié)果。兩個來自不同線程的線程事件作出的訪問操作構(gòu)成了訪問對，用（R，W）表示該訪問對，如果沒有使用同步機制進行保護，此時訪問對（R，W）就形成了數(shù)據(jù)競態(tài)條件［10］。因為組成數(shù)據(jù)競態(tài)的沖突訪問對（R，W）運行的順序不能明確，這樣程序中共享資源的最后運行結(jié)果將由沖突訪問對的運行順序決定，所以說數(shù)據(jù)競態(tài)條件會導(dǎo)致嵌入式多線程程序在運行過程中產(chǎn)生不確定性，如圖1所示。

在圖1所描述的兩個多線程程序并發(fā)運行過程中，如果兩個線程中線程事件執(zhí)行的順序不確定時，沖突訪問對（R0（x），W1（x））和（W0（x），W1（x））之間就會不被同步機制保護，以致形成了數(shù)據(jù)競態(tài)條件。針對讀訪問R0（x）所得到的x值起始于Thead0中的W0（x）與Thead1中的W1（x）這兩個寫操作事件，其結(jié)果全部依賴于讀訪問R0（x）和寫訪問W1（x）的真實的執(zhí)行順序。

圖1　嵌入式系統(tǒng)中數(shù)據(jù)競態(tài)條件案例

3　基于SM T求解器數(shù)據(jù)競態(tài)條件分析方法的相關(guān)概念

為了便于我們分析嵌入式多線程程序在程序運行時表現(xiàn)的數(shù)據(jù)競態(tài)條件，我們在這里對用于分析數(shù)據(jù)競態(tài)條件會使用到的相關(guān)概念及表示符號描述如下：

定義1：線程事件（ei）是指在嵌入式多線程程序執(zhí)行過程中，其中一個線程所表現(xiàn)出來的一個操作事件［11］。

定義2：執(zhí)行路徑（p）是指在嵌入式多線程程序任何時候執(zhí)行過程中全部執(zhí)行的線程事件（ei）所形成的一組有順序的排列，用 p＝(e1＜e2＜…＜en)表示。這里的ei表示多線程程序中的一個線程事件，執(zhí)行路徑（p）中線程事件（ei）依據(jù)程序的順序一致性語義來進行羅列［12］。

定義3：偏序關(guān)系（＜）是指在嵌入式多線程某次程序運行時，線程事件（ei）相互之間存在的前后關(guān)系，我們用符號“＜”來表示。例如用e2＜e1表示e2在 e1前面發(fā)生［13］。

定義4：數(shù)據(jù)競態(tài)條件是指在嵌入式多線程程序任何一次執(zhí)行過程中，假設(shè)Thread1中線程事件e1和Thread2中線程事件e2，如果e1先對內(nèi)存中一個沒有同步保護共享變量進行讀訪問操作，與此同時e2對該變量進行寫訪問作操，我們就說線程事件e1和e2之間具有數(shù)據(jù)竟態(tài)條件，用“→或←”符號表示。假設(shè)有兩個線程事件e1和e2它們之間存在數(shù)據(jù)競態(tài)關(guān)系并且e1比e2先執(zhí)行，我們就可以用表示為，如圖2所示。

定義5：證據(jù)數(shù)組（WA）是指在SMT求解器進行數(shù)據(jù)競態(tài)條件檢測分析完成以后，用來存儲解釋路徑的字符數(shù)組，該字符數(shù)組主要用來存儲一個二維字符［14］。

圖2　嵌入式程序中多線程數(shù)據(jù)競態(tài)條件時空圖

定義6：數(shù)據(jù)競態(tài)圖（RG）是指表示嵌入式程序中線程間的數(shù)據(jù)競態(tài)關(guān)系。一般用“○”表示線程事件，用“→或←”表示線程間競態(tài)關(guān)系［15］。

4　基于SM T求解器的數(shù)據(jù)競態(tài)條件檢測方法

在嵌入式多線程程序中用 p＝(e1＜e2＜…＜en)表示線程隊列TQ與事件記錄TMi轉(zhuǎn)換成一個執(zhí)行路徑。

4.1　建立有關(guān)時序約束條件

依據(jù)程序中語義和時序的執(zhí)行，通過在執(zhí)行路徑p的基礎(chǔ)上分解成相關(guān)的時序約束條件。

1）建立共享內(nèi)存變量值狀態(tài)的約束條件（I）。

我們通過將線程對內(nèi)存變量的訪問按照程序執(zhí)語義序列化成對應(yīng)的邏輯表達(dá)式來反映嵌入式多線程程序中內(nèi)存變量的值狀態(tài)的變化過程。例如：x∧y，這里的x和y用來代表對內(nèi)存變量的值的訪問，它們之間采用合取運算（∧），這種約束條件用 I表示［2］。

2）建立線程事件的時序約束條件（II）。

根據(jù)規(guī)定的順序一致性語義，嵌入式多線程所有線程事件必須按照線程內(nèi)部的先后順序進行各自的操作，此時就要建立體現(xiàn)執(zhí)行順序的約束條件。這里任何一個線程內(nèi)部的線程事件ei中I按規(guī)定從小到大羅列出來（即：ei＜ei+1＜…＜ei+n），它們之間的時序通過偏序（“＜”）來表示，不一樣的線程中線程事件采用合取運算（∧），這種時序約束條件采用 II表示［2］。

3）建立線程事件讀寫的時序約束條件（III）。

對線程事件進行讀或?qū)懙南群箜樞虮硎玖饲度胧蕉嗑€程程序任何一次執(zhí)行路徑（p）中線程之間的進行讀或?qū)懙南群箜樞?。比如?x∧ej＜ei∧(ek＜ej∨ej＜ek))，對x這個共享變量，線程事件 ei讀取到的值就是最近一個線程事件ej寫入的值。為了達(dá)到這個目的就要求ej必須比ei先執(zhí)行，與此同時線程事件ek在執(zhí)行寫操作時或者在寫操作ej前面執(zhí)行，或者在讀操作ei后面執(zhí)行。這種時序約束用 III表示［2］。

4.2　構(gòu)建Yices求解器的輸入量

1）構(gòu)建路徑模型（F）

在建立有關(guān)時序約束條件分析的基礎(chǔ)上，將上述推理出來的的各種約束條件表達(dá)式采用合?。ā模┻\算，形成了一個包括嵌入式多線程程序執(zhí)行過程中所有可能發(fā)生的很多約束條件的一階邏輯表達(dá)式（路徑模型F），用它作為Yices求解器的一個輸入量，這里路徑模型F如下所示。

其中，I代表內(nèi)存變量值的狀態(tài)約束條件，II代表線程事件的時序約束條件，III代表線程事件讀寫時序的約束條件。

2）構(gòu)建數(shù)據(jù)競態(tài)發(fā)生條件（Ti）

通過由路徑追蹤方法分析多線程一次執(zhí)行路徑p，依據(jù)本文中定義4（數(shù)據(jù)競態(tài)條件）得到對同一內(nèi)存變量進行讀、寫或?qū)憽懺L問操作的兩個屬于不同線程事件ei與ej。通過對這兩個線程事件進行交換，同時推出包含它們前后線程事件的一個合取范式Ti。因為在一個執(zhí)行路徑p中依據(jù)當(dāng)前狀況能構(gòu)成許多個Ti。比如：e1，e2是ei的前后線程事件，e3，e4是ej的前后線程事件，這樣構(gòu)建的數(shù)據(jù)競態(tài)發(fā)生條件 Ti=(e1＜ej＜e2∧e3＜ei＜e4)。此處在構(gòu)建Ti時，依據(jù)定義4找可能發(fā)生數(shù)據(jù)競態(tài)條件的線程事件，這樣可以減少了SMT求解器的分析次數(shù)和工作量。

5　實驗驗證

本文通過一個簡單的嵌入式多線程程序作為調(diào)試用例，如圖3所示，通過這個用例證明了本文中提出的嵌入式數(shù)據(jù)競態(tài)條件檢測分析方法在檢測分析程序一次執(zhí)行過程中發(fā)生的數(shù)據(jù)競態(tài)條件的有效性。

圖3　嵌入式多線程程序為調(diào)試用例

本用例中通過多線程程序在任何一次運行后通過路徑追蹤方法可以得出執(zhí)行路徑為 p＝(e1＜e2＜e3＜e4＜e5＜e6＜e7＜e8＜e9＜e10＜e11＜e12) 。這里用ei來表示線程事件，用i表示線程事件中的順序號。

依據(jù)規(guī)定的程序執(zhí)行時序與執(zhí)行語義要求，以現(xiàn)有的執(zhí)行路徑p做為基礎(chǔ)，然后跟源程序結(jié)合起來建立的約束條件如下：

內(nèi)存變量值共享狀態(tài)的約束條件（I）。用x和y表示源代碼中的全局共享變量，通過推理得到如下I表達(dá)式：

線程事件的時序約束條件（II）。依據(jù)執(zhí)行路徑p和線程內(nèi)執(zhí)行語義，推理出如下III表達(dá)式：

線程事件的讀寫時序約束條件（III）。用x和y表示源代碼中的全局共享變量。依據(jù)執(zhí)行路徑p，針對x變量，讀線程事件有e8和e11，寫線程事件有e1，e8和e11，通過推理得到和它相關(guān)的讀寫時序表達(dá)式為

針對y變量，讀線程事件有e6和e10，寫線程事件有e2，e6和e10，通過推理得到和它相關(guān)的讀寫時序表達(dá)式為

然后對這兩個表達(dá)式采用析?。ā牛┻\算，最終可以得出III表達(dá)式如下

結(jié)合上述推理出來的三個約束條件表達(dá)式采用合取運算，這樣就可以得出路徑模型F。

依據(jù)執(zhí)行路徑p和數(shù)據(jù)競態(tài)條件定義4，我們就能得出程序中一個可能的數(shù)據(jù)競態(tài)發(fā)生條件T1表達(dá)式如下

通過合取范式（F∧T1）輸入到Y(jié)ices求解器中進行運算，Result結(jié)果為Unsat，輸出“有競態(tài)條件”，與此同時得到的結(jié)果就是這個數(shù)據(jù)競態(tài)條件發(fā)生的解釋路徑W，這樣就證明發(fā)生條件T1成立。通過保存證據(jù)模塊將W表達(dá)式存儲到證據(jù)數(shù)組（WA）中。

最終通過數(shù)據(jù)競態(tài)條件繪圖模塊將引發(fā)數(shù)據(jù)競態(tài)條件的兩個線程事件e8和e11的數(shù)據(jù)競態(tài)圖（RG）輸出，如圖4所示。

圖4　實驗用例數(shù)據(jù)競態(tài)條件圖

6　結(jié)語

本文針對嵌入式多線程程序中出現(xiàn)的數(shù)據(jù)競態(tài)條件問題，提出了一種基于SMT求解器數(shù)據(jù)競態(tài)條件檢測分析方法。通過對多線程程序的一次執(zhí)行過程所獲取到的執(zhí)行路徑p，經(jīng)過SMT求解器判斷其中是否存在數(shù)據(jù)競態(tài)條件，如果存在就用數(shù)據(jù)競態(tài)繪圖模塊輸出競態(tài)條件圖（RG）和用證據(jù)數(shù)組（WA）來記錄相應(yīng)解釋路徑序列。通過實驗證明，本文的分析與檢測方法對嵌入式多線程程序的分析結(jié)果是可靠的和有效的，該研究有一定的使用價值。

［1］陳艷，徐曉峰，李曉潮，等.實時嵌入式系統(tǒng)的競態(tài)條件及其分析方法研究［J］.計算機研究與發(fā)展，2010，47（7）：1201-1210.CHEN Yan，XU Xiaofeng，LIXiaochao，et al.Race Condition and Its Analysis Approach of Real-time Embedded Systems［J］.Journal of Computer Research and Development，2010，47（7）：1201-1210.

［2］張晶，潘有順.嵌入式系統(tǒng)同步進程的競態(tài)條件分析與推理學(xué)習(xí)方法［J］.計算機科學(xué)，2014，41（2）：141-144.ZHANG Jing，PAN Youshun.Competitive condition analysis and reasoning learningmethod for synchronous process of embedded system［J］.Computer Science，2014，41（2）：141-144.

［3］Theodorus E Setiadi，Akihiko Ohsuga and Mamoru Maekawa.Efficient TestCase Generation for Detecting Race conditions［J］.IAENG International Journal of Computer Science，2014，41（2）：112-130.

［4］Zakharov A V and Moiseev MJ.Automatic data race detection in systemCmodels［J］.Automatic Controland Computer Sciences，2012，46（7）：356-363.

［5］霍瑋，于洪濤，馮曉兵，等.靜態(tài)檢測中斷驅(qū)動程序的數(shù)據(jù) 競 爭［J］.計 算 機 研 究 與 發(fā) 展 ，2011，48（12）：2290-2299.HUO Wei，YU Hongtao，F(xiàn)ENG Xiaobing，et al.Static Race Detection of Interrupt-Driven Programs［J］.Journal of Computer Research and Development，2011，48（12）：2290-2299.

［6］C Flanagan and SN Freund.Type-based Race Detection for Java［C］.In Proceedings of the ACM SIGPLAN PLDI'00，Vancouver，British Columbia，Canada，2000：219-232.

［7］TA Henzinger，R Jhala and R Majumdar.Race Checking by Context Inference［J］.ACM SIGPLAN Notices，2004，39（6）：1-13.

［8］Kasikei B，Zam fir C and Candea G.RaceMob：Crowd sourced data rae detection［C］//Proc of SOSP'13，2013：406-422.

［9］Engler D，Ashcraft K.RacerX：Effective static detection of race conditions and deadlocks［C］//Proceeding of the 19thACM Symp on Operating Systems Principles（SOSP）.New York：ACM，2003：237-252.

［10］Blanc N，Kroening D.Race analysis for SystemC using model checking［C］//proceeding of IEEE/ACM Int Conf on Computer Aided Design.New York：ACM，2008：356-363.

［11］Yu Y，Rodeheffer T，Chen W.Racetrack：Efficient detection of data race conditions via adaptive tracking［C］//Principles.New York：ACM，2005：221-234.

［12］Klein P N，Lu H I，Netzer R H B.Detecting race conditions in parallel programs thatuse semaphores［J］.Algorithmic，2003，35（4）：321-345.

［13］Pozniansky E，Schuster A.Efficient on-the-fly data race detection in multithreaded C++Programs［C］//Proceeding of PPoPP'03.New York：ACM，2003：179-190.

［14］Tai K C.Race analysis of traces of asynchronous message-pas-sing programs［C］//Proceeding of ECDCS'97.Piscataway，NJ：IEEE，1997：261-268.

［15］Park MY，Hai N C T，Jun Y K，et al.Visualization of message races in MPI parallel programs［C］//Proceeding of the 7th IEEE Int Conf on Computer and Information Technology.Piscataway，NJ：IEEE，2007：316-321.