@OnlyRunBy Subtyping

I just looked at the subtyping warnings generated from the normal @OnlyRunBy (before-predicate) annotations, and they definitely a bit weird. Not necessarily wrong, but perhaps not what I really want.

Let’s assume there are three classes, Super, which is extended by Mid, which is extended by Sub. Super has an @OnlyRunBy annotation, which affects all methods in all three classes. Sub has an @OnlyRunBy that affects only its own new method, fum(). The method Sub.bar() also has a @OnlyRunBy annotation.

@OnlyRunBy(@ThreadDesc(name="main"))
class Super {
public void foo() { }
}

@OnlyRunBy(@ThreadDesc(name="another"))
class Sub extends Mid {
public void fum() { }
@OnlyRunBy(@ThreadDesc(name="auxiliary"))
public void bar() { }
}

Super.foo() may only be run by the “main” thread. The same applied to Mid.bar(): It may only be run by the “main” thread.

Now it gets weird: Sub.fum() may only be run by a thread whose name is both “main” and “another”. That’s probably not what the programmer intended… The programmer might have wanted to relax the requirement and allow the threads “main” or “another”.

And now we currently get a subtyping warning: Sub.bar() may only be run by a thread whose name is both “main” and “auxiliary”, and here the method in the subclass has stricter prerequisites than the method in the superclass, so a subtyping warning is generated.

Technically, with my current implementation of combining the annotations using and, the warning is correct. However, my contention is that someone using @OnlyRunBy probably wants to relax the prerequisites, and that would mean adding @OnlyRunBy in subclasses is ok. What should generate a warning is if an @OnlyRunBy annotation in a subclass is present, but it is somehow removed in a superclass. That’s not how my current system works. Subclasses and methods in subclasses get annotations from superclasses and methods in superclasses, but not the other way around.

What would probably be the right thing is this:

• Annotations that restrict preconditions should be passed on from superclass to subclass, and if a subclass introduces a stricter precondition that the superclass doesn’t have, a warning should be generated.
• Annotatons that relax preconditions should be passed from subclass to superclass, and if a superclass has such a relaxed precondition that the subclass does not have, a warning should be generated.

That means that restricting annotations should be covariant, and relaxing annotations should be contravariant. If the annotations are found in a different way, that’s an error in the threading discipline.

Unfortunately, I don’t really know how to write this. How do I decide what gets combined using and (restricting) and what using or (relaxing)? With the user-written predicate annotations, I can’t assume which behavior is wanted because I can’t possibly figure out if a user-written Java method serving as predicate makes the preconditions stricter or more relaxed, so the user would have to pick covariant or contravariant behavior when writing the annotation. That’s not hard, but again, right now I don’t know how to combine them.

I’ll have to talk to Corky if my intuition here is right and if that should go into my current code (which would cause quite a delay), if that should just go as theory into my thesis, or if I’m completely on the wrong path here.

I don’t think I am, though, because these warnings provide static checks for the maintenance of a threading discipline in the use of extensible libraries, something that I consider one of the greatest, if not the greatest, current challenge in software engineering.