Automatic Atomicity Verification for Clients of Concurrent Data Structures

Speaker: Mohsen Lesani , UCLA

Date: Monday, April 28, 2014

Time: 10:30 AM to 12:00 PM Note: all times are in the Eastern Time Zone

Public: Yes

Location: 32-D507

Event Type:

Room Description:

Host: Adam Chlipala, CSAIL

Contact: Adam Chlipala, adamc@csail.mit.edu

Relevant URL: http://www.cs.ucla.edu/~lesani/

Speaker URL: None

Speaker Photo:
None

Reminders to: seminars@csail.mit.edu, pl@csail.mit.edu

Reminder Subject: TALK: Automatic Atomicity Verification for Clients of Concurrent Data Structures

Abstract:
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.

Bio:
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.

Research Areas:

Impact Areas:

See other events that are part of the PL/SE Seminar Series 2013/2014.

Created by Adam Chlipala at Monday, March 31, 2014 at 3:01 PM.