Automated Verification of Concurrent Search Structures
May 2022 · Springer Nature
Ebook
182
Pages
About this ebook
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 ser...
Discover more
About the author
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 tohis 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.
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 ...
Rate this ebook
Tell us what you think.
Reading information
Smartphones and tablets
Install the Google Play Books app for Android and iPad/iPhone. It syncs automatically with your account and allows you to read online or offline wherever you are.
Laptops and computers
You can listen to audiobooks purchased on Google Play using your computer's web browser.
eReaders and other devices
To read on e-ink devices like Kobo eReaders, you'll need to download a file and transfer it to your device. Follow the detailed Help Center instructions to transfer the files to supported eReaders.
