Cited By
View all- Misu MAchar RLopes C(2024)SourcererJBF: A Java Build Framework For Large-Scale CompilationACM Transactions on Software Engineering and Methodology10.1145/363571033:3(1-35)Online publication date: 15-Mar-2024
Towards generating thread-safe classes automatically
Authors: 
Haichi Wang, Zan Wang, Jun Sun, Shuang Liu, Ayesha Sadiq, Yuan-Fang LiAuthors Info & Claims
Abstract
The existing concurrency model for Java (or C) requires programmers to design and implement thread-safe classes by explicitly acquiring locks and releasing locks. Such a model is error-prone and is the reason for many concurrency bugs. While there are alternative models like transactional memory, manually writing locks remains prevalent in practice. In this work, we propose AutoLock, which aims to solve the problem by fully automatically generating thread-safe classes. Given a class which is assumed to be correct with sequential clients, AutoLock automatically generates a thread-safe class which is linearizable, and does it in a way without requiring a specification of the class. AutoLock takes three steps: (1) infer access annotations (i.e., abstract information on how variables are accessed and aliased), (2) synthesize a locking policy based on the access annotations, and (3) consistently implement the locking policy. AutoLock has been evaluated on a set of benchmark programs and the results show that AutoLock generates thread-safe classes effectively and could have prevented existing concurrency bugs.
References
[1]
Cormac Flanagan and Stephen N Freund. Fasttrack: efficient and precise dynamic race detection. In ACM Sigplan Notices, volume 44, pages 121--133. ACM, 2009.
[2]
Christoph Von Praun and Thomas R Gross. Static conflict analysis for multithreaded object-oriented programs. In ACM Sigplan Notices, volume 38, pages 115--128. ACM, 2003.
[3]
Shuang Liu, Guangdong Bai, Jun Sun, and Jin Song Dong. Towards using concurrent java api correctly. In 2016 21st International Conference on Engineering of Complex Computer Systems (ICECCS), pages 219--222. IEEE, 2016.
[4]
Kai Lu, Zhendong Wu, Xiaoping Wang, Chen Chen, and Xu Zhou. Racechecker: efficient identification of harmful data races. In 2015 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, pages 78--85. IEEE, 2015.
[5]
Dejan Perkovic and Peter J Keleher. Online data-race detection via coherency guarantees. In OSDI, volume 96, pages 47--57, 1996.
[6]
Pallavi Joshi, Chang-Seo Park, Koushik Sen, and Mayur Naik. A randomized dynamic program analysis technique for detecting real deadlocks. In ACM Sigplan Notices, volume 44, pages 110--120. ACM, 2009.
[7]
Chang-Seo Park and Koushik Sen. Randomized active atomicity violation detection in concurrent programs. In Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, pages 135--145. ACM, 2008.
[8]
Jeff Huang and Charles Zhang. Execution privatization for scheduler-oblivious concurrent programs. In ACM SIGPLAN Notices, volume 47, pages 737--752. ACM, 2012.
[9]
Guoliang Jin, Linhai Song, Wei Zhang, Shan Lu, and Ben Liblit. Automated atomicity-violation fixing. In ACM Sigplan Notices, volume 46, pages 389--400. ACM, 2011.
[10]
Guoliang Jin, Wei Zhang, and Dongdong Deng. Automated concurrency-bug fixing. In Presented as part of the 10th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 12), pages 221--236, 2012.
[11]
Peng Liu and Charles Zhang. Axis: Automatically fixing atomicity violations through solving control constraints. In 2012 34th International Conference on Software Engineering (ICSE), pages 299--309. IEEE, 2012.
[12]
Huarui Lin, Zan Wang, Shuang Liu, Jun Sun, Dongdi Zhang, and Guangning Wei. Pfix: fixing concurrency bugs based on memory access patterns. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, pages 589--600. ACM, 2018.
[13]
Bertrand Meyer. Applying'design by contract'. Computer, 25(10):40--51, 1992.
[14]
Wladimir Araujo, Lionel C Briand, and Yvan Labiche. Enabling the runtime assertion checking of concurrent contracts for the java modeling language. In Proceedings of the 33rd International Conference on Software Engineering, pages 786--795. ACM, 2011.
[15]
Mike Barnett, K Rustan M Leino, and Wolfram Schulte. The spec# programming system: An overview. In International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pages 49--69. Springer, 2004.
[16]
Nir Shavit and Dan Touitou. Software transactional memory. Distributed Computing, 10(2):99--116, 1997.
[17]
Lu Zhang, Arijit Chattopadhyay, and Chao Wang. Round-up: Runtime checking quasi linearizability of concurrent data structures. In 2013 28th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 4--14. IEEE, 2013.
[18]
Maurice P Herlihy and Jeannette M Wing. Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems (TOPLAS), 12(3):463--492, 1990.
[19]
Grande. Grande benchmark. https://www.epcc.ed.ac.uk/research/computing/performance-characterisation-and-benchmarking/java-grande-benchmark-suite.
[20]
Kevin Bierhoff and Jonathan Aldrich. Modular typestate checking of aliased objects, volume 42 of OOPSLA '07. ACM, 2007.
[21]
Nels E. Beckman, Kevin Bierhoff, and Jonathan Aldrich. Verifying correct usage of atomic blocks and typestate. In Proceedings of the 23rd ACM SIGPLAN Conference, OOPSLA '08, pages 227--244, 2008.
[22]
Brian Goetz, Tim Peierls, Doug Lea, Joshua Bloch, Joseph Bowbeer, and David Holmes. Java concurrency in practice. Pearson Education, 2006.
[23]
Autolock. https://github.com/autolock-anonymous/AutoLock, 2020.
[24]
Ayesha Sadiq, Yuan-Fang Li, Sea Ling, Li Li, and Ijaz Ahmed. Statically inferring permission-based specifications for sequential java programs. arXiv preprint arXiv:1902.05311, 2019.
[25]
A. Sadiq, L. Li, Y. Li, I. Ahmed, and S. Ling. Sip4j: Statically inferring access permission contracts for parallelising sequential java programs. In 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 1098--1101, 2019.
[26]
Ankit Choudhary, Shan Lu, and Michael Pradel. Efficient detection of thread safety violations via coverage-guided generation of concurrent tests. In 2017 IEEE/ACM 39th International Conference on Software Engineering (ICSE), pages 266--277. IEEE, 2017.
[27]
Haopeng Liu, Yuxi Chen, and Shan Lu. Understanding and generating high quality patches for concurrency bugs. In Proceedings of the 2016 24th ACM SIGSOFT international symposium on foundations of software engineering, pages 715--726. ACM, 2016.
[28]
Shan Lu, Soyeon Park, Eunsoo Seo, and Yuanyuan Zhou. Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In ACM SIGARCH Computer Architecture News, volume 36, pages 329--339. ACM, 2008.
[29]
Kevin Bierhoff, Nels E Beckman, and Jonathan Aldrich. Polymorphic fractional permission inference. 2009.
[30]
Kevin Bierhoff, Nels E Beckman, and Jonathan Aldrich. Practical api protocol checking with access permissions. In European Conference on Object-Oriented Programming, pages 195--219. Springer, 2009.
[31]
Stefan Heule, K Rustan M Leino, Peter Müller, and Alexander J Summers. Abstract read permissions: Fractional permissions without the fractions. In VM-CAI'13, pages 315--334, 2013.
[32]
Stefan Blom and Marieke Huisman. The vercors tool for verification of concurrent programs. In International Symposium on Formal Methods, pages 127--131. Springer, 2014.
[33]
jdk16. https://github.com/zxiaofan/JDK.
[34]
John Boyland. Checking Interference with Fractional Permissions. In Proceedings of the 10th International Conference on Static Analysis, SAS'03, pages 55--72. Springer-Verlag, 2003.
[35]
Kevin Bierhoff and Jonathan Aldrich. Plural: Checking protocol compliance under aliasing. In ICSE Companion '08, pages 971--972, 2008.
[36]
K. Rustan M Leino, Peter Müller, and Jan Smans. Verification of concurrent programs with chalice. In FOSAD 2007/2008/2009 Tutorial Lectures, pages 195--222. Springer Berlin Heidelberg, 2009.
[37]
K Rustan M Leino and Peter Müller. A basis for verifying multi-threaded programs. In European Symposium on Programming, pages 378--393. Springer, 2009.
[38]
Radu I. Siminiceanu, Ijaz Ahmed, and Néstor Cataño. Automated verification of specifications with typestates and access permissions. ECEASST, pages 1--15, 2012.
[39]
Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. VeriFast: A powerful, sound, predictable, fast verifier for C and java. In NASA Formal Methods Symposium, pages 41--55. Springer, 2011.
[40]
Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Viper: A verification infrastructure for permission-based reasoning. In Barbara Jobstmann and K. Rustan M. Leino, editors, Verification, Model Checking, and Abstract Interpretation, pages 41--62, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg.
[41]
Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Viper: A verification infrastructure for permission-based reasoning. In Dependable Software Systems Engineering. 2017.
[42]
Afshin Amighi, Stefan Blom, Marieke Huisman, and Marina Zaharieva-Stojanovski. The VerCors Project: Setting Up Basecamp. In Programming Languages meets Program Verification (PLPV 2012), 2012.
[43]
Marieke Huisman and Wojciech Mostowski. A symbolic approach to permission accounting for concurrent reasoning. In Proceedings - IEEE 14th International Symposium on Parallel and Distributed Computing, ISPDC 2015, 2015.
[44]
Stefan Blom, Saeed Darabi, Marieke Huisman, and Wytse Oortwijn. The vercors tool set: Verification of parallel and concurrent software. In Nadia Polikarpova and Steve Schneider, editors, Integrated Formal Methods, pages 102--110, Cham, 2017. Springer International Publishing.
[45]
Jonathan Aldrich, Robert Bocchino, Ronald Garcia, Mark Hahnenberg, Manuel Mohr, Karl Naden, Darpan Saini, Sven Stork, Joshua Sunshine, Éric Tanter, and Roger Wolff. Plaid: a permission-based programming language. In Proceedings of the ACM international conference companion on Object oriented programming systems languages and applications companion, pages 183--184. ACM, 2011.
[46]
Jonathan Aldrich, Nels E Beckman, Robert Bocchino, Karl Naden, Darpan Saini, Sven Stork, and Joshua Sunshine. The Plaid language: Typed core specification. Technical report, DTIC Document, 2012.
[47]
Sven Stork, Karl Naden, Joshua Sunshine, Manuel Mohr, Alcides Fonseca, Paulo Marques, and Jonathan Aldrich. Aeminium: A permission-based concurrent-by-default programming language approach. TOPLAS, 36(1):1--42, 2014.
[48]
Sam Blackshear, Nikos Gorogiannis, Peter W O'Hearn, and Ilya Sergey. Racerd: compositional static race detection. Proceedings of the ACM on Programming Languages, 2(OOPSLA):1--28, 2018.
[49]
Paul E McKenney and John D Slingwine. Read-copy update: Using execution history to solve concurrency problems. In Parallel and Distributed Computing and Systems, pages 509--518, 1998.
[50]
Jaeho Kim, Ajit Mathew, Sanidhya Kashyap, Madhava Krishnan Ramanathan, and Changwoo Min. Mv-rlu: Scaling read-log-update with multi-versioning. In Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, pages 779--792. ACM, 2019.
[51]
Alexander Matveev, Nir Shavit, Pascal Felber, and Patrick Marlier. Read-log-update: a lightweight synchronization mechanism for concurrent programming. In Proceedings of the 25th Symposium on Operating Systems Principles, pages 168--183. ACM, 2015.
[52]
Maurice Herlihy. A methodology for implementing highly concurrent data objects. ACM Transactions on Programming Languages and Systems (TOPLAS), 15(5):745--770, 1993.
[53]
Maurice Herlihy. Wait-free synchronization. ACM Transactions on Programming Languages and Systems (TOPLAS), 13(1):124--149, 1991.
[54]
Danny Dig, John Marrero, and Michael D Ernst. Refactoring sequential java code for concurrency via concurrent libraries. In Proceedings of the 31st International Conference on Software Engineering, pages 397--407. IEEE Computer Society, 2009.
[55]
Jiange Zhang, Qing Yi, and Damian Dechev. Automating non-blocking synchronization in concurrent data abstractions.
[56]
Michael Emmi, Jeffrey S Fischer, Ranjit Jhala, and Rupak Majumdar. Lock allocation. ACM SIGPLAN Notices, 42(1):291--296, 2007.
[57]
Bill McCloskey, Feng Zhou, David Gay, and Eric Brewer. Autolocker: synchronization inference for atomic sections. In Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 346--358, 2006.
[58]
Michael Hicks, Jeffrey S Foster, and Polyvios Pratikakis. Lock inference for atomic sections. In Proceedings of the First ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing, 2006.
[59]
Sigmund Cherem, Trishul Chilimbi, and Sumit Gulwani. Inferring locks for atomic sections. ACM SIGPLAN Notices, 43(6):304--315, 2008.
[60]
Michael Pradel, Markus Huggler, and Thomas R Gross. Performance regression testing of concurrent classes. In Proceedings of the 2014 International Symposium on Software Testing and Analysis, pages 13--25, 2014.
[61]
Soyeon Park, Shan Lu, and Yuanyuan Zhou. Ctrigger: exposing atomicity violation bugs from their hiding places. In ACM SIGARCH Computer Architecture News, volume 37, pages 25--36. ACM, 2009.
[62]
Yan Cai, Lingwei Cao, and Jing Zhao. Adaptively generating high quality fixes for atomicity violations. In Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, pages 303--314. ACM, 2017.
Index Terms
- Towards generating thread-safe classes automatically
Recommendations
Effectiveness and challenges in generating concurrent tests for thread-safe classes
ASE '18: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software EngineeringDeveloping correct and efficient concurrent programs is difficult and error-prone, due to the complexity of thread synchronization. Often, developers alleviate such problem by relying on thread-safe classes, which encapsulate most synchronization-...
Teaching students to develop thread-safe java classes
ITiCSE '08: Proceedings of the 13th annual conference on Innovation and technology in computer science educationConcurrent programming was once the preserve of experts writing systems internals; but recently the growing importance of application servers, and the excellent support in Java and C# for thread handling, has brought threads and locking as topics that ...
Freedom from Deadlock of Safe Locking Policies
The usual method for preserving the consistency of a database when accessed (read and updated) concurrently by several transactions, is by locking the transactions according to some locking policy; a locking policy that guarantees the preservation of ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
December 2020
1449 pages
ISBN:9781450367684
DOI:10.1145/3324884
- General Chair:
- John Grundy,
- Program Chairs:
- Claire Le Goues,
- David Lo
Copyright © 2020 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]
Sponsors
In-Cooperation
- IEEE CS
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 27 January 2021
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- Key-Area Research and Development Program of Guangdong Province
- National Natural Science Foundation of China
- Intelligent Manufacturing Special Fund of Tianjin
- Innovation Research Project of Tianjin University
Conference
ASE '20: 35th IEEE/ACM International Conference on Automated Software Engineering
December 21 - 25, 2020
Virtual Event, Australia
Acceptance Rates
Overall Acceptance Rate 82 of 337 submissions, 24%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 134Total Downloads
- Downloads (Last 12 months)14
- Downloads (Last 6 weeks)4
Reflects downloads up to 22 Dec 2024
Other Metrics
Citations
Cited By
View all- Misu MAchar RLopes C(2024)SourcererJBF: A Java Build Framework For Large-Scale CompilationACM Transactions on Software Engineering and Methodology10.1145/363571033:3(1-35)Online publication date: 15-Mar-2024
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in