Verifying concurrent search structure templates

Siddharth Krishna, Nisarg Patel, Dennis Shasha, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Concurrent separation logics have had great success reasoning about concurrent data structures. This success stems from their application of modularity on multiple levels, leading to proofs that are decomposed according to program structure, program state, and individual threads. Despite these advances, it remains difficult to achieve proof reuse across different data structure implementations. For the large class of search structures, we demonstrate how one can achieve further proof modularity by decoupling the proof of thread safety from the proof of structural integrity. We base our work on the template algorithms of Shasha and Goodman that dictate how threads interact but abstract from the concrete layout of nodes in memory. Building on the recently proposed flow framework of compositional abstractions and the separation logic Iris, we show how to prove correctness of template algorithms, and how to instantiate them to obtain multiple verified implementations. We demonstrate our approach by mechanizing the proofs of three concurrent search structure templates, based on link, give-up, and lock-coupling synchronization, and deriving verified implementations based on B-trees, hash tables, and linked lists. These case studies include algorithms used in real-world file systems and databases, which have been beyond the capability of prior automated or mechanized verification techniques. In addition, our approach reduces proof complexity and is able to achieve significant proof reuse.

Original languageEnglish (US)
Title of host publicationPLDI 2020 - Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsAlastair F. Donaldson, Emina Torlak
PublisherAssociation for Computing Machinery
Pages181-196
Number of pages16
ISBN (Electronic)9781450376136
DOIs
StatePublished - Jun 11 2020
Event41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020 - London, United Kingdom
Duration: Jun 15 2020Jun 20 2020

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Conference

Conference41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020
CountryUnited Kingdom
CityLondon
Period6/15/206/20/20

Keywords

  • Concurrent data structures
  • Flow framework
  • Separation logic
  • Template-based verification

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Verifying concurrent search structure templates'. Together they form a unique fingerprint.

  • Cite this

    Krishna, S., Patel, N., Shasha, D., & Wies, T. (2020). Verifying concurrent search structure templates. In A. F. Donaldson, & E. Torlak (Eds.), PLDI 2020 - Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 181-196). (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). Association for Computing Machinery. https://doi.org/10.1145/3385412.3386029