1.) Testing Atomicity of Composed Concurrent Operations (OOPSLA’11) 2.) Automatic Fine-Grain Locking using Shape Properties

1.)Testing Atomicity of Composed Concurrent Operations (OOPSLA’11)
We address the problem of testing atomicity of composed concurrent operations. Concurrent libraries help programmers exploit parallel hardware by providing scalable concurrent operations with the illusion that each operation is executed atomically. However, client code often needs to compose atomic operations in such a way that the resulting composite operation is also atomic while also preserving scalability. We present a novel technique for testing the atomicity of client code composing scalable concurrent operations. The challenge in testing this kind of client code is that a bug may occur very rarely and only on a particular interleaving with a specific thread configuration. Our technique is based on modular testing of client code in the presence of an adversarial environment; we use commutativity specifications to drastically reduce the number of executions explored to detect a bug. We implemented our approach in a tool called COLT, and evaluated its effectiveness on a range of 51 real-world concurrent Java programs. Using COLT, we found 56 atomicity violations in Apache Tomcat, Cassandra, MyFaces Trinidad, and other applications.

2.)Automatic Fine-Grain Locking using Shape Properties
We present a technique for automatically adding fine-grain locking to an abstract data type that is implemented using a dynamic forest –i.e., the data structures may be mutated, even to the point of violating forestness temporarily during the execution of a method of the ADT. Our automatic technique is based on Domination Locking, a novel locking protocol. Domination locking is designed specifically for software concurrency control, and in particular is designed for object oriented software with destructive pointer updates. Domination locking is a strict generalization of existing locking protocols for dynamically changing graphs. We show our technique can successfully add fine-grain locking to libraries where manually performing locking is extremely challenging. We show that automatic fine-grain locking is more efficient than coarse-grain locking, and obtains similar performance to hand-crafted fine-grain locking.

发言人详细信息

Ohad Shacham is a PhD student at Tel Aviv University under the supervision of Mooly Sagiv and Eran Yahav. His PhD dissertation addresses the question of checking atomicity of concurrent collection operations. Prior to his thesis, Ohad worked in IBM Haifa Research Group on hardware verification.

Guy Golan-Gueta is a PhD student at Tel Aviv University under the supervision of Mooly Sagiv and Eran Yahav. He is interested in various aspects of concurrency. In the past, Guy was a software architect on several software projects. He was responsible for the design and the development of many high performance critical systems.

专题：
Microsoft Research Talks
日期：
演讲者：
Ohad Shacham and Guy Golan-Gueta
所属机构：
Tel Aviv University

系列： Microsoft Research Talks