RCCExplanation

The Race Condition Checker (RCC) was originally developed by researchers at the Digital Systems Research Lab (DEC-SRC) in the late 1990s (FF00). Its source code was released to the general public along with the source for Simplify, Javafe, ESC/Java, and Houdini.

RCC's purpose is to (conservatively) statically check for the absence of race conditions via analysis of (type) annotated Java source code. As RCC's analysis is sound, if an annotated Java program passes RCC, then it is guaranteed to have no race conditions.

As the Mobius PVE is meant to eventually support reasoning about concurrent Java systems, determining whether a Java module is race-free is a critical first step in verifying any other properties. Unfortunately, RCC's source code release barely compiled, and was completely unmaintained.

Consequently, MOBIUS developers have "revived" RCC and released RCC version 2. This updated version of RCC incorporates the evolution of the Java language semantics, as expressed within the third revision of the JLS (GJSB05) and as realized in Java version 5, particularly with respect to the the Java Memory Model (Con04). Moreover, several critical flaws in the original RCC type system and type checker were identified and corrected in this release.

Version: 1 Time: Fri Mar 28 18:16:06 2008 Author: dcochran (dcochran) IP: 193.1.132.32