Using refinement calculus techniques to prove linearizability
Using refinement calculus techniques to prove linearizability
复制标题
使用细化微积分技术来证明线性化能力
DOI：
10.1007/s00165-012-0250-7
复制
发表时间：
2012
影响因子：
1
通讯作者：
B. Jonsson
中科院分区：
文献类型：
--
作者：
B. Jonsson
逐步细化是一种系统地将高级程序转换为有效可执行程序的方法。一个先后改进的程序序列也可以作为正确性证明，它使程序中的不同机制显化。我们提出了改进多线程共享变量并发程序的规则。我们将这些规则应用于验证并发对象的线性性问题，并发对象可以被无限数量的并发线程访问。线性性是为并发对象建立的正确性标准，它指出每个方法执行的效果可以被认为是在调用和响应之间的某个时间点自动发生的。我们展示了如何用我们的细化关系来表示线性化，并提出了通过方法体的一系列局部变换在程序之间建立这种细化关系的规则。其贡献包括加强了先前的原子性细化技术，以及一个吸收规则，该规则特别适合于对实现原子操作的并发算法进行推理。通过证明Treiber并发堆栈算法和Michael and Scott并发队列算法的线性性，说明了改进规则的应用。
Stepwise refinement is a method for systematically transforming a high-level program into an efficiently executable one. A sequence of successively refined programs can also serve as a correctness proof, which makes different mechanisms in the program explicit. We present rules for refinement of multi-threaded shared-variable concurrent programs. We apply our rules to the problem of verifying linearizability of concurrent objects, that are accessed by an unbounded number of concurrent threads. Linearizability is an established correctness criterion for concurrent objects, which states that the effect of each method execution can be considered to occur atomically at some point in time between its invocation and response. We show how linearizability can be expressed in terms of our refinement relation, and present rules for establishing this refinement relation between programs by a sequence of local transformations of method bodies. Contributions include strengthenings of previous techniques for atomicity refinement, as well as an absorption rule, which is particularly suitable for reasoning about concurrent algorithms that implement atomic operations. We illustrate the application of the refinement rules by proving linearizability of Treiber’s concurrent stack algorithm and Michael and Scott’s concurrent queue algorithm.