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 and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs. General Terms: Languages, Verification, Reliability.

• Type: Conference
• Year: 2005
• Where: TLDI
• Authors: Cormac Flanagan, Stephen N. Freund, Marina Lifshin
• Keywords: Formal Methods, Fundamental Correctness Property, Multithreaded Programs, TLDI 2005, Type Inference