發(fā)布時(shí)間：2021-03-08 10:35

　　多核處理器已經(jīng)成為目前主流的處理器,相應(yīng)的多線程并發(fā)編程也成為了目前主流的編程。多線程并發(fā)程序在充分利用多核處理器帶來的高運(yùn)行效率的同時(shí),相比于串行程序也帶來了更多線程交錯(cuò)的不確定性。線程的交錯(cuò)執(zhí)行讓程序員對并發(fā)程序的理解更加困難,使并發(fā)程序存在著比串行程序更多的錯(cuò)誤和缺陷。因此,并發(fā)程序的正確性成為了研究熱點(diǎn),而對并發(fā)程序正確性的驗(yàn)證,也成為了當(dāng)下程序驗(yàn)證領(lǐng)域的熱門話題。并發(fā)程序正確性的驗(yàn)證工作非常困難,其中一個(gè)嚴(yán)重的阻礙在于:并發(fā)程序的線程交互具有不確定性,可能的交錯(cuò)執(zhí)行順序隨著程序長度幾乎呈指數(shù)級的增長。為了減少對并發(fā)程序推理的難度,本文考慮在非搶占語義下研究并發(fā)程序的行為。非搶占語義下,只有當(dāng)線程主動(dòng)讓出執(zhí)行權(quán),其他線程才能開始執(zhí)行。這樣將線程交互限制在特定程序點(diǎn),大大降低了需要考慮的執(zhí)行過程的數(shù)量,簡化了驗(yàn)證過程。本文對無數(shù)據(jù)競爭并發(fā)程序在非搶占語義和搶占語義下的等價(jià)性進(jìn)行研究,通過對非搶占語義定義的討論,提出了形式化定義的非搶占語義,并嚴(yán)格證明了對于無數(shù)據(jù)競爭的并發(fā)程序,它進(jìn)行非搶占執(zhí)行和搶占執(zhí)行將得到一樣的結(jié)果。具體地說,本文的主要貢獻(xiàn)有以下幾點(diǎn):·我們提出了一種簡單的并... 

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

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

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

【文章目錄】：
摘要
ABSTRACT
第1章 緒論
    1.1 研究背景與研究意義
        1.1.1 軟件正確性與形式化驗(yàn)證
        1.1.2 并發(fā)程序驗(yàn)證與非搶占語義
    1.2 相關(guān)研究概況
    1.3 本文貢獻(xiàn)與結(jié)構(gòu)
第2章 背景知識(shí)介紹
    2.1 數(shù)據(jù)競爭
    2.2 精化關(guān)系與程序驗(yàn)證
    2.3 非搶占語義
第3章 并發(fā)程序語法及語義
    3.1 程序語法
    3.2 帶內(nèi)存印跡的線程執(zhí)行語義
    3.3 全局執(zhí)行語義
    3.4 多步執(zhí)行的定義
    3.5 事件路徑和程序行為
    3.6 數(shù)據(jù)競爭的定義
第4章 非搶占語義
    4.1 對非搶占語義的討論
    4.2 非搶占語義的具體定義
    4.3 多步執(zhí)行與事件路徑的定義
    4.4 非搶占語義下數(shù)據(jù)競爭的定義
    4.5 本章小結(jié)
第5章 非搶占語義和搶占語義的等價(jià)性
    5.1 無沖突的線程交換過程
    5.2 內(nèi)存印跡沖突與數(shù)據(jù)競爭
    5.3 事件路徑的一致性
    5.4 無數(shù)據(jù)競爭的等價(jià)性
    5.5 本章小結(jié)
第6章 語義等價(jià)性在編譯驗(yàn)證中的應(yīng)用
    6.1 編譯器的正確性
    6.2 實(shí)際驗(yàn)證工作
    6.3 證明工作量
第7章 結(jié)論
參考文獻(xiàn)
致謝
在讀期間發(fā)表的學(xué)術(shù)論文與取得的研究成果



本文編號(hào)：3070907