Linearizability has become the de facto correctness specification for 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 investigate linearizability monitoring -- check if an execution history of an implementation is linearizable. While this problem is 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 linearizability monitoring. At its heart, this framework asks to identify special linearizability-preserving values in a given history -- values whose presence yields an equilinearizable sub-history when removed, and whose absence indicates non-linearizability. We prove that a polynomial time algorithm for the problem of identifying linearizability-preserving values, yields a polynomial time algorithm for linearizability monitoring, while conversely, intractability of this problem implies intractability of the monitoring problem. We demonstrate our framework's effectiveness by instantiating it for several popular data types -- sets, stacks, queues and priority queues -- deriving polynomial time algorithms for each, with the unambiguity restriction, where each insertion to the underlying data structure adds a distinct value. We optimize these algorithms to achieve the optimal log-linear time complexity by amortizing the cost of solving sub-problems through efficient data structures. Our implementation and evaluation on publicly available implementations show that our approach scales to large histories and outperforms existing tools.

翻译：线性一致性已成为并发数据结构实现的事实正确性规范。虽然形式化验证此类实现仍具挑战性，但线性一致性监测作为排除定制实现开发早期问题的有前景的第一步已经出现，并成为对此类实现进行压力测试方法中的关键组成部分。在本工作中，我们研究线性一致性监测——检查实现的执行历史是否满足线性一致性。尽管该问题在一般情况下是难解的，但对其何时变得可解的系统性理解仍然缺乏。我们重新审视该问题，首先提出了一个统一的线性一致性监测"减治"算法框架。该框架的核心在于识别给定历史中的特殊线性一致性保持值——这些值的存在使得移除后产生等线性可化的子历史，而其缺失则表明非线性一致性。我们证明，针对识别线性一致性保持值问题的多项式时间算法可导出线性一致性监测的多项式时间算法；反之，该问题的难解性意味着监测问题的难解性。我们通过将该框架实例化于多种常用数据类型——集合、栈、队列和优先队列——来证明其有效性，在无歧义限制下（即底层数据结构的每次插入均添加相异值）为每种类型推导出多项式时间算法。我们通过高效数据结构分摊子问题求解成本，优化这些算法以达到最优的对数线性时间复杂度。在公开可用实现上的实验评估表明，我们的方法可扩展至大规模历史记录，且性能优于现有工具。