A Method for Predicting Two-variable Atomicity Violations

As the most common non-deadlock concurrency bugs, atomicity violations are extremely hard to detect during testing since the exhaustive testing of a multi-threaded program is impossible because of the large number of interleavings. The studies in recent years have mainly focused on single-variable atomicity violation. However, those methods are unable to predict or find atomicity violations with multiple variables involved. Many variables are inherently correlated and need to be accessed together with their correlated peers in a consistent manner. These variables need to be either updated together consistently or accessed together to avoid inconsistent update or reading. This paper presents a method for predicting two-variable atomicity violation, based on access correlation between variables and atomicity violation pattern of variable accesses, including algorithms to infer access correlation between variables and to predict atomicity violation using model checking. The effectiveness of our method is evaluated with several real-world systems.