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. The algorithm allows the hashtables to grow and shrink when needed.

A true problem of wait-free and lock-free algorithms is that they are hard to design correctly, even when apparently straightforward. The reason for this is that processes can execute all statements in every conceivable order. Since our algorithm is quite large and rather complex, we turned to the interactive theorem prover PVS to prove safety of our algorithm, which we could not have done reliably by hand. To our knowledge no algorithms of comparable complexity have ever been mechanically verified. Wait-freedom is shown informally.