libri scuola books Fumetti ebook dvd top ten sconti 0 Carrello


Torna Indietro

krishna siddharth; patel nisarg; shasha dennis; wies thomas - automated verification of concurrent search structures

Automated Verification of Concurrent Search Structures

; ; ;




Disponibilità: Normalmente disponibile in 15 giorni


PREZZO
59,98 €
NICEPRICE
56,98 €
SCONTO
5%



Questo prodotto usufruisce delle SPEDIZIONI GRATIS
selezionando l'opzione Corriere Veloce in fase di ordine.


Pagabile anche con Carta della cultura giovani e del merito, 18App Bonus Cultura e Carta del Docente


Facebook Twitter Aggiungi commento


Spese Gratis

Dettagli

Genere:Libro
Lingua: Inglese
Editore:

Springer

Pubblicazione: 06/2021





Trama

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.




Sommario

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.




Autore

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.










Altre Informazioni

ISBN:

9783031006784

Condizione: Nuovo
Collana: Synthesis Lectures on Computer Science
Dimensioni: 235 x 191 mm
Formato: Brossura
Illustration Notes:X, 182 p.
Pagine Arabe: 182
Pagine Romane: x


Dicono di noi