finelybook
Automated Verification of Concurrent Search Structures
Siddharth Krishna,Microsoft Research,Cambridge,
Nisarg Patel,New York University,
Dennis Shasha,New York University,
Thomas Wies,New York University
ISBN: 9781636391281 | PDF ISBN: 9781636391298
Hardcover ISBN: 9781636391304
Copyright © 2021 | 188 Pages
Book Description
Search structures support the fundamental data storage primitives on key-value pairs: insert a pair,delete by 作者: key,search by 作者: key,and update the value associated with a key. Concurrent search structures are parallel algorithms to speed access to search structures on multicore and distributed servers. These sophisticated algorithms perform fine-grained synchronization between threads,making them notoriously difficult to design correctly. Indeed,bugs have been found both in actual implementations and in the designs proposed by 作者: experts in peer-reviewed publications. The rapid development and deployment of these concurrent algorithms has resulted in a rift between the algorithms that can be verified by 作者: the state-of-the-art techniques and those being developed and used today. The goal of this book is to show how to bridge this gap in order to bring the certified safety of formal verification to high-performance concurrent search structures. Similar techniques and frameworks can be applied to concurrent graph and network algorithms beyond search structures.
Table of contents
Introduction
Preliminaries
Separation Logic
Ghost State
The Keyset Resource Algebra
The Edgeset Framework for Single-Copy Structures
The Flow Framework
Verifying Single-Copy Concurrent Search Structures
Verifying Multicopy Structures
The Edgeset Framework for Multicopy Structures
Reasoning about Non-Static and Non-Local Linearization Points
Verifying the LSM DAG Template
Proof Mechanization and Automation
Related Work,Future Work,and Conclusion
Bibliography
Authors' Biographies
