Lock-free dynamic hash tables with open addressing
From MaRDI portal
Abstract: We present an efficient lock-free algorithm for parallel accessible hash tables with open addressing, which promises more robust performance and reliability than conventional lock-based implementations. ``Lock-free means that it is guaranteed that always at least one process completes its operation within a bounded number of steps. For a single processor architecture our solution is as efficient as sequential hash tables. On a multiprocessor architecture this is also the case when all processors have comparable speeds. The algorithm allows processors that have widely different speeds or come to a halt. It can easily be implemented using C-like languages and requires on average only constant time for insertion, deletion or accessing of elements. The algorithm allows the hash tables to grow and shrink when needed. Lock-free algorithms are hard to design correctly, even when apparently straightforward. Ensuring the correctness of the design at the earliest possible stage is a major challenge in any responsible system development. In view of the complexity of the algorithm, we turned to the interactive theorem prover PVS for mechanical support. We employ standard deductive verification techniques to prove around 200 invariance properties of our algorithm, and describe how this is achieved with the theorem prover PVS.
Recommendations
Cites work
- scientific article; zbMATH DE number 52331 (Why is no real title available?)
- scientific article; zbMATH DE number 3473265 (Why is no real title available?)
- scientific article; zbMATH DE number 1033646 (Why is no real title available?)
- A performance evaluation of lock-free synchronization protocols
- Bounded delay for a free address
- Lock-free linked lists using compare-and-swap
- Modeling and verification of parallel processes. 4th Summer school, MOVEP 2000, Nantes, France, June 19--23, 2000. Revised tutorial lectures
- Randomized wait-free concurrent objects (extended abstract)
- Renaming in an asynchronous environment
- Split-ordered lists
Cited in
(9)- Parallel implementations of Brunotte's algorithm
- On the correctness of a lock-free compression-based elastic mechanism for a hash trie design
- Adaptive lock-free maps: purely-functional to scalable
- Split-ordered lists
- Computer Aided Verification
- Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos
- Distributed Computing
- Proving a non-blocking algorithm for process renaming with TLA\textsuperscript{+}
- A general lock-free algorithm using compare-and-swap
This page was built for publication: Lock-free dynamic hash tables with open addressing
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1953636)
