A Type System for Preventing Data Races and Deadlocks in the Java Virtual Machine Language

In previous work on SafeJava the authors presented a type system extension to the Java source language that statically prevents data races and deadlocks in multi-threaded programs. SafeJava is expressive enough to support common programming patterns, its type checking is fast and scalable, and it requires little programming overhead. SafeJava thus offers a promising approach for making multi-threaded programs more reliable. This paper presents a corresponding type system extension for the Java Virtual Machine Language (JVML). They call the resulting language SafeJVML. Well-typed SafeJVML programs are guaranteed to be free of data races and deadlocks.