Type Discovery for Parameterized Race-Free Java
Rahul Agarwal and Amit Sasturkar and Scott D. Stoller

Concurrent programs are notorious for containing data races that are difficult to reproduce and diagnose at run-time. This inspired the development of type systems that statically ensure the absence of data races. Boyapati and Rinard's Parameterized Race Free Java (PRFJ) is an extension of Java with such a type system. We give the first complete formal presentation of PRFJ; Boyapati and Rinard's paper gives only an informal sketch of an important part of the type system, namely, support for readonly objects and objects referenced by a unique pointer. We present a new method for producing the type annotations needed by the type checker to show that a program is race-free. This approach, called type discovery, uses a combination of run-time monitoring and static analysis to automatically obtain most of the annotations. We study the expressiveness of the type system and efficacy of type discovery on several programs. In our experiments, type discovery reduced the number of annotations that need to be supplied by the programmer to about 1.9 annotations/KLOC. In Boyapati and Rinard's experiments, the programmer needed to supply about 25 annotations/KLOC.

BibTeX    PDF