Automatic Atomicity Verification for Clients of Concurrent Data Structures
Date: Monday, April 28, 2014
Time: 10:30 AM to 12:00 PM Note: all times are in the Eastern Time Zone
Host: Adam Chlipala, CSAIL
Contact: Adam Chlipala, firstname.lastname@example.org
Relevant URL: http://www.cs.ucla.edu/~lesani/
Speaker URL: None
TALK: Automatic Atomicity Verification for Clients of Concurrent Data Structures
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. It rejected all non-atomic methods.
Mohsen Lesani is a Phd candidate at UCLA. Recently, he has successfully defended his dissertation titled "On the correctness of transactional memory algorithms". He has research experience with IBM Research, Oracle (Sun) Labs, HP Labs and EPFL. He is interested in the design, implementation, testing and verification of synchronization algorithms.
Created by Adam Chlipala at Monday, March 31, 2014 at 3:01 PM.