Home

A Garbage-Collecting Typed Assembly Language

A Garbage-Collecting Typed Assembly Language. Chris Hawblitzel; Heng Huang; Lea Wittie; Juan Chen.

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.

The TAL-GC proofs can be found here.

By Ehud Lamm at 2006-12-03 11:10 | Implementation | Type Theory | other blogs | 7546 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

The extent of checked logic?

They say this effort is similar to ATS, in that it provides an embedded logic as the assembly language. How powerful is the logic and what sort of checking is possible? Can it provide the full type checking that a statically typed language like OCaml provides? In other words, the "compiler" would be like a rewriting engine, which translates the source language into the typed assembly language with the requisite proofs, and the TAL-GC checks the consistency.

By naasking at Mon, 2006-12-04 21:36 | login or register to post comments