基于軟件事務(wù)內(nèi)存的并行程序驗證.pdf

1、近年來，由于物理定律的障礙，使用增加晶體管數(shù)量來提高處理器性能的摩爾定律已經(jīng)逐漸走到了盡頭。為了解決這個問題，人們將目光投向了多核處理器，它主要通過并行計算來提高性能。多核多處理等新一代系統(tǒng)結(jié)構(gòu)對并行的全面支持，引發(fā)了軟件開發(fā)方式上的巨變。軟件不再能從硬件性能提升中免費獲益，而需要充分利用硬件特性實現(xiàn)并發(fā)，才能充分發(fā)揮新一代硬件的優(yōu)勢。因此，面向多核時代的編程人員，越來越需要設(shè)計和開發(fā)并行程序，以充分利用這種多核硬件特征。然而，并行編程

2、是有相當(dāng)難度的。一方面，目前的語言和工具仍沒有做好將應(yīng)用轉(zhuǎn)化為并行程序的準(zhǔn)備；另一方面，并行編程要求程序員以人類難以適應(yīng)的方式思考。
　　 在并行編程中，對共享資源的并發(fā)訪問控制是一個關(guān)鍵性的問題。傳統(tǒng)上，程序員通常使用鎖機制來進(jìn)行并發(fā)控制，但是傳統(tǒng)的鎖機制存在以下缺陷：1）粒度選擇困難，粗粒度鎖編程簡單但并發(fā)度低；細(xì)粒度鎖能提高并發(fā)度但是難以實現(xiàn),2）不具有組合性，兩段使用鎖機制實現(xiàn)的、能正確運行的代碼合并后得到的代碼可能出現(xiàn)

3、錯誤,3）容易引起優(yōu)先級倒置、護(hù)送、死鎖等問題。
　　 為了給程序員提供一種易編程同時具有高并發(fā)度的并行編程機制，研究人員將數(shù)據(jù)庫中的并發(fā)控制概念引入到編程語言中形成事務(wù)內(nèi)存系統(tǒng)。事務(wù)內(nèi)存主要分為兩層：在高層，它提供一種比較簡單的類似串行形式的程序語義使得編程容易；在低層，研究人員使用鎖等機制設(shè)計各種不同的細(xì)粒度并發(fā)系統(tǒng)來將高層的程序翻譯到底層系統(tǒng)中并發(fā)地執(zhí)行。通過這兩層系統(tǒng)，可以有效地解決長久以來并行編程給程序員帶來的諸多困擾

4、。
　　 但是，事務(wù)內(nèi)存系統(tǒng)的出現(xiàn)也給并行程序驗證帶來了新的挑戰(zhàn)，已有的并行驗證技術(shù)與邏輯系統(tǒng)不能直接用來驗證事務(wù)內(nèi)存程序。因此，本學(xué)位論文中的工作著眼于此問題，通過深入研究軟件事務(wù)內(nèi)存系統(tǒng)的各種實現(xiàn)機制，并結(jié)合現(xiàn)有的并行程序驗證技術(shù)，設(shè)計了一種新的用于驗證軟件事務(wù)內(nèi)存程序的邏輯推理系統(tǒng)。通過驗證軟件事務(wù)內(nèi)存程序來指導(dǎo)事務(wù)內(nèi)存系統(tǒng)的實現(xiàn)，為構(gòu)造高可信并行軟件奠定基礎(chǔ)。同時，本文還關(guān)注一些現(xiàn)有的軟件事務(wù)內(nèi)存系統(tǒng)實現(xiàn)算法，使用形式化

5、方法來驗證該實現(xiàn)算法的安全性與正確性。
　　 本文的主要工作和貢獻(xiàn)可以分為以下幾個部分：? 在攜帶基礎(chǔ)證明程序的基礎(chǔ)上設(shè)計了一種用于驗證基于事務(wù)內(nèi)存同步機制的匯編級并行程序的程序邏輯系統(tǒng)。在該系統(tǒng)中，本文巧妙地設(shè)計了一種結(jié)合了并發(fā)分離邏輯和攜權(quán)限分離邏輯的程序邏輯來支持驗證事務(wù)代碼中的投機讀操作。此外，基于該系統(tǒng)本文中還提出了一種驗證事務(wù)代碼原子性的方法，以保證事務(wù)代碼執(zhí)行的正確性。
　　 ? 在定理輔助證明工具Coq中

6、完成了本文所設(shè)計的驗證事務(wù)內(nèi)存程序邏輯系統(tǒng)的所有可靠性證明，從而將該邏輯系統(tǒng)中的驗證推理規(guī)則從受信任計算基礎(chǔ)中排除出去，使其具有更高的可靠性。此外，我們通過具體的實例證明來體現(xiàn)此邏輯系統(tǒng)的有效性與實用性。
　　 ? 使用最新的程序邏輯驗證了一種經(jīng)典的軟件事務(wù)內(nèi)存實現(xiàn)算法TransactionalLocking II的安全性與正確性。在證明中，通過使用輔助變量與輔助代碼，本文總結(jié)出一種驗證基于版本化鎖實現(xiàn)的事務(wù)投機讀操作的方法。此