Journal article
Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types
ACM transactions on programming languages and systems, v 39(3), pp 1-54
01 Jul 2017
Featured in Collection : UN Sustainable Development Goals @ Drexel
Abstract
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).
Metrics
Details
- Title
- Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types
- Creators
- Colin S. Gordon - Drexel UniversityMichael A. Ernst - Univ Washington, Paul G Allen Sch Comp Sci & Engn, Box 352350,185 E Stevens Way NE, Seattle, WA 98195 USADan Grossman - University of WashingtonMatthew J. Parkinson - Microsoft Research
- Publication Details
- ACM transactions on programming languages and systems, v 39(3), pp 1-54
- Publisher
- Assoc Computing Machinery
- Number of pages
- 54
- Resource Type
- Journal article
- Language
- English
- Academic Unit
- Computer Science
- Web of Science ID
- WOS:000414327900002
- Scopus ID
- 2-s2.0-85019873752
- Other Identifier
- 991019169909004721
UN Sustainable Development Goals (SDGs)
This publication has contributed to the advancement of the following goals:
InCites Highlights
Data related to this publication, from InCites Benchmarking & Analytics tool:
- Collaboration types
- Industry collaboration
- Domestic collaboration
- International collaboration
- Web of Science research areas
- Computer Science, Software Engineering