Checking Linearizability of Encapsulated Extended Operations

Linearizable objects (data-structures) provide operations
that appear to execute atomically. Modern mainstream languages provide
many linearizable data-structures, simplifying concurrent programming.
In practice, however, programmers often find a need to execute a
sequence of operations (on linearizable objects) that executes atomically
and write extended operations for this purpose. Such extended operations
are a common source of atomicity bugs.
This paper focuses on the problem of verifying that a set of extension
operations (to a linearizable library) are themselves linearizable. We
present several reduction theorems that simplify this verification problem
enabling more efficient verification.
We first introduce the notion of an encapsulated extension: this is
an extension that (a) does not introduce new shared state (beyond the
shared state in the base linearizable library), and (b) accesses or modifies
the shared state only through the base operations. We show that
encapsulated extensions are widely prevalent in real applications.
We show that linearizability of encapsulated extended operations can
be verified by considering only histories with one occurrence of an extended
operation, interleaved with atomic occurrences of base and extended
operations. As a consequence, this verification needs to consider
only histories with two threads, whereas general linearizability verification
requires considering histories with an unbounded number of threads.
We show that when the operations satisfy certain properties, each
extended operation can be verified independently of the others, enabling
further reductions.
We have implemented a simple static analysis algorithm that conservatively
verifies linearizabilty of encapsulated extensions of Java concurrent
maps. We present empirical results illustrating the benefits of the
reduction theorems.