论文标题
通过差异抽象将可达性验证降低到可达性
Reducing Commutativity Verification to Reachability with Differencing Abstractions
论文作者
论文摘要
数据结构方法的交换性是持续的兴趣，其根源在数据库社区中。近年来，通勤性已被证明是在平行编译器，交易内存，投机执行以及更广泛的软件可扩展性等上下文中实现多项核心并发的关键要素。尽管有这种兴趣，但对于如何从其实现中自动验证数据结构的通勤规范仍然是一个悬而未决的问题。 在本文中，我们描述了自动证明数据结构实现方法的通勤条件的正确性。我们引入了一种新型的抽象，该抽象表征了两种方法的效果不同的方式，具体取决于应用方法的顺序，而摘要消除方法的效果，无论顺序如何，方法都将是相同的。然后，我们描述了一种新颖的算法，该算法将问题降低到可达性，以便现成的程序分析工具可以执行证明交通便利所必需的推理。最后，我们描述了概念验证的实现和实验结果，表明我们的工具可以验证数据结构的通勤性，例如存储单元，计数器，两个位置，基于阵列的堆栈，队列和基本哈希表。最后，我们讨论了什么使数据结构的通勤能力可以通过当今工具证明，以及需要做些什么才能证明将来更多。
Commutativity of data structure methods is of ongoing interest, with roots in the database community. In recent years commutativity has been shown to be a key ingredient to enabling multicore concurrency in contexts such as parallelizing compilers, transactional memory, speculative execution and, more broadly, software scalability. Despite this interest, it remains an open question as to how a data structure's commutativity specification can be verified automatically from its implementation. In this paper, we describe techniques to automatically prove the correctness of method commutativity conditions from data structure implementations. We introduce a new kind of abstraction that characterizes the ways in which the effects of two methods differ depending on the order in which the methods are applied, and abstracts away effects of methods that would be the same regardless of the order. We then describe a novel algorithm that reduces the problem to reachability, so that off-the-shelf program analysis tools can perform the reasoning necessary for proving commutativity. Finally, we describe a proof-of-concept implementation and experimental results, showing that our tool can verify commutativity of data structures such as a memory cell, counter, two-place Set, array-based stack, queue, and a rudimentary hash table. We conclude with a discussion of what makes a data structure's commutativity provable with today's tools and what needs to be done to prove more in the future.
