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

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

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

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