一种无锁并发跳表算法的可线性化证明

摘要

随着互联网的普及和云计算的发展，海量数据处理成为IT从业人员越来越重视的课题。海量数据处理常采用并发的方法，即多个线程同时运行在多台处理器上，共同访问和处理共享数据。由于多个线程的交互，并发程序的行为更难以预测，出现的错误也更难以定位。因此，通过严谨的数学方法在逻辑上验证一个并发程序的正确性很有意义。
　　无锁并发跳表是一种无需对各个节点加锁就能实现多个线程同时无阻塞操作的数据结构，其存取时间复杂度是对数级，类似于平衡树，另外，其采用一种概率方案来平衡数据结构，无需定期对数据结构进行重平衡，因此操作效率很高，非常适用于海量数据的并发处理，并且已经得到了广泛的应用。但是，无锁并发跳表算法的正确性并未得到严格的形式化证明。
　　可线性化是并发数据结构的正确性标准之一，指的是对象操作的细粒度实现与瞬间原子操作有相同的效果，本文即采用最新提出的不固定线性化点算法可线性化性质的模块化验证方法，验证了无锁并发跳表算法的可线性化性质。
　　为了证明无锁并发跳表算法的可线性化性质，本文做了如下工作:
　　1、给出基础逻辑集合。本文首先给出了一个简单的抽象机和语言模型，并根据机器模型构造逻辑推导规则;然后在语言模型上实现无锁并发跳表算法;最后将无锁并发跳表抽象成整数集合，再给出各具体算法对应的抽象原子操作。
　　2、确定了算法的“潜在”线性化点，并通过模块化验证方法中提出的方案在算法中添加辅助语句以标识线性化点。
　　3、用形式化语言构造算法的规范。根据LRG逻辑，算法规范包括三部分:用于描述无锁并发跳表不变特征的不变式(I);算法执行所依赖的环境规范R;算法本身所保证的规范G。
　　4、最后，对无锁并发跳表算法进行了严格地推导证明，并首次形式化的证明了无锁并发跳表算法的可线性化性质。
　　由于不固定线性化点算法可线性化性质的模块化验证方法经过形式化的可靠性证明，因此本文通过可靠地形式化验证方法首次证明了无锁并发跳表算法的可线性化性质。