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

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

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

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