A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
复制标题
DOI：
10.1145/2629496
复制
发表时间：
2014-11-01
影响因子：
0.5
通讯作者：
Wehrheim, Heike
中科院分区：
文献类型：
--
作者：
Schellhorn, Gerhard;Derrick, John;Wehrheim, Heike
数据结构（如队列、堆栈或散列表）的有效实现允许许多进程同时并发访问。为了提高并发性，这些算法通常完全不使用锁定，或者只锁定结构的一小部分。线性性是这种场景的标准正确性标准——如果并发对象的所有操作似乎在调用和返回之间的某个时间瞬间生效，那么该对象就是线性化的。对共享数据结构的潜在并发访问极大地增加了验证问题的复杂性，因此当前用于显示线性性的证明技术都是针对特定类型的数据结构量身定制的。在以前的工作中，我们已经展示了如何使用基于仿真的线性性证明条件来验证许多微妙的并发算法。在这篇文章中，我们现在证明了基于反向模拟的条件可以用来证明每一个可线性化算法的线性化，也就是说，我们证明了我们的证明技术是健全和完整的。我们通过并发队列的线性化证明来举例说明我们的方法，该方法在Herlihy和Wing关于线性化的里程碑式论文中介绍。除了他们的手工证明之外，许多其他方法都没有成功地处理过这个队列。我们的方法得到了完全机械化的支持：案例研究（如队列）的线性性证明，以及稳健性和完整性证明都是通过交互式证明器（KIV）进行的。
Efficient implementations of data structures such as queues, stacks or hash-tables allow for concurrent access by many processes at the same time. To increase concurrency, these algorithms often completely dispose with locking, or only lock small parts of the structure. Linearizability is the standard correctness criterion for such a scenario-where a concurrent object is linearizable if all of its operations appear to take effect instantaneously some time between their invocation and return.The potential concurrent access to the shared data structure tremendously increases the complexity of the verification problem, and thus current proof techniques for showing linearizability are all tailored to specific types of data structures. In previous work, we have shown how simulation-based proof conditions for linearizability can be used to verify a number of subtle concurrent algorithms. In this article, we now show that conditions based on backward simulation can be used to show linearizability of every linearizable algorithm, that is, we show that our proof technique is both sound and complete. We exemplify our approach by a linearizability proof of a concurrent queue, introduced in Herlihy and Wing's landmark paper on linearizability. Except for their manual proof, none of the numerous other approaches have successfully treated this queue.Our approach is supported by a full mechanisation: both the linearizability proofs for case studies like the queue, and the proofs of soundness and completeness have been carried out with an interactive prover, which is KIV.