本文關(guān)鍵詞：多線程程序中關(guān)聯(lián)變量原子性驗證關(guān)鍵技術(shù)研究

  更多相關(guān)文章： 關(guān)聯(lián)變量 原子性驗證 多線程程序序符號執(zhí)行 一般圖可達性 指針別名分析 并行干擾插值

【摘要】：多線程程序中關(guān)聯(lián)變量的原子性是指在共享內(nèi)存的并行模型中,保證具有一定關(guān)聯(lián)關(guān)系的共享變量集合,在任意的并行執(zhí)行順序訪問條件下,其所滿足的關(guān)聯(lián)關(guān)系仍然成立的一種性質(zhì)。該性質(zhì)是多線程程序設計過程必須滿足的約束之一,是保證多線程程序安全性的核心因素,是并行程序安全運行的重要前提。同時,隨著多核硬件環(huán)境的日益普及,越來越多的軟件通過并行化充分利用已有的計算資源以提高軟件系統(tǒng)的性能,尤其在航天、武器和醫(yī)療等安全攸關(guān)領(lǐng)域有著廣泛的應用。因此,驗證并行程序中關(guān)聯(lián)變量原子性的研究對保障并行程序的質(zhì)量安全具有重要意義。本文主要對驗證條件和驗證過程所涉及的關(guān)鍵技術(shù)進行研究,首先研究驗證條件的確定問題即確認驗證目標,本文主要是要確定保持原子性的關(guān)聯(lián)變量集合,重點解決原子性關(guān)聯(lián)變量和一般關(guān)聯(lián)變量混淆的問題。其次,研究如何判斷程序是否滿足驗證條件即驗證過程的問題,本文采取根據(jù)程序可達狀態(tài)來進行判斷的策略,先從決定程序可達狀態(tài)的控制依賴和數(shù)據(jù)依賴角度出發(fā),分別研究了面向變量訪問次序判別的圖可達性問題和指針別名分析問題,然后在此基礎上研究了可達狀態(tài)約策略問題。在圖可達性問題中,具體解決非樹邊傳遞閉包計算問題、環(huán)子圖查詢和非結(jié)構(gòu)化區(qū)域解析問題。在別名分析問題中,具體解決按需策略下分析精度不足的問題。在可達狀態(tài)約簡策略問題中,重點改善了并行程序可達狀態(tài)粒度過粗導致約簡效率低的問題,提出了并行干擾插值結(jié)構(gòu)和基于此的并行程序符號執(zhí)行算法,重點提高可達程序狀態(tài)間通過蘊含關(guān)系合并的可能性并完善輪詢語句完備性分析,進而實現(xiàn)對多線程程序原子性的高效驗證。首先,對于關(guān)聯(lián)變量提取問題,在驗證條件中的關(guān)聯(lián)變量挖掘與提取方面,針對現(xiàn)有面向原子性驗證的關(guān)聯(lián)變量提取方法誤報率高的問題,提出了基于程序依賴圖約簡的關(guān)聯(lián)變量挖掘與提取算法。通過簡化程序控制依賴圖中控制流圖信息來泛化變量間非依賴性順序的關(guān)聯(lián)關(guān)系,然后利用頻繁子圖挖掘算法挖掘關(guān)聯(lián)變量候選集合,最終通過過濾策略提取需要保持原子性的關(guān)聯(lián)變量集合。實驗中經(jīng)人工確認,與現(xiàn)有基于頻繁項挖掘的提取方法相比,該方法具有更低的關(guān)聯(lián)變量誤報率。然后,在驗證階段的控制流圖可達性判斷研究方面:(1)對于一般圖可達性分析,針對一般圖可達性算法缺少對程序控制流圖中非樹邊和循環(huán)體內(nèi)有向環(huán)子圖的優(yōu)化與處理問題,提出了一種層次線性化編碼索引模式,利用控制流圖中區(qū)域結(jié)構(gòu)所隱含的層次順序關(guān)系,建立表達多重從屬關(guān)系的可達性索引。該編碼不僅能夠避免計算有向圖非生成樹邊的可達性傳遞閉包,而且整合了程序控制流圖中有向環(huán)子圖的編碼與圖可達性判斷,進而提高可達性判斷效率。(2)對于指針別名分析問題,針對當前程序控制流圖結(jié)構(gòu)化方法難以滿足程序分析的流敏感精度要求的問題,提出了程序控制流圖的虛擬區(qū)域結(jié)構(gòu)。通過分析匹配分支節(jié)點列表和結(jié)構(gòu)化區(qū)域的對應關(guān)系,提出了一種非結(jié)構(gòu)化區(qū)域內(nèi)虛擬區(qū)域的構(gòu)造方法,該方法根據(jù)未匹配分支節(jié)點列表沖突來增加虛擬匯聚結(jié)點,進而構(gòu)造非結(jié)構(gòu)化區(qū)域內(nèi)虛擬區(qū)域。該方法不僅能夠恢復非結(jié)構(gòu)區(qū)域內(nèi)隱含的區(qū)域結(jié)構(gòu),而且還保留了非結(jié)構(gòu)化區(qū)域中原有各語句間的相對位置關(guān)系,提高了結(jié)構(gòu)化方法的流敏感分析精度。其次,在驗證階段的指針別名分析方面,針對當前基于上下文無關(guān)文法的按需別名分析方法只具有流不敏感精度的問題,提出了流敏感精度的按需別名分析算法,將別名關(guān)系查詢問題統(tǒng)一轉(zhuǎn)換為對特定變量賦值實例在控制流可達條件下賦值路徑的搜索問題,以實現(xiàn)流敏感的按需別名分析。實驗表明,與流不敏感的按需別名分析相比,該方法可以在保證查詢效率的前提下,有效提高按需別名分析的精度。最后,在并行程序可達狀態(tài)計算方面,針對當前基于干擾的有界模型檢測中限制搜索蹤跡長度導致的不完備性問題和嚴重的計算負擔問題,提出了面向多線程程序原子性驗證的符號執(zhí)行方法,該方法以約束邏輯程序為實現(xiàn)基礎,利用并行干擾插值結(jié)構(gòu)對多線程程序可達狀態(tài)空間進行搜索。該結(jié)構(gòu)對全局線程間調(diào)度進行過估計(Over-Approximate)、局部線程內(nèi)不可行蹤跡泛化、并行可達狀態(tài)泛化三個層次遞進的對并行線程間的交疊執(zhí)行狀態(tài)進行抽象,實現(xiàn)了快速的狀態(tài)空間約簡,緩解了處理循環(huán)體時對代表性蹤跡的完全展開導致的嚴重計算負擔問題,同時保證了并行驗證的完備性。上述方法的提出,有效解決了多線程程序中關(guān)聯(lián)變量原子性驗證中的關(guān)鍵問題,為提高并行程序安全性驗證的自動化程度、效率和準確性,以及提高并行軟件質(zhì)量奠定了理論基礎。
【關(guān)鍵詞】：關(guān)聯(lián)變量 原子性驗證 多線程程序序符號執(zhí)行 一般圖可達性 指針別名分析 并行干擾插值
【學位授予單位】：哈爾濱工業(yè)大學
【學位級別】：博士
【學位授予年份】：2015
【分類號】：TP391.41
【目錄】：

• 摘要4-6
• Abstract6-15
• 第1章 緒論15-33
• 1.1 課題來源15
• 1.2 課題背景及研究的目的和意義15-17
• 1.3 國內(nèi)外的研究現(xiàn)狀及分析17-29
• 1.3.1 關(guān)聯(lián)變量挖掘研究現(xiàn)狀分析17-19
• 1.3.2 控制流圖分析研究現(xiàn)狀分析19-23
• 1.3.3 指針分析研究現(xiàn)狀分析23-25
• 1.3.4 并行程序原子性違背缺陷檢測及驗證研究現(xiàn)狀分析25-29
• 1.4 主要研究內(nèi)容29-33
• 第2章 多線程程序中關(guān)聯(lián)變量挖掘與提取33-54
• 2.1 引言33-34
• 2.2 支持多程序語言的靜態(tài)信息提取方法34-40
• 2.2.1 與靜態(tài)信息提取相關(guān)的GCC源代碼分析34-35
• 2.2.2 靜態(tài)信息提取35-39
• 2.2.3 實驗結(jié)果與分析39-40
• 2.3 保持原子性的多線程關(guān)聯(lián)變量的特點分析40-43
• 2.3.1 關(guān)聯(lián)變量語義分析40-41
• 2.3.2 關(guān)聯(lián)變量行為分析41-43
• 2.4 基于程序依賴圖的關(guān)聯(lián)變量挖掘與提取43-48
• 2.4.1 原子性關(guān)聯(lián)變量集合的關(guān)聯(lián)關(guān)系分析43-44
• 2.4.2 挖掘算法概要44
• 2.4.3 約簡的程序依賴圖44-45
• 2.4.4 程序依賴圖預處理45-46
• 2.4.5 頻繁子圖挖掘46-47
• 2.4.6 多線程關(guān)聯(lián)變量提取與過濾47-48
• 2.5 實驗及分析48-53
• 2.6 本章小結(jié)53-54
• 第3章 面向變量訪問次序判別的圖可達性分析54-100
• 3.1 引言54-55
• 3.2 結(jié)構(gòu)化控制流圖可達性分析55-77
• 3.2.1 層次線性化編碼域56-62
• 3.2.2 層次線性化編碼規(guī)則62-67
• 3.2.3 基于LLC的CFG可達性判斷67-73
• 3.2.4 實驗與分析73-77
• 3.3 非結(jié)構(gòu)化控制流圖的虛擬區(qū)域77-99
• 3.3.1 結(jié)構(gòu)化區(qū)域的分析80-86
• 3.3.2 虛擬分支 -會合節(jié)點匹配對的恢復算法86-92
• 3.3.3 虛擬區(qū)域在非結(jié)構(gòu)化區(qū)域圖可達性應用92-96
• 3.3.4 實驗與分析96-99
• 3.4 本章小結(jié)99-100
• 第4章 流敏感精度的按需指針別名分析100-115
• 4.1 引言100-101
• 4.2 流敏感對別名分析精度的影響分析101-103
• 4.2.1 按需別名分析101-102
• 4.2.2 流敏感信息的表達102-103
• 4.3 流敏感信息的按需查詢103-104
• 4.4 賦值流圖104-106
• 4.5 賦值流搜索106-109
• 4.6 流敏感按需別名分析算法109-111
• 4.7 實驗與分析111-114
• 4.7.1 流敏感精度的按需別名分析與指向分析方法對比111
• 4.7.2 按需別名分析的流敏感精度方法與流不敏感精度方法對比111-112
• 4.7.3 按需流敏感別名分析中搜索邊數(shù)統(tǒng)計與分析112-114
• 4.8 本章小結(jié)114-115
• 第5章 基于并行干擾插值的多線程程序原子性驗證115-139
• 5.1 引言115-117
• 5.2 相關(guān)概念117-119
• 5.2.1 程序執(zhí)行順序117-118
• 5.2.2 程序執(zhí)行蹤跡的操作語義118-119
• 5.2.3 克雷格插值119
• 5.3 并行程序的符號分析119-121
• 5.3.1 并行干擾與調(diào)度120
• 5.3.2 并行執(zhí)行順序的約束120
• 5.3.3 并行變遷的推導樹120-121
• 5.4 并行干擾插值121-133
• 5.4.1 執(zhí)行順序偏序關(guān)系插值121-124
• 5.4.2 調(diào)度插值124-129
• 5.4.3 并行狀態(tài)插值129-133
• 5.5 算法描述133-135
• 5.6 實驗與分析135-137
• 5.7 本章小結(jié)137-139
• 結(jié)論139-141
• 參考文獻141-152
• 攻讀博士學位期間發(fā)表的學術(shù)論文152-154
• 致謝154-155
• 個人簡歷155

，

本文編號：592490