Chris Hawblitzel, Heng Huang, Lea Wittie, and Juan Chen
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.
In ACM Workshop on Types in Language Design and Implementation (TLDI 07)
Publisher Association for Computing Machinery, Inc.
Copyright © 2004 by the Association for Computing Machinery, Inc. Permission to make digital or hard copies of part or all 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, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or email@example.com. The definitive version of this paper can be found at ACM’s Digital Library –http://www.acm.org/dl/.