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

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

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

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

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

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