Mechanically verified proof obligations for linearizability
Mechanically verified proof obligations for linearizability
复制标题
DOI：
10.1145/1889997.1890001
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
J. Derrick;G. Schellhorn;H. Wehrheim
中科院分区：
文献类型：
--
作者：
J. Derrick;G. Schellhorn;H. Wehrheim
并发对象本质上是复杂的验证。在80年代末和90年代初，Herlihy和Wing提出了线性化的性能，作为并发对象的正确性条件，一旦证明，它只能使用前条件和后条件来推理并发对象。如果其所有操作似乎在其调用和返回之间立即生效，则可以将一个对象线性化。在本文中，我们定义了基于仿真的证明条件的线性化条件，并将其应用于两个并发实现，一个无锁的堆栈和带有锁耦合的设置。与其他方法类似，我们采用定理供奉献者（这里，KIV）来机械化我们的证明。与其他方法相反，我们还使用供奉献者机械地检查我们的证明义务实际上可以保证线性化。此检查采用了Herlihy的原始想法和通过可能性验证线性化的机翼。
Concurrent objects are inherently complex to verify. In the late 80s and early 90s, Herlihy and Wing proposed linearizability as a correctness condition for concurrent objects, which, once proven, allows us to reason about concurrent objects using pre- and postconditions only. A concurrent object is linearizable if all of its operations appear to take effect instantaneously some time between their invocation and return. In this article we define simulation-based proof conditions for linearizability and apply them to two concurrent implementations, a lock-free stack and a set with lock-coupling. Similar to other approaches, we employ a theorem prover (here, KIV) to mechanize our proofs. Contrary to other approaches, we also use the prover to mechanically check that our proof obligations actually guarantee linearizability. This check employs the original ideas of Herlihy and Wing of verifying linearizability via possibilities.