On Jul 1, 12:13 am, Brian Goetz <
br...@briangoetz.com> wrote:
> While @GuardedBy was not designed explicitly for read-write locks, I would say
> the natural extension would be @GuardedBy("lock"), where "lock" is a
> read-write lock.
I agree. The equivalent annotations what we currently use in
SureLogic JSure do this. Where ever we would use a "java.lang.Object"
as a lock, we can also accept a "java.util.concurrent.locks.Lock" or a
"java.util.concurrent.ReadWriteLock".
> In the case below, you'd have to refactor to not throw away the lock object.
> Then, a static analyzer could determine that m_val is only touched with either
> the reader or writer locks of "lock" held.
Agreed. JSure would require this change.
> (In the general case, the analyzer
> would have to know what methods or operations are mutative to determine if the
> correct orientation of lock is held for the operation.)
Brian, I think you are over-complicating the answer here. Really the
analyzer just has to understand field read (o.f) and field assignment
(o.f = ...).
As you know, it depends on where you draw the line about lock
responsibility. I think we all agree that the normal line is that
unless annotated otherwise, a method acquires (and releases!) all the
locks it needs during execution. So you normally don't have to worry
about what lock you need when calling a method. In this case, the
only operations are field assignment and field read, with the obvious
locking semantics. A method that doesn't acquire the necessary lock
needs its own @GuardedBy annotation. The only thing the analyzer
needs to know here is which field writes occurred without a lock,
which field reads occurred without a lock, and then to map those
fields to the locks they are supposed have. No explicit effect system
is required. (Of course, an explicit one is certainly useful for this
and for other things.)