New Book Announcement - Automated Verification of Concurrent Search Structures

We are pleased to announce the latest title in Morgan & Claypool's series on
Computer Science.

 

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

 

Paperback ISBN: 9781636391281

eBook ISBN: 9781636391298

Hardcover ISBN: 9781636391304

June 2021 | 188 Pages

 

http://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?produc
ts_id=1638

 

Abstract

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 

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

 

Series: Computer Science

https://www.morganclaypoolpublishers.com/catalog_Orig/index.php?cPath=22
<https://www.morganclaypoolpublishers.com/catalog_Orig/index.php?cPath=22&so
rt=2a&series=14> &sort=2a&series=14

 

Brent Beckley
Direct Marketing Manager
Morgan & Claypool Publishers

 <https://twitter.com/MorganClaypool> @MorganClaypool (Twitter)

 



-- 
This email has been checked for viruses by Avast antivirus software.
https://www.avast.com/antivirus

########################################################################

To unsubscribe from the IR list, click the following link:
https://www.jiscmail.ac.uk/cgi-bin/WA-JISC.exe?SUBED1=IR&A=1

This message was issued to members of www.jiscmail.ac.uk/IR, a mailing list hosted by www.jiscmail.ac.uk, terms & conditions are available at https://www.jiscmail.ac.uk/policyandsecurity/