發(fā)布時間：2021-05-16 02:51

　　多核多處理器等以共享存儲為特征的新一代系統(tǒng)結(jié)構(gòu)的出現(xiàn),加速了對快速研發(fā)基于共享資源的并行軟件的需求,這給基于共享資源的高可信并行軟件構(gòu)造帶來許多挑戰(zhàn)性研究課題。在基于共享資源的并行軟件構(gòu)造中,線程間的交互和通信主要通過訪問共享資源來實現(xiàn),對共享資源訪問的同步控制是保證并行程序正確執(zhí)行的關(guān)鍵所在。目前用于共享變量的訪問控制的同步機制主要有鎖和事務(wù)內(nèi)存兩種。傳統(tǒng)的同步機制通過鎖保護(hù)的臨界區(qū)來管理并行程序中的共享資源的并發(fā)存取,使用鎖的方式不僅限制了程序在多核處理器上的執(zhí)行效率,而且容易出現(xiàn)死鎖等導(dǎo)致程序進(jìn)入異常執(zhí)行狀態(tài)的隱患。讀寫鎖和可重入鎖是鎖同步機制的優(yōu)化實現(xiàn),其中讀寫鎖允許多個線程對共享數(shù)據(jù)進(jìn)行并發(fā)只讀訪問,而可重入鎖則通過允許線程再次獲得所持有的鎖來避免自死鎖。事務(wù)內(nèi)存是近年來為發(fā)揮多核多處理等系統(tǒng)結(jié)構(gòu)的優(yōu)勢而開展的新型同步技術(shù)研究,它試圖通過允許一組存取共享內(nèi)存的指令（稱為事務(wù)）原子且隔離地執(zhí)行來簡化并行編程。本課題小組的研究方向是驗證使用多種同步機制的并行程序正確性,本論文則重點關(guān)注如何驗證使用讀寫鎖和可重入鎖這兩種同步機制的低級并行代碼的正確性,并探討同時使用鎖和事務(wù)內(nèi)存混合... 

【文章來源】：中國科學(xué)技術(shù)大學(xué)安徽省 211工程院校 985工程院校

【文章頁數(shù)】：124 頁

【學(xué)位級別】：博士

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景及相關(guān)工作
        1.1.1 同步機制
        1.1.2 并行程序正確性驗證
    1.2 存在的問題
    1.3 本文的主要工作及貢獻(xiàn)
    1.4 章節(jié)安排
第二章 相關(guān)理論與技術(shù)基礎(chǔ)
    2.1 程序正確性檢測方法
    2.2 攜帶證明的代碼(PCC)
    2.3 同步技術(shù)基礎(chǔ)
        2.3.1 基本概念
        2.3.2 各種同步機制的實現(xiàn)
    2.4 并行程序驗證技術(shù)
        2.4.1 不變式證明技術(shù)
        2.4.2 Rely-Guarantee推理
        2.4.3 分離邏輯
        2.4.4 并發(fā)分離邏輯(CSL)
        2.4.5 結(jié)合R-G推理和分離邏輯(RGsep和SAGL)
        2.4.6 局部R-G推理(LRG)
        2.4.7 分析比較
    2.5 CCAP驗證框架
        2.5.1 元邏輯
        2.5.2 抽象機器
        2.5.3 目標(biāo)程序性質(zhì)的證明框架
        2.5.4 驗證框架構(gòu)造步驟
    2.6 本章小結(jié)
第三章 使用讀寫鎖的并行程序驗證
    3.1 問題描述
        3.1.1 CSL的局限性
    3.2 所有權(quán)轉(zhuǎn)移推理方法
    3.3 抽象機器
    3.4 擴展并發(fā)分離邏輯
    3.5 目標(biāo)程序性質(zhì)的證明框架
        3.5.1 斷言語言和規(guī)范語言的語法
        3.5.2 推理規(guī)則
        3.5.3 可靠性定理
    3.6 目標(biāo)代碼驗證舉例
    3.7 本章小結(jié)
第四章 使用可重入鎖的并行程序驗證
    4.1 問題描述
    4.2 抽象機器
    4.3 目標(biāo)程序性質(zhì)的證明框架
        4.3.1 斷言語言和規(guī)范語言的語法
        4.3.2 推理規(guī)則
        4.3.3 可靠性定理
    4.4 目標(biāo)代碼驗證舉例
    4.5 本章小結(jié)
第五章 驗證框架的Coq實現(xiàn)
    5.1 抽象機器在Coq中的描述
        5.1.1 機器語法定義
        5.1.2 機器操作語義定義
    5.2 程序規(guī)范在Coq中的描述
    5.3 強弱分離在Coq中的描述
    5.4 推理規(guī)則在Coq中的描述
    5.5 框架可靠性證明
    5.6 本章小結(jié)
第六章 使用混合同步控制機制的并行程序驗證
    6.1 問題描述
    6.2 支持可逆代碼塊的并行語言
        6.2.1 可逆代碼塊"rev{C}"
        6.2.2 語法
        6.2.3 程序?qū)嵗?br>    6.3 驗證可逆代碼塊中的問題
        6.3.1 操作語義
        6.3.2 推理規(guī)則
    6.4 本章小結(jié)
第七章 結(jié)束語
    7.1 論文工作總結(jié)
    7.2 進(jìn)一步的工作
參考文獻(xiàn)
致謝
在讀期間發(fā)表的學(xué)術(shù)論文與取得的研究成果


【參考文獻(xiàn)】：
期刊論文
[1]Certifying Concurrent Programs Using Transactional Memory[J]. 李隆,張昱,陳意云,李勇.  Journal of Computer Science & Technology. 2009(01)
[2]“可信軟件基礎(chǔ)研究”重大研究計劃綜述[J]. 劉克,單志廣,王戟,何積豐,張兆田,秦玉文.  中國科學(xué)基金. 2008(03)
[3]高可信軟件工程技術(shù)[J]. 陳火旺,王戟,董威.  電子學(xué)報. 2003(S1)
[4]模型檢測:理論、方法與應(yīng)用[J]. 林惠民,張文輝.  電子學(xué)報. 2002(S1)
[5]并發(fā)程序驗證的時序Petri網(wǎng)方法[J]. 丁志軍,蔣昌俊.  計算機學(xué)報. 2002(05)
[6]PVM并行程序驗證系統(tǒng)的原理與實現(xiàn)[J]. 張兆慶,蔣昌俊,喬如良,葉志寶,周杰.  計算機學(xué)報. 1999(04)



本文編號：3188825