Efficient almost wait-free parallel accesible dynamic hashtables

H. Gao, J.F. Groote, W.H. Hesselink

Research output: Book/ReportReportAcademic

44 Downloads (Pure)


Abstract In multiprogrammed systems, synchronization often turns out to be a performance bottleneck and the source of poor fault-tolerance. Wait-free and lock-free algorithms can do without locking mechanisms, and therefore do not suffer from these problems. We present an efficient almost wait-free algorithm for parallel accessible hashtables, which promises more robust performance and reliability than conventional lock-based implementations. Our solution is as efficient as sequential hashtables. It can easily be implemented using C-like languages and requires on average only constant time for insertion, deletion or accessing of elements. Apart from that, our new algorithm allows the hashtables to grow and shrink dynamically when needed. A true problem of lock-free algorithms is that they 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. Our algorithm contains 81 atomic statements. In view of the complexity of the algorithm and its correctness properties, 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 almost wait-free algorithm, and describe how this is achieved using the theorem prover PVS. CR Subject Classification (1991): D.1 Programming techniques AMS Subject Classification (1991): 68Q22 Distributed algorithms, 68P20 Information storage and retrieval Keywords & Phrases: Hashtables, Distributed algorithms, Lock-free, Wait-free
Original languageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages37
Publication statusPublished - 2003

Publication series

NameComputer science reports
ISSN (Print)0926-4515


Dive into the research topics of 'Efficient almost wait-free parallel accesible dynamic hashtables'. Together they form a unique fingerprint.

Cite this