Automated Verification of Concurrent Search Structures
Seiten
2021
Morgan & Claypool Publishers (Verlag)
978-1-63639-130-4 (ISBN)
Morgan & Claypool Publishers (Verlag)
978-1-63639-130-4 (ISBN)
The rapid development and deployment of 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. This book shows how to bridge this gap to bring the certified safety of formal verification to high-performance concurrent search structures.
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.
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.
Acknowledgments
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
| Erscheinungsdatum | 22.06.2021 |
|---|---|
| Reihe/Serie | Synthesis Lectures on Computer Science |
| Verlagsort | San Rafael |
| Sprache | englisch |
| Maße | 191 x 235 mm |
| Themenwelt | Informatik ► Datenbanken ► Data Warehouse / Data Mining |
| Mathematik / Informatik ► Informatik ► Theorie / Studium | |
| Mathematik / Informatik ► Informatik ► Web / Internet | |
| ISBN-10 | 1-63639-130-3 / 1636391303 |
| ISBN-13 | 978-1-63639-130-4 / 9781636391304 |
| Zustand | Neuware |
| Haben Sie eine Frage zum Produkt? |
Mehr entdecken
aus dem Bereich
aus dem Bereich
Datenanalyse für Künstliche Intelligenz
Buch | Softcover (2024)
De Gruyter Oldenbourg (Verlag)
CHF 104,90
Daten importieren, bereinigen, umformen und visualisieren
Buch | Softcover (2024)
O'Reilly (Verlag)
CHF 76,85
