Indexes are ubiquitous. Examples include associative arrays,
dictionaries, maps and hashes used in applications such as
databases, file systems and dynamic languages. Abstractly, a
sequential index can be viewed as 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.
Whilst appealingly simple, this abstract specification is insufficient
for reasoning about indexes that are accessed concurrently.
We present an abstract specification for concurrent indexes.
We verify several representative concurrent client applications
using our specification, demonstrating that clients
can reason abstractly without having to consider specific
underlying implementations. Our specification would, however,
mean nothing if it were not satisfied by standard implementations
of concurrent indexes. We verify that our specification
is satisfied by algorithms based on linked lists, hash
tables and BLink trees. The complexity of these algorithms, in
particular the BLink tree algorithm, can be completely hidden
from the client’s view by our abstract specification.