Typed memory management via static capabilities

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Typed memory management via static capabilities

Full text

Pdf (663 KB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 22 , Issue 4 (July 2000) table of contents

Pages: 701 - 771

Year of Publication: 2000

ISSN:0164-0925

Authors

David Walker	Carnegie Mellon Univ., Pittsburgh, PA
Karl Crary	Carnegie Mellon Univ., Pittsburgh, PA
Greg Morrisett	Cornell Univ., Ithaca, NY

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 10, Downloads (12 Months): 78, Citation Count: 35

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/363911.363923 What is a DOI?

ABSTRACT

Region-based memory management is an alternative to standard tracing garbage collection that makes operation such as memory deallocation explicit but verifiably safe. In this article, we present a new compiler intermediate language, called the Capability Language (CL), that supports region-based memory management and enjoys a provably safe type systems. Unlike previous region-based type system, region lifetimes need not be lexically scoped, and yet the language may be checked for safety without complex analyses. Therefore, our type system may be deployed in settings such as extensible operating systems where both the performance and safety of untrusted code is important. The central novelty of the language is the use of static capabilities to specify the permissibility of various operations, such as memory access and deallocation. In order to ensure capabilities are relinquished properly, the type system tracks aliasing information using a form of bounded quantification. Moreover, unlike previous work on region-based type systems, the proof of soundness of our type system is relatively simple, employing only standard syntactic techniques. In order to show how our language may be used in practice, we show how to translate a variant of Tofte and Talpin's high-level type-and-effects system for region-based memory management into our language. When combined with known region inference algorithms, this translation provides a way to compile source-level languages to CL.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Samson Abramsky, Computational interpretations of linear logic, Theoretical Computer Science, v.111 n.1-2, p.3-57, April 12, 1993 [doi>10.1016/0304-3975(93)90181-R]
	2	Alexander Aiken , Manuel Fähndrich , Raph Levien, Better static memory management: improving region-based analysis of higher-order languages, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.174-185, June 18-21, 1995, La Jolla, California, United States
	3	Alpern, B. and Schneider, F. 1987. Recognizing safety and liveness. Distributed Computing 2, 117-126.
	4	Henry G. Baker, Jr., List processing in real time on a serial computer, Communications of the ACM, v.21 n.4, p.280-294, April 1978 [doi>10.1145/359460.359470]
	5	B. N. Bershad , S. Savage , P. Pardyak , E. G. Sirer , M. E. Fiuczynski , D. Becker , C. Chambers , S. Eggers, Extensibility safety and performance in the SPIN operating system, Proceedings of the fifteenth ACM symposium on Operating systems principles, p.267-283, December 03-06, 1995, Copper Mountain, Colorado, United States
	6	Birkedal, L., Rothwell, N., Tofte, M., and Turner, D. N. 1993. The ML Kit (version 1). Tech. Rep. 93/14, Department of Computer Science, University of Copenhagen.
	7	Lars Birkedal , Mads Tofte , Magnus Vejlstrup, From region inference to von Neumann machines via region representation inference, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-183, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237771]
	8	Guy E. Blelloch , John Greiner, A provable time and space efficient implementation of NESL, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.213-225, May 24-26, 1996, Philadelphia, Pennsylvania, United States
	9	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]
	10	Karl Crary , Stephanie Weirich , Greg Morrisett, Intensional polymorphism in type-erasure semantics, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.301-312, September 26-29, 1998, Baltimore, Maryland, United States
	11	Danvy, O. and Filinski, A. 1992. Representing control: a study of the CPS transformation. Mathematical Structures in Computer Science 2, 4 (Dec.), 361-391.
	12	Danvy, O., Dzafic, B., and Pfenning, F. 1999. On proving syntactic properties of CPS programs. In Third International Workshop on Higher-Order Operational Techniques in Semantics, A. Gordon and A. Pitts, Eds. Electronic Notes in Computer Science, vol. 26. Elsevier, Paris, 19-31.
	13	Filinski, A. 1996. Controlling effects. Ph.D. thesis, Carnegie Mellon University, School of Computer Science, Pittsburgh, Pennsylvania.
	14	Michael J. Fischer, Lambda calculus schemata, Proceedings of ACM conference on Proving assertions about programs, p.104-109, January 06-07, 1972, Las Cruces, New Mexico, United States
	15	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
	16	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
	17	David K. Gifford , John M. Lucassen, Integrating functional and imperative programming, Proceedings of the 1986 ACM conference on LISP and functional programming, p.28-38, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319848]
	18	Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
	19	Robert Harper , Mark Lillibridge, Explicit polymorphism and CPS conversion, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.206-219, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158630]
	20	Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199475]
	21	Hawblitzel, C., Chang, C.-C., Czajkowski, G., Hu, D., and von Eicken, T. 1998. Implementing multiple protection domains in Java. In 1998 USENIX Annual Technical Conference. USENIX, New Orleans.
	22	Hawblitzel, C. and von Eicken, T. 1999. Type system support for dynamic revocation. In ACM SIGPLAN workshop on Compiler Support for System Software. ACM Press, Atlanta.
	23	Pierre Jouvelot , David Gifford, Algebraic reconstruction of types and effects, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.303-310, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99623]
	24	Dexter Kozen, Efficient Code Certification, Cornell University, Ithaca, NY, 1998
	25	Y. Lafont, The linear abstract machine, Theoretical Computer Science, v.59 n.1-2, p.157-180, July 1988 [doi>10.1016/0304-3975(88)90100-4]
	26	John Launchbury , Simon L. Peyton Jones, State in Haskell, Lisp and Symbolic Computation, v.8 n.4, p.293-341, Dec. 1995 [doi>10.1007/BF01018827]
	27	Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
	28	Lucassen, J. M. 1987. Types and effects-towards the integration of functional and imperative programming. Ph.D. thesis, MIT Laboratory for Computer Science.
	29	Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
	30	Minamide, Y. 1999. Space-profiling semantics of the call-by-value lambda calculus and the CPS transformation. In Third International Workshop on Higher-Order Operational Techniques in Semantics, A. D. Gordon and A. Pitts, Eds. Electronic Notes in Computer Science, vol. 26. Elsevier, Paris, 103-118.
	31	Eugenio Moggi, Notions of computation and monads, Information and Computation, v.93 n.1, p.55-92, July 1991 [doi>10.1016/0890-5401(91)90052-4]
	32	G. Morrisett , R. Harper, Semantics of memory management for polymorphic languages, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
	33	Morrisett, G., Crary, K., Glew, N., Grossman, D., Samuels, R., Smith, F., Walker, D., Weirich, S., and Zdancewic, S. 2000. Typed Assembly Language for the Intel IA32 architecture. See http://www.cs.cornell.edu/talc for the latest implementation.
	34	Greg Morrisett , Matthias Felleisen , Robert Harper, Abstract models of memory management, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.66-77, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224182]
	35	Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-97, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268954]
	36	Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
	37	George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
	38	George C. Necula , Peter Lee, Safe kernel extensions without run-time checking, Proceedings of the second USENIX symposium on Operating systems design and implementation, p.229-243, October 29-November 01, 1996, Seattle, Washington, United States
	39	George C. Necula , Peter Lee, The design and implementation of a certifying compiler, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.333-344, June 17-19, 1998, Montreal, Quebec, Canada
	40	Simon L. Peyton Jones , Philip Wadler, Imperative functional programming, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.71-84, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158524]
	41	Plotkin, G. D. 1975. Call-by-name, call-by-value, and the lambda calculus. Theoretical Computer Science 1, 125-159.
	42	John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
	43	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]
	44	John C. Reynolds, Syntactic Control of Inference, Part 2, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.704-722, July 11-15, 1989
	45	Amr Sabry , Matthias Felleisen, Reasoning about programs in continuation-passing style, Lisp and Symbolic Computation, v.6 n.3-4, p.289-360, Nov. 1993 [doi>10.1007/BF01019462]
	46	Fred B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security (TISSEC), v.3 n.1, p.30-50, Feb. 2000 [doi>10.1145/353323.353382]
	47	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
	48	Mads Tofte , Lars Birkedal, A region inference algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.4, p.724-767, July 1998 [doi>10.1145/291891.291894]
	49	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]
	50	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]
	51	Wadler, P. 1990. Linear types can change the world! In Programming Concepts and Methods, M. Broy and C. Jones, Eds. North Holland, Sea of Galilee, Israel. IFIP TC 2 Working Conference.
	52	Philip Wadler, A Taste of Linear Logic, Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, p.185-210, August 30-September 03, 1993
	53	Robert Wahbe , Steven Lucco , Thomas E. Anderson , Susan L. Graham, Efficient software-based fault isolation, Proceedings of the fourteenth ACM symposium on Operating systems principles, p.203-216, December 05-08, 1993, Asheville, North Carolina, United States
	54	David Walker, A type system for expressive security policies, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.254-267, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325728]
	55	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
	56	Paul R. Wilson, Uniprocessor Garbage Collection Techniques, Proceedings of the International Workshop on Memory Management, p.1-42, September 17-19, 1992
	57	Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]
	58	Wulf, W. A., Levin, R., and Harbison, S. P. 1981. Hydra/C.mmp: An Experimental Computer System. McGraw-Hill, New York, NY.

CITED BY 35

	Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, ACM SIGPLAN Notices, v.36 n.5, p.59-69, May 2001
	Naoki Kobayashi, Time regions and effects for resource usage analysis, ACM SIGPLAN Notices, v.38 n.3, March 2003
	David Walker , Kevin Watkins, On regions and linear types (extended abstract), ACM SIGPLAN Notices, v.36 n.10, October 2001
	Karl Crary , Joseph C. Vanderwaart, An expressive, scalable type theory for certified code, ACM SIGPLAN Notices, v.37 n.9, p.191-205, September 2002
	Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis, ACM SIGPLAN Notices, v.37 n.1, p.331-342, Jan. 2002
	Michael Hind, Pointer analysis: haven't we solved this problem yet?, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.54-61, June 2001, Snowbird, Utah, United States
	Sophia Drossopoulou , Ferruccio Damiani , Mariangiola Dezani-Ciancaglini , Paola Giannini, More dynamic object reclassification: Fickle∥, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.2, p.153-191, March 2002
	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
	Amal Ahmed , David Walker, The logical approach to stack typing, ACM SIGPLAN Notices, v.38 n.3, March 2003
	Dan Grossman , Greg Morrisett , Trevor Jim , Michael Hicks , Yanling Wang , James Cheney, Region-based memory management in cyclone, ACM SIGPLAN Notices, v.37 n.5, May 2002
	Dan Grossman, Type-safe multithreading in cyclone, ACM SIGPLAN Notices, v.38 n.3, March 2003
	John Tang Boyland , William Retert, Connecting effects and uniqueness with adoption, ACM SIGPLAN Notices, v.40 n.1, p.283-295, January 2005
	Michael Hicks , Greg Morrisett , Dan Grossman , Trevor Jim, Experience with safe manual memory-management in cyclone, Proceedings of the 4th international symposium on Memory management, October 24-25, 2004, Vancouver, BC, Canada
	Mads Tofte , Lars Birkedal , Martin Elsman , Niels Hallenberg, A Retrospective on Region-Based Memory Management, Higher-Order and Symbolic Computation, v.17 n.3, p.245-265, September 2004
	Matthias Neubauer , Peter Thiemann, From sequential programs to multi-tier applications by program transformation, ACM SIGPLAN Notices, v.40 n.1, p.221-232, January 2005
	Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.2, p.264-313, March 2005
	Futoshi Iwama , Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis for a functional language with exceptions, Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 09-10, 2006, Charleston, South Carolina
	Vijay S. Menon , Neal Glew , Brian R. Murphy , Andrew McCreight , Tatiana Shpeisman , Ali-Reza Adl-Tabatabai , Leaf Petersen, A verifiable SSA program representation for aggressive compiler optimization, ACM SIGPLAN Notices, v.41 n.1, p.397-408, January 2006
	Gareth Stoyle , Michael Hicks , Gavin Bierman , Peter Sewell , Iulian Neamtiu, Mutatis mutandis: safe and predictable dynamic software updating, ACM SIGPLAN Notices, v.40 n.1, p.183-194, January 2005
	Yitzhak Mandelbaum , David Walker , Robert Harper, An effective theory of type refinements, ACM SIGPLAN Notices, v.38 n.9, p.213-225, September 2003
	DEREK DREYER, Recursive type generativity, Journal of Functional Programming, v.17 n.4-5, p.433-471, July 2007
	Nadeem Abdul Hamid, Certified memory management for proof-carrying code: a region-based type system and runtime library, Proceedings of the 43rd annual southeast regional conference, March 18-20, 2005, Kennesaw, Georgia
	Nikhil Swamy , Michael Hicks , Greg Morrisett , Dan Grossman , Trevor Jim, Safe manual memory management in cyclone, Science of Computer Programming, v.62 n.2, p.122-144, 1 October 2006
	Karl Crary, Sound and complete elimination of singleton kinds, ACM Transactions on Computational Logic (TOCL), v.8 n.2, p.8-es, April 2007
	Oleg Kiselyov , Chung-chieh Shan, Lightweight Static Capabilities, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.7, p.79-104, June, 2007
	Nadeem Abdul Hamid, Integrating a certified memory management runtime with proof-carrying code, Proceedings of the 2007 ACM symposium on Applied computing, March 11-15, 2007, Seoul, Korea
	Iulian Neamtiu , Michael Hicks , Jeffrey S. Foster , Polyvios Pratikakis, Contextual effects for version-consistent dynamic software updatingalland safe concurrent programming, ACM SIGPLAN Notices, v.43 n.1, January 2008
	Simon Helsen, Bisimilarity for the Region Calculus, Higher-Order and Symbolic Computation, v.17 n.4, p.347-394, December 2004
	Gareth Stoyle , Michael Hicks , Gavin Bierman , Peter Sewell , Iulian Neamtiu, Mutatis Mutandis: Safe and predictable dynamic software updating, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.4, p.22-es, August 2007
	Amal Ahmed , Matthew Fluet , Greg Morrisett, L³: A Linear Language with Locations, Fundamenta Informaticae, v.77 n.4, p.397-449, December 2007
	Peter Sewell , Gareth Stoyle , Michael Hicks , Gavin Bierman , Keith Wansbrough, Dynamic rebinding for marshalling and update, via redex-time and destruct-time reduction, Journal of Functional Programming, v.18 n.4, p.437-502, July 2008
	Oleg Kiselyov , Chung-chieh Shan, Lightweight monadic regions, Proceedings of the first ACM SIGPLAN symposium on Haskell, September 25-25, 2008, Victoria, BC, Canada
	Edgar G. Daylight , Arnout Vandecappelle , Francky Catthoor, The formalism underlying EASYMAP: A precompiler for refinement-based exploration of hierarchical data organizations, Science of Computer Programming, v.72 n.3, p.71-135, August, 2008
	Daniel Marino , Todd Millstein, A generic type-and-effect system, Proceedings of the 4th international workshop on Types in language design and implementation, January 24-24, 2009, Savannah, GA, USA
	Robert Atkey, Parameterised notions of computation, Journal of Functional Programming, v.19 n.3-4, p.335-376, July 2009