Writing concurrent software while achieving both correctness and efficiency is a grand challenge. To facilitate this task, concurrent data structures have been introduced into the standard library of popular languages like Java and C#. Unfortunately, while the operations exposed by concurrent data structures behave atomically, compositions of these operations are not necessarily atomic. Recent studies have found many erroneous implementations of composed concurrent operations.
We address the problem of fixing nonlinearizable composed operations such that they behave atomically. We introduce Flint, an automated fixing algorithm for composed Map operations. Flint accepts as input a composed operation suffering from atomicity violations. Its output, if fixing succeeds, is a composed operation that behaves equivalently to the original operation in sequential runs and is guaranteed to be atomic. To our knowledge, Flint is the first general algorithm for fixing incorrect concurrent compositions.
We have evaluated Flint on 48 incorrect compositions from 27 popular applications, including Tomcat and MyFaces. The results are highly encouraging: Flint is able to correct 96% of the methods, and the fixed version is often the same as the fix by an expert programmer and as efficient as the original code.
Thu 23 OctDisplayed time zone: Tijuana, Baja California change
15:30 - 17:00
|CheckCell: Data Debugging for Spreadsheets|
Dan Barowy University of Massachusetts, Amherst, Dimitar Gochev University of Massachusetts, Amherst, Emery D. Berger University of Massachusetts, AmherstLink to publication
|Finding Minimum Type Error Sources|
Zvonimir Pavlinovic New York University, Tim King New York University, Thomas Wies New York UniversityLink to publication File Attached
|Flint: Fixing Linearizability Violations|
Peng Liu Purdue University, Omer Tripp IBM Thomas J. Watson Research Center, Xiangyu Zhang Purdue UniversityLink to publication
|Statistical Debugging for Real-World Performance Problems|
OOPSLALink to publication