Research Abstracts - 2007

Background

Javari is an extension to Java that allows the use of type qualifiers to specify reference immutability [1][2]. A type qualifier annotation, @ReadOnly, specifies that a reference cannot be used to mutate the object to which it points. A complementary annotation, @Mutable, explicitly states that a reference can be used for mutation. For example, consider the following method signature:

void foo(@ReadOnly Date roDate, @Mutable Date mutDate)

Within the body of foo, the reference roDate cannot be used for mutation, but the reference mutDate can be used for mutation.

A mutation is defined as any Java statement that changes the abstract state of an object. The abstract state of an object is defined as the union of the abstract state of all its fields, and the abstract state of a primitive value is simply the primitive value itself.

To indicate whether calling a certain method changes the abstract state of its receiver, the receiver can be annotated @ReadOnly. Consider the following:

int getValue() @ReadOnly { ... }
void setValue(int newValue) @Mutable { ... }

The method getValue() is specified to not be able to change the abstract state of its receiver, whereas the method setValue() can modify its receiver.

Problem

Existing Java code is not annotated with reference immutability qualifiers. For backwards compatibility, in Javari, any unannotated types default to @Mutable. Therefore, existing libraries cannot be called from Javari. Consider the following simple class that holds an Object:

public class ObjectHolder {
	private Object o;
	
	public int getValue() @ReadOnly {
		return o.hashCode();
	}
}

Calling the method getValue() on an ObjectHolder reference does not modify the abstract state of the receiver, and so the @ReadOnly annotation should be correct. However, because the Object.hashCode() method is not annotated, it defaults to having an @Mutable receiver. Therefore, the call o.hashCode() is seen as modifying the object o, and thus the method getValue() is seen as mutating its abstract state, so the @ReadOnly annotation causes a type error.

This problem of existing class files not being annotated with reference immutability is similar to Java 1.4 code not using generics. In order for generic Java 1.5 code to use existing Java 1.4 code, tools can be used to automatically infer generic type arguments to existing class files [3]. We need a tool to automatically the infer reference immutability of existing class files.

Inference algorithm

Creating a set of sound type qualifiers is simple; if every reference is @Mutable, then everything typechecks. However, we also want an inference that is complete; changing any set of @Mutable references to @ReadOnly will result in the code not typechecking. Furthermore, we also want an inference that results in a set of type qualifiers that the user finds useful.

The basic approach of our static inference algorithm is to assume every reference is @ReadOnly. Then, for every mutation that occurs within a method, we mark that method as @Mutable, and then propagate the fact that this method leads to a mutation throughout the rest of the system. For example, consider trying to infer the reference immutability of the following classes:

// Simple wrapper for an int value
public class IntCell {
	private int i;

	public int get() {
		return i;
	}	

	public void set(int i) {
		this.i = i;
	}
}

// A Counter that keeps track of a count.
public class Counter {
	private IntCell iCell;

	public int getCount() {
		return iCell.get();
	}

	public void reset() {
		iCell.set(0);
	}

	public void transferCount(IntCell c) {
		c.set(getCount());
	}
}

Initially, every reference is marked as @ReadOnly. Examining the body of IntCell.get() does not find any mutations. However, examining the body of IntCell.set() does find a mutatation, so the receiver has to be marked @Mutable. Propagating this mutation, since IntCell.set() mutates its receiver, and Counter.reset() calls this method on one of its fields, then Counter.reset() also mutates its reciever. Similarly, Counter.transferCount() calls the method IntCell.set() on its parameter c, and so this parameter must be a @Mutable reference. The receiver of Counter.transferCount() remains @ReadOnly, as do all other reference because there was no mutation found that could be performed on them.

Partial results

We have implemented this inference algorithm to work over Java class files using Soot and ASM. Soot provides a very nice intermediate representation of class files and particularly of statements within a method body, while ASM provides convenient access to read various elements of a class file. In our experience, our current implementation works over all Java 1.4 code. That is, it is complete for code that does not use generics. Although the above example with IntCell and Counter is rather simple, it actually demonstrates most of the logic behind the inference algorithm. Other uses involving more complicated programming constructs are analogous. For example, consider being able to write an anonymous class if IntCell was an interface:

public interface IntCell {
	public int get();
	public void set(int i);
}

public class Container {
	private IntCell iCell;

	public IntCell getIntCell() {
	   final int startValue = 2;
		return new IntCell() {
				private int i = startValue;
				
				public int get() {
					return i;
				}

				public void set(int i) {
					this.i = i;
				}
			};
	}
}

The inference algorithm works the same for this last example as in the first example. The mutability of the return type of Container.getIntCell() depends on whether any mutable methods get called on the returned object, and the anonymous class is analyzed just like any other class. If the anonymous class had the potential to mutate the Container object that encloses it, then the Container.getIntCell() method have to annotate its receiver @Mutable. The tool that implements the inference algorithm works on all the complicated constructs such as these that we have seen, excluding generics.

This inference tool also works on many uses of generics. For example, consider the declaration:

ArrayList<@ReadOnly Date> myList = ...

The inference tool is aware that the return type of myList.get(0) returns an @ReadOnly Date, and not just a Date reference. The inference tool also enforces the subtyping rules of Javari. One of these rules is that the mutability of a method's receiver must be the same in all methods that overwrite it. Thus, consider the following:

public class A {
	public void foo() { ... }
}

public class B extends A {
	public void foo() { ... }
}

In this case, our tool infers that the receivers of A.foo() and B.foo() have the same mutability. Further subtyping rules, such as ensuring that the parameter mutabilities in overriding methods match, are also fully implemented.

Our inference tool is also able to infer mutability of generic arguments. For example, if you have:

public class Cell < T extends Date > {
	public void foo(T t) {
		t.setTime(0);
	}
} 

The current implementation is able to recognize that the type argument T should be @Mutable T.

One construct that the current implementation is unable to recognize is when a generic class creates an anonymous class within a method, and the anonymous class is also generic and creates another anonymous generic class within one of its methods. These type of complicated constructs are not presently supported.

Future work

One piece of future work is to improve the analysis of casts. Consider the following use of a parameter:

void foo(Date d) {
	@Mutable Date mutDate = (@Mutable Date) d;
	// ... modify mutDate ...
}

Presenly, the parameter d is inferred as @Mutable, because it cannot be @ReadOnly without leaving an unchecked cast. However, one could also say that the cast would not have been written at all unless the programmer intended the parameter to be @ReadOnly, perhaps to agree with a supertype's method signature for foo.

Another potential improvement is to extend the tool to allow programmers to specifically annotate only part of a class, and have the tool infer the rest. Presently, the tool accepts each class as either being unannotated or being fully annotated (with @Mutable being the default for unannotated elements). However, in cases where a method is not yet implemented, or when a programmer wants a particular element to be annotated @Mutable in order to make the API for a class more flexible, a user may want to insert a few annotations into the code, and have our tool infer the rest of the annotations in a way that agrees with the few user-provided annotations.

References:

[1] Matthew Tschantz. Adding Reference Immutability to Java. Master's Thesis, Massachusetts Institute of Technology. August 2006.

[2] Danny Coward and Michael Ernst. JSR 308: Annotations on Java Types. http://jcp.org/en/jsr/detail?id=308 , October 17, 2006. JSR Review Ballot version.

[3] Alan Donovan, Adam Kiezun, Matthew S. Tschantz, and Michael D. Ernst. Converting Java programs to use generic libraries. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2004), (Vancouver, BC, Canada), October 26-28, 2004, pp. 15-34.