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

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

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

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

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

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

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