A Concurrent Affair

Today I finished generalizing the annotations that pass method arguments as arrays and provide OnlySynchronizedArgument, NotSynchronizedArgument, OnlyNullArgument, NotNullArgument annotations, and perhaps something more unusual, NumberBoundedArgument, along with the matching Any, All and None combinations.

Just like all the annotations named above, NumberBoundedArgument lets you specify the index of the argument you want checked, and then it lets you select several modes:

• LESS, i.e. arg < bound
• LESS_EQ, i.e. arg <= bound
• GREATER, i.e. arg > bound
• GREATER_EQ, i.e. arg >= bound
• IN, i.e. (arg > bound) && (arg < upperBound)
• IN_EQ, i.e. (arg >= bound) && (arg <= upperBound)
• OUT, i.e. (arg < bound) || (arg > upperBound)
• OUT_EQ, i.e. (arg <= bound) || (arg >= upperBound)

where arg is the argument being compared, bound is one of the bounds (either the upper bound for LESS, LESS\_EQ, IN, and IN\_EQ; or upper bound for GREATER and GREATER\_EQ), and upperBound is the upper bound for IN, IN\_EQ, GREATER and GREATER\_EQ.

I decided to use bound both as upper and lower bound for those annotations that only use one bound as that was less confusing. Otherwise, I'd have to remember whether I set ubound or lbound for LESS.

I have also finished XML importing and exporting so that it supports passing arguments, and I fixed a bug that didn't properly join predicate annotations if the invariant was repeated several times.

I also improved violation reporting: If method arguments are passed, then the actual values will also appear in the violation log.

Consider the following nice program that uses NumberBoundedArgument:

package sample.threadCheck.predicate;
import edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument;
public class TCSample17 {
public static void main(String[] args) {
TCSample17 o = new TCSample17();
System.out.println("main!");
o.succeeds();
o.fails();
System.out.println("end main!");
}

@NumberBoundedArgument(mode=NumberBoundedArgument.Mode.OUT,
index = 0, bound = 0, upperBound = 2)
void outEx(int i) {
System.out.println("outEx, i = "+i);
}
}

When executed, it produces the following log file:

========================================
Log opened 2007-03-05, 02:44:17 CST (GMT-5)
----------------------------------------
Thread Predicate Violation: (9 checks, 1 violation)
	Current thread 'main', id 1, group 'main'
	Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument
	Method arguments
		'2' : java.lang.Integer
	at sample.threadCheck.predicate.TCSample17.lt (TCSample17.java:43)
	at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:31)
	at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)
----------------------------------------
Thread Predicate Violation: (10 checks, 2 violations)
	Current thread 'main', id 1, group 'main'
	Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument
	Method arguments
		'2' : java.lang.Integer
	at sample.threadCheck.predicate.TCSample17.ltEq (TCSample17.java:48)
	at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:32)
	at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)
----------------------------------------
Thread Predicate Violation: (11 checks, 3 violations)
	Current thread 'main', id 1, group 'main'
	Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument
	Method arguments
		'-1' : java.lang.Integer
	at sample.threadCheck.predicate.TCSample17.gt (TCSample17.java:53)
	at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:33)
	at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)
----------------------------------------
Thread Predicate Violation: (12 checks, 4 violations)
	Current thread 'main', id 1, group 'main'
	Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument
	Method arguments
		'-2' : java.lang.Integer
	at sample.threadCheck.predicate.TCSample17.gtEq (TCSample17.java:58)
	at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:34)
	at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)
----------------------------------------
Thread Predicate Violation: (13 checks, 5 violations)
	Current thread 'main', id 1, group 'main'
	Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument
	Method arguments
		'1' : java.lang.Integer
	at sample.threadCheck.predicate.TCSample17.in (TCSample17.java:63)
	at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:35)
	at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)
----------------------------------------
Thread Predicate Violation: (14 checks, 6 violations)
	Current thread 'main', id 1, group 'main'
	Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument
	Method arguments
		'1' : java.lang.Integer
	at sample.threadCheck.predicate.TCSample17.inEx (TCSample17.java:68)
	at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:36)
	at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)
----------------------------------------
Thread Predicate Violation: (15 checks, 7 violations)
	Current thread 'main', id 1, group 'main'
	Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument
	Method arguments
		'2' : java.lang.Integer
	at sample.threadCheck.predicate.TCSample17.out (TCSample17.java:73)
	at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:37)
	at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)
----------------------------------------
Thread Predicate Violation: (16 checks, 8 violations)
	Current thread 'main', id 1, group 'main'
	Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument
	Method arguments
		'0' : java.lang.Integer
	at sample.threadCheck.predicate.TCSample17.outEx (TCSample17.java:78)
	at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:38)
	at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)

This is a lot more informative than it used to be.

Ok, during the last day and a bit, I changed my completely working implementation of passing method arguments. Before, there was one argument in the predicate method for each argument in the method that was annotated. That limited the applicability of the annotations. Now I pass an Object[] array that can be empty, contain one element, or however many. The coolest thing is that it automatically takes care of the subtyping problem.

Here are rewritten predicates and annotations from the last post:

public class TCSample14 {
public static class CheckSynchronized {
public static boolean check(
Object thisObject, Object args[], int value) {
if (value>=args.length) return false;
return ThreadCheckPredicates.checkMonitorOwned(args[value]);
}
public static boolean checkNot(
Object thisObject, Object args[], int value) {
if (value>=args.length) return false;
return !ThreadCheckPredicates.checkMonitorOwned(args[value]);
}
}

@NotSynchronized(1)
void notBinary2nd(Object o1, Object o2) {
System.out.println("notBinary2nd");
}
}

Now I think this is pretty cool. It even auto-boxes primitive types to their boxed types. Now I’m just running some more tests, and then it’s time to sleep.

PS: Whatever happened to Beer Bike today?

When I tried to extend the arguments=true capabilities to XML files, I ran into a small problem: All I wanted to save was “true” or “false”, but what I needed was the method signature. I didn’t want to put that into the XML file.

So I decided to change my — by now beautifully working engine — again and pass an Object array. That means the array has to be created and populated, and primitives have to be beoxed, but at leaast that way an annotation applies to a method regardless of its numbers and types of parameters.

Once I’m done with this, a simple “true” or “false” in the XML file should suffice.

I just noticed that ThreadCheckPredicateCheckTest fails at and after changelist 892, but succeeds at and before changelist 891, so I’ll be looking at the changes I made. Now I need to get ready for the noon seminar.

Update

The problem had to do with the numbering of auto-generated parameter names when arguments are not passed.

Of course, once you’ve found the cause of an error, it’s too tempting not to fix it, so I did fix it before I biked to Rice, and I was 10 minutes late to the seminar. Just in time ;)

I was just going to look at how to make the arguments=true facility accessible to XML files, but so far I haven’t been able to figure it out. It seems so easy, just add a property to the node: <predicate arguments="true">. Unfortunately, the XML only contains the definition of the predicate, but what I really need here is the signature of the method the predicate will be applied to, i.e. something like “IILjava/lang/String;”.

So I decided to ignore that issue for a while and focus on the other things that need to be done:

• @Combine-style annotations
• reflection-based code
• accept a predicate method if the classes of the arguments are all superclasses of the classes actually passed

That’s when I noticed another limitation: I don’t think I can pass arguments for the reflection-based Thread Checker. At least not easily. The reflection-based Thread Checker has one method, and it gets called with the class and method name of the predicate it is supposed to invoke. If I were to pass the method’s arguments, then that method would have to have an arbitrary number of signatures. Of course I could use an array of Object, but then I’d have to convert primitive types to objects, so I decided to ditch that issue for now, too. (@Update: Now that I am passing an array of Object, of course I can support reflection.@)

As for allowing superclasses in the predicate method: Am I going to implement full-blown Java method invocation conversion? Ugh.

To quote the JLS, from 5.3 Method Invocation Conversion:

Method invocation conversion is applied to each argument value in a method or constructor invocation (§8.8.7.1, §15.9, §15.12): the type of the argument expression must be converted to the type of the corresponding parameter. Method invocation contexts allow the use of one of the following:

• an identity conversion (§5.1.1)
• a widening primitive conversion (§5.1.2)
• a widening reference conversion (§5.1.5)
• a boxing conversion (§5.1.7) optionally followed by widening reference conversion
• an unboxing conversion (§5.1.8) optionally followed by a widening primitive conversion.

If, after the conversions listed above have been applied, the resulting type is a raw type (§4.8), an unchecked conversion (§5.1.9) may then be applied. It is a compile time error if the chain of conversions contains two parameterized types that are not not in the subtype relation.

If the type of an argument expression is either float or double, then value set conversion (§5.1.13) is applied after the type conversion:

• If an argument value of type float is an element of the float-extended-exponent value set, then the implementation must map the value to the nearest element of the float value set. This conversion may result in overflow or underflow.
• If an argument value of type double is an element of the double-extended-exponent value set, then the implementation must map the value to the nearest element of the double value set. This conversion may result in overflow or underflow.

If, after the type conversions above have been applied, the resulting value is an object which is not an instance of a subclass or subinterface of the erasure of the corresponding formal parameter type, then a ClassCastException is thrown.

From 8.4.8.3 Requirements in Overriding and Hiding:

It is a compile time error if a type declaration T has a member method m1 and there exists a method m2 declared in T or a supertype of T such that all of the following conditions hold:

• m1 and m2 have the same name.
• m2 is accessible from T.
• The signature of m1 is not a subsignature (§8.4.2) of the signature of m2.
• m1 or some method m1 overrides (directly or indirectly) has the same erasure as m2 or some method m2 overrides (directly or indirectly).

And from 8.4.2 Method Signature:

It is a compile-time error to declare two methods with override-equivalent signatures (defined below) in a class.

Two methods have the same signature if they have the same name and argument types.

Two method or constructor declarations M and N have the same argument types if all of the following conditions hold:

• They have the same number of formal parameters (possibly zero)
• They have the same number of type parameters (possibly zero)
• Let be the formal type parameters of M and let be the formal type parameters of N. After renaming each occurrence of a Bi in N’s type to Ai the bounds of corresponding type variables and the argument types of M and N are the same.

The signature of a method m1 is a subsignature of the signature of a method m2 if either

• m2 has the same signature as m1, or
• the signature of m1 is the same as the erasure of the signature of m2.

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.

Some time this morning, after seeing the results of the conversion to concurrency definition-based XML files, I had the idea of trying to turn the project to gather all information about Java’s concurrency invariants into a community effort.

I first thought I’d create a database, but then I decided I’d use what I know best: A WordPress blog. So now I’m hosting another blog, called the Concutest Community Project at http://community.concutest.org/

The idea is that anyone can register and write posts describing concurrency invariants. The posts can be sorted into categories based on the kind of invariants and the package the class is in. Other people can comment on the validity of the posts or use a 5-star gadget to rate the quality, and every once in a while, I’ll go through the posts, verify the information, and generate a new version of the Java API database.

Since the information is categorized by invariant and package, it’s also easier to browse and find concurrency invariants for classes a developer uses.

We’ll see how it goes.

During the night I looked after a person who I care about a lot who seemed to have suffered from a strange drug interaction of nose spray and inhaler. He said he felt like he wasn’t himself, he felt slow, and I was really worried. I spent probably an hour and a half Googling the different medications, trying to find some interaction. My guess is that there just was a weird interaction between a vasodilator and a vasoconstrictor (@A friend in medical school confirmed this to a degree: If the nose spray actually makes it into the lungs, it could constrict blood vessels there and make an asthma attack worse.@). There was one disturbing comment about the nose spray causing severe CNS depression in children, so even when he seemed to be sleeping, I just wanted to be safe and woke him up a couple of times.

I’ve implemented most of what seems like the import code for XML concurrency definitions. I’ve also written a tool that checks the validity of the XML files, and I’ve enhanced my unit test suite for XMLConfig. I haven’t actually tested whether XML concurrency definitions get instrumented as checks, and I’m too sleepy for now. I actually feel loopy. I should probably take my cough medicine and go to bed.

I’ve realized that, in order to maximize code-reuse, I’ll have to change the XML format for the concurrency definition again. In the past, the XML node for the annotation didn’t have any child nodes that described classes or methods; in the proposed format, the classes and methods would be the child nodes. This wouldn’t really be a problem with the example I’ve used so far, but predicate annotations are more complex, and I don’t want to mess with them. It would make it more difficult to implement, so I’m taking the easy way out and proposing the following syntax:

All I’ve done is add the invariant node, which will contain the annotation. That means the three valid child nodes for a <threadcheck:def> node are invariant, class, and method, and there needs to be at least one invariant node and at least one of the other two node types. Very simple.