Type inference for atomicity

13 years 5 months ago
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.
Cormac Flanagan, Stephen N. Freund, Marina Lifshin
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where TLDI
Authors Cormac Flanagan, Stephen N. Freund, Marina Lifshin
Comments (0)