低級(jí)并行代碼中幾種同步機(jī)制的驗(yàn)證.pdf

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

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

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

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

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

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

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