一句话：提出将 Rely-Guarantee 推理应用于引用，并用精化类型在未验证与完全验证之间验证无锁数据结构不变式。
细粒度并发数据结构的不变式验证困难，因为其他线程的干扰可能发生在任意时刻。本文提出将 Rely-Guarantee 推理应用于并发环境中的引用，从而在不验证整个程序的情况下界定线程干扰，并保持数据结构不变式。该方法位于简单类型系统与现代并发程序逻辑之间，避免封装并发数据结构实现，且能与未验证的命令式代码安全交互。作者用两个实现进行案例研究：一个公理化的 Coq 领域特定语言，以及一个 Liquid Haskell 库；并比较了交互式证明（Coq）与可自动消解的依赖精化类型（Liquid 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 C oq domain-specific language and a library for Liquid Haskell. Third, these two implementations allow us to compare and contrast verifications by interactive proof (C oq ) and a weaker form that can be expressed using automatically-discharged dependent refinement types (Liquid Haskell).
@article{GordonEGP17,
title = {Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types},
author = {Colin S. Gordon and Michael D. Ernst and Dan Grossman and Matthew J. Parkinson},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {39},
number = {3},
year = {2017},
doi = {10.1145/3064850}
}