Automatic Local Proofs of Linearizability

Poling: Proof of Linearizability Generator


Proofs of linearizability of concurrent data structures have generally relied on identifying linearization points to establish a simulation argument between the implementation and the specification. However, for many linearizable data structure methods, the linearization points may not correspond to their internal static code locations; for example, they might reside in the code of another concurrent operation. To overcome this limitation, we identify important program patterns that expose such instances, and describe a tool ({\sc Poling}) that automatically verifies the linearizability of implementations that conform to these patterns.

Technique descriptions of the Poling and its proof of correctness can be found in this manuscript [pdf]

This project is built upon CAVE: Concurrent Algorithm VErifier.