[Checkers] JCIP GuardedBy checker

Michael Ernst mernst at cs.washington.edu
Thu Jun 11 17:18:37 EDT 2009


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

 * 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

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.


More information about the checkers mailing list