Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types
Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types
复制标题
DOI：
10.1145/3064850
复制
发表时间：
2017-07-01
影响因子：
1.3
通讯作者：
Parkinson, Matthew J.
中科院分区：
文献类型：
--
作者：
Gordon, Colin S.;Ernst, Michael A.;Parkinson, Matthew J.
验证细粒并发的不变性，数据结构具有挑战性，因为其他线程的干扰可能随时发生。我们提出了一种证明不变的并发数据结构的新方法：将依赖性推理应用于并发设置中的参考。对参考的依赖保证可以验证线程干扰上的界限，而无需验证整个程序。本文提供了三个新的结果。首先，它提供了一种新方法来保存不变性并限制并发数据结构的使用。我们的方法针对简单类型系统与现代同步程序逻辑之间的空间，在未验证的代码和完整验证之间提供了一个中间点。此外，它避免了密封并发的数据结构实现，并且可以与未验证的命令代码安全地交互。其次，我们使用两种实现来证明该方法的广泛适用性：公理COQ域特异性语言和液体Haskell库。第三，这两种实现使我们能够通过交互式证明（COQ）进行比较和对比验证，并且可以使用自动放电的依赖性细化类型（液体haskell）表示较弱的形式。
Verifying invariants of fine-grained concurrent, data structures is challenging, because interference from other threads may occur at any time. We propose a new way of proving invariants of fine-grained concurrent data structures: applying rely-guarantee reasoning to references in the concurrent setting. Rely-guarantee applied to references can verify bounds on thread interference without requiring a whole program to be verified.This article provides three new results. First, it provides a new approach to preserving invariants and restricting usage of concurrent data structures. Our approach targets a space between simple type systems and modern concurrent program logics, offering an intermediate point between unverified code and full verification. Furthermore, it avoids sealing concurrent data structure implementations and can interact safely with unverified imperative code. Second, we demonstrate the approach's broad applicability through a series of case studies, using two implementations: an axiomatic COQ domain-specific language and a library for Liquid Haskell. Third, these two implementations allow us to compare and contrast verifications by interactive proof (Coq) and a weaker form that can be expressed using automatically-discharged dependent refinement types (Liquid Haskell).