張曉東，鄭慶華，劉 烴，俞樂晨，劉 沛，楊子江

( 1.西安交通大學智能網(wǎng)絡與網(wǎng)絡安全教育部重點實驗室，陜西 西安 710049；2.西安理工大學計算機科學與工程學院，陜西 西安 710049)

多線程程序數(shù)據(jù)競爭檢測與證據(jù)生成方法*

張曉東1，鄭慶華1，劉 烴1，俞樂晨1，劉 沛1，楊子江2

( 1.西安交通大學智能網(wǎng)絡與網(wǎng)絡安全教育部重點實驗室，陜西 西安 710049；2.西安理工大學計算機科學與工程學院，陜西 西安 710049)

數(shù)據(jù)競爭是多線程程序最為常見的問題之一。由于線程交織導致狀態(tài)空間爆炸，多線程程序數(shù)據(jù)競爭引起的錯誤檢測難度大、成本高、精度低；此外，即使檢測到數(shù)據(jù)競爭，由于線程調度難以控制、執(zhí)行過程難以復現(xiàn)，錯誤難以復現(xiàn)和定位。提出了一種多線程程序數(shù)據(jù)競爭檢測與證據(jù)生成方法，基于程序語義分析和執(zhí)行過程監(jiān)測，構建程序的執(zhí)行路徑約束模型和數(shù)據(jù)競爭條件，將多線程程序數(shù)據(jù)競爭檢測問題轉化為約束求解問題，降低檢測難度，提高檢測精度；利用SMT求解器計算可能的數(shù)據(jù)競爭，并生成觸發(fā)該數(shù)據(jù)競爭的程序執(zhí)行序列，協(xié)助程序員定位和驗證錯誤。實驗中對10個程序進行了測試，相比現(xiàn)有數(shù)據(jù)競爭檢測工具threadsanitizer和helgrind，本方法檢測出的數(shù)據(jù)競爭多出287.5%和264.7%，且沒有誤報，而其他方法平均誤報率為10.5%和9.8%。

多線程程序測試；數(shù)據(jù)競爭；約束求解；證據(jù)生成

1 引言

隨著處理器多核化的普及，多線程技術已經(jīng)成為軟件編程中提高CPU利用率不可或缺的技術。然而，由于線程之間交織的不確定性，多線程程序執(zhí)行過程中可能會出現(xiàn)一些難以預料的行為導致程序出錯，例如對臨界區(qū)沒有做好同步工作而導致的數(shù)據(jù)競爭問題。數(shù)據(jù)競爭是兩個不同的線程在沒有同步保護的情況下同時訪問一個內存，并且至少有一個寫操作[1]。數(shù)據(jù)競爭不一定導致程序錯誤，因為有些程序員故意讓程序有數(shù)據(jù)競爭以提高運行的效率，但是有調查表明5%～24%的數(shù)據(jù)競爭會對程序產生壞影響[2, 3]。數(shù)據(jù)競爭很難被發(fā)現(xiàn)，因為它們經(jīng)常發(fā)生在一些低概率出現(xiàn)的交織序列中，在現(xiàn)實中往往需要花很多時間去定位，其引起的錯誤如同“corner error”，即使在軟件發(fā)布時也未必能夠完全清除它們[4]。因此，數(shù)據(jù)競爭檢測是多線程程序測試領域最受關注的研究點之一。

過去幾十年中數(shù)據(jù)競爭檢測已有大量研究，設計出很多杰出的自動化檢測工具，主要分為靜態(tài)[3, 5]與動態(tài)分析技術[1, 6～9]。靜態(tài)方法通過靜態(tài)檢測程序所有的路徑來推斷程序中的所有數(shù)據(jù)競爭，可以檢測出大部分數(shù)據(jù)競爭；但由于使用大量假設，靜態(tài)分析方法會產生無效的數(shù)據(jù)競爭，導致誤報率較高。動態(tài)方法通過監(jiān)控一次執(zhí)行中內存與同步信息以確定是否存在數(shù)據(jù)競爭，能夠提供較高精度的檢測結果。但是，動態(tài)分析方法受到交織與路徑的影響，往往要通過多次執(zhí)行來提高覆蓋率。本文將靜態(tài)代碼分析與程序執(zhí)行過程監(jiān)測相結合，以提高覆蓋率且盡可能消除誤報。

現(xiàn)有的動態(tài)檢測技術主要分為三種：基于lockset[1]、基于happens-before[9, 10]與二者結合的方法[6, 11]。(1)基于lockset的方法對線程交織不敏感，但是存在誤報情況，即無效競爭。(2)基于happens-before的方法只檢測某特定交織序列上的數(shù)據(jù)競爭，檢測結果雖可靠，但敏感于線程交織。(3)混合方法結合了兩者的優(yōu)點，并且試圖減少各自的缺點，但也面臨如不能夠搜索出隱藏的錯誤、lockset高誤報引起的無效報警等問題[4]。

本文提出一種新的多線程程序數(shù)據(jù)競爭檢測方法，根據(jù)多線程程序語義構建約束表達式，將數(shù)據(jù)競爭檢測問題轉化為可滿足性模理論SMT(Satisfiability Modulo Theories)問題，采用SMT求解器求解約束表達式發(fā)現(xiàn)可能存在的數(shù)據(jù)競爭，并生成對應執(zhí)行路徑。本方法主要分為四步：(1)監(jiān)控程序以得到執(zhí)行路徑；(2)將執(zhí)行路徑轉化為無量詞一階邏輯表達式F，此約束表達式涵蓋所有可能的線程交織；(3)構建數(shù)據(jù)競爭候選集合，生成每一個候選發(fā)生競爭的條件ρ；(4)遍歷候選集合，對每一個ρ求解約束表達式F∧ρ，檢查是否存在數(shù)據(jù)競爭，如果有則生成對應的證據(jù)。實驗中，設計實現(xiàn)了一個針對Pthread多線程程序的數(shù)據(jù)競爭檢測原型系統(tǒng)，其中采用基于LLVM的插樁工具，其只對內存操作語句以及同步語句進行監(jiān)控；利用求解器Yices[12]來驗證與分析路徑信息，以檢測出所有數(shù)據(jù)競爭。另外，本文所提方法能夠生成每個數(shù)據(jù)競爭的證據(jù)序列，該序列向程序員展示數(shù)據(jù)競爭的觸發(fā)原因。

本文的主要貢獻點如下：

(1)提出一種多線程程序約束構建模型，將一次執(zhí)行中的數(shù)據(jù)競爭檢測問題轉化為約束求解問題。此模型按照程序語義進行約束構建，所構建的表達式包含了所有可能的交織序列，進而檢測出執(zhí)行路徑中的所有數(shù)據(jù)競爭。

(2)對所有數(shù)據(jù)競爭都產生一個證據(jù)序列，以給用戶提供數(shù)據(jù)競爭是如何被觸發(fā)的信息。

(3)對執(zhí)行序列進行事后分析，不存在on-the-fly技術所產生的巨大運行時開銷。

2 動機示例

在此用一個示例來說明本文方法是如何找到路徑中的數(shù)據(jù)競爭。示例程序如圖1所示，x與y為共享變量，線程0創(chuàng)建了線程1與線程2。接下來，驗證該示例程序是否存在數(shù)據(jù)競爭的情況。

sharedx,yThread0Thread1Thread21:x=0;4:lock(m);8:lock(m);2:create(1);5:x=a+b;9:x++;3:create(2);6:unlock(m);10:y++;7:y++;11:unlock(m);

Figure 1 Example program

圖1 示例程序

隨機執(zhí)行示例程序，生成路徑π=[1,2,3,4,5,6,7,8,9,10,11]。對π進行約束構建，所生成的表達式如圖2所示。下面逐一解釋圖2中所有約束的意義與作用。其中，oi表示第i行語句在一次交織序列中的排列序號。

內存模型:o1

Figure2Constraint

圖2 約束

內存模型表示程序中變量之間的關系，本文中采用順序一致性的語義。順序一致性規(guī)定CPU按照代碼中語句的順序來執(zhí)行程序，所以線程內語句之間的關系如o1

同步約束要求線程之間事件的排序必須按照同步語義，即對線程中l(wèi)ock/unlock操作的約束。在本示例中，要么線程1先獲取鎖o6

偏序約束要求線程1的首個事件在其創(chuàng)建點之后執(zhí)行，即o2

競爭條件:數(shù)據(jù)競爭定義為兩個線程同時訪問同一內存，且至少有一個寫操作。以o6

將圖2中所有表達式相與，利用求解器求解，根據(jù)結果斷定第7行與第10行之間存在數(shù)據(jù)競爭。同時，根據(jù)求解結果對每個事件進行排序，即得到圖2中的證據(jù)序列。

基于happens-before的方法根據(jù)判斷事件之間是否存在happens-before關系來斷定數(shù)據(jù)競爭。在路徑φ=[1,2,3,4,5,6,7,8,9,10,11]中，由于第7行與第10行之間沒有happens-before關系，故檢測出二者之間存在數(shù)據(jù)競爭。但是，如果檢測路徑φ的其他交織[1,2,3,8,9,10,11,4,5,6,7]，利用happens-before的方法則檢測不出數(shù)據(jù)競爭。這也恰恰說明happens-before方法對線程交織非常敏感的缺點。

雖然基于lockset方法的檢測效果不敏感于線程交織，但是檢測結果往往會有誤報。例如，該方法計算出第1行的鎖集為空，第5行的鎖集為{m},二者相交為空，即判定此兩行之間存在數(shù)據(jù)競爭，實際上二者不可能并發(fā)訪問x，檢測出的數(shù)據(jù)競爭是錯誤的。與基于happens-before的方法相比，本文所提的方法能夠檢測出執(zhí)行序列中的數(shù)據(jù)競爭；與基于lockset的方法相比，能夠識別出第1行與第5行不存在數(shù)據(jù)競爭現(xiàn)象。

3 定義

3.1 事件

本文用事件表示在多線程程序執(zhí)行過程中觀察到的原子執(zhí)行步。在解決數(shù)據(jù)競爭問題時，關注的事件類型包括以下兩類：共享變量的讀與寫、線程操作事件(一般有線程創(chuàng)建與終止、鎖的獲取與釋放、條件變量的wait與signal)。事件是計算與分析的基本單位，所以必須要包括足夠的信息以助于約束構建。

將事件定義為一個四元組〈tid,type,var,status〉，其中，tid表示線程ID，用于區(qū)別事件屬于哪一個線程。type表示事件的操作類型，包括讀寫操作或者線程控制操作。var表示相關變量，如果是賦值語句，則表示共享變量的名字；如果是同步操作語句，則表示互斥量或者條件變量；如果是線程控制語句，則表示為“-”。status表示當type為線程創(chuàng)建或者終止操作時，所控制的線程ID；其他類型的操作都表示為“-”。

例如，事件〈1,read,x,-〉表示線程1對共享變量x進行讀操作，事件〈1,fork,-,101〉表示線程1創(chuàng)建線程101。

3.2 路徑

在給定輸入π下，設定Eπ為多線程程序一次執(zhí)行中被執(zhí)行到的事件集合。一條路徑τ是指集合Eπ所有事件的一個有序排列，且此排列遵守程序的執(zhí)行語義。τ與τ的交織序列τ′在線程內的時序關系相同，但線程間的時序關系不同。

3.3 可行序列集合

在同一輸入下，每次執(zhí)行多線程程序都可能會產生不同的交織序列。假設Lπ為偏序集合(E,?)，其中：

(1)E={e|e∈Eπ}，e表示τ上的事件。

(2)?表示偏序關系，對于任意em、en∈E：

如果tid(em)=tid(en)且m

如果em為線程創(chuàng)建事件，而en為被創(chuàng)建線程的首個事件，則em

如果em為線程終止事件，而en為被終止線程的末尾事件，則en

?是傳遞閉包的。

一條路徑一定是一個對Eπ的線性化排列，且遵守順序一致性的語義。但是，任意一個Eπ的線性化排列即使符合偏序關系也未必是一條執(zhí)行路徑，因為在多線程程序執(zhí)行過程中事件之間的關系還要受同步語義的約束。

因此，結合Lπ與同步語義約束就構成了所有正確的線性化排列，稱之為FLS(Feasible Linearization Set)。驗證某一次執(zhí)行也即是對FLS進行遍歷。然而，遍歷搜索空間往往非常困難，例如，如果有n個線程，每個線程有k個執(zhí)行步，則交織數(shù)量將達到(nk)!/(k!)n。本文將數(shù)據(jù)競爭檢測問題轉化為約束求解問題，借助約束求解器的強大性能來解決遍歷難題。

4 數(shù)據(jù)競爭檢測

給定一條多線程執(zhí)行路徑τ，將τ編碼為一階邏輯表達式F，F(xiàn)組成一個包括所有線性排列的搜索空間：

其中，Φpf為路徑表達式，Φmo為內存模型順序約束，Φrw為讀寫關系約束，Φsyn為同步語義約束，Φpo為偏序約束。從搜索空間中找到所有的數(shù)據(jù)競爭，并生成每一個觸發(fā)該數(shù)據(jù)競爭發(fā)生的線性化序列作為數(shù)據(jù)競爭問題的證據(jù)。

4.1 約束構建方法

從線程的角度，也可以定義Eπ={Ti|0

(1)路徑表達式(Φpf)。

將每一個線程序列轉化為SSA格式，對于每一個SSA格式的執(zhí)行序列，除去共享訪問點都是一個完整的定義-使用鏈。類似于路徑條件(Path Condition)的收集，直接將SSA格式序列轉化為路徑表達式。此外，本文用符號值來代替系統(tǒng)調用的返回值。

(2)內存模型約束(Φmo)。

在構建內存模型約束時，本文采用順序一致性模型。順序一致性語義規(guī)定，所有操作完全按程序的順序執(zhí)行。那么在此情況下，線程內的事件順序符合約束：

其中ei與ei+1表示同一線程內連續(xù)的兩個事件。

(3)讀寫順序約束(Φrw)。

路徑表達式Φpf定義了線程內定義-使用鏈，而對于線程間的定義-使用鏈，則由讀寫順序約束Φrw定義。在線程執(zhí)行時共享變量讀取到的值，必須來自最近的寫值(包括初始值)。約束Φrw對共享變量的讀寫關系進行約束，使共享變量的讀來自于最近的寫。對于同一共享變量，令R作為所有對其進行讀操作的事件集合，令W作為所有對其進行寫操作的事件集合。給出以下公式：

其中，er為讀事件，ew與ex為寫事件，vr和vw為事件er與ew所操作的變量。公式的意思是，如果事件er中的vr取值來自于事件ew中的vw，首先要滿足er在ew之后，即O(ew)

(4)同步語義約束(Φsyn)。

在多線程程序中表達同步語義的語句主要是lock/unlock與wait/signal操作。互斥變量通過控制線程訪問共享數(shù)據(jù)來實現(xiàn)同步，而條件變量則基于數(shù)據(jù)的實際值來同步線程。那么，同步語義約束包括這兩種操作：

①lock/unlock。

在構建lock同步語義時，在同一互斥鎖的lock/unlock集合L中，對于任意兩個lock/unlock事件對：li/ui與lk/uk，須滿足公式：

在此公式中，鎖對li/ui要么發(fā)生在鎖對lk/uk之前，要么發(fā)生在其后。注意，在Φmo中已含有約束O(li)

②wait/signal。

對于條件變量同步語義，要滿足條件：每一個wait操作必須對應一個signal操作，而一個signal操作至多喚醒一個wait操作。對于同一條件變量cond，令WT為在cond上所有wait操作的集合，令SG為在cond上所有signal操作的集合。如要滿足之上的條件，須有以下公式：

(5)偏序約束(Φpo)。

如果事件創(chuàng)建一個線程，那么被創(chuàng)建線程的所有事件都要在此事件之后執(zhí)行。如果事件執(zhí)行join操作，那么被join線程的所有事件都要在此事件之前。本文用偏序關系約束來描述程序中的create/fork/join操作語義。令C為create/fork操作的事件集合，令J為join操作的事件集合。給定約束：

其中，ec為線程創(chuàng)建事件，first(ec)為ec所創(chuàng)建的線程首個事件的順序；ej為線程終止事件；last(ej)為ej所結束的線程末尾事件的順序。

(6)數(shù)據(jù)競爭條件(ρ)。

如果有這樣一條路徑τ=〈τ1eiejτ2〉，其中τ1是前綴，τ2是后綴，事件ei與ej屬于不同的線程并且都訪問同一內存，至少有一個寫，那么二者之間發(fā)生了數(shù)據(jù)競爭，而看作是與數(shù)據(jù)競爭的證據(jù)序列。

4.2 數(shù)據(jù)競爭檢測方法與證據(jù)生成

給定候選數(shù)據(jù)競爭發(fā)生的條件ρ，驗證是否存在一條交織序列使得ρ成立。因為搜索空間F包含了在給定輸入下所有可能的線程交織序列，所以將搜索空間F與數(shù)據(jù)競爭條件ρ合并，生成程序數(shù)據(jù)競爭表達式：

利用SMT求解器來檢查公式Fveri的可滿足性，判斷程序是否可能發(fā)生數(shù)據(jù)競爭。如果無解，說明此候選數(shù)據(jù)競爭不會發(fā)生；如果有解，說明存在數(shù)據(jù)競爭。在有解的情況下，生成一條觸發(fā)該數(shù)據(jù)競爭的證據(jù)序列提供給用戶，此序列與操作系統(tǒng)與運行時環(huán)境無關，可以指導程序員定位和修改錯誤。由此，數(shù)據(jù)競爭的檢測問題即轉化為SMT求解問題，大大減輕了交織組合爆炸問題。

數(shù)據(jù)競爭的驗證過程如算法1中所示，通過遍歷DRCS來驗證所有數(shù)據(jù)競爭。如果Result為sat，則說明此候選滿足競爭條件，同時根據(jù)求解結果計算出觸發(fā)序列，此觸發(fā)序列即是證據(jù)；否則，繼續(xù)遍歷DRCS。在遍歷的過程中，對每一次F∧ρ，利用SMT求解器的增量求解機制來減少求解的開銷[12]。

算法1驗證框架

輸入：所有候選數(shù)據(jù)競爭的發(fā)生條件(DRCS)與搜索空間F;

輸出：所有數(shù)據(jù)競爭以及對應的證據(jù)序列。

For eachρ∈DRCS

Result= SMT_Solving(F∧ρ);

If (Result== sat) Then

Report this data race and output its witness;

Else

Continue;

4.3 計算復雜度

假設事件數(shù)量為n，全局訪問點為m，同步操作語句lock/unlock數(shù)量為l，fork與create語句數(shù)量為k，則內存模型約束的復雜度為O(n)，同步語義約束的復雜度為O(l(l-1))，偏序約束的復雜度為O(k)，候選數(shù)據(jù)競爭約束的復雜度為O(m(m-1))。因此，本方法構建的約束表達式復雜度為多項式O(n+l(l-1)+m(m-1))，其約束構建與求解的開銷都在可接受范圍之內。

5 驗證測試

在LLVM[13]平臺上實現(xiàn)了多線程程序約束構建，在LLVM中間字節(jié)碼的粒度上，通過插樁程序并監(jiān)控程序運行過程、記錄執(zhí)行路徑。然后，根據(jù)4.1節(jié)中設計的約束模型，析取該執(zhí)行路徑下程序的各類約束表達式。利用Yices[12]作為SMT求解器，檢測是否存在數(shù)據(jù)競爭。實驗是在ubuntu 12.04環(huán)境下進行的，處理器是i5 3.2 GHz，內存是4 GB。與現(xiàn)有數(shù)據(jù)競爭檢測工具tsan[8]與helgrind[9]進行了對比(tsan結合happens-before與lockset方法，helgrind是基于happens-before的方法)。

在測試程序中，example是C語言實現(xiàn)的示例程序；程序carter、stateful、account、twostage選自文獻[14]；dekker、lamport、peterson、szymanski與time_var_mutex這五個程序來自于文獻[15]。對所有的測試程序，利用tsan、helgrind與本文方法進行分析比較，實驗結果如表1所示。在表1中，列LoC表示源碼行數(shù)，#T表示線程數(shù)，#SAP表示共享訪問點，Time表示計算開銷，其中包括判斷是否有數(shù)據(jù)競爭以及生成反例，最后一行Avg.表示各項指標的平均值。從實驗數(shù)據(jù)中得知，當共享訪問點較多時，分析時間相對較長。本文方法屬于事后分析，在時間方面不與threadsanitizer與helgrind進行比較，將重點對比在數(shù)據(jù)競爭檢測數(shù)量(N)與誤報率(FP)上的差別。

對于carter、stateful、account、twostage，本文方法檢測出的競爭數(shù)量與threadsanitizer、helgrind相同，且誤報率都為零。

在檢測example、dekker、lamport、peterson、szymanski與time_var_mutex時，本文方法所檢測出數(shù)據(jù)競爭的數(shù)量超過其他兩者。尤其是szymanski，本文方法可以檢測出34個有效數(shù)據(jù)競爭，多于其他兩者。

對于dekker、lamport、peterson、szymanski，此四程序并不是由鎖,而是由循環(huán)語句來控制同步的。

其他兩者在處理類似圖3中所示的情況時，o1與o3會被認為是數(shù)據(jù)競爭。但是，根據(jù)值傳遞與語義的限制(o1要執(zhí)行在o2之前)，o1與o3不可能并發(fā)執(zhí)行。例如，在檢測dekker所產生的四個數(shù)據(jù)競爭中[15]，其他兩者會誤報第22行x=0與第39行x=1存在數(shù)據(jù)競爭，但其實兩者中間有第23行assert(x≤0)，限定執(zhí)行中第22行要在第23行之前，而第39行必須在第23行之后。本文方法則利用路徑表達式與讀寫關系約束限制程序按照正確語義執(zhí)行，不會誤報此類無效數(shù)據(jù)競爭。

AB……1:x=02:while(x==0);…3:x=1…

Figure 3 Spurious race

圖3 假競爭

經(jīng)過實驗數(shù)據(jù)比對，tsan與helgrind在檢測此四程序時誤報率較高，其中tsan平均為29%，helgrind為27%。相比，本方法在誤報率方面低于工具threadsanitizer與helgrind。

6 相關工作

在數(shù)據(jù)競爭檢測方面已經(jīng)有很多方法。其中可以分為動態(tài)、靜態(tài)、動靜結合。靜態(tài)分析工具是通過對源代碼進行分析以輸出代碼中的所有數(shù)據(jù)競爭，當然存在一定的誤報問題[3, 16]。動態(tài)檢測方法是通過將運行時分析類庫注入到被測程序中，在具體運行程序時進行數(shù)據(jù)競爭的預測，這種方法雖然只能檢測出執(zhí)行路徑上的數(shù)據(jù)競爭，但是誤報較少[1, 8, 9]。動靜結合的方法是先靜態(tài)找出所有可能的數(shù)據(jù)競爭，然后只監(jiān)控可能發(fā)生數(shù)據(jù)競爭的內存，最后再利用動態(tài)分析方法檢測程序[4]。

Table 1 Experimental results表1 實驗結果

實際上，動態(tài)分析方法所帶來的運行時開銷是很大的，相關研究人員已做了很多工作以減少運行時開銷。Marino D等人[10]設計了工具LiteRace，通過抽樣監(jiān)控內存來減少運行時開銷。Kasikci B等人[4]通過減小監(jiān)控范圍在一定程度上減小了運行時開銷。還有一種方法通過加大監(jiān)控內存的粒度來降低運行時開銷，但是同時也有誤報[17]。

Wang C等人[18, 19]利用執(zhí)行路徑與程序源碼構建一個符號化的預測模型，以檢測并行程序中斷言預測與原子性違背問題。本文方法的思想一部分來自于Said M等人在文獻[20]中提出的方法，用于實現(xiàn)數(shù)據(jù)競爭的預測以及路徑的還原。但是，文獻[20]中只處理了Java程序路徑中某一個數(shù)據(jù)競爭，而本文是針對路徑中所有的數(shù)據(jù)競爭。

7 結束語

本文提出了一種多線程程序數(shù)據(jù)競爭檢測與證據(jù)生成方法，通過對一條執(zhí)行路徑進行約束建模，將數(shù)據(jù)競爭檢測問題轉化為約束求解問題，利用現(xiàn)有約束求解器分析出一條執(zhí)行路徑中所有可能的數(shù)據(jù)競爭，并且對于每個數(shù)據(jù)競爭都給出觸發(fā)證據(jù)序列。本方法將數(shù)據(jù)競爭靜態(tài)檢測與動態(tài)監(jiān)測相結合，有效降低分析的復雜度和檢測的誤報率。本研究通過構建多線程程序的約束模型，將程序測試轉化為約束求解的方法，可以避免由于多線程程序線程交織導致的狀態(tài)空間爆炸問題，該思路為軟件覆蓋性測試，特別是多線程程序測試提出了新的解決方案。

[1] Savage S, Burrows M, Nelson G, et al. Eraser:A dynamic data race detector for multithreaded programs[J]. ACM Transactions on Computer Systems (TOCS),1997, 15(4):391-411.

[2] Erickson J, Musuvathi M, Burckhardt S, et al. Effective data-race detection for the Kernel[C]∥Proc of OSDI’10, 2010:1-16.

[3] Voung J W, Jhala R, Lerner S. RELAY:Static race detection on millions of lines of code[C]∥Proc of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2007:205-214.

[4] Kasikci B, Zamfir C, Candea G. RaceMob:Crowd sourced data race detection[C]∥Proc of SOSP’13, 2013:406-422.

[5] Wang L, Stoller S D. Runtime analysis of atomicity for multithreaded programs[J]. IEEE Transactions on Software Engineering, 2006, 32(2):93-110.

[6] Xie X, Xue J, Zhang J. Acculock:Accurate and efficient detection of data races[J]. Software:Practice and Experience, 2013,43(5):543-576.

[7] Wester B, Devecsery D, Chen P M, et al. Parallelizing data race detection[C]∥Proc of ASPLOS’13, 2013:27-38.

[8] Serebryany K, Iskhodzhanov T. ThreadSanitizer:Data race detection in practice[C]∥Proc of WBIA’09, 2009:62-71.

[9] Helgrind:A data race detector[EB/OL].[2007-01-01].http://valgrind.org//docs/manual/hg-manual.html.

[10] Marino D, Musuvathi M, Narayanasamy S. LiteRace:Effective sampling for lightweight data-race detection[C]∥Proc of PLDI’09, 2009:134-143.

[11] Flanagan C, Freund S N. FastTrack:Efficient and precise dynamic race detection[C]∥Proc of PLDI’09, 2009:121-133.

[12] Dutertre B, De Moura L. A fast linear-arithmetic solver for DPLL(T)[M]∥Computer Aided Verification, Berlin Heidelberg: Springer,2006:81-94.

[13] Lattner C, Adve V. LLVM:A compilation framework for lifelong program analysis & transformation[C]∥Proc of TACAS’08, 2008:75-86.

[14] Cordeiro L,Fischer B.Verifying multi-threaded software using SMT-based context-bounded model checking[C]∥Proc of ICSE’11, 2011:331-340.

[15] Gupta A,Popeea C,Rybalchenko A.Threader:A constraint-based verifier for multi-threaded programs[M]∥Computer Aided Verification, Berlin Heidelberg:Springer, 2011:412-417.

[16] Engler D,Ashcraft K.RacerX:Effective,static detection of race conditions and deadlocks[C]∥Proc of SOSP’03, 2003:237-252.

[17] Von Praun C, Gross T R. Object race detection[C]∥Proc of OOPSLA’01, 2001:70-82.

[18] Wang C, Limaye R, Ganai M, et al. Trace-based symbolic analysis for atomicity violations[M]∥Tools and Algorithms for the Construction and Analysis of Systems, Berlin:Springer, 2010:328-342.

[19] Wang C, Kundu S, Limaye R, et al. Symbolic predictive analysis for concurrent programs[J]. Formal Aspects of Computing,2011,23(6):781-805.

[20] Said M, Wang C, Yang Z, et al. Generating data race witnesses by an SMT-based analysis[C]∥Proc of NASA Formal Methods, 2011:313-327.

ZHANGXiao-dong,born in 1990,PhD candidate,CCF member(E200034811G)，his research interest includes program analysis.

Adataracedetectionandwitnessgenerationmethodformultithreadedprograms

ZHANG Xiao-dong1，ZHENG Qing-hua1，LIU Ting1，YU Le-chen1，LIU Pei1，YANG Zi-jiang2

(1.MOE Key Laboratory for Intelligent Networks and Network Security,Xi’an Jiaotong University,Xi’an 710049;2.School of Computer Science and Engineering,Xi’an University of Technology,Xi’an 710049,China)

Data race is a common problem in multithreaded programs. Due to the state explosion of thread interleaving, it is difficult to accurately detect bugs triggered by data races. Moreover, it is hard to replay and triage such bugs because of the facts that thread scheduling is difficult to control and the number of interleaving is astronomically large. A data race detection and witness generation method for multithreaded programs is proposed. A semantic model is designed to encode the execution path and the condition of data races as first-order logic formula. The satisfiability of the formula, solvable by constraint solvers, indicates the existence of data races under multiple thread interleavings without requiring repeated executions. The solutions produced by an SMT solver serve as witnesses to localize and verify data races. In the experiments, we compare existing tools threadsanitizer and helgrind with ours to detect the data races for 10 multithreaded programs. It is shown that our method can detect 287.5% and 264.7% more bugs respectively without false alarm, while the false alarm positive rate of threadsanitizer and helgrind are 10.5% and 9.8%.

multithreaded program testing;data race;constraint solving;witness generation

1007-130X(2014)11-2047-0

2014-06-06;

：2014-08-31

國家自然科學基金資助項目(91118005,91218301,61221063,61203174)；國家863計劃資助項目(2012AA011003)；國家科技支撐計劃(2012BAH16F02)；教育部創(chuàng)新團隊資助項目(IRT13035)；中央高?；究蒲袠I(yè)務費專項資金資助項目

TP311

：A

10.3969/j.issn.1007-130X.2014.11.001

張曉東(1990),男,河南民權人，博士生，CCF會員(E200034811G)，研究方向為程序分析。E-mail:xdzhang@sei.xjtu.edu.cn

通信地址：710049 陜西省西安市西安交通大學智能網(wǎng)絡與網(wǎng)絡安全教育部重點實驗室

Address:MOE Key Laboratory for Intelligent Networks and Network Security,Xi’an Jiaotong University,Xi’an 710049,Shaanxi,P.R.China