Region-based memory management in cyclone

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Region-based memory management in cyclone

Full text

Pdf (249 KB)

Source

Conference on Programming Language Design and Implementation archive
Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation table of contents

Berlin, Germany

SESSION: Language Design & Implementation Issues table of contents

Pages: 282 - 293

Year of Publication: 2002

ISBN:1-58113-463-0

Also published in ...

Authors

Dan Grossman	Cornell University, Ithaca, NY
Greg Morrisett	Cornell University, Ithaca, NY
Trevor Jim	AT&T Labs Research, Florham Park, NJ
Michael Hicks	Cornell University, Ithaca, NY
Yanling Wang	Cornell University, Ithaca, NY
James Cheney	Cornell University, Ithaca, NY

Sponsor

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 13, Downloads (12 Months): 80, Citation Count: 73

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/512529.512563 What is a DOI?

ABSTRACT

Cyclone is a type-safe programming language derived from C. The primary design goal of Cyclone is to let programmers control data representation and memory management without sacrificing type-safety. In this paper, we focus on the region-based memory management of Cyclone and its static typing discipline. The design incorporates several advancements, including support for region subtyping and a coherent integration with stack allocation and a garbage collector. To support separate compilation, Cyclone requires programmers to write some explicit region annotations, but a combination of default annotations, local type inference, and a novel treatment of region effects reduces this burden. As a result, we integrate C idioms in a region-based framework. In our experience, porting legacy C to Cyclone has required altering about 8% of the code; of the changes, only 6% (of the 8%) were region annotations.

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	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
	2	Todd M. Austin , Scott E. Breach , Gurindar S. Sohi, Efficient detection of all pointer and array access errors, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.290-301, June 20-24, 1994, Orlando, Florida, United States
	3	Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
	4	Hans-Juergen Boehm , Mark Weiser, Garbage collection in an uncooperative environment, Software—Practice & Experience, v.18 n.9, p.807-820, September 1988 [doi>10.1002/spe.4380180902]
	5	Kim B. Bruce , Luca Cardelli , Benjamin C. Pierce, Comparing object encodings, Information and Computation, v.155 n.1-2, p.108-133, Nov./Dec. 1999 [doi>10.1006/inco.1999.2829]
	6	Cyclone user's manual. Technical Report 2001-1855, Department of Computer Science, Cornell University, Nov. 2001. Current version at http://www.cs.cornell.edu/projects/cyclone/
	7	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
	8	T. Dowd, F. Henderson, and P. Ross. Compiling Mercury to the .NET common language runtime. In N. Benton and A. Kennedy, editors, BABEL'01: First International Workshop on Multi-Language Infrastructure and Interoperability, volume 59.1 of Electronic Notes in Theoretical Computer Science, Florence, Italy, Sept. 2001
	9	D. Evans. LCLint user's guide. http://lclint.cs.virginia.edu/guide/
	10	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
	11	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
	12	David Gay , Alex Aiken, Language support for regions, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.70-80, June 2001, Snowbird, Utah, United States
	13	Andrew D. Gordon , Don Syme, Typing a multi-language intermediate code, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.248-260, January 2001, London, United Kingdom
	14	Dan Grossman, Existential Types for Imperative Languages, Proceedings of the 11th European Symposium on Programming Languages and Systems, p.21-35, April 08-12, 2002
	15	Dan Grossman , Greg Morrisett , Trevor Jim , Mike Hicks , Yanling Wang , James Cheney, Formal Type Soundness for Cyclone''s Region System, Cornell University, Ithaca, NY, 2001
	16	Niels Hallenberg , Martin Elsman , Mads Tofte, Combining region inference and garbage collection, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
	17	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]
	18	R. Jain. The Art of Computer Systems Performance Analysis. Wiley, 1991
	19	Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , Yanling Wang, Cyclone: A Safe Dialect of C, Proceedings of the General Track: 2002 USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
	20	G. McGary. Bounds checking projects. http://www.gnu.org/software/gcc/projects/bp/main.html
	21	Yasuhiko Minamide , Greg Morrisett , Robert Harper, Typed closure conversion, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.271-283, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237791]
	22	John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
	23	Stefan Monnier , Bratin Saha , Zhong Shao, Principled scavenging, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.81-91, June 2001, Snowbird, Utah, United States
	24	J. Gregory Morrisett , Karl Crary , Neal Glew , David Walker, Stack-Based Typed Assembly Language, Proceedings of the Second International Workshop on Types in Compilation, p.28-52, March 25-27, 1998
	25	George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
	26	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]
	27	M. Tofte, L. Birkedal, M. Elsman, N. Hallenberg, T. H. Olesen, and P. Sestoft. Programming with regions in the ML Kit (for version 4). Technical report, IT University of Copenhagen, Sept. 2001
	28	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]
	29	David Walker , Karl Crary , Greg Morrisett, Typed memory management via static capabilities, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.701-771, July 2000 [doi>10.1145/363911.363923]
	30	David Walker , Kevin Watkins, On regions and linear types (extended abstract), Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy
	31	Daniel C. Wang , Andrew W. Appel, Type-preserving garbage collectors, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.166-178, January 2001, London, United Kingdom
	32	Hongwei Xi, Imperative Programming with Dependent Types, Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, p.375, June 26-29, 2000
	33	Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]

CITED BY 73

	Niels Hallenberg , Martin Elsman , Mads Tofte, Combining region inference and garbage collection, ACM SIGPLAN Notices, v.37 n.5, May 2002
	Amal Ahmed , David Walker, The logical approach to stack typing, ACM SIGPLAN Notices, v.38 n.3, March 2003
	Sanjeev Kumar , Kai Li, Dynamic memory management for programmable devices, ACM SIGPLAN Notices, v.38 n.2 supplement, February 2003
	Dave Clarke , Sophia Drossopoulou, Ownership, encapsulation and the disjointness of type and effect, ACM SIGPLAN Notices, v.37 n.11, November 2002
	David L. Heine , Monica S. Lam, A practical flow-sensitive and context-sensitive C and C++ memory leak detector, ACM SIGPLAN Notices, v.38 n.5, May 2003
	Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, ACM SIGPLAN Notices, v.37 n.11, November 2002
	Chandrasekhar Boyapati , Barbara Liskov , Liuba Shrira, Ownership types for object encapsulation, ACM SIGPLAN Notices, v.38 n.1, p.213-223, January 2003
	Dinakar Dhurjati , Sumant Kowshik , Vikram Adve , Chris Lattner, Memory safety without runtime checks or garbage collection, ACM SIGPLAN Notices, v.38 n.7, July 2003
	Greg Morrisett, Analysis issues for cyclone, ACM SIGSOFT Software Engineering Notes, v.28 n.1, p.26-26, January 2003
	Chandrasekhar Boyapati , Alexandru Salcianu , William Beebee, Jr. , Martin Rinard, Ownership types for safe region-based memory management in real-time Java, ACM SIGPLAN Notices, v.38 n.5, May 2003
	Ovidiu Gheorghioiu , Alexandru Salcianu , Martin Rinard, Interprocedural compatibility analysis for static object preallocation, ACM SIGPLAN Notices, v.38 n.1, p.273-284, January 2003
	Dan Grossman, Type-safe multithreading in cyclone, ACM SIGPLAN Notices, v.38 n.3, March 2003
	Wei-Ngan Chin , Florin Craciun , Shengchao Qin , Martin Rinard, Region inference for an object-oriented language, ACM SIGPLAN Notices, v.39 n.6, May 2004
	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
	Michael F. Ringenburg , Dan Grossman, Types for describing coordinated data structures, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.25-36, January 10-10, 2005, Long Beach, California, USA
	Oukseh Lee , Kwangkeun Yi, Experiments on the effectiveness of an automatic insertion of memory reuses into ML-like programs, Proceedings of the 4th international symposium on Memory management, October 24-25, 2004, Vancouver, BC, Canada
	Jonathan Aldrich , Valentin Kostadinov , Craig Chambers, Alias annotations for program understanding, ACM SIGPLAN Notices, v.37 n.11, November 2002
	Emery D. Berger , Benjamin G. Zorn , Kathryn S. McKinley, Reconsidering custom memory allocation, ACM SIGPLAN Notices, v.37 n.11, November 2002
	Sigmund Cherem , Radu Rugina, Region analysis and transformation for Java programs, Proceedings of the 4th international symposium on Memory management, October 24-25, 2004, Vancouver, BC, Canada
	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
	Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.2, p.264-313, March 2005
	Matthew Fluet , Greg Morrisett, Monadic regions, ACM SIGPLAN Notices, v.39 n.9, September 2004
	Dinakar Dhurjati , Sumant Kowshik , Vikram Adve , Chris Lattner, Memory safety without garbage collection for embedded applications, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.1, p.73-111, February 2005
	Radu Rugina , Martin C. Rinard, Symbolic bounds analysis of pointers, array indices, and accessed memory regions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.2, p.185-235, March 2005
	Tachio Terauchi , Alex Aiken, Witnessing side-effects, ACM SIGPLAN Notices, v.40 n.9, September 2005
	David Koes , Mihai Budiu , Girish Venkataramani, Programmer specified pointer independence, Proceedings of the 2004 workshop on Memory system performance, June 08-08, 2004, Washington, D.C.
	Martin Berger , Kohei Honda , Nobuko Yoshida, A logical analysis of aliasing in imperative higher-order functions, ACM SIGPLAN Notices, v.40 n.9, September 2005
	Brian Chin , Shane Markstrum , Todd Millstein, Semantic type qualifiers, ACM SIGPLAN Notices, v.40 n.6, June 2005
	Matthew Hertz , Emery D. Berger, Quantifying the performance of garbage collection vs. explicit memory management, ACM SIGPLAN Notices, v.40 n.10, October 2005
	Oukseh Lee , Hongseok Yang , Kwangkeun Yi, Static insertion of safe and effective memory reuse commands into ML-like programs, Science of Computer Programming, v.58 n.1-2, p.141-178, October 2005
	Chris Lattner , Vikram Adve, Automatic pool allocation: improving performance by controlling data structure layout in the heap, ACM SIGPLAN Notices, v.40 n.6, June 2005
	Matthew Simpson , Bhuvan Middha , Rajeev Barua, Segment protection for embedded systems using run-time checks, Proceedings of the 2005 international conference on Compilers, architectures and synthesis for embedded systems, September 24-27, 2005, San Francisco, California, USA
	Dinakar Dhurjati , Sumant Kowshik , Vikram Adve, SAFECode: enforcing alias analysis for weakly typed languages, ACM SIGPLAN Notices, v.41 n.6, June 2006
	Parveen Patel , Andrew Whitaker , David Wetherall , Jay Lepreau , Tim Stack, Upgrading transport protocols using untrusted mobile code, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
	Dan Grossman, Quantified types in an imperative language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.3, p.429-475, May 2006
	Daniel Spoonhower , Joshua Auerbach , David F. Bacon , Perry Cheng , David Grove, Eventrons: a safe programming construct for high-frequency hard real-time applications, ACM SIGPLAN Notices, v.41 n.6, June 2006
	Sumant Kowshik , Dinakar Dhurjati , Vikram Adve, Ensuring code safety without runtime checks for real-time control systems, Proceedings of the 2002 international conference on Compilers, architecture, and synthesis for embedded systems, October 08-11, 2002, Grenoble, France
	Yitzhak Mandelbaum , David Walker , Robert Harper, An effective theory of type refinements, ACM SIGPLAN Notices, v.38 n.9, p.213-225, September 2003
	MARTIN BERGER , KOHEI HONDA , NOBUKO YOSHIDA, A logical analysis of aliasing in imperative higher-order functions, Journal of Functional Programming, v.17 n.4-5, p.473-546, July 2007
	Chris Lattner , Vikram Adve, LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation, Proceedings of the international symposium on Code generation and optimization: feedback-directed and runtime optimization, p.75, March 20-24, 2004, Palo Alto, California
	Sigmund Cherem , Radu Rugina, Compile-time deallocation of individual objects, Proceedings of the 2006 international symposium on Memory management, June 10-11, 2006, Ottawa, Ontario, Canada
	Alex Potanin , James Noble , Dave Clarke , Robert Biddle, Generic ownership for generic Java, ACM SIGPLAN Notices, v.41 n.10, October 2006
	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
	Emery D. Berger , Benjamin G. Zorn, DieHard: probabilistic memory safety for unsafe languages, ACM SIGPLAN Notices, v.41 n.6, June 2006
	Polyvios Pratikakis , Jeffrey S. Foster , Michael Hicks, LOCKSMITH: context-sensitive correlation analysis for race detection, ACM SIGPLAN Notices, v.41 n.6, June 2006
	David L. Heine , Monica S. Lam, Static detection of leaks in polymorphic containers, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
	Jeffrey S. Foster , Robert Johnson , John Kodumal , Alex Aiken, Flow-insensitive type qualifiers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.6, p.1035-1087, November 2006
	A. M. Webb , R. Mansell , J. W. Knight , S. J. Greenspan , D. B. Emmes, Practical software reuse for IBM System z I/O subsystems, IBM Journal of Research and Development, v.51 n.1/2, p.229-243, January 2007
	Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , Yanling Wang, Cyclone: A Safe Dialect of C, Proceedings of the General Track: 2002 USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
	Yutaka Oiwa, Implementation of the memory-safe full ANSI-C compiler, ACM SIGPLAN Notices, v.44 n.6, June 2009
	Manuel Fahndrich , Songtao Xia, Establishing object invariants with delayed types, ACM SIGPLAN Notices, v.42 n.10, October 2007
	Tachio Terauchi , Alex Aiken, Witnessing side effects, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.3, p.1-42, May 2008
	Matthew Fluet , Greg Morrisett, Monadic regions, Journal of Functional Programming, v.16 n.4-5, p.485-545, July 2006
	Feng Qin , Cheng Wang , Zhenmin Li , Ho-seop Kim , Yuanyuan Zhou , Youfeng Wu, LIFT: A Low-Overhead Practical Information Flow Tracking System for Detecting Security Attacks, Proceedings of the 39th Annual IEEE/ACM International Symposium on Microarchitecture, p.135-148, December 09-13, 2006
	Simon Helsen, Bisimilarity for the Region Calculus, Higher-Order and Symbolic Computation, v.17 n.4, p.347-394, December 2004
	Chris Andreae , Yvonne Coady , Celina Gibbs , James Noble , Jan Vitek , Tian Zhao, Scoped types and aspects for real-time Java memory management, Real-Time Systems, v.37 n.1, p.1-44, October 2007
	Kevin Marquet , Gilles Grimaud, A DSL approach for object memory management of small devices, Proceedings of the 4th workshop on Programming languages and operating systems, October 18-18, 2007, Stevenson, Washington
	Xi Wang , Zhilei Xu , Xuezheng Liu , Zhenyu Guo , Xiaoge Wang , Zheng Zhang, Conditional correlation analysis for safe region-based memory management, ACM SIGPLAN Notices, v.43 n.6, June 2008
	Matthew A. Hammer , Umut A. Acar, Memory management for self-adjusting computation, Proceedings of the 7th international symposium on Memory management, June 07-08, 2008, Tucson, AZ, USA
	Marius Nita , Dan Grossman , Craig Chambers, A theory of platform-dependent low-level software, ACM SIGPLAN Notices, v.43 n.1, January 2008
	John Criswell , Andrew Lenharth , Dinakar Dhurjati , Vikram Adve, Secure virtual architecture: a safe execution environment for commodity operating systems, ACM SIGOPS Operating Systems Review, v.41 n.6, December 2007
	Dan Grossman, The transactional memory / garbage collection analogy, ACM SIGPLAN Notices, v.42 n.10, October 2007
	Kevin Marquet , Gilles Grimaud, A DSL approach for object memory management of small devices, Proceedings of the 5th international symposium on Principles and practice of programming in Java, September 05-07, 2007, Lisboa, Portugal
	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
	Joe Devietti , Colin Blundell , Milo M. K. Martin , Steve Zdancewic, Hardbound: architectural support for spatial safety of the C programming language, ACM SIGARCH Computer Architecture News, v.36 n.1, March 2008
	Tian Zhao , Jason Baker , James Hunt , James Noble , Jan Vitek, Implicit ownership types for memory management, Science of Computer Programming, v.71 n.3, p.213-241, May, 2008
	Michael Roberson , Melanie Harries , Paul T. Darga , Chandrasekhar Boyapati, Efficient software model checking of soundness of type systems, ACM SIGPLAN Notices, v.43 n.10, September 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
	Santosh Nagarakatte , Jianzhou Zhao , Milo M.K. Martin , Steve Zdancewic, SoftBound: highly compatible and complete spatial memory safety for c, ACM SIGPLAN Notices, v.44 n.6, June 2009
	Hiroshi Inoue , Hideaki Komatsu , Toshio Nakatani, A study of memory management for web-based applications on multicore processors, ACM SIGPLAN Notices, v.44 n.6, June 2009
	Syrine Tlili , Mourad Debbabi, Interprocedural and Flow-Sensitive Type Analysis for Memory and Type Safety of C Code, Journal of Automated Reasoning, v.42 n.2-4, p.265-300, April 2009
	Tobias Wrigstad , Patrick Eugster , John Field , Nate Nystrom , Jan Vitek, Software hardening: a research agenda, Proceedings for the 1st workshop on Script to Program Evolution, p.58-70, July 06-06, 2009, Genova, Italy