Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1145/360204.360218acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
Article

Type-preserving garbage collectors

Published: 01 January 2001 Publication History

Abstract

By combining existing type systems with standard type-based compilation techniques, we describe how to write strongly typed programs that include a function that acts as a t racing garbage collector for the program. Since the garbage collector is an explicit function, we do not need to provide a t rusted garbage collector as a runtime service to manage memory.Since our language is strongly typed, the standard type soundness guarantee "Well typed programs do not go wrong" is extended to include the collector. Our type safety guarantee is non-trivial since not only does it guarantee the type safety of the garbage collector, but it guarantees that the collector preservers the type safety of the program being garbage collected. We describe the technique in detail and report performance measurements for a few microbench-marks as well as sketch the proofs of type soundness for our system.

References

[1]
Alexander Aiken, Manuel FAahndrich, and Raph Levien. Better static memory management: Improving regionbased analysis of higher-order languages. In Proceedings of SIGPLAN'95 Conference on Programming Languages Design and Implementation, volume 30 of ACM SIGPLAN Notices, pages 174-185, La Jolla, CA, June 1995. ACM Press.]]
[2]
Andrew W. Appel and Zhong Shao. Empirical and analytic study of stack versus heap cost for languages with closures. Journal of Functional Programming, 6(1):47- 74, January 1996.]]
[3]
Andrew W. Appel and Zhong Shao. Efficent and safefor-space closure conversion. ACM Transactions on Programming Languages and Systems, 22(1):129-161, January 2000.]]
[4]
Henry G. Baker. Lively linear Lisp Look Ma, no garbage. ACM SIGPLAN Notices, 27(9):89-98, August 1992.]]
[5]
Henry G. Baker. The Treadmill, real-time garbage collection without motion sickness. ACM SIGPLAN Notices, 27(3):66-70, March 1992.]]
[6]
Henry G. Baker. The boyer benchmark meets linear logic. Lisp Pointers, 6(4):3-10, October 1993.]]
[7]
Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. Region analysis and the polymorphic lambda calculus. In Proceedings, Fourteenth Annual IEEE Symposium on Logic in Computer Science, pages 88-97, Trento, Italy, 2-5 July 1999. IEEE Computer Society Press.]]
[8]
Hans-Juergen Boehm. Simple garbage-collector safety. In Proceedings of SIGPLAN'96 Conference on Programming Languages Design and Implementation, ACM SIGPLAN Notices, pages 89-98. ACM Press, 1996.]]
[9]
Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Conference Record of the Twenty-sixth Annual ACM Symposium on Principles of Programming Languages, ACM SIGPLAN Notices, pages 262-275. ACM Press, 1999.]]
[10]
Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional polymorphism in type-erasure semantics. In ICFP {15}, pages 301-312.]]
[11]
Amer Diwan, J. Eliot B. Moss, and Richard L. Hudson. Compiler support for garbage collection in a statically typed language. In Proceedings of SIGPLAN'92 Conference on Programming Languages Design and Implementation, volume 27 of ACM SIGPLAN Notices, pages 273-282, San Francisco, CA, June 1992. ACM Press.]]
[12]
David Gay and Alex Aiken. Memory management with explicit regions. In Proceedings of SIGPLAN'98 Conference on Programming Languages Design and Implementation, ACM SIGPLAN Notices, pages 313-323, Montreal, June 1998. ACM Press.]]
[13]
J. Gosling. Java intermediate bytecodes. ACM SIG- PLAN Notices, 30(3):111-118, March 1995.]]
[14]
Robert Harper and Greg Morrisett. Compiling polymorphism using intensional type analysis. In Conference Record of the Twenty-second Annual ACM Symposium on Principles of Programming Languages, ACM SIGPLAN Notices, pages 130-141. ACM Press, January 1995.]]
[15]
Proceedings of Second International Conference on Functional Programming, Baltimore, MA, September 1998.]]
[16]
Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. In Conference Record of the Twenty-third Annual ACM Symposium on Principles of Programming Languages, ACM SIG- PLAN Notices, pages 271-283. ACM Press, 1996.]]
[17]
MLton, a whole program optimizing compiler for Standard ML. http://www.neci.nj.nec.com/PLS/MLton/.]]
[18]
Stefan Monnier, Bratin Saha, and Zhong Shao. Principled scavenging. Technical Report Yale/DCS/1205, Yale University, 2000.]]
[19]
Greg Morrisett, Matthias Felleisen, and Robert Harper. Abstract models of memory management. In Functional Programming and Computer Architecture, San Diego, 1995.]]
[20]
Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. In Conference Record of the Twentyth Annual ACM Symposium on Principles of Programming Languages, ACM SIGPLAN Notices, pages 85-97. ACM Press, 1998.]]
[21]
George Necula. Proof-carrying code. In Conference Record of the Twenty-fourth Annual ACM Symposium on Principles of Programming Languages, ACM SIG- PLAN Notices, pages 106-119. ACM Press, 1997.]]
[22]
H. Schorr and W. Waite. An efficient machine independent procedure for garbage collection in various list structures. Communications of the ACM, 10(8):501- 506, August 1967.]]
[23]
Jerrey Mark Siskind. Flow-directed lightweight closure conversion. Technical Report TR99-190R, NEC Reseaarch Institute, Inc., December 1999. in preparation.]]
[24]
Frederick Smith, David Walker, and Greg Morrisett. Alias types. In Gert Smolka, editor, Ninth European Symposium on Programming, volume 1782 of Lecture Notes in Computer Science, pages 366-381, Berlin, April 2000. Springer-Verlag.]]
[25]
Jonathan Sobel and Daniel P. Friedman. Recycling continuations. In ICFP {15}, pages 251-270.]]
[26]
Mads Tofte, Lars Birkedal, Martin Elsman, Neils Hallenberg, Tommy Hejfeld Olesen, Peter Sestoft, and Peter Bertelsen. Programming with reigons in the ML Kit (for version 3). Technical Report DIKU-TR-98/25, University of Copenhagen, December 1998.]]
[27]
Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value calculus using a stack of regions. In Conference Record of the Twenty-first Annual ACM Symposium on Principles of Programming Languages, ACM SIGPLAN Notices, pages 188-201. ACM Press, January 1994.]]
[28]
Andrew Tolmach and Dino P. Oliva. From ML to Ada: Strongly-typed language interoperability via source translation. Journal of Functional Programming, 8(4):367-412, July 1998.]]
[29]
G. Veillon. Transformations de programmes recursifs. R.A.I.R.O. Informatique, 10(9):7-20, September 1976.]]
[30]
Philip Wadler and Stephen Blott. How to make adhoc polymorphism less ad-hoc. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, ACM SIGPLAN Notices, pages 60-76. ACM Press, January 1989.]]
[31]
David Walker and Greg Morrisett. Alias types for recursive data structures (extended version). Technical Report TR2000-1787, Cornell University, March 2000.]]
[32]
Daniel C. Wang and Andrew W. Appel. Typepreserving garbage collectors (extend version). Technical Report TR-624-00, Princeton University, 2000.]]
[33]
Thomas Wang. The MM garbage collector for C++. Master's thesis, California State Polytechnic University, October 1989.]]

Cited By

View all

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2001
304 pages
ISBN:1581133367
DOI:10.1145/360204
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2001

Permissions

Request permissions for this article.

Check for updates

Qualifiers

  • Article

Conference

POPL01

Acceptance Rates

POPL '01 Paper Acceptance Rate 24 of 126 submissions, 19%;
Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)6
  • Downloads (Last 6 weeks)3
Reflects downloads up to 24 Nov 2024

Other Metrics

Citations

Cited By

View all
  • (2023)Defunctionalization with Dependent TypesProceedings of the ACM on Programming Languages10.1145/35912417:PLDI(516-538)Online publication date: 6-Jun-2023
  • (2010)Automated Verification of Practical Garbage CollectorsLogical Methods in Computer Science10.2168/LMCS-6(3:6)20106:3Online publication date: 18-Aug-2010
  • (2009)Automated verification of practical garbage collectorsACM SIGPLAN Notices10.1145/1594834.148093544:1(441-453)Online publication date: 21-Jan-2009
  • (2009)Automated verification of practical garbage collectorsProceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1480881.1480935(441-453)Online publication date: 21-Jan-2009
  • (2008)Local reasoning about a copying garbage collectorACM Transactions on Programming Languages and Systems10.1145/1377492.137749930:4(1-58)Online publication date: 1-Aug-2008
  • (2007)A general framework for certifying garbage collectors and their mutatorsACM SIGPLAN Notices10.1145/1273442.125078842:6(468-479)Online publication date: 10-Jun-2007
  • (2007)A general framework for certifying garbage collectors and their mutatorsProceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/1250734.1250788(468-479)Online publication date: 15-Jun-2007
  • (2007)A garbage-collecting typed assembly languageProceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation10.1145/1190315.1190323(41-52)Online publication date: 16-Jan-2007
  • (2007)Foundational Typed Assembly Language with Certified Garbage CollectionProceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering10.1109/TASE.2007.28(326-338)Online publication date: 6-Jun-2007
  • (2007)Garbage collector verification for proof-carrying codeJournal of Computer Science and Technology10.1007/s11390-007-9049-z22:3(426-437)Online publication date: 1-May-2007
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media