一種無鎖并發(fā)跳表算法的可線性化證明.pdf

1、隨著互聯(lián)網(wǎng)的普及和云計算的發(fā)展，海量數(shù)據(jù)處理成為IT從業(yè)人員越來越重視的課題。海量數(shù)據(jù)處理常采用并發(fā)的方法，即多個線程同時運行在多臺處理器上，共同訪問和處理共享數(shù)據(jù)。由于多個線程的交互，并發(fā)程序的行為更難以預測，出現(xiàn)的錯誤也更難以定位。因此，通過嚴謹?shù)臄?shù)學方法在邏輯上驗證一個并發(fā)程序的正確性很有意義。
　　無鎖并發(fā)跳表是一種無需對各個節(jié)點加鎖就能實現(xiàn)多個線程同時無阻塞操作的數(shù)據(jù)結構，其存取時間復雜度是對數(shù)級，類似于平衡樹，另外，其

2、采用一種概率方案來平衡數(shù)據(jù)結構，無需定期對數(shù)據(jù)結構進行重平衡，因此操作效率很高，非常適用于海量數(shù)據(jù)的并發(fā)處理，并且已經(jīng)得到了廣泛的應用。但是，無鎖并發(fā)跳表算法的正確性并未得到嚴格的形式化證明。
　　可線性化是并發(fā)數(shù)據(jù)結構的正確性標準之一，指的是對象操作的細粒度實現(xiàn)與瞬間原子操作有相同的效果，本文即采用最新提出的不固定線性化點算法可線性化性質的模塊化驗證方法，驗證了無鎖并發(fā)跳表算法的可線性化性質。
　　為了證明無鎖并發(fā)跳表算法

3、的可線性化性質，本文做了如下工作:
　　1、給出基礎邏輯集合。本文首先給出了一個簡單的抽象機和語言模型，并根據(jù)機器模型構造邏輯推導規(guī)則;然后在語言模型上實現(xiàn)無鎖并發(fā)跳表算法;最后將無鎖并發(fā)跳表抽象成整數(shù)集合，再給出各具體算法對應的抽象原子操作。
　　2、確定了算法的“潛在”線性化點，并通過模塊化驗證方法中提出的方案在算法中添加輔助語句以標識線性化點。
　　3、用形式化語言構造算法的規(guī)范。根據(jù)LRG邏輯，算法規(guī)范包括三部