Concurrent programs are notorious for containing errors that are difficult to reproduce and diagnose at run-time. This motivated the development of type systems that statically ensure the absence of some common kinds of concurrent programming errors. This paper presents Extended Parameterized Atomic Java (EPAJ), a type system for specifying and verifying atomicity of methods in multi-threaded Java programs. Atomicity is a common correctness requirement for concurrent programs which requires that concurrent invocations of a set of methods be equivalent to performing the invocations serially in some order. EPAJ combines Flanagan and Qadeer's atomicity types with a new and significantly more expressive type system for analyzing data races, called Extended Parameterized Race-Free Java (EPRFJ), allowing a more accurate analysis of atomicity. The paper also presents a type discovery algorithm to automatically obtain EPRFJ types, and a static interprocedural type inference algorithm that, given EPRFJ types, infers atomicity types. These algorithms can be incorporated into testing and debugging tools, benefiting users who know nothing about type systems. We report our experience with a prototype implementation.
Details of the type system and soundness proof for the core type system.