低級并行代碼中幾種同步機制的驗證.pdf

1、多核多處理器等以共享存儲為特征的新一代系統(tǒng)結(jié)構(gòu)的出現(xiàn)，加速了對快速研發(fā)基于共享資源的并行軟件的需求，這給基于共享資源的高可信并行軟件構(gòu)造帶來許多挑戰(zhàn)性研究課題。在基于共享資源的并行軟件構(gòu)造中，線程間的交互和通信主要通過訪問共享資源來實現(xiàn)，對共享資源訪問的同步控制是保證并行程序正確執(zhí)行的關(guān)鍵所在。
　　 目前用于共享變量的訪問控制的同步機制主要有鎖和事務(wù)內(nèi)存兩種。傳統(tǒng)的同步機制通過鎖保護的臨界區(qū)來管理并行程序中的共享資源的并發(fā)存取

2、，使用鎖的方式不僅限制了程序在多核處理器上的執(zhí)行效率，而且容易出現(xiàn)死鎖等導(dǎo)致程序進入異常執(zhí)行狀態(tài)的隱患。讀寫鎖和可重入鎖是鎖同步機制的優(yōu)化實現(xiàn)，其中讀寫鎖允許多個線程對共享數(shù)據(jù)進行并發(fā)只讀訪問，而可重入鎖則通過允許線程再次獲得所持有的鎖來避免自死鎖。事務(wù)內(nèi)存是近年來為發(fā)揮多核多處理等系統(tǒng)結(jié)構(gòu)的優(yōu)勢而開展的新型同步技術(shù)研究，它試圖通過允許一組存取共享內(nèi)存的指令(稱為事務(wù))原子且隔離地執(zhí)行來簡化并行編程。
　　 本課題小組的研究方向

3、是驗證使用多種同步機制的并行程序正確性，本論文則重點關(guān)注如何驗證使用讀寫鎖和可重入鎖這兩種同步機制的低級并行代碼的正確性，并探討同時使用鎖和事務(wù)內(nèi)存混合同步機制的并行程序的形式化驗證方法。已有的形式化驗證框架及程序邏輯在推理使用鎖的并行程序的正確性時，多數(shù)只考慮語義簡單的不可重入互斥鎖，而不考慮讀寫鎖和可重入鎖，這些優(yōu)化同步機制無疑可以提高并行程序的性能和易編程性，但由于其語義復(fù)雜，導(dǎo)致現(xiàn)有邏輯系統(tǒng)不能直接應(yīng)用于推理它們。另外，鎖和事務(wù)

4、內(nèi)存同步機制都有各自的優(yōu)缺點，未來高性能并行軟件可能需要同時使用它們而獲得最大的性能收益，相應(yīng)的高可信軟件則要求設(shè)計程序邏輯保證同時使用它們的并行程序的正確性，而設(shè)計一種同時反映鎖和事務(wù)內(nèi)存同步機制特征的中間語言是推理混合同步機制的前提，而目前很少有研究工作考慮同時支持鎖和事務(wù)內(nèi)存同步機制的編程語言和程序邏輯的設(shè)計。
　　 針對鎖和事務(wù)內(nèi)存同步機制的研究現(xiàn)狀以及已有程序驗證方面的成果，本文的主要工作分為以下兩個方面：
　　

5、 一方面，在匯編語言級通過擴展邵中教授等提出的并發(fā)的經(jīng)過證明的匯編編程(CCAP)驗證框架，設(shè)計支持使用讀寫鎖和可重入鎖同步機制的并行程序正確性驗證的Hoare風(fēng)格專用程序邏輯，達到構(gòu)造攜帶基礎(chǔ)證明的程序(FPCC)的目標。我們選擇模塊性較好且適合于推理互斥臨界區(qū)的并發(fā)分離邏輯作為所提出的驗證框架的基礎(chǔ)邏輯，并針對其在推理驗證讀寫鎖和可重入鎖時的局限性分別進行了如下擴展：
　　 ●通過擴展并發(fā)分離邏輯來支持以讀寫鎖為基本同步原

6、語的并行程序的推理，將并發(fā)分離邏輯中的分離擴展為“強分離”和“弱分離”兩類，利用表示資源不相交的強分離描述寫-寫和讀-寫線程間對共享資源的劃分，利用允許資源相交的弱分離描述讀-讀線程間對共享資源的劃分，從而彌補并發(fā)分離邏輯中要求共享資源在多個并行線程間進行不相交的劃分的不足。
　　 ●在并發(fā)分離邏輯的基礎(chǔ)上設(shè)計一種推理規(guī)則同時支持推理線程首次獲得鎖和再次獲得鎖的情況，避免資源被線程重復(fù)獲得，從而使得并發(fā)分離邏輯能正確推理使用可重

7、入鎖的并行程序。我們用Coq定理證明輔助工具實現(xiàn)了所提出的驗證框架及其可靠性證明，從而將驗證框架中的驗證推理系統(tǒng)從受信任計算基礎(chǔ)中排除出去，使得本文的驗證框架具有更高的可靠性。
　　 另一方面，提出一種新穎的語言構(gòu)造“rev{C}”用于描述與事務(wù)內(nèi)存實現(xiàn)特點密切相關(guān)的可逆代碼塊，得到一種中間語言將鎖和事務(wù)融合在一個統(tǒng)一的編程模型中，并討論了驗證可逆代碼塊的困難及方法，為進一步深入研究可逆代碼塊的推理驗證打下基礎(chǔ)。通過實例說明該語