Peng Liu
Abstract
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 are atomic (or linearizable), 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.
- A. V. Aho, M. S. Lam, R. Sethi, and J. D. Ullman. Compilers: Principles, Techniques, and Tools (Second Edition). Addison-Wesley Longman Publishing Co., Inc., 2006. Google Scholar
Digital Library
- A. W. Appel and J. Palsberg. Modern Compiler Implementation in Java (Second Edition). Cambridge University Press, 2002. Google ScholarDigital Library
- S. Burckhardt, C. Dern, M. Musuvathi, and R. Tan. Line-up: a complete and automatic linearizability checker. In PLDI, 2010. Google ScholarDigital Library
- L. Chew and D. Lie. Kivati: Fast detection and prevention of atomicity violations. In EuroSys, 2010. Google ScholarDigital Library
- R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and K. F. Zadeck. Efficiently computing static single assignment form and the control dependence graph. TOPLAS, 1991. Google ScholarDigital Library
- D. Dice, O. Shalev, and N. Shavit. Transactional locking ii. In DISC, 2006. Google ScholarDigital Library
- G. Golan-Gueta, G. Ramalingam, M. Sagiv, and E. Yahav. Concurrent libraries with foresight. In PLDI, 2013. Google ScholarDigital Library
- P. Hawkins, A. Aiken, K. Fisher, M. Rinard, and M. Sagiv. Concurrent data representation synthesis. In PLDI, 2012. Google ScholarDigital Library
- M. Herlihy and E. Koskinen. Transactional boosting: a methodology for highly-concurrent transactional objects. In PPoPP, 2008. Google ScholarDigital Library
- M. Herlihy, V. Luchangco, and M. Moir. A flexible framework for implementing software transactional memory. In OOPSLA '06. Google ScholarDigital Library
- M. P. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects. TOPLAS, 1990. Google ScholarDigital Library
- G. Jin, L. Song, W. Zhang, S. Lu, and B. Liblit. Automated atomicity-violation fixing. In PLDI, 2011. Google ScholarDigital Library
- G. A. Kildall. A unified approach to global program optimization. In POPL, 1973. Google ScholarDigital Library
- M. Kulkarni, D. Nguyen, D. Prountzos, X. Sui, and K. Pingali. Exploiting the commutativity lattice. In PLDI, 2011. Google ScholarDigital Library
- H. T. Kung and J. T. Robinson. On optimistic methods for concurrency control. TODS, 1981. Google ScholarDigital Library
- Y. Lin and D. Dig. Check-then-act misuse of java concurrent collections. In ICST, pages 164--173, 2013. Google ScholarDigital Library
- P. Liu, J. Dolby, and C. Zhang. Finding incorrect compositions of atomicity. In ESEC/FSE, 2013. Google ScholarDigital Library
- P. Liu and C. Zhang. Axis: automatically fixing atomicity violations through solving control constraints. In ICSE '12. Google ScholarDigital Library
- B. Lucia, J. Devietti, K. Strauss, and L. Ceze. Atom-aid: Detecting and surviving atomicity violations. In ISCA, 2008. Google ScholarDigital Library
- D. Prountzos, R. Manevich, K. Pingali, and K. S. McKinley. A shape analysis for optimizing parallel graph programs. In POPL, 2011. Google ScholarDigital Library
- S. Rajamani, G. Ramalingam, V. P. Ranganath, and K. Vaswani. Isolator: dynamically ensuring isolation in concurrent programs. In ASPLOS, 2009. Google ScholarDigital Library
- P. Ratanaworabhan, M. Burtscher, D. Kirovski, B. G. Zorn, R. Nagpal, and K. Pattabiraman. Detecting and tolerating asymmetric races. In PPOPP, 2009. Google ScholarDigital Library
- M. Sch\"afer, M. Verbaere, T. Ekman, and O. Moor. Stepping stones over the refactoring rubicon. In ECOOP, 2009.Google Scholar
- O. Shacham. Verifying Atomicity of Composed Concurrent Operations. PhD thesis, Tel Aviv University, 2012.Google Scholar
- O. Shacham, N. G. Bronson, A. Aiken, M. Sagiv, M. T. Vechev, and E. Yahav. Testing atomicity of composed concurrent operations. 2011.Google ScholarDigital Library
- O. Shacham, E. Yahav, G. Gueta, A. Aiken, N. Bronson, M. Sagiv, and M. Vechev. Verifying atomicity via data independence. In ISSTA, 2014. Google ScholarDigital Library
- N. Shavit. Data structures in the multicore age. CACM, 2011. Google ScholarDigital Library
- O. Tripp, R. Manevich, J. Field, and M. Sagiv. Janus: exploiting parallelism via hindsight. In PLDI, 2012. Google ScholarDigital Library
- O. Tripp and N. Rinetzky. Tightfit: Adaptive parallelization with foresight. In ESEC/FSE, 2013. Google ScholarDigital Library
- O. Tripp, G. Yorsh, J. Field, and M. Sagiv. Hawkeye: effective discovery of dataflow impediments to parallelization. In OOPSLA, 2011. Google ScholarDigital Library
- P.vCerný, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, and T. Tarrach. Efficient synthesis for concurrency by semantics-preserving transformations. In CAV, 2013. Google ScholarDigital Library
- M. T. Vechev and E. Yahav. Deriving linearizable fine-grained concurrent objects. In PLDI, 2008. Google ScholarDigital Library
- D. Weeratunge, X. Zhang, and S. Jaganathan. Accentuating the positive: Atomicity inference and enforcement using correct executions. In OOPSLA, 2011. Google ScholarDigital Library
- J. Yu and S. Narayanasamy. Tolerating concurrency bugs using transactions as lifeguards. In MICRO, 2010. Google ScholarDigital Library
- W. Zhang, M. de Kruijf, A. Li, S. Lu, and K. Sankaralingam. Conair: Featherweight concurrency bug recovery via single-threaded idempotent execution. In ASPLOS, 2013. Google ScholarDigital Library
Index Terms
- Flint: fixing linearizability violations
Recommendations
Flint: fixing linearizability violations
OOPSLA '14: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & ApplicationsWriting 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, ...
A systematic survey on automated concurrency bug detection, exposing, avoidance, and fixing techniques
Currently, concurrent programs are becoming increasingly widespread to meet the demands of the rapid development of multi-core hardware. However, it could be quite expensive and challenging to guarantee the correctness and efficiency of concurrent ...
Finding incorrect compositions of atomicity
ESEC/FSE 2013: Proceedings of the 2013 9th Joint Meeting on Foundations of Software EngineeringIn object-oriented code, atomicity is ideally isolated in a library which encapsulates shared program state and provides atomic APIs for access. The library provides a convenient way for programmers to reason about the needed synchronization. However, ...
Comments