Starling: Lightweight Concurrency Verification with Views
Starling: Lightweight Concurrency Verification with Views
复制标题
Starling：带视图的轻量级并发验证
DOI：
10.1007/978-3-319-63387-9_27
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Matthew J. Parkinson
中科院分区：
文献类型：
--
作者：
Matt Windsor;Mike Dodds;Ben Simner;Matthew J. Parkinson
现代程序逻辑使得验证最复杂的并发算法成为可能。然而，许多这样的逻辑是复杂的，并且大多数缺乏自动化工具支持。我们提出了Starling，一个新的轻量级的逻辑和自动化的并发验证工具。Starling采用以抽象Hoare逻辑风格编写的证明大纲，并将其转换为可以由顺序求解器排出的证明项。Starling的方法在结构上是通用的，因此可以轻松地针对不同的求解器。在本文中，我们使用Z3 SMT求解器验证共享变量算法，使用GRASShopper求解器验证基于堆的算法。我们已经将我们的方法应用于一系列并发算法，包括Rust的原子引用计数器，Linux ticketed lock，CLH锁和细粒度列表算法。
Modern program logics have made it feasible to verify the most complex concurrent algorithms. However, many such logics are complex, and most lack automated tool support. We propose Starling, a new lightweight logic and automated tool for concurrency verification. Starling takes a proof outline written in an abstracted Hoare-logic style, and converts it into proof terms that can be discharged by a sequential solver. Starling’s approach is generic in its structure, making it easy to target different solvers. In this paper we verify shared-variable algorithms using the Z3 SMT solver, and heap-based algorithms using the GRASShopper solver. We have applied our approach to a range of concurrent algorithms, including Rust’s atomic reference counter, the Linux ticketed lock, the CLH queue-lock, and a fine-grained list algorithm.