Proving Linearizability Via Non-atomic Refinement
Proving Linearizability Via Non-atomic Refinement
复制标题
通过非原子细化证明线性化
DOI：
10.1007/978-3-540-73210-5_11
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
H. Wehrheim
中科院分区：
文献类型：
--
作者：
J. Derrick;G. Schellhorn;H. Wehrheim
可线性化性是并发对象的正确性准则。在本文中，我们证明了线性化的并发无锁堆栈实现显示的实现是一个抽象堆栈的非原子细化。为此，我们开发了一个概括的非原子细化允许一个细化到一个CSP过程中的一个单一的（Z）操作。除了这个扩展，定义还体现了一个终止条件，允许一个证明饥饿自由的并发进程。
Linearizability is a correctness criterion for concurrent objects. In this paper, we prove linearizability of a concurrent lock-free stack implementation by showing the implementation to be a nonatomic refinement of an abstract stack. To this end, we develop a generalisation of non-atomic refinement allowing one to refine a single (Z) operation into a CSP process. Besides this extension, the definition furthermore embodies a termination condition which permits one to prove starvation freedom for the concurrent processes.