Automated type-based analysis of data races and atomicity

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 including data races and atomicity violations. A method is atomic if every execution of the concurrent program is equivalent to an execution in which the atomic method is executed without being interleaved with other concurrently executed methods. Atomicity is a common correctness requirement in concurrent programs; atomicity violations may indicate incorrect synchronization. This paper presents Extended Parameterized Atomic Java (EPAJ), a type system for specifying and verifying atomicity in Java programs. EPAJ combines Flanagan and Qadeer’s atomicity types [11] 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 at...

• Type: Conference
• Year: 2005
• Where: PPOPP
• Authors: Amit Sasturkar, Rahul Agarwal, Liqiang Wang, Scott D. Stoller
• Keywords: Atomicity Violations, Concurrent Programs, Distributed And Parallel Computing, PPOPP 2005, Type Systems