Efficient Decrease-and-Conquer Linearizability Monitoring

Linearizability has become the de facto standard for specifying correctness of implementations of concurrent data structures. While formally verifying such implementations remains challenging, linearizability monitoring has emerged as a promising first step to rule out early problems in the development of custom implementations, and serves as a key component in approaches that stress test such implementations. In this work, we undertake an algorithmic investigation of the linearizability monitoring problem, which asks to check if an execution history obtained from a concurrent data structure implementation is linearizable. While this problem is largely understood to be intractable in general, a systematic understanding of when it becomes tractable has remained elusive. We revisit this problem and first present a unified ‘decrease-and-conquer’ algorithmic framework for designing linearizability monitoring. At its heart, this framework asks to identify special linearizability-preserving values in a given history — values whose presence yields an equi-linearizable sub-history (obtained by removing operations of such values), and whose absence indicates non-linearizability. More importantly, we prove that a polynomial time algorithm for the problem of identifying linearizability-preserving values, immediately yields a polynomial time algorithm for the linearizability monitoring problem, while conversely, intractability of this problem implies intractability of monitoring. We demonstrate the effectiveness of our decrease-and-conquer framework by instantiating it for several popular concurrent data types — registers, sets, stacks, queues and priority queues — deriving polynomial time algorithms for them, under the ( unambiguity ) restriction that each insertion to the underlying data structure adds a distinct value. We further optimize these algorithms to achieve log-linear running time through the use of efficient data structures for amortizing the cost of solving induced sub-problems. Our implementation and evaluation on publicly available implementations of concurrent data structures show that our approach scales to very large histories and significantly outperforms existing state-of-the-art tools.