Towards generating thread-safe classes automatically
- 21 December 2020
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM) in Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering
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.Keywords
Funding Information
- Key-Area Research and Development Program of Guangdong Province (2018B010107004)
- National Natural Science Foundation of China (61872263, U1836214, 61802275)
- Intelligent Manufacturing Special Fund of Tianjin (20191012, 20193155)
- Innovation Research Project of Tianjin University (2020XZC-0042, 2020XRG-0022)
This publication has 40 references indexed in Scilit:
- ÆminiumACM Transactions on Programming Languages and Systems, 2014
- The VerCors Tool for Verification of Concurrent ProgramsLecture Notes in Computer Science, 2014
- Abstract Read Permissions: Fractional Permissions without the FractionsLecture Notes in Computer Science, 2013
- VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and JavaLecture Notes in Computer Science, 2011
- A Basis for Verifying Multi-threaded ProgramsPublished by Springer Science and Business Media LLC ,2009
- Practical API Protocol Checking with Access PermissionsLecture Notes in Computer Science, 2009
- Verification of Concurrent Programs with ChaliceLecture Notes in Computer Science, 2009
- Inferring locks for atomic sectionsACM SIGPLAN Notices, 2008
- Lock allocationACM SIGPLAN Notices, 2007
- Software transactional memoryDistributed Computing, 1997