Contract4J and My Annotations

When I was looking up some basic theory on method preconditions today, just to make sure that my notion that preconditions act in a covariant way, I discovered an interesting piece of software: Contract4J.

It only works together with AspectJ, an aspect-oriented programming framework for Java, but seems to support convenient ways to specify pre- and postconditions for methods, fields, and classes. These conditions are much more extensive than what my annotations do. It seems like Contract4J allows programmers to specify a string of Java code that may include a few extra things, so it basically corresponds to the fourth option I considered but decided would be too difficult to implement. I think the aspect-oriented framework with their cuts made it easier to insert the source code than it would have been for plain Java, which is what I’m dealing with.

I’d love to eventually provide some support for strings like this, even if it’s just a way to replace the syntax for @Combine annotations, which I think is rather clunky, even though I believe it’s the best I can do without resorting to my own parsing. It would just be nice if I could replace the current way to combine annotations:

1
2
3
4
5
@Combine(value=Combine.Mode.AND, arguments=true)
public static @interface TestDistinctNotNullGreater {
    TestDistinctNotNull distinctNotNull() default @TestDistinctNotNull;
    TestGreater gt() default @TestGreater;
}

with something like this:

1
2
@Combine("@TestDistinctNotNull && @TestGreater")
public static @interface TestDistinctNotNullGreater { }

But then again it wouldn’t be a full-fledged annotation, and I couldn’t override the default behavior. But maybe I don’t even want that.

Right now, I think my implementation is very reasonable and very cost-effective. But maybe I should add postconditions too. They’d act covariantly; that could yield some more interesting theory.

Talking of theory: I’ve realized that it’s not only the @NotRunBy annotations that should act in a contravariant way and that can be used to statically detect problems with the concurrency invariants. That’s true for all annotations, as long as you assume that the annotations make the preconditions stricter. With @NotRunBy it’s easy to see that it makes the preconditions stricter, but @OnlyRunBy does the same, except in a much more radical way: It may very well reduce the allowed number of threads to just one, or even zero. Ignoring regular expressions, I could even prove this. Now, with predicate annotations, I can’t prove jack, but it’s still reasonable to make the assumption that an annotation makes a precondition stricter (or at least not less strict).

The result is that my subtyping relation can be applied to all the annotations that I provide in my library. That’s good.

Oh, while at the lab today, I also fixed a strange but pretty critical bug in DrJava: [ 1696060 ] Debugger Infinite Loop. Again, I heavily relied on the YourKit Java profiler to get an idea where DrJava gets stuck. After the first YourKit run, I realized that DrJava was deadlocking here:

java.awt.EventQueue.invokeAndWait(Runnable)
edu.rice.cs.util.swing.Utilities.invokeAndWait(Runnable)
edu.rice.cs.drjava.model.AbstractGlobalModel.setActiveDocument(OpenDefinitionsDocument)
edu.rice.cs.drjava.model.AbstractGlobalModel.openFile(FileOpenSelector)
edu.rice.cs.drjava.model.AbstractGlobalModel.getDocumentForFile(File)
edu.rice.cs.drjava.model.debug.jpda.JPDADebugger.scrollToSource(Location,
boolean)
edu.rice.cs.drjava.model.debug.jpda.JPDADebugger.scrollToSource(Location)
edu.rice.cs.drjava.model.debug.jpda.JPDADebugger._switchToSuspendedThread(boolean)
edu.rice.cs.drjava.model.debug.jpda.JPDADebugger._switchToSuspendedThread()
edu.rice.cs.drjava.model.debug.jpda.JPDADebugger.currThreadSuspended()
edu.rice.cs.drjava.model.debug.jpda.EventHandlerThread._handleStepEvent(StepEvent)
edu.rice.cs.drjava.model.debug.jpda.EventHandlerThread.handleEvent(Event)
edu.rice.cs.drjava.model.debug.jpda.EventHandlerThread.run()

The interesting thing about the call to setActiveDocument is that here it is not happening in the event thread, so the invokeAndWait uses Java’s original method, so the code gets put in the event queue. It looks like the event that is blocking the event queue is DebugPanel.updateData(). Somehow because it does not complete, the code from setActiveDocument never gets to run, and we have a deadlock.

In the end, I realized that the deadlock was a result of the debugger thread, already owning the lock
of the debugger, asking the global model to open a file, so setActiveDocument put code on the event queue. When this code executed, the event thread tried to call a synchronized method of the debugger, but never managed to acquire its lock, because the debugger thread already owned it.

I changed the code to have the debugger thread “preload” a document every time a step is made, before claiming the debugger lock. This brings setActiveDocument into action and the document is opened if necessary. Then the debugger lock is claimed and the response to the step is made, and the document is guaranteed to be open already, so the deadlock is avoided. The fix is in revision 4225.

YourKit does a lot for a developer. I have to admit, though, that it takes some skill to interpret the flood of information, and I’m thinking I’m getting better at it.

PS: Because in COMP 312 we were talking about some problems with Java’s very low-level implementation of concurrency tools, I again brought up an article that I had read a while ago. It’s “If I were king: A proposal for fixing the Java programming language’s threading problems” by Allen Holub. We briefly tossed around the ideas of acquiring several locks at the same time and the issues that brings up. I think all the problems can be avoided by the very common solution to the Dining Philosopher’s Problem: Putting locks in some arbitrary but fixed order, and then always acquiring them in that order. The world is very small: I just learned that Dr. Nguyen attended a seminar with Allen Holub and thus knows him first-hand.

Share

About Mathias

Software development engineer. Principal developer of DrJava. Recent Ph.D. graduate from the Department of Computer Science at Rice University.
This entry was posted in Concurrent Unit Testing, DrJava. Bookmark the permalink.

Leave a Reply