Adoption and focus: practical linear types for imperative programming

ABSTRACT

A type system with linearity is useful for checking software protocols andresource management at compile time. Linearity provides powerful reasoning about state changes, but at the price of restrictions on aliasing. The hard division between linear and nonlinear types forces the programmer to make a trade-off between checking a protocol on an object and aliasing the object. Most onerous is the restriction that any type with a linear component must itself be linear. Because of this, checking a protocol on an object imposes aliasing restrictions on any data structure that directly or indirectly points to the object. We propose a new type system that reduces these restrictions with the adoption and focus constructs. Adoption safely allows a programmer to alias objects on which she is checking protocols, and focus allows the reverse. A programmer can alias data structures that point to linear objects and use focus for safe access to those objects. We discuss how we implemented these ideas in the Vault programming language.

REFERENCES

• 1: 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]
• 2: 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]
• 3: 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
• 4: David Gay , Alex Aiken, Memory management with explicit regions, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.313-323, June 17-19, 1998, Montreal, Quebec, Canada
• 5: Fritz Henglein , Henning Makholm , Henning Niss, A direct approach to control-flow sensitive region-based memory management, Proceedings of the 3rd ACM SIGPLAN international conference on Principles and practice of declarative programming, p.175-186, September 05-07, 2001, Florence, Italy [doi>10.1145/773184.773203]
• 6: Samin S. Ishtiaq , Peter W. O'Hearn, BI as an assertion language for mutable data structures, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-26, January 2001, London, United Kingdom
• 7: Viktor Kuncak , Patrick Lam , Martin Rinard, Role analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.17-32, January 16-18, 2002, Portland, Oregon
• 8: K. R. M. Leino and G. Nelson. Data abstraction and information hiding.Technical Report 160, Compaq SRC, nov 2000
• 9: Martin Odersky, Observers for linear types, Symposium proceedings on 4th European symposium on programming, p.390-407, January 1992, Rennes, France
• 10: Conference Record of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, Jan. 1999
• 11: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-118, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292552]
• 12: Sjaak Smetsers , Erik Barendsen , Marko C. J. D. van Eekelen , Marinus J. Plasmeijer, Guaranteeing Safe Destructive Updates Through a Type System with Uniqueness Information for Graphs, Proceedings of the International Workshop on Graph Transformations in Computer Science, p.358-379, January 01, 1993
• 13: Frederick Smith , David Walker , J. Gregory Morrisett, Alias Types, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.366-381, April 02, 2000
• 14: 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
• 15: M. Tofte, L. Birkedal, M. Elsman, N. Hallenberg, T. H. Olesen, P. Sestoft, and P. Bertelsen. Programming with regions in the ml kit (for version 3). Technical Report 98/25, Department of Computer Science, University of Copenhagen, 1998
• 16: Mads Tofte , Jean-Pierre Talpin, Implementation of the typed call-by-value λ-calculus using a stack of regions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.188-201, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177855]
• 17: P. Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, Programming Concepts and Methods. Apr. 1990. IFIP TC 2 Working Conference
• 18: David Walker , J. Gregory Morrisett, Alias Types for Recursive Data Structures, Selected papers from the Third International Workshop on Types in Compilation, p.177-206, September 21, 2000
• 19: D. Walker and K. Watkins. On linear types and regions. Proceedings of the International Conference on Functional Programming (ICFP '01), Sept. 2001

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Memory management (garbage collection)

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques; Pre- and post-conditions

General Terms:
Design, Languages, Reliability

Keywords:
heap aliasing, linear types, region-based memory management