用差分抽象将交换性验证约简为可达性验证
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
