Automated verification of linearization policies

PA Abdulla, B Jonsson, CQ Trinh - … 2016, Edinburgh, UK, September 8-10 …, 2016 - Springer
Static Analysis: 23rd International Symposium, SAS 2016, Edinburgh, UK …, 2016Springer
We present a novel framework for automated verification of linearizability for concurrent data
structures that implement sets, stacks, and queues. The framework requires the user to
provide a linearization policy, which describes how linearization point placement in different
concurrent threads affect each other; such linearization policies are often provided informally
together with descriptions of new algorithms. We present a specification formalism for
linearization policies which allows the user to specify, in a simple and concise manner …
Abstract
We present a novel framework for automated verification of linearizability for concurrent data structures that implement sets, stacks, and queues. The framework requires the user to provide a linearization policy, which describes how linearization point placement in different concurrent threads affect each other; such linearization policies are often provided informally together with descriptions of new algorithms. We present a specification formalism for linearization policies which allows the user to specify, in a simple and concise manner, complex patterns including non-fixed linearization points. To automate verification, we extend thread-modular reasoning to bound the number of considered threads, and use a novel symbolic representation for unbounded heap structures that store data from an unbounded domain. We have implemented our framework in a tool and successfully used it to prove linearizability for a wide range of algorithms, including all implementations of concurrent sets, stacks, and queues based on singly-linked lists that are known to us from the literature.
Springer