Indexes – also known as associative arrays, dictionaries,
maps, or hashes – are abstract data-structures with myriad
applications, from databases to dynamic languages. Abstractly,
an index is a partial function from keys to values.
Values can be queried by their keys, and the index can be
mutated by adding or removing mappings. While appealingly
simple, this abstract view is insufficient for reasoning
about indexes that are accessed concurrently.
In this paper, we introduce an abstract specification which
views an index as a divisible resource. Multiple threads can
access the index concurrently, yet threads can still reason locally.
We show that this specification can be used to verify
a number of client applications. Our abstract specification
would mean little if it were not satisfied by the implementations
of concurrent indexes. We verify that our specification
is satisfied by linked list, hash table and BLink tree index implementations.
During verification, we uncovered a subtle
bug in the BLink tree algorithm.