A practical type system and language for reference immutability

ABSTRACT

This paper describes 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.

In order to better understand the usability and efficacy of the type system, we have implemented an extension to Java, called Javari, that includes all the features of our type system. Javari is interoperable with Java and existing JVMs. It can be viewed as a proposal for the semantics of the Java const keyword, though Javari's syntax uses readonly instead. This paper describes the design and implementation of Javari, including the type-checking rules for the language. This paper also discusses experience with 160,000 lines of Javari code. Javari was easy to use and provided a number of benefits, including detecting errors in well-tested code.

REFERENCES

• 1: Alex Aiken , Jeffrey S. Foster , John Kodumal , Tachio Terauchi, Checking and inferring local non-aliasing, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 2: Jonathan Aldrich , Valentin Kostadinov , Craig Chambers, Alias annotations for program understanding, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 3: David F. Bacon , Peter F. Sweeney, Fast static analysis of C++ virtual function calls, Proceedings of the 11th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.324-341, October 06-10, 1996, San Jose, California, United States
• 4: A. Birka. Compiler-enforced immutability for the Java language. Technical Report MIT-LCS-TR-908, MIT Laboratory for Computer Science, Cambridge, MA, June 2003. Revision of Master's thesis.
• 5: Joshua Bloch, Effective Java programming language guide, Sun Microsystems, Inc., Mountain View, CA, 2001
• 6: Chandrasekhar Boyapati , Barbara Liskov , Liuba Shrira, Ownership types for object encapsulation, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.213-223, January 15-17, 2003, New Orleans, Louisiana, USA
• 7: John Boyland , James Noble , William Retert, Capabilities for Sharing: A Generalisation of Uniqueness and Read-Only, Proceedings of the 15th European Conference on Object-Oriented Programming, p.2-27, June 18-22, 2001
• 8: Gilad Bracha , Martin Odersky , David Stoutamire , Philip Wadler, Making the future safe for the past: adding genericity to the Java programming language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.183-200, October 18-22, 1998, Vancouver, British Columbia, Canada
• 9: Jong-Deok Choi , Manish Gupta , Mauricio Serrano , Vugranam C. Sreedhar , Sam Midkiff, Escape analysis for Java, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.1-19, November 01-05, 1999, Denver, Colorado, United States
• 10: Jeffrey Dean , David Grove , Craig Chambers, Optimization of Object-Oriented Programs Using Static Class Hierarchy Analysis, Proceedings of the 9th European Conference on Object-Oriented Programming, p.77-101, August 07-11, 1995
• 11: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically discovering likely program invariants to support program evolution, Proceedings of the 21st international conference on Software engineering, p.213-224, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302467]
• 12: David Evans, Static detection of dynamic memory errors, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.44-53, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 13: Manuel Fahndrich , Robert DeLine, Adoption and focus: practical linear types for imperative programming, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 14: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
• 15: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 16: J. D. Gannon, An experimental evaluation of data type conventions, Communications of the ACM, v.20 n.8, p.584-595, Aug. 1977 [doi>10.1145/359763.359800]
• 17: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 18: Günter Kniesel , Dirk Theisen, JAC—access right based encapsulation for Java, Software—Practice & Experience, v.31 n.6, p.555-576, May 2001 [doi>10.1002/spe.372]
• 19: D. Lea. Personal communictation, Aug. 1, 2004.
• 20: X. Leroy. The Objective Caml system, release 3.07, Sept. 29, 2003. with Damien Doligez, Jacques Garrigue, Didier Rémy and Jérôme Vouillon.
• 21: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 22: Scott Meyers, Effective C++ CD, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1998
• 23: Robin Milner , Mads Tofte , Robert Harper, The Definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 24: J. H. Morris. Sniggering type checker experiment. Experiment at Xerox PARC, 1978. Personal communication, May 2004.
• 25: P. Müller and A. Poetzsch-Heffter. Universes: A type system for alias and dependency control. Technical Report 279, Fernuniversität Hagen, 2001.
• 26: Flemming Nielson , Hanne Riis Nielson, Type and Effect Systems, Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel), p.114-136, January 1999
• 27: Jens Palsberg, Type-based analysis and applications, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.20-27, June 2001, Snowbird, Utah, United States [doi>10.1145/379605.379635]
• 28: Young Gil Park , Benjamin Goldberg, Escape analysis on lists, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.116-127, June 15-19, 1992, San Francisco, California, United States
• 29: Igor Pechtchanski , Vivek Sarkar, Immutability specification and its applications, Proceedings of the 2002 joint ACM-ISCOPE conference on Java Grande, p.202-211, November 03-05, 2002, Seattle, Washington, USA [doi>10.1145/583810.583833]
• 30: Sara Porat , Marina Biberstein , Larry Koved , Bilha Mendelson, Automatic detection of immutable fields in Java, Proceedings of the 2000 conference of the Centre for Advanced Studies on Collaborative research, p.10, November 13-16, 2000, Mississauga, Ontario, Canada
• 31: Lutz Prechelt , Walter F. Tichy, A Controlled Experiment to Assess the Benefits of Procedure Argument Type Checking, IEEE Transactions on Software Engineering, v.24 n.4, p.302-312, April 1998 [doi>10.1109/32.677186]
• 32: Alexandru Salcianu , Martin Rinard, Pointer and escape analysis for multithreaded programs, Proceedings of the eighth ACM SIGPLAN symposium on Principles and practices of parallel programming, p.12-23, June 2001, Snowbird, Utah, United States
• 33: Gary T. Leavens , Sophia Drossopoulou , Susan Eisenbach , Arnd Poetzsch-Heffter , Erik Poll, Formal Techniques for Java Programs, Proceedings of the Workshops on Object-Oriented Technology, p.30-40, June 18-22, 2001
• 34: R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
• 35: Bjarne Stroustrup, The C++ Programming Language, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 36: J.-P. Talpin and P. Jouvelot. The type and effect discipline. In Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pages 162--173, Santa Cruz, CA, June 22-25 1992.
• 37: P. Wadler. Linear types can change the world! In IFIP TC 2 Working Conference on Programming Concepts and Methods, pages 347--359, Sea of Galilee, Israel, Apr. 1990.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.5 Object-oriented Programming

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Experimentation, Languages, Theory

Keywords:
Java, Javari, const, immutability, mutable, readonly, type system, verification