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

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

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

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

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景及相關(guān)工作
        1.1.1 同步機(jī)制
        1.1.2 并行程序正確性驗(yàn)證
    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 各種同步機(jī)制的實(shí)現(xiàn)
    2.4 并行程序驗(yàn)證技術(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驗(yàn)證框架
        2.5.1 元邏輯
        2.5.2 抽象機(jī)器
        2.5.3 目標(biāo)程序性質(zhì)的證明框架
        2.5.4 驗(yàn)證框架構(gòu)造步驟
    2.6 本章小結(jié)
第三章 使用讀寫鎖的并行程序驗(yàn)證
    3.1 問題描述
        3.1.1 CSL的局限性
    3.2 所有權(quán)轉(zhuǎn)移推理方法
    3.3 抽象機(jī)器
    3.4 擴(kuò)展并發(fā)分離邏輯
    3.5 目標(biāo)程序性質(zhì)的證明框架
        3.5.1 斷言語言和規(guī)范語言的語法
        3.5.2 推理規(guī)則
        3.5.3 可靠性定理
    3.6 目標(biāo)代碼驗(yàn)證舉例
    3.7 本章小結(jié)
第四章 使用可重入鎖的并行程序驗(yàn)證
    4.1 問題描述
    4.2 抽象機(jī)器
    4.3 目標(biāo)程序性質(zhì)的證明框架
        4.3.1 斷言語言和規(guī)范語言的語法
        4.3.2 推理規(guī)則
        4.3.3 可靠性定理
    4.4 目標(biāo)代碼驗(yàn)證舉例
    4.5 本章小結(jié)
第五章 驗(yàn)證框架的Coq實(shí)現(xiàn)
    5.1 抽象機(jī)器在Coq中的描述
        5.1.1 機(jī)器語法定義
        5.1.2 機(jī)器操作語義定義
    5.2 程序規(guī)范在Coq中的描述
    5.3 強(qiáng)弱分離在Coq中的描述
    5.4 推理規(guī)則在Coq中的描述
    5.5 框架可靠性證明
    5.6 本章小結(jié)
第六章 使用混合同步控制機(jī)制的并行程序驗(yàn)證
    6.1 問題描述
    6.2 支持可逆代碼塊的并行語言
        6.2.1 可逆代碼塊"rev{C}"
        6.2.2 語法
        6.2.3 程序?qū)嵗?br>    6.3 驗(yàn)證可逆代碼塊中的問題
        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ì)劃綜述[J]. 劉克,單志廣,王戟,何積豐,張兆田,秦玉文.  中國科學(xué)基金. 2008(03)
[3]高可信軟件工程技術(shù)[J]. 陳火旺,王戟,董威.  電子學(xué)報. 2003(S1)
[4]模型檢測:理論、方法與應(yīng)用[J]. 林惠民,張文輝.  電子學(xué)報. 2002(S1)
[5]并發(fā)程序驗(yàn)證的時序Petri網(wǎng)方法[J]. 丁志軍,蔣昌俊.  計(jì)算機(jī)學(xué)報. 2002(05)
[6]PVM并行程序驗(yàn)證系統(tǒng)的原理與實(shí)現(xiàn)[J]. 張兆慶,蔣昌俊,喬如良,葉志寶,周杰.  計(jì)算機(jī)學(xué)報. 1999(04)



本文編號：3188825