Linearizability of concurrent data structure implementations is notoriously hard to prove. Consequently, current verification techniques can only prove linearizability for certain classes of data structures. We introduce a generic, sound, and practical technique to statically check the linearizability of concurrent data structure implementations. Our technique involves specifying the concurrent operations as a list of sub-operations and passing this specification on to an automated checker that verifies linearizability using relationships between individual suboperations. We have proven the soundness of our technique. Our approach is expressive: we have successfully verified the linearizability of 12 popular concurrent data structure implementations including algorithms that are considered to be challenging to prove linearizable such as elimination back-off stack, lazy linked list, and time-stamped stack. Our checker is effective, as it can verify the specifications in less than a second.
展开▼
