基于操作語(yǔ)義的弱內(nèi)存模型描述及程序邏輯研究.pdf

1、程序語(yǔ)言的內(nèi)存模型規(guī)定了在程序執(zhí)行的過(guò)程中內(nèi)存訪問(wèn)是如何發(fā)生的。它作為橋梁將為程序員和語(yǔ)言實(shí)現(xiàn)連接起來(lái)，幫助程序員寫(xiě)出正確的并發(fā)程序。在現(xiàn)實(shí)世界中，大多數(shù)的硬件和編譯系統(tǒng)都是基于弱內(nèi)存模型的假設(shè)，即內(nèi)存訪問(wèn)并不是嚴(yán)格按照程序順序執(zhí)行，以用來(lái)支持各類優(yōu)化。本文研究了弱內(nèi)存模型的設(shè)計(jì)，并提出了可以支持在弱內(nèi)存模型上進(jìn)行程序驗(yàn)證的程序邏輯。具體來(lái)說(shuō)，本文在弱內(nèi)存模型和程序邏輯方面做出了如下的貢獻(xiàn):
　　首先，本文提出一種新的弱內(nèi)存模型O

2、HMM，這是Happens-before內(nèi)存模型(HMM)的變種。這個(gè)模型通過(guò)對(duì)一個(gè)簡(jiǎn)單語(yǔ)言賦予具體的操作語(yǔ)義，并通過(guò)它在抽象機(jī)上的程序行為來(lái)模擬HMM。由于OHMM所允許的程序行為是通過(guò)操作語(yǔ)義自然生成的，所以它自然而然的避免了所謂的憑空出現(xiàn)(out-of-thin-air)的程序行為。另外一方面，OHMM使用一種我們稱之為重放的機(jī)制來(lái)允許某些符合一定條件的指令在抽象機(jī)上能夠多次執(zhí)行，來(lái)模擬現(xiàn)實(shí)世界中編譯器和處理器優(yōu)化中的投機(jī)執(zhí)行和優(yōu)

3、化。總的來(lái)說(shuō)，我們的模型對(duì)于無(wú)鎖程序的約束會(huì)比Java內(nèi)存模型(JMM)更加弱一些，因此我們將會(huì)允許更多的編譯器優(yōu)化算法在我們的模型上能夠使用。同時(shí)，在OHMM上，程序行為在直觀上會(huì)比JMM更加自然。許多在JMM上可能出現(xiàn)但是明顯違反直觀認(rèn)識(shí)的程序，在我們的模型上就不再合法。我們希望OHMM可以成為可供類Java語(yǔ)言選擇的一種新內(nèi)存模型。
　　其次，本文提出一種新的用于驗(yàn)證并發(fā)程序在TSO(Total Store Order)弱內(nèi)

4、存模型下正確性的程序邏輯。TSO模型所允許的弱行為是OHMM的子集。我們知道，TSO模型已經(jīng)被用作X86和SPARC-TSO處理器族的模型基礎(chǔ)，并且在一些高級(jí)語(yǔ)言中也正在被提案作為其內(nèi)存模型的基礎(chǔ)。我們的邏輯對(duì)LRG(LocalRely-Guarantee)進(jìn)行擴(kuò)展，對(duì)其加入了關(guān)于TSO寫(xiě)緩存的斷言，這可以讓我們對(duì)TSO模型中對(duì)外部線程不可見(jiàn)的局部的寫(xiě)緩存的狀態(tài)進(jìn)行描述。如同LRG一樣，我們的程序邏輯支持對(duì)細(xì)粒度并發(fā)具有表達(dá)力強(qiáng)的rel

5、y/guarantee推理以及分離邏輯中的局部推理。同時(shí)，我們?cè)谶壿嬌蠈?duì)TSO模型進(jìn)行進(jìn)一步抽象，把TSO共享內(nèi)存分為local和shared兩部分，這可以允許我們可以將那些在訪問(wèn)時(shí)只有單個(gè)線程能夠訪問(wèn)的內(nèi)存單元（邏輯上等同于local單元）的寫(xiě)操作直接寫(xiě)入內(nèi)存，不需要經(jīng)過(guò)寫(xiě)緩存。我們使用這個(gè)邏輯證明了一些具有代表性的并發(fā)算法在TSO上的正確性，包括Peterson's lock算法，Simpson's four slot算法，conc