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

A garbage-collecting typed assembly language

Published: 16 January 2007 Publication History

Abstract

Typed assembly languages usually support heap allocation safely, but often rely on an external garbage collector to deallocate objects from the heap and prevent unsafe dangling pointers. Even if the external garbage collector is provably correct, verifying the safety of the interaction between TAL programs and garbage collection is nontrivial. This paper introduces a typed assembly language whose type system is expressive enough to type-check a Cheney-queue copying garbage collector, so that ordinary programs and garbage collection can co-exist and interact inside a single typed language. The only built-in types for memory are linear types describing individual memory words, so that TAL programmers can define their own object layouts, method table layouts, heap layouts, and memory management techniques.

References

[1]
Andrew W. Appel, Paul-Andre Mellies, Christopher D. Richards, and Jerome Vouillon. A very modal model of a modern, major, general type system. In Proceedings of the 34th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL), 2007.]]
[2]
L. Birkedal, N. Torp-Smith, and J. Reynolds. Local reasoning about a copying garbage collector. In Symposium on Principles of programming languages, 2004.]]
[3]
Bor-Yuh Evan Chang, Adam Chlipala, and George C. Necula. A framework for certified program analysis and its applications to mobile-code safety. In Conference on Verification, Model Checking, and Abstract Interpretation, 2006.]]
[4]
J. Chen, D. Wu, A. Appel, and H. Fang. A provably sound TAL for back-end optimization, 2003.]]
[5]
Juan Chen and David Tarditi. A simple typed intermediate language for object-oriented languages. In POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 38--49, New York, NY, USA, 2005. ACM Press.]]
[6]
Karl Crary and Joseph C. Vanderwaart. An expressive, scalable type theory for certified code. In Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, pages 191--205. ACM Press, 2002.]]
[7]
Karl Crary and Stephanie Weirich. Flexible type analysis. In International Conference on Functional Programming, pages 233--248, 1999.]]
[8]
Chris Hawblitzel. http://research.microsoft.com/chrishaw/.]]
[9]
Chris Hawblitzel, Heng Huang, Lea Wittie, and Juan Chen. A garbage-collecting typed assembly language (extended version). Technical Report MSR-TR-2006-169, Microsoft Research, November 2006.]]
[10]
Chris Hawblitzel, Edward Wei, Heng Huang, Eric Krupski, and Lea Wittie. Low-level linear memory management. In Workshop on Semantics, Program Analysis, and Computing Environments For Memory Management, 2004.]]
[11]
G. Huet, G. Kahn, and Ch. Paulin-Mohring. The Coq proof assistant - a tutorial, July 1999.]]
[12]
Limin Jia, Frances Spalding, David Walker, and Neal Glew. Certifying compilation for a language with stack allocation. In Logic in Computer Science, 2005, 2005.]]
[13]
Stefan Monnier, Bratin Saha, and Zhong Shao. Principled scavenging. In Proceedings of the ACM SIGPLAN'01 conference on Programming language design and implementation, pages 81--91. ACM Press, 2001.]]
[14]
Stefan Monnier and Zhong Shao. Typed regions. Technical Report YALEU/DCS/TR-1242, Department of Computer Science, Yale University, 2002.]]
[15]
Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From system F to typed assembly language. In ACM Transactions on Programming Languages and Systems (TOPLAS), volume 21, pages 527--568. ACM Press, 1999.]]
[16]
Hiroshi Nakano. A modality for recursion. In Proceedings of the IEEE Symposium on Logic in Computer Science (LICS), 2000.]]
[17]
George C. Necula and Peter Lee. Safe kernel extensions without run-time checking. In 2nd Symposium on Operating Systems Design and Implementation (OSDI'96), October 28--31, 1996. Seattle, WA, pages 229--243, 1996.]]
[18]
Zhaozhong Ni and Zhong Shao. Certified assembly programming with embedded code pointers. In POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 320--333, New York, NY, USA, 2006. ACM Press.]]
[19]
Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002.]]
[20]
Z. Shao, B. Saha, V. Trifonov, and N. Papaspyrou. A type system for certified binaries. In ACM Symposium on Principles of Programming Languages, 2002.]]
[21]
Alex K. Simpson. The proof theory and semantics of intuitionistic modal logic, phd thesis, department of philosophy, university of edinburgh, 1994.]]
[22]
Frederick Smith, David Walker, and Greg Morrisett. Alias types. In In European Symposium on Programming, 2000.]]
[23]
P. L. Wadler. A taste of linear logic. In Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, Gdánsk, New York, NY, 1993. Springer-Verlag.]]
[24]
Philip Wadler. How to declare an imperative. ACM Computing Surveys, 29(3):240--263, 1997.]]
[25]
Daniel C. Wang and Andrew W. Appel. Type-preserving garbage collectors. In Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 166--178. ACM Press, 2001.]]
[26]
Paul R. Wilson. Uniprocessor garbage collection techniques. In Proc. Int. Workshop on Memory Management, number 637, Saint-Malo (France), 1992. Springer-Verlag.]]
[27]
Hongwei Xi and Frank Pfenning. Eliminating array bound checking through dependent types. In Proceedings of the ACM SIGPLAN '98 conference on Programming language design and implementation, pages 249--257. ACM Press, 1998.]]
[28]
Dachuan Yu, Nadeem A. Hamid, and Zhong Shao. Building certified libraries for PCC: Dynamic storage allocation. In Proc. 2003 European Symposium on Programming (ESOP'03), April 2003.]]
[29]
Dengping Zhu and Hongwei Xi. Safe programming with pointers through stateful views. In Practical Aspects of Declarative Languages, 2005.]]

Cited By

View all
  • (2007)Garbage collection for safety critical JavaProceedings of the 5th international workshop on Java technologies for real-time and embedded systems10.1145/1288940.1288953(85-93)Online publication date: 26-Sep-2007
  • (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
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
TLDI '07: Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation
January 2007
86 pages
ISBN:159593393X
DOI:10.1145/1190315
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: 16 January 2007

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. garbage collection
  2. typed assembly language

Qualifiers

  • Article

Conference

TLDI07
Sponsor:

Acceptance Rates

Overall Acceptance Rate 11 of 26 submissions, 42%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)3
  • Downloads (Last 6 weeks)0
Reflects downloads up to 17 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2007)Garbage collection for safety critical JavaProceedings of the 5th international workshop on Java technologies for real-time and embedded systems10.1145/1288940.1288953(85-93)Online publication date: 26-Sep-2007
  • (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)SingularityACM SIGOPS Operating Systems Review10.1145/1243418.124342441:2(37-49)Online publication date: 1-Apr-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

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media