2025/04/23 by Li, Zhuang, Yi, Qiuping, Huang, Jeff
#FOS: Computer and information sciences #Software Engineering (cs.SE)
paper · doi:10.48550/arxiv.2504.16354
Atomicity violation is one of the most serious types of bugs in concurrent programs. Synchronizations are commonly used to enforce atomicity. However, it is very challenging to place synchronizations correctly and sufficiently due to complex thread interactions and large input space. This paper presents \textsfVeriFix, a new approach for verifying atomicity violation fixes. Given a buggy trace that exposes an atomicity violation and a corresponding fix, % in the form of locks, \textsfVeriFix effectively verifies if the fix introduces sufficient synchronizations to repair the atomicity violation without introducing new deadlocks. The key idea is that \textsfVeriFix transforms the fix verification problem into a property verification problem, in which both the observed atomicity violation and potential deadlocks are encoded as a safety property, and both the inputs and schedules are encoded as symbolic constraints. By reasoning the conjoined constraints with an SMT solver, \textsfVeriFix systematically explores all reachable paths %from the whole schedule and input space and verifies if there exists a concrete schedule+input combination to manifest the intended atomicity or any new deadlocks. We have implemented and evaluated \verifix on a collection of real-world C/C++ programs. The result shows that \textsfVeriFix significantly outperforms the state-of-the-art.