Ownership, encapsulation and the disjointness of type and effect

ABSTRACT

Ownership types provide a statically enforceable notion of object-level encapsulation. We extend ownership types with computational effects to support reasoning about object-oriented programs. The ensuing system provides both access control and effects reporting. Based on this type system, we codify two formal systems for reasoning about aliasing and the disjointness of computational effects. The first can be used to prove that evaluation of two expressions will never lead to aliases, while the latter can be used to show the non-interference of two expressions.

REFERENCES

• 1: Martin Abadi , Luca Cardelli, A Theory of Objects, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 2: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 3: 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
• 4: Paulo Sergio Almeida. Balloon Types: Controlling sharing of state in data types. In ECOOP Proceedings, June 1997.
• 5: David F. Bacon , Robert E. Strom , Ashis Tarafdar, Guava: a dialect of Java without data races, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.382-400, October 2000, Minneapolis, Minnesota, United States
• 6: Henry G. Baker, “Use-once” variables and linear objects: storage management, reflection and multi-threading, ACM SIGPLAN Notices, v.30 n.1, p.45-52, Jan. 1995 [doi>10.1145/199818.199860]
• 7: Anindya Banerjee , David A. Naumann, Representation independence, confinement and access control [extended abstract], Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.166-177, January 16-18, 2002, Portland, Oregon
• 8: Bruno Blanchet, Escape analysis for object-oriented languages: application to Java, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.20-34, November 01-05, 1999, Denver, Colorado, United States
• 9: Jan Vitek , Boris Bokowski, Confined types, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.82-96, November 01-05, 1999, Denver, Colorado, United States
• 10: James Gosling , Greg Bollella, The Real-Time Specification for Java, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 11: Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 12: Chandrasekhar Boyapati , Martin Rinard, A parameterized type system for race-free Java programs, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.56-69, October 14-18, 2001, Tampa Bay, FL, USA
• 13: John Boyland, Alias burying: unique variables without destructive reads, Software—Practice & Experience, v.31 n.6, p.533-553, May 2001 [doi>10.1002/spe.370]
• 14: John Boyland. The interdependence of effects and uniqueness. In 3rd Workshop on Formal Techniques for Java Programs, June 2001.
• 15: 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
• 16: Ciarin Bryce and Chrislain Razafimahefa. An approach to safe object sharing. In OOPSLA Proceedings, October 1999.
• 17: Edwin C. Chan , John T. Boyland , William L. Scherlis, Promises: limited specifications for analysis and manipulation, Proceedings of the 20th international conference on Software engineering, p.167-176, April 19-25, 1998, Kyoto, Japan
• 18: Zhiqun Chen, Java Card Technology for Smart Cards: Architecture and Programmer's Guide, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 19: David Clarke. An object calculus with ownership and containment. In Foundations of Object oriented Programming (FOOL8), London, January 2001. Available from
• 20: David Gerard Clarke, Object ownership and containment, 2003
• 21: David G. Clarke , James Noble , John Potter, Simple Ownership Types for Object Containment, Proceedings of the 15th European Conference on Object-Oriented Programming, p.53-76, June 18-22, 2001
• 22: David G. Clarke , John M. Potter , James Noble, Ownership types for flexible alias protection, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.48-64, October 18-22, 1998, Vancouver, British Columbia, Canada
• 23: Karl Crary , David Walker , Greg Morrisett, Typed memory management in a calculus of capabilities, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.262-275, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292564]
• 24: Frank S. de Boer, A WP-calculus for OO, Proceedings of the Second International Conference on Foundations of Software Science and Computation Structure, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, p.135-149, March 22-28, 1999
• 25: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 26: David L. Detlefs, K. Rustan M. Leino, and Greg Nelson. Wrestling with rep exposure. Technical Report SRC-RR-98-156, Compaq Systems Research Center, July 1998.
• 27: Amer Diwan , Kathryn S. McKinley , J. Eliot B. Moss, Type-based alias analysis, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.106-117, June 17-19, 1998, Montreal, Quebec, Canada
• 28: Cormac Flanagan , Martín Abadi, Types for Safe Locking, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.91-108, March 22-28, 1999
• 29: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 30: Aaron Greenhouse , John Boyland, An Object-Oriented Effects System, Proceedings of the 13th European Conference on Object-Oriented Programming, p.205-229, June 14-18, 1999
• 31: Dan Grossman , Greg Morrisett , Trevor Jim , Michael Hicks , Yanling Wang , James Cheney, Region-based memory management in cyclone, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 32: John Hogg, Islands: aliasing protection in object-oriented languages, Conference proceedings on Object-oriented programming systems, languages, and applications, p.271-285, October 06-11, 1991, Phoenix, Arizona, United States
• 33: John Hogg , Doug Lea , Alan Wills , Dennis deChampeaux , Richard Holt, The Geneva convention on the treatment of object aliasing, ACM SIGPLAN OOPS Messenger, v.3 n.2, p.11-16, April 1992 [doi>10.1145/130943.130947]
• 34: Stuart Kent and John Howse. Value types in Eiffel. In TOOLS 19, Paris, 1996.
• 35: Gunter Kniesel and Dirk Theisen. JAC -- Java with transitive readonly access control. In Intercontinental Workshop on Aliasing in Object-Oriented Systems, At ECOOP'99, Lisbon, Portugal, June 1999.
• 36: Gary T. Leavens and Olga Antropova. ACL --- eliminating parameter aliasing with dynamic dispatch. Technical Report 98-08a, Department of Computer Science, Iowa State University, Ames, Iowa, 50011, February 1999.
• 37: Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A notation for detailed design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds, editors, Behavioral Specifications of Businesses and Systems, pages 175--188. Kluwer Academic Publishers, Boston, 1999.
• 38: K. Rustan M. Leino, Data groups: specifying the modification of extended state, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.144-153, October 18-22, 1998, Vancouver, British Columbia, Canada
• 39: 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]
• 40: B. J. MacLennan, Values and objects in programming languages, ACM SIGPLAN Notices, v.17 n.12, December 1982 [doi>10.1145/988164.988172]
• 41: Naftaly H. Minsky, Towards Alias-Free Pointers, Proceedings of the 10th European Conference on Object-Oriented Programming, p.189-209, July 08-12, 1996
• 42: G. Morrisett , R. Harper, Semantics of memory management for polymorphic languages, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 43: P. Muller. Modular Specification and Verification of Object-Oriented Programs. PhD thesis, FernUniversitat Hagen, 2001.
• 44: P. Muller and A. Poetzsch-Heffter. Universes: A type system for controlling representation exposure. In A. Poetzsch-Heffter and J. Meyer, editors, Programming Languages and Fundamentals of Programming. Fernuniversitat Hagen, 1999.
• 45: Peter Muller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular specification of frame properties in JML. Technical Report TR-02-02, Department of Computer Science, Iowa State University, February 2002.
• 46: Flemming Nielson , Hanne R. Nielson , Chris Hankin, Principles of Program Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 47: James Noble , Jan Vitek , John Potter, Flexible Alias Protection, Proceedings of the 12th European Conference on Object-Oriented Programming, p.158-185, July 20-24, 1998
• 48: Martin Odersky and Christoph Zenger. Nested types. In Foundations of Object-oriented Programming (FOOL8), London, January 2001. Available from http://www.cs.williams.edu/~kim/FOOL/FOOL8.html.
• 49: J. Potter , J. Noble , D. Clarke, The Ins and Outs of Objects, Proceedings of the Australian Software Engineering Conference, p.80, November 09-13, 1998
• 50: John C. Reynolds, Syntactic control of interference, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.39-46, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512766]
• 51: Mats Skoglund and Tobias Wrigstad. Alias control with read-only references. In Sixth Conference on Computer Science and Informatics, March 2002.
• 52: Bjarne Stroustrup, The C++ programming language, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 53: J.-P Talpin and P. Jouvelot. Polymorphic type, region, and effect inference. Journal of Functional Programming, 2(3):245--271, July 1992.
• 54: Dirk Theisen. Enhancing encapsulation in OOP: A practical approach. Master's thesis, Institut fur Informatik III, Ramerst. 164, D-53117 Bonn, Universitat Bonn.
• 55: Mads Tofte , Jean-Pierre Talpin, Region-based memory management, Information and Computation, v.132 n.2, p.109-176, Feb. 1, 1997 [doi>10.1006/inco.1996.2613]
• 56: Mark Utting. Reasoning about aliasing. In The Fourth Australasian Refinement Workshop, 1995.
• 57: Joachim van den Berg , Bart Jacobs, The LOOP Compiler for Java and JML, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.299-312, April 02-06, 2001
• 58: Alan Wills. Reasoning about aliasing. In ECOOP Proceedings, 1993.
• 59: Bennett Norton Yates. A type-and-effect system for encapsulating memory in Java. Master's thesis, Department of Computer and Information Science and the Graduate School of the University of Oregon, August 1999.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

General Terms:
Languages, Theory

Keywords:
aliasing, encapsulation, ownership types, type-and-effects systems