Static detection of atomicity violations in object-oriented programs

Abstract

Violations of atomicity are possible sources of errors in parallel programs. A violation occurs if the effect of a method depends on the execution of concurrent threads that operate on the same shared data. Such unwanted thread interference can occur even if access to shared data is ordered through synchronization, hence common techniques for data race detection are not able to find such errors. We have developed a static analysis that infers atomicity constraints and identifies potential violations. The analysis is based on an abstract model of threads and data. A symbolic execution tracks object locking and access and provides information that is finally used to determine potential violations of atomicity. We provide a detailed evaluation of our algorithm for several Java programs. Although the algorithm does not guarantee to find all violations of atomicity, our experience shows that the method is efficient and effective in determining several known synchronization problems in a number of applications and the Java library. The problem of overreporting that is commonly encountered due to conservatism in static analyses is moderate.