The anchor verifier for blocking and non-blocking concurrent software
The anchor verifier for blocking and non-blocking concurrent software
复制标题
DOI：
10.1145/3428224
复制
发表时间：
2020-11
影响因子：
--
通讯作者：
C. Flanagan;Stephen N. Freund
中科院分区：
文献类型：
--
作者：
C. Flanagan;Stephen N. Freund
验证具有微妙同步的并发软件的正确性是出了名的具有挑战性。我们介绍了Anchor验证器，它基于一种用于指定同步规则的新形式体系，该形式体系描述了（1）允许哪些内存访问，以及（2）每个允许的访问如何与其他线程的并发操作交换（以便于归约证明）。Anchor支持对基于锁的阻塞算法和基于CAS（比较并交换）的非阻塞算法的验证。对多种并发数据结构和算法进行的实验表明，Anchor显著减轻了并发验证的负担。
Verifying the correctness of concurrent software with subtle synchronization is notoriously challenging. We present the Anchor verifier, which is based on a new formalism for specifying synchronization disciplines that describes both (1) what memory accesses are permitted, and (2) how each permitted access commutes with concurrent operations of other threads (to facilitate reduction proofs). Anchor supports the verification of both lock-based blocking and cas-based non-blocking algorithms. Experiments on a variety concurrent data structures and algorithms show that Anchor significantly reduces the burden of concurrent verification.