| 000 -LEADER |
|---|
| fixed length control field |
a |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION |
|---|
| fixed length control field |
211111b xxu||||| |||| 00| 0 eng d |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9781636391281 |
| 082 ## - DEWEY DECIMAL CLASSIFICATION NUMBER |
|---|
| Classification number |
005.741 |
| Item number |
KRI |
| 100 ## - MAIN ENTRY--PERSONAL NAME |
|---|
| Personal name |
Krishna, Siddharth |
| 245 ## - TITLE STATEMENT |
|---|
| Title |
Automated verification of concurrent search structures |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) |
|---|
| Name of publisher, distributor, etc |
Morgan & Claypool Publishers, |
| Date of publication, distribution, etc |
2021 |
| Place of publication, distribution, etc |
San Rafael, California : |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Extent |
xi, 176 p. ; |
| Other physical details |
ill. (some Colors), |
| Dimensions |
24 cm |
| 365 ## - TRADE PRICE |
|---|
| Price amount |
69.95 |
| Price type code |
USD |
| Unit of pricing |
78.70 |
| 490 ## - SERIES STATEMENT |
|---|
| Series statement |
Synthesis Lecture on Computer Science ; |
| Volume number/sequential designation |
13 |
| 504 ## - BIBLIOGRAPHY, ETC. NOTE |
|---|
| Bibliography, etc |
Includes bibliographical references. |
| 520 ## - SUMMARY, ETC. |
|---|
| Summary, etc |
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. |
| 650 ## - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Querying |
|
|---|
| Topical term or geographic name as entry element |
Data structures |
|
|---|
| Topical term or geographic name as entry element |
Computer logic |
|
|---|
| Topical term or geographic name as entry element |
verification |
|
|---|
| Topical term or geographic name as entry element |
separation logic |
|
|---|
| Topical term or geographic name as entry element |
concurrency |
|
|---|
| Topical term or geographic name as entry element |
search structures |
|
|---|
| Topical term or geographic name as entry element |
B trees |
|
|---|
| Topical term or geographic name as entry element |
hash structures |
|
|---|
| Topical term or geographic name as entry element |
log-structured merge trees |
|
|---|
| Topical term or geographic name as entry element |
Ghost state |
|
|---|
| Topical term or geographic name as entry element |
Multicopy structure |
|
|---|
| Topical term or geographic name as entry element |
Separation Logic |
|
|---|
| Topical term or geographic name as entry element |
Keyset Resource Algebra |
|
|---|
| Topical term or geographic name as entry element |
Single - Copy Edgeset Framework |
|
|---|
| Topical term or geographic name as entry element |
Flow Framework |
|
|---|
| Topical term or geographic name as entry element |
Multicopy Edgeset Framework |
|
|---|
| Topical term or geographic name as entry element |
LSMDAG Template |
|
|---|
| Topical term or geographic name as entry element |
Concurrency |
|
|---|
| Topical term or geographic name as entry element |
B trees |
|
|---|
| Topical term or geographic name as entry element |
Data storage |
| 710 ## - ADDED ENTRY--CORPORATE NAME |
|---|
| Corporate name or jurisdiction name as entry element |
Patel, Nisarg |
|
|---|
| Corporate name or jurisdiction name as entry element |
Shasha, Dennis |
|
|---|
| Corporate name or jurisdiction name as entry element |
Wies, Thomas |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) |
|---|
| Source of classification or shelving scheme |
|
| Item type |
Books |