高效的分而治之线性化可行性监控方法

《Proceedings of the ACM on Programming Languages》：Efficient Decrease-and-Conquer Linearizability Monitoring

该研究提出了一种统一的“降维征服”算法框架来监测并发数据结构的线性化性，适用于寄存器、集合等数据类型，优化后实现log线性时间，并通过实验验证其高效性。

　　

摘要

线性化已成为指定并发数据结构实现正确性的事实标准。虽然正式验证这些实现仍然具有挑战性，但“线性化监控”已成为排除自定义实现早期问题的一个有前景的初步步骤，并且是进行压力测试的关键组成部分。在这项工作中，我们对线性化监控问题进行了算法研究，该问题旨在检查从并发数据结构实现中获得的执行历史是否具有线性化特性。

尽管普遍认为这个问题在一般情况下是难以解决的，但对其何时可解的系统理解仍然缺失。我们重新审视了这个问题，并首先提出了一个统一的“分而治之”算法框架来设计线性化监控方法。该框架的核心是识别给定历史中的特殊“保持线性化”值——这些值的存在会产生一个等线性化的子历史（通过移除这些值对应的操作获得），而它们的缺失则表明系统不具备线性化特性。更重要的是，我们证明了用于识别保持线性化值的多项式时间算法可以直接用于线性化监控问题；反之，如果线性化监控问题本身难以解决，那么保持线性化值的算法也同样难以实现。

我们通过将该框架应用于几种流行的并发数据类型（寄存器、集合、栈、队列和优先队列）来展示其有效性，在每个插入操作都会为底层数据结构添加一个唯一值的（“无歧义”）限制条件下，我们为这些类型推导出了多项式时间算法。此外，我们还通过使用高效的数据结构来分摊解决子问题的成本，进一步优化了这些算法，使其运行时间为对数线性。我们对公开可用的并发数据结构实现的测试表明，我们的方法能够处理非常长的历史记录，并且显著优于现有的最先进工具。