VeriFix: Verifying Your Fix Towards An Atomicity Violation

TL;DR

VeriFix addresses the challenging problem of verifying atomicity-violation fixes in concurrent programs by turning fix verification into safety-property checking and encoding both program behavior and the intended atomicity (and potential deadlocks) as symbolic constraints solved by an SMT solver. It introduces a constraint-based, parallel path-exploration framework that systematically enumerates schedule+input combinations across the whole input and schedule space, generating concrete executions to verify the fix or reveal insufficient synchronizations and deadlocks. The key contributions include a formal fix-verification formulation, a detailed constraint encoding for one trace (including atomicity and deadlock constraints), and a parallel exploration algorithm with path-prefix guidance, demonstrated to outperform state-of-the-art approaches on real-world C/C++ programs and in conjunction with APR tools. VeriFix thus provides a practical, scalable method to validate concurrency fixes, enabling reliable repair workflows and safer concurrent software deployment.

Abstract

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 \textsf{VeriFix}, 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, \textsf{VeriFix} effectively verifies if the fix introduces sufficient synchronizations to repair the atomicity violation without introducing new deadlocks. The key idea is that \textsf{VeriFix} 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, \textsf{VeriFix} systematically explores all reachable paths %from the whole schedule and input space and verifies if there exists a concrete \textit{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 \textsf{VeriFix} significantly outperforms the state-of-the-art.

Figures (10)

• Figure 1: SLING Bug-2812. The insufficient synchronization using a object field (handler), which is always different for different objects, to synchronize the codes. It will make the global object (handlerMap) broken. The incorrect fix for this issue wasn't identified until two years later.
• Figure 2: An atomicity violation in Aget, which occurs when $U_3$ is interleaved by $U_1$ or $U_2$.
• Figure 3: The motivating example with three fixes (fix1—the black statements, fix2—the blue statements, and fix3—the blue and red statements). An atomicity violation between lines 6-7 can be exposed by a buggy trace $\tau_0 = \{16-17,19-25,1-3, 5-6, 11-15, 7\}$ with input $i = 2$, $j = 1$.
• Figure 4: Overview of VeriFix.
• Figure 5: The lock-event graph for the trace $\tau_{0}$ in Figure \ref{['fig:movitation']}.

Theorems & Definitions (3)

• Definition 1
• Definition 2
• Definition 3