Type Discovery for Parameterized Race-Free Java
Abstract
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 read-only 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 10, 2004
- Accession Number
- ADA580699
Entities
People
- Amit Sasturkar
- Rahul Agarwal
- Scott D. Stoller
Organizations
- Stony Brook University