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

申請號：	201410320943.2	申請日：	2014-07-07
公開（公告）號：	CN104077144A	公開（公告）日：	2014-10-01
發明（設計）人：	劉烴;張曉東;俞樂晨;劉沛;鄭慶華	申請（專利權）人：	西安交通大學
主分類號：	G06F9/44	分類號：	G06F9/44
代理公司：	西安智大知識產權代理事務所 61215	代理人：	段俊濤
地址：	710049***	國省代碼：	陜西;61
權利要求書：	查看更多	說明書：	查看更多
摘要：
搜索關鍵詞：	基于多線程程序約束構建數據競爭檢測證據生成方法
鉆瓜網技術展會專利詞庫專利權人專利榜在售專利公布日期熱門專利

【說明書】：

技術領域

本發明涉及可信軟件及軟件測試領域，特別涉及一種基于多線程程序約束構建的數據競爭檢測與證據生成方法。

背景技術

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

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

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

發明內容

為了克服上述現有技術的缺點，本發明的目的在于提供一種基于多線程程序約束構建的數據競爭檢測與證據生成方法，根據多線程程序語義構建約束表達式，將數據競爭檢測問題轉化為約束求解問題，采用約束求解器檢測可能存在的數據競爭，并生成觸發數據競爭的程序執行路徑。

為了實現上述目的，本發明采用的技術方案是：

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

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

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

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

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

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

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

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

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