Composing Concurrent Libraries

Writing concurrent programs manually is challenging. Therefore many modern programming languages such as Java, Scala, and C# already provide efficient concurrent data structure implementations which hides the complexity of developing concurrent system.

However it is tricky to use these implementations. It is hard for programmers to build complex operations from a few primitive ones. Therefore, much of the art of API design comes in choosing a set of primitives that is both simple and complete. Unfortunately, existing efficient concurrent data structures do not allow to safely compose operations. The lack of a generic mechanism for composition of concurrent ADTs leads to complex and less complete APIs.

The theme of this project is developing effective tools to ease the task of employing such concurrent data structures for more secure and effective programming.

Preliminary Results

• In Testing Atomicity of Composed Concurrent Operations. we have shown that 44% of the public domain usages of concurrent Map operations are buggy. As a result of this paper the Java concurrent library is being modified. Click here and here for more information.
• In a follow-on work by Ohad Shacham to be available soon, we developed an effective technique which can be used to prove the absence of atomicity violations.
• In Concurrent Data Representation Synthesis, we show to infer serializable and deadlock free composed operations using relational specifications.
• In Transactional Objects with Foresight, we show how to avoid atomicity violations and deadlocks using static analysis on the client and smart libraries which perform synchronization operations in lazy manner. The library implementation utilize the semantics of the ADT interface in order to allow more potential parallelism.