Automatic Atomicity Verification for Clients of Concurrent Data Structures

Abstract. Mainstream programming languages offer libraries of concur-rent data structures. Each method call on a concurrent data structure appears to take effect atomically. However, clients of such data struc-tures 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 sev-eral 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.