Research Abstracts - 2007

Overview

We describe 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 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. Improvements that are new to our work 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 type soundness proof for a core calculus. Furthermore, it 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.

Motivation

Reference immutability provides a variety of benefits in different situations. The following simple examples suggest a few uses of immutability constraints and give a flavor of the Javari language.

Consider a voting system containing the following routine:

  ElectionResults tabulate(Ballots votes) { ... }

It is necessary to safeguard the integrity of the ballots. This requires a machine-checked guarantee that the routine does not modify its input votes. Using Javari, the specification of tabulate could declare that votes is read-only:

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

and the compiler ensures that implementers of tabulate do not violate the contract.

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;
    }
  }

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.

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. This works, but is error-prone and expensive. For example, a file system may allow a client read-only access to its contents:

  class FileSystem {
    private List<Inode> inodes;
    List<Inode> getInodes() {
      ... // Unrealistic to copy
    }
  }

Javari allows the programmer to avoid the high cost of copying inodes by writing the return type of the method as:

    readonly List<readonly Inode> getInodes()

This return type prevents the List or any of its contents from being modified by the client. As with all parameterized classes, the client specifies the type argument, including whether it is read-only or not, independently of the parameterized typed.

A similar form of dangerous, mutation-permitting aliasing can occur when a data structure stores information passed to it (for instance, in a constructor) and a client retains a reference. Use of the readonly keyword again ensures that either the client's copy is read-only and cannot be modified, or else the data structure makes a copy, insulating it from changes performed by the client. In other words, the annotations force programmers to copy only when necessary.

As a final example, reference immutability can be used, in conjunction with a subsequent analysis, to establish the stronger guarantee of object immutability: a value is never modified, via any reference, if all references are immutable. For example, there is only one reference when an object is first constructed. As another simple example, some data structures must be treated as mutable when they are being initialized, but as immutable thereafter; an analysis can build upon Javari in order to make both the code and the reasoning simple.

  Graph g1 = new Graph();
  ... construct cyclic graph g1 ...
  // Suppose no aliases to g1 exist.
  readonly Graph g = g1;
  g1 = null;

Language design and further details

The full language design is laid out at the Javari website.

References:

[1] Matthew S. Tschantz and Michael D. Ernst. Javari: Adding reference immutability to Java. In Proceedings of OOPSLA 2005, pp. 211--230, San Diego, CA, USA, October 2005.