Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types

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 sett...

Full description

Saved in:
Bibliographic Details
Published in:ACM transactions on programming languages and systems 2017-09, Vol.39 (3), p.1-54, Article 11
Main Authors: Gordon, Colin S., Ernst, Michael D., Grossman, Dan, Parkinson, Matthew J.
Format: Article
Language:English
Subjects:
Computing methodologies
Concurrent computing methodologies
Concurrent programming languages
Invariants
Program constructs
Program reasoning
Program verification
Semantics and reasoning
Theory of computation
Type structures
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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).
ISSN:0164-0925
1558-4593
DOI:10.1145/3064850