多線程程序中關(guān)聯(lián)變量原子性驗(yàn)證關(guān)鍵技術(shù)研究.pdf

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

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

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

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

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

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

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

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