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

Linearizability of a Lock-free Concurrent Skiplist

为了证明无锁并发跳表算法的可线性化性质,采用最新提出的不固定线性化点算法可线性化性质的模块化验证方法,首先建立一个简单的抽象机和语言模型,在抽象机上实现无锁并发跳表算法并生成局部依赖与保证风格的推导规则,然后寻找算法的线性化点并通过模块化验证方法中的方案在算法实现中添加辅助语句以标识线性化点,接着构造基本断言如不变式I、算法执行所依赖的环境规范R和算法规范G,最后根据推导规则对算法进行严格的推导证明.由于不固定线性化点算法可线性化性质的模块化验证方法经过形式化的可靠性证明,因此本文通过可靠地形式化验证方法首次证明了无锁并发跳表算法的可线性化性质.

Based on the modular verification method of linearizability with non-fixed linearization points, we verify the linearizability of lock-free concurrent skiplist. First,we build a simple abstract machine and language model,and implement the algorithm on the ab- stract machine. Then, we find the linearization points of the algorithm and add corresponding auxiliary statements based on the modular verification method. After that, we construct basic assertions like the invariant I, the environment specifications R, and the algorithm specification G. Finally, we verify the linearizability of the algorithm step by step using inference rules. The modular verification meth- od＇s soundness have been formally verified,so we verify the thelinearizability of lock-free concurrent skiplist formally and reliably for the first time.