Automatic Atomicity Verification for Clients of Concurrent Data Structures
Automatic Atomicity Verification for Clients of Concurrent Data Structures
复制标题
并发数据结构客户端的自动原子性验证
DOI：
10.1007/978-3-319-08867-9_37
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
J. Palsberg
中科院分区：
文献类型：
--
作者：
M. Lesani;T. Millstein;J. Palsberg
主流编程语言提供并发数据结构库。并发数据结构上的每个方法调用似乎都原子地生效。然而，这种数据结构的客户端通常需要更强的保证。例如，使用并发map实现的直方图类可能需要一个方法来原子地增加直方图条，但其实现需要多次调用map，因此默认情况下不是原子的。事实上，以前的工作已经表明，在客户端的并发数据结构的原子性错误经常发生在productioncode.We提出了一个自动和模块化的并发数据结构的客户端验证技术。我们定义了一个新的充分条件原子的客户端称为凝聚性。我们提出了一个名为雪花的工具，产生证明Java客户端方法的可压缩性的义务，并使用现成的SMT求解器排出它们。我们将Snowflake应用于几个开源应用程序的现有客户端方法套件。它成功地验证了76.9%的原子方法，没有任何更改，并通过小的代码重构和/或注释验证了其余的方法。
Mainstream programming languages offer libraries of concurrent data structures. Each method call on a concurrent data structure appears to take effect atomically. However, clients of such data structures often require stronger guarantees. For instance, a histogram class that is implemented using a concurrent map may require a method to atomically increment a histogram bar, but its implementation requires multiple calls to the map and hence is not atomic by default. Indeed, prior work has shown that atomicity errors in clients of concurrent data structures occur frequently in production code.We present an automatic and modular verification technique for clients of concurrent data structures. We define a novel sufficient condition for atomicity of clients called condensability. We present a tool called Snowflake that generates proof obligations for condensability of Java client methods and discharges them using an off-the-shelf SMT solver. We applied Snowflake to an existing suite of client methods from several open-source applications. It successfully verified 76.9% of the atomic methods without any change and verified the rest of them with small code refactoring and/or annotations.