并发优先级队列的线性化检验
Checking Linearizability of Concurrent Priority Queues
摘要：
并发对象（如原子集合）的有效实现对现代计算至关重要。对这样的对象进行编程是容易出错的：在最小化并发对象调用之间的同步开销时，可能会出现与顺序规范的一致性的风险--或者用正式的术语来说，可能会违反线性化。不幸的是，验证线性化一般是不可判定的，即使在通常的控制状态可达性是可判定的实现类上也是如此。在这项工作中，我们考虑并发优先级队列，这是许多多线程应用程序，如任务调度或离散事件模拟的基础，并表明，验证这种实现的线性化可以减少到控制状态的可达性。这种减少需要的第一个可判定性的结果验证并发优先级队列的上下文中的一个无限数量的线程，它使现有的安全验证工具的应用程序建立其正确性。
英文摘要：
Efficient implementations of concurrent objects such as atomic collections are essential to modern computing. Programming such objects is error prone: in minimizing the synchronization overhead between concurrent object invocations, one risks the conformance to sequential specifications -- or in formal terms, one risks violating linearizability. Unfortunately, verifying linearizability is undecidable in general, even on classes of implementations where the usual control-state reachability is decidable. In this work we consider concurrent priority queues which are fundamental to many multi-threaded applications such as task scheduling or discrete event simulation, and show that verifying linearizability of such implementations can be reduced to control-state reachability. This reduction entails the first decidability results for verifying concurrent priority queues in the context of an unbounded number of threads, and it enables the application of existing safety-verification tools for establishing their correctness.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
