Cyclone

Yesterday I went to a talk at Harvard, titled "Implementation and Evaluation of a Safe Runtime in Cyclone", by Matthew Fluet.

In this talk we outline the implementation of a simple Scheme interpreter and a copying garbage collector that manages the memory allocated by the interpreter. The entire system including the garbage collector is implemented in Cyclone, a safe dialect of C, which supports safe and explicit memory management...

Greg Morrisett, one of the designers of Cyclone, was also present and answered some of the more advanced questions about Cyclone itself.

Cyclone is a "safe" version of C, and it uses static analysis to catch memory leaks. The talk focused on how to write a garbage collector such that the implementation would be accepted by Cyclone's (strict) memory leak detection requirements. First I'll explain how memory leak detection is done in Cyclone, and then I'll explain why it's not trivial to implement a garbage collector using the scheme.

Cyclone's memory leak detection is based on regions. There are several different types of region, but the relevant kind for this talk was the "dynamic" kind. The main characteristics of dynamic regions are that you can allocate new objects into them incrementally, but they have to be freed all at once in one big batch. Perfect for a stop-and-copy garbage collector.

Cyclone restricts the operations you can perform on regions so it can guarantee that you don't leak regions, and that you don't dereference data within a region after it has been freed. This static analysis is based on the idea of capabilities (unforgeable, uncopyable unique handles). Briefly, all the data in a Cyclone program is statically tagged with the region it belongs to (the tag is part of the type, so "an integer in region 1" is different than "an integer in region 2"). You can't actually *use* the data in a region unless you present the requisite capability to the compiler (each region has its own capability). This is done syntactically, kind of like this:

present (region_capability) {
    ... data in the region can be accessed here ...
}
... but not here...

Note that I used my own syntax here. The actual syntax used by Cyclone seems less intuitive to me.

The Cyclone compiler makes it impossible to leak regions by making it illegal to let a capability go out of scope. It also prevents you from referencing previously-freed memory by revoking the capability for the region as soon as you free it. It's actually a pretty simple and straightforward scheme, so if it seems confusing it's probably because I've explained it poorly.

The garbage collector that Matthew Fluet implemented uses a simple stop-and-copy scheme. In other words it takes an old heap, traces through it to find memory still in use, copies that the memory to the new heap, and leaves a "forwarding pointer" in the old heap so that the garbage collector can handle cycles correctly.

It's the forwarding pointers that make things difficult. Because all datatypes have an embedded region name which specifies what region they belong to, it makes it difficult to come up with a type name for the forwarding pointers. Matthew had a very amusing slide that illustrated this. You end up with a type like this:

A pointer to a block in the region after this one, which has a pointer to a block in the region after the one after this one, which has a pointer to a block in the region after the one after the one after this one, which has a pointer to a block in the region after the one after the one after the one after this one, which has ...

To get around this, they introduced a new primitive into the Cyclone runtime, which lets you express this kind of recursion. There was some explanation about how they "used an existential to prime the pump", and some other feature which made some of the verbosity in the type signature become implicit... but I didn't really follow that part.

However what I did glean from the discussion was that Cyclone's straightforward memory leak detection algorithm doesn't lead to a small, well-defined interface. Case in point: in order to implement a garbage collector they had to extend the runtime. It was a small function (only 5 lines of code) but nevertheless it was not possible at the user level. In effect, they had to introduce a new proof rule into the type system. That's disturbing to me -- it means the type system is incomplete. And these are smart people, so if it wasn't complete to start with, that probably means it'll never be complete.

What's even more disturbing is that at the end of the talk, Norman Ramsey asked how they would implement a generational garbage collector. And the answer was, "We haven't figured out how to do that yet... it may require dependent types." Eeek! Suddenly I realized at a deep level that advanced type systems are equivalent to mathematical proofs, and that if you start trying to prove too much about such an unpredictable beast as a program, it will resist you with a vengence.

Just imagine trying to explain to a systems programmer that the reason they can't implement a "simple" generational GC scheme is because that would require that the type checker be extended to support dependent types. They'll look at you like you have three heads, and then they'll toss you and your silly little language into /dev/null.

Posted on February 19, 2004 06:42 PM
More languages articles