Automatic Verification of Linearization Policies

We consider the problem of proving linearizability for concurrent threads that access a shared data structure. Such systems give rise to unbounded numbers of threads that operate on an bounded data domain and that access dynamically allocated memory. Furthermore, proving linearizability is harder than proving control state reachability due to existentially quantified linearization points. The problem is further complicated by the presence of advanced features such as non-fixed linearization points, speculation, and helping. In this presentation, we present a framework that can automatically verify linearizability for concurrent data structures that implement sets, stacks, and queues. We use a specification formalism for linearization techniques which allows the user to specify, in a simple and and concise manner, complex patterns including non-fixed linearization points. Then, we define abstraction techniques that allow to make the size of the data domain and the number of threads finite.