When I was writing simple Java examples that may be problematic, even with Thread Checker annotations in place, I noticed two annotations that were still missing.
The general problem I was describing is a result of subclassing: If a method of a superclass A was written one way, there is no guarantee that a subclass B extends A doesn’t change the behavior. Or, more indirectly, an instance of a subclass may be passed as a parameter, which could alter the behavior of a method call to it.
For the second case, it is very difficult to write predicate annotations right now, because there’s no direct access to method arguments. I guess I could change the link between annotations and predicates and not only pass this as first parameter, but pass all other arguments as well. That probably wouldn’t be very difficult to implement, but it would limit an annotation to a particular method signature. Perhaps I could specify which, if any, arguments should be passed… I’ll have to mull this over. Right now, this doesn’t have very high priority for me.
Another annotation that may be useful would be an @SuppressSubtypingWarning annotation. In some cases, for example when implementing Runnable.run or overriding Object.toString, it may be useful to specify invariants without getting the static subtyping warnings that would normally be generated, since both methods are first introduced higher up in the hierarchy without invariants. But again, this doesn’t have very high priority right now. For now, I’ll just require programmers to manually ignore the warnings.
What is a little disappointing is the realization that these two problems can only be avoided if programmers consistently annotate their concurrency invariants. If a method makes a call to an unannotated, carelessly written method, or an annotated class is extended but the invariants not correctly adapted, all bets are off.
