[發明專利]基于多線程程序約束構建的數據競爭檢測與證據生成方法

有效

• 申請號: 201410320943.2
• 申請日: 2014-07-07
• 公開（公告）號: CN104077144A
• 公開（公告）日: 2014-10-01
• 發明（設計）人: 劉烴;張曉東;俞樂晨;劉沛;鄭慶華
• 申請（專利權）人: 西安交通大學
• 主分類號: G06F9/44
• 分類號: G06F9/44
• 代理公司: 西安智大知識產權代理事務所 61215
• 代理人: 段俊濤

1.一種基于多線程程序約束構建的數據競爭檢測與證據生成方法，其特征在于，包括如下步驟：

S1)在給定輸入下，通過執行已插樁的待測程序以生成路徑記錄文件，且識別出執行路徑中公有變量的訪問點以便于約束構建；

S2)根據程序執行語義將執行路徑中狀態轉移、線程交織關系轉化為無量詞一階邏輯表達式，構建蘊含了所有可能的交織序列的多線程程序執行路徑約束模型F；

S3)將路徑中所有線程上可能發生數據競爭的兩點視為數據競爭候選，收集所有候選并構建數據競爭候選集合DRCS，同時根據數據競爭的定義構建每個候選的競爭發生條件ρ；

S4)針對每一個候選競爭發生條件ρ，利用約束求解器驗證F∧ρ是否有解；

S5)如果有解，則表示此競爭條件會觸發真實的數據競爭；如果無解，則表示此候選不會觸發數據競爭；

S6)當存在數據競爭時，輸出該數據競爭的證據序列；

S7)對于數據競爭候選集合DRCS，如果遍歷結束，則輸出所有結果；否則，繼續遍歷下一個競爭候選；

S8)驗證結束后，輸出檢測到的所有數據競爭以及對應的證據序列。

2.根據權利要求1所述基于多線程程序約束構建的數據競爭檢測與證據生成方法，其特征在于，所述步驟S1)中插樁工作并非在源碼或者二進制的層面上進行，而是在字節碼的層面上完成，具體實施方法為：首先將待測多線程程序源碼轉化為中間字節碼格式，即LLVM字節碼；然后將具有監控功能的語句植入待測程序；最后將植入監控代碼的字節碼鏈接成可執行程序。

3.根據權利要求1所述基于多線程程序約束構建的數據競爭檢測與證據生成方法，其特征在于，所述步驟S2)中多線程程序執行路徑約束模型F蘊含了執行路徑所有可能的交織序列，包括五種約束：路徑表達式、內存模型約束、讀寫關系約束、偏序約束以及同步語義約束，定義分別如下：

1)路徑表達式：描述線程內部的定義-使用鏈，以及控制線程內部狀態轉換；

2)內存模型約束：表示程序中語句、變量之間的關系，采用順序一致性的語義，順序一致性規定CPU按照代碼中語句的順序來執行程序；

3)讀寫關系約束：定義線程間的定義-使用鏈，規定共享變量所讀取到的值，必須來自初始值以及最近的寫值；

4)偏序約束：定義線程之間創建線程與終止線程操作語句于被操作線程語句之間的時序關系；

5)同步語義約束：定義線程之間同步控制操作語句之間的時序關系；

其中，定義-使用鏈為：將每一個線程序列轉化為SSA格式，對于每一個SSA格式的執行序列，除去共享訪問點都是一個完整的定義-使用鏈。

4.根據權利要求3所述基于多線程程序約束構建的數據競爭檢測與證據生成方法，其特征在于，所述步驟S2)中多線程程序執行路徑約束模型F的構建方法包括以下操作：

1)計算路徑表達式，以控制線程內部狀態轉移；

2)計算內存模型約束，以線程內限制語句之間的關系；

3)計算讀寫關系約束，以建立線程間的定義-使用鏈；

4)計算同步語義約束，以定義線程間同步關系；

5)計算偏序約束，以描述線程創建與終止的語義；

最后，結合以上五種約束，構成約束模型F。