Provably Correct Garbage Collection

25 10 2007

Working towards my honors thesis, my partners and I have read several interesting papers on using type systems to prove correctness (safety) of garbage collection implementations:

  • Type-Preserving Garbage Collectors: In this paper, Wang and Appel present a way of writing garbage collectors in the language being collected, and relying on a statically checked type system to prove safety of their collector. They implement a copying collector as a function written in the ML-like language they are collecting, basically by parameterizing all types by memory regions. Each data type and language function are parametrized over a single region as a type. The garbage collection routines are a basic collector plus per-datatype collector routines parameterized over a from-space and a to-space. Each copy function deep-copies a structure in the from-space, and returns a copy located in the to-space. They address pointer sharing by providing an implementation with forwarding pointers (for which they perform an odd version of subtyping to guarantee the user program can’t modify the forwarding pointers in objects, since the collector is being written in the language being collected). To guarantee that the collector returns no pointers to data in the from-space, they introduce a language construct ‘only’ which takes one or more regions and a body, and executes the body with only the specified regions in scope. The problem with this is that if you forget to use the object, you could actually return the original The paper is fairly well-written, and the work is presented in a series of progressively more complete garbage collector functions. A fair amount of time is spent addressing particulars of their implementation, because they make a number of simplifying assumptions. The language supported is first-order only, and is written in CPS with closures converted to datastructures. Also presented are performance results, which are interesting, but largely inconclusive because the system they present is intended only to show that it is possible to write a safe garbage collector, and not meant to be a practical system. Many optimizations are mentioned throughout the paper as future work.
  • Implementation and Performance Evaluation of a Safe Runtime System in Cyclone: This paper by Fluet and Wang aims to show that a similar approach to that above can actually be done with reasonable performance. They implement a Scheme interpreter in Cyclone (a safe dialect of C). They also build a copying collector, using Cyclone’s region primitives to do so. The approach is relatively straightforward (and largely similar to the approach above) with one exception. Instead of a safe upcast with a construct which prevents later downcasts, they use linear types (unique pointers) along with some under-specified functions to create a sequence of region types, to support forwarding pointers. They compare their interpreter running some standard Scheme benchmarks to a couple others. Their interpreter running their garbage collector actually slightly outperforms their interpreter using the standard Cyclone conservative collector – consistently. That is fairly impressive, and shows the overhead for safe collection alone is not a significant bottleneck. Comparisons to MzScheme however are not so great – with the exception of the continuation-based benchmark, MzScheme far outperforms their implementation, by a factor of 2 to 3. And this was done in 2004, before MzScheme had a JIT compiler. This may be a result of the structure of their interpreter; it is a very basic interpreter, which performs a predefined number of steps on an abstract machine structure, checks to see if a collection is necessary, and repeats. They perform a comparison however of the total amount of unsafe code in each implementation, and come in at about 1/6th the amount of unsafe code as the next ‘cleanest’ implementation. Most of this apparently is from a highly optimized version of malloc() used to implement the region primitives.

Both papers write their main programs in slighly odd ways – the Wang/Appel paper does CPS and closure conversion to make stacks and environments safely traversable, and the Fluet/Wang paper sort of cheats by writing a straight interpreter in a separate language. Not to degrade the latter – they still write a garbage collector which is (itself) free of unsafe code, which wonderful. But the constructions as state machines and the CPS and closure conversions definitely hurt performance. They’re necessary, however, in order to safely collect stacks and environments.  My thesis adviser told my partners and me that he may be aware of a way to walk these structures without the efficiency loss of the explicit structures used in these papers.  So next on the block: Continuations from Generalized Stack Inspection.  That, and figuring out just how the two mysteriously underspecified primitives in the Cyclone paper really work (time to read the corresponding technical report), and contemplate the problems of forgetting to use the ‘only’ construct in the first paper.

Advertisements




Monads! (and Why Monad Tutorials Are All Awful)

26 07 2007

If you have an affinity for programming language theory (as I do), and wander around the internet searching for topics of interest, eventually you will run into references to monads. They’re neither trivial, nor as complex as the dearth of proper explanations of them might suggest.

In a nutshell, they are the PLT manifestation of a concept from category theory, and abstract away propagation of results and side effects, without actually performing side effects or leaving a pure-functional paradigm. Any attempt at description beyond that point tends to either

  • a) get terribly botched*, or
  • b) turn into a real category theory explanation, which most people don’t have the background to understand easily

and for those reasons I will refrain from attempting further explanation myself. I don’t have confidence in my own ability to explain in a non-interactive medium, and I certainly don’t have the mathematics background to formalize it.

The internet is littered with tutorials and explanations “in laymen’s terms” of what monads are, what they are for, why we care, etc. Every such tutorial I have started (at least a dozen, probably several more – all highly recommended) has either bored me to tears, struck me as completely inane, or simply confused me.

I had decided that I was simply going to have to learn abstract algebra and category theory in order to really get a handle on what they were, until a wonderful post appeared on LtU, linking to one of the earlier papers on monads. The paper, by Philip Wadler, gives not only a clear explanation of what a monad is, but also provides a strong motivation for looking for monads, an approachable description of how they are derived from a practical point of view for use in a type system, and a number of useful, nontrivial examples. Probably one of the most well-written academic papers I’ve read. You should be familiar with an ML-style type system and notation to understand the examples. Or you need be be good at picking up such things on the fly.

Monads for Functional Programming. Enjoy.


* The canonical example of a monad is for some reason the Maybe monad, though I don’t know why – it’s certainly a monad, but it’s actually not the most intuitive first example. Most of the monad explanations I found online immediately launch into using Maybe as an example of why monads aren’t hard. They’re not, but the example is usually provided far too early, without enough background, motivation, or explanation, making the reader simply feel like he or she is missing some greater complexity (which is true) which was already explained (which usually is not the case). Wadler’s example of a simple interpreter is much clearer.