This looks like interesting work, and I hope something like this gets
folded into a release soon. A few things occurred to me when reading
the writeup at google (sorry, I haven't started looking through the
code much yet):
All the examples seem to be C++ oriented; is it, in fact, a goal for
the annotations and analysis to be just as useful in C?
What are the scoping rules used for finding the mutex referenced in
the GUARDED_BY macro within a C++ class definition? Are they the same
as for looking up identifiers in other contexts? How is the lookup
done for C structures?
Will the compiler get built-in knowledge of the OS library routines
(e.g., pthread_mutex_lock) on various platforms?
You list separate annotations for "trylock" functions. It appears
that the difference is that "trylock" functions can fail. However,
pthread_mutex_lock can fail, if the mutex isn't properly initialized,
if recursive locking of a non-recursive mutex is detected, or other
reasons; the difference between pthread_mutex_lock and
pthread_mutex_trylock is whether it will wait or immediately return
EBUSY for a mutex locked by another thread. So I think
pthread_mutex_lock should be described as a "trylock" function too,
under your semantics. Conservatively written code will check for
errors, and will have a path in which the lock is assumed *not* to
have been acquired; if the analysis assumes pthread_mutex_lock always
succeeds, that path may be analyzed incorrectly. (I ran into a tool
once before that complained about my locking code until I added an
unlock call to the error handling path. Since it's actively
encouraging writing incorrect code, I'm not using it any more.)
Ken
