[Checkers] JCIP GuardedBy checker

[Michael Ernst]

Brian-

It was great to see you again last week, and to talk about a variety of
topics including concurrency, immutability, and the relationship between
static and dynamic typing.

Spurred by your encouragement and that of other people at JavaOne, we wrote
a checker for the JCIP GuardedBy annotation, as a type-checker built on the
Checker Framework.

It seems to me that the JCIP GuardedBy annotation is serving two different
purposes.

 * When applied to a field, it means that the given lock must be held when
   accessing the field.  The lock acquisition and the field access may be
   arbitrarily far in the future.
 * When applied to a method, it means that the given lock must be held by
   the caller at the time that the method is called -- in other words, at
   the time that execution passes the @GuardedBy annotation.

It's elegant that the same annotation name is used for two distinct but
closely related concepts.  However, this got in our way when writing a
checker.  The first meaning for GuardedBy can be viewed as a type
annotation that can appear on an arbitrary type (including the type of a
parameter, return value, local variable, generic type parameter, etc.).
The second one is a method annotation.  In order to prevent the two
meanings from conflicting with one another, we renamed the latter to
@Holding.

We've checked a couple of projects that already had a few @GuardedBy
annotations.  We found no errors with those particular annotations.  We
will look into additional projects.  The biggest difficulty with such a
case study is knowing what the intended locking semantics is.  If you have
projects where you know that information, we would be happy to try our
checker on your codebase.

                    -Mike