CSAIL Research Abstracts - 2005 link to http://publications.csail.mit.edu/abstracts/abstracts05/index.html link to http://www.csail.mit.edu
bullet Introduction bullet Architecture, Systems
& Networks
bullet Language, Learning,
Vision & Graphics
bullet Physical, Biological
& Social Systems
bullet Theory bullet

horizontal line

Javari: Adding Reference Immutability to Java

Matthew S. Tschantz, Pramook Khungurn, Adrian Birka & Michael D. Ernst

What

We have developed a type system that is capable of expressing and enforcing immutability constraints. The specific constraint expressed is that the abstract state of the object to which an immutable reference refers cannot be modified using that reference. The abstract state is (part of) the transitively reachable state: that is, the state of the object and all state reachable from it by following references. The type system permits explicitly excluding fields or objects from the abstract state of an object. For a statically type-safe language, the type system guarantees reference immutability. If the language is extended with immutability downcasts, then run-time checks enforce the reference immutability constraints.

This research builds upon previous research in language support for reference immutability [1]. Improvements we are adding to the previous system include distinguishing the notions of assignability and mutability; integration with Java 5's generic types and with multi-dimensional arrays; a mutability polymorphism approach to avoiding code duplication; type-safe support for reflection and serialization; and formal type rules and a type soundness proof for a core calculus. Furthermore, the system retains the valuable features of the previous dialect, including usability by humans (as evidenced by experience with 160,000 lines of Javari code) and interoperability with Java and existing JVMs. Although there already exists a compiler for the previous dialect, we are in the process of implementing a new, more robust compiler for the current version of Javari.

Why

The Javari type system provides support for the enforcement of reference immutability. A type system enforcing reference immutability has a number of benefits: it can increase expressiveness; it can enhance program understanding and reasoning by providing explicit, machine-checked documentation; it can save time by preventing and detecting errors that would otherwise be very difficult to track down; and it can enable analyses and transformations that depend on compiler-verified properties. Below are several examples of Javari being used to enforce immutability constraints.

Method specifications describe both what a method must do and what it must not do. For instance, a method contract may state that the method does not modify some of its arguments. For example, consider a voting system containing the following routine:

  ElectionResults tabulate(Ballots votes) { ... } 

The users of tabulate would like the specification to state that the routine will not modify its argument. This specification can be enforced by the Javari compiler by declaring votes to be read-only.

  ElectionResults tabulate(readonly Ballots votes) {
    ...  // cannot tamper with the votes
  }

Accessor methods often return data that already exists as part of the representation of the module. For example, consider the Class.getSigners method, which returns the entities that have digitally signed a particular implementation. In JDK 1.1.1, its implementation is approximately:

  class Class {
    private Object[] signers;
    Object[] getSigners() { 
      return signers; 
    }
  }

This is a security hole, because a malicious client can call getSigners and add elements to the signers array, which is part of the class's internal representation.

Javari permits the following solution:

  class Class {
    private Object[] signers;
    readonly Object[] getSigners() {
      return signers; 
    }
  }

The readonly keyword ensures that the caller of Class.getSigners cannot modify the returned array, thus permitting the simple and efficient implementation of the method to remain in place without exposing the representation to undesired changes.

An alternate solution to the getSigners problem, which was actually implemented in later versions of the JDK, is to return a copy of the array signers [2]. This works, but is slower, more error-prone, and harder to reason about. Furthermore, in some cases it may be prohibitively expensive for an accessor to copy a field before returning it to a client.

How

Javari's type system differs from previous proposals (for Java, C++, and other languages) in a number of ways. First, it offers reference, not object, immutability; reference immutability is more flexible, as it provides useful guarantees even about code that manipulates mutable objects. For example, many objects are modified during a construction phase but not thereafter. As another example, an interface can specify that a method that receives an immutable reference as a parameter does not modify the parameter through that reference, or that a caller does not modify a return value. Furthermore, a subsequent analysis can strengthen reference immutability into stronger guarantees, such as object immutability, where desired.

Second, Javari offers guarantees for the entire transitively reachable state of an object -- the state of the object and all state reachable by following references through its (non-static) fields. A programmer may use the type system to support reasoning about either the representation state of an object or its abstract state; in order to support the latter, parts of a class can be marked as not part of its abstract state.

Javari allows references to be declared immutable with the readonly keyword. Additionally, a programmer may declare that a field is not a part of an object's abstract state and, thus, modifiable through read-only references, with the assignable and mutable keywords. A field that is declare to be assignable may always be assigned to, even through read-only references. A field that is declared mutable may always be mutated even through read-only references.

Javari is compatible with generic types allows programmers to declare the type arguments to a parameterized type to be read-only or mutable. For example, a programmer may declare lists with the following four types:

  /*mutable*/ List </*mutable*/ Date> ld1; // add/remove, mutate
  /*mutable*/ List <readonly    Date> ld2; // add/remove
  readonly    List </*mutable*/ Date> ld3; // mutate
  readonly    List <readonly    Date> ld4; // (neither)
Progress

We have created formal rules for the semantics of Javari; however, a type system is of limited interest if programmers cannot effectively use it. In the absence of experience using an implementation, the practicality of previous proposals is speculative.

To test the usefulness of the type system, we created a compiler for a previous dialect of Javari. Using this compiler, we obtained experience with Javari by writing code in it, as well as by annotating Java code with readonly to convert it to Javari. In total, we have over 160,000 lines of Javari code, including the Javari compiler itself. Additionally, Javari revealed over two dozen real errors in well-tested code.

Given the benefits of an actual compiler implementation, we are currently implementing a new, more robust Javari compiler for the current dialect of the language. Additionally, we are implementing other tools to support Javari, including a JVM byte-code verifier and an automated tool to infer read-only constraints in previously written Java code.

Research Support

This work was supported in part by NSF grants CCR-0133580 and CCR-0234651, DARPA contract FA8750-04-2-0254, and gifts from IBM and Microsoft.

References:

[1] Adrian Birka and Michael D. Ernst. A practical type system and language for reference immutability. In Object-Oriented Programming Systems, Languages, and Applications, pp. 35-49, Vancouver, British Columbia, Canada, October 2004.

[2] Joshua Bloch. Effective Java Programming Language Guide. Addison Wesley, Boston, MA, 2001.

horizontal line

MIT logo Computer Science and Artificial Intelligence Laboratory (CSAIL)
The Stata Center, Building 32 - 32 Vassar Street - Cambridge, MA 02139 - USA
tel:+1-617-253-0073 - publications@csail.mit.edu
(Note: On July 1, 2003, the AI Lab and LCS merged to form CSAIL.)