1、多線程程序中關聯變量的原子性是指在共享內存的并行模型中，保證具有一定關聯關系的共享變量集合，在任意的并行執(zhí)行順序訪問條件下，其所滿足的關聯關系仍然成立的一種性質。該性質是多線程程序設計過程必須滿足的約束之一，是保證多線程程序安全性的核心因素，是并行程序安全運行的重要前提。同時，隨著多核硬件環(huán)境的日益普及，越來越多的軟件通過并行化充分利用已有的計算資源以提高軟件系統的性能，尤其在航天、武器和醫(yī)療等安全攸關領域有著廣泛的應用。因此，驗證并行

2、程序中關聯變量原子性的研究對保障并行程序的質量安全具有重要意義。
　　本文主要對驗證條件和驗證過程所涉及的關鍵技術進行研究，首先研究驗證條件的確定問題即確認驗證目標，本文主要是要確定保持原子性的關聯變量集合，重點解決原子性關聯變量和一般關聯變量混淆的問題。其次，研究如何判斷程序是否滿足驗證條件即驗證過程的問題，本文采取根據程序可達狀態(tài)來進行判斷的策略，先從決定程序可達狀態(tài)的控制依賴和數據依賴角度出發(fā)，分別研究了面向變量訪問次序判別

3、的圖可達性問題和指針別名分析問題，然后在此基礎上研究了可達狀態(tài)約策略問題。在圖可達性問題中，具體解決非樹邊傳遞閉包計算問題、環(huán)子圖查詢和非結構化區(qū)域解析問題。在別名分析問題中，具體解決按需策略下分析精度不足的問題。在可達狀態(tài)約簡策略問題中，重點改善了并行程序可達狀態(tài)粒度過粗導致約簡效率低的問題，提出了并行干擾插值結構和基于此的并行程序符號執(zhí)行算法，重點提高可達程序狀態(tài)間通過蘊含關系合并的可能性并完善輪詢語句完備性分析，進而實現對多線程程

4、序原子性的高效驗證。
　　首先，對于關聯變量提取問題，在驗證條件中的關聯變量挖掘與提取方面，針對現有面向原子性驗證的關聯變量提取方法誤報率高的問題，提出了基于程序依賴圖約簡的關聯變量挖掘與提取算法。通過簡化程序控制依賴圖中控制流圖信息來泛化變量間非依賴性順序的關聯關系，然后利用頻繁子圖挖掘算法挖掘關聯變量候選集合，最終通過過濾策略提取需要保持原子性的關聯變量集合。實驗中經人工確認，與現有基于頻繁項挖掘的提取方法相比，該方法具有更低

5、的關聯變量誤報率。
　　然后，在驗證階段的控制流圖可達性判斷研究方面：
　　(1)對于一般圖可達性分析，針對一般圖可達性算法缺少對程序控制流圖中非樹邊和循環(huán)體內有向環(huán)子圖的優(yōu)化與處理問題，提出了一種層次線性化編碼索引模式，利用控制流圖中區(qū)域結構所隱含的層次順序關系，建立表達多重從屬關系的可達性索引。該編碼不僅能夠避免計算有向圖非生成樹邊的可達性傳遞閉包，而且整合了程序控制流圖中有向環(huán)子圖的編碼與圖可達性判斷，進而提高可達性判

6、斷效率。
　　(2)對于指針別名分析問題，針對當前程序控制流圖結構化方法難以滿足程序分析的流敏感精度要求的問題，提出了程序控制流圖的虛擬區(qū)域結構。通過分析匹配分支節(jié)點列表和結構化區(qū)域的對應關系，提出了一種非結構化區(qū)域內虛擬區(qū)域的構造方法，該方法根據未匹配分支節(jié)點列表沖突來增加虛擬匯聚結點，進而構造非結構化區(qū)域內虛擬區(qū)域。該方法不僅能夠恢復非結構區(qū)域內隱含的區(qū)域結構，而且還保留了非結構化區(qū)域中原有各語句間的相對位置關系，提高了結構化

7、方法的流敏感分析精度。
　　其次，在驗證階段的指針別名分析方面，針對當前基于上下文無關文法的按需別名分析方法只具有流不敏感精度的問題，提出了流敏感精度的按需別名分析算法，將別名關系查詢問題統一轉換為對特定變量賦值實例在控制流可達條件下賦值路徑的搜索問題，以實現流敏感的按需別名分析。實驗表明，與流不敏感的按需別名分析相比，該方法可以在保證查詢效率的前提下，有效提高按需別名分析的精度。
　　最后，在并行程序可達狀態(tài)計算方面，針對

8、當前基于干擾的有界模型檢測中限制搜索蹤跡長度導致的不完備性問題和嚴重的計算負擔問題，提出了面向多線程程序原子性驗證的符號執(zhí)行方法，該方法以約束邏輯程序為實現基礎，利用并行干擾插值結構對多線程程序可達狀態(tài)空間進行搜索。該結構對全局線程間調度進行過估計(Over-Approximate)、局部線程內不可行蹤跡泛化、并行可達狀態(tài)泛化三個層次遞進的對并行線程間的交疊執(zhí)行狀態(tài)進行抽象，實現了快速的狀態(tài)空間約簡，緩解了處理循環(huán)體時對代表性蹤跡的完全