本文關(guān)鍵詞：基于操作語義的弱內(nèi)存模型描述及程序邏輯研究，由筆耕文化傳播整理發(fā)布。

【摘要】：程序語言的內(nèi)存模型規(guī)定了在程序執(zhí)行的過程中內(nèi)存訪問是如何發(fā)生的。它作為橋梁將為程序員和語言實現(xiàn)連接起來,幫助程序員寫出正確的并發(fā)程序。在現(xiàn)實世界中,大多數(shù)的硬件和編譯系統(tǒng)都是基于弱內(nèi)存模型的假設(shè),即內(nèi)存訪問并不是嚴(yán)格按照程序順序執(zhí)行,以用來支持各類優(yōu)化。本文研究了弱內(nèi)存模型的設(shè)計,并提出了可以支持在弱內(nèi)存模型上進行程序驗證的程序邏輯。具體來說,本文在弱內(nèi)存模型和程序邏輯方面做出了如下的貢獻： 首先,本文提出一種新的弱內(nèi)存模型OHMM,這是Happens-before內(nèi)存模型(HMM)的變種。這個模型通過對一個簡單語言賦予具體的操作語義,并通過它在抽象機上的程序行為來模擬HMM。由于OHMM所允許的程序行為是通過操作語義自然生成的,所以它自然而然的避免了所謂的憑空出現(xiàn)(out-of-thin-air)的程序行為。另外一方面,OHMM使用一種我們稱之為重放的機制來允許某些符合一定條件的指令在抽象機上能夠多次執(zhí)行,來模擬現(xiàn)實世界中編譯器和處理器優(yōu)化中的投機執(zhí)行和優(yōu)化。總的來說,我們的模型對于無鎖程序的約束會比Java內(nèi)存模型(JMM)更加弱一些,因此我們將會允許更多的編譯器優(yōu)化算法在我們的模型上能夠使用。同時,在OHMM上,程序行為在直觀上會比JMM更加自然。許多在JMM上可能出現(xiàn)但是明顯違反直觀認(rèn)識的程序,在我們的模型上就不再合法。我們希望OHMM可以成為可供類Java語言選擇的一種新內(nèi)存模型。 其次,本文提出一種新的用于驗證并發(fā)程序在TSO(Total Store Order)弱內(nèi)存模型下正確性的程序邏輯。TSO模型所允許的弱行為是OHMM的子集。我們知道,TSO模型已經(jīng)被用作X86和SPARC-TSO處理器族的模型基礎(chǔ),并且在一些高級語言中也正在被提案作為其內(nèi)存模型的基礎(chǔ)。我們的邏輯對LRG(Local Rely-Guarantee)進行擴展,對其加入了關(guān)于TSO寫緩存的斷言,這可以讓我們對TSO模型中對外部線程不可見的局部的寫緩存的狀態(tài)進行描述。如同LRG一樣,我們的程序邏輯支持對細(xì)粒度并發(fā)具有表達力強的rely/guarantee推理以及分離邏輯中的局部推理。同時,我們在邏輯上對TSO模型進行進一步抽象,把TSO共享內(nèi)存分為local和shared兩部分,這可以允許我們可以將那些在訪問時只有單個線程能夠訪問的內(nèi)存單元(邏輯上等同于local單元)的寫操作直接寫入內(nèi)存,不需要經(jīng)過寫緩存。我們使用這個邏輯證明了一些具有代表性的并發(fā)算法在TSO上的正確性,包括Peterson's lock算法,Simpson's four slot算法,concurrent GCD算法以及l(fā)ock的優(yōu)化實現(xiàn)算法。
【關(guān)鍵詞】：弱內(nèi)存模型 程序驗證 并發(fā) 程序邏輯
【學(xué)位授予單位】：中國科學(xué)技術(shù)大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2015
【分類號】：TP311.1
【目錄】：

• 摘要5-6
• ABSTRACT6-10
• 插圖索引10-12
• 主要符號對照表12-13
• 第一章 緒論13-23
• 1.1 弱內(nèi)存模型的設(shè)計15-17
• 1.2 運用于弱內(nèi)存模型的程序邏輯設(shè)計17-23
• 第二章 背景知識介紹23-31
• 2.1 順序一致性模型23-24
• 2.2 弱內(nèi)存模型24-28
• 2.2.1 TSO弱內(nèi)存模型24-25
• 2.2.2 Happens-Before弱內(nèi)存模型25-28
• 2.3 程序邏輯28-31
• 第三章 基于操作語義的Happens-Before弱內(nèi)存模型31-67
• 3.1 OHMM非形式化的描述32-42
• 3.1.1 OHMM語言32-33
• 3.1.2 OHMM抽象機33-35
• 3.1.3 事件執(zhí)行順序35-37
• 3.1.4 歷史記錄和內(nèi)存訪問37-39
• 3.1.5 重放事件39-42
• 3.2 OHMM形式化定義42-45
• 3.3 一些簡單的例子45-50
• 3.3.1 JMM中不允許但OHMM中允許46-48
• 3.3.2 OHMM中禁止JMM中違反直觀的例子出現(xiàn)48-50
• 3.4 DRF-Guarantee性質(zhì)證明50-57
• 3.4.1 無數(shù)據(jù)競爭51-54
• 3.4.2 帶標(biāo)簽的弱操作語義54
• 3.4.3 模擬關(guān)系(Simulation)54-57
• 3.5 程序變換算法的正確性57-62
• 3.5.1 程序變換58-61
• 3.5.2 變換的正確性61-62
• 3.6 相關(guān)工作62-64
• 3.7 總結(jié)和弱點探討64-67
• 第四章 從OHMM到TSO弱內(nèi)存模型67-71
• 4.1 OHMM-TSO模型67-71
• 第五章 用于TSO模型局部推理的程序邏輯71-99
• 5.1 語言71-78
• 5.1.1 TSO標(biāo)準(zhǔn)模型72
• 5.1.2 ATSO內(nèi)存模型72-78
• 5.2 斷言定義78-83
• 5.3 邏輯系統(tǒng)83-86
• 5.4 一些例子86-91
• 5.4.1 Optimzed Implementation of Locks算法86-87
• 5.4.2 Peterson's Lock算法87-88
• 5.4.3 Simpson's Four Slot算法88-91
• 5.4.4 Concurrent GCD算法91
• 5.5 邏輯可靠性證明91-97
• 5.5.1 TSO是ATSO的精化93-94
• 5.5.2 邏輯系統(tǒng)在ATSO上的可靠性94-97
• 5.6 相關(guān)工作和總結(jié)97-99
• 第六章 結(jié)論99-101
• 參考文獻101-105
• 附錄A Simulation引理證明105-113
• 附錄B 程序變換的正確性證明113-123
• B.1 E-WAR的正確性113-115
• B.2 E-WBW和E-IR正確性115
• B.3 E-RAR和E-RAW正確性115-117
• B.4 調(diào)序變換的正確性117-120
• B.5 I-IR的正確性120-123
• 附錄C TSO和ATSO精化關(guān)系證明123-125
• 附錄D 邏輯在ATSO上可靠性主引理的證明125-129
• 致謝129-131
• 在讀期間發(fā)表的學(xué)術(shù)論文與取得的研究成果131

【共引文獻】

中國期刊全文數(shù)據(jù)庫 前10條

1 余偉;;基于消元法生成非線性循環(huán)不變式[J];電子技術(shù)與軟件工程;2014年16期

2 萬良;石文昌;馮慧;;基于分離邏輯的并行程序性質(zhì)驗證方法[J];計算機科學(xué);2013年10期

3 羅軍;王宏;李文生;;基于向量時鐘模型的NoSQL最終一致性的研究[J];計算機工程與應(yīng)用;2013年23期

4 張晶;潘有順;;嵌入式系統(tǒng)同步進程的競態(tài)條件分析與推理學(xué)習(xí)方法[J];計算機科學(xué);2014年02期

5 萬良;;基于隔離邏輯的并行程序可靠性驗證方法[J];計算機工程;2014年02期

6 SHEN YuPing;ZHAO XiShun;;Proof systems for planning under 0-approximation semantics[J];Science China(Information Sciences);2014年07期

7 劉恒;李美安;蘇萌;;基于重復(fù)數(shù)的最短循環(huán)請求集生成算法[J];計算機應(yīng)用;2014年05期

8 張展;左德承;黃友富;何輝;;一種基于準(zhǔn)同步檢查點的虛擬機卷回恢復(fù)算法[J];計算機科學(xué);2014年05期

9 余偉;;循環(huán)不變式在程序設(shè)計教學(xué)中的應(yīng)用[J];科技風(fēng);2014年14期

10 林菲;孫勇;丁宏;任一支;;自穩(wěn)定的分布式事務(wù)內(nèi)存模型及算法[J];計算機研究與發(fā)展;2014年09期

中國博士學(xué)位論文全文數(shù)據(jù)庫 前9條

1 朱素霞;面向多核處理器確定性重演的內(nèi)存競爭記錄機制研究[D];哈爾濱工業(yè)大學(xué);2013年

2 劉洋;網(wǎng)絡(luò)式軟件需求驗證的形式化方法研究[D];電子科技大學(xué);2013年

3 毛華堅;云環(huán)境中的移動文件存儲和時空數(shù)據(jù)分析關(guān)鍵技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2013年

4 劉光輝;高效處理器容錯技術(shù)研究與實現(xiàn)[D];國防科學(xué)技術(shù)大學(xué);2013年

5 吳曉峰;面向無線網(wǎng)絡(luò)的形式化方法研究[D];華東師范大學(xué);2014年

6 楊哲a\;Java語言的程序漏洞檢測與診斷技術(shù)[D];復(fù)旦大學(xué);2012年

7 王濤;任務(wù)關(guān)鍵系統(tǒng)的軟件行為建模與檢測技術(shù)研究[D];燕山大學(xué);2014年

8 周寧;代數(shù)化符號模擬驗證的應(yīng)用研究[D];北京交通大學(xué);2015年

9 陳艷文;分布式系統(tǒng)的時間化通信行為模型[D];華東師范大學(xué);2014年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前10條

1 劉恒;并發(fā)數(shù)據(jù)結(jié)構(gòu)及其在動態(tài)內(nèi)存管理中的應(yīng)用[D];重慶大學(xué);2013年

2 張越;鐵路信號聯(lián)鎖系統(tǒng)安全規(guī)范的形式化描述與驗證方法[D];北京交通大學(xué);2013年

3 顧飛;基于SPARC架構(gòu)面向確定性重演的多核訪存競爭記錄方法的研究[D];哈爾濱工業(yè)大學(xué);2013年

4 王勇;動態(tài)可重構(gòu)的DSM語義研究[D];哈爾濱工業(yè)大學(xué);2012年

5 齊蓓;基于軟件體系結(jié)構(gòu)的軟件可靠性驗證測評方法研究[D];東華大學(xué);2013年

6 劉彥武;綜合信息系統(tǒng)的開發(fā)與建設(shè)[D];天津大學(xué);2012年

7 劉曼霞;基于XYZ/SE的C/S體系結(jié)構(gòu)風(fēng)格研究[D];湖南大學(xué);2013年

8 王文苑;分布式緩存可用性相關(guān)問題研究[D];華中科技大學(xué);2013年

9 孫建良;分布式存儲系統(tǒng)可用性與一致性研究[D];華中科技大學(xué);2013年

10 曹粟;基于非即停調(diào)試模式的嵌入式應(yīng)用級調(diào)試系統(tǒng)[D];華中科技大學(xué);2013年

  本文關(guān)鍵詞：基于操作語義的弱內(nèi)存模型描述及程序邏輯研究，，由筆耕文化傳播整理發(fā)布。

本文編號：266401