关于将可线性化化为状态可达性
On Reducing Linearizability to State Reachability
摘要：
原子对象（如并发堆栈和队列）的有效实现特别容易受到编程错误的影响，并且需要自动验证。不幸的是，他们的正确性标准-相对于给定的ADT规格的线性化-很难验证。即使在通常的时间安全属性（如控制状态可达性）是可判定的实现类上，线性化也是不可判定的。在这项工作中，我们证明了验证线性化某些固定ADT规格是可减少控制状态的可达性，尽管更难任意ADT。我们实现了几个最流行的原子对象的这种减少。这种减少产生的第一个可判定性结果的验证，而不限制并发线程的数量。此外，它使现有的安全验证工具的线性化验证的应用。
英文摘要：
Efficient implementations of atomic objects such as concurrent stacks and queues are especially susceptible to programming errors, and necessitate automatic verification. Unfortunately their correctness criteria - linearizability with respect to given ADT specifications - are hard to verify. Even on classes of implementations where the usual temporal safety properties like control-state reachability are decidable, linearizability is undecidable. In this work we demonstrate that verifying linearizability for certain fixed ADT specifications is reducible to control-state reachability, despite being harder for arbitrary ADTs. We effectuate this reduction for several of the most popular atomic objects. This reduction yields the first decidability results for verification without bounding the number of concurrent threads. Furthermore, it enables the application of existing safety-verification tools to linearizability verification.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
