Automated Verification of 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.

Auteur

Siddharth Krishna is a post-doctoral researcher at Microsoft Research Cambridge, UK. He completed his Ph.D. in logic and verification at New York University, where he had the good fortune to work with Nisarg, Dennis, and Thomas. He now works on parallel and distributed algorithms for large-scale machine learning workloads. When he is not pleading with computers to do his bidding, he likes to watch comedy panel/news shows and play ultimate frisbee.Nisarg Patel is a Ph.D. student at New York University's Department of Computer Science, where he works with Siddharth, Dennis, and Thomas on automated verification of concurrent programs. His academic interests also include synthesis of controller programs for robots. Outside of computer science, he loves playing football and reading about history and politics.Dennis Shasha is a Julius Silver Professor of computer science at the Courant Institute of New York University and an Associate Director of NYU Wireless. In addition to his long fascination with concurrent algorithms, he works on meta-algorithms for machine learning to achieve guaranteed correctness rates; with biologists on pattern discovery for network inference; with physicists and financial people on algorithms for time series; on database tuning; and tree and graph matching. Because he likes to type, he has written six books of puzzles about a mathematical detective named Dr. Ecco, a biography about great computer scientists, and a book about the future of computing. He has also written technical books about database tuning, biological pattern recognition, time series, DNA computing, resampling statistics, and causal inference in molecular networks. He has written the puzzle column for various publications including Scientific American, Dr. Dobb's Journal, and currently the Communications of the ACM. He is a fellow of the ACM and an INRIA International Chair.Thomas Wies is an Associate Professor in computer science at the Courant Institute of New York University and a member of the Analysis of Computer Systems Group. His research interests are in programming languages and formal methods with a focus on program analysis and verification, automated deduction, and correctness of concurrent software. He is the recipient of an NSF CAREER Award and has won multiple best paper awards. His fascination with concurrent tree traversals extends to his spare time: he enjoys hikes in the woods.

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