* Type-Based Race Detection for Java
* Authors: Cormac Flanagan and Stephen N. Freund
* Field: Compilers/StaticChecking
* Reference: Programming Language Design and Implementation, June 2000
* Theme: Annotations can be used to statically check for race conditions.

* Implementation: Implemented on a simplified subset of Java which is
type-safe.  Requires many annotations -- annotate each field with the
lock that protects it, each method with the locks held upon calling
it.  Some common cases are included to reduce the number of
annotations required.

* Examples: Caught several race conditions in Java libraries.

* Problems: No assurance of complete correctness (they assume a
"programming discipline" that is admittedly often followed but not
necessarily.  What if the system uses different semantics for locking?
Annotations are a problem.  A more global analysis can remove lots of
the annotations.

* Razor: (pithy author's opinion/observation from paper)

* Take: Not user-extensible, but interesting that this method caught
real bugs.  It *might* be applicable to other systems, especially if
they follow the same locking discipline used by the Java libraries,
but that is not always the case.  May be that they designed this too
closely to fit Java library code?