Type inference for parameterized race-free Java

Abstract

We study the type system introduced by Boyapati and Rinard in their paper “A Parameterized Type System for Race-Free Java Programs” and try to infer the type annotations (“lock types”) needed by their type checker to show that a program is free of race conditions. Boyapati and Rinard automatically generate some of these annotations using default types and static inference of lock types for local variables, but in practice, the programmer still needs to annotate on the order of 1 in every 25 lines of code. We use run-time techniques, based on the lockset algorithm, in conjunction with some static analysis to automatically infer most or all of the annotations.