Consistency Checking for Refactoring from Coarse-grained locks to Fine-grained locks

Refactoring for locks is widely used to improve the scalability and performance of concurrent programs. However, when refactoring from coarse-grained locks to fine-grained locks, the behavior of concurrent programs may be changed. To this end, we present LockCheck, a consistency-checking approach based on the parallel extended finite automaton for fine-grained locks. First, we model the critical sections of concurrent programs through control flow analysis and dependency analysis. Second, we sequentialize the concurrent programs to get all the possible transition paths. Furthermore, it reduces the exploration of the redundant paths using partial order theory to obtain the compared transition paths. Finally, we combine consistency rules to check the consistency of the program before and after refactoring. We evaluated LockCheck in five open-source projects. A total of 1528 refactoring operations have been evaluated and 93 inconsistent refactoring operations have been detected. The results show that LockCheck can effectively detect inconsistent behavior when coarse-grained locks are refactored into fine-grained locks.