A Larch Specification of Copying
Author: Scott Nettles
Appears as CMU-CS-92-219.
The full text of this paper is here (in
More Larch-related information
is also available.
Garbage collection (GC) is an important part of many language
implementations. One of the most important garbage collection techniques is
copying GC. This paper consists of an informal but abstract description of
copying collection, a formal specification of copying collection written in
the Larch Shared Language and the Larch/C Interface Language, a simple
implementation of a copying collector written in C, an informal proof that
the implementation satisfies the specification, and a discussion of how the
specification applies to other types of copying GC such as generational
copying collectors. Limited familiarity with copying GC or Larch is needed
to read the specification.