research-article

Flint: fixing linearizability violations

Authors:

Xiangyu ZhangAuthors Info & Claims

ACM SIGPLAN Notices, Volume 49, Issue 10

Pages 543 - 560

https://doi.org/10.1145/2714064.2660217

Published: 15 October 2014 Publication History

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.

References

[1]

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.

Digital Library

[2]

A. W. Appel and J. Palsberg. Modern Compiler Implementation in Java (Second Edition). Cambridge University Press, 2002.

Digital Library

[3]

S. Burckhardt, C. Dern, M. Musuvathi, and R. Tan. Line-up: a complete and automatic linearizability checker. In PLDI, 2010.

Digital Library

[4]

L. Chew and D. Lie. Kivati: Fast detection and prevention of atomicity violations. In EuroSys, 2010.

Digital Library

[5]

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.

Digital Library

[6]

D. Dice, O. Shalev, and N. Shavit. Transactional locking ii. In DISC, 2006.

Digital Library

[7]

G. Golan-Gueta, G. Ramalingam, M. Sagiv, and E. Yahav. Concurrent libraries with foresight. In PLDI, 2013.

Digital Library

[8]

P. Hawkins, A. Aiken, K. Fisher, M. Rinard, and M. Sagiv. Concurrent data representation synthesis. In PLDI, 2012.

Digital Library

[9]

M. Herlihy and E. Koskinen. Transactional boosting: a methodology for highly-concurrent transactional objects. In PPoPP, 2008.

Digital Library

[10]

M. Herlihy, V. Luchangco, and M. Moir. A flexible framework for implementing software transactional memory. In OOPSLA '06.

Digital Library

[11]

M. P. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects. TOPLAS, 1990.

Digital Library

[12]

G. Jin, L. Song, W. Zhang, S. Lu, and B. Liblit. Automated atomicity-violation fixing. In PLDI, 2011.

Digital Library

[13]

G. A. Kildall. A unified approach to global program optimization. In POPL, 1973.

Digital Library

[14]

M. Kulkarni, D. Nguyen, D. Prountzos, X. Sui, and K. Pingali. Exploiting the commutativity lattice. In PLDI, 2011.

Digital Library

[15]

H. T. Kung and J. T. Robinson. On optimistic methods for concurrency control. TODS, 1981.

Digital Library

[16]

Y. Lin and D. Dig. Check-then-act misuse of java concurrent collections. In ICST, pages 164--173, 2013.

Digital Library

[17]

P. Liu, J. Dolby, and C. Zhang. Finding incorrect compositions of atomicity. In ESEC/FSE, 2013.

Digital Library

[18]

P. Liu and C. Zhang. Axis: automatically fixing atomicity violations through solving control constraints. In ICSE '12.

Digital Library

[19]

B. Lucia, J. Devietti, K. Strauss, and L. Ceze. Atom-aid: Detecting and surviving atomicity violations. In ISCA, 2008.

Digital Library

[20]

D. Prountzos, R. Manevich, K. Pingali, and K. S. McKinley. A shape analysis for optimizing parallel graph programs. In POPL, 2011.

Digital Library

[21]

S. Rajamani, G. Ramalingam, V. P. Ranganath, and K. Vaswani. Isolator: dynamically ensuring isolation in concurrent programs. In ASPLOS, 2009.

Digital Library

[22]

P. Ratanaworabhan, M. Burtscher, D. Kirovski, B. G. Zorn, R. Nagpal, and K. Pattabiraman. Detecting and tolerating asymmetric races. In PPOPP, 2009.

Digital Library

[23]

M. Sch\"afer, M. Verbaere, T. Ekman, and O. Moor. Stepping stones over the refactoring rubicon. In ECOOP, 2009.

[24]

O. Shacham. Verifying Atomicity of Composed Concurrent Operations. PhD thesis, Tel Aviv University, 2012.

[25]

O. Shacham, N. G. Bronson, A. Aiken, M. Sagiv, M. T. Vechev, and E. Yahav. Testing atomicity of composed concurrent operations. 2011.

Digital Library

[26]

O. Shacham, E. Yahav, G. Gueta, A. Aiken, N. Bronson, M. Sagiv, and M. Vechev. Verifying atomicity via data independence. In ISSTA, 2014.

Digital Library

[27]

N. Shavit. Data structures in the multicore age. CACM, 2011.

Digital Library

[28]

O. Tripp, R. Manevich, J. Field, and M. Sagiv. Janus: exploiting parallelism via hindsight. In PLDI, 2012.

Digital Library

[29]

O. Tripp and N. Rinetzky. Tightfit: Adaptive parallelization with foresight. In ESEC/FSE, 2013.

Digital Library

[30]

O. Tripp, G. Yorsh, J. Field, and M. Sagiv. Hawkeye: effective discovery of dataflow impediments to parallelization. In OOPSLA, 2011.

Digital Library

[31]

P.vCerný, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, and T. Tarrach. Efficient synthesis for concurrency by semantics-preserving transformations. In CAV, 2013.

Digital Library

[32]

M. T. Vechev and E. Yahav. Deriving linearizable fine-grained concurrent objects. In PLDI, 2008.

Digital Library

[33]

D. Weeratunge, X. Zhang, and S. Jaganathan. Accentuating the positive: Atomicity inference and enforcement using correct executions. In OOPSLA, 2011.

Digital Library

[34]

J. Yu and S. Narayanasamy. Tolerating concurrency bugs using transactions as lifeguards. In MICRO, 2010.

Digital Library

[35]

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.

Digital Library

Cited By

Al‐Mahfoudh MStutsman RGopalakrishnan G(2023)Efficient linearizability checking for actor‐based systemsSoftware: Practice and Experience10.1002/spe.325153:11(2163-2199)Online publication date: 22-Aug-2023
https://doi.org/10.1002/spe.3251
Chakraborty SDing YAllamanis MRay B(2022)CODIT: Code Editing With Tree-Based Neural ModelsIEEE Transactions on Software Engineering10.1109/TSE.2020.302050248:4(1385-1399)Online publication date: 1-Apr-2022
https://doi.org/10.1109/TSE.2020.3020502
Fu HWang ZChen XFan X(2018)A systematic survey on automated concurrency bug detection, exposing, avoidance, and fixing techniquesSoftware Quality Journal10.1007/s11219-017-9385-326:3(855-889)Online publication date: 1-Sep-2018
https://dl.acm.org/doi/10.1007/s11219-017-9385-3
Show More Cited By

Index Terms

Flint: fixing linearizability violations
1. Computing methodologies
  1. Concurrent computing methodologies
    1. Concurrent programming languages
2. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Concurrent programming languages

Recommendations

Flint: fixing linearizability violations
OOPSLA '14: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications

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, ...
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 Engineering

In 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 49, Issue 10

OOPSLA '14

October 2014

907 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2714064

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

OOPSLA '14: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications
October 2014
946 pages
ISBN:9781450325851
DOI:10.1145/2660193
General Chair:
Andrew Black
Portland State University, USA
,
Program Chair:
Todd Millstein
University of California, Los Angeles, USA

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 October 2014

Published in SIGPLAN Volume 49, Issue 10

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
275
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Al‐Mahfoudh MStutsman RGopalakrishnan G(2023)Efficient linearizability checking for actor‐based systemsSoftware: Practice and Experience10.1002/spe.325153:11(2163-2199)Online publication date: 22-Aug-2023
https://doi.org/10.1002/spe.3251
Chakraborty SDing YAllamanis MRay B(2022)CODIT: Code Editing With Tree-Based Neural ModelsIEEE Transactions on Software Engineering10.1109/TSE.2020.302050248:4(1385-1399)Online publication date: 1-Apr-2022
https://doi.org/10.1109/TSE.2020.3020502
Fu HWang ZChen XFan X(2018)A systematic survey on automated concurrency bug detection, exposing, avoidance, and fixing techniquesSoftware Quality Journal10.1007/s11219-017-9385-326:3(855-889)Online publication date: 1-Sep-2018
https://dl.acm.org/doi/10.1007/s11219-017-9385-3
Tian YRay BBodden ESchäfer WDeursen AZisman A(2017)Automatically diagnosing and repairing error handling bugs in CProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3106300(752-762)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3106300
Lesani MXia LKaseorg ABell CChlipala APierce BZdancewic S(2022)C4: verified transactional objectsProceedings of the ACM on Programming Languages10.1145/35273246:OOPSLA1(1-31)Online publication date: 29-Apr-2022
https://dl.acm.org/doi/10.1145/3527324
Çirisci BEnea CFarzan AMutluergil S(2020)Root Causing Linearizability ViolationsComputer Aided Verification10.1007/978-3-030-53288-8_17(350-375)Online publication date: 14-Jul-2020
https://doi.org/10.1007/978-3-030-53288-8_17
Tian YRay BBodden ESchäfer WDeursen AZisman A(2017)Automatically diagnosing and repairing error handling bugs in CProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3106300(752-762)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3106300
Cai YCao LZhao JBodden ESchäfer WDeursen AZisman A(2017)Adaptively generating high quality fixes for atomicity violationsProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3106239(303-314)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3106239
Liu HChen YLu SZimmermann TCleland-Huang JSu Z(2016)Understanding and generating high quality patches for concurrency bugsProceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2950290.2950309(715-726)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1145/2950290.2950309
Zhang MWu YLu SQi SRen JZheng W(2016)A Lightweight System for Detecting and Tolerating Concurrency BugsIEEE Transactions on Software Engineering10.1109/TSE.2016.253166642:10(899-917)Online publication date: 1-Oct-2016
https://dl.acm.org/doi/10.1109/TSE.2016.2531666
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents