We have developed a lightweight Java annotation language that can be used to specify and check the threading invariants of both existing and new code.
More information and the source will be available soon.
The tclib.jar file contains only the class files necessary to add Thread Checker annotations to your program and specify thread invariants. They can then be treated more or less like comments. The tclib.jar file is small (35 kB, 47 class files) and can easily be included with other projects without increasing their size in an unreasonable fashion.
The tcrt.jar file, on the other hand, contains both the annotation classes necessary to specify thread invariants using annotations, the procesor to rewrite class files to check the specified invariants, and tools to find and analize violations of the specified invariants at runtime. The tcrt.jar file is quite large (734 kB, 617 class files), but only needs to be distributed to the developers who want to make use of the Thread Checker.
Here are instructions on how to use the annotation library tclib.jar, as well as the processor and runtime tools in tcrt.jar.
Here is a preliminary version of the subtyping relation the Thread Checker uses, based on Featherweight Java: