Research Abstracts - 2007

Introduction

Immutability information is useful in many software engineering tasks, such as modeling [2], verification [10], compile- and runtime optimizations [7], refactoring [5], test input generation [1], regression oracle creation [12], invariant detection [4], specification mining [3], and program comprehension [6]. Three important varieties of immutability guarantee are immutable classes, object immutability, and reference immutability.

No instance of an immutable class may be changed; examples in Java include String and all subclasses of Number including Integer and BigDecimal. Java's type system has no way of expressing or checking this property.

Object immutability guarantees that an object cannot be modified, even if other instances of the same class can be. For example, some instances of List in a given program may be immutable, whereas others can be modified. Object immutability gives strong guarantees that can be used for pointer analysis and optimizations, such as sharing between threads without synchronization.

Reference immutability [7, 8, 9, 11] guarantees that a given reference cannot be used to modify its referent. Such a system supports readonly references that have no mutating privileges, and mutable references that point to a mutable object and can call mutating methods. Reference immutability is required in order to specify interfaces, such as that a procedure may not modify its arguments (even if the caller retains the right to do so) or a client cannot modify values returned from a module. However, past work does not guarantee object immutability, unless the reference immutability is combined with an alias/escape analysis to guarantee that no aliases to an object exist.

Immutability Generic Java (IGJ)

This work develops a language extension of Java called Immutability Generic Java (IGJ) that supports both object immutability (an immutable reference points to an immutable object) and reference immutability (only mutable references can mutate an object). Each object is either mutable or immutable, and each reference is Immutable, Mutable, or ReadOnly. Inspired by work that combines ownership and generics [8], the distinctions are expressed without changing Java’s syntax by adding one new generic parameter (at the beginning of the list of generic parameters):
1: // An immutable reference to an immutable date
2: // Side effects are prohibited
3: Date<Immutable> immutD = new Date<Immutable>();
4: // A mutable reference to a mutable date
5: // Side effects are permitted
6: Date<Mutable> mutD = new Date<Mutable>();
7: // A readonly reference to any date
8: // Side effects are prohibited
9: Date<ReadOnly> roD = ... ? immutD : mutD;


IGJ is the first proposal for enforcing object immutability within Java’s syntax and type system, and its reference immutability is more expressive than previous work. IGJ also permits covariant changes of generic arguments in a type-safe manner, e.g., a readonly list of integers is a subtype of a readonly list of numbers. IGJ extends Java’s type system with a few simple rules. We formalize this type system and prove it sound. Our IGJ compiler generates byte-code that can be executed on any JVM without runtime penalty.

IGJ is designed to satisfy the following design principles:

1. Transitivity: The design must provide transitive (deep) immutability that protects the entire abstract state of an object. For example, an immutable graph can contain an immutable set of immutable edges. However, a transitive guarantee of immutability for all fields of an object may be too strong, thus it should be possible to exclude some fields from the abstract state. For example, fields used for caching can be mutated even in an immutable object.
2. Purely static: There should be no runtime representation for immutability, e.g., an "immutability bit" that is checked before assignments or method calls. The ability to test at runtime whether an object is immutable hampers program understanding.
3. Polymorphism: It must be possible to abstract over immutability without code duplication, e.g., it is possible to write a method expecting an argument that is either mutable or immutable. For instance, all the collection classes in C++'s STL have two overloaded versions of iterator, operator[], etc. The underlying problem is the inability to return a reference whose mutability depends on the mutability of this.
4. Simplicity: The design should not change Java's syntax and have a small set of typing rules. Phrased differently, the technique should not use rules which do not fit naturally into Java's design.

The following presents two IGJ classes:
1: class Edge<I extends ReadOnly> {
2:    private long id;
3:    @AssignFields Edge(long id) { this.setId(id); }
4:    @AssignFields synchronized void setId(long id) { this.id = id; }
5:    @ReadOnly synchronized long getId() { return id; }
6:    @Immutable long getIdImmutable() { return id; }
7:    static void print(Edge<ReadOnly> n) { ... }
8: }
9: class Graph<I extends ReadOnly> {
10:    Edge<I> lastN;
11:    List<I,Edge<I>> l;
12:    @AssignFields Graph(List<I,Edge<I>> l) { this.l = l; }
13:    @Mutable void addEdge(Edge<I> n) { this.l.add(n); this.lastN = n; }
14:    @ReadOnly Edge<I> getLast() { return this.lastN; }
15:    static <T extends ReadOnly> Edge<T> findEdge(Graph<T> nl, long id) { ... }
16: }
Erasing the immutability parameters/annotations from a legal IGJ program yields a legal Java program with same semantics. Thus, the program can be understood without the IGJ additions.

References:

[1] S. Artzi, M. D. Ernst, A. Kiezun, C. Pacheco, and J. H. Perkins. Finding the needles in the haystack: Generating legal test inputs for object-oriented programs. Technical Report MIT-CSAIL-TR-2006- 056, MIT CSAIL, Sept. 5, 2006.

[2] L. Burdy, Y. Cheon, D. Cok, M. D. Ernst, J. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of JML tools and applications. STTT, 7(3):212–232, June 2005.

[3] V. Dallmeier, C. Lindig, A. Wasylkowski, and A. Zeller. Mining object behavior with ADABU. In WODA, pages 17–24, May 2006.

[4] M. D. Ernst, J. Cockrell,W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE TSE, 27(2):99–123, Feb. 2001.

[5] M. Fowler. Refactoring: Improving the Design of Existing Code. Addison-Wesley, 2000.

[6] Jose Javier Dolado and Mark Harman and Mari Carmen Otero and Lin Hu. An empirical investigation of the influence of a type of side effects on program comprehension. IEEE TSE, 29(7):665–670, July 2003.

[7] I. Pechtchanski and V. Sarkar. Immutability specification and its applications. In Java Grande, pages 202–211, Nov. 2002.

[8] A. Potanin, J. Noble, D. Clarke, and R. Biddle. Generic ownership for generic Java. In OOPSLA, pages 311–324, Oct. 2006.

[9] M. Skoglund and T. Wrigstad. A mode system for read-only references in Java. In 3rd Workshop on Formal Techniques for Java Programs, June 18, 2001. Revised.

[10] O. Tkachuk and M. B. Dwyer. Adapting side effects analysis for modular program model checking. In ESEC/FSE, pages 188–197, Sept. 2003.

[11] M. S. Tschantz and M. D. Ernst. Javari: Adding reference immutability to Java. In OOPSLA, pages 211–230, Oct. 2005.

[12] T. Xie. Augmenting automatically generated unit-test suites with regression oracle checking. In ECOOP, pages 380–403, July 2006.