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

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

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

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

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

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

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