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