Abstract Type Inference For Atomicity

Atomicity is a fundamental correctness property in multithreaded programs. This paper presents an algorithm for verifying atomicity via type inference. The underlying type system supports guarded, write-guarded, and unguarded fields, as well as thread-local data, parameterized classes and methods, and protected locks. We describe an implementation of this algorithm for Java and discuss its performance and usability on benchmarks totaling sixty thousand lines of code. Categories and Subject Descriptors: D.2.4 [Software Engineering]: Software/Program Verification–reliability; F.3.1 [Logics an